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