(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "ASM/BitVectorTrie.ma".

let rec map (A : Type[0]) (B : Type[0]) (f : A → B) (n : nat) 
(t : BitVectorTrie A n) on t : BitVectorTrie B n ≝ 
match t with
[Leaf a ⇒ Leaf ? (f a)
|Node n1 t1 t2 ⇒ Node … n1 (map A B f n1 t1) (map A B f n1 t2)
|Stub n1 ⇒ Stub … n1
].

lemma map_ext : ∀A,B : Type[0]. ∀n : nat. ∀t: BitVectorTrie A n.
∀f,g : A→B. (∀a.f a =g a) → map A B f n t = map A B g n t.
#A #B #n #t elim t 
[#x #f #g #H normalize >(H x) %
|#n1 #l #r #Hl #Hr #f #g #H normalize >(Hl f g H) >(Hr f g H) %
|#n1 #f #g #H %
]
qed.


lemma insert_map: ∀ A,B : Type[0].∀ n: nat.∀t : BitVectorTrie A n.
∀f : A → B.∀a,b.
map A B f n (insert A n b a t) = insert B n b (f a) (map A B f n t).
#A #B #n #t elim t -n
[  #x #f #a #b >(BitVector_O b) -b %
| #n #l #r #IHl #IHr #f #a #b
  cases (BitVector_Sn … b) * * #tl #EQ >EQ -b normalize
  [ >IHr | >IHl ] %
| #n #f #a * -n [ % ]
  #n #hd #tl change with (map ???? (prepare_trie_for_insertion ????) = prepare_trie_for_insertion ????)
  elim (hd:::tl) [%] #n' * #tl' #Htl' normalize @eq_f2 try @Htl' %
]
qed.

lemma lookup_map :  ∀ A,B : Type[0].∀ n: nat.∀t : BitVectorTrie A n.
∀f : A → B.∀a,b. lookup B n b (map A B f n t) (f a) = f (lookup A n b t a).
#A #B #n #t elim t
[ #a #f #a1 #b >(BitVector_O b) %
| #n1 #l #r #Hl #Hr #f #a #b cases (BitVector_Sn … b) * * #tl #EQ >EQ 
  normalize [@Hr|@Hl]
| #n1 #f #a * [%] #n2 #hd #tl %
]
qed.