# HG changeset patch # User kuncar # Date 1394468097 -3600 # Node ID 682bba24e474f474ac8b38574050721d4d5756c2 # Parent c3fc8692dbc1a074416b8c2575fa4b2082423908 hide implementation details diff -r c3fc8692dbc1 -r 682bba24e474 src/HOL/Library/RBT.thy --- a/src/HOL/Library/RBT.thy Mon Mar 10 15:24:49 2014 +0100 +++ b/src/HOL/Library/RBT.thy Mon Mar 10 17:14:57 2014 +0100 @@ -36,7 +36,6 @@ subsection {* Primitive operations *} setup_lifting type_definition_rbt -print_theorems lift_definition lookup :: "('a\linorder, 'b) rbt \ 'a \ 'b" is "rbt_lookup" . @@ -187,4 +186,14 @@ quickcheck_generator rbt predicate: is_rbt constructors: empty, insert +subsection {* Hide implementation details *} + +lifting_update rbt.lifting +lifting_forget rbt.lifting + +hide_const (open) impl_of empty lookup keys entries bulkload delete map fold union insert map_entry foldi + is_empty +hide_fact (open) empty_def lookup_def keys_def entries_def bulkload_def delete_def map_def fold_def + union_def insert_def map_entry_def foldi_def is_empty_def + end diff -r c3fc8692dbc1 -r 682bba24e474 src/HOL/Library/RBT_Mapping.thy --- a/src/HOL/Library/RBT_Mapping.thy Mon Mar 10 15:24:49 2014 +0100 +++ b/src/HOL/Library/RBT_Mapping.thy Mon Mar 10 17:14:57 2014 +0100 @@ -11,42 +11,46 @@ subsection {* Implementation of mappings *} -lift_definition Mapping :: "('a\linorder, 'b) rbt \ ('a, 'b) mapping" is lookup . +context includes rbt.lifting begin +lift_definition Mapping :: "('a\linorder, 'b) rbt \ ('a, 'b) mapping" is RBT.lookup . +end code_datatype Mapping +context includes rbt.lifting begin + lemma lookup_Mapping [simp, code]: - "Mapping.lookup (Mapping t) = lookup t" + "Mapping.lookup (Mapping t) = RBT.lookup t" by (transfer fixing: t) rule -lemma empty_Mapping [code]: "Mapping.empty = Mapping empty" +lemma empty_Mapping [code]: "Mapping.empty = Mapping RBT.empty" proof - note RBT.empty.transfer[transfer_rule del] show ?thesis by transfer simp qed lemma is_empty_Mapping [code]: - "Mapping.is_empty (Mapping t) \ is_empty t" + "Mapping.is_empty (Mapping t) \ RBT.is_empty t" unfolding is_empty_def by (transfer fixing: t) simp lemma insert_Mapping [code]: - "Mapping.update k v (Mapping t) = Mapping (insert k v t)" + "Mapping.update k v (Mapping t) = Mapping (RBT.insert k v t)" by (transfer fixing: t) simp lemma delete_Mapping [code]: - "Mapping.delete k (Mapping t) = Mapping (delete k t)" + "Mapping.delete k (Mapping t) = Mapping (RBT.delete k t)" by (transfer fixing: t) simp lemma map_entry_Mapping [code]: - "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" - apply (transfer fixing: t) by (case_tac "lookup t k") auto + "Mapping.map_entry k f (Mapping t) = Mapping (RBT.map_entry k f t)" + apply (transfer fixing: t) by (case_tac "RBT.lookup t k") auto lemma keys_Mapping [code]: - "Mapping.keys (Mapping t) = set (keys t)" + "Mapping.keys (Mapping t) = set (RBT.keys t)" by (transfer fixing: t) (simp add: lookup_keys) lemma ordered_keys_Mapping [code]: - "Mapping.ordered_keys (Mapping t) = keys t" + "Mapping.ordered_keys (Mapping t) = RBT.keys t" unfolding ordered_keys_def by (transfer fixing: t) (auto simp add: lookup_keys intro: sorted_distinct_set_unique) @@ -55,7 +59,7 @@ unfolding size_def by transfer simp lemma size_Mapping [code]: - "Mapping.size (Mapping t) = length (keys t)" + "Mapping.size (Mapping t) = length (RBT.keys t)" unfolding size_def by (transfer fixing: t) (simp add: lookup_keys distinct_card) @@ -63,25 +67,24 @@ notes RBT.bulkload.transfer[transfer_rule del] begin lemma tabulate_Mapping [code]: - "Mapping.tabulate ks f = Mapping (bulkload (List.map (\k. (k, f k)) ks))" + "Mapping.tabulate ks f = Mapping (RBT.bulkload (List.map (\k. (k, f k)) ks))" by transfer (simp add: map_of_map_restrict) lemma bulkload_Mapping [code]: - "Mapping.bulkload vs = Mapping (bulkload (List.map (\n. (n, vs ! n)) [0..n. (n, vs ! n)) [0.. entries t1 = entries t2" + "HOL.equal (Mapping t1) (Mapping t2) \ RBT.entries t1 = RBT.entries t2" by (transfer fixing: t1 t2) (simp add: entries_lookup) lemma [code nbe]: "HOL.equal (x :: (_, _) mapping) x \ True" by (fact equal_refl) +end -hide_const (open) impl_of lookup empty insert delete - entries keys bulkload map_entry map fold (*>*) text {* diff -r c3fc8692dbc1 -r 682bba24e474 src/HOL/Library/RBT_Set.thy --- a/src/HOL/Library/RBT_Set.thy Mon Mar 10 15:24:49 2014 +0100 +++ b/src/HOL/Library/RBT_Set.thy Mon Mar 10 17:14:57 2014 +0100 @@ -19,7 +19,7 @@ section {* Definition of code datatype constructors *} definition Set :: "('a\linorder, unit) rbt \ 'a set" - where "Set t = {x . lookup t x = Some ()}" + where "Set t = {x . RBT.lookup t x = Some ()}" definition Coset :: "('a\linorder, unit) rbt \ 'a set" where [simp]: "Coset t = - Set t" @@ -146,31 +146,31 @@ lemma [simp]: "x \ Some () \ x = None" by (auto simp: not_Some_eq[THEN iffD1]) -lemma Set_set_keys: "Set x = dom (lookup x)" +lemma Set_set_keys: "Set x = dom (RBT.lookup x)" by (auto simp: Set_def) lemma finite_Set [simp, intro!]: "finite (Set x)" by (simp add: Set_set_keys) -lemma set_keys: "Set t = set(keys t)" +lemma set_keys: "Set t = set(RBT.keys t)" by (simp add: Set_set_keys lookup_keys) subsection {* fold and filter *} lemma finite_fold_rbt_fold_eq: assumes "comp_fun_commute f" - shows "Finite_Set.fold f A (set(entries t)) = fold (curry f) t A" + shows "Finite_Set.fold f A (set (RBT.entries t)) = RBT.fold (curry f) t A" proof - - have *: "remdups (entries t) = entries t" + have *: "remdups (RBT.entries t) = RBT.entries t" using distinct_entries distinct_map by (auto intro: distinct_remdups_id) show ?thesis using assms by (auto simp: fold_def_alt comp_fun_commute.fold_set_fold_remdups *) qed definition fold_keys :: "('a :: linorder \ 'b \ 'b) \ ('a, _) rbt \ 'b \ 'b" - where [code_unfold]:"fold_keys f t A = fold (\k _ t. f k t) t A" + where [code_unfold]:"fold_keys f t A = RBT.fold (\k _ t. f k t) t A" lemma fold_keys_def_alt: - "fold_keys f t s = List.fold f (keys t) s" + "fold_keys f t s = List.fold f (RBT.keys t) s" by (auto simp: fold_map o_def split_def fold_def_alt keys_def_alt fold_keys_def) lemma finite_fold_fold_keys: @@ -179,15 +179,15 @@ using assms proof - interpret comp_fun_commute f by fact - have "set (keys t) = fst ` (set (entries t))" by (auto simp: fst_eq_Domain keys_entries) - moreover have "inj_on fst (set (entries t))" using distinct_entries distinct_map by auto + have "set (RBT.keys t) = fst ` (set (RBT.entries t))" by (auto simp: fst_eq_Domain keys_entries) + moreover have "inj_on fst (set (RBT.entries t))" using distinct_entries distinct_map by auto ultimately show ?thesis by (auto simp add: set_keys fold_keys_def curry_def fold_image finite_fold_rbt_fold_eq comp_comp_fun_commute) qed definition rbt_filter :: "('a :: linorder \ bool) \ ('a, 'b) rbt \ 'a set" where - "rbt_filter P t = fold (\k _ A'. if P k then Set.insert k A' else A') t {}" + "rbt_filter P t = RBT.fold (\k _ A'. if P k then Set.insert k A' else A') t {}" lemma Set_filter_rbt_filter: "Set.filter P (Set t) = rbt_filter P t" @@ -207,8 +207,8 @@ by (cases "RBT_Impl.fold (\k v s. s \ P k) t1 True") (simp_all add: Ball_False) qed simp -lemma foldi_fold_conj: "foldi (\s. s = True) (\k v s. s \ P k) t val = fold_keys (\k s. s \ P k) t val" -unfolding fold_keys_def by transfer (rule rbt_foldi_fold_conj) +lemma foldi_fold_conj: "RBT.foldi (\s. s = True) (\k v s. s \ P k) t val = fold_keys (\k s. s \ P k) t val" +unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_conj) subsection {* foldi and Bex *} @@ -223,8 +223,8 @@ by (cases "RBT_Impl.fold (\k v s. s \ P k) t1 False") (simp_all add: Bex_True) qed simp -lemma foldi_fold_disj: "foldi (\s. s = False) (\k v s. s \ P k) t val = fold_keys (\k s. s \ P k) t val" -unfolding fold_keys_def by transfer (rule rbt_foldi_fold_disj) +lemma foldi_fold_disj: "RBT.foldi (\s. s = False) (\k v s. s \ P k) t val = fold_keys (\k s. s \ P k) t val" +unfolding fold_keys_def including rbt.lifting by transfer (rule rbt_foldi_fold_disj) subsection {* folding over non empty trees and selecting the minimal and maximal element *} @@ -422,16 +422,17 @@ (** abstract **) +context includes rbt.lifting begin lift_definition fold1_keys :: "('a \ 'a \ 'a) \ ('a::linorder, 'b) rbt \ 'a" is rbt_fold1_keys . lemma fold1_keys_def_alt: - "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))" + "fold1_keys f t = List.fold f (tl (RBT.keys t)) (hd (RBT.keys t))" by transfer (simp add: rbt_fold1_keys_def) lemma finite_fold1_fold1_keys: assumes "semilattice f" - assumes "\ is_empty t" + assumes "\ RBT.is_empty t" shows "semilattice_set.F f (Set t) = fold1_keys f t" proof - from `semilattice f` interpret semilattice_set f by (rule semilattice_set.intro) @@ -449,13 +450,13 @@ by transfer (simp add: rbt_min_def) lemma r_min_eq_r_min_opt: - assumes "\ (is_empty t)" + assumes "\ (RBT.is_empty t)" shows "r_min t = r_min_opt t" using assms unfolding is_empty_empty by transfer (auto intro: rbt_min_eq_rbt_min_opt) lemma fold_keys_min_top_eq: fixes t :: "('a :: {linorder, bounded_lattice_top}, unit) rbt" - assumes "\ (is_empty t)" + assumes "\ (RBT.is_empty t)" shows "fold_keys min t top = fold1_keys min t" proof - have *: "\t. RBT_Impl.keys t \ [] \ List.fold min (RBT_Impl.keys t) top = @@ -487,13 +488,13 @@ by transfer (simp add: rbt_max_def) lemma r_max_eq_r_max_opt: - assumes "\ (is_empty t)" + assumes "\ (RBT.is_empty t)" shows "r_max t = r_max_opt t" using assms unfolding is_empty_empty by transfer (auto intro: rbt_max_eq_rbt_max_opt) lemma fold_keys_max_bot_eq: fixes t :: "('a :: {linorder, bounded_lattice_bot}, unit) rbt" - assumes "\ (is_empty t)" + assumes "\ (RBT.is_empty t)" shows "fold_keys max t bot = fold1_keys max t" proof - have *: "\t. RBT_Impl.keys t \ [] \ List.fold max (RBT_Impl.keys t) bot = @@ -515,6 +516,7 @@ done qed +end section {* Code equations *} @@ -584,7 +586,7 @@ qed lemma union_Set_Set [code]: - "Set t1 \ Set t2 = Set (union t1 t2)" + "Set t1 \ Set t2 = Set (RBT.union t1 t2)" by (auto simp add: lookup_union map_add_Some_iff Set_def) lemma inter_Coset [code]: @@ -592,7 +594,7 @@ by (simp add: Diff_eq [symmetric] minus_Set) lemma inter_Coset_Coset [code]: - "Coset t1 \ Coset t2 = Coset (union t1 t2)" + "Coset t1 \ Coset t2 = Coset (RBT.union t1 t2)" by (auto simp add: lookup_union map_add_Some_iff Set_def) lemma minus_Coset [code]: @@ -611,7 +613,7 @@ qed lemma Ball_Set [code]: - "Ball (Set t) P \ foldi (\s. s = True) (\k v s. s \ P k) t True" + "Ball (Set t) P \ RBT.foldi (\s. s = True) (\k v s. s \ P k) t True" proof - have "comp_fun_commute (\k s. s \ P k)" by default auto then show ?thesis @@ -619,7 +621,7 @@ qed lemma Bex_Set [code]: - "Bex (Set t) P \ foldi (\s. s = False) (\k v s. s \ P k) t False" + "Bex (Set t) P \ RBT.foldi (\s. s = False) (\k v s. s \ P k) t False" proof - have "comp_fun_commute (\k s. s \ P k)" by default auto then show ?thesis @@ -632,11 +634,11 @@ by auto lemma subset_Coset_empty_Set_empty [code]: - "Coset t1 \ Set t2 \ (case (impl_of t1, impl_of t2) of + "Coset t1 \ Set t2 \ (case (RBT.impl_of t1, RBT.impl_of t2) of (rbt.Empty, rbt.Empty) => False | (_, _) => Code.abort (STR ''non_empty_trees'') (\_. Coset t1 \ Set t2))" proof - - have *: "\t. impl_of t = rbt.Empty \ t = RBT rbt.Empty" + have *: "\t. RBT.impl_of t = rbt.Empty \ t = RBT rbt.Empty" by (subst(asm) RBT_inverse[symmetric]) (auto simp: impl_of_inject) have **: "Lifting.invariant is_rbt rbt.Empty rbt.Empty" unfolding Lifting.invariant_def by simp show ?thesis @@ -645,7 +647,7 @@ text {* A frequent case – avoid intermediate sets *} lemma [code_unfold]: - "Set t1 \ Set t2 \ foldi (\s. s = True) (\k v s. s \ k \ Set t2) t1 True" + "Set t1 \ Set t2 \ RBT.foldi (\s. s = True) (\k v s. s \ k \ Set t2) t1 True" by (simp add: subset_code Ball_Set) lemma card_Set [code]: @@ -662,7 +664,7 @@ lemma the_elem_set [code]: fixes t :: "('a :: linorder, unit) rbt" - shows "the_elem (Set t) = (case impl_of t of + shows "the_elem (Set t) = (case RBT.impl_of t of (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \ x | _ \ Code.abort (STR ''not_a_singleton_tree'') (\_. the_elem (Set t)))" proof - @@ -672,7 +674,7 @@ have *:"?t \ {t. is_rbt t}" unfolding is_rbt_def by auto then have **:"Lifting.invariant is_rbt ?t ?t" unfolding Lifting.invariant_def by auto - have "impl_of t = ?t \ the_elem (Set t) = x" + have "RBT.impl_of t = ?t \ the_elem (Set t) = x" by (subst(asm) RBT_inverse[symmetric, OF *]) (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject) } @@ -726,7 +728,7 @@ lemma Min_fin_set_fold [code]: "Min (Set t) = - (if is_empty t + (if RBT.is_empty t then Code.abort (STR ''not_non_empty_tree'') (\_. Min (Set t)) else r_min_opt t)" proof - @@ -742,10 +744,10 @@ lemma Inf_Set_fold: fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt" - shows "Inf (Set t) = (if is_empty t then top else r_min_opt t)" + shows "Inf (Set t) = (if RBT.is_empty t then top else r_min_opt t)" proof - have "comp_fun_commute (min :: 'a \ 'a \ 'a)" by default (simp add: fun_eq_iff ac_simps) - then have "t \ empty \ Finite_Set.fold min top (Set t) = fold1_keys min t" + then have "t \ RBT.empty \ Finite_Set.fold min top (Set t) = fold1_keys min t" by (simp add: finite_fold_fold_keys fold_keys_min_top_eq) then show ?thesis by (auto simp add: Inf_fold_inf inf_min empty_Set[symmetric] r_min_eq_r_min_opt[symmetric] r_min_alt_def) @@ -767,7 +769,7 @@ lemma Max_fin_set_fold [code]: "Max (Set t) = - (if is_empty t + (if RBT.is_empty t then Code.abort (STR ''not_non_empty_tree'') (\_. Max (Set t)) else r_max_opt t)" proof - @@ -783,10 +785,10 @@ lemma Sup_Set_fold: fixes t :: "('a :: {linorder, complete_lattice}, unit) rbt" - shows "Sup (Set t) = (if is_empty t then bot else r_max_opt t)" + shows "Sup (Set t) = (if RBT.is_empty t then bot else r_max_opt t)" proof - have "comp_fun_commute (max :: 'a \ 'a \ 'a)" by default (simp add: fun_eq_iff ac_simps) - then have "t \ empty \ Finite_Set.fold max bot (Set t) = fold1_keys max t" + then have "t \ RBT.empty \ Finite_Set.fold max bot (Set t) = fold1_keys max t" by (simp add: finite_fold_fold_keys fold_keys_max_bot_eq) then show ?thesis by (auto simp add: Sup_fold_sup sup_max empty_Set[symmetric] r_max_eq_r_max_opt[symmetric] r_max_alt_def) @@ -807,14 +809,14 @@ qed lemma sorted_list_set[code]: - "sorted_list_of_set (Set t) = keys t" + "sorted_list_of_set (Set t) = RBT.keys t" by (auto simp add: set_keys intro: sorted_distinct_set_unique) lemma Bleast_code [code]: - "Bleast (Set t) P = (case filter P (keys t) of + "Bleast (Set t) P = (case filter P (RBT.keys t) of x#xs \ x | [] \ abort_Bleast (Set t) P)" -proof (cases "filter P (keys t)") +proof (cases "filter P (RBT.keys t)") case Nil thus ?thesis by (simp add: Bleast_def abort_Bleast_def) next case (Cons x ys) @@ -831,7 +833,6 @@ thus ?thesis using Cons by (simp add: Bleast_def) qed - hide_const (open) RBT_Set.Set RBT_Set.Coset end