Theory Containers.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  (aA. 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 "zA - 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)  (zabove 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)  (zabove 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)  (zabove 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.a2"
| "proper_interval_finite_2 (Some x) None  x = finite_2.a1"
| "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.a1"
| "proper_interval_finite_3 (Some x) None  x  finite_3.a3"
| "proper_interval_finite_3 (Some x) (Some y)  x = finite_3.a1  y = finite_3.a3"
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