Theory Set_Linorder

(*  Title:      Containers/Set_Linorder.thy
    Author:     Andreas Lochbihler, KIT *)

theory Set_Linorder 
imports
  Containers_Auxiliary
  Lexicographic_Order
  Extend_Partial_Order
  "HOL-Library.Cardinality"
begin

section ‹An executable linear order on sets›

subsection ‹Definition of the linear order›

subsubsection ‹Extending finite and cofinite sets›

text ‹
  Partition sets into finite and cofinite sets and distribute the rest arbitrarily such that
  complement switches between the two.
›

consts infinite_complement_partition :: "'a set set"

specification (infinite_complement_partition)
  finite_complement_partition: "finite (A :: 'a set) ⟹ A ∈ infinite_complement_partition"
  complement_partition: "¬ finite (UNIV :: 'a set)
    ⟹ (A :: 'a set) ∈ infinite_complement_partition ⟷ - A ∉ infinite_complement_partition"
proof(cases "finite (UNIV :: 'a set)")
  case False
  define Field_r where "Field_r = {𝒫 :: 'a set set. (∀C ∈ 𝒫. - C ∉ 𝒫) ∧ (∀A. finite A ⟶ A ∈ 𝒫)}"
  define r where "r = {(𝒫1, 𝒫2). 𝒫1 ⊆ 𝒫2 ∧ 𝒫1 ∈ Field_r ∧ 𝒫2 ∈ Field_r}"
  have in_Field_r [simp]: "⋀𝒫. 𝒫 ∈ Field_r ⟷ (∀C ∈ 𝒫. - C ∉ 𝒫) ∧ (∀A. finite A ⟶ A ∈ 𝒫)"
    unfolding Field_r_def by simp
  have in_r [simp]: "⋀𝒫1 𝒫2. (𝒫1, 𝒫2) ∈ r ⟷ 𝒫1 ⊆ 𝒫2 ∧ 𝒫1 ∈ Field_r ∧ 𝒫2 ∈ Field_r"
    unfolding r_def by simp
  have Field_r [simp]: "Field r = Field_r" by(auto simp add: Field_def Field_r_def)
  
  have "Partial_order r"
    by(auto simp add: Field_def r_def partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI)
  moreover have "∃ℬ ∈ Field r. ∀𝒜 ∈ ℭ. (𝒜, ℬ) ∈ r" if ℭ: "ℭ ∈ Chains r" for ℭ
  proof -
    let ?ℬ = "⋃ℭ ∪ {A. finite A}"
    have *: "?ℬ ∈ Field r" using False ℭ
      by clarsimp(safe, drule (2) ChainsD, auto 4 4 dest: Chains_Field)
    hence "⋀𝒜. 𝒜 ∈ ℭ ⟹ (𝒜, ?ℬ) ∈ r"
      using ℭ by(auto simp del: in_Field_r dest: Chains_Field)
    with * show "∃ℬ ∈ Field r. ∀𝒜 ∈ ℭ. (𝒜, ℬ) ∈ r" by blast
  qed
  ultimately have "∃𝒫 ∈ Field r. ∀𝒜 ∈ Field r. (𝒫, 𝒜) ∈ r ⟶ 𝒜 = 𝒫"
    by(rule Zorns_po_lemma)
  then obtain 𝒫 where 𝒫: "𝒫 ∈ Field r" 
    and max: "⋀𝒜. ⟦ 𝒜 ∈ Field r; (𝒫, 𝒜) ∈ r ⟧ ⟹ 𝒜 = 𝒫" by blast
  have "∀A. finite A ⟶ A ∈ 𝒫" using 𝒫 by simp
  moreover {
    fix C
    have "C ∈ 𝒫 ∨ - C ∈ 𝒫"
    proof(rule ccontr)
      assume "¬ ?thesis"
      hence C: "C ∉ 𝒫" "- C ∉ 𝒫" by simp_all
      let ?𝒜 = "insert C 𝒫"
      have *: "?𝒜 ∈ Field r" using C 𝒫 by auto
      hence "(𝒫, ?𝒜) ∈ r" using 𝒫 by auto
      with * have "?𝒜 = 𝒫" by(rule max)
      thus False using C by auto
    qed
    hence "C ∈ 𝒫 ⟷ - C ∉ 𝒫" using 𝒫 by auto }
  ultimately have "∃𝒫 :: 'a set set. (∀A. finite A ⟶ A ∈ 𝒫) ∧ (∀C. C ∈ 𝒫 ⟷ - C ∉ 𝒫)"
    by blast
  thus ?thesis by metis
qed auto

lemma not_in_complement_partition:
  "¬ finite (UNIV :: 'a set)
  ⟹ (A :: 'a set) ∉ infinite_complement_partition ⟷ - A ∈ infinite_complement_partition"
by(metis complement_partition)

lemma not_in_complement_partition_False:
  "⟦ (A :: 'a set) ∈ infinite_complement_partition; ¬ finite (UNIV :: 'a set) ⟧ 
  ⟹ - A ∈ infinite_complement_partition = False"
by(simp add: not_in_complement_partition)

lemma infinite_complement_partition_finite [simp]:
  "finite (UNIV :: 'a set) ⟹ infinite_complement_partition = (UNIV :: 'a set set)"
by(auto intro: finite_subset finite_complement_partition)

lemma Compl_eq_empty_iff: "- A = {} ⟷ A = UNIV"
by auto

subsubsection ‹A lexicographic-style order on finite subsets›

context ord begin

definition set_less_aux :: "'a set ⇒ 'a set ⇒ bool" (infix ‹⊏''› 50)
where "A ⊏' B ⟷ finite A ∧ finite B ∧ (∃y ∈ B - A. ∀z ∈ (A - B) ∪ (B - A). y ≤ z ∧ (z ≤ y ⟶ y = z))"

definition set_less_eq_aux :: "'a set ⇒ 'a set ⇒ bool" (infix ‹⊑''› 50)
where "A ⊑' B ⟷ A ∈ infinite_complement_partition ∧ A = B ∨ A ⊏' B"

lemma set_less_aux_irrefl [iff]: "¬ A ⊏' A"
by(auto simp add: set_less_aux_def)

lemma set_less_eq_aux_refl [iff]: "A ⊑' A ⟷ A ∈ infinite_complement_partition"
by(simp add: set_less_eq_aux_def)

lemma set_less_aux_empty [simp]: "¬ A ⊏' {}"
by(auto simp add: set_less_aux_def intro: finite_subset finite_complement_partition)

lemma set_less_eq_aux_empty [simp]: "A ⊑' {} ⟷ A = {}"
by(auto simp add: set_less_eq_aux_def finite_complement_partition)

lemma set_less_aux_antisym: "⟦ A ⊏' B; B ⊏' A ⟧ ⟹ False"
by(auto simp add: set_less_aux_def split: if_split_asm)

lemma set_less_aux_conv_set_less_eq_aux:
  "A ⊏' B ⟷ A ⊑' B ∧ ¬ B ⊑' A"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym)

lemma set_less_eq_aux_antisym: "⟦ A ⊑' B; B ⊑' A ⟧ ⟹ A = B"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_antisym)

lemma set_less_aux_finiteD: "A ⊏' B ⟹ finite A ∧ B ∈ infinite_complement_partition"
by(auto simp add: set_less_aux_def finite_complement_partition)

lemma set_less_eq_aux_infinite_complement_partitionD:
  "A ⊑' B ⟹ A ∈ infinite_complement_partition ∧ B ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_finiteD intro: finite_complement_partition)

lemma Compl_set_less_aux_Compl:
  "finite (UNIV :: 'a set) ⟹ - A ⊏' - B ⟷ B ⊏' A"
by(auto simp add: set_less_aux_def finite_subset[OF subset_UNIV])

lemma Compl_set_less_eq_aux_Compl: 
  "finite (UNIV :: 'a set) ⟹ - A ⊑' - B ⟷ B ⊑' A"
by(auto simp add: set_less_eq_aux_def Compl_set_less_aux_Compl)

lemma set_less_aux_insert_same:
  "x ∈ A ⟷ x ∈ B ⟹ insert x A ⊏' insert x B ⟷ A ⊏' B"
by(auto simp add: set_less_aux_def)

lemma set_less_eq_aux_insert_same:
  "⟦ A ∈ infinite_complement_partition; insert x B ∈ infinite_complement_partition;
    x ∈ A ⟷ x ∈ B ⟧
  ⟹ insert x A ⊑' insert x B ⟷ A ⊑' B"
by(auto simp add: set_less_eq_aux_def set_less_aux_insert_same)

end

context order begin

lemma set_less_aux_singleton_iff: "A ⊏' {x} ⟷ finite A ∧ (∀a∈A. x < a)"
by(auto simp add: set_less_aux_def less_le Bex_def)

end

context linorder begin

lemma wlog_le [case_names sym le]:
  assumes "⋀a b. P a b ⟹ P b a"
  and "⋀a b. a ≤ b ⟹ P a b"
  shows "P b a"
by (metis assms linear)

lemma empty_set_less_aux [simp]: "{} ⊏' A ⟷ A ≠ {} ∧ finite A"
by(auto 4 3 simp add: set_less_aux_def intro!: Min_eqI intro: bexI[where x="Min A"] order_trans[where y="Min A"] Min_in)

lemma empty_set_less_eq_aux [simp]: "{} ⊑' A ⟷ finite A"
by(auto simp add: set_less_eq_aux_def finite_complement_partition)

lemma set_less_aux_trans:
  assumes AB: "A ⊏' B" and BC: "B ⊏' C"
  shows "A ⊏' C"
proof -
  from AB BC have A: "finite A" and B: "finite B" and C: "finite C"
    by(auto simp add: set_less_aux_def)
  from AB A B obtain ab where ab: "ab ∈ B - A"
    and minAB: "⋀x. ⟦ x ∈ A; x ∉ B ⟧ ⟹ ab ≤ x ∧ (x ≤ ab ⟶ ab = x)"
    and minBA: "⋀x. ⟦ x ∈ B; x ∉ A ⟧ ⟹ ab ≤ x ∧ (x ≤ ab ⟶ ab = x)" 
    unfolding set_less_aux_def by auto
  from BC B C obtain bc where bc: "bc ∈ C - B"
    and minBC: "⋀x. ⟦ x ∈ B; x ∉ C ⟧ ⟹ bc ≤ x ∧ (x ≤ bc ⟶ bc = x)"
    and minCB: "⋀x. ⟦ x ∈ C; x ∉ B ⟧ ⟹ bc ≤ x ∧ (x ≤ bc ⟶ bc = x)"
    unfolding set_less_aux_def by auto
  show ?thesis
  proof(cases "ab ≤ bc")
    case True
    hence "ab ∈ C - A" "ab ∉ A - C"
      using ab bc by(auto dest: minBC antisym)
    moreover {
      fix x
      assume x: "x ∈ (C - A) ∪ (A - C)"
      hence "ab ≤ x" 
        by(cases "x ∈ B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF True])
      moreover hence "ab ≠ x ⟶ ¬ x ≤ ab" using ab bc x
        by(cases "x ∈ B")(auto dest: antisym)
      moreover note calculation }
    ultimately show ?thesis using A C unfolding set_less_aux_def by auto
  next
    case False
    with linear[of ab bc] have "bc ≤ ab" by simp
    with ab bc have "bc ∈ C - A" "bc ∉ A - C" by(auto dest: minAB antisym)
    moreover {
      fix x
      assume x: "x ∈ (C - A) ∪ (A - C)"
      hence "bc ≤ x"
        by(cases "x ∈ B")(auto dest: minAB minBA minBC minCB intro: order_trans[OF ‹bc ≤ ab›])
      moreover hence "bc ≠ x ⟶ ¬ x ≤ bc" using ab bc x
        by(cases "x ∈ B")(auto dest: antisym) 
      moreover note calculation }
    ultimately show ?thesis using A C unfolding set_less_aux_def by auto
  qed
qed

lemma set_less_eq_aux_trans [trans]:
  "⟦ A ⊑' B; B ⊑' C ⟧ ⟹ A ⊑' C"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans)

lemma set_less_trans_set_less_eq [trans]:
  "⟦ A ⊏' B; B ⊑' C ⟧ ⟹ A ⊏' C"
by(auto simp add: set_less_eq_aux_def dest: set_less_aux_trans)

lemma set_less_eq_aux_porder: "partial_order_on infinite_complement_partition {(A, B). A ⊑' B}"
by(auto simp add: preorder_on_def partial_order_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux_infinite_complement_partitionD intro: set_less_eq_aux_antisym set_less_eq_aux_trans del: equalityI)

lemma psubset_finite_imp_set_less_aux:
  assumes AsB: "A ⊂ B" and B: "finite B"
  shows "A ⊏' B"
proof -
  from AsB B have A: "finite A" by(auto intro: finite_subset)
  moreover from AsB B have "Min (B - A) ∈ B - A" by - (rule Min_in, auto)
  ultimately show ?thesis using B AsB
    by(auto simp add: set_less_aux_def intro!: rev_bexI[where x="Min (B - A)"] Min_eqI dest: Min_ge_iff[THEN iffD1, rotated 2])
qed

lemma subset_finite_imp_set_less_eq_aux:
  "⟦ A ⊆ B; finite B ⟧ ⟹ A ⊑' B"
by(cases "A = B")(auto simp add: set_less_eq_aux_def finite_complement_partition intro: psubset_finite_imp_set_less_aux)

lemma empty_set_less_aux_finite_iff: 
  "finite A ⟹ {} ⊏' A ⟷ A ≠ {}"
by(auto intro: psubset_finite_imp_set_less_aux)

lemma set_less_aux_finite_total:
  assumes A: "finite A" and B: "finite B"
  shows "A ⊏' B ∨ A = B ∨ B ⊏' A"
proof(cases "A ⊆ B ∨ B ⊆ A")
  case True thus ?thesis
    using A B psubset_finite_imp_set_less_aux[of A B] psubset_finite_imp_set_less_aux[of B A]
    by auto
next
  case False
  hence A': "¬ A ⊆ B" and B': "¬ B ⊆ A" and AnB: "A ≠ B" by auto
  thus ?thesis using A B
  proof(induct "Min (B - A)" "Min (A - B)" arbitrary: A B rule: wlog_le)
    case (sym m n)
    from sym.hyps[OF refl refl] sym.prems show ?case by blast
  next
    case (le A B)
    note A = ‹finite A› and B = ‹finite B›
      and A' = ‹¬ A ⊆ B› and B' = ‹¬ B ⊆ A›
    { fix z
      assume z: "z ∈ (A - B) ∪ (B - A)"
      hence "Min (B - A) ≤ z ∧ (z ≤ Min (B - A) ⟶ Min (B - A) = z)"
      proof
        assume "z ∈ B - A" 
        hence "Min (B - A) ≤ z" by(simp add: B)
        thus ?thesis by auto
      next
        assume "z ∈ A - B"
        hence "Min (A - B) ≤ z" by(simp add: A)
        with le.hyps show ?thesis by(auto)
      qed }
    moreover have "Min (B - A) ∈ B - A" by(rule Min_in)(simp_all add: B B')
    ultimately have "A ⊏' B" using A B by(auto simp add: set_less_aux_def)
    thus ?case ..
  qed
qed

lemma set_less_eq_aux_finite_total:
  "⟦ finite A; finite B ⟧ ⟹ A ⊑' B ∨ A = B ∨ B ⊑' A"
by(drule (1) set_less_aux_finite_total)(auto simp add: set_less_eq_aux_def)

lemma set_less_eq_aux_finite_total2:
  "⟦ finite A; finite B ⟧ ⟹ A ⊑' B ∨ B ⊑' A"
by(drule (1) set_less_eq_aux_finite_total)(auto simp add: finite_complement_partition)

lemma set_less_aux_rec:
  assumes A: "finite A" and B: "finite B"
  and A': "A ≠ {}" and B': "B ≠ {}"
  shows "A ⊏' B ⟷ Min B < Min A ∨ Min A = Min B ∧ A - {Min A} ⊏' B - {Min A}"
proof(cases "Min A = Min B")
  case True
  from A A' B B' have "insert (Min A) A = A" "insert (Min B) B = B"
    by(auto simp add: ex_in_conv[symmetric] exI)
  with True show ?thesis
    by(subst (2) set_less_aux_insert_same[symmetric, where x="Min A"]) simp_all
next
  case False
  have "A ⊏' B ⟷ Min B < Min A"
  proof
    assume AB: "A ⊏' B"
    with B A obtain ab where ab: "ab ∈ B - A"
      and AB: "⋀x. ⟦ x ∈ A; x ∉ B ⟧ ⟹ ab ≤ x"
      by(auto simp add: set_less_aux_def)
    { fix a assume "a ∈ A"
      hence "Min B ≤ a" using A A' B B' ab
        by(cases "a ∈ B")(auto intro: order_trans[where y=ab] dest: AB) }
    hence "Min B ≤ Min A" using A A' by simp
    with False show "Min B < Min A" using False by auto
  next
    assume "Min B < Min A"
    hence "∀z∈A - B ∪ (B - A). Min B ≤ z ∧ (z ≤ Min B ⟶ Min B = z)"
      using A B A' B' by(auto 4 4 intro: Min_in Min_eqI dest: bspec bspec[where x="Min B"])
    moreover have "Min B ∉ A" using ‹Min B < Min A› by (metis A Min_le not_less)
    ultimately show "A ⊏' B" using A B A' B' by(simp add: set_less_aux_def bexI[where x="Min B"])
  qed
  thus ?thesis using False by simp
qed

lemma set_less_eq_aux_rec:
  assumes "finite A" "finite B" "A ≠ {}" "B ≠ {}"
  shows "A ⊑' B ⟷ Min B < Min A ∨ Min A = Min B ∧ A - {Min A} ⊑' B - {Min A}"
proof(cases "A = B")
  case True thus ?thesis using assms by(simp add: finite_complement_partition)
next
  case False
  moreover 
  hence "Min A = Min B ⟹ A - {Min A} ≠ B - {Min B}"
    by (metis (lifting) assms Min_in insert_Diff)
  ultimately show ?thesis using set_less_aux_rec[OF assms]
    by(simp add: set_less_eq_aux_def cong: conj_cong)
qed

lemma set_less_aux_Min_antimono:
  "⟦ Min A < Min B;  finite A; finite B; A ≠ {} ⟧ ⟹ B ⊏' A"
using set_less_aux_rec[of B A] 
by(cases "B = {}")(simp_all add: empty_set_less_aux_finite_iff)

lemma sorted_Cons_Min: "sorted (x # xs) ⟹ Min (insert x (set xs)) = x"
  by(auto simp add: intro: Min_eqI)

lemma set_less_aux_code:
  "⟦ sorted xs; distinct xs; sorted ys; distinct ys ⟧
  ⟹ set xs ⊏' set ys ⟷ ord.lexordp (>) xs ys"
  apply(induct xs ys rule: list_induct2')
     apply(simp_all add: empty_set_less_aux_finite_iff sorted_Cons_Min set_less_aux_rec neq_Nil_conv)
  apply(auto cong: conj_cong)
  done

lemma set_less_eq_aux_code:
  assumes "sorted xs" "distinct xs" "sorted ys" "distinct ys"
  shows "set xs ⊑' set ys ⟷ ord.lexordp_eq (>) xs ys"
proof -
  have dual: "class.linorder (≥) (>)"
    by(rule linorder.dual_linorder) unfold_locales
  from assms show ?thesis
    by(auto simp add: set_less_eq_aux_def finite_complement_partition linorder.lexordp_eq_conv_lexord[OF dual] set_less_aux_code intro: sorted_distinct_set_unique)
qed

end

subsubsection ‹Extending @{term set_less_eq_aux} to have @{term "{}"} as least element›

context ord begin

definition set_less_eq_aux' :: "'a set ⇒ 'a set ⇒ bool" (infix ‹⊑''''› 50)
where "A ⊑'' B ⟷ A ⊑' B ∨ A = {} ∧ B ∈ infinite_complement_partition"

lemma set_less_eq_aux'_refl:
  "A ⊑'' A ⟷ A ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux'_def)

lemma set_less_eq_aux'_antisym: "⟦ A ⊑'' B; B ⊑'' A ⟧ ⟹ A = B"
by(auto simp add: set_less_eq_aux'_def intro: set_less_eq_aux_antisym del: equalityI)

lemma set_less_eq_aux'_infinite_complement_partitionD:
  "A ⊑'' B ⟹ A ∈ infinite_complement_partition ∧ B ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux'_def intro: finite_complement_partition dest: set_less_eq_aux_infinite_complement_partitionD)

lemma empty_set_less_eq_def [simp]: "{} ⊑'' B ⟷ B ∈ infinite_complement_partition"
by(auto simp add: set_less_eq_aux'_def dest: set_less_eq_aux_infinite_complement_partitionD)

end

context linorder begin

lemma set_less_eq_aux'_trans: "⟦ A ⊑'' B; B ⊑'' C ⟧ ⟹ A ⊑'' C"
by(auto simp add: set_less_eq_aux'_def del: equalityI intro: set_less_eq_aux_trans dest: set_less_eq_aux_infinite_complement_partitionD)

lemma set_less_eq_aux'_porder: "partial_order_on infinite_complement_partition {(A, B). A ⊑'' B}"
by(auto simp add: partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI dest: set_less_eq_aux'_antisym set_less_eq_aux'_infinite_complement_partitionD simp add: set_less_eq_aux'_refl intro: set_less_eq_aux'_trans)

end

subsubsection ‹Extend @{term set_less_eq_aux'} to a total order on @{term infinite_complement_partition}›

context ord begin

definition set_less_eq_aux'' :: "'a set ⇒ 'a set ⇒ bool" (infix ‹⊑''''''› 50)
where "set_less_eq_aux'' =
  (SOME sleq. 
    (linear_order_on UNIV {(a, b). a ≤ b} ⟶ linear_order_on infinite_complement_partition {(A, B). sleq A B}) ∧ order_consistent {(A, B). A ⊑'' B} {(A, B). sleq A B})"

lemma set_less_eq_aux''_spec:
  shows "linear_order {(a, b). a ≤ b} ⟹ linear_order_on infinite_complement_partition {(A, B). A ⊑''' B}"
  (is "PROP ?thesis1")
  and "order_consistent {(A, B). A ⊑'' B} {(A, B). A ⊑''' B}" (is ?thesis2)
proof -
  let ?P = "λsleq. (linear_order {(a, b). a ≤ b} ⟶ linear_order_on infinite_complement_partition {(A, B). sleq A B}) ∧ 
                  order_consistent {(A, B). A ⊑'' B} {(A, B). sleq A B}"
  have "Ex ?P"
  proof(cases "linear_order {(a, b). a ≤ b}")
    case False
    have "antisym {(a, b). a ⊑'' b}"
      by (rule antisymI) (simp add: set_less_eq_aux'_antisym)
    then show ?thesis using False
      by (auto intro: antisym_order_consistent_self)
  next
    case True
    hence "partial_order_on infinite_complement_partition {(A, B). A ⊑'' B}"
      by(rule linorder.set_less_eq_aux'_porder[OF linear_order_imp_linorder])
    then obtain s where "linear_order_on infinite_complement_partition s"
      and "order_consistent {(A, B). A ⊑'' B} s" by(rule porder_extend_to_linorder)
    thus ?thesis by(auto intro: exI[where x="λA B. (A, B) ∈ s"])
  qed
  hence "?P (Eps ?P)" by(rule someI_ex)
  thus "PROP ?thesis1" ?thesis2 by(simp_all add: set_less_eq_aux''_def)
qed

end

context linorder begin

lemma set_less_eq_aux''_linear_order:
  "linear_order_on infinite_complement_partition {(A, B). A ⊑''' B}"
by(rule set_less_eq_aux''_spec)(rule linear_order)

lemma set_less_eq_aux''_refl [iff]: "A ⊑''' A ⟷ A ∈ infinite_complement_partition"
using set_less_eq_aux''_linear_order
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: refl_onD refl_onD1)

lemma set_less_eq_aux'_into_set_less_eq_aux'':
  assumes "A ⊑'' B" 
  shows "A ⊑''' B"
proof(rule ccontr)
  assume nleq: "¬ ?thesis"
  moreover from assms have A: "A ∈ infinite_complement_partition" 
    and B: "B ∈ infinite_complement_partition"
    by(auto dest: set_less_eq_aux'_infinite_complement_partitionD)
  with set_less_eq_aux''_linear_order have "A ⊑''' B ∨ A = B ∨ B ⊑''' A"
    by(auto simp add: linear_order_on_def dest: total_onD)
  ultimately have "B ⊑''' A" using B by auto
  with assms have "A = B" using set_less_eq_aux''_spec(2)
    by(simp add: order_consistent_def)
  with A nleq show False by simp
qed

lemma finite_set_less_eq_aux''_finite:
  assumes "finite A" and "finite B"
  shows "A ⊑''' B ⟷ A ⊑'' B"
proof
  assume "A ⊑''' B"
  from assms have "A ⊑' B ∨ B ⊑' A" by(rule set_less_eq_aux_finite_total2)
  hence "A ⊑'' B ∨ B ⊑'' A" by(auto simp add: set_less_eq_aux'_def)
  thus "A ⊑'' B"
  proof
    assume "B ⊑'' A"
    hence "B ⊑''' A" by(rule set_less_eq_aux'_into_set_less_eq_aux'')
    with ‹A ⊑''' B› set_less_eq_aux''_linear_order have "A = B"
      by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD)
    thus ?thesis using assms by(simp add: finite_complement_partition set_less_eq_aux'_def)
  qed
qed(rule set_less_eq_aux'_into_set_less_eq_aux'')

lemma set_less_eq_aux''_finite:
  "finite (UNIV :: 'a set) ⟹ set_less_eq_aux'' = set_less_eq_aux"
by(auto simp add: fun_eq_iff finite_set_less_eq_aux''_finite set_less_eq_aux'_def finite_subset[OF subset_UNIV])

lemma set_less_eq_aux''_antisym:
  "⟦ A ⊑''' B; B ⊑''' A; 
     A ∈ infinite_complement_partition; B ∈ infinite_complement_partition ⟧
  ⟹ A = B"
using set_less_eq_aux''_linear_order 
by(auto simp add: linear_order_on_def partial_order_on_def dest: antisymD del: equalityI)

lemma set_less_eq_aux''_trans: "⟦ A ⊑''' B; B ⊑''' C ⟧ ⟹ A ⊑''' C"
using set_less_eq_aux''_linear_order
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: transD)

lemma set_less_eq_aux''_total:
  "⟦ A ∈ infinite_complement_partition; B ∈ infinite_complement_partition ⟧
  ⟹ A ⊑''' B ∨ B ⊑''' A"
using set_less_eq_aux''_linear_order
by(auto simp add: linear_order_on_def dest: total_onD)

end

subsubsection ‹Extend @{term set_less_eq_aux''} to cofinite sets›

context ord begin

definition set_less_eq :: "'a set ⇒ 'a set ⇒ bool" (infix ‹⊑› 50)
where 
  "A ⊑ B ⟷ 
  (if A ∈ infinite_complement_partition then A ⊑''' B ∨ B ∉ infinite_complement_partition
   else B ∉ infinite_complement_partition ∧ - B ⊑''' - A)"

definition set_less :: "'a set ⇒ 'a set ⇒ bool" (infix ‹⊏› 50)
where "A ⊏ B ⟷ A ⊑ B ∧ ¬ B ⊑ A"

lemma set_less_eq_def2:
  "A ⊑ B ⟷
  (if finite (UNIV :: 'a set) then A ⊑''' B 
   else if A ∈ infinite_complement_partition then A ⊑''' B ∨ B ∉ infinite_complement_partition
   else B ∉ infinite_complement_partition ∧ - B ⊑''' - A)"
by(simp add: set_less_eq_def)

end

context linorder begin

lemma set_less_eq_refl [iff]: "A ⊑ A"
by(auto simp add: set_less_eq_def2 not_in_complement_partition)

lemma set_less_eq_antisym: "⟦ A ⊑ B; B ⊑ A ⟧ ⟹ A = B"
by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False del: equalityI split: if_split_asm dest: set_less_eq_aux_antisym set_less_eq_aux''_antisym)

lemma set_less_eq_trans: "⟦ A ⊑ B; B ⊑ C ⟧ ⟹ A ⊑ C"
by(auto simp add: set_less_eq_def split: if_split_asm intro: set_less_eq_aux''_trans)

lemma set_less_eq_total: "A ⊑ B ∨ B ⊑ A"
by(auto simp add: set_less_eq_def2 set_less_eq_aux''_finite not_in_complement_partition not_in_complement_partition_False intro: set_less_eq_aux_finite_total2 finite_subset[OF subset_UNIV] del: disjCI dest: set_less_eq_aux''_total)

lemma set_less_eq_linorder: "class.linorder (⊑) (⊏)"
by(unfold_locales)(auto simp add: set_less_def set_less_eq_antisym set_less_eq_total intro: set_less_eq_trans)

lemma set_less_eq_conv_set_less: "set_less_eq A B ⟷ A = B ∨ set_less A B"
by(auto simp add: set_less_def del: equalityI dest: set_less_eq_antisym)

lemma Compl_set_less_eq_Compl: "- A ⊑ - B ⟷ B ⊑ A"
by(auto simp add: set_less_eq_def2 not_in_complement_partition_False not_in_complement_partition set_less_eq_aux''_finite Compl_set_less_eq_aux_Compl)

lemma Compl_set_less_Compl: "- A ⊏ - B ⟷ B ⊏ A"
by(simp add: set_less_def Compl_set_less_eq_Compl)

lemma set_less_eq_finite_iff: "⟦ finite A; finite B ⟧ ⟹ A ⊑ B ⟷ A ⊑' B"
by(auto simp add: set_less_eq_def finite_complement_partition set_less_eq_aux'_def finite_set_less_eq_aux''_finite)

lemma set_less_finite_iff: "⟦ finite A; finite B ⟧ ⟹ A ⊏ B ⟷ A ⊏' B"
by(simp add: set_less_def set_less_aux_conv_set_less_eq_aux set_less_eq_finite_iff)

lemma infinite_set_less_eq_Complement:
  "⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ A ⊑ - B"
by(simp add: set_less_eq_def finite_complement_partition not_in_complement_partition)

lemma infinite_set_less_Complement:
  "⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ A ⊏ - B"
by(auto simp add: set_less_def dest: set_less_eq_antisym intro: infinite_set_less_eq_Complement)

lemma infinite_Complement_set_less_eq:
  "⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ ¬ - A ⊑ B"
using infinite_set_less_eq_Complement[of A B] Compl_set_less_eq_Compl[of A "- B"]
by(auto dest: set_less_eq_antisym)

lemma infinite_Complement_set_less:
  "⟦ finite A; finite B; ¬ finite (UNIV :: 'a set) ⟧ ⟹ ¬ - A ⊏ B"
using infinite_Complement_set_less_eq[of A B]
by(simp add: set_less_def)

lemma empty_set_less_eq [iff]: "{} ⊑ A"
by(auto simp add: set_less_eq_def finite_complement_partition intro: set_less_eq_aux'_into_set_less_eq_aux'')

lemma set_less_eq_empty [iff]: "A ⊑ {} ⟷ A = {}"
by (metis empty_set_less_eq set_less_eq_antisym)

lemma empty_set_less_iff [iff]: "{} ⊏ A ⟷ A ≠ {}"
by(simp add: set_less_def)

lemma not_set_less_empty [simp]: "¬ A ⊏ {}"
by(simp add: set_less_def)

lemma set_less_eq_UNIV [iff]: "A ⊑ UNIV"
using Compl_set_less_eq_Compl[of "- A" "{}"] by simp

lemma UNIV_set_less_eq [iff]: "UNIV ⊑ A ⟷ A = UNIV"
using Compl_set_less_eq_Compl[of "{}" "- A"]
by(simp add: Compl_eq_empty_iff)

lemma set_less_UNIV_iff [iff]: "A ⊏ UNIV ⟷ A ≠ UNIV"
by(simp add: set_less_def)

lemma not_UNIV_set_less [simp]: "¬ UNIV ⊏ A"
by(simp add: set_less_def)

end

subsection ‹Implementation based on sorted lists›

type_synonym 'a proper_interval = "'a option ⇒ 'a option ⇒ bool"

class proper_intrvl = ord +
  fixes proper_interval :: "'a proper_interval"

class proper_interval = proper_intrvl +
  assumes proper_interval_simps:
  "proper_interval None None = True"
  "proper_interval None (Some y) = (∃z. z < y)"
  "proper_interval (Some x) None = (∃z. x < z)"
  "proper_interval (Some x) (Some y) = (∃z. x < z ∧ z < y)"

context proper_intrvl begin

function set_less_eq_aux_Compl :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool"
where
  "set_less_eq_aux_Compl ao [] ys ⟷ True"
| "set_less_eq_aux_Compl ao xs [] ⟷ True"
| "set_less_eq_aux_Compl ao (x # xs) (y # ys) ⟷
  (if x < y then proper_interval ao (Some x) ∨ set_less_eq_aux_Compl (Some x) xs (y # ys)
   else if y < x then proper_interval ao (Some y) ∨ set_less_eq_aux_Compl (Some y) (x # xs) ys
   else proper_interval ao (Some y))"
by(pat_completeness) simp_all
termination by(lexicographic_order)

fun Compl_set_less_eq_aux :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool"
where
  "Compl_set_less_eq_aux ao [] [] ⟷ ¬ proper_interval ao None"
| "Compl_set_less_eq_aux ao [] (y # ys) ⟷ ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux (Some y) [] ys"
| "Compl_set_less_eq_aux ao (x # xs) [] ⟷ ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux (Some x) xs []"
| "Compl_set_less_eq_aux ao (x # xs) (y # ys) ⟷
  (if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux (Some x) xs (y # ys)
   else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux (Some y) (x # xs) ys
   else ¬ proper_interval ao (Some y))"

fun set_less_aux_Compl :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool" where
  "set_less_aux_Compl ao [] [] ⟷ proper_interval ao None"
| "set_less_aux_Compl ao [] (y # ys) ⟷ proper_interval ao (Some y) ∨ set_less_aux_Compl (Some y) [] ys"
| "set_less_aux_Compl ao (x # xs) [] ⟷ proper_interval ao (Some x) ∨ set_less_aux_Compl (Some x) xs []"
| "set_less_aux_Compl ao (x # xs) (y # ys) ⟷
  (if x < y then proper_interval ao (Some x) ∨ set_less_aux_Compl (Some x) xs (y # ys)
   else if y < x then proper_interval ao (Some y) ∨ set_less_aux_Compl (Some y) (x # xs) ys
   else proper_interval ao (Some y))"

function Compl_set_less_aux :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool" where
  "Compl_set_less_aux ao [] ys ⟷ False"
| "Compl_set_less_aux ao xs [] ⟷ False"
| "Compl_set_less_aux ao (x # xs) (y # ys) ⟷
  (if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_aux (Some x) xs (y # ys)
   else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_aux (Some y) (x # xs) ys
   else ¬ proper_interval ao (Some y))"
by pat_completeness simp_all
termination by lexicographic_order

end

lemmas [code] =
  proper_intrvl.set_less_eq_aux_Compl.simps
  proper_intrvl.set_less_aux_Compl.simps
  proper_intrvl.Compl_set_less_eq_aux.simps
  proper_intrvl.Compl_set_less_aux.simps

class linorder_proper_interval = linorder + proper_interval 
begin

theorem assumes fin: "finite (UNIV :: 'a set)"
  and xs: "sorted xs" "distinct xs"
  and ys: "sorted ys" "distinct ys"
  shows set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl:
  "set xs ⊑' - set ys ⟷ set_less_eq_aux_Compl None xs ys" (is ?Compl2)
  and Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux:
  "- set xs ⊑' set ys ⟷ Compl_set_less_eq_aux None xs ys" (is ?Compl1)
proof -
  note fin' [simp] = finite_subset[OF subset_UNIV fin]

  define above where "above = case_option UNIV (Collect ∘ less)"
  have above_simps [simp]: "above None = UNIV" "⋀x. above (Some x) = {y. x < y}"
    and above_upclosed: "⋀x y ao. ⟦ x ∈ above ao; x < y ⟧ ⟹ y ∈ above ao"
    and proper_interval_Some2: "⋀x ao. proper_interval ao (Some x) ⟷ (∃z∈above ao. z < x)"
    and proper_interval_None2: "⋀ao. proper_interval ao None ⟷ above ao ≠ {}"
    by(simp_all add: proper_interval_simps above_def split: option.splits)

  { fix ao x A B
    assume ex: "proper_interval ao (Some x)"
      and A: "∀a ∈ A. x ≤ a"
      and B: "∀b ∈ B. x ≤ b"
    from ex obtain z where z_ao: "z ∈ above ao" and z: "z < x"
      by(auto simp add: proper_interval_Some2)
    with A have A_eq: "A ∩ above ao = A"
      by(auto simp add: above_upclosed)
    from z_ao z B have B_eq: "B ∩ above ao = B"
      by(auto simp add: above_upclosed)
    define w where "w = Min (above ao)"
    with z_ao have "w ≤ z" "∀z ∈ above ao. w ≤ z" "w ∈ above ao"
      by(auto simp add: Min_le_iff intro: Min_in)
    hence "A ∩ above ao ⊏' (- B) ∩ above ao" (is "?lhs ⊏' ?rhs")
      using A B z by(auto simp add: set_less_aux_def intro!: bexI[where x="w"])
    hence "A ⊑' ?rhs" unfolding A_eq by(simp add: set_less_eq_aux_def)
    moreover 
    from z_ao z A B have "z ∈ - A ∩ above ao" "z ∉ B" by auto
    hence neq: "- A ∩ above ao ≠ B ∩ above ao" by auto
    have "¬ - A ∩ above ao ⊏' B ∩ above ao" (is "¬ ?lhs' ⊏' ?rhs'")
      using A B z z_ao by(force simp add: set_less_aux_def not_less dest: bspec[where x=z])
    with neq have "¬ ?lhs' ⊑' B" unfolding B_eq by(auto simp add: set_less_eq_aux_def)
    moreover note calculation }
  note proper_interval_set_less_eqI = this(1)
    and proper_interval_not_set_less_eq_auxI = this(2)

  { fix ao
    assume "set xs ∪ set ys ⊆ above ao"
    with xs ys
    have "set_less_eq_aux_Compl ao xs ys ⟷ set xs ⊑' (- set ys) ∩ above ao"
    proof(induction ao xs ys rule: set_less_eq_aux_Compl.induct)
      case 1 thus ?case by simp
    next
      case 2 thus ?case by(auto intro: subset_finite_imp_set_less_eq_aux)
    next
      case (3 ao x xs y ys)
      note ao = ‹set (x # xs) ∪ set (y # ys) ⊆ above ao›
      hence x_ao: "x ∈ above ao" and y_ao: "y ∈ above ao" by simp_all
      note yys = ‹sorted (y # ys)› ‹distinct (y # ys)›
      hence ys: "sorted ys" "distinct ys" and y_Min: "∀y' ∈ set ys. y < y'"
        by(auto simp add: less_le)
      note xxs = ‹sorted (x # xs)› ‹distinct (x # xs)›
      hence xs: "sorted xs" "distinct xs" and x_Min: "∀x' ∈ set xs. x < x'"
        by(auto simp add: less_le)
      let ?lhs = "set (x # xs)" and ?rhs = "- set (y # ys) ∩ above ao"
      show ?case
      proof(cases "x < y")
        case True
        show ?thesis
        proof(cases "proper_interval ao (Some x)")
          case True
          hence "?lhs ⊑' ?rhs" using x_Min y_Min ‹x < y›
            by(auto intro!: proper_interval_set_less_eqI)
          with True show ?thesis using ‹x < y› by simp
        next
          case False
          have "set xs ∪ set (y # ys) ⊆ above (Some x)" using True x_Min y_Min by auto
          with True xs yys
          have IH: "set_less_eq_aux_Compl (Some x) xs (y # ys) = 
            (set xs ⊑' - set (y # ys) ∩ above (Some x))"
            by(rule "3.IH")
          from True y_Min x_ao have "x ∈ - set (y # ys) ∩ above ao" by auto
          hence "?rhs ≠ {}" by blast
          moreover have "Min ?lhs = x" using x_Min x_ao by(auto intro!: Min_eqI)
          moreover have "Min ?rhs = x" using ‹x < y› y_Min x_ao False
            by(auto intro!: Min_eqI simp add: proper_interval_Some2)
          moreover have "set xs = set xs - {x}"
            using ao x_Min by auto
          moreover have "- set (y # ys) ∩ above (Some x) = - set (y # ys) ∩ above ao - {x}"
            using False x_ao by(auto simp add: proper_interval_Some2 intro: above_upclosed)
          ultimately show ?thesis using True False IH
            by(simp del: set_simps)(subst (2) set_less_eq_aux_rec, simp_all add: x_ao)
        qed
      next
        case False
        show ?thesis
        proof(cases "y < x")
          case True
          show ?thesis
          proof(cases "proper_interval ao (Some y)")
            case True
            hence "?lhs ⊑' ?rhs" using x_Min y_Min ‹¬ x < y›
              by(auto intro!: proper_interval_set_less_eqI)
            with True show ?thesis using ‹¬ x < y› by simp
          next
            case False
            have "set (x # xs) ∪ set ys ⊆ above (Some y)"
              using ‹y < x› x_Min y_Min by auto
            with ‹¬ x < y› ‹y < x› xxs ys
            have IH: "set_less_eq_aux_Compl (Some y) (x # xs) ys = 
              (set (x # xs) ⊑' - set ys ∩ above (Some y))"
              by(rule "3.IH")
            moreover have "- set ys ∩ above (Some y) = ?rhs"
              using y_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2)
            ultimately show ?thesis using ‹¬ x < y› True False by simp
          qed
        next
          case False with ‹¬ x < y› have "x = y" by auto
          { assume "proper_interval ao (Some y)"
            hence "?lhs ⊑' ?rhs" using x_Min y_Min ‹x = y›
              by(auto intro!: proper_interval_set_less_eqI) }
          moreover
          { assume "?lhs ⊑' ?rhs"
            moreover have "?lhs ≠ ?rhs"
            proof
              assume eq: "?lhs = ?rhs"
              have "x ∈ ?lhs" using x_ao by simp
              also note eq also note ‹x = y›
              finally show False by simp
            qed
            ultimately obtain z where "z ∈ above ao" "z < y" using ‹x = y› y_ao
              by(fastforce simp add: set_less_eq_aux_def set_less_aux_def not_le dest!: bspec[where x=y])
            hence "proper_interval ao (Some y)" by(auto simp add: proper_interval_Some2) }
          ultimately show ?thesis using ‹x = y› ‹¬ x < y› ‹¬ y < x› by auto
        qed
      qed
    qed }
  from this[of None] show ?Compl2 by simp
  
  { fix ao
    assume "set xs ∪ set ys ⊆ above ao"
    with xs ys
    have "Compl_set_less_eq_aux ao xs ys ⟷ (- set xs) ∩ above ao ⊑' set ys"
    proof(induction ao xs ys rule: Compl_set_less_eq_aux.induct)
      case 1 thus ?case by(simp add: proper_interval_None2)
    next
      case (2 ao y ys)
      from ‹sorted (y # ys)› ‹distinct (y # ys)›
      have ys: "sorted ys" "distinct ys" and y_Min: "∀y' ∈ set ys. y < y'"
        by(auto simp add: less_le)
      show ?case
      proof(cases "proper_interval ao (Some y)")
        case True 
        hence "¬ - set [] ∩ above ao ⊑' set (y # ys)" using y_Min
          by -(erule proper_interval_not_set_less_eq_auxI, auto)
        thus ?thesis using True by simp
      next
        case False
        note ao = ‹set [] ∪ set (y # ys) ⊆ above ao› 
        hence y_ao: "y ∈ above ao" by simp
        from ao y_Min have "set [] ∪ set ys ⊆ above (Some y)" by auto
        with ‹sorted []› ‹distinct []› ys
        have "Compl_set_less_eq_aux (Some y) [] ys ⟷ - set [] ∩ above (Some y) ⊑' set ys"
          by(rule "2.IH")
        moreover have "above ao ≠ {}" using y_ao by auto
        moreover have "Min (above ao) = y" 
          and "Min (set (y # ys)) = y"
          using y_ao False ao by(auto intro!: Min_eqI simp add: proper_interval_Some2 not_less)
        moreover have "above ao - {y} = above (Some y)" using False y_ao
          by(auto simp add: proper_interval_Some2 intro: above_upclosed)
        moreover have "set ys - {y} = set ys" 
          using y_Min y_ao by(auto)
        ultimately show ?thesis using False y_ao
          by(simp)(subst (2) set_less_eq_aux_rec, simp_all)
      qed
    next
      case (3 ao x xs)
      from ‹sorted (x # xs)› ‹distinct (x # xs)›
      have xs: "sorted xs" "distinct xs" and x_Min: "∀x'∈set xs. x < x'"
        by(auto simp add: less_le)
      show ?case
      proof(cases "proper_interval ao (Some x)")
        case True
        then obtain z where "z ∈ above ao" "z < x" by(auto simp add: proper_interval_Some2)
        hence "z ∈ - set (x # xs) ∩ above ao" using x_Min by auto
        thus ?thesis using True by auto
      next
        case False
        note ao = ‹set (x # xs) ∪ set [] ⊆ above ao›
        hence x_ao: "x ∈ above ao" by simp
        from ao have "set xs ∪ set [] ⊆ above (Some x)" using x_Min by auto
        with xs ‹sorted []› ‹distinct []› 
        have "Compl_set_less_eq_aux (Some x) xs [] ⟷
          - set xs ∩ above (Some x) ⊑' set []"
          by(rule "3.IH")
        moreover have "- set (x # xs) ∩ above ao = - set xs ∩ above (Some x)" 
          using False x_ao by(auto simp add: proper_interval_Some2 intro: above_upclosed)
        ultimately show ?thesis using False by simp
      qed
    next
      case (4 ao x xs y ys)
      note ao = ‹set (x # xs) ∪ set (y # ys) ⊆ above ao›
      hence x_ao: "x ∈ above ao" and y_ao: "y ∈ above ao" by simp_all
      note xxs = ‹sorted (x # xs)› ‹distinct (x # xs)›
      hence xs: "sorted xs" "distinct xs" and x_Min: "∀x'∈set xs. x < x'"
        by(auto simp add: less_le)
      note yys = ‹sorted (y # ys)› ‹distinct (y # ys)›
      hence ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"
        by(auto simp add: less_le)
      let ?lhs = "- set (x # xs) ∩ above ao" and ?rhs = "set (y # ys)"
      show ?case
      proof(cases "x < y")
        case True
        show ?thesis
        proof(cases "proper_interval ao (Some x)")
          case True
          hence "¬ ?lhs ⊑' ?rhs" using x_Min y_Min ‹x < y›
            by -(erule proper_interval_not_set_less_eq_auxI, auto)
          thus ?thesis using True ‹x < y› by simp
        next
          case False
          have "set xs ∪ set (y # ys) ⊆ above (Some x)" 
            using ao x_Min y_Min True by auto
          with True xs yys
          have "Compl_set_less_eq_aux (Some x) xs (y # ys) ⟷ 
            - set xs ∩ above (Some x) ⊑' set (y # ys)"
            by(rule "4.IH")
          moreover have "- set xs ∩ above (Some x) = ?lhs"
            using x_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2)
          ultimately show ?thesis using False True by simp
        qed
      next
        case False
        show ?thesis
        proof(cases "y < x")
          case True
          show ?thesis
          proof(cases "proper_interval ao (Some y)")
            case True
            hence "¬ ?lhs ⊑' ?rhs" using x_Min y_Min ‹y < x›
              by -(erule proper_interval_not_set_less_eq_auxI, auto)
            thus ?thesis using True ‹y < x› ‹¬ x < y› by simp
          next
            case False
            from ao True x_Min y_Min 
            have "set (x # xs) ∪ set ys ⊆ above (Some y)" by auto
            with ‹¬ x < y› True xxs ys
            have "Compl_set_less_eq_aux (Some y) (x # xs) ys ⟷
              - set (x # xs) ∩ above (Some y) ⊑' set ys"
              by(rule "4.IH")
            moreover have "y ∈ ?lhs" using True x_Min y_ao by auto
            hence "?lhs ≠ {}" by auto
            moreover have "Min ?lhs = y" using True False x_Min y_ao
              by(auto intro!: Min_eqI simp add: not_le not_less proper_interval_Some2)
            moreover have "Min ?rhs = y" using y_Min y_ao by(auto intro!: Min_eqI)
            moreover have "- set (x # xs) ∩ above (Some y) = ?lhs - {y}"
              using y_ao False by(auto intro: above_upclosed simp add: proper_interval_Some2)
            moreover have "set ys = set ys - {y}"
              using y_ao y_Min by(auto intro: above_upclosed)
            ultimately show ?thesis using True False ‹¬ x < y› y_ao
              by(simp)(subst (2) set_less_eq_aux_rec, simp_all)
          qed
        next
          case False
          with ‹¬ x < y› have "x = y" by auto
          { assume "proper_interval ao (Some y)"
            hence "¬ ?lhs ⊑' ?rhs" using x_Min y_Min ‹x = y›
              by -(erule proper_interval_not_set_less_eq_auxI, auto) }
          moreover
          { assume "¬ ?lhs ⊑' ?rhs"
            also have "?rhs = set (y # ys) ∩ above ao"
              using ao by auto
            finally obtain z where "z ∈ above ao" "z < y" 
              using ‹x = y› x_ao x_Min[unfolded Ball_def]
              by(fastforce simp add: set_less_eq_aux_def set_less_aux_def simp add: less_le not_le dest!: bspec[where x=y])
            hence "proper_interval ao (Some y)" 
              by(auto simp add: proper_interval_Some2) }
          ultimately show ?thesis using ‹x = y› by auto
        qed
      qed
    qed }
  from this[of None] show ?Compl1 by simp
qed

lemma set_less_aux_Compl_iff:
  "set_less_aux_Compl ao xs ys ⟷ set_less_eq_aux_Compl ao xs ys ∧ ¬ Compl_set_less_eq_aux ao ys xs"
by(induct ao xs ys rule: set_less_aux_Compl.induct)(auto simp add: not_less_iff_gr_or_eq)

lemma Compl_set_less_aux_Compl_iff:
  "Compl_set_less_aux ao xs ys ⟷ Compl_set_less_eq_aux ao xs ys ∧ ¬ set_less_eq_aux_Compl ao ys xs"
by(induct ao xs ys rule: Compl_set_less_aux.induct)(auto simp add: not_less_iff_gr_or_eq)

theorem assumes fin: "finite (UNIV :: 'a set)"
  and xs: "sorted xs" "distinct xs"
  and ys: "sorted ys" "distinct ys"
  shows set_less_aux_Compl2_conv_set_less_aux_Compl:
  "set xs ⊏' - set ys ⟷ set_less_aux_Compl None xs ys" (is ?Compl2)
  and Compl1_set_less_aux_conv_Compl_set_less_aux:
  "- set xs ⊏' set ys ⟷ Compl_set_less_aux None xs ys" (is ?Compl1)
using assms
by(simp_all only: set_less_aux_conv_set_less_eq_aux set_less_aux_Compl_iff Compl_set_less_aux_Compl_iff set_less_eq_aux_Compl2_conv_set_less_eq_aux_Compl Compl1_set_less_eq_aux_conv_Compl_set_less_eq_aux)

end

subsection ‹Implementation of proper intervals for sets›

definition length_last :: "'a list ⇒ nat × 'a"
where "length_last xs = (length xs, last xs)"

lemma length_last_Nil [code]: "length_last [] = (0, undefined)"
by(simp add: length_last_def last_def)

lemma length_last_Cons_code [symmetric, code]:
  "fold (λx (n, _) . (n + 1, x)) xs (1, x) = length_last (x # xs)"
by(induct xs rule: rev_induct)(simp_all add: length_last_def)

context proper_intrvl begin

fun exhaustive_above :: "'a ⇒ 'a list ⇒ bool" where
  "exhaustive_above x [] ⟷ ¬ proper_interval (Some x) None"
| "exhaustive_above x (y # ys) ⟷ ¬ proper_interval (Some x) (Some y) ∧ exhaustive_above y ys"

fun exhaustive :: "'a list ⇒ bool" where 
  "exhaustive [] = False"
| "exhaustive (x # xs) ⟷ ¬ proper_interval None (Some x) ∧ exhaustive_above x xs"

fun proper_interval_set_aux :: "'a list ⇒ 'a list ⇒ bool"
where
  "proper_interval_set_aux xs [] ⟷ False"
| "proper_interval_set_aux [] (y # ys) ⟷ ys ≠ [] ∨ proper_interval (Some y) None"
| "proper_interval_set_aux (x # xs) (y # ys) ⟷
  (if x < y then False
   else if y < x then proper_interval (Some y) (Some x) ∨ ys ≠ [] ∨ ¬ exhaustive_above x xs
   else proper_interval_set_aux xs ys)"

fun proper_interval_set_Compl_aux :: "'a option ⇒ nat ⇒ 'a list ⇒ 'a list ⇒ bool"
where
  "proper_interval_set_Compl_aux ao n [] [] ⟷
   CARD('a) > n + 1"
| "proper_interval_set_Compl_aux ao n [] (y # ys) ⟷
   (let m = CARD('a) - n; (len_y, y') = length_last (y # ys)
    in m ≠ len_y ∧ (m = len_y + 1 ⟶ ¬ proper_interval (Some y') None))"
| "proper_interval_set_Compl_aux ao n (x # xs) [] ⟷
   (let m = CARD('a) - n; (len_x, x') = length_last (x # xs)
    in m ≠ len_x ∧ (m = len_x + 1 ⟶ ¬ proper_interval (Some x') None))"
| "proper_interval_set_Compl_aux ao n (x # xs) (y # ys) ⟷
  (if x < y then 
     proper_interval ao (Some x) ∨ 
     proper_interval_set_Compl_aux (Some x) (n + 1) xs (y # ys)
   else if y < x then 
     proper_interval ao (Some y) ∨ 
     proper_interval_set_Compl_aux (Some y) (n + 1) (x # xs) ys
   else proper_interval ao (Some x) ∧ 
     (let m = card (UNIV :: 'a set) - n in m - length ys ≠ 2 ∨ m - length xs ≠ 2))"

fun proper_interval_Compl_set_aux :: "'a option ⇒ 'a list ⇒ 'a list ⇒ bool"
where
  "proper_interval_Compl_set_aux ao (x # xs) (y # ys) ⟷
  (if x < y then 
     ¬ proper_interval ao (Some x) ∧ 
     proper_interval_Compl_set_aux (Some x) xs (y # ys)
   else if y < x then
     ¬ proper_interval ao (Some y) ∧
     proper_interval_Compl_set_aux (Some y) (x # xs) ys
   else ¬ proper_interval ao (Some x) ∧ (ys = [] ⟶ xs ≠ []))"
| "proper_interval_Compl_set_aux ao _ _ ⟷ False"

end

lemmas [code] = 
  proper_intrvl.exhaustive_above.simps
  proper_intrvl.exhaustive.simps
  proper_intrvl.proper_interval_set_aux.simps
  proper_intrvl.proper_interval_set_Compl_aux.simps
  proper_intrvl.proper_interval_Compl_set_aux.simps

context linorder_proper_interval begin

lemma exhaustive_above_iff:
  "⟦ sorted xs; distinct xs; ∀x'∈set xs. x < x' ⟧ ⟹ exhaustive_above x xs ⟷ set xs = {z. z > x}"
proof(induction x xs rule: exhaustive_above.induct)
  case 1 thus ?case by(simp add: proper_interval_simps)
next
  case (2 x y ys)
  from ‹sorted (y # ys)› ‹distinct (y # ys)›
  have ys: "sorted ys" "distinct ys" and y: "∀y'∈set ys. y < y'"
    by(auto simp add: less_le)
  hence "exhaustive_above y ys = (set ys = {z. y < z})" by(rule "2.IH")
  moreover from ‹∀y'∈set (y # ys). x < y'› have "x < y" by simp
  ultimately show ?case using y 
    by(fastforce simp add: proper_interval_simps)
qed

lemma exhaustive_correct:
  assumes "sorted xs" "distinct xs"
  shows "exhaustive xs ⟷ set xs = UNIV"
proof(cases xs)
  case Nil thus ?thesis by auto
next
  case Cons
  show ?thesis using assms unfolding Cons exhaustive.simps
    apply(subst exhaustive_above_iff)
       apply(auto simp add: less_le proper_interval_simps not_less intro: order_antisym)
    done
qed

theorem proper_interval_set_aux:
  assumes fin: "finite (UNIV :: 'a set)"
  and xs: "sorted xs" "distinct xs" 
  and ys: "sorted ys" "distinct ys"
  shows "proper_interval_set_aux xs ys ⟷ (∃A. set xs ⊏' A ∧ A ⊏' set ys)"
proof -
  note [simp] = finite_subset[OF subset_UNIV fin]
  show ?thesis using xs ys
  proof(induction xs ys rule: proper_interval_set_aux.induct)
    case 1 thus ?case by simp
  next
    case (2 y ys)
    hence "∀y'∈set ys. y < y'" by(auto simp add: less_le)
    thus ?case
      by(cases ys)(auto simp add: proper_interval_simps set_less_aux_singleton_iff intro: psubset_finite_imp_set_less_aux)
  next
    case (3 x xs y ys)
    from ‹sorted (x # xs)› ‹distinct (x # xs)›
    have xs: "sorted xs" "distinct xs" and x: "∀x'∈set xs. x < x'"
      by(auto simp add: less_le)
    from ‹sorted (y # ys)› ‹distinct (y # ys)›
    have ys: "sorted ys" "distinct ys" and y: "∀y'∈set ys. y < y'"
      by(auto simp add: less_le)
    have Minxxs: "Min (set (x # xs)) = x" and xnxs: "x ∉ set xs"
      using x by(auto intro!: Min_eqI)
    have Minyys: "Min (set (y # ys)) = y" and ynys: "y ∉ set ys" 
      using y by(auto intro!: Min_eqI)
    show ?case
    proof(cases "x < y")
      case True
      hence "set (y # ys) ⊏' set (x # xs)" using Minxxs Minyys
        by -(rule set_less_aux_Min_antimono, simp_all)
      thus ?thesis using True by(auto dest: set_less_aux_trans set_less_aux_antisym)
    next
      case False
      show ?thesis
      proof(cases "y < x")
        case True
        { assume "proper_interval (Some y) (Some x)"
          then obtain z where z: "y < z" "z < x" by(auto simp add: proper_interval_simps)
          hence "set (x # xs) ⊏' {z}" using x
            by -(rule set_less_aux_Min_antimono, auto)
          moreover have "{z} ⊏' set (y # ys)" using z y Minyys
            by -(rule set_less_aux_Min_antimono, auto)
          ultimately have "∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys)" by blast }
        moreover
        { assume "ys ≠ []"
          hence "{y} ⊏' set (y # ys)" using y
            by -(rule psubset_finite_imp_set_less_aux, auto simp add: neq_Nil_conv)
          moreover have "set (x # xs) ⊏' {y}" using False True x
            by -(rule set_less_aux_Min_antimono, auto)
          ultimately have "∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys)" by blast }
        moreover
        { assume "¬ exhaustive_above x xs"
          then obtain z where z: "z > x" "z ∉ set xs" using x
            by(auto simp add: exhaustive_above_iff[OF xs x])
          let ?A = "insert z (set (x # xs))"
          have "set (x # xs) ⊏' ?A" using z
            by -(rule psubset_finite_imp_set_less_aux, auto)
          moreover have "?A ⊏' set (y # ys)" using Minyys False True z x
            by -(rule set_less_aux_Min_antimono, auto)
          ultimately have "∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys)" by blast }
        moreover
        { fix A
          assume A: "set (x # xs) ⊏' A" and A': "A ⊏' {y}"
            and pi: "¬ proper_interval (Some y) (Some x)"
          from A have nempty: "A ≠ {}" by auto
          have "y ∉ A"
          proof
            assume "y ∈ A"
            moreover with A' have "A ≠ {y}" by auto
            ultimately have "{y} ⊏' A" by -(rule psubset_finite_imp_set_less_aux, auto)
            with A' show False by(rule set_less_aux_antisym)
          qed
          have "y < Min A" unfolding not_le[symmetric]
          proof
            assume "Min A ≤ y"
            moreover have "Min A ≠ y" using ‹y ∉ A› nempty by clarsimp
            ultimately have "Min A < Min {y}" by simp
            hence "{y} ⊏' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
            with A' show False by(rule set_less_aux_antisym)
          qed
          with pi nempty have "x ≤ Min A" by(auto simp add: proper_interval_simps)
          moreover
          from A obtain z where z: "z ∈ A" "z ∉ set (x # xs)"
            by(auto simp add: set_less_aux_def)
          with ‹x ≤ Min A› nempty have "x < z" by auto
          with z have "¬ exhaustive_above x xs"
            by(auto simp add: exhaustive_above_iff[OF xs x]) }
        ultimately show ?thesis using True False by fastforce
      next
        case False
        with ‹¬ x < y› have "x = y" by auto
        from ‹¬ x < y› False
        have "proper_interval_set_aux xs ys = (∃A. set xs ⊏' A ∧ A ⊏' set ys)" 
          using xs ys by(rule "3.IH")
        also have "… = (∃A. set (x # xs) ⊏' A ∧ A ⊏' set (y # ys))"
          (is "?lhs = ?rhs")
        proof
          assume ?lhs
          then obtain A where A: "set xs ⊏' A" 
            and A': "A ⊏' set ys" by blast
          hence nempty: "A ≠ {}" "ys ≠ []" by auto
          let ?A = "insert y A"
          { assume "Min A ≤ y"
            also from y nempty have "y < Min (set ys)" by auto
            finally have "set ys ⊏' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
            with A' have False by(rule set_less_aux_antisym) }
          hence MinA: "y < Min A" by(metis not_le)
          with nempty have "y ∉ A" by auto
          moreover
          with MinA nempty have MinyA: "Min ?A = y" by -(rule Min_eqI, auto)
          ultimately have A1: "set (x # xs) ⊏' ?A" using ‹x = y› A Minxxs xnxs
            by(subst set_less_aux_rec) simp_all
          moreover
          have "?A ⊏' set (y # ys)" using ‹x = y› MinyA ‹y ∉ A› A' Minyys ynys
            by(subst set_less_aux_rec) simp_all
          ultimately show ?rhs by blast
        next
          assume "?rhs"
          then obtain A where A: "set (x # xs) ⊏' A"
            and A': "A ⊏' set (y # ys)" by blast
          let ?A = "A - {x}"
          from A have nempty: "A ≠ {}" by auto
          { assume "x < Min A"
            hence "Min (set (x # xs)) < Min A" unfolding Minxxs .
            hence "A ⊏' set (x # xs)"
              by(rule set_less_aux_Min_antimono) simp_all
            with A have False by(rule set_less_aux_antisym) }
          moreover
          { assume "Min A < x"
            hence "Min A < Min (set (y # ys))" unfolding ‹x = y› Minyys .
            hence "set (y # ys) ⊏' A" by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
            with A' have False by(rule set_less_aux_antisym) }
          ultimately have MinA: "Min A = x" by(metis less_linear)
          hence "x ∈ A" using nempty by(metis Min_in ‹finite A›)
          
          from A nempty Minxxs xnxs have "set xs ⊏' ?A"
            by(subst (asm) set_less_aux_rec)(auto simp add: MinA)
          moreover from A' ‹x = y› nempty Minyys MinA ynys have "?A ⊏' set ys"
            by(subst (asm) set_less_aux_rec) simp_all
          ultimately show ?lhs by blast
        qed
        finally show ?thesis using ‹x = y› by simp
      qed
    qed
  qed
qed

lemma proper_interval_set_Compl_aux:
  assumes fin: "finite (UNIV :: 'a set)"
  and xs: "sorted xs" "distinct xs" 
  and ys: "sorted ys" "distinct ys" 
  shows "proper_interval_set_Compl_aux None 0 xs ys ⟷ (∃A. set xs ⊏' A ∧ A ⊏' - set ys)"
proof -
  note [simp] = finite_subset[OF subset_UNIV fin]

  define above where "above = case_option UNIV (Collect ∘ less)"
  have above_simps [simp]: "above None = UNIV" "⋀x. above (Some x) = {y. x < y}"
    and above_upclosed: "⋀x y ao. ⟦ x ∈ above ao; x < y ⟧ ⟹ y ∈ above ao"
    and proper_interval_Some2: "⋀x ao. proper_interval ao (Some x) ⟷ (∃z∈above ao. z < x)"
    by(simp_all add: proper_interval_simps above_def split: option.splits)

  { fix ao n
    assume "set xs ⊆ above ao" "set ys ⊆ above ao"
    from xs ‹set xs ⊆ above ao› ys ‹set ys ⊆ above ao›
    have "proper_interval_set_Compl_aux ao (card (UNIV - above ao)) xs ys ⟷
          (∃A ⊆ above ao. set xs ⊏' A ∧ A ⊏' - set ys ∩ above ao)"
    proof(induct ao n≡"card (UNIV - above ao)" xs ys rule: proper_interval_set_Compl_aux.induct)
      case (1 ao)
      have "card (UNIV - above ao) + 1 < CARD('a) ⟷ (∃A ⊆ above ao. A ≠ {} ∧ A ⊏' above ao)"
        (is "?lhs ⟷ ?rhs")
      proof
        assume ?lhs
        hence "card (UNIV - (UNIV - above ao)) > 1" by(simp add: card_Diff_subset)
        from card_gt_1D[OF this]
        obtain x y where above: "x ∈ above ao" "y ∈ above ao"
          and neq: "x ≠ y" by blast
        hence "{x} ⊏' {x, y} ∩ above ao"
          by(simp_all add: psubsetI psubset_finite_imp_set_less_aux)
        also have "… ⊑' above ao"
          by(auto intro: subset_finite_imp_set_less_eq_aux)
        finally show ?rhs using above by blast
      next
        assume ?rhs
        then obtain A where nempty: "A ∩ above ao ≠ {}"
          and subset: "A ⊆ above ao"
          and less: "A ⊏' above ao" by blast
        from nempty obtain x where x: "x ∈ A" "x ∈ above ao" by blast
        show ?lhs
        proof(rule ccontr)
          assume "¬ ?lhs"
          moreover have "CARD('a) ≥ card (UNIV - above ao)" by(rule card_mono) simp_all
          moreover from card_Un_disjoint[of "UNIV - above ao" "above ao"]
          have "CARD('a) = card (UNIV - above ao) + card (above ao)" by auto
          ultimately have "card (above ao) = 1" using x
            by(cases "card (above ao)")(auto simp add: not_less_eq less_Suc_eq_le)
          with x have "above ao = {x}" unfolding card_eq_1_iff by auto
          moreover with x subset have A: "A = {x}" by auto
          ultimately show False using less by simp
        qed
      qed
      thus ?case by simp
    next
      case (2 ao y ys)
      note ys = ‹sorted (y # ys)› ‹distinct (y # ys)› ‹set (y # ys) ⊆ above ao›
      have len_ys: "length ys = card (set ys)"
        using ys by(auto simp add: List.card_set intro: sym)

      define m where "m = CARD('a) - card (UNIV - above ao)"
      have "CARD('a) = card (above ao) + card (UNIV - above ao)"
        using card_Un_disjoint[of "above ao" "UNIV - above ao"] by auto
      hence m_eq: "m = card (above ao)" unfolding m_def by simp
        
      have "m ≠ length ys + 1 ∧ (m = length ys + 2 ⟶ ¬ proper_interval (Some (last (y # ys))) None) ⟷
        (∃A ⊆ above ao. A ≠ {} ∧ A ⊏' - set (y # ys) ∩ above ao)" (is "?lhs ⟷ ?rhs")
      proof
        assume ?lhs
        hence m: "m ≠ length ys + 1"
          and pi: "m = length ys + 2 ⟹ ¬ proper_interval (Some (last (y # ys))) None"
          by simp_all
        have "length ys + 1 = card (set (y # ys))" using ys len_ys by simp
        also have "… ≤ m" unfolding m_eq by(rule card_mono)(simp, rule ys)
        finally have "length ys + 2 ≤ m" using m by simp
        show ?rhs
        proof(cases "m = length ys + 2")
          case True
          hence "card (UNIV - (UNIV - above ao) - set (y # ys)) = 1"
            using ys len_ys
            by(subst card_Diff_subset)(auto simp add: m_def card_Diff_subset)
          then obtain z where z: "z ∈ above ao" "z ≠ y" "z ∉ set ys"
            unfolding card_eq_1_iff by auto
          from True have "¬ proper_interval (Some (last (y # ys))) None" by(rule pi)
          hence "z ≤ last (y # ys)" by(simp add: proper_interval_simps not_less del: last.simps)
          moreover have ly: "last (y # ys) ∈ set (y # ys)" by(rule last_in_set) simp
          with z have "z ≠ last (y # ys)" by auto
          ultimately have "z < last (y # ys)" by simp
          hence "{last (y # ys)} ⊏' {z}"
            using z ly ys by(auto 4 3 simp add: set_less_aux_def)
          also have "… ⊑' - set (y # ys) ∩ above ao"
            using z by(auto intro: subset_finite_imp_set_less_eq_aux)
          also have "{last (y # ys)} ≠ {}" using ly ys by blast
          moreover have "{last (y # ys)} ⊆ above ao" using ys by auto
          ultimately show ?thesis by blast
        next
          case False
          with ‹length ys + 2 ≤ m› ys len_ys
          have "card (UNIV - (UNIV - above ao) - set (y # ys)) > 1"
            by(subst card_Diff_subset)(auto simp add: card_Diff_subset m_def)
          from card_gt_1D[OF this]
          obtain x x' where x: "x ∈ above ao" "x ≠ y" "x ∉ set ys"
            and x': "x' ∈ above ao" "x' ≠ y" "x' ∉ set ys"
            and neq: "x ≠ x'" by auto
          hence "{x} ⊏' {x, x'} ∩ above ao"
            by(simp_all add: psubsetI psubset_finite_imp_set_less_aux)
          also have "… ⊑' - set (y # ys) ∩ above ao" using x x' ys
            by(auto intro: subset_finite_imp_set_less_eq_aux)
          also have "{x} ∩ above ao ≠ {}" using x by simp
          ultimately show ?rhs by blast
        qed
      next
        assume ?rhs
        then obtain A where nempty: "A ≠ {}"
          and less: "A ⊏' - set (y # ys) ∩ above ao"
          and subset: "A ⊆ above ao" by blast
        have "card (set (y # ys)) ≤ card (above ao)" using ys(3) by(simp add: card_mono)
        hence "length ys + 1 ≤ m" unfolding m_eq using ys by(simp add: len_ys)
        have "m ≠ length ys + 1"
        proof
          assume "m = length ys + 1"
          hence "card (above ao) ≤ card (set (y # ys))"
            unfolding m_eq using ys len_ys by auto
          from card_seteq[OF _ _ this] ys have "set (y # ys) = above ao" by simp
          with nempty less show False by(auto simp add: set_less_aux_def)
        qed
        moreover
        { assume "m = length ys + 2"
          hence "card (above ao - set (y # ys)) = 1"
            using ys len_ys m_eq by(auto simp add: card_Diff_subset)
          then obtain z where z: "above ao - set (y # ys) = {z}"
            unfolding card_eq_1_iff ..
          hence eq_z: "- set (y # ys) ∩ above ao = {z}" by auto
          with less have "A ⊏' {z}" by simp
          have "¬ proper_interval (Some (last (y # ys))) None"
          proof
            assume "proper_interval (Some (last (y # ys))) None"
            then obtain z' where z': "last (y # ys) < z'"
              by(clarsimp simp add: proper_interval_simps)
            have "last (y # ys) ∈ set (y # ys)" by(rule last_in_set) simp
            with ys z' have "z' ∈ above ao" "z' ∉ set (y # ys)"
              using above_upclosed local.not_less local.sorted_last ys(1) z' by blast+
            with eq_z have "z = z'" by fastforce
            from z' have "⋀x. x ∈ set (y # ys) ⟹ x < z'" using ys
              by(auto dest: sorted_last simp del: sorted_wrt.simps(2))
            with eq_z ‹z = z'›
            have "⋀x. x ∈ above ao ⟹ x ≤ z'" by(fastforce)
            with ‹A ⊏' {z}› nempty ‹z = z'› subset
            show False by(auto simp add: set_less_aux_def)
          qed }
        ultimately show ?lhs by simp
      qed
      thus ?case by(simp add: length_last_def m_def Let_def)
    next
      case (3 ao x xs)
      note xs = ‹sorted (x # xs)› ‹distinct (x # xs)› ‹set (x # xs) ⊆ above ao›
      have len_xs: "length xs = card (set xs)"
        using xs by(auto simp add: List.card_set intro: sym)
      
      define m where "m = CARD('a) - card (UNIV - above ao)"
      have "CARD('a) = card (above ao) + card (UNIV - above ao)"
        using card_Un_disjoint[of "above ao" "UNIV - above ao"] by auto
      hence m_eq: "m = card (above ao)" unfolding m_def by simp
      have "m ≠ length xs + 1 ∧ (m = length xs + 2 ⟶ ¬ proper_interval (Some (last (x # xs))) None) ⟷
        (∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' above ao)" (is "?lhs ⟷ ?rhs")
      proof
        assume ?lhs
        hence m: "m ≠ length xs + 1"
          and pi: "m = length xs + 2 ⟹ ¬ proper_interval (Some (last (x # xs))) None"
          by simp_all
        have "length xs + 1 = card (set (x # xs))" using xs len_xs by simp
        also have "… ≤ m" unfolding m_eq by(rule card_mono)(simp, rule xs)
        finally have "length xs + 2 ≤ m" using m by simp
        show ?rhs
        proof(cases "m = length xs + 2")
          case True
          hence "card (UNIV - (UNIV - above ao) - set (x # xs)) = 1"
            using xs len_xs
            by(subst card_Diff_subset)(auto simp add: m_def card_Diff_subset)
          then obtain z where z: "z ∈ above ao" "z ≠ x" "z ∉ set xs"
            unfolding card_eq_1_iff by auto
          define A where "A = insert z {y. y ∈ set (x # xs) ∧ y < z}"

          from True have "¬ proper_interval (Some (last (x # xs))) None" by(rule pi)
          hence "z ≤ last (x # xs)" by(simp add: proper_interval_simps not_less del: last.simps)
          moreover have lx: "last (x # xs) ∈ set (x # xs)" by(rule last_in_set) simp
          with z have "z ≠ last (x # xs)" by auto
          ultimately have "z < last (x # xs)" by simp
          hence "set (x # xs) ⊏' A" 
            using z xs by(auto simp add: A_def set_less_aux_def intro: rev_bexI[where x=z])
          moreover have "last (x # xs) ∉ A" using xs ‹z < last (x # xs)›
            by(auto simp add: A_def simp del: last.simps)
          hence "A ⊂ insert (last (x # xs)) A" by blast
          hence less': "A ⊏' insert (last (x # xs)) A"
            by(rule psubset_finite_imp_set_less_aux) simp
          have "… ⊆ above ao" using xs lx z
            by(auto simp del: last.simps simp add: A_def)
          hence "insert (last (x # xs)) A ⊑' above ao"
            by(auto intro: subset_finite_imp_set_less_eq_aux)
          with less' have "A ⊏' above ao"
            by(rule set_less_trans_set_less_eq)
          moreover have "A ⊆ above ao" using xs z by(auto simp add: A_def)
          ultimately show ?thesis by blast
        next
          case False
          with ‹length xs + 2 ≤ m› xs len_xs
          have "card (UNIV - (UNIV - above ao) - set (x # xs)) > 1"
            by(subst card_Diff_subset)(auto simp add: card_Diff_subset m_def)
          from card_gt_1D[OF this]
          obtain y y' where y: "y ∈ above ao" "y ≠ x" "y ∉ set xs"
            and y': "y' ∈ above ao" "y' ≠ x" "y' ∉ set xs"
            and neq: "y ≠ y'" by auto
          define A where "A = insert y (set (x # xs) ∩ above ao)"
          hence "set (x # xs) ⊂ A" using y xs by auto
          hence "set (x # xs) ⊏' …"
            by(fastforce intro: psubset_finite_imp_set_less_aux)
          moreover have *: "… ⊂ above ao"
            using y y' neq by(auto simp add: A_def)
          moreover from * have "A ⊏' above ao"
            by(auto intro: psubset_finite_imp_set_less_aux)
          ultimately show ?thesis by blast
        qed
      next
        assume ?rhs
        then obtain A where lessA: "set (x # xs) ⊏' A"
          and Aless: "A ⊏' above ao" and subset: "A ⊆ above ao" by blast
        have "card (set (x # xs)) ≤ card (above ao)" using xs(3) by(simp add: card_mono)
        hence "length xs + 1 ≤ m" unfolding m_eq using xs by(simp add: len_xs)
        have "m ≠ length xs + 1"
        proof
          assume "m = length xs + 1"
          hence "card (above ao) ≤ card (set (x # xs))"
            unfolding m_eq using xs len_xs by auto
          from card_seteq[OF _ _ this] xs have "set (x # xs) = above ao" by simp
          with lessA Aless show False by(auto dest: set_less_aux_antisym)
        qed
        moreover
        { assume "m = length xs + 2"
          hence "card (above ao - set (x # xs)) = 1"
            using xs len_xs m_eq by(auto simp add: card_Diff_subset)
          then obtain z where z: "above ao - set (x # xs) = {z}"
            unfolding card_eq_1_iff ..
          have "¬ proper_interval (Some (last (x # xs))) None"
          proof
            assume "proper_interval (Some (last (x # xs))) None"
            then obtain z' where z': "last (x # xs) < z'"
              by(clarsimp simp add: proper_interval_simps)
            have "last (x # xs) ∈ set (x # xs)" by(rule last_in_set) simp
            with xs z' have "z' ∈ above ao" "z' ∉ set (x # xs)"
              by(auto simp del: last.simps sorted_wrt.simps(2) intro: above_upclosed dest: sorted_last)
            with z have "z = z'" by fastforce
            from z' have y_less: "⋀y. y ∈ set (x # xs) ⟹ y < z'" using xs
              by(auto simp del: sorted_wrt.simps(2) dest: sorted_last)
            with z ‹z = z'› have "⋀y. y ∈ above ao ⟹ y ≤ z'" by(fastforce)
            
            from lessA subset obtain y where y: "y ∈ A" "y ∈ above ao" "y ∉ set (x # xs)"
              and min: "⋀y'. ⟦ y' ∈ set (x # xs); y' ∈ above ao; y' ∉ A ⟧ ⟹ y ≤ y'"
              by(auto simp add: set_less_aux_def)
            with z ‹z = z'› have "y = z'" by auto
            have "set (x # xs) ⊆ A"
            proof
              fix y'
              assume y': "y' ∈ set (x # xs)"
              show "y' ∈ A"
              proof(rule ccontr)
                assume "y' ∉ A"
                from y' xs have "y' ∈ above ao" by auto
                with y' have "y ≤ y'" using ‹y' ∉ A› by(rule min)
                moreover from y' have "y' < z'" by(rule y_less)
                ultimately show False using ‹y = z'› by simp
              qed
            qed
            moreover from z xs have "above ao = insert z (set (x # xs))" by auto
            ultimately have "A = above ao" using y ‹y = z'› ‹z = z'› subset by auto
            with Aless show False by simp
          qed }
        ultimately show ?lhs by simp
      qed
      thus ?case by(simp add: length_last_def m_def Let_def del: last.simps)
    next
      case (4 ao x xs y ys)
      note xxs = ‹sorted (x # xs)› ‹distinct (x # xs)›
        and yys = ‹sorted (y # ys)› ‹distinct (y # ys)›
        and xxs_above = ‹set (x # xs) ⊆ above ao›
        and yys_above = ‹set (y # ys) ⊆ above ao›
      from xxs have xs: "sorted xs" "distinct xs" and x_Min: "∀x'∈set xs. x < x'"
        by(auto simp add: less_le)
      from yys have ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"
        by(auto simp add: less_le)

      have len_xs: "length xs = card (set xs)"
        using xs by(auto simp add: List.card_set intro: sym)
      have len_ys: "length ys = card (set ys)"
        using ys by(auto simp add: List.card_set intro: sym)

      show ?case
      proof(cases "x < y")
        case True

        have "proper_interval ao (Some x) ∨
          proper_interval_set_Compl_aux (Some x) (card (UNIV - above ao) + 1) xs (y # ys) ⟷
          (∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' - set (y # ys) ∩ above ao)"
          (is "?lhs ⟷ ?rhs")
        proof(cases "proper_interval ao (Some x)")
          case True
          then obtain z where z: "z ∈ above ao" "z < x"
            by(clarsimp simp add: proper_interval_Some2)
          moreover with xxs have "∀x'∈set xs. z < x'" by(auto)
          ultimately have "set (x # xs) ⊏' {z}"
            by(auto simp add: set_less_aux_def intro!: bexI[where x=z])
          moreover {
            from z yys ‹x < y› have "z < y" "∀y'∈set ys. z < y'"
              by(auto)
            hence subset: "{z} ⊆ - set (y # ys) ∩ above ao"
              using ys ‹x < y› z by auto
            moreover have "x ∈ …" using yys xxs ‹x < y› xxs_above by(auto)
            ultimately have "{z} ⊂ …" using ‹z < x› by fastforce
            hence "{z} ⊏' …"
              by(fastforce intro: psubset_finite_imp_set_less_aux) }
          moreover have "{z} ⊆ above ao" using z by simp
          ultimately have ?rhs by blast
          thus ?thesis using True by simp
        next
          case False
          hence above_eq: "above ao = insert x (above (Some x))" using xxs_above
            by(auto simp add: proper_interval_Some2 intro: above_upclosed)
          moreover have "card (above (Some x)) < CARD('a)"
            by(rule psubset_card_mono)(auto)
          ultimately have card_eq: "card (UNIV - above ao) + 1 = card (UNIV - above (Some x))"
            by(simp add: card_Diff_subset)
          from xxs_above x_Min have xs_above: "set xs ⊆ above (Some x)" by(auto)
          from ‹x < y› y_Min have "set (y # ys) ⊆ above (Some x)" by(auto)
          with ‹x < y› card_eq xs xs_above yys
          have "proper_interval_set_Compl_aux (Some x) (card (UNIV - above ao) + 1) xs (y # ys) ⟷
               (∃A ⊆ above (Some x). set xs ⊏' A ∧ A ⊏' - set (y # ys) ∩ above (Some x))"
            by(subst card_eq)(rule 4)
          also have "… ⟷ ?rhs" (is "?lhs' ⟷ _")
          proof
            assume ?lhs'
            then obtain A where less_A: "set xs ⊏' A"
              and A_less: "A ⊏' - set (y # ys) ∩ above (Some x)"
              and subset: "A ⊆ above (Some x)" by blast
            let ?A = "insert x A"

            have Min_A': "Min ?A = x" using xxs_above False subset
              by(auto intro!: Min_eqI simp add: proper_interval_Some2)
            moreover have "Min (set (x # xs)) = x"
              using x_Min by(auto intro!: Min_eqI)
            moreover have Amx: "A - {x} = A"
              using False subset 
              by(auto simp add: proper_interval_Some2 intro: above_upclosed)
            moreover have "set xs - {x} = set xs" using x_Min by auto
            ultimately have less_A': "set (x # xs) ⊏' ?A"
              using less_A xxs_above x_Min by(subst set_less_aux_rec) simp_all
            
            have "x ∈ - insert y (set ys) ∩ above ao"
              using ‹x < y› xxs_above y_Min by auto
            hence "- insert y (set ys) ∩ above ao ≠ {}" by auto
            moreover have "Min (- insert y (set ys) ∩ above ao) = x"
              using yys y_Min xxs_above ‹x < y› False
              by(auto intro!: Min_eqI simp add: proper_interval_Some2)
            moreover have "- set (y # ys) ∩ above ao - {x} = - set (y # ys) ∩ above (Some x)"
              using yys_above False xxs_above
              by(auto simp add: proper_interval_Some2 intro: above_upclosed)
            ultimately have A'_less: "?A ⊏' - set (y # ys) ∩ above ao"
              using Min_A' A_less Amx xxs_above by(subst set_less_aux_rec) simp_all
            moreover have "?A ⊆ above ao" using subset xxs_above by(auto intro: above_upclosed)
            ultimately show ?rhs using less_A' by blast
          next
            assume ?rhs
            then obtain A where less_A: "set (x # xs) ⊏' A"
              and A_less: "A ⊏' - set (y # ys) ∩ above ao" 
              and subset: "A ⊆ above ao" by blast
            let ?A = "A - {x}"

            from less_A subset xxs_above have "set (x # xs) ∩ above ao ⊏' A ∩ above ao"
              by(simp add: Int_absorb2)
            with False xxs_above subset have "x ∈ A"
              by(auto simp add: set_less_aux_def proper_interval_Some2)
            hence "… ≠ {}" by auto
            moreover from ‹x ∈ A› False subset
            have Min_A: "Min A = x"
              by(auto intro!: Min_eqI simp add: proper_interval_Some2 not_less)
            moreover have "Min (set (x # xs)) = x"
              using x_Min by(auto intro!: Min_eqI)
            moreover have eq_A: "?A ⊆ above (Some x)"
              using xxs_above False subset 
              by(fastforce simp add: proper_interval_Some2 not_less intro: above_upclosed)
            moreover have "set xs - {x} = set xs"
              using x_Min by(auto)
            ultimately have less_A': "set xs ⊏' ?A"
              using xxs_above less_A by(subst (asm) set_less_aux_rec)(simp_all cong: conj_cong)
            
            have "x ∈ - insert y (set ys) ∩ above ao"
              using ‹x < y› xxs_above y_Min by auto
            hence "- insert y (set ys) ∩ above ao ≠ {}" by auto
            moreover have "Min (- set (y # ys) ∩ above ao) = x"
              using yys y_Min xxs_above ‹x < y› False
              by(auto intro!: Min_eqI simp add: proper_interval_Some2)
            moreover have "- set (y # ys) ∩ above (Some x) = - set (y # ys) ∩ above ao - {x}"
              by(auto simp add: above_eq)
            ultimately have "?A ⊏' - set (y # ys) ∩ above (Some x)"
              using A_less ‹A ≠ {}› eq_A Min_A
              by(subst (asm) set_less_aux_rec) simp_all
            
            with less_A' eq_A show ?lhs' by blast
          qed
          finally show ?thesis using False by simp
        qed
        thus ?thesis using True by simp
      next
        case False
        show ?thesis
        proof(cases "y < x")
          case True
          have "proper_interval ao (Some y) ∨ 
                proper_interval_set_Compl_aux (Some y) (card (UNIV - above ao) + 1) (x # xs) ys ⟷
               (∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' - set (y # ys) ∩ above ao)"
            (is "?lhs ⟷ ?rhs")
          proof(cases "proper_interval ao (Some y)")
            case True
            then obtain z where z: "z ∈ above ao" "z < y"
              by(clarsimp simp add: proper_interval_Some2)
            from xxs ‹y < x› have "∀x'∈set (x # xs). y < x'" by(auto)
            hence less_A: "set (x # xs) ⊏' {y}" 
              by(auto simp add: set_less_aux_def intro!: bexI[where x=y])

            have "{y} ⊏' {z}"
              using z y_Min by(auto simp add: set_less_aux_def intro: bexI[where x=z])
            also have "… ⊆ - set (y # ys) ∩ above ao" using z y_Min by auto
            hence "{z} ⊑' …" by(auto intro: subset_finite_imp_set_less_eq_aux)
            finally have "{y} ⊏' …" .
            moreover have "{y} ⊆ above ao" using yys_above by auto
            ultimately have ?rhs using less_A by blast
            thus ?thesis using True by simp
          next
            case False
            hence above_eq: "above ao = insert y (above (Some y))" using yys_above
              by(auto simp add: proper_interval_Some2 intro: above_upclosed)
            moreover have "card (above (Some y)) < CARD('a)"
              by(rule psubset_card_mono)(auto)
            ultimately have card_eq: "card (UNIV - above ao) + 1 = card (UNIV - above (Some y))"
              by(simp add: card_Diff_subset)
            from yys_above y_Min have ys_above: "set ys ⊆ above (Some y)" by(auto)

            have eq_ys: "- set ys ∩ above (Some y) = - set (y # ys) ∩ above ao"
              by(auto simp add: above_eq)

            from ‹y < x› x_Min have "set (x # xs) ⊆ above (Some y)" by(auto)
            with ‹¬ x < y› ‹y < x› card_eq xxs ys ys_above
            have "proper_interval_set_Compl_aux (Some y) (card (UNIV - above ao) + 1) (x # xs) ys ⟷
              (∃A ⊆ above (Some y). set (x # xs) ⊏' A ∧ A ⊏' - set ys ∩ above (Some y))"
              by(subst card_eq)(rule 4)
            also have "… ⟷ ?rhs" (is "?lhs' ⟷ _")
            proof
              assume ?lhs'
              then obtain A where "set (x # xs) ⊏' A" and subset: "A ⊆ above (Some y)"
                and "A ⊏' - set ys ∩ above (Some y)" by blast
              moreover from subset have "A - {y} = A" by auto
              ultimately have "set (x # xs) ⊏' A - {y}"
                and "A - {y} ⊏' - set (y # ys) ∩ above ao"
                using eq_ys by simp_all
              moreover from subset have "A - {y} ⊆ above ao"
                using yys_above by(auto intro: above_upclosed)
              ultimately show ?rhs by blast
            next
              assume ?rhs
              then obtain A where "set (x # xs) ⊏' A" 
                and A_less: "A ⊏' - set (y # ys) ∩ above ao" 
                and subset: "A ⊆ above ao" by blast
              moreover
              from A_less False yys_above have "y ∉ A"
                by(auto simp add: set_less_aux_def proper_interval_Some2 not_less)
              ultimately have "set (x # xs) ⊏' A"
                and "A ⊏' - set ys ∩ above (Some y)"
                using eq_ys by simp_all
              moreover from ‹y ∉ A› subset above_eq have "A ⊆ above (Some y)" by auto
              ultimately show ?lhs' by blast
            qed
            finally show ?thesis using False by simp
          qed
          with False True show ?thesis by simp
        next
          case False
          with ‹¬ x < y› have "x = y" by simp
          have "proper_interval ao (Some x) ∧ 
                (CARD('a) - (card (UNIV - above ao) + length ys) ≠ 2 ∨
                 CARD('a) - (card (UNIV - above ao) + length xs) ≠ 2) ⟷
               (∃A ⊆ above ao. set (x # xs) ⊏' A ∧ A ⊏' - set (y # ys) ∩ above ao)"
            (is "?below ∧ ?card ⟷ ?rhs")
          proof(cases "?below")
            case False
            hence "- set (y # ys) ∩ above ao ⊏' set (x # xs)"
              using ‹x = y› yys_above xxs_above y_Min
              by(auto simp add: not_less set_less_aux_def proper_interval_Some2 intro!: bexI[where x=y])
            with False show ?thesis by(auto dest: set_less_aux_trans)
          next
            case True
            then obtain z where z: "z ∈ above ao" "z < x"
              by(clarsimp simp add: proper_interval_Some2)

            have "?card ⟷ ?rhs"
            proof
              assume ?rhs
              then obtain A where less_A: "set (x # xs)  ⊏' A"
                and A_less: "A ⊏' - set (y # ys) ∩ above ao"
                and subset: "A ⊆ above ao" by blast

              { 
                assume c_ys: "CARD('a) - (card (UNIV - above ao) + length ys) = 2"
                  and c_xs: "CARD('a) - (card (UNIV - above ao) + length xs) = 2"
                from c_ys yys_above len_ys y_Min have "card (UNIV - (UNIV - above ao) - set (y # ys)) = 1"
                  by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
                then obtain z' where eq_y: "- set (y # ys) ∩ above ao = {z'}"
                  unfolding card_eq_1_iff by auto
                moreover from z have "z ∉ set (y # ys)" using ‹x = y› y_Min by auto
                ultimately have "z' = z" using z by fastforce
                
                from c_xs xxs_above len_xs x_Min have "card (UNIV - (UNIV - above ao) - set (x # xs)) = 1"
                  by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
                then obtain z'' where eq_x: "- set (x # xs) ∩ above ao = {z''}"
                  unfolding card_eq_1_iff by auto
                moreover from z have "z ∉ set (x # xs)" using x_Min by auto
                ultimately have "z'' = z" using z by fastforce

                from less_A subset obtain q where "q ∈ A" "q ∈ above ao" "q ∉ set (x # xs)"
                  by(auto simp add: set_less_aux_def)
                hence "q ∈ {z''}" unfolding eq_x[symmetric] by simp
                hence "q = z''" by simp
                with ‹q ∈ A› ‹z' = z› ‹z'' = z› z 
                have "- set (y # ys) ∩ above ao ⊆ A"
                  unfolding eq_y by simp
                hence "- set (y # ys) ∩ above ao ⊑' A"
                  by(auto intro: subset_finite_imp_set_less_eq_aux)
                with A_less have False by(auto dest: set_less_trans_set_less_eq) }
              thus ?card by auto
            next
              assume ?card (is "?card_ys ∨ ?card_xs")
              thus ?rhs
              proof
                assume ?card_ys
                let ?YS = "UNIV - (UNIV - above ao) - set (y # ys)"
                from ‹?card_ys› yys_above len_ys y_Min have "card ?YS ≠ 1" 
                  by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
                moreover have "?YS ≠ {}" using True y_Min yys_above ‹x = y›
                  by(fastforce simp add: proper_interval_Some2)
                hence "card ?YS ≠ 0" by simp
                ultimately have "card ?YS > 1" by(cases "card ?YS") simp_all
                from card_gt_1D[OF this] obtain x' y' 
                  where x': "x' ∈ above ao" "x' ∉ set (y # ys)"
                  and y': "y' ∈ above ao" "y' ∉ set (y # ys)"
                  and neq: "x' ≠ y'" by auto
                let ?A = "{z}"
                have "set (x # xs) ⊏' ?A" using z x_Min
                  by(auto simp add: set_less_aux_def intro!: rev_bexI)
                moreover
                { have "?A ⊆ - set (y # ys) ∩ above ao"
                    using z ‹x = y› y_Min by(auto)
                  moreover have "x' ∉ ?A ∨ y' ∉ ?A" using neq by auto
                  with x' y' have "?A ≠ - set (y # ys) ∩ above ao" by auto
                  ultimately have "?A ⊂ - set (y # ys) ∩ above ao" by(rule psubsetI)
                  hence "?A ⊏' …" by(fastforce intro: psubset_finite_imp_set_less_aux) } 
                ultimately show ?thesis using z by blast
              next
                assume ?card_xs
                let ?XS = "UNIV - (UNIV - above ao) - set (x # xs)"
                from ‹?card_xs› xxs_above len_xs x_Min have "card ?XS ≠ 1" 
                  by(subst card_Diff_subset)(auto simp add: card_Diff_subset)
                moreover have "?XS ≠ {}" using True x_Min xxs_above
                  by(fastforce simp add: proper_interval_Some2)
                hence "card ?XS ≠ 0" by simp
                ultimately have "card ?XS > 1" by(cases "card ?XS") simp_all
                from card_gt_1D[OF this] obtain x' y' 
                  where x': "x' ∈ above ao" "x' ∉ set (x # xs)"
                  and y': "y' ∈ above ao" "y' ∉ set (x # xs)"
                  and neq: "x' ≠ y'" by auto

                define A
                  where "A = (if x' = Min (above ao) then insert y' (set (x # xs)) else insert x' (set (x # xs)))"
                hence "set (x # xs) ⊆ A" by auto
                moreover have "set (x # xs) ≠ …"
                  using neq x' y' by(auto simp add: A_def)
                ultimately have "set (x # xs) ⊂ A" ..
                hence "set (x # xs) ⊏' …"
                  by(fastforce intro: psubset_finite_imp_set_less_aux)
                moreover {
                  have nempty: "above ao ≠ {}" using z by auto
                  have "A ⊏' {Min (above ao)}" 
                    using z x' y' neq ‹x = y› x_Min xxs_above
                    by(auto 6 4 simp add: set_less_aux_def A_def nempty intro!: rev_bexI Min_eqI)
                  also have "Min (above ao) ≤ z" using z by(simp)
                  hence "Min (above ao) < x" using ‹z < x› by(rule le_less_trans)
                  with ‹x = y› y_Min have "Min (above ao) ∉ set (y # ys)" by auto
                  hence "{Min (above ao)} ⊆ - set (y # ys) ∩ above ao"
                    by(auto simp add: nempty)
                  hence "{Min (above ao)} ⊑' …" by(auto intro: subset_finite_imp_set_less_eq_aux)
                  finally have "A ⊏' …" . }
                moreover have "A ⊆ above ao" using xxs_above yys_above x' y' 
                  by(auto simp add: A_def)
                ultimately show ?rhs by blast
              qed
            qed
            thus ?thesis using True by simp
          qed            
          thus ?thesis using ‹x = y› by simp
        qed
      qed
    qed }
  from this[of None]
  show ?thesis by(simp)
qed

lemma proper_interval_Compl_set_aux:
  assumes fin: "finite (UNIV :: 'a set)"
  and xs: "sorted xs" "distinct xs" 
  and ys: "sorted ys" "distinct ys" 
  shows "proper_interval_Compl_set_aux None xs ys ⟷ (∃A. - set xs ⊏' A ∧ A ⊏' set ys)"
proof -
  note [simp] = finite_subset[OF subset_UNIV fin]

  define above where "above = case_option UNIV (Collect ∘ less)"
  have above_simps [simp]: "above None = UNIV" "⋀x. above (Some x) = {y. x < y}"
    and above_upclosed: "⋀x y ao. ⟦ x ∈ above ao; x < y ⟧ ⟹ y ∈ above ao"
    and proper_interval_Some2: "⋀x ao. proper_interval ao (Some x) ⟷ (∃z∈above ao. z < x)"
    by(simp_all add: proper_interval_simps above_def split: option.splits)

  { fix ao n
    assume "set xs ⊆ above ao" "set ys ⊆ above ao"
    from xs ‹set xs ⊆ above ao› ys ‹set ys ⊆ above ao›
    have "proper_interval_Compl_set_aux ao xs ys ⟷
          (∃A. - set xs ∩ above ao ⊏' A ∩ above ao ∧ A ∩ above ao ⊏' set ys ∩ above ao)"
    proof(induction ao xs ys rule: proper_interval_Compl_set_aux.induct)
      case ("2_1" ao ys)
      { fix A
        assume "above ao ⊏' A ∩ above ao"
        also have "… ⊆ above ao" by simp
        hence "A ∩ above ao ⊑' above ao"
          by(auto intro: subset_finite_imp_set_less_eq_aux)
        finally have False by simp }
      thus ?case by auto
    next
      case ("2_2" ao xs) thus ?case by simp
    next
      case (1 ao x xs y ys)
      note xxs = ‹sorted (x # xs)› ‹distinct (x # xs)›
      hence xs: "sorted xs" "distinct xs" and x_Min: "∀x' ∈ set xs. x < x'"
        by(auto simp add: less_le)
      note yys = ‹sorted (y # ys)› ‹distinct (y # ys)›
      hence ys: "sorted ys" "distinct ys" and y_Min: "∀y'∈set ys. y < y'"
        by(auto simp add: less_le)
      note xxs_above = ‹set (x # xs) ⊆ above ao›
      note yys_above = ‹set (y # ys) ⊆ above ao›

      show ?case
      proof(cases "x < y")
        case True
        have "¬ proper_interval ao (Some x) ∧ proper_interval_Compl_set_aux (Some x) xs (y # ys) ⟷
              (∃A. - set (x # xs) ∩ above ao ⊏' A ∩ above ao ∧ A ∩ above ao ⊏' set (y # ys) ∩ above ao)"
          (is "?lhs ⟷ ?rhs")
        proof(cases "proper_interval ao (Some x)")
          case True
          then obtain z where z: "z < x" "z ∈ above ao"
            by(auto simp add: proper_interval_Some2)
          hence nempty: "above ao ≠ {}" by auto
          with z have "Min (above ao) ≤ z" by auto
          hence "Min (above ao) < x" using ‹z < x› by(rule le_less_trans)
          hence "set (y # ys) ∩ above ao ⊏' - set (x # xs) ∩ above ao"
            using y_Min x_Min z ‹x < y›
            by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
          thus ?thesis using True by(auto dest: set_less_aux_trans set_less_aux_antisym)
        next
          case False
          hence above_eq: "above ao = insert x (above (Some x))"
            using xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed)
          from x_Min have xs_above: "set xs ⊆ above (Some x)" by auto
          from ‹x < y› y_Min have ys_above: "set (y # ys) ⊆ above (Some x)" by auto

          have eq_xs: "- set xs ∩ above (Some x) = - set (x # xs) ∩ above ao"
            using above_eq by auto
          have eq_ys: "set (y # ys) ∩ above (Some x) = set (y # ys) ∩ above ao"
            using y_Min ‹x < y› xxs_above by(auto intro: above_upclosed)
          
          from ‹x < y› xs xs_above yys ys_above
          have "proper_interval_Compl_set_aux (Some x) xs (y # ys) ⟷
               (∃A. - set xs ∩ above (Some x) ⊏' A ∩ above (Some x) ∧
                    A ∩ above (Some x) ⊏' set (y # ys) ∩ above (Some x))"
            by(rule "1.IH")
          also have "… ⟷ ?rhs" (is "?lhs ⟷ _")
          proof
            assume ?lhs
            then obtain A where "- set xs ∩ above (Some x) ⊏' A ∩ above (Some x)"
              and "A ∩ above (Some x) ⊏' set (y # ys) ∩ above (Some x)" by blast
            moreover have "A ∩ above (Some x) = (A - {x}) ∩ above ao"
              using above_eq by auto
            ultimately have "- set (x # xs) ∩ above ao ⊏' (A - {x}) ∩ above ao"
              and "(A - {x}) ∩ above ao ⊏' set (y # ys) ∩ above ao"
              using eq_xs eq_ys by simp_all
            thus ?rhs by blast
          next
            assume ?rhs
            then obtain A where "- set (x # xs) ∩ above ao ⊏' A ∩ above ao"
              and A_less: "A ∩ above ao ⊏' set (y # ys) ∩ above ao" by blast
            moreover have "x ∉ A"
            proof
              assume "x ∈ A"
              hence "set (y # ys) ∩ above ao ⊏' A ∩ above ao"
                using y_Min ‹x < y› by(auto simp add: above_eq set_less_aux_def intro!: bexI[where x=x])
              with A_less show False by(auto dest: set_less_aux_antisym)
            qed
            hence "A ∩ above ao = A ∩ above (Some x)" using above_eq by auto
            ultimately show ?lhs using eq_xs eq_ys by auto
          qed
          finally show ?thesis using False by simp
        qed
        thus ?thesis using True by simp
      next
        case False
        show ?thesis
        proof(cases "y < x")
          case True
          show ?thesis (is "?lhs ⟷ ?rhs")
          proof(cases "proper_interval ao (Some y)")
            case True
            then obtain z where z: "z < y" "z ∈ above ao"
              by(auto simp add: proper_interval_Some2)
            hence nempty: "above ao ≠ {}" by auto
            with z have "Min (above ao) ≤ z" by auto
            hence "Min (above ao) < y" using ‹z < y› by(rule le_less_trans)
            hence "set (y # ys) ∩ above ao ⊏' - set (x # xs) ∩ above ao"
              using y_Min x_Min z ‹y < x›
              by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
            thus ?thesis using True ‹y < x› by(auto dest: set_less_aux_trans set_less_aux_antisym)
          next
            case False
            hence above_eq: "above ao = insert y (above (Some y))"
              using yys_above by(auto simp add: proper_interval_Some2 intro: above_upclosed)
            from y_Min have ys_above: "set ys ⊆ above (Some y)" by auto
            from ‹y < x› x_Min have xs_above: "set (x # xs) ⊆ above (Some y)" by auto

            have "y ∈ - set (x # xs) ∩ above ao" using ‹y < x› x_Min yys_above by auto
            hence nempty: "- set (x # xs) ∩ above ao ≠ {}" by auto
            have Min_x: "Min (- set (x # xs) ∩ above ao) = y"
              using above_eq ‹y < x› x_Min by(auto intro!: Min_eqI)
            have Min_y: "Min (set (y # ys) ∩ above ao) = y"
              using y_Min above_eq by(auto intro!: Min_eqI)
            have eq_xs: "- set (x # xs) ∩ above ao - {y} = - set (x # xs) ∩ above (Some y)"
                by(auto simp add: above_eq)
            have eq_ys: "set ys ∩ above ao - {y} = set ys ∩ above (Some y)"
              using y_Min above_eq by auto

            from ‹¬ x < y› ‹y < x› xxs xs_above ys ys_above
            have "proper_interval_Compl_set_aux (Some y) (x # xs) ys ⟷
                 (∃A. - set (x # xs) ∩ above (Some y) ⊏' A ∩ above (Some y) ∧
                      A ∩ above (Some y) ⊏' set ys ∩ above (Some y))"
              by(rule "1.IH")
            also have "… ⟷ ?rhs" (is "?lhs' ⟷ _")
            proof
              assume ?lhs'
              then obtain A where less_A: "- set (x # xs) ∩ above (Some y) ⊏' A ∩ above (Some y)"
                and A_less: "A ∩ above (Some y) ⊏' set ys ∩ above (Some y)" by blast
              let ?A = "insert y A"

              have Min_A: "Min (?A ∩ above ao) = y"
                using above_eq by(auto intro!: Min_eqI)
              moreover have A_eq: "A ∩ above ao - {y} = A ∩ above (Some y)"
                using above_eq by auto
              ultimately have less_A': "- set (x # xs) ∩ above ao ⊏' ?A ∩ above ao"
                using nempty yys_above less_A Min_x eq_xs by(subst set_less_aux_rec) simp_all

              have A'_less: "?A ∩ above ao ⊏' set (y # ys) ∩ above ao"
                using yys_above nempty Min_A A_eq A_less Min_y eq_ys
                by(subst set_less_aux_rec) simp_all
              
              with less_A' show ?rhs by blast
            next
              assume ?rhs
              then obtain A where less_A: "- set (x # xs) ∩ above ao ⊏' A ∩ above ao"
                and A_less: "A ∩ above ao ⊏' set (y # ys) ∩ above ao" by blast

              from less_A have nempty': "A ∩ above ao ≠ {}" by auto
              moreover have A_eq: "A ∩ above ao - {y} = A ∩ above (Some y)"
                using above_eq by auto
              moreover have y_in_xxs: "y ∈ - set (x # xs) ∩ above ao"
                using ‹y < x› x_Min yys_above by auto
              moreover have "y ∈ A"
              proof(rule ccontr)
                assume "y ∉ A"
                hence "A ∩ above ao ⊏' - set (x # xs) ∩ above ao"
                  using ‹y < x› x_Min y_in_xxs
                  by(auto simp add: set_less_aux_def above_eq intro: bexI[where x=y])
                with less_A show False by(rule set_less_aux_antisym)
              qed
              hence Min_A: "Min (A ∩ above ao) = y" using above_eq y_Min by(auto intro!: Min_eqI)
              ultimately have less_A': "- set (x # xs) ∩ above (Some y) ⊏' A ∩ above (Some y)"
                using nempty less_A Min_x eq_xs
                by(subst (asm) set_less_aux_rec)(auto dest: bspec[where x=y])
              
              have A'_less: "A ∩ above (Some y) ⊏' set ys ∩ above (Some y)"
                using A_less nempty' yys_above Min_A Min_y A_eq eq_ys
                by(subst (asm) set_less_aux_rec) simp_all
              with less_A' show ?lhs' by blast
            qed
            finally show ?thesis using ‹¬ x < y› ‹y < x› False by simp
          qed
        next
          case False
          with ‹¬ x < y› have "x = y" by auto
          thus ?thesis (is "?lhs ⟷ ?rhs")
          proof(cases "proper_interval ao (Some x)")
            case True
            then obtain z where z: "z < x" "z ∈ above ao"
              by(auto simp add: proper_interval_Some2)
            hence nempty: "above ao ≠ {}" by auto
            with z have "Min (above ao) ≤ z" by auto
            hence "Min (above ao) < x" using ‹z < x› by(rule le_less_trans)
            hence "set (y # ys) ∩ above ao ⊏' - set (x # xs) ∩ above ao"
              using y_Min x_Min z ‹x = y›
              by(fastforce simp add: set_less_aux_def nempty intro!: Min_eqI bexI[where x="Min (above ao)"])
            thus ?thesis using True ‹x = y› by(auto dest: set_less_aux_trans set_less_aux_antisym)
          next
            case False
            hence above_eq: "above ao = insert x (above (Some x))"
              using xxs_above by(auto simp add: proper_interval_Some2 intro: above_upclosed)

            have "(ys = [] ⟶ xs ≠ []) ⟷ ?rhs" (is "?lhs' ⟷ _")
            proof(intro iffI strip notI)
              assume ?lhs'
              show ?rhs
              proof(cases ys)
                case Nil
                with ‹?lhs'› obtain x' xs' where xs_eq: "xs = x' # xs'"
                  by(auto simp add: neq_Nil_conv)
                with xs have x'_Min: "∀x'' ∈ set xs'. x' < x''"
                  by(auto simp add: less_le)
                let ?A = "- set (x # xs')"
                have "- set (x # xs) ∩ above ao ⊆ ?A ∩ above ao"
                  using xs_eq by auto
                moreover have "x' ∉ - set (x # xs) ∩ above ao" "x' ∈ ?A ∩ above ao"
                  using xs_eq xxs_above x'_Min x_Min by auto
                ultimately have "- set (x # xs) ∩ above ao ⊂ ?A ∩ above ao"
                  by blast
                hence "- set (x # xs) ∩ above ao ⊏' … "
                  by(fastforce intro: psubset_finite_imp_set_less_aux)
                moreover have "… ⊏' set (y # ys) ∩ above ao" 
                  using Nil ‹x = y› by(auto simp add: set_less_aux_def above_eq)
                ultimately show ?thesis by blast
              next
                case (Cons y' ys')
                let ?A = "{y}"
                have "- set (x # xs) ∩ above ao ⊏' ?A ∩ above ao"
                  using ‹x = y› x_Min by(auto simp add: set_less_aux_def above_eq)
                moreover have "… ⊂ set (y # ys) ∩ above ao"
                  using yys_above yys Cons by auto
                hence "?A ∩ above ao ⊏' …" by(fastforce intro: psubset_finite_imp_set_less_aux)
                ultimately show ?thesis by blast
              qed
            next
              assume Nil: "ys = []" "xs = []" and ?rhs
              then obtain A where less_A: "- {x} ∩ above ao ⊏' A ∩ above ao" 
                and A_less: "A ∩ above ao ⊏' {x}" using ‹x = y› above_eq by auto
              have "x ∉ A" using A_less by(auto simp add: set_less_aux_def above_eq)
              hence "A ∩ above ao ⊆ - {x} ∩ above ao" by auto
              hence "A ∩ above ao ⊑' …" by(auto intro: subset_finite_imp_set_less_eq_aux)
              with less_A have "… ⊏' …" by(rule set_less_trans_set_less_eq)
              thus False by simp
            qed
            with ‹x = y› False show ?thesis by simp
          qed
        qed
      qed
    qed }
  from this[of None] show ?thesis by simp
qed

end

subsection ‹Proper intervals for HOL types›

instantiation unit :: proper_interval begin
fun proper_interval_unit :: "unit proper_interval" where
  "proper_interval_unit None None = True"
| "proper_interval_unit _ _ = False"
instance by intro_classes auto
end

instantiation bool :: proper_interval begin
fun proper_interval_bool :: "bool proper_interval" where
  "proper_interval_bool (Some x) (Some y) ⟷ False"
| "proper_interval_bool (Some x) None ⟷ ¬ x"
| "proper_interval_bool None (Some y) ⟷ y"
| "proper_interval_bool None None = True"
instance by intro_classes auto
end

instantiation nat :: proper_interval begin
fun proper_interval_nat :: "nat proper_interval" where
  "proper_interval_nat no None = True"
| "proper_interval_nat None (Some x) ⟷ x > 0"
| "proper_interval_nat (Some x) (Some y) ⟷ y - x > 1"
instance by intro_classes auto
end

instantiation int :: proper_interval begin
fun proper_interval_int :: "int proper_interval" where
  "proper_interval_int (Some x) (Some y) ⟷ y - x > 1"
| "proper_interval_int _ _ = True"
instance by intro_classes (auto intro: less_add_one, metis less_add_one minus_less_iff)
end

instantiation integer :: proper_interval begin
context includes integer.lifting begin
lift_definition proper_interval_integer :: "integer proper_interval" is "proper_interval" .
instance by(intro_classes)(transfer, simp only: proper_interval_simps)+
end
end
lemma proper_interval_integer_simps [code]:
  includes integer.lifting fixes x y :: integer and xo yo :: "integer option" shows
  "proper_interval (Some x) (Some y) = (1 < y - x)"
  "proper_interval None yo = True"
  "proper_interval xo None = True"
by(transfer, simp)+

instantiation natural :: proper_interval begin
context includes natural.lifting begin
lift_definition proper_interval_natural :: "natural proper_interval" is "proper_interval" .
instance by(intro_classes)(transfer, simp only: proper_interval_simps)+
end
end
lemma proper_interval_natural_simps [code]:
  includes natural.lifting fixes x y :: natural and xo :: "natural option" shows
  "proper_interval xo None = True"
  "proper_interval None (Some y) ⟷ y > 0"
  "proper_interval (Some x) (Some y) ⟷ y - x > 1"
by(transfer, simp)+

lemma char_less_iff_nat_of_char: "x < y ⟷ of_char x < (of_char y :: nat)"
  by (fact less_char_def)

lemma nat_of_char_inject [simp]: "of_char x = (of_char y :: nat) ⟷ x = y"
  by (fact of_char_eq_iff)

lemma char_le_iff_nat_of_char: "x ≤ y ⟷ of_char x ≤ (of_char y :: nat)"
  by (fact less_eq_char_def)

instantiation char :: proper_interval
begin

fun proper_interval_char :: "char proper_interval" where
  "proper_interval_char None None ⟷ True"
| "proper_interval_char None (Some x) ⟷ x ≠ CHR 0x00"
| "proper_interval_char (Some x) None ⟷ x ≠ CHR 0xFF"
| "proper_interval_char (Some x) (Some y) ⟷ of_char y - of_char x > (1 :: nat)"

instance proof
  fix y :: char
  { assume "y ≠ CHR 0x00"
    have "CHR 0x00 < y" 
    proof (rule ccontr)
      assume "¬ CHR 0x00 < y"
      then have "of_char y = (of_char CHR 0x00 :: nat)"
        by (simp add: not_less char_le_iff_nat_of_char)
      then have "y = CHR 0x00"
        using nat_of_char_inject [of y "CHR 0x00"] by simp
      with ‹y ≠ CHR 0x00› show False
        by simp
    qed }
  moreover
  { fix z :: char
    assume "z < CHR 0x00"
    hence False
      by (simp add: char_less_iff_nat_of_char of_char_eq_iff [symmetric]) }
  ultimately show "proper_interval None (Some y) = (∃z. z < y)"
    by auto

  fix x :: char
  { assume "x ≠ CHR 0xFF"
    then have "x < CHR 0xFF"
      by (auto simp add: neq_iff char_less_iff_nat_of_char)
        (insert nat_of_char_less_256 [of x], simp)
    hence "∃z. x < z" .. }
  moreover
  { fix z :: char
    assume "CHR 0xFF < z"
    hence "False"
      by (simp add: char_less_iff_nat_of_char)
        (insert nat_of_char_less_256 [of z], simp) }
  ultimately show "proper_interval (Some x) None = (∃z. x < z)" by auto

  { assume gt: "of_char y - of_char x > (1 :: nat)"
    let ?z = "char_of (of_char x + (1 :: nat))"
    from gt nat_of_char_less_256 [of y]
    have 255: "of_char x < (255 :: nat)" by arith
    with gt have "x < ?z" "?z < y"
      by (simp_all add: char_less_iff_nat_of_char)
    hence "∃z. x < z ∧ z < y" by blast }
  moreover
  { fix z
    assume "x < z" "z < y"
    hence "(1 :: nat) < of_char y - of_char x"
      by (simp add: char_less_iff_nat_of_char) }
  ultimately show "proper_interval (Some x) (Some y) = (∃z>x. z < y)"
    by auto
qed simp

end

instantiation Enum.finite_1 :: proper_interval begin
definition proper_interval_finite_1 :: "Enum.finite_1 proper_interval" 
where "proper_interval_finite_1 x y ⟷ x = None ∧ y = None"
instance by intro_classes (simp_all add: proper_interval_finite_1_def less_finite_1_def)
end

instantiation Enum.finite_2 :: proper_interval begin
fun proper_interval_finite_2 :: "Enum.finite_2 proper_interval" where 
  "proper_interval_finite_2 None None ⟷ True"
| "proper_interval_finite_2 None (Some x) ⟷ x = finite_2.a⇩2"
| "proper_interval_finite_2 (Some x) None ⟷ x = finite_2.a⇩1"
| "proper_interval_finite_2 (Some x) (Some y) ⟷ False"
instance by intro_classes (auto simp add: less_finite_2_def)
end

instantiation Enum.finite_3 :: proper_interval begin
fun proper_interval_finite_3 :: "Enum.finite_3 proper_interval" where
  "proper_interval_finite_3 None None ⟷ True"
| "proper_interval_finite_3 None (Some x) ⟷ x ≠ finite_3.a⇩1"
| "proper_interval_finite_3 (Some x) None ⟷ x ≠ finite_3.a⇩3"
| "proper_interval_finite_3 (Some x) (Some y) ⟷ x = finite_3.a⇩1 ∧ y = finite_3.a⇩3"
instance
proof
  fix x y :: Enum.finite_3
  show "proper_interval None (Some y) = (∃z. z < y)"
    by(cases y)(auto simp add: less_finite_3_def split: finite_3.split)
  show "proper_interval (Some x) None = (∃z. x < z)"
    by(cases x)(auto simp add: less_finite_3_def)
  show "proper_interval (Some x) (Some y) = (∃z>x. z < y)"
    by(auto simp add: less_finite_3_def split: finite_3.split_asm)
qed simp
end

subsection ‹List fusion for the order and proper intervals on @{typ "'a set"}›

definition length_last_fusion :: "('a, 's) generator ⇒ 's ⇒ nat × 'a"
where "length_last_fusion g s = length_last (list.unfoldr g s)"

lemma length_last_fusion_code [code]:
  "length_last_fusion g s =
  (if list.has_next g s then
     let (x, s') = list.next g s
     in fold_fusion g (λx (n, _). (n + 1, x)) s' (1, x)
   else (0, undefined))"
unfolding length_last_fusion_def
by(subst list.unfoldr.simps)(simp add: length_last_Nil length_last_Cons_code fold_fusion_def split_beta)

declare length_last_fusion_def [symmetric, code_unfold]

context proper_intrvl begin

definition set_less_eq_aux_Compl_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
  "set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 = 
   set_less_eq_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition Compl_set_less_eq_aux_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
  "Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 = 
   Compl_set_less_eq_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition set_less_aux_Compl_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
  "set_less_aux_Compl_fusion g1 g2 ao s1 s2 =
   set_less_aux_Compl ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition Compl_set_less_aux_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
  "Compl_set_less_aux_fusion g1 g2 ao s1 s2 =
   Compl_set_less_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition exhaustive_above_fusion :: "('a, 's) generator ⇒ 'a ⇒ 's ⇒ bool"
where "exhaustive_above_fusion g a s = exhaustive_above a (list.unfoldr g s)"

definition exhaustive_fusion :: "('a, 's) generator ⇒ 's ⇒ bool"
where "exhaustive_fusion g s = exhaustive (list.unfoldr g s)"

definition proper_interval_set_aux_fusion :: "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 's1 ⇒ 's2 ⇒ bool"
where
  "proper_interval_set_aux_fusion g1 g2 s1 s2 =
   proper_interval_set_aux (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition proper_interval_set_Compl_aux_fusion :: 
  "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ nat ⇒ 's1 ⇒ 's2 ⇒ bool"
where
  "proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 =
   proper_interval_set_Compl_aux ao n (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition proper_interval_Compl_set_aux_fusion ::
  "('a, 's1) generator ⇒ ('a, 's2) generator ⇒ 'a option ⇒ 's1 ⇒ 's2 ⇒ bool"
where
  "proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 =
   proper_interval_Compl_set_aux ao (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma set_less_eq_aux_Compl_fusion_code:
  "set_less_eq_aux_Compl_fusion g1 g2 ao s1 s2 ⟷
   (list.has_next g1 s1 ⟶ list.has_next g2 s2 ⟶
    (let (x, s1') = list.next g1 s1;
         (y, s2') = list.next g2 s2
     in if x < y then proper_interval ao (Some x) ∨ set_less_eq_aux_Compl_fusion g1 g2 (Some x) s1' s2
        else if y < x then proper_interval ao (Some y) ∨ set_less_eq_aux_Compl_fusion g1 g2 (Some y) s1 s2'
        else proper_interval ao (Some y)))"
unfolding set_less_eq_aux_Compl_fusion_def
by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta)

lemma Compl_set_less_eq_aux_fusion_code:
  "Compl_set_less_eq_aux_fusion g1 g2 ao s1 s2 ⟷
  (if list.has_next g1 s1 then
     let (x, s1') = list.next g1 s1
     in if list.has_next g2 s2 then
          let (y, s2') = list.next g2 s2
          in if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2
             else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2'
             else ¬ proper_interval ao (Some y)
        else ¬ proper_interval ao (Some x) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some x) s1' s2
   else if list.has_next g2 s2 then
     let (y, s2') = list.next g2 s2
     in ¬ proper_interval ao (Some y) ∧ Compl_set_less_eq_aux_fusion g1 g2 (Some y) s1 s2'
   else ¬ proper_interval ao None)"
unfolding Compl_set_less_eq_aux_fusion_def
by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta)

lemma set_less_aux_Compl_fusion_code:
  "set_less_aux_Compl_fusion g1 g2 ao s1 s2 ⟷
  (if list.has_next g1 s1 then
     let (x, s1') = list.next g1 s1
     in if list.has_next g2 s2 then
          let (y, s2') = list.next g2 s2
          in if x < y then proper_interval ao (Some x) ∨ set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2
             else if y < x then proper_interval ao (Some y) ∨ set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2'
             else proper_interval ao (Some y)
        else proper_interval ao (Some x) ∨ set_less_aux_Compl_fusion g1 g2 (Some x) s1' s2
   else if list.has_next g2 s2 then
     let (y, s2') = list.next g2 s2
     in proper_interval ao (Some y) ∨ set_less_aux_Compl_fusion g1 g2 (Some y) s1 s2'
   else proper_interval ao None)"
unfolding set_less_aux_Compl_fusion_def
by(subst (1 2 4 5 8 9) list.unfoldr.simps)(simp add: split_beta)

lemma Compl_set_less_aux_fusion_code:
  "Compl_set_less_aux_fusion g1 g2 ao s1 s2 ⟷
   list.has_next g1 s1 ∧ list.has_next g2 s2 ∧
  (let (x, s1') = list.next g1 s1;
       (y, s2') = list.next g2 s2
   in if x < y then ¬ proper_interval ao (Some x) ∧ Compl_set_less_aux_fusion g1 g2 (Some x) s1' s2
      else if y < x then ¬ proper_interval ao (Some y) ∧ Compl_set_less_aux_fusion g1 g2 (Some y) s1 s2'
      else ¬ proper_interval ao (Some y))"
unfolding Compl_set_less_aux_fusion_def
by(subst (1 2 4 5) list.unfoldr.simps)(simp add: split_beta)

lemma exhaustive_above_fusion_code:
  "exhaustive_above_fusion g y s ⟷
  (if list.has_next g s then
     let (x, s') = list.next g s
     in ¬ proper_interval (Some y) (Some x) ∧ exhaustive_above_fusion g x s'
   else ¬ proper_interval (Some y) None)"
unfolding exhaustive_above_fusion_def
by(subst list.unfoldr.simps)(simp add: split_beta)

lemma exhaustive_fusion_code:
  "exhaustive_fusion g s =
  (list.has_next g s ∧ 
   (let (x, s') = list.next g s
    in ¬ proper_interval None (Some x) ∧ exhaustive_above_fusion g x s'))"
unfolding exhaustive_fusion_def exhaustive_above_fusion_def
by(subst (1) list.unfoldr.simps)(simp add: split_beta)

lemma proper_interval_set_aux_fusion_code:
  "proper_interval_set_aux_fusion g1 g2 s1 s2 ⟷
   list.has_next g2 s2 ∧
  (let (y, s2') = list.next g2 s2
   in if list.has_next g1 s1 then
        let (x, s1') = list.next g1 s1
        in if x < y then False
           else if y < x then proper_interval (Some y) (Some x) ∨ list.has_next g2 s2' ∨ ¬ exhaustive_above_fusion g1 x s1'
           else proper_interval_set_aux_fusion g1 g2 s1' s2'
      else list.has_next g2 s2' ∨ proper_interval (Some y) None)"
unfolding proper_interval_set_aux_fusion_def exhaustive_above_fusion_def
by(subst (1 2) list.unfoldr.simps)(simp add: split_beta)

lemma proper_interval_set_Compl_aux_fusion_code:
  "proper_interval_set_Compl_aux_fusion g1 g2 ao n s1 s2 ⟷
  (if list.has_next g1 s1 then
     let (x, s1') = list.next g1 s1
     in if list.has_next g2 s2 then
          let (y, s2') = list.next g2 s2
          in if x < y then 
               proper_interval ao (Some x) ∨ 
               proper_interval_set_Compl_aux_fusion g1 g2 (Some x) (n + 1) s1' s2
             else if y < x then 
               proper_interval ao (Some y) ∨ 
               proper_interval_set_Compl_aux_fusion g1 g2 (Some y) (n + 1) s1 s2'
             else
               proper_interval ao (Some x) ∧
               (let m = CARD('a) - n 
                in m - length_fusion g2 s2' ≠ 2 ∨ m - length_fusion g1 s1' ≠ 2)
        else 
          let m = CARD('a) - n; (len_x, x') = length_last_fusion g1 s1
          in m ≠ len_x ∧ (m = len_x + 1 ⟶ ¬ proper_interval (Some x') None)

   else if list.has_next g2 s2 then
     let (y, s2') = list.next g2 s2;
         m = CARD('a) - n;
         (len_y, y') = length_last_fusion g2 s2
     in m ≠ len_y ∧ (m = len_y + 1 ⟶ ¬ proper_interval (Some y') None)
   else CARD('a) > n + 1)"
unfolding proper_interval_set_Compl_aux_fusion_def length_last_fusion_def length_fusion_def
by(subst (1 2 4 5 9 10) list.unfoldr.simps)(simp add: split_beta)

lemma proper_interval_Compl_set_aux_fusion_code:
  "proper_interval_Compl_set_aux_fusion g1 g2 ao s1 s2 ⟷
   list.has_next g1 s1 ∧ list.has_next g2 s2 ∧
   (let (x, s1') = list.next g1 s1;
        (y, s2') = list.next g2 s2
    in if x < y then
         ¬ proper_interval ao (Some x) ∧ proper_interval_Compl_set_aux_fusion g1 g2 (Some x) s1' s2
       else if y < x then
         ¬ proper_interval ao (Some y) ∧ proper_interval_Compl_set_aux_fusion g1 g2 (Some y) s1 s2'
       else ¬ proper_interval ao (Some x) ∧ (list.has_next g2 s2' ∨ list.has_next g1 s1'))"
unfolding proper_interval_Compl_set_aux_fusion_def
by(subst (1 2 4 5) list.unfoldr.simps)(auto simp add: split_beta)

end

lemmas [code] =
  set_less_eq_aux_Compl_fusion_code proper_intrvl.set_less_eq_aux_Compl_fusion_code
  Compl_set_less_eq_aux_fusion_code proper_intrvl.Compl_set_less_eq_aux_fusion_code
  set_less_aux_Compl_fusion_code proper_intrvl.set_less_aux_Compl_fusion_code
  Compl_set_less_aux_fusion_code proper_intrvl.Compl_set_less_aux_fusion_code
  exhaustive_above_fusion_code proper_intrvl.exhaustive_above_fusion_code
  exhaustive_fusion_code proper_intrvl.exhaustive_fusion_code
  proper_interval_set_aux_fusion_code proper_intrvl.proper_interval_set_aux_fusion_code
  proper_interval_set_Compl_aux_fusion_code proper_intrvl.proper_interval_set_Compl_aux_fusion_code
  proper_interval_Compl_set_aux_fusion_code proper_intrvl.proper_interval_Compl_set_aux_fusion_code

lemmas [symmetric, code_unfold] =
  set_less_eq_aux_Compl_fusion_def proper_intrvl.set_less_eq_aux_Compl_fusion_def
  Compl_set_less_eq_aux_fusion_def proper_intrvl.Compl_set_less_eq_aux_fusion_def
  set_less_aux_Compl_fusion_def proper_intrvl.set_less_aux_Compl_fusion_def
  Compl_set_less_aux_fusion_def proper_intrvl.Compl_set_less_aux_fusion_def
  exhaustive_above_fusion_def proper_intrvl.exhaustive_above_fusion_def
  exhaustive_fusion_def proper_intrvl.exhaustive_fusion_def
  proper_interval_set_aux_fusion_def proper_intrvl.proper_interval_set_aux_fusion_def
  proper_interval_set_Compl_aux_fusion_def proper_intrvl.proper_interval_set_Compl_aux_fusion_def
  proper_interval_Compl_set_aux_fusion_def proper_intrvl.proper_interval_Compl_set_aux_fusion_def

subsection ‹Drop notation›

context ord begin

no_notation set_less_aux (infix ‹⊏''› 50)
  and set_less_eq_aux (infix ‹⊑''› 50)
  and set_less_eq_aux' (infix ‹⊑''''› 50)
  and set_less_eq_aux'' (infix ‹⊑''''''› 50)
  and set_less_eq (infix ‹⊑› 50)
  and set_less (infix ‹⊏› 50)

end

end