[STATEMENT]
theorem correctness:
  assumes "v \<in> vertices"
  shows "sccs (dfs v (init_env v)) = {S . is_scc S \<and> (\<forall>n\<in>S. reachable v n)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sccs (dfs v (init_env v)) = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
using assms init_env_pre_dfs[of v]
[PROOF STATE]
proof (prove)
using this:
v \<in> vertices
pre_dfs v (init_env v)

goal (1 subgoal):
 1. sccs (dfs v (init_env v)) = {S. is_scc S \<and> (\<forall>n\<in>S. reachable v n)}
[PROOF STEP]
by (simp add: dfs_dfss_termination partial_correctness)


[STATEMENT]
lemma is_process_REP_Bot :
  "is_process  ({(s,X). front_tickFree s}, {d. front_tickFree d})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_process ({(s, X). front_tickFree s}, {d. front_tickFree d})
[PROOF STEP]
by(auto simp: tickFree_implies_front_tickFree is_process_def
              FAILURES_def DIVERGENCES_def
        elim: Process.front_tickFree_dw_closed
        elim: Process.front_tickFree_append)


[STATEMENT]
lemma Rep_Abs_Bot :"Rep_process (Abs_process ({(s,X). front_tickFree s},{d. front_tickFree d})) =
                    ({(s,X). front_tickFree s},{d. front_tickFree d})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_process (Abs_process ({(s, X). front_tickFree s}, {d. front_tickFree d})) = ({(s, X). front_tickFree s}, {d. front_tickFree d})
[PROOF STEP]
by(subst Abs_process_inverse, simp_all only: CollectI Rep_process is_process_REP_Bot)


[STATEMENT]
lemma F_Bot: "F Bot = {(s,X). front_tickFree s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F Bot = {(s, X). front_tickFree s}
[PROOF STEP]
by(simp add: Bot_def FAILURES_def F_def Rep_Abs_Bot)


[STATEMENT]
lemma D_Bot: "D Bot = {d. front_tickFree d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D Bot = {d. front_tickFree d}
[PROOF STEP]
by(simp add: Bot_def DIVERGENCES_def D_def Rep_Abs_Bot)


[STATEMENT]
lemma T_Bot: "T Bot = {s. front_tickFree s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T Bot = {s. front_tickFree s}
[PROOF STEP]
by(simp add: Bot_def TRACES_def T_def FAILURES_def Rep_Abs_Bot)


[STATEMENT]
lemma Bot_is_UU[simp]: "Bot = \<bottom>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Bot = \<bottom>
[PROOF STEP]
apply(auto simp: Pcpo.eq_bottom_iff Process.le_approx_def Ra_def
                 min_elems_Collect_ftF_is_Nil Process.Nil_elem_T
                 F_Bot D_Bot T_Bot
           elim: D_imp_front_tickFree)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>\<not> front_tickFree s; (s, x) \<in> F \<bottom>\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
apply(metis Process.is_processT2)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma F_UU: "F \<bottom> = {(s,X). front_tickFree s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F \<bottom> = {(s, X). front_tickFree s}
[PROOF STEP]
using F_Bot
[PROOF STATE]
proof (prove)
using this:
F Bot = {(s, X). front_tickFree s}

goal (1 subgoal):
 1. F \<bottom> = {(s, X). front_tickFree s}
[PROOF STEP]
by auto


[STATEMENT]
lemma D_UU: "D \<bottom> = {d. front_tickFree d}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<bottom> = {d. front_tickFree d}
[PROOF STEP]
using D_Bot
[PROOF STATE]
proof (prove)
using this:
D Bot = {d. front_tickFree d}

goal (1 subgoal):
 1. D \<bottom> = {d. front_tickFree d}
[PROOF STEP]
by auto


[STATEMENT]
lemma T_UU: "T \<bottom> = {s. front_tickFree s}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<bottom> = {s. front_tickFree s}
[PROOF STEP]
using T_Bot
[PROOF STATE]
proof (prove)
using this:
T Bot = {s. front_tickFree s}

goal (1 subgoal):
 1. T \<bottom> = {s. front_tickFree s}
[PROOF STEP]
by auto


[STATEMENT]
lemma facetrelI: "v \<notin> y \<Longrightarrow> x = insert v y \<Longrightarrow> y \<lhd> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>v \<notin> y; x = insert v y\<rbrakk> \<Longrightarrow> y \<lhd> x
[PROOF STEP]
using facetrel_def
[PROOF STATE]
proof (prove)
using this:
?y \<lhd> ?x \<equiv> \<exists>v. v \<notin> ?y \<and> ?x = insert v ?y

goal (1 subgoal):
 1. \<lbrakk>v \<notin> y; x = insert v y\<rbrakk> \<Longrightarrow> y \<lhd> x
[PROOF STEP]
by fast


[STATEMENT]
lemma facetrelI_card: "y \<subseteq> x \<Longrightarrow> card (x-y) = 1 \<Longrightarrow> y \<lhd> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<subseteq> x; card (x - y) = 1\<rbrakk> \<Longrightarrow> y \<lhd> x
[PROOF STEP]
using card1[of "x-y"]
[PROOF STATE]
proof (prove)
using this:
card (x - y) = 1 \<Longrightarrow> \<exists>a. x - y = {a}

goal (1 subgoal):
 1. \<lbrakk>y \<subseteq> x; card (x - y) = 1\<rbrakk> \<Longrightarrow> y \<lhd> x
[PROOF STEP]
by (blast intro: facetrelI)


[STATEMENT]
lemma facetrel_complement_vertex: "y\<lhd>x \<Longrightarrow> x = insert v y \<Longrightarrow> v\<notin>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<lhd> x; x = insert v y\<rbrakk> \<Longrightarrow> v \<notin> y
[PROOF STEP]
using facetrel_def[of y x]
[PROOF STATE]
proof (prove)
using this:
y \<lhd> x \<equiv> \<exists>v. v \<notin> y \<and> x = insert v y

goal (1 subgoal):
 1. \<lbrakk>y \<lhd> x; x = insert v y\<rbrakk> \<Longrightarrow> v \<notin> y
[PROOF STEP]
by fastforce


[STATEMENT]
lemma facetrel_diff_vertex: "v\<in>x \<Longrightarrow> x-{v} \<lhd> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> x \<Longrightarrow> x - {v} \<lhd> x
[PROOF STEP]
by (auto intro: facetrelI)


[STATEMENT]
lemma facetrel_conv_insert: "y \<lhd> x \<Longrightarrow> v \<in> x - y \<Longrightarrow> x = insert v y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y \<lhd> x; v \<in> x - y\<rbrakk> \<Longrightarrow> x = insert v y
[PROOF STEP]
unfolding facetrel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>v. v \<notin> y \<and> x = insert v y; v \<in> x - y\<rbrakk> \<Longrightarrow> x = insert v y
[PROOF STEP]
by fast


[STATEMENT]
lemma facetrel_psubset: "y \<lhd> x \<Longrightarrow> y \<subset> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<lhd> x \<Longrightarrow> y \<subset> x
[PROOF STEP]
unfolding facetrel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>v. v \<notin> y \<and> x = insert v y \<Longrightarrow> y \<subset> x
[PROOF STEP]
by fast


[STATEMENT]
lemma facetrel_subset: "y \<lhd> x \<Longrightarrow> y \<subseteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<lhd> x \<Longrightarrow> y \<subseteq> x
[PROOF STEP]
using facetrel_psubset
[PROOF STATE]
proof (prove)
using this:
?y \<lhd> ?x \<Longrightarrow> ?y \<subset> ?x

goal (1 subgoal):
 1. y \<lhd> x \<Longrightarrow> y \<subseteq> x
[PROOF STEP]
by fast


[STATEMENT]
lemma facetrel_card: "y \<lhd> x \<Longrightarrow> card (x-y) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<lhd> x \<Longrightarrow> card (x - y) = 1
[PROOF STEP]
using insert_Diff_if[of _ y y]
[PROOF STATE]
proof (prove)
using this:
insert ?x y - y = (if ?x \<in> y then y - y else insert ?x (y - y))

goal (1 subgoal):
 1. y \<lhd> x \<Longrightarrow> card (x - y) = 1
[PROOF STEP]
unfolding facetrel_def
[PROOF STATE]
proof (prove)
using this:
insert ?x y - y = (if ?x \<in> y then y - y else insert ?x (y - y))

goal (1 subgoal):
 1. \<exists>v. v \<notin> y \<and> x = insert v y \<Longrightarrow> card (x - y) = 1
[PROOF STEP]
by fastforce


[STATEMENT]
lemma finite_facetrel_card: "finite x \<Longrightarrow> y\<lhd>x \<Longrightarrow> card x = Suc (card y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite x; y \<lhd> x\<rbrakk> \<Longrightarrow> card x = Suc (card y)
[PROOF STEP]
using facetrel_def[of y x] card_insert_disjoint[of x]
[PROOF STATE]
proof (prove)
using this:
y \<lhd> x \<equiv> \<exists>v. v \<notin> y \<and> x = insert v y
\<lbrakk>finite x; ?x \<notin> x\<rbrakk> \<Longrightarrow> card (insert ?x x) = Suc (card x)

goal (1 subgoal):
 1. \<lbrakk>finite x; y \<lhd> x\<rbrakk> \<Longrightarrow> card x = Suc (card y)
[PROOF STEP]
by auto


[STATEMENT]
lemma facetrelI_cardSuc: "z\<subseteq>x \<Longrightarrow> card x = Suc (card z) \<Longrightarrow> z\<lhd>x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<subseteq> x; card x = Suc (card z)\<rbrakk> \<Longrightarrow> z \<lhd> x
[PROOF STEP]
using card_ge_0_finite finite_subset[of z] card_Diff_subset[of z x]
[PROOF STATE]
proof (prove)
using this:
0 < card ?A \<Longrightarrow> finite ?A
\<lbrakk>z \<subseteq> ?B; finite ?B\<rbrakk> \<Longrightarrow> finite z
\<lbrakk>finite z; z \<subseteq> x\<rbrakk> \<Longrightarrow> card (x - z) = card x - card z

goal (1 subgoal):
 1. \<lbrakk>z \<subseteq> x; card x = Suc (card z)\<rbrakk> \<Longrightarrow> z \<lhd> x
[PROOF STEP]
by    (force intro: facetrelI_card)


[STATEMENT]
lemma facet2_subset: "\<lbrakk> z\<lhd>x; z\<lhd>y; x\<inter>y - z \<noteq> {} \<rbrakk> \<Longrightarrow> x \<subseteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<lhd> x; z \<lhd> y; x \<inter> y - z \<noteq> {}\<rbrakk> \<Longrightarrow> x \<subseteq> y
[PROOF STEP]
unfolding facetrel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>v. v \<notin> z \<and> x = insert v z; \<exists>v. v \<notin> z \<and> y = insert v z; x \<inter> y - z \<noteq> {}\<rbrakk> \<Longrightarrow> x \<subseteq> y
[PROOF STEP]
by force


[STATEMENT]
lemma inj_on_pullback_facet:
  assumes "inj_on f x" "z \<lhd> f`x"
  obtains y where "y \<lhd> x" "f`y = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?y2 \<lhd> x
 2. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> f ` ?y2 = z
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
z \<lhd> f ` x
[PROOF STEP]
obtain v where v: "v\<notin>z" "f`x = insert v z"
[PROOF STATE]
proof (prove)
using this:
z \<lhd> f ` x

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<notin> z; f ` x = insert v z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using facetrel_def[of z]
[PROOF STATE]
proof (prove)
using this:
z \<lhd> f ` x
z \<lhd> ?x \<equiv> \<exists>v. v \<notin> z \<and> ?x = insert v z

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<notin> z; f ` x = insert v z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
v \<notin> z
f ` x = insert v z

goal (2 subgoals):
 1. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?y2 \<lhd> x
 2. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> f ` ?y2 = z
[PROOF STEP]
define u and y where "u \<equiv> the_inv_into x f v" and y: "y \<equiv> {v\<in>x. f v \<in> z}"
[PROOF STATE]
proof (state)
this:
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}

goal (2 subgoals):
 1. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?y2 \<lhd> x
 2. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> f ` ?y2 = z
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}

goal (2 subgoals):
 1. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?y2 \<lhd> x
 2. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> f ` ?y2 = z
[PROOF STEP]
with assms(2) v
[PROOF STATE]
proof (chain)
picking this:
z \<lhd> f ` x
v \<notin> z
f ` x = insert v z
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}
[PROOF STEP]
have "x = insert u y"
[PROOF STATE]
proof (prove)
using this:
z \<lhd> f ` x
v \<notin> z
f ` x = insert v z
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}

goal (1 subgoal):
 1. x = insert u y
[PROOF STEP]
using the_inv_into_f_eq[OF assms(1)] the_inv_into_into[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
z \<lhd> f ` x
v \<notin> z
f ` x = insert v z
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}
\<lbrakk>f ?x = ?y; ?x \<in> x\<rbrakk> \<Longrightarrow> the_inv_into x f ?y = ?x
\<lbrakk>?x \<in> f ` x; x \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into x f ?x \<in> ?B

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

goal (2 subgoals):
 1. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> ?y2 \<lhd> x
 2. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> f ` ?y2 = z
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}
x = insert u y
[PROOF STEP]
show "y \<lhd> x"
[PROOF STATE]
proof (prove)
using this:
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}
x = insert u y

goal (1 subgoal):
 1. y \<lhd> x
[PROOF STEP]
using v f_the_inv_into_f[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
u \<equiv> the_inv_into x f v
y \<equiv> {v \<in> x. f v \<in> z}
x = insert u y
v \<notin> z
f ` x = insert v z
?y \<in> f ` x \<Longrightarrow> f (the_inv_into x f ?y) = ?y

goal (1 subgoal):
 1. y \<lhd> x
[PROOF STEP]
by (force intro: facetrelI)
[PROOF STATE]
proof (state)
this:
y \<lhd> x

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<lhd> x; f ` y = z\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> f ` {v \<in> x. f v \<in> z} = z
[PROOF STEP]
from y assms(2)
[PROOF STATE]
proof (chain)
picking this:
y \<equiv> {v \<in> x. f v \<in> z}
z \<lhd> f ` x
[PROOF STEP]
show "f`y = z"
[PROOF STATE]
proof (prove)
using this:
y \<equiv> {v \<in> x. f v \<in> z}
z \<lhd> f ` x

goal (1 subgoal):
 1. f ` y = z
[PROOF STEP]
using facetrel_subset
[PROOF STATE]
proof (prove)
using this:
y \<equiv> {v \<in> x. f v \<in> z}
z \<lhd> f ` x
?y \<lhd> ?x \<Longrightarrow> ?y \<subseteq> ?x

goal (1 subgoal):
 1. f ` y = z
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
f ` y = z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjacentI: "z\<lhd>x \<Longrightarrow> z\<lhd>y \<Longrightarrow> x \<sim> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<lhd> x; z \<lhd> y\<rbrakk> \<Longrightarrow> x \<sim> y
[PROOF STEP]
using adjacent_def
[PROOF STATE]
proof (prove)
using this:
?x \<sim> ?y \<equiv> \<exists>z. z \<lhd> ?x \<and> z \<lhd> ?y

goal (1 subgoal):
 1. \<lbrakk>z \<lhd> x; z \<lhd> y\<rbrakk> \<Longrightarrow> x \<sim> y
[PROOF STEP]
by fast


[STATEMENT]
lemma empty_not_adjacent: "\<not> {} \<sim> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> {} \<sim> x
[PROOF STEP]
unfolding facetrel_def adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>z. (\<exists>v. v \<notin> z \<and> {} = insert v z) \<and> (\<exists>v. v \<notin> z \<and> x = insert v z)
[PROOF STEP]
by fast


[STATEMENT]
lemma adjacent_sym: "x \<sim> y \<Longrightarrow> y \<sim> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sim> y \<Longrightarrow> y \<sim> x
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. z \<lhd> x \<and> z \<lhd> y \<Longrightarrow> \<exists>z. z \<lhd> y \<and> z \<lhd> x
[PROOF STEP]
by fast


[STATEMENT]
lemma adjacent_refl:
  assumes "x \<noteq> {}"
  shows   "x \<sim> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sim> x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<sim> x
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> {}
[PROOF STEP]
obtain v where v: "v\<in>x"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> {}

goal (1 subgoal):
 1. (\<And>v. v \<in> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
v \<in> x

goal (1 subgoal):
 1. x \<sim> x
[PROOF STEP]
thus "x \<sim> x"
[PROOF STATE]
proof (prove)
using this:
v \<in> x

goal (1 subgoal):
 1. x \<sim> x
[PROOF STEP]
using facetrelI[of v "x-{v}"]
[PROOF STATE]
proof (prove)
using this:
v \<in> x
\<lbrakk>v \<notin> x - {v}; ?x = insert v (x - {v})\<rbrakk> \<Longrightarrow> x - {v} \<lhd> ?x

goal (1 subgoal):
 1. x \<sim> x
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
using this:
v \<in> x
\<lbrakk>v \<notin> x - {v}; ?x = insert v (x - {v})\<rbrakk> \<Longrightarrow> x - {v} \<lhd> ?x

goal (1 subgoal):
 1. \<exists>z. z \<lhd> x \<and> z \<lhd> x
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<sim> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma common_facet: "\<lbrakk> z\<lhd>x; z\<lhd>y; x \<noteq> y \<rbrakk> \<Longrightarrow> z = x \<inter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>z \<lhd> x; z \<lhd> y; x \<noteq> y\<rbrakk> \<Longrightarrow> z = x \<inter> y
[PROOF STEP]
using facetrel_subset facet2_subset
[PROOF STATE]
proof (prove)
using this:
?y \<lhd> ?x \<Longrightarrow> ?y \<subseteq> ?x
\<lbrakk>?z \<lhd> ?x; ?z \<lhd> ?y; ?x \<inter> ?y - ?z \<noteq> {}\<rbrakk> \<Longrightarrow> ?x \<subseteq> ?y

goal (1 subgoal):
 1. \<lbrakk>z \<lhd> x; z \<lhd> y; x \<noteq> y\<rbrakk> \<Longrightarrow> z = x \<inter> y
[PROOF STEP]
by fast


[STATEMENT]
lemma adjacent_int_facet1: "x \<sim> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> (x \<inter> y) \<lhd> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<inter> y \<lhd> x
[PROOF STEP]
using common_facet
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?z \<lhd> ?x; ?z \<lhd> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> ?z = ?x \<inter> ?y

goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<inter> y \<lhd> x
[PROOF STEP]
unfolding adjacent_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?z \<lhd> ?x; ?z \<lhd> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> ?z = ?x \<inter> ?y

goal (1 subgoal):
 1. \<lbrakk>\<exists>z. z \<lhd> x \<and> z \<lhd> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<inter> y \<lhd> x
[PROOF STEP]
by fast


[STATEMENT]
lemma adjacent_int_facet2: "x \<sim> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> (x \<inter> y) \<lhd> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<inter> y \<lhd> y
[PROOF STEP]
using adjacent_sym adjacent_int_facet1
[PROOF STATE]
proof (prove)
using this:
?x \<sim> ?y \<Longrightarrow> ?y \<sim> ?x
\<lbrakk>?x \<sim> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> ?x \<inter> ?y \<lhd> ?x

goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<inter> y \<lhd> y
[PROOF STEP]
by (fastforce simp add: Int_commute)


[STATEMENT]
lemma adjacent_conv_insert: "x \<sim> y \<Longrightarrow> v \<in> x - y \<Longrightarrow> x = insert v (x\<inter>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; v \<in> x - y\<rbrakk> \<Longrightarrow> x = insert v (x \<inter> y)
[PROOF STEP]
using adjacent_int_facet1 facetrel_conv_insert
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<sim> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> ?x \<inter> ?y \<lhd> ?x
\<lbrakk>?y \<lhd> ?x; ?v \<in> ?x - ?y\<rbrakk> \<Longrightarrow> ?x = insert ?v ?y

goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; v \<in> x - y\<rbrakk> \<Longrightarrow> x = insert v (x \<inter> y)
[PROOF STEP]
by fast


[STATEMENT]
lemma adjacent_int_decomp:
  "x \<sim> y \<Longrightarrow> x \<noteq> y \<Longrightarrow> \<exists>v. v \<notin> y \<and> x = insert v (x\<inter>y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>v. v \<notin> y \<and> x = insert v (x \<inter> y)
[PROOF STEP]
using adjacent_int_facet1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<sim> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> ?x \<inter> ?y \<lhd> ?x

goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>v. v \<notin> y \<and> x = insert v (x \<inter> y)
[PROOF STEP]
unfolding facetrel_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<sim> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> \<exists>v. v \<notin> ?x \<inter> ?y \<and> ?x = insert v (?x \<inter> ?y)

goal (1 subgoal):
 1. \<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>v. v \<notin> y \<and> x = insert v (x \<inter> y)
[PROOF STEP]
by fast


[STATEMENT]
lemma adj_antivertex:
  assumes "x\<sim>y" "x\<noteq>y"
  shows   "\<exists>!v. v\<in>x-y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!v. v \<in> x - y
[PROOF STEP]
proof (rule ex_ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>v. v \<in> x - y
 2. \<And>v ya. \<lbrakk>v \<in> x - y; ya \<in> x - y\<rbrakk> \<Longrightarrow> v = ya
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<sim> y
x \<noteq> y
[PROOF STEP]
obtain w where w: "w\<notin>y" "x = insert w (x\<inter>y)"
[PROOF STATE]
proof (prove)
using this:
x \<sim> y
x \<noteq> y

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w \<notin> y; x = insert w (x \<inter> y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using adjacent_int_decomp
[PROOF STATE]
proof (prove)
using this:
x \<sim> y
x \<noteq> y
\<lbrakk>?x \<sim> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> \<exists>v. v \<notin> ?y \<and> ?x = insert v (?x \<inter> ?y)

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w \<notin> y; x = insert w (x \<inter> y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
w \<notin> y
x = insert w (x \<inter> y)

goal (2 subgoals):
 1. \<exists>v. v \<in> x - y
 2. \<And>v ya. \<lbrakk>v \<in> x - y; ya \<in> x - y\<rbrakk> \<Longrightarrow> v = ya
[PROOF STEP]
thus "\<exists>v. v\<in>x-y"
[PROOF STATE]
proof (prove)
using this:
w \<notin> y
x = insert w (x \<inter> y)

goal (1 subgoal):
 1. \<exists>v. v \<in> x - y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v. v \<in> x - y

goal (1 subgoal):
 1. \<And>v ya. \<lbrakk>v \<in> x - y; ya \<in> x - y\<rbrakk> \<Longrightarrow> v = ya
[PROOF STEP]
from w
[PROOF STATE]
proof (chain)
picking this:
w \<notin> y
x = insert w (x \<inter> y)
[PROOF STEP]
have "\<And>v. v\<in>x-y \<Longrightarrow> v=w"
[PROOF STATE]
proof (prove)
using this:
w \<notin> y
x = insert w (x \<inter> y)

goal (1 subgoal):
 1. \<And>v. v \<in> x - y \<Longrightarrow> v = w
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
?v \<in> x - y \<Longrightarrow> ?v = w

goal (1 subgoal):
 1. \<And>v ya. \<lbrakk>v \<in> x - y; ya \<in> x - y\<rbrakk> \<Longrightarrow> v = ya
[PROOF STEP]
thus "\<And>v v'. v\<in>x-y \<Longrightarrow> v'\<in>x-y \<Longrightarrow> v=v'"
[PROOF STATE]
proof (prove)
using this:
?v \<in> x - y \<Longrightarrow> ?v = w

goal (1 subgoal):
 1. \<And>v v'. \<lbrakk>v \<in> x - y; v' \<in> x - y\<rbrakk> \<Longrightarrow> v = v'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?v \<in> x - y; ?v' \<in> x - y\<rbrakk> \<Longrightarrow> ?v = ?v'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjacent_card: "x \<sim> y \<Longrightarrow> card x = card y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sim> y \<Longrightarrow> card x = card y
[PROOF STEP]
unfolding adjacent_def facetrel_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>z. (\<exists>v. v \<notin> z \<and> x = insert v z) \<and> (\<exists>v. v \<notin> z \<and> y = insert v z) \<Longrightarrow> card x = card y
[PROOF STEP]
by (cases "finite x" "x=y" rule: two_cases) auto


[STATEMENT]
lemma adjacent_to_adjacent_int_subset:
  assumes "C \<sim> D" "f`C \<sim> f`D" "f`C \<noteq> f`D"
  shows   "f`C \<inter> f`D \<subseteq> f`(C\<inter>D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` C \<inter> f ` D \<subseteq> f ` (C \<inter> D)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
from assms(1,3)
[PROOF STATE]
proof (chain)
picking this:
C \<sim> D
f ` C \<noteq> f ` D
[PROOF STEP]
obtain v where v: "v \<notin> D" "C = insert v (C\<inter>D)"
[PROOF STATE]
proof (prove)
using this:
C \<sim> D
f ` C \<noteq> f ` D

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<notin> D; C = insert v (C \<inter> D)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using adjacent_int_decomp
[PROOF STATE]
proof (prove)
using this:
C \<sim> D
f ` C \<noteq> f ` D
\<lbrakk>?x \<sim> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> \<exists>v. v \<notin> ?y \<and> ?x = insert v (?x \<inter> ?y)

goal (1 subgoal):
 1. (\<And>v. \<lbrakk>v \<notin> D; C = insert v (C \<inter> D)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
v \<notin> D
C = insert v (C \<inter> D)

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
from assms(2,3)
[PROOF STATE]
proof (chain)
picking this:
f ` C \<sim> f ` D
f ` C \<noteq> f ` D
[PROOF STEP]
obtain w where w: "w \<notin> f`D" "f`C = insert w (f`C\<inter>f`D)"
[PROOF STATE]
proof (prove)
using this:
f ` C \<sim> f ` D
f ` C \<noteq> f ` D

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w \<notin> f ` D; f ` C = insert w (f ` C \<inter> f ` D)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using adjacent_int_decomp[of "f`C" "f`D"]
[PROOF STATE]
proof (prove)
using this:
f ` C \<sim> f ` D
f ` C \<noteq> f ` D
\<lbrakk>f ` C \<sim> f ` D; f ` C \<noteq> f ` D\<rbrakk> \<Longrightarrow> \<exists>v. v \<notin> f ` D \<and> f ` C = insert v (f ` C \<inter> f ` D)

goal (1 subgoal):
 1. (\<And>w. \<lbrakk>w \<notin> f ` D; f ` C = insert w (f ` C \<inter> f ` D)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
w \<notin> f ` D
f ` C = insert w (f ` C \<inter> f ` D)

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
from w
[PROOF STATE]
proof (chain)
picking this:
w \<notin> f ` D
f ` C = insert w (f ` C \<inter> f ` D)
[PROOF STEP]
have w': "w \<in> f`C - f`D"
[PROOF STATE]
proof (prove)
using this:
w \<notin> f ` D
f ` C = insert w (f ` C \<inter> f ` D)

goal (1 subgoal):
 1. w \<in> f ` C - f ` D
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
w \<in> f ` C - f ` D

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
with v assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
v \<notin> D
C = insert v (C \<inter> D)
C \<sim> D
f ` C \<sim> f ` D
w \<in> f ` C - f ` D
[PROOF STEP]
have fv_w: "f v = w"
[PROOF STATE]
proof (prove)
using this:
v \<notin> D
C = insert v (C \<inter> D)
C \<sim> D
f ` C \<sim> f ` D
w \<in> f ` C - f ` D

goal (1 subgoal):
 1. f v = w
[PROOF STEP]
using adjacent_conv_insert
[PROOF STATE]
proof (prove)
using this:
v \<notin> D
C = insert v (C \<inter> D)
C \<sim> D
f ` C \<sim> f ` D
w \<in> f ` C - f ` D
\<lbrakk>?x \<sim> ?y; ?v \<in> ?x - ?y\<rbrakk> \<Longrightarrow> ?x = insert ?v (?x \<inter> ?y)

goal (1 subgoal):
 1. f v = w
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
f v = w

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
assume "b \<in> f`C \<inter> f`D"
[PROOF STATE]
proof (state)
this:
b \<in> f ` C \<inter> f ` D

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
b \<in> f ` C \<inter> f ` D
[PROOF STEP]
obtain a1 a2
    where a1: "a1 \<in> C" "b = f a1"
    and   a2: "a2 \<in> D" "b = f a2"
[PROOF STATE]
proof (prove)
using this:
b \<in> f ` C \<inter> f ` D

goal (1 subgoal):
 1. (\<And>a1 a2. \<lbrakk>a1 \<in> C; b = f a1; a2 \<in> D; b = f a2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by    fast
[PROOF STATE]
proof (state)
this:
a1 \<in> C
b = f a1
a2 \<in> D
b = f a2

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
from v a1 a2(2)
[PROOF STATE]
proof (chain)
picking this:
v \<notin> D
C = insert v (C \<inter> D)
a1 \<in> C
b = f a1
b = f a2
[PROOF STEP]
have "a1 \<notin> D \<Longrightarrow> f a2 = w"
[PROOF STATE]
proof (prove)
using this:
v \<notin> D
C = insert v (C \<inter> D)
a1 \<in> C
b = f a1
b = f a2

goal (1 subgoal):
 1. a1 \<notin> D \<Longrightarrow> f a2 = w
[PROOF STEP]
using fv_w
[PROOF STATE]
proof (prove)
using this:
v \<notin> D
C = insert v (C \<inter> D)
a1 \<in> C
b = f a1
b = f a2
f v = w

goal (1 subgoal):
 1. a1 \<notin> D \<Longrightarrow> f a2 = w
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a1 \<notin> D \<Longrightarrow> f a2 = w

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
with a2(1) w'
[PROOF STATE]
proof (chain)
picking this:
a2 \<in> D
w \<in> f ` C - f ` D
a1 \<notin> D \<Longrightarrow> f a2 = w
[PROOF STEP]
have "a1 \<in> D"
[PROOF STATE]
proof (prove)
using this:
a2 \<in> D
w \<in> f ` C - f ` D
a1 \<notin> D \<Longrightarrow> f a2 = w

goal (1 subgoal):
 1. a1 \<in> D
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
a1 \<in> D

goal (1 subgoal):
 1. \<And>x. x \<in> f ` C \<inter> f ` D \<Longrightarrow> x \<in> f ` (C \<inter> D)
[PROOF STEP]
with a1
[PROOF STATE]
proof (chain)
picking this:
a1 \<in> C
b = f a1
a1 \<in> D
[PROOF STEP]
show "b \<in> f`(C\<inter>D)"
[PROOF STATE]
proof (prove)
using this:
a1 \<in> C
b = f a1
a1 \<in> D

goal (1 subgoal):
 1. b \<in> f ` (C \<inter> D)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
b \<in> f ` (C \<inter> D)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma adjacent_to_adjacent_int:
  "\<lbrakk> C \<sim> D; f`C \<sim> f`D; f`C \<noteq> f`D \<rbrakk> \<Longrightarrow> f`(C\<inter>D) = f`C \<inter> f`D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<sim> D; f ` C \<sim> f ` D; f ` C \<noteq> f ` D\<rbrakk> \<Longrightarrow> f ` (C \<inter> D) = f ` C \<inter> f ` D
[PROOF STEP]
using adjacent_to_adjacent_int_subset
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?C \<sim> ?D; ?f ` ?C \<sim> ?f ` ?D; ?f ` ?C \<noteq> ?f ` ?D\<rbrakk> \<Longrightarrow> ?f ` ?C \<inter> ?f ` ?D \<subseteq> ?f ` (?C \<inter> ?D)

goal (1 subgoal):
 1. \<lbrakk>C \<sim> D; f ` C \<sim> f ` D; f ` C \<noteq> f ` D\<rbrakk> \<Longrightarrow> f ` (C \<inter> D) = f ` C \<inter> f ` D
[PROOF STEP]
by fast


[STATEMENT]
lemma adjacentchain_card: "adjacentchain (x#xs@[y]) \<Longrightarrow> card x = card y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. adjacentchain (x # xs @ [y]) \<Longrightarrow> card x = card y
[PROOF STEP]
using adjacent_card
[PROOF STATE]
proof (prove)
using this:
?x \<sim> ?y \<Longrightarrow> card ?x = card ?y

goal (1 subgoal):
 1. adjacentchain (x # xs @ [y]) \<Longrightarrow> card x = card y
[PROOF STEP]
by (induct xs arbitrary: x) auto


[STATEMENT]
lemma singleton_simplex: "v\<in>\<Union>X \<Longrightarrow> {v} \<in> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> \<Union> X \<Longrightarrow> {v} \<in> X
[PROOF STEP]
using faces
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<subseteq> ?x\<rbrakk> \<Longrightarrow> ?y \<in> X

goal (1 subgoal):
 1. v \<in> \<Union> X \<Longrightarrow> {v} \<in> X
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimpI: "x \<in> X \<Longrightarrow> (\<And>z. z\<in>X \<Longrightarrow> x\<subseteq>z \<Longrightarrow> z=x) \<Longrightarrow> maxsimp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> X; \<And>z. \<lbrakk>z \<in> X; x \<subseteq> z\<rbrakk> \<Longrightarrow> z = x\<rbrakk> \<Longrightarrow> maxsimp x
[PROOF STEP]
using maxsimp_def
[PROOF STATE]
proof (prove)
using this:
maxsimp ?x \<equiv> ?x \<in> X \<and> (\<forall>z\<in>X. ?x \<subseteq> z \<longrightarrow> z = ?x)

goal (1 subgoal):
 1. \<lbrakk>x \<in> X; \<And>z. \<lbrakk>z \<in> X; x \<subseteq> z\<rbrakk> \<Longrightarrow> z = x\<rbrakk> \<Longrightarrow> maxsimp x
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimpD_simplex: "maxsimp x \<Longrightarrow> x\<in>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimp x \<Longrightarrow> x \<in> X
[PROOF STEP]
using maxsimp_def
[PROOF STATE]
proof (prove)
using this:
maxsimp ?x \<equiv> ?x \<in> X \<and> (\<forall>z\<in>X. ?x \<subseteq> z \<longrightarrow> z = ?x)

goal (1 subgoal):
 1. maxsimp x \<Longrightarrow> x \<in> X
[PROOF STEP]
by fast


[STATEMENT]
lemma maxsimpD_maximal: "maxsimp x \<Longrightarrow> z\<in>X \<Longrightarrow> x\<subseteq>z \<Longrightarrow> z=x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimp x; z \<in> X; x \<subseteq> z\<rbrakk> \<Longrightarrow> z = x
[PROOF STEP]
using maxsimp_def
[PROOF STATE]
proof (prove)
using this:
maxsimp ?x \<equiv> ?x \<in> X \<and> (\<forall>z\<in>X. ?x \<subseteq> z \<longrightarrow> z = ?x)

goal (1 subgoal):
 1. \<lbrakk>maxsimp x; z \<in> X; x \<subseteq> z\<rbrakk> \<Longrightarrow> z = x
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimp_nempty: "X \<noteq> {{}} \<Longrightarrow> maxsimp x \<Longrightarrow> x \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<noteq> {{}}; maxsimp x\<rbrakk> \<Longrightarrow> x \<noteq> {}
[PROOF STEP]
unfolding maxsimp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>X \<noteq> {{}}; x \<in> X \<and> (\<forall>z\<in>X. x \<subseteq> z \<longrightarrow> z = x)\<rbrakk> \<Longrightarrow> x \<noteq> {}
[PROOF STEP]
by fast


[STATEMENT]
lemma maxsimp_vertices: "maxsimp x \<Longrightarrow> x\<subseteq>\<Union>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimp x \<Longrightarrow> x \<subseteq> \<Union> X
[PROOF STEP]
using maxsimpD_simplex
[PROOF STATE]
proof (prove)
using this:
maxsimp ?x \<Longrightarrow> ?x \<in> X

goal (1 subgoal):
 1. maxsimp x \<Longrightarrow> x \<subseteq> \<Union> X
[PROOF STEP]
by fast


[STATEMENT]
lemma adjacentsetD_adj: "y \<in> adjacentset x \<Longrightarrow> x\<sim>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> adjacentset x \<Longrightarrow> x \<sim> y
[PROOF STEP]
using adjacentset_def
[PROOF STATE]
proof (prove)
using this:
adjacentset ?x = {y \<in> X. ?x \<sim> y}

goal (1 subgoal):
 1. y \<in> adjacentset x \<Longrightarrow> x \<sim> y
[PROOF STEP]
by fast


[STATEMENT]
lemma max_in_subcomplex:
  "\<lbrakk> Subcomplex Y; y \<in> Y; maxsimp y \<rbrakk> \<Longrightarrow> SimplicialComplex.maxsimp Y y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subcomplex Y; y \<in> Y; maxsimp y\<rbrakk> \<Longrightarrow> SimplicialComplex.maxsimp Y y
[PROOF STEP]
using maxsimpD_maximal
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>maxsimp ?x; ?z \<in> X; ?x \<subseteq> ?z\<rbrakk> \<Longrightarrow> ?z = ?x

goal (1 subgoal):
 1. \<lbrakk>Subcomplex Y; y \<in> Y; maxsimp y\<rbrakk> \<Longrightarrow> SimplicialComplex.maxsimp Y y
[PROOF STEP]
by (fast intro: SimplicialComplex.maxsimpI)


[STATEMENT]
lemma face_im:
  assumes "w \<in> X" "y \<subseteq> f`w"
  defines "u \<equiv> {a\<in>w. f a \<in> y}"
  shows "y \<in> f\<turnstile>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> f \<turnstile> X
[PROOF STEP]
using assms faces[of w u] image_eqI[of y "(`) f" u X]
[PROOF STATE]
proof (prove)
using this:
w \<in> X
y \<subseteq> f ` w
u \<equiv> {a \<in> w. f a \<in> y}
\<lbrakk>w \<in> X; u \<subseteq> w\<rbrakk> \<Longrightarrow> u \<in> X
\<lbrakk>y = f ` u; u \<in> X\<rbrakk> \<Longrightarrow> y \<in> f \<turnstile> X

goal (1 subgoal):
 1. y \<in> f \<turnstile> X
[PROOF STEP]
by    fast


[STATEMENT]
lemma im_faces: "x \<in> f \<turnstile> X \<Longrightarrow> y \<subseteq> x \<Longrightarrow> y \<in> f \<turnstile> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> f \<turnstile> X; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> f \<turnstile> X
[PROOF STEP]
using faces face_im[of _ y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<subseteq> ?x\<rbrakk> \<Longrightarrow> ?y \<in> X
\<lbrakk>?w \<in> X; y \<subseteq> ?f ` ?w\<rbrakk> \<Longrightarrow> y \<in> ?f \<turnstile> X

goal (1 subgoal):
 1. \<lbrakk>x \<in> f \<turnstile> X; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> f \<turnstile> X
[PROOF STEP]
by (cases "y={}") auto


[STATEMENT]
lemma map_is_simplicial_morph: "SimplicialComplex (f\<turnstile>X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SimplicialComplex (f \<turnstile> X)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<forall>x\<in>f \<turnstile> X. finite x
 2. \<And>x y. \<lbrakk>x \<in> f \<turnstile> X; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> f \<turnstile> X
[PROOF STEP]
show "\<forall>x\<in>f\<turnstile>X. finite x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>f \<turnstile> X. finite x
[PROOF STEP]
using finite_simplices
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>X. finite x

goal (1 subgoal):
 1. \<forall>x\<in>f \<turnstile> X. finite x
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>f \<turnstile> X. finite x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> f \<turnstile> X; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> f \<turnstile> X
[PROOF STEP]
show "\<And>x y. x \<in>f\<turnstile>X \<Longrightarrow> y\<subseteq>x \<Longrightarrow> y\<in>f\<turnstile>X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> f \<turnstile> X; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> f \<turnstile> X
[PROOF STEP]
using im_faces
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> ?f \<turnstile> X; ?y \<subseteq> ?x\<rbrakk> \<Longrightarrow> ?y \<in> ?f \<turnstile> X

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> f \<turnstile> X; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> f \<turnstile> X
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> f \<turnstile> X; ?y \<subseteq> ?x\<rbrakk> \<Longrightarrow> ?y \<in> f \<turnstile> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vertex_set_int:
  assumes "SimplicialComplex Y"
  shows   "\<Union>(X\<inter>Y) = \<Union>X \<inter> \<Union>Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (X \<inter> Y) = \<Union> X \<inter> \<Union> Y
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Union> (X \<inter> Y) \<subseteq> \<Union> X \<inter> \<Union> Y
 2. \<Union> X \<inter> \<Union> Y \<subseteq> \<Union> (X \<inter> Y)
[PROOF STEP]
have "\<And>v. v \<in> \<Union>X \<inter> \<Union>Y \<Longrightarrow> v\<in> \<Union>(X\<inter>Y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. v \<in> \<Union> X \<inter> \<Union> Y \<Longrightarrow> v \<in> \<Union> (X \<inter> Y)
[PROOF STEP]
using faces SimplicialComplex.faces[OF assms]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> X; ?y \<subseteq> ?x\<rbrakk> \<Longrightarrow> ?y \<in> X
\<lbrakk>?x \<in> Y; ?y \<subseteq> ?x\<rbrakk> \<Longrightarrow> ?y \<in> Y

goal (1 subgoal):
 1. \<And>v. v \<in> \<Union> X \<inter> \<Union> Y \<Longrightarrow> v \<in> \<Union> (X \<inter> Y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?v \<in> \<Union> X \<inter> \<Union> Y \<Longrightarrow> ?v \<in> \<Union> (X \<inter> Y)

goal (2 subgoals):
 1. \<Union> (X \<inter> Y) \<subseteq> \<Union> X \<inter> \<Union> Y
 2. \<Union> X \<inter> \<Union> Y \<subseteq> \<Union> (X \<inter> Y)
[PROOF STEP]
thus "\<Union>(X\<inter>Y) \<supseteq> \<Union>X \<inter> \<Union>Y"
[PROOF STATE]
proof (prove)
using this:
?v \<in> \<Union> X \<inter> \<Union> Y \<Longrightarrow> ?v \<in> \<Union> (X \<inter> Y)

goal (1 subgoal):
 1. \<Union> X \<inter> \<Union> Y \<subseteq> \<Union> (X \<inter> Y)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<Union> X \<inter> \<Union> Y \<subseteq> \<Union> (X \<inter> Y)

goal (1 subgoal):
 1. \<Union> (X \<inter> Y) \<subseteq> \<Union> X \<inter> \<Union> Y
[PROOF STEP]
qed auto


[STATEMENT]
lemma maxsimpchain_snocI:
  "\<lbrakk> maxsimpchain (xs@[x]); maxsimp y; x\<sim>y \<rbrakk> \<Longrightarrow> maxsimpchain (xs@[x,y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimpchain (xs @ [x]); maxsimp y; x \<sim> y\<rbrakk> \<Longrightarrow> maxsimpchain (xs @ [x, y])
[PROOF STEP]
using maxsimpchain_def binrelchain_snoc maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs
\<lbrakk>binrelchain ?P (?xs @ [?x]); ?P ?x ?y\<rbrakk> \<Longrightarrow> binrelchain ?P (?xs @ [?x, ?y])
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. \<lbrakk>maxsimpchain (xs @ [x]); maxsimp y; x \<sim> y\<rbrakk> \<Longrightarrow> maxsimpchain (xs @ [x, y])
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimpchainD_maxsimp:
  "maxsimpchain xs \<Longrightarrow> x \<in> set xs \<Longrightarrow> maxsimp x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimpchain xs; x \<in> set xs\<rbrakk> \<Longrightarrow> maxsimp x
[PROOF STEP]
using maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. \<lbrakk>maxsimpchain xs; x \<in> set xs\<rbrakk> \<Longrightarrow> maxsimp x
[PROOF STEP]
by fast


[STATEMENT]
lemma maxsimpchainD_adj: "maxsimpchain xs \<Longrightarrow> adjacentchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain xs \<Longrightarrow> adjacentchain xs
[PROOF STEP]
using maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. maxsimpchain xs \<Longrightarrow> adjacentchain xs
[PROOF STEP]
by fast


[STATEMENT]
lemma maxsimpchain_CConsI:
  "\<lbrakk> maxsimp w; maxsimpchain (x#xs); w\<sim>x \<rbrakk> \<Longrightarrow> maxsimpchain (w#x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimp w; maxsimpchain (x # xs); w \<sim> x\<rbrakk> \<Longrightarrow> maxsimpchain (w # x # xs)
[PROOF STEP]
using maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. \<lbrakk>maxsimp w; maxsimpchain (x # xs); w \<sim> x\<rbrakk> \<Longrightarrow> maxsimpchain (w # x # xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimpchain_Cons_reduce:
  "maxsimpchain (x#xs) \<Longrightarrow> maxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain (x # xs) \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
using     adjacentchain_Cons_reduce maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
adjacentchain (?x # ?xs) \<Longrightarrow> adjacentchain ?xs
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. maxsimpchain (x # xs) \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
by fastforce


[STATEMENT]
lemma maxsimpchain_append_reduce1:
  "maxsimpchain (xs@ys) \<Longrightarrow> maxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain (xs @ ys) \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
using binrelchain_append_reduce1 maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
binrelchain ?P (?xs @ ?ys) \<Longrightarrow> binrelchain ?P ?xs
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. maxsimpchain (xs @ ys) \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimpchain_append_reduce2:
  "maxsimpchain (xs@ys) \<Longrightarrow> maxsimpchain ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain (xs @ ys) \<Longrightarrow> maxsimpchain ys
[PROOF STEP]
using binrelchain_append_reduce2 maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
binrelchain ?P (?xs @ ?ys) \<Longrightarrow> binrelchain ?P ?ys
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. maxsimpchain (xs @ ys) \<Longrightarrow> maxsimpchain ys
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimpchain_remdup_adj:
  "maxsimpchain (xs@[x,x]@ys) \<Longrightarrow> maxsimpchain (xs@[x]@ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain (xs @ [x, x] @ ys) \<Longrightarrow> maxsimpchain (xs @ [x] @ ys)
[PROOF STEP]
using maxsimpchain_def binrelchain_remdup_adj
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs
binrelchain ?P (?xs @ [?x, ?x] @ ?ys) \<Longrightarrow> binrelchain ?P (?xs @ ?x # ?ys)

goal (1 subgoal):
 1. maxsimpchain (xs @ [x, x] @ ys) \<Longrightarrow> maxsimpchain (xs @ [x] @ ys)
[PROOF STEP]
by auto


[STATEMENT]
lemma maxsimpchain_rev: "maxsimpchain xs \<Longrightarrow> maxsimpchain (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain xs \<Longrightarrow> maxsimpchain (rev xs)
[PROOF STEP]
using     maxsimpchainD_maxsimp adjacent_sym
            binrelchain_sym_rev[of adjacent]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>maxsimpchain ?xs; ?x \<in> set ?xs\<rbrakk> \<Longrightarrow> maxsimp ?x
?x \<sim> ?y \<Longrightarrow> ?y \<sim> ?x
\<lbrakk>\<And>x y. x \<sim> y \<Longrightarrow> y \<sim> x; adjacentchain ?xs\<rbrakk> \<Longrightarrow> adjacentchain (rev ?xs)

goal (1 subgoal):
 1. maxsimpchain xs \<Longrightarrow> maxsimpchain (rev xs)
[PROOF STEP]
unfolding maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>Ball (set ?xs) maxsimp \<and> adjacentchain ?xs; ?x \<in> set ?xs\<rbrakk> \<Longrightarrow> maxsimp ?x
?x \<sim> ?y \<Longrightarrow> ?y \<sim> ?x
\<lbrakk>\<And>x y. x \<sim> y \<Longrightarrow> y \<sim> x; adjacentchain ?xs\<rbrakk> \<Longrightarrow> adjacentchain (rev ?xs)

goal (1 subgoal):
 1. Ball (set xs) maxsimp \<and> adjacentchain xs \<Longrightarrow> Ball (set (rev xs)) maxsimp \<and> adjacentchain (rev xs)
[PROOF STEP]
by        fastforce


[STATEMENT]
lemma maxsimpchain_overlap_join:
  "maxsimpchain (xs@[w]) \<Longrightarrow> maxsimpchain (w#ys) \<Longrightarrow>
    maxsimpchain (xs@w#ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimpchain (xs @ [w]); maxsimpchain (w # ys)\<rbrakk> \<Longrightarrow> maxsimpchain (xs @ w # ys)
[PROOF STEP]
using binrelchain_overlap_join maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>binrelchain ?P (?xs @ [?x]); binrelchain ?P (?x # ?ys)\<rbrakk> \<Longrightarrow> binrelchain ?P (?xs @ ?x # ?ys)
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. \<lbrakk>maxsimpchain (xs @ [w]); maxsimpchain (w # ys)\<rbrakk> \<Longrightarrow> maxsimpchain (xs @ w # ys)
[PROOF STEP]
by auto


[STATEMENT]
lemma pmaxsimpchain: "pmaxsimpchain xs \<Longrightarrow> maxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmaxsimpchain xs \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
using maxsimpchain_def pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs
pmaxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> padjacentchain ?xs

goal (1 subgoal):
 1. pmaxsimpchain xs \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
by fast


[STATEMENT]
lemma pmaxsimpchainI_maxsimpchain:
  "maxsimpchain xs \<Longrightarrow> distinct xs \<Longrightarrow> pmaxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimpchain xs; distinct xs\<rbrakk> \<Longrightarrow> pmaxsimpchain xs
[PROOF STEP]
using maxsimpchain_def pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs
pmaxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> padjacentchain ?xs

goal (1 subgoal):
 1. \<lbrakk>maxsimpchain xs; distinct xs\<rbrakk> \<Longrightarrow> pmaxsimpchain xs
[PROOF STEP]
by fast


[STATEMENT]
lemma pmaxsimpchain_CConsI:
  "\<lbrakk> maxsimp w; pmaxsimpchain (x#xs); w\<sim>x; w \<notin> set (x#xs) \<rbrakk> \<Longrightarrow>
    pmaxsimpchain (w#x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimp w; pmaxsimpchain (x # xs); w \<sim> x; w \<notin> set (x # xs)\<rbrakk> \<Longrightarrow> pmaxsimpchain (w # x # xs)
[PROOF STEP]
using pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> padjacentchain ?xs

goal (1 subgoal):
 1. \<lbrakk>maxsimp w; pmaxsimpchain (x # xs); w \<sim> x; w \<notin> set (x # xs)\<rbrakk> \<Longrightarrow> pmaxsimpchain (w # x # xs)
[PROOF STEP]
by auto


[STATEMENT]
lemma pmaxsimpchainD_distinct: "pmaxsimpchain xs \<Longrightarrow> distinct xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmaxsimpchain xs \<Longrightarrow> distinct xs
[PROOF STEP]
using pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> padjacentchain ?xs

goal (1 subgoal):
 1. pmaxsimpchain xs \<Longrightarrow> distinct xs
[PROOF STEP]
by fast


[STATEMENT]
lemma pmaxsimpchain_Cons_reduce:
  "pmaxsimpchain (x#xs) \<Longrightarrow> pmaxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmaxsimpchain (x # xs) \<Longrightarrow> pmaxsimpchain xs
[PROOF STEP]
using maxsimpchain_Cons_reduce pmaxsimpchain pmaxsimpchainD_distinct
[PROOF STATE]
proof (prove)
using this:
maxsimpchain (?x # ?xs) \<Longrightarrow> maxsimpchain ?xs
pmaxsimpchain ?xs \<Longrightarrow> maxsimpchain ?xs
pmaxsimpchain ?xs \<Longrightarrow> distinct ?xs

goal (1 subgoal):
 1. pmaxsimpchain (x # xs) \<Longrightarrow> pmaxsimpchain xs
[PROOF STEP]
by    (fastforce intro: pmaxsimpchainI_maxsimpchain)


[STATEMENT]
lemma pmaxsimpchain_append_reduce1:
  "pmaxsimpchain (xs@ys) \<Longrightarrow> pmaxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmaxsimpchain (xs @ ys) \<Longrightarrow> pmaxsimpchain xs
[PROOF STEP]
using maxsimpchain_append_reduce1 pmaxsimpchain pmaxsimpchainD_distinct
[PROOF STATE]
proof (prove)
using this:
maxsimpchain (?xs @ ?ys) \<Longrightarrow> maxsimpchain ?xs
pmaxsimpchain ?xs \<Longrightarrow> maxsimpchain ?xs
pmaxsimpchain ?xs \<Longrightarrow> distinct ?xs

goal (1 subgoal):
 1. pmaxsimpchain (xs @ ys) \<Longrightarrow> pmaxsimpchain xs
[PROOF STEP]
by    (fastforce intro: pmaxsimpchainI_maxsimpchain)


[STATEMENT]
lemma maxsimpchain_obtain_pmaxsimpchain:
  assumes "x\<noteq>y" "maxsimpchain (x#xs@[y])"
  shows   "\<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and>
            pmaxsimpchain (x#ys@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and> pmaxsimpchain (x # ys @ [y])
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and> pmaxsimpchain (x # ys @ [y])
[PROOF STEP]
obtain ys
    where ys: "set ys \<subseteq> set xs" "length ys \<le> length xs" "padjacentchain (x#ys@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ys. \<lbrakk>set ys \<subseteq> set xs; length ys \<le> length xs; padjacentchain (x # ys @ [y])\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using maxsimpchainD_adj[OF assms(2)]
          adjacentchain_obtain_proper[OF assms(1)]
[PROOF STATE]
proof (prove)
using this:
adjacentchain (x # xs @ [y])
adjacentchain (x # ?xs @ [y]) \<Longrightarrow> \<exists>zs. set zs \<subseteq> set ?xs \<and> length zs \<le> length ?xs \<and> padjacentchain (x # zs @ [y])

goal (1 subgoal):
 1. (\<And>ys. \<lbrakk>set ys \<subseteq> set xs; length ys \<le> length xs; padjacentchain (x # ys @ [y])\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by    auto
[PROOF STATE]
proof (state)
this:
set ys \<subseteq> set xs
length ys \<le> length xs
padjacentchain (x # ys @ [y])

goal (1 subgoal):
 1. \<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and> pmaxsimpchain (x # ys @ [y])
[PROOF STEP]
from ys(1) assms(2)
[PROOF STATE]
proof (chain)
picking this:
set ys \<subseteq> set xs
maxsimpchain (x # xs @ [y])
[PROOF STEP]
have "\<forall>a\<in>set (x#ys@[y]). maxsimp a"
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> set xs
maxsimpchain (x # xs @ [y])

goal (1 subgoal):
 1. Ball (set (x # ys @ [y])) maxsimp
[PROOF STEP]
using maxsimpchainD_maxsimp
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> set xs
maxsimpchain (x # xs @ [y])
\<lbrakk>maxsimpchain ?xs; ?x \<in> set ?xs\<rbrakk> \<Longrightarrow> maxsimp ?x

goal (1 subgoal):
 1. Ball (set (x # ys @ [y])) maxsimp
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Ball (set (x # ys @ [y])) maxsimp

goal (1 subgoal):
 1. \<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and> pmaxsimpchain (x # ys @ [y])
[PROOF STEP]
with ys
[PROOF STATE]
proof (chain)
picking this:
set ys \<subseteq> set xs
length ys \<le> length xs
padjacentchain (x # ys @ [y])
Ball (set (x # ys @ [y])) maxsimp
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> set xs
length ys \<le> length xs
padjacentchain (x # ys @ [y])
Ball (set (x # ys @ [y])) maxsimp

goal (1 subgoal):
 1. \<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and> pmaxsimpchain (x # ys @ [y])
[PROOF STEP]
unfolding pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
set ys \<subseteq> set xs
length ys \<le> length xs
padjacentchain (x # ys @ [y])
Ball (set (x # ys @ [y])) maxsimp

goal (1 subgoal):
 1. \<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and> Ball (set (x # ys @ [y])) maxsimp \<and> padjacentchain (x # ys @ [y])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>ys. set ys \<subseteq> set xs \<and> length ys \<le> length xs \<and> pmaxsimpchain (x # ys @ [y])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_maxsimpchainD_maxsimpchain:
  assumes "min_maxsimpchain xs"
  shows   "maxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain xs
[PROOF STEP]
proof (cases xs rule: list_cases_Cons_snoc)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs = [] \<Longrightarrow> maxsimpchain xs
 2. \<And>x. xs = [x] \<Longrightarrow> maxsimpchain xs
 3. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
xs = []

goal (3 subgoals):
 1. xs = [] \<Longrightarrow> maxsimpchain xs
 2. \<And>x. xs = [x] \<Longrightarrow> maxsimpchain xs
 3. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = []

goal (1 subgoal):
 1. maxsimpchain xs
[PROOF STEP]
using maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
xs = []
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. maxsimpchain xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
maxsimpchain xs

goal (2 subgoals):
 1. \<And>x. xs = [x] \<Longrightarrow> maxsimpchain xs
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. xs = [x] \<Longrightarrow> maxsimpchain xs
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
case Single
[PROOF STATE]
proof (state)
this:
xs = [x_]

goal (2 subgoals):
 1. \<And>x. xs = [x] \<Longrightarrow> maxsimpchain xs
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain xs
xs = [x_]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = [x_]

goal (1 subgoal):
 1. maxsimpchain xs
[PROOF STEP]
using maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = [x_]
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. maxsimpchain xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
maxsimpchain xs

goal (1 subgoal):
 1. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
case Cons_snoc
[PROOF STATE]
proof (state)
this:
xs = x_ # ys_ @ [y_]

goal (1 subgoal):
 1. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> maxsimpchain xs
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain xs
xs = x_ # ys_ @ [y_]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x_ # ys_ @ [y_]

goal (1 subgoal):
 1. maxsimpchain xs
[PROOF STEP]
using is_arg_minD1
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x_ # ys_ @ [y_]
is_arg_min ?m ?P ?x \<Longrightarrow> ?P ?x

goal (1 subgoal):
 1. maxsimpchain xs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
maxsimpchain xs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_maxsimpchainI_betw:
  assumes "x\<noteq>y" "maxsimpchain (x#xs@[y])"
          "\<And>ys. maxsimpchain (x#ys@[y]) \<Longrightarrow> length xs \<le> length ys"
  shows   "min_maxsimpchain (x#xs@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_maxsimpchain (x # xs @ [y])
[PROOF STEP]
using   assms
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
maxsimpchain (x # xs @ [y])
maxsimpchain (x # ?ys @ [y]) \<Longrightarrow> length xs \<le> length ?ys

goal (1 subgoal):
 1. min_maxsimpchain (x # xs @ [y])
[PROOF STEP]
by (simp add: is_arg_min_linorderI)


[STATEMENT]
lemma min_maxsimpchainI_betw_compare:
  assumes "x\<noteq>y" "maxsimpchain (x#xs@[y])"
          "min_maxsimpchain (x#ys@[y])" "length xs = length ys"
  shows   "min_maxsimpchain (x#xs@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_maxsimpchain (x # xs @ [y])
[PROOF STEP]
using   assms min_maxsimpchainD_min_betw min_maxsimpchainI_betw
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
maxsimpchain (x # xs @ [y])
min_maxsimpchain (x # ys @ [y])
length xs = length ys
\<lbrakk>min_maxsimpchain (?x # ?xs @ [?y]); maxsimpchain (?x # ?ys @ [?y])\<rbrakk> \<Longrightarrow> length ?xs \<le> length ?ys
\<lbrakk>?x \<noteq> ?y; maxsimpchain (?x # ?xs @ [?y]); \<And>ys. maxsimpchain (?x # ys @ [?y]) \<Longrightarrow> length ?xs \<le> length ys\<rbrakk> \<Longrightarrow> min_maxsimpchain (?x # ?xs @ [?y])

goal (1 subgoal):
 1. min_maxsimpchain (x # xs @ [y])
[PROOF STEP]
by      auto


[STATEMENT]
lemma min_maxsimpchain_pmaxsimpchain:
  assumes "min_maxsimpchain xs"
  shows   "pmaxsimpchain xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmaxsimpchain xs
[PROOF STEP]
proof (
  rule pmaxsimpchainI_maxsimpchain, rule min_maxsimpchainD_maxsimpchain,
  rule assms, cases xs rule: list_cases_Cons_snoc
)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs = [] \<Longrightarrow> distinct xs
 2. \<And>x. xs = [x] \<Longrightarrow> distinct xs
 3. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> distinct xs
[PROOF STEP]
case (Cons_snoc x ys y)
[PROOF STATE]
proof (state)
this:
xs = x # ys @ [y]

goal (3 subgoals):
 1. xs = [] \<Longrightarrow> distinct xs
 2. \<And>x. xs = [x] \<Longrightarrow> distinct xs
 3. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> distinct xs
[PROOF STEP]
have "\<not> distinct (x#ys@[y]) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> distinct (x # ys @ [y]) \<Longrightarrow> False
[PROOF STEP]
proof (cases "x\<in>set ys" "y\<in>set ys" rule: two_cases)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case both
[PROOF STATE]
proof (state)
this:
x \<in> set ys
y \<in> set ys

goal (4 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from both(1)
[PROOF STATE]
proof (chain)
picking this:
x \<in> set ys
[PROOF STEP]
obtain as bs where "ys = as@x#bs"
[PROOF STATE]
proof (prove)
using this:
x \<in> set ys

goal (1 subgoal):
 1. (\<And>as bs. ys = as @ x # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using in_set_conv_decomp[of x ys]
[PROOF STATE]
proof (prove)
using this:
x \<in> set ys
(x \<in> set ys) = (\<exists>ysa zs. ys = ysa @ x # zs)

goal (1 subgoal):
 1. (\<And>as bs. ys = as @ x # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
ys = as @ x # bs

goal (4 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 4. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ x # bs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ x # bs

goal (1 subgoal):
 1. False
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain[OF assms]
            maxsimpchain_append_reduce2[of "x#as"]
            min_maxsimpchainD_min_betw[of x ys y]
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ x # bs
maxsimpchain xs
maxsimpchain ((x # as) @ ?ys) \<Longrightarrow> maxsimpchain ?ys
\<lbrakk>min_maxsimpchain (x # ys @ [y]); maxsimpchain (x # ?ys @ [y])\<rbrakk> \<Longrightarrow> length ys \<le> length ?ys

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

goal (3 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case one
[PROOF STATE]
proof (state)
this:
x \<in> set ys
y \<notin> set ys

goal (3 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from one(1)
[PROOF STATE]
proof (chain)
picking this:
x \<in> set ys
[PROOF STEP]
obtain as bs where "ys = as@x#bs"
[PROOF STATE]
proof (prove)
using this:
x \<in> set ys

goal (1 subgoal):
 1. (\<And>as bs. ys = as @ x # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using in_set_conv_decomp[of x ys]
[PROOF STATE]
proof (prove)
using this:
x \<in> set ys
(x \<in> set ys) = (\<exists>ysa zs. ys = ysa @ x # zs)

goal (1 subgoal):
 1. (\<And>as bs. ys = as @ x # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
ys = as @ x # bs

goal (3 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<in> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 3. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ x # bs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ x # bs

goal (1 subgoal):
 1. False
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain[OF assms]
            maxsimpchain_append_reduce2[of "x#as"]
            min_maxsimpchainD_min_betw[of x ys y]
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ x # bs
maxsimpchain xs
maxsimpchain ((x # as) @ ?ys) \<Longrightarrow> maxsimpchain ?ys
\<lbrakk>min_maxsimpchain (x # ys @ [y]); maxsimpchain (x # ?ys @ [y])\<rbrakk> \<Longrightarrow> length ys \<le> length ?ys

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

goal (2 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case other
[PROOF STATE]
proof (state)
this:
x \<notin> set ys
y \<in> set ys

goal (2 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
from other(2)
[PROOF STATE]
proof (chain)
picking this:
y \<in> set ys
[PROOF STEP]
obtain as bs where "ys = as@y#bs"
[PROOF STATE]
proof (prove)
using this:
y \<in> set ys

goal (1 subgoal):
 1. (\<And>as bs. ys = as @ y # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using in_set_conv_decomp[of y ys]
[PROOF STATE]
proof (prove)
using this:
y \<in> set ys
(y \<in> set ys) = (\<exists>ysa zs. ys = ysa @ y # zs)

goal (1 subgoal):
 1. (\<And>as bs. ys = as @ y # bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
ys = as @ y # bs

goal (2 subgoals):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<in> set ys\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ y # bs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ y # bs

goal (1 subgoal):
 1. False
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain[OF assms]
            maxsimpchain_append_reduce1[of "x#as@[y]"]
            min_maxsimpchainD_min_betw[of x ys y]
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ y # bs
maxsimpchain xs
maxsimpchain ((x # as @ [y]) @ ?ys) \<Longrightarrow> maxsimpchain (x # as @ [y])
\<lbrakk>min_maxsimpchain (x # ys @ [y]); maxsimpchain (x # ?ys @ [y])\<rbrakk> \<Longrightarrow> length ys \<le> length ?ys

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

goal (1 subgoal):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case neither
[PROOF STATE]
proof (state)
this:
x \<notin> set ys
y \<notin> set ys

goal (1 subgoal):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x \<notin> set ys
y \<notin> set ys

goal (1 subgoal):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume "\<not> distinct (x # ys @ [y])"
[PROOF STATE]
proof (state)
this:
\<not> distinct (x # ys @ [y])

goal (1 subgoal):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x \<notin> set ys
y \<notin> set ys
\<not> distinct (x # ys @ [y])
[PROOF STEP]
obtain as a bs cs where "ys = as@[a]@bs@[a]@cs"
[PROOF STATE]
proof (prove)
using this:
x \<notin> set ys
y \<notin> set ys
\<not> distinct (x # ys @ [y])

goal (1 subgoal):
 1. (\<And>as a bs cs. ys = as @ [a] @ bs @ [a] @ cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms Cons_snoc not_distinct_decomp[of ys]
[PROOF STATE]
proof (prove)
using this:
x \<notin> set ys
y \<notin> set ys
\<not> distinct (x # ys @ [y])
min_maxsimpchain xs
xs = x # ys @ [y]
\<not> distinct ys \<Longrightarrow> \<exists>xs ysa zs y. ys = xs @ [y] @ ysa @ [y] @ zs

goal (1 subgoal):
 1. (\<And>as a bs cs. ys = as @ [a] @ bs @ [a] @ cs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ys = as @ [a] @ bs @ [a] @ cs

goal (1 subgoal):
 1. \<lbrakk>\<not> distinct (x # ys @ [y]); x \<notin> set ys; y \<notin> set ys\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
with assms Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ [a] @ bs @ [a] @ cs
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ [a] @ bs @ [a] @ cs

goal (1 subgoal):
 1. False
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain[OF assms]
            maxsimpchain_append_reduce1[of "x#as@[a]"]
            maxsimpchain_append_reduce2[of "x#as@[a]@bs" "a#cs@[y]"]
            maxsimpchain_overlap_join[of "x#as" a "cs@[y]"]
            min_maxsimpchainD_min_betw[of x ys y "as@a#cs"]
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = x # ys @ [y]
ys = as @ [a] @ bs @ [a] @ cs
maxsimpchain xs
maxsimpchain ((x # as @ [a]) @ ?ys) \<Longrightarrow> maxsimpchain (x # as @ [a])
maxsimpchain ((x # as @ [a] @ bs) @ a # cs @ [y]) \<Longrightarrow> maxsimpchain (a # cs @ [y])
\<lbrakk>maxsimpchain ((x # as) @ [a]); maxsimpchain (a # cs @ [y])\<rbrakk> \<Longrightarrow> maxsimpchain ((x # as) @ a # cs @ [y])
\<lbrakk>min_maxsimpchain (x # ys @ [y]); maxsimpchain (x # (as @ a # cs) @ [y])\<rbrakk> \<Longrightarrow> length ys \<le> length (as @ a # cs)

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> distinct (x # ys @ [y]) \<Longrightarrow> False

goal (3 subgoals):
 1. xs = [] \<Longrightarrow> distinct xs
 2. \<And>x. xs = [x] \<Longrightarrow> distinct xs
 3. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> distinct xs
[PROOF STEP]
with Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
xs = x # ys @ [y]
\<not> distinct (x # ys @ [y]) \<Longrightarrow> False
[PROOF STEP]
show "distinct xs"
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]
\<not> distinct (x # ys @ [y]) \<Longrightarrow> False

goal (1 subgoal):
 1. distinct xs
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
distinct xs

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> distinct xs
 2. \<And>x. xs = [x] \<Longrightarrow> distinct xs
[PROOF STEP]
qed auto


[STATEMENT]
lemma min_maxsimpchain_rev:
  assumes "min_maxsimpchain xs"
  shows   "min_maxsimpchain (rev xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_maxsimpchain (rev xs)
[PROOF STEP]
proof (cases xs rule: list_cases_Cons_snoc)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
 2. \<And>x. xs = [x] \<Longrightarrow> min_maxsimpchain (rev xs)
 3. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
case Single
[PROOF STATE]
proof (state)
this:
xs = [x_]

goal (3 subgoals):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
 2. \<And>x. xs = [x] \<Longrightarrow> min_maxsimpchain (rev xs)
 3. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain xs
xs = [x_]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = [x_]

goal (1 subgoal):
 1. min_maxsimpchain (rev xs)
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain maxsimpchainD_maxsimp
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain xs
xs = [x_]
min_maxsimpchain ?xs \<Longrightarrow> maxsimpchain ?xs
\<lbrakk>maxsimpchain ?xs; ?x \<in> set ?xs\<rbrakk> \<Longrightarrow> maxsimp ?x

goal (1 subgoal):
 1. min_maxsimpchain (rev xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
min_maxsimpchain (rev xs)

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
case (Cons_snoc x ys y)
[PROOF STATE]
proof (state)
this:
xs = x # ys @ [y]

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xs = x # ys @ [y]

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
have "min_maxsimpchain (y # rev ys @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_maxsimpchain (y # rev ys @ [x])
[PROOF STEP]
proof (rule min_maxsimpchainI_betw)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. y \<noteq> x
 2. maxsimpchain (y # rev ys @ [x])
 3. \<And>ysa. maxsimpchain (y # ysa @ [x]) \<Longrightarrow> length (rev ys) \<le> length ysa
[PROOF STEP]
from Cons_snoc assms
[PROOF STATE]
proof (chain)
picking this:
xs = x # ys @ [y]
min_maxsimpchain xs
[PROOF STEP]
show "y\<noteq>x"
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]
min_maxsimpchain xs

goal (1 subgoal):
 1. y \<noteq> x
[PROOF STEP]
using min_maxsimpchain_pmaxsimpchain pmaxsimpchainD_distinct
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]
min_maxsimpchain xs
min_maxsimpchain ?xs \<Longrightarrow> pmaxsimpchain ?xs
pmaxsimpchain ?xs \<Longrightarrow> distinct ?xs

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

goal (2 subgoals):
 1. maxsimpchain (y # rev ys @ [x])
 2. \<And>ysa. maxsimpchain (y # ysa @ [x]) \<Longrightarrow> length (rev ys) \<le> length ysa
[PROOF STEP]
from Cons_snoc
[PROOF STATE]
proof (chain)
picking this:
xs = x # ys @ [y]
[PROOF STEP]
show "maxsimpchain (y # rev ys @ [x])"
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]

goal (1 subgoal):
 1. maxsimpchain (y # rev ys @ [x])
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_rev
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]
maxsimpchain xs
maxsimpchain ?xs \<Longrightarrow> maxsimpchain (rev ?xs)

goal (1 subgoal):
 1. maxsimpchain (y # rev ys @ [x])
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
maxsimpchain (y # rev ys @ [x])

goal (1 subgoal):
 1. \<And>ysa. maxsimpchain (y # ysa @ [x]) \<Longrightarrow> length (rev ys) \<le> length ysa
[PROOF STEP]
from Cons_snoc assms
[PROOF STATE]
proof (chain)
picking this:
xs = x # ys @ [y]
min_maxsimpchain xs
[PROOF STEP]
show  "\<And>zs. maxsimpchain (y#zs@[x]) \<Longrightarrow> length (rev ys) \<le> length zs"
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]
min_maxsimpchain xs

goal (1 subgoal):
 1. \<And>zs. maxsimpchain (y # zs @ [x]) \<Longrightarrow> length (rev ys) \<le> length zs
[PROOF STEP]
using maxsimpchain_rev min_maxsimpchainD_min_betw[of x ys y]
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]
min_maxsimpchain xs
maxsimpchain ?xs \<Longrightarrow> maxsimpchain (rev ?xs)
\<lbrakk>min_maxsimpchain (x # ys @ [y]); maxsimpchain (x # ?ys @ [y])\<rbrakk> \<Longrightarrow> length ys \<le> length ?ys

goal (1 subgoal):
 1. \<And>zs. maxsimpchain (y # zs @ [x]) \<Longrightarrow> length (rev ys) \<le> length zs
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
maxsimpchain (y # ?zs @ [x]) \<Longrightarrow> length (rev ys) \<le> length ?zs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
min_maxsimpchain (y # rev ys @ [x])

goal (2 subgoals):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
 2. \<And>x ys y. xs = x # ys @ [y] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
xs = x # ys @ [y]
min_maxsimpchain (y # rev ys @ [x])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = x # ys @ [y]
min_maxsimpchain (y # rev ys @ [x])

goal (1 subgoal):
 1. min_maxsimpchain (rev xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
min_maxsimpchain (rev xs)

goal (1 subgoal):
 1. xs = [] \<Longrightarrow> min_maxsimpchain (rev xs)
[PROOF STEP]
qed simp


[STATEMENT]
lemma min_maxsimpchain_adj:
  "\<lbrakk> maxsimp x; maxsimp y; x\<sim>y; x\<noteq>y \<rbrakk> \<Longrightarrow> min_maxsimpchain [x,y]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimp x; maxsimp y; x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> min_maxsimpchain [x, y]
[PROOF STEP]
using maxsimpchain_def min_maxsimpchainI_betw[of x y "[]"]
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs
\<lbrakk>x \<noteq> y; maxsimpchain (x # [] @ [y]); \<And>ys. maxsimpchain (x # ys @ [y]) \<Longrightarrow> length [] \<le> length ys\<rbrakk> \<Longrightarrow> min_maxsimpchain (x # [] @ [y])

goal (1 subgoal):
 1. \<lbrakk>maxsimp x; maxsimp y; x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> min_maxsimpchain [x, y]
[PROOF STEP]
by simp


[STATEMENT]
lemma min_maxsimpchain_betw_CCons_reduce:
  assumes "min_maxsimpchain (w#x#ys@[z])"
  shows   "min_maxsimpchain (x#ys@[z])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. min_maxsimpchain (x # ys @ [z])
[PROOF STEP]
proof (rule min_maxsimpchainI_betw)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x \<noteq> z
 2. maxsimpchain (x # ys @ [z])
 3. \<And>ysa. maxsimpchain (x # ysa @ [z]) \<Longrightarrow> length ys \<le> length ysa
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain (w # x # ys @ [z])
[PROOF STEP]
show "x\<noteq>z"
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain (w # x # ys @ [z])

goal (1 subgoal):
 1. x \<noteq> z
[PROOF STEP]
using min_maxsimpchain_pmaxsimpchain pmaxsimpchainD_distinct
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain (w # x # ys @ [z])
min_maxsimpchain ?xs \<Longrightarrow> pmaxsimpchain ?xs
pmaxsimpchain ?xs \<Longrightarrow> distinct ?xs

goal (1 subgoal):
 1. x \<noteq> z
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
x \<noteq> z

goal (2 subgoals):
 1. maxsimpchain (x # ys @ [z])
 2. \<And>ysa. maxsimpchain (x # ysa @ [z]) \<Longrightarrow> length ys \<le> length ysa
[PROOF STEP]
show "maxsimpchain (x#ys@[z])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimpchain (x # ys @ [z])
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain[OF assms]
          maxsimpchain_Cons_reduce
[PROOF STATE]
proof (prove)
using this:
maxsimpchain (w # x # ys @ [z])
maxsimpchain (?x # ?xs) \<Longrightarrow> maxsimpchain ?xs

goal (1 subgoal):
 1. maxsimpchain (x # ys @ [z])
[PROOF STEP]
by    fast
[PROOF STATE]
proof (state)
this:
maxsimpchain (x # ys @ [z])

goal (1 subgoal):
 1. \<And>ysa. maxsimpchain (x # ysa @ [z]) \<Longrightarrow> length ys \<le> length ysa
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ysa. maxsimpchain (x # ysa @ [z]) \<Longrightarrow> length ys \<le> length ysa
[PROOF STEP]
fix zs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>ysa. maxsimpchain (x # ysa @ [z]) \<Longrightarrow> length ys \<le> length ysa
[PROOF STEP]
assume "maxsimpchain (x#zs@[z])"
[PROOF STATE]
proof (state)
this:
maxsimpchain (x # zs @ [z])

goal (1 subgoal):
 1. \<And>ysa. maxsimpchain (x # ysa @ [z]) \<Longrightarrow> length ys \<le> length ysa
[PROOF STEP]
hence "maxsimpchain (w#x#zs@[z])"
[PROOF STATE]
proof (prove)
using this:
maxsimpchain (x # zs @ [z])

goal (1 subgoal):
 1. maxsimpchain (w # x # zs @ [z])
[PROOF STEP]
using min_maxsimpchainD_maxsimpchain[OF assms] maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain (x # zs @ [z])
maxsimpchain (w # x # ys @ [z])
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs

goal (1 subgoal):
 1. maxsimpchain (w # x # zs @ [z])
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
maxsimpchain (w # x # zs @ [z])

goal (1 subgoal):
 1. \<And>ysa. maxsimpchain (x # ysa @ [z]) \<Longrightarrow> length ys \<le> length ysa
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
min_maxsimpchain (w # x # ys @ [z])
maxsimpchain (w # x # zs @ [z])
[PROOF STEP]
show "length ys \<le> length zs"
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain (w # x # ys @ [z])
maxsimpchain (w # x # zs @ [z])

goal (1 subgoal):
 1. length ys \<le> length zs
[PROOF STEP]
using min_maxsimpchainD_min_betw[of w "x#ys" z "x#zs"]
[PROOF STATE]
proof (prove)
using this:
min_maxsimpchain (w # x # ys @ [z])
maxsimpchain (w # x # zs @ [z])
\<lbrakk>min_maxsimpchain (w # (x # ys) @ [z]); maxsimpchain (w # (x # zs) @ [z])\<rbrakk> \<Longrightarrow> length (x # ys) \<le> length (x # zs)

goal (1 subgoal):
 1. length ys \<le> length zs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length ys \<le> length zs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma min_maxsimpchain_betw_uniform_length:
  assumes "min_maxsimpchain (x#xs@[y])" "min_maxsimpchain (x#ys@[y])"
  shows   "length xs = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
using   min_maxsimpchainD_min_betw[OF assms(1)]
          min_maxsimpchainD_min_betw[OF assms(2)]
          min_maxsimpchainD_maxsimpchain[OF assms(1)]
          min_maxsimpchainD_maxsimpchain[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
maxsimpchain (x # ?ys @ [y]) \<Longrightarrow> length xs \<le> length ?ys
maxsimpchain (x # ?ys @ [y]) \<Longrightarrow> length ys \<le> length ?ys
maxsimpchain (x # xs @ [y])
maxsimpchain (x # ys @ [y])

goal (1 subgoal):
 1. length xs = length ys
[PROOF STEP]
by      fastforce


[STATEMENT]
lemma not_min_maxsimpchainI_betw:
  "\<lbrakk> maxsimpchain (x#ys@[y]); length ys < length xs \<rbrakk> \<Longrightarrow>
    \<not> min_maxsimpchain (x#xs@[y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimpchain (x # ys @ [y]); length ys < length xs\<rbrakk> \<Longrightarrow> \<not> min_maxsimpchain (x # xs @ [y])
[PROOF STEP]
using min_maxsimpchainD_min_betw not_less
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>min_maxsimpchain (?x # ?xs @ [?y]); maxsimpchain (?x # ?ys @ [?y])\<rbrakk> \<Longrightarrow> length ?xs \<le> length ?ys
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. \<lbrakk>maxsimpchain (x # ys @ [y]); length ys < length xs\<rbrakk> \<Longrightarrow> \<not> min_maxsimpchain (x # xs @ [y])
[PROOF STEP]
by blast


[STATEMENT]
lemma maxsimpchain_in_subcomplex:
  "\<lbrakk> Subcomplex Y; set ys \<subseteq> Y; maxsimpchain ys \<rbrakk> \<Longrightarrow>
    SimplicialComplex.maxsimpchain Y ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Subcomplex Y; set ys \<subseteq> Y; maxsimpchain ys\<rbrakk> \<Longrightarrow> SimplicialComplex.maxsimpchain Y ys
[PROOF STEP]
using maxsimpchain_def max_in_subcomplex
        SimplicialComplex.maxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
maxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> adjacentchain ?xs
\<lbrakk>Subcomplex ?Y; ?y \<in> ?Y; maxsimp ?y\<rbrakk> \<Longrightarrow> SimplicialComplex.maxsimp ?Y ?y
SimplicialComplex ?X \<Longrightarrow> SimplicialComplex.maxsimpchain ?X ?xs \<equiv> (\<forall>x\<in>set ?xs. SimplicialComplex.maxsimp ?X x) \<and> adjacentchain ?xs

goal (1 subgoal):
 1. \<lbrakk>Subcomplex Y; set ys \<subseteq> Y; maxsimpchain ys\<rbrakk> \<Longrightarrow> SimplicialComplex.maxsimpchain Y ys
[PROOF STEP]
by    force


[STATEMENT]
lemma iso_codim_map:
  "x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> card (f`x - f`y) = card (x-y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> card (f ` x - f ` y) = card (x - y)
[PROOF STEP]
using inj inj_on_image_set_diff[of f _ x y] finite_simplex subset_inj_on[of f _ "x-y"]
        inj_on_iff_eq_card[of "x-y"]
[PROOF STATE]
proof (prove)
using this:
inj_on f (\<Union> X)
\<lbrakk>inj_on f ?C; x - y \<subseteq> ?C; y \<subseteq> ?C\<rbrakk> \<Longrightarrow> f ` (x - y) = f ` x - f ` y
?x \<in> X \<Longrightarrow> finite ?x
\<lbrakk>inj_on f ?B; x - y \<subseteq> ?B\<rbrakk> \<Longrightarrow> inj_on f (x - y)
finite (x - y) \<Longrightarrow> inj_on ?f (x - y) = (card (?f ` (x - y)) = card (x - y))

goal (1 subgoal):
 1. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> card (f ` x - f ` y) = card (x - y)
[PROOF STEP]
by    fastforce


[STATEMENT]
lemma maxsimp_im_max: "maxsimp x \<Longrightarrow> w \<in> X \<Longrightarrow> f`x \<subseteq> f`w \<Longrightarrow> f`w = f`x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>maxsimp x; w \<in> X; f ` x \<subseteq> f ` w\<rbrakk> \<Longrightarrow> f ` w = f ` x
[PROOF STEP]
using maxsimpD_simplex inj_onD[OF inj] maxsimpD_maximal[of x w]
[PROOF STATE]
proof (prove)
using this:
maxsimp ?x \<Longrightarrow> ?x \<in> X
\<lbrakk>f ?x = f ?y; ?x \<in> \<Union> X; ?y \<in> \<Union> X\<rbrakk> \<Longrightarrow> ?x = ?y
\<lbrakk>maxsimp x; w \<in> X; x \<subseteq> w\<rbrakk> \<Longrightarrow> w = x

goal (1 subgoal):
 1. \<lbrakk>maxsimp x; w \<in> X; f ` x \<subseteq> f ` w\<rbrakk> \<Longrightarrow> f ` w = f ` x
[PROOF STEP]
by blast


[STATEMENT]
lemma maxsimp_map:
  "maxsimp x \<Longrightarrow> SimplicialComplex.maxsimp (f\<turnstile>X) (f`x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. maxsimp x \<Longrightarrow> SimplicialComplex.maxsimp (f \<turnstile> X) (f ` x)
[PROOF STEP]
using maxsimpD_simplex maxsimp_im_max morph
        SimplicialComplex.maxsimpI[of "f\<turnstile>X" "f`x"]
[PROOF STATE]
proof (prove)
using this:
maxsimp ?x \<Longrightarrow> ?x \<in> X
\<lbrakk>maxsimp ?x; ?w \<in> X; f ` ?x \<subseteq> f ` ?w\<rbrakk> \<Longrightarrow> f ` ?w = f ` ?x
SimplicialComplex (f \<turnstile> X)
\<lbrakk>SimplicialComplex (f \<turnstile> X); f ` x \<in> f \<turnstile> X; \<And>z. \<lbrakk>z \<in> f \<turnstile> X; f ` x \<subseteq> z\<rbrakk> \<Longrightarrow> z = f ` x\<rbrakk> \<Longrightarrow> SimplicialComplex.maxsimp (f \<turnstile> X) (f ` x)

goal (1 subgoal):
 1. maxsimp x \<Longrightarrow> SimplicialComplex.maxsimp (f \<turnstile> X) (f ` x)
[PROOF STEP]
by    fastforce


[STATEMENT]
lemma iso_adj_int_im:
  assumes "maxsimp x" "maxsimp y" "x\<sim>y" "x\<noteq>y"
  shows "(f`x \<inter> f`y) \<lhd> f`x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` x \<inter> f ` y \<lhd> f ` x
[PROOF STEP]
proof (rule facetrelI_card)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f ` x \<inter> f ` y \<subseteq> f ` x
 2. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
maxsimp x
maxsimp y
[PROOF STEP]
have  1: "f ` x \<subseteq> f ` y \<Longrightarrow> f ` y = f ` x"
[PROOF STATE]
proof (prove)
using this:
maxsimp x
maxsimp y

goal (1 subgoal):
 1. f ` x \<subseteq> f ` y \<Longrightarrow> f ` y = f ` x
[PROOF STEP]
using maxsimp_map SimplicialComplex.maxsimpD_simplex[OF morph]
          SimplicialComplex.maxsimpD_maximal[OF morph]
[PROOF STATE]
proof (prove)
using this:
maxsimp x
maxsimp y
maxsimp ?x \<Longrightarrow> SimplicialComplex.maxsimp (f \<turnstile> X) (f ` ?x)
SimplicialComplex.maxsimp (f \<turnstile> X) ?x \<Longrightarrow> ?x \<in> f \<turnstile> X
\<lbrakk>SimplicialComplex.maxsimp (f \<turnstile> X) ?x; ?z \<in> f \<turnstile> X; ?x \<subseteq> ?z\<rbrakk> \<Longrightarrow> ?z = ?x

goal (1 subgoal):
 1. f ` x \<subseteq> f ` y \<Longrightarrow> f ` y = f ` x
[PROOF STEP]
by    simp
[PROOF STATE]
proof (state)
this:
f ` x \<subseteq> f ` y \<Longrightarrow> f ` y = f ` x

goal (2 subgoals):
 1. f ` x \<inter> f ` y \<subseteq> f ` x
 2. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
thus "f`x \<inter> f`y \<subseteq> f`x"
[PROOF STATE]
proof (prove)
using this:
f ` x \<subseteq> f ` y \<Longrightarrow> f ` y = f ` x

goal (1 subgoal):
 1. f ` x \<inter> f ` y \<subseteq> f ` x
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
f ` x \<inter> f ` y \<subseteq> f ` x

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
maxsimp x
[PROOF STEP]
have "card (f`x - f`x \<inter> f`y) \<le> card (f`x - f`(x\<inter>y))"
[PROOF STATE]
proof (prove)
using this:
maxsimp x

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) \<le> card (f ` x - f ` (x \<inter> y))
[PROOF STEP]
using finite_maxsimp card_mono[of "f`x - f`(x\<inter>y)" "f`x - f`x \<inter> f`y"]
[PROOF STATE]
proof (prove)
using this:
maxsimp x
maxsimp ?x \<Longrightarrow> finite ?x
\<lbrakk>finite (f ` x - f ` (x \<inter> y)); f ` x - f ` x \<inter> f ` y \<subseteq> f ` x - f ` (x \<inter> y)\<rbrakk> \<Longrightarrow> card (f ` x - f ` x \<inter> f ` y) \<le> card (f ` x - f ` (x \<inter> y))

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) \<le> card (f ` x - f ` (x \<inter> y))
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
card (f ` x - f ` x \<inter> f ` y) \<le> card (f ` x - f ` (x \<inter> y))

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (f ` x - f ` x \<inter> f ` y) \<le> card (f ` x - f ` (x \<inter> y))

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
from assms(1,3,4)
[PROOF STATE]
proof (chain)
picking this:
maxsimp x
x \<sim> y
x \<noteq> y
[PROOF STEP]
have "card (f`x - f`(x\<inter>y)) = 1"
[PROOF STATE]
proof (prove)
using this:
maxsimp x
x \<sim> y
x \<noteq> y

goal (1 subgoal):
 1. card (f ` x - f ` (x \<inter> y)) = 1
[PROOF STEP]
using maxsimpD_simplex faces[of x] maxsimpD_simplex
          iso_codim_map adjacent_int_facet1[of x y] facetrel_card
[PROOF STATE]
proof (prove)
using this:
maxsimp x
x \<sim> y
x \<noteq> y
maxsimp ?x \<Longrightarrow> ?x \<in> X
\<lbrakk>x \<in> X; ?y \<subseteq> x\<rbrakk> \<Longrightarrow> ?y \<in> X
maxsimp ?x \<Longrightarrow> ?x \<in> X
\<lbrakk>?x \<in> X; ?y \<in> X\<rbrakk> \<Longrightarrow> card (f ` ?x - f ` ?y) = card (?x - ?y)
\<lbrakk>x \<sim> y; x \<noteq> y\<rbrakk> \<Longrightarrow> x \<inter> y \<lhd> x
?y \<lhd> ?x \<Longrightarrow> card (?x - ?y) = 1

goal (1 subgoal):
 1. card (f ` x - f ` (x \<inter> y)) = 1
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
card (f ` x - f ` (x \<inter> y)) = 1

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (f ` x - f ` x \<inter> f ` y) \<le> card (f ` x - f ` (x \<inter> y))
card (f ` x - f ` (x \<inter> y)) = 1
[PROOF STEP]
have "card (f`x - f`x \<inter> f`y) \<le> 1"
[PROOF STATE]
proof (prove)
using this:
card (f ` x - f ` x \<inter> f ` y) \<le> card (f ` x - f ` (x \<inter> y))
card (f ` x - f ` (x \<inter> y)) = 1

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) \<le> 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (f ` x - f ` x \<inter> f ` y) \<le> 1

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
card (f ` x - f ` x \<inter> f ` y) \<le> 1

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
from assms(1,2,4)
[PROOF STATE]
proof (chain)
picking this:
maxsimp x
maxsimp y
x \<noteq> y
[PROOF STEP]
have "card (f`x - f`x \<inter> f`y) \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
maxsimp x
maxsimp y
x \<noteq> y

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) \<noteq> 0
[PROOF STEP]
using 1 maxsimpD_simplex finite_maxsimp
          inj_onD[OF induced_pow_fun_inj_on, OF inj, of x y]
[PROOF STATE]
proof (prove)
using this:
maxsimp x
maxsimp y
x \<noteq> y
f ` x \<subseteq> f ` y \<Longrightarrow> f ` y = f ` x
maxsimp ?x \<Longrightarrow> ?x \<in> X
maxsimp ?x \<Longrightarrow> finite ?x
\<lbrakk>f ` x = f ` y; x \<in> Pow (\<Union> X); y \<in> Pow (\<Union> X)\<rbrakk> \<Longrightarrow> x = y

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) \<noteq> 0
[PROOF STEP]
by    auto
[PROOF STATE]
proof (state)
this:
card (f ` x - f ` x \<inter> f ` y) \<noteq> 0

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
card (f ` x - f ` x \<inter> f ` y) \<le> 1
card (f ` x - f ` x \<inter> f ` y) \<noteq> 0
[PROOF STEP]
show "card (f`x - f`x \<inter> f`y) = 1"
[PROOF STATE]
proof (prove)
using this:
card (f ` x - f ` x \<inter> f ` y) \<le> 1
card (f ` x - f ` x \<inter> f ` y) \<noteq> 0

goal (1 subgoal):
 1. card (f ` x - f ` x \<inter> f ` y) = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card (f ` x - f ` x \<inter> f ` y) = 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_adj_map:
  assumes "maxsimp x" "maxsimp y" "x\<sim>y" "x\<noteq>y"
  shows   "f`x \<sim> f`y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` x \<sim> f ` y
[PROOF STEP]
using assms(3,4) iso_adj_int_im[OF assms] adjacent_sym
        iso_adj_int_im[OF assms(2) assms(1)]
[PROOF STATE]
proof (prove)
using this:
x \<sim> y
x \<noteq> y
f ` x \<inter> f ` y \<lhd> f ` x
?x \<sim> ?y \<Longrightarrow> ?y \<sim> ?x
\<lbrakk>y \<sim> x; y \<noteq> x\<rbrakk> \<Longrightarrow> f ` y \<inter> f ` x \<lhd> f ` y

goal (1 subgoal):
 1. f ` x \<sim> f ` y
[PROOF STEP]
by    (auto simp add: Int_commute intro: adjacentI)