# Theory Prelim

theory Prelim
imports Set_Algebras
```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

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]

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"

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)"

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 same_length_eq_append:
"length as = length bs ⟹ as@cs = bs@ds ⟹ as = bs"
by (induct as bs rule: list_induct2) auto

lemma count_list_append:
"count_list (xs@ys) a = count_list xs a + count_list ys a"
by (induct xs) auto

lemma count_list_snoc:
"count_list (xs@[x]) y = (if y=x then Suc (count_list xs y) else count_list xs y)"
by (induct xs) 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

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

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

"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 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

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

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 ‹Dual ordering›

context ordering
begin

abbreviation greater_eq  :: "'a⇒'a⇒bool" (infix "≽" 50)
where "greater_eq a b ≡ less_eq b a"
abbreviation greater  :: "'a⇒'a⇒bool" (infix "≻" 50)
where "greater a b ≡ less b a"

lemma dual: "ordering greater_eq greater"
using strict_iff_order refl antisym trans by unfold_locales fastforce

end (* context ordering *)

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 (
intro_locales, rule OrderingSetMap.axioms(2), rule assms(1), unfold_locales
)
from assms(2)
show  "⋀a b. a ∈ P ⟹ b ∈ P ⟹ a ❙≤ b ⟹ less_eq'' ((g ∘ f) a) ((g ∘ f) b)"
using ordsetmap OrderingSetMap.ordsetmap[OF assms(1)]
by    force
qed

lemma subset: "Q⊆P ⟹ OrderingSetMap (❙≤) (❙<) (❙≤*) (❙<*) Q f"
using ordsetmap by unfold_locales fast

lemma dual:
"OrderingSetMap domain.greater_eq domain.greater
codomain.greater_eq codomain.greater P f"
proof (intro_locales, rule domain.dual, rule codomain.dual, unfold_locales)
from ordsetmap show "⋀a b. a∈P ⟹ b∈P ⟹ a≽b ⟹ f b ❙≤* f a" by fast
qed

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
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 domain.greater_eq domain.greater
codomain.greater_eq codomain.greater P f"
by  (
rule OrderingSetMap.isoI, rule OrderingSetMap.dual, unfold_locales,
rule inj, rule rev_ordsetmap
)

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"

lemma is_arg_min_linorderI:
"⟦ P x; ⋀y. P y ⟹ m x ≤ (m y::_::linorder) ⟧ ⟹ is_arg_min m P x"

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 fast
moreover from assms(2) have "((-) A) ` ((Pow A).⊇X) = Pow (A-X)"
by auto
ultimately
show  "ordering.simplex_like (⊆) (⊂) ( ((-) A) ` ((Pow A).⊇X))"
using simplex_like_pow
by    fastforce
qed fast

end (* theory *)
```