src/HOL/Hoare_Parallel/RG_Tran.thy
author wenzelm
Sat Nov 04 15:24:40 2017 +0100 (21 months ago)
changeset 67003 49850a679c2c
parent 62390 842917225d56
child 67443 3abf6a722518
permissions -rw-r--r--
more robust sorted_entries;
     1 section \<open>Operational Semantics\<close>
     2 
     3 theory RG_Tran
     4 imports RG_Com
     5 begin
     6 
     7 subsection \<open>Semantics of Component Programs\<close>
     8 
     9 subsubsection \<open>Environment transitions\<close>
    10 
    11 type_synonym 'a conf = "(('a com) option) \<times> 'a"
    12 
    13 inductive_set
    14   etran :: "('a conf \<times> 'a conf) set" 
    15   and etran' :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"  ("_ -e\<rightarrow> _" [81,81] 80)
    16 where
    17   "P -e\<rightarrow> Q \<equiv> (P,Q) \<in> etran"
    18 | Env: "(P, s) -e\<rightarrow> (P, t)"
    19 
    20 lemma etranE: "c -e\<rightarrow> c' \<Longrightarrow> (\<And>P s t. c = (P, s) \<Longrightarrow> c' = (P, t) \<Longrightarrow> Q) \<Longrightarrow> Q"
    21   by (induct c, induct c', erule etran.cases, blast)
    22 
    23 subsubsection \<open>Component transitions\<close>
    24 
    25 inductive_set
    26   ctran :: "('a conf \<times> 'a conf) set"
    27   and ctran' :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c\<rightarrow> _" [81,81] 80)
    28   and ctrans :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c*\<rightarrow> _" [81,81] 80)
    29 where
    30   "P -c\<rightarrow> Q \<equiv> (P,Q) \<in> ctran"
    31 | "P -c*\<rightarrow> Q \<equiv> (P,Q) \<in> ctran^*"
    32 
    33 | Basic:  "(Some(Basic f), s) -c\<rightarrow> (None, f s)"
    34 
    35 | Seq1:   "(Some P0, s) -c\<rightarrow> (None, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some P1, t)"
    36 
    37 | Seq2:   "(Some P0, s) -c\<rightarrow> (Some P2, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some(Seq P2 P1), t)"
    38 
    39 | CondT: "s\<in>b  \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P1, s)"
    40 | CondF: "s\<notin>b \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P2, s)"
    41 
    42 | WhileF: "s\<notin>b \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (None, s)"
    43 | WhileT: "s\<in>b  \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (Some(Seq P (While b P)), s)"
    44 
    45 | Await:  "\<lbrakk>s\<in>b; (Some P, s) -c*\<rightarrow> (None, t)\<rbrakk> \<Longrightarrow> (Some(Await b P), s) -c\<rightarrow> (None, t)" 
    46 
    47 monos "rtrancl_mono"
    48 
    49 subsection \<open>Semantics of Parallel Programs\<close>
    50 
    51 type_synonym 'a par_conf = "('a par_com) \<times> 'a"
    52 
    53 inductive_set
    54   par_etran :: "('a par_conf \<times> 'a par_conf) set"
    55   and par_etran' :: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pe\<rightarrow> _" [81,81] 80)
    56 where
    57   "P -pe\<rightarrow> Q \<equiv> (P,Q) \<in> par_etran"
    58 | ParEnv:  "(Ps, s) -pe\<rightarrow> (Ps, t)"
    59 
    60 inductive_set
    61   par_ctran :: "('a par_conf \<times> 'a par_conf) set"
    62   and par_ctran' :: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pc\<rightarrow> _" [81,81] 80)
    63 where
    64   "P -pc\<rightarrow> Q \<equiv> (P,Q) \<in> par_ctran"
    65 | ParComp: "\<lbrakk>i<length Ps; (Ps!i, s) -c\<rightarrow> (r, t)\<rbrakk> \<Longrightarrow> (Ps, s) -pc\<rightarrow> (Ps[i:=r], t)"
    66 
    67 lemma par_ctranE: "c -pc\<rightarrow> c' \<Longrightarrow>
    68   (\<And>i Ps s r t. c = (Ps, s) \<Longrightarrow> c' = (Ps[i := r], t) \<Longrightarrow> i < length Ps \<Longrightarrow>
    69      (Ps ! i, s) -c\<rightarrow> (r, t) \<Longrightarrow> P) \<Longrightarrow> P"
    70   by (induct c, induct c', erule par_ctran.cases, blast)
    71 
    72 subsection \<open>Computations\<close>
    73 
    74 subsubsection \<open>Sequential computations\<close>
    75 
    76 type_synonym 'a confs = "'a conf list"
    77 
    78 inductive_set cptn :: "'a confs set"
    79 where
    80   CptnOne: "[(P,s)] \<in> cptn"
    81 | CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
    82 | CptnComp: "\<lbrakk>(P,s) -c\<rightarrow> (Q,t); (Q, t)#xs \<in> cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> cptn"
    83 
    84 definition cp :: "('a com) option \<Rightarrow> 'a \<Rightarrow> ('a confs) set" where
    85   "cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> cptn}"  
    86 
    87 subsubsection \<open>Parallel computations\<close>
    88 
    89 type_synonym 'a par_confs = "'a par_conf list"
    90 
    91 inductive_set par_cptn :: "'a par_confs set"
    92 where
    93   ParCptnOne: "[(P,s)] \<in> par_cptn"
    94 | ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
    95 | ParCptnComp: "\<lbrakk> (P,s) -pc\<rightarrow> (Q,t); (Q,t)#xs \<in> par_cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> par_cptn"
    96 
    97 definition par_cp :: "'a par_com \<Rightarrow> 'a \<Rightarrow> ('a par_confs) set" where
    98   "par_cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> par_cptn}"  
    99 
   100 subsection\<open>Modular Definition of Computation\<close>
   101 
   102 definition lift :: "'a com \<Rightarrow> 'a conf \<Rightarrow> 'a conf" where
   103   "lift Q \<equiv> \<lambda>(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))"
   104 
   105 inductive_set cptn_mod :: "('a confs) set"
   106 where
   107   CptnModOne: "[(P, s)] \<in> cptn_mod"
   108 | CptnModEnv: "(P, t)#xs \<in> cptn_mod \<Longrightarrow> (P, s)#(P, t)#xs \<in> cptn_mod"
   109 | CptnModNone: "\<lbrakk>(Some P, s) -c\<rightarrow> (None, t); (None, t)#xs \<in> cptn_mod \<rbrakk> \<Longrightarrow> (Some P,s)#(None, t)#xs \<in>cptn_mod"
   110 | CptnModCondT: "\<lbrakk>(Some P0, s)#ys \<in> cptn_mod; s \<in> b \<rbrakk> \<Longrightarrow> (Some(Cond b P0 P1), s)#(Some P0, s)#ys \<in> cptn_mod"
   111 | CptnModCondF: "\<lbrakk>(Some P1, s)#ys \<in> cptn_mod; s \<notin> b \<rbrakk> \<Longrightarrow> (Some(Cond b P0 P1), s)#(Some P1, s)#ys \<in> cptn_mod"
   112 | CptnModSeq1: "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; zs=map (lift P1) xs \<rbrakk>
   113                  \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod"
   114 | CptnModSeq2: 
   115   "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; fst(last ((Some P0, s)#xs)) = None; 
   116   (Some P1, snd(last ((Some P0, s)#xs)))#ys \<in> cptn_mod; 
   117   zs=(map (lift P1) xs)@ys \<rbrakk> \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod"
   118 
   119 | CptnModWhile1: 
   120   "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; s \<in> b; zs=map (lift (While b P)) xs \<rbrakk> 
   121   \<Longrightarrow> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \<in> cptn_mod"
   122 | CptnModWhile2: 
   123   "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; fst(last ((Some P, s)#xs))=None; s \<in> b; 
   124   zs=(map (lift (While b P)) xs)@ys; 
   125   (Some(While b P), snd(last ((Some P, s)#xs)))#ys \<in> cptn_mod\<rbrakk> 
   126   \<Longrightarrow> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \<in> cptn_mod"
   127 
   128 subsection \<open>Equivalence of Both Definitions.\<close>
   129 
   130 lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
   131   by (induct xs) auto
   132 
   133 lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow>
   134  (\<forall>s P Q zs. list=(Some (Seq P Q), s)#zs \<longrightarrow>
   135   (\<exists>xs. (Some P, s)#xs \<in> cptn_mod  \<and> (zs=(map (lift Q) xs) \<or>
   136   ( fst(((Some P, s)#xs)!length xs)=None \<and> 
   137   (\<exists>ys. (Some Q, snd(((Some P, s)#xs)!length xs))#ys \<in> cptn_mod  
   138   \<and> zs=(map (lift (Q)) xs)@ys)))))"
   139 apply(erule cptn_mod.induct)
   140 apply simp_all
   141     apply clarify
   142     apply(force intro:CptnModOne)
   143    apply clarify
   144    apply(erule_tac x=Pa in allE)
   145    apply(erule_tac x=Q in allE)
   146    apply simp
   147    apply clarify
   148    apply(erule disjE)
   149     apply(rule_tac x="(Some Pa,t)#xsa" in exI)
   150     apply(rule conjI)
   151      apply clarify
   152      apply(erule CptnModEnv)
   153     apply(rule disjI1)
   154     apply(simp add:lift_def)
   155    apply clarify
   156    apply(rule_tac x="(Some Pa,t)#xsa" in exI)
   157    apply(rule conjI)
   158     apply(erule CptnModEnv)
   159    apply(rule disjI2)
   160    apply(rule conjI)
   161     apply(case_tac xsa,simp,simp)
   162    apply(rule_tac x="ys" in exI)
   163    apply(rule conjI)
   164     apply simp
   165    apply(simp add:lift_def)
   166   apply clarify
   167   apply(erule ctran.cases,simp_all)
   168  apply clarify
   169  apply(rule_tac x="xs" in exI)
   170  apply simp
   171  apply clarify
   172 apply(rule_tac x="xs" in exI)
   173 apply(simp add: last_length)
   174 done
   175 
   176 lemma cptn_onlyif_cptn_mod_aux [rule_format]:
   177   "\<forall>s Q t xs.((Some a, s), Q, t) \<in> ctran \<longrightarrow> (Q, t) # xs \<in> cptn_mod 
   178   \<longrightarrow> (Some a, s) # (Q, t) # xs \<in> cptn_mod"
   179 apply(induct a)
   180 apply simp_all
   181 \<comment>\<open>basic\<close>
   182 apply clarify
   183 apply(erule ctran.cases,simp_all)
   184 apply(rule CptnModNone,rule Basic,simp)
   185 apply clarify
   186 apply(erule ctran.cases,simp_all)
   187 \<comment>\<open>Seq1\<close>
   188 apply(rule_tac xs="[(None,ta)]" in CptnModSeq2)
   189   apply(erule CptnModNone)
   190   apply(rule CptnModOne)
   191  apply simp
   192 apply simp
   193 apply(simp add:lift_def)
   194 \<comment>\<open>Seq2\<close>
   195 apply(erule_tac x=sa in allE)
   196 apply(erule_tac x="Some P2" in allE)
   197 apply(erule allE,erule impE, assumption)
   198 apply(drule div_seq,simp)
   199 apply clarify
   200 apply(erule disjE)
   201  apply clarify
   202  apply(erule allE,erule impE, assumption)
   203  apply(erule_tac CptnModSeq1)
   204  apply(simp add:lift_def)
   205 apply clarify 
   206 apply(erule allE,erule impE, assumption)
   207 apply(erule_tac CptnModSeq2)
   208   apply (simp add:last_length)
   209  apply (simp add:last_length)
   210 apply(simp add:lift_def)
   211 \<comment>\<open>Cond\<close>
   212 apply clarify
   213 apply(erule ctran.cases,simp_all)
   214 apply(force elim: CptnModCondT)
   215 apply(force elim: CptnModCondF)
   216 \<comment>\<open>While\<close>
   217 apply  clarify
   218 apply(erule ctran.cases,simp_all)
   219 apply(rule CptnModNone,erule WhileF,simp)
   220 apply(drule div_seq,force)
   221 apply clarify
   222 apply (erule disjE)
   223  apply(force elim:CptnModWhile1)
   224 apply clarify
   225 apply(force simp add:last_length elim:CptnModWhile2)
   226 \<comment>\<open>await\<close>
   227 apply clarify
   228 apply(erule ctran.cases,simp_all)
   229 apply(rule CptnModNone,erule Await,simp+)
   230 done
   231 
   232 lemma cptn_onlyif_cptn_mod [rule_format]: "c \<in> cptn \<Longrightarrow> c \<in> cptn_mod"
   233 apply(erule cptn.induct)
   234   apply(rule CptnModOne)
   235  apply(erule CptnModEnv)
   236 apply(case_tac P)
   237  apply simp
   238  apply(erule ctran.cases,simp_all)
   239 apply(force elim:cptn_onlyif_cptn_mod_aux)
   240 done
   241 
   242 lemma lift_is_cptn: "c\<in>cptn \<Longrightarrow> map (lift P) c \<in> cptn"
   243 apply(erule cptn.induct)
   244   apply(force simp add:lift_def CptnOne)
   245  apply(force intro:CptnEnv simp add:lift_def)
   246 apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.cases)
   247 done
   248 
   249 lemma cptn_append_is_cptn [rule_format]: 
   250  "\<forall>b a. b#c1\<in>cptn \<longrightarrow>  a#c2\<in>cptn \<longrightarrow> (b#c1)!length c1=a \<longrightarrow> b#c1@c2\<in>cptn"
   251 apply(induct c1)
   252  apply simp
   253 apply clarify
   254 apply(erule cptn.cases,simp_all)
   255  apply(force intro:CptnEnv)
   256 apply(force elim:CptnComp)
   257 done
   258 
   259 lemma last_lift: "\<lbrakk>xs\<noteq>[]; fst(xs!(length xs - (Suc 0)))=None\<rbrakk> 
   260  \<Longrightarrow> fst((map (lift P) xs)!(length (map (lift P) xs)- (Suc 0)))=(Some P)"
   261   by (cases "(xs ! (length xs - (Suc 0)))") (simp add:lift_def)
   262 
   263 lemma last_fst [rule_format]: "P((a#x)!length x) \<longrightarrow> \<not>P a \<longrightarrow> P (x!(length x - (Suc 0)))" 
   264   by (induct x) simp_all
   265 
   266 lemma last_fst_esp: 
   267  "fst(((Some a,s)#xs)!(length xs))=None \<Longrightarrow> fst(xs!(length xs - (Suc 0)))=None" 
   268 apply(erule last_fst)
   269 apply simp
   270 done
   271 
   272 lemma last_snd: "xs\<noteq>[] \<Longrightarrow> 
   273   snd(((map (lift P) xs))!(length (map (lift P) xs) - (Suc 0)))=snd(xs!(length xs - (Suc 0)))"
   274   by (cases "(xs ! (length xs - (Suc 0)))") (simp_all add:lift_def)
   275 
   276 lemma Cons_lift: "(Some (Seq P Q), s) # (map (lift Q) xs) = map (lift Q) ((Some P, s) # xs)"
   277   by (simp add:lift_def)
   278 
   279 lemma Cons_lift_append: 
   280   "(Some (Seq P Q), s) # (map (lift Q) xs) @ ys = map (lift Q) ((Some P, s) # xs)@ ys "
   281   by (simp add:lift_def)
   282 
   283 lemma lift_nth: "i<length xs \<Longrightarrow> map (lift Q) xs ! i = lift Q  (xs! i)"
   284   by (simp add:lift_def)
   285 
   286 lemma snd_lift: "i< length xs \<Longrightarrow> snd(lift Q (xs ! i))= snd (xs ! i)"
   287   by (cases "xs!i") (simp add:lift_def)
   288 
   289 lemma cptn_if_cptn_mod: "c \<in> cptn_mod \<Longrightarrow> c \<in> cptn"
   290 apply(erule cptn_mod.induct)
   291         apply(rule CptnOne)
   292        apply(erule CptnEnv)
   293       apply(erule CptnComp,simp)
   294      apply(rule CptnComp)
   295       apply(erule CondT,simp)
   296     apply(rule CptnComp)
   297      apply(erule CondF,simp)
   298 \<comment>\<open>Seq1\<close>
   299 apply(erule cptn.cases,simp_all)
   300   apply(rule CptnOne)
   301  apply clarify
   302  apply(drule_tac P=P1 in lift_is_cptn)
   303  apply(simp add:lift_def)
   304  apply(rule CptnEnv,simp)
   305 apply clarify
   306 apply(simp add:lift_def)
   307 apply(rule conjI)
   308  apply clarify
   309  apply(rule CptnComp)
   310   apply(rule Seq1,simp)
   311  apply(drule_tac P=P1 in lift_is_cptn)
   312  apply(simp add:lift_def)
   313 apply clarify
   314 apply(rule CptnComp)
   315  apply(rule Seq2,simp)
   316 apply(drule_tac P=P1 in lift_is_cptn)
   317 apply(simp add:lift_def)
   318 \<comment>\<open>Seq2\<close>
   319 apply(rule cptn_append_is_cptn)
   320   apply(drule_tac P=P1 in lift_is_cptn)
   321   apply(simp add:lift_def)
   322  apply simp
   323 apply(simp split: if_split_asm)
   324 apply(frule_tac P=P1 in last_lift)
   325  apply(rule last_fst_esp)
   326  apply (simp add:last_length)
   327 apply(simp add:Cons_lift lift_def split_def last_conv_nth)
   328 \<comment>\<open>While1\<close>
   329 apply(rule CptnComp)
   330  apply(rule WhileT,simp)
   331 apply(drule_tac P="While b P" in lift_is_cptn)
   332 apply(simp add:lift_def)
   333 \<comment>\<open>While2\<close>
   334 apply(rule CptnComp)
   335  apply(rule WhileT,simp)
   336 apply(rule cptn_append_is_cptn)
   337   apply(drule_tac P="While b P" in lift_is_cptn)
   338   apply(simp add:lift_def)
   339  apply simp
   340 apply(simp split: if_split_asm)
   341 apply(frule_tac P="While b P" in last_lift)
   342  apply(rule last_fst_esp,simp add:last_length)
   343 apply(simp add:Cons_lift lift_def split_def last_conv_nth)
   344 done
   345 
   346 theorem cptn_iff_cptn_mod: "(c \<in> cptn) = (c \<in> cptn_mod)"
   347 apply(rule iffI)
   348  apply(erule cptn_onlyif_cptn_mod)
   349 apply(erule cptn_if_cptn_mod)
   350 done
   351 
   352 section \<open>Validity  of Correctness Formulas\<close>
   353 
   354 subsection \<open>Validity for Component Programs.\<close>
   355 
   356 type_synonym 'a rgformula =
   357   "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
   358 
   359 definition assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set" where
   360   "assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
   361                c!i -e\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}"
   362 
   363 definition comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a confs) set" where
   364   "comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow> 
   365                c!i -c\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
   366                (fst (last c) = None \<longrightarrow> snd (last c) \<in> post)}"
   367 
   368 definition com_validity :: "'a com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool" 
   369                  ("\<Turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45) where
   370   "\<Turnstile> P sat [pre, rely, guar, post] \<equiv> 
   371    \<forall>s. cp (Some P) s \<inter> assum(pre, rely) \<subseteq> comm(guar, post)"
   372 
   373 subsection \<open>Validity for Parallel Programs.\<close>
   374 
   375 definition All_None :: "(('a com) option) list \<Rightarrow> bool" where
   376   "All_None xs \<equiv> \<forall>c\<in>set xs. c=None"
   377 
   378 definition par_assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a par_confs) set" where
   379   "par_assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
   380              c!i -pe\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}"
   381 
   382 definition par_comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a par_confs) set" where
   383   "par_comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow>   
   384         c!i -pc\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
   385          (All_None (fst (last c)) \<longrightarrow> snd( last c) \<in> post)}"
   386 
   387 definition par_com_validity :: "'a  par_com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set 
   388 \<Rightarrow> 'a set \<Rightarrow> bool"  ("\<Turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45) where
   389   "\<Turnstile> Ps SAT [pre, rely, guar, post] \<equiv> 
   390    \<forall>s. par_cp Ps s \<inter> par_assum(pre, rely) \<subseteq> par_comm(guar, post)"
   391 
   392 subsection \<open>Compositionality of the Semantics\<close>
   393 
   394 subsubsection \<open>Definition of the conjoin operator\<close>
   395 
   396 definition same_length :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
   397   "same_length c clist \<equiv> (\<forall>i<length clist. length(clist!i)=length c)"
   398  
   399 definition same_state :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
   400   "same_state c clist \<equiv> (\<forall>i <length clist. \<forall>j<length c. snd(c!j) = snd((clist!i)!j))"
   401 
   402 definition same_program :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
   403   "same_program c clist \<equiv> (\<forall>j<length c. fst(c!j) = map (\<lambda>x. fst(nth x j)) clist)"
   404 
   405 definition compat_label :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" where
   406   "compat_label c clist \<equiv> (\<forall>j. Suc j<length c \<longrightarrow> 
   407          (c!j -pc\<rightarrow> c!Suc j \<and> (\<exists>i<length clist. (clist!i)!j -c\<rightarrow> (clist!i)! Suc j \<and> 
   408                        (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> 
   409          (c!j -pe\<rightarrow> c!Suc j \<and> (\<forall>i<length clist. (clist!i)!j -e\<rightarrow> (clist!i)! Suc j)))"
   410 
   411 definition conjoin :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"  ("_ \<propto> _" [65,65] 64) where
   412   "c \<propto> clist \<equiv> (same_length c clist) \<and> (same_state c clist) \<and> (same_program c clist) \<and> (compat_label c clist)"
   413 
   414 subsubsection \<open>Some previous lemmas\<close>
   415 
   416 lemma list_eq_if [rule_format]: 
   417   "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)"
   418   by (induct xs) auto
   419 
   420 lemma list_eq: "(length xs = length ys \<and> (\<forall>i<length xs. xs!i=ys!i)) = (xs=ys)"
   421 apply(rule iffI)
   422  apply clarify
   423  apply(erule nth_equalityI)
   424  apply simp+
   425 done
   426 
   427 lemma nth_tl: "\<lbrakk> ys!0=a; ys\<noteq>[] \<rbrakk> \<Longrightarrow> ys=(a#(tl ys))"
   428   by (cases ys) simp_all
   429 
   430 lemma nth_tl_if [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P ys \<longrightarrow> P (a#(tl ys))"
   431   by (induct ys) simp_all
   432 
   433 lemma nth_tl_onlyif [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P (a#(tl ys)) \<longrightarrow> P ys"
   434   by (induct ys) simp_all
   435 
   436 lemma seq_not_eq1: "Seq c1 c2\<noteq>c1"
   437   by (induct c1) auto
   438 
   439 lemma seq_not_eq2: "Seq c1 c2\<noteq>c2"
   440   by (induct c2) auto
   441 
   442 lemma if_not_eq1: "Cond b c1 c2 \<noteq>c1"
   443   by (induct c1) auto
   444 
   445 lemma if_not_eq2: "Cond b c1 c2\<noteq>c2"
   446   by (induct c2) auto
   447 
   448 lemmas seq_and_if_not_eq [simp] = seq_not_eq1 seq_not_eq2 
   449 seq_not_eq1 [THEN not_sym] seq_not_eq2 [THEN not_sym] 
   450 if_not_eq1 if_not_eq2 if_not_eq1 [THEN not_sym] if_not_eq2 [THEN not_sym]
   451 
   452 lemma prog_not_eq_in_ctran_aux:
   453   assumes c: "(P,s) -c\<rightarrow> (Q,t)"
   454   shows "P\<noteq>Q" using c
   455   by (induct x1 \<equiv> "(P,s)" x2 \<equiv> "(Q,t)" arbitrary: P s Q t) auto
   456 
   457 lemma prog_not_eq_in_ctran [simp]: "\<not> (P,s) -c\<rightarrow> (P,t)"
   458 apply clarify
   459 apply(drule prog_not_eq_in_ctran_aux)
   460 apply simp
   461 done
   462 
   463 lemma prog_not_eq_in_par_ctran_aux [rule_format]: "(P,s) -pc\<rightarrow> (Q,t) \<Longrightarrow> (P\<noteq>Q)"
   464 apply(erule par_ctran.induct)
   465 apply(drule prog_not_eq_in_ctran_aux)
   466 apply clarify
   467 apply(drule list_eq_if)
   468  apply simp_all
   469 apply force
   470 done
   471 
   472 lemma prog_not_eq_in_par_ctran [simp]: "\<not> (P,s) -pc\<rightarrow> (P,t)"
   473 apply clarify
   474 apply(drule prog_not_eq_in_par_ctran_aux)
   475 apply simp
   476 done
   477 
   478 lemma tl_in_cptn: "\<lbrakk> a#xs \<in>cptn; xs\<noteq>[] \<rbrakk> \<Longrightarrow> xs\<in>cptn"
   479   by (force elim: cptn.cases)
   480 
   481 lemma tl_zero[rule_format]: 
   482   "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)"
   483   by (induct ys) simp_all
   484 
   485 subsection \<open>The Semantics is Compositional\<close>
   486 
   487 lemma aux_if [rule_format]: 
   488   "\<forall>xs s clist. (length clist = length xs \<and> (\<forall>i<length xs. (xs!i,s)#clist!i \<in> cptn) 
   489   \<and> ((xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#snd i) (zip xs clist)) 
   490    \<longrightarrow> (xs, s)#ys \<in> par_cptn)"
   491 apply(induct ys)
   492  apply(clarify)
   493  apply(rule ParCptnOne)
   494 apply(clarify)
   495 apply(simp add:conjoin_def compat_label_def)
   496 apply clarify
   497 apply(erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (P j \<or> Q j)" for H P Q in all_dupE, simp)
   498 apply(erule disjE)
   499 \<comment>\<open>first step is a Component step\<close>
   500  apply clarify 
   501  apply simp
   502  apply(subgoal_tac "a=(xs[i:=(fst(clist!i!0))])")
   503   apply(subgoal_tac "b=snd(clist!i!0)",simp)
   504    prefer 2
   505    apply(simp add: same_state_def)
   506    apply(erule_tac x=i in allE,erule impE,assumption, 
   507          erule_tac x=1 and P="\<lambda>j. (H j) \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE, simp)
   508   prefer 2
   509   apply(simp add:same_program_def)
   510   apply(erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=(t j)" for H s t in allE,simp)
   511   apply(rule nth_equalityI,simp)
   512   apply clarify
   513   apply(case_tac "i=ia",simp,simp)
   514   apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   515   apply(drule_tac t=i in not_sym,simp)
   516   apply(erule etranE,simp)
   517  apply(rule ParCptnComp)
   518   apply(erule ParComp,simp)
   519 \<comment>\<open>applying the induction hypothesis\<close>
   520  apply(erule_tac x="xs[i := fst (clist ! i ! 0)]" in allE)
   521  apply(erule_tac x="snd (clist ! i ! 0)" in allE)
   522  apply(erule mp)
   523  apply(rule_tac x="map tl clist" in exI,simp)
   524  apply(rule conjI,clarify)
   525   apply(case_tac "i=ia",simp)
   526    apply(rule nth_tl_if)
   527      apply(force simp add:same_length_def length_Suc_conv)
   528     apply simp
   529    apply(erule allE,erule impE,assumption,erule tl_in_cptn)
   530    apply(force simp add:same_length_def length_Suc_conv)
   531   apply(rule nth_tl_if)
   532     apply(force simp add:same_length_def length_Suc_conv)
   533    apply(simp add:same_state_def)
   534    apply(erule_tac x=ia in allE, erule impE, assumption, 
   535      erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   536    apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   537    apply(drule_tac t=i  in not_sym,simp)
   538    apply(erule etranE,simp)
   539   apply(erule allE,erule impE,assumption,erule tl_in_cptn)
   540   apply(force simp add:same_length_def length_Suc_conv)
   541  apply(simp add:same_length_def same_state_def)
   542  apply(rule conjI)
   543   apply clarify
   544   apply(case_tac j,simp,simp)
   545   apply(erule_tac x=ia in allE, erule impE, assumption,
   546         erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   547   apply(force simp add:same_length_def length_Suc_conv)
   548  apply(rule conjI)
   549   apply(simp add:same_program_def)
   550   apply clarify
   551   apply(case_tac j,simp)
   552    apply(rule nth_equalityI,simp)
   553    apply clarify
   554    apply(case_tac "i=ia",simp,simp)
   555   apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=(t j)" for H s t in allE,simp)
   556   apply(rule nth_equalityI,simp,simp)
   557   apply(force simp add:length_Suc_conv)
   558  apply(rule allI,rule impI)
   559  apply(erule_tac x="Suc j" and P="\<lambda>j. H j \<longrightarrow> (I j \<or> J j)" for H I J in allE,simp)
   560  apply(erule disjE) 
   561   apply clarify
   562   apply(rule_tac x=ia in exI,simp)
   563   apply(case_tac "i=ia",simp)
   564    apply(rule conjI)
   565     apply(force simp add: length_Suc_conv)
   566    apply clarify
   567    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE,assumption)
   568    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE,assumption)
   569    apply simp
   570    apply(case_tac j,simp)
   571     apply(rule tl_zero)
   572       apply(erule_tac x=l in allE, erule impE, assumption, 
   573             erule_tac x=1 and P="\<lambda>j.  (H j) \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   574       apply(force elim:etranE intro:Env)
   575      apply force
   576     apply force
   577    apply simp
   578    apply(rule tl_zero)
   579      apply(erule tl_zero)
   580       apply force
   581      apply force
   582     apply force
   583    apply force
   584   apply(rule conjI,simp)
   585    apply(rule nth_tl_if)
   586      apply force
   587     apply(erule_tac x=ia  in allE, erule impE, assumption,
   588           erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   589     apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   590     apply(drule_tac t=i  in not_sym,simp)
   591     apply(erule etranE,simp)
   592    apply(erule tl_zero)
   593     apply force
   594    apply force
   595   apply clarify
   596   apply(case_tac "i=l",simp)
   597    apply(rule nth_tl_if)
   598      apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   599     apply simp
   600    apply(erule_tac P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE,assumption,erule impE,assumption)
   601    apply(erule tl_zero,force)
   602    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   603    apply(rule nth_tl_if)
   604      apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   605     apply(erule_tac x=l  in allE, erule impE, assumption,
   606           erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   607     apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE, assumption,simp)
   608     apply(erule etranE,simp)
   609    apply(rule tl_zero)
   610     apply force
   611    apply force
   612   apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   613  apply(rule disjI2)
   614  apply(case_tac j,simp)
   615   apply clarify
   616   apply(rule tl_zero)
   617     apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j\<in>etran" for H I in allE,erule impE, assumption)
   618     apply(case_tac "i=ia",simp,simp)
   619     apply(erule_tac x=ia  in allE, erule impE, assumption,
   620     erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   621     apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE,erule impE, assumption,simp)
   622     apply(force elim:etranE intro:Env)
   623    apply force
   624   apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   625  apply simp
   626  apply clarify
   627  apply(rule tl_zero)
   628    apply(rule tl_zero,force)
   629     apply force
   630    apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   631   apply force
   632  apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   633 \<comment>\<open>first step is an environmental step\<close>
   634 apply clarify
   635 apply(erule par_etran.cases)
   636 apply simp
   637 apply(rule ParCptnEnv)
   638 apply(erule_tac x="Ps" in allE)
   639 apply(erule_tac x="t" in allE)
   640 apply(erule mp)
   641 apply(rule_tac x="map tl clist" in exI,simp)
   642 apply(rule conjI)
   643  apply clarify
   644  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> I j \<in> cptn" for H I in allE,simp)
   645  apply(erule cptn.cases)
   646    apply(simp add:same_length_def)
   647    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   648   apply(simp add:same_state_def)
   649   apply(erule_tac x=i  in allE, erule impE, assumption,
   650    erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   651  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> J j \<in>etran" for H J in allE,simp)
   652  apply(erule etranE,simp)
   653 apply(simp add:same_state_def same_length_def)
   654 apply(rule conjI,clarify)
   655  apply(case_tac j,simp,simp)
   656  apply(erule_tac x=i  in allE, erule impE, assumption,
   657        erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   658  apply(rule tl_zero)
   659    apply(simp)
   660   apply force
   661  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   662 apply(rule conjI)
   663  apply(simp add:same_program_def)
   664  apply clarify
   665  apply(case_tac j,simp)
   666   apply(rule nth_equalityI,simp)
   667   apply clarify
   668   apply simp
   669  apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=(t j)" for H s t in allE,simp)
   670  apply(rule nth_equalityI,simp,simp)
   671  apply(force simp add:length_Suc_conv)
   672 apply(rule allI,rule impI)
   673 apply(erule_tac x="Suc j" and P="\<lambda>j. H j \<longrightarrow> (I j \<or> J j)" for H I J in allE,simp)
   674 apply(erule disjE) 
   675  apply clarify
   676  apply(rule_tac x=i in exI,simp)
   677  apply(rule conjI)
   678   apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
   679   apply(erule etranE,simp)
   680   apply(erule_tac x=i  in allE, erule impE, assumption,
   681         erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   682   apply(rule nth_tl_if)
   683    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   684   apply simp
   685  apply(erule tl_zero,force) 
   686   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   687  apply clarify
   688  apply(erule_tac x=l and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
   689  apply(erule etranE,simp)
   690  apply(erule_tac x=l  in allE, erule impE, assumption,
   691        erule_tac x=1 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   692  apply(rule nth_tl_if)
   693    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   694   apply simp
   695   apply(rule tl_zero,force)
   696   apply force
   697  apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   698 apply(rule disjI2)
   699 apply simp
   700 apply clarify
   701 apply(case_tac j,simp)
   702  apply(rule tl_zero)
   703    apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
   704    apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> J i \<in>etran" for H J in allE, erule impE, assumption)
   705    apply(force elim:etranE intro:Env)
   706   apply force
   707  apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   708 apply simp
   709 apply(rule tl_zero)
   710   apply(rule tl_zero,force)
   711    apply force
   712   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   713  apply force
   714 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   715 done
   716 
   717 lemma aux_onlyif [rule_format]: "\<forall>xs s. (xs, s)#ys \<in> par_cptn \<longrightarrow> 
   718   (\<exists>clist. (length clist = length xs) \<and> 
   719   (xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist) \<and> 
   720   (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))"
   721 apply(induct ys)
   722  apply(clarify)
   723  apply(rule_tac x="map (\<lambda>i. []) [0..<length xs]" in exI)
   724  apply(simp add: conjoin_def same_length_def same_state_def same_program_def compat_label_def)
   725  apply(rule conjI)
   726   apply(rule nth_equalityI,simp,simp)
   727  apply(force intro: cptn.intros)
   728 apply(clarify)
   729 apply(erule par_cptn.cases,simp)
   730  apply simp
   731  apply(erule_tac x="xs" in allE)
   732  apply(erule_tac x="t" in allE,simp)
   733  apply clarify
   734  apply(rule_tac x="(map (\<lambda>j. (P!j, t)#(clist!j)) [0..<length P])" in exI,simp)
   735  apply(rule conjI)
   736   prefer 2
   737   apply clarify
   738   apply(rule CptnEnv,simp)
   739  apply(simp add:conjoin_def same_length_def same_state_def)
   740  apply (rule conjI)
   741   apply clarify
   742   apply(case_tac j,simp,simp)
   743  apply(rule conjI)
   744   apply(simp add:same_program_def)
   745   apply clarify
   746   apply(case_tac j,simp)
   747    apply(rule nth_equalityI,simp,simp)
   748   apply simp
   749   apply(rule nth_equalityI,simp,simp)
   750  apply(simp add:compat_label_def)
   751  apply clarify
   752  apply(case_tac j,simp)
   753   apply(simp add:ParEnv)
   754   apply clarify
   755   apply(simp add:Env)
   756  apply simp
   757  apply(erule_tac x=nat in allE,erule impE, assumption)
   758  apply(erule disjE,simp)
   759   apply clarify
   760   apply(rule_tac x=i in exI,simp)
   761  apply force
   762 apply(erule par_ctran.cases,simp)
   763 apply(erule_tac x="Ps[i:=r]" in allE)
   764 apply(erule_tac x="ta" in allE,simp)
   765 apply clarify
   766 apply(rule_tac x="(map (\<lambda>j. (Ps!j, ta)#(clist!j)) [0..<length Ps]) [i:=((r, ta)#(clist!i))]" in exI,simp)
   767 apply(rule conjI)
   768  prefer 2
   769  apply clarify
   770  apply(case_tac "i=ia",simp)
   771   apply(erule CptnComp)
   772   apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (I j \<in> cptn)" for H I in allE,simp)
   773  apply simp
   774  apply(erule_tac x=ia in allE)
   775  apply(rule CptnEnv,simp)
   776 apply(simp add:conjoin_def)
   777 apply (rule conjI)
   778  apply(simp add:same_length_def)
   779  apply clarify
   780  apply(case_tac "i=ia",simp,simp)
   781 apply(rule conjI)
   782  apply(simp add:same_state_def)
   783  apply clarify
   784  apply(case_tac j, simp, simp (no_asm_simp))
   785  apply(case_tac "i=ia",simp,simp)
   786 apply(rule conjI)
   787  apply(simp add:same_program_def)
   788  apply clarify
   789  apply(case_tac j,simp)
   790   apply(rule nth_equalityI,simp,simp)
   791  apply simp
   792  apply(rule nth_equalityI,simp,simp)
   793  apply(erule_tac x=nat and P="\<lambda>j. H j \<longrightarrow> (fst (a j))=((b j))" for H a b in allE)
   794  apply(case_tac nat)
   795   apply clarify
   796   apply(case_tac "i=ia",simp,simp)
   797  apply clarify
   798  apply(case_tac "i=ia",simp,simp)
   799 apply(simp add:compat_label_def)
   800 apply clarify
   801 apply(case_tac j)
   802  apply(rule conjI,simp)
   803   apply(erule ParComp,assumption)
   804   apply clarify
   805   apply(rule_tac x=i in exI,simp)
   806  apply clarify
   807  apply(rule Env)
   808 apply simp
   809 apply(erule_tac x=nat and P="\<lambda>j. H j \<longrightarrow> (P j \<or> Q j)" for H P Q in allE,simp)
   810 apply(erule disjE)
   811  apply clarify
   812  apply(rule_tac x=ia in exI,simp)
   813  apply(rule conjI)
   814   apply(case_tac "i=ia",simp,simp)
   815  apply clarify
   816  apply(case_tac "i=l",simp)
   817   apply(case_tac "l=ia",simp,simp)
   818   apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
   819  apply simp
   820  apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
   821 apply clarify
   822 apply(erule_tac x=ia and P="\<lambda>j. H j \<longrightarrow> (P j)\<in>etran" for H P in allE, erule impE, assumption)
   823 apply(case_tac "i=ia",simp,simp)
   824 done
   825 
   826 lemma one_iff_aux: "xs\<noteq>[] \<Longrightarrow> (\<forall>ys. ((xs, s)#ys \<in> par_cptn) = 
   827  (\<exists>clist. length clist= length xs \<and> 
   828  ((xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist)) \<and> 
   829  (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))) = 
   830  (par_cp (xs) s = {c. \<exists>clist. (length clist)=(length xs) \<and>
   831  (\<forall>i<length clist. (clist!i) \<in> cp(xs!i) s) \<and> c \<propto> clist})" 
   832 apply (rule iffI)
   833  apply(rule subset_antisym)
   834   apply(rule subsetI) 
   835   apply(clarify)
   836   apply(simp add:par_cp_def cp_def)
   837   apply(case_tac x)
   838    apply(force elim:par_cptn.cases)
   839   apply simp
   840   apply(rename_tac a list)
   841   apply(erule_tac x="list" in allE)
   842   apply clarify
   843   apply simp
   844   apply(rule_tac x="map (\<lambda>i. (fst i, s) # snd i) (zip xs clist)" in exI,simp)
   845  apply(rule subsetI) 
   846  apply(clarify)
   847  apply(case_tac x)
   848   apply(erule_tac x=0 in allE)
   849   apply(simp add:cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def)
   850   apply clarify
   851   apply(erule cptn.cases,force,force,force)
   852  apply(simp add:par_cp_def conjoin_def  same_length_def same_program_def same_state_def compat_label_def)
   853  apply clarify
   854  apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in all_dupE)
   855  apply(subgoal_tac "a = xs")
   856   apply(subgoal_tac "b = s",simp)
   857    prefer 3
   858    apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (fst (s j))=((t j))" for H s t in allE)
   859    apply (simp add:cp_def)
   860    apply(rule nth_equalityI,simp,simp)
   861   prefer 2
   862   apply(erule_tac x=0 in allE)
   863   apply (simp add:cp_def)
   864   apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (\<forall>i. T i \<longrightarrow> (snd (d j i))=(snd (e j i)))" for H T d e in allE,simp)
   865   apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   866  apply(erule_tac x=list in allE)
   867  apply(rule_tac x="map tl clist" in exI,simp) 
   868  apply(rule conjI)
   869   apply clarify
   870   apply(case_tac j,simp)
   871    apply(erule_tac x=i  in allE, erule impE, assumption,
   872         erule_tac x="0" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE,simp)
   873   apply(erule_tac x=i  in allE, erule impE, assumption,
   874         erule_tac x="Suc nat" and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   875   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   876   apply(case_tac "clist!i",simp,simp)
   877  apply(rule conjI)
   878   apply clarify
   879   apply(rule nth_equalityI,simp,simp)
   880   apply(case_tac j)
   881    apply clarify
   882    apply(erule_tac x=i in allE)
   883    apply(simp add:cp_def)
   884   apply clarify
   885   apply simp
   886   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   887   apply(case_tac "clist!i",simp,simp)
   888  apply(thin_tac "H = (\<exists>i. J i)" for H J)
   889  apply(rule conjI)
   890   apply clarify
   891   apply(erule_tac x=j in allE,erule impE, assumption,erule disjE)
   892    apply clarify
   893    apply(rule_tac x=i in exI,simp)
   894    apply(case_tac j,simp)
   895     apply(rule conjI)
   896      apply(erule_tac x=i in allE)
   897      apply(simp add:cp_def)
   898      apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   899      apply(case_tac "clist!i",simp,simp)
   900     apply clarify
   901     apply(erule_tac x=l in allE)
   902     apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   903     apply clarify
   904     apply(simp add:cp_def)
   905     apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   906     apply(case_tac "clist!l",simp,simp)
   907    apply simp
   908    apply(rule conjI)
   909     apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   910     apply(case_tac "clist!i",simp,simp)
   911    apply clarify
   912    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   913    apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   914    apply(case_tac "clist!l",simp,simp)
   915   apply clarify
   916   apply(erule_tac x=i in allE)
   917   apply(simp add:cp_def)
   918   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   919   apply(case_tac "clist!i",simp)
   920   apply(rule nth_tl_if,simp,simp)
   921   apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (P j)\<in>etran" for H P in allE, erule impE, assumption,simp)
   922   apply(simp add:cp_def)
   923   apply clarify
   924   apply(rule nth_tl_if)
   925    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   926    apply(case_tac "clist!i",simp,simp)
   927   apply force
   928  apply force
   929 apply clarify
   930 apply(rule iffI)
   931  apply(simp add:par_cp_def)
   932  apply(erule_tac c="(xs, s) # ys" in equalityCE)
   933   apply simp
   934   apply clarify
   935   apply(rule_tac x="map tl clist" in exI)
   936   apply simp
   937   apply (rule conjI)
   938    apply(simp add:conjoin_def cp_def)
   939    apply(rule conjI)
   940     apply clarify
   941     apply(unfold same_length_def)
   942     apply clarify
   943     apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,simp)
   944    apply(rule conjI)
   945     apply(simp add:same_state_def)
   946     apply clarify
   947     apply(erule_tac x=i in allE, erule impE, assumption,
   948        erule_tac x=j and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE)
   949     apply(case_tac j,simp)
   950     apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   951     apply(case_tac "clist!i",simp,simp)
   952    apply(rule conjI)
   953     apply(simp add:same_program_def)
   954     apply clarify
   955     apply(rule nth_equalityI,simp,simp)
   956     apply(case_tac j,simp)
   957     apply clarify
   958     apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   959     apply(case_tac "clist!i",simp,simp)
   960    apply clarify
   961    apply(simp add:compat_label_def)
   962    apply(rule allI,rule impI)
   963    apply(erule_tac x=j in allE,erule impE, assumption)
   964    apply(erule disjE)
   965     apply clarify
   966     apply(rule_tac x=i in exI,simp)
   967     apply(rule conjI)
   968      apply(erule_tac x=i in allE)
   969      apply(case_tac j,simp)
   970       apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   971       apply(case_tac "clist!i",simp,simp)
   972      apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   973      apply(case_tac "clist!i",simp,simp)
   974     apply clarify
   975     apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> I j \<longrightarrow> J j" for H I J in allE)
   976     apply(erule_tac x=l and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE)
   977     apply(case_tac "clist!l",simp,simp)
   978     apply(erule_tac x=l in allE,simp)
   979    apply(rule disjI2)
   980    apply clarify
   981    apply(rule tl_zero)
   982      apply(case_tac j,simp,simp)
   983      apply(rule tl_zero,force)   
   984       apply force
   985      apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   986     apply force
   987    apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (length (s j) = t)" for H s t in allE,force)
   988   apply clarify
   989   apply(erule_tac x=i in allE)
   990   apply(simp add:cp_def)
   991   apply(rule nth_tl_if)
   992     apply(simp add:conjoin_def)
   993     apply clarify
   994     apply(simp add:same_length_def)
   995     apply(erule_tac x=i in allE,simp)
   996    apply simp
   997   apply simp
   998  apply simp
   999 apply clarify
  1000 apply(erule_tac c="(xs, s) # ys" in equalityCE)
  1001  apply(simp add:par_cp_def)
  1002 apply simp
  1003 apply(erule_tac x="map (\<lambda>i. (fst i, s) # snd i) (zip xs clist)" in allE)
  1004 apply simp
  1005 apply clarify
  1006 apply(simp add:cp_def)
  1007 done
  1008 
  1009 theorem one: "xs\<noteq>[] \<Longrightarrow> 
  1010  par_cp xs s = {c. \<exists>clist. (length clist)=(length xs) \<and> 
  1011                (\<forall>i<length clist. (clist!i) \<in> cp(xs!i) s) \<and> c \<propto> clist}"
  1012 apply(frule one_iff_aux)
  1013 apply(drule sym)
  1014 apply(erule iffD2)
  1015 apply clarify
  1016 apply(rule iffI)
  1017  apply(erule aux_onlyif)
  1018 apply clarify
  1019 apply(force intro:aux_if)
  1020 done
  1021 
  1022 end