Quelle  RG_Tran.thy   Sprache: Isabelle

section ‹Operational Semantics›

theory RG_Tran
imports RG_Com
begin

subsection ‹Semantics of Component Programs›

subsubsection ‹Environment transitions›

type_synonym 'a conf = "(('a com) option) × 'a"

inductive_set
  etran :: "('a conf \ 'a conf) set" 
  and etran' :: "'a conf ==> 'a conf \ bool" (\_ -e\ _\ [81,81] 80)
where
  "P -e\ Q \ (P,Q) \ etran"
| Env: "(P, s) -e\ (P, t)"

lemma etranE: "c -e\ c' \ (\P s t. c = (P, s) \ c' = (P, t) \ Q) \ Q"
  by (induct c, induct c', erule etran.cases, blast)

subsubsection ‹Component transitions›

inductive_set
  ctran :: "('a conf \ 'a conf) set"
  and ctran' :: "'a conf ==> 'a conf \ bool" (\_ -c\ _\ [81,81] 80)
  and ctrans :: "'a conf \ 'a conf \ bool"   (‹_ -c*→ _› [81,81] 80)
where
  "P -c\ Q \ (P,Q) \ ctran"
| "P -c*\ Q \ (P,Q) \ ctran\<^sup>*"

| Basic:  "(Some(Basic f), s) -c\ (None, f s)"

| Seq1:   "(Some P0, s) -c\ (None, t) \ (Some(Seq P0 P1), s) -c\ (Some P1, t)"

| Seq2:   "(Some P0, s) -c\ (Some P2, t) \ (Some(Seq P0 P1), s) -c\ (Some(Seq P2 P1), t)"

| CondT: "s\b \ (Some(Cond b P1 P2), s) -c\ (Some P1, s)"
| CondF: "s\b \ (Some(Cond b P1 P2), s) -c\ (Some P2, s)"

| WhileF: "s\b \ (Some(While b P), s) -c\ (None, s)"
| WhileT: "s\b \ (Some(While b P), s) -c\ (Some(Seq P (While b P)), s)"

| Await:  "\s\b; (Some P, s) -c*\ (None, t)\ \ (Some(Await b P), s) -c\ (None, t)" 

monos "rtrancl_mono"

subsection ‹Semantics of Parallel Programs›

type_synonym 'a par_conf = "('a par_com) × 'a"

inductive_set
  par_etran :: "('a par_conf \ 'a par_conf) set"
  and par_etran' :: "['a par_conf,'a par_conf] \ bool" (\_ -pe\ _\ [81,81] 80)
where
  "P -pe\ Q \ (P,Q) \ par_etran"
| ParEnv:  "(Ps, s) -pe\ (Ps, t)"

inductive_set
  par_ctran :: "('a par_conf \ 'a par_conf) set"
  and par_ctran' :: "['a par_conf,'a par_conf] \ bool" (\_ -pc\ _\ [81,81] 80)
where
  "P -pc\ Q \ (P,Q) \ par_ctran"
| ParComp: "\i (r, t)\ \ (Ps, s) -pc\ (Ps[i:=r], t)"

lemma par_ctranE: "c -pc\ c' \
  (∧i Ps s r t. c = (Ps, s) ==> c' = (Ps[i := r], t) \ i < length Ps \
     (Ps ! i, s) -c→ (r, t) ==> P) ==> P"
  by (induct c, induct c', erule par_ctran.cases, blast)

subsection ‹Computations›

subsubsection ‹Sequential computations›

type_synonym 'a confs = "'a conf list"

inductive_set cptn :: "'a confs set"
where
  CptnOne: "[(P,s)] \ cptn"
| CptnEnv: "(P, t)#xs \ cptn \ (P,s)#(P,t)#xs \ cptn"
| CptnComp: "\(P,s) -c\ (Q,t); (Q, t)#xs \ cptn \ \ (P,s)#(Q,t)#xs \ cptn"

definition cp :: "('a com) option \ 'a \ ('a confs) set" where
  "cp P s \ {l. l!0=(P,s) \ l \ cptn}"  

subsubsection ‹Parallel computations›

type_synonym 'a par_confs = "'a par_conf list"

inductive_set par_cptn :: "'a par_confs set"
where
  ParCptnOne: "[(P,s)] \ par_cptn"
| ParCptnEnv: "(P,t)#xs \ par_cptn \ (P,s)#(P,t)#xs \ par_cptn"
| ParCptnComp: "\ (P,s) -pc\ (Q,t); (Q,t)#xs \ par_cptn \ \ (P,s)#(Q,t)#xs \ par_cptn"

definition par_cp :: "'a par_com \ 'a \ ('a par_confs) set" where
  "par_cp P s \ {l. l!0=(P,s) \ l \ par_cptn}"  

subsection‹Modular Definition of Computation›

definition lift :: "'a com \ 'a conf \ 'a conf" where
  "lift Q \ \(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))"

inductive_set cptn_mod :: "('a confs) set"
where
  CptnModOne: "[(P, s)] \ cptn_mod"
| CptnModEnv: "(P, t)#xs \ cptn_mod \ (P, s)#(P, t)#xs \ cptn_mod"
| CptnModNone: "\(Some P, s) -c\ (None, t); (None, t)#xs \ cptn_mod \ \ (Some P,s)#(None, t)#xs \cptn_mod"
| CptnModCondT: "\(Some P0, s)#ys \ cptn_mod; s \ b \ \ (Some(Cond b P0 P1), s)#(Some P0, s)#ys \ cptn_mod"
| CptnModCondF: "\(Some P1, s)#ys \ cptn_mod; s \ b \ \ (Some(Cond b P0 P1), s)#(Some P1, s)#ys \ cptn_mod"
| CptnModSeq1: "\(Some P0, s)#xs \ cptn_mod; zs=map (lift P1) xs \
                 ==> (Some(Seq P0 P1), s)#zs ∈ cptn_mod"
| CptnModSeq2: 
  "\(Some P0, s)#xs \ cptn_mod; fst(last ((Some P0, s)#xs)) = None;
  (Some P1, snd(last ((Some P0, s)#xs)))#ys ∈ cptn_mod; 
  zs=(map (lift P1) xs)@ys ] ==> (Some(Seq P0 P1), s)#zs ∈ cptn_mod"

| CptnModWhile1: 
  "\ (Some P, s)#xs \ cptn_mod; s \ b; zs=map (lift (While b P)) xs \
  ==> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs ∈ cptn_mod"
| CptnModWhile2: 
  "\ (Some P, s)#xs \ cptn_mod; fst(last ((Some P, s)#xs))=None; s \ b;
  zs=(map (lift (While b P)) xs)@ys; 
  (Some(While b P), snd(last ((Some P, s)#xs)))#ys ∈ cptn_mod] 
  ==> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs ∈ cptn_mod"

subsection ‹Equivalence of Both Definitions.›

lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
  by (induct xs) auto

lemma div_seq [rule_format]: "list \ cptn_mod \
 (∀s P Q zs. list=(Some (Seq P Q), s)#zs ⟶
  (∃xs. (Some P, s)#xs ∈ cptn_mod  ∧ (zs=(map (lift Q) xs) ∨
  ( fst(((Some P, s)#xs)!length xs)=None ∧ 
  (∃ys. (Some Q, snd(((Some P, s)#xs)!length xs))#ys ∈ cptn_mod  
  ∧ zs=(map (lift (Q)) xs)@ys)))))"
apply(erule cptn_mod.induct)
apply simp_all
    apply clarify
    apply(force intro:CptnModOne)
   apply clarify
   apply(erule_tac x=Pa in allE)
   apply(erule_tac x=Q in allE)
   apply simp
   apply clarify
   apply(erule disjE)
    apply(rule_tac x="(Some Pa,t)#xsa" in exI)
    apply(rule conjI)
     apply clarify
     apply(erule CptnModEnv)
    apply(rule disjI1)
    apply(simp add:lift_def)
   apply clarify
   apply(rule_tac x="(Some Pa,t)#xsa" in exI)
   apply(rule conjI)
    apply(erule CptnModEnv)
   apply(rule disjI2)
   apply(rule conjI)
    apply(case_tac xsa,simp,simp)
   apply(rule_tac x="ys" in exI)
   apply(rule conjI)
    apply simp
   apply(simp add:lift_def)
  apply clarify
  apply(erule ctran.cases,simp_all)
 apply clarify
 apply(rule_tac x="xs" in exI)
 apply simp
 apply clarify
apply(rule_tac x="xs" in exI)
apply(simp add: last_length)
done

lemma cptn_onlyif_cptn_mod_aux [rule_format]:
  "\s Q t xs.((Some a, s), Q, t) \ ctran \ (Q, t) # xs \ cptn_mod
  ⟶ (Some a, s) # (Q, t) # xs ∈ cptn_mod"
  supply [[simproc del: defined_all]]
apply(induct a)
apply simp_all
🍋 ‹basic›
apply clarify
apply(erule ctran.cases,simp_all)
apply(rule CptnModNone,rule Basic,simp)
apply clarify
apply(erule ctran.cases,simp_all)
🍋 ‹Seq1›
apply(rule_tac xs="[(None,ta)]" in CptnModSeq2)
  apply(erule CptnModNone)
  apply(rule CptnModOne)
 apply simp
apply simp
apply(simp add:lift_def)
🍋 ‹Seq2›
apply(erule_tac x=sa in allE)
apply(erule_tac x="Some P2" in allE)
apply(erule allE,erule impE, assumption)
apply(drule div_seq,simp)
apply clarify
apply(erule disjE)
 apply clarify
 apply(erule allE,erule impE, assumption)
 apply(erule_tac CptnModSeq1)
 apply(simp add:lift_def)
apply clarify 
apply(erule allE,erule impE, assumption)
apply(erule_tac CptnModSeq2)
  apply (simp add:last_length)
 apply (simp add:last_length)
apply(simp add:lift_def)
🍋 ‹Cond›
apply clarify
apply(erule ctran.cases,simp_all)
apply(force elim: CptnModCondT)
apply(force elim: CptnModCondF)
🍋 ‹While›
apply  clarify
apply(erule ctran.cases,simp_all)
apply(rule CptnModNone,erule WhileF,simp)
apply(drule div_seq,force)
apply clarify
apply (erule disjE)
 apply(force elim:CptnModWhile1)
apply clarify
apply(force simp add:last_length elim:CptnModWhile2)
🍋 ‹await›
apply clarify
apply(erule ctran.cases,simp_all)
apply(rule CptnModNone,erule Await,simp+)
done

lemma cptn_onlyif_cptn_mod [rule_format]: "c \ cptn \ c \ cptn_mod"
apply(erule cptn.induct)
  apply(rule CptnModOne)
 apply(erule CptnModEnv)
apply(case_tac P)
 apply simp
 apply(erule ctran.cases,simp_all)
apply(force elim:cptn_onlyif_cptn_mod_aux)
done

lemma lift_is_cptn: "c\cptn \ map (lift P) c \ cptn"
apply(erule cptn.induct)
  apply(force simp add:lift_def CptnOne)
 apply(force intro:CptnEnv simp add:lift_def)
apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.cases)
done

lemma cptn_append_is_cptn [rule_format]: 
 "\b a. b#c1\cptn \ a#c2\cptn \ (b#c1)!length c1=a \ b#c1@c2\cptn"
apply(induct c1)
 apply simp
apply clarify
apply(erule cptn.cases,simp_all)
 apply(force intro:CptnEnv)
apply(force elim:CptnComp)
done

lemma last_lift: "\xs\[]; fst(xs!(length xs - (Suc 0)))=None\
 ==> fst((map (lift P) xs)!(length (map (lift P) xs)- (Suc 0)))=(Some P)"
  by (cases "(xs ! (length xs - (Suc 0)))") (simp add:lift_def)

lemma last_fst [rule_format]: "P((a#x)!length x) \ \P a \ P (x!(length x - (Suc 0)))" 
  by (induct x) simp_all

lemma last_fst_esp: 
 "fst(((Some a,s)#xs)!(length xs))=None \ fst(xs!(length xs - (Suc 0)))=None" 
apply(erule last_fst)
apply simp
done

lemma last_snd: "xs\[] \
  snd(((map (lift P) xs))!(length (map (lift P) xs) - (Suc 0)))=snd(xs!(length xs - (Suc 0)))"
  by (cases "(xs ! (length xs - (Suc 0)))") (simp_all add:lift_def)

lemma Cons_lift: "(Some (Seq P Q), s) # (map (lift Q) xs) = map (lift Q) ((Some P, s) # xs)"
  by (simp add:lift_def)

lemma Cons_lift_append: 
  "(Some (Seq P Q), s) # (map (lift Q) xs) @ ys = map (lift Q) ((Some P, s) # xs)@ ys "
  by (simp add:lift_def)

lemma lift_nth: "i map (lift Q) xs ! i = lift Q (xs! i)"
  by (simp add:lift_def)

lemma snd_lift: "i< length xs \ snd(lift Q (xs ! i))= snd (xs ! i)"
  by (cases "xs!i") (simp add:lift_def)

lemma cptn_if_cptn_mod: "c \ cptn_mod \ c \ cptn"
apply(erule cptn_mod.induct)
        apply(rule CptnOne)
       apply(erule CptnEnv)
      apply(erule CptnComp,simp)
     apply(rule CptnComp)
      apply(erule CondT,simp)
    apply(rule CptnComp)
     apply(erule CondF,simp)
🍋 ‹Seq1›
apply(erule cptn.cases,simp_all)
  apply(rule CptnOne)
 apply clarify
 apply(drule_tac P=P1 in lift_is_cptn)
 apply(simp add:lift_def)
 apply(rule CptnEnv,simp)
apply clarify
apply(simp add:lift_def)
apply(rule conjI)
 apply clarify
 apply(rule CptnComp)
  apply(rule Seq1,simp)
 apply(drule_tac P=P1 in lift_is_cptn)
 apply(simp add:lift_def)
apply clarify
apply(rule CptnComp)
 apply(rule Seq2,simp)
apply(drule_tac P=P1 in lift_is_cptn)
apply(simp add:lift_def)
🍋 ‹Seq2›
apply(rule cptn_append_is_cptn)
  apply(drule_tac P=P1 in lift_is_cptn)
  apply(simp add:lift_def)
 apply simp
apply(simp split: if_split_asm)
apply(frule_tac P=P1 in last_lift)
 apply(rule last_fst_esp)
 apply (simp add:last_length)
apply(simp add:Cons_lift lift_def split_def last_conv_nth)
🍋 ‹While1›
apply(rule CptnComp)
 apply(rule WhileT,simp)
apply(drule_tac P="While b P" in lift_is_cptn)
apply(simp add:lift_def)
🍋 ‹While2›
apply(rule CptnComp)
 apply(rule WhileT,simp)
apply(rule cptn_append_is_cptn)
  apply(drule_tac P="While b P" in lift_is_cptn)
  apply(simp add:lift_def)
 apply simp
apply(simp split: if_split_asm)
apply(frule_tac P="While b P" in last_lift)
 apply(rule last_fst_esp,simp add:last_length)
apply(simp add:Cons_lift lift_def split_def last_conv_nth)
done

theorem cptn_iff_cptn_mod: "(c \ cptn) = (c \ cptn_mod)"
apply(rule iffI)
 apply(erule cptn_onlyif_cptn_mod)
apply(erule cptn_if_cptn_mod)
done

section ‹Validity  of Correctness Formulas›

subsection ‹Validity for Component Programs.›

type_synonym 'a rgformula =
  "'a com \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set"

definition assum :: "('a set \ ('a \ 'a) set) \ ('a confs) set" where
  "assum \ \(pre, rely). {c. snd(c!0) \ pre \ (\i. Suc i
               c!i -e→ c!(Suc i) ⟶ (snd(c!i), snd(c!Suc i)) ∈ rely)}"

definition comm :: "(('a \ 'a) set \ 'a set) \ ('a confs) set" where
  "comm \ \(guar, post). {c. (\i. Suc i
               c!i -c→ c!(Suc i) ⟶ (snd(c!i), snd(c!Suc i)) ∈ guar) ∧ 
               (fst (last c) = None ⟶ snd (last c) ∈ post)}"

definition com_validity :: "'a com \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set \ 'a set \ bool" 
                 (‹⊨ _ sat [_, _, _, _]› [60,0,0,0,0] 45) where
  "\ P sat [pre, rely, guar, post] \
   ∀s. cp (Some P) s ∩ assum(pre, rely) ⊆ comm(guar, post)"

subsection ‹Validity for Parallel Programs.›

definition All_None :: "(('a com) option) list \ bool" where
  "All_None xs \ \c\set xs. c=None"

definition par_assum :: "('a set \ ('a \ 'a) set) \ ('a par_confs) set" where
  "par_assum \ \(pre, rely). {c. snd(c!0) \ pre \ (\i. Suc i
             c!i -pe→ c!Suc i ⟶ (snd(c!i), snd(c!Suc i)) ∈ rely)}"

definition par_comm :: "(('a \ 'a) set \ 'a set) \ ('a par_confs) set" where
  "par_comm \ \(guar, post). {c. (\i. Suc i
        c!i -pc→ c!Suc i ⟶ (snd(c!i), snd(c!Suc i)) ∈ guar) ∧ 
         (All_None (fst (last c)) ⟶ snd( last c) ∈ post)}"

definition par_com_validity :: "'a par_com \ 'a set \ ('a \ 'a) set \ ('a \ 'a) set
==> 'a set \ bool" (\\ _ SAT [_, _, _, _]\ [60,0,0,0,0] 45) where
  "\ Ps SAT [pre, rely, guar, post] \
   ∀s. par_cp Ps s ∩ par_assum(pre, rely) ⊆ par_comm(guar, post)"

subsection ‹Compositionality of the Semantics›

subsubsection ‹Definition of the conjoin operator›

definition same_length :: "'a par_confs \ ('a confs) list \ bool" where
  "same_length c clist \ (\i
 
definition same_state :: "'a par_confs \ ('a confs) list \ bool" where
  "same_state c clist \ (\i j

definition same_program :: "'a par_confs \ ('a confs) list \ bool" where
  "same_program c clist \ (\jx. fst(nth x j)) clist)"

definition compat_label :: "'a par_confs \ ('a confs) list \ bool" where
  "compat_label c clist \ (\j. Suc j
         (c!j -pc→ c!Suc j ∧ (∃i<length clist. (clist!i)!j -c→ (clist!i)! Suc j ∧ 
                       (∀l<length clist. l≠i ⟶ (clist!l)!j -e→ (clist!l)! Suc j))) ∨ 
         (c!j -pe→ c!Suc j ∧ (∀i<length clist. (clist!i)!j -e→ (clist!i)! Suc j)))"

definition conjoin :: "'a par_confs \ ('a confs) list \ bool"  (‹_ ∝ _› [65,65] 64) where
  "c \ clist \ (same_length c clist) \ (same_state c clist) \ (same_program c clist) \ (compat_label c clist)"

subsubsection ‹Some previous lemmas›

lemma list_eq_if [rule_format]: 
  "\ys. xs=ys \ (length xs = length ys) \ (\i
  by (induct xs) auto

lemma list_eq: "(length xs = length ys \ (\i
apply(rule iffI)
 apply clarify
 apply(erule nth_equalityI)
 apply simp+
done

lemma nth_tl: "\ ys!0=a; ys\[] \ \ ys=(a#(tl ys))"
  by (cases ys) simp_all

lemma nth_tl_if [rule_format]: "ys\[] \ ys!0=a \ P ys \ P (a#(tl ys))"
  by (induct ys) simp_all

lemma nth_tl_onlyif [rule_format]: "ys\[] \ ys!0=a \ P (a#(tl ys)) \ P ys"
  by (induct ys) simp_all

lemma seq_not_eq1: "Seq c1 c2\c1"
  by (induct c1) auto

lemma seq_not_eq2: "Seq c1 c2\c2"
  by (induct c2) auto

lemma if_not_eq1: "Cond b c1 c2 \c1"
  by (induct c1) auto

lemma if_not_eq2: "Cond b c1 c2\c2"
  by (induct c2) auto

lemmas seq_and_if_not_eq [simp] = seq_not_eq1 seq_not_eq2 
seq_not_eq1 [THEN not_sym] seq_not_eq2 [THEN not_sym] 
if_not_eq1 if_not_eq2 if_not_eq1 [THEN not_sym] if_not_eq2 [THEN not_sym]

lemma prog_not_eq_in_ctran_aux:
  assumes c: "(P,s) -c\ (Q,t)"
  shows "P\Q" using c
  by (induct x1 ≡ "(P,s)" x2 ≡ "(Q,t)" arbitrary: P s Q t) auto

lemma prog_not_eq_in_ctran [simp]: "\ (P,s) -c\ (P,t)"
apply clarify
apply(drule prog_not_eq_in_ctran_aux)
apply simp
done

lemma prog_not_eq_in_par_ctran_aux [rule_format]: "(P,s) -pc\ (Q,t) \ (P\Q)"
apply(erule par_ctran.induct)
apply(drule prog_not_eq_in_ctran_aux)
apply clarify
apply(drule list_eq_if)
 apply simp_all
apply force
done

lemma prog_not_eq_in_par_ctran [simp]: "\ (P,s) -pc\ (P,t)"
apply clarify
apply(drule prog_not_eq_in_par_ctran_aux)
apply simp
done

lemma tl_in_cptn: "\ a#xs \cptn; xs\[] \ \ xs\cptn"
  by (force elim: cptn.cases)

lemma tl_zero[rule_format]: 
  "P (ys!Suc j) \ Suc j ys\[] \ P (tl(ys)!j)"
  by (induct ys) simp_all

subsection ‹The Semantics is Compositional›

lemma aux_if [rule_format]: 
  "\xs s clist. (length clist = length xs \ (\i cptn)
  ∧ ((xs, s)#ys ∝ map (λi. (fst i,s)#snd i) (zip xs clist)) 
   ⟶ (xs, s)#ys ∈ par_cptn)"
apply(induct ys)
 apply(clarify)
 apply(rule ParCptnOne)
apply(clarify)
apply(simp add:conjoin_def compat_label_def)
apply clarify
apply(erule_tac x="0" and P="\j. H j \ (P j \ Q j)" for H P Q in all_dupE, simp)
apply(erule disjE)
🍋 ‹first step is a Component step›
 apply clarify 
 apply simp
 apply(subgoal_tac "a=(xs[i:=(fst(clist!i!0))])")
  apply(subgoal_tac "b=snd(clist!i!0)",simp)
   prefer 2
   apply(simp add: same_state_def)
   apply(erule_tac x=i in allE,erule impE,assumption, 
         erule_tac x=1 and P="\j. (H j) \ (snd (d j))=(snd (e j))" for H d e in allE, simp)
  prefer 2
  apply(simp add:same_program_def)
  apply(erule_tac x=1 and P="\j. H j \ (fst (s j))=(t j)" for H s t in allE,simp)
  apply(rule nth_equalityI,simp)
  apply clarify
  apply(case_tac "i=ia",simp,simp)
  apply(erule_tac x=ia and P="\j. H j \ I j \ J j" for H I J in allE)
  apply(drule_tac t=i in not_sym,simp)
  apply(erule etranE,simp)
 apply(rule ParCptnComp)
  apply(erule ParComp,simp)
🍋 ‹applying the induction hypothesis›
 apply(erule_tac x="xs[i := fst (clist ! i ! 0)]" in allE)
 apply(erule_tac x="snd (clist ! i ! 0)" in allE)
 apply(erule mp)
 apply(rule_tac x="map tl clist" in exI,simp)
 apply(rule conjI,clarify)
  apply(case_tac "i=ia",simp)
   apply(rule nth_tl_if)
     apply(force simp add:same_length_def length_Suc_conv)
    apply simp
   apply(erule allE,erule impE,assumption,erule tl_in_cptn)
   apply(force simp add:same_length_def length_Suc_conv)
  apply(rule nth_tl_if)
    apply(force simp add:same_length_def length_Suc_conv)
   apply(simp add:same_state_def)
   apply(erule_tac x=ia in allE, erule impE, assumption, 
     erule_tac x=1 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE)
   apply(erule_tac x=ia and P="\j. H j \ I j \ J j" for H I J in allE)
   apply(drule_tac t=i  in not_sym,simp)
   apply(erule etranE,simp)
  apply(erule allE,erule impE,assumption,erule tl_in_cptn)
  apply(force simp add:same_length_def length_Suc_conv)
 apply(simp add:same_length_def same_state_def)
 apply(rule conjI)
  apply clarify
  apply(case_tac j,simp,simp)
  apply(erule_tac x=ia in allE, erule impE, assumption,
        erule_tac x="Suc(Suc nat)" and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
  apply(force simp add:same_length_def length_Suc_conv)
 apply(rule conjI)
  apply(simp add:same_program_def)
  apply clarify
  apply(case_tac j,simp)
   apply(rule nth_equalityI,simp)
   apply clarify
   apply(case_tac "i=ia",simp,simp)
  apply(erule_tac x="Suc(Suc nat)" and P="\j. H j \ (fst (s j))=(t j)" for H s t in allE,simp)
  apply(rule nth_equalityI,simp,simp)
  apply(force simp add:length_Suc_conv)
 apply(rule allI,rule impI)
 apply(erule_tac x="Suc j" and P="\j. H j \ (I j \ J j)" for H I J in allE,simp)
 apply(erule disjE) 
  apply clarify
  apply(rule_tac x=ia in exI,simp)
  apply(case_tac "i=ia",simp)
   apply(rule conjI)
    apply(force simp add: length_Suc_conv)
   apply clarify
   apply(erule_tac x=l and P="\j. H j \ I j \ J j" for H I J in allE,erule impE,assumption)
   apply(erule_tac x=l and P="\j. H j \ I j \ J j" for H I J in allE,erule impE,assumption)
   apply simp
   apply(case_tac j,simp)
    apply(rule tl_zero)
      apply(erule_tac x=l in allE, erule impE, assumption, 
            erule_tac x=1 and P="\j. (H j) \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
      apply(force elim:etranE intro:Env)
     apply force
    apply force
   apply simp
   apply(rule tl_zero)
     apply(erule tl_zero)
      apply force
     apply force
    apply force
   apply force
  apply(rule conjI,simp)
   apply(rule nth_tl_if)
     apply force
    apply(erule_tac x=ia  in allE, erule impE, assumption,
          erule_tac x=1 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE)
    apply(erule_tac x=ia and P="\j. H j \ I j \ J j" for H I J in allE)
    apply(drule_tac t=i  in not_sym,simp)
    apply(erule etranE,simp)
   apply(erule tl_zero)
    apply force
   apply force
  apply clarify
  apply(case_tac "i=l",simp)
   apply(rule nth_tl_if)
     apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
    apply simp
   apply(erule_tac P="\j. H j \ I j \ J j" for H I J in allE,erule impE,assumption,erule impE,assumption)
   apply(erule tl_zero,force)
   apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
   apply(rule nth_tl_if)
     apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
    apply(erule_tac x=l  in allE, erule impE, assumption,
          erule_tac x=1 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE)
    apply(erule_tac x=l and P="\j. H j \ I j \ J j" for H I J in allE,erule impE, assumption,simp)
    apply(erule etranE,simp)
   apply(rule tl_zero)
    apply force
   apply force
  apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
 apply(rule disjI2)
 apply(case_tac j,simp)
  apply clarify
  apply(rule tl_zero)
    apply(erule_tac x=ia and P="\j. H j \ I j\etran" for H I in allE,erule impE, assumption)
    apply(case_tac "i=ia",simp,simp)
    apply(erule_tac x=ia  in allE, erule impE, assumption,
    erule_tac x=1 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE)
    apply(erule_tac x=ia and P="\j. H j \ I j \ J j" for H I J in allE,erule impE, assumption,simp)
    apply(force elim:etranE intro:Env)
   apply force
  apply(erule_tac x=ia and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
 apply simp
 apply clarify
 apply(rule tl_zero)
   apply(rule tl_zero,force)
    apply force
   apply(erule_tac x=ia and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
  apply force
 apply(erule_tac x=ia and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
🍋 ‹first step is an environmental step›
apply clarify
apply(erule par_etran.cases)
apply simp
apply(rule ParCptnEnv)
apply(erule_tac x="Ps" in allE)
apply(erule_tac x="t" in allE)
apply(erule mp)
apply(rule_tac x="map tl clist" in exI,simp)
apply(rule conjI)
 apply clarify
 apply(erule_tac x=i and P="\j. H j \ I j \ cptn" for H I in allE,simp)
 apply(erule cptn.cases)
   apply(simp add:same_length_def)
   apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
  apply(simp add:same_state_def)
  apply(erule_tac x=i  in allE, erule impE, assumption,
   erule_tac x=1 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
 apply(erule_tac x=i and P="\j. H j \ J j \etran" for H J in allE,simp)
 apply(erule etranE,simp)
apply(simp add:same_state_def same_length_def)
apply(rule conjI,clarify)
 apply(case_tac j,simp,simp)
 apply(erule_tac x=i  in allE, erule impE, assumption,
       erule_tac x="Suc(Suc nat)" and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
 apply(rule tl_zero)
   apply(simp)
  apply force
 apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
apply(rule conjI)
 apply(simp add:same_program_def)
 apply clarify
 apply(case_tac j,simp)
  apply(rule nth_equalityI,simp)
  apply clarify
  apply simp
 apply(erule_tac x="Suc(Suc nat)" and P="\j. H j \ (fst (s j))=(t j)" for H s t in allE,simp)
 apply(rule nth_equalityI,simp,simp)
 apply(force simp add:length_Suc_conv)
apply(rule allI,rule impI)
apply(erule_tac x="Suc j" and P="\j. H j \ (I j \ J j)" for H I J in allE,simp)
apply(erule disjE) 
 apply clarify
 apply(rule_tac x=i in exI,simp)
 apply(rule conjI)
  apply(erule_tac x=i and P="\i. H i \ J i \etran" for H J in allE, erule impE, assumption)
  apply(erule etranE,simp)
  apply(erule_tac x=i  in allE, erule impE, assumption,
        erule_tac x=1 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
  apply(rule nth_tl_if)
   apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
  apply simp
 apply(erule tl_zero,force) 
  apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
 apply clarify
 apply(erule_tac x=l and P="\i. H i \ J i \etran" for H J in allE, erule impE, assumption)
 apply(erule etranE,simp)
 apply(erule_tac x=l  in allE, erule impE, assumption,
       erule_tac x=1 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
 apply(rule nth_tl_if)
   apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
  apply simp
  apply(rule tl_zero,force)
  apply force
 apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
apply(rule disjI2)
apply simp
apply clarify
apply(case_tac j,simp)
 apply(rule tl_zero)
   apply(erule_tac x=i and P="\i. H i \ J i \etran" for H J in allE, erule impE, assumption)
   apply(erule_tac x=i and P="\i. H i \ J i \etran" for H J in allE, erule impE, assumption)
   apply(force elim:etranE intro:Env)
  apply force
 apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
apply simp
apply(rule tl_zero)
  apply(rule tl_zero,force)
   apply force
  apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
 apply force
apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
done

lemma aux_onlyif [rule_format]: "\xs s. (xs, s)#ys \ par_cptn \
  (∃clist. (length clist = length xs) ∧ 
  (xs, s)#ys ∝ map (λi. (fst i,s)#(snd i)) (zip xs clist) ∧ 
  (∀i<length xs. (xs!i,s)#(clist!i) ∈ cptn))"
  supply [[simproc del: defined_all]]
apply(induct ys)
 apply(clarify)
 apply(rule_tac x="map (\i. []) [0.. in exI)
 apply(simp add: conjoin_def same_length_def same_state_def same_program_def compat_label_def)
 apply(rule conjI)
  apply(rule nth_equalityI,simp,simp)
 apply(force intro: cptn.intros)
apply(clarify)
apply(erule par_cptn.cases,simp)
 apply simp
 apply(erule_tac x="xs" in allE)
 apply(erule_tac x="t" in allE,simp)
 apply clarify
 apply(rule_tac x="(map (\j. (P!j, t)#(clist!j)) [0.. in exI,simp)
 apply(rule conjI)
  prefer 2
  apply clarify
  apply(rule CptnEnv,simp)
 apply(simp add:conjoin_def same_length_def same_state_def)
 apply (rule conjI)
  apply clarify
  apply(case_tac j,simp,simp)
 apply(rule conjI)
  apply(simp add:same_program_def)
  apply clarify
  apply(case_tac j,simp)
   apply(rule nth_equalityI,simp,simp)
  apply simp
  apply(rule nth_equalityI,simp,simp)
 apply(simp add:compat_label_def)
 apply clarify
 apply(case_tac j,simp)
  apply(simp add:ParEnv)
  apply clarify
  apply(simp add:Env)
 apply simp
 apply(erule_tac x=nat in allE,erule impE, assumption)
 apply(erule disjE,simp)
  apply clarify
  apply(rule_tac x=i in exI,simp)
 apply force
apply(erule par_ctran.cases,simp)
apply(erule_tac x="Ps[i:=r]" in allE)
apply(erule_tac x="ta" in allE,simp)
apply clarify
apply(rule_tac x="(map (\j. (Ps!j, ta)#(clist!j)) [0.. in exI,simp)
apply(rule conjI)
 prefer 2
 apply clarify
 apply(case_tac "i=ia",simp)
  apply(erule CptnComp)
  apply(erule_tac x=ia and P="\j. H j \ (I j \ cptn)" for H I in allE,simp)
 apply simp
 apply(erule_tac x=ia in allE)
 apply(rule CptnEnv,simp)
apply(simp add:conjoin_def)
apply (rule conjI)
 apply(simp add:same_length_def)
 apply clarify
 apply(case_tac "i=ia",simp,simp)
apply(rule conjI)
 apply(simp add:same_state_def)
 apply clarify
 apply(case_tac j, simp, simp (no_asm_simp))
 apply(case_tac "i=ia",simp,simp)
apply(rule conjI)
 apply(simp add:same_program_def)
 apply clarify
 apply(case_tac j,simp)
  apply(rule nth_equalityI,simp,simp)
 apply simp
 apply(rule nth_equalityI,simp,simp)
 apply(erule_tac x=nat and P="\j. H j \ (fst (a j))=((b j))" for H a b in allE)
 apply(case_tac nat)
  apply clarify
  apply(case_tac "i=ia",simp,simp)
 apply clarify
 apply(case_tac "i=ia",simp,simp)
apply(simp add:compat_label_def)
apply clarify
apply(case_tac j)
 apply(rule conjI,simp)
  apply(erule ParComp,assumption)
  apply clarify
  apply(rule_tac x=i in exI,simp)
 apply clarify
 apply(rule Env)
apply simp
apply(erule_tac x=nat and P="\j. H j \ (P j \ Q j)" for H P Q in allE,simp)
apply(erule disjE)
 apply clarify
 apply(rule_tac x=ia in exI,simp)
 apply(rule conjI)
  apply(case_tac "i=ia",simp,simp)
 apply clarify
 apply(case_tac "i=l",simp)
  apply(case_tac "l=ia",simp,simp)
  apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
 apply simp
 apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
apply clarify
apply(erule_tac x=ia and P="\j. H j \ (P j)\etran" for H P in allE, erule impE, assumption)
apply(case_tac "i=ia",simp,simp)
done

lemma one_iff_aux: "xs\[] \ (\ys. ((xs, s)#ys \ par_cptn) =
 (∃clist. length clist= length xs ∧ 
 ((xs, s)#ys ∝ map (λi. (fst i,s)#(snd i)) (zip xs clist)) ∧ 
 (∀i<length xs. (xs!i,s)#(clist!i) ∈ cptn))) = 
 (par_cp (xs) s = {c. ∃clist. (length clist)=(length xs) ∧
 (∀i<length clist. (clist!i) ∈ cp(xs!i) s) ∧ c ∝ clist})"
apply (rule iffI)
 apply(rule subset_antisym)
  apply(rule subsetI) 
  apply(clarify)
  apply(simp add:par_cp_def cp_def)
  apply(case_tac x)
   apply(force elim:par_cptn.cases)
  apply simp
  apply(rename_tac a list)
  apply(erule_tac x="list" in allE)
  apply clarify
  apply simp
  apply(rule_tac x="map (\i. (fst i, s) # snd i) (zip xs clist)" in exI,simp)
 apply(rule subsetI) 
 apply(clarify)
 apply(case_tac x)
  apply(erule_tac x=0 in allE)
  apply(simp add:cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def)
  apply clarify
  apply(erule cptn.cases,force,force,force)
 apply(simp add:par_cp_def conjoin_def  same_length_def same_program_def same_state_def compat_label_def)
 apply clarify
 apply(erule_tac x=0 and P="\j. H j \ (length (s j) = t)" for H s t in all_dupE)
 apply(subgoal_tac "a = xs")
  apply(subgoal_tac "b = s",simp)
   prefer 3
   apply(erule_tac x=0 and P="\j. H j \ (fst (s j))=((t j))" for H s t in allE)
   apply (simp add:cp_def)
   apply(rule nth_equalityI,simp,simp)
  prefer 2
  apply(erule_tac x=0 in allE)
  apply (simp add:cp_def)
  apply(erule_tac x=0 and P="\j. H j \ (\i. T i \ (snd (d j i))=(snd (e j i)))" for H T d e in allE,simp)
  apply(erule_tac x=0 and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
 apply(erule_tac x=list in allE)
 apply(rule_tac x="map tl clist" in exI,simp) 
 apply(rule conjI)
  apply clarify
  apply(case_tac j,simp)
   apply(erule_tac x=i  in allE, erule impE, assumption,
        erule_tac x="0" and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE,simp)
  apply(erule_tac x=i  in allE, erule impE, assumption,
        erule_tac x="Suc nat" and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE)
  apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
  apply(case_tac "clist!i",simp,simp)
 apply(rule conjI)
  apply clarify
  apply(rule nth_equalityI,simp,simp)
  apply(case_tac j)
   apply clarify
   apply(erule_tac x=i in allE)
   apply(simp add:cp_def)
  apply clarify
  apply simp
  apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
  apply(case_tac "clist!i",simp,simp)
 apply(thin_tac "H = (\i. J i)" for H J)
 apply(rule conjI)
  apply clarify
  apply(erule_tac x=j in allE,erule impE, assumption,erule disjE)
   apply clarify
   apply(rule_tac x=i in exI,simp)
   apply(case_tac j,simp)
    apply(rule conjI)
     apply(erule_tac x=i in allE)
     apply(simp add:cp_def)
     apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
     apply(case_tac "clist!i",simp,simp)
    apply clarify
    apply(erule_tac x=l in allE)
    apply(erule_tac x=l and P="\j. H j \ I j \ J j" for H I J in allE)
    apply clarify
    apply(simp add:cp_def)
    apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE)
    apply(case_tac "clist!l",simp,simp)
   apply simp
   apply(rule conjI)
    apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
    apply(case_tac "clist!i",simp,simp)
   apply clarify
   apply(erule_tac x=l and P="\j. H j \ I j \ J j" for H I J in allE)
   apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE)
   apply(case_tac "clist!l",simp,simp)
  apply clarify
  apply(erule_tac x=i in allE)
  apply(simp add:cp_def)
  apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
  apply(case_tac "clist!i",simp)
  apply(rule nth_tl_if,simp,simp)
  apply(erule_tac x=i and P="\j. H j \ (P j)\etran" for H P in allE, erule impE, assumption,simp)
  apply(simp add:cp_def)
  apply clarify
  apply(rule nth_tl_if)
   apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
   apply(case_tac "clist!i",simp,simp)
  apply force
 apply force
apply clarify
apply(rule iffI)
 apply(simp add:par_cp_def)
 apply(erule_tac c="(xs, s) # ys" in equalityCE)
  apply simp
  apply clarify
  apply(rule_tac x="map tl clist" in exI)
  apply simp
  apply (rule conjI)
   apply(simp add:conjoin_def cp_def)
   apply(rule conjI)
    apply clarify
    apply(unfold same_length_def)
    apply clarify
    apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,simp)
   apply(rule conjI)
    apply(simp add:same_state_def)
    apply clarify
    apply(erule_tac x=i in allE, erule impE, assumption,
       erule_tac x=j and P="\j. H j \ (snd (d j))=(snd (e j))" for H d e in allE)
    apply(case_tac j,simp)
    apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
    apply(case_tac "clist!i",simp,simp)
   apply(rule conjI)
    apply(simp add:same_program_def)
    apply clarify
    apply(rule nth_equalityI,simp,simp)
    apply(case_tac j,simp)
    apply clarify
    apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
    apply(case_tac "clist!i",simp,simp)
   apply clarify
   apply(simp add:compat_label_def)
   apply(rule allI,rule impI)
   apply(erule_tac x=j in allE,erule impE, assumption)
   apply(erule disjE)
    apply clarify
    apply(rule_tac x=i in exI,simp)
    apply(rule conjI)
     apply(erule_tac x=i in allE)
     apply(case_tac j,simp)
      apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
      apply(case_tac "clist!i",simp,simp)
     apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE)
     apply(case_tac "clist!i",simp,simp)
    apply clarify
    apply(erule_tac x=l and P="\j. H j \ I j \ J j" for H I J in allE)
    apply(erule_tac x=l and P="\j. H j \ (length (s j) = t)" for H s t in allE)
    apply(case_tac "clist!l",simp,simp)
    apply(erule_tac x=l in allE,simp)
   apply(rule disjI2)
   apply clarify
   apply(rule tl_zero)
     apply(case_tac j,simp,simp)
     apply(rule tl_zero,force)   
      apply force
     apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
    apply force
   apply(erule_tac x=i and P="\j. H j \ (length (s j) = t)" for H s t in allE,force)
  apply clarify
  apply(erule_tac x=i in allE)
  apply(simp add:cp_def)
  apply(rule nth_tl_if)
    apply(simp add:conjoin_def)
    apply clarify
    apply(simp add:same_length_def)
    apply(erule_tac x=i in allE,simp)
   apply simp
  apply simp
 apply simp
apply clarify
apply(erule_tac c="(xs, s) # ys" in equalityCE)
 apply(simp add:par_cp_def)
apply simp
apply(erule_tac x="map (\i. (fst i, s) # snd i) (zip xs clist)" in allE)
apply simp
apply clarify
apply(simp add:cp_def)
done

theorem one: "xs\[] \
 par_cp xs s = {c. ∃clist. (length clist)=(length xs) ∧ 
               (∀i<length clist. (clist!i) ∈ cp(xs!i) s) ∧ c ∝ clist}"
apply(frule one_iff_aux)
apply(drule sym)
apply(erule iffD2)
apply clarify
apply(rule iffI)
 apply(erule aux_onlyif)
apply clarify
apply(force intro:aux_if)
done

end