equal
deleted
inserted
replaced
69 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}" |
69 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}" |
70 apply (unfold hoare_valids_def) |
70 apply (unfold hoare_valids_def) |
71 apply (simp (no_asm_use) add: triple_valid_def2) |
71 apply (simp (no_asm_use) add: triple_valid_def2) |
72 apply clarsimp |
72 apply clarsimp |
73 apply (drule_tac x = "s<Y>" in spec) |
73 apply (drule_tac x = "s<Y>" in spec) |
74 apply (tactic "smp_tac 1 1") |
74 apply (tactic "smp_tac @{context} 1 1") |
75 apply (drule spec) |
75 apply (drule spec) |
76 apply (drule_tac x = "s[Loc Y::=a s]" in spec) |
76 apply (drule_tac x = "s[Loc Y::=a s]" in spec) |
77 apply (simp (no_asm_use)) |
77 apply (simp (no_asm_use)) |
78 apply (erule (1) notE impE) |
78 apply (erule (1) notE impE) |
79 apply (tactic "smp_tac 1 1") |
79 apply (tactic "smp_tac @{context} 1 1") |
80 apply simp |
80 apply simp |
81 done |
81 done |
82 |
82 |
83 lemma classic_Local: "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. |
83 lemma classic_Local: "!v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. |
84 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}" |
84 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}" |