[STATEMENT]
lemma set_less_aux_Compl_iff:
  "set_less_aux_Compl ao xs ys \<longleftrightarrow> set_less_eq_aux_Compl ao xs ys \<and> \<not> Compl_set_less_eq_aux ao ys xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_less_aux_Compl ao xs ys = (set_less_eq_aux_Compl ao xs ys \<and> \<not> Compl_set_less_eq_aux ao ys xs)
[PROOF STEP]
by(induct ao xs ys rule: set_less_aux_Compl.induct)(auto simp add: not_less_iff_gr_or_eq)


[STATEMENT]
lemma Compl_set_less_aux_Compl_iff:
  "Compl_set_less_aux ao xs ys \<longleftrightarrow> Compl_set_less_eq_aux ao xs ys \<and> \<not> set_less_eq_aux_Compl ao ys xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Compl_set_less_aux ao xs ys = (Compl_set_less_eq_aux ao xs ys \<and> \<not> set_less_eq_aux_Compl ao ys xs)
[PROOF STEP]
by(induct ao xs ys rule: Compl_set_less_aux.induct)(auto simp add: not_less_iff_gr_or_eq)


[STATEMENT]
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 \<sqsubset>' - set ys \<longleftrightarrow> set_less_aux_Compl None xs ys" (is ?Compl2)
  and Compl1_set_less_aux_conv_Compl_set_less_aux:
  "- set xs \<sqsubset>' set ys \<longleftrightarrow> Compl_set_less_aux None xs ys" (is ?Compl1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (set xs \<sqsubset>' - set ys) = set_less_aux_Compl None xs ys &&& (- set xs \<sqsubset>' set ys) = Compl_set_less_aux None xs ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite UNIV
sorted xs
distinct xs
sorted ys
distinct ys

goal (1 subgoal):
 1. (set xs \<sqsubset>' - set ys) = set_less_aux_Compl None xs ys &&& (- set xs \<sqsubset>' set ys) = Compl_set_less_aux None xs ys
[PROOF STEP]
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)


[STATEMENT]
lemma length_last_Nil [code]: "length_last [] = (0, undefined)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length_last [] = (0, undefined)
[PROOF STEP]
by(simp add: length_last_def last_def)


[STATEMENT]
lemma length_last_Cons_code [symmetric, code]:
  "fold (\<lambda>x (n, _) . (n + 1, x)) xs (1, x) = length_last (x # xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold (\<lambda>x (n, uu_). (n + 1, x)) xs (1, x) = length_last (x # xs)
[PROOF STEP]
by(induct xs rule: rev_induct)(simp_all add: length_last_def)


[STATEMENT]
lemma exhaustive_above_iff:
  "\<lbrakk> sorted xs; distinct xs; \<forall>x'\<in>set xs. x < x' \<rbrakk> \<Longrightarrow> exhaustive_above x xs \<longleftrightarrow> set xs = {z. z > x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sorted xs; distinct xs; \<forall>x'\<in>set xs. x < x'\<rbrakk> \<Longrightarrow> exhaustive_above x xs = (set xs = {z. x < z})
[PROOF STEP]
proof(induction x xs rule: exhaustive_above.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted []; distinct []; Ball (set []) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x [] = (set [] = Collect ((<) x))
 2. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
sorted []
distinct []
\<forall>a\<in>set []. x_ < a

goal (2 subgoals):
 1. \<And>x. \<lbrakk>sorted []; distinct []; Ball (set []) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x [] = (set [] = Collect ((<) x))
 2. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted []
distinct []
\<forall>a\<in>set []. x_ < a

goal (1 subgoal):
 1. exhaustive_above x_ [] = (set [] = {a. x_ < a})
[PROOF STEP]
by(simp add: proper_interval_simps)
[PROOF STATE]
proof (state)
this:
exhaustive_above x_ [] = (set [] = {a. x_ < a})

goal (1 subgoal):
 1. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
case (2 x y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sorted ys; distinct ys; \<forall>a\<in>set ys. y < a\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = {a. y < a})
sorted (y # ys)
distinct (y # ys)
\<forall>a\<in>set (y # ys). x < a

goal (1 subgoal):
 1. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
from \<open>sorted (y # ys)\<close> \<open>distinct (y # ys)\<close>
[PROOF STATE]
proof (chain)
picking this:
sorted (y # ys)
distinct (y # ys)
[PROOF STEP]
have ys: "sorted ys" "distinct ys" and y: "\<forall>y'\<in>set ys. y < y'"
[PROOF STATE]
proof (prove)
using this:
sorted (y # ys)
distinct (y # ys)

goal (1 subgoal):
 1. (sorted ys &&& distinct ys) &&& \<forall>y'\<in>set ys. y < y'
[PROOF STEP]
by(auto simp add: less_le)
[PROOF STATE]
proof (state)
this:
sorted ys
distinct ys
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
hence "exhaustive_above y ys = (set ys = {z. y < z})"
[PROOF STATE]
proof (prove)
using this:
sorted ys
distinct ys
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. exhaustive_above y ys = (set ys = {z. y < z})
[PROOF STEP]
by(rule "2.IH")
[PROOF STATE]
proof (state)
this:
exhaustive_above y ys = (set ys = {z. y < z})

goal (1 subgoal):
 1. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
exhaustive_above y ys = (set ys = {z. y < z})

goal (1 subgoal):
 1. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
from \<open>\<forall>y'\<in>set (y # ys). x < y'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<forall>y'\<in>set (y # ys). x < y'
[PROOF STEP]
have "x < y"
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set (y # ys). x < y'

goal (1 subgoal):
 1. x < y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x < y

goal (1 subgoal):
 1. \<And>x y ys. \<lbrakk>\<lbrakk>sorted ys; distinct ys; Ball (set ys) ((<) y)\<rbrakk> \<Longrightarrow> exhaustive_above y ys = (set ys = Collect ((<) y)); sorted (y # ys); distinct (y # ys); Ball (set (y # ys)) ((<) x)\<rbrakk> \<Longrightarrow> exhaustive_above x (y # ys) = (set (y # ys) = Collect ((<) x))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
exhaustive_above y ys = (set ys = {z. y < z})
x < y
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
exhaustive_above y ys = (set ys = {z. y < z})
x < y

goal (1 subgoal):
 1. exhaustive_above x (y # ys) = (set (y # ys) = {a. x < a})
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
exhaustive_above y ys = (set ys = {z. y < z})
x < y
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. exhaustive_above x (y # ys) = (set (y # ys) = {a. x < a})
[PROOF STEP]
by(fastforce simp add: proper_interval_simps)
[PROOF STATE]
proof (state)
this:
exhaustive_above x (y # ys) = (set (y # ys) = {a. x < a})

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exhaustive_correct:
  assumes "sorted xs" "distinct xs"
  shows "exhaustive xs \<longleftrightarrow> set xs = UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustive xs = (set xs = UNIV)
[PROOF STEP]
proof(cases xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> exhaustive xs = (set xs = UNIV)
 2. \<And>a list. xs = a # list \<Longrightarrow> exhaustive xs = (set xs = UNIV)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs = []

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> exhaustive xs = (set xs = UNIV)
 2. \<And>a list. xs = a # list \<Longrightarrow> exhaustive xs = (set xs = UNIV)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. exhaustive xs = (set xs = UNIV)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
exhaustive xs = (set xs = UNIV)

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> exhaustive xs = (set xs = UNIV)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> exhaustive xs = (set xs = UNIV)
[PROOF STEP]
case Cons
[PROOF STATE]
proof (state)
this:
xs = a_ # list_

goal (1 subgoal):
 1. \<And>a list. xs = a # list \<Longrightarrow> exhaustive xs = (set xs = UNIV)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. exhaustive xs = (set xs = UNIV)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs

goal (1 subgoal):
 1. exhaustive xs = (set xs = UNIV)
[PROOF STEP]
unfolding Cons exhaustive.simps
[PROOF STATE]
proof (prove)
using this:
sorted (a_ # list_)
distinct (a_ # list_)

goal (1 subgoal):
 1. (\<not> proper_interval None (Some a_) \<and> exhaustive_above a_ list_) = (set (a_ # list_) = UNIV)
[PROOF STEP]
apply(subst exhaustive_above_iff)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>sorted (a_ # list_); distinct (a_ # list_)\<rbrakk> \<Longrightarrow> sorted list_
 2. \<lbrakk>sorted (a_ # list_); distinct (a_ # list_)\<rbrakk> \<Longrightarrow> distinct list_
 3. \<lbrakk>sorted (a_ # list_); distinct (a_ # list_)\<rbrakk> \<Longrightarrow> Ball (set list_) ((<) a_)
 4. \<lbrakk>sorted (a_ # list_); distinct (a_ # list_)\<rbrakk> \<Longrightarrow> (\<not> proper_interval None (Some a_) \<and> set list_ = Collect ((<) a_)) = (set (a_ # list_) = UNIV)
[PROOF STEP]
apply(auto simp add: less_le proper_interval_simps not_less intro: order_antisym)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
exhaustive xs = (set xs = UNIV)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
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 \<longleftrightarrow> (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
note [simp] = finite_subset[OF subset_UNIV fin]
[PROOF STATE]
proof (state)
this:
finite ?A

goal (1 subgoal):
 1. proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
using xs ys
[PROOF STATE]
proof (prove)
using this:
sorted xs
distinct xs
sorted ys
distinct ys

goal (1 subgoal):
 1. proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
proof(induction xs ys rule: proper_interval_set_aux.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>xs. \<lbrakk>sorted xs; distinct xs; sorted []; distinct []\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs [] = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set [])
 2. \<And>y ys. \<lbrakk>sorted []; distinct []; sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 3. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
sorted xs_
distinct xs_
sorted []
distinct []

goal (3 subgoals):
 1. \<And>xs. \<lbrakk>sorted xs; distinct xs; sorted []; distinct []\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs [] = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set [])
 2. \<And>y ys. \<lbrakk>sorted []; distinct []; sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 3. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
sorted xs_
distinct xs_
sorted []
distinct []

goal (1 subgoal):
 1. proper_interval_set_aux xs_ [] = (\<exists>A. set xs_ \<sqsubset>' A \<and> A \<sqsubset>' set [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux xs_ [] = (\<exists>A. set xs_ \<sqsubset>' A \<and> A \<sqsubset>' set [])

goal (2 subgoals):
 1. \<And>y ys. \<lbrakk>sorted []; distinct []; sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y ys. \<lbrakk>sorted []; distinct []; sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
case (2 y ys)
[PROOF STATE]
proof (state)
this:
sorted []
distinct []
sorted (y # ys)
distinct (y # ys)

goal (2 subgoals):
 1. \<And>y ys. \<lbrakk>sorted []; distinct []; sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
hence "\<forall>y'\<in>set ys. y < y'"
[PROOF STATE]
proof (prove)
using this:
sorted []
distinct []
sorted (y # ys)
distinct (y # ys)

goal (1 subgoal):
 1. \<forall>y'\<in>set ys. y < y'
[PROOF STEP]
by(auto simp add: less_le)
[PROOF STATE]
proof (state)
this:
\<forall>y'\<in>set ys. y < y'

goal (2 subgoals):
 1. \<And>y ys. \<lbrakk>sorted []; distinct []; sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
by(cases ys)(auto simp add: proper_interval_simps set_less_aux_singleton_iff intro: psubset_finite_imp_set_less_aux)
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux [] (y # ys) = (\<exists>A. set [] \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
case (3 x xs y ys)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
sorted (x # xs)
distinct (x # xs)
sorted (y # ys)
distinct (y # ys)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
from \<open>sorted (x # xs)\<close> \<open>distinct (x # xs)\<close>
[PROOF STATE]
proof (chain)
picking this:
sorted (x # xs)
distinct (x # xs)
[PROOF STEP]
have xs: "sorted xs" "distinct xs" and x: "\<forall>x'\<in>set xs. x < x'"
[PROOF STATE]
proof (prove)
using this:
sorted (x # xs)
distinct (x # xs)

goal (1 subgoal):
 1. (sorted xs &&& distinct xs) &&& \<forall>x'\<in>set xs. x < x'
[PROOF STEP]
by(auto simp add: less_le)
[PROOF STATE]
proof (state)
this:
sorted xs
distinct xs
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
from \<open>sorted (y # ys)\<close> \<open>distinct (y # ys)\<close>
[PROOF STATE]
proof (chain)
picking this:
sorted (y # ys)
distinct (y # ys)
[PROOF STEP]
have ys: "sorted ys" "distinct ys" and y: "\<forall>y'\<in>set ys. y < y'"
[PROOF STATE]
proof (prove)
using this:
sorted (y # ys)
distinct (y # ys)

goal (1 subgoal):
 1. (sorted ys &&& distinct ys) &&& \<forall>y'\<in>set ys. y < y'
[PROOF STEP]
by(auto simp add: less_le)
[PROOF STATE]
proof (state)
this:
sorted ys
distinct ys
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have Minxxs: "Min (set (x # xs)) = x" and xnxs: "x \<notin> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (set (x # xs)) = x &&& x \<notin> set xs
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. Min (set (x # xs)) = x &&& x \<notin> set xs
[PROOF STEP]
by(auto intro!: Min_eqI)
[PROOF STATE]
proof (state)
this:
Min (set (x # xs)) = x
x \<notin> set xs

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have Minyys: "Min (set (y # ys)) = y" and ynys: "y \<notin> set ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min (set (y # ys)) = y &&& y \<notin> set ys
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. Min (set (y # ys)) = y &&& y \<notin> set ys
[PROOF STEP]
by(auto intro!: Min_eqI)
[PROOF STATE]
proof (state)
this:
Min (set (y # ys)) = y
y \<notin> set ys

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>\<lbrakk>\<not> x < y; \<not> y < x; sorted xs; distinct xs; sorted ys; distinct ys\<rbrakk> \<Longrightarrow> proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys); sorted (x # xs); distinct (x # xs); sorted (y # ys); distinct (y # ys)\<rbrakk> \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
proof(cases "x < y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < y

goal (2 subgoals):
 1. x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
hence "set (y # ys) \<sqsubset>' set (x # xs)"
[PROOF STATE]
proof (prove)
using this:
x < y

goal (1 subgoal):
 1. set (y # ys) \<sqsubset>' set (x # xs)
[PROOF STEP]
using Minxxs Minyys
[PROOF STATE]
proof (prove)
using this:
x < y
Min (set (x # xs)) = x
Min (set (y # ys)) = y

goal (1 subgoal):
 1. set (y # ys) \<sqsubset>' set (x # xs)
[PROOF STEP]
by -(rule set_less_aux_Min_antimono, simp_all)
[PROOF STATE]
proof (state)
this:
set (y # ys) \<sqsubset>' set (x # xs)

goal (2 subgoals):
 1. x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<sqsubset>' set (x # xs)

goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
set (y # ys) \<sqsubset>' set (x # xs)
x < y

goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
by(auto dest: set_less_aux_trans set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < y

goal (1 subgoal):
 1. \<not> x < y \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
proof(cases "y < x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
y < x

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
y < x

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
assume "proper_interval (Some y) (Some x)"
[PROOF STATE]
proof (state)
this:
proper_interval (Some y) (Some x)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
proper_interval (Some y) (Some x)
[PROOF STEP]
obtain z where z: "y < z" "z < x"
[PROOF STATE]
proof (prove)
using this:
proper_interval (Some y) (Some x)

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>y < z; z < x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: proper_interval_simps)
[PROOF STATE]
proof (state)
this:
y < z
z < x

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
hence "set (x # xs) \<sqsubset>' {z}"
[PROOF STATE]
proof (prove)
using this:
y < z
z < x

goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' {z}
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
y < z
z < x
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' {z}
[PROOF STEP]
by -(rule set_less_aux_Min_antimono, auto)
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' {z}

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' {z}

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have "{z} \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z} \<sqsubset>' set (y # ys)
[PROOF STEP]
using z y Minyys
[PROOF STATE]
proof (prove)
using this:
y < z
z < x
\<forall>y'\<in>set ys. y < y'
Min (set (y # ys)) = y

goal (1 subgoal):
 1. {z} \<sqsubset>' set (y # ys)
[PROOF STEP]
by -(rule set_less_aux_Min_antimono, auto)
[PROOF STATE]
proof (state)
this:
{z} \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' {z}
{z} \<sqsubset>' set (y # ys)
[PROOF STEP]
have "\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' {z}
{z} \<sqsubset>' set (y # ys)

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
proper_interval (Some y) (Some x) \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
proper_interval (Some y) (Some x) \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
proper_interval (Some y) (Some x) \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
assume "ys \<noteq> []"
[PROOF STATE]
proof (state)
this:
ys \<noteq> []

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
hence "{y} \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []

goal (1 subgoal):
 1. {y} \<sqsubset>' set (y # ys)
[PROOF STEP]
using y
[PROOF STATE]
proof (prove)
using this:
ys \<noteq> []
\<forall>y'\<in>set ys. y < y'

goal (1 subgoal):
 1. {y} \<sqsubset>' set (y # ys)
[PROOF STEP]
by -(rule psubset_finite_imp_set_less_aux, auto simp add: neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
{y} \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{y} \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have "set (x # xs) \<sqsubset>' {y}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' {y}
[PROOF STEP]
using False True x
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
y < x
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' {y}
[PROOF STEP]
by -(rule set_less_aux_Min_antimono, auto)
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' {y}

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{y} \<sqsubset>' set (y # ys)
set (x # xs) \<sqsubset>' {y}
[PROOF STEP]
have "\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
{y} \<sqsubset>' set (y # ys)
set (x # xs) \<sqsubset>' {y}

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
ys \<noteq> [] \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys \<noteq> [] \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ys \<noteq> [] \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
assume "\<not> exhaustive_above x xs"
[PROOF STATE]
proof (state)
this:
\<not> exhaustive_above x xs

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> exhaustive_above x xs
[PROOF STEP]
obtain z where z: "z > x" "z \<notin> set xs"
[PROOF STATE]
proof (prove)
using this:
\<not> exhaustive_above x xs

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>x < z; z \<notin> set xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
\<not> exhaustive_above x xs
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>x < z; z \<notin> set xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: exhaustive_above_iff[OF xs x])
[PROOF STATE]
proof (state)
this:
x < z
z \<notin> set xs

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
let ?A = "insert z (set (x # xs))"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have "set (x # xs) \<sqsubset>' ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' insert z (set (x # xs))
[PROOF STEP]
using z
[PROOF STATE]
proof (prove)
using this:
x < z
z \<notin> set xs

goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' insert z (set (x # xs))
[PROOF STEP]
by -(rule psubset_finite_imp_set_less_aux, auto)
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' insert z (set (x # xs))

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' insert z (set (x # xs))

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have "?A \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert z (set (x # xs)) \<sqsubset>' set (y # ys)
[PROOF STEP]
using Minyys False True z x
[PROOF STATE]
proof (prove)
using this:
Min (set (y # ys)) = y
\<not> x < y
y < x
x < z
z \<notin> set xs
\<forall>x'\<in>set xs. x < x'

goal (1 subgoal):
 1. insert z (set (x # xs)) \<sqsubset>' set (y # ys)
[PROOF STEP]
by -(rule set_less_aux_Min_antimono, auto)
[PROOF STATE]
proof (state)
this:
insert z (set (x # xs)) \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' insert z (set (x # xs))
insert z (set (x # xs)) \<sqsubset>' set (y # ys)
[PROOF STEP]
have "\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' insert z (set (x # xs))
insert z (set (x # xs)) \<sqsubset>' set (y # ys)

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<not> exhaustive_above x xs \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> exhaustive_above x xs \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<not> exhaustive_above x xs \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
assume A: "set (x # xs) \<sqsubset>' A" and A': "A \<sqsubset>' {y}"
            and pi: "\<not> proper_interval (Some y) (Some x)"
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' A
A \<sqsubset>' {y}
\<not> proper_interval (Some y) (Some x)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' A
[PROOF STEP]
have nempty: "A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' A

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have "y \<notin> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<notin> A
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<in> A \<Longrightarrow> False
[PROOF STEP]
assume "y \<in> A"
[PROOF STATE]
proof (state)
this:
y \<in> A

goal (1 subgoal):
 1. y \<in> A \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<in> A

goal (1 subgoal):
 1. y \<in> A \<Longrightarrow> False
[PROOF STEP]
with A'
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' {y}
y \<in> A
[PROOF STEP]
have "A \<noteq> {y}"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' {y}
y \<in> A

goal (1 subgoal):
 1. A \<noteq> {y}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<noteq> {y}

goal (1 subgoal):
 1. y \<in> A \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<in> A
A \<noteq> {y}
[PROOF STEP]
have "{y} \<sqsubset>' A"
[PROOF STATE]
proof (prove)
using this:
y \<in> A
A \<noteq> {y}

goal (1 subgoal):
 1. {y} \<sqsubset>' A
[PROOF STEP]
by -(rule psubset_finite_imp_set_less_aux, auto)
[PROOF STATE]
proof (state)
this:
{y} \<sqsubset>' A

goal (1 subgoal):
 1. y \<in> A \<Longrightarrow> False
[PROOF STEP]
with A'
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' {y}
{y} \<sqsubset>' A
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' {y}
{y} \<sqsubset>' A

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y \<notin> A

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have "y < Min A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y < Min A
[PROOF STEP]
unfolding not_le[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Min A \<le> y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Min A \<le> y \<Longrightarrow> False
[PROOF STEP]
assume "Min A \<le> y"
[PROOF STATE]
proof (state)
this:
Min A \<le> y

goal (1 subgoal):
 1. Min A \<le> y \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Min A \<le> y

goal (1 subgoal):
 1. Min A \<le> y \<Longrightarrow> False
[PROOF STEP]
have "Min A \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Min A \<noteq> y
[PROOF STEP]
using \<open>y \<notin> A\<close> nempty
[PROOF STATE]
proof (prove)
using this:
y \<notin> A
A \<noteq> {}

goal (1 subgoal):
 1. Min A \<noteq> y
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
Min A \<noteq> y

goal (1 subgoal):
 1. Min A \<le> y \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Min A \<le> y
Min A \<noteq> y
[PROOF STEP]
have "Min A < Min {y}"
[PROOF STATE]
proof (prove)
using this:
Min A \<le> y
Min A \<noteq> y

goal (1 subgoal):
 1. Min A < Min {y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Min A < Min {y}

goal (1 subgoal):
 1. Min A \<le> y \<Longrightarrow> False
[PROOF STEP]
hence "{y} \<sqsubset>' A"
[PROOF STATE]
proof (prove)
using this:
Min A < Min {y}

goal (1 subgoal):
 1. {y} \<sqsubset>' A
[PROOF STEP]
by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
[PROOF STATE]
proof (state)
this:
{y} \<sqsubset>' A

goal (1 subgoal):
 1. Min A \<le> y \<Longrightarrow> False
[PROOF STEP]
with A'
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' {y}
{y} \<sqsubset>' A
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' {y}
{y} \<sqsubset>' A

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y < Min A

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
with pi nempty
[PROOF STATE]
proof (chain)
picking this:
\<not> proper_interval (Some y) (Some x)
A \<noteq> {}
y < Min A
[PROOF STEP]
have "x \<le> Min A"
[PROOF STATE]
proof (prove)
using this:
\<not> proper_interval (Some y) (Some x)
A \<noteq> {}
y < Min A

goal (1 subgoal):
 1. x \<le> Min A
[PROOF STEP]
by(auto simp add: proper_interval_simps)
[PROOF STATE]
proof (state)
this:
x \<le> Min A

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<le> Min A

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' A
[PROOF STEP]
obtain z where z: "z \<in> A" "z \<notin> set (x # xs)"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' A

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>z \<in> A; z \<notin> set (x # xs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: set_less_aux_def)
[PROOF STATE]
proof (state)
this:
z \<in> A
z \<notin> set (x # xs)

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
with \<open>x \<le> Min A\<close> nempty
[PROOF STATE]
proof (chain)
picking this:
x \<le> Min A
A \<noteq> {}
z \<in> A
z \<notin> set (x # xs)
[PROOF STEP]
have "x < z"
[PROOF STATE]
proof (prove)
using this:
x \<le> Min A
A \<noteq> {}
z \<in> A
z \<notin> set (x # xs)

goal (1 subgoal):
 1. x < z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x < z

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
with z
[PROOF STATE]
proof (chain)
picking this:
z \<in> A
z \<notin> set (x # xs)
x < z
[PROOF STEP]
have "\<not> exhaustive_above x xs"
[PROOF STATE]
proof (prove)
using this:
z \<in> A
z \<notin> set (x # xs)
x < z

goal (1 subgoal):
 1. \<not> exhaustive_above x xs
[PROOF STEP]
by(auto simp add: exhaustive_above_iff[OF xs x])
[PROOF STATE]
proof (state)
this:
\<not> exhaustive_above x xs

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>set (x # xs) \<sqsubset>' ?A2; ?A2 \<sqsubset>' {y}; \<not> proper_interval (Some y) (Some x)\<rbrakk> \<Longrightarrow> \<not> exhaustive_above x xs

goal (2 subgoals):
 1. y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
 2. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
proper_interval (Some y) (Some x) \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
ys \<noteq> [] \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
\<not> exhaustive_above x xs \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
\<lbrakk>set (x # xs) \<sqsubset>' ?A2; ?A2 \<sqsubset>' {y}; \<not> proper_interval (Some y) (Some x)\<rbrakk> \<Longrightarrow> \<not> exhaustive_above x xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proper_interval (Some y) (Some x) \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
ys \<noteq> [] \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
\<not> exhaustive_above x xs \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
\<lbrakk>set (x # xs) \<sqsubset>' ?A2; ?A2 \<sqsubset>' {y}; \<not> proper_interval (Some y) (Some x)\<rbrakk> \<Longrightarrow> \<not> exhaustive_above x xs

goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
using True False
[PROOF STATE]
proof (prove)
using this:
proper_interval (Some y) (Some x) \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
ys \<noteq> [] \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
\<not> exhaustive_above x xs \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
\<lbrakk>set (x # xs) \<sqsubset>' ?A2; ?A2 \<sqsubset>' {y}; \<not> proper_interval (Some y) (Some x)\<rbrakk> \<Longrightarrow> \<not> exhaustive_above x xs
y < x
\<not> x < y

goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> y < x

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
with \<open>\<not> x < y\<close>
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y
\<not> y < x
[PROOF STEP]
have "x = y"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
\<not> y < x

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
from \<open>\<not> x < y\<close> False
[PROOF STATE]
proof (chain)
picking this:
\<not> x < y
\<not> y < x
[PROOF STEP]
have "proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)"
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
\<not> y < x

goal (1 subgoal):
 1. proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
using xs ys
[PROOF STATE]
proof (prove)
using this:
\<not> x < y
\<not> y < x
sorted xs
distinct xs
sorted ys
distinct ys

goal (1 subgoal):
 1. proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)
[PROOF STEP]
by(rule "3.IH")
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
have "\<dots> = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))"
          (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
assume ?lhs
[PROOF STATE]
proof (state)
this:
\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
obtain A where A: "set xs \<sqsubset>' A"
            and A': "A \<sqsubset>' set ys"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>set xs \<sqsubset>' A; A \<sqsubset>' set ys\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set xs \<sqsubset>' A
A \<sqsubset>' set ys

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
hence nempty: "A \<noteq> {}" "ys \<noteq> []"
[PROOF STATE]
proof (prove)
using this:
set xs \<sqsubset>' A
A \<sqsubset>' set ys

goal (1 subgoal):
 1. A \<noteq> {} &&& ys \<noteq> []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<noteq> {}
ys \<noteq> []

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
let ?A = "insert y A"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
assume "Min A \<le> y"
[PROOF STATE]
proof (state)
this:
Min A \<le> y

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Min A \<le> y

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
from y nempty
[PROOF STATE]
proof (chain)
picking this:
\<forall>y'\<in>set ys. y < y'
A \<noteq> {}
ys \<noteq> []
[PROOF STEP]
have "y < Min (set ys)"
[PROOF STATE]
proof (prove)
using this:
\<forall>y'\<in>set ys. y < y'
A \<noteq> {}
ys \<noteq> []

goal (1 subgoal):
 1. y < Min (set ys)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y < Min (set ys)

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Min A < Min (set ys)
[PROOF STEP]
have "set ys \<sqsubset>' A"
[PROOF STATE]
proof (prove)
using this:
Min A < Min (set ys)

goal (1 subgoal):
 1. set ys \<sqsubset>' A
[PROOF STEP]
by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
[PROOF STATE]
proof (state)
this:
set ys \<sqsubset>' A

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
with A'
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' set ys
set ys \<sqsubset>' A
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' set ys
set ys \<sqsubset>' A

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Min A \<le> y \<Longrightarrow> False

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
hence MinA: "y < Min A"
[PROOF STATE]
proof (prove)
using this:
Min A \<le> y \<Longrightarrow> False

goal (1 subgoal):
 1. y < Min A
[PROOF STEP]
by(metis not_le)
[PROOF STATE]
proof (state)
this:
y < Min A

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
with nempty
[PROOF STATE]
proof (chain)
picking this:
A \<noteq> {}
ys \<noteq> []
y < Min A
[PROOF STEP]
have "y \<notin> A"
[PROOF STATE]
proof (prove)
using this:
A \<noteq> {}
ys \<noteq> []
y < Min A

goal (1 subgoal):
 1. y \<notin> A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<notin> A

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<notin> A

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
with MinA nempty
[PROOF STATE]
proof (chain)
picking this:
y < Min A
A \<noteq> {}
ys \<noteq> []
y \<notin> A
[PROOF STEP]
have MinyA: "Min ?A = y"
[PROOF STATE]
proof (prove)
using this:
y < Min A
A \<noteq> {}
ys \<noteq> []
y \<notin> A

goal (1 subgoal):
 1. Min (insert y A) = y
[PROOF STEP]
by -(rule Min_eqI, auto)
[PROOF STATE]
proof (state)
this:
Min (insert y A) = y

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<notin> A
Min (insert y A) = y
[PROOF STEP]
have A1: "set (x # xs) \<sqsubset>' ?A"
[PROOF STATE]
proof (prove)
using this:
y \<notin> A
Min (insert y A) = y

goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' insert y A
[PROOF STEP]
using \<open>x = y\<close> A Minxxs xnxs
[PROOF STATE]
proof (prove)
using this:
y \<notin> A
Min (insert y A) = y
x = y
set xs \<sqsubset>' A
Min (set (x # xs)) = x
x \<notin> set xs

goal (1 subgoal):
 1. set (x # xs) \<sqsubset>' insert y A
[PROOF STEP]
by(subst set_less_aux_rec) simp_all
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' insert y A

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' insert y A

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
have "?A \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert y A \<sqsubset>' set (y # ys)
[PROOF STEP]
using \<open>x = y\<close> MinyA \<open>y \<notin> A\<close> A' Minyys ynys
[PROOF STATE]
proof (prove)
using this:
x = y
Min (insert y A) = y
y \<notin> A
A \<sqsubset>' set ys
Min (set (y # ys)) = y
y \<notin> set ys

goal (1 subgoal):
 1. insert y A \<sqsubset>' set (y # ys)
[PROOF STEP]
by(subst set_less_aux_rec) simp_all
[PROOF STATE]
proof (state)
this:
insert y A \<sqsubset>' set (y # ys)

goal (2 subgoals):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys \<Longrightarrow> \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
 2. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' insert y A
insert y A \<sqsubset>' set (y # ys)
[PROOF STEP]
show ?rhs
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' insert y A
insert y A \<sqsubset>' set (y # ys)

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
assume "?rhs"
[PROOF STATE]
proof (state)
this:
\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)
[PROOF STEP]
obtain A where A: "set (x # xs) \<sqsubset>' A"
            and A': "A \<sqsubset>' set (y # ys)"
[PROOF STATE]
proof (prove)
using this:
\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys)

goal (1 subgoal):
 1. (\<And>A. \<lbrakk>set (x # xs) \<sqsubset>' A; A \<sqsubset>' set (y # ys)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
set (x # xs) \<sqsubset>' A
A \<sqsubset>' set (y # ys)

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
let ?A = "A - {x}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' A
[PROOF STEP]
have nempty: "A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' A

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
assume "x < Min A"
[PROOF STATE]
proof (state)
this:
x < Min A

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
hence "Min (set (x # xs)) < Min A"
[PROOF STATE]
proof (prove)
using this:
x < Min A

goal (1 subgoal):
 1. Min (set (x # xs)) < Min A
[PROOF STEP]
unfolding Minxxs
[PROOF STATE]
proof (prove)
using this:
x < Min A

goal (1 subgoal):
 1. x < Min A
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Min (set (x # xs)) < Min A

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
hence "A \<sqsubset>' set (x # xs)"
[PROOF STATE]
proof (prove)
using this:
Min (set (x # xs)) < Min A

goal (1 subgoal):
 1. A \<sqsubset>' set (x # xs)
[PROOF STEP]
by(rule set_less_aux_Min_antimono) simp_all
[PROOF STATE]
proof (state)
this:
A \<sqsubset>' set (x # xs)

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
with A
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' A
A \<sqsubset>' set (x # xs)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' A
A \<sqsubset>' set (x # xs)

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x < Min A \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x < Min A \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x < Min A \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
assume "Min A < x"
[PROOF STATE]
proof (state)
this:
Min A < x

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
hence "Min A < Min (set (y # ys))"
[PROOF STATE]
proof (prove)
using this:
Min A < x

goal (1 subgoal):
 1. Min A < Min (set (y # ys))
[PROOF STEP]
unfolding \<open>x = y\<close> Minyys
[PROOF STATE]
proof (prove)
using this:
Min A < y

goal (1 subgoal):
 1. Min A < y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Min A < Min (set (y # ys))

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
hence "set (y # ys) \<sqsubset>' A"
[PROOF STATE]
proof (prove)
using this:
Min A < Min (set (y # ys))

goal (1 subgoal):
 1. set (y # ys) \<sqsubset>' A
[PROOF STEP]
by(rule set_less_aux_Min_antimono)(simp_all add: nempty)
[PROOF STATE]
proof (state)
this:
set (y # ys) \<sqsubset>' A

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
with A'
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' set (y # ys)
set (y # ys) \<sqsubset>' A
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' set (y # ys)
set (y # ys) \<sqsubset>' A

goal (1 subgoal):
 1. False
[PROOF STEP]
by(rule set_less_aux_antisym)
[PROOF STATE]
proof (state)
this:
False

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Min A < x \<Longrightarrow> False

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x < Min A \<Longrightarrow> False
Min A < x \<Longrightarrow> False
[PROOF STEP]
have MinA: "Min A = x"
[PROOF STATE]
proof (prove)
using this:
x < Min A \<Longrightarrow> False
Min A < x \<Longrightarrow> False

goal (1 subgoal):
 1. Min A = x
[PROOF STEP]
by(metis less_linear)
[PROOF STATE]
proof (state)
this:
Min A = x

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
hence "x \<in> A"
[PROOF STATE]
proof (prove)
using this:
Min A = x

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
using nempty
[PROOF STATE]
proof (prove)
using this:
Min A = x
A \<noteq> {}

goal (1 subgoal):
 1. x \<in> A
[PROOF STEP]
by(metis Min_in \<open>finite A\<close>)
[PROOF STATE]
proof (state)
this:
x \<in> A

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
from A nempty Minxxs xnxs
[PROOF STATE]
proof (chain)
picking this:
set (x # xs) \<sqsubset>' A
A \<noteq> {}
Min (set (x # xs)) = x
x \<notin> set xs
[PROOF STEP]
have "set xs \<sqsubset>' ?A"
[PROOF STATE]
proof (prove)
using this:
set (x # xs) \<sqsubset>' A
A \<noteq> {}
Min (set (x # xs)) = x
x \<notin> set xs

goal (1 subgoal):
 1. set xs \<sqsubset>' A - {x}
[PROOF STEP]
by(subst (asm) set_less_aux_rec)(auto simp add: MinA)
[PROOF STATE]
proof (state)
this:
set xs \<sqsubset>' A - {x}

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set xs \<sqsubset>' A - {x}

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
from A' \<open>x = y\<close> nempty Minyys MinA ynys
[PROOF STATE]
proof (chain)
picking this:
A \<sqsubset>' set (y # ys)
x = y
A \<noteq> {}
Min (set (y # ys)) = y
Min A = x
y \<notin> set ys
[PROOF STEP]
have "?A \<sqsubset>' set ys"
[PROOF STATE]
proof (prove)
using this:
A \<sqsubset>' set (y # ys)
x = y
A \<noteq> {}
Min (set (y # ys)) = y
Min A = x
y \<notin> set ys

goal (1 subgoal):
 1. A - {x} \<sqsubset>' set ys
[PROOF STEP]
by(subst (asm) set_less_aux_rec) simp_all
[PROOF STATE]
proof (state)
this:
A - {x} \<sqsubset>' set ys

goal (1 subgoal):
 1. \<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys) \<Longrightarrow> \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set xs \<sqsubset>' A - {x}
A - {x} \<sqsubset>' set ys
[PROOF STEP]
show ?lhs
[PROOF STATE]
proof (prove)
using this:
set xs \<sqsubset>' A - {x}
A - {x} \<sqsubset>' set ys

goal (1 subgoal):
 1. \<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal (1 subgoal):
 1. \<not> y < x \<Longrightarrow> proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
proper_interval_set_aux xs ys = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
proper_interval_set_aux xs ys = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
using \<open>x = y\<close>
[PROOF STATE]
proof (prove)
using this:
proper_interval_set_aux xs ys = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
x = y

goal (1 subgoal):
 1. proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux (x # xs) (y # ys) = (\<exists>A. set (x # xs) \<sqsubset>' A \<and> A \<sqsubset>' set (y # ys))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
proper_interval_set_aux xs ys = (\<exists>A. set xs \<sqsubset>' A \<and> A \<sqsubset>' set ys)

goal:
No subgoals!
[PROOF STEP]
qed