diff --git a/thys/Containers/Lexicographic_Order.thy b/thys/Containers/Lexicographic_Order.thy --- a/thys/Containers/Lexicographic_Order.thy +++ b/thys/Containers/Lexicographic_Order.thy @@ -1,92 +1,92 @@ (* Title: Containers/Lexicographic_Order.thy Author: Andreas Lochbihler, KIT *) theory Lexicographic_Order imports List_Fusion "HOL-Library.Char_ord" begin hide_const (open) List.lexordp section \List fusion for lexicographic order\ context linorder begin lemma lexordp_take_index_conv: "lexordp xs ys \ (length xs < length ys \ take (length xs) ys = xs) \ (\i < min (length xs) (length ys). take i xs = take i ys \ xs ! i < ys ! i)" (is "?lhs = ?rhs") proof assume ?lhs thus ?rhs by induct (auto 4 3 del: disjCI intro: disjI2 exI[where x="Suc i" for i]) next assume ?rhs (is "?prefix \ ?less") thus ?lhs proof assume "?prefix" hence "ys = xs @ hd (drop (length xs) ys) # tl (drop (length xs) ys)" by (metis append_Nil2 append_take_drop_id less_not_refl list.collapse) thus ?thesis unfolding lexordp_iff by blast next assume "?less" then obtain i where "i < min (length xs) (length ys)" and "take i xs = take i ys" and nth: "xs ! i < ys ! i" by blast hence "xs = take i xs @ xs ! i # drop (Suc i) xs" "ys = take i xs @ ys ! i # drop (Suc i) ys" by -(subst append_take_drop_id[symmetric, of _ i], simp_all add: Cons_nth_drop_Suc) with nth show ?thesis unfolding lexordp_iff by blast qed qed \ \lexord is extension of partial ordering List.lex\ lemma lexordp_lex: "(xs, ys) \ lex {(xs, ys). xs < ys} \ lexordp xs ys \ length xs = length ys" proof(induct xs arbitrary: ys) case Nil thus ?case by clarsimp next case Cons thus ?case by(cases ys)(simp_all, safe, simp) qed -end +end subsection \Setup for list fusion\ -context order begin +context ord begin definition lexord_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 's1 \ 's2 \ bool" where [code del]: "lexord_fusion g1 g2 s1 s2 = lexordp (list.unfoldr g1 s1) (list.unfoldr g2 s2)" definition lexord_eq_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 's1 \ 's2 \ bool" where [code del]: "lexord_eq_fusion g1 g2 s1 s2 = lexordp_eq (list.unfoldr g1 s1) (list.unfoldr g2 s2)" lemma lexord_fusion_code: "lexord_fusion g1 g2 s1 s2 \ (if list.has_next g1 s1 then if list.has_next g2 s2 then let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in x < y \ \ y < x \ lexord_fusion g1 g2 s1' s2' else False else list.has_next g2 s2)" unfolding lexord_fusion_def by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm) lemma lexord_eq_fusion_code: "lexord_eq_fusion g1 g2 s1 s2 \ (list.has_next g1 s1 \ list.has_next g2 s2 \ (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in x < y \ \ y < x \ lexord_eq_fusion g1 g2 s1' s2'))" unfolding lexord_eq_fusion_def by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm) end lemmas [code] = - lexord_fusion_code order.lexord_fusion_code - lexord_eq_fusion_code order.lexord_eq_fusion_code + lexord_fusion_code ord.lexord_fusion_code + lexord_eq_fusion_code ord.lexord_eq_fusion_code lemmas [symmetric, code_unfold] = - lexord_fusion_def order.lexord_fusion_def - lexord_eq_fusion_def order.lexord_eq_fusion_def + lexord_fusion_def ord.lexord_fusion_def + lexord_eq_fusion_def ord.lexord_eq_fusion_def end diff --git a/thys/Containers/List_Proper_Interval.thy b/thys/Containers/List_Proper_Interval.thy --- a/thys/Containers/List_Proper_Interval.thy +++ b/thys/Containers/List_Proper_Interval.thy @@ -1,66 +1,71 @@ (* Title: Containers/List_Proper_Interval.thy Author: Andreas Lochbihler, ETH Zurich *) theory List_Proper_Interval imports "HOL-Library.List_Lexorder" Collection_Order begin section \Instantiate @{class proper_interval} of for @{typ "'a list"}\ lemma Nil_less_conv_neq_Nil: "[] < xs \ xs \ []" by(cases xs) simp_all lemma less_append_same_iff: fixes xs :: "'a :: preorder list" shows "xs < xs @ ys \ [] < ys" by(induct xs) simp_all lemma less_append_same2_iff: fixes xs :: "'a :: preorder list" shows "xs @ ys < xs @ zs \ ys < zs" by(induct xs) simp_all lemma Cons_less_iff: fixes x :: "'a :: preorder" shows "x # xs < ys \ (\y ys'. ys = y # ys' \ (x < y \ x = y \ xs < ys'))" by(cases ys) auto instantiation list :: ("{proper_interval, order}") proper_interval begin definition proper_interval_list_aux :: "'a list \ 'a list \ bool" where proper_interval_list_aux_correct: "proper_interval_list_aux xs ys \ (\zs. xs < zs \ zs < ys)" -lemma proper_interval_list_aux_simps [code]: +lemma proper_interval_list_aux_simp_1: "proper_interval_list_aux xs [] \ False" + by (simp add: proper_interval_list_aux_correct) + +lemma proper_interval_list_aux_simp_2: "proper_interval_list_aux [] (y # ys) \ ys \ [] \ proper_interval None (Some y)" - "proper_interval_list_aux (x # xs) (y # ys) \ x < y \ x = y \ proper_interval_list_aux xs ys" -apply(simp_all add: proper_interval_list_aux_correct proper_interval_simps Nil_less_conv_neq_Nil) - apply(fastforce simp add: neq_Nil_conv) -apply(rule iffI) - apply(fastforce simp add: Cons_less_iff intro: less_trans) -apply(erule disjE) - apply(rule exI[where x="x # xs @ [undefined]"]) - apply(simp add: less_append_same_iff) -apply(auto 4 3 simp add: Cons_less_iff) -done + apply(auto simp add: proper_interval_list_aux_correct proper_interval_simps Nil_less_conv_neq_Nil) + apply (metis Cons_less_Cons neq_Nil_conv not_less_Nil) + by (metis Cons_less_Cons Nil_less_Cons neq_Nil_conv) + +lemma proper_interval_list_aux_simp_3: + "proper_interval_list_aux (x # xs) (y # ys) \ (if x = y then proper_interval_list_aux xs ys else x < y)" + apply(auto simp add: proper_interval_list_aux_correct proper_interval_simps Nil_less_conv_neq_Nil Cons_less_iff) + apply fastforce + by (metis Cons_less_Cons Nil_less_Cons less_append_same_iff) + +lemmas proper_interval_list_aux_simps [code] = + proper_interval_list_aux_simp_1 proper_interval_list_aux_simp_2 proper_interval_list_aux_simp_3 fun proper_interval_list :: "'a list option \ 'a list option \ bool" where "proper_interval_list None None \ True" | "proper_interval_list None (Some xs) \ (xs \ [])" | "proper_interval_list (Some xs) None \ True" | "proper_interval_list (Some xs) (Some ys) \ proper_interval_list_aux xs ys" instance proof(intro_classes) fix xs ys :: "'a list" show "proper_interval None (Some ys) \ (\zs. zs < ys)" by(auto simp add: Nil_less_conv_neq_Nil intro: exI[where x="[]"]) show "proper_interval (Some xs) None \ (\zs. xs < zs)" by(simp add: exI[where x="xs @ [undefined]"] less_append_same_iff) show "proper_interval (Some xs) (Some ys) \ (\zs. xs < zs \ zs < ys)" by(simp add: proper_interval_list_aux_correct) qed simp end end diff --git a/thys/Containers/Set_Impl.thy b/thys/Containers/Set_Impl.thy --- a/thys/Containers/Set_Impl.thy +++ b/thys/Containers/Set_Impl.thy @@ -1,2066 +1,2064 @@ (* Title: Containers/Set_Impl.thy Author: Andreas Lochbihler, KIT René Thiemann, UIBK *) theory Set_Impl imports Collection_Enum DList_Set RBT_Set2 Closure_Set Containers_Generator Complex_Main begin section \Different implementations of sets\ subsection \Auxiliary functions\ text \A simple quicksort implementation\ context ord begin function (sequential) quicksort_acc :: "'a list \ 'a list \ 'a list" and quicksort_part :: "'a list \ 'a \ 'a list \ 'a list \ 'a list \ 'a list \ 'a list" where "quicksort_acc ac [] = ac" | "quicksort_acc ac [x] = x # ac" | "quicksort_acc ac (x # xs) = quicksort_part ac x [] [] [] xs" | "quicksort_part ac x lts eqs gts [] = quicksort_acc (eqs @ x # quicksort_acc ac gts) lts" | "quicksort_part ac x lts eqs gts (z # zs) = (if z > x then quicksort_part ac x lts eqs (z # gts) zs else if z < x then quicksort_part ac x (z # lts) eqs gts zs else quicksort_part ac x lts (z # eqs) gts zs)" by pat_completeness simp_all lemma length_quicksort_accp: "quicksort_acc_quicksort_part_dom (Inl (ac, xs)) \ length (quicksort_acc ac xs) = length ac + length xs" and length_quicksort_partp: "quicksort_acc_quicksort_part_dom (Inr (ac, x, lts, eqs, gts, zs)) \ length (quicksort_part ac x lts eqs gts zs) = length ac + 1 + length lts + length eqs + length gts + length zs" apply(induct rule: quicksort_acc_quicksort_part.pinduct) apply(simp_all add: quicksort_acc.psimps quicksort_part.psimps) done termination apply(relation "measure (case_sum (\(_, xs). 2 * length xs ^ 2) (\(_, _, lts, eqs, gts, zs). 2 * (length lts + length eqs + length gts + length zs) ^ 2 + length zs + 1))") apply(simp_all add: power2_eq_square add_mult_distrib add_mult_distrib2 length_quicksort_accp) done definition quicksort :: "'a list \ 'a list" where "quicksort = quicksort_acc []" lemma set_quicksort_acc [simp]: "set (quicksort_acc ac xs) = set ac \ set xs" and set_quicksort_part [simp]: "set (quicksort_part ac x lts eqs gts zs) = set ac \ {x} \ set lts \ set eqs \ set gts \ set zs" by(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct)(auto split: if_split_asm) lemma set_quicksort [simp]: "set (quicksort xs) = set xs" by(simp add: quicksort_def) lemma distinct_quicksort_acc: "distinct (quicksort_acc ac xs) = distinct (ac @ xs)" and distinct_quicksort_part: "distinct (quicksort_part ac x lts eqs gts zs) = distinct (ac @ [x] @ lts @ eqs @ gts @ zs)" by(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct) auto lemma distinct_quicksort [simp]: "distinct (quicksort xs) = distinct xs" by(simp add: quicksort_def distinct_quicksort_acc) end lemmas [code] = ord.quicksort_acc.simps quicksort_acc.simps ord.quicksort_part.simps quicksort_part.simps ord.quicksort_def quicksort_def context linorder begin lemma sorted_quicksort_acc: "\ sorted ac; \x \ set xs. \a \ set ac. x < a \ \ sorted (quicksort_acc ac xs)" and sorted_quicksort_part: "\ sorted ac; \y \ set lts \ {x} \ set eqs \ set gts \ set zs. \a \ set ac. y < a; \y \ set lts. y < x; \y \ set eqs. y = x; \y \ set gts. y > x \ \ sorted (quicksort_part ac x lts eqs gts zs)" proof(induction ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct) case 1 thus ?case by simp next case 2 thus ?case by(auto) next case 3 thus ?case by simp next case (4 ac x lts eqs gts) note ac_greater = \\y\set lts \ {x} \ set eqs \ set gts \ set []. \a\set ac. y < a\ have "sorted eqs" "set eqs \ {x}" using \\y\set eqs. y = x\ by(induct eqs)(simp_all) moreover have "\y \ set ac \ set gts. x \ y" using \\a\set gts. x < a\ ac_greater by auto moreover have "sorted (quicksort_acc ac gts)" using \sorted ac\ ac_greater by(auto intro: "4.IH") ultimately have "sorted (eqs @ x # quicksort_acc ac gts)" by(auto simp add: sorted_append) moreover have "\y\set lts. \a\set (eqs @ x # quicksort_acc ac gts). y < a" using \\y\set lts. y < x\ ac_greater \\a\set gts. x < a\ \\y\set eqs. y = x\ by fastforce ultimately show ?case by(simp add: "4.IH") next case 5 thus ?case by(simp add: not_less eq_iff) qed lemma sorted_quicksort [simp]: "sorted (quicksort xs)" by(simp add: quicksort_def sorted_quicksort_acc) lemma insort_key_append1: "\y \ set ys. f x < f y \ insort_key f x (xs @ ys) = insort_key f x xs @ ys" proof(induct xs) case Nil thus ?case by(cases ys) auto qed simp lemma insort_key_append2: "\y \ set xs. f x > f y \ insort_key f x (xs @ ys) = xs @ insort_key f x ys" by(induct xs) auto lemma sort_key_append: "\x\set xs. \y\set ys. f x < f y \ sort_key f (xs @ ys) = sort_key f xs @ sort_key f ys" by(induct xs)(simp_all add: insort_key_append1) definition single_list :: "'a \ 'a list" where "single_list a = [a]" lemma to_single_list: "x # xs = single_list x @ xs" by(simp add: single_list_def) lemma sort_snoc: "sort (xs @ [x]) = insort x (sort xs)" by(induct xs)(simp_all add: insort_left_comm) lemma sort_append_swap: "sort (xs @ ys) = sort (ys @ xs)" by(induct xs arbitrary: ys rule: rev_induct)(simp_all add: sort_snoc[symmetric]) lemma sort_append_swap2: "sort (xs @ ys @ zs) = sort (ys @ xs @ zs)" by(induct xs)(simp_all, subst (1 2) sort_append_swap, simp) lemma sort_Cons_append_swap: "sort (x # xs) = sort (xs @ [x])" by(subst sort_append_swap) simp lemma sort_append_Cons_swap: "sort (ys @ x # xs) = sort (ys @ xs @ [x])" apply(induct ys) apply(simp only: append.simps sort_Cons_append_swap) apply simp done lemma quicksort_acc_conv_sort: "quicksort_acc ac xs = sort xs @ ac" and quicksort_part_conv_sort: "\ \y \ set lts. y < x; \y \ set eqs. y = x; \y \ set gts. y > x \ \ quicksort_part ac x lts eqs gts zs = sort (lts @ eqs @ gts @ x # zs) @ ac" proof(induct ac xs and ac x lts eqs gts zs rule: quicksort_acc_quicksort_part.induct) case 1 thus ?case by simp next case 2 thus ?case by simp next case 3 thus ?case by simp next case (4 ac x lts eqs gts) note eqs = \\y\set eqs. y = x\ { fix eqs assume "\y\set eqs. y = x" hence "insort x eqs = x # eqs" by(induct eqs) simp_all } note [simp] = this from eqs have [simp]: "sort eqs = eqs" by(induct eqs) simp_all from eqs have [simp]: "eqs @ [x] = x # eqs" by(induct eqs) simp_all show ?case using 4 apply(subst sort_key_append) apply(auto 4 3 dest: bspec)[1] apply(simp add: append_assoc[symmetric] sort_snoc del: append_assoc) apply(subst sort_key_append) apply(auto 4 3 simp add: insort_key_append1 dest: bspec) done next case (5 ac x lts eqs gts z zs) have "\ \ z < x; \ x < z \ \ z = x" by simp thus ?case using 5 apply(simp del: sort_key_simps) apply(safe, simp_all del: sort_key_simps add: to_single_list) apply(subst sort_append_swap) apply(fold append_assoc) apply(subst (2) sort_append_swap) apply(subst sort_append_swap2) apply(unfold append_assoc) apply(rule refl) apply(subst (1 5) append_assoc[symmetric]) apply(subst (1 2) sort_append_swap) apply(unfold append_assoc) apply(subst sort_append_swap2) apply(subst (1 2) sort_append_swap) apply(unfold append_assoc) apply(subst sort_append_swap2) apply(rule refl) apply(subst (2 6) append_assoc[symmetric]) apply(subst (2 5) append_assoc[symmetric]) apply(subst (1 2) sort_append_swap2) apply(subst (4) append_assoc) apply(subst (2) sort_append_swap2) apply simp done qed lemma quicksort_conv_sort: "quicksort xs = sort xs" by(simp add: quicksort_def quicksort_acc_conv_sort) lemma sort_remdups: "sort (remdups xs) = remdups (sort xs)" by(rule sorted_distinct_set_unique) simp_all end text \Removing duplicates from a sorted list\ context ord begin fun remdups_sorted :: "'a list \ 'a list" where "remdups_sorted [] = []" | "remdups_sorted [x] = [x]" | "remdups_sorted (x#y#xs) = (if x < y then x # remdups_sorted (y#xs) else remdups_sorted (y#xs))" end lemmas [code] = ord.remdups_sorted.simps context linorder begin lemma [simp]: assumes "sorted xs" shows sorted_remdups_sorted: "sorted (remdups_sorted xs)" and set_remdups_sorted: "set (remdups_sorted xs) = set xs" using assms by(induct xs rule: remdups_sorted.induct)(auto) lemma distinct_remdups_sorted [simp]: "sorted xs \ distinct (remdups_sorted xs)" by(induct xs rule: remdups_sorted.induct)(auto) lemma remdups_sorted_conv_remdups: "sorted xs \ remdups_sorted xs = remdups xs" by(induct xs rule: remdups_sorted.induct)(auto) end text \An specialised operation to convert a finite set into a sorted list\ definition csorted_list_of_set :: "'a :: ccompare set \ 'a list" where [code del]: "csorted_list_of_set A = (if ID CCOMPARE('a) = None \ \ finite A then undefined else linorder.sorted_list_of_set cless_eq A)" lemma csorted_list_of_set_set [simp]: "\ ID CCOMPARE('a :: ccompare) = Some c; linorder.sorted (le_of_comp c) xs; distinct xs \ \ linorder.sorted_list_of_set (le_of_comp c) (set xs) = xs" by(simp add: distinct_remdups_id linorder.sorted_list_of_set_sort_remdups[OF ID_ccompare] linorder.sorted_sort_id[OF ID_ccompare]) lemma csorted_list_of_set_split: fixes A :: "'a :: ccompare set" shows "P (csorted_list_of_set A) \ (\xs. ID CCOMPARE('a) \ None \ finite A \ A = set xs \ distinct xs \ linorder.sorted cless_eq xs \ P xs) \ (ID CCOMPARE('a) = None \ \ finite A \ P undefined)" by(auto simp add: csorted_list_of_set_def linorder.sorted_list_of_set[OF ID_ccompare]) code_identifier code_module Set \ (SML) Set_Impl | code_module Set_Impl \ (SML) Set_Impl subsection \Delete code equation with set as constructor\ lemma is_empty_unfold [code_unfold]: "set_eq A {} = Set.is_empty A" "set_eq {} A = Set.is_empty A" by(auto simp add: Set.is_empty_def set_eq_def) definition is_UNIV :: "'a set \ bool" where [code del]: "is_UNIV A \ A = UNIV" lemma is_UNIV_unfold [code_unfold]: "A = UNIV \ is_UNIV A" "UNIV = A \ is_UNIV A" "set_eq A UNIV \ is_UNIV A" "set_eq UNIV A \ is_UNIV A" by(auto simp add: is_UNIV_def set_eq_def) lemma [code_unfold del, symmetric, code_post del]: "x \ set xs \ List.member xs x" by(simp add: List.member_def) lemma [code_unfold del, symmetric, code_post del]: "finite \ Cardinality.finite'" by(simp) lemma [code_unfold del, symmetric, code_post del]: "card \ Cardinality.card'" by simp declare [[code drop: Set.empty Set.is_empty uminus_set_inst.uminus_set Set.member Set.insert Set.remove UNIV Set.filter image Set.subset_eq Ball Bex Set.union minus_set_inst.minus_set Set.inter card Set.bind the_elem Pow sum Gcd Lcm Product_Type.product Id_on Image trancl relcomp wf Min Inf_fin Max Sup_fin "Inf :: 'a set set \ 'a set" "Sup :: 'a set set \ 'a set" sorted_list_of_set List.map_project Sup_pred_inst.Sup_pred finite Cardinality.finite' card Cardinality.card' Inf_pred_inst.Inf_pred pred_of_set Cardinality.subset' Cardinality.eq_set Wellfounded.acc Bleast can_select "set_eq :: 'a set \ 'a set \ bool" irrefl bacc set_of_pred set_of_seq ]] declare Cardinality.finite'_def[code] Cardinality.card'_def[code] subsection \Set implementations\ definition Collect_set :: "('a \ bool) \ 'a set" where [simp]: "Collect_set = Collect" definition DList_set :: "'a :: ceq set_dlist \ 'a set" where "DList_set = Collect o DList_Set.member" definition RBT_set :: "'a :: ccompare set_rbt \ 'a set" where "RBT_set = Collect o RBT_Set2.member" definition Complement :: "'a set \ 'a set" where [simp]: "Complement A = - A" definition Set_Monad :: "'a list \ 'a set" where [simp]: "Set_Monad = set" code_datatype Collect_set DList_set RBT_set Set_Monad Complement lemma DList_set_empty [simp]: "DList_set DList_Set.empty = {}" by(simp add: DList_set_def) lemma RBT_set_empty [simp]: "RBT_set RBT_Set2.empty = {}" by(simp add: RBT_set_def) lemma RBT_set_conv_keys: "ID CCOMPARE('a :: ccompare) \ None \ RBT_set (t :: 'a set_rbt) = set (RBT_Set2.keys t)" by(clarsimp simp add: RBT_set_def member_conv_keys) subsection \Set operations\ text \ A collection of all the theorems about @{const Complement}. \ ML \ structure Set_Complement_Eqs = Named_Thms ( val name = @{binding set_complement_code} val description = "Code equations involving set complement" ) \ setup \Set_Complement_Eqs.setup\ text \Various fold operations over sets\ typedef ('a, 'b) comp_fun_commute = "{f :: 'a \ 'b \ 'b. comp_fun_commute f}" morphisms comp_fun_commute_apply Abs_comp_fun_commute by(rule exI[where x="\_. id"])(simp, unfold_locales, auto) setup_lifting type_definition_comp_fun_commute lemma comp_fun_commute_apply' [simp]: "comp_fun_commute (comp_fun_commute_apply f)" using comp_fun_commute_apply[of f] by simp lift_definition set_fold_cfc :: "('a, 'b) comp_fun_commute \ 'b \ 'a set \ 'b" is "Finite_Set.fold" . declare [[code drop: set_fold_cfc]] lemma set_fold_cfc_code [code]: fixes xs :: "'a :: ceq list" and dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows set_fold_cfc_Complement[set_complement_code]: "set_fold_cfc f''' b (Complement A) = Code.abort (STR ''set_fold_cfc not supported on Complement'') (\_. set_fold_cfc f''' b (Complement A))" and "set_fold_cfc f''' b (Collect_set P) = Code.abort (STR ''set_fold_cfc not supported on Collect_set'') (\_. set_fold_cfc f''' b (Collect_set P))" "set_fold_cfc f b (Set_Monad xs) = (case ID CEQ('a) of None \ Code.abort (STR ''set_fold_cfc Set_Monad: ceq = None'') (\_. set_fold_cfc f b (Set_Monad xs)) | Some eq \ List.fold (comp_fun_commute_apply f) (equal_base.list_remdups eq xs) b)" (is ?Set_Monad) "set_fold_cfc f' b (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''set_fold_cfc DList_set: ceq = None'') (\_. set_fold_cfc f' b (DList_set dxs)) | Some _ \ DList_Set.fold (comp_fun_commute_apply f') dxs b)" (is ?DList_set) "set_fold_cfc f'' b (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''set_fold_cfc RBT_set: ccompare = None'') (\_. set_fold_cfc f'' b (RBT_set rbt)) | Some _ \ RBT_Set2.fold (comp_fun_commute_apply f'') rbt b)" (is ?RBT_set) proof - show ?Set_Monad by(auto split: option.split dest!: Collection_Eq.ID_ceq simp add: set_fold_cfc_def comp_fun_commute.fold_set_fold_remdups) show ?DList_set apply(auto split: option.split simp add: DList_set_def) apply transfer apply(auto dest: Collection_Eq.ID_ceq simp add: List.member_def[abs_def] comp_fun_commute.fold_set_fold_remdups distinct_remdups_id) done show ?RBT_set apply(auto split: option.split simp add: RBT_set_conv_keys fold_conv_fold_keys) apply transfer apply(simp add: comp_fun_commute.fold_set_fold_remdups distinct_remdups_id linorder.distinct_keys[OF ID_ccompare] ord.is_rbt_rbt_sorted) done qed simp_all typedef ('a, 'b) comp_fun_idem = "{f :: 'a \ 'b \ 'b. comp_fun_idem f}" morphisms comp_fun_idem_apply Abs_comp_fun_idem by(rule exI[where x="\_. id"])(simp, unfold_locales, auto) setup_lifting type_definition_comp_fun_idem lemma comp_fun_idem_apply' [simp]: "comp_fun_idem (comp_fun_idem_apply f)" using comp_fun_idem_apply[of f] by simp lift_definition set_fold_cfi :: "('a, 'b) comp_fun_idem \ 'b \ 'a set \ 'b" is "Finite_Set.fold" . declare [[code drop: set_fold_cfi]] lemma set_fold_cfi_code [code]: fixes xs :: "'a list" and dxs :: "'b :: ceq set_dlist" and rbt :: "'c :: ccompare set_rbt" shows "set_fold_cfi f b (Complement A) = Code.abort (STR ''set_fold_cfi not supported on Complement'') (\_. set_fold_cfi f b (Complement A))" "set_fold_cfi f b (Collect_set P) = Code.abort (STR ''set_fold_cfi not supported on Collect_set'') (\_. set_fold_cfi f b (Collect_set P))" "set_fold_cfi f b (Set_Monad xs) = List.fold (comp_fun_idem_apply f) xs b" (is ?Set_Monad) "set_fold_cfi f' b (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''set_fold_cfi DList_set: ceq = None'') (\_. set_fold_cfi f' b (DList_set dxs)) | Some _ \ DList_Set.fold (comp_fun_idem_apply f') dxs b)" (is ?DList_set) "set_fold_cfi f'' b (RBT_set rbt) = (case ID CCOMPARE('c) of None \ Code.abort (STR ''set_fold_cfi RBT_set: ccompare = None'') (\_. set_fold_cfi f'' b (RBT_set rbt)) | Some _ \ RBT_Set2.fold (comp_fun_idem_apply f'') rbt b)" (is ?RBT_set) proof - show ?Set_Monad by(auto split: option.split dest!: Collection_Eq.ID_ceq simp add: set_fold_cfi_def comp_fun_idem.fold_set_fold) show ?DList_set apply(auto split: option.split simp add: DList_set_def) apply transfer apply(auto dest: Collection_Eq.ID_ceq simp add: List.member_def[abs_def] comp_fun_idem.fold_set_fold) done show ?RBT_set apply(auto split: option.split simp add: RBT_set_conv_keys fold_conv_fold_keys) apply transfer apply(simp add: comp_fun_idem.fold_set_fold) done qed simp_all typedef 'a semilattice_set = "{f :: 'a \ 'a \ 'a. semilattice_set f}" morphisms semilattice_set_apply Abs_semilattice_set proof show "(\x y. if x = y then x else undefined) \ ?semilattice_set" unfolding mem_Collect_eq by(unfold_locales) simp_all qed setup_lifting type_definition_semilattice_set lemma semilattice_set_apply' [simp]: "semilattice_set (semilattice_set_apply f)" using semilattice_set_apply[of f] by simp lemma comp_fun_idem_semilattice_set_apply [simp]: "comp_fun_idem (semilattice_set_apply f)" proof - interpret semilattice_set "semilattice_set_apply f" by simp show ?thesis by(unfold_locales)(simp_all add: fun_eq_iff left_commute) qed lift_definition set_fold1 :: "'a semilattice_set \ 'a set \ 'a" is "semilattice_set.F" . lemma (in semilattice_set) F_set_conv_fold: "xs \ [] \ F (set xs) = Finite_Set.fold f (hd xs) (set (tl xs))" by(clarsimp simp add: neq_Nil_conv eq_fold) lemma set_fold1_code [code]: fixes rbt :: "'a :: {ccompare, lattice} set_rbt" and dxs :: "'b :: {ceq, lattice} set_dlist" shows set_fold1_Complement[set_complement_code]: "set_fold1 f (Complement A) = Code.abort (STR ''set_fold1: Complement'') (\_. set_fold1 f (Complement A))" and "set_fold1 f (Collect_set P) = Code.abort (STR ''set_fold1: Collect_set'') (\_. set_fold1 f (Collect_set P))" and "set_fold1 f (Set_Monad (x # xs)) = fold (semilattice_set_apply f) xs x" (is "?Set_Monad") and "set_fold1 f' (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''set_fold1 DList_set: ceq = None'') (\_. set_fold1 f' (DList_set dxs)) | Some _ \ if DList_Set.null dxs then Code.abort (STR ''set_fold1 DList_set: empty set'') (\_. set_fold1 f' (DList_set dxs)) else DList_Set.fold (semilattice_set_apply f') (DList_Set.tl dxs) (DList_Set.hd dxs))" (is "?DList_set") and "set_fold1 f'' (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''set_fold1 RBT_set: ccompare = None'') (\_. set_fold1 f'' (RBT_set rbt)) | Some _ \ if RBT_Set2.is_empty rbt then Code.abort (STR ''set_fold1 RBT_set: empty set'') (\_. set_fold1 f'' (RBT_set rbt)) else RBT_Set2.fold1 (semilattice_set_apply f'') rbt)" (is "?RBT_set") proof - show ?Set_Monad by(simp add: set_fold1_def semilattice_set.eq_fold comp_fun_idem.fold_set_fold) show ?DList_set by(simp add: set_fold1_def semilattice_set.F_set_conv_fold comp_fun_idem.fold_set_fold DList_set_def DList_Set.Collect_member split: option.split)(transfer, simp) show ?RBT_set by(simp add: set_fold1_def semilattice_set.F_set_conv_fold comp_fun_idem.fold_set_fold RBT_set_def RBT_Set2.member_conv_keys RBT_Set2.fold1_conv_fold split: option.split) qed simp_all text \Implementation of set operations\ lemma Collect_code [code]: fixes P :: "'a :: cenum \ bool" shows "Collect P = (case ID CENUM('a) of None \ Collect_set P | Some (enum, _) \ Set_Monad (filter P enum))" by(auto split: option.split dest: in_cenum) lemma finite_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" and A :: "'c :: finite_UNIV set" and P :: "'c \ bool" shows "finite (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''finite DList_set: ceq = None'') (\_. finite (DList_set dxs)) | Some _ \ True)" "finite (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''finite RBT_set: ccompare = None'') (\_. finite (RBT_set rbt)) | Some _ \ True)" and finite_Complement [set_complement_code]: "finite (Complement A) \ (if of_phantom (finite_UNIV :: 'c finite_UNIV) then True else if finite A then False else Code.abort (STR ''finite Complement: infinite set'') (\_. finite (Complement A)))" and "finite (Set_Monad xs) = True" "finite (Collect_set P) \ of_phantom (finite_UNIV :: 'c finite_UNIV) \ Code.abort (STR ''finite Collect_set'') (\_. finite (Collect_set P))" by(auto simp add: DList_set_def RBT_set_def member_conv_keys card_gt_0_iff finite_UNIV split: option.split elim: finite_subset[rotated 1]) lemma card_code [code]: fixes dxs :: "'a :: ceq set_dlist" and xs :: "'a list" and rbt :: "'b :: ccompare set_rbt" and A :: "'c :: card_UNIV set" shows "card (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''card DList_set: ceq = None'') (\_. card (DList_set dxs)) | Some _ \ DList_Set.length dxs)" "card (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''card RBT_set: ccompare = None'') (\_. card (RBT_set rbt)) | Some _ \ length (RBT_Set2.keys rbt))" "card (Set_Monad xs) = (case ID CEQ('a) of None \ Code.abort (STR ''card Set_Monad: ceq = None'') (\_. card (Set_Monad xs)) | Some eq \ length (equal_base.list_remdups eq xs))" and card_Complement [set_complement_code]: "card (Complement A) = (let a = card A; s = CARD('c) in if s > 0 then s - a else if finite A then 0 else Code.abort (STR ''card Complement: infinite'') (\_. card (Complement A)))" by(auto simp add: RBT_set_def member_conv_keys distinct_card DList_set_def Let_def card_UNIV Compl_eq_Diff_UNIV card_Diff_subset_Int card_gt_0_iff finite_subset[of A UNIV] List.card_set dest: Collection_Eq.ID_ceq split: option.split) lemma is_UNIV_code [code]: fixes rbt :: "'a :: {cproper_interval, finite_UNIV} set_rbt" and A :: "'b :: card_UNIV set" shows "is_UNIV A \ (let a = CARD('b); b = card A in if a > 0 then a = b else if b > 0 then False else Code.abort (STR ''is_UNIV called on infinite type and set'') (\_. is_UNIV A))" (is ?generic) "is_UNIV (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''is_UNIV RBT_set: ccompare = None'') (\_. is_UNIV (RBT_set rbt)) | Some _ \ of_phantom (finite_UNIV :: 'a finite_UNIV) \ proper_intrvl.exhaustive_fusion cproper_interval rbt_keys_generator (RBT_Set2.init rbt))" (is ?rbt) proof - { fix c assume linorder: "ID CCOMPARE('a) = Some c" have "is_UNIV (RBT_set rbt) = (finite (UNIV :: 'a set) \ proper_intrvl.exhaustive cproper_interval (RBT_Set2.keys rbt))" (is "?lhs \ ?rhs") proof assume ?lhs have "finite (UNIV :: 'a set)" unfolding \?lhs\[unfolded is_UNIV_def, symmetric] using linorder by(simp add: finite_code) moreover hence "proper_intrvl.exhaustive cproper_interval (RBT_Set2.keys rbt)" using linorder \?lhs\ by(simp add: linorder_proper_interval.exhaustive_correct[OF ID_ccompare_interval[OF linorder]] sorted_RBT_Set_keys is_UNIV_def RBT_set_conv_keys) ultimately show ?rhs .. next assume ?rhs thus ?lhs using linorder by(auto simp add: linorder_proper_interval.exhaustive_correct[OF ID_ccompare_interval[OF linorder]] sorted_RBT_Set_keys is_UNIV_def RBT_set_conv_keys) qed } thus ?rbt by(auto simp add: finite_UNIV proper_intrvl.exhaustive_fusion_def unfoldr_rbt_keys_generator is_UNIV_def split: option.split) show ?generic by(auto simp add: Let_def is_UNIV_def dest: card_seteq[of UNIV A] dest!: card_ge_0_finite) qed lemma is_empty_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" and A :: "'c set" shows "Set.is_empty (Set_Monad xs) \ xs = []" "Set.is_empty (DList_set dxs) \ (case ID CEQ('a) of None \ Code.abort (STR ''is_empty DList_set: ceq = None'') (\_. Set.is_empty (DList_set dxs)) | Some _ \ DList_Set.null dxs)" (is ?DList_set) "Set.is_empty (RBT_set rbt) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''is_empty RBT_set: ccompare = None'') (\_. Set.is_empty (RBT_set rbt)) | Some _ \ RBT_Set2.is_empty rbt)" (is ?RBT_set) and is_empty_Complement [set_complement_code]: "Set.is_empty (Complement A) \ is_UNIV A" (is ?Complement) proof - show ?DList_set by(clarsimp simp add: DList_set_def Set.is_empty_def DList_Set.member_empty_empty split: option.split) show ?RBT_set by(clarsimp simp add: RBT_set_def Set.is_empty_def RBT_Set2.member_empty_empty[symmetric] fun_eq_iff simp del: RBT_Set2.member_empty_empty split: option.split) show ?Complement by(auto simp add: is_UNIV_def Set.is_empty_def) qed(simp_all add: Set.is_empty_def List.null_def) lemma Set_insert_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "\x. Set.insert x (Collect_set A) = (case ID CEQ('a) of None \ Code.abort (STR ''insert Collect_set: ceq = None'') (\_. Set.insert x (Collect_set A)) | Some eq \ Collect_set (equal_base.fun_upd eq A x True))" "\x. Set.insert x (Set_Monad xs) = Set_Monad (x # xs)" "\x. Set.insert x (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''insert DList_set: ceq = None'') (\_. Set.insert x (DList_set dxs)) | Some _ \ DList_set (DList_Set.insert x dxs))" "\x. Set.insert x (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''insert RBT_set: ccompare = None'') (\_. Set.insert x (RBT_set rbt)) | Some _ \ RBT_set (RBT_Set2.insert x rbt))" and insert_Complement [set_complement_code]: "\x. Set.insert x (Complement X) = Complement (Set.remove x X)" by(auto split: option.split dest: equal.equal_eq[OF ID_ceq] simp add: DList_set_def DList_Set.member_insert RBT_set_def) lemma Set_member_code [code]: fixes xs :: "'a :: ceq list" shows "\x. x \ Collect_set A \ A x" "\x. x \ DList_set dxs \ DList_Set.member dxs x" "\x. x \ RBT_set rbt \ RBT_Set2.member rbt x" and mem_Complement [set_complement_code]: "\x. x \ Complement X \ x \ X" and "\x. x \ Set_Monad xs \ (case ID CEQ('a) of None \ Code.abort (STR ''member Set_Monad: ceq = None'') (\_. x \ Set_Monad xs) | Some eq \ equal_base.list_member eq xs x)" by(auto simp add: DList_set_def RBT_set_def List.member_def split: option.split dest!: Collection_Eq.ID_ceq) lemma Set_remove_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: ceq set_dlist" shows "\x. Set.remove x (Collect_set A) = (case ID CEQ('b) of None \ Code.abort (STR ''remove Collect: ceq = None'') (\_. Set.remove x (Collect_set A)) | Some eq \ Collect_set (equal_base.fun_upd eq A x False))" "\x. Set.remove x (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''remove DList_set: ceq = None'') (\_. Set.remove x (DList_set dxs)) | Some _ \ DList_set (DList_Set.remove x dxs))" "\x. Set.remove x (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''remove RBT_set: ccompare = None'') (\_. Set.remove x (RBT_set rbt)) | Some _ \ RBT_set (RBT_Set2.remove x rbt))" and remove_Complement [set_complement_code]: "\x A. Set.remove x (Complement A) = Complement (Set.insert x A)" by(auto split: option.split if_split_asm dest: equal.equal_eq[OF ID_ceq] simp add: DList_set_def DList_Set.member_remove RBT_set_def) lemma Set_uminus_code [code, set_complement_code]: "- A = Complement A" "- (Collect_set P) = Collect_set (\x. \ P x)" "- (Complement B) = B" by auto text \ These equations represent complements as true complements. If you want that the complement operations returns an explicit enumeration of the elements, use the following set of equations which use @{class cenum}. \ lemma Set_uminus_cenum: fixes A :: "'a :: cenum set" shows "- A = (case ID CENUM('a) of None \ Complement A | Some (enum, _) \ Set_Monad (filter (\x. x \ A) enum))" and "- (Complement B) = B" by(auto split: option.split dest: ID_cEnum) lemma Set_minus_code [code]: "A - B = A \ (- B)" by(rule Diff_eq) lemma Set_union_code [code]: fixes rbt1 rbt2 :: "'a :: ccompare set_rbt" and rbt :: "'b :: {ccompare, ceq} set_rbt" and dxs :: "'b set_dlist" and dxs1 dxs2 :: "'c :: ceq set_dlist" shows "RBT_set rbt1 \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''union RBT_set RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ RBT_set rbt2) | Some _ \ RBT_set (RBT_Set2.union rbt1 rbt2))" (is ?RBT_set_RBT_set) "RBT_set rbt \ DList_set dxs = (case ID CCOMPARE('b) of None \ Code.abort (STR ''union RBT_set DList_set: ccompare = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''union RBT_set DList_set: ceq = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ RBT_set (DList_Set.fold RBT_Set2.insert dxs rbt))" (is ?RBT_set_DList_set) "DList_set dxs \ RBT_set rbt = (case ID CCOMPARE('b) of None \ Code.abort (STR ''union DList_set RBT_set: ccompare = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''union DList_set RBT_set: ceq = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ RBT_set (DList_Set.fold RBT_Set2.insert dxs rbt))" (is ?DList_set_RBT_set) "DList_set dxs1 \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''union DList_set DList_set: ceq = None'') (\_. DList_set dxs1 \ DList_set dxs2) | Some _ \ DList_set (DList_Set.union dxs1 dxs2))" (is ?DList_set_DList_set) "Set_Monad zs \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''union Set_Monad RBT_set: ccompare = None'') (\_. Set_Monad zs \ RBT_set rbt2) | Some _ \ RBT_set (fold RBT_Set2.insert zs rbt2))" (is ?Set_Monad_RBT_set) "RBT_set rbt1 \ Set_Monad zs = (case ID CCOMPARE('a) of None \ Code.abort (STR ''union RBT_set Set_Monad: ccompare = None'') (\_. RBT_set rbt1 \ Set_Monad zs) | Some _ \ RBT_set (fold RBT_Set2.insert zs rbt1))" (is ?RBT_set_Set_Monad) "Set_Monad ws \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''union Set_Monad DList_set: ceq = None'') (\_. Set_Monad ws \ DList_set dxs2) | Some _ \ DList_set (fold DList_Set.insert ws dxs2))" (is ?Set_Monad_DList_set) "DList_set dxs1 \ Set_Monad ws = (case ID CEQ('c) of None \ Code.abort (STR ''union DList_set Set_Monad: ceq = None'') (\_. DList_set dxs1 \ Set_Monad ws) | Some _ \ DList_set (fold DList_Set.insert ws dxs1))" (is ?DList_set_Set_Monad) "Set_Monad xs \ Set_Monad ys = Set_Monad (xs @ ys)" "Collect_set A \ B = Collect_set (\x. A x \ x \ B)" "B \ Collect_set A = Collect_set (\x. A x \ x \ B)" and Set_union_Complement [set_complement_code]: "Complement B \ B' = Complement (B \ - B')" "B' \ Complement B = Complement (- B' \ B)" proof - show ?RBT_set_RBT_set ?Set_Monad_RBT_set ?RBT_set_Set_Monad by(auto split: option.split simp add: RBT_set_def) show ?RBT_set_DList_set ?DList_set_RBT_set by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.fold_def DList_Set.member_def List.member_def dest: equal.equal_eq[OF ID_ceq]) show ?DList_set_Set_Monad ?Set_Monad_DList_set by(auto split: option.split simp add: DList_set_def DList_Set.member_fold_insert) show ?DList_set_DList_set by(auto split: option.split simp add: DList_set_def DList_Set.member_union) qed(auto) lemma Set_inter_code [code]: fixes rbt1 rbt2 :: "'a :: ccompare set_rbt" and rbt :: "'b :: {ccompare, ceq} set_rbt" and dxs :: "'b set_dlist" and dxs1 dxs2 :: "'c :: ceq set_dlist" and xs1 xs2 :: "'c list" shows "Collect_set A'' \ J = Collect_set (\x. A'' x \ x \ J)" (is ?collect1) "J \ Collect_set A'' = Collect_set (\x. A'' x \ x \ J)" (is ?collect2) "Set_Monad xs'' \ I = Set_Monad (filter (\x. x \ I) xs'')" (is ?monad1) "I \ Set_Monad xs'' = Set_Monad (filter (\x. x \ I) xs'')" (is ?monad2) "DList_set dxs1 \ H = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set1: ceq = None'') (\_. DList_set dxs1 \ H) | Some eq \ DList_set (DList_Set.filter (\x. x \ H) dxs1))" (is ?dlist1) "H \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set2: ceq = None'') (\_. H \ DList_set dxs2) | Some eq \ DList_set (DList_Set.filter (\x. x \ H) dxs2))" (is ?dlist2) "RBT_set rbt1 \ G = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set1: ccompare = None'') (\_. RBT_set rbt1 \ G) | Some _ \ RBT_set (RBT_Set2.filter (\x. x \ G) rbt1))" (is ?rbt1) "G \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set2: ccompare = None'') (\_. G \ RBT_set rbt2) | Some _ \ RBT_set (RBT_Set2.filter (\x. x \ G) rbt2))" (is ?rbt2) and Set_inter_Complement [set_complement_code]: "Complement B'' \ Complement B''' = Complement (B'' \ B''')" (is ?complement) and "Set_Monad xs \ RBT_set rbt1 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter Set_Monad RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ Set_Monad xs) | Some _ \ RBT_set (RBT_Set2.inter_list rbt1 xs))" (is ?monad_rbt) "Set_Monad xs' \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter Set_Monad DList_set: ceq = None'') (\_. Set_Monad xs' \ DList_set dxs2) | Some eq \ DList_set (DList_Set.filter (equal_base.list_member eq xs') dxs2))" (is ?monad_dlist) "Set_Monad xs1 \ Set_Monad xs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter Set_Monad Set_Monad: ceq = None'') (\_. Set_Monad xs1 \ Set_Monad xs2) | Some eq \ Set_Monad (filter (equal_base.list_member eq xs2) xs1))" (is ?monad) "DList_set dxs \ RBT_set rbt = (case ID CCOMPARE('b) of None \ Code.abort (STR ''inter DList_set RBT_set: ccompare = None'') (\_. DList_set dxs \ RBT_set rbt) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''inter DList_set RBT_set: ceq = None'') (\_. DList_set dxs \ RBT_set rbt) | Some _ \ RBT_set (RBT_Set2.inter_list rbt (list_of_dlist dxs)))" (is ?dlist_rbt) "DList_set dxs1 \ DList_set dxs2 = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set DList_set: ceq = None'') (\_. DList_set dxs1 \ DList_set dxs2) | Some _ \ DList_set (DList_Set.filter (DList_Set.member dxs2) dxs1))" (is ?dlist) "DList_set dxs1 \ Set_Monad xs' = (case ID CEQ('c) of None \ Code.abort (STR ''inter DList_set Set_Monad: ceq = None'') (\_. DList_set dxs1 \ Set_Monad xs') | Some eq \ DList_set (DList_Set.filter (equal_base.list_member eq xs') dxs1))" (is ?dlist_monad) "RBT_set rbt1 \ RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ RBT_set rbt2) | Some _ \ RBT_set (RBT_Set2.inter rbt1 rbt2))" (is ?rbt_rbt) "RBT_set rbt \ DList_set dxs = (case ID CCOMPARE('b) of None \ Code.abort (STR ''inter RBT_set DList_set: ccompare = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''inter RBT_set DList_set: ceq = None'') (\_. RBT_set rbt \ DList_set dxs) | Some _ \ RBT_set (RBT_Set2.inter_list rbt (list_of_dlist dxs)))" (is ?rbt_dlist) "RBT_set rbt1 \ Set_Monad xs = (case ID CCOMPARE('a) of None \ Code.abort (STR ''inter RBT_set Set_Monad: ccompare = None'') (\_. RBT_set rbt1 \ Set_Monad xs) | Some _ \ RBT_set (RBT_Set2.inter_list rbt1 xs))" (is ?rbt_monad) proof - show ?rbt_rbt ?rbt1 ?rbt2 ?rbt_dlist ?rbt_monad ?dlist_rbt ?monad_rbt by(auto simp add: RBT_set_def DList_set_def DList_Set.member_def List.member_def dest: equal.equal_eq[OF ID_ceq] split: option.split) show ?dlist ?dlist1 ?dlist2 ?dlist_monad ?monad_dlist ?monad ?monad1 ?monad2 ?collect1 ?collect2 ?complement by(auto simp add: DList_set_def List.member_def dest!: Collection_Eq.ID_ceq split: option.splits) qed lemma Set_bind_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "Set.bind (Set_Monad xs) f = fold ((\) \ f) xs (Set_Monad [])" (is ?Set_Monad) "Set.bind (DList_set dxs) f' = (case ID CEQ('a) of None \ Code.abort (STR ''bind DList_set: ceq = None'') (\_. Set.bind (DList_set dxs) f') | Some _ \ DList_Set.fold (union \ f') dxs {})" (is ?DList) "Set.bind (RBT_set rbt) f'' = (case ID CCOMPARE('b) of None \ Code.abort (STR ''bind RBT_set: ccompare = None'') (\_. Set.bind (RBT_set rbt) f'') | Some _ \ RBT_Set2.fold (union \ f'') rbt {})" (is ?RBT) proof - show ?Set_Monad by(simp add: set_bind_conv_fold) show ?DList by(auto simp add: DList_set_def DList_Set.member_def List.member_def List.member_def[abs_def] set_bind_conv_fold DList_Set.fold_def split: option.split dest: equal.equal_eq[OF ID_ceq] ID_ceq) show ?RBT by(clarsimp split: option.split simp add: RBT_set_def RBT_Set2.fold_conv_fold_keys RBT_Set2.member_conv_keys set_bind_conv_fold) qed lemma UNIV_code [code]: "UNIV = - {}" by(simp) lift_definition inf_sls :: "'a :: lattice semilattice_set" is "inf" by unfold_locales lemma Inf_fin_code [code]: "Inf_fin A = set_fold1 inf_sls A" by transfer(simp add: Inf_fin_def) lift_definition sup_sls :: "'a :: lattice semilattice_set" is "sup" by unfold_locales lemma Sup_fin_code [code]: "Sup_fin A = set_fold1 sup_sls A" by transfer(simp add: Sup_fin_def) lift_definition inf_cfi :: "('a :: lattice, 'a) comp_fun_idem" is "inf" by(rule comp_fun_idem_inf) lemma Inf_code: fixes A :: "'a :: complete_lattice set" shows "Inf A = (if finite A then set_fold_cfi inf_cfi top A else Code.abort (STR ''Inf: infinite'') (\_. Inf A))" by transfer(simp add: Inf_fold_inf) lift_definition sup_cfi :: "('a :: lattice, 'a) comp_fun_idem" is "sup" by(rule comp_fun_idem_sup) lemma Sup_code: fixes A :: "'a :: complete_lattice set" shows "Sup A = (if finite A then set_fold_cfi sup_cfi bot A else Code.abort (STR ''Sup: infinite'') (\_. Sup A))" by transfer(simp add: Sup_fold_sup) lemmas Inter_code [code] = Inf_code[where ?'a = "_ :: type set"] lemmas Union_code [code] = Sup_code[where ?'a = "_ :: type set"] lemmas Predicate_Inf_code [code] = Inf_code[where ?'a = "_ :: type Predicate.pred"] lemmas Predicate_Sup_code [code] = Sup_code[where ?'a = "_ :: type Predicate.pred"] lemmas Inf_fun_code [code] = Inf_code[where ?'a = "_ :: type \ _ :: complete_lattice"] lemmas Sup_fun_code [code] = Sup_code[where ?'a = "_ :: type \ _ :: complete_lattice"] lift_definition min_sls :: "'a :: linorder semilattice_set" is min by unfold_locales lemma Min_code [code]: "Min A = set_fold1 min_sls A" by transfer(simp add: Min_def) lift_definition max_sls :: "'a :: linorder semilattice_set" is max by unfold_locales lemma Max_code [code]: "Max A = set_fold1 max_sls A" by transfer(simp add: Max_def) text \ We do not implement @{term Ball}, @{term Bex}, and @{term sorted_list_of_set} for @{term Collect_set} using @{term cEnum}, because it should already have been converted to an explicit list of elements if that is possible. \ lemma Ball_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: ceq set_dlist" shows "Ball (Set_Monad xs) P = list_all P xs" "Ball (DList_set dxs) P' = (case ID CEQ('b) of None \ Code.abort (STR ''Ball DList_set: ceq = None'') (\_. Ball (DList_set dxs) P') | Some _ \ DList_Set.dlist_all P' dxs)" "Ball (RBT_set rbt) P'' = (case ID CCOMPARE('a) of None \ Code.abort (STR ''Ball RBT_set: ccompare = None'') (\_. Ball (RBT_set rbt) P'') | Some _ \ RBT_Set2.all P'' rbt)" by(simp_all add: DList_set_def RBT_set_def list_all_iff dlist_all_conv_member RBT_Set2.all_conv_all_member split: option.splits) lemma Bex_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: ceq set_dlist" shows "Bex (Set_Monad xs) P = list_ex P xs" "Bex (DList_set dxs) P' = (case ID CEQ('b) of None \ Code.abort (STR ''Bex DList_set: ceq = None'') (\_. Bex (DList_set dxs) P') | Some _ \ DList_Set.dlist_ex P' dxs)" "Bex (RBT_set rbt) P'' = (case ID CCOMPARE('a) of None \ Code.abort (STR ''Bex RBT_set: ccompare = None'') (\_. Bex (RBT_set rbt) P'') | Some _ \ RBT_Set2.ex P'' rbt)" by(simp_all add: DList_set_def RBT_set_def list_ex_iff dlist_ex_conv_member RBT_Set2.ex_conv_ex_member split: option.splits) lemma csorted_list_of_set_code [code]: fixes rbt :: "'a :: ccompare set_rbt" and dxs :: "'b :: {ccompare, ceq} set_dlist" and xs :: "'a :: ccompare list" shows "csorted_list_of_set (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''csorted_list_of_set RBT_set: ccompare = None'') (\_. csorted_list_of_set (RBT_set rbt)) | Some _ \ RBT_Set2.keys rbt)" "csorted_list_of_set (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''csorted_list_of_set DList_set: ceq = None'') (\_. csorted_list_of_set (DList_set dxs)) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''csorted_list_of_set DList_set: ccompare = None'') (\_. csorted_list_of_set (DList_set dxs)) | Some c \ ord.quicksort (lt_of_comp c) (list_of_dlist dxs))" "csorted_list_of_set (Set_Monad xs) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''csorted_list_of_set Set_Monad: ccompare = None'') (\_. csorted_list_of_set (Set_Monad xs)) | Some c \ ord.remdups_sorted (lt_of_comp c) (ord.quicksort (lt_of_comp c) xs))" by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.Collect_member member_conv_keys sorted_RBT_Set_keys linorder.sorted_list_of_set_sort_remdups[OF ID_ccompare] linorder.quicksort_conv_sort[OF ID_ccompare] distinct_remdups_id distinct_list_of_dlist linorder.remdups_sorted_conv_remdups[OF ID_ccompare] linorder.sorted_sort[OF ID_ccompare] linorder.sort_remdups[OF ID_ccompare] csorted_list_of_set_def) lemma cless_set_code [code]: fixes rbt rbt' :: "'a :: ccompare set_rbt" and rbt1 rbt2 :: "'b :: cproper_interval set_rbt" and A B :: "'a set" and A' B' :: "'b set" shows "cless_set A B \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_set: ccompare = None'') (\_. cless_set A B) | Some c \ - if finite A \ finite B then order.lexordp (\x y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B) + if finite A \ finite B then ord.lexordp (\x y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B) else Code.abort (STR ''cless_set: infinite set'') (\_. cless_set A B))" (is "?fin_fin") and cless_set_Complement2 [set_complement_code]: "cless_set A' (Complement B') \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set Complement2: ccompare = None'') (\_. cless_set A' (Complement B')) | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.set_less_aux_Compl (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_set Complement2: infinite set'') (\_. cless_set A' (Complement B')))" (is "?fin_Compl_fin") and cless_set_Complement1 [set_complement_code]: "cless_set (Complement A') B' \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set Complement1: ccompare = None'') (\_. cless_set (Complement A') B') | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_set Complement1: infinite set'') (\_. cless_set (Complement A') B'))" (is "?Compl_fin_fin") and cless_set_Complement12 [set_complement_code]: "cless_set (Complement A) (Complement B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_set Complement Complement: ccompare = None'') (\_. cless_set (Complement A) (Complement B)) | Some _ \ cless B A)" (is ?Compl_Compl) and "cless_set (RBT_set rbt) (RBT_set rbt') \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_set RBT_set RBT_set: ccompare = None'') (\_. cless_set (RBT_set rbt) (RBT_set rbt')) - | Some c \ order.lexord_fusion (\x y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))" + | Some c \ ord.lexord_fusion (\x y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))" (is ?rbt_rbt) and cless_set_rbt_Complement2 [set_complement_code]: "cless_set (RBT_set rbt1) (Complement (RBT_set rbt2)) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set RBT_set (Complement RBT_set): ccompare = None'') (\_. cless_set (RBT_set rbt1) (Complement (RBT_set rbt2))) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.set_less_aux_Compl_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_Compl) and cless_set_rbt_Complement1 [set_complement_code]: "cless_set (Complement (RBT_set rbt1)) (RBT_set rbt2) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_set (Complement RBT_set) RBT_set: ccompare = None'') (\_. cless_set (Complement (RBT_set rbt1)) (RBT_set rbt2)) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?Compl_rbt) proof - note [split] = option.split csorted_list_of_set_split and [simp] = le_of_comp_of_ords_linorder[OF ID_ccompare] lt_of_comp_of_ords finite_subset[OF subset_UNIV] ccompare_set_def ID_Some - order.lexord_fusion_def + ord.lexord_fusion_def proper_intrvl.Compl_set_less_aux_fusion_def proper_intrvl.set_less_aux_Compl_fusion_def unfoldr_rbt_keys_generator RBT_set_def sorted_RBT_Set_keys member_conv_keys linorder.set_less_finite_iff[OF ID_ccompare] linorder.set_less_aux_code[OF ID_ccompare, symmetric] linorder.Compl_set_less_Compl[OF ID_ccompare] linorder.infinite_set_less_Complement[OF ID_ccompare] linorder.infinite_Complement_set_less[OF ID_ccompare] linorder_proper_interval.set_less_aux_Compl2_conv_set_less_aux_Compl[OF ID_ccompare_interval, symmetric] linorder_proper_interval.Compl1_set_less_aux_conv_Compl_set_less_aux[OF ID_ccompare_interval, symmetric] show ?Compl_Compl by simp - show ?rbt_rbt - apply (subst order.lexord_fusion_def) - apply (auto simp: ) + show ?rbt_rbt by auto show ?rbt_Compl by(cases "finite (UNIV :: 'b set)") auto show ?Compl_rbt by(cases "finite (UNIV :: 'b set)") auto show ?fin_fin by auto show ?fin_Compl_fin by(cases "finite (UNIV :: 'b set)", auto) show ?Compl_fin_fin by(cases "finite (UNIV :: 'b set)") auto qed lemma le_of_comp_set_less_eq: "le_of_comp (comp_of_ords (ord.set_less_eq le) (ord.set_less le)) = ord.set_less_eq le" by (rule le_of_comp_of_ords_gen, simp add: ord.set_less_def) lemma cless_eq_set_code [code]: fixes rbt rbt' :: "'a :: ccompare set_rbt" and rbt1 rbt2 :: "'b :: cproper_interval set_rbt" and A B :: "'a set" and A' B' :: "'b set" shows "cless_eq_set A B \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_eq_set: ccompare = None'') (\_. cless_eq_set A B) | Some c \ if finite A \ finite B then - order.lexordp_eq (\x y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B) + ord.lexordp_eq (\x y. lt_of_comp c y x) (csorted_list_of_set A) (csorted_list_of_set B) else Code.abort (STR ''cless_eq_set: infinite set'') (\_. cless_eq_set A B))" (is "?fin_fin") and cless_eq_set_Complement2 [set_complement_code]: "cless_eq_set A' (Complement B') \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set Complement2: ccompare = None'') (\_. cless_eq_set A' (Complement B')) | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.set_less_eq_aux_Compl (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_eq_set Complement2: infinite set'') (\_. cless_eq_set A' (Complement B')))" (is "?fin_Compl_fin") and cless_eq_set_Complement1 [set_complement_code]: "cless_eq_set (Complement A') B' \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set Complement1: ccompare = None'') (\_. cless_eq_set (Complement A') B') | Some c \ if finite A' \ finite B' then finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_eq_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A') (csorted_list_of_set B') else Code.abort (STR ''cless_eq_set Complement1: infinite set'') (\_. cless_eq_set (Complement A') B'))" (is "?Compl_fin_fin") and cless_eq_set_Complement12 [set_complement_code]: "cless_eq_set (Complement A) (Complement B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_eq_set Complement Complement: ccompare = None'') (\_. cless_eq (Complement A) (Complement B)) | Some c \ cless_eq_set B A)" (is ?Compl_Compl) "cless_eq_set (RBT_set rbt) (RBT_set rbt') \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cless_eq_set RBT_set RBT_set: ccompare = None'') (\_. cless_eq_set (RBT_set rbt) (RBT_set rbt')) - | Some c \ order.lexord_eq_fusion (\x y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))" + | Some c \ ord.lexord_eq_fusion (\x y. lt_of_comp c y x) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt) (RBT_Set2.init rbt'))" (is ?rbt_rbt) and cless_eq_set_rbt_Complement2 [set_complement_code]: "cless_eq_set (RBT_set rbt1) (Complement (RBT_set rbt2)) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set RBT_set (Complement RBT_set): ccompare = None'') (\_. cless_eq_set (RBT_set rbt1) (Complement (RBT_set rbt2))) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.set_less_eq_aux_Compl_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_Compl) and cless_eq_set_rbt_Complement1 [set_complement_code]: "cless_eq_set (Complement (RBT_set rbt1)) (RBT_set rbt2) \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''cless_eq_set (Complement RBT_set) RBT_set: ccompare = None'') (\_. cless_eq_set (Complement (RBT_set rbt1)) (RBT_set rbt2)) | Some c \ finite (UNIV :: 'b set) \ proper_intrvl.Compl_set_less_eq_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?Compl_rbt) proof - note [split] = option.split csorted_list_of_set_split and [simp] = le_of_comp_set_less_eq finite_subset[OF subset_UNIV] ccompare_set_def ID_Some - order.lexord_eq_fusion_def proper_intrvl.Compl_set_less_eq_aux_fusion_def + ord.lexord_eq_fusion_def proper_intrvl.Compl_set_less_eq_aux_fusion_def proper_intrvl.set_less_eq_aux_Compl_fusion_def unfoldr_rbt_keys_generator RBT_set_def sorted_RBT_Set_keys member_conv_keys linorder.set_less_eq_finite_iff[OF ID_ccompare] linorder.set_less_eq_aux_code[OF ID_ccompare, symmetric] linorder.Compl_set_less_eq_Compl[OF ID_ccompare] linorder.infinite_set_less_eq_Complement[OF ID_ccompare] linorder.infinite_Complement_set_less_eq[OF ID_ccompare] linorder_proper_interval.set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl[OF ID_ccompare_interval, symmetric] linorder_proper_interval.Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux[OF ID_ccompare_interval, symmetric] show ?Compl_Compl by simp show ?rbt_rbt by auto show ?rbt_Compl by(cases "finite (UNIV :: 'b set)") auto show ?Compl_rbt by(cases "finite (UNIV :: 'b set)") auto show ?fin_fin by auto show ?fin_Compl_fin by (cases "finite (UNIV :: 'b set)", auto) show ?Compl_fin_fin by(cases "finite (UNIV :: 'b set)") auto qed lemma cproper_interval_set_Some_Some_code [code]: fixes rbt1 rbt2 :: "'a :: cproper_interval set_rbt" and A B :: "'a set" shows "cproper_interval (Some A) (Some B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval: ccompare = None'') (\_. cproper_interval (Some A) (Some B)) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_aux (lt_of_comp c) cproper_interval (csorted_list_of_set A) (csorted_list_of_set B))" (is ?fin_fin) and cproper_interval_set_Some_Some_Complement [set_complement_code]: "cproper_interval (Some A) (Some (Complement B)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval Complement2: ccompare = None'') (\_. cproper_interval (Some A) (Some (Complement B))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_Compl_aux (lt_of_comp c) cproper_interval None 0 (csorted_list_of_set A) (csorted_list_of_set B))" (is ?fin_Compl_fin) and cproper_interval_set_Some_Complement_Some [set_complement_code]: "cproper_interval (Some (Complement A)) (Some B) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval Complement1: ccompare = None'') (\_. cproper_interval (Some (Complement A)) (Some B)) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_Compl_set_aux (lt_of_comp c) cproper_interval None (csorted_list_of_set A) (csorted_list_of_set B))" (is ?Compl_fin_fin) and cproper_interval_set_Some_Complement_Some_Complement [set_complement_code]: "cproper_interval (Some (Complement A)) (Some (Complement B)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval Complement Complement: ccompare = None'') (\_. cproper_interval (Some (Complement A)) (Some (Complement B))) | Some _ \ cproper_interval (Some B) (Some A))" (is ?Compl_Compl) "cproper_interval (Some (RBT_set rbt1)) (Some (RBT_set rbt2)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval RBT_set RBT_set: ccompare = None'') (\_. cproper_interval (Some (RBT_set rbt1)) (Some (RBT_set rbt2))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_rbt) and cproper_interval_set_Some_rbt_Some_Complement [set_complement_code]: "cproper_interval (Some (RBT_set rbt1)) (Some (Complement (RBT_set rbt2))) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval RBT_set (Complement RBT_set): ccompare = None'') (\_. cproper_interval (Some (RBT_set rbt1)) (Some (Complement (RBT_set rbt2)))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_set_Compl_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None 0 (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?rbt_Compl_rbt) and cproper_interval_set_Some_Complement_Some_rbt [set_complement_code]: "cproper_interval (Some (Complement (RBT_set rbt1))) (Some (RBT_set rbt2)) \ (case ID CCOMPARE('a) of None \ Code.abort (STR ''cproper_interval (Complement RBT_set) RBT_set: ccompare = None'') (\_. cproper_interval (Some (Complement (RBT_set rbt1))) (Some (RBT_set rbt2))) | Some c \ finite (UNIV :: 'a set) \ proper_intrvl.proper_interval_Compl_set_aux_fusion (lt_of_comp c) cproper_interval rbt_keys_generator rbt_keys_generator None (RBT_Set2.init rbt1) (RBT_Set2.init rbt2))" (is ?Compl_rbt_rbt) proof - note [split] = option.split csorted_list_of_set_split and [simp] = lt_of_comp_of_ords finite_subset[OF subset_UNIV] ccompare_set_def ID_Some linorder.set_less_finite_iff[OF ID_ccompare] RBT_set_def sorted_RBT_Set_keys member_conv_keys linorder.distinct_entries[OF ID_ccompare] unfoldr_rbt_keys_generator proper_intrvl.proper_interval_set_aux_fusion_def proper_intrvl.proper_interval_set_Compl_aux_fusion_def proper_intrvl.proper_interval_Compl_set_aux_fusion_def linorder_proper_interval.proper_interval_set_aux[OF ID_ccompare_interval] linorder_proper_interval.proper_interval_set_Compl_aux[OF ID_ccompare_interval] linorder_proper_interval.proper_interval_Compl_set_aux[OF ID_ccompare_interval] and [cong] = conj_cong show ?Compl_Compl by(clarsimp simp add: Complement_cproper_interval_set_Complement simp del: cproper_interval_set_Some_Some) show ?rbt_rbt ?rbt_Compl_rbt ?Compl_rbt_rbt by auto show ?fin_fin ?fin_Compl_fin ?Compl_fin_fin by auto qed context ord begin fun sorted_list_subset :: "('a \ 'a \ bool) \ 'a list \ 'a list \ bool" where "sorted_list_subset eq [] ys = True" | "sorted_list_subset eq (x # xs) [] = False" | "sorted_list_subset eq (x # xs) (y # ys) \ (if eq x y then sorted_list_subset eq xs ys else x > y \ sorted_list_subset eq (x # xs) ys)" end context linorder begin lemma sorted_list_subset_correct: "\ sorted xs; distinct xs; sorted ys; distinct ys \ \ sorted_list_subset (=) xs ys \ set xs \ set ys" apply(induct "(=) :: 'a \ 'a \ bool" xs ys rule: sorted_list_subset.induct) apply(auto 6 2) apply auto by (metis eq_iff insert_iff subsetD) end context ord begin definition sorted_list_subset_fusion :: "('a \ 'a \ bool) \ ('a, 's1) generator \ ('a, 's2) generator \ 's1 \ 's2 \ bool" where "sorted_list_subset_fusion eq g1 g2 s1 s2 = sorted_list_subset eq (list.unfoldr g1 s1) (list.unfoldr g2 s2)" lemma sorted_list_subset_fusion_code: "sorted_list_subset_fusion eq g1 g2 s1 s2 = (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in list.has_next g2 s2 \ ( let (y, s2') = list.next g2 s2 in if eq x y then sorted_list_subset_fusion eq g1 g2 s1' s2' else y < x \ sorted_list_subset_fusion eq g1 g2 s1 s2') else True)" unfolding sorted_list_subset_fusion_def by(subst (1 2 5) list.unfoldr.simps)(simp add: split_beta Let_def) end lemmas [code] = ord.sorted_list_subset_fusion_code text \ Define a new constant for the subset operation because @{theory "HOL-Library.Cardinality"} introduces @{const "Cardinality.subset'"} and rewrites @{const "subset"} to @{const "Cardinality.subset'"} based on the sort of the element type. \ definition subset_eq :: "'a set \ 'a set \ bool" where [simp, code del]: "subset_eq = (\)" lemma subseteq_code [code]: "(\) = subset_eq" by simp lemma subset'_code [code]: "Cardinality.subset' = subset_eq" by simp lemma subset_eq_code [folded subset_eq_def, code]: fixes A1 A2 :: "'a set" and rbt :: "'b :: ccompare set_rbt" and rbt1 rbt2 :: "'d :: {ccompare, ceq} set_rbt" and dxs :: "'c :: ceq set_dlist" and xs :: "'c list" shows "RBT_set rbt \ B \ (case ID CCOMPARE('b) of None \ Code.abort (STR ''subset RBT_set1: ccompare = None'') (\_. RBT_set rbt \ B) | Some _ \ list_all_fusion rbt_keys_generator (\x. x \ B) (RBT_Set2.init rbt))" (is ?rbt) "DList_set dxs \ C \ (case ID CEQ('c) of None \ Code.abort (STR ''subset DList_set1: ceq = None'') (\_. DList_set dxs \ C) | Some _ \ DList_Set.dlist_all (\x. x \ C) dxs)" (is ?dlist) "Set_Monad xs \ C \ list_all (\x. x \ C) xs" (is ?Set_Monad) and Collect_subset_eq_Complement [folded subset_eq_def, set_complement_code]: "Collect_set P \ Complement A \ A \ {x. \ P x}" (is ?Collect_set_Compl) and Complement_subset_eq_Complement [folded subset_eq_def, set_complement_code]: "Complement A1 \ Complement A2 \ A2 \ A1" (is ?Compl) and "RBT_set rbt1 \ RBT_set rbt2 \ (case ID CCOMPARE('d) of None \ Code.abort (STR ''subset RBT_set RBT_set: ccompare = None'') (\_. RBT_set rbt1 \ RBT_set rbt2) | Some c \ (case ID CEQ('d) of None \ ord.sorted_list_subset_fusion (lt_of_comp c) (\ x y. c x y = Eq) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2) | Some eq \ ord.sorted_list_subset_fusion (lt_of_comp c) eq rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)))" (is ?rbt_rbt) proof - show ?rbt_rbt by (auto simp add: comparator.eq[OF ID_ccompare'] RBT_set_def member_conv_keys unfoldr_rbt_keys_generator ord.sorted_list_subset_fusion_def linorder.sorted_list_subset_correct[OF ID_ccompare] sorted_RBT_Set_keys split: option.split dest!: ID_ceq[THEN equal.equal_eq] del: iffI) show ?rbt by(auto simp add: RBT_set_def member_conv_keys list_all_fusion_def unfoldr_rbt_keys_generator keys.rep_eq list_all_iff split: option.split) show ?dlist by(auto simp add: DList_set_def dlist_all_conv_member split: option.split) show ?Set_Monad by(auto simp add: list_all_iff split: option.split) show ?Collect_set_Compl ?Compl by auto qed hide_const (open) subset_eq hide_fact (open) subset_eq_def lemma eq_set_code [code]: "Cardinality.eq_set = set_eq" by(simp add: set_eq_def) lemma set_eq_code [code]: fixes rbt1 rbt2 :: "'b :: {ccompare, ceq} set_rbt" shows "set_eq A B \ A \ B \ B \ A" and set_eq_Complement_Complement [set_complement_code]: "set_eq (Complement A) (Complement B) = set_eq A B" and "set_eq (RBT_set rbt1) (RBT_set rbt2) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''set_eq RBT_set RBT_set: ccompare = None'') (\_. set_eq (RBT_set rbt1) (RBT_set rbt2)) | Some c \ (case ID CEQ('b) of None \ list_all2_fusion (\ x y. c x y = Eq) rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2) | Some eq \ list_all2_fusion eq rbt_keys_generator rbt_keys_generator (RBT_Set2.init rbt1) (RBT_Set2.init rbt2)))" (is ?rbt_rbt) proof - show ?rbt_rbt by (auto 4 3 split: option.split simp add: comparator.eq[OF ID_ccompare'] sorted_RBT_Set_keys list_all2_fusion_def unfoldr_rbt_keys_generator RBT_set_conv_keys set_eq_def list.rel_eq dest!: ID_ceq[THEN equal.equal_eq] intro: linorder.sorted_distinct_set_unique[OF ID_ccompare]) qed(auto simp add: set_eq_def) lemma Set_project_code [code]: "Set.filter P A = A \ Collect_set P" by(auto simp add: Set.filter_def) lemma Set_image_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "image f (Set_Monad xs) = Set_Monad (map f xs)" "image f (Collect_set A) = Code.abort (STR ''image Collect_set'') (\_. image f (Collect_set A))" and image_Complement_Complement [set_complement_code]: "image f (Complement (Complement B)) = image f B" and "image g (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''image DList_set: ceq = None'') (\_. image g (DList_set dxs)) | Some _ \ DList_Set.fold (insert \ g) dxs {})" (is ?dlist) "image h (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''image RBT_set: ccompare = None'') (\_. image h (RBT_set rbt)) | Some _ \ RBT_Set2.fold (insert \ h) rbt {})" (is ?rbt) proof - { fix xs have "fold (insert \ g) xs {} = g ` set xs" by(induct xs rule: rev_induct) simp_all } thus ?dlist by(simp add: DList_set_def DList_Set.fold_def DList_Set.Collect_member split: option.split) { fix xs have "fold (insert \ h) xs {} = h ` set xs" by(induct xs rule: rev_induct) simp_all } thus ?rbt by(auto simp add: RBT_set_def fold_conv_fold_keys member_conv_keys split: option.split) qed simp_all lemma the_elem_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "the_elem (Set_Monad [x]) = x" "the_elem (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''the_elem DList_set: ceq = None'') (\_. the_elem (DList_set dxs)) | Some _ \ case list_of_dlist dxs of [x] \ x | _ \ Code.abort (STR ''the_elem DList_set: not unique'') (\_. the_elem (DList_set dxs)))" "the_elem (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''the_elem RBT_set: ccompare = None'') (\_. the_elem (RBT_set rbt)) | Some _ \ case RBT_Mapping2.impl_of rbt of RBT_Impl.Branch _ RBT_Impl.Empty x _ RBT_Impl.Empty \ x | _ \ Code.abort (STR ''the_elem RBT_set: not unique'') (\_. the_elem (RBT_set rbt)))" by(auto simp add: RBT_set_def DList_set_def DList_Set.Collect_member the_elem_def member_conv_keys split: option.split list.split rbt.split)(simp add: RBT_Set2.keys_def) lemma Pow_set_conv_fold: "Pow (set xs \ A) = fold (\x A. A \ insert x ` A) xs (Pow A)" by(induct xs rule: rev_induct)(auto simp add: Pow_insert) lemma Pow_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "Pow A = Collect_set (\B. B \ A)" "Pow (Set_Monad xs) = fold (\x A. A \ insert x ` A) xs {{}}" "Pow (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''Pow DList_set: ceq = None'') (\_. Pow (DList_set dxs)) | Some _ \ DList_Set.fold (\x A. A \ insert x ` A) dxs {{}})" "Pow (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''Pow RBT_set: ccompare = None'') (\_. Pow (RBT_set rbt)) | Some _ \ RBT_Set2.fold (\x A. A \ insert x ` A) rbt {{}})" by(auto simp add: DList_set_def DList_Set.Collect_member DList_Set.fold_def RBT_set_def fold_conv_fold_keys member_conv_keys Pow_set_conv_fold[where A="{}", simplified] split: option.split) lemma fold_singleton: "Finite_Set.fold f x {y} = f y x" by(fastforce simp add: Finite_Set.fold_def intro: fold_graph.intros elim: fold_graph.cases) lift_definition sum_cfc :: "('a \ 'b :: comm_monoid_add) \ ('a, 'b) comp_fun_commute" is "\f :: 'a \ 'b. plus \ f" by(unfold_locales)(simp add: fun_eq_iff add.left_commute) lemma sum_code [code]: "sum f A = (if finite A then set_fold_cfc (sum_cfc f) 0 A else 0)" by transfer(simp add: sum.eq_fold) lemma product_code [code]: fixes dxs :: "'a :: ceq set_dlist" and dys :: "'b :: ceq set_dlist" and rbt1 :: "'c :: ccompare set_rbt" and rbt2 :: "'d :: ccompare set_rbt" shows "Product_Type.product A B = Collect_set (\(x, y). x \ A \ y \ B)" "Product_Type.product (Set_Monad xs) (Set_Monad ys) = Set_Monad (fold (\x. fold (\y rest. (x, y) # rest) ys) xs [])" (is ?Set_Monad) "Product_Type.product (DList_set dxs) B1 = (case ID CEQ('a) of None \ Code.abort (STR ''product DList_set1: ceq = None'') (\_. Product_Type.product (DList_set dxs) B1) | Some _ \ DList_Set.fold (\x rest. Pair x ` B1 \ rest) dxs {})" (is "?dlist1") "Product_Type.product A1 (DList_set dys) = (case ID CEQ('b) of None \ Code.abort (STR ''product DList_set2: ceq = None'') (\_. Product_Type.product A1 (DList_set dys)) | Some _ \ DList_Set.fold (\y rest. (\x. (x, y)) ` A1 \ rest) dys {})" (is "?dlist2") "Product_Type.product (DList_set dxs) (DList_set dys) = (case ID CEQ('a) of None \ Code.abort (STR ''product DList_set DList_set: ceq1 = None'') (\_. Product_Type.product (DList_set dxs) (DList_set dys)) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''product DList_set DList_set: ceq2 = None'') (\_. Product_Type.product (DList_set dxs) (DList_set dys)) | Some _ \ DList_set (DList_Set.product dxs dys))" "Product_Type.product (RBT_set rbt1) B2 = (case ID CCOMPARE('c) of None \ Code.abort (STR ''product RBT_set: ccompare1 = None'') (\_. Product_Type.product (RBT_set rbt1) B2) | Some _ \ RBT_Set2.fold (\x rest. Pair x ` B2 \ rest) rbt1 {})" (is "?rbt1") "Product_Type.product A2 (RBT_set rbt2) = (case ID CCOMPARE('d) of None \ Code.abort (STR ''product RBT_set: ccompare2 = None'') (\_. Product_Type.product A2 (RBT_set rbt2)) | Some _ \ RBT_Set2.fold (\y rest. (\x. (x, y)) ` A2 \ rest) rbt2 {})" (is "?rbt2") "Product_Type.product (RBT_set rbt1) (RBT_set rbt2) = (case ID CCOMPARE('c) of None \ Code.abort (STR ''product RBT_set RBT_set: ccompare1 = None'') (\_. Product_Type.product (RBT_set rbt1) (RBT_set rbt2)) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''product RBT_set RBT_set: ccompare2 = None'') (\_. Product_Type.product (RBT_set rbt1) (RBT_set rbt2)) | Some _ \ RBT_set (RBT_Set2.product rbt1 rbt2))" proof - have [simp]: "\a zs. fold (\y. (#) (a, y)) ys zs = rev (map (Pair a) ys) @ zs" by(induct ys) simp_all have [simp]: "\zs. fold (\x. fold (\y rest. (x, y) # rest) ys) xs zs = rev (concat (map (\x. map (Pair x) ys) xs)) @ zs" by(induct xs) simp_all show ?Set_Monad by(auto simp add: Product_Type.product_def) { fix xs :: "'a list" have "fold (\x. (\) (Pair x ` B1)) xs {} = set xs \ B1" by(induct xs rule: rev_induct) auto } thus ?dlist1 by(simp add: Product_Type.product_def DList_set_def DList_Set.fold.rep_eq DList_Set.Collect_member split: option.split) { fix ys :: "'b list" have "fold (\y. (\) ((\x. (x, y)) ` A1)) ys {} = A1 \ set ys" by(induct ys rule: rev_induct) auto } thus ?dlist2 by(simp add: Product_Type.product_def DList_set_def DList_Set.fold.rep_eq DList_Set.Collect_member split: option.split) { fix xs :: "'c list" have "fold (\x. (\) (Pair x ` B2)) xs {} = set xs \ B2" by(induct xs rule: rev_induct) auto } thus ?rbt1 by(simp add: Product_Type.product_def RBT_set_def RBT_Set2.member_product RBT_Set2.member_conv_keys fold_conv_fold_keys split: option.split) { fix ys :: "'d list" have "fold (\y. (\) ((\x. (x, y)) ` A2)) ys {} = A2 \ set ys" by(induct ys rule: rev_induct) auto } thus ?rbt2 by(simp add: Product_Type.product_def RBT_set_def RBT_Set2.member_product RBT_Set2.member_conv_keys fold_conv_fold_keys split: option.split) qed(auto simp add: RBT_set_def DList_set_def Product_Type.product_def DList_Set.product_member RBT_Set2.member_product split: option.split) lemma Id_on_code [code]: fixes A :: "'a :: ceq set" and dxs :: "'a set_dlist" and P :: "'a \ bool" and rbt :: "'b :: ccompare set_rbt" shows "Id_on B = (\x. (x, x)) ` B" and Id_on_Complement [set_complement_code]: "Id_on (Complement A) = (case ID CEQ('a) of None \ Code.abort (STR ''Id_on Complement: ceq = None'') (\_. Id_on (Complement A)) | Some eq \ Collect_set (\(x, y). eq x y \ x \ A))" and "Id_on (Collect_set P) = (case ID CEQ('a) of None \ Code.abort (STR ''Id_on Collect_set: ceq = None'') (\_. Id_on (Collect_set P)) | Some eq \ Collect_set (\(x, y). eq x y \ P x))" "Id_on (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''Id_on DList_set: ceq = None'') (\_. Id_on (DList_set dxs)) | Some _ \ DList_set (DList_Set.Id_on dxs))" "Id_on (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''Id_on RBT_set: ccompare = None'') (\_. Id_on (RBT_set rbt)) | Some _ \ RBT_set (RBT_Set2.Id_on rbt))" by(auto simp add: DList_set_def RBT_set_def DList_Set.member_Id_on RBT_Set2.member_Id_on dest: equal.equal_eq[OF ID_ceq] split: option.split) lemma Image_code [code]: fixes dxs :: "('a :: ceq \ 'b :: ceq) set_dlist" and rbt :: "('c :: ccompare \ 'd :: ccompare) set_rbt" shows "X `` Y = snd ` Set.filter (\(x, y). x \ Y) X" (is ?generic) "Set_Monad rxs `` A = Set_Monad (fold (\(x, y) rest. if x \ A then y # rest else rest) rxs [])" (is ?Set_Monad) "DList_set dxs `` B = (case ID CEQ('a) of None \ Code.abort (STR ''Image DList_set: ceq1 = None'') (\_. DList_set dxs `` B) | Some _ \ case ID CEQ('b) of None \ Code.abort (STR ''Image DList_set: ceq2 = None'') (\_. DList_set dxs `` B) | Some _ \ DList_Set.fold (\(x, y) acc. if x \ B then insert y acc else acc) dxs {})" (is ?DList_set) "RBT_set rbt `` C = (case ID CCOMPARE('c) of None \ Code.abort (STR ''Image RBT_set: ccompare1 = None'') (\_. RBT_set rbt `` C) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''Image RBT_set: ccompare2 = None'') (\_. RBT_set rbt `` C) | Some _ \ RBT_Set2.fold (\(x, y) acc. if x \ C then insert y acc else acc) rbt {})" (is ?RBT_set) proof - show ?generic by(auto intro: rev_image_eqI) have "set (fold (\(x, y) rest. if x \ A then y # rest else rest) rxs []) = set rxs `` A" by(induct rxs rule: rev_induct)(auto split: if_split_asm) thus ?Set_Monad by(auto) { fix dxs :: "('a \ 'b) list" have "fold (\(x, y) acc. if x \ B then insert y acc else acc) dxs {} = set dxs `` B" by(induct dxs rule: rev_induct)(auto split: if_split_asm) } thus ?DList_set by(clarsimp simp add: DList_set_def Collect_member ceq_prod_def ID_Some DList_Set.fold.rep_eq split: option.split) { fix rbt :: "(('c \ 'd) \ unit) list" have "fold (\(a, _). case a of (x, y) \ \acc. if x \ C then insert y acc else acc) rbt {} = (fst ` set rbt) `` C" by(induct rbt rule: rev_induct)(auto simp add: split_beta split: if_split_asm) } thus ?RBT_set by(clarsimp simp add: RBT_set_def ccompare_prod_def ID_Some RBT_Set2.fold.rep_eq member_conv_keys RBT_Set2.keys.rep_eq RBT_Impl.fold_def RBT_Impl.keys_def split: option.split) qed lemma insert_relcomp: "insert (a, b) A O B = A O B \ {a} \ {c. (b, c) \ B}" by auto lemma trancl_code [code]: "trancl A = (if finite A then ntrancl (card A - 1) A else Code.abort (STR ''trancl: infinite set'') (\_. trancl A))" by (simp add: finite_trancl_ntranl) lemma set_relcomp_set: "set xs O set ys = fold (\(x, y). fold (\(y', z) A. if y = y' then insert (x, z) A else A) ys) xs {}" proof(induct xs rule: rev_induct) case Nil show ?case by simp next case (snoc x xs) note [[show_types]] { fix a :: 'a and b :: 'c and X :: "('a \ 'b) set" have "fold (\(y', z) A. if b = y' then insert (a, z) A else A) ys X = X \ {a} \ {c. (b, c) \ set ys}" by(induct ys arbitrary: X rule: rev_induct)(auto split: if_split_asm) } thus ?case using snoc by(cases x)(simp add: insert_relcomp) qed lemma If_not: "(if \ a then b else c) = (if a then c else b)" by auto lemma relcomp_code [code]: fixes rbt1 :: "('a :: ccompare \ 'b :: ccompare) set_rbt" and rbt2 :: "('b \ 'c :: ccompare) set_rbt" and rbt3 :: "('a \ 'd :: {ccompare, ceq}) set_rbt" and rbt4 :: "('d \ 'a) set_rbt" and rbt5 :: "('b \ 'a) set_rbt" and dxs1 :: "('d \ 'e :: ceq) set_dlist" and dxs2 :: "('e \ 'd) set_dlist" and dxs3 :: "('e \ 'f :: ceq) set_dlist" and dxs4 :: "('f \ 'g :: ceq) set_dlist" and xs1 :: "('h \ 'i :: ceq) list" and xs2 :: "('i \ 'j) list" and xs3 :: "('b \ 'h) list" and xs4 :: "('h \ 'b) list" and xs5 :: "('f \ 'h) list" and xs6 :: "('h \ 'f) list" shows "RBT_set rbt1 O RBT_set rbt2 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp RBT_set RBT_set: ccompare1 = None'') (\_. RBT_set rbt1 O RBT_set rbt2) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''relcomp RBT_set RBT_set: ccompare2 = None'') (\_. RBT_set rbt1 O RBT_set rbt2) | Some c_b \ case ID CCOMPARE('c) of None \ Code.abort (STR ''relcomp RBT_set RBT_set: ccompare3 = None'') (\_. RBT_set rbt1 O RBT_set rbt2) | Some _ \ RBT_Set2.fold (\(x, y). RBT_Set2.fold (\(y', z) A. if c_b y y' \ Eq then A else insert (x, z) A) rbt2) rbt1 {})" (is ?rbt_rbt) "RBT_set rbt3 O DList_set dxs1 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ccompare1 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ccompare2 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some _ \ case ID CEQ('d) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ceq2 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some eq \ case ID CEQ('e) of None \ Code.abort (STR ''relcomp RBT_set DList_set: ceq3 = None'') (\_. RBT_set rbt3 O DList_set dxs1) | Some _ \ RBT_Set2.fold (\(x, y). DList_Set.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) dxs1) rbt3 {})" (is ?rbt_dlist) "DList_set dxs2 O RBT_set rbt4 = (case ID CEQ('e) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ceq1 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some _ \ case ID CCOMPARE('d) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ceq2 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some _ \ case ID CEQ('d) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ccompare2 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some eq \ case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp DList_set RBT_set: ccompare3 = None'') (\_. DList_set dxs2 O RBT_set rbt4) | Some _ \ DList_Set.fold (\(x, y). RBT_Set2.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) rbt4) dxs2 {})" (is ?dlist_rbt) "DList_set dxs3 O DList_set dxs4 = (case ID CEQ('e) of None \ Code.abort (STR ''relcomp DList_set DList_set: ceq1 = None'') (\_. DList_set dxs3 O DList_set dxs4) | Some _ \ case ID CEQ('f) of None \ Code.abort (STR ''relcomp DList_set DList_set: ceq2 = None'') (\_. DList_set dxs3 O DList_set dxs4) | Some eq \ case ID CEQ('g) of None \ Code.abort (STR ''relcomp DList_set DList_set: ceq3 = None'') (\_. DList_set dxs3 O DList_set dxs4) | Some _ \ DList_Set.fold (\(x, y). DList_Set.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) dxs4) dxs3 {})" (is ?dlist_dlist) "Set_Monad xs1 O Set_Monad xs2 = (case ID CEQ('i) of None \ Code.abort (STR ''relcomp Set_Monad Set_Monad: ceq = None'') (\_. Set_Monad xs1 O Set_Monad xs2) | Some eq \ fold (\(x, y). fold (\(y', z) A. if eq y y' then insert (x, z) A else A) xs2) xs1 {})" (is ?monad_monad) "RBT_set rbt1 O Set_Monad xs3 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp RBT_set Set_Monad: ccompare1 = None'') (\_. RBT_set rbt1 O Set_Monad xs3) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''relcomp RBT_set Set_Monad: ccompare2 = None'') (\_. RBT_set rbt1 O Set_Monad xs3) | Some c_b \ RBT_Set2.fold (\(x, y). fold (\(y', z) A. if c_b y y' \ Eq then A else insert (x, z) A) xs3) rbt1 {})" (is ?rbt_monad) "Set_Monad xs4 O RBT_set rbt5 = (case ID CCOMPARE('a) of None \ Code.abort (STR ''relcomp Set_Monad RBT_set: ccompare1 = None'') (\_. Set_Monad xs4 O RBT_set rbt5) | Some _ \ case ID CCOMPARE('b) of None \ Code.abort (STR ''relcomp Set_Monad RBT_set: ccompare2 = None'') (\_. Set_Monad xs4 O RBT_set rbt5) | Some c_b \ fold (\(x, y). RBT_Set2.fold (\(y', z) A. if c_b y y' \ Eq then A else insert (x, z) A) rbt5) xs4 {})" (is ?monad_rbt) "DList_set dxs3 O Set_Monad xs5 = (case ID CEQ('e) of None \ Code.abort (STR ''relcomp DList_set Set_Monad: ceq1 = None'') (\_. DList_set dxs3 O Set_Monad xs5) | Some _ \ case ID CEQ('f) of None \ Code.abort (STR ''relcomp DList_set Set_Monad: ceq2 = None'') (\_. DList_set dxs3 O Set_Monad xs5) | Some eq \ DList_Set.fold (\(x, y). fold (\(y', z) A. if eq y y' then insert (x, z) A else A) xs5) dxs3 {})" (is ?dlist_monad) "Set_Monad xs6 O DList_set dxs4 = (case ID CEQ('f) of None \ Code.abort (STR ''relcomp Set_Monad DList_set: ceq1 = None'') (\_. Set_Monad xs6 O DList_set dxs4) | Some eq \ case ID CEQ('g) of None \ Code.abort (STR ''relcomp Set_Monad DList_set: ceq2 = None'') (\_. Set_Monad xs6 O DList_set dxs4) | Some _ \ fold (\(x, y). DList_Set.fold (\(y', z) A. if eq y y' then insert (x, z) A else A) dxs4) xs6 {})" (is ?monad_dlist) proof - show ?rbt_rbt ?rbt_monad ?monad_rbt by(auto simp add: comparator.eq[OF ID_ccompare'] RBT_set_def ccompare_prod_def member_conv_keys ID_Some RBT_Set2.fold_conv_fold_keys' RBT_Set2.keys.rep_eq If_not set_relcomp_set split: option.split del: equalityI) show ?rbt_dlist ?dlist_rbt ?dlist_dlist ?monad_monad ?dlist_monad ?monad_dlist by(auto simp add: RBT_set_def DList_set_def member_conv_keys ID_Some ccompare_prod_def ceq_prod_def Collect_member RBT_Set2.fold_conv_fold_keys' RBT_Set2.keys.rep_eq DList_Set.fold.rep_eq set_relcomp_set dest: equal.equal_eq[OF ID_ceq] split: option.split del: equalityI) qed lemma irrefl_code [code]: fixes r :: "('a :: {ceq, ccompare} \ 'a) set" shows "irrefl r \ (case ID CEQ('a) of Some eq \ (\(x, y) \ r. \ eq x y) | None \ case ID CCOMPARE('a) of None \ Code.abort (STR ''irrefl: ceq = None & ccompare = None'') (\_. irrefl r) | Some c \ (\(x, y) \ r. c x y \ Eq))" apply(auto simp add: irrefl_distinct comparator.eq[OF ID_ccompare'] split: option.split dest!: ID_ceq[THEN equal.equal_eq]) done lemma wf_code [code]: fixes rbt :: "('a :: ccompare \ 'a) set_rbt" and dxs :: "('b :: ceq \ 'b) set_dlist" shows "wf (Set_Monad xs) = acyclic (Set_Monad xs)" "wf (RBT_set rbt) = (case ID CCOMPARE('a) of None \ Code.abort (STR ''wf RBT_set: ccompare = None'') (\_. wf (RBT_set rbt)) | Some _ \ acyclic (RBT_set rbt))" "wf (DList_set dxs) = (case ID CEQ('b) of None \ Code.abort (STR ''wf DList_set: ceq = None'') (\_. wf (DList_set dxs)) | Some _ \ acyclic (DList_set dxs))" by(auto simp add: wf_iff_acyclic_if_finite split: option.split del: iffI)(simp_all add: wf_iff_acyclic_if_finite finite_code ccompare_prod_def ceq_prod_def ID_Some) lemma bacc_code [code]: "bacc R 0 = - snd ` R" "bacc R (Suc n) = (let rec = bacc R n in rec \ - snd ` (Set.filter (\(y, x). y \ rec) R))" by(auto intro: rev_image_eqI simp add: Let_def) (* TODO: acc could also be computed for infinite universes if r is finite *) lemma acc_code [code]: fixes A :: "('a :: {finite, card_UNIV} \ 'a) set" shows "Wellfounded.acc A = bacc A (of_phantom (card_UNIV :: 'a card_UNIV))" by(simp add: card_UNIV acc_bacc_eq) lemma sorted_list_of_set_code [code]: fixes dxs :: "'a :: {linorder, ceq} set_dlist" and rbt :: "'b :: {linorder, ccompare} set_rbt" shows "sorted_list_of_set (Set_Monad xs) = sort (remdups xs)" "sorted_list_of_set (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''sorted_list_of_set DList_set: ceq = None'') (\_. sorted_list_of_set (DList_set dxs)) | Some _ \ sort (list_of_dlist dxs))" "sorted_list_of_set (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''sorted_list_of_set RBT_set: ccompare = None'') (\_. sorted_list_of_set (RBT_set rbt)) | Some _ \ sort (RBT_Set2.keys rbt))" \ \We must sort the keys because @{term ccompare}'s ordering need not coincide with @{term linorder}'s.\ by(auto simp add: DList_set_def RBT_set_def sorted_list_of_set_sort_remdups Collect_member distinct_remdups_id distinct_list_of_dlist member_conv_keys split: option.split) lemma map_project_set: "List.map_project f (set xs) = set (List.map_filter f xs)" by(auto simp add: List.map_project_def List.map_filter_def intro: rev_image_eqI) lemma map_project_simps: shows map_project_empty: "List.map_project f {} = {}" and map_project_insert: "List.map_project f (insert x A) = (case f x of None \ List.map_project f A | Some y \ insert y (List.map_project f A))" by(auto simp add: List.map_project_def split: option.split) lemma map_project_conv_fold: "List.map_project f (set xs) = fold (\x A. case f x of None \ A | Some y \ insert y A) xs {}" by(induct xs rule: rev_induct)(simp_all add: map_project_simps cong: option.case_cong) lemma map_project_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "List.map_project f (Set_Monad xs) = Set_Monad (List.map_filter f xs)" "List.map_project g (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''map_project DList_set: ceq = None'') (\_. List.map_project g (DList_set dxs)) | Some _ \ DList_Set.fold (\x A. case g x of None \ A | Some y \ insert y A) dxs {})" (is ?dlist) "List.map_project h (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''map_project RBT_set: ccompare = None'') (\_. List.map_project h (RBT_set rbt)) | Some _ \ RBT_Set2.fold (\x A. case h x of None \ A | Some y \ insert y A) rbt {})" (is ?rbt) proof - show ?dlist ?rbt by(auto split: option.split simp add: RBT_set_def DList_set_def DList_Set.fold.rep_eq Collect_member map_project_conv_fold RBT_Set2.fold_conv_fold_keys member_conv_keys del: equalityI) qed(auto simp add: List.map_project_def List.map_filter_def intro: rev_image_eqI) lemma Bleast_code [code]: "Bleast A P = (if finite A then case filter P (sorted_list_of_set A) of [] \ abort_Bleast A P | x # xs \ x else abort_Bleast A P)" proof(cases "finite A") case True hence *: "A = set (sorted_list_of_set A)" by(simp add: sorted_list_of_set) show ?thesis using True by(subst (1 3) *)(unfold Bleast_code, simp add: sorted_sort_id) qed(simp add: abort_Bleast_def Bleast_def) lemma can_select_code [code]: fixes xs :: "'a :: ceq list" and dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "can_select P (Set_Monad xs) = (case ID CEQ('a) of None \ Code.abort (STR ''can_select Set_Monad: ceq = None'') (\_. can_select P (Set_Monad xs)) | Some eq \ case filter P xs of Nil \ False | x # xs \ list_all (eq x) xs)" (is ?Set_Monad) "can_select Q (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''can_select DList_set: ceq = None'') (\_. can_select Q (DList_set dxs)) | Some _ \ DList_Set.length (DList_Set.filter Q dxs) = 1)" (is ?dlist) "can_select R (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''can_select RBT_set: ccompare = None'') (\_. can_select R (RBT_set rbt)) | Some _ \ singleton_list_fusion (filter_generator R rbt_keys_generator) (RBT_Set2.init rbt))" (is ?rbt) proof - show ?Set_Monad apply(auto split: option.split list.split dest!: ID_ceq[THEN equal.equal_eq] dest: filter_eq_ConsD simp add: can_select_def filter_empty_conv list_all_iff) apply(drule filter_eq_ConsD, fastforce) apply(drule filter_eq_ConsD, clarsimp, blast) done show ?dlist by(clarsimp simp add: can_select_def card_eq_length[symmetric] Set_member_code card_eq_Suc_0_ex1 simp del: card_eq_length split: option.split) note [simp del] = distinct_keys show ?rbt using distinct_keys[of rbt] apply(auto simp add: can_select_def singleton_list_fusion_def unfoldr_filter_generator unfoldr_rbt_keys_generator Set_member_code member_conv_keys filter_empty_conv empty_filter_conv split: option.split list.split dest: filter_eq_ConsD) apply(drule filter_eq_ConsD, fastforce) apply(drule filter_eq_ConsD, fastforce simp add: empty_filter_conv) apply(drule filter_eq_ConsD) apply clarsimp apply(drule Cons_eq_filterD) apply clarify apply(simp (no_asm_use)) apply blast done qed lemma pred_of_set_code [code]: fixes dxs :: "'a :: ceq set_dlist" and rbt :: "'b :: ccompare set_rbt" shows "pred_of_set (Set_Monad xs) = fold (sup \ Predicate.single) xs bot" "pred_of_set (DList_set dxs) = (case ID CEQ('a) of None \ Code.abort (STR ''pred_of_set DList_set: ceq = None'') (\_. pred_of_set (DList_set dxs)) | Some _ \ DList_Set.fold (sup \ Predicate.single) dxs bot)" "pred_of_set (RBT_set rbt) = (case ID CCOMPARE('b) of None \ Code.abort (STR ''pred_of_set RBT_set: ccompare = None'') (\_. pred_of_set (RBT_set rbt)) | Some _ \ RBT_Set2.fold (sup \ Predicate.single) rbt bot)" by(auto simp add: pred_of_set_set_fold_sup fold_map DList_set_def RBT_set_def Collect_member member_conv_keys DList_Set.fold.rep_eq fold_conv_fold_keys split: option.split) text \ @{typ "'a Predicate.pred"} is implemented as a monad, so we keep the monad when converting to @{typ "'a set"}. For this case, @{term insert_monad} and @{term union_monad} avoid the unnecessary dictionary construction. \ definition insert_monad :: "'a \ 'a set \ 'a set" where [simp]: "insert_monad = insert" definition union_monad :: "'a set \ 'a set \ 'a set" where [simp]: "union_monad = (\)" lemma insert_monad_code [code]: "insert_monad x (Set_Monad xs) = Set_Monad (x # xs)" by simp lemma union_monad_code [code]: "union_monad (Set_Monad xs) (Set_Monad ys) = Set_Monad (xs @ ys)" by(simp) lemma set_of_pred_code [code]: "set_of_pred (Predicate.Seq f) = (case f () of seq.Empty \ Set_Monad [] | seq.Insert x P \ insert_monad x (set_of_pred P) | seq.Join P xq \ union_monad (set_of_pred P) (set_of_seq xq))" by(simp add: of_pred_code cong: seq.case_cong) lemma set_of_seq_code [code]: "set_of_seq seq.Empty = Set_Monad []" "set_of_seq (seq.Insert x P) = insert_monad x (set_of_pred P)" "set_of_seq (seq.Join P xq) = union_monad (set_of_pred P) (set_of_seq xq)" by(simp_all add: of_seq_code) hide_const (open) insert_monad union_monad subsection \Type class instantiations\ datatype set_impl = Set_IMPL declare set_impl.eq.simps [code del] set_impl.size [code del] set_impl.rec [code del] set_impl.case [code del] lemma [code]: fixes x :: set_impl shows "size x = 0" and "size_set_impl x = 0" by(case_tac [!] x) simp_all definition set_Choose :: set_impl where [simp]: "set_Choose = Set_IMPL" definition set_Collect :: set_impl where [simp]: "set_Collect = Set_IMPL" definition set_DList :: set_impl where [simp]: "set_DList = Set_IMPL" definition set_RBT :: set_impl where [simp]: "set_RBT = Set_IMPL" definition set_Monad :: set_impl where [simp]: "set_Monad = Set_IMPL" code_datatype set_Choose set_Collect set_DList set_RBT set_Monad definition set_empty_choose :: "'a set" where [simp]: "set_empty_choose = {}" lemma set_empty_choose_code [code]: "(set_empty_choose :: 'a :: {ceq, ccompare} set) = (case CCOMPARE('a) of Some _ \ RBT_set RBT_Set2.empty | None \ case CEQ('a) of None \ Set_Monad [] | Some _ \ DList_set (DList_Set.empty))" by(simp split: option.split) definition set_impl_choose2 :: "set_impl \ set_impl \ set_impl" where [simp]: "set_impl_choose2 = (\_ _. Set_IMPL)" lemma set_impl_choose2_code [code]: "set_impl_choose2 x y = set_Choose" "set_impl_choose2 set_Collect set_Collect = set_Collect" "set_impl_choose2 set_DList set_DList = set_DList" "set_impl_choose2 set_RBT set_RBT = set_RBT" "set_impl_choose2 set_Monad set_Monad = set_Monad" by(simp_all) definition set_empty :: "set_impl \ 'a set" where [simp]: "set_empty = (\_. {})" lemma set_empty_code [code]: "set_empty set_Collect = Collect_set (\_. False)" "set_empty set_DList = DList_set DList_Set.empty" "set_empty set_RBT = RBT_set RBT_Set2.empty" "set_empty set_Monad = Set_Monad []" "set_empty set_Choose = set_empty_choose" by(simp_all) class set_impl = fixes set_impl :: "('a, set_impl) phantom" syntax (input) "_SET_IMPL" :: "type => logic" ("(1SET'_IMPL/(1'(_')))") parse_translation \ let fun set_impl_tr [ty] = (Syntax.const @{syntax_const "_constrain"} $ Syntax.const @{const_syntax "set_impl"} $ (Syntax.const @{type_syntax phantom} $ ty $ Syntax.const @{type_syntax set_impl})) | set_impl_tr ts = raise TERM ("set_impl_tr", ts); in [(@{syntax_const "_SET_IMPL"}, K set_impl_tr)] end \ declare [[code drop: "{}"]] lemma empty_code [code, code_unfold]: "({} :: 'a :: set_impl set) = set_empty (of_phantom SET_IMPL('a))" by simp subsection \Generator for the @{class set_impl}-class\ text \ This generator registers itself at the derive-manager for the classes @{class set_impl}. Here, one can choose the desired implementation via the parameter. \begin{itemize} \item \texttt{instantiation type :: (type,\ldots,type) (rbt,dlist,collect,monad,choose, or arbitrary constant name) set-impl} \end{itemize} \ text \ This generator can be used for arbitrary types, not just datatypes. \ ML_file \set_impl_generator.ML\ derive (dlist) set_impl unit bool derive (rbt) set_impl nat derive (set_RBT) set_impl int (* shows usage of constant names *) derive (dlist) set_impl Enum.finite_1 Enum.finite_2 Enum.finite_3 derive (rbt) set_impl integer natural derive (rbt) set_impl char instantiation sum :: (set_impl, set_impl) set_impl begin definition "SET_IMPL('a + 'b) = Phantom('a + 'b) (set_impl_choose2 (of_phantom SET_IMPL('a)) (of_phantom SET_IMPL('b)))" instance .. end instantiation prod :: (set_impl, set_impl) set_impl begin definition "SET_IMPL('a * 'b) = Phantom('a * 'b) (set_impl_choose2 (of_phantom SET_IMPL('a)) (of_phantom SET_IMPL('b)))" instance .. end derive (choose) set_impl list derive (rbt) set_impl String.literal instantiation option :: (set_impl) set_impl begin definition "SET_IMPL('a option) = Phantom('a option) (of_phantom SET_IMPL('a))" instance .. end derive (monad) set_impl "fun" derive (choose) set_impl set instantiation phantom :: (type, set_impl) set_impl begin definition "SET_IMPL(('a, 'b) phantom) = Phantom (('a, 'b) phantom) (of_phantom SET_IMPL('b))" instance .. end text \ We enable automatic implementation selection for sets constructed by @{const set}, although they could be directly converted using @{const Set_Monad} in constant time. However, then it is more likely that the parameters of binary operators have different implementations, which can lead to less efficient execution. However, we test whether automatic selection picks @{const Set_Monad} anyway and take a short-cut. \ definition set_aux :: "set_impl \ 'a list \ 'a set" where [simp, code del]: "set_aux _ = set" lemma set_aux_code [code]: defines "conv \ foldl (\s (x :: 'a). insert x s)" shows "set_aux impl = conv (set_empty impl)" (is "?thesis1") "set_aux set_Choose = (case CCOMPARE('a :: {ccompare, ceq}) of Some _ \ conv (RBT_set RBT_Set2.empty) | None \ case CEQ('a) of None \ Set_Monad | Some _ \ conv (DList_set DList_Set.empty))" (is "?thesis2") "set_aux set_Monad = Set_Monad" proof - have "conv {} = set" by(rule ext)(induct_tac x rule: rev_induct, simp_all add: conv_def) thus ?thesis1 ?thesis2 by(simp_all split: option.split) qed simp lemma set_code [code]: fixes xs :: "'a :: set_impl list" shows "set xs = set_aux (of_phantom (ID SET_IMPL('a))) xs" by(simp) subsection \Pretty printing for sets\ text \ @{term code_post} marks contexts (as hypothesis) in which we use code\_post as a decision procedure rather than a pretty-printing engine. The intended use is to enable more rules when proving assumptions of rewrite rules. \ definition code_post :: bool where "code_post = True" lemma conj_code_post [code_post]: assumes code_post shows "True & x \ x" "False & x \ False" by simp_all text \ A flag to switch post-processing of sets on and off. Use \verb$declare pretty_sets[code_post del]$ to disable pretty printing of sets in value. \ definition code_post_set :: bool where pretty_sets [code_post, simp]: "code_post_set = True" definition collapse_RBT_set :: "'a set_rbt \ 'a :: ccompare set \ 'a set" where "collapse_RBT_set r M = set (RBT_Set2.keys r) \ M" lemma RBT_set_collapse_RBT_set [code_post]: fixes r :: "'a :: ccompare set_rbt" assumes "code_post \ is_ccompare TYPE('a)" and code_post_set shows "RBT_set r = collapse_RBT_set r {}" using assms by(clarsimp simp add: code_post_def is_ccompare_def RBT_set_def member_conv_keys collapse_RBT_set_def) lemma collapse_RBT_set_Branch [code_post]: "collapse_RBT_set (Mapping_RBT (Branch c l x v r)) M = collapse_RBT_set (Mapping_RBT l) (insert x (collapse_RBT_set (Mapping_RBT r) M))" unfolding collapse_RBT_set_def by(auto simp add: is_ccompare_def set_keys_Mapping_RBT) lemma collapse_RBT_set_Empty [code_post]: "collapse_RBT_set (Mapping_RBT rbt.Empty) M = M" by(auto simp add: collapse_RBT_set_def set_keys_Mapping_RBT) definition collapse_DList_set :: "'a :: ceq set_dlist \ 'a set" where "collapse_DList_set dxs = set (DList_Set.list_of_dlist dxs)" lemma DList_set_collapse_DList_set [code_post]: fixes dxs :: "'a :: ceq set_dlist" assumes "code_post \ is_ceq TYPE('a)" and code_post_set shows "DList_set dxs = collapse_DList_set dxs" using assms by(clarsimp simp add: code_post_def DList_set_def is_ceq_def collapse_DList_set_def Collect_member) lemma collapse_DList_set_empty [code_post]: "collapse_DList_set (Abs_dlist []) = {}" by(simp add: collapse_DList_set_def Abs_dlist_inverse) lemma collapse_DList_set_Cons [code_post]: "collapse_DList_set (Abs_dlist (x # xs)) = insert x (collapse_DList_set (Abs_dlist xs))" by(simp add: collapse_DList_set_def set_list_of_dlist_Abs_dlist) lemma Set_Monad_code_post [code_post]: assumes code_post_set shows "Set_Monad [] = {}" and "Set_Monad (x#xs) = insert x (Set_Monad xs)" by simp_all end diff --git a/thys/Containers/Set_Linorder.thy b/thys/Containers/Set_Linorder.thy --- a/thys/Containers/Set_Linorder.thy +++ b/thys/Containers/Set_Linorder.thy @@ -1,2481 +1,2481 @@ (* Title: Containers/Set_Linorder.thy Author: Andreas Lochbihler, KIT *) theory Set_Linorder imports Containers_Auxiliary Lexicographic_Order Extend_Partial_Order "HOL-Library.Cardinality" begin section \An executable linear order on sets\ subsection \Definition of the linear order\ subsubsection \Extending finite and cofinite sets\ text \ Partition sets into finite and cofinite sets and distribute the rest arbitrarily such that complement switches between the two. \ consts infinite_complement_partition :: "'a set set" specification (infinite_complement_partition) finite_complement_partition: "finite (A :: 'a set) \ A \ infinite_complement_partition" complement_partition: "\ finite (UNIV :: 'a set) \ (A :: 'a set) \ infinite_complement_partition \ - A \ infinite_complement_partition" proof(cases "finite (UNIV :: 'a set)") case False define Field_r where "Field_r = {\

:: 'a set set. (\C \ \

. - C \ \

) \ (\A. finite A \ A \ \

)}" define r where "r = {(\

1, \

2). \

1 \ \

2 \ \

1 \ Field_r \ \

2 \ Field_r}" have in_Field_r [simp]: "\\

. \

\ Field_r \ (\C \ \

. - C \ \

) \ (\A. finite A \ A \ \

)" unfolding Field_r_def by simp have in_r [simp]: "\\

1 \

2. (\

1, \

2) \ r \ \

1 \ \

2 \ \

1 \ Field_r \ \

2 \ Field_r" unfolding r_def by simp have Field_r [simp]: "Field r = Field_r" by(auto simp add: Field_def Field_r_def) have "Partial_order r" by(auto simp add: Field_def r_def partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI) moreover have "\\ \ Field r. \\ \ \. (\, \) \ r" if \: "\ \ Chains r" for \ proof - let ?\ = "\\ \ {A. finite A}" have *: "?\ \ Field r" using False \ by clarsimp(safe, drule (2) ChainsD, auto 4 4 dest: Chains_Field) hence "\\. \ \ \ \ (\, ?\) \ r" using \ by(auto simp del: in_Field_r dest: Chains_Field) with * show "\\ \ Field r. \\ \ \. (\, \) \ r" by blast qed ultimately have "\\

\ Field r. \\ \ Field r. (\

, \) \ r \ \ = \

" by(rule Zorns_po_lemma) then obtain \

where \

: "\

\ Field r" and max: "\\. \ \ \ Field r; (\

, \) \ r \ \ \ = \

" by blast have "\A. finite A \ A \ \

" using \

by simp moreover { fix C have "C \ \

\ - C \ \

" proof(rule ccontr) assume "\ ?thesis" hence C: "C \ \

" "- C \ \

" by simp_all let ?\ = "insert C \

" have *: "?\ \ Field r" using C \

by auto hence "(\

, ?\) \ r" using \

by auto with * have "?\ = \

" by(rule max) thus False using C by auto qed hence "C \ \

\ - C \ \

" using \

by auto } ultimately have "\\

:: 'a set set. (\A. finite A \ A \ \

) \ (\C. C \ \

\ - C \ \

)" by blast thus ?thesis by metis qed auto lemma not_in_complement_partition: "\ finite (UNIV :: 'a set) \ (A :: 'a set) \ infinite_complement_partition \ - A \ infinite_complement_partition" by(metis complement_partition) lemma not_in_complement_partition_False: "\ (A :: 'a set) \ infinite_complement_partition; \ finite (UNIV :: 'a set) \ \ - A \ infinite_complement_partition = False" by(simp add: not_in_complement_partition) lemma infinite_complement_partition_finite [simp]: "finite (UNIV :: 'a set) \ infinite_complement_partition = (UNIV :: 'a set set)" by(auto intro: finite_subset finite_complement_partition) lemma Compl_eq_empty_iff: "- A = {} \ A = UNIV" by auto subsubsection \A lexicographic-style order on finite subsets\ context ord begin definition set_less_aux :: "'a set \ 'a set \ bool" (infix "\''" 50) where "A \' B \ finite A \ finite B \ (\y \ B - A. \z \ (A - B) \ (B - A). y \ z \ (z \ y \ y = z))" definition set_less_eq_aux :: "'a set \ 'a set \ bool" (infix "\''" 50) where "A \' B \ A \ infinite_complement_partition \ A = B \ A \' B" lemma set_less_aux_irrefl [iff]: "\ A \' A" by(auto simp add: set_less_aux_def) lemma set_less_eq_aux_refl [iff]: "A \' A \ A \ infinite_complement_partition" by(simp add: set_less_eq_aux_def) lemma set_less_aux_empty [simp]: "\ A \' {}" by(auto simp add: set_less_aux_def intro: finite_subset finite_complement_partition) lemma set_less_eq_aux_empty [simp]: "A \' {} \ A = {}" by(auto simp add: set_less_eq_aux_def finite_complement_partition) lemma set_less_aux_antisym: "\ A \' B; B \' A \ \ False" by(auto simp add: set_less_aux_def split: if_split_asm) lemma set_less_aux_conv_set_less_eq_aux: "A \' B \ A \' B \ \ B \' A" by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym) lemma set_less_eq_aux_antisym: "\ A \' B; B \' A \ \ A = B" by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym) lemma set_less_aux_finiteD: "A \' B \ finite A \ B \ infinite_complement_partition" by(auto simp add: set_less_aux_def finite_complement_partition) lemma set_less_eq_aux_infinite_complement_partitionD: "A \' B \ A \ infinite_complement_partition \ B \ infinite_complement_partition" by(auto simp add: set_less_eq_aux_def dest: set_less_aux_finiteD intro: finite_complement_partition) lemma Compl_set_less_aux_Compl: "finite (UNIV :: 'a set) \ - A \' - B \ B \' A" by(auto simp add: set_less_aux_def finite_subset[OF subset_UNIV]) lemma Compl_set_less_eq_aux_Compl: "finite (UNIV :: 'a set) \ - A \' - B \ B \' A" by(auto simp add: set_less_eq_aux_def Compl_set_less_aux_Compl) lemma set_less_aux_insert_same: "x \ A \ x \ B \ insert x A \' insert x B \ A \' B" by(auto simp add: set_less_aux_def) lemma set_less_eq_aux_insert_same: "\ A \ infinite_complement_partition; insert x B \ infinite_complement_partition; x \ A \ x \ B \ \ insert x A \' insert x B \ A \' B" by(auto simp add: set_less_eq_aux_def set_less_aux_insert_same) end context order begin lemma set_less_aux_singleton_iff: "A \' {x} \ finite A \ (\a\A. x < a)" by(auto simp add: set_less_aux_def less_le Bex_def) end context linorder begin lemma wlog_le [case_names sym le]: assumes "\a b. P a b \ P b a" and "\a b. a \ b \ P a b" shows "P b a" by (metis assms linear) lemma empty_set_less_aux [simp]: "{} \' A \ A \ {} \ finite A" by(auto 4 3 simp add: set_less_aux_def intro!: Min_eqI intro: bexI[where x="Min A"] order_trans[where y="Min A"] Min_in) lemma empty_set_less_eq_aux [simp]: "{} \' A \ finite A" by(auto simp add: set_less_eq_aux_def finite_complement_partition) lemma set_less_aux_trans: assumes AB: "A \' B" and BC: "B \' C" shows "A \' C" proof - from AB BC have A: "finite A" and B: "finite B" and C: "finite C" by(auto simp add: set_less_aux_def) from AB A B obtain ab where ab: "ab \ B - A" and minAB: "\x. \ x \ A; x \ B \ \ ab \ x \ (x \ ab \ ab = x)" and minBA: "\x. \ x \ B; x \ A \ \ ab \ x \ (x \ ab \ ab = x)" unfolding set_less_aux_def by auto from BC B C obtain bc where bc: "bc \ C - B" and minBC: "\x. \ x \ B; x \ C \ \ bc \ x \ (x \ bc \ bc = x)" and minCB: "\x. \ x \ C; x \ B \ \ bc \ x \ (x \ bc \ bc = x)" unfolding set_less_aux_def by auto show ?thesis proof(cases "ab \ bc") case True hence "ab \ C - A" "ab \ A - C" using ab bc by(auto dest: minBC antisym) moreover { fix x assume x: "x \ (C - A) \ (A - C)" hence "ab \ x" by(cases "x \ B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF True]) moreover hence "ab \ x \ \ x \ ab" using ab bc x by(cases "x \ B")(auto dest: antisym) moreover note calculation } ultimately show ?thesis using A C unfolding set_less_aux_def by auto next case False with linear[of ab bc] have "bc \ ab" by simp with ab bc have "bc \ C - A" "bc \ A - C" by(auto dest: minAB antisym) moreover { fix x assume x: "x \ (C - A) \ (A - C)" hence "bc \ x" by(cases "x \ B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF \bc \ ab\]) moreover hence "bc \ x \ \ x \ bc" using ab bc x by(cases "x \ B")(auto dest: antisym) moreover note calculation } ultimately show ?thesis using A C unfolding set_less_aux_def by auto qed qed lemma set_less_eq_aux_trans [trans]: "\ A \' B; B \' C \ \ A \' C" by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans) lemma set_less_trans_set_less_eq [trans]: "\ A \' B; B \' C \ \ A \' C" by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans) lemma set_less_eq_aux_porder: "partial_order_on infinite_complement_partition {(A, B). A \' B}" by(auto simp add: preorder_on_def partial_order_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux_infinite_complement_partitionD intro: set_less_eq_aux_antisym set_less_eq_aux_trans del: equalityI) lemma psubset_finite_imp_set_less_aux: assumes AsB: "A \ B" and B: "finite B" shows "A \' B" proof - from AsB B have A: "finite A" by(auto intro: finite_subset) moreover from AsB B have "Min (B - A) \ B - A" by - (rule Min_in, auto) ultimately show ?thesis using B AsB by(auto simp add: set_less_aux_def intro!: rev_bexI[where x="Min (B - A)"] Min_eqI dest: Min_ge_iff[THEN iffD1, rotated 2]) qed lemma subset_finite_imp_set_less_eq_aux: "\ A \ B; finite B \ \ A \' B" by(cases "A = B")(auto simp add: set_less_eq_aux_def finite_complement_partition intro: psubset_finite_imp_set_less_aux) lemma empty_set_less_aux_finite_iff: "finite A \ {} \' A \ A \ {}" by(auto intro: psubset_finite_imp_set_less_aux) lemma set_less_aux_finite_total: assumes A: "finite A" and B: "finite B" shows "A \' B \ A = B \ B \' A" proof(cases "A \ B \ B \ A") case True thus ?thesis using A B psubset_finite_imp_set_less_aux[of A B] psubset_finite_imp_set_less_aux[of B A] by auto next case False hence A': "\ A \ B" and B': "\ B \ A" and AnB: "A \ B" by auto thus ?thesis using A B proof(induct "Min (B - A)" "Min (A - B)" arbitrary: A B rule: wlog_le) case (sym m n) from sym.hyps[OF refl refl] sym.prems show ?case by blast next case (le A B) note A = \finite A\ and B = \finite B\ and A' = \\ A \ B\ and B' = \\ B \ A\ { fix z assume z: "z \ (A - B) \ (B - A)" hence "Min (B - A) \ z \ (z \ Min (B - A) \ Min (B - A) = z)" proof assume "z \ B - A" hence "Min (B - A) \ z" by(simp add: B) thus ?thesis by auto next assume "z \ A - B" hence "Min (A - B) \ z" by(simp add: A) with le.hyps show ?thesis by(auto) qed } moreover have "Min (B - A) \ B - A" by(rule Min_in)(simp_all add: B B') ultimately have "A \' B" using A B by(auto simp add: set_less_aux_def) thus ?case .. qed qed lemma set_less_eq_aux_finite_total: "\ finite A; finite B \ \ A \' B \ A = B \ B \' A" by(drule (1) set_less_aux_finite_total)(auto simp add: set_less_eq_aux_def) lemma set_less_eq_aux_finite_total2: "\ finite A; finite B \ \ A \' B \ B \' A" by(drule (1) set_less_eq_aux_finite_total)(auto simp add: finite_complement_partition) lemma set_less_aux_rec: assumes A: "finite A" and B: "finite B" and A': "A \ {}" and B': "B \ {}" shows "A \' B \ Min B < Min A \ Min A = Min B \ A - {Min A} \' B - {Min A}" proof(cases "Min A = Min B") case True from A A' B B' have "insert (Min A) A = A" "insert (Min B) B = B" by(auto simp add: ex_in_conv[symmetric] exI) with True show ?thesis by(subst (2) set_less_aux_insert_same[symmetric, where x="Min A"]) simp_all next case False have "A \' B \ Min B < Min A" proof assume AB: "A \' B" with B A obtain ab where ab: "ab \ B - A" and AB: "\x. \ x \ A; x \ B \ \ ab \ x" by(auto simp add: set_less_aux_def) { fix a assume "a \ A" hence "Min B \ a" using A A' B B' ab by(cases "a \ B")(auto intro: order_trans[where y=ab] dest: AB) } hence "Min B \ Min A" using A A' by simp with False show "Min B < Min A" using False by auto next assume "Min B < Min A" hence "\z\A - B \ (B - A). Min B \ z \ (z \ Min B \ Min B = z)" using A B A' B' by(auto 4 4 intro: Min_in Min_eqI dest: bspec bspec[where x="Min B"]) moreover have "Min B \ A" using \Min B < Min A\ by (metis A Min_le not_less) ultimately show "A \' B" using A B A' B' by(simp add: set_less_aux_def bexI[where x="Min B"]) qed thus ?thesis using False by simp qed lemma set_less_eq_aux_rec: assumes "finite A" "finite B" "A \ {}" "B \ {}" shows "A \' B \ Min B < Min A \ Min A = Min B \ A - {Min A} \' B - {Min A}" proof(cases "A = B") case True thus ?thesis using assms by(simp add: finite_complement_partition) next case False moreover hence "Min A = Min B \ A - {Min A} \ B - {Min B}" by (metis (lifting) assms Min_in insert_Diff) ultimately show ?thesis using set_less_aux_rec[OF assms] by(simp add: set_less_eq_aux_def cong: conj_cong) qed lemma set_less_aux_Min_antimono: "\ Min A < Min B; finite A; finite B; A \ {} \ \ B \' A" using set_less_aux_rec[of B A] by(cases "B = {}")(simp_all add: empty_set_less_aux_finite_iff) lemma sorted_Cons_Min: "sorted (x # xs) \ Min (insert x (set xs)) = x" by(auto simp add: intro: Min_eqI) lemma set_less_aux_code: "\ sorted xs; distinct xs; sorted ys; distinct ys \ - \ set xs \' set ys \ order.lexordp (>) xs ys" + \ set xs \' set ys \ ord.lexordp (>) xs ys" apply(induct xs ys rule: list_induct2') - apply(simp_all add: order.lexordp_simps[OF local.dual_order] empty_set_less_aux_finite_iff sorted_Cons_Min set_less_aux_rec neq_Nil_conv) + apply(simp_all add: empty_set_less_aux_finite_iff sorted_Cons_Min set_less_aux_rec neq_Nil_conv) apply(auto cong: conj_cong) done lemma set_less_eq_aux_code: assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys" - shows "set xs \' set ys \ order.lexordp_eq (>) xs ys" + shows "set xs \' set ys \ ord.lexordp_eq (>) xs ys" proof - have dual: "class.linorder (\) (>)" by(rule linorder.dual_linorder) unfold_locales from assms show ?thesis by(auto simp add: set_less_eq_aux_def finite_complement_partition linorder.lexordp_eq_conv_lexord[OF dual] set_less_aux_code intro: sorted_distinct_set_unique) qed end subsubsection \Extending @{term set_less_eq_aux} to have @{term "{}"} as least element\ context ord begin definition set_less_eq_aux' :: "'a set \ 'a set \ bool" (infix "\''''" 50) where "A \'' B \ A \' B \ A = {} \ B \ infinite_complement_partition" lemma set_less_eq_aux'_refl: "A \'' A \ A \ infinite_complement_partition" by(auto simp add: set_less_eq_aux'_def) lemma set_less_eq_aux'_antisym: "\ A \'' B; B \'' A \ \ A = B" by(auto simp add: set_less_eq_aux'_def intro: set_less_eq_aux_antisym del: equalityI) lemma set_less_eq_aux'_infinite_complement_partitionD: "A \'' B \ A \ infinite_complement_partition \ B \ infinite_complement_partition" by(auto simp add: set_less_eq_aux'_def intro: finite_complement_partition dest: set_less_eq_aux_infinite_complement_partitionD) lemma empty_set_less_eq_def [simp]: "{} \'' B \ B \ infinite_complement_partition" by(auto simp add: set_less_eq_aux'_def dest: set_less_eq_aux_infinite_complement_partitionD) end context linorder begin lemma set_less_eq_aux'_trans: "\ A \'' B; B \'' C \ \ A \'' C" by(auto simp add: set_less_eq_aux'_def del: equalityI intro: set_less_eq_aux_trans dest: set_less_eq_aux_infinite_complement_partitionD) lemma set_less_eq_aux'_porder: "partial_order_on infinite_complement_partition {(A, B). A \'' B}" by(auto simp add: partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux'_antisym set_less_eq_aux'_infinite_complement_partitionD simp add: set_less_eq_aux'_refl intro: set_less_eq_aux'_trans) end subsubsection \Extend @{term set_less_eq_aux'} to a total order on @{term infinite_complement_partition}\ context ord begin definition set_less_eq_aux'' :: "'a set \ 'a set \ bool" (infix "\''''''" 50) where "set_less_eq_aux'' = (SOME sleq. (linear_order_on UNIV {(a, b). a \ b} \ linear_order_on infinite_complement_partition {(A, B). sleq A B}) \ order_consistent {(A, B). A \'' B} {(A, B). sleq A B})" lemma set_less_eq_aux''_spec: shows "linear_order {(a, b). a \ b} \ linear_order_on infinite_complement_partition {(A, B). A \''' B}" (is "PROP ?thesis1") and "order_consistent {(A, B). A \'' B} {(A, B). A \''' B}" (is ?thesis2) proof - let ?P = "\sleq. (linear_order {(a, b). a \ b} \ linear_order_on infinite_complement_partition {(A, B). sleq A B}) \ order_consistent {(A, B). A \'' B} {(A, B). sleq A B}" have "Ex ?P" proof(cases "linear_order {(a, b). a \ b}") case False have "antisym {(a, b). a \'' b}" by (rule antisymI) (simp add: set_less_eq_aux'_antisym) then show ?thesis using False by (auto intro: antisym_order_consistent_self) next case True hence "partial_order_on infinite_complement_partition {(A, B). A \'' B}" by(rule linorder.set_less_eq_aux'_porder[OF linear_order_imp_linorder]) then obtain s where "linear_order_on infinite_complement_partition s" and "order_consistent {(A, B). A \'' B} s" by(rule porder_extend_to_linorder) thus ?thesis by(auto intro: exI[where x="\A B. (A, B) \ s"]) qed hence "?P (Eps ?P)" by(rule someI_ex) thus "PROP ?thesis1" ?thesis2 by(simp_all add: set_less_eq_aux''_def) qed end context linorder begin lemma set_less_eq_aux''_linear_order: "linear_order_on infinite_complement_partition {(A, B). A \''' B}" by(rule set_less_eq_aux''_spec)(rule linear_order) lemma set_less_eq_aux''_refl [iff]: "A \''' A \ A \ infinite_complement_partition" using set_less_eq_aux''_linear_order by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: refl_onD refl_onD1) lemma set_less_eq_aux'_into_set_less_eq_aux'': assumes "A \'' B" shows "A \''' B" proof(rule ccontr) assume nleq: "\ ?thesis" moreover from assms have A: "A \ infinite_complement_partition" and B: "B \ infinite_complement_partition" by(auto dest: set_less_eq_aux'_infinite_complement_partitionD) with set_less_eq_aux''_linear_order have "A \''' B \ A = B \ B \''' A" by(auto simp add: linear_order_on_def dest: total_onD) ultimately have "B \''' A" using B by auto with assms have "A = B" using set_less_eq_aux''_spec(2) by(simp add: order_consistent_def) with A nleq show False by simp qed lemma finite_set_less_eq_aux''_finite: assumes "finite A" and "finite B" shows "A \''' B \ A \'' B" proof assume "A \''' B" from assms have "A \' B \ B \' A" by(rule set_less_eq_aux_finite_total2) hence "A \'' B \ B \'' A" by(auto simp add: set_less_eq_aux'_def) thus "A \'' B" proof assume "B \'' A" hence "B \''' A" by(rule set_less_eq_aux'_into_set_less_eq_aux'') with \A \''' B\ set_less_eq_aux''_linear_order have "A = B" by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD) thus ?thesis using assms by(simp add: finite_complement_partition set_less_eq_aux'_def) qed qed(rule set_less_eq_aux'_into_set_less_eq_aux'') lemma set_less_eq_aux''_finite: "finite (UNIV :: 'a set) \ set_less_eq_aux'' = set_less_eq_aux" by(auto simp add: fun_eq_iff finite_set_less_eq_aux''_finite set_less_eq_aux'_def finite_subset[OF subset_UNIV]) lemma set_less_eq_aux''_antisym: "\ A \''' B; B \''' A; A \ infinite_complement_partition; B \ infinite_complement_partition \ \ A = B" using set_less_eq_aux''_linear_order by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD del: equalityI) lemma set_less_eq_aux''_trans: "\ A \''' B; B \''' C \ \ A \''' C" using set_less_eq_aux''_linear_order by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: transD) lemma set_less_eq_aux''_total: "\ A \ infinite_complement_partition; B \ infinite_complement_partition \ \ A \''' B \ B \''' A" using set_less_eq_aux''_linear_order by(auto simp add: linear_order_on_def dest: total_onD) end subsubsection \Extend @{term set_less_eq_aux''} to cofinite sets\ context ord begin definition set_less_eq :: "'a set \ 'a set \ bool" (infix "\" 50) where "A \ B \ (if A \ infinite_complement_partition then A \''' B \ B \ infinite_complement_partition else B \ infinite_complement_partition \ - B \''' - A)" definition set_less :: "'a set \ 'a set \ bool" (infix "\" 50) where "A \ B \ A \ B \ \ B \ A" lemma set_less_eq_def2: "A \ B \ (if finite (UNIV :: 'a set) then A \''' B else if A \ infinite_complement_partition then A \''' B \ B \ infinite_complement_partition else B \ infinite_complement_partition \ - B \''' - A)" by(simp add: set_less_eq_def) end context linorder begin lemma set_less_eq_refl [iff]: "A \ A" by(auto simp add: set_less_eq_def2 not_in_complement_partition) lemma set_less_eq_antisym: "\ A \ B; B \ A \ \ A = B" by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False del: equalityI split: if_split_asm dest: set_less_eq_aux_antisym set_less_eq_aux''_antisym) lemma set_less_eq_trans: "\ A \ B; B \ C \ \ A \ C" by(auto simp add: set_less_eq_def split: if_split_asm intro: set_less_eq_aux''_trans) lemma set_less_eq_total: "A \ B \ B \ A" by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False intro: set_less_eq_aux_finite_total2 finite_subset[OF subset_UNIV] del: disjCI dest: set_less_eq_aux''_total) lemma set_less_eq_linorder: "class.linorder (\) (\)" by(unfold_locales)(auto simp add: set_less_def set_less_eq_antisym set_less_eq_total intro: set_less_eq_trans) lemma set_less_eq_conv_set_less: "set_less_eq A B \ A = B \ set_less A B" by(auto simp add: set_less_def del: equalityI dest: set_less_eq_antisym) lemma Compl_set_less_eq_Compl: "- A \ - B \ B \ A" by(auto simp add: set_less_eq_def2 not_in_complement_partition_False not_in_complement_partition set_less_eq_aux''_finite Compl_set_less_eq_aux_Compl) lemma Compl_set_less_Compl: "- A \ - B \ B \ A" by(simp add: set_less_def Compl_set_less_eq_Compl) lemma set_less_eq_finite_iff: "\ finite A; finite B \ \ A \ B \ A \' B" by(auto simp add: set_less_eq_def finite_complement_partition set_less_eq_aux'_def finite_set_less_eq_aux''_finite) lemma set_less_finite_iff: "\ finite A; finite B \ \ A \ B \ A \' B" by(simp add: set_less_def set_less_aux_conv_set_less_eq_aux set_less_eq_finite_iff) lemma infinite_set_less_eq_Complement: "\ finite A; finite B; \ finite (UNIV :: 'a set) \ \ A \ - B" by(simp add: set_less_eq_def finite_complement_partition not_in_complement_partition) lemma infinite_set_less_Complement: "\ finite A; finite B; \ finite (UNIV :: 'a set) \ \ A \ - B" by(auto simp add: set_less_def dest: set_less_eq_antisym intro: infinite_set_less_eq_Complement) lemma infinite_Complement_set_less_eq: "\ finite A; finite B; \ finite (UNIV :: 'a set) \ \ \ - A \ B" using infinite_set_less_eq_Complement[of A B] Compl_set_less_eq_Compl[of A "- B"] by(auto dest: set_less_eq_antisym) lemma infinite_Complement_set_less: "\ finite A; finite B; \ finite (UNIV :: 'a set) \ \ \ - A \ B" using infinite_Complement_set_less_eq[of A B] by(simp add: set_less_def) lemma empty_set_less_eq [iff]: "{} \ A" by(auto simp add: set_less_eq_def finite_complement_partition intro: set_less_eq_aux'_into_set_less_eq_aux'') lemma set_less_eq_empty [iff]: "A \ {} \ A = {}" by (metis empty_set_less_eq set_less_eq_antisym) lemma empty_set_less_iff [iff]: "{} \ A \ A \ {}" by(simp add: set_less_def) lemma not_set_less_empty [simp]: "\ A \ {}" by(simp add: set_less_def) lemma set_less_eq_UNIV [iff]: "A \ UNIV" using Compl_set_less_eq_Compl[of "- A" "{}"] by simp lemma UNIV_set_less_eq [iff]: "UNIV \ A \ A = UNIV" using Compl_set_less_eq_Compl[of "{}" "- A"] by(simp add: Compl_eq_empty_iff) lemma set_less_UNIV_iff [iff]: "A \ UNIV \ A \ UNIV" by(simp add: set_less_def) lemma not_UNIV_set_less [simp]: "\ UNIV \ A" by(simp add: set_less_def) end subsection \Implementation based on sorted lists\ type_synonym 'a proper_interval = "'a option \ 'a option \ bool" class proper_intrvl = ord + fixes proper_interval :: "'a proper_interval" class proper_interval = proper_intrvl + assumes proper_interval_simps: "proper_interval None None = True" "proper_interval None (Some y) = (\z. z < y)" "proper_interval (Some x) None = (\z. x < z)" "proper_interval (Some x) (Some y) = (\z. x < z \ z < y)" context proper_intrvl begin function set_less_eq_aux_Compl :: "'a option \ 'a list \ 'a list \ bool" where "set_less_eq_aux_Compl ao [] ys \ True" | "set_less_eq_aux_Compl ao xs [] \ True" | "set_less_eq_aux_Compl ao (x # xs) (y # ys) \ (if x < y then proper_interval ao (Some x) \ set_less_eq_aux_Compl (Some x) xs (y # ys) else if y < x then proper_interval ao (Some y) \ set_less_eq_aux_Compl (Some y) (x # xs) ys else proper_interval ao (Some y))" by(pat_completeness) simp_all termination by(lexicographic_order) fun Compl_set_less_eq_aux :: "'a option \ 'a list \ 'a list \ bool" where "Compl_set_less_eq_aux ao [] [] \ \ proper_interval ao None" | "Compl_set_less_eq_aux ao [] (y # ys) \ \ proper_interval ao (Some y) \ Compl_set_less_eq_aux (Some y) [] ys" | "Compl_set_less_eq_aux ao (x # xs) [] \ \ proper_interval ao (Some x) \ Compl_set_less_eq_aux (Some x) xs []" | "Compl_set_less_eq_aux ao (x # xs) (y # ys) \ (if x < y then \ proper_interval ao (Some x) \ Compl_set_less_eq_aux (Some x) xs (y # ys) else if y < x then \ proper_interval ao (Some y) \ Compl_set_less_eq_aux (Some y) (x # xs) ys else \ proper_interval ao (Some y))" fun set_less_aux_Compl :: "'a option \ 'a list \ 'a list \ bool" where "set_less_aux_Compl ao [] [] \ proper_interval ao None" | "set_less_aux_Compl ao [] (y # ys) \ proper_interval ao (Some y) \ set_less_aux_Compl (Some y) [] ys" | "set_less_aux_Compl ao (x # xs) [] \ proper_interval ao (Some x) \ set_less_aux_Compl (Some x) xs []" | "set_less_aux_Compl ao (x # xs) (y # ys) \ (if x < y then proper_interval ao (Some x) \ set_less_aux_Compl (Some x) xs (y # ys) else if y < x then proper_interval ao (Some y) \ set_less_aux_Compl (Some y) (x # xs) ys else proper_interval ao (Some y))" function Compl_set_less_aux :: "'a option \ 'a list \ 'a list \ bool" where "Compl_set_less_aux ao [] ys \ False" | "Compl_set_less_aux ao xs [] \ False" | "Compl_set_less_aux ao (x # xs) (y # ys) \ (if x < y then \ proper_interval ao (Some x) \ Compl_set_less_aux (Some x) xs (y # ys) else if y < x then \ proper_interval ao (Some y) \ Compl_set_less_aux (Some y) (x # xs) ys else \ proper_interval ao (Some y))" by pat_completeness simp_all termination by lexicographic_order end lemmas [code] = proper_intrvl.set_less_eq_aux_Compl.simps proper_intrvl.set_less_aux_Compl.simps proper_intrvl.Compl_set_less_eq_aux.simps proper_intrvl.Compl_set_less_aux.simps class linorder_proper_interval = linorder + proper_interval begin theorem assumes fin: "finite (UNIV :: 'a set)" and xs: "sorted xs" "distinct xs" and ys: "sorted ys" "distinct ys" shows set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl: "set xs \' - set ys \ set_less_eq_aux_Compl None xs ys" (is ?Compl2) and Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux: "- set xs \' set ys \ Compl_set_less_eq_aux None xs ys" (is ?Compl1) proof - note fin' [simp] = finite_subset[OF subset_UNIV fin] define above where "above = case_option UNIV (Collect \ less)" have above_simps [simp]: "above None = UNIV" "\x. above (Some x) = {y. x < y}" and above_upclosed: "\x y ao. \ x \ above ao; x < y \ \ y \ above ao" and proper_interval_Some2: "\x ao. proper_interval ao (Some x) \ (\z\above ao. z < x)" and proper_interval_None2: "\ao. proper_interval ao None \ above ao \ {}" by(simp_all add: proper_interval_simps above_def split: option.splits) { fix ao x A B assume ex: "proper_interval ao (Some x)" and A: "\a \ A. x \ a" and B: "\b \ B. x \ b" from ex obtain z where z_ao: "z \ above ao" and z: "z < x" by(auto simp add: proper_interval_Some2) with A have A_eq: "A \ above ao = A" by(auto simp add: above_upclosed) from z_ao z B have B_eq: "B \ above ao = B" by(auto simp add: above_upclosed) define w where "w = Min (above ao)" with z_ao have "w \ z" "\z \ above ao. w \ z" "w \ above ao" by(auto simp add: Min_le_iff intro: Min_in) hence "A \ above ao \' (- B) \ above ao" (is "?lhs \' ?rhs") using A B z by(auto simp add: set_less_aux_def intro!: bexI[where x="w"]) hence "A \' ?rhs" unfolding A_eq by(simp add: set_less_eq_aux_def) moreover from z_ao z A B have "z \ - A \ above ao" "z \ B" by auto hence neq: "- A \ above ao \ B \ above ao" by auto have "\ - A \ above ao \' B \ above ao" (is "\ ?lhs' \' ?rhs'") using A B z z_ao by(force simp add: set_less_aux_def not_less dest: bspec[where x=z]) with neq have "\ ?lhs' \' B" unfolding B_eq by(auto simp add: set_less_eq_aux_def) moreover note calculation } note proper_interval_set_less_eqI = this(1) and proper_interval_not_set_less_eq_auxI = this(2) { fix ao assume "set xs \ set ys \ above ao" with xs ys have "set_less_eq_aux_Compl ao xs ys \ set xs \' (- set ys) \ above ao" proof(induction ao xs ys rule: set_less_eq_aux_Compl.induct) case 1 thus ?case by simp next case 2 thus ?case by(auto intro: subset_finite_imp_set_less_eq_aux) next case (3 ao x xs y ys) note ao = \set (x # xs) \ set (y # ys) \ above ao\ hence x_ao: "x \ above ao" and y_ao: "y \ above ao" by simp_all note yys = \sorted (y # ys)\ \distinct (y # ys)\ hence ys: "sorted ys" "distinct ys" and y_Min: "\y' \ set ys. y < y'" by(auto simp add: less_le) note xxs = \sorted (x # xs)\ \distinct (x # xs)\ hence xs: "sorted xs" "distinct xs" and x_Min: "\x' \ set xs. x < x'" by(auto simp add: less_le) let ?lhs = "set (x # xs)" and ?rhs = "- set (y # ys) \ above ao" show ?case proof(cases "x < y") case True show ?thesis proof(cases "proper_interval ao (Some x)") case True hence "?lhs \' ?rhs" using x_Min y_Min \x < y\ by(auto intro!: proper_interval_set_less_eqI) with True show ?thesis using \x < y\ by simp next case False have "set xs \ set (y # ys) \ above (Some x)" using True x_Min y_Min by auto with True xs yys have IH: "set_less_eq_aux_Compl (Some x) xs (y # ys) = (set xs \' - set (y # ys) \ above (Some x))" by(rule "3.IH") from True y_Min x_ao have "x \ - set (y # ys) \ above ao" by auto hence "?rhs \ {}" by blast moreover have "Min ?lhs = x" using x_Min x_ao by(auto intro!: Min_eqI) moreover have "Min ?rhs = x" using \x < y\ y_Min x_ao False by(auto intro!: Min_eqI simp add: proper_interval_Some2) moreover have "set xs = set xs - {x}" using ao x_Min by auto moreover have "- set (y # ys) \ above (Some x) = - set (y # ys) \ above ao - {x}" using False x_ao by(auto simp add: proper_interval_Some2 intro: above_upclosed) ultimately show ?thesis using True False IH by(simp del: set_simps)(subst (2) set_less_eq_aux_rec, simp_all add: x_ao) qed next case False show ?thesis proof(cases "y < x") case True show ?thesis proof(cases "proper_interval ao (Some y)") case True hence "?lhs \' ?rhs" using x_Min y_Min \\ x < y\ by(auto intro!: proper_interval_set_less_eqI) with True show ?thesis using \\ x < y\ by simp next case False have "set (x # xs) \ set ys \ above (Some y)" using \y < x\ x_Min y_Min by auto with \\ x < y\ \y < x\ xxs ys have IH: "set_less_eq_aux_Compl (Some y) (x # xs) ys = (set (x # xs) \' - set ys \ above (Some y))" by(rule "3.IH") moreover have "- set ys \ above (Some y) = ?rhs" using y_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2) ultimately show ?thesis using \\ x < y\ True False by simp qed next case False with \\ x < y\ have "x = y" by auto { assume "proper_interval ao (Some y)" hence "?lhs \' ?rhs" using x_Min y_Min \x = y\ by(auto intro!: proper_interval_set_less_eqI) } moreover { assume "?lhs \' ?rhs" moreover have "?lhs \ ?rhs" proof assume eq: "?lhs = ?rhs" have "x \ ?lhs" using x_ao by simp also note eq also note \x = y\ finally show False by simp qed ultimately obtain z where "z \ above ao" "z < y" using \x = y\ y_ao by(fastforce simp add: set_less_eq_aux_def set_less_aux_def not_le dest!: bspec[where x=y]) hence "proper_interval ao (Some y)" by(auto simp add: proper_interval_Some2) } ultimately show ?thesis using \x = y\ \\ x < y\ \\ y < x\ by auto qed qed qed } from this[of None] show ?Compl2 by simp { fix ao assume "set xs \ set ys \ above ao" with xs ys have "Compl_set_less_eq_aux ao xs ys \ (- set xs) \ above ao \' set ys" proof(induction ao xs ys rule: Compl_set_less_eq_aux.induct) case 1 thus ?case by(simp add: proper_interval_None2) next case (2 ao y ys) from \sorted (y # ys)\ \distinct (y # ys)\ have ys: "sorted ys" "distinct ys" and y_Min: "\y' \ set ys. y < y'" by(auto simp add: less_le) show ?case proof(cases "proper_interval ao (Some y)") case True hence "\ - set [] \ above ao \' set (y # ys)" using y_Min by -(erule proper_interval_not_set_less_eq_auxI, auto) thus ?thesis using True by simp next case False note ao = \set [] \ set (y # ys) \ above ao\ hence y_ao: "y \ above ao" by simp from ao y_Min have "set [] \ set ys \ above (Some y)" by auto with \sorted []\ \distinct []\ ys have "Compl_set_less_eq_aux (Some y) [] ys \ - set [] \ above (Some y) \' set ys" by(rule "2.IH") moreover have "above ao \ {}" using y_ao by auto moreover have "Min (above ao) = y" and "Min (set (y # ys)) = y" using y_ao False ao by(auto intro!: Min_eqI simp add: proper_interval_Some2 not_less) moreover have "above ao - {y} = above (Some y)" using False y_ao by(auto simp add: proper_interval_Some2 intro: above_upclosed) moreover have "set ys - {y} = set ys" using y_Min y_ao by(auto) ultimately show ?thesis using False y_ao by(simp)(subst (2) set_less_eq_aux_rec, simp_all) qed next case (3 ao x xs) from \sorted (x # xs)\ \distinct (x # xs)\ have xs: "sorted xs" "distinct xs" and x_Min: "\x'\set xs. x < x'" by(auto simp add: less_le) show ?case proof(cases "proper_interval ao (Some x)") case True then obtain z where "z \ above ao" "z < x" by(auto simp add: proper_interval_Some2) hence "z \ - set (x # xs) \ above ao" using x_Min by auto thus ?thesis using True by auto next case False note ao = \set (x # xs) \ set [] \ above ao\ hence x_ao: "x \ above ao" by simp from ao have "set xs \ set [] \ above (Some x)" using x_Min by auto with xs \sorted []\ \distinct []\ have "Compl_set_less_eq_aux (Some x) xs [] \ - set xs \ above (Some x) \' set []" by(rule "3.IH") moreover have "- set (x # xs) \ above ao = - set xs \ above (Some x)" using False x_ao by(auto simp add: proper_interval_Some2 intro: above_upclosed) ultimately show ?thesis using False by simp qed next case (4 ao x xs y ys) note ao = \set (x # xs) \ set (y # ys) \ above ao\ hence x_ao: "x \ above ao" and y_ao: "y \ above ao" by simp_all note xxs = \sorted (x # xs)\ \distinct (x # xs)\ hence xs: "sorted xs" "distinct xs" and x_Min: "\x'\set xs. x < x'" by(auto simp add: less_le) note yys = \sorted (y # ys)\ \distinct (y # ys)\ hence ys: "sorted ys" "distinct ys" and y_Min: "\y'\set ys. y < y'" by(auto simp add: less_le) let ?lhs = "- set (x # xs) \ above ao" and ?rhs = "set (y # ys)" show ?case proof(cases "x < y") case True show ?thesis proof(cases "proper_interval ao (Some x)") case True hence "\ ?lhs \' ?rhs" using x_Min y_Min \x < y\ by -(erule proper_interval_not_set_less_eq_auxI, auto) thus ?thesis using True \x < y\ by simp next case False have "set xs \ set (y # ys) \ above (Some x)" using ao x_Min y_Min True by auto with True xs yys have "Compl_set_less_eq_aux (Some x) xs (y # ys) \ - set xs \ above (Some x) \' set (y # ys)" by(rule "4.IH") moreover have "- set xs \ above (Some x) = ?lhs" using x_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2) ultimately show ?thesis using False True by simp qed next case False show ?thesis proof(cases "y < x") case True show ?thesis proof(cases "proper_interval ao (Some y)") case True hence "\ ?lhs \' ?rhs" using x_Min y_Min \y < x\ by -(erule proper_interval_not_set_less_eq_auxI, auto) thus ?thesis using True \y < x\ \\ x < y\ by simp next case False from ao True x_Min y_Min have "set (x # xs) \ set ys \ above (Some y)" by auto with \\ x < y\ True xxs ys have "Compl_set_less_eq_aux (Some y) (x # xs) ys \ - set (x # xs) \ above (Some y) \' set ys" by(rule "4.IH") moreover have "y \ ?lhs" using True x_Min y_ao by auto hence "?lhs \ {}" by auto moreover have "Min ?lhs = y" using True False x_Min y_ao by(auto intro!: Min_eqI simp add: not_le not_less proper_interval_Some2) moreover have "Min ?rhs = y" using y_Min y_ao by(auto intro!: Min_eqI) moreover have "- set (x # xs) \ above (Some y) = ?lhs - {y}" using y_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2) moreover have "set ys = set ys - {y}" using y_ao y_Min by(auto intro: above_upclosed) ultimately show ?thesis using True False \\ x < y\ y_ao by(simp)(subst (2) set_less_eq_aux_rec, simp_all) qed next case False with \\ x < y\ have "x = y" by auto { assume "proper_interval ao (Some y)" hence "\ ?lhs \' ?rhs" using x_Min y_Min \x = y\ by -(erule proper_interval_not_set_less_eq_auxI, auto) } moreover { assume "\ ?lhs \' ?rhs" also have "?rhs = set (y # ys) \ above ao" using ao by auto finally obtain z where "z \ above ao" "z < y" using \x = y\ x_ao x_Min[unfolded Ball_def] by(fastforce simp add: set_less_eq_aux_def set_less_aux_def simp add: less_le not_le dest!: bspec[where x=y]) hence "proper_interval ao (Some y)" by(auto simp add: proper_interval_Some2) } ultimately show ?thesis using \x = y\ by auto qed qed qed } from this[of None] show ?Compl1 by simp qed lemma set_less_aux_Compl_iff: "set_less_aux_Compl ao xs ys \ set_less_eq_aux_Compl ao xs ys \ \ Compl_set_less_eq_aux ao ys xs" by(induct ao xs ys rule: set_less_aux_Compl.induct)(auto simp add: not_less_iff_gr_or_eq) lemma Compl_set_less_aux_Compl_iff: "Compl_set_less_aux ao xs ys \ Compl_set_less_eq_aux ao xs ys \ \ set_less_eq_aux_Compl ao ys xs" by(induct ao xs ys rule: Compl_set_less_aux.induct)(auto simp add: not_less_iff_gr_or_eq) theorem assumes fin: "finite (UNIV :: 'a set)" and xs: "sorted xs" "distinct xs" and ys: "sorted ys" "distinct ys" shows set_less_aux_Compl2_conv_set_less_aux_Compl: "set xs \' - set ys \ set_less_aux_Compl None xs ys" (is ?Compl2) and Compl1_set_less_aux_conv_Compl_set_less_aux: "- set xs \' set ys \ Compl_set_less_aux None xs ys" (is ?Compl1) using assms by(simp_all only: set_less_aux_conv_set_less_eq_aux set_less_aux_Compl_iff Compl_set_less_aux_Compl_iff set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux) end subsection \Implementation of proper intervals for sets\ definition length_last :: "'a list \ nat \ 'a" where "length_last xs = (length xs, last xs)" lemma length_last_Nil [code]: "length_last [] = (0, undefined)" by(simp add: length_last_def last_def) lemma length_last_Cons_code [symmetric, code]: "fold (\x (n, _) . (n + 1, x)) xs (1, x) = length_last (x # xs)" by(induct xs rule: rev_induct)(simp_all add: length_last_def) context proper_intrvl begin fun exhaustive_above :: "'a \ 'a list \ bool" where "exhaustive_above x [] \ \ proper_interval (Some x) None" | "exhaustive_above x (y # ys) \ \ proper_interval (Some x) (Some y) \ exhaustive_above y ys" fun exhaustive :: "'a list \ bool" where "exhaustive [] = False" | "exhaustive (x # xs) \ \ proper_interval None (Some x) \ exhaustive_above x xs" fun proper_interval_set_aux :: "'a list \ 'a list \ bool" where "proper_interval_set_aux xs [] \ False" | "proper_interval_set_aux [] (y # ys) \ ys \ [] \ proper_interval (Some y) None" | "proper_interval_set_aux (x # xs) (y # ys) \ (if x < y then False else if y < x then proper_interval (Some y) (Some x) \ ys \ [] \ \ exhaustive_above x xs else proper_interval_set_aux xs ys)" fun proper_interval_set_Compl_aux :: "'a option \ nat \ 'a list \ 'a list \ bool" where "proper_interval_set_Compl_aux ao n [] [] \ CARD('a) > n + 1" | "proper_interval_set_Compl_aux ao n [] (y # ys) \ (let m = CARD('a) - n; (len_y, y') = length_last (y # ys) in m \ len_y \ (m = len_y + 1 \ \ proper_interval (Some y') None))" | "proper_interval_set_Compl_aux ao n (x # xs) [] \ (let m = CARD('a) - n; (len_x, x') = length_last (x # xs) in m \ len_x \ (m = len_x + 1 \ \ proper_interval (Some x') None))" | "proper_interval_set_Compl_aux ao n (x # xs) (y # ys) \ (if x < y then proper_interval ao (Some x) \ proper_interval_set_Compl_aux (Some x) (n + 1) xs (y # ys) else if y < x then proper_interval ao (Some y) \ proper_interval_set_Compl_aux (Some y) (n + 1) (x # xs) ys else proper_interval ao (Some x) \ (let m = card (UNIV :: 'a set) - n in m - length ys \ 2 \ m - length xs \ 2))" fun proper_interval_Compl_set_aux :: "'a option \ 'a list \ 'a list \ bool" where "proper_interval_Compl_set_aux ao (x # xs) (y # ys) \ (if x < y then \ proper_interval ao (Some x) \ proper_interval_Compl_set_aux (Some x) xs (y # ys) else if y < x then \ proper_interval ao (Some y) \ proper_interval_Compl_set_aux (Some y) (x # xs) ys else \ proper_interval ao (Some x) \ (ys = [] \ xs \ []))" | "proper_interval_Compl_set_aux ao _ _ \ False" end lemmas [code] = proper_intrvl.exhaustive_above.simps proper_intrvl.exhaustive.simps proper_intrvl.proper_interval_set_aux.simps proper_intrvl.proper_interval_set_Compl_aux.simps proper_intrvl.proper_interval_Compl_set_aux.simps context linorder_proper_interval begin lemma exhaustive_above_iff: "\ sorted xs; distinct xs; \x'\set xs. x < x' \ \ exhaustive_above x xs \ set xs = {z. z > x}" proof(induction x xs rule: exhaustive_above.induct) case 1 thus ?case by(simp add: proper_interval_simps) next case (2 x y ys) from \sorted (y # ys)\ \distinct (y # ys)\ have ys: "sorted ys" "distinct ys" and y: "\y'\set ys. y < y'" by(auto simp add: less_le) hence "exhaustive_above y ys = (set ys = {z. y < z})" by(rule "2.IH") moreover from \\y'\set (y # ys). x < y'\ have "x < y" by simp ultimately show ?case using y by(fastforce simp add: proper_interval_simps) qed lemma exhaustive_correct: assumes "sorted xs" "distinct xs" shows "exhaustive xs \ set xs = UNIV" proof(cases xs) case Nil thus ?thesis by auto next case Cons show ?thesis using assms unfolding Cons exhaustive.simps apply(subst exhaustive_above_iff) apply(auto simp add: less_le proper_interval_simps not_less) by (metis List.set_simps(2) UNIV_I eq_iff set_ConsD) qed theorem proper_interval_set_aux: assumes fin: "finite (UNIV :: 'a set)" and xs: "sorted xs" "distinct xs" and ys: "sorted ys" "distinct ys" shows "proper_interval_set_aux xs ys \ (\A. set xs \' A \ A \' set ys)" proof - note [simp] = finite_subset[OF subset_UNIV fin] show ?thesis using xs ys proof(induction xs ys rule: proper_interval_set_aux.induct) case 1 thus ?case by simp next case (2 y ys) hence "\y'\set ys. y < y'" by(auto simp add: less_le) thus ?case by(cases ys)(auto simp add: proper_interval_simps set_less_aux_singleton_iff intro: psubset_finite_imp_set_less_aux) next case (3 x xs y ys) from \sorted (x # xs)\ \distinct (x # xs)\ have xs: "sorted xs" "distinct xs" and x: "\x'\set xs. x < x'" by(auto simp add: less_le) from \sorted (y # ys)\ \distinct (y # ys)\ have ys: "sorted ys" "distinct ys" and y: "\y'\set ys. y < y'" by(auto simp add: less_le) have Minxxs: "Min (set (x # xs)) = x" and xnxs: "x \ set xs" using x by(auto intro!: Min_eqI) have Minyys: "Min (set (y # ys)) = y" and ynys: "y \ set ys" using y by(auto intro!: Min_eqI) show ?case proof(cases "x < y") case True hence "set (y # ys) \' set (x # xs)" using Minxxs Minyys by -(rule set_less_aux_Min_antimono, simp_all) thus ?thesis using True by(auto dest: set_less_aux_trans set_less_aux_antisym) next case False show ?thesis proof(cases "y < x") case True { assume "proper_interval (Some y) (Some x)" then obtain z where z: "y < z" "z < x" by(auto simp add: proper_interval_simps) hence "set (x # xs) \' {z}" using x by -(rule set_less_aux_Min_antimono, auto) moreover have "{z} \' set (y # ys)" using z y Minyys by -(rule set_less_aux_Min_antimono, auto) ultimately have "\A. set (x # xs) \' A \ A \' set (y # ys)" by blast } moreover { assume "ys \ []" hence "{y} \' set (y # ys)" using y by -(rule psubset_finite_imp_set_less_aux, auto simp add: neq_Nil_conv) moreover have "set (x # xs) \' {y}" using False True x by -(rule set_less_aux_Min_antimono, auto) ultimately have "\A. set (x # xs) \' A \ A \' set (y # ys)" by blast } moreover { assume "\ exhaustive_above x xs" then obtain z where z: "z > x" "z \ set xs" using x by(auto simp add: exhaustive_above_iff[OF xs x]) let ?A = "insert z (set (x # xs))" have "set (x # xs) \' ?A" using z by -(rule psubset_finite_imp_set_less_aux, auto) moreover have "?A \' set (y # ys)" using Minyys False True z x by -(rule set_less_aux_Min_antimono, auto) ultimately have "\A. set (x # xs) \' A \ A \' set (y # ys)" by blast } moreover { fix A assume A: "set (x # xs) \' A" and A': "A \' {y}" and pi: "\ proper_interval (Some y) (Some x)" from A have nempty: "A \ {}" by auto have "y \ A" proof assume "y \ A" moreover with A' have "A \ {y}" by auto ultimately have "{y} \' A" by -(rule psubset_finite_imp_set_less_aux, auto) with A' show False by(rule set_less_aux_antisym) qed have "y < Min A" unfolding not_le[symmetric] proof assume "Min A \ y" moreover have "Min A \ y" using \y \ A\ nempty by clarsimp ultimately have "Min A < Min {y}" by simp hence "{y} \' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty) with A' show False by(rule set_less_aux_antisym) qed with pi nempty have "x \ Min A" by(auto simp add: proper_interval_simps) moreover from A obtain z where z: "z \ A" "z \ set (x # xs)" by(auto simp add: set_less_aux_def) with \x \ Min A\ nempty have "x < z" by auto with z have "\ exhaustive_above x xs" by(auto simp add: exhaustive_above_iff[OF xs x]) } ultimately show ?thesis using True False by fastforce next case False with \\ x < y\ have "x = y" by auto from \\ x < y\ False have "proper_interval_set_aux xs ys = (\A. set xs \' A \ A \' set ys)" using xs ys by(rule "3.IH") also have "\ = (\A. set (x # xs) \' A \ A \' set (y # ys))" (is "?lhs = ?rhs") proof assume ?lhs then obtain A where A: "set xs \' A" and A': "A \' set ys" by blast hence nempty: "A \ {}" "ys \ []" by auto let ?A = "insert y A" { assume "Min A \ y" also from y nempty have "y < Min (set ys)" by auto finally have "set ys \' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty) with A' have False by(rule set_less_aux_antisym) } hence MinA: "y < Min A" by(metis not_le) with nempty have "y \ A" by auto moreover with MinA nempty have MinyA: "Min ?A = y" by -(rule Min_eqI, auto) ultimately have A1: "set (x # xs) \' ?A" using \x = y\ A Minxxs xnxs by(subst set_less_aux_rec) simp_all moreover have "?A \' set (y # ys)" using \x = y\ MinyA \y \ A\ A' Minyys ynys by(subst set_less_aux_rec) simp_all ultimately show ?rhs by blast next assume "?rhs" then obtain A where A: "set (x # xs) \' A" and A': "A \' set (y # ys)" by blast let ?A = "A - {x}" from A have nempty: "A \ {}" by auto { assume "x < Min A" hence "Min (set (x # xs)) < Min A" unfolding Minxxs . hence "A \' set (x # xs)" by(rule set_less_aux_Min_antimono) simp_all with A have False by(rule set_less_aux_antisym) } moreover { assume "Min A < x" hence "Min A < Min (set (y # ys))" unfolding \x = y\ Minyys . hence "set (y # ys) \' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty) with A' have False by(rule set_less_aux_antisym) } ultimately have MinA: "Min A = x" by(metis less_linear) hence "x \ A" using nempty by(metis Min_in \finite A\) from A nempty Minxxs xnxs have "set xs \' ?A" by(subst (asm) set_less_aux_rec)(auto simp add: MinA) moreover from A' \x = y\ nempty Minyys MinA ynys have "?A \' set ys" by(subst (asm) set_less_aux_rec) simp_all ultimately show ?lhs by blast qed finally show ?thesis using \x = y\ by simp qed qed qed qed lemma proper_interval_set_Compl_aux: assumes fin: "finite (UNIV :: 'a set)" and xs: "sorted xs" "distinct xs" and ys: "sorted ys" "distinct ys" shows "proper_interval_set_Compl_aux None 0 xs ys \ (\A. set xs \' A \ A \' - set ys)" proof - note [simp] = finite_subset[OF subset_UNIV fin] define above where "above = case_option UNIV (Collect \ less)" have above_simps [simp]: "above None = UNIV" "\x. above (Some x) = {y. x < y}" and above_upclosed: "\x y ao. \ x \ above ao; x < y \ \ y \ above ao" and proper_interval_Some2: "\x ao. proper_interval ao (Some x) \ (\z\above ao. z < x)" by(simp_all add: proper_interval_simps above_def split: option.splits) { fix ao n assume "set xs \ above ao" "set ys \ above ao" from xs \set xs \ above ao\ ys \set ys \ above ao\ have "proper_interval_set_Compl_aux ao (card (UNIV - above ao)) xs ys \ (\A \ above ao. set xs \' A \ A \' - set ys \ above ao)" proof(induct ao n\"card (UNIV - above ao)" xs ys rule: proper_interval_set_Compl_aux.induct) case (1 ao) have "card (UNIV - above ao) + 1 < CARD('a) \ (\A \ above ao. A \ {} \ A \' above ao)" (is "?lhs \ ?rhs") proof assume ?lhs hence "card (UNIV - (UNIV - above ao)) > 1" by(simp add: card_Diff_subset) from card_gt_1D[OF this] obtain x y where above: "x \ above ao" "y \ above ao" and neq: "x \ y" by blast hence "{x} \' {x, y} \ above ao" by(simp_all add: psubsetI psubset_finite_imp_set_less_aux) also have "\ \' above ao" by(auto intro: subset_finite_imp_set_less_eq_aux) finally show ?rhs using above by blast next assume ?rhs then obtain A where nempty: "A \ above ao \ {}" and subset: "A \ above ao" and less: "A \' above ao" by blast from nempty obtain x where x: "x \ A" "x \ above ao" by blast show ?lhs proof(rule ccontr) assume "\ ?lhs" moreover have "CARD('a) \ card (UNIV - above ao)" by(rule card_mono) simp_all moreover from card_Un_disjoint[of "UNIV - above ao" "above ao"] have "CARD('a) = card (UNIV - above ao) + card (above ao)" by auto ultimately have "card (above ao) = 1" using x by(cases "card (above ao)")(auto simp add: not_less_eq less_Suc_eq_le) with x have "above ao = {x}" unfolding card_eq_1_iff by auto moreover with x subset have A: "A = {x}" by auto ultimately show False using less by simp qed qed thus ?case by simp next case (2 ao y ys) note ys = \sorted (y # ys)\ \distinct (y # ys)\ \set (y # ys) \ above ao\ have len_ys: "length ys = card (set ys)" using ys by(auto simp add: List.card_set intro: sym) define m where "m = CARD('a) - card (UNIV - above ao)" have "CARD('a) = card (above ao) + card (UNIV - above ao)" using card_Un_disjoint[of "above ao" "UNIV - above ao"] by auto hence m_eq: "m = card (above ao)" unfolding m_def by simp have "m \ length ys + 1 \ (m = length ys + 2 \ \ proper_interval (Some (last (y # ys))) None) \ (\A \ above ao. A \ {} \ A \' - set (y # ys) \ above ao)" (is "?lhs \ ?rhs") proof assume ?lhs hence m: "m \ length ys + 1" and pi: "m = length ys + 2 \ \ proper_interval (Some (last (y # ys))) None" by simp_all have "length ys + 1 = card (set (y # ys))" using ys len_ys by simp also have "\ \ m" unfolding m_eq by(rule card_mono)(simp, rule ys) finally have "length ys + 2 \ m" using m by simp show ?rhs proof(cases "m = length ys + 2") case True hence "card (UNIV - (UNIV - above ao) - set (y # ys)) = 1" using ys len_ys by(subst card_Diff_subset)(auto simp add: m_def card_Diff_subset) then obtain z where z: "z \ above ao" "z \ y" "z \ set ys" unfolding card_eq_1_iff by auto from True have "\ proper_interval (Some (last (y # ys))) None" by(rule pi) hence "z \ last (y # ys)" by(simp add: proper_interval_simps not_less del: last.simps) moreover have ly: "last (y # ys) \ set (y # ys)" by(rule last_in_set) simp with z have "z \ last (y # ys)" by auto ultimately have "z < last (y # ys)" by simp hence "{last (y # ys)} \' {z}" using z ly ys by(auto 4 3 simp add: set_less_aux_def) also have "\ \' - set (y # ys) \ above ao" using z by(auto intro: subset_finite_imp_set_less_eq_aux) also have "{last (y # ys)} \ {}" using ly ys by blast moreover have "{last (y # ys)} \ above ao" using ys by auto ultimately show ?thesis by blast next case False with \length ys + 2 \ m\ ys len_ys have "card (UNIV - (UNIV - above ao) - set (y # ys)) > 1" by(subst card_Diff_subset)(auto simp add: card_Diff_subset m_def) from card_gt_1D[OF this] obtain x x' where x: "x \ above ao" "x \ y" "x \ set ys" and x': "x' \ above ao" "x' \ y" "x' \ set ys" and neq: "x \ x'" by auto hence "{x} \' {x, x'} \ above ao" by(simp_all add: psubsetI psubset_finite_imp_set_less_aux) also have "\ \' - set (y # ys) \ above ao" using x x' ys by(auto intro: subset_finite_imp_set_less_eq_aux) also have "{x} \ above ao \ {}" using x by simp ultimately show ?rhs by blast qed next assume ?rhs then obtain A where nempty: "A \ {}" and less: "A \' - set (y # ys) \ above ao" and subset: "A \ above ao" by blast have "card (set (y # ys)) \ card (above ao)" using ys(3) by(simp add: card_mono) hence "length ys + 1 \ m" unfolding m_eq using ys by(simp add: len_ys) have "m \ length ys + 1" proof assume "m = length ys + 1" hence "card (above ao) \ card (set (y # ys))" unfolding m_eq using ys len_ys by auto from card_seteq[OF _ _ this] ys have "set (y # ys) = above ao" by simp with nempty less show False by(auto simp add: set_less_aux_def) qed moreover { assume "m = length ys + 2" hence "card (above ao - set (y # ys)) = 1" using ys len_ys m_eq by(auto simp add: card_Diff_subset) then obtain z where z: "above ao - set (y # ys) = {z}" unfolding card_eq_1_iff .. hence eq_z: "- set (y # ys) \ above ao = {z}" by auto with less have "A \' {z}" by simp have "\ proper_interval (Some (last (y # ys))) None" proof assume "proper_interval (Some (last (y # ys))) None" then obtain z' where z': "last (y # ys) < z'" by(clarsimp simp add: proper_interval_simps) have "last (y # ys) \ set (y # ys)" by(rule last_in_set) simp with ys z' have "z' \ above ao" "z' \ set (y # ys)" by(auto simp del: last.simps sorted.simps(2) intro: above_upclosed dest: sorted_last) with eq_z have "z = z'" by fastforce from z' have "\x. x \ set (y # ys) \ x < z'" using ys by(auto dest: sorted_last simp del: sorted.simps(2)) with eq_z \z = z'\ have "\x. x \ above ao \ x \ z'" by(fastforce) with \A \' {z}\ nempty \z = z'\ subset show False by(auto simp add: set_less_aux_def) qed } ultimately show ?lhs by simp qed thus ?case by(simp add: length_last_def m_def Let_def) next case (3 ao x xs) note xs = \sorted (x # xs)\ \distinct (x # xs)\ \set (x # xs) \ above ao\ have len_xs: "length xs = card (set xs)" using xs by(auto simp add: List.card_set intro: sym) define m where "m = CARD('a) - card (UNIV - above ao)" have "CARD('a) = card (above ao) + card (UNIV - above ao)" using card_Un_disjoint[of "above ao" "UNIV - above ao"] by auto hence m_eq: "m = card (above ao)" unfolding m_def by simp have "m \ length xs + 1 \ (m = length xs + 2 \ \ proper_interval (Some (last (x # xs))) None) \ (\A \ above ao. set (x # xs) \' A \ A \' above ao)" (is "?lhs \ ?rhs") proof assume ?lhs hence m: "m \ length xs + 1" and pi: "m = length xs + 2 \ \ proper_interval (Some (last (x # xs))) None" by simp_all have "length xs + 1 = card (set (x # xs))" using xs len_xs by simp also have "\ \ m" unfolding m_eq by(rule card_mono)(simp, rule xs) finally have "length xs + 2 \ m" using m by simp show ?rhs proof(cases "m = length xs + 2") case True hence "card (UNIV - (UNIV - above ao) - set (x # xs)) = 1" using xs len_xs by(subst card_Diff_subset)(auto simp add: m_def card_Diff_subset) then obtain z where z: "z \ above ao" "z \ x" "z \ set xs" unfolding card_eq_1_iff by auto define A where "A = insert z {y. y \ set (x # xs) \ y < z}" from True have "\ proper_interval (Some (last (x # xs))) None" by(rule pi) hence "z \ last (x # xs)" by(simp add: proper_interval_simps not_less del: last.simps) moreover have lx: "last (x # xs) \ set (x # xs)" by(rule last_in_set) simp with z have "z \ last (x # xs)" by auto ultimately have "z < last (x # xs)" by simp hence "set (x # xs) \' A" using z xs by(auto simp add: A_def set_less_aux_def intro: rev_bexI[where x=z]) moreover have "last (x # xs) \ A" using xs \z < last (x # xs)\ by(auto simp add: A_def simp del: last.simps) hence "A \ insert (last (x # xs)) A" by blast hence less': "A \' insert (last (x # xs)) A" by(rule psubset_finite_imp_set_less_aux) simp have "\ \ above ao" using xs lx z by(auto simp del: last.simps simp add: A_def) hence "insert (last (x # xs)) A \' above ao" by(auto intro: subset_finite_imp_set_less_eq_aux) with less' have "A \' above ao" by(rule set_less_trans_set_less_eq) moreover have "A \ above ao" using xs z by(auto simp add: A_def) ultimately show ?thesis by blast next case False with \length xs + 2 \ m\ xs len_xs have "card (UNIV - (UNIV - above ao) - set (x # xs)) > 1" by(subst card_Diff_subset)(auto simp add: card_Diff_subset m_def) from card_gt_1D[OF this] obtain y y' where y: "y \ above ao" "y \ x" "y \ set xs" and y': "y' \ above ao" "y' \ x" "y' \ set xs" and neq: "y \ y'" by auto define A where "A = insert y (set (x # xs) \ above ao)" hence "set (x # xs) \ A" using y xs by auto hence "set (x # xs) \' \" by(fastforce intro: psubset_finite_imp_set_less_aux) moreover have *: "\ \ above ao" using y y' neq by(auto simp add: A_def) moreover from * have "A \' above ao" by(auto intro: psubset_finite_imp_set_less_aux) ultimately show ?thesis by blast qed next assume ?rhs then obtain A where lessA: "set (x # xs) \' A" and Aless: "A \' above ao" and subset: "A \ above ao" by blast have "card (set (x # xs)) \ card (above ao)" using xs(3) by(simp add: card_mono) hence "length xs + 1 \ m" unfolding m_eq using xs by(simp add: len_xs) have "m \ length xs + 1" proof assume "m = length xs + 1" hence "card (above ao) \ card (set (x # xs))" unfolding m_eq using xs len_xs by auto from card_seteq[OF _ _ this] xs have "set (x # xs) = above ao" by simp with lessA Aless show False by(auto dest: set_less_aux_antisym) qed moreover { assume "m = length xs + 2" hence "card (above ao - set (x # xs)) = 1" using xs len_xs m_eq by(auto simp add: card_Diff_subset) then obtain z where z: "above ao - set (x # xs) = {z}" unfolding card_eq_1_iff .. have "\ proper_interval (Some (last (x # xs))) None" proof assume "proper_interval (Some (last (x # xs))) None" then obtain z' where z': "last (x # xs) < z'" by(clarsimp simp add: proper_interval_simps) have "last (x # xs) \ set (x # xs)" by(rule last_in_set) simp with xs z' have "z' \ above ao" "z' \ set (x # xs)" by(auto simp del: last.simps sorted.simps(2) intro: above_upclosed dest: sorted_last) with z have "z = z'" by fastforce from z' have y_less: "\y. y \ set (x # xs) \ y < z'" using xs by(auto simp del: sorted.simps(2) dest: sorted_last) with z \z = z'\ have "\y. y \ above ao \ y \ z'" by(fastforce) from lessA subset obtain y where y: "y \ A" "y \ above ao" "y \ set (x # xs)" and min: "\y'. \ y' \ set (x # xs); y' \ above ao; y' \ A \ \ y \ y'" by(auto simp add: set_less_aux_def) with z \z = z'\ have "y = z'" by auto have "set (x # xs) \ A" proof fix y' assume y': "y' \ set (x # xs)" show "y' \ A" proof(rule ccontr) assume "y' \ A" from y' xs have "y' \ above ao" by auto with y' have "y \ y'" using \y' \ A\ by(rule min) moreover from y' have "y' < z'" by(rule y_less) ultimately show False using \y = z'\ by simp qed qed moreover from z xs have "above ao = insert z (set (x # xs))" by auto ultimately have "A = above ao" using y \y = z'\ \z = z'\ subset by auto with Aless show False by simp qed } ultimately show ?lhs by simp qed thus ?case by(simp add: length_last_def m_def Let_def del: last.simps) next case (4 ao x xs y ys) note xxs = \sorted (x # xs)\ \distinct (x # xs)\ and yys = \sorted (y # ys)\ \distinct (y # ys)\ and xxs_above = \set (x # xs) \ above ao\ and yys_above = \set (y # ys) \ above ao\ from xxs have xs: "sorted xs" "distinct xs" and x_Min: "\x'\set xs. x < x'" by(auto simp add: less_le) from yys have ys: "sorted ys" "distinct ys" and y_Min: "\y'\set ys. y < y'" by(auto simp add: less_le) have len_xs: "length xs = card (set xs)" using xs by(auto simp add: List.card_set intro: sym) have len_ys: "length ys = card (set ys)" using ys by(auto simp add: List.card_set intro: sym) show ?case proof(cases "x < y") case True have "proper_interval ao (Some x) \ proper_interval_set_Compl_aux (Some x) (card (UNIV - above ao) + 1) xs (y # ys) \ (\A \ above ao. set (x # xs) \' A \ A \' - set (y # ys) \ above ao)" (is "?lhs \ ?rhs") proof(cases "proper_interval ao (Some x)") case True then obtain z where z: "z \ above ao" "z < x" by(clarsimp simp add: proper_interval_Some2) moreover with xxs have "\x'\set xs. z < x'" by(auto) ultimately have "set (x # xs) \' {z}" by(auto simp add: set_less_aux_def intro!: bexI[where x=z]) moreover { from z yys \x < y\ have "z < y" "\y'\set ys. z < y'" by(auto) hence subset: "{z} \ - set (y # ys) \ above ao" using ys \x < y\ z by auto moreover have "x \ \" using yys xxs \x < y\ xxs_above by(auto) ultimately have "{z} \ \" using \z < x\ by fastforce hence "{z} \' \" by(fastforce intro: psubset_finite_imp_set_less_aux) } moreover have "{z} \ above ao" using z by simp ultimately have ?rhs by blast thus ?thesis using True by simp next case False hence above_eq: "above ao = insert x (above (Some x))" using xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed) moreover have "card (above (Some x)) < CARD('a)" by(rule psubset_card_mono)(auto) ultimately have card_eq: "card (UNIV - above ao) + 1 = card (UNIV - above (Some x))" by(simp add: card_Diff_subset) from xxs_above x_Min have xs_above: "set xs \ above (Some x)" by(auto) from \x < y\ y_Min have "set (y # ys) \ above (Some x)" by(auto) with \x < y\ card_eq xs xs_above yys have "proper_interval_set_Compl_aux (Some x) (card (UNIV - above ao) + 1) xs (y # ys) \ (\A \ above (Some x). set xs \' A \ A \' - set (y # ys) \ above (Some x))" by(subst card_eq)(rule 4) also have "\ \ ?rhs" (is "?lhs' \ _") proof assume ?lhs' then obtain A where less_A: "set xs \' A" and A_less: "A \' - set (y # ys) \ above (Some x)" and subset: "A \ above (Some x)" by blast let ?A = "insert x A" have Min_A': "Min ?A = x" using xxs_above False subset by(auto intro!: Min_eqI simp add: proper_interval_Some2) moreover have "Min (set (x # xs)) = x" using x_Min by(auto intro!: Min_eqI) moreover have Amx: "A - {x} = A" using False subset by(auto simp add: proper_interval_Some2 intro: above_upclosed) moreover have "set xs - {x} = set xs" using x_Min by auto ultimately have less_A': "set (x # xs) \' ?A" using less_A xxs_above x_Min by(subst set_less_aux_rec) simp_all have "x \ - insert y (set ys) \ above ao" using \x < y\ xxs_above y_Min by auto hence "- insert y (set ys) \ above ao \ {}" by auto moreover have "Min (- insert y (set ys) \ above ao) = x" using yys y_Min xxs_above \x < y\ False by(auto intro!: Min_eqI simp add: proper_interval_Some2) moreover have "- set (y # ys) \ above ao - {x} = - set (y # ys) \ above (Some x)" using yys_above False xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed) ultimately have A'_less: "?A \' - set (y # ys) \ above ao" using Min_A' A_less Amx xxs_above by(subst set_less_aux_rec) simp_all moreover have "?A \ above ao" using subset xxs_above by(auto intro: above_upclosed) ultimately show ?rhs using less_A' by blast next assume ?rhs then obtain A where less_A: "set (x # xs) \' A" and A_less: "A \' - set (y # ys) \ above ao" and subset: "A \ above ao" by blast let ?A = "A - {x}" from less_A subset xxs_above have "set (x # xs) \ above ao \' A \ above ao" by(simp add: Int_absorb2) with False xxs_above subset have "x \ A" by(auto simp add: set_less_aux_def proper_interval_Some2) hence "\ \ {}" by auto moreover from \x \ A\ False subset have Min_A: "Min A = x" by(auto intro!: Min_eqI simp add: proper_interval_Some2 not_less) moreover have "Min (set (x # xs)) = x" using x_Min by(auto intro!: Min_eqI) moreover have eq_A: "?A \ above (Some x)" using xxs_above False subset by(fastforce simp add: proper_interval_Some2 not_less intro: above_upclosed) moreover have "set xs - {x} = set xs" using x_Min by(auto) ultimately have less_A': "set xs \' ?A" using xxs_above less_A by(subst (asm) set_less_aux_rec)(simp_all cong: conj_cong) have "x \ - insert y (set ys) \ above ao" using \x < y\ xxs_above y_Min by auto hence "- insert y (set ys) \ above ao \ {}" by auto moreover have "Min (- set (y # ys) \ above ao) = x" using yys y_Min xxs_above \x < y\ False by(auto intro!: Min_eqI simp add: proper_interval_Some2) moreover have "- set (y # ys) \ above (Some x) = - set (y # ys) \ above ao - {x}" by(auto simp add: above_eq) ultimately have "?A \' - set (y # ys) \ above (Some x)" using A_less \A \ {}\ eq_A Min_A by(subst (asm) set_less_aux_rec) simp_all with less_A' eq_A show ?lhs' by blast qed finally show ?thesis using False by simp qed thus ?thesis using True by simp next case False show ?thesis proof(cases "y < x") case True have "proper_interval ao (Some y) \ proper_interval_set_Compl_aux (Some y) (card (UNIV - above ao) + 1) (x # xs) ys \ (\A \ above ao. set (x # xs) \' A \ A \' - set (y # ys) \ above ao)" (is "?lhs \ ?rhs") proof(cases "proper_interval ao (Some y)") case True then obtain z where z: "z \ above ao" "z < y" by(clarsimp simp add: proper_interval_Some2) from xxs \y < x\ have "\x'\set (x # xs). y < x'" by(auto) hence less_A: "set (x # xs) \' {y}" by(auto simp add: set_less_aux_def intro!: bexI[where x=y]) have "{y} \' {z}" using z y_Min by(auto simp add: set_less_aux_def intro: bexI[where x=z]) also have "\ \ - set (y # ys) \ above ao" using z y_Min by auto hence "{z} \' \" by(auto intro: subset_finite_imp_set_less_eq_aux) finally have "{y} \' \" . moreover have "{y} \ above ao" using yys_above by auto ultimately have ?rhs using less_A by blast thus ?thesis using True by simp next case False hence above_eq: "above ao = insert y (above (Some y))" using yys_above by(auto simp add: proper_interval_Some2 intro: above_upclosed) moreover have "card (above (Some y)) < CARD('a)" by(rule psubset_card_mono)(auto) ultimately have card_eq: "card (UNIV - above ao) + 1 = card (UNIV - above (Some y))" by(simp add: card_Diff_subset) from yys_above y_Min have ys_above: "set ys \ above (Some y)" by(auto) have eq_ys: "- set ys \ above (Some y) = - set (y # ys) \ above ao" by(auto simp add: above_eq) from \y < x\ x_Min have "set (x # xs) \ above (Some y)" by(auto) with \\ x < y\ \y < x\ card_eq xxs ys ys_above have "proper_interval_set_Compl_aux (Some y) (card (UNIV - above ao) + 1) (x # xs) ys \ (\A \ above (Some y). set (x # xs) \' A \ A \' - set ys \ above (Some y))" by(subst card_eq)(rule 4) also have "\ \ ?rhs" (is "?lhs' \ _") proof assume ?lhs' then obtain A where "set (x # xs) \' A" and subset: "A \ above (Some y)" and "A \' - set ys \ above (Some y)" by blast moreover from subset have "A - {y} = A" by auto ultimately have "set (x # xs) \' A - {y}" and "A - {y} \' - set (y # ys) \ above ao" using eq_ys by simp_all moreover from subset have "A - {y} \ above ao" using yys_above by(auto intro: above_upclosed) ultimately show ?rhs by blast next assume ?rhs then obtain A where "set (x # xs) \' A" and A_less: "A \' - set (y # ys) \ above ao" and subset: "A \ above ao" by blast moreover from A_less False yys_above have "y \ A" by(auto simp add: set_less_aux_def proper_interval_Some2 not_less) ultimately have "set (x # xs) \' A" and "A \' - set ys \ above (Some y)" using eq_ys by simp_all moreover from \y \ A\ subset above_eq have "A \ above (Some y)" by auto ultimately show ?lhs' by blast qed finally show ?thesis using False by simp qed with False True show ?thesis by simp next case False with \\ x < y\ have "x = y" by simp have "proper_interval ao (Some x) \ (CARD('a) - (card (UNIV - above ao) + length ys) \ 2 \ CARD('a) - (card (UNIV - above ao) + length xs) \ 2) \ (\A \ above ao. set (x # xs) \' A \ A \' - set (y # ys) \ above ao)" (is "?below \ ?card \ ?rhs") proof(cases "?below") case False hence "- set (y # ys) \ above ao \' set (x # xs)" using \x = y\ yys_above xxs_above y_Min by(auto simp add: not_less set_less_aux_def proper_interval_Some2 intro!: bexI[where x=y]) with False show ?thesis by(auto dest: set_less_aux_trans) next case True then obtain z where z: "z \ above ao" "z < x" by(clarsimp simp add: proper_interval_Some2) have "?card \ ?rhs" proof assume ?rhs then obtain A where less_A: "set (x # xs) \' A" and A_less: "A \' - set (y # ys) \ above ao" and subset: "A \ above ao" by blast { assume c_ys: "CARD('a) - (card (UNIV - above ao) + length ys) = 2" and c_xs: "CARD('a) - (card (UNIV - above ao) + length xs) = 2" from c_ys yys_above len_ys y_Min have "card (UNIV - (UNIV - above ao) - set (y # ys)) = 1" by(subst card_Diff_subset)(auto simp add: card_Diff_subset) then obtain z' where eq_y: "- set (y # ys) \ above ao = {z'}" unfolding card_eq_1_iff by auto moreover from z have "z \ set (y # ys)" using \x = y\ y_Min by auto ultimately have "z' = z" using z by fastforce from c_xs xxs_above len_xs x_Min have "card (UNIV - (UNIV - above ao) - set (x # xs)) = 1" by(subst card_Diff_subset)(auto simp add: card_Diff_subset) then obtain z'' where eq_x: "- set (x # xs) \ above ao = {z''}" unfolding card_eq_1_iff by auto moreover from z have "z \ set (x # xs)" using x_Min by auto ultimately have "z'' = z" using z by fastforce from less_A subset obtain q where "q \ A" "q \ above ao" "q \ set (x # xs)" by(auto simp add: set_less_aux_def) hence "q \ {z''}" unfolding eq_x[symmetric] by simp hence "q = z''" by simp with \q \ A\ \z' = z\ \z'' = z\ z have "- set (y # ys) \ above ao \ A" unfolding eq_y by simp hence "- set (y # ys) \ above ao \' A" by(auto intro: subset_finite_imp_set_less_eq_aux) with A_less have False by(auto dest: set_less_trans_set_less_eq) } thus ?card by auto next assume ?card (is "?card_ys \ ?card_xs") thus ?rhs proof assume ?card_ys let ?YS = "UNIV - (UNIV - above ao) - set (y # ys)" from \?card_ys\ yys_above len_ys y_Min have "card ?YS \ 1" by(subst card_Diff_subset)(auto simp add: card_Diff_subset) moreover have "?YS \ {}" using True y_Min yys_above \x = y\ by(fastforce simp add: proper_interval_Some2) hence "card ?YS \ 0" by simp ultimately have "card ?YS > 1" by(cases "card ?YS") simp_all from card_gt_1D[OF this] obtain x' y' where x': "x' \ above ao" "x' \ set (y # ys)" and y': "y' \ above ao" "y' \ set (y # ys)" and neq: "x' \ y'" by auto let ?A = "{z}" have "set (x # xs) \' ?A" using z x_Min by(auto simp add: set_less_aux_def intro!: rev_bexI) moreover { have "?A \ - set (y # ys) \ above ao" using z \x = y\ y_Min by(auto) moreover have "x' \ ?A \ y' \ ?A" using neq by auto with x' y' have "?A \ - set (y # ys) \ above ao" by auto ultimately have "?A \ - set (y # ys) \ above ao" by(rule psubsetI) hence "?A \' \" by(fastforce intro: psubset_finite_imp_set_less_aux) } ultimately show ?thesis using z by blast next assume ?card_xs let ?XS = "UNIV - (UNIV - above ao) - set (x # xs)" from \?card_xs\ xxs_above len_xs x_Min have "card ?XS \ 1" by(subst card_Diff_subset)(auto simp add: card_Diff_subset) moreover have "?XS \ {}" using True x_Min xxs_above by(fastforce simp add: proper_interval_Some2) hence "card ?XS \ 0" by simp ultimately have "card ?XS > 1" by(cases "card ?XS") simp_all from card_gt_1D[OF this] obtain x' y' where x': "x' \ above ao" "x' \ set (x # xs)" and y': "y' \ above ao" "y' \ set (x # xs)" and neq: "x' \ y'" by auto define A where "A = (if x' = Min (above ao) then insert y' (set (x # xs)) else insert x' (set (x # xs)))" hence "set (x # xs) \ A" by auto moreover have "set (x # xs) \ \" using neq x' y' by(auto simp add: A_def) ultimately have "set (x # xs) \ A" .. hence "set (x # xs) \' \" by(fastforce intro: psubset_finite_imp_set_less_aux) moreover { have nempty: "above ao \ {}" using z by auto have "A \' {Min (above ao)}" using z x' y' neq \x = y\ x_Min xxs_above by(auto 6 4 simp add: set_less_aux_def A_def nempty intro!: rev_bexI Min_eqI) also have "Min (above ao) \ z" using z by(simp) hence "Min (above ao) < x" using \z < x\ by(rule le_less_trans) with \x = y\ y_Min have "Min (above ao) \ set (y # ys)" by auto hence "{Min (above ao)} \ - set (y # ys) \ above ao" by(auto simp add: nempty) hence "{Min (above ao)} \' \" by(auto intro: subset_finite_imp_set_less_eq_aux) finally have "A \' \" . } moreover have "A \ above ao" using xxs_above yys_above x' y' by(auto simp add: A_def) ultimately show ?rhs by blast qed qed thus ?thesis using True by simp qed thus ?thesis using \x = y\ by simp qed qed qed } from this[of None] show ?thesis by(simp) qed lemma proper_interval_Compl_set_aux: assumes fin: "finite (UNIV :: 'a set)" and xs: "sorted xs" "distinct xs" and ys: "sorted ys" "distinct ys" shows "proper_interval_Compl_set_aux None xs ys \ (\A. - set xs \' A \ A \' set ys)" proof - note [simp] = finite_subset[OF subset_UNIV fin] define above where "above = case_option UNIV (Collect \ less)" have above_simps [simp]: "above None = UNIV" "\x. above (Some x) = {y. x < y}" and above_upclosed: "\x y ao. \ x \ above ao; x < y \ \ y \ above ao" and proper_interval_Some2: "\x ao. proper_interval ao (Some x) \ (\z\above ao. z < x)" by(simp_all add: proper_interval_simps above_def split: option.splits) { fix ao n assume "set xs \ above ao" "set ys \ above ao" from xs \set xs \ above ao\ ys \set ys \ above ao\ have "proper_interval_Compl_set_aux ao xs ys \ (\A. - set xs \ above ao \' A \ above ao \ A \ above ao \' set ys \ above ao)" proof(induction ao xs ys rule: proper_interval_Compl_set_aux.induct) case ("2_1" ao ys) { fix A assume "above ao \' A \ above ao" also have "\ \ above ao" by simp hence "A \ above ao \' above ao" by(auto intro: subset_finite_imp_set_less_eq_aux) finally have False by simp } thus ?case by auto next case ("2_2" ao xs) thus ?case by simp next case (1 ao x xs y ys) note xxs = \sorted (x # xs)\ \distinct (x # xs)\ hence xs: "sorted xs" "distinct xs" and x_Min: "\x' \ set xs. x < x'" by(auto simp add: less_le) note yys = \sorted (y # ys)\ \distinct (y # ys)\ hence ys: "sorted ys" "distinct ys" and y_Min: "\y'\set ys. y < y'" by(auto simp add: less_le) note xxs_above = \set (x # xs) \ above ao\ note yys_above = \set (y # ys) \ above ao\ show ?case proof(cases "x < y") case True have "\ proper_interval ao (Some x) \ proper_interval_Compl_set_aux (Some x) xs (y # ys) \ (\A. - set (x # xs) \ above ao \' A \ above ao \ A \ above ao \' set (y # ys) \ above ao)" (is "?lhs \ ?rhs") proof(cases "proper_interval ao (Some x)") case True then obtain z where z: "z < x" "z \ above ao" by(auto simp add: proper_interval_Some2) hence nempty: "above ao \ {}" by auto with z have "Min (above ao) \ z" by auto hence "Min (above ao) < x" using \z < x\ by(rule le_less_trans) hence "set (y # ys) \ above ao \' - set (x # xs) \ above ao" using y_Min x_Min z \x < y\ by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"]) thus ?thesis using True by(auto dest: set_less_aux_trans set_less_aux_antisym) next case False hence above_eq: "above ao = insert x (above (Some x))" using xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed) from x_Min have xs_above: "set xs \ above (Some x)" by auto from \x < y\ y_Min have ys_above: "set (y # ys) \ above (Some x)" by auto have eq_xs: "- set xs \ above (Some x) = - set (x # xs) \ above ao" using above_eq by auto have eq_ys: "set (y # ys) \ above (Some x) = set (y # ys) \ above ao" using y_Min \x < y\ xxs_above by(auto intro: above_upclosed) from \x < y\ xs xs_above yys ys_above have "proper_interval_Compl_set_aux (Some x) xs (y # ys) \ (\A. - set xs \ above (Some x) \' A \ above (Some x) \ A \ above (Some x) \' set (y # ys) \ above (Some x))" by(rule "1.IH") also have "\ \ ?rhs" (is "?lhs \ _") proof assume ?lhs then obtain A where "- set xs \ above (Some x) \' A \ above (Some x)" and "A \ above (Some x) \' set (y # ys) \ above (Some x)" by blast moreover have "A \ above (Some x) = (A - {x}) \ above ao" using above_eq by auto ultimately have "- set (x # xs) \ above ao \' (A - {x}) \ above ao" and "(A - {x}) \ above ao \' set (y # ys) \ above ao" using eq_xs eq_ys by simp_all thus ?rhs by blast next assume ?rhs then obtain A where "- set (x # xs) \ above ao \' A \ above ao" and A_less: "A \ above ao \' set (y # ys) \ above ao" by blast moreover have "x \ A" proof assume "x \ A" hence "set (y # ys) \ above ao \' A \ above ao" using y_Min \x < y\ by(auto simp add: above_eq set_less_aux_def intro!: bexI[where x=x]) with A_less show False by(auto dest: set_less_aux_antisym) qed hence "A \ above ao = A \ above (Some x)" using above_eq by auto ultimately show ?lhs using eq_xs eq_ys by auto qed finally show ?thesis using False by simp qed thus ?thesis using True by simp next case False show ?thesis proof(cases "y < x") case True show ?thesis (is "?lhs \ ?rhs") proof(cases "proper_interval ao (Some y)") case True then obtain z where z: "z < y" "z \ above ao" by(auto simp add: proper_interval_Some2) hence nempty: "above ao \ {}" by auto with z have "Min (above ao) \ z" by auto hence "Min (above ao) < y" using \z < y\ by(rule le_less_trans) hence "set (y # ys) \ above ao \' - set (x # xs) \ above ao" using y_Min x_Min z \y < x\ by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"]) thus ?thesis using True \y < x\ by(auto dest: set_less_aux_trans set_less_aux_antisym) next case False hence above_eq: "above ao = insert y (above (Some y))" using yys_above by(auto simp add: proper_interval_Some2 intro: above_upclosed) from y_Min have ys_above: "set ys \ above (Some y)" by auto from \y < x\ x_Min have xs_above: "set (x # xs) \ above (Some y)" by auto have "y \ - set (x # xs) \ above ao" using \y < x\ x_Min yys_above by auto hence nempty: "- set (x # xs) \ above ao \ {}" by auto have Min_x: "Min (- set (x # xs) \ above ao) = y" using above_eq \y < x\ x_Min by(auto intro!: Min_eqI) have Min_y: "Min (set (y # ys) \ above ao) = y" using y_Min above_eq by(auto intro!: Min_eqI) have eq_xs: "- set (x # xs) \ above ao - {y} = - set (x # xs) \ above (Some y)" by(auto simp add: above_eq) have eq_ys: "set ys \ above ao - {y} = set ys \ above (Some y)" using y_Min above_eq by auto from \\ x < y\ \y < x\ xxs xs_above ys ys_above have "proper_interval_Compl_set_aux (Some y) (x # xs) ys \ (\A. - set (x # xs) \ above (Some y) \' A \ above (Some y) \ A \ above (Some y) \' set ys \ above (Some y))" by(rule "1.IH") also have "\ \ ?rhs" (is "?lhs' \ _") proof assume ?lhs' then obtain A where less_A: "- set (x # xs) \ above (Some y) \' A \ above (Some y)" and A_less: "A \ above (Some y) \' set ys \ above (Some y)" by blast let ?A = "insert y A" have Min_A: "Min (?A \ above ao) = y" using above_eq by(auto intro!: Min_eqI) moreover have A_eq: "A \ above ao - {y} = A \ above (Some y)" using above_eq by auto ultimately have less_A': "- set (x # xs) \ above ao \' ?A \ above ao" using nempty yys_above less_A Min_x eq_xs by(subst set_less_aux_rec) simp_all have A'_less: "?A \ above ao \' set (y # ys) \ above ao" using yys_above nempty Min_A A_eq A_less Min_y eq_ys by(subst set_less_aux_rec) simp_all with less_A' show ?rhs by blast next assume ?rhs then obtain A where less_A: "- set (x # xs) \ above ao \' A \ above ao" and A_less: "A \ above ao \' set (y # ys) \ above ao" by blast from less_A have nempty': "A \ above ao \ {}" by auto moreover have A_eq: "A \ above ao - {y} = A \ above (Some y)" using above_eq by auto moreover have y_in_xxs: "y \ - set (x # xs) \ above ao" using \y < x\ x_Min yys_above by auto moreover have "y \ A" proof(rule ccontr) assume "y \ A" hence "A \ above ao \' - set (x # xs) \ above ao" using \y < x\ x_Min y_in_xxs by(auto simp add: set_less_aux_def above_eq intro: bexI[where x=y]) with less_A show False by(rule set_less_aux_antisym) qed hence Min_A: "Min (A \ above ao) = y" using above_eq y_Min by(auto intro!: Min_eqI) ultimately have less_A': "- set (x # xs) \ above (Some y) \' A \ above (Some y)" using nempty less_A Min_x eq_xs by(subst (asm) set_less_aux_rec)(auto dest: bspec[where x=y]) have A'_less: "A \ above (Some y) \' set ys \ above (Some y)" using A_less nempty' yys_above Min_A Min_y A_eq eq_ys by(subst (asm) set_less_aux_rec) simp_all with less_A' show ?lhs' by blast qed finally show ?thesis using \\ x < y\ \y < x\ False by simp qed next case False with \\ x < y\ have "x = y" by auto thus ?thesis (is "?lhs \ ?rhs") proof(cases "proper_interval ao (Some x)") case True then obtain z where z: "z < x" "z \ above ao" by(auto simp add: proper_interval_Some2) hence nempty: "above ao \ {}" by auto with z have "Min (above ao) \ z" by auto hence "Min (above ao) < x" using \z < x\ by(rule le_less_trans) hence "set (y # ys) \ above ao \' - set (x # xs) \ above ao" using y_Min x_Min z \x = y\ by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"]) thus ?thesis using True \x = y\ by(auto dest: set_less_aux_trans set_less_aux_antisym) next case False hence above_eq: "above ao = insert x (above (Some x))" using xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed) have "(ys = [] \ xs \ []) \ ?rhs" (is "?lhs' \ _") proof(intro iffI strip notI) assume ?lhs' show ?rhs proof(cases ys) case Nil with \?lhs'\ obtain x' xs' where xs_eq: "xs = x' # xs'" by(auto simp add: neq_Nil_conv) with xs have x'_Min: "\x'' \ set xs'. x' < x''" by(auto simp add: less_le) let ?A = "- set (x # xs')" have "- set (x # xs) \ above ao \ ?A \ above ao" using xs_eq by auto moreover have "x' \ - set (x # xs) \ above ao" "x' \ ?A \ above ao" using xs_eq xxs_above x'_Min x_Min by auto ultimately have "- set (x # xs) \ above ao \ ?A \ above ao" by blast hence "- set (x # xs) \ above ao \' \ " by(fastforce intro: psubset_finite_imp_set_less_aux) moreover have "\ \' set (y # ys) \ above ao" using Nil \x = y\ by(auto simp add: set_less_aux_def above_eq) ultimately show ?thesis by blast next case (Cons y' ys') let ?A = "{y}" have "- set (x # xs) \ above ao \' ?A \ above ao" using \x = y\ x_Min by(auto simp add: set_less_aux_def above_eq) moreover have "\ \ set (y # ys) \ above ao" using yys_above yys Cons by auto hence "?A \ above ao \' \" by(fastforce intro: psubset_finite_imp_set_less_aux) ultimately show ?thesis by blast qed next assume Nil: "ys = []" "xs = []" and ?rhs then obtain A where less_A: "- {x} \ above ao \' A \ above ao" and A_less: "A \ above ao \' {x}" using \x = y\ above_eq by auto have "x \ A" using A_less by(auto simp add: set_less_aux_def above_eq) hence "A \ above ao \ - {x} \ above ao" by auto hence "A \ above ao \' \" by(auto intro: subset_finite_imp_set_less_eq_aux) with less_A have "\ \' \" by(rule set_less_trans_set_less_eq) thus False by simp qed with \x = y\ False show ?thesis by simp qed qed qed qed } from this[of None] show ?thesis by simp qed end subsection \Proper intervals for HOL types\ instantiation unit :: proper_interval begin fun proper_interval_unit :: "unit proper_interval" where "proper_interval_unit None None = True" | "proper_interval_unit _ _ = False" instance by intro_classes auto end instantiation bool :: proper_interval begin fun proper_interval_bool :: "bool proper_interval" where "proper_interval_bool (Some x) (Some y) \ False" | "proper_interval_bool (Some x) None \ \ x" | "proper_interval_bool None (Some y) \ y" | "proper_interval_bool None None = True" instance by intro_classes auto end instantiation nat :: proper_interval begin fun proper_interval_nat :: "nat proper_interval" where "proper_interval_nat no None = True" | "proper_interval_nat None (Some x) \ x > 0" | "proper_interval_nat (Some x) (Some y) \ y - x > 1" instance by intro_classes auto end instantiation int :: proper_interval begin fun proper_interval_int :: "int proper_interval" where "proper_interval_int (Some x) (Some y) \ y - x > 1" | "proper_interval_int _ _ = True" instance by intro_classes (auto intro: less_add_one, metis less_add_one minus_less_iff) end instantiation integer :: proper_interval begin context includes integer.lifting begin lift_definition proper_interval_integer :: "integer proper_interval" is "proper_interval" . instance by(intro_classes)(transfer, simp only: proper_interval_simps)+ end end lemma proper_interval_integer_simps [code]: includes integer.lifting fixes x y :: integer and xo yo :: "integer option" shows "proper_interval (Some x) (Some y) = (1 < y - x)" "proper_interval None yo = True" "proper_interval xo None = True" by(transfer, simp)+ instantiation natural :: proper_interval begin context includes natural.lifting begin lift_definition proper_interval_natural :: "natural proper_interval" is "proper_interval" . instance by(intro_classes)(transfer, simp only: proper_interval_simps)+ end end lemma proper_interval_natural_simps [code]: includes natural.lifting fixes x y :: natural and xo :: "natural option" shows "proper_interval xo None = True" "proper_interval None (Some y) \ y > 0" "proper_interval (Some x) (Some y) \ y - x > 1" by(transfer, simp)+ lemma char_less_iff_nat_of_char: "x < y \ of_char x < (of_char y :: nat)" by (fact less_char_def) lemma nat_of_char_inject [simp]: "of_char x = (of_char y :: nat) \ x = y" by (fact of_char_eq_iff) lemma char_le_iff_nat_of_char: "x \ y \ of_char x \ (of_char y :: nat)" by (fact less_eq_char_def) instantiation char :: proper_interval begin fun proper_interval_char :: "char proper_interval" where "proper_interval_char None None \ True" | "proper_interval_char None (Some x) \ x \ CHR 0x00" | "proper_interval_char (Some x) None \ x \ CHR 0xFF" | "proper_interval_char (Some x) (Some y) \ of_char y - of_char x > (1 :: nat)" instance proof fix y :: char { assume "y \ CHR 0x00" have "CHR 0x00 < y" proof (rule ccontr) assume "\ CHR 0x00 < y" then have "of_char y = (of_char CHR 0x00 :: nat)" by (simp add: not_less char_le_iff_nat_of_char) then have "y = CHR 0x00" using nat_of_char_inject [of y "CHR 0x00"] by simp with \y \ CHR 0x00\ show False by simp qed } moreover { fix z :: char assume "z < CHR 0x00" hence False by (simp add: char_less_iff_nat_of_char of_char_eq_iff [symmetric]) } ultimately show "proper_interval None (Some y) = (\z. z < y)" by auto fix x :: char { assume "x \ CHR 0xFF" then have "x < CHR 0xFF" by (auto simp add: neq_iff char_less_iff_nat_of_char) (insert nat_of_char_less_256 [of x], simp) hence "\z. x < z" .. } moreover { fix z :: char assume "CHR 0xFF < z" hence "False" by (simp add: char_less_iff_nat_of_char) (insert nat_of_char_less_256 [of z], simp) } ultimately show "proper_interval (Some x) None = (\z. x < z)" by auto { assume gt: "of_char y - of_char x > (1 :: nat)" let ?z = "char_of (of_char x + (1 :: nat))" from gt nat_of_char_less_256 [of y] have 255: "of_char x < (255 :: nat)" by arith with gt have "x < ?z" "?z < y" by (simp_all add: char_less_iff_nat_of_char) hence "\z. x < z \ z < y" by blast } moreover { fix z assume "x < z" "z < y" hence "(1 :: nat) < of_char y - of_char x" by (simp add: char_less_iff_nat_of_char) } ultimately show "proper_interval (Some x) (Some y) = (\z>x. z < y)" by auto qed simp end instantiation Enum.finite_1 :: proper_interval begin definition proper_interval_finite_1 :: "Enum.finite_1 proper_interval" where "proper_interval_finite_1 x y \ x = None \ y = None" instance by intro_classes (simp_all add: proper_interval_finite_1_def less_finite_1_def) end instantiation Enum.finite_2 :: proper_interval begin fun proper_interval_finite_2 :: "Enum.finite_2 proper_interval" where "proper_interval_finite_2 None None \ True" | "proper_interval_finite_2 None (Some x) \ x = finite_2.a\<^sub>2" | "proper_interval_finite_2 (Some x) None \ x = finite_2.a\<^sub>1" | "proper_interval_finite_2 (Some x) (Some y) \ False" instance by intro_classes (auto simp add: less_finite_2_def) end instantiation Enum.finite_3 :: proper_interval begin fun proper_interval_finite_3 :: "Enum.finite_3 proper_interval" where "proper_interval_finite_3 None None \ True" | "proper_interval_finite_3 None (Some x) \ x \ finite_3.a\<^sub>1" | "proper_interval_finite_3 (Some x) None \ x \ finite_3.a\<^sub>3" | "proper_interval_finite_3 (Some x) (Some y) \ x = finite_3.a\<^sub>1 \ y = finite_3.a\<^sub>3" instance proof fix x y :: Enum.finite_3 show "proper_interval None (Some y) = (\z. z < y)" by(cases y)(auto simp add: less_finite_3_def split: finite_3.split) show "proper_interval (Some x) None = (\z. x < z)" by(cases x)(auto simp add: less_finite_3_def) show "proper_interval (Some x) (Some y) = (\z>x. z < y)" by(auto simp add: less_finite_3_def split: finite_3.split_asm) qed simp end subsection \List fusion for the order and proper intervals on @{typ "'a set"}\ definition length_last_fusion :: "('a, 's) generator \ 's \ nat \ 'a" where "length_last_fusion g s = length_last (list.unfoldr g s)" lemma length_last_fusion_code [code]: "length_last_fusion g s = (if list.has_next g s then let (x, s') = list.next g s in fold_fusion g (\x (n, _). (n + 1, x)) s' (1, x) else (0, undefined))" unfolding length_last_fusion_def by(subst list.unfoldr.simps)(simp add: length_last_Nil length_last_Cons_code fold_fusion_def split_beta) declare length_last_fusion_def [symmetric, code_unfold] context proper_intrvl begin definition set_less_eq_aux_Compl_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 'a option \ 's1 \ 's2 \ bool" where "set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 = set_less_eq_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)" definition Compl_set_less_eq_aux_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 'a option \ 's1 \ 's2 \ bool" where "Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 = Compl_set_less_eq_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)" definition set_less_aux_Compl_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 'a option \ 's1 \ 's2 \ bool" where "set_less_aux_Compl_fusion g1 g2 ao s1 s2 = set_less_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)" definition Compl_set_less_aux_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 'a option \ 's1 \ 's2 \ bool" where "Compl_set_less_aux_fusion g1 g2 ao s1 s2 = Compl_set_less_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)" definition exhaustive_above_fusion :: "('a, 's) generator \ 'a \ 's \ bool" where "exhaustive_above_fusion g a s = exhaustive_above a (list.unfoldr g s)" definition exhaustive_fusion :: "('a, 's) generator \ 's \ bool" where "exhaustive_fusion g s = exhaustive (list.unfoldr g s)" definition proper_interval_set_aux_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 's1 \ 's2 \ bool" where "proper_interval_set_aux_fusion g1 g2 s1 s2 = proper_interval_set_aux (list.unfoldr g1 s1) (list.unfoldr g2 s2)" definition proper_interval_set_Compl_aux_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 'a option \ nat \ 's1 \ 's2 \ bool" where "proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 = proper_interval_set_Compl_aux ao n (list.unfoldr g1 s1) (list.unfoldr g2 s2)" definition proper_interval_Compl_set_aux_fusion :: "('a, 's1) generator \ ('a, 's2) generator \ 'a option \ 's1 \ 's2 \ bool" where "proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 = proper_interval_Compl_set_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)" lemma set_less_eq_aux_Compl_fusion_code: "set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 \ (list.has_next g1 s1 \ list.has_next g2 s2 \ (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \ set_less_eq_aux_Compl_fusion g1 g2 (Some x) s1' s2 else if y < x then proper_interval ao (Some y) \ set_less_eq_aux_Compl_fusion g1 g2 (Some y) s1 s2' else proper_interval ao (Some y)))" unfolding set_less_eq_aux_Compl_fusion_def by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta) lemma Compl_set_less_eq_aux_fusion_code: "Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 \ (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then \ proper_interval ao (Some x) \ Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2 else if y < x then \ proper_interval ao (Some y) \ Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2' else \ proper_interval ao (Some y) else \ proper_interval ao (Some x) \ Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2 else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in \ proper_interval ao (Some y) \ Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2' else \ proper_interval ao None)" unfolding Compl_set_less_eq_aux_fusion_def by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta) lemma set_less_aux_Compl_fusion_code: "set_less_aux_Compl_fusion g1 g2 ao s1 s2 \ (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \ set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2 else if y < x then proper_interval ao (Some y) \ set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2' else proper_interval ao (Some y) else proper_interval ao (Some x) \ set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2 else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in proper_interval ao (Some y) \ set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2' else proper_interval ao None)" unfolding set_less_aux_Compl_fusion_def by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta) lemma Compl_set_less_aux_fusion_code: "Compl_set_less_aux_fusion g1 g2 ao s1 s2 \ list.has_next g1 s1 \ list.has_next g2 s2 \ (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then \ proper_interval ao (Some x) \ Compl_set_less_aux_fusion g1 g2 (Some x) s1' s2 else if y < x then \ proper_interval ao (Some y) \ Compl_set_less_aux_fusion g1 g2 (Some y) s1 s2' else \ proper_interval ao (Some y))" unfolding Compl_set_less_aux_fusion_def by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta) lemma exhaustive_above_fusion_code: "exhaustive_above_fusion g y s \ (if list.has_next g s then let (x, s') = list.next g s in \ proper_interval (Some y) (Some x) \ exhaustive_above_fusion g x s' else \ proper_interval (Some y) None)" unfolding exhaustive_above_fusion_def by(subst list.unfoldr.simps)(simp add: split_beta) lemma exhaustive_fusion_code: "exhaustive_fusion g s = (list.has_next g s \ (let (x, s') = list.next g s in \ proper_interval None (Some x) \ exhaustive_above_fusion g x s'))" unfolding exhaustive_fusion_def exhaustive_above_fusion_def by(subst (1) list.unfoldr.simps)(simp add: split_beta) lemma proper_interval_set_aux_fusion_code: "proper_interval_set_aux_fusion g1 g2 s1 s2 \ list.has_next g2 s2 \ (let (y, s2') = list.next g2 s2 in if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if x < y then False else if y < x then proper_interval (Some y) (Some x) \ list.has_next g2 s2' \ \ exhaustive_above_fusion g1 x s1' else proper_interval_set_aux_fusion g1 g2 s1' s2' else list.has_next g2 s2' \ proper_interval (Some y) None)" unfolding proper_interval_set_aux_fusion_def exhaustive_above_fusion_def by(subst (1 2) list.unfoldr.simps)(simp add: split_beta) lemma proper_interval_set_Compl_aux_fusion_code: "proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 \ (if list.has_next g1 s1 then let (x, s1') = list.next g1 s1 in if list.has_next g2 s2 then let (y, s2') = list.next g2 s2 in if x < y then proper_interval ao (Some x) \ proper_interval_set_Compl_aux_fusion g1 g2 (Some x) (n + 1) s1' s2 else if y < x then proper_interval ao (Some y) \ proper_interval_set_Compl_aux_fusion g1 g2 (Some y) (n + 1) s1 s2' else proper_interval ao (Some x) \ (let m = CARD('a) - n in m - length_fusion g2 s2' \ 2 \ m - length_fusion g1 s1' \ 2) else let m = CARD('a) - n; (len_x, x') = length_last_fusion g1 s1 in m \ len_x \ (m = len_x + 1 \ \ proper_interval (Some x') None) else if list.has_next g2 s2 then let (y, s2') = list.next g2 s2; m = CARD('a) - n; (len_y, y') = length_last_fusion g2 s2 in m \ len_y \ (m = len_y + 1 \ \ proper_interval (Some y') None) else CARD('a) > n + 1)" unfolding proper_interval_set_Compl_aux_fusion_def length_last_fusion_def length_fusion_def by(subst (1 2 4 5 9 10) list.unfoldr.simps)(simp add: split_beta) lemma proper_interval_Compl_set_aux_fusion_code: "proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 \ list.has_next g1 s1 \ list.has_next g2 s2 \ (let (x, s1') = list.next g1 s1; (y, s2') = list.next g2 s2 in if x < y then \ proper_interval ao (Some x) \ proper_interval_Compl_set_aux_fusion g1 g2 (Some x) s1' s2 else if y < x then \ proper_interval ao (Some y) \ proper_interval_Compl_set_aux_fusion g1 g2 (Some y) s1 s2' else \ proper_interval ao (Some x) \ (list.has_next g2 s2' \ list.has_next g1 s1'))" unfolding proper_interval_Compl_set_aux_fusion_def by(subst (1 2 4 5) list.unfoldr.simps)(auto simp add: split_beta) end lemmas [code] = set_less_eq_aux_Compl_fusion_code proper_intrvl.set_less_eq_aux_Compl_fusion_code Compl_set_less_eq_aux_fusion_code proper_intrvl.Compl_set_less_eq_aux_fusion_code set_less_aux_Compl_fusion_code proper_intrvl.set_less_aux_Compl_fusion_code Compl_set_less_aux_fusion_code proper_intrvl.Compl_set_less_aux_fusion_code exhaustive_above_fusion_code proper_intrvl.exhaustive_above_fusion_code exhaustive_fusion_code proper_intrvl.exhaustive_fusion_code proper_interval_set_aux_fusion_code proper_intrvl.proper_interval_set_aux_fusion_code proper_interval_set_Compl_aux_fusion_code proper_intrvl.proper_interval_set_Compl_aux_fusion_code proper_interval_Compl_set_aux_fusion_code proper_intrvl.proper_interval_Compl_set_aux_fusion_code lemmas [symmetric, code_unfold] = set_less_eq_aux_Compl_fusion_def proper_intrvl.set_less_eq_aux_Compl_fusion_def Compl_set_less_eq_aux_fusion_def proper_intrvl.Compl_set_less_eq_aux_fusion_def set_less_aux_Compl_fusion_def proper_intrvl.set_less_aux_Compl_fusion_def Compl_set_less_aux_fusion_def proper_intrvl.Compl_set_less_aux_fusion_def exhaustive_above_fusion_def proper_intrvl.exhaustive_above_fusion_def exhaustive_fusion_def proper_intrvl.exhaustive_fusion_def proper_interval_set_aux_fusion_def proper_intrvl.proper_interval_set_aux_fusion_def proper_interval_set_Compl_aux_fusion_def proper_intrvl.proper_interval_set_Compl_aux_fusion_def proper_interval_Compl_set_aux_fusion_def proper_intrvl.proper_interval_Compl_set_aux_fusion_def subsection \Drop notation\ context ord begin no_notation set_less_aux (infix "\''" 50) and set_less_eq_aux (infix "\''" 50) and set_less_eq_aux' (infix "\''''" 50) and set_less_eq_aux'' (infix "\''''''" 50) and set_less_eq (infix "\" 50) and set_less (infix "\" 50) end end diff --git a/thys/Jinja/DFA/Kildall.thy b/thys/Jinja/DFA/Kildall.thy --- a/thys/Jinja/DFA/Kildall.thy +++ b/thys/Jinja/DFA/Kildall.thy @@ -1,513 +1,517 @@ (* Title: HOL/MicroJava/BV/Kildall.thy Author: Tobias Nipkow, Gerwin Klein Copyright 2000 TUM Kildall's algorithm. *) section \Kildall's Algorithm \label{sec:Kildall}\ theory Kildall imports SemilatAlg begin primrec propa :: "'s binop \ (nat \ 's) list \ 's list \ nat set \ 's list * nat set" where "propa f [] \s w = (\s,w)" | "propa f (q'#qs) \s w = (let (q,\) = q'; u = \ \\<^bsub>f\<^esub> \s!q; w' = (if u = \s!q then w else insert q w) in propa f qs (\s[q := u]) w')" definition iter :: "'s binop \ 's step_type \ 's list \ nat set \ 's list \ nat set" where "iter f step \s w = while (\(\s,w). w \ {}) (\(\s,w). let p = SOME p. p \ w in propa f (step p (\s!p)) \s (w-{p})) (\s,w)" definition unstables :: "'s ord \ 's step_type \ 's list \ nat set" where "unstables r step \s = {p. p < size \s \ \stable r step \s p}" definition kildall :: "'s ord \ 's binop \ 's step_type \ 's list \ 's list" where "kildall r f step \s = fst(iter f step \s (unstables r step \s))" primrec merges :: "'s binop \ (nat \ 's) list \ 's list \ 's list" where "merges f [] \s = \s" | "merges f (p'#ps) \s = (let (p,\) = p' in merges f ps (\s[p := \ \\<^bsub>f\<^esub> \s!p]))" lemmas [simp] = Let_def Semilat.le_iff_plus_unchanged [OF Semilat.intro, symmetric] lemma (in Semilat) nth_merges: "\ss. \p < length ss; ss \ list n A; \(p,t)\set ps. p t\A \ \ (merges f ps ss)!p = map snd [(p',t') \ ps. p'=p] \\<^bsub>f\<^esub> ss!p" (is "\ss. \_; _; ?steptype ps\ \ ?P ss ps") (*<*) proof (induct ps) show "\ss. ?P ss []" by simp fix ss p' ps' assume ss: "ss \ list n A" assume l: "p < length ss" assume "?steptype (p'#ps')" then obtain a b where p': "p'=(a,b)" and ab: "aA" and ps': "?steptype ps'" by (cases p') auto assume "\ss. p< length ss \ ss \ list n A \ ?steptype ps' \ ?P ss ps'" hence IH: "\ss. ss \ list n A \ p < length ss \ ?P ss ps'" using ps' by iprover from ss ab have "ss[a := b \\<^bsub>f\<^esub> ss!a] \ list n A" by (simp add: closedD) moreover with l have "p < length (ss[a := b \\<^bsub>f\<^esub> ss!a])" by simp ultimately have "?P (ss[a := b \\<^bsub>f\<^esub> ss!a]) ps'" by (rule IH) with p' l show "?P ss (p'#ps')" by simp qed (*>*) (** merges **) lemma length_merges [simp]: "\ss. size(merges f ps ss) = size ss" (*<*) by (induct ps, auto) (*>*) lemma (in Semilat) merges_preserves_type_lemma: shows "\xs. xs \ list n A \ (\(p,x) \ set ps. p x\A) \ merges f ps xs \ list n A" (*<*) apply (insert closedI) apply (unfold closed_def) apply (induct ps) apply simp apply clarsimp done (*>*) lemma (in Semilat) merges_preserves_type [simp]: "\ xs \ list n A; \(p,x) \ set ps. p x\A \ \ merges f ps xs \ list n A" by (simp add: merges_preserves_type_lemma) lemma (in Semilat) merges_incr_lemma: "\xs. xs \ list n A \ (\(p,x)\set ps. p x \ A) \ xs [\\<^bsub>r\<^esub>] merges f ps xs" (*<*) apply (induct ps) apply simp apply simp apply clarify apply (rule order_trans) apply simp apply (erule list_update_incr) apply simp apply simp apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) done (*>*) lemma (in Semilat) merges_incr: "\ xs \ list n A; \(p,x)\set ps. p x \ A \ \ xs [\\<^bsub>r\<^esub>] merges f ps xs" by (simp add: merges_incr_lemma) lemma (in Semilat) merges_same_conv [rule_format]: "(\xs. xs \ list n A \ (\(p,x)\set ps. p x\A) \ (merges f ps xs = xs) = (\(p,x)\set ps. x \\<^bsub>r\<^esub> xs!p))" (*<*) apply (induct_tac ps) apply simp apply clarsimp apply (rename_tac p x ps xs) apply (rule iffI) apply (rule context_conjI) apply (subgoal_tac "xs[p := x \\<^bsub>f\<^esub> xs!p] [\\<^bsub>r\<^esub>] xs") apply (force dest!: le_listD simp add: nth_list_update) apply (erule subst, rule merges_incr) apply (blast intro!: listE_set intro: closedD listE_length [THEN nth_in]) apply clarify apply (rule conjI) apply simp apply (blast dest: boundedD) apply blast apply clarify apply (erule allE) apply (erule impE) apply assumption apply (drule bspec) apply assumption apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) apply blast apply clarify apply (simp add: le_iff_plus_unchanged [THEN iffD1] list_update_same_conv [THEN iffD2]) done (*>*) lemma (in Semilat) list_update_le_listI [rule_format]: "set xs \ A \ set ys \ A \ xs [\\<^bsub>r\<^esub>] ys \ p < size xs \ x \\<^bsub>r\<^esub> ys!p \ x\A \ xs[p := x \\<^bsub>f\<^esub> xs!p] [\\<^bsub>r\<^esub>] ys" (*<*) apply (insert semilat) apply (simp only: Listn.le_def lesub_def semilat_def) apply (simp add: list_all2_conv_all_nth nth_list_update) done (*>*) lemma (in Semilat) merges_pres_le_ub: assumes "set ts \ A" "set ss \ A" "\(p,t)\set ps. t \\<^bsub>r\<^esub> ts!p \ t \ A \ p < size ts" "ss [\\<^bsub>r\<^esub>] ts" shows "merges f ps ss [\\<^bsub>r\<^esub>] ts" (*<*) proof - { fix t ts ps have "\qs. \set ts \ A; \(p,t)\set ps. t \\<^bsub>r\<^esub> ts!p \ t \ A \ p< size ts \ \ set qs \ set ps \ (\ss. set ss \ A \ ss [\\<^bsub>r\<^esub>] ts \ merges f qs ss [\\<^bsub>r\<^esub>] ts)" apply (induct_tac qs) apply simp apply (simp (no_asm_simp)) apply clarify apply simp apply (erule allE, erule impE, erule_tac [2] mp) apply (drule bspec, assumption) apply (simp add: closedD) apply (drule bspec, assumption) apply (simp add: list_update_le_listI) done } note this [dest] from assms show ?thesis by blast qed (*>*) (** propa **) lemma decomp_propa: "\ss w. (\(q,t)\set qs. q < size ss) \ propa f qs ss w = (merges f qs ss, {q. \t.(q,t)\set qs \ t \\<^bsub>f\<^esub> ss!q \ ss!q} \ w)" (*<*) apply (induct qs) apply simp apply (simp (no_asm)) apply clarify apply simp apply (rule conjI) apply blast apply (simp add: nth_list_update) apply blast done (*>*) (** iter **) lemma (in Semilat) stable_pres_lemma: shows "\pres_type step n A; bounded step n; ss \ list n A; p \ w; \q\w. q < n; \q. q < n \ q \ w \ stable r step ss q; q < n; \s'. (q,s') \ set (step p (ss!p)) \ s' \\<^bsub>f\<^esub> ss!q = ss!q; q \ w \ q = p \ \ stable r step (merges f (step p (ss!p)) ss) q" (*<*) apply (unfold stable_def) apply (subgoal_tac "\s'. (q,s') \ set (step p (ss!p)) \ s' : A") prefer 2 apply clarify apply (erule pres_typeD) prefer 3 apply assumption apply (rule listE_nth_in) apply assumption apply simp apply simp apply simp apply clarify apply (subst nth_merges) apply simp apply (blast dest: boundedD) apply assumption apply clarify apply (rule conjI) apply (blast dest: boundedD) apply (erule pres_typeD) prefer 3 apply assumption apply simp apply simp apply(subgoal_tac "q < length ss") prefer 2 apply simp apply (frule nth_merges [of q _ _ "step p (ss!p)"]) (* fixme: why does method subst not work?? *) apply assumption apply clarify apply (rule conjI) apply (blast dest: boundedD) apply (erule pres_typeD) prefer 3 apply assumption apply simp apply simp apply (drule_tac P = "\x. (a, b) \ set (step q x)" in subst) apply assumption apply (simp add: plusplus_empty) apply (cases "q \ w") apply simp apply (rule ub1') apply (rule Semilat.intro) apply (rule semilat) apply clarify apply (rule pres_typeD) apply assumption prefer 3 apply assumption apply (blast intro: listE_nth_in dest: boundedD) apply (blast intro: pres_typeD dest: boundedD) apply (blast intro: listE_nth_in dest: boundedD) apply assumption apply simp apply (erule allE, erule impE, assumption, erule impE, assumption) apply (rule order_trans) apply simp defer apply (rule pp_ub2)(* apply assumption*) apply simp apply clarify apply simp apply (rule pres_typeD) apply assumption prefer 3 apply assumption apply (blast intro: listE_nth_in dest: boundedD) apply (blast intro: pres_typeD dest: boundedD) apply (blast intro: listE_nth_in dest: boundedD) apply blast done (*>*) lemma (in Semilat) merges_bounded_lemma: "\ mono r step n A; bounded step n; \(p',s') \ set (step p (ss!p)). s' \ A; ss \ list n A; ts \ list n A; p < n; ss [\\<^sub>r] ts; \p. p < n \ stable r step ts p \ \ merges f (step p (ss!p)) ss [\\<^sub>r] ts" (*<*) apply (unfold stable_def) apply (rule merges_pres_le_ub) apply simp apply simp prefer 2 apply assumption apply clarsimp apply (drule boundedD, assumption+) apply (erule allE, erule impE, assumption) apply (drule bspec, assumption) apply simp apply (drule monoD [of _ _ _ _ p "ss!p" "ts!p"]) apply assumption apply simp apply (simp add: le_listD) apply (drule lesub_step_typeD, assumption) apply clarify apply (drule bspec, assumption) apply simp apply (blast intro: order_trans) done (*>*) lemma termination_lemma: assumes "Semilat A r f" shows "\ ss \ list n A; \(q,t)\set qs. q t\A; p\w \ \ ss [\\<^sub>r] merges f qs ss \ merges f qs ss = ss \ {q. \t. (q,t)\set qs \ t \\<^bsub>f\<^esub> ss!q \ ss!q} \ (w-{p}) \ w" (*<*) (is "PROP ?P") proof - interpret Semilat A r f by fact show "PROP ?P" apply(insert semilat) apply (unfold lesssub_def) apply (simp (no_asm_simp) add: merges_incr) apply (rule impI) apply (rule merges_same_conv [THEN iffD1, elim_format]) apply assumption+ defer apply (rule sym, assumption) defer apply simp apply (subgoal_tac "\q t. \((q, t) \ set qs \ t \\<^bsub>f\<^esub> ss ! q \ ss ! q)") apply (blast intro!: psubsetI elim: equalityE) apply clarsimp apply (drule bspec, assumption) apply (drule bspec, assumption) apply clarsimp done qed (*>*) +(*for lex*) +lemma ne_lesssub_iff [simp]: "y\x \ x [\\<^sub>r] y \ x [\\<^sub>r] y" + by (meson lesssub_def) + lemma iter_properties[rule_format]: assumes "Semilat A r f" shows "\ acc r; pres_type step n A; mono r step n A; bounded step n; \p\w0. p < n; ss0 \ list n A; \p w0 \ stable r step ss0 p \ \ iter f step ss0 w0 = (ss',w') \ ss' \ list n A \ stables r step ss' \ ss0 [\\<^sub>r] ss' \ (\ts\list n A. ss0 [\\<^sub>r] ts \ stables r step ts \ ss' [\\<^sub>r] ts)" (*<*) (is "PROP ?P") proof - interpret Semilat A r f by fact show "PROP ?P" apply(insert semilat) apply (unfold iter_def stables_def) apply (rule_tac P = "\(ss,w). ss \ list n A \ (\p w \ stable r step ss p) \ ss0 [\\<^sub>r] ss \ (\ts\list n A. ss0 [\\<^sub>r] ts \ stables r step ts \ ss [\\<^sub>r] ts) \ (\p\w. p < n)" and r = "{(ss',ss) . ss [\\<^sub>r] ss'} <*lex*> finite_psubset" in while_rule) \ \Invariant holds initially:\ apply (simp add:stables_def) \ \Invariant is preserved:\ apply(simp add: stables_def split_paired_all) apply(rename_tac ss w) apply(subgoal_tac "(SOME p. p \ w) \ w") prefer 2 apply (fast intro: someI) apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ w))). q < length ss \ t \ A") prefer 2 apply clarify apply (rule conjI) apply(clarsimp, blast dest!: boundedD) apply (erule pres_typeD) prefer 3 apply assumption apply (erule listE_nth_in) apply blast apply blast apply (subst decomp_propa) apply blast apply simp apply (rule conjI) apply (rule merges_preserves_type) apply blast apply clarify apply (rule conjI) apply(clarsimp, blast dest!: boundedD) apply (erule pres_typeD) prefer 3 apply assumption apply (erule listE_nth_in) apply blast apply blast apply (rule conjI) apply clarify apply (blast intro!: stable_pres_lemma) apply (rule conjI) apply (blast intro!: merges_incr intro: le_list_trans) apply (rule conjI) apply clarsimp apply (blast intro!: merges_bounded_lemma) apply (blast dest!: boundedD) \ \Postcondition holds upon termination:\ apply(clarsimp simp add: stables_def split_paired_all) \ \Well-foundedness of the termination relation:\ apply (rule wf_lex_prod) apply (insert orderI [THEN acc_le_listI]) apply (simp only: acc_def lesssub_def) apply (rule wf_finite_psubset) \ \Loop decreases along termination relation:\ apply(simp add: stables_def split_paired_all) apply(rename_tac ss w) apply(subgoal_tac "(SOME p. p \ w) \ w") prefer 2 apply (fast intro: someI) apply(subgoal_tac "\(q,t) \ set (step (SOME p. p \ w) (ss ! (SOME p. p \ w))). q < length ss \ t \ A") prefer 2 apply clarify apply (rule conjI) apply(clarsimp, blast dest!: boundedD) apply (erule pres_typeD) prefer 3 apply assumption apply (erule listE_nth_in) apply blast apply blast apply (subst decomp_propa) apply blast apply clarify apply (simp del: listE_length add: lex_prod_def finite_psubset_def bounded_nat_set_is_finite) apply (rule termination_lemma) apply (rule assms) apply assumption+ defer apply assumption apply clarsimp done qed (*>*) lemma kildall_properties: assumes "Semilat A r f" shows "\ acc r; pres_type step n A; mono r step n A; bounded step n; ss0 \ list n A \ \ kildall r f step ss0 \ list n A \ stables r step (kildall r f step ss0) \ ss0 [\\<^sub>r] kildall r f step ss0 \ (\ts\list n A. ss0 [\\<^sub>r] ts \ stables r step ts \ kildall r f step ss0 [\\<^sub>r] ts)" (*<*) (is "PROP ?P") proof - interpret Semilat A r f by fact show "PROP ?P" apply (unfold kildall_def) apply(case_tac "iter f step ss0 (unstables r step ss0)") apply(simp) apply (rule iter_properties) apply (simp_all add: unstables_def stable_def) apply (rule Semilat.intro) apply (rule semilat) done qed lemma is_bcv_kildall: assumes "Semilat A r f" shows "\ acc r; top r T; pres_type step n A; bounded step n; mono r step n A \ \ is_bcv r T step n A (kildall r f step)" (is "PROP ?P") proof - interpret Semilat A r f by fact show "PROP ?P" apply(unfold is_bcv_def wt_step_def) apply(insert \Semilat A r f\ semilat kildall_properties[of A]) apply(simp add:stables_def) apply clarify apply(subgoal_tac "kildall r f step \s\<^sub>0 \ list n A") prefer 2 apply (simp(no_asm_simp)) apply (rule iffI) apply (rule_tac x = "kildall r f step \s\<^sub>0" in bexI) apply (rule conjI) apply (blast) apply (simp (no_asm_simp)) apply(assumption) apply clarify apply(subgoal_tac "kildall r f step \s\<^sub>0!p <=_r \s!p") apply simp apply (blast intro!: le_listD less_lengthI) done qed (*>*) end