(* Title: HOL/IMPP/Misc.thy ID: $Id: Misc.thy,v 1.2 2005/09/17 18:14:30 wenzelm Exp $ Author: David von Oheimb Copyright 1999 TUM *) header {* Several examples for Hoare logic *} theory Misc imports Hoare begin defs newlocs_def: "newlocs == %x. arbitrary" setlocs_def: "setlocs s l' == case s of st g l => st g l'" getlocs_def: "getlocs s == case s of st g l => l" update_def: "update s vn v == case vn of Glb gn => (case s of st g l => st (g(gn:=v)) l) | Loc ln => (case s of st g l => st g (l(ln:=v)))" ML {* use_legacy_bindings (the_context ()) *} end
theorem getlocs_def2:
getlocs (st g l) = l
theorem update_Loc_idem2:
s[Loc Y::=s<Y>] = s
theorem update_overwrt:
s[X::=x][X::=y] = s[X::=y]
theorem getlocs_Loc_update:
s[Loc Y::=k]<Y'> = (if Y = Y' then k else s<Y'>)
theorem getlocs_Glb_update:
getlocs (s[Glb Y::=k]) = getlocs s
theorem getlocs_setlocs:
getlocs (setlocs s l) = l
theorem getlocs_setlocs_lemma:
getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])
theorem classic_Local_valid:
∀v. G|={%Z s. P Z (s[Loc Y::=v]) ∧ s<Y> = a (s[Loc Y::=v])}. c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}
theorem classic_Local:
∀v. G|-{%Z s. P Z (s[Loc Y::=v]) ∧ s<Y> = a (s[Loc Y::=v])}. c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}
theorem classic_Local_indep:
[| Y ≠ Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}
theorem Local_indep:
[| Y ≠ Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}
theorem weak_Local_indep:
[| Y' ≠ Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}
theorem export_Local_invariant:
G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}
theorem classic_Local_invariant:
G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}
theorem Call_invariant:
G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==> G|-{%Z s. s' = s ∧ I Z (getlocs (s[X::=k Z])) ∧ P Z (setlocs s newlocs[Loc Arg::=a s])}. X:=CALL pn(a) .{%Z s. I Z (getlocs (s[X::=k Z])) ∧ Q Z s}