Theory Prelim
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"
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]"
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 :
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
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
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
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
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"
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
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
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
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
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