src/HOL/Library/RBT.thy
changeset 32237 cdc76a42fed4
parent 30738 0842e906300c
child 32245 0c1cb95a434d
     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)"