# HG changeset patch # User kuncar # Date 1343735739 -7200 # Node ID bea613f2543d5a2cf4fc9639269064543c4db77e # Parent caaa1a02c650e6e12da388eef4d5c7230cc64558 implementation of sets by RBT trees for the code generator diff -r caaa1a02c650 -r bea613f2543d src/HOL/Library/Library.thy --- a/src/HOL/Library/Library.thy Tue Jul 31 13:55:39 2012 +0200 +++ b/src/HOL/Library/Library.thy Tue Jul 31 13:55:39 2012 +0200 @@ -55,6 +55,7 @@ Ramsey Reflection RBT_Mapping + (* RBT_Set *) (* not included because it breaks Codegenerator_Test/Generate*.thy *) Saturated Set_Algebras State_Monad diff -r caaa1a02c650 -r bea613f2543d src/HOL/Library/RBT_Set.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Library/RBT_Set.thy Tue Jul 31 13:55:39 2012 +0200 @@ -0,0 +1,824 @@ +(* Title: HOL/Library/RBT_Set.thy + Author: Ondrej Kuncar +*) + +header {* Implementation of sets using RBT trees *} + +theory RBT_Set +imports RBT Product_ord +begin + +(* + Users should be aware that by including this file all code equations + outside of List.thy using 'a list as an implenentation of sets cannot be + used for code generation. If such equations are not needed, they can be + deleted from the code generator. Otherwise, a user has to provide their + own equations using RBT trees. +*) + +section {* Definition of code datatype constructors *} + +definition Set :: "('a\linorder, unit) rbt \ 'a set" + where "Set t = {x . lookup t x = Some ()}" + +definition Coset :: "('a\linorder, unit) rbt \ 'a set" + where [simp]: "Coset t = - Set t" + + +section {* Deletion of already existing code equations *} + +lemma [code, code del]: + "Set.empty = Set.empty" .. + +lemma [code, code del]: + "Set.is_empty = Set.is_empty" .. + +lemma [code, code del]: + "uminus_set_inst.uminus_set = uminus_set_inst.uminus_set" .. + +lemma [code, code del]: + "Set.member = Set.member" .. + +lemma [code, code del]: + "Set.insert = Set.insert" .. + +lemma [code, code del]: + "Set.remove = Set.remove" .. + +lemma [code, code del]: + "UNIV = UNIV" .. + +lemma [code, code del]: + "Set.project = Set.project" .. + +lemma [code, code del]: + "image = image" .. + +lemma [code, code del]: + "Set.subset_eq = Set.subset_eq" .. + +lemma [code, code del]: + "Ball = Ball" .. + +lemma [code, code del]: + "Bex = Bex" .. + +lemma [code, code del]: + "Set.union = Set.union" .. + +lemma [code, code del]: + "minus_set_inst.minus_set = minus_set_inst.minus_set" .. + +lemma [code, code del]: + "Set.inter = Set.inter" .. + +lemma [code, code del]: + "card = card" .. + +lemma [code, code del]: + "the_elem = the_elem" .. + +lemma [code, code del]: + "Pow = Pow" .. + +lemma [code, code del]: + "setsum = setsum" .. + +lemma [code, code del]: + "Product_Type.product = Product_Type.product" .. + +lemma [code, code del]: + "Id_on = Id_on" .. + +lemma [code, code del]: + "Image = Image" .. + +lemma [code, code del]: + "trancl = trancl" .. + +lemma [code, code del]: + "relcomp = relcomp" .. + +lemma [code, code del]: + "wf = wf" .. + +lemma [code, code del]: + "Min = Min" .. + +lemma [code, code del]: + "Inf_fin = Inf_fin" .. + +lemma [code, code del]: + "INFI = INFI" .. + +lemma [code, code del]: + "Max = Max" .. + +lemma [code, code del]: + "Sup_fin = Sup_fin" .. + +lemma [code, code del]: + "SUPR = SUPR" .. + +lemma [code, code del]: + "(Inf :: 'a set set \ 'a set) = Inf" .. + +lemma [code, code del]: + "(Sup :: 'a set set \ 'a set) = Sup" .. + +lemma [code, code del]: + "sorted_list_of_set = sorted_list_of_set" .. + +lemma [code, code del]: + "List.map_project = List.map_project" .. + +section {* Lemmas *} + + +subsection {* Auxiliary lemmas *} + +lemma [simp]: "x \ Some () \ x = None" +by (auto simp: not_Some_eq[THEN iffD1]) + +lemma finite_Set [simp, intro!]: "finite (Set x)" +proof - + have "Set x = dom (lookup x)" by (auto simp: Set_def) + then show ?thesis by simp +qed + +lemma set_keys: "Set t = set(keys t)" +proof - + have "\k. ((k, ()) \ set (entries t)) = (k \ set (keys t))" + by (simp add: keys_entries) + then show ?thesis by (auto simp: lookup_in_tree Set_def) +qed + +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" +proof - + have *: "remdups (entries t) = 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" + +lemma fold_keys_def_alt: + "fold_keys f t s = List.fold f (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: + assumes "comp_fun_commute f" + shows "Finite_Set.fold f A (Set t) = fold_keys f t A" +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 + 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 {}" + +lemma finite_filter_rbt_filter: + "Finite_Set.filter P (Set t) = rbt_filter P t" +by (simp add: fold_keys_def Finite_Set.filter_def rbt_filter_def + finite_fold_fold_keys[OF comp_fun_commute_filter_fold]) + + +subsection {* foldi and Ball *} + +lemma Ball_False: "RBT_Impl.fold (\k v s. s \ P k) t False = False" +by (induction t) auto + +lemma rbt_foldi_fold_conj: + "RBT_Impl.foldi (\s. s = True) (\k v s. s \ P k) t val = RBT_Impl.fold (\k v s. s \ P k) t val" +proof (induction t arbitrary: val) + case (Branch c t1) then show ?case + 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) + + +subsection {* foldi and Bex *} + +lemma Bex_True: "RBT_Impl.fold (\k v s. s \ P k) t True = True" +by (induction t) auto + +lemma rbt_foldi_fold_disj: + "RBT_Impl.foldi (\s. s = False) (\k v s. s \ P k) t val = RBT_Impl.fold (\k v s. s \ P k) t val" +proof (induction t arbitrary: val) + case (Branch c t1) then show ?case + 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) + + +subsection {* folding over non empty trees and selecting the minimal and maximal element *} + +(** concrete **) + +(* The concrete part is here because it's probably not general enough to be moved to RBT_Impl *) + +definition rbt_fold1_keys :: "('a \ 'a \ 'a) \ ('a::linorder, 'b) RBT_Impl.rbt \ 'a" + where "rbt_fold1_keys f t = List.fold f (tl(RBT_Impl.keys t)) (hd(RBT_Impl.keys t))" + +(* minimum *) + +definition rbt_min :: "('a::linorder, unit) RBT_Impl.rbt \ 'a" + where "rbt_min t = rbt_fold1_keys min t" + +lemma key_le_right: "rbt_sorted (Branch c lt k v rt) \ (\x. x \set (RBT_Impl.keys rt) \ k \ x)" +by (auto simp: rbt_greater_prop less_imp_le) + +lemma left_le_key: "rbt_sorted (Branch c lt k v rt) \ (\x. x \set (RBT_Impl.keys lt) \ x \ k)" +by (auto simp: rbt_less_prop less_imp_le) + +lemma fold_min_triv: + fixes k :: "_ :: linorder" + shows "(\x\set xs. k \ x) \ List.fold min xs k = k" +by (induct xs) (auto simp add: min_def) + +lemma rbt_min_simps: + "is_rbt (Branch c RBT_Impl.Empty k v rt) \ rbt_min (Branch c RBT_Impl.Empty k v rt) = k" +by (auto intro: fold_min_triv dest: key_le_right is_rbt_rbt_sorted simp: rbt_fold1_keys_def rbt_min_def) + +fun rbt_min_opt where + "rbt_min_opt (Branch c RBT_Impl.Empty k v rt) = k" | + "rbt_min_opt (Branch c (Branch lc llc lk lv lrt) k v rt) = rbt_min_opt (Branch lc llc lk lv lrt)" + +lemma rbt_min_opt_Branch: + "t1 \ rbt.Empty \ rbt_min_opt (Branch c t1 k () t2) = rbt_min_opt t1" +by (cases t1) auto + +lemma rbt_min_opt_induct [case_names empty left_empty left_non_empty]: + fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" + assumes "P rbt.Empty" + assumes "\color t1 a b t2. P t1 \ P t2 \ t1 = rbt.Empty \ P (Branch color t1 a b t2)" + assumes "\color t1 a b t2. P t1 \ P t2 \ t1 \ rbt.Empty \ P (Branch color t1 a b t2)" + shows "P t" +using assms + apply (induction t) + apply simp + apply (case_tac "t1 = rbt.Empty") + apply simp_all +done + +lemma rbt_min_opt_in_set: + fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" + assumes "t \ rbt.Empty" + shows "rbt_min_opt t \ set (RBT_Impl.keys t)" +using assms by (induction t rule: rbt_min_opt.induct) (auto) + +lemma rbt_min_opt_is_min: + fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" + assumes "rbt_sorted t" + assumes "t \ rbt.Empty" + shows "\y. y \ set (RBT_Impl.keys t) \ y \ rbt_min_opt t" +using assms +proof (induction t rule: rbt_min_opt_induct) + case empty + then show ?case by simp +next + case left_empty + then show ?case by (auto intro: key_le_right simp del: rbt_sorted.simps) +next + case (left_non_empty c t1 k v t2 y) + then have "y = k \ y \ set (RBT_Impl.keys t1) \ y \ set (RBT_Impl.keys t2)" by auto + with left_non_empty show ?case + proof(elim disjE) + case goal1 then show ?case + by (auto simp add: rbt_min_opt_Branch intro: left_le_key rbt_min_opt_in_set) + next + case goal2 with left_non_empty show ?case by (auto simp add: rbt_min_opt_Branch) + next + case goal3 show ?case + proof - + from goal3 have "rbt_min_opt t1 \ k" by (simp add: left_le_key rbt_min_opt_in_set) + moreover from goal3 have "k \ y" by (simp add: key_le_right) + ultimately show ?thesis using goal3 by (simp add: rbt_min_opt_Branch) + qed + qed +qed + +lemma rbt_min_eq_rbt_min_opt: + assumes "t \ RBT_Impl.Empty" + assumes "is_rbt t" + shows "rbt_min t = rbt_min_opt t" +proof - + interpret ab_semigroup_idem_mult "(min :: 'a \ 'a \ 'a)" using ab_semigroup_idem_mult_min + unfolding class.ab_semigroup_idem_mult_def by blast + show ?thesis + by (simp add: Min_eqI rbt_min_opt_is_min rbt_min_opt_in_set assms Min_def[symmetric] + non_empty_rbt_keys fold1_set_fold[symmetric] rbt_min_def rbt_fold1_keys_def) +qed + +(* maximum *) + +definition rbt_max :: "('a::linorder, unit) RBT_Impl.rbt \ 'a" + where "rbt_max t = rbt_fold1_keys max t" + +lemma fold_max_triv: + fixes k :: "_ :: linorder" + shows "(\x\set xs. x \ k) \ List.fold max xs k = k" +by (induct xs) (auto simp add: max_def) + +lemma fold_max_rev_eq: + fixes xs :: "('a :: linorder) list" + assumes "xs \ []" + shows "List.fold max (tl xs) (hd xs) = List.fold max (tl (rev xs)) (hd (rev xs))" +proof - + interpret ab_semigroup_idem_mult "(max :: 'a \ 'a \ 'a)" using ab_semigroup_idem_mult_max + unfolding class.ab_semigroup_idem_mult_def by blast + show ?thesis + using assms by (auto simp add: fold1_set_fold[symmetric]) +qed + +lemma rbt_max_simps: + assumes "is_rbt (Branch c lt k v RBT_Impl.Empty)" + shows "rbt_max (Branch c lt k v RBT_Impl.Empty) = k" +proof - + have "List.fold max (tl (rev(RBT_Impl.keys lt @ [k]))) (hd (rev(RBT_Impl.keys lt @ [k]))) = k" + using assms by (auto intro!: fold_max_triv dest!: left_le_key is_rbt_rbt_sorted) + then show ?thesis by (auto simp add: rbt_max_def rbt_fold1_keys_def fold_max_rev_eq) +qed + +fun rbt_max_opt where + "rbt_max_opt (Branch c lt k v RBT_Impl.Empty) = k" | + "rbt_max_opt (Branch c lt k v (Branch rc rlc rk rv rrt)) = rbt_max_opt (Branch rc rlc rk rv rrt)" + +lemma rbt_max_opt_Branch: + "t2 \ rbt.Empty \ rbt_max_opt (Branch c t1 k () t2) = rbt_max_opt t2" +by (cases t2) auto + +lemma rbt_max_opt_induct [case_names empty right_empty right_non_empty]: + fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" + assumes "P rbt.Empty" + assumes "\color t1 a b t2. P t1 \ P t2 \ t2 = rbt.Empty \ P (Branch color t1 a b t2)" + assumes "\color t1 a b t2. P t1 \ P t2 \ t2 \ rbt.Empty \ P (Branch color t1 a b t2)" + shows "P t" +using assms + apply (induction t) + apply simp + apply (case_tac "t2 = rbt.Empty") + apply simp_all +done + +lemma rbt_max_opt_in_set: + fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" + assumes "t \ rbt.Empty" + shows "rbt_max_opt t \ set (RBT_Impl.keys t)" +using assms by (induction t rule: rbt_max_opt.induct) (auto) + +lemma rbt_max_opt_is_max: + fixes t :: "('a :: linorder, unit) RBT_Impl.rbt" + assumes "rbt_sorted t" + assumes "t \ rbt.Empty" + shows "\y. y \ set (RBT_Impl.keys t) \ y \ rbt_max_opt t" +using assms +proof (induction t rule: rbt_max_opt_induct) + case empty + then show ?case by simp +next + case right_empty + then show ?case by (auto intro: left_le_key simp del: rbt_sorted.simps) +next + case (right_non_empty c t1 k v t2 y) + then have "y = k \ y \ set (RBT_Impl.keys t2) \ y \ set (RBT_Impl.keys t1)" by auto + with right_non_empty show ?case + proof(elim disjE) + case goal1 then show ?case + by (auto simp add: rbt_max_opt_Branch intro: key_le_right rbt_max_opt_in_set) + next + case goal2 with right_non_empty show ?case by (auto simp add: rbt_max_opt_Branch) + next + case goal3 show ?case + proof - + from goal3 have "rbt_max_opt t2 \ k" by (simp add: key_le_right rbt_max_opt_in_set) + moreover from goal3 have "y \ k" by (simp add: left_le_key) + ultimately show ?thesis using goal3 by (simp add: rbt_max_opt_Branch) + qed + qed +qed + +lemma rbt_max_eq_rbt_max_opt: + assumes "t \ RBT_Impl.Empty" + assumes "is_rbt t" + shows "rbt_max t = rbt_max_opt t" +proof - + interpret ab_semigroup_idem_mult "(max :: 'a \ 'a \ 'a)" using ab_semigroup_idem_mult_max + unfolding class.ab_semigroup_idem_mult_def by blast + show ?thesis + by (simp add: Max_eqI rbt_max_opt_is_max rbt_max_opt_in_set assms Max_def[symmetric] + non_empty_rbt_keys fold1_set_fold[symmetric] rbt_max_def rbt_fold1_keys_def) +qed + + +(** abstract **) + +lift_definition fold1_keys :: "('a \ 'a \ 'a) \ ('a::linorder, 'b) rbt \ 'a" + is rbt_fold1_keys by simp + +lemma fold1_keys_def_alt: + "fold1_keys f t = List.fold f (tl(keys t)) (hd(keys t))" + by transfer (simp add: rbt_fold1_keys_def) + +lemma finite_fold1_fold1_keys: + assumes "class.ab_semigroup_mult f" + assumes "\ (is_empty t)" + shows "Finite_Set.fold1 f (Set t) = fold1_keys f t" +proof - + interpret ab_semigroup_mult f by fact + show ?thesis using assms + by (auto simp: fold1_keys_def_alt set_keys fold_def_alt fold1_distinct_set_fold non_empty_keys) +qed + +(* minimum *) + +lift_definition r_min :: "('a :: linorder, unit) rbt \ 'a" is rbt_min by simp + +lift_definition r_min_opt :: "('a :: linorder, unit) rbt \ 'a" is rbt_min_opt by simp + +lemma r_min_alt_def: "r_min t = fold1_keys min t" +by transfer (simp add: rbt_min_def) + +lemma r_min_eq_r_min_opt: + assumes "\ (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)" + 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 = + List.fold min (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) top" + by (simp add: hd_Cons_tl[symmetric]) + { fix x :: "_ :: {linorder, bounded_lattice_top}" and xs + have "List.fold min (x#xs) top = List.fold min xs x" + by (simp add: inf_min[symmetric]) + } note ** = this + show ?thesis using assms + unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty + apply transfer + apply (case_tac t) + apply simp + apply (subst *) + apply simp + apply (subst **) + apply simp + done +qed + +(* maximum *) + +lift_definition r_max :: "('a :: linorder, unit) rbt \ 'a" is rbt_max by simp + +lift_definition r_max_opt :: "('a :: linorder, unit) rbt \ 'a" is rbt_max_opt by simp + +lemma r_max_alt_def: "r_max t = fold1_keys max t" +by transfer (simp add: rbt_max_def) + +lemma r_max_eq_r_max_opt: + assumes "\ (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)" + 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 = + List.fold max (hd(RBT_Impl.keys t) # tl(RBT_Impl.keys t)) bot" + by (simp add: hd_Cons_tl[symmetric]) + { fix x :: "_ :: {linorder, bounded_lattice_bot}" and xs + have "List.fold max (x#xs) bot = List.fold max xs x" + by (simp add: sup_max[symmetric]) + } note ** = this + show ?thesis using assms + unfolding fold_keys_def_alt fold1_keys_def_alt is_empty_empty + apply transfer + apply (case_tac t) + apply simp + apply (subst *) + apply simp + apply (subst **) + apply simp + done +qed + + +section {* Code equations *} + +code_datatype Set Coset + +lemma empty_Set [code]: + "Set.empty = Set RBT.empty" +by (auto simp: Set_def) + +lemma UNIV_Coset [code]: + "UNIV = Coset RBT.empty" +by (auto simp: Set_def) + +lemma is_empty_Set [code]: + "Set.is_empty (Set t) = RBT.is_empty t" + unfolding Set.is_empty_def by (auto simp: fun_eq_iff Set_def intro: lookup_empty_empty[THEN iffD1]) + +lemma compl_code [code]: + "- Set xs = Coset xs" + "- Coset xs = Set xs" +by (simp_all add: Set_def) + +lemma member_code [code]: + "x \ (Set t) = (RBT.lookup t x = Some ())" + "x \ (Coset t) = (RBT.lookup t x = None)" +by (simp_all add: Set_def) + +lemma insert_code [code]: + "Set.insert x (Set t) = Set (RBT.insert x () t)" + "Set.insert x (Coset t) = Coset (RBT.delete x t)" +by (auto simp: Set_def) + +lemma remove_code [code]: + "Set.remove x (Set t) = Set (RBT.delete x t)" + "Set.remove x (Coset t) = Coset (RBT.insert x () t)" +by (auto simp: Set_def) + +lemma union_Set [code]: + "Set t \ A = fold_keys Set.insert t A" +proof - + interpret comp_fun_idem Set.insert + by (fact comp_fun_idem_insert) + from finite_fold_fold_keys[OF `comp_fun_commute Set.insert`] + show ?thesis by (auto simp add: union_fold_insert) +qed + +lemma inter_Set [code]: + "A \ Set t = rbt_filter (\k. k \ A) t" +by (simp add: inter_filter finite_filter_rbt_filter) + +lemma minus_Set [code]: + "A - Set t = fold_keys Set.remove t A" +proof - + interpret comp_fun_idem Set.remove + by (fact comp_fun_idem_remove) + from finite_fold_fold_keys[OF `comp_fun_commute Set.remove`] + show ?thesis by (auto simp add: minus_fold_remove) +qed + +lemma union_Coset [code]: + "Coset t \ A = - rbt_filter (\k. k \ A) t" +proof - + have *: "\A B. (-A \ B) = -(-B \ A)" by blast + show ?thesis by (simp del: boolean_algebra_class.compl_inf add: * inter_Set) +qed + +lemma union_Set_Set [code]: + "Set t1 \ Set t2 = Set (union t1 t2)" +by (auto simp add: lookup_union map_add_Some_iff Set_def) + +lemma inter_Coset [code]: + "A \ Coset t = fold_keys Set.remove t A" +by (simp add: Diff_eq [symmetric] minus_Set) + +lemma inter_Coset_Coset [code]: + "Coset t1 \ Coset t2 = Coset (union t1 t2)" +by (auto simp add: lookup_union map_add_Some_iff Set_def) + +lemma minus_Coset [code]: + "A - Coset t = rbt_filter (\k. k \ A) t" +by (simp add: inter_Set[simplified Int_commute]) + +lemma project_Set [code]: + "Set.project P (Set t) = (rbt_filter P t)" +by (auto simp add: project_filter finite_filter_rbt_filter) + +lemma image_Set [code]: + "image f (Set t) = fold_keys (\k A. Set.insert (f k) A) t {}" +proof - + have "comp_fun_commute (\k. Set.insert (f k))" by default auto + then show ?thesis by (auto simp add: image_fold_insert intro!: finite_fold_fold_keys) +qed + +lemma Ball_Set [code]: + "Ball (Set t) P \ 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 + by (simp add: foldi_fold_conj[symmetric] Ball_fold finite_fold_fold_keys) +qed + +lemma Bex_Set [code]: + "Bex (Set t) P \ 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 + by (simp add: foldi_fold_disj[symmetric] Bex_fold finite_fold_fold_keys) +qed + +lemma subset_code [code]: + "Set t \ B \ (\x\Set t. x \ B)" + "A \ Coset t \ (\y\Set t. y \ A)" +by auto + +definition non_empty_trees where [code del]: "non_empty_trees t1 t2 \ Coset t1 \ Set t2" + +code_abort non_empty_trees + +lemma subset_Coset_empty_Set_empty [code]: + "Coset t1 \ Set t2 \ (case (impl_of t1, impl_of t2) of + (rbt.Empty, rbt.Empty) => False | + (_, _) => non_empty_trees t1 t2)" +proof - + have *: "\t. 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 + by (auto simp: Set_def lookup.abs_eq[OF **] dest!: * split: rbt.split simp: non_empty_trees_def) +qed + +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" +by (simp add: subset_code Ball_Set) + +lemma card_Set [code]: + "card (Set t) = fold_keys (\_ n. n + 1) t 0" +by (auto simp add: card_def fold_image_def intro!: finite_fold_fold_keys) (default, simp) + +lemma setsum_Set [code]: + "setsum f (Set xs) = fold_keys (plus o f) xs 0" +proof - + have "comp_fun_commute (\x. op + (f x))" by default (auto simp: add_ac) + then show ?thesis + by (auto simp add: setsum_def fold_image_def finite_fold_fold_keys o_def) +qed + +definition not_a_singleton_tree where [code del]: "not_a_singleton_tree x y = x y" + +code_abort not_a_singleton_tree + +lemma the_elem_set [code]: + fixes t :: "('a :: linorder, unit) rbt" + shows "the_elem (Set t) = (case impl_of t of + (Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty) \ x + | _ \ not_a_singleton_tree the_elem (Set t))" +proof - + { + fix x :: "'a :: linorder" + let ?t = "Branch RBT_Impl.B RBT_Impl.Empty x () RBT_Impl.Empty" + 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" + by (subst(asm) RBT_inverse[symmetric, OF *]) + (auto simp: Set_def the_elem_def lookup.abs_eq[OF **] impl_of_inject) + } + then show ?thesis unfolding not_a_singleton_tree_def + by(auto split: rbt.split unit.split color.split) +qed + +lemma Pow_Set [code]: + "Pow (Set t) = fold_keys (\x A. A \ Set.insert x ` A) t {{}}" +by (simp add: Pow_fold finite_fold_fold_keys[OF comp_fun_commute_Pow_fold]) + +lemma product_Set [code]: + "Product_Type.product (Set t1) (Set t2) = + fold_keys (\x A. fold_keys (\y. Set.insert (x, y)) t2 A) t1 {}" +proof - + have *:"\x. comp_fun_commute (\y. Set.insert (x, y))" by default auto + show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_product_fold, of "Set t2" "{}" "t1"] + by (simp add: product_fold Product_Type.product_def finite_fold_fold_keys[OF *]) +qed + +lemma Id_on_Set [code]: + "Id_on (Set t) = fold_keys (\x. Set.insert (x, x)) t {}" +proof - + have "comp_fun_commute (\x. Set.insert (x, x))" by default auto + then show ?thesis + by (auto simp add: Id_on_fold intro!: finite_fold_fold_keys) +qed + +lemma Image_Set [code]: + "(Set t) `` S = fold_keys (\(x,y) A. if x \ S then Set.insert y A else A) t {}" +by (auto simp add: Image_fold finite_fold_fold_keys[OF comp_fun_commute_Image_fold]) + +lemma trancl_set_ntrancl [code]: + "trancl (Set t) = ntrancl (card (Set t) - 1) (Set t)" +by (simp add: finite_trancl_ntranl) + +lemma relcomp_Set[code]: + "(Set t1) O (Set t2) = fold_keys + (\(x,y) A. fold_keys (\(w,z) A'. if y = w then Set.insert (x,z) A' else A') t2 A) t1 {}" +proof - + interpret comp_fun_idem Set.insert by (fact comp_fun_idem_insert) + have *: "\x y. comp_fun_commute (\(w, z) A'. if y = w then Set.insert (x, z) A' else A')" + by default (auto simp add: fun_eq_iff) + show ?thesis using finite_fold_fold_keys[OF comp_fun_commute_relcomp_fold, of "Set t2" "{}" t1] + by (simp add: relcomp_fold finite_fold_fold_keys[OF *]) +qed + +lemma wf_set [code]: + "wf (Set t) = acyclic (Set t)" +by (simp add: wf_iff_acyclic_if_finite) + +definition not_non_empty_tree where [code del]: "not_non_empty_tree x y = x y" + +code_abort not_non_empty_tree + +lemma Min_fin_set_fold [code]: + "Min (Set t) = (if is_empty t then not_non_empty_tree Min (Set t) else r_min_opt t)" +proof - + have *:"(class.ab_semigroup_mult (min :: 'a \ 'a \ 'a))" using ab_semigroup_idem_mult_min + unfolding class.ab_semigroup_idem_mult_def by blast + show ?thesis + by (auto simp add: Min_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_min_alt_def + r_min_eq_r_min_opt[symmetric]) +qed + +lemma Inf_fin_set_fold [code]: + "Inf_fin (Set t) = Min (Set t)" +by (simp add: inf_min Inf_fin_def Min_def) + +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)" +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" + 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) +qed + +definition Inf' :: "'a :: {linorder, complete_lattice} set \ 'a" where [code del]: "Inf' x = Inf x" +declare Inf'_def[symmetric, code_unfold] +declare Inf_Set_fold[folded Inf'_def, code] + +lemma INFI_Set_fold [code]: + "INFI (Set t) f = fold_keys (inf \ f) t top" +proof - + have "comp_fun_commute ((inf :: 'a \ 'a \ 'a) \ f)" + by default (auto simp add: fun_eq_iff ac_simps) + then show ?thesis + by (auto simp: INF_fold_inf finite_fold_fold_keys) +qed + +lemma Max_fin_set_fold [code]: + "Max (Set t) = (if is_empty t then not_non_empty_tree Max (Set t) else r_max_opt t)" +proof - + have *:"(class.ab_semigroup_mult (max :: 'a \ 'a \ 'a))" using ab_semigroup_idem_mult_max + unfolding class.ab_semigroup_idem_mult_def by blast + show ?thesis + by (auto simp add: Max_def not_non_empty_tree_def finite_fold1_fold1_keys[OF *] r_max_alt_def + r_max_eq_r_max_opt[symmetric]) +qed + +lemma Sup_fin_set_fold [code]: + "Sup_fin (Set t) = Max (Set t)" +by (simp add: sup_max Sup_fin_def Max_def) + +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)" +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" + 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) +qed + +definition Sup' :: "'a :: {linorder, complete_lattice} set \ 'a" where [code del]: "Sup' x = Sup x" +declare Sup'_def[symmetric, code_unfold] +declare Sup_Set_fold[folded Sup'_def, code] + +lemma SUPR_Set_fold [code]: + "SUPR (Set t) f = fold_keys (sup \ f) t bot" +proof - + have "comp_fun_commute ((sup :: 'a \ 'a \ 'a) \ f)" + by default (auto simp add: fun_eq_iff ac_simps) + then show ?thesis + by (auto simp: SUP_fold_sup finite_fold_fold_keys) +qed + +lemma sorted_list_set[code]: + "sorted_list_of_set (Set t) = keys t" +by (auto simp add: set_keys intro: sorted_distinct_set_unique) + +hide_const (open) RBT_Set.Set RBT_Set.Coset + +end