Session Containers

Theory Containers_Auxiliary

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

theory Containers_Auxiliary imports
  "HOL-Library.Monad_Syntax"
begin

chapter ‹An executable linear order on sets›
text_raw ‹\label{chapter:linear:order:set}›

section ‹Auxiliary definitions›

lemma insert_bind_set: "insert a A  f = f a  (A  f)"
by(auto simp add: Set.bind_def)

lemma set_bind_iff:
  "set (List.bind xs f) = Set.bind (set xs) (set  f)"
by(induct xs)(simp_all add: insert_bind_set)

lemma set_bind_conv_fold: "set xs  f = fold ((∪)  f) xs {}"
by(induct xs rule: rev_induct)(simp_all add: insert_bind_set)

lemma card_gt_1D:
  assumes "card A > 1"
  shows "x y. x  A  y  A  x  y"
proof(rule ccontr)
  from assms have "A  {}" by auto
  then obtain x where "x  A" by auto
  moreover
  assume "¬ ?thesis"
  ultimately have "A = {x}" by auto
  with assms show False by simp
qed

lemma card_eq_1_iff: "card A = 1  (x. A = {x})"
proof
  assume card: "card A = 1"
  hence [simp]: "finite A" using card_gt_0_iff[of A] by simp
  have "A = {THE x. x  A}"
  proof(intro equalityI subsetI)
    fix x
    assume x: "x  A"
    hence "(THE x. x  A) = x"
    proof(rule the_equality)
      fix x'
      assume x': "x'  A"
      show "x' = x"
      proof(rule ccontr)
        assume neq: "x'  x"
        from x x' have eq: "A = insert x (insert x' (A - {x, x'}))" by auto
        have "card A = 2 + card (A - {x, x'})" using neq by(subst eq)(simp)
        with card show False by simp
      qed
    qed
    thus "x  {THE x. x  A}" by simp
  next
    fix x
    assume "x  {THE x. x  A}"
    hence x: "x = (THE x. x  A)" by simp
    from card have "A  {}" by auto
    then obtain x' where x': "x'  A" by blast
    thus "x  A" unfolding x
    proof(rule theI)
      fix x
      assume x: "x  A"
      show "x = x'"
      proof(rule ccontr)
        assume neq: "x  x'"
        from x x' have eq: "A = insert x (insert x' (A - {x, x'}))" by auto
        have "card A = 2 + card (A - {x, x'})" using neq by(subst eq)(simp)
        with card show False by simp
      qed
    qed
  qed
  thus "x. A = {x}" ..
qed auto

lemma card_eq_Suc_0_ex1: "card A = Suc 0  (∃!x. x  A)"
by(auto simp only: One_nat_def[symmetric] card_eq_1_iff)

context linorder begin

lemma sorted_last: " sorted xs; x  set xs   x  last xs"
by(cases xs rule: rev_cases)(auto simp add: sorted_append)

end

lemma empty_filter_conv: "[] = filter P xs  (xset xs. ¬ P x)"
by(auto dest: sym simp add: filter_empty_conv)


definition ID :: "'a  'a" where "ID = id"

lemma ID_code [code, code_unfold]: "ID = (λx. x)"
by(simp add: ID_def id_def)

lemma ID_Some: "ID (Some x) = Some x"
by(simp add: ID_def)

lemma ID_None: "ID None = None" 
by(simp add: ID_def)

text ‹lexicographic order on pairs›

context
  fixes leq_a :: "'a  'a  bool" (infix "a" 50) 
  and less_a :: "'a  'a  bool" (infix "a" 50) 
  and leq_b :: "'b  'b  bool" (infix "b" 50) 
  and less_b :: "'b  'b  bool" (infix "b" 50) 
begin

definition less_eq_prod :: "('a × 'b)  ('a × 'b)  bool" (infix "" 50)
where "less_eq_prod = (λ(x1, x2) (y1, y2). x1 a y1  x1 a y1  x2 b y2)"

definition less_prod :: "('a × 'b)  ('a × 'b)  bool" (infix "" 50)
where "less_prod = (λ(x1, x2) (y1, y2). x1 a y1  x1 a y1  x2 b y2)"

lemma less_eq_prod_simps [simp]:
  "(x1, x2)  (y1, y2)  x1 a y1  x1 a y1  x2 b y2"
by(simp add: less_eq_prod_def)

lemma less_prod_simps [simp]:
  "(x1, x2)  (y1, y2)  x1 a y1  x1 a y1  x2 b y2"
by(simp add: less_prod_def)

end

context
  fixes leq_a :: "'a  'a  bool" (infix "a" 50) 
  and less_a :: "'a  'a  bool" (infix "a" 50) 
  and leq_b :: "'b  'b  bool" (infix "b" 50) 
  and less_b :: "'b  'b  bool" (infix "b" 50) 
  assumes lin_a: "class.linorder leq_a less_a" 
  and lin_b: "class.linorder leq_b less_b"
begin

abbreviation (input) less_eq_prod' :: "('a × 'b)  ('a × 'b)  bool" (infix "" 50)
where "less_eq_prod'  less_eq_prod leq_a less_a leq_b"

abbreviation (input) less_prod' :: "('a × 'b)  ('a × 'b)  bool" (infix "" 50)
where "less_prod'  less_prod leq_a less_a less_b"

lemma linorder_prod:
  "class.linorder (⊑) (⊏)"
proof -
  interpret a: linorder "(⊑a)" "(⊏a)" by(fact lin_a)
  interpret b: linorder "(⊑b)" "(⊏b)" by(fact lin_b)
  show ?thesis by unfold_locales auto
qed

end

hide_const less_eq_prod' less_prod'

end

Theory Card_Datatype

(*  Title:      Containers/Card_Datatype.thy
    Author:     Andreas Lochbihler, ETH Zurich *)

theory Card_Datatype
imports "HOL-Library.Cardinality"
begin

section ‹Definitions to prove equations about the cardinality of data types›

subsection ‹Specialised @{term range} constants›

definition rangeIt :: "'a  ('a  'a)  'a set"
where "rangeIt x f = range (λn. (f ^^ n) x)"

definition rangeC :: "('a  'b) set  'b set"
where "rangeC F = (f  F. range f)"

lemma infinite_rangeIt: 
  assumes inj: "inj f"
  and x: "y. x  f y"
  shows "¬ finite (rangeIt x f)"
proof -
  have "inj (λn. (f ^^ n) x)"
  proof(rule injI)
    fix n m
    assume "(f ^^ n) x = (f ^^ m) x"
    thus "n = m"
    proof(induct n arbitrary: m)
      case 0
      thus ?case using x by(cases m)(auto intro: sym)
    next
      case (Suc n)
      thus ?case using x by(cases m)(auto intro: sym dest: injD[OF inj])
    qed
  qed
  thus ?thesis
    by(auto simp add: rangeIt_def dest: finite_imageD)
qed

lemma in_rangeC: "f  A  f x  rangeC A"
by(auto simp add: rangeC_def)

lemma in_rangeCE: assumes "y  rangeC A"
  obtains f x where "f  A" "y = f x"
using assms by(auto simp add: rangeC_def)

lemma in_rangeC_singleton: "f x  rangeC {f}"
by(auto simp add: rangeC_def)

lemma in_rangeC_singleton_const: "x  rangeC {λ_. x}"
by(rule in_rangeC_singleton)

lemma rangeC_rangeC: "f  rangeC A  f x  rangeC (rangeC A)"
by(auto simp add: rangeC_def)

lemma rangeC_eq_empty: "rangeC A = {}  A = {}"
by(auto simp add: rangeC_def)

lemma Ball_rangeC_iff:
  "(x  rangeC A. P x)  (f  A. x. P (f x))"
by(auto intro: in_rangeC elim: in_rangeCE)

lemma Ball_rangeC_singleton:
  "(x  rangeC {f}. P x)  (x. P (f x))"
by(simp add: Ball_rangeC_iff)

lemma Ball_rangeC_rangeC:
  "(x  rangeC (rangeC A). P x)  (f  rangeC A. x. P (f x))"
by(simp add: Ball_rangeC_iff)

lemma finite_rangeC:
  assumes inj: "f  A. inj f"
  and disjoint: "f  A. g  A. f  g  (x y. f x  g y)"
  shows "finite (rangeC (A :: ('a  'b) set))  finite A  (A  {}  finite (UNIV :: 'a set))"
  (is "?lhs  ?rhs")
proof
  assume ?lhs
  thus ?rhs using inj disjoint
  proof(induct "rangeC A" arbitrary: A rule: finite_psubset_induct)
    case (psubset A)
    show ?case
    proof(cases "A = {}")
      case True thus ?thesis by simp
    next
      case False
      then obtain f A' where A: "A = insert f A'" and f: "f  A" "f  A'"
        by(fastforce dest: mk_disjoint_insert)
      from A have rA: "rangeC A = rangeC A'  range f"
        by(auto simp add: rangeC_def)

      have "¬ range f  rangeC A'" 
      proof
        assume "range f  rangeC A'"
        moreover obtain x where x: "x  range f" by auto
        ultimately have "x  rangeC A'" by auto
        then obtain g where "g  A'" "x  range g" by(auto simp add: rangeC_def)
        with f  A' A have "g  A" "f  g" by auto
        with f  A have "x y. f x  g y" by(rule psubset.prems[rule_format])
        thus False using x x  range g by auto
      qed
      hence "rangeC A'  rangeC A" unfolding rA by auto
      hence "finite A'  (A'  {}  finite (UNIV :: 'a set))"
        using psubset.prems
        by -(erule psubset.hyps, auto simp add: A)
      with A have "finite A" by simp
      moreover with ‹finite (rangeC A) A f  A. inj f
      have "finite (UNIV :: 'a set)"
        by(auto simp add: rangeC_def dest: finite_imageD)
      ultimately show ?thesis by blast
    qed
  qed
qed(auto simp add: rangeC_def)

lemma finite_rangeC_singleton_const:
  "finite (rangeC {λ_. x})"
by(auto simp add: rangeC_def image_def)

lemma card_Un:
  " finite A; finite B   card (A  B) = card (A) + card (B) - card(A  B)"
by(subst card_Un_Int) simp_all

lemma card_rangeC_singleton_const:
  "card (rangeC {λ_. f}) = 1"
by(simp add: rangeC_def image_def)

lemma card_rangeC:
  assumes inj: "f  A. inj f"
  and disjoint: "f  A. g  A. f  g  (x y. f x  g y)"
  shows "card (rangeC (A :: ('a  'b) set)) = CARD('a) * card A"
  (is "?lhs = ?rhs")
proof(cases "finite (UNIV :: 'a set)  finite A")
  case False
  thus ?thesis using False finite_rangeC[OF assms]
    by(auto simp add: card_eq_0_iff rangeC_eq_empty)
next
  case True
  { fix f
    assume "f  A"
    hence "card (range f) = CARD('a)" using inj by(simp add: card_image) }
  thus ?thesis using disjoint True unfolding rangeC_def
    by(subst card_UN_disjoint) auto
qed

lemma rangeC_Int_rangeC:
  " f  A. g  B. x y. f x  g y   rangeC A  rangeC B = {}"
by(auto simp add: rangeC_def)

lemmas rangeC_simps =
  in_rangeC_singleton
  in_rangeC_singleton_const
  rangeC_rangeC
  rangeC_eq_empty
  Ball_rangeC_singleton
  Ball_rangeC_rangeC
  finite_rangeC
  finite_rangeC_singleton_const
  card_rangeC_singleton_const
  card_rangeC
  rangeC_Int_rangeC

bundle card_datatype =
  rangeC_simps [simp]
  card_Un [simp]
  fun_eq_iff [simp]
  Int_Un_distrib [simp]
  Int_Un_distrib2 [simp]
  card_eq_0_iff [simp]
  imageI [simp] image_eqI [simp del]
  conj_cong [cong]
  infinite_rangeIt [simp]

subsection ‹Cardinality primitives for polymorphic HOL types›

ML structure Card_Simp_Rules = Named_Thms
(
  val name = @{binding card_simps}
  val description = "Simplification rules for cardinality of types"
)
setup Card_Simp_Rules.setup

definition card_fun :: "nat  nat  nat"
where "card_fun a b = (if a  0  b  0  b = 1 then b ^ a else 0)"

lemma CARD_fun [card_simps]:
  "CARD('a  'b) = card_fun CARD('a) CARD('b)"
by(simp add: card_fun card_fun_def)

definition card_sum :: "nat  nat  nat"
where "card_sum a b = (if a = 0  b = 0 then 0 else a + b)"

lemma CARD_sum [card_simps]:
  "CARD('a + 'b) = card_sum CARD('a) CARD('b)"
by(simp add: card_UNIV_sum card_sum_def)

definition card_option :: "nat  nat"
where "card_option n = (if n = 0 then 0 else Suc n)"

lemma CARD_option [card_simps]:
  "CARD('a option) = card_option CARD('a)"
by(simp add: card_option_def card_UNIV_option)

definition card_prod :: "nat  nat  nat"
where "card_prod a b = a * b"

lemma CARD_prod [card_simps]:
  "CARD('a * 'b) = card_prod CARD('a) CARD('b)"
by(simp add: card_prod_def)

definition card_list :: "nat  nat"
where "card_list _ = 0"

lemma CARD_list [card_simps]: "CARD('a list) = card_list CARD('a)"
by(simp add: card_list_def infinite_UNIV_listI)

end

Theory List_Fusion

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

theory List_Fusion
imports 
  Main
begin

section ‹Shortcut fusion for lists›

lemma Option_map_mono [partial_function_mono]:
  "mono_option f  mono_option (λx. map_option g (f x))"
apply(rule monotoneI)
apply(drule (1) monotoneD)
apply(auto simp add: map_option_case flat_ord_def split: option.split)
done

lemma list_all2_coinduct [consumes 1, case_names Nil Cons, case_conclusion Cons hd tl, coinduct pred: list_all2]:
  assumes X: "X xs ys"
  and Nil': "xs ys. X xs ys  xs = []  ys = []"
  and Cons': "xs ys.  X xs ys; xs  []; ys  []   A (hd xs) (hd ys)  (X (tl xs) (tl ys)  list_all2 A (tl xs) (tl ys))"
  shows "list_all2 A xs ys"
using X
proof(induction xs arbitrary: ys)
  case Nil
  from Nil'[OF this] show ?case by simp
next
  case (Cons x xs)
  from Nil'[OF Cons.prems] Cons'[OF Cons.prems] Cons.IH
  show ?case by(auto simp add: neq_Nil_conv)
qed



subsection ‹The type of generators for finite lists›

type_synonym ('a, 's) raw_generator = "('s  bool) × ('s  'a × 's)"

inductive_set terminates_on :: "('a, 's) raw_generator  's set"
  for g :: "('a, 's) raw_generator"
where
  stop: "¬ fst g s  s  terminates_on g"
| unfold: " fst g s; snd (snd g s)  terminates_on g   s  terminates_on g"

definition terminates :: "('a, 's) raw_generator  bool"
where "terminates g  (terminates_on g = UNIV)"

lemma terminatesI [intro?]:
  "(s. s  terminates_on g)  terminates g"
by(auto simp add: terminates_def)

lemma terminatesD:
  "terminates g  s  terminates_on g"
by(auto simp add: terminates_def)

lemma terminates_on_stop:
  "terminates_on (λ_. False, next) = UNIV"
by(auto intro: terminates_on.stop)

lemma wf_terminates:
  assumes "wf R"
  and step: "s. fst g s  (snd (snd g s), s)  R"
  shows "terminates g"
proof(rule terminatesI)
  fix s
  from ‹wf R show "s  terminates_on g"
  proof(induction rule: wf_induct[rule_format, consumes 1, case_names wf])
    case (wf s)
    show ?case
    proof(cases "fst g s")
      case True
      hence "(snd (snd g s), s)  R" by(rule step)
      hence "snd (snd g s)  terminates_on g" by(rule wf.IH)
      with True show ?thesis by(rule terminates_on.unfold)
    qed(rule terminates_on.stop)
  qed
qed

lemma terminates_wfD:
  assumes "terminates g"
  shows "wf {(snd (snd g s), s) | s . fst g s}"
proof(rule wfUNIVI)
  fix thesis s
  assume wf [rule_format]: "s. (s'. (s', s)  {(snd (snd g s), s) |s. fst g s}  thesis s')  thesis s"
  from assms have "s  terminates_on g" by(auto simp add: terminates_def)
  thus "thesis s" by induct (auto intro: wf)
qed

lemma terminates_wfE:
  assumes "terminates g"
  obtains R where "wf R" "s. fst g s  (snd (snd g s), s)  R"
by(rule that)(rule terminates_wfD[OF assms], simp)

context fixes g :: "('a, 's) raw_generator" begin

partial_function (option) terminates_within :: "'s  nat option"
where
  "terminates_within s =
   (let (has_next, next) = g
    in if has_next s then 
          map_option (λn. n + 1) (terminates_within (snd (next s))) 
       else Some 0)"

lemma terminates_on_conv_dom_terminates_within:
  "terminates_on g = dom terminates_within"
proof(safe)
  fix s
  assume "s  terminates_on g"
  then show "n. terminates_within s = Some n"
    by(induct)(subst terminates_within.simps, simp add: split_beta)+
next
  fix s n
  assume "terminates_within s = Some n"
  then show "s  terminates_on g"
    by(induct rule: terminates_within.raw_induct[rotated 1, consumes 1])(auto simp add: split_beta split: if_split_asm intro: terminates_on.intros)
qed

end

lemma terminates_within_unfold:
  "has_next s  
  terminates_within (has_next, next) s = map_option (λn. n + 1) (terminates_within (has_next, next) (snd (next s)))"
by(simp add: terminates_within.simps)

typedef ('a, 's) generator = "{g :: ('a, 's) raw_generator. terminates g}"
  morphisms generator Generator
proof
  show "(λ_. False, undefined)  ?generator"
    by(simp add: terminates_on_stop terminates_def)
qed

setup_lifting type_definition_generator

lemma terminates_on_generator_eq_UNIV:
  "terminates_on (generator g) = UNIV"
by transfer(simp add: terminates_def)

lemma terminates_within_stop:
  "terminates_within (λ_. False, next) s = Some 0"
by(simp add: terminates_within.simps)

lemma terminates_within_generator_neq_None:
  "terminates_within (generator g) s  None"
by(transfer)(auto simp add: terminates_def terminates_on_conv_dom_terminates_within)

locale list = 
  fixes g :: "('a, 's) generator" begin

definition has_next :: "'s  bool"
where "has_next = fst (generator g)"

definition "next" :: "'s  'a × 's"
where "next = snd (generator g)"

function unfoldr :: "'s  'a list"
where "unfoldr s = (if has_next s then let (a, s') = next s in a # unfoldr s' else [])"
by pat_completeness auto
termination
proof -
  have "terminates (generator g)" using generator[of g] by simp
  thus ?thesis
    by(rule terminates_wfE)(erule "termination", metis has_next_def next_def snd_conv)
qed

declare unfoldr.simps [simp del]

lemma unfoldr_simps:
  "has_next s  unfoldr s = fst (next s) # unfoldr (snd (next s))"
  "¬ has_next s  unfoldr s = []"
by(simp_all add: unfoldr.simps split_beta)

end

declare 
  list.has_next_def[code]
  list.next_def[code]
  list.unfoldr.simps[code]

context includes lifting_syntax
begin

lemma generator_has_next_transfer [transfer_rule]: 
  "(pcr_generator (=) (=) ===> (=)) fst list.has_next"
by(auto simp add: generator.pcr_cr_eq cr_generator_def list.has_next_def dest: sym)

lemma generator_next_transfer [transfer_rule]:
  "(pcr_generator (=) (=) ===> (=)) snd list.next"
by(auto simp add: generator.pcr_cr_eq cr_generator_def list.next_def)

end

lemma unfoldr_eq_Nil_iff [iff]:
  "list.unfoldr g s = []  ¬ list.has_next g s"
by(subst list.unfoldr.simps)(simp add: split_beta)

lemma Nil_eq_unfoldr_iff [simp]:
  "[] = list.unfoldr g s  ¬ list.has_next g s"
by(auto intro: sym dest: sym)

subsection ‹Generators for @{typ "'a list"}

primrec list_has_next :: "'a list  bool"
where
  "list_has_next []  False"
| "list_has_next (x # xs)  True"

primrec list_next :: "'a list  'a × 'a list"
where
  "list_next (x # xs) = (x, xs)"

lemma terminates_list_generator: "terminates (list_has_next, list_next)"
proof
  fix xs
  show "xs  terminates_on (list_has_next, list_next)"
    by(induct xs)(auto intro: terminates_on.intros)
qed

lift_definition list_generator :: "('a, 'a list) generator" 
  is "(list_has_next, list_next)"
by(rule terminates_list_generator)

lemma has_next_list_generator [simp]: 
  "list.has_next list_generator = list_has_next"
by transfer simp

lemma next_list_generator [simp]: 
  "list.next list_generator = list_next"
by transfer simp

lemma unfoldr_list_generator:
  "list.unfoldr list_generator xs = xs"
by(induct xs)(simp_all add: list.unfoldr_simps)

lemma terminates_replicate_generator:
  "terminates (λn :: nat. 0 < n, λn. (a, n - 1))"
by(rule wf_terminates)(lexicographic_order)

lift_definition replicate_generator :: "'a  ('a, nat) generator"
  is "λa. (λn. 0 < n, λn. (a, n - 1))"
by(rule terminates_replicate_generator)

lemma has_next_replicate_generator [simp]:
  "list.has_next (replicate_generator a) n  0 < n"
by transfer simp

lemma next_replicate_generator [simp]:
  "list.next (replicate_generator a) n = (a, n - 1)"
by transfer simp

lemma unfoldr_replicate_generator:
  "list.unfoldr (replicate_generator a) n = replicate n a"
by(induct n)(simp_all add: list.unfoldr_simps)

context fixes f :: "'a  'b" begin

lift_definition map_generator :: "('a, 's) generator  ('b, 's) generator"
  is "λ(has_next, next). (has_next, λs. let (a, s') = next s in (f a, s'))"
by(erule terminates_wfE)(erule wf_terminates, auto simp add: split_beta)

lemma has_next_map_generator [simp]:
  "list.has_next (map_generator g) = list.has_next g"
by transfer clarsimp

lemma next_map_generator [simp]:
  "list.next (map_generator g) = apfst f  list.next g"
by transfer(simp add: fun_eq_iff split_beta apfst_def map_prod_def)

lemma unfoldr_map_generator:
  "list.unfoldr (map_generator g) = map f  list.unfoldr g"
  (is "?lhs = ?rhs")
proof(rule ext)
  fix s
  show "?lhs s = ?rhs s"
    by(induct s taking: "map_generator g" rule: list.unfoldr.induct)
      (subst (1 2) list.unfoldr.simps, auto simp add: split_beta apfst_def map_prod_def)
qed

end

context fixes g1 :: "('a, 's1) raw_generator"
  and g2 :: "('a, 's2) raw_generator" 
begin

fun append_has_next :: "'s1 × 's2 + 's2  bool"
where
  "append_has_next (Inl (s1, s2))  fst g1 s1  fst g2 s2"
| "append_has_next (Inr s2)  fst g2 s2"

fun append_next :: "'s1 × 's2 + 's2  'a × ('s1 × 's2 + 's2)"
where
  "append_next (Inl (s1, s2)) = 
  (if fst g1 s1 then 
     let (x, s1') = snd g1 s1 in (x, Inl (s1', s2)) 
   else append_next (Inr s2))"
| "append_next (Inr s2) = (let (x, s2') = snd g2 s2 in (x, Inr s2'))"

end

lift_definition append_generator :: "('a, 's1) generator  ('a, 's2) generator  ('a, 's1 × 's2 + 's2) generator"
  is "λg1 g2. (append_has_next g1 g2, append_next g1 g2)"
proof(rule terminatesI, safe)
  fix has_next1 and next1 :: "'s1  'a × 's1"
    and has_next2 and next2 :: "'s2  'a × 's2"
    and s
  assume t1: "terminates (has_next1, next1)" 
    and t2: "terminates (has_next2, next2)"
  let ?has_next = "append_has_next (has_next1, next1) (has_next2, next2)"
  let ?next = "append_next (has_next1, next1) (has_next2, next2)"
  note [simp] = split_beta
    and [intro] = terminates_on.intros
  { fix s2 :: 's2
    from t2 have "s2  terminates_on (has_next2, next2)" by(rule terminatesD)
    hence "Inr s2  terminates_on (?has_next, ?next)" by induct auto }
  note Inr' = this

  show "s  terminates_on (?has_next, ?next)"
  proof(cases s)
    case Inr thus ?thesis by(simp add: Inr')
  next
    case (Inl s1s2)
    moreover obtain s1 s2 where "s1s2 = (s1, s2)" by(cases s1s2)
    ultimately have s: "s = Inl (s1, s2)" by simp
    from t1 have "s1  terminates_on (has_next1, next1)" by(rule terminatesD)
    thus ?thesis unfolding s
    proof induct
      case stop thus ?case
        by(cases "has_next2 s2")(auto simp add: Inr')
    qed auto
  qed
qed

definition append_init :: "'s1  's2  's1 × 's2 + 's2"
where "append_init s1 s2 = Inl (s1, s2)"

lemma has_next_append_generator [simp]:
  "list.has_next (append_generator g1 g2) (Inl (s1, s2)) 
   list.has_next g1 s1  list.has_next g2 s2"
  "list.has_next (append_generator g1 g2) (Inr s2)  list.has_next g2 s2"
by(transfer, simp)+

lemma next_append_generator [simp]:
  "list.next (append_generator g1 g2) (Inl (s1, s2)) =
  (if list.has_next g1 s1 then 
     let (x, s1') = list.next g1 s1 in (x, Inl (s1', s2))
   else list.next (append_generator g1 g2) (Inr s2))"
  "list.next (append_generator g1 g2) (Inr s2) = apsnd Inr (list.next g2 s2)"
by(transfer, simp add: apsnd_def map_prod_def)+

lemma unfoldr_append_generator_Inr: 
  "list.unfoldr (append_generator g1 g2) (Inr s2) = list.unfoldr g2 s2"
by(induct s2 taking: g2 rule: list.unfoldr.induct)(subst (1 2) list.unfoldr.simps, auto split: prod.splits)

lemma unfoldr_append_generator_Inl:
  "list.unfoldr (append_generator g1 g2) (Inl (s1, s2)) = 
   list.unfoldr g1 s1 @ list.unfoldr g2 s2"
apply(induct s1 taking: g1 rule: list.unfoldr.induct)
apply(subst (1 2 3) list.unfoldr.simps)
apply(auto split: prod.splits simp add: apsnd_def map_prod_def unfoldr_append_generator_Inr)
apply(simp add: list.unfoldr_simps)
done

lemma unfoldr_append_generator:
  "list.unfoldr (append_generator g1 g2) (append_init s1 s2) =
   list.unfoldr g1 s1 @ list.unfoldr g2 s2"
by(simp add: unfoldr_append_generator_Inl append_init_def)


lift_definition zip_generator :: "('a, 's1) generator  ('b, 's2) generator  ('a × 'b, 's1 × 's2) generator"
  is "λ(has_next1, next1) (has_next2, next2). 
      (λ(s1, s2). has_next1 s1  has_next2 s2, 
       λ(s1, s2). let (x, s1') = next1 s1; (y, s2') = next2 s2
                  in ((x, y), (s1', s2')))"
proof(rule terminatesI, safe)
  fix has_next1 next1 has_next2 next2 s1 s2
  assume t1: "terminates (has_next1, next1)" 
    and t2: "terminates (has_next2, next2)"
  have "s1  terminates_on (has_next1, next1)" "s2  terminates_on (has_next2, next2)"
    using t1 t2 by(simp_all add: terminatesD)
  thus "(s1, s2)  terminates_on (λ(s1, s2). has_next1 s1  has_next2 s2, λ(s1, s2). let (x, s1') = next1 s1; (y, s2') = next2 s2 in ((x, y), (s1', s2')))"
    by(induct arbitrary: s2)(auto 4 3 elim: terminates_on.cases intro: terminates_on.intros simp add: split_beta Let_def)
qed

abbreviation (input) zip_init :: "'s1  's2  's1 × 's2"
where "zip_init  Pair"

lemma has_next_zip_generator [simp]: 
  "list.has_next (zip_generator g1 g2) (s1, s2)  
   list.has_next g1 s1  list.has_next g2 s2"
by transfer clarsimp

lemma next_zip_generator [simp]: 
  "list.next (zip_generator g1 g2) (s1, s2) = 
  ((fst (list.next g1 s1), fst (list.next g2 s2)), 
   (snd (list.next g1 s1), snd (list.next g2 s2)))"
by transfer(simp add: split_beta)

lemma unfoldr_zip_generator:
  "list.unfoldr (zip_generator g1 g2) (zip_init s1 s2) = 
   zip (list.unfoldr g1 s1) (list.unfoldr g2 s2)"
by(induct "(s1, s2)" arbitrary: s1 s2 taking: "zip_generator g1 g2" rule: list.unfoldr.induct)
  (subst (1 2 3) list.unfoldr.simps, auto 9 2 simp add: split_beta)

context fixes bound :: nat begin

lift_definition upt_generator :: "(nat, nat) generator"
  is "(λn. n < bound, λn. (n, Suc n))"
by(rule wf_terminates)(relation "measure (λn. bound - n)", auto)

lemma has_next_upt_generator [simp]:
  "list.has_next upt_generator n  n < bound"
by transfer simp

lemma next_upt_generator [simp]:
  "list.next upt_generator n = (n, Suc n)"
by transfer simp

lemma unfoldr_upt_generator:
  "list.unfoldr upt_generator n = [n..<bound]"
by(induct "bound - n" arbitrary: n)(simp_all add: list.unfoldr_simps upt_conv_Cons)

end

context fixes bound :: int begin

lift_definition upto_generator :: "(int, int) generator"
  is "(λn. n  bound, λn. (n, n + 1))"
by(rule wf_terminates)(relation "measure (λn. nat (bound + 1 - n))", auto)

lemma has_next_upto_generator [simp]:
  "list.has_next upto_generator n  n  bound"
by transfer simp

lemma next_upto_generator [simp]:
  "list.next upto_generator n = (n, n + 1)"
by transfer simp

lemma unfoldr_upto_generator:
  "list.unfoldr upto_generator n = [n..bound]"
by(induct n taking: upto_generator rule: list.unfoldr.induct)(subst list.unfoldr.simps, subst upto.simps, auto)

end

context
  fixes P :: "'a  bool"
begin

context 
  fixes g :: "('a, 's) raw_generator"
begin

inductive filter_has_next :: "'s  bool"
where
  " fst g s; P (fst (snd g s))   filter_has_next s"
| " fst g s; ¬ P (fst (snd g s)); filter_has_next (snd (snd g s))   filter_has_next s"

partial_function (tailrec) filter_next :: "'s  'a × 's"
where
  "filter_next s = (let (x, s') = snd g s in if P x then (x, s') else filter_next s')"

end

lift_definition filter_generator :: "('a, 's) generator  ('a, 's) generator"
  is "λg. (filter_has_next g, filter_next g)"
proof(rule wf_terminates)
  fix g :: "('a, 's) raw_generator" and s
  let ?R = "{(snd (snd g s), s) | s. fst g s}"
  let ?g = "(filter_has_next g, filter_next g)"
  assume "terminates g"
  thus "wf (?R+)" by(rule terminates_wfD[THEN wf_trancl])
  assume "fst ?g s"
  hence "filter_has_next g s" by simp
  thus "(snd (snd ?g s), s)  ?R+"
    by induct(subst filter_next.simps, auto simp add: split_beta filter_next.simps split del: if_split intro: trancl_into_trancl)
qed

lemma has_next_filter_generator:
  "list.has_next (filter_generator g) s 
  list.has_next g s  (let (x, s') = list.next g s in if P x then True else list.has_next (filter_generator g) s')"
apply(transfer)
apply simp
apply(subst filter_has_next.simps)
apply auto
done

lemma next_filter_generator:
   "list.next (filter_generator g) s =
   (let (x, s') = list.next g s
    in if P x then (x, s') else list.next (filter_generator g) s')"
apply transfer
apply simp
apply(subst filter_next.simps)
apply(simp cong: if_cong)
done

lemma has_next_filter_generator_induct [consumes 1, case_names find step]:
  assumes "list.has_next (filter_generator g) s"
  and find: "s.  list.has_next g s; P (fst (list.next g s))   Q s"
  and step: "s.  list.has_next g s; ¬ P (fst (list.next g s)); Q (snd (list.next g s))   Q s"
  shows "Q s"
using assms by transfer(auto elim: filter_has_next.induct)

lemma filter_generator_empty_conv:
  "list.has_next (filter_generator g) s  (xset (list.unfoldr g s). P x)" (is "?lhs  ?rhs")
proof
  assume "?lhs"
  thus ?rhs
  proof(induct rule: has_next_filter_generator_induct)
    case (find s)
    thus ?case
      by(cases "list.next g s")(subst list.unfoldr.simps, auto)
  next
    case (step s)
    thus ?case
      by(cases "list.next g s")(subst list.unfoldr.simps, auto)
  qed
next
  assume ?rhs
  then obtain x where "x  set (list.unfoldr g s)" "P x" by blast
  thus ?lhs
  proof(induct xs"list.unfoldr g s" arbitrary: s)
    case Nil thus ?case by(simp del: Nil_eq_unfoldr_iff)
  next
    case (Cons x' xs)
    from x' # xs = list.unfoldr g s[symmetric, simp]
    have [simp]: "fst (list.next g s) = x'  list.has_next g s  list.unfoldr g (snd (list.next g s)) = xs"
      by(subst (asm) list.unfoldr.simps)(simp add: split_beta split: if_split_asm)
    from Cons.hyps(1)[of "snd (list.next g s)"] x  set (list.unfoldr g s) P x show ?case
      by(subst has_next_filter_generator)(auto simp add: split_beta)
  qed
qed

lemma unfoldr_filter_generator:
  "list.unfoldr (filter_generator g) s = filter P (list.unfoldr g s)"
unfolding list_all2_eq
proof(coinduction arbitrary: s)
  case Nil
  thus ?case by(simp add: filter_empty_conv filter_generator_empty_conv)
next
  case (Cons s)
  hence "list.has_next (filter_generator g) s" by simp
  thus ?case
  proof(induction rule: has_next_filter_generator_induct)
    case (find s)
    thus ?case
      apply(subst (1 2 3 5) list.unfoldr.simps)
      apply(subst (1 2) has_next_filter_generator)
      apply(subst next_filter_generator)
      apply(simp add: split_beta)
      apply(rule disjI1 exI conjI refl)+
      apply(subst next_filter_generator)
      apply(simp add: split_beta)
      done
  next
    case (step s)
    from step.hyps
    have "list.unfoldr (filter_generator g) s = list.unfoldr (filter_generator g) (snd (list.next g s))"
      apply(subst (1 2) list.unfoldr.simps)
      apply(subst has_next_filter_generator)
      apply(subst next_filter_generator)
      apply(auto simp add: split_beta)
      done
    moreover from step.hyps
    have "filter P (list.unfoldr g (snd (list.next g s))) = filter P (list.unfoldr g s)"
      by(subst (2) list.unfoldr.simps)(auto simp add: split_beta)
    ultimately show ?case using step.IH by simp
  qed
qed

end

subsection ‹Destroying lists›

definition hd_fusion :: "('a, 's) generator  's  'a"
where "hd_fusion g s = hd (list.unfoldr g s)"

lemma hd_fusion_code [code]:
  "hd_fusion g s = (if list.has_next g s then fst (list.next g s) else undefined)"
unfolding hd_fusion_def
by(subst list.unfoldr.simps)(simp add: hd_def split_beta)

declare hd_fusion_def [symmetric, code_unfold]

definition fold_fusion :: "('a, 's) generator  ('a  'b  'b)  's  'b  'b"
where "fold_fusion g f s = fold f (list.unfoldr g s)"

lemma fold_fusion_code [code]:
  "fold_fusion g f s b =
  (if list.has_next g s then
     let (x, s') = list.next g s
     in fold_fusion g f s' (f x b)
   else b)"
unfolding fold_fusion_def
by(subst list.unfoldr.simps)(simp add: split_beta)

declare fold_fusion_def[symmetric, code_unfold]

definition gen_length_fusion :: "('a, 's) generator  nat  's  nat"
where "gen_length_fusion g n s = n + length (list.unfoldr g s)"

lemma gen_length_fusion_code [code]:
  "gen_length_fusion g n s =
  (if list.has_next g s then gen_length_fusion g (Suc n) (snd (list.next g s)) else n)"
unfolding gen_length_fusion_def
by(subst list.unfoldr.simps)(simp add: split_beta)

definition length_fusion :: "('a, 's) generator  's  nat"
where "length_fusion g s = length (list.unfoldr g s)"

lemma length_fusion_code [code]:
  "length_fusion g = gen_length_fusion g 0"
by(simp add: fun_eq_iff length_fusion_def gen_length_fusion_def)

declare length_fusion_def[symmetric, code_unfold]

definition map_fusion :: "('a  'b)  ('a, 's) generator  's  'b list"
where "map_fusion f g s = map f (list.unfoldr g s)"

lemma map_fusion_code [code]:
  "map_fusion f g s =
  (if list.has_next g s then
     let (x, s') = list.next g s
     in f x # map_fusion f g s'
   else [])"
unfolding map_fusion_def
by(subst list.unfoldr.simps)(simp add: split_beta)

declare map_fusion_def[symmetric, code_unfold]

definition append_fusion :: "('a, 's1) generator  ('a, 's2) generator  's1  's2  'a list"
where "append_fusion g1 g2 s1 s2 = list.unfoldr g1 s1 @ list.unfoldr g2 s2"

lemma append_fusion [code]:
  "append_fusion g1 g2 s1 s2 =
  (if list.has_next g1 s1 then
     let (x, s1') = list.next g1 s1
     in x # append_fusion g1 g2 s1' s2
   else list.unfoldr g2 s2)"
unfolding append_fusion_def
by(subst list.unfoldr.simps)(simp add: split_beta)

declare append_fusion_def[symmetric, code_unfold]

definition zip_fusion :: "('a, 's1) generator  ('b, 's2) generator  's1  's2  ('a × 'b) list"
where "zip_fusion g1 g2 s1 s2 = zip (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma zip_fusion_code [code]:
  "zip_fusion g1 g2 s1 s2 =
  (if list.has_next g1 s1  list.has_next g2 s2 then
     let (x, s1') = list.next g1 s1;
         (y, s2') = list.next g2 s2
     in (x, y) # zip_fusion g1 g2 s1' s2'
   else [])"
unfolding zip_fusion_def
by(subst (1 2) list.unfoldr.simps)(simp add: split_beta)

declare zip_fusion_def[symmetric, code_unfold]

definition list_all_fusion :: "('a, 's) generator  ('a  bool)  's  bool"
where "list_all_fusion g P s = List.list_all P (list.unfoldr g s)"

lemma list_all_fusion_code [code]:
  "list_all_fusion g P s 
  (list.has_next g s 
   (let (x, s') = list.next g s
    in P x  list_all_fusion g P s'))"
unfolding list_all_fusion_def
by(subst list.unfoldr.simps)(simp add: split_beta)

declare list_all_fusion_def[symmetric, code_unfold]

definition list_all2_fusion :: "('a  'b  bool)  ('a, 's1) generator  ('b, 's2) generator  's1  's2  bool"
where
  "list_all2_fusion P g1 g2 s1 s2 = 
   list_all2 P (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma list_all2_fusion_code [code]:
  "list_all2_fusion P g1 g2 s1 s2 =
  (if list.has_next g1 s1 then
     list.has_next g2 s2 
     (let (x, s1') = list.next g1 s1;
          (y, s2') = list.next g2 s2
      in P x y  list_all2_fusion P g1 g2 s1' s2')
   else ¬ list.has_next g2 s2)"
unfolding list_all2_fusion_def
by(subst (1 2) list.unfoldr.simps)(simp add: split_beta)

declare list_all2_fusion_def[symmetric, code_unfold]

definition singleton_list_fusion :: "('a, 'state) generator  'state  bool"
where "singleton_list_fusion gen state = (case list.unfoldr gen state of [_]  True | _  False)"

lemma singleton_list_fusion_code [code]:
  "singleton_list_fusion g s 
  list.has_next g s  ¬ list.has_next g (snd (list.next g s))"
by(auto 4 5 simp add: singleton_list_fusion_def split: list.split if_split_asm prod.splits elim: list.unfoldr.elims dest: sym)

end

Theory Lexicographic_Order

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

theory Lexicographic_Order imports
  List_Fusion
  "HOL-Library.Char_ord"
begin

hide_const (open) List.lexordp

section ‹List fusion for lexicographic order›

context linorder begin

lemma lexordp_take_index_conv:
  "lexordp xs ys  
   (length xs < length ys  take (length xs) ys = xs) 
   (i < min (length xs) (length ys). take i xs = take i ys  xs ! i < ys ! i)"
  (is "?lhs = ?rhs")
proof
  assume ?lhs thus ?rhs
    by induct (auto 4 3 del: disjCI intro: disjI2 exI[where x="Suc i" for i])
next
  assume ?rhs (is "?prefix  ?less") thus ?lhs 
  proof
    assume "?prefix"
    hence "ys = xs @ hd (drop (length xs) ys) # tl (drop (length xs) ys)"
      by (metis append_Nil2 append_take_drop_id less_not_refl list.collapse)
    thus ?thesis unfolding lexordp_iff by blast
  next
    assume "?less"
    then obtain i where "i < min (length xs) (length ys)"
      and "take i xs = take i ys" and nth: "xs ! i < ys ! i" by blast
    hence "xs = take i xs @ xs ! i # drop (Suc i) xs" "ys = take i xs @ ys ! i # drop (Suc i) ys"
      by -(subst append_take_drop_id[symmetric, of _ i], simp_all add: Cons_nth_drop_Suc)
    with nth show ?thesis unfolding lexordp_iff by blast
  qed
qed

― ‹lexord is extension of partial ordering List.lex› 
lemma lexordp_lex: "(xs, ys)  lex {(xs, ys). xs < ys}  lexordp xs ys  length xs = length ys"
proof(induct xs arbitrary: ys)
  case Nil thus ?case by clarsimp
next
  case Cons thus ?case by(cases ys)(simp_all, safe, simp)
qed

end                

subsection ‹Setup for list fusion›

context ord begin

definition lexord_fusion :: "('a, 's1) generator  ('a, 's2) generator  's1  's2  bool"
where [code del]: "lexord_fusion g1 g2 s1 s2 = lexordp (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

definition lexord_eq_fusion :: "('a, 's1) generator  ('a, 's2) generator  's1  's2  bool"
where [code del]: "lexord_eq_fusion g1 g2 s1 s2 = lexordp_eq (list.unfoldr g1 s1) (list.unfoldr g2 s2)"

lemma lexord_fusion_code:
  "lexord_fusion g1 g2 s1 s2 
  (if list.has_next g1 s1 then
     if list.has_next g2 s2 then
       let (x, s1') = list.next g1 s1;
           (y, s2') = list.next g2 s2
       in x < y  ¬ y < x  lexord_fusion g1 g2 s1' s2'
     else False
   else list.has_next g2 s2)"
unfolding lexord_fusion_def
by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm)

lemma lexord_eq_fusion_code:
  "lexord_eq_fusion g1 g2 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 x < y  ¬ y < x  lexord_eq_fusion g1 g2 s1' s2'))"
unfolding lexord_eq_fusion_def
by(subst (1 2) list.unfoldr.simps)(auto split: prod.split_asm)

end

lemmas [code] =
  lexord_fusion_code ord.lexord_fusion_code
  lexord_eq_fusion_code ord.lexord_eq_fusion_code

lemmas [symmetric, code_unfold] =
  lexord_fusion_def ord.lexord_fusion_def
  lexord_eq_fusion_def ord.lexord_eq_fusion_def

end

Theory Extend_Partial_Order

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

theory Extend_Partial_Order
imports Main
begin

section ‹Every partial order can be extended to a total order›

lemma ChainsD: " x  C; C  Chains r; y  C   (x, y)  r  (y, x)  r"
by(simp add: Chains_def)

lemma Chains_Field: " C  Chains r; x  C   x  Field r"
by(auto simp add: Chains_def Field_def)

lemma total_onD:
  " total_on A r; x  A; y  A   (x, y)  r  x = y  (y, x)  r"
unfolding total_on_def by blast

lemma linear_order_imp_linorder: "linear_order {(A, B). leq A B}  class.linorder leq (λx y. leq x y  ¬ leq y x)"
by(unfold_locales)(auto 4 4 simp add: linear_order_on_def partial_order_on_def preorder_on_def dest: refl_onD antisymD transD total_onD)

lemma (in linorder) linear_order: "linear_order {(A, B). A  B}"
by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def total_on_def intro: refl_onI antisymI transI)


definition order_consistent :: "('a × 'a) set  ('a × 'a) set  bool"
where "order_consistent r s  (a a'. (a, a')  r  (a', a)  s  a = a')"

lemma order_consistent_sym:
  "order_consistent r s  order_consistent s r"
by(auto simp add: order_consistent_def)

lemma antisym_order_consistent_self:
  "antisym r  order_consistent r r"
by(auto simp add: order_consistent_def dest: antisymD)


lemma refl_on_trancl:
  assumes "refl_on A r"
  shows "refl_on A (r^+)"
proof(rule refl_onI, safe del: conjI)
  fix a b
  assume "(a, b)  r^+"
  thus "a  A  b  A"
    by induct(blast intro: refl_onD1[OF assms] refl_onD2[OF assms])+
qed(blast dest: refl_onD[OF assms])

lemma total_on_refl_on_consistent_into:
  assumes r: "total_on A r" "refl_on A r"
  and consist: "order_consistent r s"
  and x: "x  A" and y: "y  A" and s: "(x, y)  s"
  shows "(x, y)  r"
proof(cases "x = y")
  case False
  with r x y have "(x, y)  r  (y, x)  r" unfolding total_on_def by blast
  thus ?thesis
  proof
    assume "(y, x)  r"
    with s consist have "x = y" unfolding order_consistent_def by blast
    with False show ?thesis by contradiction
  qed
qed(blast intro: refl_onD r x y)

lemma porder_linorder_tranclpE [consumes 5, case_names base step]:
  assumes r: "partial_order_on A r"
  and s: "linear_order_on B s"
  and consist: "order_consistent r s"
  and B_subset_A: "B  A"
  and trancl: "(x, y)  (r  s)^+"
  obtains "(x, y)  r"
        | u v where "(x, u)  r" "(u, v)  s" "(v, y)  r"
proof(atomize_elim)
  from r have "refl_on A r" "trans r" by(simp_all add: partial_order_on_def preorder_on_def)
  from s have "refl_on B s" "total_on B s" "trans s"
    by(simp_all add: partial_order_on_def preorder_on_def linear_order_on_def)

  from trancl show "(x, y)  r  (u v. (x, u)  r  (u, v)  s  (v, y)  r)"
  proof(induction)
    case (base y)
    thus ?case
    proof
      assume "(x, y)  s"
      with ‹refl_on B s have "x  B" "y  B"
        by(blast dest: refl_onD1 refl_onD2)+
      with B_subset_A have "x  A" "y  A" by blast+
      hence "(x, x)  r" "(y, y)  r"
        using ‹refl_on A r by(blast intro: refl_onD)+
      with (x, y)  s show ?thesis by blast
    qed(simp)
  next
    case (step y z)
    from (y, z)  r  s show ?case
    proof
      assume "(y, z)  s"
      with ‹refl_on B s have "y  B" "z  B"
        by(blast dest: refl_onD2 refl_onD1)+
      from step.IH show ?thesis
      proof
        assume "(x, y)  r"
        moreover from z  B B_subset_A ‹refl_on A r 
        have "(z, z)  r" by(blast dest: refl_onD)
        ultimately show ?thesis using (y, z)  s by blast
      next
        assume "u v. (x, u)  r  (u, v)  s  (v, y)  r"
        then obtain u v where "(x, u)  r" "(u, v)  s" "(v, y)  r" by blast
        from ‹refl_on B s (u, v)  s have "v  B" by(rule refl_onD2)
        with ‹total_on B s ‹refl_on B s order_consistent_sym[OF consist]
        have "(v, y)  s" using y  B (v, y)  r
          by(rule total_on_refl_on_consistent_into)
        with ‹trans s have "(v, z)  s" using (y, z)  s by(rule transD)
        with ‹trans s (u, v)  s have "(u, z)  s" by(rule transD)
        moreover from z  B B_subset_A have "z  A" ..
        with ‹refl_on A r have "(z, z)  r" by(rule refl_onD)
        ultimately show ?thesis using (x, u)  r by blast
      qed
    next
      assume "(y, z)  r"
      with step.IH show ?thesis
        by(blast intro: transD[OF ‹trans r])
    qed
  qed
qed

lemma porder_on_consistent_linorder_on_trancl_antisym:
  assumes r: "partial_order_on A r"
  and s: "linear_order_on B s"
  and consist: "order_consistent r s"
  and B_subset_A: "B  A"
  shows "antisym ((r  s)^+)"
proof(rule antisymI)
  fix x y
  let ?rs = "(r  s)^+"
  assume "(x, y)  ?rs" "(y, x)  ?rs"
  from r have "antisym r" "trans r" by(simp_all add: partial_order_on_def preorder_on_def)
  from s have "total_on B s" "refl_on B s" "trans s" "antisym s"
    by(simp_all add: partial_order_on_def preorder_on_def linear_order_on_def)

  from r s consist B_subset_A (x, y)  ?rs
  show "x = y"
  proof(cases rule: porder_linorder_tranclpE)
    case base
    from r s consist B_subset_A (y, x)  ?rs
    show ?thesis
    proof(cases rule: porder_linorder_tranclpE)
      case base
      with ‹antisym r (x, y)  r show ?thesis by(rule antisymD)
    next
      case (step u v)
      from (v, x)  r (x, y)  r (y, u)  r have "(v, u)  r"
        by(blast intro: transD[OF ‹trans r])
      with consist have "v = u" using (u, v)  s 
        by(simp add: order_consistent_def) 
      with (y, u)  r (v, x)  r have "(y, x)  r"
        by(blast intro: transD[OF ‹trans r])
      with ‹antisym r (x, y)  r show ?thesis by(rule antisymD)
    qed
  next
    case (step u v)
    from r s consist B_subset_A (y, x)  ?rs
    show ?thesis
    proof(cases rule: porder_linorder_tranclpE)
      case base
      from (v, y)  r (y, x)  r (x, u)  r have "(v, u)  r"
        by(blast intro: transD[OF ‹trans r])
      with consist (u, v)  s
      have "u = v" by(auto simp add: order_consistent_def)
      with (v, y)  r (x, u)  r have "(x, y)  r"
        by(blast intro: transD[OF ‹trans r])
      with ‹antisym r show ?thesis using (y, x)  r by(rule antisymD)
    next
      case (step u' v')
      note r_into_s = total_on_refl_on_consistent_into[OF ‹total_on B s ‹refl_on B s order_consistent_sym[OF consist]]
      from ‹refl_on B s (u, v)  s (u', v')  s
      have "u  B" "v  B" "u'  B" "v'  B" by(blast dest: refl_onD1 refl_onD2)+
      from ‹trans r (v', x)  r (x, u)  r have "(v', u)  r" by(rule transD)
      with v'  B u  B have "(v', u)  s" by(rule r_into_s)
      also note (u, v)  s also (transD[OF ‹trans s])
      from ‹trans r (v, y)  r (y, u')  r have "(v, u')  r" by(rule transD)
      with v  B u'  B have "(v, u')  s" by(rule r_into_s)
      finally (transD[OF ‹trans s])
      have "v' = u'" using (u', v')  s by(rule antisymD[OF ‹antisym s])
      moreover with (v, u')  s (v', u)  s have "(v, u)  s"
        by(blast intro: transD[OF ‹trans s])
      with ‹antisym s (u, v)  s have "u = v" by(rule antisymD)
      ultimately have "(x, y)  r" "(y, x)  r"
        using (x, u)  r (v, y)  r (y, u')  r (v', x)  r
        by(blast intro: transD[OF ‹trans r])+
      with ‹antisym r show ?thesis by(rule antisymD)
    qed
  qed
qed

lemma porder_on_linorder_on_tranclp_porder_onI:
  assumes r: "partial_order_on A r"
  and s: "linear_order_on B s" 
  and consist: "order_consistent r s"
  and subset: "B  A"
  shows "partial_order_on A ((r  s)^+)"
  unfolding partial_order_on_def preorder_on_def
proof(intro conjI)
  let ?rs = "r  s"
  from r have "refl_on A r" by(simp add: partial_order_on_def preorder_on_def)
  moreover from s have "refl_on B s"
    by(simp add: linear_order_on_def partial_order_on_def preorder_on_def)
  ultimately have "refl_on (A  B) ?rs" by(rule refl_on_Un)
  also from subset have "A  B = A" by blast
  finally show "refl_on A (?rs^+)" by(rule refl_on_trancl)

  show "trans (?rs^+)" by(rule trans_trancl)

  from r s consist subset show "antisym (?rs^+)"
    by(rule porder_on_consistent_linorder_on_trancl_antisym)
qed

lemma porder_extend_to_linorder:
  assumes r: "partial_order_on A r"
  obtains s where "linear_order_on A s" "order_consistent r s"
proof(atomize_elim)
  define S where "S = {s. partial_order_on A s  r  s}"
  from r have r_in_S: "r  S" unfolding S_def by auto

  have "yS. xS. y  x  x = y"
  proof(rule Zorn_Lemma2[rule_format])
    fix c
    assume "c  chains S"
    hence "c  S" by(rule chainsD2)

    show "yS. xc. x  y"
    proof(cases "c = {}")
      case True
      with r_in_S show ?thesis by blast
    next
      case False
      then obtain s where "s  c" by blast
      hence s: "partial_order_on A s"
        and r_in_s: "r  s"
        using c  S unfolding S_def by blast+

      have "partial_order_on A (c)"
        unfolding partial_order_on_def preorder_on_def
      proof(intro conjI)
        show "refl_on A (c)"
        proof(rule refl_onI[OF subsetI])
          fix x
          assume "x  c"
          then obtain X where "X  c" and "x  X" by blast
          from X  c c  S have "X  S" ..
          hence "partial_order_on A X" unfolding S_def by simp
          with x  X show "x  A × A"
            by(cases x)(auto simp add: partial_order_on_def preorder_on_def dest: refl_onD1 refl_onD2)
        next
          fix x
          assume "x  A"
          with s have "(x, x)  s" unfolding partial_order_on_def preorder_on_def
            by(blast dest: refl_onD)
          with s  c show "(x, x)  c" by(rule UnionI)
        qed

        show "antisym (c)"
        proof(rule antisymI)
          fix x y
          assume "(x, y)  c" "(y, x)  c"
          then obtain X Y where "X  c" "Y  c" "(x, y)  X" "(y, x)  Y" by blast
          from X  c Y  c c  S have "antisym X" "antisym Y"
            unfolding S_def by(auto simp add: partial_order_on_def)
          moreover from c  chains S X  c Y  c 
          have "X  Y  Y  X" by(rule chainsD)
          ultimately show "x = y" using (x, y)  X (y, x)  Y 
            by(auto dest: antisymD)
        qed

        show "trans (c)"
        proof(rule transI)
          fix x y z
          assume "(x, y)  c" "(y, z)  c"
          then obtain X Y where "X  c" "Y  c" "(x, y)  X" "(y, z)  Y" by blast
          from X  c Y  c c  S have "trans X" "trans Y"
            unfolding S_def by(auto simp add: partial_order_on_def preorder_on_def)
          from c  chains S X  c Y  c 
          have "X  Y  Y  X" by(rule chainsD)
          thus "(x, z)  c"
          proof
            assume "X  Y"
            with ‹trans Y (x, y)  X (y, z)  Y
            have "(x, z)  Y" by(blast dest: transD)
            with Y  c show ?thesis by(rule UnionI)
          next
            assume "Y  X"
            with ‹trans X (x, y)  X (y, z)  Y
            have "(x, z)  X" by(blast dest: transD)
            with X  c show ?thesis by(rule UnionI)
          qed
        qed
      qed
      moreover
      have "r  c" using r_in_s s  c by blast
      ultimately have "c  S" unfolding S_def by simp
      thus ?thesis by blast
    qed
  qed
  then obtain s where "s  S" and y_max: "t.  t  S; s  t   s = t" by blast

  have "partial_order_on A s" using s  S
    unfolding S_def by simp
  moreover
  have r_in_s: "r  s" using s  S unfolding S_def by blast

  have "total_on A s"
    unfolding total_on_def
  proof(intro strip)
    fix x y
    assume "x  A" "y  A" "x  y" 
    show "(x, y)  s  (y, x)  s"
    proof(rule ccontr)
      assume "¬ ?thesis"
      hence xy: "(x, y)  s" "(y, x)  s" by simp_all

      define s' where "s' = {(a, b). a = x  (b = y  b = x)  a = y  b = y}"
      let ?s' = "(s  s')^+"
      note ‹partial_order_on A s
      moreover have "linear_order_on {x, y} s'" unfolding s'_def
        by(auto simp add: linear_order_on_def partial_order_on_def preorder_on_def total_on_def intro: refl_onI transI antisymI)
      moreover have "order_consistent s s'"
        unfolding s'_def using xy unfolding order_consistent_def by blast
      moreover have "{x, y}  A" using x  A y  A by blast
      ultimately have "partial_order_on A ?s'"
        by(rule porder_on_linorder_on_tranclp_porder_onI)
      moreover have "r  ?s'" using r_in_s by auto
      ultimately have "?s'  S" unfolding S_def by simp
      moreover have "s  ?s'" by auto
      ultimately have "s = ?s'" by(rule y_max)
      moreover have "(x, y)  ?s'" by(auto simp add: s'_def)
      ultimately show False using (x, y)  s by simp
    qed
  qed
  ultimately have "linear_order_on A s" by(simp add: linear_order_on_def)
  moreover have "order_consistent r s" unfolding order_consistent_def
  proof(intro strip)
    fix a a'
    assume "(a, a')  r" "(a', a)  s"
    from (a, a')  r have "(a, a')  s" using r_in_s by blast
    with ‹partial_order_on A s (a', a)  s
    show "a = a'" unfolding partial_order_on_def by(blast dest: antisymD)
  qed
  ultimately show "s. linear_order_on A s  order_consistent r s" by blast
qed

end

Theory Set_Linorder

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

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

section ‹An executable linear order on sets›

subsection ‹Definition of the linear order›

subsubsection ‹Extending finite and cofinite sets›

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

consts infinite_complement_partition :: "'a set set"

specification (infinite_complement_partition)
  finite_complement_partition: "finite (A :: 'a set)  A  infinite_complement_partition"
  complement_partition: "¬ finite (UNIV :: 'a set)
     (A :: 'a set)  infinite_complement_partition  - A  infinite_complement_partition"
proof(cases "finite (UNIV :: 'a set)")
  case False
  define Field_r where "Field_r = {𝒫 :: 'a set set. (C  𝒫. - C  𝒫)  (A. finite A  A  𝒫)}"
  define r where "r = {(𝒫1, 𝒫2). 𝒫1  𝒫2  𝒫1  Field_r  𝒫2  Field_r}"
  have in_Field_r [simp]: "𝒫. 𝒫  Field_r  (C  𝒫. - C  𝒫)  (A. finite A  A  𝒫)"
    unfolding Field_r_def by simp
  have in_r [simp]: "𝒫1 𝒫2. (𝒫1, 𝒫2)  r  𝒫1  𝒫2  𝒫1  Field_r  𝒫2  Field_r"
    unfolding r_def by simp
  have Field_r [simp]: "Field r = Field_r" by(auto simp add: Field_def Field_r_def)
  
  have "Partial_order r"
    by(auto simp add: Field_def r_def partial_order_on_def preorder_on_def intro!: refl_onI transI antisymI)
  moreover have "  Field r. 𝒜  . (𝒜, )  r" if: "  Chains r" for 
  proof -
    let ?ℬ = "  {A. finite A}"
    have *: "?ℬ  Field r" using False ℭ
      by clarsimp(safe, drule (2) ChainsD, auto 4 4 dest: Chains_Field)
    hence "𝒜. 𝒜    (𝒜, ?ℬ)  r"
      usingby(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)"
              by(auto simp del: last.simps sorted.simps(2) intro: above_upclosed dest: sorted_last)
            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.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.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.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