[STATEMENT]
lemma pmaxsimpchain_map:
  "pmaxsimpchain xs \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f\<turnstile>X) (f\<Turnstile>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmaxsimpchain xs \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> xs)
[PROOF STEP]
proof (induct xs rule: list_induct_CCons)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. pmaxsimpchain [] \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [])
 2. \<And>x. pmaxsimpchain [x] \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])
 3. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
pmaxsimpchain []

goal (3 subgoals):
 1. pmaxsimpchain [] \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [])
 2. \<And>x. pmaxsimpchain [x] \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])
 3. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [])
[PROOF STEP]
using map_is_simplicial_morph SimplicialComplex.pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
SimplicialComplex (?f \<turnstile> X)
SimplicialComplex ?X \<Longrightarrow> SimplicialComplex.pmaxsimpchain ?X ?xs \<equiv> (\<forall>x\<in>set ?xs. SimplicialComplex.maxsimp ?X x) \<and> padjacentchain ?xs

goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [])
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [])

goal (2 subgoals):
 1. \<And>x. pmaxsimpchain [x] \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])
 2. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. pmaxsimpchain [x] \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])
 2. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
case (Single x)
[PROOF STATE]
proof (state)
this:
pmaxsimpchain [x]

goal (2 subgoals):
 1. \<And>x. pmaxsimpchain [x] \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])
 2. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain [x]

goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])
[PROOF STEP]
using map_is_simplicial_morph pmaxsimpchainD_maxsimp maxsimp_map
          SimplicialComplex.pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain [x]
SimplicialComplex (?f \<turnstile> X)
\<lbrakk>pmaxsimpchain ?xs; ?x \<in> set ?xs\<rbrakk> \<Longrightarrow> maxsimp ?x
maxsimp ?x \<Longrightarrow> SimplicialComplex.maxsimp (f \<turnstile> X) (f ` ?x)
SimplicialComplex ?X \<Longrightarrow> SimplicialComplex.pmaxsimpchain ?X ?xs \<equiv> (\<forall>x\<in>set ?xs. SimplicialComplex.maxsimp ?X x) \<and> padjacentchain ?xs

goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])
[PROOF STEP]
by    fastforce
[PROOF STATE]
proof (state)
this:
SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> [x])

goal (1 subgoal):
 1. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
case (CCons x y xs)
[PROOF STATE]
proof (state)
this:
pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs))
pmaxsimpchain (x # y # xs)

goal (1 subgoal):
 1. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
have "SimplicialComplex.pmaxsimpchain (f \<turnstile> X) ( f`x # f`y # f\<Turnstile>xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` x # f ` y # f \<Turnstile> xs)
[PROOF STEP]
proof (
    rule SimplicialComplex.pmaxsimpchain_CConsI,
    rule map_is_simplicial_morph
  )
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. SimplicialComplex.maxsimp (f \<turnstile> X) (f ` x)
 2. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` y # f \<Turnstile> xs)
 3. f ` x \<sim> f ` y
 4. f ` x \<notin> set (f ` y # f \<Turnstile> xs)
[PROOF STEP]
from CCons(2)
[PROOF STATE]
proof (chain)
picking this:
pmaxsimpchain (x # y # xs)
[PROOF STEP]
show "SimplicialComplex.maxsimp (f\<turnstile>X) (f`x)"
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain (x # y # xs)

goal (1 subgoal):
 1. SimplicialComplex.maxsimp (f \<turnstile> X) (f ` x)
[PROOF STEP]
using pmaxsimpchainD_maxsimp maxsimp_map
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain (x # y # xs)
\<lbrakk>pmaxsimpchain ?xs; ?x \<in> set ?xs\<rbrakk> \<Longrightarrow> maxsimp ?x
maxsimp ?x \<Longrightarrow> SimplicialComplex.maxsimp (f \<turnstile> X) (f ` ?x)

goal (1 subgoal):
 1. SimplicialComplex.maxsimp (f \<turnstile> X) (f ` x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
SimplicialComplex.maxsimp (f \<turnstile> X) (f ` x)

goal (3 subgoals):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` y # f \<Turnstile> xs)
 2. f ` x \<sim> f ` y
 3. f ` x \<notin> set (f ` y # f \<Turnstile> xs)
[PROOF STEP]
from CCons
[PROOF STATE]
proof (chain)
picking this:
pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs))
pmaxsimpchain (x # y # xs)
[PROOF STEP]
show "SimplicialComplex.pmaxsimpchain (f\<turnstile>X) (f`y # f\<Turnstile>xs)"
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs))
pmaxsimpchain (x # y # xs)

goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` y # f \<Turnstile> xs)
[PROOF STEP]
using pmaxsimpchain_Cons_reduce
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs))
pmaxsimpchain (x # y # xs)
pmaxsimpchain (?x # ?xs) \<Longrightarrow> pmaxsimpchain ?xs

goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` y # f \<Turnstile> xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` y # f \<Turnstile> xs)

goal (2 subgoals):
 1. f ` x \<sim> f ` y
 2. f ` x \<notin> set (f ` y # f \<Turnstile> xs)
[PROOF STEP]
from CCons(2)
[PROOF STATE]
proof (chain)
picking this:
pmaxsimpchain (x # y # xs)
[PROOF STEP]
show "f`x \<sim> f`y"
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain (x # y # xs)

goal (1 subgoal):
 1. f ` x \<sim> f ` y
[PROOF STEP]
using pmaxsimpchain_def iso_adj_map
[PROOF STATE]
proof (prove)
using this:
pmaxsimpchain (x # y # xs)
pmaxsimpchain ?xs \<equiv> Ball (set ?xs) maxsimp \<and> padjacentchain ?xs
\<lbrakk>maxsimp ?x; maxsimp ?y; ?x \<sim> ?y; ?x \<noteq> ?y\<rbrakk> \<Longrightarrow> f ` ?x \<sim> f ` ?y

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

goal (1 subgoal):
 1. f ` x \<notin> set (f ` y # f \<Turnstile> xs)
[PROOF STEP]
from inj CCons(2)
[PROOF STATE]
proof (chain)
picking this:
inj_on f (\<Union> X)
pmaxsimpchain (x # y # xs)
[PROOF STEP]
have "distinct (f\<Turnstile>(x#y#xs))"
[PROOF STATE]
proof (prove)
using this:
inj_on f (\<Union> X)
pmaxsimpchain (x # y # xs)

goal (1 subgoal):
 1. distinct (f \<Turnstile> (x # y # xs))
[PROOF STEP]
using     maxsimpD_simplex inj_on_distinct_setlistmapim
[PROOF STATE]
proof (prove)
using this:
inj_on f (\<Union> X)
pmaxsimpchain (x # y # xs)
maxsimp ?x \<Longrightarrow> ?x \<in> X
\<lbrakk>inj_on ?f ?A; \<forall>X\<in>set ?Xs. X \<subseteq> ?A; distinct ?Xs\<rbrakk> \<Longrightarrow> distinct (?f \<Turnstile> ?Xs)

goal (1 subgoal):
 1. distinct (f \<Turnstile> (x # y # xs))
[PROOF STEP]
unfolding pmaxsimpchain_def
[PROOF STATE]
proof (prove)
using this:
inj_on f (\<Union> X)
Ball (set (x # y # xs)) maxsimp \<and> padjacentchain (x # y # xs)
maxsimp ?x \<Longrightarrow> ?x \<in> X
\<lbrakk>inj_on ?f ?A; \<forall>X\<in>set ?Xs. X \<subseteq> ?A; distinct ?Xs\<rbrakk> \<Longrightarrow> distinct (?f \<Turnstile> ?Xs)

goal (1 subgoal):
 1. distinct (f \<Turnstile> (x # y # xs))
[PROOF STEP]
by        blast
[PROOF STATE]
proof (state)
this:
distinct (f \<Turnstile> (x # y # xs))

goal (1 subgoal):
 1. f ` x \<notin> set (f ` y # f \<Turnstile> xs)
[PROOF STEP]
thus "f`x \<notin> set (f`y # f\<Turnstile>xs)"
[PROOF STATE]
proof (prove)
using this:
distinct (f \<Turnstile> (x # y # xs))

goal (1 subgoal):
 1. f ` x \<notin> set (f ` y # f \<Turnstile> xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
f ` x \<notin> set (f ` y # f \<Turnstile> xs)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` x # f ` y # f \<Turnstile> xs)

goal (1 subgoal):
 1. \<And>x y xs. \<lbrakk>pmaxsimpchain (y # xs) \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (y # xs)); pmaxsimpchain (x # y # xs)\<rbrakk> \<Longrightarrow> SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f ` x # f ` y # f \<Turnstile> xs)

goal (1 subgoal):
 1. SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
SimplicialComplex.pmaxsimpchain (f \<turnstile> X) (f \<Turnstile> (x # y # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poset_is_SimplicialComplex:
  assumes "\<forall>x\<in>P. simplex_like (P.\<^bold>\<le>x)"
  shows   "SimplicialComplex (PosetComplex P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SimplicialComplex (PosetComplex P)
[PROOF STEP]
proof (rule SimplicialComplex.intro, rule ballI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> PosetComplex P \<Longrightarrow> finite x
 2. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> PosetComplex P \<Longrightarrow> finite x
 2. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
assume "a \<in> PosetComplex P"
[PROOF STATE]
proof (state)
this:
a \<in> PosetComplex P

goal (2 subgoals):
 1. \<And>x. x \<in> PosetComplex P \<Longrightarrow> finite x
 2. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
a \<in> PosetComplex P
[PROOF STEP]
obtain x where "x\<in>P" "a = {y. pseudominimal_in (P.\<^bold>\<le>x) y}"
[PROOF STATE]
proof (prove)
using this:
a \<in> PosetComplex P

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> P; a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding PosetComplex_def
[PROOF STATE]
proof (prove)
using this:
a \<in> (\<Union>x\<in>P. {{y. pseudominimal_in (P .\<^bold>\<le> x) y}})

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> P; a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}

goal (2 subgoals):
 1. \<And>x. x \<in> PosetComplex P \<Longrightarrow> finite x
 2. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>P. simplex_like (P .\<^bold>\<le> x)
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
[PROOF STEP]
show "finite a"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. simplex_like (P .\<^bold>\<le> x)
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}

goal (1 subgoal):
 1. finite a
[PROOF STEP]
using pseudominimal_inD1 simplex_likeD_finite finite_subset[of a "P.\<^bold>\<le>x"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. simplex_like (P .\<^bold>\<le> x)
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
pseudominimal_in ?P ?x \<Longrightarrow> ?x \<in> ?P
simplex_like ?P \<Longrightarrow> finite ?P
\<lbrakk>a \<subseteq> P .\<^bold>\<le> x; finite (P .\<^bold>\<le> x)\<rbrakk> \<Longrightarrow> finite a

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

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
assume ab: "a \<in> PosetComplex P" "b\<subseteq>a"
[PROOF STATE]
proof (state)
this:
a \<in> PosetComplex P
b \<subseteq> a

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
from ab(1)
[PROOF STATE]
proof (chain)
picking this:
a \<in> PosetComplex P
[PROOF STEP]
obtain x where x: "x\<in>P" "a = {y. pseudominimal_in (P.\<^bold>\<le>x) y}"
[PROOF STATE]
proof (prove)
using this:
a \<in> PosetComplex P

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> P; a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding PosetComplex_def
[PROOF STATE]
proof (prove)
using this:
a \<in> (\<Union>x\<in>P. {{y. pseudominimal_in (P .\<^bold>\<le> x) y}})

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> P; a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
from assms x(1)
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>P. simplex_like (P .\<^bold>\<le> x)
x \<in> P
[PROOF STEP]
obtain f and A::"nat set"
    where fA: "OrderingSetIso less_eq less (\<subseteq>) (\<subset>) (P.\<^bold>\<le>x) f"
              "f`(P.\<^bold>\<le>x) = Pow A"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. simplex_like (P .\<^bold>\<le> x)
x \<in> P

goal (1 subgoal):
 1. (\<And>f A. \<lbrakk>OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f; f ` (P .\<^bold>\<le> x) = Pow A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using simplex_likeD_iso[of "P.\<^bold>\<le>x"]
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>P. simplex_like (P .\<^bold>\<le> x)
x \<in> P
simplex_like (P .\<^bold>\<le> x) \<Longrightarrow> \<exists>f A. OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f \<and> f ` (P .\<^bold>\<le> x) = Pow A

goal (1 subgoal):
 1. (\<And>f A. \<lbrakk>OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f; f ` (P .\<^bold>\<le> x) = Pow A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by    auto
[PROOF STATE]
proof (state)
this:
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f
f ` (P .\<^bold>\<le> x) = Pow A

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
define x' where x': "x' \<equiv> the_inv_into (P.\<^bold>\<le>x) f (\<Union>(f`b))"
[PROOF STATE]
proof (state)
this:
x' \<equiv> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` b))

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
from fA x(2) ab(2) x'
[PROOF STATE]
proof (chain)
picking this:
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f
f ` (P .\<^bold>\<le> x) = Pow A
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
b \<subseteq> a
x' \<equiv> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` b))
[PROOF STEP]
have x'_P: "x'\<in>P"
[PROOF STATE]
proof (prove)
using this:
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f
f ` (P .\<^bold>\<le> x) = Pow A
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
b \<subseteq> a
x' \<equiv> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` b))

goal (1 subgoal):
 1. x' \<in> P
[PROOF STEP]
using collect_pseudominimals_below_in_poset[of P x f]
[PROOF STATE]
proof (prove)
using this:
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f
f ` (P .\<^bold>\<le> x) = Pow A
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
b \<subseteq> a
x' \<equiv> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` b))
\<lbrakk>OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f; f ` (P .\<^bold>\<le> x) = Pow ?A; ?a \<subseteq> {y. pseudominimal_in (P .\<^bold>\<le> x) y}\<rbrakk> \<Longrightarrow> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` ?a)) \<in> P

goal (1 subgoal):
 1. x' \<in> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x' \<in> P

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x' \<in> P

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
from x fA ab(2) x'
[PROOF STATE]
proof (chain)
picking this:
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f
f ` (P .\<^bold>\<le> x) = Pow A
b \<subseteq> a
x' \<equiv> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` b))
[PROOF STEP]
have "b = {y. pseudominimal_in (P.\<^bold>\<le>x') y}"
[PROOF STATE]
proof (prove)
using this:
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f
f ` (P .\<^bold>\<le> x) = Pow A
b \<subseteq> a
x' \<equiv> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` b))

goal (1 subgoal):
 1. b = {y. pseudominimal_in (P .\<^bold>\<le> x') y}
[PROOF STEP]
using collect_pseudominimals_below_in_eq[of x P f]
[PROOF STATE]
proof (prove)
using this:
x \<in> P
a = {y. pseudominimal_in (P .\<^bold>\<le> x) y}
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f
f ` (P .\<^bold>\<le> x) = Pow A
b \<subseteq> a
x' \<equiv> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` b))
\<lbrakk>x \<in> P; OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> x) f; f ` (P .\<^bold>\<le> x) = Pow ?A; ?a \<subseteq> {y. pseudominimal_in (P .\<^bold>\<le> x) y}\<rbrakk> \<Longrightarrow> ?a = {y. pseudominimal_in (P .\<^bold>\<le> the_inv_into (P .\<^bold>\<le> x) f (\<Union> (f ` ?a))) y}

goal (1 subgoal):
 1. b = {y. pseudominimal_in (P .\<^bold>\<le> x') y}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = {y. pseudominimal_in (P .\<^bold>\<le> x') y}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> PosetComplex P; y \<subseteq> x\<rbrakk> \<Longrightarrow> y \<in> PosetComplex P
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x' \<in> P
b = {y. pseudominimal_in (P .\<^bold>\<le> x') y}
[PROOF STEP]
show "b \<in> PosetComplex P"
[PROOF STATE]
proof (prove)
using this:
x' \<in> P
b = {y. pseudominimal_in (P .\<^bold>\<le> x') y}

goal (1 subgoal):
 1. b \<in> PosetComplex P
[PROOF STEP]
unfolding PosetComplex_def
[PROOF STATE]
proof (prove)
using this:
x' \<in> P
b = {y. pseudominimal_in (P .\<^bold>\<le> x') y}

goal (1 subgoal):
 1. b \<in> (\<Union>x\<in>P. {{y. pseudominimal_in (P .\<^bold>\<le> x) y}})
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
b \<in> PosetComplex P

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma poset_to_PosetComplex_OrderingSetMap:
  assumes "\<And>x. x\<in>P \<Longrightarrow> simplex_like (P.\<^bold>\<le>x)"
  shows   "OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P (poset_simplex_map P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P (poset_simplex_map P)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; a \<^bold>\<le> b\<rbrakk> \<Longrightarrow> poset_simplex_map P a \<subseteq> poset_simplex_map P b
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)
[PROOF STEP]
show  "\<And>a b. \<lbrakk> a\<in>P; b\<in>P; a\<^bold>\<le>b \<rbrakk> \<Longrightarrow>
            poset_simplex_map P a \<subseteq> poset_simplex_map P b"
[PROOF STATE]
proof (prove)
using this:
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; a \<^bold>\<le> b\<rbrakk> \<Longrightarrow> poset_simplex_map P a \<subseteq> poset_simplex_map P b
[PROOF STEP]
using     simplex_like_has_bottom pseudominimal_in_below_in
[PROOF STATE]
proof (prove)
using this:
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)
simplex_like ?P \<Longrightarrow> has_bottom ?P
\<lbrakk>has_bottom (?P .\<^bold>\<le> ?y); ?x \<in> ?P; ?x \<^bold>\<le> ?y; pseudominimal_in (?P .\<^bold>\<le> ?x) ?w\<rbrakk> \<Longrightarrow> pseudominimal_in (?P .\<^bold>\<le> ?y) ?w

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; a \<^bold>\<le> b\<rbrakk> \<Longrightarrow> poset_simplex_map P a \<subseteq> poset_simplex_map P b
[PROOF STEP]
unfolding poset_simplex_map_def
[PROOF STATE]
proof (prove)
using this:
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)
simplex_like ?P \<Longrightarrow> has_bottom ?P
\<lbrakk>has_bottom (?P .\<^bold>\<le> ?y); ?x \<in> ?P; ?x \<^bold>\<le> ?y; pseudominimal_in (?P .\<^bold>\<le> ?x) ?w\<rbrakk> \<Longrightarrow> pseudominimal_in (?P .\<^bold>\<le> ?y) ?w

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; a \<^bold>\<le> b\<rbrakk> \<Longrightarrow> Collect (pseudominimal_in (P .\<^bold>\<le> a)) \<subseteq> Collect (pseudominimal_in (P .\<^bold>\<le> b))
[PROOF STEP]
by        fast
[PROOF STATE]
proof (state)
this:
\<lbrakk>?a \<in> P; ?b \<in> P; ?a \<^bold>\<le> ?b\<rbrakk> \<Longrightarrow> poset_simplex_map P ?a \<subseteq> poset_simplex_map P ?b

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smap_onto_PosetComplex: "smap ` P = PosetComplex P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smap ` P = PosetComplex P
[PROOF STEP]
using poset_simplex_map_def PosetComplex_def
[PROOF STATE]
proof (prove)
using this:
poset_simplex_map ?P ?x = {y. pseudominimal_in (?P .\<^bold>\<le> ?x) y}
PosetComplex ?P \<equiv> \<Union>x\<in>?P. {{y. pseudominimal_in (?P .\<^bold>\<le> x) y}}

goal (1 subgoal):
 1. smap ` P = PosetComplex P
[PROOF STEP]
by auto


[STATEMENT]
lemma ordsetmap_smap: "\<lbrakk> a\<in>P; b\<in>P; a\<^bold>\<le>b \<rbrakk> \<Longrightarrow> smap a \<subseteq> smap b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<in> P; b \<in> P; a \<^bold>\<le> b\<rbrakk> \<Longrightarrow> smap a \<subseteq> smap b
[PROOF STEP]
using OrderingSetMap.ordsetmap[
          OF poset_to_PosetComplex_OrderingSetMap, OF below_in_P_simplex_like
        ]
        poset_simplex_map_def
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x. x \<in> P \<Longrightarrow> x \<in> P; ?a \<in> P; ?b \<in> P; ?a \<^bold>\<le> ?b\<rbrakk> \<Longrightarrow> smap ?a \<subseteq> smap ?b
poset_simplex_map ?P ?x = {y. pseudominimal_in (?P .\<^bold>\<le> ?x) y}

goal (1 subgoal):
 1. \<lbrakk>a \<in> P; b \<in> P; a \<^bold>\<le> b\<rbrakk> \<Longrightarrow> smap a \<subseteq> smap b
[PROOF STEP]
by    simp


[STATEMENT]
lemma inj_on_smap: "inj_on smap P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on smap P
[PROOF STEP]
proof (rule inj_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> P; y \<in> P; smap x = smap y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> P; y \<in> P; smap x = smap y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume xy: "x\<in>P" "y\<in>P" "smap x = smap y"
[PROOF STATE]
proof (state)
this:
x \<in> P
y \<in> P
smap x = smap y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> P; y \<in> P; smap x = smap y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
show "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
proof (cases "smap x = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. smap x = {} \<Longrightarrow> x = y
 2. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
smap x = {}

goal (2 subgoals):
 1. smap x = {} \<Longrightarrow> x = y
 2. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
with xy
[PROOF STATE]
proof (chain)
picking this:
x \<in> P
y \<in> P
smap x = smap y
smap x = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in> P
y \<in> P
smap x = smap y
smap x = {}

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using poset_simplex_map_def below_in_P_simplex_like P_has_bottom
            simplex_like_no_pseudominimal_in_below_in_imp_singleton[of x P]
            simplex_like_no_pseudominimal_in_below_in_imp_singleton[of y P]
            below_in_singleton_is_bottom[of P x] below_in_singleton_is_bottom[of P y]
[PROOF STATE]
proof (prove)
using this:
x \<in> P
y \<in> P
smap x = smap y
smap x = {}
poset_simplex_map ?P ?x = {y. pseudominimal_in (?P .\<^bold>\<le> ?x) y}
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)
has_bottom P
\<lbrakk>x \<in> P; simplex_like (P .\<^bold>\<le> x); \<And>z. \<not> pseudominimal_in (P .\<^bold>\<le> x) z\<rbrakk> \<Longrightarrow> P .\<^bold>\<le> x = {x}
\<lbrakk>y \<in> P; simplex_like (P .\<^bold>\<le> y); \<And>z. \<not> pseudominimal_in (P .\<^bold>\<le> y) z\<rbrakk> \<Longrightarrow> P .\<^bold>\<le> y = {y}
\<lbrakk>has_bottom P; x \<in> P; P .\<^bold>\<le> x = {x}\<rbrakk> \<Longrightarrow> x = bottom P
\<lbrakk>has_bottom P; y \<in> P; P .\<^bold>\<le> y = {y}\<rbrakk> \<Longrightarrow> y = bottom P

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

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
smap x \<noteq> {}

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
smap x \<noteq> {}
[PROOF STEP]
obtain z where "z \<in> smap x"
[PROOF STATE]
proof (prove)
using this:
smap x \<noteq> {}

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

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
with xy(3)
[PROOF STATE]
proof (chain)
picking this:
smap x = smap y
z \<in> smap x
[PROOF STEP]
have z1: "z \<in> P.\<^bold>\<le>x" "z \<in> P.\<^bold>\<le>y"
[PROOF STATE]
proof (prove)
using this:
smap x = smap y
z \<in> smap x

goal (1 subgoal):
 1. z \<in> P .\<^bold>\<le> x &&& z \<in> P .\<^bold>\<le> y
[PROOF STEP]
using pseudominimal_inD1 poset_simplex_map_def
[PROOF STATE]
proof (prove)
using this:
smap x = smap y
z \<in> smap x
pseudominimal_in ?P ?x \<Longrightarrow> ?x \<in> ?P
poset_simplex_map ?P ?x = {y. pseudominimal_in (?P .\<^bold>\<le> ?x) y}

goal (1 subgoal):
 1. z \<in> P .\<^bold>\<le> x &&& z \<in> P .\<^bold>\<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> P .\<^bold>\<le> x
z \<in> P .\<^bold>\<le> y

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
hence "lbound_of x y z"
[PROOF STATE]
proof (prove)
using this:
z \<in> P .\<^bold>\<le> x
z \<in> P .\<^bold>\<le> y

goal (1 subgoal):
 1. lbound_of x y z
[PROOF STEP]
by (auto intro: lbound_ofI)
[PROOF STATE]
proof (state)
this:
lbound_of x y z

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
with z1(1)
[PROOF STATE]
proof (chain)
picking this:
z \<in> P .\<^bold>\<le> x
lbound_of x y z
[PROOF STEP]
obtain b where b: "glbound_in_of P x y b"
[PROOF STATE]
proof (prove)
using this:
z \<in> P .\<^bold>\<le> x
lbound_of x y z

goal (1 subgoal):
 1. (\<And>b. glbound_in_of P x y b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using xy(1,2) P_has_glbs
[PROOF STATE]
proof (prove)
using this:
z \<in> P .\<^bold>\<le> x
lbound_of x y z
x \<in> P
y \<in> P
\<lbrakk>?x \<in> P; ?y \<in> P\<rbrakk> \<Longrightarrow> \<exists>b. glbound_in_of P ?x ?y b

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

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
glbound_in_of P x y b

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
have "b \<in> P.\<^bold>\<le>x" "b \<in> P.\<^bold>\<le>y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b \<in> P .\<^bold>\<le> x &&& b \<in> P .\<^bold>\<le> y
[PROOF STEP]
using glbound_in_ofD_in[OF b] glbound_in_of_less_eq1[OF b]
            glbound_in_of_less_eq2[OF b]
[PROOF STATE]
proof (prove)
using this:
b \<in> P
b \<^bold>\<le> x
b \<^bold>\<le> y

goal (1 subgoal):
 1. b \<in> P .\<^bold>\<le> x &&& b \<in> P .\<^bold>\<le> y
[PROOF STEP]
by    auto
[PROOF STATE]
proof (state)
this:
b \<in> P .\<^bold>\<le> x
b \<in> P .\<^bold>\<le> y

goal (1 subgoal):
 1. smap x \<noteq> {} \<Longrightarrow> x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
glbound_in_of P x y b
b \<in> P .\<^bold>\<le> x
b \<in> P .\<^bold>\<le> y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
glbound_in_of P x y b
b \<in> P .\<^bold>\<le> x
b \<in> P .\<^bold>\<le> y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
using     xy below_in_P_simplex_like
                pseudominimal_in_below_in_less_eq_glbound[of P x _ y b]
                simplex_like_below_in_above_pseudominimal_is_top[of x P]
                simplex_like_below_in_above_pseudominimal_is_top[of y P]
[PROOF STATE]
proof (prove)
using this:
glbound_in_of P x y b
b \<in> P .\<^bold>\<le> x
b \<in> P .\<^bold>\<le> y
x \<in> P
y \<in> P
smap x = smap y
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)
\<lbrakk>pseudominimal_in (P .\<^bold>\<le> x) ?w; pseudominimal_in (P .\<^bold>\<le> y) ?w; glbound_in_of P x y b\<rbrakk> \<Longrightarrow> ?w \<^bold>\<le> b
\<lbrakk>x \<in> P; simplex_like (P .\<^bold>\<le> x); ?t \<in> P .\<^bold>\<le> x; \<And>y. pseudominimal_in (P .\<^bold>\<le> x) y \<Longrightarrow> y \<^bold>\<le> ?t\<rbrakk> \<Longrightarrow> ?t = x
\<lbrakk>y \<in> P; simplex_like (P .\<^bold>\<le> y); ?t \<in> P .\<^bold>\<le> y; \<And>ya. pseudominimal_in (P .\<^bold>\<le> y) ya \<Longrightarrow> ya \<^bold>\<le> ?t\<rbrakk> \<Longrightarrow> ?t = y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
unfolding poset_simplex_map_def
[PROOF STATE]
proof (prove)
using this:
glbound_in_of P x y b
b \<in> P .\<^bold>\<le> x
b \<in> P .\<^bold>\<le> y
x \<in> P
y \<in> P
Collect (pseudominimal_in (P .\<^bold>\<le> x)) = Collect (pseudominimal_in (P .\<^bold>\<le> y))
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)
\<lbrakk>pseudominimal_in (P .\<^bold>\<le> x) ?w; pseudominimal_in (P .\<^bold>\<le> y) ?w; glbound_in_of P x y b\<rbrakk> \<Longrightarrow> ?w \<^bold>\<le> b
\<lbrakk>x \<in> P; simplex_like (P .\<^bold>\<le> x); ?t \<in> P .\<^bold>\<le> x; \<And>y. pseudominimal_in (P .\<^bold>\<le> x) y \<Longrightarrow> y \<^bold>\<le> ?t\<rbrakk> \<Longrightarrow> ?t = x
\<lbrakk>y \<in> P; simplex_like (P .\<^bold>\<le> y); ?t \<in> P .\<^bold>\<le> y; \<And>ya. pseudominimal_in (P .\<^bold>\<le> y) ya \<Longrightarrow> ya \<^bold>\<le> ?t\<rbrakk> \<Longrightarrow> ?t = y

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma OrderingSetIso_smap:
  "OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P smap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P smap
[PROOF STEP]
proof (rule OrderingSetMap.isoI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P smap
 2. inj_on smap P
 3. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; smap a \<subseteq> smap b\<rbrakk> \<Longrightarrow> a \<^bold>\<le> b
[PROOF STEP]
show "OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P smap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P smap
[PROOF STEP]
using poset_simplex_map_def below_in_P_simplex_like
          poset_to_PosetComplex_OrderingSetMap
[PROOF STATE]
proof (prove)
using this:
poset_simplex_map ?P ?x = {y. pseudominimal_in (?P .\<^bold>\<le> ?x) y}
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)
(\<And>x. x \<in> ?P \<Longrightarrow> simplex_like (?P .\<^bold>\<le> x)) \<Longrightarrow> OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) ?P (poset_simplex_map ?P)

goal (1 subgoal):
 1. OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P smap
[PROOF STEP]
by    simp
[PROOF STATE]
proof (state)
this:
OrderingSetMap (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) P smap

goal (2 subgoals):
 1. inj_on smap P
 2. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; smap a \<subseteq> smap b\<rbrakk> \<Longrightarrow> a \<^bold>\<le> b
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on smap P
 2. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; smap a \<subseteq> smap b\<rbrakk> \<Longrightarrow> a \<^bold>\<le> b
[PROOF STEP]
fix x y
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inj_on smap P
 2. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; smap a \<subseteq> smap b\<rbrakk> \<Longrightarrow> a \<^bold>\<le> b
[PROOF STEP]
assume xy: "x\<in>P" "y\<in>P" "smap x \<subseteq> smap y"
[PROOF STATE]
proof (state)
this:
x \<in> P
y \<in> P
smap x \<subseteq> smap y

goal (2 subgoals):
 1. inj_on smap P
 2. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; smap a \<subseteq> smap b\<rbrakk> \<Longrightarrow> a \<^bold>\<le> b
[PROOF STEP]
from xy(2)
[PROOF STATE]
proof (chain)
picking this:
y \<in> P
[PROOF STEP]
have "simplex_like (P.\<^bold>\<le>y)"
[PROOF STATE]
proof (prove)
using this:
y \<in> P

goal (1 subgoal):
 1. simplex_like (P .\<^bold>\<le> y)
[PROOF STEP]
using below_in_P_simplex_like
[PROOF STATE]
proof (prove)
using this:
y \<in> P
?x \<in> P \<Longrightarrow> simplex_like (P .\<^bold>\<le> ?x)

goal (1 subgoal):
 1. simplex_like (P .\<^bold>\<le> y)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
simplex_like (P .\<^bold>\<le> y)

goal (2 subgoals):
 1. inj_on smap P
 2. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; smap a \<subseteq> smap b\<rbrakk> \<Longrightarrow> a \<^bold>\<le> b
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
simplex_like (P .\<^bold>\<le> y)
[PROOF STEP]
obtain g and A::"nat set"
    where "OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P.\<^bold>\<le>y) g"
          "g`(P.\<^bold>\<le>y) = Pow A"
[PROOF STATE]
proof (prove)
using this:
simplex_like (P .\<^bold>\<le> y)

goal (1 subgoal):
 1. (\<And>g A. \<lbrakk>OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g; g ` (P .\<^bold>\<le> y) = Pow A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using simplex_likeD_iso[of "P.\<^bold>\<le>y"]
[PROOF STATE]
proof (prove)
using this:
simplex_like (P .\<^bold>\<le> y)
simplex_like (P .\<^bold>\<le> y) \<Longrightarrow> \<exists>f A. OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) f \<and> f ` (P .\<^bold>\<le> y) = Pow A

goal (1 subgoal):
 1. (\<And>g A. \<lbrakk>OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g; g ` (P .\<^bold>\<le> y) = Pow A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by    auto
[PROOF STATE]
proof (state)
this:
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g
g ` (P .\<^bold>\<le> y) = Pow A

goal (2 subgoals):
 1. inj_on smap P
 2. \<And>a b. \<lbrakk>a \<in> P; b \<in> P; smap a \<subseteq> smap b\<rbrakk> \<Longrightarrow> a \<^bold>\<le> b
[PROOF STEP]
with xy
[PROOF STATE]
proof (chain)
picking this:
x \<in> P
y \<in> P
smap x \<subseteq> smap y
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g
g ` (P .\<^bold>\<le> y) = Pow A
[PROOF STEP]
show "x\<^bold>\<le>y"
[PROOF STATE]
proof (prove)
using this:
x \<in> P
y \<in> P
smap x \<subseteq> smap y
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g
g ` (P .\<^bold>\<le> y) = Pow A

goal (1 subgoal):
 1. x \<^bold>\<le> y
[PROOF STEP]
using poset_simplex_map_def collect_pseudominimals_below_in_eq[of y P g]
          collect_pseudominimals_below_in_poset[of P y g]
          inj_onD[OF inj_on_smap, of "the_inv_into (P.\<^bold>\<le>y) g (\<Union>(g ` smap x))" x]
          collect_pseudominimals_below_in_less_eq_top[of P y g A "smap x"]
[PROOF STATE]
proof (prove)
using this:
x \<in> P
y \<in> P
smap x \<subseteq> smap y
OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g
g ` (P .\<^bold>\<le> y) = Pow A
poset_simplex_map ?P ?x = {y. pseudominimal_in (?P .\<^bold>\<le> ?x) y}
\<lbrakk>y \<in> P; OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g; g ` (P .\<^bold>\<le> y) = Pow ?A; ?a \<subseteq> {ya. pseudominimal_in (P .\<^bold>\<le> y) ya}\<rbrakk> \<Longrightarrow> ?a = {ya. pseudominimal_in (P .\<^bold>\<le> the_inv_into (P .\<^bold>\<le> y) g (\<Union> (g ` ?a))) ya}
\<lbrakk>OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g; g ` (P .\<^bold>\<le> y) = Pow ?A; ?a \<subseteq> {ya. pseudominimal_in (P .\<^bold>\<le> y) ya}\<rbrakk> \<Longrightarrow> the_inv_into (P .\<^bold>\<le> y) g (\<Union> (g ` ?a)) \<in> P
\<lbrakk>smap (the_inv_into (P .\<^bold>\<le> y) g (\<Union> (g ` smap x))) = smap x; the_inv_into (P .\<^bold>\<le> y) g (\<Union> (g ` smap x)) \<in> P; x \<in> P\<rbrakk> \<Longrightarrow> the_inv_into (P .\<^bold>\<le> y) g (\<Union> (g ` smap x)) = x
\<lbrakk>OrderingSetIso (\<^bold>\<le>) (\<^bold><) (\<subseteq>) (\<subset>) (P .\<^bold>\<le> y) g; g ` (P .\<^bold>\<le> y) = Pow A; smap x \<subseteq> {ya. pseudominimal_in (P .\<^bold>\<le> y) ya}\<rbrakk> \<Longrightarrow> the_inv_into (P .\<^bold>\<le> y) g (\<Union> (g ` smap x)) \<^bold>\<le> y

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

goal (1 subgoal):
 1. inj_on smap P
[PROOF STEP]
qed (rule inj_on_smap)


[STATEMENT]
lemma concurrentI [intro!]: "\<not> (s1 \<prec> s2) \<Longrightarrow> \<not> (s2 \<prec> s1) \<Longrightarrow> s1 \<parallel> s2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> s1 \<prec> s2; \<not> s2 \<prec> s1\<rbrakk> \<Longrightarrow> s1 \<parallel> s2
[PROOF STEP]
by (auto simp: concurrent_def)


[STATEMENT]
lemma concurrentD1 [dest]: "s1 \<parallel> s2 \<Longrightarrow> \<not> (s1 \<prec> s2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 \<parallel> s2 \<Longrightarrow> \<not> s1 \<prec> s2
[PROOF STEP]
by (auto simp: concurrent_def)


[STATEMENT]
lemma concurrentD2 [dest]: "s1 \<parallel> s2 \<Longrightarrow> \<not> (s2 \<prec> s1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s1 \<parallel> s2 \<Longrightarrow> \<not> s2 \<prec> s1
[PROOF STEP]
by (auto simp: concurrent_def)


[STATEMENT]
lemma concurrent_refl [intro!, simp]: "s \<parallel> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<parallel> s
[PROOF STEP]
by (auto simp: concurrent_def)


[STATEMENT]
lemma concurrent_comm: "s1 \<parallel> s2 \<longleftrightarrow> s2 \<parallel> s1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (s1 \<parallel> s2) = (s2 \<parallel> s1)
[PROOF STEP]
by (auto simp: concurrent_def)


[STATEMENT]
lemma concurrent_set_empty [simp, intro!]:
  "concurrent_set x []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_set x []
[PROOF STEP]
by (auto simp: concurrent_set_def)


[STATEMENT]
lemma concurrent_set_ConsE [elim!]:
  assumes "concurrent_set a (x#xs)"
      and "concurrent_set a xs \<Longrightarrow> concurrent x a \<Longrightarrow> G"
    shows "G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
concurrent_set a (x # xs)
\<lbrakk>concurrent_set a xs; x \<parallel> a\<rbrakk> \<Longrightarrow> G

goal (1 subgoal):
 1. G
[PROOF STEP]
by (auto simp: concurrent_set_def)


[STATEMENT]
lemma concurrent_set_ConsI [intro!]:
  "concurrent_set a xs \<Longrightarrow> concurrent a x \<Longrightarrow> concurrent_set a (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>concurrent_set a xs; a \<parallel> x\<rbrakk> \<Longrightarrow> concurrent_set a (x # xs)
[PROOF STEP]
by (auto simp: concurrent_set_def)


[STATEMENT]
lemma concurrent_set_appendI [intro!]:
  "concurrent_set a xs \<Longrightarrow> concurrent_set a ys \<Longrightarrow> concurrent_set a (xs@ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>concurrent_set a xs; concurrent_set a ys\<rbrakk> \<Longrightarrow> concurrent_set a (xs @ ys)
[PROOF STEP]
by (auto simp: concurrent_set_def)


[STATEMENT]
lemma concurrent_set_Cons_Snoc [simp]:
  "concurrent_set a (xs@[x]) = concurrent_set a (x#xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_set a (xs @ [x]) = concurrent_set a (x # xs)
[PROOF STEP]
by (auto simp: concurrent_set_def)


[STATEMENT]
lemma "(x \<prec> y \<or> concurrent x y) = (\<not> y \<prec> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<prec> y \<or> x \<parallel> y) = (\<not> y \<prec> x)
[PROOF STEP]
using less_asym
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<prec> ?y; \<not> ?P \<Longrightarrow> ?y \<prec> ?x\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (x \<prec> y \<or> x \<parallel> y) = (\<not> y \<prec> x)
[PROOF STEP]
by blast


[STATEMENT]
lemma consistentI [intro!]:
  assumes "hb_consistent (xs @ ys)"
  and     "\<forall>x \<in> set (xs @ ys). \<not> z \<prec> x"
  shows   "hb_consistent (xs @ ys @ [z])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent (xs @ ys @ [z])
[PROOF STEP]
using assms hb_consistent.intros append_assoc
[PROOF STATE]
proof (prove)
using this:
hb_consistent (xs @ ys)
\<forall>x\<in>set (xs @ ys). \<not> z \<prec> x
hb_consistent []
\<lbrakk>hb_consistent ?xs; \<forall>x\<in>set ?xs. \<not> ?y \<prec> x\<rbrakk> \<Longrightarrow> hb_consistent (?xs @ [?y])
(?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs

goal (1 subgoal):
 1. hb_consistent (xs @ ys @ [z])
[PROOF STEP]
by metis


[STATEMENT]
lemma hb_consistent_append_D1 [dest]:
  assumes "hb_consistent (xs @ ys)"
  shows   "hb_consistent xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent (xs @ ys)

goal (1 subgoal):
 1. hb_consistent xs
[PROOF STEP]
by(induction ys arbitrary: xs rule: List.rev_induct) auto


[STATEMENT]
lemma hb_consistent_append_D2 [dest]:
  assumes "hb_consistent (xs @ ys)"
  shows   "hb_consistent ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent (xs @ ys)

goal (1 subgoal):
 1. hb_consistent ys
[PROOF STEP]
by(induction ys arbitrary: xs rule: List.rev_induct) fastforce+


[STATEMENT]
lemma hb_consistent_append_elim_ConsD [elim]:
  assumes "hb_consistent (y#ys)"
  shows   "hb_consistent ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent ys
[PROOF STEP]
using assms hb_consistent_append_D2
[PROOF STATE]
proof (prove)
using this:
hb_consistent (y # ys)
hb_consistent (?xs @ ?ys) \<Longrightarrow> hb_consistent ?ys

goal (1 subgoal):
 1. hb_consistent ys
[PROOF STEP]
by(metis append_Cons append_Nil)


[STATEMENT]
lemma hb_consistent_remove1 [intro]:
  assumes "hb_consistent xs"
  shows   "hb_consistent (remove1 x xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent (remove1 x xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent xs

goal (1 subgoal):
 1. hb_consistent (remove1 x xs)
[PROOF STEP]
by (induction rule: hb_consistent.induct) (auto simp: remove1_append)


[STATEMENT]
lemma hb_consistent_singleton [intro!]:
  shows "hb_consistent [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent [x]
[PROOF STEP]
using hb_consistent.intros
[PROOF STATE]
proof (prove)
using this:
hb_consistent []
\<lbrakk>hb_consistent ?xs; \<forall>x\<in>set ?xs. \<not> ?y \<prec> x\<rbrakk> \<Longrightarrow> hb_consistent (?xs @ [?y])

goal (1 subgoal):
 1. hb_consistent [x]
[PROOF STEP]
by fastforce


[STATEMENT]
lemma hb_consistent_prefix_suffix_exists:
  assumes "hb_consistent ys"
          "hb_consistent (xs @ [x])"
          "{x} \<union> set xs = set ys"
          "distinct (x#xs)"
          "distinct ys"
  shows "\<exists>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent ys
hb_consistent (xs @ [x])
{x} \<union> set xs = set ys
distinct (x # xs)
distinct ys

goal (1 subgoal):
 1. \<exists>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
proof (induction arbitrary: xs rule: hb_consistent.induct, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
fix xs y ys
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
assume IH: "(\<And>xs. hb_consistent (xs @ [x]) \<Longrightarrow>
               {x} \<union> set xs = set ys \<Longrightarrow>
               distinct (x # xs) \<Longrightarrow> distinct ys \<Longrightarrow>
             \<exists>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix) "
[PROOF STATE]
proof (state)
this:
\<lbrakk>hb_consistent (?xs1 @ [x]); {x} \<union> set ?xs1 = set ys; distinct (x # ?xs1); distinct ys\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
assume assms: "hb_consistent ys" "\<forall>x\<in>set ys. \<not> hb y x"
                "hb_consistent (xs @ [x])"
                "{x} \<union> set xs = set (ys @ [y])"
                "distinct (x # xs)" "distinct (ys @ [y])"
[PROOF STATE]
proof (state)
this:
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
hence "x = y \<or> y \<in> set xs"
[PROOF STATE]
proof (prove)
using this:
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])

goal (1 subgoal):
 1. x = y \<or> y \<in> set xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])

goal (1 subgoal):
 1. x = y \<or> y \<in> set xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = y \<or> y \<in> set xs

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = y \<or> y \<in> set xs

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x = y \<or> y \<in> set xs

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
assume "x = y"
[PROOF STATE]
proof (state)
this:
x = y

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
hence "\<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix"
[PROOF STATE]
proof (prove)
using this:
x = y

goal (1 subgoal):
 1. \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
x = y \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
assume y_in_xs: "y \<in> set xs"
[PROOF STATE]
proof (state)
this:
y \<in> set xs

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
hence "{x} \<union> (set xs - {y}) = set ys"
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs

goal (1 subgoal):
 1. {x} \<union> (set xs - {y}) = set ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
y \<in> set xs
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])

goal (1 subgoal):
 1. {x} \<union> (set xs - {y}) = set ys
[PROOF STEP]
by (auto intro: set_equality_technical)
[PROOF STATE]
proof (state)
this:
{x} \<union> (set xs - {y}) = set ys

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
hence remove_y_in_xs: "{x} \<union> set (remove1 y xs) = set ys"
[PROOF STATE]
proof (prove)
using this:
{x} \<union> (set xs - {y}) = set ys

goal (1 subgoal):
 1. {x} \<union> set (remove1 y xs) = set ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{x} \<union> (set xs - {y}) = set ys
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])

goal (1 subgoal):
 1. {x} \<union> set (remove1 y xs) = set ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x} \<union> set (remove1 y xs) = set ys

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{x} \<union> set (remove1 y xs) = set ys

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
have "hb_consistent ((remove1 y xs) @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent (remove1 y xs @ [x])
[PROOF STEP]
using assms hb_consistent_remove1
[PROOF STATE]
proof (prove)
using this:
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])
hb_consistent ?xs \<Longrightarrow> hb_consistent (remove1 ?x ?xs)

goal (1 subgoal):
 1. hb_consistent (remove1 y xs @ [x])
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
hb_consistent (remove1 y xs @ [x])

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
hb_consistent (remove1 y xs @ [x])

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
have "distinct (x # (remove1 y xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (x # remove1 y xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])

goal (1 subgoal):
 1. distinct (x # remove1 y xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct (x # remove1 y xs)

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
distinct (x # remove1 y xs)

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
have "distinct ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct ys
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])

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

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{x} \<union> set (remove1 y xs) = set ys
hb_consistent (remove1 y xs @ [x])
distinct (x # remove1 y xs)
distinct ys
[PROOF STEP]
obtain prefix suffix where ys_split: "ys = prefix @ x # suffix \<and> concurrent_set x suffix"
[PROOF STATE]
proof (prove)
using this:
{x} \<union> set (remove1 y xs) = set ys
hb_consistent (remove1 y xs @ [x])
distinct (x # remove1 y xs)
distinct ys

goal (1 subgoal):
 1. (\<And>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
{x} \<union> set (remove1 y xs) = set ys
hb_consistent (remove1 y xs @ [x])
distinct (x # remove1 y xs)
distinct ys
\<lbrakk>hb_consistent (?xs1 @ [x]); {x} \<union> set ?xs1 = set ys; distinct (x # ?xs1); distinct ys\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. (\<And>prefix suffix. ys = prefix @ x # suffix \<and> concurrent_set x suffix \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
have "concurrent x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<parallel> y
[PROOF STEP]
using assms y_in_xs remove_y_in_xs concurrent_def
[PROOF STATE]
proof (prove)
using this:
hb_consistent ys
\<forall>x\<in>set ys. \<not> y \<prec> x
hb_consistent (xs @ [x])
{x} \<union> set xs = set (ys @ [y])
distinct (x # xs)
distinct (ys @ [y])
y \<in> set xs
{x} \<union> set (remove1 y xs) = set ys
?s1.0 \<parallel> ?s2.0 \<equiv> \<not> ?s1.0 \<prec> ?s2.0 \<and> \<not> ?s2.0 \<prec> ?s1.0

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

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
hence "concurrent_set x (suffix@[y])"
[PROOF STATE]
proof (prove)
using this:
x \<parallel> y

goal (1 subgoal):
 1. concurrent_set x (suffix @ [y])
[PROOF STEP]
using ys_split
[PROOF STATE]
proof (prove)
using this:
x \<parallel> y
ys = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. concurrent_set x (suffix @ [y])
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
concurrent_set x (suffix @ [y])

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
concurrent_set x (suffix @ [y])

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
concurrent_set x (suffix @ [y])
[PROOF STEP]
have "\<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix"
[PROOF STATE]
proof (prove)
using this:
ys = prefix @ x # suffix \<and> concurrent_set x suffix
concurrent_set x (suffix @ [y])

goal (1 subgoal):
 1. \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
\<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
y \<in> set xs \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<And>xs y xsa. \<lbrakk>hb_consistent xs; \<And>xsa. \<lbrakk>hb_consistent (xsa @ [x]); {x} \<union> set xsa = set xs; distinct (x # xsa); distinct xs\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs = prefix @ x # suffix \<and> concurrent_set x suffix; \<forall>x\<in>set xs. \<not> y \<prec> x; hb_consistent (xsa @ [x]); {x} \<union> set xsa = set (xs @ [y]); distinct (x # xsa); distinct (xs @ [y])\<rbrakk> \<Longrightarrow> \<exists>prefix suffix. xs @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = y \<or> y \<in> set xs
x = y \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
y \<in> set xs \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
show "\<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix"
[PROOF STATE]
proof (prove)
using this:
x = y \<or> y \<in> set xs
x = y \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
y \<in> set xs \<Longrightarrow> \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal (1 subgoal):
 1. \<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>prefix suffix. ys @ [y] = prefix @ x # suffix \<and> concurrent_set x suffix

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma hb_consistent_append [intro!]:
  assumes "hb_consistent suffix"
          "hb_consistent prefix"
          "\<And>s p. s \<in> set suffix \<Longrightarrow> p \<in> set prefix \<Longrightarrow> \<not> s \<prec> p"
  shows "hb_consistent (prefix @ suffix)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hb_consistent (prefix @ suffix)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent suffix
hb_consistent prefix
\<lbrakk>?s1 \<in> set suffix; ?p1 \<in> set prefix\<rbrakk> \<Longrightarrow> \<not> ?s1 \<prec> ?p1

goal (1 subgoal):
 1. hb_consistent (prefix @ suffix)
[PROOF STEP]
by (induction rule: hb_consistent.induct) force+


[STATEMENT]
lemma hb_consistent_append_porder:
  assumes "hb_consistent (xs @ ys)"
          "x \<in> set xs"
          "y \<in> set ys"
  shows   "\<not> y \<prec> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> y \<prec> x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
hb_consistent (xs @ ys)
x \<in> set xs
y \<in> set ys

goal (1 subgoal):
 1. \<not> y \<prec> x
[PROOF STEP]
by (induction ys arbitrary: xs rule: rev_induct) force+


[STATEMENT]
lemma apply_operations_empty [simp]: "apply_operations [] s = Some s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations [] s = Some s
[PROOF STEP]
by(auto simp: apply_operations_def)


[STATEMENT]
lemma apply_operations_Snoc [simp]:
  "apply_operations (xs@[x]) = (apply_operations xs) \<rhd> \<langle>x\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations (xs @ [x]) = apply_operations xs \<rhd> \<langle>x\<rangle>
[PROOF STEP]
by(auto simp add: apply_operations_def kleisli_def)


[STATEMENT]
lemma concurrent_ops_commute_empty [intro!]: "concurrent_ops_commute []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_ops_commute []
[PROOF STEP]
by(auto simp: concurrent_ops_commute_def)


[STATEMENT]
lemma concurrent_ops_commute_singleton [intro!]: "concurrent_ops_commute [x]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_ops_commute [x]
[PROOF STEP]
by(auto simp: concurrent_ops_commute_def)


[STATEMENT]
lemma concurrent_ops_commute_appendD [dest]:
  assumes "concurrent_ops_commute (xs@ys)"
    shows "concurrent_ops_commute xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_ops_commute xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
concurrent_ops_commute (xs @ ys)

goal (1 subgoal):
 1. concurrent_ops_commute xs
[PROOF STEP]
by (auto simp: concurrent_ops_commute_def)


[STATEMENT]
lemma concurrent_ops_commute_rearrange:
  "concurrent_ops_commute (xs@x#ys) = concurrent_ops_commute (xs@ys@[x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_ops_commute (xs @ x # ys) = concurrent_ops_commute (xs @ ys @ [x])
[PROOF STEP]
by (clarsimp simp: concurrent_ops_commute_def)


[STATEMENT]
lemma concurrent_ops_commute_concurrent_set:
  assumes "concurrent_ops_commute (prefix@suffix@[x])"
          "concurrent_set x suffix"
          "distinct (prefix @ x # suffix)"
  shows   "apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
concurrent_ops_commute (prefix @ suffix @ [x])
concurrent_set x suffix
distinct (prefix @ x # suffix)

goal (1 subgoal):
 1. apply_operations (prefix @ suffix @ [x]) = apply_operations (prefix @ x # suffix)
[PROOF STEP]
proof(induction suffix arbitrary: rule: rev_induct, force)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
fix a xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
assume IH: "concurrent_ops_commute (prefix @ xs @ [x]) \<Longrightarrow>
              concurrent_set x xs \<Longrightarrow> distinct (prefix @ x # xs) \<Longrightarrow>
              apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs)"
[PROOF STATE]
proof (state)
this:
\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs)

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
assume assms: "concurrent_ops_commute (prefix @ (xs @ [a]) @ [x])"
                "concurrent_set x (xs @ [a])" "distinct (prefix @ x # xs @ [a])"
[PROOF STATE]
proof (state)
this:
concurrent_ops_commute (prefix @ (xs @ [a]) @ [x])
concurrent_set x (xs @ [a])
distinct (prefix @ x # xs @ [a])

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
hence ac_comm: "\<langle>a\<rangle> \<rhd> \<langle>x\<rangle> = \<langle>x\<rangle> \<rhd> \<langle>a\<rangle>"
[PROOF STATE]
proof (prove)
using this:
concurrent_ops_commute (prefix @ (xs @ [a]) @ [x])
concurrent_set x (xs @ [a])
distinct (prefix @ x # xs @ [a])

goal (1 subgoal):
 1. \<langle>a\<rangle> \<rhd> \<langle>x\<rangle> = \<langle>x\<rangle> \<rhd> \<langle>a\<rangle>
[PROOF STEP]
by (clarsimp simp: concurrent_ops_commute_def) blast
[PROOF STATE]
proof (state)
this:
\<langle>a\<rangle> \<rhd> \<langle>x\<rangle> = \<langle>x\<rangle> \<rhd> \<langle>a\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
have copc: "concurrent_ops_commute (prefix @ xs @ [x])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concurrent_ops_commute (prefix @ xs @ [x])
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
concurrent_ops_commute (prefix @ (xs @ [a]) @ [x])
concurrent_set x (xs @ [a])
distinct (prefix @ x # xs @ [a])

goal (1 subgoal):
 1. concurrent_ops_commute (prefix @ xs @ [x])
[PROOF STEP]
by (clarsimp simp: concurrent_ops_commute_def) blast
[PROOF STATE]
proof (state)
this:
concurrent_ops_commute (prefix @ xs @ [x])

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
have "apply_operations ((prefix @ x # xs) @ [a]) = (apply_operations (prefix @ x # xs)) \<rhd> \<langle>a\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations ((prefix @ x # xs) @ [a]) = apply_operations (prefix @ x # xs) \<rhd> \<langle>a\<rangle>
[PROOF STEP]
by (simp del: append_assoc)
[PROOF STATE]
proof (state)
this:
apply_operations ((prefix @ x # xs) @ [a]) = apply_operations (prefix @ x # xs) \<rhd> \<langle>a\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
apply_operations ((prefix @ x # xs) @ [a]) = apply_operations (prefix @ x # xs) \<rhd> \<langle>a\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
have "... = (apply_operations (prefix @ xs @ [x])) \<rhd> \<langle>a\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations (prefix @ x # xs) \<rhd> \<langle>a\<rangle> = apply_operations (prefix @ xs @ [x]) \<rhd> \<langle>a\<rangle>
[PROOF STEP]
using IH assms copc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs)
concurrent_ops_commute (prefix @ (xs @ [a]) @ [x])
concurrent_set x (xs @ [a])
distinct (prefix @ x # xs @ [a])
concurrent_ops_commute (prefix @ xs @ [x])

goal (1 subgoal):
 1. apply_operations (prefix @ x # xs) \<rhd> \<langle>a\<rangle> = apply_operations (prefix @ xs @ [x]) \<rhd> \<langle>a\<rangle>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
apply_operations (prefix @ x # xs) \<rhd> \<langle>a\<rangle> = apply_operations (prefix @ xs @ [x]) \<rhd> \<langle>a\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
apply_operations (prefix @ x # xs) \<rhd> \<langle>a\<rangle> = apply_operations (prefix @ xs @ [x]) \<rhd> \<langle>a\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
have "... = ((apply_operations (prefix @ xs)) \<rhd> \<langle>x\<rangle>) \<rhd> \<langle>a\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. apply_operations (prefix @ xs @ [x]) \<rhd> \<langle>a\<rangle> = (apply_operations (prefix @ xs) \<rhd> \<langle>x\<rangle>) \<rhd> \<langle>a\<rangle>
[PROOF STEP]
by (simp add: append_assoc[symmetric] del: append_assoc)
[PROOF STATE]
proof (state)
this:
apply_operations (prefix @ xs @ [x]) \<rhd> \<langle>a\<rangle> = (apply_operations (prefix @ xs) \<rhd> \<langle>x\<rangle>) \<rhd> \<langle>a\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
apply_operations (prefix @ xs @ [x]) \<rhd> \<langle>a\<rangle> = (apply_operations (prefix @ xs) \<rhd> \<langle>x\<rangle>) \<rhd> \<langle>a\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
have "... = (apply_operations (prefix @ xs)) \<rhd> (\<langle>a\<rangle> \<rhd> \<langle>x\<rangle>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (apply_operations (prefix @ xs) \<rhd> \<langle>x\<rangle>) \<rhd> \<langle>a\<rangle> = apply_operations (prefix @ xs) \<rhd> \<langle>a\<rangle> \<rhd> \<langle>x\<rangle>
[PROOF STEP]
using ac_comm kleisli_comm_cong kleisli_assoc
[PROOF STATE]
proof (prove)
using this:
\<langle>a\<rangle> \<rhd> \<langle>x\<rangle> = \<langle>x\<rangle> \<rhd> \<langle>a\<rangle>
?x \<rhd> ?y = ?y \<rhd> ?x \<Longrightarrow> ?z \<rhd> ?x \<rhd> ?y = ?z \<rhd> ?y \<rhd> ?x
(?z \<rhd> ?x) \<rhd> ?y = ?z \<rhd> ?x \<rhd> ?y

goal (1 subgoal):
 1. (apply_operations (prefix @ xs) \<rhd> \<langle>x\<rangle>) \<rhd> \<langle>a\<rangle> = apply_operations (prefix @ xs) \<rhd> \<langle>a\<rangle> \<rhd> \<langle>x\<rangle>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(apply_operations (prefix @ xs) \<rhd> \<langle>x\<rangle>) \<rhd> \<langle>a\<rangle> = apply_operations (prefix @ xs) \<rhd> \<langle>a\<rangle> \<rhd> \<langle>x\<rangle>

goal (1 subgoal):
 1. \<And>xa xs. \<lbrakk>\<lbrakk>concurrent_ops_commute (prefix @ xs @ [x]); concurrent_set x xs; distinct (prefix @ x # xs)\<rbrakk> \<Longrightarrow> apply_operations (prefix @ xs @ [x]) = apply_operations (prefix @ x # xs); concurrent_ops_commute (prefix @ (xs @ [xa]) @ [x]); concurrent_set x (xs @ [xa]); distinct (prefix @ x # xs @ [xa])\<rbrakk> \<Longrightarrow> apply_operations (prefix @ (xs @ [xa]) @ [x]) = apply_operations (prefix @ x # xs @ [xa])
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
apply_operations ((prefix @ x # xs) @ [a]) = apply_operations (prefix @ xs) \<rhd> \<langle>a\<rangle> \<rhd> \<langle>x\<rangle>
[PROOF STEP]
show "apply_operations (prefix @ (xs @ [a]) @ [x]) = apply_operations (prefix @ x # xs @ [a])"
[PROOF STATE]
proof (prove)
using this:
apply_operations ((prefix @ x # xs) @ [a]) = apply_operations (prefix @ xs) \<rhd> \<langle>a\<rangle> \<rhd> \<langle>x\<rangle>

goal (1 subgoal):
 1. apply_operations (prefix @ (xs @ [a]) @ [x]) = apply_operations (prefix @ x # xs @ [a])
[PROOF STEP]
by (metis Cons_eq_appendI append_assoc apply_operations_Snoc kleisli_assoc)
[PROOF STATE]
proof (state)
this:
apply_operations (prefix @ (xs @ [a]) @ [x]) = apply_operations (prefix @ x # xs @ [a])

goal:
No subgoals!
[PROOF STEP]
qed