src/HOL/Hoare_Parallel/RG_Tran.thy
changeset 32621 a073cb249a06
parent 23746 a455e69c31cc
child 35416 d8d7d1b785af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hoare_Parallel/RG_Tran.thy	Mon Sep 21 10:58:25 2009 +0200
     1.3 @@ -0,0 +1,1075 @@
     1.4 +header {* \section{Operational Semantics} *}
     1.5 +
     1.6 +theory RG_Tran
     1.7 +imports RG_Com
     1.8 +begin
     1.9 +
    1.10 +subsection {* Semantics of Component Programs *}
    1.11 +
    1.12 +subsubsection {* Environment transitions *}
    1.13 +
    1.14 +types 'a conf = "(('a com) option) \<times> 'a"
    1.15 +
    1.16 +inductive_set
    1.17 +  etran :: "('a conf \<times> 'a conf) set" 
    1.18 +  and etran' :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"  ("_ -e\<rightarrow> _" [81,81] 80)
    1.19 +where
    1.20 +  "P -e\<rightarrow> Q \<equiv> (P,Q) \<in> etran"
    1.21 +| Env: "(P, s) -e\<rightarrow> (P, t)"
    1.22 +
    1.23 +lemma etranE: "c -e\<rightarrow> c' \<Longrightarrow> (\<And>P s t. c = (P, s) \<Longrightarrow> c' = (P, t) \<Longrightarrow> Q) \<Longrightarrow> Q"
    1.24 +  by (induct c, induct c', erule etran.cases, blast)
    1.25 +
    1.26 +subsubsection {* Component transitions *}
    1.27 +
    1.28 +inductive_set
    1.29 +  ctran :: "('a conf \<times> 'a conf) set"
    1.30 +  and ctran' :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c\<rightarrow> _" [81,81] 80)
    1.31 +  and ctrans :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c*\<rightarrow> _" [81,81] 80)
    1.32 +where
    1.33 +  "P -c\<rightarrow> Q \<equiv> (P,Q) \<in> ctran"
    1.34 +| "P -c*\<rightarrow> Q \<equiv> (P,Q) \<in> ctran^*"
    1.35 +
    1.36 +| Basic:  "(Some(Basic f), s) -c\<rightarrow> (None, f s)"
    1.37 +
    1.38 +| Seq1:   "(Some P0, s) -c\<rightarrow> (None, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some P1, t)"
    1.39 +
    1.40 +| Seq2:   "(Some P0, s) -c\<rightarrow> (Some P2, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some(Seq P2 P1), t)"
    1.41 +
    1.42 +| CondT: "s\<in>b  \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P1, s)"
    1.43 +| CondF: "s\<notin>b \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P2, s)"
    1.44 +
    1.45 +| WhileF: "s\<notin>b \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (None, s)"
    1.46 +| WhileT: "s\<in>b  \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (Some(Seq P (While b P)), s)"
    1.47 +
    1.48 +| Await:  "\<lbrakk>s\<in>b; (Some P, s) -c*\<rightarrow> (None, t)\<rbrakk> \<Longrightarrow> (Some(Await b P), s) -c\<rightarrow> (None, t)" 
    1.49 +
    1.50 +monos "rtrancl_mono"
    1.51 +
    1.52 +subsection {* Semantics of Parallel Programs *}
    1.53 +
    1.54 +types 'a par_conf = "('a par_com) \<times> 'a"
    1.55 +
    1.56 +inductive_set
    1.57 +  par_etran :: "('a par_conf \<times> 'a par_conf) set"
    1.58 +  and par_etran' :: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pe\<rightarrow> _" [81,81] 80)
    1.59 +where
    1.60 +  "P -pe\<rightarrow> Q \<equiv> (P,Q) \<in> par_etran"
    1.61 +| ParEnv:  "(Ps, s) -pe\<rightarrow> (Ps, t)"
    1.62 +
    1.63 +inductive_set
    1.64 +  par_ctran :: "('a par_conf \<times> 'a par_conf) set"
    1.65 +  and par_ctran' :: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pc\<rightarrow> _" [81,81] 80)
    1.66 +where
    1.67 +  "P -pc\<rightarrow> Q \<equiv> (P,Q) \<in> par_ctran"
    1.68 +| ParComp: "\<lbrakk>i<length Ps; (Ps!i, s) -c\<rightarrow> (r, t)\<rbrakk> \<Longrightarrow> (Ps, s) -pc\<rightarrow> (Ps[i:=r], t)"
    1.69 +
    1.70 +lemma par_ctranE: "c -pc\<rightarrow> c' \<Longrightarrow>
    1.71 +  (\<And>i Ps s r t. c = (Ps, s) \<Longrightarrow> c' = (Ps[i := r], t) \<Longrightarrow> i < length Ps \<Longrightarrow>
    1.72 +     (Ps ! i, s) -c\<rightarrow> (r, t) \<Longrightarrow> P) \<Longrightarrow> P"
    1.73 +  by (induct c, induct c', erule par_ctran.cases, blast)
    1.74 +
    1.75 +subsection {* Computations *}
    1.76 +
    1.77 +subsubsection {* Sequential computations *}
    1.78 +
    1.79 +types 'a confs = "('a conf) list"
    1.80 +
    1.81 +inductive_set cptn :: "('a confs) set"
    1.82 +where
    1.83 +  CptnOne: "[(P,s)] \<in> cptn"
    1.84 +| CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
    1.85 +| CptnComp: "\<lbrakk>(P,s) -c\<rightarrow> (Q,t); (Q, t)#xs \<in> cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> cptn"
    1.86 +
    1.87 +constdefs
    1.88 +  cp :: "('a com) option \<Rightarrow> 'a \<Rightarrow> ('a confs) set"
    1.89 +  "cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> cptn}"  
    1.90 +
    1.91 +subsubsection {* Parallel computations *}
    1.92 +
    1.93 +types  'a par_confs = "('a par_conf) list"
    1.94 +
    1.95 +inductive_set par_cptn :: "('a par_confs) set"
    1.96 +where
    1.97 +  ParCptnOne: "[(P,s)] \<in> par_cptn"
    1.98 +| ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
    1.99 +| ParCptnComp: "\<lbrakk> (P,s) -pc\<rightarrow> (Q,t); (Q,t)#xs \<in> par_cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> par_cptn"
   1.100 +
   1.101 +constdefs
   1.102 +  par_cp :: "'a par_com \<Rightarrow> 'a \<Rightarrow> ('a par_confs) set"
   1.103 +  "par_cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> par_cptn}"  
   1.104 +
   1.105 +subsection{* Modular Definition of Computation *}
   1.106 +
   1.107 +constdefs 
   1.108 +  lift :: "'a com \<Rightarrow> 'a conf \<Rightarrow> 'a conf"
   1.109 +  "lift Q \<equiv> \<lambda>(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))"
   1.110 +
   1.111 +inductive_set cptn_mod :: "('a confs) set"
   1.112 +where
   1.113 +  CptnModOne: "[(P, s)] \<in> cptn_mod"
   1.114 +| CptnModEnv: "(P, t)#xs \<in> cptn_mod \<Longrightarrow> (P, s)#(P, t)#xs \<in> cptn_mod"
   1.115 +| 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"
   1.116 +| 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"
   1.117 +| 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"
   1.118 +| CptnModSeq1: "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; zs=map (lift P1) xs \<rbrakk>
   1.119 +                 \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod"
   1.120 +| CptnModSeq2: 
   1.121 +  "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; fst(last ((Some P0, s)#xs)) = None; 
   1.122 +  (Some P1, snd(last ((Some P0, s)#xs)))#ys \<in> cptn_mod; 
   1.123 +  zs=(map (lift P1) xs)@ys \<rbrakk> \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod"
   1.124 +
   1.125 +| CptnModWhile1: 
   1.126 +  "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; s \<in> b; zs=map (lift (While b P)) xs \<rbrakk> 
   1.127 +  \<Longrightarrow> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \<in> cptn_mod"
   1.128 +| CptnModWhile2: 
   1.129 +  "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; fst(last ((Some P, s)#xs))=None; s \<in> b; 
   1.130 +  zs=(map (lift (While b P)) xs)@ys; 
   1.131 +  (Some(While b P), snd(last ((Some P, s)#xs)))#ys \<in> cptn_mod\<rbrakk> 
   1.132 +  \<Longrightarrow> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \<in> cptn_mod"
   1.133 +
   1.134 +subsection {* Equivalence of Both Definitions.*}
   1.135 +
   1.136 +lemma last_length: "((a#xs)!(length xs))=last (a#xs)"
   1.137 +apply simp
   1.138 +apply(induct xs,simp+)
   1.139 +apply(case_tac xs)
   1.140 +apply simp_all
   1.141 +done
   1.142 +
   1.143 +lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow>
   1.144 + (\<forall>s P Q zs. list=(Some (Seq P Q), s)#zs \<longrightarrow>
   1.145 +  (\<exists>xs. (Some P, s)#xs \<in> cptn_mod  \<and> (zs=(map (lift Q) xs) \<or>
   1.146 +  ( fst(((Some P, s)#xs)!length xs)=None \<and> 
   1.147 +  (\<exists>ys. (Some Q, snd(((Some P, s)#xs)!length xs))#ys \<in> cptn_mod  
   1.148 +  \<and> zs=(map (lift (Q)) xs)@ys)))))"
   1.149 +apply(erule cptn_mod.induct)
   1.150 +apply simp_all
   1.151 +    apply clarify
   1.152 +    apply(force intro:CptnModOne)
   1.153 +   apply clarify
   1.154 +   apply(erule_tac x=Pa in allE)
   1.155 +   apply(erule_tac x=Q in allE)
   1.156 +   apply simp
   1.157 +   apply clarify
   1.158 +   apply(erule disjE)
   1.159 +    apply(rule_tac x="(Some Pa,t)#xsa" in exI)
   1.160 +    apply(rule conjI)
   1.161 +     apply clarify
   1.162 +     apply(erule CptnModEnv)
   1.163 +    apply(rule disjI1)
   1.164 +    apply(simp add:lift_def)
   1.165 +   apply clarify
   1.166 +   apply(rule_tac x="(Some Pa,t)#xsa" in exI)
   1.167 +   apply(rule conjI)
   1.168 +    apply(erule CptnModEnv)
   1.169 +   apply(rule disjI2)
   1.170 +   apply(rule conjI)
   1.171 +    apply(case_tac xsa,simp,simp)
   1.172 +   apply(rule_tac x="ys" in exI)
   1.173 +   apply(rule conjI)
   1.174 +    apply simp
   1.175 +   apply(simp add:lift_def)
   1.176 +  apply clarify
   1.177 +  apply(erule ctran.cases,simp_all)
   1.178 + apply clarify
   1.179 + apply(rule_tac x="xs" in exI)
   1.180 + apply simp
   1.181 + apply clarify
   1.182 +apply(rule_tac x="xs" in exI)
   1.183 +apply(simp add: last_length)
   1.184 +done
   1.185 +
   1.186 +lemma cptn_onlyif_cptn_mod_aux [rule_format]:
   1.187 +  "\<forall>s Q t xs.((Some a, s), Q, t) \<in> ctran \<longrightarrow> (Q, t) # xs \<in> cptn_mod 
   1.188 +  \<longrightarrow> (Some a, s) # (Q, t) # xs \<in> cptn_mod"
   1.189 +apply(induct a)
   1.190 +apply simp_all
   1.191 +--{* basic *}
   1.192 +apply clarify
   1.193 +apply(erule ctran.cases,simp_all)
   1.194 +apply(rule CptnModNone,rule Basic,simp)
   1.195 +apply clarify
   1.196 +apply(erule ctran.cases,simp_all)
   1.197 +--{* Seq1 *}
   1.198 +apply(rule_tac xs="[(None,ta)]" in CptnModSeq2)
   1.199 +  apply(erule CptnModNone)
   1.200 +  apply(rule CptnModOne)
   1.201 + apply simp
   1.202 +apply simp
   1.203 +apply(simp add:lift_def)
   1.204 +--{* Seq2 *}
   1.205 +apply(erule_tac x=sa in allE)
   1.206 +apply(erule_tac x="Some P2" in allE)
   1.207 +apply(erule allE,erule impE, assumption)
   1.208 +apply(drule div_seq,simp)
   1.209 +apply force
   1.210 +apply clarify
   1.211 +apply(erule disjE)
   1.212 + apply clarify
   1.213 + apply(erule allE,erule impE, assumption)
   1.214 + apply(erule_tac CptnModSeq1)
   1.215 + apply(simp add:lift_def)
   1.216 +apply clarify 
   1.217 +apply(erule allE,erule impE, assumption)
   1.218 +apply(erule_tac CptnModSeq2)
   1.219 +  apply (simp add:last_length)
   1.220 + apply (simp add:last_length)
   1.221 +apply(simp add:lift_def)
   1.222 +--{* Cond *}
   1.223 +apply clarify
   1.224 +apply(erule ctran.cases,simp_all)
   1.225 +apply(force elim: CptnModCondT)
   1.226 +apply(force elim: CptnModCondF)
   1.227 +--{* While *}
   1.228 +apply  clarify
   1.229 +apply(erule ctran.cases,simp_all)
   1.230 +apply(rule CptnModNone,erule WhileF,simp)
   1.231 +apply(drule div_seq,force)
   1.232 +apply clarify
   1.233 +apply (erule disjE)
   1.234 + apply(force elim:CptnModWhile1)
   1.235 +apply clarify
   1.236 +apply(force simp add:last_length elim:CptnModWhile2)
   1.237 +--{* await *}
   1.238 +apply clarify
   1.239 +apply(erule ctran.cases,simp_all)
   1.240 +apply(rule CptnModNone,erule Await,simp+)
   1.241 +done
   1.242 +
   1.243 +lemma cptn_onlyif_cptn_mod [rule_format]: "c \<in> cptn \<Longrightarrow> c \<in> cptn_mod"
   1.244 +apply(erule cptn.induct)
   1.245 +  apply(rule CptnModOne)
   1.246 + apply(erule CptnModEnv)
   1.247 +apply(case_tac P)
   1.248 + apply simp
   1.249 + apply(erule ctran.cases,simp_all)
   1.250 +apply(force elim:cptn_onlyif_cptn_mod_aux)
   1.251 +done
   1.252 +
   1.253 +lemma lift_is_cptn: "c\<in>cptn \<Longrightarrow> map (lift P) c \<in> cptn"
   1.254 +apply(erule cptn.induct)
   1.255 +  apply(force simp add:lift_def CptnOne)
   1.256 + apply(force intro:CptnEnv simp add:lift_def)
   1.257 +apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.cases)
   1.258 +done
   1.259 +
   1.260 +lemma cptn_append_is_cptn [rule_format]: 
   1.261 + "\<forall>b a. b#c1\<in>cptn \<longrightarrow>  a#c2\<in>cptn \<longrightarrow> (b#c1)!length c1=a \<longrightarrow> b#c1@c2\<in>cptn"
   1.262 +apply(induct c1)
   1.263 + apply simp
   1.264 +apply clarify
   1.265 +apply(erule cptn.cases,simp_all)
   1.266 + apply(force intro:CptnEnv)
   1.267 +apply(force elim:CptnComp)
   1.268 +done
   1.269 +
   1.270 +lemma last_lift: "\<lbrakk>xs\<noteq>[]; fst(xs!(length xs - (Suc 0)))=None\<rbrakk> 
   1.271 + \<Longrightarrow> fst((map (lift P) xs)!(length (map (lift P) xs)- (Suc 0)))=(Some P)"
   1.272 +apply(case_tac "(xs ! (length xs - (Suc 0)))")
   1.273 +apply (simp add:lift_def)
   1.274 +done
   1.275 +
   1.276 +lemma last_fst [rule_format]: "P((a#x)!length x) \<longrightarrow> \<not>P a \<longrightarrow> P (x!(length x - (Suc 0)))" 
   1.277 +apply(induct x,simp+)
   1.278 +done
   1.279 +
   1.280 +lemma last_fst_esp: 
   1.281 + "fst(((Some a,s)#xs)!(length xs))=None \<Longrightarrow> fst(xs!(length xs - (Suc 0)))=None" 
   1.282 +apply(erule last_fst)
   1.283 +apply simp
   1.284 +done
   1.285 +
   1.286 +lemma last_snd: "xs\<noteq>[] \<Longrightarrow> 
   1.287 +  snd(((map (lift P) xs))!(length (map (lift P) xs) - (Suc 0)))=snd(xs!(length xs - (Suc 0)))"
   1.288 +apply(case_tac "(xs ! (length xs - (Suc 0)))",simp)
   1.289 +apply (simp add:lift_def)
   1.290 +done
   1.291 +
   1.292 +lemma Cons_lift: "(Some (Seq P Q), s) # (map (lift Q) xs) = map (lift Q) ((Some P, s) # xs)"
   1.293 +by(simp add:lift_def)
   1.294 +
   1.295 +lemma Cons_lift_append: 
   1.296 +  "(Some (Seq P Q), s) # (map (lift Q) xs) @ ys = map (lift Q) ((Some P, s) # xs)@ ys "
   1.297 +by(simp add:lift_def)
   1.298 +
   1.299 +lemma lift_nth: "i<length xs \<Longrightarrow> map (lift Q) xs ! i = lift Q  (xs! i)"
   1.300 +by (simp add:lift_def)
   1.301 +
   1.302 +lemma snd_lift: "i< length xs \<Longrightarrow> snd(lift Q (xs ! i))= snd (xs ! i)"
   1.303 +apply(case_tac "xs!i")
   1.304 +apply(simp add:lift_def)
   1.305 +done
   1.306 +
   1.307 +lemma cptn_if_cptn_mod: "c \<in> cptn_mod \<Longrightarrow> c \<in> cptn"
   1.308 +apply(erule cptn_mod.induct)
   1.309 +        apply(rule CptnOne)
   1.310 +       apply(erule CptnEnv)
   1.311 +      apply(erule CptnComp,simp)
   1.312 +     apply(rule CptnComp)
   1.313 +     apply(erule CondT,simp)
   1.314 +    apply(rule CptnComp)
   1.315 +    apply(erule CondF,simp)
   1.316 +--{* Seq1 *}   
   1.317 +apply(erule cptn.cases,simp_all)
   1.318 +  apply(rule CptnOne)
   1.319 + apply clarify
   1.320 + apply(drule_tac P=P1 in lift_is_cptn)
   1.321 + apply(simp add:lift_def)
   1.322 + apply(rule CptnEnv,simp)
   1.323 +apply clarify
   1.324 +apply(simp add:lift_def)
   1.325 +apply(rule conjI)
   1.326 + apply clarify
   1.327 + apply(rule CptnComp)
   1.328 +  apply(rule Seq1,simp)
   1.329 + apply(drule_tac P=P1 in lift_is_cptn)
   1.330 + apply(simp add:lift_def)
   1.331 +apply clarify
   1.332 +apply(rule CptnComp)
   1.333 + apply(rule Seq2,simp)
   1.334 +apply(drule_tac P=P1 in lift_is_cptn)
   1.335 +apply(simp add:lift_def)
   1.336 +--{* Seq2 *}
   1.337 +apply(rule cptn_append_is_cptn)
   1.338 +  apply(drule_tac P=P1 in lift_is_cptn)
   1.339 +  apply(simp add:lift_def)
   1.340 + apply simp
   1.341 +apply(case_tac "xs\<noteq>[]")
   1.342 + apply(drule_tac P=P1 in last_lift)
   1.343 +  apply(rule last_fst_esp)
   1.344 +  apply (simp add:last_length)
   1.345 + apply(simp add:Cons_lift del:map.simps)
   1.346 + apply(rule conjI, clarify, simp)
   1.347 + apply(case_tac "(((Some P0, s) # xs) ! length xs)")
   1.348 + apply clarify
   1.349 + apply (simp add:lift_def last_length)
   1.350 +apply (simp add:last_length)
   1.351 +--{* While1 *}
   1.352 +apply(rule CptnComp)
   1.353 +apply(rule WhileT,simp)
   1.354 +apply(drule_tac P="While b P" in lift_is_cptn)
   1.355 +apply(simp add:lift_def)
   1.356 +--{* While2 *}
   1.357 +apply(rule CptnComp)
   1.358 +apply(rule WhileT,simp)
   1.359 +apply(rule cptn_append_is_cptn)
   1.360 +apply(drule_tac P="While b P" in lift_is_cptn)
   1.361 +  apply(simp add:lift_def)
   1.362 + apply simp
   1.363 +apply(case_tac "xs\<noteq>[]")
   1.364 + apply(drule_tac P="While b P" in last_lift)
   1.365 +  apply(rule last_fst_esp,simp add:last_length)
   1.366 + apply(simp add:Cons_lift del:map.simps)
   1.367 + apply(rule conjI, clarify, simp)
   1.368 + apply(case_tac "(((Some P, s) # xs) ! length xs)")
   1.369 + apply clarify
   1.370 + apply (simp add:last_length lift_def)
   1.371 +apply simp
   1.372 +done
   1.373 +
   1.374 +theorem cptn_iff_cptn_mod: "(c \<in> cptn) = (c \<in> cptn_mod)"
   1.375 +apply(rule iffI)
   1.376 + apply(erule cptn_onlyif_cptn_mod)
   1.377 +apply(erule cptn_if_cptn_mod)
   1.378 +done
   1.379 +
   1.380 +section {* Validity  of Correctness Formulas*}
   1.381 +
   1.382 +subsection {* Validity for Component Programs. *}
   1.383 +
   1.384 +types 'a rgformula = "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set"
   1.385 +
   1.386 +constdefs
   1.387 +  assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set"
   1.388 +  "assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
   1.389 +               c!i -e\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}"
   1.390 +
   1.391 +  comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a confs) set"
   1.392 +  "comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow> 
   1.393 +               c!i -c\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
   1.394 +               (fst (last c) = None \<longrightarrow> snd (last c) \<in> post)}"
   1.395 +
   1.396 +  com_validity :: "'a com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool" 
   1.397 +                 ("\<Turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45)
   1.398 +  "\<Turnstile> P sat [pre, rely, guar, post] \<equiv> 
   1.399 +   \<forall>s. cp (Some P) s \<inter> assum(pre, rely) \<subseteq> comm(guar, post)"
   1.400 +
   1.401 +subsection {* Validity for Parallel Programs. *}
   1.402 +
   1.403 +constdefs
   1.404 +  All_None :: "(('a com) option) list \<Rightarrow> bool"
   1.405 +  "All_None xs \<equiv> \<forall>c\<in>set xs. c=None"
   1.406 +
   1.407 +  par_assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a par_confs) set"
   1.408 +  "par_assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> 
   1.409 +             c!i -pe\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}"
   1.410 +
   1.411 +  par_comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a par_confs) set"
   1.412 +  "par_comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow>   
   1.413 +        c!i -pc\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> 
   1.414 +         (All_None (fst (last c)) \<longrightarrow> snd( last c) \<in> post)}"
   1.415 +
   1.416 +  par_com_validity :: "'a  par_com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set 
   1.417 +\<Rightarrow> 'a set \<Rightarrow> bool"  ("\<Turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45)
   1.418 +  "\<Turnstile> Ps SAT [pre, rely, guar, post] \<equiv> 
   1.419 +   \<forall>s. par_cp Ps s \<inter> par_assum(pre, rely) \<subseteq> par_comm(guar, post)"
   1.420 +
   1.421 +subsection {* Compositionality of the Semantics *}
   1.422 +
   1.423 +subsubsection {* Definition of the conjoin operator *}
   1.424 +
   1.425 +constdefs
   1.426 +  same_length :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
   1.427 +  "same_length c clist \<equiv> (\<forall>i<length clist. length(clist!i)=length c)"
   1.428 + 
   1.429 +  same_state :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
   1.430 +  "same_state c clist \<equiv> (\<forall>i <length clist. \<forall>j<length c. snd(c!j) = snd((clist!i)!j))"
   1.431 +
   1.432 +  same_program :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
   1.433 +  "same_program c clist \<equiv> (\<forall>j<length c. fst(c!j) = map (\<lambda>x. fst(nth x j)) clist)"
   1.434 +
   1.435 +  compat_label :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"
   1.436 +  "compat_label c clist \<equiv> (\<forall>j. Suc j<length c \<longrightarrow> 
   1.437 +         (c!j -pc\<rightarrow> c!Suc j \<and> (\<exists>i<length clist. (clist!i)!j -c\<rightarrow> (clist!i)! Suc j \<and> 
   1.438 +                       (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> 
   1.439 +         (c!j -pe\<rightarrow> c!Suc j \<and> (\<forall>i<length clist. (clist!i)!j -e\<rightarrow> (clist!i)! Suc j)))"
   1.440 +
   1.441 +  conjoin :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool"  ("_ \<propto> _" [65,65] 64)
   1.442 +  "c \<propto> clist \<equiv> (same_length c clist) \<and> (same_state c clist) \<and> (same_program c clist) \<and> (compat_label c clist)"
   1.443 +
   1.444 +subsubsection {* Some previous lemmas *}
   1.445 +
   1.446 +lemma list_eq_if [rule_format]: 
   1.447 +  "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)"
   1.448 +apply (induct xs)
   1.449 + apply simp
   1.450 +apply clarify
   1.451 +done
   1.452 +
   1.453 +lemma list_eq: "(length xs = length ys \<and> (\<forall>i<length xs. xs!i=ys!i)) = (xs=ys)"
   1.454 +apply(rule iffI)
   1.455 + apply clarify
   1.456 + apply(erule nth_equalityI)
   1.457 + apply simp+
   1.458 +done
   1.459 +
   1.460 +lemma nth_tl: "\<lbrakk> ys!0=a; ys\<noteq>[] \<rbrakk> \<Longrightarrow> ys=(a#(tl ys))"
   1.461 +apply(case_tac ys)
   1.462 + apply simp+
   1.463 +done
   1.464 +
   1.465 +lemma nth_tl_if [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P ys \<longrightarrow> P (a#(tl ys))"
   1.466 +apply(induct ys)
   1.467 + apply simp+
   1.468 +done
   1.469 +
   1.470 +lemma nth_tl_onlyif [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P (a#(tl ys)) \<longrightarrow> P ys"
   1.471 +apply(induct ys)
   1.472 + apply simp+
   1.473 +done
   1.474 +
   1.475 +lemma seq_not_eq1: "Seq c1 c2\<noteq>c1"
   1.476 +apply(rule com.induct)
   1.477 +apply simp_all
   1.478 +apply clarify
   1.479 +done
   1.480 +
   1.481 +lemma seq_not_eq2: "Seq c1 c2\<noteq>c2"
   1.482 +apply(rule com.induct)
   1.483 +apply simp_all
   1.484 +apply clarify
   1.485 +done
   1.486 +
   1.487 +lemma if_not_eq1: "Cond b c1 c2 \<noteq>c1"
   1.488 +apply(rule com.induct)
   1.489 +apply simp_all
   1.490 +apply clarify
   1.491 +done
   1.492 +
   1.493 +lemma if_not_eq2: "Cond b c1 c2\<noteq>c2"
   1.494 +apply(rule com.induct)
   1.495 +apply simp_all
   1.496 +apply clarify
   1.497 +done
   1.498 +
   1.499 +lemmas seq_and_if_not_eq [simp] = seq_not_eq1 seq_not_eq2 
   1.500 +seq_not_eq1 [THEN not_sym] seq_not_eq2 [THEN not_sym] 
   1.501 +if_not_eq1 if_not_eq2 if_not_eq1 [THEN not_sym] if_not_eq2 [THEN not_sym]
   1.502 +
   1.503 +lemma prog_not_eq_in_ctran_aux:
   1.504 +  assumes c: "(P,s) -c\<rightarrow> (Q,t)"
   1.505 +  shows "P\<noteq>Q" using c
   1.506 +  by (induct x1 \<equiv> "(P,s)" x2 \<equiv> "(Q,t)" arbitrary: P s Q t) auto
   1.507 +
   1.508 +lemma prog_not_eq_in_ctran [simp]: "\<not> (P,s) -c\<rightarrow> (P,t)"
   1.509 +apply clarify
   1.510 +apply(drule prog_not_eq_in_ctran_aux)
   1.511 +apply simp
   1.512 +done
   1.513 +
   1.514 +lemma prog_not_eq_in_par_ctran_aux [rule_format]: "(P,s) -pc\<rightarrow> (Q,t) \<Longrightarrow> (P\<noteq>Q)"
   1.515 +apply(erule par_ctran.induct)
   1.516 +apply(drule prog_not_eq_in_ctran_aux)
   1.517 +apply clarify
   1.518 +apply(drule list_eq_if)
   1.519 + apply simp_all
   1.520 +apply force
   1.521 +done
   1.522 +
   1.523 +lemma prog_not_eq_in_par_ctran [simp]: "\<not> (P,s) -pc\<rightarrow> (P,t)"
   1.524 +apply clarify
   1.525 +apply(drule prog_not_eq_in_par_ctran_aux)
   1.526 +apply simp
   1.527 +done
   1.528 +
   1.529 +lemma tl_in_cptn: "\<lbrakk> a#xs \<in>cptn; xs\<noteq>[] \<rbrakk> \<Longrightarrow> xs\<in>cptn"
   1.530 +apply(force elim:cptn.cases)
   1.531 +done
   1.532 +
   1.533 +lemma tl_zero[rule_format]: 
   1.534 +  "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)"
   1.535 +apply(induct ys)
   1.536 + apply simp_all
   1.537 +done
   1.538 +
   1.539 +subsection {* The Semantics is Compositional *}
   1.540 +
   1.541 +lemma aux_if [rule_format]: 
   1.542 +  "\<forall>xs s clist. (length clist = length xs \<and> (\<forall>i<length xs. (xs!i,s)#clist!i \<in> cptn) 
   1.543 +  \<and> ((xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#snd i) (zip xs clist)) 
   1.544 +   \<longrightarrow> (xs, s)#ys \<in> par_cptn)"
   1.545 +apply(induct ys)
   1.546 + apply(clarify)
   1.547 + apply(rule ParCptnOne)
   1.548 +apply(clarify)
   1.549 +apply(simp add:conjoin_def compat_label_def)
   1.550 +apply clarify
   1.551 +apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in all_dupE,simp)
   1.552 +apply(erule disjE)
   1.553 +--{* first step is a Component step *}
   1.554 + apply clarify 
   1.555 + apply simp
   1.556 + apply(subgoal_tac "a=(xs[i:=(fst(clist!i!0))])")
   1.557 +  apply(subgoal_tac "b=snd(clist!i!0)",simp)
   1.558 +   prefer 2
   1.559 +   apply(simp add: same_state_def)
   1.560 +   apply(erule_tac x=i in allE,erule impE,assumption, 
   1.561 +         erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.562 +  prefer 2
   1.563 +  apply(simp add:same_program_def)
   1.564 +  apply(erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
   1.565 +  apply(rule nth_equalityI,simp)
   1.566 +  apply clarify
   1.567 +  apply(case_tac "i=ia",simp,simp)
   1.568 +  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.569 +  apply(drule_tac t=i in not_sym,simp)
   1.570 +  apply(erule etranE,simp)
   1.571 + apply(rule ParCptnComp)
   1.572 +  apply(erule ParComp,simp)
   1.573 +--{* applying the induction hypothesis *}
   1.574 + apply(erule_tac x="xs[i := fst (clist ! i ! 0)]" in allE)
   1.575 + apply(erule_tac x="snd (clist ! i ! 0)" in allE)
   1.576 + apply(erule mp)
   1.577 + apply(rule_tac x="map tl clist" in exI,simp)
   1.578 + apply(rule conjI,clarify)
   1.579 +  apply(case_tac "i=ia",simp)
   1.580 +   apply(rule nth_tl_if)
   1.581 +     apply(force simp add:same_length_def length_Suc_conv)
   1.582 +    apply simp
   1.583 +   apply(erule allE,erule impE,assumption,erule tl_in_cptn)
   1.584 +   apply(force simp add:same_length_def length_Suc_conv)
   1.585 +  apply(rule nth_tl_if)
   1.586 +    apply(force simp add:same_length_def length_Suc_conv)
   1.587 +   apply(simp add:same_state_def)
   1.588 +   apply(erule_tac x=ia in allE, erule impE, assumption, 
   1.589 +     erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.590 +   apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.591 +   apply(drule_tac t=i  in not_sym,simp)
   1.592 +   apply(erule etranE,simp)
   1.593 +  apply(erule allE,erule impE,assumption,erule tl_in_cptn)
   1.594 +  apply(force simp add:same_length_def length_Suc_conv)
   1.595 + apply(simp add:same_length_def same_state_def)
   1.596 + apply(rule conjI)
   1.597 +  apply clarify
   1.598 +  apply(case_tac j,simp,simp)
   1.599 +  apply(erule_tac x=ia in allE, erule impE, assumption,
   1.600 +        erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.601 +  apply(force simp add:same_length_def length_Suc_conv)
   1.602 + apply(rule conjI)
   1.603 +  apply(simp add:same_program_def)
   1.604 +  apply clarify
   1.605 +  apply(case_tac j,simp)
   1.606 +   apply(rule nth_equalityI,simp)
   1.607 +   apply clarify
   1.608 +   apply(case_tac "i=ia",simp,simp)
   1.609 +  apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
   1.610 +  apply(rule nth_equalityI,simp,simp)
   1.611 +  apply(force simp add:length_Suc_conv)
   1.612 + apply(rule allI,rule impI)
   1.613 + apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp)
   1.614 + apply(erule disjE) 
   1.615 +  apply clarify
   1.616 +  apply(rule_tac x=ia in exI,simp)
   1.617 +  apply(case_tac "i=ia",simp)
   1.618 +   apply(rule conjI)
   1.619 +    apply(force simp add: length_Suc_conv)
   1.620 +   apply clarify
   1.621 +   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption)
   1.622 +   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption)
   1.623 +   apply simp
   1.624 +   apply(case_tac j,simp)
   1.625 +    apply(rule tl_zero)
   1.626 +      apply(erule_tac x=l in allE, erule impE, assumption, 
   1.627 +            erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.628 +      apply(force elim:etranE intro:Env)
   1.629 +     apply force
   1.630 +    apply force
   1.631 +   apply simp
   1.632 +   apply(rule tl_zero)
   1.633 +     apply(erule tl_zero)
   1.634 +      apply force
   1.635 +     apply force
   1.636 +    apply force
   1.637 +   apply force
   1.638 +  apply(rule conjI,simp)
   1.639 +   apply(rule nth_tl_if)
   1.640 +     apply force
   1.641 +    apply(erule_tac x=ia  in allE, erule impE, assumption,
   1.642 +          erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.643 +    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.644 +    apply(drule_tac t=i  in not_sym,simp)
   1.645 +    apply(erule etranE,simp)
   1.646 +   apply(erule tl_zero)
   1.647 +    apply force
   1.648 +   apply force
   1.649 +  apply clarify
   1.650 +  apply(case_tac "i=l",simp)
   1.651 +   apply(rule nth_tl_if)
   1.652 +     apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.653 +    apply simp
   1.654 +   apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption,erule impE,assumption)
   1.655 +   apply(erule tl_zero,force)
   1.656 +   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.657 +   apply(rule nth_tl_if)
   1.658 +     apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.659 +    apply(erule_tac x=l  in allE, erule impE, assumption,
   1.660 +          erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.661 +    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
   1.662 +    apply(erule etranE,simp)
   1.663 +   apply(rule tl_zero)
   1.664 +    apply force
   1.665 +   apply force
   1.666 +  apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.667 + apply(rule disjI2)
   1.668 + apply(case_tac j,simp)
   1.669 +  apply clarify
   1.670 +  apply(rule tl_zero)
   1.671 +    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j\<in>etran" in allE,erule impE, assumption)
   1.672 +    apply(case_tac "i=ia",simp,simp)
   1.673 +    apply(erule_tac x=ia  in allE, erule impE, assumption,
   1.674 +    erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.675 +    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
   1.676 +    apply(force elim:etranE intro:Env)
   1.677 +   apply force
   1.678 +  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.679 + apply simp
   1.680 + apply clarify
   1.681 + apply(rule tl_zero)
   1.682 +   apply(rule tl_zero,force)
   1.683 +    apply force
   1.684 +   apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.685 +  apply force
   1.686 + apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.687 +--{* first step is an environmental step *}
   1.688 +apply clarify
   1.689 +apply(erule par_etran.cases)
   1.690 +apply simp
   1.691 +apply(rule ParCptnEnv)
   1.692 +apply(erule_tac x="Ps" in allE)
   1.693 +apply(erule_tac x="t" in allE)
   1.694 +apply(erule mp)
   1.695 +apply(rule_tac x="map tl clist" in exI,simp)
   1.696 +apply(rule conjI)
   1.697 + apply clarify
   1.698 + apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I ?s j) \<in> cptn" in allE,simp)
   1.699 + apply(erule cptn.cases)
   1.700 +   apply(simp add:same_length_def)
   1.701 +   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.702 +  apply(simp add:same_state_def)
   1.703 +  apply(erule_tac x=i  in allE, erule impE, assumption,
   1.704 +   erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.705 + apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<in>etran" in allE,simp)
   1.706 + apply(erule etranE,simp)
   1.707 +apply(simp add:same_state_def same_length_def)
   1.708 +apply(rule conjI,clarify)
   1.709 + apply(case_tac j,simp,simp)
   1.710 + apply(erule_tac x=i  in allE, erule impE, assumption,
   1.711 +       erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.712 + apply(rule tl_zero)
   1.713 +   apply(simp)
   1.714 +  apply force
   1.715 + apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.716 +apply(rule conjI)
   1.717 + apply(simp add:same_program_def)
   1.718 + apply clarify
   1.719 + apply(case_tac j,simp)
   1.720 +  apply(rule nth_equalityI,simp)
   1.721 +  apply clarify
   1.722 +  apply simp
   1.723 + apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp)
   1.724 + apply(rule nth_equalityI,simp,simp)
   1.725 + apply(force simp add:length_Suc_conv)
   1.726 +apply(rule allI,rule impI)
   1.727 +apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp)
   1.728 +apply(erule disjE) 
   1.729 + apply clarify
   1.730 + apply(rule_tac x=i in exI,simp)
   1.731 + apply(rule conjI)
   1.732 +  apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.733 +  apply(erule etranE,simp)
   1.734 +  apply(erule_tac x=i  in allE, erule impE, assumption,
   1.735 +        erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.736 +  apply(rule nth_tl_if)
   1.737 +   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.738 +  apply simp
   1.739 + apply(erule tl_zero,force) 
   1.740 +  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.741 + apply clarify
   1.742 + apply(erule_tac x=l and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.743 + apply(erule etranE,simp)
   1.744 + apply(erule_tac x=l  in allE, erule impE, assumption,
   1.745 +       erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.746 + apply(rule nth_tl_if)
   1.747 +   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.748 +  apply simp
   1.749 +  apply(rule tl_zero,force)
   1.750 +  apply force
   1.751 + apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.752 +apply(rule disjI2)
   1.753 +apply simp
   1.754 +apply clarify
   1.755 +apply(case_tac j,simp)
   1.756 + apply(rule tl_zero)
   1.757 +   apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.758 +   apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.759 +   apply(force elim:etranE intro:Env)
   1.760 +  apply force
   1.761 + apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.762 +apply simp
   1.763 +apply(rule tl_zero)
   1.764 +  apply(rule tl_zero,force)
   1.765 +   apply force
   1.766 +  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.767 + apply force
   1.768 +apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.769 +done
   1.770 +
   1.771 +lemma less_Suc_0 [iff]: "(n < Suc 0) = (n = 0)"
   1.772 +by auto
   1.773 +
   1.774 +lemma aux_onlyif [rule_format]: "\<forall>xs s. (xs, s)#ys \<in> par_cptn \<longrightarrow> 
   1.775 +  (\<exists>clist. (length clist = length xs) \<and> 
   1.776 +  (xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist) \<and> 
   1.777 +  (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))"
   1.778 +apply(induct ys)
   1.779 + apply(clarify)
   1.780 + apply(rule_tac x="map (\<lambda>i. []) [0..<length xs]" in exI)
   1.781 + apply(simp add: conjoin_def same_length_def same_state_def same_program_def compat_label_def)
   1.782 + apply(rule conjI)
   1.783 +  apply(rule nth_equalityI,simp,simp)
   1.784 + apply(force intro: cptn.intros)
   1.785 +apply(clarify)
   1.786 +apply(erule par_cptn.cases,simp)
   1.787 + apply simp
   1.788 + apply(erule_tac x="xs" in allE)
   1.789 + apply(erule_tac x="t" in allE,simp)
   1.790 + apply clarify
   1.791 + apply(rule_tac x="(map (\<lambda>j. (P!j, t)#(clist!j)) [0..<length P])" in exI,simp)
   1.792 + apply(rule conjI)
   1.793 +  prefer 2
   1.794 +  apply clarify
   1.795 +  apply(rule CptnEnv,simp)
   1.796 + apply(simp add:conjoin_def same_length_def same_state_def)
   1.797 + apply (rule conjI)
   1.798 +  apply clarify
   1.799 +  apply(case_tac j,simp,simp)
   1.800 + apply(rule conjI)
   1.801 +  apply(simp add:same_program_def)
   1.802 +  apply clarify
   1.803 +  apply(case_tac j,simp)
   1.804 +   apply(rule nth_equalityI,simp,simp)
   1.805 +  apply simp
   1.806 +  apply(rule nth_equalityI,simp,simp)
   1.807 + apply(simp add:compat_label_def)
   1.808 + apply clarify
   1.809 + apply(case_tac j,simp)
   1.810 +  apply(simp add:ParEnv)
   1.811 +  apply clarify
   1.812 +  apply(simp add:Env)
   1.813 + apply simp
   1.814 + apply(erule_tac x=nat in allE,erule impE, assumption)
   1.815 + apply(erule disjE,simp)
   1.816 +  apply clarify
   1.817 +  apply(rule_tac x=i in exI,simp)
   1.818 + apply force
   1.819 +apply(erule par_ctran.cases,simp)
   1.820 +apply(erule_tac x="Ps[i:=r]" in allE)
   1.821 +apply(erule_tac x="ta" in allE,simp)
   1.822 +apply clarify
   1.823 +apply(rule_tac x="(map (\<lambda>j. (Ps!j, ta)#(clist!j)) [0..<length Ps]) [i:=((r, ta)#(clist!i))]" in exI,simp)
   1.824 +apply(rule conjI)
   1.825 + prefer 2
   1.826 + apply clarify
   1.827 + apply(case_tac "i=ia",simp)
   1.828 +  apply(erule CptnComp)
   1.829 +  apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<in> cptn)" in allE,simp)
   1.830 + apply simp
   1.831 + apply(erule_tac x=ia in allE)
   1.832 + apply(rule CptnEnv,simp)
   1.833 +apply(simp add:conjoin_def)
   1.834 +apply (rule conjI)
   1.835 + apply(simp add:same_length_def)
   1.836 + apply clarify
   1.837 + apply(case_tac "i=ia",simp,simp)
   1.838 +apply(rule conjI)
   1.839 + apply(simp add:same_state_def)
   1.840 + apply clarify
   1.841 + apply(case_tac j, simp, simp (no_asm_simp))
   1.842 + apply(case_tac "i=ia",simp,simp)
   1.843 +apply(rule conjI)
   1.844 + apply(simp add:same_program_def)
   1.845 + apply clarify
   1.846 + apply(case_tac j,simp)
   1.847 +  apply(rule nth_equalityI,simp,simp)
   1.848 + apply simp
   1.849 + apply(rule nth_equalityI,simp,simp)
   1.850 + apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (fst (?a j))=((?b j))" in allE)
   1.851 + apply(case_tac nat)
   1.852 +  apply clarify
   1.853 +  apply(case_tac "i=ia",simp,simp)
   1.854 + apply clarify
   1.855 + apply(case_tac "i=ia",simp,simp)
   1.856 +apply(simp add:compat_label_def)
   1.857 +apply clarify
   1.858 +apply(case_tac j)
   1.859 + apply(rule conjI,simp)
   1.860 +  apply(erule ParComp,assumption)
   1.861 +  apply clarify
   1.862 +  apply(rule_tac x=i in exI,simp)
   1.863 + apply clarify
   1.864 + apply(rule Env)
   1.865 +apply simp
   1.866 +apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in allE,simp)
   1.867 +apply(erule disjE)
   1.868 + apply clarify
   1.869 + apply(rule_tac x=ia in exI,simp)
   1.870 + apply(rule conjI)
   1.871 +  apply(case_tac "i=ia",simp,simp)
   1.872 + apply clarify
   1.873 + apply(case_tac "i=l",simp)
   1.874 +  apply(case_tac "l=ia",simp,simp)
   1.875 +  apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
   1.876 + apply simp
   1.877 + apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp)
   1.878 +apply clarify
   1.879 +apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption)
   1.880 +apply(case_tac "i=ia",simp,simp)
   1.881 +done
   1.882 +
   1.883 +lemma one_iff_aux: "xs\<noteq>[] \<Longrightarrow> (\<forall>ys. ((xs, s)#ys \<in> par_cptn) = 
   1.884 + (\<exists>clist. length clist= length xs \<and> 
   1.885 + ((xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist)) \<and> 
   1.886 + (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))) = 
   1.887 + (par_cp (xs) s = {c. \<exists>clist. (length clist)=(length xs) \<and>
   1.888 + (\<forall>i<length clist. (clist!i) \<in> cp(xs!i) s) \<and> c \<propto> clist})" 
   1.889 +apply (rule iffI)
   1.890 + apply(rule subset_antisym)
   1.891 +  apply(rule subsetI) 
   1.892 +  apply(clarify)
   1.893 +  apply(simp add:par_cp_def cp_def)
   1.894 +  apply(case_tac x)
   1.895 +   apply(force elim:par_cptn.cases)
   1.896 +  apply simp
   1.897 +  apply(erule_tac x="list" in allE)
   1.898 +  apply clarify
   1.899 +  apply simp
   1.900 +  apply(rule_tac x="map (\<lambda>i. (fst i, s) # snd i) (zip xs clist)" in exI,simp)
   1.901 + apply(rule subsetI) 
   1.902 + apply(clarify)
   1.903 + apply(case_tac x)
   1.904 +  apply(erule_tac x=0 in allE)
   1.905 +  apply(simp add:cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def)
   1.906 +  apply clarify
   1.907 +  apply(erule cptn.cases,force,force,force)
   1.908 + apply(simp add:par_cp_def conjoin_def  same_length_def same_program_def same_state_def compat_label_def)
   1.909 + apply clarify
   1.910 + apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in all_dupE)
   1.911 + apply(subgoal_tac "a = xs")
   1.912 +  apply(subgoal_tac "b = s",simp)
   1.913 +   prefer 3
   1.914 +   apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=((?t j))" in allE)
   1.915 +   apply (simp add:cp_def)
   1.916 +   apply(rule nth_equalityI,simp,simp)
   1.917 +  prefer 2
   1.918 +  apply(erule_tac x=0 in allE)
   1.919 +  apply (simp add:cp_def)
   1.920 +  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)
   1.921 +  apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.922 + apply(erule_tac x=list in allE)
   1.923 + apply(rule_tac x="map tl clist" in exI,simp) 
   1.924 + apply(rule conjI)
   1.925 +  apply clarify
   1.926 +  apply(case_tac j,simp)
   1.927 +   apply(erule_tac x=i  in allE, erule impE, assumption,
   1.928 +        erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.929 +  apply(erule_tac x=i  in allE, erule impE, assumption,
   1.930 +        erule_tac x="Suc nat" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.931 +  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.932 +  apply(case_tac "clist!i",simp,simp)
   1.933 + apply(rule conjI)
   1.934 +  apply clarify
   1.935 +  apply(rule nth_equalityI,simp,simp)
   1.936 +  apply(case_tac j)
   1.937 +   apply clarify
   1.938 +   apply(erule_tac x=i in allE)
   1.939 +   apply(simp add:cp_def)
   1.940 +  apply clarify
   1.941 +  apply simp
   1.942 +  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.943 +  apply(case_tac "clist!i",simp,simp)
   1.944 + apply(thin_tac "?H = (\<exists>i. ?J i)")
   1.945 + apply(rule conjI)
   1.946 +  apply clarify
   1.947 +  apply(erule_tac x=j in allE,erule impE, assumption,erule disjE)
   1.948 +   apply clarify
   1.949 +   apply(rule_tac x=i in exI,simp)
   1.950 +   apply(case_tac j,simp)
   1.951 +    apply(rule conjI)
   1.952 +     apply(erule_tac x=i in allE)
   1.953 +     apply(simp add:cp_def)
   1.954 +     apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.955 +     apply(case_tac "clist!i",simp,simp)
   1.956 +    apply clarify
   1.957 +    apply(erule_tac x=l in allE)
   1.958 +    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.959 +    apply clarify
   1.960 +    apply(simp add:cp_def)
   1.961 +    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.962 +    apply(case_tac "clist!l",simp,simp)
   1.963 +   apply simp
   1.964 +   apply(rule conjI)
   1.965 +    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.966 +    apply(case_tac "clist!i",simp,simp)
   1.967 +   apply clarify
   1.968 +   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.969 +   apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.970 +   apply(case_tac "clist!l",simp,simp)
   1.971 +  apply clarify
   1.972 +  apply(erule_tac x=i in allE)
   1.973 +  apply(simp add:cp_def)
   1.974 +  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.975 +  apply(case_tac "clist!i",simp)
   1.976 +  apply(rule nth_tl_if,simp,simp)
   1.977 +  apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption,simp)
   1.978 +  apply(simp add:cp_def)
   1.979 +  apply clarify
   1.980 +  apply(rule nth_tl_if)
   1.981 +   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
   1.982 +   apply(case_tac "clist!i",simp,simp)
   1.983 +  apply force
   1.984 + apply force
   1.985 +apply clarify
   1.986 +apply(rule iffI)
   1.987 + apply(simp add:par_cp_def)
   1.988 + apply(erule_tac c="(xs, s) # ys" in equalityCE)
   1.989 +  apply simp
   1.990 +  apply clarify
   1.991 +  apply(rule_tac x="map tl clist" in exI)
   1.992 +  apply simp
   1.993 +  apply (rule conjI)
   1.994 +   apply(simp add:conjoin_def cp_def)
   1.995 +   apply(rule conjI)
   1.996 +    apply clarify
   1.997 +    apply(unfold same_length_def)
   1.998 +    apply clarify
   1.999 +    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,simp)
  1.1000 +   apply(rule conjI)
  1.1001 +    apply(simp add:same_state_def)
  1.1002 +    apply clarify
  1.1003 +    apply(erule_tac x=i in allE, erule impE, assumption,
  1.1004 +       erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
  1.1005 +    apply(case_tac j,simp)
  1.1006 +    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  1.1007 +    apply(case_tac "clist!i",simp,simp)
  1.1008 +   apply(rule conjI)
  1.1009 +    apply(simp add:same_program_def)
  1.1010 +    apply clarify
  1.1011 +    apply(rule nth_equalityI,simp,simp)
  1.1012 +    apply(case_tac j,simp)
  1.1013 +    apply clarify
  1.1014 +    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  1.1015 +    apply(case_tac "clist!i",simp,simp)
  1.1016 +   apply clarify
  1.1017 +   apply(simp add:compat_label_def)
  1.1018 +   apply(rule allI,rule impI)
  1.1019 +   apply(erule_tac x=j in allE,erule impE, assumption)
  1.1020 +   apply(erule disjE)
  1.1021 +    apply clarify
  1.1022 +    apply(rule_tac x=i in exI,simp)
  1.1023 +    apply(rule conjI)
  1.1024 +     apply(erule_tac x=i in allE)
  1.1025 +     apply(case_tac j,simp)
  1.1026 +      apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  1.1027 +      apply(case_tac "clist!i",simp,simp)
  1.1028 +     apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  1.1029 +     apply(case_tac "clist!i",simp,simp)
  1.1030 +    apply clarify
  1.1031 +    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
  1.1032 +    apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE)
  1.1033 +    apply(case_tac "clist!l",simp,simp)
  1.1034 +    apply(erule_tac x=l in allE,simp)
  1.1035 +   apply(rule disjI2)
  1.1036 +   apply clarify
  1.1037 +   apply(rule tl_zero)
  1.1038 +     apply(case_tac j,simp,simp)
  1.1039 +     apply(rule tl_zero,force)   
  1.1040 +      apply force
  1.1041 +     apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  1.1042 +    apply force
  1.1043 +   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
  1.1044 +  apply clarify
  1.1045 +  apply(erule_tac x=i in allE)
  1.1046 +  apply(simp add:cp_def)
  1.1047 +  apply(rule nth_tl_if)
  1.1048 +    apply(simp add:conjoin_def)
  1.1049 +    apply clarify
  1.1050 +    apply(simp add:same_length_def)
  1.1051 +    apply(erule_tac x=i in allE,simp)
  1.1052 +   apply simp
  1.1053 +  apply simp
  1.1054 + apply simp
  1.1055 +apply clarify
  1.1056 +apply(erule_tac c="(xs, s) # ys" in equalityCE)
  1.1057 + apply(simp add:par_cp_def)
  1.1058 +apply simp
  1.1059 +apply(erule_tac x="map (\<lambda>i. (fst i, s) # snd i) (zip xs clist)" in allE)
  1.1060 +apply simp
  1.1061 +apply clarify
  1.1062 +apply(simp add:cp_def)
  1.1063 +done
  1.1064 +
  1.1065 +theorem one: "xs\<noteq>[] \<Longrightarrow> 
  1.1066 + par_cp xs s = {c. \<exists>clist. (length clist)=(length xs) \<and> 
  1.1067 +               (\<forall>i<length clist. (clist!i) \<in> cp(xs!i) s) \<and> c \<propto> clist}"
  1.1068 +apply(frule one_iff_aux)
  1.1069 +apply(drule sym)
  1.1070 +apply(erule iffD2)
  1.1071 +apply clarify
  1.1072 +apply(rule iffI)
  1.1073 + apply(erule aux_onlyif)
  1.1074 +apply clarify
  1.1075 +apply(force intro:aux_if)
  1.1076 +done
  1.1077 +
  1.1078 +end