284 apply blast |
284 apply blast |
285 apply (blast) (* asm *) |
285 apply (blast) (* asm *) |
286 apply (blast) (* cut *) |
286 apply (blast) (* cut *) |
287 apply (blast) (* weaken *) |
287 apply (blast) (* weaken *) |
288 apply (tactic {* ALLGOALS (EVERY' |
288 apply (tactic {* ALLGOALS (EVERY' |
289 [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs ?x ?y" [], |
289 [REPEAT o Rule_Insts.thin_tac @{context} "hoare_derivs _ _" [], |
290 simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *}) |
290 simp_tac @{context}, clarify_tac @{context}, REPEAT o smp_tac @{context} 1]) *}) |
291 apply (simp_all (no_asm_use) add: triple_valid_def2) |
291 apply (simp_all (no_asm_use) add: triple_valid_def2) |
292 apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *) |
292 apply (intro strip, tactic "smp_tac @{context} 2 1", blast) (* conseq *) |
293 apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *) |
293 apply (tactic {* ALLGOALS (clarsimp_tac @{context}) *}) (* Skip, Ass, Local *) |
294 prefer 3 apply (force) (* Call *) |
294 prefer 3 apply (force) (* Call *) |
313 lemma MGT_alternD: "state_not_singleton ==> |
313 lemma MGT_alternD: "state_not_singleton ==> |
314 G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c" |
314 G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1} ==> G|-MGT c" |
315 apply (unfold MGT_def) |
315 apply (unfold MGT_def) |
316 apply (erule conseq12) |
316 apply (erule conseq12) |
317 apply auto |
317 apply auto |
318 apply (case_tac "? t. <c,?s> -c-> t") |
318 apply (case_tac "\<exists>t. <c,s> -c-> t" for s) |
319 apply (fast elim: com_det) |
319 apply (fast elim: com_det) |
320 apply clarsimp |
320 apply clarsimp |
321 apply (drule single_stateE) |
321 apply (drule single_stateE) |
322 apply blast |
322 apply blast |
323 done |
323 done |