src/HOL/HoareParallel/RG_Tran.thy
changeset 23746 a455e69c31cc
parent 15425 6356d2523f73
     1.1 --- a/src/HOL/HoareParallel/RG_Tran.thy	Wed Jul 11 11:13:08 2007 +0200
     1.2 +++ b/src/HOL/HoareParallel/RG_Tran.thy	Wed Jul 11 11:14:51 2007 +0200
     1.3 @@ -10,73 +10,76 @@
     1.4  
     1.5  types 'a conf = "(('a com) option) \<times> 'a"
     1.6  
     1.7 -consts etran    :: "('a conf \<times> 'a conf) set" 
     1.8 -syntax  "_etran"  :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"  ("_ -e\<rightarrow> _" [81,81] 80)
     1.9 -translations  "P -e\<rightarrow> Q"  \<rightleftharpoons> "(P,Q) \<in> etran"
    1.10 -inductive etran
    1.11 -intros
    1.12 -  Env: "(P, s) -e\<rightarrow> (P, t)"
    1.13 +inductive_set
    1.14 +  etran :: "('a conf \<times> 'a conf) set" 
    1.15 +  and etran' :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"  ("_ -e\<rightarrow> _" [81,81] 80)
    1.16 +where
    1.17 +  "P -e\<rightarrow> Q \<equiv> (P,Q) \<in> etran"
    1.18 +| Env: "(P, s) -e\<rightarrow> (P, t)"
    1.19 +
    1.20 +lemma etranE: "c -e\<rightarrow> c' \<Longrightarrow> (\<And>P s t. c = (P, s) \<Longrightarrow> c' = (P, t) \<Longrightarrow> Q) \<Longrightarrow> Q"
    1.21 +  by (induct c, induct c', erule etran.cases, blast)
    1.22  
    1.23  subsubsection {* Component transitions *}
    1.24  
    1.25 -consts ctran    :: "('a conf \<times> 'a conf) set"
    1.26 -syntax
    1.27 -  "_ctran"  :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c\<rightarrow> _" [81,81] 80)
    1.28 -  "_ctran_*":: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c*\<rightarrow> _" [81,81] 80)
    1.29 -translations
    1.30 -  "P -c\<rightarrow> Q"  \<rightleftharpoons> "(P,Q) \<in> ctran"
    1.31 -  "P -c*\<rightarrow> Q" \<rightleftharpoons> "(P,Q) \<in> ctran^*"
    1.32 +inductive_set
    1.33 +  ctran :: "('a conf \<times> 'a conf) set"
    1.34 +  and ctran' :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c\<rightarrow> _" [81,81] 80)
    1.35 +  and ctrans :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool"   ("_ -c*\<rightarrow> _" [81,81] 80)
    1.36 +where
    1.37 +  "P -c\<rightarrow> Q \<equiv> (P,Q) \<in> ctran"
    1.38 +| "P -c*\<rightarrow> Q \<equiv> (P,Q) \<in> ctran^*"
    1.39  
    1.40 -inductive  ctran 
    1.41 -intros
    1.42 -  Basic:  "(Some(Basic f), s) -c\<rightarrow> (None, f s)"
    1.43 +| Basic:  "(Some(Basic f), s) -c\<rightarrow> (None, f s)"
    1.44  
    1.45 -  Seq1:   "(Some P0, s) -c\<rightarrow> (None, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some P1, t)"
    1.46 +| Seq1:   "(Some P0, s) -c\<rightarrow> (None, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some P1, t)"
    1.47  
    1.48 -  Seq2:   "(Some P0, s) -c\<rightarrow> (Some P2, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some(Seq P2 P1), t)"
    1.49 +| Seq2:   "(Some P0, s) -c\<rightarrow> (Some P2, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some(Seq P2 P1), t)"
    1.50  
    1.51 -  CondT: "s\<in>b  \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P1, s)"
    1.52 -  CondF: "s\<notin>b \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P2, s)"
    1.53 +| CondT: "s\<in>b  \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P1, s)"
    1.54 +| CondF: "s\<notin>b \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P2, s)"
    1.55  
    1.56 -  WhileF: "s\<notin>b \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (None, s)"
    1.57 -  WhileT: "s\<in>b  \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (Some(Seq P (While b P)), s)"
    1.58 +| WhileF: "s\<notin>b \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (None, s)"
    1.59 +| WhileT: "s\<in>b  \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (Some(Seq P (While b P)), s)"
    1.60  
    1.61 -  Await:  "\<lbrakk>s\<in>b; (Some P, s) -c*\<rightarrow> (None, t)\<rbrakk> \<Longrightarrow> (Some(Await b P), s) -c\<rightarrow> (None, t)" 
    1.62 +| Await:  "\<lbrakk>s\<in>b; (Some P, s) -c*\<rightarrow> (None, t)\<rbrakk> \<Longrightarrow> (Some(Await b P), s) -c\<rightarrow> (None, t)" 
    1.63  
    1.64  monos "rtrancl_mono"
    1.65  
    1.66  subsection {* Semantics of Parallel Programs *}
    1.67  
    1.68  types 'a par_conf = "('a par_com) \<times> 'a"
    1.69 -consts
    1.70 +
    1.71 +inductive_set
    1.72    par_etran :: "('a par_conf \<times> 'a par_conf) set"
    1.73 +  and par_etran' :: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pe\<rightarrow> _" [81,81] 80)
    1.74 +where
    1.75 +  "P -pe\<rightarrow> Q \<equiv> (P,Q) \<in> par_etran"
    1.76 +| ParEnv:  "(Ps, s) -pe\<rightarrow> (Ps, t)"
    1.77 +
    1.78 +inductive_set
    1.79    par_ctran :: "('a par_conf \<times> 'a par_conf) set"
    1.80 -syntax
    1.81 -  "_par_etran":: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pe\<rightarrow> _" [81,81] 80)
    1.82 -  "_par_ctran":: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pc\<rightarrow> _" [81,81] 80)
    1.83 -translations
    1.84 -  "P -pe\<rightarrow> Q"  \<rightleftharpoons> "(P,Q) \<in> par_etran"
    1.85 -  "P -pc\<rightarrow> Q"  \<rightleftharpoons> "(P,Q) \<in> par_ctran"
    1.86 +  and par_ctran' :: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pc\<rightarrow> _" [81,81] 80)
    1.87 +where
    1.88 +  "P -pc\<rightarrow> Q \<equiv> (P,Q) \<in> par_ctran"
    1.89 +| ParComp: "\<lbrakk>i<length Ps; (Ps!i, s) -c\<rightarrow> (r, t)\<rbrakk> \<Longrightarrow> (Ps, s) -pc\<rightarrow> (Ps[i:=r], t)"
    1.90  
    1.91 -inductive  par_etran
    1.92 -intros
    1.93 -  ParEnv:  "(Ps, s) -pe\<rightarrow> (Ps, t)"
    1.94 -
    1.95 -inductive  par_ctran
    1.96 -intros
    1.97 -  ParComp: "\<lbrakk>i<length Ps; (Ps!i, s) -c\<rightarrow> (r, t)\<rbrakk> \<Longrightarrow> (Ps, s) -pc\<rightarrow> (Ps[i:=r], t)"
    1.98 +lemma par_ctranE: "c -pc\<rightarrow> c' \<Longrightarrow>
    1.99 +  (\<And>i Ps s r t. c = (Ps, s) \<Longrightarrow> c' = (Ps[i := r], t) \<Longrightarrow> i < length Ps \<Longrightarrow>
   1.100 +     (Ps ! i, s) -c\<rightarrow> (r, t) \<Longrightarrow> P) \<Longrightarrow> P"
   1.101 +  by (induct c, induct c', erule par_ctran.cases, blast)
   1.102  
   1.103  subsection {* Computations *}
   1.104  
   1.105  subsubsection {* Sequential computations *}
   1.106  
   1.107  types 'a confs = "('a conf) list"
   1.108 -consts cptn :: "('a confs) set"
   1.109 -inductive  "cptn"
   1.110 -intros
   1.111 +
   1.112 +inductive_set cptn :: "('a confs) set"
   1.113 +where
   1.114    CptnOne: "[(P,s)] \<in> cptn"
   1.115 -  CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
   1.116 -  CptnComp: "\<lbrakk>(P,s) -c\<rightarrow> (Q,t); (Q, t)#xs \<in> cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> cptn"
   1.117 +| CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn"
   1.118 +| CptnComp: "\<lbrakk>(P,s) -c\<rightarrow> (Q,t); (Q, t)#xs \<in> cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> cptn"
   1.119  
   1.120  constdefs
   1.121    cp :: "('a com) option \<Rightarrow> 'a \<Rightarrow> ('a confs) set"
   1.122 @@ -85,12 +88,12 @@
   1.123  subsubsection {* Parallel computations *}
   1.124  
   1.125  types  'a par_confs = "('a par_conf) list"
   1.126 -consts par_cptn :: "('a par_confs) set"
   1.127 -inductive  "par_cptn"
   1.128 -intros
   1.129 +
   1.130 +inductive_set par_cptn :: "('a par_confs) set"
   1.131 +where
   1.132    ParCptnOne: "[(P,s)] \<in> par_cptn"
   1.133 -  ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
   1.134 -  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.135 +| ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn"
   1.136 +| 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.137  
   1.138  constdefs
   1.139    par_cp :: "'a par_com \<Rightarrow> 'a \<Rightarrow> ('a par_confs) set"
   1.140 @@ -102,25 +105,24 @@
   1.141    lift :: "'a com \<Rightarrow> 'a conf \<Rightarrow> 'a conf"
   1.142    "lift Q \<equiv> \<lambda>(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))"
   1.143  
   1.144 -consts  cptn_mod :: "('a confs) set"
   1.145 -inductive  "cptn_mod"
   1.146 -intros
   1.147 +inductive_set cptn_mod :: "('a confs) set"
   1.148 +where
   1.149    CptnModOne: "[(P, s)] \<in> cptn_mod"
   1.150 -  CptnModEnv: "(P, t)#xs \<in> cptn_mod \<Longrightarrow> (P, s)#(P, t)#xs \<in> cptn_mod"
   1.151 -  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.152 -  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.153 -  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.154 -  CptnModSeq1: "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; zs=map (lift P1) xs \<rbrakk>
   1.155 +| CptnModEnv: "(P, t)#xs \<in> cptn_mod \<Longrightarrow> (P, s)#(P, t)#xs \<in> cptn_mod"
   1.156 +| 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.157 +| 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.158 +| 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.159 +| CptnModSeq1: "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; zs=map (lift P1) xs \<rbrakk>
   1.160                   \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod"
   1.161 -  CptnModSeq2: 
   1.162 +| CptnModSeq2: 
   1.163    "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; fst(last ((Some P0, s)#xs)) = None; 
   1.164    (Some P1, snd(last ((Some P0, s)#xs)))#ys \<in> cptn_mod; 
   1.165    zs=(map (lift P1) xs)@ys \<rbrakk> \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod"
   1.166  
   1.167 -  CptnModWhile1: 
   1.168 +| CptnModWhile1: 
   1.169    "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; s \<in> b; zs=map (lift (While b P)) xs \<rbrakk> 
   1.170    \<Longrightarrow> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \<in> cptn_mod"
   1.171 -  CptnModWhile2: 
   1.172 +| CptnModWhile2: 
   1.173    "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; fst(last ((Some P, s)#xs))=None; s \<in> b; 
   1.174    zs=(map (lift (While b P)) xs)@ys; 
   1.175    (Some(While b P), snd(last ((Some P, s)#xs)))#ys \<in> cptn_mod\<rbrakk> 
   1.176 @@ -169,7 +171,7 @@
   1.177      apply simp
   1.178     apply(simp add:lift_def)
   1.179    apply clarify
   1.180 -  apply(erule ctran.elims,simp_all)
   1.181 +  apply(erule ctran.cases,simp_all)
   1.182   apply clarify
   1.183   apply(rule_tac x="xs" in exI)
   1.184   apply simp
   1.185 @@ -185,10 +187,10 @@
   1.186  apply simp_all
   1.187  --{* basic *}
   1.188  apply clarify
   1.189 -apply(erule ctran.elims,simp_all)
   1.190 +apply(erule ctran.cases,simp_all)
   1.191  apply(rule CptnModNone,rule Basic,simp)
   1.192  apply clarify
   1.193 -apply(erule ctran.elims,simp_all)
   1.194 +apply(erule ctran.cases,simp_all)
   1.195  --{* Seq1 *}
   1.196  apply(rule_tac xs="[(None,ta)]" in CptnModSeq2)
   1.197    apply(erule CptnModNone)
   1.198 @@ -216,12 +218,12 @@
   1.199  apply(simp add:lift_def)
   1.200  --{* Cond *}
   1.201  apply clarify
   1.202 -apply(erule ctran.elims,simp_all)
   1.203 +apply(erule ctran.cases,simp_all)
   1.204  apply(force elim: CptnModCondT)
   1.205  apply(force elim: CptnModCondF)
   1.206  --{* While *}
   1.207  apply  clarify
   1.208 -apply(erule ctran.elims,simp_all)
   1.209 +apply(erule ctran.cases,simp_all)
   1.210  apply(rule CptnModNone,erule WhileF,simp)
   1.211  apply(drule div_seq,force)
   1.212  apply clarify
   1.213 @@ -231,7 +233,7 @@
   1.214  apply(force simp add:last_length elim:CptnModWhile2)
   1.215  --{* await *}
   1.216  apply clarify
   1.217 -apply(erule ctran.elims,simp_all)
   1.218 +apply(erule ctran.cases,simp_all)
   1.219  apply(rule CptnModNone,erule Await,simp+)
   1.220  done
   1.221  
   1.222 @@ -241,7 +243,7 @@
   1.223   apply(erule CptnModEnv)
   1.224  apply(case_tac P)
   1.225   apply simp
   1.226 - apply(erule ctran.elims,simp_all)
   1.227 + apply(erule ctran.cases,simp_all)
   1.228  apply(force elim:cptn_onlyif_cptn_mod_aux)
   1.229  done
   1.230  
   1.231 @@ -249,7 +251,7 @@
   1.232  apply(erule cptn.induct)
   1.233    apply(force simp add:lift_def CptnOne)
   1.234   apply(force intro:CptnEnv simp add:lift_def)
   1.235 -apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.elims)
   1.236 +apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.cases)
   1.237  done
   1.238  
   1.239  lemma cptn_append_is_cptn [rule_format]: 
   1.240 @@ -257,7 +259,7 @@
   1.241  apply(induct c1)
   1.242   apply simp
   1.243  apply clarify
   1.244 -apply(erule cptn.elims,simp_all)
   1.245 +apply(erule cptn.cases,simp_all)
   1.246   apply(force intro:CptnEnv)
   1.247  apply(force elim:CptnComp)
   1.248  done
   1.249 @@ -309,7 +311,7 @@
   1.250      apply(rule CptnComp)
   1.251      apply(erule CondF,simp)
   1.252  --{* Seq1 *}   
   1.253 -apply(erule cptn.elims,simp_all)
   1.254 +apply(erule cptn.cases,simp_all)
   1.255    apply(rule CptnOne)
   1.256   apply clarify
   1.257   apply(drule_tac P=P1 in lift_is_cptn)
   1.258 @@ -495,10 +497,10 @@
   1.259  seq_not_eq1 [THEN not_sym] seq_not_eq2 [THEN not_sym] 
   1.260  if_not_eq1 if_not_eq2 if_not_eq1 [THEN not_sym] if_not_eq2 [THEN not_sym]
   1.261  
   1.262 -lemma prog_not_eq_in_ctran_aux [rule_format]: "(P,s) -c\<rightarrow> (Q,t) \<Longrightarrow> (P\<noteq>Q)"
   1.263 -apply(erule ctran.induct)
   1.264 -apply simp_all
   1.265 -done
   1.266 +lemma prog_not_eq_in_ctran_aux:
   1.267 +  assumes c: "(P,s) -c\<rightarrow> (Q,t)"
   1.268 +  shows "P\<noteq>Q" using c
   1.269 +  by (induct x1 \<equiv> "(P,s)" x2 \<equiv> "(Q,t)" arbitrary: P s Q t) auto
   1.270  
   1.271  lemma prog_not_eq_in_ctran [simp]: "\<not> (P,s) -c\<rightarrow> (P,t)"
   1.272  apply clarify
   1.273 @@ -522,7 +524,7 @@
   1.274  done
   1.275  
   1.276  lemma tl_in_cptn: "\<lbrakk> a#xs \<in>cptn; xs\<noteq>[] \<rbrakk> \<Longrightarrow> xs\<in>cptn"
   1.277 -apply(force elim:cptn.elims)
   1.278 +apply(force elim:cptn.cases)
   1.279  done
   1.280  
   1.281  lemma tl_zero[rule_format]: 
   1.282 @@ -562,7 +564,7 @@
   1.283    apply(case_tac "i=ia",simp,simp)
   1.284    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.285    apply(drule_tac t=i in not_sym,simp)
   1.286 -  apply(erule etran.elims,simp)
   1.287 +  apply(erule etranE,simp)
   1.288   apply(rule ParCptnComp)
   1.289    apply(erule ParComp,simp)
   1.290  --{* applying the induction hypothesis *}
   1.291 @@ -584,7 +586,7 @@
   1.292       erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.293     apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.294     apply(drule_tac t=i  in not_sym,simp)
   1.295 -   apply(erule etran.elims,simp)
   1.296 +   apply(erule etranE,simp)
   1.297    apply(erule allE,erule impE,assumption,erule tl_in_cptn)
   1.298    apply(force simp add:same_length_def length_Suc_conv)
   1.299   apply(simp add:same_length_def same_state_def)
   1.300 @@ -620,7 +622,7 @@
   1.301      apply(rule tl_zero)
   1.302        apply(erule_tac x=l in allE, erule impE, assumption, 
   1.303              erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.304 -      apply(force elim:etran.elims intro:Env)
   1.305 +      apply(force elim:etranE intro:Env)
   1.306       apply force
   1.307      apply force
   1.308     apply simp
   1.309 @@ -637,7 +639,7 @@
   1.310            erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.311      apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE)
   1.312      apply(drule_tac t=i  in not_sym,simp)
   1.313 -    apply(erule etran.elims,simp)
   1.314 +    apply(erule etranE,simp)
   1.315     apply(erule tl_zero)
   1.316      apply force
   1.317     apply force
   1.318 @@ -654,7 +656,7 @@
   1.319      apply(erule_tac x=l  in allE, erule impE, assumption,
   1.320            erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.321      apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
   1.322 -    apply(erule etran.elims,simp)
   1.323 +    apply(erule etranE,simp)
   1.324     apply(rule tl_zero)
   1.325      apply force
   1.326     apply force
   1.327 @@ -668,7 +670,7 @@
   1.328      apply(erule_tac x=ia  in allE, erule impE, assumption,
   1.329      erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE)
   1.330      apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp)
   1.331 -    apply(force elim:etran.elims intro:Env)
   1.332 +    apply(force elim:etranE intro:Env)
   1.333     apply force
   1.334    apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.335   apply simp
   1.336 @@ -681,7 +683,7 @@
   1.337   apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.338  --{* first step is an environmental step *}
   1.339  apply clarify
   1.340 -apply(erule par_etran.elims)
   1.341 +apply(erule par_etran.cases)
   1.342  apply simp
   1.343  apply(rule ParCptnEnv)
   1.344  apply(erule_tac x="Ps" in allE)
   1.345 @@ -691,14 +693,14 @@
   1.346  apply(rule conjI)
   1.347   apply clarify
   1.348   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I ?s j) \<in> cptn" in allE,simp)
   1.349 - apply(erule cptn.elims)
   1.350 + apply(erule cptn.cases)
   1.351     apply(simp add:same_length_def)
   1.352     apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.353    apply(simp add:same_state_def)
   1.354    apply(erule_tac x=i  in allE, erule impE, assumption,
   1.355     erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.356   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<in>etran" in allE,simp)
   1.357 - apply(erule etran.elims,simp)
   1.358 + apply(erule etranE,simp)
   1.359  apply(simp add:same_state_def same_length_def)
   1.360  apply(rule conjI,clarify)
   1.361   apply(case_tac j,simp,simp)
   1.362 @@ -725,7 +727,7 @@
   1.363   apply(rule_tac x=i in exI,simp)
   1.364   apply(rule conjI)
   1.365    apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.366 -  apply(erule etran.elims,simp)
   1.367 +  apply(erule etranE,simp)
   1.368    apply(erule_tac x=i  in allE, erule impE, assumption,
   1.369          erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.370    apply(rule nth_tl_if)
   1.371 @@ -735,7 +737,7 @@
   1.372    apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.373   apply clarify
   1.374   apply(erule_tac x=l and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.375 - apply(erule etran.elims,simp)
   1.376 + apply(erule etranE,simp)
   1.377   apply(erule_tac x=l  in allE, erule impE, assumption,
   1.378         erule_tac x=1 and P="\<lambda>j.  (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp)
   1.379   apply(rule nth_tl_if)
   1.380 @@ -751,7 +753,7 @@
   1.381   apply(rule tl_zero)
   1.382     apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.383     apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption)
   1.384 -   apply(force elim:etran.elims intro:Env)
   1.385 +   apply(force elim:etranE intro:Env)
   1.386    apply force
   1.387   apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force)
   1.388  apply simp
   1.389 @@ -778,7 +780,7 @@
   1.390    apply(rule nth_equalityI,simp,simp)
   1.391   apply(force intro: cptn.intros)
   1.392  apply(clarify)
   1.393 -apply(erule par_cptn.elims,simp)
   1.394 +apply(erule par_cptn.cases,simp)
   1.395   apply simp
   1.396   apply(erule_tac x="xs" in allE)
   1.397   apply(erule_tac x="t" in allE,simp)
   1.398 @@ -811,7 +813,7 @@
   1.399    apply clarify
   1.400    apply(rule_tac x=i in exI,simp)
   1.401   apply force
   1.402 -apply(erule par_ctran.elims,simp)
   1.403 +apply(erule par_ctran.cases,simp)
   1.404  apply(erule_tac x="Ps[i:=r]" in allE)
   1.405  apply(erule_tac x="ta" in allE,simp)
   1.406  apply clarify
   1.407 @@ -887,7 +889,7 @@
   1.408    apply(clarify)
   1.409    apply(simp add:par_cp_def cp_def)
   1.410    apply(case_tac x)
   1.411 -   apply(force elim:par_cptn.elims)
   1.412 +   apply(force elim:par_cptn.cases)
   1.413    apply simp
   1.414    apply(erule_tac x="list" in allE)
   1.415    apply clarify
   1.416 @@ -899,7 +901,7 @@
   1.417    apply(erule_tac x=0 in allE)
   1.418    apply(simp add:cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def)
   1.419    apply clarify
   1.420 -  apply(erule cptn.elims,force,force,force)
   1.421 +  apply(erule cptn.cases,force,force,force)
   1.422   apply(simp add:par_cp_def conjoin_def  same_length_def same_program_def same_state_def compat_label_def)
   1.423   apply clarify
   1.424   apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in all_dupE)