author | krauss |

Mon Jul 27 22:50:04 2009 +0200 (2009-07-27) | |

changeset 32237 | cdc76a42fed4 |

parent 32236 | 0203e1006f1b |

child 32238 | 74ae5e9f312c |

added missing proof of RBT.map_of_alist_of (contributed by Peter Lammich)

1.1 --- a/src/HOL/Library/RBT.thy Mon Jul 27 22:50:01 2009 +0200 1.2 +++ b/src/HOL/Library/RBT.thy Mon Jul 27 22:50:04 2009 +0200 1.3 @@ -916,9 +916,72 @@ 1.4 "alist_of Empty = []" 1.5 | "alist_of (Tr _ l k v r) = alist_of l @ (k,v) # alist_of r" 1.6 1.7 +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" 1.8 +proof (rule ext) 1.9 + fix x 1.10 + assume ST: "st (Tr c t1 k v t2)" 1.11 + let ?thesis = "RBT.map_of (Tr c t1 k v t2) x = (RBT.map_of t2 ++ [k \<mapsto> v] ++ RBT.map_of t1) x" 1.12 + 1.13 + have DOM_T1: "!!k'. k'\<in>dom (RBT.map_of t1) \<Longrightarrow> k>k'" 1.14 + proof - 1.15 + fix k' 1.16 + from ST have "t1 |\<guillemotleft> k" by simp 1.17 + with tlt_prop have "\<forall>k'\<in>keys t1. k>k'" by auto 1.18 + moreover assume "k'\<in>dom (RBT.map_of t1)" 1.19 + ultimately show "k>k'" using RBT.mapof_keys ST by auto 1.20 + qed 1.21 + 1.22 + have DOM_T2: "!!k'. k'\<in>dom (RBT.map_of t2) \<Longrightarrow> k<k'" 1.23 + proof - 1.24 + fix k' 1.25 + from ST have "k \<guillemotleft>| t2" by simp 1.26 + with tgt_prop have "\<forall>k'\<in>keys t2. k<k'" by auto 1.27 + moreover assume "k'\<in>dom (RBT.map_of t2)" 1.28 + ultimately show "k<k'" using RBT.mapof_keys ST by auto 1.29 + qed 1.30 + 1.31 + { 1.32 + assume C: "x<k" 1.33 + hence "RBT.map_of (Tr c t1 k v t2) x = RBT.map_of t1 x" by simp 1.34 + moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp 1.35 + moreover have "x\<notin>dom (RBT.map_of t2)" proof 1.36 + assume "x\<in>dom (RBT.map_of t2)" 1.37 + with DOM_T2 have "k<x" by blast 1.38 + with C show False by simp 1.39 + qed 1.40 + ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 1.41 + } moreover { 1.42 + assume [simp]: "x=k" 1.43 + hence "RBT.map_of (Tr c t1 k v t2) x = [k \<mapsto> v] x" by simp 1.44 + moreover have "x\<notin>dom (RBT.map_of t1)" proof 1.45 + assume "x\<in>dom (RBT.map_of t1)" 1.46 + with DOM_T1 have "k>x" by blast 1.47 + thus False by simp 1.48 + qed 1.49 + ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 1.50 + } moreover { 1.51 + assume C: "x>k" 1.52 + 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]) 1.53 + moreover from C have "x\<notin>dom [k\<mapsto>v]" by simp 1.54 + moreover have "x\<notin>dom (RBT.map_of t1)" proof 1.55 + assume "x\<in>dom (RBT.map_of t1)" 1.56 + with DOM_T1 have "k>x" by simp 1.57 + with C show False by simp 1.58 + qed 1.59 + ultimately have ?thesis by (simp add: map_add_upd_left map_add_dom_app_simps) 1.60 + } ultimately show ?thesis using less_linear by blast 1.61 +qed 1.62 + 1.63 lemma map_of_alist_of: 1.64 shows "st t \<Longrightarrow> Map.map_of (alist_of t) = map_of t" 1.65 - oops 1.66 +proof (induct t) 1.67 + case Empty thus ?case by (simp add: RBT.map_of_Empty) 1.68 +next 1.69 + case (Tr c t1 k v t2) 1.70 + 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 1.71 + also note map_of_alist_of_aux[OF Tr.prems,symmetric] 1.72 + finally show ?case . 1.73 +qed 1.74 1.75 lemma fold_alist_fold: 1.76 "foldwithkey f t x = foldl (\<lambda>x (k,v). f k v x) x (alist_of t)"