1264 apply(erule one [THEN equalityD1]) |
1264 apply(erule one [THEN equalityD1]) |
1265 apply(erule subsetD) |
1265 apply(erule subsetD) |
1266 apply simp |
1266 apply simp |
1267 apply clarify |
1267 apply clarify |
1268 apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))") |
1268 apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))") |
1269 apply(erule_tac x=i and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption) |
1269 apply(erule_tac x=xa and P="\<lambda>i. H i \<longrightarrow> \<Turnstile> (J i) sat [I i,K i,M i,N i]" for H J I K M N in allE,erule impE,assumption) |
1270 apply(simp add:com_validity_def) |
1270 apply(simp add:com_validity_def) |
1271 apply(erule_tac x=s in allE) |
1271 apply(erule_tac x=s in allE) |
1272 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp) |
1272 apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> (I j) \<in> cp (J j) s" for H I J in allE,simp) |
1273 apply(drule_tac c="clist!i" in subsetD) |
1273 apply(drule_tac c="clist!xa" in subsetD) |
1274 apply (force simp add:Com_def) |
1274 apply (force simp add:Com_def) |
1275 apply(simp add:comm_def conjoin_def same_program_def del:last.simps) |
1275 apply(simp add:comm_def conjoin_def same_program_def del:last.simps) |
1276 apply clarify |
1276 apply clarify |
1277 apply(erule_tac x="length x - 1" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE) |
1277 apply(erule_tac x="length x - 1" and P="\<lambda>j. H j \<longrightarrow> fst(I j)=(J j)" for H I J in allE) |
1278 apply (simp add:All_None_def same_length_def) |
1278 apply (simp add:All_None_def same_length_def) |
1279 apply(erule_tac x=i and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE) |
1279 apply(erule_tac x=xa and P="\<lambda>j. H j \<longrightarrow> length(J j)=(K j)" for H J K in allE) |
1280 apply(subgoal_tac "length x - 1 < length x",simp) |
1280 apply(subgoal_tac "length x - 1 < length x",simp) |
1281 apply(case_tac "x\<noteq>[]") |
1281 apply(case_tac "x\<noteq>[]") |
1282 apply(simp add: last_conv_nth) |
1282 apply(simp add: last_conv_nth) |
1283 apply(erule_tac x="clist!i" in ballE) |
1283 apply(erule_tac x="clist!xa" in ballE) |
1284 apply(simp add:same_state_def) |
1284 apply(simp add:same_state_def) |
1285 apply(subgoal_tac "clist!i\<noteq>[]") |
1285 apply(subgoal_tac "clist!xa\<noteq>[]") |
1286 apply(simp add: last_conv_nth) |
1286 apply(simp add: last_conv_nth) |
1287 apply(case_tac x) |
1287 apply(case_tac x) |
1288 apply (force simp add:par_cp_def) |
1288 apply (force simp add:par_cp_def) |
1289 apply (force simp add:par_cp_def) |
1289 apply (force simp add:par_cp_def) |
1290 apply force |
1290 apply force |
1295 apply clarify |
1295 apply clarify |
1296 apply(simp add:assum_def) |
1296 apply(simp add:assum_def) |
1297 apply(rule conjI) |
1297 apply(rule conjI) |
1298 apply(simp add:conjoin_def same_state_def par_cp_def) |
1298 apply(simp add:conjoin_def same_state_def par_cp_def) |
1299 apply clarify |
1299 apply clarify |
1300 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)))" for T H d e in allE,simp) |
1300 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)))" for T H d e in allE,simp) |
1301 apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE) |
1301 apply(erule_tac x=0 and P="\<lambda>j. H j \<longrightarrow> (snd (d j))=(snd (e j))" for H d e in allE) |
1302 apply(case_tac x,simp+) |
1302 apply(case_tac x,simp+) |
1303 apply (simp add:par_assum_def) |
1303 apply (simp add:par_assum_def) |
1304 apply clarify |
1304 apply clarify |
1305 apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD) |
1305 apply(drule_tac c="snd (clist ! i ! 0)" in subsetD) |
1306 apply assumption |
1306 apply assumption |
1307 apply simp |
1307 apply simp |
1308 apply clarify |
1308 apply clarify |
1309 apply(erule_tac x=ia in all_dupE) |
1309 apply(erule_tac x=i in all_dupE) |
1310 apply(rule subsetD, erule mp, assumption) |
1310 apply(rule subsetD, erule mp, assumption) |
1311 apply(erule_tac pre=pre and rely=rely and x=x and s=s in three) |
1311 apply(erule_tac pre=pre and rely=rely and x=x and s=s in three) |
1312 apply(erule_tac x=ic in allE,erule mp) |
1312 apply(erule_tac x=ib in allE,erule mp) |
1313 apply simp_all |
1313 apply simp_all |
1314 apply(simp add:ParallelCom_def) |
1314 apply(simp add:ParallelCom_def) |
1315 apply(force simp add:Com_def) |
1315 apply(force simp add:Com_def) |
1316 apply(simp add:conjoin_def same_length_def) |
1316 apply(simp add:conjoin_def same_length_def) |
1317 done |
1317 done |