equal
deleted
inserted
replaced
85 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}" |
85 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}" |
86 apply (unfold hoare_valids_def) |
86 apply (unfold hoare_valids_def) |
87 apply (simp (no_asm_use) add: triple_valid_def2) |
87 apply (simp (no_asm_use) add: triple_valid_def2) |
88 apply clarsimp |
88 apply clarsimp |
89 apply (drule_tac x = "s<Y>" in spec) |
89 apply (drule_tac x = "s<Y>" in spec) |
90 apply (tactic "smp_tac @{context} 1 1") |
90 apply (tactic "smp_tac \<^context> 1 1") |
91 apply (drule spec) |
91 apply (drule spec) |
92 apply (drule_tac x = "s[Loc Y::=a s]" in spec) |
92 apply (drule_tac x = "s[Loc Y::=a s]" in spec) |
93 apply (simp (no_asm_use)) |
93 apply (simp (no_asm_use)) |
94 apply (erule (1) notE impE) |
94 apply (erule (1) notE impE) |
95 apply (tactic "smp_tac @{context} 1 1") |
95 apply (tactic "smp_tac \<^context> 1 1") |
96 apply simp |
96 apply simp |
97 done |
97 done |
98 |
98 |
99 lemma classic_Local: "\<forall>v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. |
99 lemma classic_Local: "\<forall>v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. |
100 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}" |
100 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}" |