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<