section ‹Preliminaries› text ‹ In this section, we establish some basic facts about natural numbers, logic, sets, functions and relations, lists, and orderings and posets, that are either not available in the HOL library or are in a form not suitable for our purposes. › theory Prelim imports Main "HOL-Library.Set_Algebras" begin declare image_cong_simp [cong del] subsection ‹Natural numbers› lemma nat_cases_2Suc [case_names 0 1 SucSuc]: assumes 0: "n = 0 ⟹ P" and 1: "n = 1 ⟹ P" and SucSuc: "⋀m. n = Suc (Suc m) ⟹ P" shows "P" proof (cases n) case (Suc m) with 1 SucSuc show ?thesis by (cases m) auto qed (simp add: 0) lemma nat_even_induct [case_names _ 0 SucSuc]: assumes even: "even n" and 0: "P 0" and SucSuc: "⋀m. even m ⟹ P m ⟹ P (Suc (Suc m))" shows "P n" proof- from assms obtain k where "n = 2*k" using evenE by auto moreover from assms have "P (2*k)" by (induct k) auto ultimately show ?thesis by fast qed lemma nat_induct_step2 [case_names 0 1 SucSuc]: assumes 0: "P 0" and 1: "P 1" and SucSuc: "⋀m. P m ⟹ P (Suc (Suc m))" shows "P n" proof (cases "even n") case True from this obtain k where "n = 2*k" using evenE by auto moreover have "P (2*k)" using 0 SucSuc by (induct k) auto ultimately show ?thesis by fast next case False from this obtain k where "n = 2*k+1" using oddE by blast moreover have "P (2*k+1)" using 1 SucSuc by (induct k) auto ultimately show ?thesis by fast qed subsection ‹Logic› lemma ex1_unique: "∃!x. P x ⟹ P a ⟹ P b ⟹ a=b" by blast lemma not_the1: assumes "∃!x. P x" "y ≠ (THE x. P x)" shows "¬ P y" using assms(2) the1_equality[OF assms(1)] by auto lemma two_cases [case_names both one other neither]: assumes both : "P ⟹ Q ⟹ R" and one : "P ⟹ ¬Q ⟹ R" and other : "¬P ⟹ Q ⟹ R" and neither: "¬P ⟹ ¬Q ⟹ R" shows "R" using assms by fast subsection ‹Sets› lemma bex1_equality: "⟦ ∃!x∈A. P x; x∈A; P x; y∈A; P y ⟧ ⟹ x=y" by blast lemma prod_ballI: "(⋀a b. (a,b)∈A ⟹ P a b) ⟹ ∀(a,b)∈A. P a b" by fast lemmas seteqI = set_eqI[OF iffI] lemma set_decomp_subset: "⟦ U = A∪B; A⊆X; B⊆Y; X⊆U; X∩Y = {} ⟧ ⟹ A = X" by auto lemma insert_subset_equality: "⟦ a∉A; a∉B; insert a A = insert a B ⟧ ⟹ A=B" by auto lemma insert_compare_element: "a∉A ⟹ insert b A = insert a A ⟹ b=a" by auto lemma card1: assumes "card A = 1" shows "∃a. A = {a}" proof- from assms obtain a where a: "a ∈ A" by fastforce with assms show ?thesis using card_ge_0_finite[of A] card_subset_eq[of A "{a}"] by auto qed lemma singleton_pow: "a∈A ⟹ {a}∈Pow A" using Pow_mono Pow_top by fast definition separated_by :: "'a set set ⇒ 'a ⇒ 'a ⇒ bool" where "separated_by w x y ≡ ∃A B. w={A,B} ∧ x∈A ∧ y∈B" lemma separated_byI: "x∈A ⟹ y∈B ⟹ separated_by {A,B} x y" using separated_by_def by fastforce lemma separated_by_disjoint: "⟦ separated_by {A,B} x y; A∩B={}; x∈A ⟧ ⟹ y∈B" unfolding separated_by_def by fast lemma separated_by_in_other: "separated_by {A,B} x y ⟹ x∉A ⟹ x∈B ∧ y∈A" unfolding separated_by_def by auto lemma separated_by_not_empty: "separated_by w x y ⟹ w≠{}" unfolding separated_by_def by fast lemma not_self_separated_by_disjoint: "A∩B={} ⟹ ¬ separated_by {A,B} x x" unfolding separated_by_def by auto subsection ‹Functions and relations› subsubsection ‹Miscellaneous› lemma cong_let: "(let x = y in f x) = f y" by simp lemma sym_sym: "sym (A×A)" by (fast intro: symI) lemma trans_sym: "trans (A×A)" by (fast intro: transI) lemma map_prod_sym: "sym A ⟹ sym (map_prod f f ` A)" using symD[of A] map_prod_def by (fast intro: symI) abbreviation restrict1 :: "('a⇒'a) ⇒ 'a set ⇒ ('a⇒'a)" where "restrict1 f A ≡ (λa. if a∈A then f a else a)" lemma restrict1_image: "B⊆A ⟹ restrict1 f A ` B = f`B" by auto subsubsection ‹Equality of functions restricted to a set› definition "fun_eq_on f g A ≡ (∀a∈A. f a = g a)" lemma fun_eq_onI: "(⋀a. a∈A ⟹ f a = g a) ⟹ fun_eq_on f g A" using fun_eq_on_def by fast lemma fun_eq_onD: "fun_eq_on f g A ⟹ a ∈ A ⟹ f a = g a" using fun_eq_on_def by fast lemma fun_eq_on_UNIV: "(fun_eq_on f g UNIV) = (f=g)" unfolding fun_eq_on_def by fast lemma fun_eq_on_subset: "fun_eq_on f g A ⟹ B⊆A ⟹ fun_eq_on f g B" unfolding fun_eq_on_def by fast lemma fun_eq_on_sym: "fun_eq_on f g A ⟹ fun_eq_on g f A" using fun_eq_onD by (fastforce intro: fun_eq_onI) lemma fun_eq_on_trans: "fun_eq_on f g A ⟹ fun_eq_on g h A ⟹ fun_eq_on f h A" using fun_eq_onD fun_eq_onD by (fastforce intro: fun_eq_onI) lemma fun_eq_on_cong: "fun_eq_on f h A ⟹ fun_eq_on g h A ⟹ fun_eq_on f g A" using fun_eq_on_trans fun_eq_on_sym by fastforce lemma fun_eq_on_im : "fun_eq_on f g A ⟹ B⊆A ⟹ f`B = g`B" using fun_eq_onD by force lemma fun_eq_on_subset_and_diff_imp_eq_on: assumes "A⊆B" "fun_eq_on f g A" "fun_eq_on f g (B-A)" shows "fun_eq_on f g B" proof (rule fun_eq_onI) fix x assume "x∈B" with assms(1) show "f x = g x" using fun_eq_onD[OF assms(2)] fun_eq_onD[OF assms(3)] by (cases "x∈A") auto qed lemma fun_eq_on_set_and_comp_imp_eq: "fun_eq_on f g A ⟹ fun_eq_on f g (-A) ⟹ f = g" using fun_eq_on_subset_and_diff_imp_eq_on[of A UNIV] by (simp add: Compl_eq_Diff_UNIV fun_eq_on_UNIV) lemma fun_eq_on_bij_betw: "fun_eq_on f g A ⟹ bij_betw f A B = bij_betw g A B" using bij_betw_cong unfolding fun_eq_on_def by fast lemma fun_eq_on_restrict1: "fun_eq_on (restrict1 f A) f A" by (auto intro: fun_eq_onI) abbreviation "fixespointwise f A ≡ fun_eq_on f id A" lemmas fixespointwiseI = fun_eq_onI [of _ _ id] lemmas fixespointwiseD = fun_eq_onD [of _ id] lemmas fixespointwise_cong = fun_eq_on_trans [of _ _ _ id] lemmas fixespointwise_subset = fun_eq_on_subset [of _ id] lemmas fixespointwise2_imp_eq_on = fun_eq_on_cong [of _ id] lemmas fixespointwise_subset_and_diff_imp_eq_on = fun_eq_on_subset_and_diff_imp_eq_on[of _ _ _ id] lemma id_fixespointwise: "fixespointwise id A" using fun_eq_on_def by fast lemma fixespointwise_im: "fixespointwise f A ⟹ B⊆A ⟹ f`B = B" by (auto simp add: fun_eq_on_im) lemma fixespointwise_comp: "fixespointwise f A ⟹ fixespointwise g A ⟹ fixespointwise (g∘f) A" unfolding fun_eq_on_def by simp lemma fixespointwise_insert: assumes "fixespointwise f A" "f ` (insert a A) = insert a A" shows "fixespointwise f (insert a A)" using assms(2) insert_compare_element[of a A "f a"] fixespointwiseD[OF assms(1)] fixespointwise_im[OF assms(1)] by (cases "a∈A") (auto intro: fixespointwiseI) lemma fixespointwise_restrict1: "fixespointwise f A ⟹ fixespointwise (restrict1 f B) A" using fixespointwiseD[of f] by (auto intro: fixespointwiseI) lemma fold_fixespointwise: "∀x∈set xs. fixespointwise (f x) A ⟹ fixespointwise (fold f xs) A" proof (induct xs) case Nil show ?case using id_fixespointwise subst[of id] by fastforce next case (Cons x xs) hence "fixespointwise (fold f xs ∘ f x) A" using fixespointwise_comp[of "f x" A "fold f xs"] by fastforce moreover have "fold f xs ∘ f x = fold f (x#xs)" by simp ultimately show ?case using subst[of _ _ "λf. fixespointwise f A"] by fast qed lemma funpower_fixespointwise: assumes "fixespointwise f A" shows "fixespointwise (f^^n) A" proof (induct n) case 0 show ?case using id_fixespointwise subst[of id] by fastforce next case (Suc m) with assms have "fixespointwise (f ∘ (f^^m)) A" using fixespointwise_comp by fast moreover have "f ∘ (f^^m) = f^^(Suc m)" by simp ultimately show ?case using subst[of _ _ "λf. fixespointwise f A"] by fast qed subsubsection ‹Injectivity, surjectivity, bijectivity, and inverses› lemma inj_on_to_singleton: assumes "inj_on f A" "f`A = {b}" shows "∃a. A = {a}" proof- from assms(2) obtain a where a: "a∈A" "f a = b" by force with assms have "A = {a}" using inj_onD[of f A] by blast thus ?thesis by fast qed lemmas inj_inj_on = subset_inj_on[of _ UNIV, OF _ subset_UNIV] lemma inj_on_eq_image': "⟦ inj_on f A; X⊆A; Y⊆A; f`X⊆f`Y ⟧ ⟹ X⊆Y" unfolding inj_on_def by fast lemma inj_on_eq_image: "⟦ inj_on f A; X⊆A; Y⊆A; f`X=f`Y ⟧ ⟹ X=Y" using inj_on_eq_image'[of f A X Y] inj_on_eq_image'[of f A Y X] by simp lemmas inj_eq_image = inj_on_eq_image[OF _ subset_UNIV subset_UNIV] lemma induced_pow_fun_inj_on: assumes "inj_on f A" shows "inj_on ((`) f) (Pow A)" using inj_onD[OF assms] inj_onI[of "Pow A" "(`) f"] by blast lemma inj_on_minus_set: "inj_on ((-) A) (Pow A)" by (fast intro: inj_onI) lemma induced_pow_fun_surj: "((`) f) ` (Pow A) = Pow (f`A)" proof (rule seteqI) fix X show "X ∈ ((`) f) ` (Pow A) ⟹ X ∈ Pow (f`A)" by fast next fix Y assume Y: "Y ∈ Pow (f`A)" moreover hence "Y = f`{a∈A. f a ∈ Y}" by fast ultimately show "Y∈ ((`) f) ` (Pow A)" by auto qed lemma bij_betw_f_the_inv_into_f: "bij_betw f A B ⟹ y∈B ⟹ f (the_inv_into A f y) = y" ― ‹an equivalent lemma appears in the HOL library, but this version avoids the double @{const bij_betw} premises› unfolding bij_betw_def by (blast intro: f_the_inv_into_f) lemma bij_betw_the_inv_into_onto: "bij_betw f A B ⟹ the_inv_into A f ` B = A" unfolding bij_betw_def by force lemma bij_betw_imp_bij_betw_Pow: assumes "bij_betw f A B" shows "bij_betw ((`) f) (Pow A) (Pow B)" unfolding bij_betw_def proof (rule conjI, rule inj_onI) show "⋀x y. ⟦ x∈Pow A; y∈Pow A; f`x = f`y ⟧ ⟹ x=y" using inj_onD[OF bij_betw_imp_inj_on, OF assms] by blast show "(`) f ` Pow A = Pow B" proof show "(`) f ` Pow A ⊆ Pow B" using bij_betw_imp_surj_on[OF assms] by fast show "(`) f ` Pow A ⊇ Pow B" proof fix y assume y: "y∈Pow B" with assms have "y = f ` the_inv_into A f ` y" using bij_betw_f_the_inv_into_f[THEN sym] by fastforce moreover from y assms have "the_inv_into A f ` y ⊆ A" using bij_betw_the_inv_into_onto by fastforce ultimately show "y ∈ (`) f ` Pow A" by auto qed qed qed lemma comps_fixpointwise_imp_bij_betw: assumes "f`X⊆Y" "g`Y⊆X" "fixespointwise (g∘f) X" "fixespointwise (f∘g) Y" shows "bij_betw f X Y" unfolding bij_betw_def proof show "inj_on f X" proof (rule inj_onI) fix x y show "⟦ x∈X; y∈X; f x = f y ⟧ ⟹ x=y" using fixespointwiseD[OF assms(3), of x] fixespointwiseD[OF assms(3), of y] by simp qed from assms(1,2) show "f`X = Y" using fixespointwiseD[OF assms(4)] by force qed lemma set_permutation_bij_restrict1: assumes "bij_betw f A A" shows "bij (restrict1 f A)" proof (rule bijI) have bij_f: "inj_on f A" "f`A = A" using iffD1[OF bij_betw_def, OF assms] by auto show "inj (restrict1 f A)" proof (rule injI) fix x y show "restrict1 f A x = restrict1 f A y ⟹ x=y" using inj_onD bij_f by (cases "x∈A" "y∈A" rule: two_cases) auto qed show "surj (restrict1 f A)" proof (rule surjI) fix x define y where "y ≡ restrict1 (the_inv_into A f) A x" thus "restrict1 f A y = x" using the_inv_into_into[of f] bij_f f_the_inv_into_f[of f] by (cases "x∈A") auto qed qed lemma set_permutation_the_inv_restrict1: assumes "bij_betw f A A" shows "the_inv (restrict1 f A) = restrict1 (the_inv_into A f) A" proof (rule ext, rule the_inv_into_f_eq) from assms show "inj (restrict1 f A)" using bij_is_inj set_permutation_bij_restrict1 by fast next fix a from assms show "restrict1 f A (restrict1 (the_inv_into A f) A a) = a" using bij_betw_def[of f] by (simp add: the_inv_into_into f_the_inv_into_f) qed simp lemma the_inv_into_the_inv_into: "inj_on f A ⟹ a∈A ⟹ the_inv_into (f`A) (the_inv_into A f) a = f a" using inj_on_the_inv_into by (force intro: the_inv_into_f_eq imageI) lemma the_inv_into_f_im_f_im: assumes "inj_on f A" "x⊆A" shows "the_inv_into A f ` f ` x = x" using assms(2) the_inv_into_f_f[OF assms(1)] by force lemma f_im_the_inv_into_f_im: assumes "inj_on f A" "x⊆f`A" shows "f ` the_inv_into A f ` x = x" using assms(2) f_the_inv_into_f[OF assms(1)] by force lemma the_inv_leftinv: "bij f ⟹ the_inv f ∘ f = id" using bij_def[of f] the_inv_f_f by fastforce subsubsection ‹Induced functions on sets of sets and lists of sets› text ‹ Here we create convenience abbreviations for distributing a function over a set of sets and over a list of sets. › abbreviation setsetmapim :: "('a⇒'b) ⇒ 'a set set ⇒ 'b set set" (infix "⊢" 70) where "f⊢X ≡ ((`) f) ` X" abbreviation setlistmapim :: "('a⇒'b) ⇒ 'a set list ⇒ 'b set list" (infix "⊨" 70) where "f⊨Xs ≡ map ((`) f) Xs" lemma setsetmapim_comp: "(f∘g)⊢A = f⊢(g⊢A)" by (auto simp add: image_comp) lemma setlistmapim_comp: "(f∘g)⊨xs = f⊨(g⊨xs)" by auto lemma setsetmapim_cong_subset: assumes "fun_eq_on g f (⋃A)" "B⊆A" shows "g⊢B ⊆ f⊢B" proof fix y assume "y ∈ g⊢B" from this obtain x where "x∈B" "y = g`x" by fast with assms(2) show "y ∈ f⊢B" using fun_eq_on_im[OF assms(1), of x] by fast qed lemma setsetmapim_cong: assumes "fun_eq_on g f (⋃A)" "B⊆A" shows "g⊢B = f⊢B" using setsetmapim_cong_subset[OF assms] setsetmapim_cong_subset[OF fun_eq_on_sym, OF assms] by fast lemma setsetmapim_restrict1: "B⊆A ⟹ restrict1 f (⋃A) ⊢ B = f⊢B" using setsetmapim_cong[of _ f] fun_eq_on_restrict1[of "⋃A" f] by simp lemma setsetmapim_the_inv_into: assumes "inj_on f (⋃A)" shows "(the_inv_into (⋃A) f) ⊢ (f⊢A) = A" proof (rule seteqI) fix x assume "x ∈ (the_inv_into (⋃A) f) ⊢ (f⊢A)" from this obtain y where y: "y ∈ f⊢A" "x = the_inv_into (⋃A) f ` y" by auto from y(1) obtain z where z: "z∈A" "y = f`z" by fast moreover from z(1) have "the_inv_into (⋃A) f ` f ` z = z" using the_inv_into_f_f[OF assms] by force ultimately show "x∈A" using y(2) the_inv_into_f_im_f_im[OF assms] by simp next fix x assume x: "x∈A" moreover hence "the_inv_into (⋃A) f ` f ` x = x" using the_inv_into_f_im_f_im[OF assms, of x] by fast ultimately show "x ∈ (the_inv_into (⋃A) f) ⊢ (f⊢A)" by auto qed subsubsection ‹Induced functions on quotients› text ‹ Here we construct the induced function on a quotient for an inducing function that respects the relation that defines the quotient. › lemma respects_imp_unique_image_rel: "f respects r ⟹ y∈f`r``{a} ⟹ y = f a" using congruentD[of r f] by auto lemma ex1_class_image: assumes "refl_on A r" "f respects r" "X∈A//r" shows "∃!b. b∈f`X" proof- from assms(3) obtain a where a: "a∈A" "X = r``{a}" by (auto intro: quotientE) thus ?thesis using refl_onD[OF assms(1)] ex1I[of _ "f a"] respects_imp_unique_image_rel[OF assms(2), of _ a] by force qed definition quotientfun :: "('a⇒'b) ⇒ 'a set ⇒ 'b" where "quotientfun f X = (THE b. b∈f`X)" lemma quotientfun_equality: assumes "refl_on A r" "f respects r" "X∈A//r" "b∈f`X" shows "quotientfun f X = b" unfolding quotientfun_def using assms(4) ex1_class_image[OF assms(1-3)] by (auto intro: the1_equality) lemma quotientfun_classrep_equality: "⟦ refl_on A r; f respects r; a∈A ⟧ ⟹ quotientfun f (r``{a}) = f a" using refl_onD by (fastforce intro: quotientfun_equality quotientI) subsubsection ‹Support of a function› definition supp :: "('a ⇒ 'b::zero) ⇒ 'a set" where "supp f = {x. f x ≠ 0}" lemma suppI_contra: "x ∉ supp f ⟹ f x = 0" using supp_def by fast lemma suppD_contra: "f x = 0 ⟹ x ∉ supp f" using supp_def by fast abbreviation restrict0 :: "('a⇒'b::zero) ⇒ 'a set ⇒ ('a⇒'b)" where "restrict0 f A ≡ (λa. if a ∈ A then f a else 0)" lemma supp_restrict0 : "supp (restrict0 f A) ⊆ A" proof- have "⋀a. a ∉ A ⟹ a ∉ supp (restrict0 f A)" using suppD_contra[of "restrict0 f A"] by simp thus ?thesis by fast qed subsection ‹Lists› subsubsection ‹Miscellaneous facts› lemma snoc_conv_cons: "∃x xs. ys@[y] = x#xs" by (cases ys) auto lemma cons_conv_snoc: "∃ys y. x#xs = ys@[y]" by (cases xs rule: rev_cases) auto lemma distinct_count_list: "distinct xs ⟹ count_list xs a = (if a ∈ set xs then 1 else 0)" by (induct xs) auto lemma map_fst_map_const_snd: "map fst (map (λs. (s,b)) xs) = xs" by (induct xs) auto lemma inj_on_distinct_setlistmapim: assumes "inj_on f A" shows "∀X∈set Xs. X ⊆ A ⟹ distinct Xs ⟹ distinct (f⊨Xs)" proof (induct Xs) case (Cons X Xs) show ?case proof (cases "f`X ∈ set (f⊨Xs)") case True from this obtain Y where Y: "Y∈set Xs" "f`X = f`Y" by auto with assms Y(1) Cons(2,3) show ?thesis using inj_on_eq_image[of f A X Y] by fastforce next case False with Cons show ?thesis by simp qed qed simp subsubsection ‹Cases› lemma list_cases_Cons_snoc [case_names Nil Single Cons_snoc]: assumes Nil: "xs = [] ⟹ P" and Single: "⋀x. xs = [x] ⟹ P" and Cons_snoc: "⋀x ys y. xs = x # ys @ [y] ⟹ P" shows "P" proof (cases xs, rule Nil) case (Cons x xs) with Single Cons_snoc show ?thesis by (cases xs rule: rev_cases) auto qed lemma two_lists_cases_Cons_Cons [case_names Nil1 Nil2 ConsCons]: assumes Nil1: "⋀ys. as = [] ⟹ bs = ys ⟹ P" and Nil2: "⋀xs. as = xs ⟹ bs = [] ⟹ P" and ConsCons: "⋀x xs y ys. as = x # xs ⟹ bs = y # ys ⟹ P" shows "P" proof (cases as) case Cons with assms(2,3) show ?thesis by (cases bs) auto qed (simp add: Nil1) lemma two_lists_cases_snoc_Cons [case_names Nil1 Nil2 snoc_Cons]: assumes Nil1: "⋀ys. as = [] ⟹ bs = ys ⟹ P" and Nil2: "⋀xs. as = xs ⟹ bs = [] ⟹ P" and snoc_Cons: "⋀xs x y ys. as = xs @ [x] ⟹ bs = y # ys ⟹ P" shows "P" proof (cases as rule: rev_cases) case snoc with Nil2 snoc_Cons show ?thesis by (cases bs) auto qed (simp add: Nil1) lemma two_lists_cases_snoc_Cons' [case_names both_Nil Nil1 Nil2 snoc_Cons]: assumes both_Nil: "as = [] ⟹ bs = [] ⟹ P" and Nil1: "⋀y ys. as = [] ⟹ bs = y#ys ⟹ P" and Nil2: "⋀xs x. as = xs@[x] ⟹ bs = [] ⟹ P" and snoc_Cons: "⋀xs x y ys. as = xs @ [x] ⟹ bs = y # ys ⟹ P" shows "P" proof (cases as bs rule: two_lists_cases_snoc_Cons) case (Nil1 ys) with assms(1,2) show "P" by (cases ys) auto next case (Nil2 xs) with assms(1,3) show "P" by (cases xs rule: rev_cases) auto qed (rule snoc_Cons) lemma two_prod_lists_cases_snoc_Cons: assumes "⋀xs. as = xs ⟹ bs = [] ⟹ P" "⋀ys. as = [] ⟹ bs = ys ⟹ P" "⋀xs aa ba ab bb ys. as = xs @ [(aa, ba)] ∧ bs = (ab, bb) # ys ⟹ P" shows "P" proof (rule two_lists_cases_snoc_Cons) from assms show "⋀ys. as = [] ⟹ bs = ys ⟹ P" "⋀xs. as = xs ⟹ bs = [] ⟹ P" by auto from assms(3) show "⋀xs x y ys. as = xs @ [x] ⟹ bs = y # ys ⟹ P" by fast qed lemma three_lists_cases_snoc_mid_Cons [case_names Nil1 Nil2 Nil3 snoc_single_Cons snoc_mid_Cons]: assumes Nil1: "⋀ys zs. as = [] ⟹ bs = ys ⟹ cs = zs ⟹ P" and Nil2: "⋀xs zs. as = xs ⟹ bs = [] ⟹ cs = zs ⟹ P" and Nil3: "⋀xs ys. as = xs ⟹ bs = ys ⟹ cs = [] ⟹ P" and snoc_single_Cons: "⋀xs x y z zs. as = xs @ [x] ⟹ bs = [y] ⟹ cs = z # zs ⟹ P" and snoc_mid_Cons: "⋀xs x w ys y z zs. as = xs @ [x] ⟹ bs = w # ys @ [y] ⟹ cs = z # zs ⟹ P" shows "P" proof (cases as cs rule: two_lists_cases_snoc_Cons) case Nil1 with assms(1) show "P" by simp next case Nil2 with assms(3) show "P" by simp next case snoc_Cons with Nil2 snoc_single_Cons snoc_mid_Cons show "P" by (cases bs rule: list_cases_Cons_snoc) auto qed subsubsection ‹Induction› lemma list_induct_CCons [case_names Nil Single CCons]: assumes Nil : "P []" and Single: "⋀x. P [x]" and CCons : "⋀x y xs. P (y#xs) ⟹ P (x # y # xs)" shows "P xs" proof (induct xs) case (Cons x xs) with Single CCons show ?case by (cases xs) auto qed (rule Nil) lemma list_induct_ssnoc [case_names Nil Single ssnoc]: assumes Nil : "P []" and Single: "⋀x. P [x]" and ssnoc : "⋀xs x y. P (xs@[x]) ⟹ P (xs@[x,y])" shows "P xs" proof (induct xs rule: rev_induct) case (snoc x xs) with Single ssnoc show ?case by (cases xs rule: rev_cases) auto qed (rule Nil) lemma list_induct2_snoc [case_names Nil1 Nil2 snoc]: assumes Nil1: "⋀ys. P [] ys" and Nil2: "⋀xs. P xs []" and snoc: "⋀xs x ys y. P xs ys ⟹ P (xs@[x]) (ys@[y])" shows "P xs ys" proof (induct xs arbitrary: ys rule: rev_induct, rule Nil1) case (snoc b bs) with assms(2,3) show ?case by (cases ys rule: rev_cases) auto qed lemma list_induct2_snoc_Cons [case_names Nil1 Nil2 snoc_Cons]: assumes Nil1 : "⋀ys. P [] ys" and Nil2 : "⋀xs. P xs []" and snoc_Cons: "⋀xs x y ys. P xs ys ⟹ P (xs@[x]) (y#ys)" shows "P xs ys" proof (induct ys arbitrary: xs, rule Nil2) case (Cons y ys) with Nil1 snoc_Cons show ?case by (cases xs rule: rev_cases) auto qed lemma prod_list_induct3_snoc_Conssnoc_Cons_pairwise: assumes "⋀ys zs. Q ([],ys,zs)" "⋀xs zs. Q (xs,[],zs)" "⋀xs ys. Q (xs,ys,[])" "⋀xs x y z zs. Q (xs@[x],[y],z#zs)" and step: "⋀xs x y ys w z zs. Q (xs,ys,zs) ⟹ Q (xs,ys@[w],z#zs) ⟹ Q (xs@[x],y#ys,zs) ⟹ Q (xs@[x],y#ys@[w],z#zs)" shows "Q t" proof ( induct t taking: "λ(xs,ys,zs). length xs + length ys + length zs" rule : measure_induct_rule ) case (less t) show ?case proof (cases t) case (fields xs ys zs) from assms less fields show ?thesis by (cases xs ys zs rule: three_lists_cases_snoc_mid_Cons) auto qed qed lemma list_induct3_snoc_Conssnoc_Cons_pairwise [case_names Nil1 Nil2 Nil3 snoc_single_Cons snoc_Conssnoc_Cons]: assumes Nil1 : "⋀ys zs. P [] ys zs" and Nil2 : "⋀xs zs. P xs [] zs" and Nil3 : "⋀xs ys. P xs ys []" and snoc_single_Cons : "⋀xs x y z zs. P (xs@[x]) [y] (z#zs)" and snoc_Conssnoc_Cons: "⋀xs x y ys w z zs. P xs ys zs ⟹ P xs (ys@[w]) (z#zs) ⟹ P (xs@[x]) (y#ys) zs ⟹ P (xs@[x]) (y#ys@[w]) (z#zs)" shows "P xs ys zs" using assms prod_list_induct3_snoc_Conssnoc_Cons_pairwise[of "λ(xs,ys,zs). P xs ys zs"] by auto subsubsection ‹Alternating lists› primrec alternating_list :: "nat ⇒ 'a ⇒ 'a ⇒ 'a list" where zero: "alternating_list 0 s t = []" | Suc : "alternating_list (Suc k) s t = alternating_list k s t @ [if even k then s else t]" ― ‹could be defined using Cons, but we want the alternating list to always start with the same letter as it grows, and it's easier to do that via append› lemma alternating_list2: "alternating_list 2 s t = [s,t]" using arg_cong[OF Suc_1, THEN sym, of "λn. alternating_list n s t"] by simp lemma length_alternating_list: "length (alternating_list n s t) = n" by (induct n) auto lemma alternating_list_Suc_Cons: "alternating_list (Suc k) s t = s # alternating_list k t s" by (induct k) auto lemma alternating_list_SucSuc_ConsCons: "alternating_list (Suc (Suc k)) s t = s # t # alternating_list k s t" using alternating_list_Suc_Cons[of "Suc k" s] alternating_list_Suc_Cons[of k t] by simp lemma alternating_list_alternates: "alternating_list n s t = as@[a,b,c]@bs ⟹ a=c" proof (induct n arbitrary: bs) case (Suc m) hence prevcase: "⋀xs. alternating_list m s t = as @ [a,b,c] @ xs ⟹ a = c" "alternating_list (Suc m) s t = as @ [a,b,c] @ bs" by auto show ?case proof (cases bs rule: rev_cases) case Nil show ?thesis proof (cases m) case 0 with prevcase(2) show ?thesis by simp next case (Suc k) with prevcase(2) Nil show ?thesis by (cases k) auto qed next case (snoc ds d) with prevcase show ?thesis by simp qed qed simp lemma alternating_list_split: "alternating_list (m+n) s t = alternating_list m s t @ (if even m then alternating_list n s t else alternating_list n t s)" using alternating_list_SucSuc_ConsCons[of _ s] by (induct n rule: nat_induct_step2) auto lemma alternating_list_append: "even m ⟹ alternating_list m s t @ alternating_list n s t = alternating_list (m+n) s t" "odd m ⟹ alternating_list m s t @ alternating_list n t s = alternating_list (m+n) s t" using alternating_list_split[THEN sym, of m] by auto lemma rev_alternating_list: "rev (alternating_list n s t) = (if even n then alternating_list n t s else alternating_list n s t)" using alternating_list_SucSuc_ConsCons[of _ s] by (induct n rule: nat_induct_step2) auto lemma set_alternating_list: "set (alternating_list n s t) ⊆ {s,t}" by (induct n) auto lemma set_alternating_list1: assumes "n ≥ 1" shows "s ∈ set (alternating_list n s t)" proof (cases n) case 0 with assms show ?thesis by simp next case (Suc m) thus ?thesis using alternating_list_Suc_Cons[of m s] by simp qed lemma set_alternating_list2: "n ≥ 2 ⟹ set (alternating_list n s t) = {s,t}" proof (induct n rule: nat_induct_step2) case (SucSuc m) thus ?case using set_alternating_list alternating_list_SucSuc_ConsCons[of m s t] by fastforce qed auto lemma alternating_list_in_lists: "a∈A ⟹ b∈A ⟹ alternating_list n a b ∈ lists A" by (induct n) auto subsubsection ‹Binary relation chains› text ‹Here we consider lists where each pair of adjacent elements satisfy a given relation.› fun binrelchain :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool" where "binrelchain P [] = True" | "binrelchain P [x] = True" | "binrelchain P (x # y # xs) = (P x y ∧ binrelchain P (y#xs))" lemma binrelchain_Cons_reduce: "binrelchain P (x#xs) ⟹ binrelchain P xs" by (induct xs) auto lemma binrelchain_append_reduce1: "binrelchain P (xs@ys) ⟹ binrelchain P xs" proof (induct xs rule: list_induct_CCons) case (CCons x y xs) with binrelchain_Cons_reduce show ?case by fastforce qed auto lemma binrelchain_append_reduce2: "binrelchain P (xs@ys) ⟹ binrelchain P ys" proof (induct xs) case (Cons x xs) with binrelchain_Cons_reduce show ?case by fastforce qed simp lemma binrelchain_Conssnoc_reduce: "binrelchain P (x#xs@[y]) ⟹ binrelchain P xs" using binrelchain_append_reduce1 binrelchain_Cons_reduce by fastforce lemma binrelchain_overlap_join: "binrelchain P (xs@[x]) ⟹ binrelchain P (x#ys) ⟹ binrelchain P (xs@x#ys)" by (induct xs rule: list_induct_CCons) auto lemma binrelchain_join: "⟦ binrelchain P (xs@[x]); binrelchain P (y#ys); P x y ⟧ ⟹ binrelchain P (xs @ x # y # ys)" using binrelchain_overlap_join by fastforce lemma binrelchain_snoc: "binrelchain P (xs@[x]) ⟹ P x y ⟹ binrelchain P (xs@[x,y])" using binrelchain_join by fastforce lemma binrelchain_sym_rev: assumes "⋀x y. P x y ⟹ P y x" shows "binrelchain P xs ⟹ binrelchain P (rev xs)" proof (induct xs rule: list_induct_CCons) case (CCons x y xs) with assms show ?case by (auto intro: binrelchain_snoc) qed auto lemma binrelchain_remdup_adj: "binrelchain P (xs@[x,x]@ys) ⟹ binrelchain P (xs@x#ys)" by (induct xs rule: list_induct_CCons) auto abbreviation "proper_binrelchain P xs ≡ binrelchain P xs ∧ distinct xs" lemma binrelchain_obtain_proper: "x≠y ⟹ binrelchain P (x#xs@[y]) ⟹ ∃zs. set zs ⊆ set xs ∧ length zs ≤ length xs ∧ proper_binrelchain P (x#zs@[y])" proof (induct xs arbitrary: x) case (Cons w ws) show ?case proof (cases "w=x" "w=y" rule: two_cases) case one from one(1) Cons(3) have "binrelchain P (x#ws@[y])" using binrelchain_Cons_reduce by simp with Cons(1,2) obtain zs where "set zs ⊆ set ws" "length zs ≤ length ws" "proper_binrelchain P (x#zs@[y])" by auto thus ?thesis by auto next case other with Cons(3) have "proper_binrelchain P (x#[]@[y])" using binrelchain_append_reduce1 by simp moreover have "length [] ≤ length (w#ws)" "set [] ⊆ set (w#ws)" by auto ultimately show ?thesis by blast next case neither from Cons(3) have "binrelchain P (w#ws@[y])" using binrelchain_Cons_reduce by simp with neither(2) Cons(1) obtain zs where zs: "set zs ⊆ set ws" "length zs ≤ length ws" "proper_binrelchain P (w#zs@[y])" by auto show ?thesis proof (cases "x∈set zs") case True from this obtain as bs where asbs: "zs = as@x#bs" using in_set_conv_decomp[of x] by auto with zs(3) have "proper_binrelchain P (x#bs@[y])" using binrelchain_append_reduce2[of P "w#as"] by auto moreover from zs(1) asbs have "set bs ⊆ set (w#ws)" by auto moreover from asbs zs(2) have "length bs ≤ length (w#ws)" by simp ultimately show ?thesis by auto next case False with zs(3) neither(1) Cons(2,3) have "proper_binrelchain P (x#(w#zs)@[y])" by simp moreover from zs(1) have "set (w#zs) ⊆ set (w#ws)" by auto moreover from zs(2) have "length (w#zs) ≤ length (w#ws)" by simp ultimately show ?thesis by blast qed qed (fastforce simp add: Cons(2)) qed simp lemma binrelchain_trans_Cons_snoc: assumes "⋀x y z. P x y ⟹ P y z ⟹ P x z" shows "binrelchain P (x#xs@[y]) ⟹ P x y" proof (induct xs arbitrary: x) case Cons with assms show ?case using binrelchain_Cons_reduce by auto qed simp lemma binrelchain_cong: assumes "⋀x y. P x y ⟹ Q x y" shows "binrelchain P xs ⟹ binrelchain Q xs" using assms binrelchain_Cons_reduce by (induct xs rule: list_induct_CCons) auto lemma binrelchain_funcong_Cons_snoc: assumes "⋀x y. P x y ⟹ f y = f x" "binrelchain P (x#xs@[y])" shows "f y = f x" using assms binrelchain_cong[of P] binrelchain_trans_Cons_snoc[of "λx y. f y = f x" x xs y] by auto lemma binrelchain_funcong_extra_condition_Cons_snoc: assumes "⋀x y. Q x ⟹ P x y ⟹ Q y" "⋀x y. Q x ⟹ P x y ⟹ f y = f x" shows "Q x ⟹ binrelchain P (x#zs@[y]) ⟹ f y = f x" proof (induct zs arbitrary: x) case (Cons z zs) with assms show ?case using binrelchain_Cons_reduce[of P x "z#zs@[y]"] by fastforce qed (simp add: assms) lemma binrelchain_setfuncong_Cons_snoc: "⟦ ∀x∈A. ∀y. P x y ⟶ y∈A; ∀x∈A. ∀y. P x y ⟶ f y = f x; x∈A; binrelchain P (x#zs@[y]) ⟧ ⟹ f y = f x" using binrelchain_funcong_extra_condition_Cons_snoc[of "λx. x∈A" P f x zs y] by fast lemma binrelchain_propcong_Cons_snoc: assumes "⋀x y. Q x ⟹ P x y ⟹ Q y" shows "Q x ⟹ binrelchain P (x#xs@[y]) ⟹ Q y" proof (induct xs arbitrary: x) case Cons with assms show ?case using binrelchain_Cons_reduce by auto qed (simp add: assms) subsubsection ‹Set of subseqs› lemma subseqs_Cons: "subseqs (x#xs) = map (Cons x) (subseqs xs) @ (subseqs xs)" using cong_let[of "subseqs xs" "λxss. map (Cons x) xss @ xss"] by simp abbreviation "ssubseqs xs ≡ set (subseqs xs)" lemma nil_ssubseqs: "[] ∈ ssubseqs xs" proof (induct xs) case (Cons x xs) thus ?case using subseqs_Cons[of x] by simp qed simp lemma ssubseqs_Cons: "ssubseqs (x#xs) = (Cons x) ` (ssubseqs xs) ∪ ssubseqs xs" using subseqs_Cons[of x] by simp lemma ssubseqs_refl: "xs ∈ ssubseqs xs" proof (induct xs) case (Cons x xs) thus ?case using ssubseqs_Cons by fast qed (rule nil_ssubseqs) lemma ssubseqs_subset: "as ∈ ssubseqs bs ⟹ ssubseqs as ⊆ ssubseqs bs" proof (induct bs arbitrary: as) case (Cons b bs) show ?case proof (cases "as ∈ set (subseqs bs)") case True with Cons show ?thesis using ssubseqs_Cons by fastforce next case False with Cons show ?thesis using nil_ssubseqs[of "b#bs"] ssubseqs_Cons[of "hd as"] ssubseqs_Cons[of b] by (cases as) auto qed qed simp lemma ssubseqs_lists: "as ∈ lists A ⟹ bs ∈ ssubseqs as ⟹ bs ∈ lists A" proof (induct as arbitrary: bs) case (Cons a as) thus ?case using ssubseqs_Cons[of a] by fastforce qed simp lemma delete1_ssubseqs: "as@bs ∈ ssubseqs (as@[a]@bs)" proof (induct as) case Nil show ?case using ssubseqs_refl ssubseqs_Cons[of a bs] by auto next case (Cons x xs) thus ?case using ssubseqs_Cons[of x] by simp qed lemma delete2_ssubseqs: "as@bs@cs ∈ ssubseqs (as@[a]@bs@[b]@cs)" using delete1_ssubseqs[of "as@[a]@bs"] delete1_ssubseqs ssubseqs_subset by fastforce subsection ‹Orders and posets› text ‹ We have chosen to work with the @{const ordering} locale instead of the @{class order} class to more easily facilitate simultaneously working with both an order and its dual. › subsubsection ‹Morphisms of posets› locale OrderingSetMap = domain : ordering less_eq less + codomain: ordering less_eq' less' for less_eq :: "'a⇒'a⇒bool" (infix "❙≤" 50) and less :: "'a⇒'a⇒bool" (infix "❙<" 50) and less_eq' :: "'b⇒'b⇒bool" (infix "❙≤*" 50) and less' :: "'b⇒'b⇒bool" (infix "❙<*" 50) + fixes P :: "'a set" and f :: "'a⇒'b" assumes ordsetmap: "a∈P ⟹ b∈P ⟹ a ❙≤b ⟹ f a ❙≤* f b" begin lemma comp: assumes "OrderingSetMap less_eq' less' less_eq'' less'' Q g" "f`P ⊆ Q" shows "OrderingSetMap less_eq less less_eq'' less'' P (g∘f)" proof - from assms(1) interpret I: OrderingSetMap less_eq' less' less_eq'' less'' Q g . show ?thesis by standard (use assms(2) in ‹auto intro: ordsetmap I.ordsetmap›) qed lemma subset: "Q⊆P ⟹ OrderingSetMap (❙≤) (❙<) (❙≤*) (❙<*) Q f" using ordsetmap by unfold_locales fast end (* context OrderingSetMap *) locale OrderingSetIso = OrderingSetMap less_eq less less_eq' less' P f for less_eq :: "'a⇒'a⇒bool" (infix "❙≤" 50) and less :: "'a⇒'a⇒bool" (infix "❙<" 50) and less_eq' :: "'b⇒'b⇒bool" (infix "❙≤*" 50) and less' :: "'b⇒'b⇒bool" (infix "❙<*" 50) and P :: "'a set" and f :: "'a⇒'b" + assumes inj : "inj_on f P" and rev_OrderingSetMap: "OrderingSetMap less_eq' less' less_eq less (f`P) (the_inv_into P f)" abbreviation "subset_ordering_iso ≡ OrderingSetIso (⊆) (⊂) (⊆) (⊂)" lemma (in OrderingSetMap) isoI: assumes "inj_on f P" "⋀a b. a∈P ⟹ b∈P ⟹ f a ❙≤* f b ⟹ a ❙≤b" shows "OrderingSetIso less_eq less less_eq' less' P f" using assms the_inv_into_f_f[OF assms(1)] by unfold_locales auto lemma OrderingSetIsoI_orders_greater2less: fixes f :: "'a::order ⇒ 'b::order" assumes "inj_on f P" "⋀a b. a ∈ P ⟹ b ∈ P ⟹ (b≤a) = (f a ≤ f b)" shows "OrderingSetIso (greater_eq::'a⇒'a⇒bool) (greater::'a⇒'a⇒bool) (less_eq::'b⇒'b⇒bool) (less::'b⇒'b⇒bool) P f" proof from assms(2) show "⋀a b. a ∈ P ⟹ b ∈ P ⟹ b≤a ⟹ f a ≤ f b" by auto from assms(2) show "⋀a b. a ∈ f ` P ⟹ b ∈ f ` P ⟹ b≤a ⟹ the_inv_into P f a ≤ the_inv_into P f b" using the_inv_into_f_f[OF assms(1)] by force qed (rule assms(1)) context OrderingSetIso begin lemmas ordsetmap = ordsetmap lemma ordsetmap_strict: "⟦ a∈P; b∈P; a❙<b ⟧ ⟹ f a ❙<* f b" using domain.strict_iff_order codomain.strict_iff_order ordsetmap inj inj_on_contraD by fastforce lemmas inv_ordsetmap = OrderingSetMap.ordsetmap[OF rev_OrderingSetMap] lemma rev_ordsetmap: "⟦ a∈P; b∈P; f a ❙≤* f b ⟧ ⟹ a ❙≤b" using inv_ordsetmap the_inv_into_f_f[OF inj] by fastforce lemma inv_iso: "OrderingSetIso less_eq' less' less_eq less (f`P) (the_inv_into P f)" using inv_ordsetmap inj_on_the_inv_into[OF inj] the_inv_into_onto[OF inj] ordsetmap the_inv_into_the_inv_into[OF inj] by unfold_locales auto lemmas inv_ordsetmap_strict = OrderingSetIso.ordsetmap_strict[OF inv_iso] lemma rev_ordsetmap_strict: "⟦ a∈P; b∈P; f a ❙<* f b ⟧ ⟹ a ❙<b" using inv_ordsetmap_strict the_inv_into_f_f[OF inj] by fastforce lemma iso_comp: assumes "OrderingSetIso less_eq' less' less_eq'' less'' Q g" "f`P ⊆ Q" shows "OrderingSetIso less_eq less less_eq'' less'' P (g∘f)" proof (rule OrderingSetMap.isoI) from assms show "OrderingSetMap (❙≤) (❙<) less_eq'' less'' P (g ∘ f)" using OrderingSetIso.axioms(1) comp by fast from assms(2) show "inj_on (g ∘ f) P" using OrderingSetIso.inj[OF assms(1)] comp_inj_on[OF inj, OF subset_inj_on] by fast next fix a b from assms(2) show "⟦ a∈P; b∈P; less_eq'' ((g∘f) a) ((g∘f) b) ⟧ ⟹ a❙≤b" using OrderingSetIso.rev_ordsetmap[OF assms(1)] rev_ordsetmap by force qed lemma iso_subset: "Q⊆P ⟹ OrderingSetIso (❙≤) (❙<) (❙≤*) (❙<*) Q f" using subset[of Q] subset_inj_on[OF inj] rev_ordsetmap by (blast intro: OrderingSetMap.isoI) lemma iso_dual: ‹OrderingSetIso (λa b. less_eq b a) (λa b. less b a) (λa b. less_eq' b a) (λa b. less' b a) P f› apply (rule OrderingSetMap.isoI) apply unfold_locales using inj apply (auto simp add: domain.refl codomain.refl domain.irrefl codomain.irrefl domain.order_iff_strict codomain.order_iff_strict ordsetmap_strict rev_ordsetmap_strict inj_onD intro: domain.trans codomain.trans domain.strict_trans codomain.strict_trans domain.antisym codomain.antisym) done end (* context OrderingSetIso *) lemma induced_pow_fun_subset_ordering_iso: assumes "inj_on f A" shows "subset_ordering_iso (Pow A) ((`) f)" proof show "⋀a b. a ∈ Pow A ⟹ b ∈ Pow A ⟹ a ⊆ b ⟹ f ` a ⊆ f ` b" by fast from assms show 2:"inj_on ((`) f) (Pow A)" using induced_pow_fun_inj_on by fast show "⋀a b. a ∈ (`) f ` Pow A ⟹ b ∈ (`) f ` Pow A ⟹ a ⊆ b ⟹ the_inv_into (Pow A) ((`) f) a ⊆ the_inv_into (Pow A) ((`) f) b" proof- fix Y1 Y2 assume Y: "Y1 ∈ ((`) f) ` Pow A" "Y2 ∈ ((`) f) ` Pow A" "Y1 ⊆ Y2" from Y(1,2) obtain X1 X2 where "X1⊆A" "X2⊆A" "Y1 = f`X1" "Y2 = f`X2" by auto with assms Y(3) show "the_inv_into (Pow A) ((`) f) Y1 ⊆ the_inv_into (Pow A) ((`) f) Y2" using inj_onD[OF assms] the_inv_into_f_f[OF 2, of X1] the_inv_into_f_f[OF 2, of X2] by blast qed qed subsubsection ‹More @{const arg_min}› lemma is_arg_minI: "⟦ P x; ⋀y. P y ⟹ ¬ m y < m x ⟧ ⟹ is_arg_min m P x" by (simp add: is_arg_min_def) lemma is_arg_min_linorderI: "⟦ P x; ⋀y. P y ⟹ m x ≤ (m y::_::linorder) ⟧ ⟹ is_arg_min m P x" by (simp add: is_arg_min_linorder) lemma is_arg_min_eq: "⟦ is_arg_min m P x; P z; m z = m x ⟧ ⟹ is_arg_min m P z" by (metis is_arg_min_def) lemma is_arg_minD1: "is_arg_min m P x ⟹ P x" unfolding is_arg_min_def by fast lemma is_arg_minD2: "is_arg_min m P x ⟹ P y ⟹ ¬ m y < m x" unfolding is_arg_min_def by fast lemma is_arg_min_size: fixes m :: "'a ⇒ 'b::linorder" shows "is_arg_min m P x ⟹ m x = m (arg_min m P)" by (metis arg_min_equality is_arg_min_linorder) lemma is_arg_min_size_subprop: fixes m :: "'a⇒'b::linorder" assumes "is_arg_min m P x" "Q x" "⋀y. Q y ⟹ P y" shows "m (arg_min m Q) = m (arg_min m P)" proof- have "¬ is_arg_min m Q x ⟹ ¬ is_arg_min m P x" proof assume x: "¬ is_arg_min m Q x" from assms(2,3) show False using contrapos_nn[OF x, OF is_arg_minI] is_arg_minD2[OF assms(1)] by auto qed with assms(1) show ?thesis using is_arg_min_size[of m] is_arg_min_size[of m] by fastforce qed subsubsection ‹Bottom of a set› context ordering begin definition has_bottom :: "'a set ⇒ bool" where "has_bottom P ≡ ∃z∈P. ∀x∈P. z ❙≤x" lemma has_bottomI: "z∈P ⟹ (⋀x. x∈P ⟹ z ❙≤x) ⟹ has_bottom P" using has_bottom_def by auto lemma has_uniq_bottom: "has_bottom P ⟹ ∃!z∈P. ∀x∈P. z❙≤x" using has_bottom_def antisym by force definition bottom :: "'a set ⇒ 'a" where "bottom P ≡ (THE z. z∈P ∧ (∀x∈P. z❙≤x))" lemma bottomD: assumes "has_bottom P" shows "bottom P ∈ P" "x∈P ⟹ bottom P ❙≤x" using assms has_uniq_bottom theI'[of "λz. z∈P ∧ (∀x∈P. z❙≤x)"] unfolding bottom_def by auto lemma bottomI: "z∈P ⟹ (⋀y. y∈P ⟹ z ❙≤y) ⟹ z = bottom P" using has_bottomI has_uniq_bottom the1_equality[THEN sym, of "λz. z∈P ∧ (∀x∈P. z❙≤x)"] unfolding bottom_def by simp end (* context ordering *) lemma has_bottom_pow: "order.has_bottom (Pow A)" by (fast intro: order.has_bottomI) lemma bottom_pow: "order.bottom (Pow A) = {}" proof (rule order.bottomI[THEN sym]) qed auto context OrderingSetMap begin abbreviation "dombot ≡ domain.bottom P" abbreviation "codbot ≡ codomain.bottom (f`P)" lemma im_has_bottom: "domain.has_bottom P ⟹ codomain.has_bottom (f`P)" using domain.bottomD ordsetmap by (fast intro: codomain.has_bottomI) lemma im_bottom: "domain.has_bottom P ⟹ f dombot = codbot" using domain.bottomD ordsetmap by (auto intro: codomain.bottomI) end (* context OrderingSetMap *) lemma (in OrderingSetIso) pullback_has_bottom: assumes "codomain.has_bottom (f`P)" shows "domain.has_bottom P" proof (rule domain.has_bottomI) from assms show "the_inv_into P f codbot ∈ P" using codomain.bottomD(1) the_inv_into_into[OF inj] by fast from assms show "⋀x. x∈P ⟹ the_inv_into P f codbot ❙≤x" using codomain.bottomD inv_ordsetmap[of codbot] the_inv_into_f_f[OF inj] by fastforce qed lemma (in OrderingSetIso) pullback_bottom: "⟦ domain.has_bottom P; x∈P; f x = codomain.bottom (f`P) ⟧ ⟹ x = domain.bottom P" using im_has_bottom codomain.bottomD(2) rev_ordsetmap by (auto intro: domain.bottomI) subsubsection ‹Minimal and pseudominimal elements in sets› text ‹ We will call an element of a poset pseudominimal if the only element below it is the bottom of the poset. › context ordering begin definition minimal_in :: "'a set ⇒ 'a ⇒ bool" where "minimal_in P x ≡ x∈P ∧ (∀z∈P. ¬ z ❙<x)" definition pseudominimal_in :: "'a set ⇒ 'a ⇒ bool" where "pseudominimal_in P x ≡ minimal_in (P - {bottom P}) x" ― ‹only makes sense for @{term "has_bottom P"}› lemma minimal_inD1: "minimal_in P x ⟹ x∈P" using minimal_in_def by fast lemma minimal_inD2: "minimal_in P x ⟹ z∈P ⟹ ¬ z ❙<x" using minimal_in_def by fast lemma pseudominimal_inD1: "pseudominimal_in P x ⟹ x∈P" using pseudominimal_in_def minimal_inD1 by fast lemma pseudominimal_inD2: "pseudominimal_in P x ⟹ z∈P ⟹ z❙<x ⟹ z = bottom P" using pseudominimal_in_def minimal_inD2 by fast lemma pseudominimal_inI: assumes "x∈P" "x ≠ bottom P" "⋀z. z∈P ⟹ z❙<x ⟹ z = bottom P" shows "pseudominimal_in P x" using assms unfolding pseudominimal_in_def minimal_in_def by fast lemma pseudominimal_ne_bottom: "pseudominimal_in P x ⟹ x ≠ bottom P" using pseudominimal_in_def minimal_inD1 by fast lemma pseudominimal_comp: "⟦ pseudominimal_in P x; pseudominimal_in P y; x❙≤y ⟧ ⟹ x = y" using pseudominimal_inD1 pseudominimal_inD2 pseudominimal_ne_bottom strict_iff_order[of x y] by force end (* context ordering *) lemma pseudominimal_in_pow: assumes "order.pseudominimal_in (Pow A) x" shows "∃a∈A. x = {a}" proof- from assms obtain a where "{a} ⊆ x" using order.pseudominimal_ne_bottom bottom_pow[of A] by fast with assms show ?thesis using order.pseudominimal_inD1 order.pseudominimal_inD2[of _ x "{a}"] bottom_pow by fast qed lemma pseudominimal_in_pow_singleton: "a∈A ⟹ order.pseudominimal_in (Pow A) {a}" using singleton_pow bottom_pow by (fast intro: order.pseudominimal_inI) lemma no_pseudominimal_in_pow_is_empty: "(⋀x. ¬ order.pseudominimal_in (Pow A) {x}) ⟹ A = {}" using pseudominimal_in_pow_singleton by (fast intro: equals0I) lemma (in OrderingSetIso) pseudominimal_map: "domain.has_bottom P ⟹ domain.pseudominimal_in P x ⟹ codomain.pseudominimal_in (f`P) (f x)" using domain.pseudominimal_inD1 pullback_bottom domain.pseudominimal_ne_bottom rev_ordsetmap_strict domain.pseudominimal_inD2 im_bottom by (blast intro: codomain.pseudominimal_inI) lemma (in OrderingSetIso) pullback_pseudominimal_in: "⟦ domain.has_bottom P; x∈P; codomain.pseudominimal_in (f`P) (f x) ⟧ ⟹ domain.pseudominimal_in P x" using im_bottom codomain.pseudominimal_ne_bottom ordsetmap_strict codomain.pseudominimal_inD2 pullback_bottom by (blast intro: domain.pseudominimal_inI) subsubsection ‹Set of elements below another› abbreviation (in ordering) below_in :: "'a set ⇒ 'a ⇒ 'a set" (infix ".❙≤" 70) where "P.❙≤x ≡ {y∈P. y❙≤x}" abbreviation (in ord) below_in :: "'a set ⇒ 'a ⇒ 'a set" (infix ".≤" 70) where "P.≤x ≡ {y∈P. y≤x}" context ordering begin lemma below_in_refl: "x∈P ⟹ x ∈ P.❙≤x" using refl by fast lemma below_in_singleton: "x∈P ⟹ P.❙≤x ⊆ {y} ⟹ y = x" using below_in_refl by fast lemma bottom_in_below_in: "has_bottom P ⟹ x∈P ⟹ bottom P ∈ P.❙≤x" using bottomD by fast lemma below_in_singleton_is_bottom: "⟦ has_bottom P; x∈P; P.❙≤x = {x} ⟧ ⟹ x = bottom P" using bottom_in_below_in by fast lemma bottom_below_in: "has_bottom P ⟹ x∈P ⟹ bottom (P.❙≤x) = bottom P" using bottom_in_below_in by (fast intro: bottomI[THEN sym]) lemma bottom_below_in_relative: "⟦ has_bottom (P.❙≤y); x∈P; x❙≤y ⟧ ⟹ bottom (P.❙≤x) = bottom (P.❙≤y)" using bottomD trans by (blast intro: bottomI[THEN sym]) lemma has_bottom_pseudominimal_in_below_inI: assumes "has_bottom P" "x∈P" "pseudominimal_in P y" "y❙≤x" shows "pseudominimal_in (P.❙≤x) y" using assms(3,4) pseudominimal_inD1[OF assms(3)] pseudominimal_inD2[OF assms(3)] bottom_below_in[OF assms(1,2)] pseudominimal_ne_bottom by (force intro: pseudominimal_inI) lemma has_bottom_pseudominimal_in_below_in: assumes "has_bottom P" "x∈P" "pseudominimal_in (P.❙≤x) y" shows "pseudominimal_in P y" using pseudominimal_inD1[OF assms(3)] pseudominimal_inD2[OF assms(3)] pseudominimal_ne_bottom[OF assms(3)] bottom_below_in[OF assms(1,2)] strict_implies_order[of _ y] trans[of _ y x] by (force intro: pseudominimal_inI) lemma pseudominimal_in_below_in: assumes "has_bottom (P.❙≤y)" "x∈P" "x❙≤y" "pseudominimal_in (P.❙≤x) w" shows "pseudominimal_in (P.❙≤y) w" using assms(3) trans[of w x y] trans[of _ w x] strict_iff_order pseudominimal_inD1[OF assms(4)] pseudominimal_inD2[OF assms(4)] pseudominimal_ne_bottom[OF assms(4)] bottom_below_in_relative[OF assms(1-3)] by (force intro: pseudominimal_inI) lemma collect_pseudominimals_below_in_less_eq_top: assumes "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f" "f`(P.❙≤x) = Pow A" "a ⊆ {y. pseudominimal_in (P.❙≤x) y}" defines "w ≡ the_inv_into (P.❙≤x) f (⋃(f`a))" shows "w ❙≤x" proof- from assms(2,3) have "(⋃(f`a)) ∈ f`(P.❙≤x)" using pseudominimal_inD1 by fastforce with assms(4) show ?thesis using OrderingSetIso.inj[OF assms(1)] the_inv_into_into[of f "P.❙≤x"] by force qed lemma collect_pseudominimals_below_in_poset: assumes "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f" "f`(P.❙≤x) = Pow A" "a ⊆ {y. pseudominimal_in (P.❙≤x) y}" defines "w ≡ the_inv_into (P.❙≤x) f (⋃(f`a))" shows "w ∈ P" using assms(2-4) OrderingSetIso.inj[OF assms(1)] pseudominimal_inD1 the_inv_into_into[of f "P.❙≤x" "⋃(f`a)"] by force lemma collect_pseudominimals_below_in_eq: assumes "x∈P" "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f" "f`(P.❙≤x) = Pow A" "a ⊆ {y. pseudominimal_in (P.❙≤x) y}" defines w: "w ≡ the_inv_into (P.❙≤x) f (⋃(f`a))" shows "a = {y. pseudominimal_in (P.❙≤w) y}" proof from assms(3) have has_bot_ltx: "has_bottom (P.❙≤x)" using has_bottom_pow OrderingSetIso.pullback_has_bottom[OF assms(2)] by auto from assms(3,4) have Un_fa: "(⋃(f`a)) ∈ f`(P.❙≤x)" using pseudominimal_inD1 by fastforce from assms have w_le_x: "w❙≤x" and w_P: "w∈P" using collect_pseudominimals_below_in_less_eq_top collect_pseudominimals_below_in_poset by auto show "a ⊆ {y. pseudominimal_in (P.❙≤w) y}" proof fix y assume y: "y ∈ a" show "y ∈ {y. pseudominimal_in (P.❙≤w) y}" proof (rule CollectI, rule pseudominimal_inI, rule CollectI, rule conjI) from y assms(4) have y_le_x: "y ∈ P.❙≤x" using pseudominimal_inD1 by fast thus "y∈P" by simp from y w show "y ❙≤w" using y_le_x Un_fa OrderingSetIso.inv_ordsetmap[OF assms(2)] the_inv_into_f_f[OF OrderingSetIso.inj, OF assms(2), of y] by fastforce from assms(1) y assms(4) show "y ≠ bottom (P.❙≤w)" using w_P w_le_x has_bot_ltx bottom_below_in_relative pseudominimal_ne_bottom by fast next fix z assume z: "z ∈ P.❙≤w" "z❙<y" with y assms(4) have "z = bottom (P.❙≤x)" using w_le_x trans pseudominimal_inD2[ of "P.❙≤x" y z] by fast moreover from assms(1) have "bottom (P.❙≤w) = bottom (P.❙≤x)" using has_bot_ltx w_P w_le_x bottom_below_in_relative by fast ultimately show "z = bottom (P.❙≤w)" by simp qed qed show "a ⊇ {y. pseudominimal_in (P.❙≤w) y}" proof fix v assume "v ∈ {y. pseudominimal_in (P.❙≤w) y}" hence "pseudominimal_in (P.❙≤w) v" by fast moreover hence v_pm_ltx: "pseudominimal_in (P.❙≤x) v" using has_bot_ltx w_P w_le_x pseudominimal_in_below_in by fast ultimately have "f v ≤ (⋃(f`a))" using w pseudominimal_inD1[of _ v] pseudominimal_inD1[of _ v] w_le_x w_P OrderingSetIso.ordsetmap[OF assms(2), of v w] Un_fa OrderingSetIso.inj[OF assms(2)] f_the_inv_into_f by force with assms(3) obtain y where "y∈a" "f v ⊆ f y" using v_pm_ltx has_bot_ltx pseudominimal_in_pow OrderingSetIso.pseudominimal_map[OF assms(2)] by force with assms(2,4) show "v ∈ a" using v_pm_ltx pseudominimal_inD1 pseudominimal_comp[of _ v y] OrderingSetIso.rev_ordsetmap[OF assms(2), of v y] by fast qed qed end (* context ordering *) subsubsection ‹Lower bounds› context ordering begin definition lbound_of :: "'a ⇒ 'a ⇒ 'a ⇒ bool" where "lbound_of x y b ≡ b❙≤x ∧ b❙≤y" lemma lbound_ofI: "b❙≤x ⟹ b❙≤y ⟹ lbound_of x y b" using lbound_of_def by fast lemma lbound_ofD1: "lbound_of x y b ⟹ b❙≤x" using lbound_of_def by fast lemma lbound_ofD2: "lbound_of x y b ⟹ b❙≤y" using lbound_of_def by fast definition glbound_in_of :: "'a set ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool" where "glbound_in_of P x y b ≡ b∈P ∧ lbound_of x y b ∧ (∀a∈P. lbound_of x y a ⟶ a❙≤b)" lemma glbound_in_ofI: "⟦ b∈P; lbound_of x y b; ⋀a. a∈P ⟹ lbound_of x y a ⟹ a❙≤b ⟧ ⟹ glbound_in_of P x y b" using glbound_in_of_def by auto lemma glbound_in_ofD_in: "glbound_in_of P x y b ⟹ b∈P" using glbound_in_of_def by fast lemma glbound_in_ofD_lbound: "glbound_in_of P x y b ⟹ lbound_of x y b" using glbound_in_of_def by fast lemma glbound_in_ofD_glbound: "glbound_in_of P x y b ⟹ a∈P ⟹ lbound_of x y a ⟹ a❙≤b" using glbound_in_of_def by fast lemma glbound_in_of_less_eq1: "glbound_in_of P x y b ⟹ b❙≤x" using glbound_in_ofD_lbound lbound_ofD1 by fast lemma glbound_in_of_less_eq2: "glbound_in_of P x y b ⟹ b❙≤y" using glbound_in_ofD_lbound lbound_ofD2 by fast lemma pseudominimal_in_below_in_less_eq_glbound: assumes "pseudominimal_in (P.❙≤x) w" "pseudominimal_in (P.❙≤y) w" "glbound_in_of P x y b" shows "w ❙≤b" using assms lbound_ofI glbound_in_ofD_glbound pseudominimal_inD1[of "P.❙≤x"] pseudominimal_inD1[of "P.❙≤y"] by fast end (* context ordering *) subsubsection ‹Simplex-like posets› text ‹Define a poset to be simplex-like if it is isomorphic to the power set of some set.› context ordering begin definition simplex_like :: "'a set ⇒ bool" where "simplex_like P ≡ finite P ∧ (∃f A::nat set. OrderingSetIso less_eq less (⊆) (⊂) P f ∧ f`P = Pow A )" lemma simplex_likeI: assumes "finite P" "OrderingSetIso less_eq less (⊆) (⊂) P f" "f`P = Pow (A::nat set)" shows "simplex_like P" using assms simplex_like_def by auto lemma simplex_likeD_finite: "simplex_like P ⟹ finite P" using simplex_like_def by simp lemma simplex_likeD_iso: "simplex_like P ⟹ ∃f A::nat set. OrderingSetIso less_eq less (⊆) (⊂) P f ∧ f`P = Pow A" using simplex_like_def by simp lemma simplex_like_has_bottom: "simplex_like P ⟹ has_bottom P" using simplex_likeD_iso has_bottom_pow OrderingSetIso.pullback_has_bottom by fastforce lemma simplex_like_no_pseudominimal_imp_singleton: assumes "simplex_like P" "⋀x. ¬ pseudominimal_in P x" shows "∃p. P = {p}" proof- obtain f and A::"nat set" where fA: "OrderingSetIso less_eq less (⊆) (⊂) P f" "f`P = Pow A" using simplex_likeD_iso[OF assms(1)] by auto define e where e: "e ≡ {}:: nat set" with fA(2) have "e ∈ f`P" using Pow_bottom by simp from this obtain p where "p ∈ P" "f p = e" by fast have "⋀x. ¬ order.pseudominimal_in (Pow A) {x}" proof fix x::nat assume "order.pseudominimal_in (Pow A) {x}" moreover with fA(2) have "{x} ∈ f`P" using order.pseudominimal_inD1 by fastforce ultimately show False using assms fA simplex_like_has_bottom OrderingSetIso.pullback_pseudominimal_in by fastforce qed with e fA(2) show ?thesis using no_pseudominimal_in_pow_is_empty inj_on_to_singleton[OF OrderingSetIso.inj, OF fA(1)] by force qed lemma simplex_like_no_pseudominimal_in_below_in_imp_singleton: "⟦ x∈P; simplex_like (P.❙≤x); ⋀z. ¬ pseudominimal_in (P.❙≤x) z ⟧ ⟹ P.❙≤x = {x}" using simplex_like_no_pseudominimal_imp_singleton below_in_singleton[of x P] by fast lemma pseudo_simplex_like_has_bottom: "OrderingSetIso less_eq less (⊆) (⊂) P f ⟹ f`P = Pow A ⟹ has_bottom P" using has_bottom_pow OrderingSetIso.pullback_has_bottom by fastforce lemma pseudo_simplex_like_above_pseudominimal_is_top: assumes "OrderingSetIso less_eq less (⊆) (⊂) P f" "f`P = Pow A" "t∈P" "⋀x. pseudominimal_in P x ⟹ x ❙≤t" shows "f t = A" proof from assms(2,3) show "f t ⊆ A" by fast show "A ⊆ f t" proof fix a assume "a∈A" moreover with assms(2) have "{a} ∈ f`P" by simp ultimately show "a ∈ f t" using assms pseudominimal_in_pow_singleton[of a A] pseudo_simplex_like_has_bottom[of P f] OrderingSetIso.pullback_pseudominimal_in[OF assms(1)] OrderingSetIso.ordsetmap[OF assms(1), of _ t] by force qed qed lemma pseudo_simplex_like_below_in_above_pseudominimal_is_top: assumes "x∈P" "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f" "f`(P.❙≤x) = Pow A" "t ∈ P.❙≤x" "⋀y. pseudominimal_in (P.❙≤x) y ⟹ y ❙≤t" shows "t = x" using assms(1,3-5) pseudo_simplex_like_above_pseudominimal_is_top[OF assms(2)] below_in_refl[of x P] OrderingSetIso.ordsetmap[OF assms(2), of t x] inj_onD[OF OrderingSetIso.inj[OF assms(2)], of t x] by auto lemma simplex_like_below_in_above_pseudominimal_is_top: assumes "x∈P" "simplex_like (P.❙≤x)" "t ∈ P.❙≤x" "⋀y. pseudominimal_in (P.❙≤x) y ⟹ y ❙≤t" shows "t = x" using assms simplex_likeD_iso pseudo_simplex_like_below_in_above_pseudominimal_is_top[of x P _ _ t] by blast end (* context ordering *) lemma (in OrderingSetIso) simplex_like_map: assumes "domain.simplex_like P" shows "codomain.simplex_like (f`P)" proof- obtain g::"'a ⇒ nat set" and A::"nat set" where gA: "OrderingSetIso (❙≤) (❙<) (⊆) (⊂) P g" "g`P = Pow A" using domain.simplex_likeD_iso[OF assms] by auto from gA(1) inj have "OrderingSetIso (❙≤*) (❙<*) (⊆) (⊂) (f`P) (g ∘ (the_inv_into P f))" using OrderingSetIso.iso_comp[OF inv_iso] the_inv_into_onto by fast moreover from gA(2) inj have "(g ∘ (the_inv_into P f)) ` (f`P) = Pow A" using the_inv_into_onto by (auto simp add: image_comp[THEN sym]) moreover from assms have "finite (f`P)" using domain.simplex_likeD_finite by fast ultimately show ?thesis by (auto intro: codomain.simplex_likeI) qed lemma (in OrderingSetIso) pullback_simplex_like: assumes "finite P" "codomain.simplex_like (f`P)" shows "domain.simplex_like P" proof- obtain g::"'b ⇒ nat set" and A::"nat set" where gA: "OrderingSetIso (❙≤*) (❙<*) (⊆) (⊂) (f`P) g" "g`(f`P) = Pow A" using codomain.simplex_likeD_iso[OF assms(2)] by auto from assms(1) gA(2) show ?thesis using iso_comp[OF gA(1)] by (auto intro: domain.simplex_likeI simp add: image_comp) qed lemma simplex_like_pow: assumes "finite A" shows "order.simplex_like (Pow A)" proof- from assms obtain f::"'a⇒nat" where "inj_on f A" using finite_imp_inj_to_nat_seg[of A] by auto hence "subset_ordering_iso (Pow A) ((`) f)" using induced_pow_fun_subset_ordering_iso by fast with assms show ?thesis using induced_pow_fun_surj by (blast intro: order.simplex_likeI) qed subsubsection ‹The superset ordering› abbreviation "supset_has_bottom ≡ ordering.has_bottom (⊇)" abbreviation "supset_bottom ≡ ordering.bottom (⊇)" abbreviation "supset_lbound_of ≡ ordering.lbound_of (⊇)" abbreviation "supset_glbound_in_of ≡ ordering.glbound_in_of (⊇)" abbreviation "supset_simplex_like ≡ ordering.simplex_like (⊇) (⊃)" abbreviation "supset_pseudominimal_in ≡ ordering.pseudominimal_in (⊇) (⊃)" abbreviation supset_below_in :: "'a set set ⇒ 'a set ⇒ 'a set set" (infix ".⊇" 70) where "P.⊇A ≡ ordering.below_in (⊇) P A" lemma supset_poset: "ordering (⊇) (⊃)" .. lemmas supset_bottomI = ordering.bottomI [OF supset_poset] lemmas supset_pseudominimal_inI = ordering.pseudominimal_inI [OF supset_poset] lemmas supset_pseudominimal_inD1 = ordering.pseudominimal_inD1 [OF supset_poset] lemmas supset_pseudominimal_inD2 = ordering.pseudominimal_inD2 [OF supset_poset] lemmas supset_lbound_ofI = ordering.lbound_ofI [OF supset_poset] lemmas supset_lbound_of_def = ordering.lbound_of_def [OF supset_poset] lemmas supset_glbound_in_ofI = ordering.glbound_in_ofI [OF supset_poset] lemmas supset_pseudominimal_ne_bottom = ordering.pseudominimal_ne_bottom[OF supset_poset] lemmas supset_has_bottom_pseudominimal_in_below_inI = ordering.has_bottom_pseudominimal_in_below_inI[OF supset_poset] lemmas supset_has_bottom_pseudominimal_in_below_in = ordering.has_bottom_pseudominimal_in_below_in[OF supset_poset] lemma OrderingSetIso_pow_complement: "OrderingSetIso (⊇) (⊃) (⊆) (⊂) (Pow A) ((-) A)" using inj_on_minus_set by (fast intro: OrderingSetIsoI_orders_greater2less) lemma simplex_like_pow_above_in: assumes "finite A" "X⊆A" shows "supset_simplex_like ((Pow A).⊇X)" proof ( rule OrderingSetIso.pullback_simplex_like, rule OrderingSetIso.iso_subset, rule OrderingSetIso_pow_complement ) from assms(1) show "finite ((Pow A).⊇X)" by simp from assms(1) have "finite (Pow (A-X))" by