*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Lemma: Library/RBT.map-of-alist-of*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Mon, 27 Jul 2009 19:12:45 +0200*User-agent*: Thunderbird 2.0.0.22 (X11/20090605)

Hi all, in the current distribution, the lemma "Library/RBT.map-of-alist-of" is not shown, but marked with an "oops". The whole development of folding an RB-tree is marked with "text {* The following is still incomplete... *}". In case no one has already proven this lemma, and someone is interested in a proof, here is one. Regards, Peter

theory RBT_add imports RBT begin (* The next two lemmas are in my standard simpset, however I made them explicit for this proof: *) lemma map_add_dom_app_simps: "\<lbrakk> m\<in>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m" "\<lbrakk> m\<notin>dom l1 \<rbrakk> \<Longrightarrow> (l1++l2) m = l2 m" "\<lbrakk> m\<notin>dom l2 \<rbrakk> \<Longrightarrow> (l1++l2) m = l1 m" by (auto simp add: map_add_def split: option.split_asm) lemma map_add_upd2: "m\<notin>dom e2 \<Longrightarrow> e1(m \<mapsto> u1) ++ e2 = (e1 ++ e2)(m \<mapsto> u1)" apply (unfold map_add_def) apply (rule ext) apply (auto split: option.split) done lemma map_of_alist_of_aux: "st (Tr c t1 k v t2) \<Longrightarrow> RBT.map_of (Tr c t1 k v t2) = RBT.map_of t2 ++ [k\<mapsto>v] ++ RBT.map_of t1" proof (rule ext) fix x assume ST: "st (Tr c t1 k v t2)" let ?thesis = "RBT.map_of (Tr c t1 k v t2) x = (RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1) x" have DOM_T1: "!!k'. k'\<in>dom (RBT.map_of t1) \<Longrightarrow> k>k'" proof - fix k' from ST have "t1 |\<guillemotleft> k" by simp with tlt_prop have "\<forall>k'\<in>keys t1. k>k'" by auto moreover assume "k'\<in>dom (RBT.map_of t1)" ultimately show "k>k'" using RBT.mapof_keys ST by auto qed have DOM_T2: "!!k'. k'\<in>dom (RBT.map_of t2) \<Longrightarrow> k<k'" proof - fix k' from ST have "k \<guillemotleft>| t2" by simp with tgt_prop have "\<forall>k'\<in>keys t2. k<k'" by auto moreover assume "k'\<in>dom (RBT.map_of t2)" ultimately show "k<k'" using RBT.mapof_keys ST by auto qed { assume C: "x<k" hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t1 x" by simp moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp moreover have "x\<notin>dom (RBT.map_of t2)" proof assume "x\<in>dom (RBT.map_of t2)" with DOM_T2 have "k<x" by blast with C show False by simp qed ultimately have ?thesis by (simp add: map_add_upd2 map_add_dom_app_simps) } moreover { assume [simp]: "x=k" hence "RBT.map_of (Tr c t1 k v t2) x = [k \<mapsto> v] x" by simp moreover have "x\<notin>dom (RBT.map_of t1)" proof assume "x\<in>dom (RBT.map_of t1)" with DOM_T1 have "k>x" by blast thus False by simp qed ultimately have ?thesis by (simp add: map_add_upd2 map_add_dom_app_simps) } moreover { assume C: "x>k" hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t2 x" by (simp add: less_not_sym[of k x]) moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp moreover have "x\<notin>dom (RBT.map_of t1)" proof assume "x\<in>dom (RBT.map_of t1)" with DOM_T1 have "k>x" by simp with C show False by simp qed ultimately have ?thesis by (simp add: map_add_upd2 map_add_dom_app_simps) } ultimately show ?thesis using less_linear by blast qed (* This one is marked with an oops in RBT.thy *) lemma map_of_alist_of: shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t" proof (induct t) case Empty thus ?case by (simp add: RBT.map_of_Empty) next case (Tr c t1 k v t2) hence "Map.map_of (alist_of (Tr c t1 k v t2)) = RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1" by simp also note map_of_alist_of_aux[OF Tr.prems,symmetric] finally show ?case . qed end

**Follow-Ups**:**Re: [isabelle] Lemma: Library/RBT.map-of-alist-of***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] ProofGeneral font-lock-mode and antiquoatations
- Next by Date: Re: [isabelle] Lemma: Library/RBT.map-of-alist-of
- Previous by Thread: Re: [isabelle] all Re: [Fwd: Re: Qualified name for Set.insert]
- Next by Thread: Re: [isabelle] Lemma: Library/RBT.map-of-alist-of
- Cl-isabelle-users July 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list