section ‹Computations of PiCore Language›
theory PiCore_Computation
imports PiCore_Semantics Computation List_Lemmata
begin
type_synonym ('l,'k,'s,'prog) escpt = ‹(('l,'k,'s,'prog) esconf) list›
locale event_comp = event ptran fin_com
for ptran :: "'Env ⇒ (('s,'prog) pconf × ('s,'prog) pconf) set"
and fin_com :: "'prog"
begin
inductive_cases estran_from_anon_cases: ‹Γ ⊢ (EAnon p, S) ─es[a]→ c›
lemma cpts_from_anon:
assumes h: ‹cpt ∈ cpts_from (estran Γ) (EAnon p0, s0,x0)›
shows ‹∀i. i < length cpt ⟶ (∃p. fst(cpt!i) = EAnon p)›
proof
from h have cpt_nonnil: "cpt ≠ []" using cpts_nonnil by auto
from h have h1: ‹cpt ∈ cpts (estran Γ)› by fastforce
from h have h2: ‹hd cpt = (EAnon p0, s0,x0)› by auto
fix i
show ‹i < length cpt ⟶ (∃p. fst(cpt!i) = EAnon p)›
proof
assume i_lt: ‹i < length cpt›
show ‹(∃p. fst(cpt!i) = EAnon p)›
using i_lt
proof(induct i)
case 0
from h have "hd cpt = (EAnon p0, s0,x0)" by simp
then show ?case using hd_conv_nth cpt_nonnil by fastforce
next
case (Suc i')
then obtain p where fst_cpt_i': "fst(cpt!i') = (EAnon p)" by fastforce
have ‹(cpt!i', cpt!(Suc i')) ∈ estran Γ ∨ cpt!i' ─e→ cpt!(Suc i')›
using cpts_tran h1 Suc(2) by blast
then show ?case
proof
assume ‹(cpt ! i', cpt ! Suc i') ∈ estran Γ›
then show ?thesis
apply(simp add: estran_def)
apply(erule exE)
apply(subst(asm) surjective_pairing[of ‹cpt!i'›])
apply(subst(asm) fst_cpt_i')
apply(erule estran_from_anon_cases)
by simp+
next
assume ‹cpt ! i' ─e→ cpt ! Suc i'›
then show ?thesis
apply simp
using fst_cpt_i' by metis
qed
qed
qed
qed
lemma cpts_from_anon':
assumes h: ‹cpt ∈ cpts_from (estran Γ) (EAnon p0, s0)›
shows ‹∀i. i < length cpt ⟶ (∃p s x. cpt!i = (EAnon p, s, x))›
using cpts_from_anon by (metis h prod.collapse)
primrec (nonexhaustive) unlift_prog where
‹unlift_prog (EAnon p) = p›
definition ‹unlift_conf ≡ λ(p,s,_). (unlift_prog p, s)›
definition unlift_cpt :: ‹(('l, 'k, 's, 'prog) esconf) list ⇒ ('prog × 's) list› where
‹unlift_cpt ≡ map unlift_conf›
declare unlift_conf_def[simp] unlift_cpt_def[simp]
definition lift_conf :: "('l,'k,'s,'prog) ectx ⇒ ('prog×'s) ⇒ (('l,'k,'s,'prog) esconf)" where
‹lift_conf x ≡ λ(p,s). (EAnon p, s,x)›
declare lift_conf_def[simp]
lemma lift_conf_def': ‹lift_conf x (p, s) = (EAnon p, s,x)› by simp
definition lift_cpt :: "('l,'k,'s,'prog) ectx ⇒ ('prog×'s) list ⇒ (('l,'k,'s,'prog) esconf) list" where
‹lift_cpt x ≡ map (lift_conf x)›
declare lift_cpt_def[simp]
inductive_cases estran_anon_to_anon_cases: ‹Γ ⊢ (EAnon p, s,x) ─es[a]→ (EAnon q, t,y)›
lemma unlift_tran: ‹((EAnon p, s,x), (EAnon q, t,x)) ∈ estran Γ ⟹ ((p,s),(q,t)) ∈ ptran Γ›
apply(simp add: case_prod_unfold estran_def)
apply(erule exE)
apply(erule estran_anon_to_anon_cases)
apply simp+
done
lemma unlift_tran': ‹(lift_conf x c, lift_conf x c') ∈ estran Γ ⟹ (c, c') ∈ ptran Γ›
apply (simp add: case_prod_unfold)
apply(subst surjective_pairing[of c])
apply(subst surjective_pairing[of c'])
using unlift_tran by fastforce
lemma cpt_unlift_aux:
‹((EAnon p0, s0,x), Q, t,y) ∈ estran Γ ⟹ ∃Q'. Q = EAnon Q' ∧ ((p0,s0),(Q',t)) ∈ ptran Γ›
by (simp add: estran_def, erule exE, erule estran_p.cases, auto)
lemma ctran_or_etran:
‹cpt ∈ cpts (estran Γ) ⟹
Suc i < length cpt ⟹
(cpt!i, cpt!Suc i) ∈ estran Γ ∧ (¬ cpt!i ─e→ cpt!Suc i) ∨
(cpt!i ─e→ cpt!Suc i) ∧ (cpt!i, cpt!Suc i) ∉ estran Γ›
proof-
assume cpt: ‹cpt ∈ cpts (estran Γ)›
assume Suc_i_lt: ‹Suc i < length cpt›
from cpts_drop[OF cpt Suc_i_lt[THEN Suc_lessD]] have
‹drop i cpt ∈ cpts (estran Γ)› by assumption
then show
‹(cpt!i, cpt!Suc i) ∈ estran Γ ∧ (¬ cpt!i ─e→ cpt!Suc i) ∨
(cpt!i ─e→ cpt!Suc i) ∧ (cpt!i, cpt!Suc i) ∉ estran Γ›
proof(cases)
case (CptsOne P s)
then have False
by (metis (no_types, lifting) Cons_nth_drop_Suc Suc_i_lt Suc_lessD drop_eq_Nil list.inject not_less)
then show ?thesis by blast
next
case (CptsEnv P t cs s)
from nth_via_drop[OF CptsEnv(1)] have ‹cpt!i = (P,s)› by assumption
moreover from CptsEnv(1) have ‹cpt!Suc i = (P,t)›
by (metis Suc_i_lt drop_Suc hd_drop_conv_nth list.sel(1) list.sel(3) tl_drop)
ultimately show ?thesis
by (simp add: no_estran_to_self')
next
case (CptsComp P s Q t cs)
from nth_via_drop[OF CptsComp(1)] have ‹cpt!i = (P,s)› by assumption
moreover from CptsComp(1) have ‹cpt!Suc i = (Q,t)›
by (metis Suc_i_lt drop_Suc hd_drop_conv_nth list.sel(1) list.sel(3) tl_drop)
ultimately show ?thesis
apply simp
apply(rule disjI1)
apply(rule conjI)
apply(rule CptsComp(2))
using CptsComp(2) no_estran_to_self' by blast
qed
qed
lemma ctran_or_etran_par:
‹cpt ∈ cpts (pestran Γ) ⟹
Suc i < length cpt ⟹
(cpt!i, cpt!Suc i) ∈ pestran Γ ∧ (¬ cpt!i ─e→ cpt!Suc i) ∨
(cpt!i ─e→ cpt!Suc i) ∧ (cpt!i, cpt!Suc i) ∉ pestran Γ›
proof-
assume cpt: ‹cpt ∈ cpts (pestran Γ)›
assume Suc_i_lt: ‹Suc i < length cpt›
from cpts_drop[OF cpt Suc_i_lt[THEN Suc_lessD]] have
‹drop i cpt ∈ cpts (pestran Γ)› by assumption
then show
‹(cpt!i, cpt!Suc i) ∈ pestran Γ ∧ (¬ cpt!i ─e→ cpt!Suc i) ∨
(cpt!i ─e→ cpt!Suc i) ∧ (cpt!i, cpt!Suc i) ∉ pestran Γ›
proof(cases)
case (CptsOne P s)
then have False using Suc_i_lt
by (metis Cons_nth_drop_Suc drop_Suc drop_tl list.sel(3) list.simps(3))
then show ?thesis by blast
next
case (CptsEnv P t cs s)
from nth_via_drop[OF CptsEnv(1)] have ‹cpt!i = (P,s)› by assumption
moreover from CptsEnv(1) have ‹cpt!Suc i = (P,t)›
by (metis Suc_i_lt drop_Suc hd_drop_conv_nth list.sel(1) list.sel(3) tl_drop)
ultimately show ?thesis
using no_pestran_to_self
by (simp add: no_pestran_to_self')
next
case (CptsComp P s Q t cs)
from nth_via_drop[OF CptsComp(1)] have ‹cpt!i = (P,s)› by assumption
moreover from CptsComp(1) have ‹cpt!Suc i = (Q,t)›
by (metis Suc_i_lt drop_Suc hd_drop_conv_nth list.sel(1) list.sel(3) tl_drop)
ultimately show ?thesis
apply simp
apply(rule disjI1)
apply(rule conjI)
apply(rule CptsComp(2))
using CptsComp(2) no_pestran_to_self' by blast
qed
qed
abbreviation "lift_seq Q P ≡ ESeq P Q"
primrec lift_seq_esconf where "lift_seq_esconf Q (P,s) = (lift_seq Q P, s)"
abbreviation ‹lift_seq_cpt Q ≡ map (lift_seq_esconf Q)›
primrec lift_seq_esconf' where "lift_seq_esconf' Q (P,s) = (if P = fin then (Q,s) else (lift_seq Q P, s))"
abbreviation ‹lift_seq_cpt' Q ≡ map (lift_seq_esconf' Q)›
lemma all_fin_after_fin:
‹(fin, s) # cs ∈ cpts (estran Γ) ⟹ ∀c∈set cs. fst c = fin›
proof-
obtain cpt where cpt: "cpt = (fin, s)#cs" by simp
assume ‹(fin, s) # cs ∈ cpts (estran Γ)›
with cpt have ‹cpt ∈ cpts (estran Γ)› by simp
then show ?thesis using cpt
apply (induct arbitrary: s cs)
apply simp
proof-
fix P s t sa
fix cs csa :: ‹('a,'k,'s,'prog) escpt›
assume h: ‹⋀s csa. (P, t) # cs = (fin, s) # csa ⟹ ∀c∈set csa. fst c = fin›
assume eq: ‹(P, s) # (P, t) # cs = (fin, sa) # csa›
then have P_fin: ‹P = fin› by simp
with h have ‹∀c∈set cs. fst c = fin› by blast
moreover from eq P_fin have "csa = (fin, t)#cs" by fast
ultimately show ‹∀c∈set csa. fst c = fin› by simp
next
fix P Q :: ‹('a,'k,'s,'prog) esys›
fix s t sa :: ‹'s ×('a,'k,'s,'prog) ectx›
fix cs csa :: ‹('a,'k,'s,'prog) escpt›
assume tran: ‹((P, s), Q, t) ∈ estran Γ›
assume ‹(P, s) # (Q, t) # cs = (fin, sa) # csa›
then have P_fin: ‹P = fin› by simp
with tran have ‹((fin, s), (Q,t)) ∈ estran Γ› by simp
then have False
apply(simp add: estran_def)
using no_estran_from_fin by fast
then show ‹∀c∈set csa. fst c = fin› by blast
qed
qed
lemma lift_seq_cpt_partial:
assumes ‹cpt∈cpts (estran Γ)›
and ‹fst (last cpt) ≠ fin›
shows ‹lift_seq_cpt Q cpt ∈ cpts (estran Γ)›
using assms
proof(induct)
case (CptsOne P s)
show ?case by auto
next
case (CptsEnv P t cs s)
then show ?case by auto
next
case (CptsComp P S Q1 T cs)
from CptsComp(4) have 1: ‹fst (last ((Q1, T) # cs)) ≠ fin› by simp
from CptsComp(3)[OF 1] have IH': ‹map (lift_seq_esconf Q) ((Q1, T) # cs) ∈ cpts (estran Γ)› .
have ‹Q1≠fin›
proof
assume ‹Q1=fin›
with all_fin_after_fin CptsComp(2) have ‹fst (last ((Q1, T) # cs)) = fin› by fastforce
with 1 show False by blast
qed
obtain s x where S: ‹S=(s,x)› by fastforce
obtain t y where T: ‹T=(t,y)› by fastforce
show ?case
apply simp
apply(rule cpts.CptsComp)
apply(insert CptsComp(1))
apply(simp add: estran_def) apply(erule exE) apply(rule exI)
apply(simp add: S T)
apply(erule ESeq)
apply(rule ‹Q1≠fin›)
using IH'[simplified] .
qed
lemma lift_seq_cpt:
assumes ‹cpt∈cpts (estran Γ)›
and ‹Γ ⊢ last cpt ─es[a]→ (fin,t,y)›
shows ‹lift_seq_cpt Q cpt @ [(Q,t,y)] ∈ cpts (estran Γ)›
using assms
proof(induct)
case (CptsOne P S)
obtain s x where S: ‹S=(s,x)› by fastforce
show ?case apply simp
apply(rule CptsComp)
apply (simp add: estran_def)
apply(rule exI)
apply(subst S)
apply(rule ESeq_fin)
using CptsOne S apply simp
by (rule cpts.CptsOne)
next
case (CptsEnv P T1 cs S)
have ‹map (lift_seq_esconf Q) ((P, T1) # cs) @ [(Q, t,y)] ∈ cpts (estran Γ)›
apply(rule CptsEnv(2))
using CptsEnv(3) by fastforce
then show ?case apply simp by (erule cpts.CptsEnv)
next
case (CptsComp P S Q1 T1 cs)
from CptsComp(1) have ctran: ‹∃a. Γ ⊢ (P,S)─es[a]→(Q1,T1)›
by (simp add: estran_def)
have ‹Q1≠fin›
proof
assume ‹Q1=fin›
with all_fin_after_fin CptsComp(2) have ‹∀c∈set cs. fst c = fin› by fastforce
with ‹Q1=fin› have ‹fst (last ((P, S) # (Q1, T1) # cs)) = fin› by simp
with CptsComp(4) have ‹Γ ⊢ (fin, snd (last ((P, S) # (Q1, T1) # cs))) ─es[a]→ (fin, t,y)› using surjective_pairing by metis
with no_estran_from_fin show False by blast
qed
obtain s x where S:‹S=(s,x)› by fastforce
obtain t1 y1 where T1:‹T1=(t1,y1)› by fastforce
have ‹map (lift_seq_esconf Q) ((Q1, T1) # cs) @ [(Q, t,y)] ∈ cpts (estran Γ)› using CptsComp(3,4) by fastforce
then show ?case apply simp apply(rule cpts.CptsComp)
apply(simp add: estran_def) apply(insert ctran) apply(erule exE) apply(rule exI)
apply(simp add: S T1)
apply(erule ESeq)
apply(rule ‹Q1≠fin›)
by assumption
qed
lemma all_etran_from_fin:
assumes cpt: "cpt ∈ cpts (estran Γ)"
and cpt_eq: "cpt = (fin, t) # cs"
shows ‹∀i. Suc i < length cpt ⟶ cpt!i ─e→ cpt!Suc i›
using cpt cpt_eq
proof(induct arbitrary:t cs)
case (CptsOne P s)
then show ?case by simp
next
case (CptsEnv P t1 cs1 s)
then have et: ‹∀i. Suc i < length ((P, t1) # cs1) ⟶ ((P, t1) # cs1) ! i ─e→ ((P, t1) # cs1) ! Suc i› by fast
show ?case
proof
fix i
show ‹Suc i < length ((P, s) # (P, t1) # cs1) ⟶ ((P, s) # (P, t1) # cs1) ! i ─e→ ((P, s) # (P, t1) # cs1) ! Suc i›
proof(cases i)
case 0
then show ?thesis by simp
next
case (Suc i')
then show ?thesis using et by auto
qed
qed
next
case (CptsComp P s Q t1 cs1)
then have ‹((EAnon fin_com, t), Q, t1) ∈ estran Γ› by fast
then obtain a where
‹Γ ⊢ (EAnon fin_com, t) ─es[a]→ (Q, t1)› using estran_def by blast
then have False using no_estran_from_fin by blast
then show ?case by blast
qed
lemma no_ctran_from_fin:
assumes cpt: "cpt ∈ cpts (estran Γ)"
and cpt_eq: "cpt = (fin, t) # cs"
shows ‹∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∉ estran Γ›
proof
fix i
have 1: ‹∀i. Suc i < length cpt ⟶ cpt!i ─e→ cpt!Suc i› by (rule all_etran_from_fin[OF cpt cpt_eq])
show ‹Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∉ estran Γ›
proof
assume ‹Suc i < length cpt›
with 1 have ‹cpt!i ─e→ cpt!Suc i› by blast
then show ‹(cpt ! i, cpt ! Suc i) ∉ estran Γ›
apply simp
using no_estran_to_self'' by blast
qed
qed
inductive_set cpts_es_mod for Γ where
CptsModOne[intro]: "[(P,s,x)] ∈ cpts_es_mod Γ" |
CptsModEnv[intro]: "(P,t,y)#cs ∈ cpts_es_mod Γ ⟹ (P,s,x)#(P,t,y)#cs ∈ cpts_es_mod Γ" |
CptsModAnon: "⟦ Γ ⊢ (P, s) ─c→ (Q, t); Q ≠ fin_com; (EAnon Q, t,x)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EAnon P, s,x)#(EAnon Q, t,x)#cs ∈ cpts_es_mod Γ" |
CptsModAnon_fin: "⟦ Γ ⊢ (P, s) ─c→ (Q, t); Q = fin_com; y = x(k:=None); (EAnon Q, t,y)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EAnon P, s,x)#(EAnon Q, t,y)#cs ∈ cpts_es_mod Γ" |
CptsModBasic: ‹⟦ P = body e; s ∈ guard e; y=x(k:=Some e); (EAnon P, s,y)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EBasic e, s,x)#(EAnon P, s,y)#cs ∈ cpts_es_mod Γ› |
CptsModAtom: ‹⟦ P = body e; s ∈ guard e; Γ ⊢ (P,s)─c*→(fin_com,t); (EAnon fin_com, t,x)#cs ∈ cpts_es_mod Γ ⟧
⟹ (EAtom e, s,x)#(EAnon fin_com, t,x)#cs ∈ cpts_es_mod Γ› |
CptsModSeq: ‹Γ ⊢ (P,s,x)─es[a]→(Q,t,y) ⟹ Q≠fin ⟹ (ESeq Q R, t,y)#cs ∈ cpts_es_mod Γ ⟹ (ESeq P R, s,x)#(ESeq Q R, t,y)#cs ∈ cpts_es_mod Γ› |
CptsModSeq_fin: ‹Γ ⊢ (P,s,x)─es[a]→(fin,t,y) ⟹ (Q,t,y)#cs ∈ cpts_es_mod Γ ⟹ (P NEXT Q, s,x)#(Q,t,y)#cs ∈ cpts_es_mod Γ› |
CptsModChc1: ‹⟦ Γ ⊢ (P,s,x) ─es[a]→ (Q,t,y); (Q,t,y)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EChc P R, s,x)#(Q,t,y)#cs ∈ cpts_es_mod Γ› |
CptsModChc2: ‹⟦ Γ ⊢ (P,s,x) ─es[a]→ (Q,t,y); (Q,t,y)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EChc R P, s,x)#(Q,t,y)#cs ∈ cpts_es_mod Γ› |
CptsModJoin1: ‹⟦ Γ ⊢ (P,s,x) ─es[a]→ (Q,t,y); (EJoin Q R, t,y)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EJoin P R, s,x)#(EJoin Q R, t,y)#cs ∈ cpts_es_mod Γ› |
CptsModJoin2: ‹⟦ Γ ⊢ (P,s,x) ─es[a]→ (Q,t,y); (EJoin R Q, t,y)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EJoin R P, s,x)#(EJoin R Q, t,y)#cs ∈ cpts_es_mod Γ› |
CptsModJoin_fin: ‹(fin,t,y)#cs ∈ cpts_es_mod Γ ⟹ (fin⋈fin,t,y)#(fin,t,y)#cs ∈ cpts_es_mod Γ› |
CptsModWhileTMore: ‹⟦ s∈b; (P,s,x)#cs ∈ cpts (estran Γ); Γ ⊢ (last ((P,s,x)#cs)) ─es[a]→ (fin,t,y); (EWhile b P, t,y)#cs' ∈ cpts_es_mod Γ ⟧
⟹ (EWhile b P, s,x) # lift_seq_cpt (EWhile b P) ((P,s,x)#cs) @ (EWhile b P, t,y) # cs' ∈ cpts_es_mod Γ› |
CptsModWhileTOnePartial: ‹⟦ s∈b; (P,s,x)#cs ∈ cpts (estran Γ); fst (last ((P,s,x)#cs)) ≠ fin ⟧ ⟹ (EWhile b P, s,x) # lift_seq_cpt (EWhile b P) ((P,s,x)#cs) ∈ cpts_es_mod Γ› |
CptsModWhileTOneFull: ‹⟦ s∈b; (P,s,x)#cs ∈ cpts (estran Γ); Γ ⊢ (last ((P,s,x)#cs))─es[a]→(fin,t,y); (fin,t,y)#cs' ∈ cpts_es_mod Γ ⟧ ⟹
(EWhile b P, s,x) # lift_seq_cpt (EWhile b P) ((P,s,x)#cs) @ map (λ(_,s,x). (EWhile b P, s,x)) ((fin,t,y)#cs') ∈ cpts_es_mod Γ› |
CptsModWhileF: ‹⟦ s∉b; (fin, s,x)#cs ∈ cpts_es_mod Γ ⟧ ⟹ (EWhile b P, s,x)#(fin, s,x)#cs ∈ cpts_es_mod Γ›
definition ‹all_seq Q cs ≡ ∀c∈set cs. ∃P. fst c = P NEXT Q›
lemma equiv_aux1:
‹cs ∈ cpts (estran Γ) ⟹
hd cs = (P NEXT Q, s) ⟹
P ≠ fin ⟹
all_seq Q cs ⟹
∃cs0. cs = lift_seq_cpt Q ((P, s) # cs0) ∧ (P,s)#cs0 ∈ cpts (estran Γ) ∧ fst (last ((P,s)#cs0)) ≠ fin›
proof-
assume cpt: ‹cs ∈ cpts (estran Γ)›
assume cs: ‹hd cs = (P NEXT Q, s)›
assume ‹P≠fin›
assume all_seq: ‹all_seq Q cs›
show ?thesis
using cpt cs ‹P≠fin› all_seq
proof(induct arbitrary: P s)
case (CptsOne P1 s1)
then show ?case apply-
apply(rule exI[where x=‹[]›])
apply simp
by (rule cpts.CptsOne)
next
case (CptsEnv P1 t cs s1)
from CptsEnv(3) have 1: ‹hd ((P1, t) # cs) = (P NEXT Q, t)› by simp
from ‹all_seq Q ((P1, s1) # (P1, t) # cs)› have 2: ‹all_seq Q ((P1, t) # cs)› by (simp add: all_seq_def)
from CptsEnv(3) have ‹s1=s› by simp
from CptsEnv(2)[OF 1 CptsEnv(4) 2] obtain cs0 where
‹(P1, t) # cs = map (lift_seq_esconf Q) ((P, t) # cs0) ∧ (P, t) # cs0 ∈ cpts (estran Γ) ∧ fst (last ((P, t) # cs0)) ≠ fin› by meson
then show ?case apply- apply(rule exI[where x=‹(P,t)#cs0›])
apply (simp add: ‹s1=s›)
apply(rule cpts.CptsEnv)
by blast
next
case (CptsComp P1 s1 Q1 t cs)
from CptsComp(6) obtain P' where Q1: ‹Q1 = P' NEXT Q› by (auto simp add: all_seq_def)
then have 1: ‹hd ((Q1, t) # cs) = (P' NEXT Q, t)› by simp
from CptsComp(4) have P1: ‹P1=P NEXT Q› and ‹s1=s› by simp+
from CptsComp(1) P1 Q1 have ‹P'≠fin›
apply (simp add: estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)[]
using Q1 seq_neq2 by blast
from CptsComp(1) P1 Q1 have tran: ‹((P, s), P', t) ∈ estran Γ›
apply(simp add: estran_def) apply(erule exE) apply(erule estran_p.cases, auto)[]
apply(rule exI) apply (simp add: ‹s1=s›)
using seq_neq2 by blast
from CptsComp(6) have 2: ‹all_seq Q ((Q1, t) # cs)› by (simp add: all_seq_def)
from CptsComp(3)[OF 1 ‹P'≠fin› 2] obtain cs0 where
‹(Q1, t) # cs = map (lift_seq_esconf Q) ((P', t) # cs0) ∧ (P', t) # cs0 ∈ cpts (estran Γ) ∧ fst (last ((P', t) # cs0)) ≠ fin› by meson
then show ?case apply- apply(rule exI[where x=‹(P',t)#cs0›])
apply(rule conjI)
apply (simp add: ‹s1=s› P1)
apply(rule conjI)
apply(rule cpts.CptsComp)
apply(rule tran)
apply blast
by simp
qed
qed
lemma split_seq_mod:
assumes cpt: ‹cpt ∈ cpts_es_mod Γ›
and hd_cpt: ‹hd cpt = (es1 NEXT es2, S0)›
and not_all_seq: ‹¬ all_seq es2 cpt›
shows
"∃i S'. cpt!i = (es2, S') ∧
i ≠ 0 ∧
i < length cpt ∧
(∃cpt'. take i cpt = lift_seq_cpt es2 ((es1,S0)#cpt') ∧ ((es1,S0)#cpt')∈cpts (estran Γ) ∧ (last ((es1,S0)#cpt'), (fin, S'))∈estran Γ) ∧
all_seq es2 (take i cpt) ∧
drop i cpt ∈ cpts_es_mod Γ"
using cpt hd_cpt not_all_seq
proof(induct arbitrary: es1 S0)
case (CptsModOne P S)
then show ?case by (simp add: all_seq_def)
next
case (CptsModEnv P t y cs s x)
from CptsModEnv(3) have P_dest: ‹P = es1 NEXT es2› by simp
from P_dest have 1: ‹(hd ((P, t, y) # cs)) = (es1 NEXT es2, t, y)› by simp
from CptsModEnv(4) have 2: ‹¬ all_seq es2 ((P, t, y) # cs)› by (simp add: all_seq_def)
from CptsModEnv(2)[OF 1 2] obtain i S' where
‹((P, t, y) # cs) ! i = (es2, S') ∧
i ≠ 0 ∧
i < length ((P, t, y) # cs) ∧
(∃cpt'. take i ((P, t, y) # cs) = map (lift_seq_esconf es2) ((es1, t, y) # cpt') ∧ (es1, t, y) # cpt' ∈ cpts (estran Γ) ∧ (last ((es1, t, y) # cpt'), fin, S') ∈ estran Γ) ∧
all_seq es2 (take i ((P, t, y) # cs)) ∧ drop i ((P, t, y) # cs) ∈ cpts_es_mod Γ›
by meson
then have
p1: ‹((P, t, y) # cs) ! i = (es2, S')› and
p2: ‹i≠0› and
p3: ‹i < length ((P, t, y) # cs)› and
p4: ‹∃cpt'. take i ((P, t, y) # cs) = map (lift_seq_esconf es2) ((es1, t, y) # cpt') ∧ ((es1, t, y) # cpt') ∈ cpts (estran Γ) ∧ (last ((es1, t, y) # cpt'), fin, S') ∈ estran Γ› and
p5: ‹all_seq es2 (take i ((P, t, y) # cs))› and
p6: ‹drop i ((P, t, y) # cs) ∈ cpts_es_mod Γ› by argo+
from p4 obtain cpt' where
p4_1: ‹take i ((P, t, y) # cs) = map (lift_seq_esconf es2) ((es1, t, y) # cpt')› and
p4_2: ‹((es1, t, y) # cpt') ∈ cpts (estran Γ)› and
p4_3: ‹(last ((es1, t, y) # cpt'), fin, S') ∈ estran Γ› by meson
show ?case
apply(rule exI[where x="Suc i"])
apply(rule exI[where x=S'])
apply(rule conjI)
using p1 apply simp
apply(rule conjI) apply simp
apply(rule conjI) using p3 apply simp
apply(rule conjI)
apply(rule exI[where x=‹(es1,t,y)#cpt'›])
apply(rule conjI)
using p4_1 P_dest apply simp
using CptsModEnv(3) apply simp
apply(rule conjI)
apply(rule CptsEnv)
using p4_2 apply fastforce
using p4_3 apply fastforce
using p5 P_dest apply(simp add: all_seq_def)
using p6 apply simp.
next
case (CptsModAnon)
then show ?case by simp
next
case (CptsModAnon_fin)
then show ?case by simp
next
case (CptsModBasic)
then show ?case by simp
next
case (CptsModAtom)
then show ?case by simp
next
case (CptsModSeq P s x a Q t y R cs)
from CptsModSeq(5) have ‹R=es2› by simp
then have 1: ‹(hd ((Q NEXT R, t,y) # cs)) = (Q NEXT es2, t,y)› by simp
from CptsModSeq(6) ‹R=es2› have 2: ‹¬ all_seq es2 ((Q NEXT R, t,y) # cs)› by (simp add: all_seq_def)
from CptsModSeq(4)[OF 1 2] obtain i S' where
‹((Q NEXT R, t, y) # cs) ! i = (es2, S') ∧
i ≠ 0 ∧
i < length ((Q NEXT R, t, y) # cs) ∧
(∃cpt'. take i ((Q NEXT R, t, y) # cs) = map (lift_seq_esconf es2) ((Q, t, y) # cpt') ∧ (Q, t, y) # cpt' ∈ cpts (estran Γ) ∧ (last ((Q, t, y) # cpt'), fin, S') ∈ estran Γ) ∧
all_seq es2 (take i ((Q NEXT R, t, y) # cs)) ∧ drop i ((Q NEXT R, t, y) # cs) ∈ cpts_es_mod Γ› by meson
then have
p1: ‹((Q NEXT R, t,y) # cs) ! i = (es2, S')› and
p2: ‹i≠0› and
p3: ‹i < length ((Q NEXT R, t,y) # cs)› and
p4: ‹∃cpt'. take i ((Q NEXT R, t,y) # cs) = map (lift_seq_esconf es2) ((Q, t,y) # cpt') ∧ ((Q, t,y) # cpt') ∈ cpts (estran Γ) ∧ (last ((Q, t,y) # cpt'), fin, S') ∈ estran Γ› and
p5: ‹all_seq es2 (take i ((Q NEXT R, t,y) # cs))› and
p6: ‹drop i ((Q NEXT R, t,y) # cs) ∈ cpts_es_mod Γ› by argo+
from p4 obtain cpt' where
p4_1: ‹take i ((Q NEXT R, t,y) # cs) = map (lift_seq_esconf es2) ((Q, t,y) # cpt')› and
p4_2: ‹((Q, t,y) # cpt') ∈ cpts (estran Γ)› and
p4_3: ‹(last ((Q, t,y) # cpt'), fin, S') ∈ estran Γ› by meson
show ?case
apply(rule exI[where x="Suc i"])
apply(rule exI[where x=S'])
apply(rule conjI)
using p1 apply simp
apply(rule conjI) apply simp
apply(rule conjI) using p3 apply simp
apply(rule conjI)
apply(rule exI[where x=‹(Q,t,y)#cpt'›])
apply(rule conjI)
using p4_1 CptsModSeq(5) apply simp
apply(rule conjI)
apply(rule CptsComp)
using CptsModSeq(1,5) apply (auto simp add: estran_def)[]
using p4_2 apply simp
using p4_3 apply simp
using p5 ‹R=es2› apply(simp add: all_seq_def)
using p6 by fastforce
next
case (CptsModSeq_fin P s x a t y Q cs)
from CptsModSeq_fin(4) have ‹P=es1› ‹Q=es2› ‹(s,x)=S0› by simp+
show ?case
apply(rule exI[where x=1])
apply(rule exI[where x=‹(t,y)›])
apply(simp add: all_seq_def ‹P=es1› ‹Q=es2› ‹(s,x)=S0›)
apply(rule conjI)
apply(rule CptsOne)
apply(rule conjI)
using CptsModSeq_fin(1) ‹P=es1› ‹(s,x)=S0› apply (auto simp add: estran_def)[]
using CptsModSeq_fin(2) ‹Q=es2› by simp
next
case (CptsModChc1)
then show ?case by simp
next
case (CptsModChc2)
then show ?case by simp
next
case (CptsModJoin1)
then show ?case by simp
next
case (CptsModJoin2)
then show ?case by simp
next
case (CptsModJoin_fin)
then show ?case by simp
next
case (CptsModWhileTMore)
then show ?case by simp
next
case (CptsModWhileTOnePartial)
then show ?case by simp
next
case (CptsModWhileTOneFull)
then show ?case by simp
next
case (CptsModWhileF)
then show ?case by simp
qed
lemma equiv_aux2:
‹∀i<length cs. fst (cs!i) = P ⟹ (P,s)#cs ∈ cpts tran›
proof(induct cs arbitrary:s)
case Nil
show ?case by (rule CptsOne)
next
case (Cons c cs)
from Cons(2)[THEN spec[where x=0]] have ‹fst c = P› by simp
show ?case apply(subst surjective_pairing[of c]) apply(subst ‹fst c = P›)
apply(rule CptsEnv)
apply(rule Cons(1))
using Cons(2) by fastforce
qed
theorem cpts_es_mod_equiv:
‹cpts (estran Γ) = cpts_es_mod Γ›
proof
show ‹cpts (estran Γ) ⊆ cpts_es_mod Γ›
proof
fix cpt
assume ‹cpt ∈ cpts (estran Γ)›
then show ‹cpt ∈ cpts_es_mod Γ›
proof(induct)
case (CptsOne P S)
obtain s x where ‹S=(s,x)› by fastforce
from CptsOne this CptsModOne show ?case by fast
next
case (CptsEnv P T cs S)
obtain s x where S:‹S=(s,x)› by fastforce
obtain t y where T:‹T=(t,y)› by fastforce
show ?case using CptsModEnv estran_def S T CptsEnv by fast
next
case (CptsComp P S Q T cs)
from CptsComp(1) obtain a where h:
‹Γ ⊢ (P,S)─es[a]→(Q,T)› using estran_def by blast
then show ?case
proof(cases)
case (EAnon)
then show ?thesis apply clarify
apply(erule CptsModAnon) apply blast
using CptsComp EAnon by blast
next
case (EAnon_fin)
then show ?thesis apply clarify
apply(erule CptsModAnon_fin) apply blast+
using CptsComp EAnon by blast
next
case (EBasic)
then show ?thesis apply clarify
apply(rule CptsModBasic, auto)
using CptsComp EBasic by simp
next
case (EAtom)
then show ?thesis apply clarify
apply(rule CptsModAtom) using CptsComp by auto
next
case (ESeq)
then show ?thesis apply clarify
apply(rule CptsModSeq) using CptsComp by auto
next
case (ESeq_fin)
then show ?thesis apply clarify
apply(rule CptsModSeq_fin) using CptsComp by auto
next
case (EChc1)
then show ?thesis apply clarify
apply(rule CptsModChc1) using CptsComp by auto
next
case (EChc2)
then show ?thesis apply clarify
apply(rule CptsModChc2) using CptsComp by auto
next
case (EJoin1)
then show ?thesis apply clarify
apply(rule CptsModJoin1) using CptsComp by auto
next
case (EJoin2)
then show ?thesis apply clarify
apply(rule CptsModJoin2) using CptsComp by auto
next
case EJoin_fin
then show ?thesis apply clarify
apply(rule CptsModJoin_fin) using CptsComp by auto
next
case EWhileF
then show ?thesis apply clarify
apply(rule CptsModWhileF) using CptsComp by auto
next
case (EWhileT s b P1 x k)
thm CptsComp
show ?thesis
proof(cases ‹all_seq (EWhile b P1) ((P1 NEXT EWhile b P1, T) # cs)›)
case True
from EWhileT(4) have 1: ‹hd ((Q, T) # cs) = (P1 NEXT EWhile b P1, T)› by simp
from True EWhileT(4) have 2: ‹all_seq (EWhile b P1) ((Q, T) # cs)› by simp
from equiv_aux1[OF CptsComp(2) 1 ‹P1≠fin› 2] obtain cs0 where
3: ‹(Q, T) # cs = map (lift_seq_esconf (EWhile b P1)) ((P1, T) # cs0) ∧ (P1, T) # cs0 ∈ cpts (estran Γ) ∧ fst (last ((P1, T) # cs0)) ≠ fin› by meson
then have p3_1: ‹(Q, T) # cs = map (lift_seq_esconf (EWhile b P1)) ((P1, T) # cs0)› and
p3_2: ‹(P1, s, x) # cs0 ∈ cpts (estran Γ)› and
p3_3: ‹fst (last ((P1, s, x) # cs0)) ≠ fin› using ‹T=(s,x)› by blast+
from CptsModWhileTOnePartial[OF ‹s∈b› p3_2 p3_3]
have ‹(EWhile b P1, s,x) # map (lift_seq_esconf (EWhile b P1)) ((P1, s,x) # cs0) ∈ cpts_es_mod Γ› .
with EWhileT 3 show ?thesis by simp
next
case False
with EWhileT(4) have not_all_seq: ‹¬all_seq (EWhile b P1) ((Q,T)#cs)› by simp
from EWhileT(4) have ‹(hd ((Q, T) # cs)) = (P1 NEXT EWhile b P1, T)› by simp
from split_seq_mod[OF CptsComp(3) this not_all_seq] obtain i S' where split:
‹((Q, T) # cs) ! i = (EWhile b P1, S') ∧
i ≠ 0 ∧
i < length ((Q, T) # cs) ∧
(∃cpt'. take i ((Q, T) # cs) = map (lift_seq_esconf (EWhile b P1)) ((P1, T) # cpt') ∧ (P1, T) # cpt' ∈ cpts (estran Γ) ∧ (last ((P1, T) # cpt'), fin, S') ∈ estran Γ) ∧
all_seq (EWhile b P1) (take i ((Q, T) # cs)) ∧ drop i ((Q, T) # cs) ∈ cpts_es_mod Γ›
by blast
then have 3: ‹all_seq (EWhile b P1) (take i ((Q, T) # cs))›
and ‹i≠0›
and i_lt: ‹i < length ((Q, T) # cs)›
and part2_cpt: ‹drop i ((Q, T) # cs) ∈ cpts_es_mod Γ›
and ex_cpt': ‹∃cpt'. take i ((Q, T) # cs) = map (lift_seq_esconf (EWhile b P1)) ((P1, T) # cpt') ∧ (P1, T) # cpt' ∈ cpts (estran Γ) ∧ (last ((P1, T) # cpt'), fin, S') ∈ estran Γ› by blast+
from ex_cpt' obtain cpt' where cpt'1: ‹take i ((Q, T) # cs) = map (lift_seq_esconf (EWhile b P1)) ((P1, T) # cpt')› and
cpt'2: ‹((P1, s,x) # cpt') ∈ cpts (estran Γ)› and
cpt'3: ‹(last ((P1, s,x) # cpt'), fin, S') ∈ estran Γ› using ‹T=(s,x)› by meson
from cpts_take[OF CptsComp(2)] ‹i≠0› have 1: ‹take i ((Q, T) # cs) ∈ cpts (estran Γ)› by fast
have 2: ‹hd (take i ((Q, T) # cs)) = (P1 NEXT EWhile b P1, T)› using ‹i≠0› EWhileT(4) by simp
obtain s' x' where S': ‹S'=(s',x')› by fastforce
obtain cs' where part2_eq: ‹drop i ((Q, T) # cs) = (EWhile b P1, S') # cs'›
proof
from split have ‹((Q, T) # cs) ! i = (EWhile b P1, S')› by argo
with i_lt show ‹drop i ((Q, T) # cs) = (EWhile b P1, S') # drop (Suc i) ((Q,T)#cs)›
using Cons_nth_drop_Suc by metis
qed
with part2_cpt S' have ‹(EWhile b P1, s',x') # cs' ∈ cpts_es_mod Γ› by argo
from cpt'3 have ‹∃a. Γ ⊢ last ((P1, s,x) # cpt') ─es[a]→ (fin, S')› by (simp add: estran_def)
then obtain a where ‹Γ ⊢ last ((P1, s,x) # cpt') ─es[a]→ (fin, s', x')› using S' by meson
from CptsModWhileTMore[OF ‹s∈b› cpt'2[simplified] this ‹(EWhile b P1, s',x') # cs' ∈ cpts_es_mod Γ›] have
‹(EWhile b P1, s, x) # map (lift_seq_esconf (EWhile b P1)) ((P1, s, x) # cpt') @ (EWhile b P1, s', x') # cs' ∈ cpts_es_mod Γ› .
moreover have ‹(Q,T)#cs = map (lift_seq_esconf (EWhile b P1)) ((P1, T) # cpt') @ (EWhile b P1, S') # cs'›
using cpt'1 part2_eq i_lt by (metis append_take_drop_id)
ultimately show ?thesis using EWhileT S' by argo
qed
qed
qed
qed
next
show ‹cpts_es_mod Γ ⊆ cpts (estran Γ)›
proof
fix cpt
assume ‹cpt ∈ cpts_es_mod Γ›
then show ‹cpt ∈ cpts (estran Γ)›
proof(induct)
case (CptsModOne)
then show ?case by (rule CptsOne)
next
case (CptsModEnv)
then show ?case using CptsEnv by fast
next
case (CptsModAnon P s Q t x cs)
from CptsModAnon(1) have ‹((P,s),(Q,t))∈ptran Γ› by simp
with CptsModAnon show ?case apply- apply(rule CptsComp, auto simp add: estran_def)
apply(rule exI)
apply(rule EAnon)
apply simp+
done
next
case (CptsModAnon_fin P s Q t y x k cs)
from CptsModAnon_fin(1) have ‹((P,s),(Q,t))∈ptran Γ› by simp
with CptsModAnon_fin show ?case apply- apply(rule CptsComp, auto simp add: estran_def)
apply(rule exI)
apply(rule EAnon_fin)
by simp+
next
case (CptsModBasic)
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EBasic, auto) done
next
case (CptsModAtom)
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EAtom, auto) done
next
case (CptsModSeq)
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule ESeq, auto) done
next
case CptsModSeq_fin
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule ESeq_fin).
next
case (CptsModChc1)
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EChc1, auto) done
next
case (CptsModChc2)
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EChc2, auto) done
next
case (CptsModJoin1)
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EJoin1, auto) done
next
case (CptsModJoin2)
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EJoin2, auto) done
next
case CptsModJoin_fin
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EJoin_fin).
next
case CptsModWhileF
then show ?case apply- apply(rule CptsComp, auto simp add: estran_def, rule exI)
apply(rule EWhileF, auto) done
next
case (CptsModWhileTMore s b P x cs a t y cs')
from CptsModWhileTMore(2,3) all_fin_after_fin no_estran_from_fin have ‹P≠fin›
by (metis last_in_set list.distinct(1) prod.collapse set_ConsD)
have 1: ‹map (lift_seq_esconf (EWhile b P)) ((P, s,x) # cs) @ (EWhile b P, t,y) # cs' ∈ cpts (estran Γ)›
proof-
from lift_seq_cpt[OF ‹(P, s,x) # cs ∈ cpts (estran Γ)› CptsModWhileTMore(3)]
have ‹map (lift_seq_esconf (EWhile b P)) ((P, s,x) # cs) @ [(EWhile b P, t,y)] ∈ cpts (estran Γ)› .
then have cpt_part1: ‹map (lift_seq_esconf (EWhile b P)) ((P, s,x) # cs) ∈ cpts (estran Γ)›
apply simp using cpts_remove_last by fast
from CptsModWhileTMore(3)
have tran: ‹(last (map (lift_seq_esconf (EWhile b P)) ((P, s,x) # cs)), hd ((EWhile b P, t,y) # cs')) ∈ estran Γ›
apply (auto simp add: estran_def)
apply(rule exI)
apply(erule ESeq_fin)
apply(rule exI)
apply(subst last_map)
apply assumption
apply(simp add: lift_seq_esconf_def case_prod_unfold)
apply(subst surjective_pairing[of‹snd (last cs)›])
apply(rule ESeq_fin)
by simp
show ?thesis
apply(rule cpts_append_comp)
apply(rule cpt_part1)
apply(rule CptsModWhileTMore(5))
apply(rule tran)
done
qed
show ?case
apply simp
apply(rule CptsComp)
apply (simp add: estran_def)
apply(rule exI)
apply(rule EWhileT)
apply(rule ‹s∈b›)
apply(rule ‹P≠fin›)
using 1 by fastforce
next
case (CptsModWhileTOnePartial s b P x cs)
from CptsModWhileTOnePartial(3) all_fin_after_fin have ‹P≠fin›
by (metis CptsModWhileTOnePartial.hyps(2) fst_conv last_in_set list.distinct(1) set_ConsD)
from lift_seq_cpt_partial[OF ‹(P, s,x) # cs ∈ cpts (estran Γ)› ‹fst (last ((P, s,x) # cs)) ≠ fin›]
have 1: ‹lift_seq_cpt (EWhile b P) ((P, s,x) # cs) ∈ cpts (estran Γ)› .
show ?case
apply simp
apply(rule CptsComp)
apply (simp add: estran_def)
apply(rule exI)
apply(rule EWhileT)
apply(rule ‹s∈b›)
apply(rule ‹P≠fin›)
using 1 by simp
next
case (CptsModWhileTOneFull s b P x cs a t y cs')
from lift_seq_cpt[OF ‹(P, s,x) # cs ∈ cpts (estran Γ)› ‹Γ ⊢ last ((P, s,x) # cs) ─es[a]→ (fin, t,y)›]
have 1: ‹map (lift_seq_esconf (EWhile b P)) ((P, s,x) # cs) @ [(EWhile b P, t,y)] ∈ cpts (estran Γ)› .
let ?map = ‹map (λ(_, s,x). (EWhile b P, s,x)) cs'›
have p: ‹∀i<length ?map. fst (?map!i) = EWhile b P› by (simp add: case_prod_unfold)
have 2: ‹(EWhile b P, t,y) # map (λ(_, s,x). (EWhile b P, s,x)) cs' ∈ cpts (estran Γ)›
using equiv_aux2[OF p] .
from cpts_append[OF 1 2] have 3: ‹map (lift_seq_esconf (EWhile b P)) ((P, s,x) # cs) @ (EWhile b P, t,y) # map (λ(_, s,x). (EWhile b P, s,x)) cs' ∈ cpts (estran Γ)› .
from CptsModWhileTOneFull(2,3) all_fin_after_fin no_estran_from_fin have ‹P≠fin›
by (metis last_in_set list.distinct(1) prod.collapse set_ConsD)
show ?case
apply simp
apply(rule CptsComp)
apply(simp add: estran_def) apply (rule exI) apply(rule EWhileT) apply(rule ‹s∈b›)
apply(rule ‹P≠fin›)
using 3[simplified] .
qed
qed
qed
lemma ctran_imp_not_etran:
‹(c1,c2)∈estran Γ ⟹ ¬ c1 ─e→ c2›
apply (simp add: estran_def)
apply(erule exE)
using no_estran_to_self by (metis prod.collapse)
fun split :: ‹('l,'k,'s,'prog) escpt ⇒ ('l,'k,'s,'prog) escpt × ('l,'k,'s,'prog) escpt› where
‹split ((P ⋈ Q, s) # rest) = ((P,s) # fst (split rest), (Q,s) # snd (split rest))› |
‹split _ = ([],[])›
inductive_cases estran_all_cases: ‹(P ⋈ Q, s) # (R, t) # cs ∈ cpts_es_mod Γ›
lemma split_same_length:
‹length (fst (split cpt)) = length (snd (split cpt))›
by (induct cpt rule: split.induct) auto
lemma split_same_state1:
‹i < length (fst (split cpt)) ⟹ snd (fst (split cpt) ! i) = snd (cpt ! i)›
apply (induct cpt arbitrary: i rule: split.induct, auto)
apply(case_tac i; simp)
done
lemma split_same_state2:
‹i < length (snd (split cpt)) ⟹ snd (snd (split cpt) ! i) = snd (cpt ! i)›
apply (induct cpt arbitrary: i rule: split.induct, auto)
apply(case_tac i; simp)
done
lemma split_length_le1:
‹length (fst (split cpt)) ≤ length cpt›
by (induct cpt rule: split.induct, auto)
lemma split_length_le2:
‹length (snd (split cpt)) ≤ length cpt›
by (induct cpt rule: split.induct, auto)
lemma all_neq1[simp]: ‹P ⋈ Q ≠ P›
proof
assume ‹P ⋈ Q = P›
then have ‹es_size (P ⋈ Q) = es_size P› by simp
then show False by simp
qed
lemma all_neq2[simp]: ‹P ⋈ Q ≠ Q›
proof
assume ‹P ⋈ Q = Q›
then have ‹es_size (P ⋈ Q) = es_size Q› by simp
then show False by simp
qed
lemma split_cpt_aux1:
‹((P ⋈ Q, s0), fin, t) ∈ estran Γ ⟹ P = fin ∧ Q = fin›
apply(simp add: estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
done
lemma split_cpt_aux3:
‹((P ⋈ Q, s), (R, t)) ∈ estran Γ ⟹
R ≠ fin ⟹
∃P' Q'. R = P' ⋈ Q' ∧ (P = P' ∧ ((Q,s),(Q',t)) ∈ estran Γ ∨ Q = Q' ∧ ((P,s),(P',t)) ∈ estran Γ)›
proof-
assume ‹((P ⋈ Q, s), (R, t)) ∈ estran Γ›
with estran_def obtain a where h: ‹Γ ⊢ (P ⋈ Q, s) ─es[a]→ (R, t)› by blast
assume ‹R ≠ fin›
with h show ?thesis apply- by (erule estran_p.cases, auto simp add: estran_def)
qed
lemma split_cpt:
assumes cpt_from:
‹cpt ∈ cpts_from (estran Γ) (P ⋈ Q, s0)›
shows
‹fst (split cpt) ∈ cpts_from (estran Γ) (P, s0) ∧
snd (split cpt) ∈ cpts_from (estran Γ) (Q, s0)›
proof-
from cpt_from have cpt: ‹cpt ∈ cpts (estran Γ)› and hd_cpt: ‹hd cpt = (P ⋈ Q, s0)› by auto
show ?thesis using cpt hd_cpt
proof(induct arbitrary: P Q s0)
case (CptsOne)
then show ?case
apply(simp add: split_def)
apply(rule conjI; rule cpts.CptsOne)
done
next
case (CptsEnv)
then show ?case
apply(simp add: split_def)
apply(rule conjI; rule cpts.CptsEnv, simp)
done
next
case (CptsComp P1 S Q1 T cs)
show ?case
proof(cases ‹Q1 = fin›)
case True
with CptsComp show ?thesis
apply(simp add: split_def)
apply(drule split_cpt_aux1)
apply clarify
apply(rule conjI; rule CptsOne)
done
next
case False
with CptsComp show ?thesis
apply(simp add: split_def)
apply(rule conjI)
apply(drule split_cpt_aux3, assumption)
apply clarify
apply simp
apply(erule disjE)
apply simp
apply(rule CptsEnv) using surjective_pairing apply metis
apply clarify
apply (rule cpts.CptsComp, assumption)
apply simp
using surjective_pairing apply metis
apply(drule split_cpt_aux3) apply assumption
apply clarsimp
apply(erule disjE)
apply clarify
apply(rule cpts.CptsComp, assumption)
using surjective_pairing apply metis
apply clarify
apply(rule CptsEnv)
using surjective_pairing apply metis
done
qed
qed
qed
lemma estran_from_all_both_fin:
‹Γ ⊢ (fin ⋈ fin, s) ─es[a]→ (Q1, t) ⟹ Q1 = fin›
apply(erule estran_p.cases, auto)
using no_estran_from_fin apply blast+
done
lemma estran_from_all:
‹Γ ⊢ (P ⋈ Q, s) ─es[a]→ (Q1, t) ⟹ ¬ (P = fin ∧ Q = fin) ⟹ ∃P' Q'. Q1 = P' ⋈ Q'›
by (erule estran_p.cases, auto)
lemma all_fin_after_fin':
‹(fin, s) # cs ∈ cpts (estran Γ) ⟹ i < Suc (length cs) ⟹ fst (((fin,s)#cs)!i) = fin›
apply(cases i) apply simp
using all_fin_after_fin by fastforce
lemma all_fin_after_fin'':
assumes cpt: ‹cpt ∈ cpts (estran Γ)›
and i_lt: ‹i < length cpt›
and fin: ‹fst (cpt!i) = fin›
shows ‹∀j. j > i ⟶ j < length cpt ⟶ fst (cpt!j) = fin›
proof(auto)
have ‹drop i cpt = cpt!i # drop (Suc i) cpt›
by (simp add: Cons_nth_drop_Suc i_lt)
then have ‹drop i cpt = (fst (cpt!i), snd (cpt!i)) # drop (Suc i) cpt›
using surjective_pairing by simp
with fin have 1: ‹drop i cpt = (fin, snd (cpt!i)) # drop (Suc i) cpt› by simp
from cpts_drop[OF cpt i_lt] have ‹drop i cpt ∈ cpts (estran Γ)› .
with 1 have 2: ‹(fin, snd (cpt!i)) # drop (Suc i) cpt ∈ cpts (estran Γ)› by simp
fix j
assume ‹i < j›
assume ‹j < length cpt›
have ‹j-i < Suc (length (drop (Suc i) cpt))›
by (simp add: Suc_diff_Suc ‹i < j› ‹j < length cpt› diff_less_mono i_lt less_imp_le)
from all_fin_after_fin'[OF 2 this] 1 have ‹fst (drop i cpt ! (j-i)) = fin› by simp
then show ‹fst (cpt!j) = fin›
apply(subst (asm) nth_drop) using i_lt apply linarith
using ‹i<j› by simp
qed
lemma estran_from_fin_AND_fin:
‹((fin ⋈ fin, s), Q1, t) ∈ estran Γ ⟹ Q1 = fin›
apply(simp add: estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
using no_estran_from_fin by blast+
lemma split_etran_aux:
‹P1 = P ⋈ Q ⟹ ((P1,s),(Q1,t)) ∈ estran Γ ⟹ (Q1,t)#cs ∈ cpts (estran Γ) ⟹ Suc i < length ((P1, s) # (Q1, t) # cs) ⟹ fst (((P1, s) # (Q1, t) # cs) ! Suc i) ≠ fin ⟹ ∃P' Q'. Q1 = P' ⋈ Q'›
apply(cases ‹P = fin ∧ Q = fin›)
apply simp
apply(drule estran_from_fin_AND_fin)
apply simp
using all_fin_after_fin' apply blast
apply(simp add: estran_def)
apply(erule exE)
using estran_from_all by blast
lemma split_etran:
assumes cpt: "cpt ∈ cpts (estran Γ)"
assumes fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
assumes Suc_i_lt: "Suc i < length cpt"
assumes etran: "cpt!i ─e→ cpt!Suc i"
assumes not_fin: ‹fst (cpt!Suc i) ≠ fin›
shows
"fst (split cpt) ! i ─e→ fst (split cpt) ! Suc i ∧
snd (split cpt) ! i ─e→ snd (split cpt) ! Suc i"
using cpt fst_hd_cpt Suc_i_lt etran not_fin
proof(induct arbitrary:P Q i)
case (CptsOne P s)
then show ?case by simp
next
case (CptsEnv P1 t cs s)
show ?case
proof(cases i)
case 0
with CptsEnv show ?thesis by simp
next
case (Suc i')
from CptsEnv(3) have 1:
‹fst (hd ((P1, t) # cs)) = P ⋈ Q› by simp
then have P1_conv: ‹P1 = P ⋈ Q› by simp
from Suc ‹Suc i < length ((P1, s) # (P1, t) # cs)› have 2: ‹Suc i' < length ((P1,t)#cs)› by simp
from Suc ‹((P1, s) # (P1, t) # cs) ! i ─e→ ((P1, s) # (P1, t) # cs) ! Suc i› have 3:
‹((P1, t) # cs) ! i' ─e→ ((P1, t) # cs) ! Suc i'› by simp
from CptsEnv(6) Suc have 4: ‹fst (((P1, t) # cs) ! Suc i') ≠ fin› by simp
have
‹fst (split ((P1, t) # cs)) ! i' ─e→ fst (split ((P1, t) # cs)) ! Suc i' ∧
snd (split ((P1, t) # cs)) ! i' ─e→ snd (split ((P1, t) # cs)) ! Suc i'›
by (rule CptsEnv(2)[OF 1 2 3 4])
with Suc P1_conv show ?thesis by simp
qed
next
case (CptsComp P1 s Q1 t cs)
show ?case
proof(cases i)
case 0
with CptsComp show ?thesis using no_estran_to_self' by auto
next
case (Suc i')
from CptsComp(4) have 1: ‹P1 = P ⋈ Q› by simp
have ‹∃P' Q'. Q1 = P' ⋈ Q'› using split_etran_aux[OF 1 CptsComp(1) CptsComp(2)] CptsComp(5,7) by force
then obtain P' Q' where 2: ‹Q1 = P' ⋈ Q'› by blast
from 2 have 3: ‹fst (hd ((Q1, t) # cs)) = P' ⋈ Q'› by simp
from CptsComp(5) Suc have 4: ‹Suc i' < length ((Q1,t)#cs)› by simp
from CptsComp(6) Suc have 5: ‹((Q1, t) # cs) ! i' ─e→ ((Q1, t) # cs) ! Suc i'› by simp
from CptsComp(7) Suc have 6: ‹fst (((Q1, t) # cs) ! Suc i') ≠ fin› by simp
have
‹fst (split ((Q1, t) # cs)) ! i' ─e→ fst (split ((Q1, t) # cs)) ! Suc i' ∧
snd (split ((Q1, t) # cs)) ! i' ─e→ snd (split ((Q1, t) # cs)) ! Suc i'›
by (rule CptsComp(3)[OF 3 4 5 6])
with Suc 1 show ?thesis by simp
qed
qed
lemma all_join_aux:
‹(c1, c2) ∈ estran Γ ⟹
fst c1 = P ⋈ Q ⟹
fst c2 ≠ fin ⟹
∃P' Q'. fst c2 = P' ⋈ Q'›
apply(simp add: estran_def, erule exE)
apply(erule estran_p.cases, auto)
done
lemma all_join:
‹cpt ∈ cpts (estran Γ) ⟹
fst (hd cpt) = P ⋈ Q ⟹
n < length cpt ⟹
fst (cpt!n) ≠ fin ⟹
∀i ≤ n. ∃P' Q'. fst (cpt!i) = P' ⋈ Q'›
proof-
assume cpt: ‹cpt ∈ cpts (estran Γ)›
with cpts_nonnil have ‹cpt≠[]› by blast
from cpt cpts_def' have ct_or_et:
‹∀i. Suc i < length cpt ⟶ (cpt!i, cpt!Suc i) ∈ estran Γ ∨ cpt!i ─e→ cpt!Suc i› by blast
assume fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
assume n_lt: ‹n < length cpt›
assume not_fin: ‹fst (cpt!n) ≠ fin›
show ‹∀i ≤ n. ∃P' Q'. fst (cpt!i) = P' ⋈ Q'›
proof
fix i
show ‹i ≤ n ⟶ (∃P' Q'. fst (cpt!i) = P' ⋈ Q')›
proof(induct i)
case 0
then show ?case
apply(rule impI)
apply(rule exI)+
apply(subst hd_conv_nth[THEN sym])
apply(rule ‹cpt≠[]›)
apply(rule fst_hd_cpt)
done
next
case (Suc i)
show ?case
proof
assume Suc_i_le: ‹Suc i ≤ n›
then have ‹i ≤ n› by simp
with Suc obtain P' Q' where fst_cpt_i: ‹fst (cpt ! i) = P' ⋈ Q'› by blast
from Suc_i_le n_lt have Suc_i_lt: ‹Suc i < length cpt› by linarith
have ‹Suc i < length cpt ⟶ (cpt ! i, cpt ! Suc i) ∈ estran Γ ∨ cpt ! i ─e→ cpt ! Suc i›
by (rule ct_or_et[THEN spec[where x=i]])
with Suc_i_lt have ct_or_et':
‹(cpt ! i, cpt ! Suc i) ∈ estran Γ ∨ cpt ! i ─e→ cpt ! Suc i› by blast
then show ‹∃P' Q'. fst (cpt ! Suc i) = P' ⋈ Q'›
proof
assume ctran: ‹(cpt ! i, cpt ! Suc i) ∈ estran Γ›
show ‹∃P' Q'. fst (cpt ! Suc i) = P' ⋈ Q'›
proof(cases ‹fst (cpt!Suc i) = fin›)
case True
have 1: ‹(fin, snd (cpt!Suc i)) # drop (Suc (Suc i)) cpt ∈ cpts (estran Γ)›
proof-
have cpt_Suc_i: ‹cpt!Suc i = (fin, snd (cpt!Suc i))›
apply(subst True[THEN sym]) by simp
moreover have ‹drop (Suc i) cpt ∈ cpts (estran Γ)› by (rule cpts_drop[OF cpt Suc_i_lt])
ultimately show ?thesis
by (simp add: Cons_nth_drop_Suc Suc_i_lt)
qed
let ?cpt' = ‹drop (Suc (Suc i)) cpt›
have ‹∀c∈set ?cpt'. fst c = fin› by (rule all_fin_after_fin[OF 1])
then have ‹∀j<length ?cpt'. fst (?cpt'!j) = fin› using nth_mem by blast
then have all_fin: ‹∀j. Suc (Suc i) + j < length cpt ⟶ fst (cpt!(Suc (Suc i) + j)) = fin› by auto
have ‹fst (cpt!n) = fin›
proof(cases ‹Suc i = n›)
case True
then show ?thesis using ‹fst (cpt ! Suc i) = fin› by simp
next
case False
with ‹Suc i ≤ n› have ‹Suc (Suc i) ≤ n› by linarith
then show ?thesis using all_fin n_lt le_Suc_ex by blast
qed
with not_fin have False by blast
then show ?thesis by blast
next
case False
from Suc ‹i≤n› obtain P' Q' where 1: ‹fst (cpt ! i) = P' ⋈ Q'› by blast
show ?thesis by (rule all_join_aux[OF ctran 1 False])
qed
next
assume etran: ‹cpt ! i ─e→ cpt ! Suc i›
then show ‹∃P' Q'. fst (cpt ! Suc i) = P' ⋈ Q'›
apply simp
using fst_cpt_i by metis
qed
qed
qed
qed
qed
lemma all_join_aux':
‹fst (cpt ! m) = fin ⟹ length (fst (split cpt)) ≤ m ∧ length (snd (split cpt)) ≤ m›
apply(induct cpt arbitrary:m rule:split.induct; simp)
apply(case_tac m; simp)
done
lemma all_join1:
‹∀i < length (fst (split cpt)). ∃P' Q'. fst (cpt!i) = P' ⋈ Q'›
apply(induct cpt rule:split.induct, auto)
apply(case_tac i; simp)
done
lemma all_join2:
‹∀i < length (snd (split cpt)). ∃P' Q'. fst (cpt!i) = P' ⋈ Q'›
apply(induct cpt rule:split.induct, auto)
apply(case_tac i; simp)
done
lemma split_length:
‹cpt ∈ cpts (estran Γ) ⟹
fst (hd cpt) = P ⋈ Q ⟹
Suc m < length cpt ⟹
fst (cpt ! m) ≠ fin ⟹
fst (cpt ! Suc m) = fin ⟹
length (fst (split cpt)) = Suc m ∧ length (snd (split cpt)) = Suc m›
proof(induct cpt arbitrary: P Q m rule: split.induct; simp)
fix P Q s Pa Qa m
fix rest
assume IH:
‹⋀P Q m.
rest ∈ cpts (estran Γ) ⟹
fst (hd rest) = P ⋈ Q ⟹
Suc m < length rest ⟹ fst (rest ! m) ≠ fin ⟹ fst (rest ! Suc m) = fin ⟹ length (fst (split rest)) = Suc m ∧ length (snd (split rest)) = Suc m›
assume a1: ‹(Pa ⋈ Qa, s) # rest ∈ cpts (estran Γ)›
assume a2: ‹m < length rest›
then have ‹rest≠[]› by fastforce
from cpts_tl[OF a1] this have 1: ‹rest ∈ cpts (estran Γ)› by simp
assume a3: ‹fst (((Pa ⋈ Qa, s) # rest) ! m) ≠ fin›
from all_join[OF a1] a2 a3 have 2: ‹∀i≤m. ∃P' Q'. fst (((Pa ⋈ Qa, s) # rest) ! i) = P' ⋈ Q'›
by (metis fstI length_Cons less_SucI list.sel(1))
assume a4: ‹fst (rest ! m) = fin›
show ‹length (fst (split rest)) = m ∧ length (snd (split rest)) = m›
proof(cases ‹m=0›)
case True
with a4 have ‹fst (rest ! 0) = fin› by simp
with hd_conv_nth[OF ‹rest≠[]›] have ‹fst (hd rest) = fin› by simp
then obtain t where ‹hd rest = (fin,t)› using surjective_pairing by metis
then have ‹rest = (fin,t) # tl rest› using hd_Cons_tl[OF ‹rest≠[]›] by simp
then have ‹split rest = ([],[])› apply- apply(erule ssubst) by simp
then show ?thesis using True by simp
next
case False
then have ‹m≥1› by fastforce
from 2[rule_format, of 1, OF this] obtain P' Q' where ‹fst (((Pa ⋈ Qa, s) # rest) ! 1) = P' ⋈ Q'› by blast
with hd_conv_nth[OF ‹rest≠[]›] have fst_hd_rest: ‹fst (hd rest) = P' ⋈ Q'› by simp
from not0_implies_Suc[OF False] obtain m' where m': ‹m = Suc m'› by blast
from a2 m' have Suc_m'_lt: ‹Suc m' < length rest› by simp
from a3 m' have not_fin: ‹fst (rest ! m') ≠ fin› by simp
from a4 m' have fin: ‹fst (rest ! Suc m') = fin› by simp
from IH[OF 1 fst_hd_rest Suc_m'_lt not_fin fin] m' show ?thesis by simp
qed
qed
lemma split_prog1:
‹i < length (fst (split cpt)) ⟹ fst (cpt!i) = P ⋈ Q ⟹ fst (fst (split cpt) ! i) = P›
apply(induct cpt arbitrary:i rule:split.induct, auto)
apply(case_tac i; simp)
done
lemma split_prog2:
‹i < length (snd (split cpt)) ⟹ fst (cpt!i) = P ⋈ Q ⟹ fst (snd (split cpt) ! i) = Q›
apply(induct cpt arbitrary:i rule:split.induct, auto)
apply(case_tac i; simp)
done
lemma split_ctran_aux:
‹((P ⋈ Q, s), P' ⋈ Q', t) ∈ estran Γ ⟹
((P, s), P', t) ∈ estran Γ ∧ Q = Q' ∨ ((Q, s), Q', t) ∈ estran Γ ∧ P = P'›
apply(simp add: estran_def, erule exE)
apply(erule estran_p.cases, auto)
done
lemma split_ctran:
assumes cpt: "cpt ∈ cpts (estran Γ)"
assumes fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
assumes not_fin : ‹fst (cpt!Suc i) ≠ fin›
assumes Suc_i_lt: "Suc i < length cpt"
assumes ctran: "(cpt!i, cpt!Suc i) ∈ estran Γ"
shows
‹(fst (split cpt) ! i, fst (split cpt) ! Suc i) ∈ estran Γ ∧ snd (split cpt) ! i ─e→ snd (split cpt) ! Suc i ∨
(snd (split cpt) ! i, snd (split cpt) ! Suc i) ∈ estran Γ ∧ fst (split cpt) ! i ─e→ fst (split cpt) ! Suc i›
proof-
have all_All': ‹∀j≤Suc i. ∃P' Q'. fst (cpt ! j) = P' ⋈ Q'› by (rule all_join[OF cpt fst_hd_cpt Suc_i_lt not_fin])
show ?thesis
using cpt fst_hd_cpt Suc_i_lt ctran all_All'
proof(induct arbitrary:P Q i)
case (CptsOne P s)
then show ?case by simp
next
case (CptsEnv P1 t cs s)
from CptsEnv(3) have 1: ‹fst (hd ((P1, t) # cs)) = P ⋈ Q› by simp
show ?case
proof(cases i)
case 0
with CptsEnv show ?thesis
apply (simp add: split_def)
using no_estran_to_self' by blast
next
case (Suc i')
with CptsEnv have
‹(fst (split ((P1, t) # cs)) ! i', fst (split ((P1, t) # cs)) ! Suc i') ∈ estran Γ ∧ snd (split ((P1, t) # cs)) ! i' ─e→ snd (split ((P1, t) # cs)) ! Suc i' ∨
(snd (split ((P1, t) # cs)) ! i', snd (split ((P1, t) # cs)) ! Suc i') ∈ estran Γ ∧ fst (split ((P1, t) # cs)) ! i' ─e→ fst (split ((P1, t) # cs)) ! Suc i'›
by fastforce
then show ?thesis using Suc 1 by simp
qed
next
case (CptsComp P1 s Q1 t cs)
from CptsComp(7)[THEN spec[where x=1]] obtain P' Q' where Q1: ‹Q1 = P' ⋈ Q'› by auto
show ?case
proof(cases i)
case 0
with Q1 CptsComp show ?thesis
apply(simp add: split_def)
using split_ctran_aux by fast
next
case (Suc i')
from Q1 have 1: ‹fst (hd ((Q1, t) # cs)) = P' ⋈ Q'› by simp
from CptsComp(5) Suc have 2: ‹Suc i' < length ((Q1, t) # cs)› by simp
from CptsComp(6) Suc have 3: ‹(((Q1, t) # cs) ! i', ((Q1, t) # cs) ! Suc i') ∈ estran Γ› by simp
from CptsComp(7) Suc have 4: ‹∀j≤Suc i'. ∃P' Q'. fst (((Q1, t) # cs) ! j) = P' ⋈ Q'› by auto
have
‹(fst (split ((Q1, t) # cs)) ! i', fst (split ((Q1, t) # cs)) ! Suc i') ∈ estran Γ ∧ snd (split ((Q1, t) # cs)) ! i' ─e→ snd (split ((Q1, t) # cs)) ! Suc i' ∨
(snd (split ((Q1, t) # cs)) ! i', snd (split ((Q1, t) # cs)) ! Suc i') ∈ estran Γ ∧ fst (split ((Q1, t) # cs)) ! i' ─e→ fst (split ((Q1, t) # cs)) ! Suc i'›
by (rule CptsComp(3)[OF 1 2 3 4])
with Suc CptsComp(4) show ?thesis by simp
qed
qed
qed
lemma etran_imp_not_ctran:
‹c1 ─e→ c2 ⟹ ¬((c1,c2) ∈ estran Γ)›
using no_estran_to_self'' by fastforce
lemma split_etran1_aux:
‹((P' ⋈ Q, s), P' ⋈ Q', t) ∈ estran Γ ⟹ P = P' ⟹ ((Q, s), Q', t) ∈ estran Γ›
apply(simp add: estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
using no_estran_to_self by blast
lemma split_etran1:
assumes cpt: ‹cpt ∈ cpts (estran Γ)›
and fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
and Suc_i_lt: ‹Suc i < length cpt›
and not_fin: ‹fst (cpt ! Suc i) ≠ fin›
and etran: ‹fst (split cpt) ! i ─e→ fst (split cpt) ! Suc i›
shows
‹cpt ! i ─e→ cpt ! Suc i ∨
(snd (split cpt) ! i, snd (split cpt) ! Suc i) ∈ estran Γ›
proof-
have all_All': ‹∀j≤Suc i. ∃P' Q'. fst (cpt ! j) = P' ⋈ Q'›
by (rule all_join[OF cpt fst_hd_cpt Suc_i_lt not_fin])
show ?thesis
using cpt fst_hd_cpt Suc_i_lt not_fin etran all_All'
proof(induct arbitrary:P Q i)
case (CptsOne P s)
then show ?case by simp
next
case (CptsEnv P1 t cs s)
show ?case
proof(cases i)
case 0
then show ?thesis by simp
next
case (Suc i')
from CptsEnv(3) have 1: ‹fst (hd ((P1, t) # cs)) = P ⋈ Q› by simp
then have P1: ‹P1 = P ⋈ Q› by simp
from CptsEnv(4) Suc have 2: ‹Suc i' < length ((P1, t) # cs)› by simp
from CptsEnv(5) Suc have 3: ‹fst (((P1, t) # cs) ! Suc i') ≠ fin› by simp
from CptsEnv(6) Suc P1
have 4: ‹fst (split ((P1, t) # cs)) ! i' ─e→ fst (split ((P1, t) # cs)) ! Suc i'› by simp
from CptsEnv(7) Suc have 5: ‹∀j≤Suc i'. ∃P' Q'. fst (((P1, t) # cs) ! j) = P' ⋈ Q'› by auto
from CptsEnv(2)[OF 1 2 3 4 5]
have ‹((P1, t) # cs) ! i' ─e→ ((P1, t) # cs) ! Suc i' ∨ (snd (split ((P1, t) # cs)) ! i', snd (split ((P1, t) # cs)) ! Suc i') ∈ estran Γ› .
then show ?thesis using Suc P1 by simp
qed
next
case (CptsComp P1 s Q1 t cs)
from CptsComp(4) have P1: ‹P1 = P ⋈ Q› by simp
from CptsComp(8)[THEN spec[where x=1]] obtain P' Q' where Q1: ‹Q1 = P' ⋈ Q'› by auto
show ?case
proof(cases i)
case 0
with P1 Q1 CptsComp(1) CptsComp(7) show ?thesis
apply (simp add: split_def)
apply(rule disjI2)
apply(erule split_etran1_aux, assumption)
done
next
case (Suc i')
have 1: ‹fst (hd ((Q1, t) # cs)) = P' ⋈ Q'› using Q1 by simp
from CptsComp(5) Suc have 2: ‹Suc i' < length ((Q1, t) # cs)› by simp
from CptsComp(6) Suc have 3: ‹fst (((Q1, t) # cs) ! Suc i') ≠ fin› by simp
from CptsComp(7) Suc P1 have 4: ‹fst (split ((Q1, t) # cs)) ! i' ─e→ fst (split ((Q1, t) # cs)) ! Suc i'› by simp
from CptsComp(8) Suc have 5: ‹∀j≤Suc i'. ∃P' Q'. fst (((Q1, t) # cs) ! j) = P' ⋈ Q'› by auto
from CptsComp(3)[OF 1 2 3 4 5]
have ‹((Q1, t) # cs) ! i' ─e→ ((Q1, t) # cs) ! Suc i' ∨ (snd (split ((Q1, t) # cs)) ! i', snd (split ((Q1, t) # cs)) ! Suc i') ∈ estran Γ› .
then show ?thesis using Suc P1 by simp
qed
qed
qed
lemma split_etran2_aux:
‹((P ⋈ Q', s), P' ⋈ Q', t) ∈ estran Γ ⟹ Q = Q' ⟹ ((P, s), P', t) ∈ estran Γ›
apply(simp add: estran_def)
apply(erule exE)
apply(erule estran_p.cases, auto)
using no_estran_to_self by blast
lemma split_etran2:
assumes cpt: ‹cpt ∈ cpts (estran Γ)›
and fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
and Suc_i_lt: ‹Suc i < length cpt›
and not_fin: ‹fst (cpt ! Suc i) ≠ fin›
and etran: ‹snd (split cpt) ! i ─e→ snd (split cpt) ! Suc i›
shows
‹cpt ! i ─e→ cpt ! Suc i ∨
(fst (split cpt) ! i, fst (split cpt) ! Suc i) ∈ estran Γ›
proof-
have all_All': ‹∀j≤Suc i. ∃P' Q'. fst (cpt ! j) = P' ⋈ Q'›
by (rule all_join[OF cpt fst_hd_cpt Suc_i_lt not_fin])
show ?thesis
using cpt fst_hd_cpt Suc_i_lt not_fin etran all_All'
proof(induct arbitrary:P Q i)
case (CptsOne P s)
then show ?case by simp
next
case (CptsEnv P1 t cs s)
show ?case
proof(cases i)
case 0
then show ?thesis by simp
next
case (Suc i')
from CptsEnv(3) have 1: ‹fst (hd ((P1, t) # cs)) = P ⋈ Q› by simp
then have P1: ‹P1 = P ⋈ Q› by simp
from CptsEnv(4) Suc have 2: ‹Suc i' < length ((P1, t) # cs)› by simp
from CptsEnv(5) Suc have 3: ‹fst (((P1, t) # cs) ! Suc i') ≠ fin› by simp
from CptsEnv(6) Suc P1 have 4: ‹snd (split ((P1, t) # cs)) ! i' ─e→ snd (split ((P1, t) # cs)) ! Suc i'› by simp
from CptsEnv(7) Suc have 5: ‹∀j≤Suc i'. ∃P' Q'. fst (((P1, t) # cs) ! j) = P' ⋈ Q'› by auto
have ‹((P1, t) # cs) ! i' ─e→ ((P1, t) # cs) ! Suc i' ∨ (fst (split ((P1, t) # cs)) ! i', fst (split ((P1, t) # cs)) ! Suc i') ∈ estran Γ›
by (rule CptsEnv(2)[OF 1 2 3 4 5])
then show ?thesis using Suc P1 by simp
qed
next
case (CptsComp P1 s Q1 t cs)
from CptsComp(4) have P1: ‹P1 = P ⋈ Q› by simp
from CptsComp(8)[THEN spec[where x=1]] obtain P' Q' where Q1: ‹Q1 = P' ⋈ Q'› by auto
show ?case
proof(cases i)
case 0
with P1 Q1 CptsComp(1) CptsComp(7) show ?thesis
apply (simp add: split_def)
apply(rule disjI2)
apply(erule split_etran2_aux, assumption)
done
next
case (Suc i')
have 1: ‹fst (hd ((Q1, t) # cs)) = P' ⋈ Q'› using Q1 by simp
from CptsComp(5) Suc have 2: ‹Suc i' < length ((Q1, t) # cs)› by simp
from CptsComp(6) Suc have 3: ‹fst (((Q1, t) # cs) ! Suc i') ≠ fin› by simp
from CptsComp(7) Suc P1 have 4: ‹snd (split ((Q1, t) # cs)) ! i' ─e→ snd (split ((Q1, t) # cs)) ! Suc i'› by simp
from CptsComp(8) Suc have 5: ‹∀j≤Suc i'. ∃P' Q'. fst (((Q1, t) # cs) ! j) = P' ⋈ Q'› by auto
have ‹((Q1, t) # cs) ! i' ─e→ ((Q1, t) # cs) ! Suc i' ∨ (fst (split ((Q1, t) # cs)) ! i', fst (split ((Q1, t) # cs)) ! Suc i') ∈ estran Γ›
by (rule CptsComp(3)[OF 1 2 3 4 5])
then show ?thesis using Suc P1 by simp
qed
qed
qed
lemma split_ctran1_aux:
‹i < length (fst (split cpt)) ⟹
fst (cpt!i) ≠ fin›
apply(induct cpt arbitrary: i rule: split.induct, auto)
apply(case_tac i; simp)
done
lemma split_ctran1:
‹cpt ∈ cpts (estran Γ) ⟹
fst (hd cpt) = P ⋈ Q ⟹
Suc i < length (fst (split cpt)) ⟹
(fst (split cpt) ! i, fst (split cpt) ! Suc i) ∈ estran Γ ⟹
(cpt!i, cpt!Suc i) ∈ estran Γ›
proof(rule ccontr)
assume cpt: ‹cpt ∈ cpts (estran Γ)›
assume fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
assume Suc_i_lt1: ‹Suc i < length (fst (split cpt))›
with split_length_le1[of cpt]
have Suc_i_lt: ‹Suc i < length cpt› by fastforce
assume ctran1: ‹(fst (split cpt) ! i, fst (split cpt) ! Suc i) ∈ estran Γ›
assume ‹(cpt ! i, cpt ! Suc i) ∉ estran Γ›
with ctran_or_etran[OF cpt Suc_i_lt] have etran: ‹cpt!i ─e→ cpt!Suc i› by blast
from split_ctran1_aux[OF Suc_i_lt1] have ‹fst (cpt ! Suc i) ≠ fin› .
from split_etran[OF cpt fst_hd_cpt Suc_i_lt etran this, THEN conjunct1] have ‹fst (split cpt) ! i ─e→ fst (split cpt) ! Suc i› .
with ctran1 no_estran_to_self'' show False by fastforce
qed
lemma split_ctran2_aux:
‹i < length (snd (split cpt)) ⟹
fst (cpt!i) ≠ fin›
apply(induct cpt arbitrary: i rule: split.induct, auto)
apply(case_tac i; simp)
done
lemma split_ctran2:
‹cpt ∈ cpts (estran Γ) ⟹
fst (hd cpt) = P ⋈ Q ⟹
Suc i < length (snd (split cpt)) ⟹
(snd (split cpt) ! i, snd (split cpt) ! Suc i) ∈ estran Γ ⟹
(cpt!i, cpt!Suc i) ∈ estran Γ›
proof(rule ccontr)
assume cpt: ‹cpt ∈ cpts (estran Γ)›
assume fst_hd_cpt: ‹fst (hd cpt) = P ⋈ Q›
assume Suc_i_lt2: ‹Suc i < length (snd (split cpt))›
with split_length_le2[of cpt]
have Suc_i_lt: ‹Suc i < length cpt› by fastforce
assume ctran2: ‹(snd (split cpt) ! i, snd (split cpt) ! Suc i) ∈ estran Γ›
assume ‹(cpt ! i, cpt ! Suc i) ∉ estran Γ›
with ctran_or_etran[OF cpt Suc_i_lt] have etran: ‹cpt!i ─e→ cpt!Suc i› by blast
from split_ctran2_aux[OF Suc_i_lt2] have ‹fst (cpt ! Suc i) ≠ fin› .
from split_etran[OF cpt fst_hd_cpt Suc_i_lt etran this, THEN conjunct2] have ‹snd (split cpt) ! i ─e→ snd (split cpt) ! Suc i› .
with ctran2 no_estran_to_self'' show False by fastforce
qed
lemma no_fin_before_non_fin:
assumes cpt: ‹cpt ∈ cpts (estran Γ)›
and m_lt: ‹m < length cpt›
and m_not_fin: "fst (cpt!m) ≠ fin"
and ‹i≤m›
shows ‹fst (cpt!i) ≠ fin›
proof(rule ccontr, simp)
assume i_fin: ‹fst (cpt!i) = fin›
from m_lt ‹i≤m› have i_lt: ‹i < length cpt› by simp
from cpts_drop[OF cpt this] have ‹drop i cpt ∈ cpts (estran Γ)› by assumption
have 1: ‹drop i cpt = (fin, snd (cpt!i)) # drop (Suc i) cpt› using i_fin i_lt
by (metis Cons_nth_drop_Suc surjective_pairing)
from cpts_drop[OF cpt i_lt] have ‹drop i cpt ∈ cpts (estran Γ)› by assumption
with 1 have ‹(fin, snd (cpt!i)) # drop (Suc i) cpt ∈ cpts (estran Γ)› by simp
from all_fin_after_fin[OF this] have ‹∀c∈set (drop (Suc i) cpt). fst c = fin› by assumption
then have ‹∀j<length (drop (Suc i) cpt). fst (drop (Suc i) cpt ! j) = fin› using nth_mem by blast
then have 2: ‹∀j. Suc i + j < length cpt ⟶ fst (cpt ! (Suc i + j)) = fin› by simp
find_theorems nth drop
show False
proof(cases ‹i=m›)
case True
then show False using m_not_fin i_fin by simp
next
case False
with ‹i≤m› have ‹i<m› by simp
with 2 m_not_fin show False
using Suc_leI le_Suc_ex m_lt by blast
qed
qed
lemma no_estran_from_fin':
‹(c1, c2) ∈ estran Γ ⟹ fst c1 ≠ fin›
apply(simp add: estran_def)
apply(subst (asm) surjective_pairing[of c1])
using no_estran_from_fin by metis
subsection ‹Compositionality of the Semantics›
subsubsection ‹Definition of the conjoin operator›
definition same_length :: "('l,'k,'s,'prog) pesconf list ⇒ ('k ⇒ ('l,'k,'s,'prog) esconf list) ⇒ bool" where
"same_length c cs ≡ ∀k. length (cs k) = length c"
definition same_state :: "('l,'k,'s,'prog) pesconf list ⇒ ('k ⇒ ('l,'k,'s,'prog) esconf list) ⇒ bool" where
"same_state c cs ≡ ∀k j. j < length c ⟶ snd (c!j) = snd (cs k ! j)"
definition same_spec :: "('l,'k,'s,'prog) pesconf list ⇒ ('k ⇒ ('l,'k,'s,'prog) esconf list) ⇒ bool" where
"same_spec c cs ≡ ∀k j. j < length c ⟶ fst (c!j) k = fst (cs k ! j)"
definition compat_tran :: "('l,'k,'s,'prog) pesconf list ⇒ ('k ⇒ ('l,'k,'s,'prog) esconf list) ⇒ bool" where
"compat_tran c cs ≡
∀j. Suc j < length c ⟶
((∃t k Γ. (Γ ⊢ c!j ─pes[t♯k]→ c!Suc j)) ∧
(∀k t Γ. (Γ ⊢ c!j ─pes[t♯k]→ c!Suc j) ⟶
(Γ ⊢ cs k ! j ─es[t♯k]→ cs k ! Suc j) ∧ (∀k'. k' ≠ k ⟶ (cs k' ! j ─e→ cs k' ! Suc j)))) ∨
(c!j ─e→ c!Suc j ∧ (∀k. cs k ! j ─e→ cs k ! Suc j))"
definition conjoin :: "('l,'k,'s,'prog) pesconf list ⇒ ('k ⇒ ('l,'k,'s,'prog) esconf list) ⇒ bool" ("_ ∝ _" [65,65] 64) where
"c ∝ cs ≡ (same_length c cs) ∧ (same_state c cs) ∧ (same_spec c cs) ∧ (compat_tran c cs)"
subsubsection ‹Properties of the conjoin operator›
lemma conjoin_ctran:
assumes conjoin: ‹pc ∝ cs›
assumes Suc_i_lt: ‹Suc i < length pc›
assumes ctran: ‹Γ ⊢ pc!i ─pes[a♯k]→ pc!Suc i›
shows
‹(Γ ⊢ cs k ! i ─es[a♯k]→ cs k ! Suc i) ∧
(∀k'. k'≠k ⟶ (cs k' ! i ─e→ cs k' ! Suc i))›
proof-
from conjoin have ‹compat_tran pc cs› using conjoin_def by blast
then have
h: ‹∀j. Suc j < length pc ⟶
(∃t k Γ. Γ ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j) ∧
(∀k t Γ. (Γ ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j) ⟶ (Γ ⊢ cs k ! j ─es[t♯k]→ cs k ! Suc j) ∧ (∀k'. k' ≠ k ⟶ fst (cs k' ! j) = fst (cs k' ! Suc j))) ∨
fst (pc ! j) = fst (pc ! Suc j) ∧ (∀k. fst (cs k ! j) = fst (cs k ! Suc j))› by (simp add: compat_tran_def)
from ctran have ‹fst (pc ! i) ≠ fst (pc ! Suc i)› using no_pestran_to_self by (metis prod.collapse)
with h[rule_format, OF Suc_i_lt] have
‹∀k t Γ. (Γ ⊢ pc ! i ─pes[t♯k]→ pc ! Suc i) ⟶ (Γ ⊢ cs k ! i ─es[t♯k]→ cs k ! Suc i) ∧ (∀k'. k' ≠ k ⟶ fst (cs k' ! i) = fst (cs k' ! Suc i))›
by argo
from this[rule_format, OF ctran] show ?thesis by fastforce
qed
lemma conjoin_etran:
assumes conjoin: ‹pc ∝ cs›
assumes Suc_i_lt: ‹Suc i < length pc›
assumes etran: ‹pc!i ─e→ pc!Suc i›
shows ‹∀k. cs k ! i ─e→ cs k ! Suc i›
proof-
from conjoin have ‹compat_tran pc cs› using conjoin_def by blast
then have
‹∀j. Suc j < length pc ⟶
(∃t k Γ. Γ ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j) ∧
(∀k t Γ. (Γ ⊢ pc ! j ─pes[t♯k]→ pc ! Suc j) ⟶ (Γ ⊢ cs k ! j ─es[t♯k]→ cs k ! Suc j) ∧ (∀k'. k' ≠ k ⟶ fst (cs k' ! j) = fst (cs k' ! Suc j))) ∨
fst (pc ! j) = fst (pc ! Suc j) ∧ (∀k. fst (cs k ! j) = fst (cs k ! Suc j))› by (simp add: compat_tran_def)
from this[rule_format, OF Suc_i_lt] have h:
‹(∃t k Γ. Γ ⊢ pc ! i ─pes[t♯k]→ pc ! Suc i) ∧
(∀k t Γ. (Γ ⊢ pc ! i ─pes[t♯k]→ pc ! Suc i) ⟶ (Γ ⊢ cs k ! i ─es[t♯k]→ cs k ! Suc i) ∧ (∀k'. k' ≠ k ⟶ fst (cs k' ! i) = fst (cs k' ! Suc i))) ∨
fst (pc ! i) = fst (pc ! Suc i) ∧ (∀k. fst (cs k ! i) = fst (cs k ! Suc i))› by blast
from etran have ‹¬(∃t k Γ. Γ ⊢ pc ! i ─pes[t♯k]→ pc ! Suc i)› using no_pestran_to_self
by (metis (mono_tags, lifting) etran_def etran_p_def mem_Collect_eq prod.simps(2) surjective_pairing)
with h have ‹∀k. fst (cs k ! i) = fst (cs k ! Suc i)› by blast
then show ?thesis by simp
qed
lemma conjoin_cpt:
assumes pc: ‹pc ∈ cpts (pestran Γ)›
assumes conjoin: ‹pc ∝ cs›
shows ‹cs k ∈ cpts (estran Γ)›
proof-
from pc cpts_def'[of pc ‹pestran Γ›] have
‹pc ≠ []› and 1: ‹(∀i. Suc i < length pc ⟶ (pc ! i, pc ! Suc i) ∈ pestran Γ ∨ pc ! i ─e→ pc ! Suc i)›
by auto
from ‹pc≠[]› have ‹length pc ≠ 0› by simp
then have ‹length (cs k) ≠ 0› using conjoin by (simp add: conjoin_def same_length_def)
then have ‹cs k ≠ []› by simp
moreover have ‹∀i. Suc i < length (cs k) ⟶ (cs k ! i) ─e→ (cs k ! Suc i) ∨ (cs k ! i, cs k ! Suc i) ∈ estran Γ›
proof(rule allI, rule impI)
fix i
assume ‹Suc i < length (cs k)›
then have Suc_i_lt: ‹Suc i < length pc› using conjoin conjoin_def same_length_def by metis
from 1[rule_format, OF this]
have ctran_or_etran_par: ‹(pc ! i, pc ! Suc i) ∈ pestran Γ ∨ pc ! i ─e→ pc ! Suc i› by assumption
then show ‹cs k ! i ─e→ cs k ! Suc i ∨ (cs k ! i, cs k ! Suc i) ∈ estran Γ›
proof
assume ‹(pc ! i, pc ! Suc i) ∈ pestran Γ›
then have ‹∃a k. Γ ⊢ pc!i ─pes[a♯k]→ pc!Suc i› by (simp add: pestran_def)
then obtain a k' where ‹Γ ⊢ pc!i ─pes[a♯k']→ pc!Suc i› by blast
from conjoin_ctran[OF conjoin Suc_i_lt this]
have 2: ‹(Γ ⊢ cs k' ! i ─es[a♯k']→ cs k' ! Suc i) ∧ (∀k'a. k'a ≠ k' ⟶ cs k'a ! i ─e→ cs k'a ! Suc i)›
by assumption
show ?thesis
proof(cases ‹k'=k›)
case True
then show ?thesis
using 2 apply (simp add: estran_def)
apply(rule disjI2)
by auto
next
case False
then show ?thesis using 2 by simp
qed
next
assume ‹pc ! i ─e→ pc ! Suc i›
from conjoin_etran[OF conjoin Suc_i_lt this] show ?thesis
apply-
apply (rule disjI1)
by blast
qed
qed
ultimately show ‹cs k ∈ cpts (estran Γ)› using cpts_def' by blast
qed
lemma conjoin_cpt':
assumes pc: ‹pc ∈ cpts_from (pestran Γ) (Ps, s0)›
assumes conjoin: ‹pc ∝ cs›
shows ‹cs k ∈ cpts_from (estran Γ) (Ps k, s0)›
proof-
from pc have pc_cpt: ‹pc ∈ cpts (pestran Γ)› and hd_pc: ‹hd pc = (Ps, s0)› by auto
from pc_cpt cpts_nonnil have ‹pc≠[]› by blast
have ck_cpt: ‹cs k ∈ cpts (estran Γ)› using conjoin_cpt[OF pc_cpt conjoin] by assumption
moreover have ‹hd (cs k) = (Ps k, s0)›
proof-
from ck_cpt cpts_nonnil have ‹cs k ≠ []› by blast
from conjoin conjoin_def have ‹same_spec pc cs› and ‹same_state pc cs› by blast+
then show ?thesis using hd_pc ‹pc≠[]› ‹cs k ≠ []›
apply(simp add: same_spec_def same_state_def hd_conv_nth)
apply(erule allE[where x=k])
apply(erule allE[where x=0])
apply simp
by (simp add: prod_eqI)
qed
ultimately show ?thesis by auto
qed
lemma conjoin_same_length:
‹pc ∝ cs ⟹ length pc = length (cs k)›
by (simp add: conjoin_def same_length_def)
lemma conjoin_same_spec:
‹pc ∝ cs ⟹ ∀k i. i < length pc ⟶ fst (pc!i) k = fst (cs k ! i)›
by (simp add: conjoin_def same_spec_def)
lemma conjoin_same_state:
‹pc ∝ cs ⟹ ∀k i. i < length pc ⟶ snd (pc!i) = snd (cs k!i)›
by (simp add: conjoin_def same_state_def)
lemma conjoin_all_etran:
assumes conjoin: ‹pc ∝ cs›
and Suc_i_lt: ‹Suc i < length pc›
and all_etran: ‹∀k. cs k ! i ─e→ cs k ! Suc i›
shows ‹pc!i ─e→ pc!Suc i›
proof-
from conjoin_same_spec[OF conjoin]
have same_spec: ‹∀k i. i < length pc ⟶ fst (pc ! i) k = fst (cs k ! i)› by assumption
from same_spec[rule_format, OF Suc_i_lt[THEN Suc_lessD]]
have eq1: ‹∀k. fst (pc ! i) k = fst (cs k ! i)› by blast
from same_spec[rule_format, OF Suc_i_lt]
have eq2: ‹∀k. fst (pc ! Suc i) k = fst (cs k ! Suc i)› by blast
have ‹∀k. fst (pc!i) k = fst (pc!Suc i) k›
proof
fix k
from eq1[THEN spec[where x=k]] have 1: ‹fst (pc ! i) k = fst (cs k ! i)› by assumption
from eq2[THEN spec[where x=k]] have 2: ‹fst (pc!Suc i) k = fst (cs k ! Suc i)› by assumption
from 1 2 all_etran[THEN spec[where x=k]]
show ‹fst (pc!i) k = fst (pc!Suc i) k› by simp
qed
then have ‹fst (pc!i) = fst (pc!Suc i)› by blast
then show ?thesis by simp
qed
lemma conjoin_etran_k:
assumes pc: ‹pc ∈ cpts (pestran Γ)›
and conjoin: ‹pc ∝ cs›
and Suc_i_lt: ‹Suc i < length pc›
and etran: ‹cs k!i ─e→ cs k!Suc i›
shows ‹(pc!i ─e→ pc!Suc i) ∨ (∃k'. k'≠k ∧ (cs k'!i, cs k'!Suc i) ∈ estran Γ)›
proof(rule ccontr, clarsimp)
assume neq: ‹fst (pc ! i) ≠ fst (pc ! Suc i)›
assume 1: ‹∀k'. k' = k ∨ (cs k' ! i, cs k' ! Suc i) ∉ estran Γ›
have ‹∀k'. cs k' ! i ─e→ cs k' ! Suc i›
proof
fix k'
show ‹cs k' ! i ─e→ cs k' ! Suc i›
proof(cases ‹k=k'›)
case True
then show ?thesis using etran by blast
next
case False
with 1 have not_ctran: ‹(cs k' ! i, cs k' ! Suc i) ∉ estran Γ› by fast
from conjoin_same_length[OF conjoin] Suc_i_lt have Suc_i_lt': ‹Suc i < length (cs k')› by simp
from conjoin_cpt[OF pc conjoin] have ‹cs k' ∈ cpts (estran Γ)› by assumption
from ctran_or_etran[OF this Suc_i_lt'] not_ctran
show ?thesis by blast
qed
qed
from conjoin_all_etran[OF conjoin Suc_i_lt this]
have ‹fst (pc!i) = fst (pc!Suc i)› by simp
with neq show False by blast
qed
end
end