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