671 apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)") |
671 apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)") |
672 apply clarify |
672 apply clarify |
673 apply(case_tac xsa,simp,simp) |
673 apply(case_tac xsa,simp,simp) |
674 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp) |
674 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp) |
675 apply(rule conjI,erule CptnEnv) |
675 apply(rule conjI,erule CptnEnv) |
676 apply(simp add:lift_def) |
676 apply(simp (no_asm_use) add:lift_def) |
677 apply clarify |
677 apply clarify |
678 apply(erule_tac x="Suc i" in allE, simp) |
678 apply(erule_tac x="Suc i" in allE, simp) |
679 apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran") |
679 apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran") |
680 apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def) |
680 apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def) |
681 apply(erule_tac x="length xs" in allE, simp) |
681 apply(erule_tac x="length xs" in allE, simp) |
704 prefer 2 |
704 prefer 2 |
705 apply force |
705 apply force |
706 apply(case_tac xsa,simp,simp) |
706 apply(case_tac xsa,simp,simp) |
707 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp) |
707 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp) |
708 apply(rule conjI,erule CptnEnv) |
708 apply(rule conjI,erule CptnEnv) |
709 apply(simp add:lift_def) |
709 apply(simp (no_asm_use) add:lift_def) |
710 apply(rule_tac x=ys in exI,simp) |
710 apply(rule_tac x=ys in exI,simp) |
711 apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran") |
711 apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran") |
712 apply simp |
712 apply simp |
713 apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp) |
713 apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp) |
714 apply(rule conjI) |
714 apply(rule conjI) |
1236 apply(erule disjE) |
1236 apply(erule disjE) |
1237 --{* a c-tran in some @{text "\<sigma>_{ib}"} *} |
1237 --{* a c-tran in some @{text "\<sigma>_{ib}"} *} |
1238 apply clarify |
1238 apply clarify |
1239 apply(case_tac "i=ib",simp) |
1239 apply(case_tac "i=ib",simp) |
1240 apply(erule etran.elims,simp) |
1240 apply(erule etran.elims,simp) |
1241 apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp) |
1241 apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE) |
|
1242 apply (erule etran.elims) |
1242 apply(case_tac "ia=m",simp) |
1243 apply(case_tac "ia=m",simp) |
1243 apply(erule etran.elims,simp) |
1244 apply simp |
1244 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE) |
1245 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE) |
1245 apply(subgoal_tac "ia<m",simp) |
1246 apply(subgoal_tac "ia<m",simp) |
1246 prefer 2 |
1247 prefer 2 |
1247 apply arith |
1248 apply arith |
1248 apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp) |
1249 apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp) |
1249 apply(simp add:same_state_def) |
1250 apply(simp add:same_state_def) |
1250 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp) |
1251 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE) |
1251 apply(erule_tac x=ib and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
1252 apply(erule_tac x=ib and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
1252 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE) |
|
1253 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE) |
|
1254 apply(erule_tac x="Suc ia" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
1255 apply(erule_tac x="Suc ia" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
1256 apply simp |
|
1257 --{* or an e-tran in @{text "\<sigma>"}, |
1253 --{* or an e-tran in @{text "\<sigma>"}, |
1258 therefore it satisfies @{text "rely \<or> guar_{ib}"} *} |
1254 therefore it satisfies @{text "rely \<or> guar_{ib}"} *} |
1259 apply (force simp add:par_assum_def same_state_def) |
1255 apply (force simp add:par_assum_def same_state_def) |
1260 done |
1256 done |
1261 |
1257 |
1283 apply(erule etran.elims,simp) |
1279 apply(erule etran.elims,simp) |
1284 apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp) |
1280 apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp) |
1285 apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE) |
1281 apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE) |
1286 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE) |
1282 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE) |
1287 apply(simp add:same_state_def) |
1283 apply(simp add:same_state_def) |
1288 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp) |
1284 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE) |
1289 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
1285 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
1290 apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE) |
|
1291 apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE) |
|
1292 apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
1293 apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
1294 apply simp |
|
1295 done |
1286 done |
1296 |
1287 |
1297 lemma four: |
1288 lemma four: |
1298 "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) |
1289 "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) |
1299 \<subseteq> Rely (xs ! i); |
1290 \<subseteq> Rely (xs ! i); |
1375 apply(erule_tac x="length x - 1" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE) |
1366 apply(erule_tac x="length x - 1" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE) |
1376 apply (simp add:All_None_def same_length_def) |
1367 apply (simp add:All_None_def same_length_def) |
1377 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE) |
1368 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE) |
1378 apply(subgoal_tac "length x - 1 < length x",simp) |
1369 apply(subgoal_tac "length x - 1 < length x",simp) |
1379 apply(case_tac "x\<noteq>[]") |
1370 apply(case_tac "x\<noteq>[]") |
1380 apply(drule last_length2,simp) |
1371 apply(simp add: last_length2) |
1381 apply(erule_tac x="clist!i" in ballE) |
1372 apply(erule_tac x="clist!i" in ballE) |
1382 apply(simp add:same_state_def) |
1373 apply(simp add:same_state_def) |
1383 apply(subgoal_tac "clist!i\<noteq>[]") |
1374 apply(subgoal_tac "clist!i\<noteq>[]") |
1384 apply(drule_tac xs="clist!i" in last_length2,simp) |
1375 apply(simp add: last_length2) |
1385 apply(case_tac x) |
1376 apply(case_tac x) |
1386 apply (force simp add:par_cp_def) |
1377 apply (force simp add:par_cp_def) |
1387 apply (force simp add:par_cp_def) |
1378 apply (force simp add:par_cp_def) |
1388 apply force |
1379 apply force |
1389 apply (force simp add:par_cp_def) |
1380 apply (force simp add:par_cp_def) |
1403 apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD) |
1394 apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD) |
1404 apply assumption |
1395 apply assumption |
1405 apply simp |
1396 apply simp |
1406 apply clarify |
1397 apply clarify |
1407 apply(erule_tac x=ia in all_dupE) |
1398 apply(erule_tac x=ia in all_dupE) |
1408 apply simp |
1399 apply(rule subsetD, erule mp, assumption) |
1409 apply(rule subsetD) |
|
1410 apply simp |
|
1411 apply(erule_tac pre=pre and rely=rely and x=x and s=s in three) |
1400 apply(erule_tac pre=pre and rely=rely and x=x and s=s in three) |
1412 apply(erule_tac x=ic in allE,erule mp) |
1401 apply(erule_tac x=ic in allE,erule mp) |
1413 apply simp_all |
1402 apply simp_all |
1414 apply(simp add:ParallelCom_def) |
1403 apply(simp add:ParallelCom_def) |
1415 apply(force simp add:Com_def) |
1404 apply(force simp add:Com_def) |