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"
― ‹an equivalent lemma appears in the HOL library, but this version avoids the double
  @{const bij_betw} premises›
  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)

lemma bij_betw_the_inv_into_onto: "bij_betw f A B ⟹ the_inv_into A f ` B = A"
  unfolding bij_betw_def by force

lemma bij_betw_imp_bij_betw_Pow:
  assumes "bij_betw f A B"
  shows   "bij_betw ((`) f) (Pow A) (Pow B)"
  unfolding bij_betw_def
proof (rule conjI, rule inj_onI)
  show "⋀x y. ⟦ x∈Pow A; y∈Pow A; f`x = f`y ⟧ ⟹ x=y"
    using inj_onD[OF bij_betw_imp_inj_on, OF assms] by blast
  show "(`) f ` Pow A = Pow B"
  proof
    show "(`) f ` Pow A ⊆ Pow B" using bij_betw_imp_surj_on[OF assms] by fast
    show "(`) f ` Pow A ⊇ Pow B"
    proof
      fix y assume y: "y∈Pow B"
      with assms have "y = f ` the_inv_into A f ` y"
        using bij_betw_f_the_inv_into_f[THEN sym] by fastforce
      moreover from y assms have "the_inv_into A f ` y ⊆ A"
        using bij_betw_the_inv_into_onto by fastforce
      ultimately show "y ∈ (`) f ` Pow A" by auto
    qed
  qed
qed

lemma comps_fixpointwise_imp_bij_betw:
  assumes "f`X⊆Y" "g`Y⊆X" "fixespointwise (g∘f) X" "fixespointwise (f∘g) Y"
  shows   "bij_betw f X Y"
  unfolding bij_betw_def
proof
  show "inj_on f X"
  proof (rule inj_onI)
    fix x y show "⟦ x∈X; y∈X; f x = f y ⟧ ⟹ x=y"
      using fixespointwiseD[OF assms(3), of x] fixespointwiseD[OF assms(3), of y]
      by    simp
  qed
  from assms(1,2) show "f`X = Y" using fixespointwiseD[OF assms(4)] by force
qed

lemma set_permutation_bij_restrict1:
  assumes "bij_betw f A A"
  shows   "bij (restrict1 f A)"
proof (rule bijI)
  have bij_f: "inj_on f A" "f`A = A" using iffD1[OF bij_betw_def, OF assms] by auto
  show "inj (restrict1 f A)"
  proof (rule injI)
    fix x y show "restrict1 f A x = restrict1 f A y ⟹ x=y"
      using inj_onD bij_f by (cases "x∈A" "y∈A" rule: two_cases) auto
  qed
  show "surj (restrict1 f A)"
  proof (rule surjI)
    fix x
    define y where "y ≡ restrict1 (the_inv_into A f) A x"
    thus "restrict1 f A y = x"
      using the_inv_into_into[of f] bij_f f_the_inv_into_f[of f] by (cases "x∈A") auto
  qed
qed

lemma set_permutation_the_inv_restrict1:
  assumes "bij_betw f A A"
  shows   "the_inv (restrict1 f A) = restrict1 (the_inv_into A f) A"
proof (rule ext, rule the_inv_into_f_eq)
  from assms show "inj (restrict1 f A)"
    using bij_is_inj set_permutation_bij_restrict1 by fast
next
  fix a from assms show  "restrict1 f A (restrict1 (the_inv_into A f) A a) = a"
    using bij_betw_def[of f] by (simp add: the_inv_into_into f_the_inv_into_f)
qed simp

lemma the_inv_into_the_inv_into:
  "inj_on f A ⟹ a∈A ⟹ the_inv_into (f`A) (the_inv_into A f) a = f a"
  using inj_on_the_inv_into by (force intro: the_inv_into_f_eq imageI)

lemma the_inv_into_f_im_f_im:
  assumes "inj_on f A" "x⊆A"
  shows   "the_inv_into A f ` f ` x = x"
  using   assms(2) the_inv_into_f_f[OF assms(1)]
  by      force

lemma f_im_the_inv_into_f_im:
  assumes "inj_on f A" "x⊆f`A"
  shows   "f ` the_inv_into A f ` x = x"
  using   assms(2) f_the_inv_into_f[OF assms(1)]
  by      force

lemma the_inv_leftinv: "bij f ⟹ the_inv f ∘ f = id"
  using bij_def[of f] the_inv_f_f by fastforce


subsubsection ‹Induced functions on sets of sets and lists of sets›

text ‹
  Here we create convenience abbreviations for distributing a function over a set of sets and over
  a list of sets.
›

abbreviation setsetmapim :: "('a⇒'b) ⇒ 'a set set ⇒ 'b set set" (infix ‹⊢› 70)
  where "f⊢X ≡ ((`) f) ` X"

abbreviation setlistmapim :: "('a⇒'b) ⇒ 'a set list ⇒ 'b set list" (infix ‹⊨› 70)
  where "f⊨Xs ≡ map ((`) f) Xs"

lemma setsetmapim_comp: "(f∘g)⊢A = f⊢(g⊢A)"
  by (auto simp add: image_comp)

lemma setlistmapim_comp: "(f∘g)⊨xs = f⊨(g⊨xs)"
  by auto

lemma setsetmapim_cong_subset:
  assumes "fun_eq_on g f (⋃A)" "B⊆A"
  shows   "g⊢B ⊆ f⊢B"
proof
  fix y assume "y ∈ g⊢B"
  from this obtain x where "x∈B" "y = g`x" by fast
  with assms(2) show "y ∈ f⊢B" using fun_eq_on_im[OF assms(1), of x] by fast
qed

lemma setsetmapim_cong: 
  assumes "fun_eq_on g f (⋃A)" "B⊆A"
  shows   "g⊢B = f⊢B"
  using   setsetmapim_cong_subset[OF assms]
          setsetmapim_cong_subset[OF fun_eq_on_sym, OF assms]
  by      fast

lemma setsetmapim_restrict1: "B⊆A ⟹ restrict1 f (⋃A) ⊢ B = f⊢B"
  using setsetmapim_cong[of _ f] fun_eq_on_restrict1[of "⋃A" f] by simp

lemma setsetmapim_the_inv_into:
  assumes "inj_on f (⋃A)"
  shows   "(the_inv_into (⋃A) f) ⊢ (f⊢A) = A"
proof (rule seteqI)
  fix x assume "x ∈ (the_inv_into (⋃A) f) ⊢ (f⊢A)"
  from this obtain y where y: "y ∈ f⊢A" "x = the_inv_into (⋃A) f ` y" by auto
  from y(1) obtain z where z: "z∈A" "y = f`z" by fast
  moreover from z(1) have "the_inv_into (⋃A) f ` f ` z = z"
    using the_inv_into_f_f[OF assms] by force
  ultimately show "x∈A" using y(2) the_inv_into_f_im_f_im[OF assms] by simp
next
  fix x assume x: "x∈A"
  moreover hence "the_inv_into (⋃A) f ` f ` x = x"
    using the_inv_into_f_im_f_im[OF assms, of x] by fast
  ultimately show "x ∈ (the_inv_into (⋃A) f) ⊢ (f⊢A)" by auto
qed


subsubsection ‹Induced functions on quotients›

text ‹
  Here we construct the induced function on a quotient for an inducing function that respects the
  relation that defines the quotient.
›

lemma respects_imp_unique_image_rel: "f respects r ⟹ y∈f`r``{a} ⟹ y = f a"
  using congruentD[of r f] by auto

lemma ex1_class_image:
  assumes "refl_on A r" "f respects r" "X∈A//r"
  shows   "∃!b. b∈f`X"
proof-
  from assms(3) obtain a where a: "a∈A" "X = r``{a}" by (auto intro: quotientE)
  thus ?thesis
    using refl_onD[OF assms(1)] ex1I[of _ "f a"]
          respects_imp_unique_image_rel[OF assms(2), of _ a]
    by    force
qed

definition quotientfun :: "('a⇒'b) ⇒ 'a set ⇒ 'b"
  where "quotientfun f X = (THE b. b∈f`X)"

lemma quotientfun_equality:
  assumes   "refl_on A r" "f respects r" "X∈A//r" "b∈f`X"
  shows     "quotientfun f X = b"
  unfolding quotientfun_def
  using     assms(4) ex1_class_image[OF assms(1-3)]
  by        (auto intro: the1_equality)

lemma quotientfun_classrep_equality:
  "⟦ refl_on A r; f respects r; a∈A ⟧ ⟹ quotientfun f (r``{a}) = f a"
  using refl_onD by (fastforce intro: quotientfun_equality quotientI)


subsubsection ‹Support of a function›

definition supp :: "('a ⇒ 'b::zero) ⇒ 'a set" where "supp f = {x. f x ≠ 0}"

lemma suppI_contra: "x ∉ supp f ⟹ f x = 0"
  using supp_def by fast

lemma suppD_contra: "f x = 0 ⟹ x ∉ supp f"
  using supp_def by fast

abbreviation restrict0 :: "('a⇒'b::zero) ⇒ 'a set ⇒ ('a⇒'b)"
  where "restrict0 f A ≡ (λa. if a ∈ A then f a else 0)"

lemma supp_restrict0 : "supp (restrict0 f A) ⊆ A"
proof-
  have "⋀a. a ∉ A ⟹ a ∉ supp (restrict0 f A)"
    using suppD_contra[of "restrict0 f A"] by simp
  thus ?thesis by fast
qed


subsection ‹Lists›


subsubsection ‹Miscellaneous facts›

lemma snoc_conv_cons: "∃x xs. ys@[y] = x#xs"
  by (cases ys) auto

lemma cons_conv_snoc: "∃ys y. x#xs = ys@[y]"
  by (cases xs rule: rev_cases) auto

lemma distinct_count_list:
  "distinct xs ⟹ count_list xs a = (if a ∈ set xs then 1 else 0)"
  by (induct xs) auto

lemma map_fst_map_const_snd: "map fst (map (λs. (s,b)) xs) = xs"
  by (induct xs) auto

lemma inj_on_distinct_setlistmapim:
  assumes "inj_on f A"
  shows "∀X∈set Xs. X ⊆ A ⟹ distinct Xs ⟹ distinct (f⊨Xs)"
proof (induct Xs)
  case (Cons X Xs)
  show ?case
  proof (cases "f`X ∈ set (f⊨Xs)")
    case True
    from this obtain Y where Y: "Y∈set Xs" "f`X = f`Y" by auto
    with assms Y(1) Cons(2,3) show ?thesis
      using inj_on_eq_image[of f A X Y] by fastforce
  next
    case False with Cons show ?thesis by simp
  qed
qed simp

subsubsection ‹Cases›

lemma list_cases_Cons_snoc [case_names Nil Single Cons_snoc]:
  assumes       Nil: "xs = [] ⟹ P"
  and        Single: "⋀x. xs = [x] ⟹ P"
  and     Cons_snoc: "⋀x ys y. xs = x # ys @ [y] ⟹ P"
  shows "P"
proof (cases xs, rule Nil)
  case (Cons x xs) with Single Cons_snoc show ?thesis
    by (cases xs rule: rev_cases) auto
qed

lemma two_lists_cases_Cons_Cons [case_names Nil1 Nil2 ConsCons]:
  assumes     Nil1: "⋀ys. as = [] ⟹ bs = ys ⟹ P"
  and         Nil2: "⋀xs. as = xs ⟹ bs = [] ⟹ P"
  and     ConsCons: "⋀x xs y ys. as = x # xs ⟹ bs = y # ys ⟹ P"
  shows "P"
proof (cases as)
  case Cons with assms(2,3) show ?thesis by (cases bs) auto
qed (simp add: Nil1)

lemma two_lists_cases_snoc_Cons [case_names Nil1 Nil2 snoc_Cons]:
  assumes      Nil1: "⋀ys. as = [] ⟹ bs = ys ⟹ P"
  and          Nil2: "⋀xs. as = xs ⟹ bs = [] ⟹ P"
  and     snoc_Cons: "⋀xs x y ys. as = xs @ [x] ⟹ bs = y # ys ⟹ P"
  shows "P"
proof (cases as rule: rev_cases)
  case snoc with Nil2 snoc_Cons show ?thesis by (cases bs) auto
qed (simp add: Nil1)

lemma two_lists_cases_snoc_Cons' [case_names both_Nil Nil1 Nil2 snoc_Cons]:
  assumes  both_Nil: "as = [] ⟹ bs = [] ⟹ P"
  and          Nil1: "⋀y ys. as = [] ⟹ bs = y#ys ⟹ P"
  and          Nil2: "⋀xs x. as = xs@[x] ⟹ bs = [] ⟹ P"
  and     snoc_Cons: "⋀xs x y ys. as = xs @ [x] ⟹ bs = y # ys ⟹ P"
  shows "P"
proof (cases as bs rule: two_lists_cases_snoc_Cons)
  case (Nil1 ys) with assms(1,2) show "P" by (cases ys) auto
next
  case (Nil2 xs) with assms(1,3) show "P" by (cases xs rule: rev_cases) auto
qed (rule snoc_Cons)

lemma two_prod_lists_cases_snoc_Cons:
  assumes "⋀xs. as = xs ⟹ bs = [] ⟹ P" "⋀ys. as = [] ⟹ bs = ys ⟹ P"
          "⋀xs aa ba ab bb ys. as = xs @ [(aa, ba)] ∧ bs = (ab, bb) # ys ⟹ P"
  shows "P"
proof (rule two_lists_cases_snoc_Cons)
  from assms
    show  "⋀ys. as = [] ⟹ bs = ys ⟹ P" "⋀xs. as = xs ⟹ bs = [] ⟹ P"
    by    auto
  from assms(3) show "⋀xs x y ys. as = xs @ [x] ⟹ bs = y # ys ⟹ P"
    by fast
qed

lemma three_lists_cases_snoc_mid_Cons
      [case_names Nil1 Nil2 Nil3 snoc_single_Cons snoc_mid_Cons]:
  assumes             Nil1: "⋀ys zs. as = [] ⟹ bs = ys ⟹ cs = zs ⟹ P"
  and                 Nil2: "⋀xs zs. as = xs ⟹ bs = [] ⟹ cs = zs ⟹ P"
  and                 Nil3: "⋀xs ys. as = xs ⟹ bs = ys ⟹ cs = [] ⟹ P"
  and     snoc_single_Cons:
    "⋀xs x y z zs. as = xs @ [x] ⟹ bs = [y] ⟹ cs = z # zs ⟹ P"
  and        snoc_mid_Cons:
    "⋀xs x w ys y z zs. as = xs @ [x] ⟹ bs = w # ys @ [y] ⟹
      cs = z # zs ⟹ P"
  shows "P"
proof (cases as cs rule: two_lists_cases_snoc_Cons)
  case Nil1 with assms(1) show "P" by simp
next
  case Nil2 with assms(3) show "P" by simp
next
  case snoc_Cons
  with Nil2 snoc_single_Cons snoc_mid_Cons show "P"
    by (cases bs rule: list_cases_Cons_snoc) auto
qed


subsubsection ‹Induction›

lemma list_induct_CCons [case_names Nil Single CCons]:
  assumes Nil   : "P []"
  and     Single: "⋀x. P [x]"
  and     CCons : "⋀x y xs. P (y#xs) ⟹ P (x # y # xs)"
  shows   "P xs"
proof (induct xs)
  case (Cons x xs) with Single CCons show ?case by (cases xs) auto
qed (rule Nil)

lemma list_induct_ssnoc [case_names Nil Single ssnoc]:
  assumes Nil   : "P []"
  and     Single: "⋀x. P [x]"
  and     ssnoc : "⋀xs x y. P (xs@[x]) ⟹ P (xs@[x,y])"
  shows   "P xs"
proof (induct xs rule: rev_induct)
  case (snoc x xs) with Single ssnoc show ?case by (cases xs rule: rev_cases) auto
qed (rule Nil)

lemma list_induct2_snoc [case_names Nil1 Nil2 snoc]:
  assumes Nil1: "⋀ys. P [] ys"
  and     Nil2: "⋀xs. P xs []"
  and     snoc: "⋀xs x ys y. P xs ys ⟹ P (xs@[x]) (ys@[y])"
  shows   "P xs ys"
proof (induct xs arbitrary: ys rule: rev_induct, rule Nil1)
  case (snoc b bs) with assms(2,3) show ?case by (cases ys rule: rev_cases) auto
qed

lemma list_induct2_snoc_Cons [case_names Nil1 Nil2 snoc_Cons]:
  assumes Nil1     : "⋀ys. P [] ys"
  and     Nil2     : "⋀xs. P xs []"
  and     snoc_Cons: "⋀xs x y ys. P xs ys ⟹ P (xs@[x]) (y#ys)"
  shows   "P xs ys"
proof (induct ys arbitrary: xs, rule Nil2)
  case (Cons y ys) with Nil1 snoc_Cons show ?case
    by (cases xs rule: rev_cases) auto
qed

lemma prod_list_induct3_snoc_Conssnoc_Cons_pairwise:
  assumes "⋀ys zs. Q ([],ys,zs)" "⋀xs zs. Q (xs,[],zs)" "⋀xs ys. Q (xs,ys,[])"
          "⋀xs x y z zs. Q (xs@[x],[y],z#zs)"
  and     step:
    "⋀xs x y ys w z zs. Q (xs,ys,zs) ⟹ Q (xs,ys@[w],z#zs) ⟹
      Q (xs@[x],y#ys,zs) ⟹ Q (xs@[x],y#ys@[w],z#zs)"
  shows   "Q t"
proof (
  induct  t
  taking: "λ(xs,ys,zs). length xs + length ys + length zs"
  rule  : measure_induct_rule
)
  case (less t)
  show ?case
  proof (cases t)
    case (fields xs ys zs) from assms less fields show ?thesis
      by (cases xs ys zs rule: three_lists_cases_snoc_mid_Cons) auto
  qed
qed

lemma list_induct3_snoc_Conssnoc_Cons_pairwise
      [case_names Nil1 Nil2 Nil3 snoc_single_Cons snoc_Conssnoc_Cons]:
  assumes Nil1              : "⋀ys zs. P [] ys zs"
  and     Nil2              : "⋀xs zs. P xs [] zs"
  and     Nil3              : "⋀xs ys. P xs ys []"
  and     snoc_single_Cons  : "⋀xs x y z zs. P (xs@[x]) [y] (z#zs)"
  and     snoc_Conssnoc_Cons:
    "⋀xs x y ys w z zs. P xs ys zs ⟹ P xs (ys@[w]) (z#zs) ⟹
      P (xs@[x]) (y#ys) zs ⟹ P (xs@[x]) (y#ys@[w]) (z#zs)"
  shows   "P xs ys zs"
  using   assms
          prod_list_induct3_snoc_Conssnoc_Cons_pairwise[of "λ(xs,ys,zs). P xs ys zs"]
  by      auto


subsubsection ‹Alternating lists›

primrec alternating_list :: "nat ⇒ 'a ⇒ 'a ⇒ 'a list"
  where zero: "alternating_list 0 s t = []"
      | Suc : "alternating_list (Suc k) s t =
                alternating_list k s t @ [if even k then s else t]"
― ‹could be defined using Cons, but we want the alternating list to always start with the same
letter as it grows, and it's easier to do that via append›

lemma alternating_list2: "alternating_list 2 s t = [s,t]"
  using arg_cong[OF Suc_1, THEN sym, of "λn. alternating_list n s t"] by simp

lemma length_alternating_list: "length (alternating_list n s t) = n"
  by (induct n) auto

lemma alternating_list_Suc_Cons:
  "alternating_list (Suc k) s t = s # alternating_list k t s"
  by (induct k) auto

lemma alternating_list_SucSuc_ConsCons:
  "alternating_list (Suc (Suc k)) s t = s # t # alternating_list k s t"
  using alternating_list_Suc_Cons[of "Suc k" s] alternating_list_Suc_Cons[of k t]
  by    simp

lemma alternating_list_alternates:
  "alternating_list n s t = as@[a,b,c]@bs ⟹ a=c"
proof (induct n arbitrary: bs)
  case (Suc m) hence prevcase:
    "⋀xs. alternating_list m s t = as @ [a,b,c] @ xs ⟹ a = c"
    "alternating_list (Suc m) s t = as @ [a,b,c] @ bs"
    by auto
  show ?case
  proof (cases bs rule: rev_cases)
    case Nil show ?thesis
    proof (cases m)
      case 0 with prevcase(2) show ?thesis by simp
    next
      case (Suc k) with prevcase(2) Nil show ?thesis by (cases k) auto
    qed
  next
    case (snoc ds d) with prevcase show ?thesis by simp
  qed      
qed simp

lemma alternating_list_split:
  "alternating_list (m+n) s t = alternating_list m s t @
    (if even m then alternating_list n s t else alternating_list n t s)"
  using alternating_list_SucSuc_ConsCons[of _ s]
  by    (induct n rule: nat_induct_step2) auto

lemma alternating_list_append:
  "even m ⟹
    alternating_list m s t @ alternating_list n s t = alternating_list (m+n) s t"
  "odd m ⟹
    alternating_list m s t @ alternating_list n t s = alternating_list (m+n) s t"
  using alternating_list_split[THEN sym, of m] by auto

lemma rev_alternating_list:
  "rev (alternating_list n s t) =
    (if even n then alternating_list n t s else alternating_list n s t)"
  using alternating_list_SucSuc_ConsCons[of _ s]
  by    (induct n rule: nat_induct_step2) auto

lemma set_alternating_list: "set (alternating_list n s t) ⊆ {s,t}"
  by (induct n) auto

lemma set_alternating_list1:
  assumes "n ≥ 1"
  shows "s ∈ set (alternating_list n s t)"
proof (cases n)
  case 0 with assms show ?thesis by simp
next
  case (Suc m) thus ?thesis using alternating_list_Suc_Cons[of m s] by simp
qed

lemma set_alternating_list2:
  "n ≥ 2 ⟹ set (alternating_list n s t) = {s,t}"
proof (induct n rule: nat_induct_step2)
  case (SucSuc m) thus ?case
    using set_alternating_list alternating_list_SucSuc_ConsCons[of m s t] by fastforce
qed auto

lemma alternating_list_in_lists: "a∈A ⟹ b∈A ⟹ alternating_list n a b ∈ lists A"
  by (induct n) auto


subsubsection ‹Binary relation chains›

text ‹Here we consider lists where each pair of adjacent elements satisfy a given relation.›

fun binrelchain :: "('a ⇒ 'a ⇒ bool) ⇒ 'a list ⇒ bool"
  where "binrelchain P []  = True"
      | "binrelchain P [x] = True"
      | "binrelchain P (x # y # xs) = (P x y ∧ binrelchain P (y#xs))"

lemma binrelchain_Cons_reduce: "binrelchain P (x#xs) ⟹ binrelchain P xs"
  by (induct xs) auto

lemma binrelchain_append_reduce1: "binrelchain P (xs@ys) ⟹ binrelchain P xs"
proof (induct xs rule: list_induct_CCons)
  case (CCons x y xs) with binrelchain_Cons_reduce show ?case by fastforce
qed auto

lemma binrelchain_append_reduce2:
  "binrelchain P (xs@ys) ⟹ binrelchain P ys"
proof (induct xs)
  case (Cons x xs) with binrelchain_Cons_reduce show ?case by fastforce
qed simp

lemma binrelchain_Conssnoc_reduce:
  "binrelchain P (x#xs@[y]) ⟹ binrelchain P xs"
  using binrelchain_append_reduce1 binrelchain_Cons_reduce by fastforce

lemma binrelchain_overlap_join:
  "binrelchain P (xs@[x]) ⟹ binrelchain P (x#ys) ⟹ binrelchain P (xs@x#ys)"
  by (induct xs rule: list_induct_CCons) auto

lemma binrelchain_join:
  "⟦ binrelchain P (xs@[x]); binrelchain P (y#ys); P x y ⟧ ⟹
    binrelchain P (xs @ x # y # ys)"
  using binrelchain_overlap_join by fastforce

lemma binrelchain_snoc:
  "binrelchain P (xs@[x]) ⟹ P x y ⟹ binrelchain P (xs@[x,y])"
  using binrelchain_join by fastforce

lemma binrelchain_sym_rev:
  assumes "⋀x y. P x y ⟹ P y x"
  shows   "binrelchain P xs ⟹ binrelchain P (rev xs)"
proof (induct xs rule: list_induct_CCons)
  case (CCons x y xs) with assms show ?case by (auto intro: binrelchain_snoc)
qed auto

lemma binrelchain_remdup_adj:
  "binrelchain P (xs@[x,x]@ys) ⟹ binrelchain P (xs@x#ys)"
  by (induct xs rule: list_induct_CCons) auto

abbreviation "proper_binrelchain P xs ≡ binrelchain P xs ∧ distinct xs"

lemma binrelchain_obtain_proper:
  "x≠y ⟹ binrelchain P (x#xs@[y]) ⟹
    ∃zs. set zs ⊆ set xs ∧ length zs ≤ length xs ∧ proper_binrelchain P (x#zs@[y])"
proof (induct xs arbitrary: x)
  case (Cons w ws)
  show ?case
  proof (cases "w=x" "w=y" rule: two_cases)
    case one
    from one(1) Cons(3) have "binrelchain P (x#ws@[y])"
      using binrelchain_Cons_reduce by simp
    with Cons(1,2) obtain zs
      where "set zs ⊆ set ws" "length zs ≤ length ws" "proper_binrelchain P (x#zs@[y])"
      by    auto
    thus ?thesis by auto
  next
    case other
    with Cons(3) have "proper_binrelchain P (x#[]@[y])"
      using binrelchain_append_reduce1 by simp
    moreover have "length [] ≤ length (w#ws)" "set [] ⊆ set (w#ws)" by auto
    ultimately show ?thesis by blast
  next
    case neither
    from Cons(3) have "binrelchain P (w#ws@[y])"
      using binrelchain_Cons_reduce by simp
    with neither(2) Cons(1) obtain zs 
      where zs: "set zs ⊆ set ws" "length zs ≤ length ws"
                "proper_binrelchain P (w#zs@[y])"
      by    auto
    show ?thesis
    proof (cases "x∈set zs")
      case True
      from this obtain as bs where asbs: "zs = as@x#bs"
        using in_set_conv_decomp[of x] by auto
      with zs(3) have "proper_binrelchain P (x#bs@[y])"
        using binrelchain_append_reduce2[of P "w#as"] by auto
      moreover from zs(1) asbs have "set bs ⊆ set (w#ws)" by auto
      moreover from asbs zs(2) have "length bs ≤ length (w#ws)" by simp
      ultimately show ?thesis by auto
    next
      case False
      with zs(3) neither(1) Cons(2,3) have "proper_binrelchain P (x#(w#zs)@[y])"
        by simp
      moreover from zs(1) have "set (w#zs) ⊆ set (w#ws)" by auto
      moreover from zs(2) have "length (w#zs) ≤ length (w#ws)" by simp
      ultimately show ?thesis by blast
    qed
  qed (fastforce simp add: Cons(2))
qed simp

lemma binrelchain_trans_Cons_snoc:
  assumes "⋀x y z. P x y ⟹ P y z ⟹ P x z"
  shows   "binrelchain P (x#xs@[y]) ⟹ P x y"
proof (induct xs arbitrary: x)
  case Cons with assms show ?case using binrelchain_Cons_reduce by auto
qed simp

lemma binrelchain_cong:
  assumes "⋀x y. P x y ⟹ Q x y"
  shows   "binrelchain P xs ⟹ binrelchain Q xs"
  using   assms binrelchain_Cons_reduce
  by      (induct xs rule: list_induct_CCons) auto

lemma binrelchain_funcong_Cons_snoc:
  assumes "⋀x y. P x y ⟹ f y = f x" "binrelchain P (x#xs@[y])"
  shows   "f y = f x"
  using   assms binrelchain_cong[of P]
          binrelchain_trans_Cons_snoc[of "λx y. f y = f x" x xs y]
  by      auto

lemma binrelchain_funcong_extra_condition_Cons_snoc:
  assumes "⋀x y. Q x ⟹ P x y ⟹ Q y" "⋀x y. Q x ⟹ P x y ⟹ f y = f x"
  shows   "Q x ⟹ binrelchain P (x#zs@[y]) ⟹ f y = f x"
proof (induct zs arbitrary: x)
  case (Cons z zs) with assms show ?case
    using binrelchain_Cons_reduce[of P x "z#zs@[y]"] by fastforce
qed (simp add: assms)

lemma binrelchain_setfuncong_Cons_snoc:
  "⟦ ∀x∈A. ∀y. P x y ⟶ y∈A; ∀x∈A. ∀y. P x y ⟶ f y = f x; x∈A;
      binrelchain P (x#zs@[y]) ⟧ ⟹ f y = f x"
  using binrelchain_funcong_extra_condition_Cons_snoc[of "λx. x∈A" P f x zs y]
  by    fast

lemma binrelchain_propcong_Cons_snoc:
  assumes "⋀x y. Q x ⟹ P x y ⟹ Q y"
  shows   "Q x ⟹ binrelchain P (x#xs@[y]) ⟹ Q y"
proof (induct xs arbitrary: x)
  case Cons with assms show ?case using binrelchain_Cons_reduce by auto
qed (simp add: assms)

subsubsection ‹Set of subseqs›

lemma subseqs_Cons: "subseqs (x#xs) = map (Cons x) (subseqs xs) @ (subseqs xs)"
  using cong_let[of "subseqs xs" "λxss. map (Cons x) xss @ xss"] by simp

abbreviation "ssubseqs xs ≡ set (subseqs xs)"

lemma nil_ssubseqs: "[] ∈ ssubseqs xs"
proof (induct xs)
  case (Cons x xs) thus ?case using subseqs_Cons[of x] by simp
qed simp

lemma ssubseqs_Cons: "ssubseqs (x#xs) = (Cons x) ` (ssubseqs xs) ∪ ssubseqs xs"
  using subseqs_Cons[of x] by simp

lemma ssubseqs_refl: "xs ∈ ssubseqs xs"
proof (induct xs)
  case (Cons x xs) thus ?case using ssubseqs_Cons by fast
qed (rule nil_ssubseqs)

lemma ssubseqs_subset: "as ∈ ssubseqs bs ⟹ ssubseqs as ⊆ ssubseqs bs"
proof (induct bs arbitrary: as)
  case (Cons b bs) show ?case
  proof (cases "as ∈ set (subseqs bs)")
    case True with Cons show ?thesis using ssubseqs_Cons by fastforce
  next
    case False with Cons show ?thesis
      using nil_ssubseqs[of "b#bs"] ssubseqs_Cons[of "hd as"] ssubseqs_Cons[of b]
      by    (cases as) auto
  qed
qed simp

lemma ssubseqs_lists:
  "as ∈ lists A ⟹ bs ∈ ssubseqs as ⟹ bs ∈ lists A"
proof (induct as arbitrary: bs)
  case (Cons a as) thus ?case using ssubseqs_Cons[of a] by fastforce
qed simp

lemma delete1_ssubseqs:
  "as@bs ∈ ssubseqs (as@[a]@bs)"
proof (induct as)
  case Nil show ?case using ssubseqs_refl ssubseqs_Cons[of a bs] by auto
next
  case (Cons x xs) thus ?case using ssubseqs_Cons[of x] by simp
qed

lemma delete2_ssubseqs:
  "as@bs@cs ∈ ssubseqs (as@[a]@bs@[b]@cs)"
  using delete1_ssubseqs[of "as@[a]@bs"] delete1_ssubseqs ssubseqs_subset
  by    fastforce



subsection ‹Orders and posets›

text ‹
  We have chosen to work with the @{const ordering} locale instead of the @{class order} class to
  more easily facilitate simultaneously working with both an order and its dual.
›

subsubsection ‹Morphisms of posets›

locale OrderingSetMap =
  domain  : ordering less_eq less
+ codomain: ordering less_eq' less' 
  for less_eq  :: "'a⇒'a⇒bool" (infix ‹❙≤›  50)
  and less     :: "'a⇒'a⇒bool" (infix ‹❙<›  50)
  and less_eq' :: "'b⇒'b⇒bool" (infix ‹❙≤*› 50)
  and less'    :: "'b⇒'b⇒bool" (infix ‹❙<*› 50)
+ fixes P :: "'a set"
  and   f :: "'a⇒'b"
  assumes ordsetmap: "a∈P ⟹ b∈P ⟹ a ❙≤ b ⟹ f a ❙≤* f b"
begin

lemma comp:
  assumes "OrderingSetMap less_eq' less' less_eq'' less'' Q g"
    "f`P ⊆ Q"
  shows   "OrderingSetMap less_eq less less_eq'' less'' P (g∘f)"
proof -
  from assms(1) interpret I: OrderingSetMap less_eq' less' less_eq'' less'' Q g .
  show ?thesis
    by standard (use assms(2) in ‹auto intro: ordsetmap I.ordsetmap›)
qed

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

end (* context OrderingSetMap *)

locale OrderingSetIso = OrderingSetMap less_eq less less_eq' less' P f
  for less_eq  :: "'a⇒'a⇒bool" (infix ‹❙≤›  50)
  and less     :: "'a⇒'a⇒bool" (infix ‹❙<›  50)
  and less_eq' :: "'b⇒'b⇒bool" (infix ‹❙≤*› 50)
  and less'    :: "'b⇒'b⇒bool" (infix ‹❙<*› 50)
  and P :: "'a set"
  and f :: "'a⇒'b"
+ assumes inj               : "inj_on f P"
  and     rev_OrderingSetMap:
    "OrderingSetMap less_eq' less' less_eq less (f`P) (the_inv_into P f)"

abbreviation "subset_ordering_iso ≡ OrderingSetIso (⊆) (⊂) (⊆) (⊂)"

lemma (in OrderingSetMap) isoI:
  assumes "inj_on f P" "⋀a b. a∈P ⟹ b∈P ⟹ f a ❙≤* f b ⟹ a ❙≤ b"
  shows   "OrderingSetIso less_eq less less_eq' less' P f"
  using   assms the_inv_into_f_f[OF assms(1)]
  by      unfold_locales auto

lemma OrderingSetIsoI_orders_greater2less:
  fixes f :: "'a::order ⇒ 'b::order"
  assumes "inj_on f P" "⋀a b. a ∈ P ⟹ b ∈ P ⟹ (b≤a) = (f a ≤ f b)"
  shows   "OrderingSetIso (greater_eq::'a⇒'a⇒bool) (greater::'a⇒'a⇒bool)
            (less_eq::'b⇒'b⇒bool) (less::'b⇒'b⇒bool) P f"
proof
  from assms(2) show "⋀a b. a ∈ P ⟹ b ∈ P ⟹ b≤a ⟹ f a ≤ f b" by auto
  from assms(2)
    show  "⋀a b. a ∈ f ` P ⟹ b ∈ f ` P ⟹ b≤a ⟹
            the_inv_into P f a ≤ the_inv_into P f b"
    using the_inv_into_f_f[OF assms(1)]
    by    force
qed (rule assms(1))


context OrderingSetIso
begin

lemmas ordsetmap = ordsetmap

lemma ordsetmap_strict: "⟦ a∈P; b∈P; a❙<b ⟧ ⟹ f a ❙<* f b"
  using domain.strict_iff_order codomain.strict_iff_order ordsetmap inj
        inj_on_contraD
  by    fastforce

lemmas inv_ordsetmap = OrderingSetMap.ordsetmap[OF rev_OrderingSetMap]

lemma rev_ordsetmap: "⟦ a∈P; b∈P; f a ❙≤* f b ⟧ ⟹ a ❙≤ b"
  using inv_ordsetmap the_inv_into_f_f[OF inj] by fastforce

lemma inv_iso: "OrderingSetIso less_eq' less' less_eq less (f`P) (the_inv_into P f)"
  using inv_ordsetmap inj_on_the_inv_into[OF inj] the_inv_into_onto[OF inj]
        ordsetmap the_inv_into_the_inv_into[OF inj]
  by    unfold_locales auto

lemmas inv_ordsetmap_strict = OrderingSetIso.ordsetmap_strict[OF inv_iso]

lemma rev_ordsetmap_strict: "⟦ a∈P; b∈P; f a ❙<* f b ⟧ ⟹ a ❙< b"
  using inv_ordsetmap_strict the_inv_into_f_f[OF inj] by fastforce

lemma iso_comp:
  assumes "OrderingSetIso less_eq' less' less_eq'' less'' Q g" "f`P ⊆ Q"
  shows   "OrderingSetIso less_eq less less_eq'' less'' P (g∘f)"
proof (rule OrderingSetMap.isoI)
  from assms show "OrderingSetMap (❙≤) (❙<) less_eq'' less'' P (g ∘ f)"
    using OrderingSetIso.axioms(1) comp by fast
  from assms(2) show "inj_on (g ∘ f) P"
    using OrderingSetIso.inj[OF assms(1)]
          comp_inj_on[OF inj, OF subset_inj_on]
    by    fast
next
  fix a b
  from assms(2) show "⟦ a∈P; b∈P; less_eq'' ((g∘f) a) ((g∘f) b) ⟧ ⟹ a❙≤b"
    using OrderingSetIso.rev_ordsetmap[OF assms(1)] rev_ordsetmap by force
qed

lemma iso_subset:
  "Q⊆P ⟹ OrderingSetIso (❙≤) (❙<) (❙≤*) (❙<*) Q f"
  using subset[of Q] subset_inj_on[OF inj] rev_ordsetmap
  by    (blast intro: OrderingSetMap.isoI)

lemma iso_dual:
  ‹OrderingSetIso (λa b. less_eq b a) (λa b. less b a)
    (λa b. less_eq' b a) (λa b. less' b a) P f›
  apply (rule OrderingSetMap.isoI)
    apply unfold_locales
  using inj
            apply (auto simp add: domain.refl codomain.refl
              domain.irrefl codomain.irrefl
              domain.order_iff_strict codomain.order_iff_strict
              ordsetmap_strict rev_ordsetmap_strict inj_onD
              intro: domain.trans codomain.trans
              domain.strict_trans codomain.strict_trans
              domain.antisym codomain.antisym)
  done

end (* context OrderingSetIso *)

lemma induced_pow_fun_subset_ordering_iso:
  assumes "inj_on f A"
  shows   "subset_ordering_iso (Pow A) ((`) f)"
proof
  show "⋀a b. a ∈ Pow A ⟹ b ∈ Pow A ⟹ a ⊆ b ⟹ f ` a ⊆ f ` b" by fast
  from assms show 2:"inj_on ((`) f) (Pow A)"
    using induced_pow_fun_inj_on by fast
  show "⋀a b. a ∈ (`) f ` Pow A ⟹ b ∈ (`) f ` Pow A ⟹ a ⊆ b
        ⟹ the_inv_into (Pow A) ((`) f) a ⊆ the_inv_into (Pow A) ((`) f) b"
  proof-
    fix Y1 Y2
    assume Y: "Y1 ∈ ((`) f) ` Pow A" "Y2 ∈ ((`) f) ` Pow A" "Y1 ⊆ Y2"
    from Y(1,2) obtain X1 X2 where "X1⊆A" "X2⊆A" "Y1 = f`X1" "Y2 = f`X2"
      by auto
    with assms Y(3)
      show  "the_inv_into (Pow A) ((`) f) Y1 ⊆ the_inv_into (Pow A) ((`) f) Y2"
      using inj_onD[OF assms] the_inv_into_f_f[OF 2, of X1]
            the_inv_into_f_f[OF 2, of X2]
      by    blast
  qed
qed

subsubsection ‹More @{const arg_min}›

lemma is_arg_minI:
  "⟦ P x; ⋀y. P y ⟹ ¬ m y < m x ⟧ ⟹ is_arg_min m P x"
by (simp add: is_arg_min_def)

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

lemma is_arg_min_eq:
  "⟦ is_arg_min m P x; P z; m z = m x ⟧ ⟹ is_arg_min m P z"
by (metis is_arg_min_def)

lemma is_arg_minD1: "is_arg_min m P x ⟹ P x"
unfolding is_arg_min_def by fast

lemma is_arg_minD2: "is_arg_min m P x ⟹ P y ⟹ ¬ m y < m x"
unfolding is_arg_min_def by fast

lemma is_arg_min_size: fixes m :: "'a ⇒ 'b::linorder"
shows "is_arg_min m P x ⟹ m x = m (arg_min m P)"
by (metis arg_min_equality is_arg_min_linorder)

lemma is_arg_min_size_subprop:
  fixes   m :: "'a⇒'b::linorder"
  assumes "is_arg_min m P x" "Q x" "⋀y. Q y ⟹ P y"
  shows   "m (arg_min m Q) = m (arg_min m P)"
proof-
  have "¬ is_arg_min m Q x ⟹ ¬ is_arg_min m P x"
  proof
    assume x: "¬ is_arg_min m Q x"
    from assms(2,3) show False
      using contrapos_nn[OF x, OF is_arg_minI] is_arg_minD2[OF assms(1)] by auto
  qed
  with assms(1) show ?thesis
    using is_arg_min_size[of m] is_arg_min_size[of m] by fastforce
qed

subsubsection ‹Bottom of a set›

context ordering
begin

definition has_bottom :: "'a set ⇒ bool"
  where "has_bottom P ≡ ∃z∈P. ∀x∈P. z ❙≤ x"

lemma has_bottomI: "z∈P ⟹ (⋀x. x∈P ⟹ z ❙≤ x) ⟹ has_bottom P"
  using has_bottom_def by auto

lemma has_uniq_bottom: "has_bottom P ⟹ ∃!z∈P. ∀x∈P. z❙≤x"
  using has_bottom_def antisym by force

definition bottom :: "'a set ⇒ 'a"
  where "bottom P ≡ (THE z. z∈P ∧ (∀x∈P. z❙≤x))"

lemma bottomD:
  assumes   "has_bottom P"
  shows     "bottom P ∈ P" "x∈P ⟹ bottom P ❙≤ x"
  using     assms has_uniq_bottom theI'[of "λz. z∈P ∧ (∀x∈P. z❙≤x)"]
  unfolding bottom_def
  by        auto

lemma bottomI: "z∈P ⟹ (⋀y. y∈P ⟹ z ❙≤ y) ⟹ z = bottom P"
  using     has_bottomI has_uniq_bottom
            the1_equality[THEN sym, of "λz. z∈P ∧ (∀x∈P. z❙≤x)"]
  unfolding bottom_def
  by        simp

end (* context ordering *)

lemma has_bottom_pow: "order.has_bottom (Pow A)"
  by (fast intro: order.has_bottomI)

lemma bottom_pow: "order.bottom (Pow A) = {}"
proof (rule order.bottomI[THEN sym]) qed auto

context OrderingSetMap
begin

abbreviation "dombot ≡ domain.bottom P"
abbreviation "codbot ≡ codomain.bottom (f`P)"

lemma im_has_bottom: "domain.has_bottom P ⟹ codomain.has_bottom (f`P)"
  using domain.bottomD ordsetmap by (fast intro: codomain.has_bottomI)

lemma im_bottom: "domain.has_bottom P ⟹ f dombot = codbot"
  using domain.bottomD ordsetmap by (auto intro: codomain.bottomI)

end (* context OrderingSetMap *)

lemma (in OrderingSetIso) pullback_has_bottom:
  assumes "codomain.has_bottom (f`P)"
  shows   "domain.has_bottom P"
proof (rule domain.has_bottomI)
  from assms show "the_inv_into P f codbot ∈ P"
    using codomain.bottomD(1) the_inv_into_into[OF inj] by fast
  from assms show "⋀x. x∈P ⟹ the_inv_into P f codbot ❙≤ x"
    using codomain.bottomD inv_ordsetmap[of codbot] the_inv_into_f_f[OF inj]
    by    fastforce
qed

lemma (in OrderingSetIso) pullback_bottom:
  "⟦ domain.has_bottom P; x∈P; f x = codomain.bottom (f`P) ⟧ ⟹
    x = domain.bottom P"
  using im_has_bottom codomain.bottomD(2) rev_ordsetmap
  by    (auto intro: domain.bottomI)

subsubsection ‹Minimal and pseudominimal elements in sets›

text ‹
  We will call an element of a poset pseudominimal if the only element below it is the bottom of
  the poset.
›

context ordering
begin

definition minimal_in :: "'a set ⇒ 'a ⇒ bool"
  where "minimal_in P x ≡ x∈P ∧ (∀z∈P. ¬ z ❙< x)"

definition pseudominimal_in :: "'a set ⇒ 'a ⇒ bool"
  where "pseudominimal_in P x ≡ minimal_in (P - {bottom P}) x"
― ‹only makes sense for @{term "has_bottom P"}›

lemma minimal_inD1: "minimal_in P x ⟹ x∈P"
  using minimal_in_def by fast

lemma minimal_inD2: "minimal_in P x ⟹ z∈P ⟹ ¬ z ❙< x"
  using minimal_in_def by fast

lemma pseudominimal_inD1: "pseudominimal_in P x ⟹ x∈P"
  using pseudominimal_in_def minimal_inD1 by fast

lemma pseudominimal_inD2:
  "pseudominimal_in P x ⟹ z∈P ⟹ z❙<x ⟹ z = bottom P"
  using pseudominimal_in_def minimal_inD2 by fast

lemma pseudominimal_inI:
  assumes   "x∈P" "x ≠ bottom P" "⋀z. z∈P ⟹ z❙<x ⟹ z = bottom P"
  shows     "pseudominimal_in P x"
  using     assms
  unfolding pseudominimal_in_def minimal_in_def
  by        fast

lemma pseudominimal_ne_bottom: "pseudominimal_in P x ⟹ x ≠ bottom P"
  using pseudominimal_in_def minimal_inD1 by fast

lemma pseudominimal_comp:
  "⟦ pseudominimal_in P x; pseudominimal_in P y; x❙≤y ⟧ ⟹ x = y"
  using pseudominimal_inD1 pseudominimal_inD2 pseudominimal_ne_bottom
        strict_iff_order[of x y]
  by    force

end (* context ordering *)

lemma pseudominimal_in_pow:
  assumes "order.pseudominimal_in (Pow A) x"
  shows "∃a∈A. x = {a}"
proof-
  from assms obtain a where "{a} ⊆ x"
    using order.pseudominimal_ne_bottom bottom_pow[of A] by fast
  with assms show ?thesis
    using order.pseudominimal_inD1 order.pseudominimal_inD2[of _ x "{a}"]
          bottom_pow
    by    fast
qed

lemma pseudominimal_in_pow_singleton:
  "a∈A ⟹ order.pseudominimal_in (Pow A) {a}"
  using singleton_pow bottom_pow by (fast intro: order.pseudominimal_inI)

lemma no_pseudominimal_in_pow_is_empty:
  "(⋀x. ¬ order.pseudominimal_in (Pow A) {x}) ⟹ A = {}"
  using pseudominimal_in_pow_singleton by (fast intro: equals0I)

lemma (in OrderingSetIso) pseudominimal_map:
  "domain.has_bottom P ⟹ domain.pseudominimal_in P x ⟹
    codomain.pseudominimal_in (f`P) (f x)"
  using domain.pseudominimal_inD1 pullback_bottom
        domain.pseudominimal_ne_bottom rev_ordsetmap_strict
        domain.pseudominimal_inD2 im_bottom
  by    (blast intro: codomain.pseudominimal_inI)

lemma (in OrderingSetIso) pullback_pseudominimal_in:
  "⟦ domain.has_bottom P; x∈P; codomain.pseudominimal_in (f`P) (f x) ⟧ ⟹
      domain.pseudominimal_in P x"
  using im_bottom codomain.pseudominimal_ne_bottom ordsetmap_strict
        codomain.pseudominimal_inD2 pullback_bottom
  by    (blast intro: domain.pseudominimal_inI)

subsubsection ‹Set of elements below another›

abbreviation (in ordering) below_in :: "'a set ⇒ 'a ⇒ 'a set" (infix ‹.❙≤› 70)
  where "P.❙≤x ≡ {y∈P. y❙≤x}"

abbreviation (in ord) below_in :: "'a set ⇒ 'a ⇒ 'a set" (infix ‹.≤› 70)
  where "P.≤x ≡ {y∈P. y≤x}"

context ordering
begin

lemma below_in_refl: "x∈P ⟹ x ∈ P.❙≤x"
  using refl by fast

lemma below_in_singleton: "x∈P ⟹ P.❙≤x ⊆ {y} ⟹ y = x"
  using below_in_refl by fast

lemma bottom_in_below_in: "has_bottom P ⟹ x∈P ⟹ bottom P ∈ P.❙≤x"
  using bottomD by fast

lemma below_in_singleton_is_bottom:
  "⟦ has_bottom P; x∈P; P.❙≤x = {x} ⟧ ⟹ x = bottom P"
  using bottom_in_below_in by fast

lemma bottom_below_in:
  "has_bottom P ⟹ x∈P ⟹ bottom (P.❙≤x) = bottom P"
  using bottom_in_below_in by (fast intro: bottomI[THEN sym])

lemma bottom_below_in_relative:
  "⟦ has_bottom (P.❙≤y); x∈P; x❙≤y ⟧ ⟹ bottom (P.❙≤x) = bottom (P.❙≤y)"
  using bottomD trans by (blast intro: bottomI[THEN sym])

lemma has_bottom_pseudominimal_in_below_inI:
  assumes "has_bottom P" "x∈P" "pseudominimal_in P y" "y❙≤x"
  shows   "pseudominimal_in (P.❙≤x) y"
  using   assms(3,4) pseudominimal_inD1[OF assms(3)]
          pseudominimal_inD2[OF assms(3)]
          bottom_below_in[OF assms(1,2)] pseudominimal_ne_bottom
  by      (force intro: pseudominimal_inI)

lemma has_bottom_pseudominimal_in_below_in:
  assumes "has_bottom P" "x∈P" "pseudominimal_in (P.❙≤x) y"
  shows   "pseudominimal_in P y"
  using   pseudominimal_inD1[OF assms(3)]
          pseudominimal_inD2[OF assms(3)]
          pseudominimal_ne_bottom[OF assms(3)]
          bottom_below_in[OF assms(1,2)]
          strict_implies_order[of _ y] trans[of _ y x]
  by      (force intro: pseudominimal_inI)

lemma pseudominimal_in_below_in:
  assumes   "has_bottom (P.❙≤y)" "x∈P" "x❙≤y" "pseudominimal_in (P.❙≤x) w"
  shows     "pseudominimal_in (P.❙≤y) w"
  using     assms(3) trans[of w x y] trans[of _ w x] strict_iff_order
            pseudominimal_inD1[OF assms(4)]
            pseudominimal_inD2[OF assms(4)]
            pseudominimal_ne_bottom[OF assms(4)]
            bottom_below_in_relative[OF assms(1-3)]
  by        (force intro: pseudominimal_inI)

lemma collect_pseudominimals_below_in_less_eq_top:
  assumes "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f"
          "f`(P.❙≤x) = Pow A" "a ⊆ {y. pseudominimal_in (P.❙≤x) y}"
  defines "w ≡ the_inv_into (P.❙≤x) f (⋃(f`a))"
  shows   "w ❙≤ x"
proof-
  from assms(2,3) have "(⋃(f`a)) ∈ f`(P.❙≤x)"
    using pseudominimal_inD1 by fastforce
  with assms(4) show ?thesis
    using OrderingSetIso.inj[OF assms(1)] the_inv_into_into[of f "P.❙≤x"] by force
qed

lemma collect_pseudominimals_below_in_poset:
  assumes   "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f"
            "f`(P.❙≤x) = Pow A"
            "a ⊆ {y. pseudominimal_in (P.❙≤x) y}"
  defines   "w ≡ the_inv_into (P.❙≤x) f (⋃(f`a))"
  shows     "w ∈ P"
  using     assms(2-4) OrderingSetIso.inj[OF assms(1)] pseudominimal_inD1
            the_inv_into_into[of f "P.❙≤x" "⋃(f`a)"]
  by        force

lemma collect_pseudominimals_below_in_eq:
  assumes "x∈P" "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f"
          "f`(P.❙≤x) = Pow A" "a ⊆ {y. pseudominimal_in (P.❙≤x) y}"
  defines w: "w ≡ the_inv_into (P.❙≤x) f (⋃(f`a))"
  shows   "a = {y. pseudominimal_in (P.❙≤w) y}"
proof
  from assms(3) have has_bot_ltx: "has_bottom (P.❙≤x)"
    using has_bottom_pow OrderingSetIso.pullback_has_bottom[OF assms(2)]
    by    auto
  from assms(3,4) have Un_fa: "(⋃(f`a)) ∈ f`(P.❙≤x)"
    using pseudominimal_inD1 by fastforce
  from assms have w_le_x: "w❙≤x" and w_P: "w∈P"
    using collect_pseudominimals_below_in_less_eq_top
          collect_pseudominimals_below_in_poset
    by    auto
  show "a ⊆ {y. pseudominimal_in (P.❙≤w) y}"
  proof
    fix y assume y: "y ∈ a"
    show "y ∈ {y. pseudominimal_in (P.❙≤w) y}"
    proof (rule CollectI, rule pseudominimal_inI, rule CollectI, rule conjI)
      from y assms(4) have y_le_x: "y ∈ P.❙≤x" using pseudominimal_inD1 by fast
      thus "y∈P" by simp
      from y w show "y ❙≤ w"
        using y_le_x Un_fa OrderingSetIso.inv_ordsetmap[OF assms(2)]
              the_inv_into_f_f[OF OrderingSetIso.inj, OF assms(2), of y]
        by    fastforce
      from assms(1) y assms(4) show "y ≠ bottom (P.❙≤w)"
        using w_P w_le_x has_bot_ltx bottom_below_in_relative
              pseudominimal_ne_bottom
        by    fast
    next
      fix z assume z: "z ∈ P.❙≤w" "z❙<y"
      with y assms(4) have "z = bottom (P.❙≤x)"
        using w_le_x trans pseudominimal_inD2[ of "P.❙≤x" y z] by fast
      moreover from assms(1) have "bottom (P.❙≤w) = bottom (P.❙≤x)"
        using has_bot_ltx w_P w_le_x bottom_below_in_relative by fast
      ultimately show "z = bottom (P.❙≤w)" by simp
    qed
  qed
  show "a ⊇ {y. pseudominimal_in (P.❙≤w) y}"
  proof
    fix v assume "v ∈ {y. pseudominimal_in (P.❙≤w) y}"
    hence "pseudominimal_in (P.❙≤w) v" by fast
    moreover hence v_pm_ltx: "pseudominimal_in (P.❙≤x) v"
      using has_bot_ltx w_P w_le_x pseudominimal_in_below_in by fast
    ultimately
      have  "f v ≤ (⋃(f`a))"
      using w pseudominimal_inD1[of _ v] pseudominimal_inD1[of _ v] w_le_x w_P
            OrderingSetIso.ordsetmap[OF assms(2), of v w] Un_fa
            OrderingSetIso.inj[OF assms(2)]
            f_the_inv_into_f
      by    force
    with assms(3) obtain y where "y∈a" "f v ⊆ f y"
      using v_pm_ltx has_bot_ltx pseudominimal_in_pow
            OrderingSetIso.pseudominimal_map[OF assms(2)]
      by    force
    with assms(2,4) show "v ∈ a"
      using v_pm_ltx pseudominimal_inD1 pseudominimal_comp[of _ v y]
            OrderingSetIso.rev_ordsetmap[OF assms(2), of v y]
      by    fast
  qed
qed

end (* context ordering *)

subsubsection ‹Lower bounds›

context ordering
begin

definition lbound_of :: "'a ⇒ 'a ⇒ 'a ⇒ bool"
  where "lbound_of x y b ≡ b❙≤x ∧ b❙≤y"

lemma lbound_ofI: "b❙≤x ⟹ b❙≤y ⟹ lbound_of x y b"
  using lbound_of_def by fast

lemma lbound_ofD1: "lbound_of x y b ⟹ b❙≤x"
  using lbound_of_def by fast

lemma lbound_ofD2: "lbound_of x y b ⟹ b❙≤y"
  using lbound_of_def by fast

definition glbound_in_of :: "'a set ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool"
  where "glbound_in_of P x y b ≡
          b∈P ∧ lbound_of x y b ∧ (∀a∈P. lbound_of x y a ⟶ a❙≤b)"

lemma glbound_in_ofI:
  "⟦ b∈P; lbound_of x y b; ⋀a. a∈P ⟹ lbound_of x y a ⟹ a❙≤b ⟧ ⟹
    glbound_in_of P x y b"
  using glbound_in_of_def by auto

lemma glbound_in_ofD_in: "glbound_in_of P x y b ⟹ b∈P"
  using glbound_in_of_def by fast

lemma glbound_in_ofD_lbound: "glbound_in_of P x y b ⟹ lbound_of x y b"
  using glbound_in_of_def by fast

lemma glbound_in_ofD_glbound:
  "glbound_in_of P x y b ⟹ a∈P ⟹ lbound_of x y a ⟹ a❙≤b"
  using glbound_in_of_def by fast

lemma glbound_in_of_less_eq1: "glbound_in_of P x y b ⟹ b❙≤x"
  using glbound_in_ofD_lbound lbound_ofD1 by fast

lemma glbound_in_of_less_eq2: "glbound_in_of P x y b ⟹ b❙≤y"
  using glbound_in_ofD_lbound lbound_ofD2 by fast

lemma pseudominimal_in_below_in_less_eq_glbound:
  assumes "pseudominimal_in (P.❙≤x) w" "pseudominimal_in (P.❙≤y) w"
          "glbound_in_of P x y b"
  shows   "w ❙≤ b"
  using assms lbound_ofI glbound_in_ofD_glbound
        pseudominimal_inD1[of "P.❙≤x"] pseudominimal_inD1[of "P.❙≤y"]
  by    fast

end (* context ordering *)

subsubsection ‹Simplex-like posets›

text ‹Define a poset to be simplex-like if it is isomorphic to the power set of some set.›

context ordering
begin

definition simplex_like :: "'a set ⇒ bool"
  where "simplex_like P ≡ finite P ∧
          (∃f A::nat set.
            OrderingSetIso less_eq less (⊆) (⊂) P f ∧ f`P = Pow A
          )"

lemma simplex_likeI:
  assumes "finite P" "OrderingSetIso less_eq less (⊆) (⊂) P f"
          "f`P = Pow (A::nat set)"
  shows   "simplex_like P"
  using assms simplex_like_def by auto

lemma simplex_likeD_finite: "simplex_like P ⟹ finite P"
  using simplex_like_def by simp

lemma simplex_likeD_iso:
  "simplex_like P ⟹
    ∃f A::nat set. OrderingSetIso less_eq less (⊆) (⊂) P f ∧ f`P = Pow A"
  using simplex_like_def by simp

lemma simplex_like_has_bottom: "simplex_like P ⟹ has_bottom P"
  using simplex_likeD_iso has_bottom_pow OrderingSetIso.pullback_has_bottom
  by    fastforce

lemma simplex_like_no_pseudominimal_imp_singleton:
  assumes "simplex_like P" "⋀x. ¬ pseudominimal_in P x"
  shows "∃p. P = {p}"
proof-
  obtain f and A::"nat set"
    where fA: "OrderingSetIso less_eq less (⊆) (⊂) P f" "f`P = Pow A"
    using simplex_likeD_iso[OF assms(1)]
    by    auto
  define e where e: "e ≡ {}:: nat set"
  with fA(2) have "e ∈ f`P" using Pow_bottom by simp
  from this obtain p where "p ∈ P" "f p = e" by fast
  have "⋀x. ¬ order.pseudominimal_in (Pow A) {x}"
  proof
    fix x::nat assume "order.pseudominimal_in (Pow A) {x}"
    moreover with fA(2) have "{x} ∈ f`P"
      using order.pseudominimal_inD1 by fastforce
    ultimately show False
      using assms fA simplex_like_has_bottom
            OrderingSetIso.pullback_pseudominimal_in
      by    fastforce
  qed
  with e fA(2) show ?thesis
    using no_pseudominimal_in_pow_is_empty
          inj_on_to_singleton[OF OrderingSetIso.inj, OF fA(1)]
    by    force
qed

lemma simplex_like_no_pseudominimal_in_below_in_imp_singleton:
  "⟦ x∈P; simplex_like (P.❙≤x); ⋀z. ¬ pseudominimal_in (P.❙≤x) z ⟧ ⟹
    P.❙≤x = {x}"
  using simplex_like_no_pseudominimal_imp_singleton below_in_singleton[of x P]
  by    fast

lemma pseudo_simplex_like_has_bottom:
  "OrderingSetIso less_eq less (⊆) (⊂) P f ⟹ f`P = Pow A ⟹
    has_bottom P"
  using has_bottom_pow OrderingSetIso.pullback_has_bottom by fastforce

lemma pseudo_simplex_like_above_pseudominimal_is_top:
  assumes "OrderingSetIso less_eq less (⊆) (⊂) P f" "f`P = Pow A" "t∈P"
          "⋀x. pseudominimal_in P x ⟹ x ❙≤ t"
  shows   "f t = A"
proof
  from assms(2,3) show "f t ⊆ A" by fast
  show "A ⊆ f t"
  proof
    fix a assume "a∈A"
    moreover with assms(2) have "{a} ∈ f`P" by simp
    ultimately show "a ∈ f t"
      using assms pseudominimal_in_pow_singleton[of a A]
            pseudo_simplex_like_has_bottom[of P f]
            OrderingSetIso.pullback_pseudominimal_in[OF assms(1)]
            OrderingSetIso.ordsetmap[OF assms(1), of _ t]
      by    force
  qed
qed

lemma pseudo_simplex_like_below_in_above_pseudominimal_is_top:
  assumes "x∈P" "OrderingSetIso less_eq less (⊆) (⊂) (P.❙≤x) f"
          "f`(P.❙≤x) = Pow A" "t ∈ P.❙≤x"
          "⋀y. pseudominimal_in (P.❙≤x) y ⟹ y ❙≤ t"
  shows   "t = x"
  using   assms(1,3-5)
          pseudo_simplex_like_above_pseudominimal_is_top[OF assms(2)]
          below_in_refl[of x P] OrderingSetIso.ordsetmap[OF assms(2), of t x]
          inj_onD[OF OrderingSetIso.inj[OF assms(2)], of t x]
  by      auto

lemma simplex_like_below_in_above_pseudominimal_is_top:
  assumes "x∈P" "simplex_like (P.❙≤x)" "t ∈ P.❙≤x"
          "⋀y. pseudominimal_in (P.❙≤x) y ⟹ y ❙≤ t"
  shows   "t = x"
  using assms simplex_likeD_iso
        pseudo_simplex_like_below_in_above_pseudominimal_is_top[of x P _ _ t]
  by    blast

end (* context ordering *)

lemma (in OrderingSetIso) simplex_like_map:
  assumes "domain.simplex_like P"
  shows   "codomain.simplex_like (f`P)"
proof-
  obtain g::"'a ⇒ nat set" and A::"nat set"
    where gA: "OrderingSetIso (❙≤) (❙<) (⊆) (⊂) P g" "g`P = Pow A"
    using domain.simplex_likeD_iso[OF assms]
    by    auto
  from gA(1) inj
    have  "OrderingSetIso (❙≤*) (❙<*) (⊆) (⊂) (f`P)
            (g ∘ (the_inv_into P f))"
    using OrderingSetIso.iso_comp[OF inv_iso] the_inv_into_onto
    by    fast
  moreover from gA(2) inj have "(g ∘ (the_inv_into P f)) ` (f`P) = Pow A"
    using the_inv_into_onto by (auto simp add: image_comp[THEN sym])
  moreover from assms have "finite (f`P)"
    using domain.simplex_likeD_finite by fast
  ultimately show ?thesis by (auto intro: codomain.simplex_likeI)
qed

lemma (in OrderingSetIso) pullback_simplex_like:
  assumes "finite P" "codomain.simplex_like (f`P)"
  shows   "domain.simplex_like P"
proof-
  obtain g::"'b ⇒ nat set" and A::"nat set"
    where gA:  "OrderingSetIso (❙≤*) (❙<*) (⊆) (⊂) (f`P) g"
               "g`(f`P) = Pow A"
    using codomain.simplex_likeD_iso[OF assms(2)]
    by    auto
  from assms(1) gA(2) show ?thesis
    using iso_comp[OF gA(1)]
    by    (auto intro: domain.simplex_likeI simp add: image_comp)
qed

lemma simplex_like_pow:
  assumes "finite A"
  shows "order.simplex_like (Pow A)"
proof-
  from assms obtain f::"'a⇒nat" where "inj_on f A"
    using finite_imp_inj_to_nat_seg[of A] by auto
  hence "subset_ordering_iso (Pow A) ((`) f)"
    using induced_pow_fun_subset_ordering_iso by fast
  with assms show ?thesis using induced_pow_fun_surj
    by (blast intro: order.simplex_likeI)
qed

subsubsection ‹The superset ordering›

abbreviation "supset_has_bottom       ≡ ordering.has_bottom       (⊇)"
abbreviation "supset_bottom           ≡ ordering.bottom           (⊇)"
abbreviation "supset_lbound_of        ≡ ordering.lbound_of        (⊇)"
abbreviation "supset_glbound_in_of    ≡ ordering.glbound_in_of    (⊇)"
abbreviation "supset_simplex_like     ≡ ordering.simplex_like     (⊇) (⊃)"
abbreviation "supset_pseudominimal_in ≡
                ordering.pseudominimal_in (⊇) (⊃)"

abbreviation supset_below_in :: "'a set set ⇒ 'a set ⇒ 'a set set" (infix ‹.⊇› 70)
  where "P.⊇A ≡ ordering.below_in (⊇) P A"

lemma supset_poset: "ordering (⊇) (⊃)" ..

lemmas supset_bottomI            = ordering.bottomI            [OF supset_poset]
lemmas supset_pseudominimal_inI  = ordering.pseudominimal_inI  [OF supset_poset]
lemmas supset_pseudominimal_inD1 = ordering.pseudominimal_inD1 [OF supset_poset]
lemmas supset_pseudominimal_inD2 = ordering.pseudominimal_inD2 [OF supset_poset]
lemmas supset_lbound_ofI         = ordering.lbound_ofI         [OF supset_poset]
lemmas supset_lbound_of_def      = ordering.lbound_of_def      [OF supset_poset]
lemmas supset_glbound_in_ofI     = ordering.glbound_in_ofI     [OF supset_poset]
lemmas supset_pseudominimal_ne_bottom =
  ordering.pseudominimal_ne_bottom[OF supset_poset]
lemmas supset_has_bottom_pseudominimal_in_below_inI =
  ordering.has_bottom_pseudominimal_in_below_inI[OF supset_poset]
lemmas supset_has_bottom_pseudominimal_in_below_in =
  ordering.has_bottom_pseudominimal_in_below_in[OF supset_poset]

lemma OrderingSetIso_pow_complement:
  "OrderingSetIso (⊇) (⊃) (⊆) (⊂) (Pow A) ((-) A)"
  using inj_on_minus_set by (fast intro: OrderingSetIsoI_orders_greater2less)

lemma simplex_like_pow_above_in:
  assumes "finite A" "X⊆A"
  shows   "supset_simplex_like ((Pow A).⊇X)"
proof (
  rule OrderingSetIso.pullback_simplex_like, rule OrderingSetIso.iso_subset,
  rule OrderingSetIso_pow_complement
)
  from assms(1) show "finite ((Pow A).⊇X)" by simp
  from assms(1) have "finite (Pow (A-X))" by 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 *)