src/HOL/Library/RBT_Set.thy
changeset 56019 682bba24e474
parent 55584 a879f14b6f95
child 56212 3253aaf73a01
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Mon Mar 10 15:24:49 2014 +0100
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Mon Mar 10 17:14:57 2014 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  section {* Definition of code datatype constructors *}
     1.5  
     1.6  definition Set :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
     1.7 -  where "Set t = {x . lookup t x = Some ()}"
     1.8 +  where "Set t = {x . RBT.lookup t x = Some ()}"
     1.9  
    1.10  definition Coset :: "('a\<Colon>linorder, unit) rbt \<Rightarrow> 'a set" 
    1.11    where [simp]: "Coset t = - Set t"
    1.12 @@ -146,31 +146,31 @@
    1.13  lemma [simp]: "x \<noteq> Some () \<longleftrightarrow> x = None"
    1.14  by (auto simp: not_Some_eq[THEN iffD1])
    1.15  
    1.16 -lemma Set_set_keys: "Set x = dom (lookup x)" 
    1.17 +lemma Set_set_keys: "Set x = dom (RBT.lookup x)" 
    1.18  by (auto simp: Set_def)
    1.19  
    1.20  lemma finite_Set [simp, intro!]: "finite (Set x)"
    1.21  by (simp add: Set_set_keys)
    1.22  
    1.23 -lemma set_keys: "Set t = set(keys t)"
    1.24 +lemma set_keys: "Set t = set(RBT.keys t)"
    1.25  by (simp add: Set_set_keys lookup_keys)
    1.26  
    1.27  subsection {* fold and filter *}
    1.28  
    1.29  lemma finite_fold_rbt_fold_eq:
    1.30    assumes "comp_fun_commute f" 
    1.31 -  shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A"
    1.32 +  shows "Finite_Set.fold f A (set (RBT.entries t)) = RBT.fold (curry f) t A"
    1.33  proof -
    1.34 -  have *: "remdups (entries t) = entries t"
    1.35 +  have *: "remdups (RBT.entries t) = RBT.entries t"
    1.36      using distinct_entries distinct_map by (auto intro: distinct_remdups_id)
    1.37    show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *)
    1.38  qed
    1.39  
    1.40  definition fold_keys :: "('a :: linorder \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> ('a, _) rbt \<Rightarrow> 'b \<Rightarrow> 'b" 
    1.41 -  where [code_unfold]:"fold_keys f t A = fold (\<lambda>k _ t. f k t) t A"
    1.42 +  where [code_unfold]:"fold_keys f t A = RBT.fold (\<lambda>k _ t. f k t) t A"
    1.43  
    1.44  lemma fold_keys_def_alt:
    1.45 -  "fold_keys f t s = List.fold f (keys t) s"
    1.46 +  "fold_keys f t s = List.fold f (RBT.keys t) s"
    1.47  by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def)
    1.48  
    1.49  lemma finite_fold_fold_keys:
    1.50 @@ -179,15 +179,15 @@
    1.51  using assms
    1.52  proof -
    1.53    interpret comp_fun_commute f by fact
    1.54 -  have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries)
    1.55 -  moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto
    1.56 +  have "set (RBT.keys t) = fst ` (set (RBT.entries t))" by (auto simp: fst_eq_Domain keys_entries)
    1.57 +  moreover have "inj_on fst (set (RBT.entries t))" using distinct_entries distinct_map by auto
    1.58    ultimately show ?thesis 
    1.59      by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq 
    1.60        comp_comp_fun_commute)
    1.61  qed
    1.62  
    1.63  definition rbt_filter :: "('a :: linorder \<Rightarrow> bool) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'a set" where
    1.64 -  "rbt_filter P t = fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
    1.65 +  "rbt_filter P t = RBT.fold (\<lambda>k _ A'. if P k then Set.insert k A' else A') t {}"
    1.66  
    1.67  lemma Set_filter_rbt_filter:
    1.68    "Set.filter P (Set t) = rbt_filter P t"
    1.69 @@ -207,8 +207,8 @@
    1.70      by (cases "RBT_Impl.fold (\<lambda>k v s. s \<and> P k) t1 True") (simp_all add: Ball_False) 
    1.71  qed simp
    1.72  
    1.73 -lemma foldi_fold_conj: "foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
    1.74 -unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj)
    1.75 +lemma foldi_fold_conj: "RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t val = fold_keys (\<lambda>k s. s \<and> P k) t val"
    1.76 +unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_conj)
    1.77  
    1.78  
    1.79  subsection {* foldi and Bex *}
    1.80 @@ -223,8 +223,8 @@
    1.81      by (cases "RBT_Impl.fold (\<lambda>k v s. s \<or> P k) t1 False") (simp_all add: Bex_True) 
    1.82  qed simp
    1.83  
    1.84 -lemma foldi_fold_disj: "foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
    1.85 -unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj)
    1.86 +lemma foldi_fold_disj: "RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t val = fold_keys (\<lambda>k s. s \<or> P k) t val"
    1.87 +unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_disj)
    1.88  
    1.89  
    1.90  subsection {* folding over non empty trees and selecting the minimal and maximal element *}
    1.91 @@ -422,16 +422,17 @@
    1.92  
    1.93  (** abstract **)
    1.94  
    1.95 +context includes rbt.lifting begin
    1.96  lift_definition fold1_keys :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a::linorder, 'b) rbt \<Rightarrow> 'a"
    1.97    is rbt_fold1_keys .
    1.98  
    1.99  lemma fold1_keys_def_alt:
   1.100 -  "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))"
   1.101 +  "fold1_keys f t = List.fold f (tl (RBT.keys t)) (hd (RBT.keys t))"
   1.102    by transfer (simp add: rbt_fold1_keys_def)
   1.103  
   1.104  lemma finite_fold1_fold1_keys:
   1.105    assumes "semilattice f"
   1.106 -  assumes "\<not> is_empty t"
   1.107 +  assumes "\<not> RBT.is_empty t"
   1.108    shows "semilattice_set.F f (Set t) = fold1_keys f t"
   1.109  proof -
   1.110    from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro)
   1.111 @@ -449,13 +450,13 @@
   1.112  by transfer (simp add: rbt_min_def)
   1.113  
   1.114  lemma r_min_eq_r_min_opt:
   1.115 -  assumes "\<not> (is_empty t)"
   1.116 +  assumes "\<not> (RBT.is_empty t)"
   1.117    shows "r_min t = r_min_opt t"
   1.118  using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt)
   1.119  
   1.120  lemma fold_keys_min_top_eq:
   1.121    fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt"
   1.122 -  assumes "\<not> (is_empty t)"
   1.123 +  assumes "\<not> (RBT.is_empty t)"
   1.124    shows "fold_keys min t top = fold1_keys min t"
   1.125  proof -
   1.126    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold min (RBT_Impl.keys t) top = 
   1.127 @@ -487,13 +488,13 @@
   1.128  by transfer (simp add: rbt_max_def)
   1.129  
   1.130  lemma r_max_eq_r_max_opt:
   1.131 -  assumes "\<not> (is_empty t)"
   1.132 +  assumes "\<not> (RBT.is_empty t)"
   1.133    shows "r_max t = r_max_opt t"
   1.134  using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt)
   1.135  
   1.136  lemma fold_keys_max_bot_eq:
   1.137    fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt"
   1.138 -  assumes "\<not> (is_empty t)"
   1.139 +  assumes "\<not> (RBT.is_empty t)"
   1.140    shows "fold_keys max t bot = fold1_keys max t"
   1.141  proof -
   1.142    have *: "\<And>t. RBT_Impl.keys t \<noteq> [] \<Longrightarrow> List.fold max (RBT_Impl.keys t) bot = 
   1.143 @@ -515,6 +516,7 @@
   1.144    done
   1.145  qed
   1.146  
   1.147 +end
   1.148  
   1.149  section {* Code equations *}
   1.150  
   1.151 @@ -584,7 +586,7 @@
   1.152  qed
   1.153   
   1.154  lemma union_Set_Set [code]:
   1.155 -  "Set t1 \<union> Set t2 = Set (union t1 t2)"
   1.156 +  "Set t1 \<union> Set t2 = Set (RBT.union t1 t2)"
   1.157  by (auto simp add: lookup_union map_add_Some_iff Set_def)
   1.158  
   1.159  lemma inter_Coset [code]:
   1.160 @@ -592,7 +594,7 @@
   1.161  by (simp add: Diff_eq [symmetric] minus_Set)
   1.162  
   1.163  lemma inter_Coset_Coset [code]:
   1.164 -  "Coset t1 \<inter> Coset t2 = Coset (union t1 t2)"
   1.165 +  "Coset t1 \<inter> Coset t2 = Coset (RBT.union t1 t2)"
   1.166  by (auto simp add: lookup_union map_add_Some_iff Set_def)
   1.167  
   1.168  lemma minus_Coset [code]:
   1.169 @@ -611,7 +613,7 @@
   1.170  qed
   1.171  
   1.172  lemma Ball_Set [code]:
   1.173 -  "Ball (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   1.174 +  "Ball (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> P k) t True"
   1.175  proof -
   1.176    have "comp_fun_commute (\<lambda>k s. s \<and> P k)" by default auto
   1.177    then show ?thesis 
   1.178 @@ -619,7 +621,7 @@
   1.179  qed
   1.180  
   1.181  lemma Bex_Set [code]:
   1.182 -  "Bex (Set t) P \<longleftrightarrow> foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   1.183 +  "Bex (Set t) P \<longleftrightarrow> RBT.foldi (\<lambda>s. s = False) (\<lambda>k v s. s \<or> P k) t False"
   1.184  proof -
   1.185    have "comp_fun_commute (\<lambda>k s. s \<or> P k)" by default auto
   1.186    then show ?thesis 
   1.187 @@ -632,11 +634,11 @@
   1.188  by auto
   1.189  
   1.190  lemma subset_Coset_empty_Set_empty [code]:
   1.191 -  "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (impl_of t1, impl_of t2) of 
   1.192 +  "Coset t1 \<le> Set t2 \<longleftrightarrow> (case (RBT.impl_of t1, RBT.impl_of t2) of 
   1.193      (rbt.Empty, rbt.Empty) => False |
   1.194      (_, _) => Code.abort (STR ''non_empty_trees'') (\<lambda>_. Coset t1 \<le> Set t2))"
   1.195  proof -
   1.196 -  have *: "\<And>t. impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   1.197 +  have *: "\<And>t. RBT.impl_of t = rbt.Empty \<Longrightarrow> t = RBT rbt.Empty"
   1.198      by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject)
   1.199    have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp
   1.200    show ?thesis  
   1.201 @@ -645,7 +647,7 @@
   1.202  
   1.203  text {* A frequent case – avoid intermediate sets *}
   1.204  lemma [code_unfold]:
   1.205 -  "Set t1 \<subseteq> Set t2 \<longleftrightarrow> foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   1.206 +  "Set t1 \<subseteq> Set t2 \<longleftrightarrow> RBT.foldi (\<lambda>s. s = True) (\<lambda>k v s. s \<and> k \<in> Set t2) t1 True"
   1.207  by (simp add: subset_code Ball_Set)
   1.208  
   1.209  lemma card_Set [code]:
   1.210 @@ -662,7 +664,7 @@
   1.211  
   1.212  lemma the_elem_set [code]:
   1.213    fixes t :: "('a :: linorder, unit) rbt"
   1.214 -  shows "the_elem (Set t) = (case impl_of t of 
   1.215 +  shows "the_elem (Set t) = (case RBT.impl_of t of 
   1.216      (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \<Rightarrow> x
   1.217      | _ \<Rightarrow> Code.abort (STR ''not_a_singleton_tree'') (\<lambda>_. the_elem (Set t)))"
   1.218  proof -
   1.219 @@ -672,7 +674,7 @@
   1.220      have *:"?t \<in> {t. is_rbt t}" unfolding is_rbt_def by auto
   1.221      then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto
   1.222  
   1.223 -    have "impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   1.224 +    have "RBT.impl_of t = ?t \<Longrightarrow> the_elem (Set t) = x" 
   1.225        by (subst(asm) RBT_inverse[symmetric, OF *])
   1.226          (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject)
   1.227    }
   1.228 @@ -726,7 +728,7 @@
   1.229  
   1.230  lemma Min_fin_set_fold [code]:
   1.231    "Min (Set t) = 
   1.232 -  (if is_empty t
   1.233 +  (if RBT.is_empty t
   1.234     then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Min (Set t))
   1.235     else r_min_opt t)"
   1.236  proof -
   1.237 @@ -742,10 +744,10 @@
   1.238  
   1.239  lemma Inf_Set_fold:
   1.240    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   1.241 -  shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)"
   1.242 +  shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)"
   1.243  proof -
   1.244    have "comp_fun_commute (min :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   1.245 -  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   1.246 +  then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold min top (Set t) = fold1_keys min t"
   1.247      by (simp add: finite_fold_fold_keys fold_keys_min_top_eq)
   1.248    then show ?thesis 
   1.249      by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def)
   1.250 @@ -767,7 +769,7 @@
   1.251  
   1.252  lemma Max_fin_set_fold [code]:
   1.253    "Max (Set t) = 
   1.254 -  (if is_empty t
   1.255 +  (if RBT.is_empty t
   1.256     then Code.abort (STR ''not_non_empty_tree'') (\<lambda>_. Max (Set t))
   1.257     else r_max_opt t)"
   1.258  proof -
   1.259 @@ -783,10 +785,10 @@
   1.260  
   1.261  lemma Sup_Set_fold:
   1.262    fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt"
   1.263 -  shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)"
   1.264 +  shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)"
   1.265  proof -
   1.266    have "comp_fun_commute (max :: 'a \<Rightarrow> 'a \<Rightarrow> 'a)" by default (simp add: fun_eq_iff ac_simps)
   1.267 -  then have "t \<noteq> empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   1.268 +  then have "t \<noteq> RBT.empty \<Longrightarrow> Finite_Set.fold max bot (Set t) = fold1_keys max t"
   1.269      by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq)
   1.270    then show ?thesis 
   1.271      by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def)
   1.272 @@ -807,14 +809,14 @@
   1.273  qed
   1.274  
   1.275  lemma sorted_list_set[code]:
   1.276 -  "sorted_list_of_set (Set t) = keys t"
   1.277 +  "sorted_list_of_set (Set t) = RBT.keys t"
   1.278  by (auto simp add: set_keys intro: sorted_distinct_set_unique) 
   1.279  
   1.280  lemma Bleast_code [code]:
   1.281 - "Bleast (Set t) P = (case filter P (keys t) of
   1.282 + "Bleast (Set t) P = (case filter P (RBT.keys t) of
   1.283      x#xs \<Rightarrow> x |
   1.284      [] \<Rightarrow> abort_Bleast (Set t) P)"
   1.285 -proof (cases "filter P (keys t)")
   1.286 +proof (cases "filter P (RBT.keys t)")
   1.287    case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def)
   1.288  next
   1.289    case (Cons x ys)
   1.290 @@ -831,7 +833,6 @@
   1.291    thus ?thesis using Cons by (simp add: Bleast_def)
   1.292  qed
   1.293  
   1.294 -
   1.295  hide_const (open) RBT_Set.Set RBT_Set.Coset
   1.296  
   1.297  end