Theory Misc

Up to index of Isabelle/HOL/IMPP

(*  Title:      HOL/IMPP/Misc.thy
    ID:         $Id: Misc.thy,v 1.1 1999/11/12 17:09:09 oheimb Exp $
    Author:     David von Oheimb
    Copyright   1999 TUM

Several examples for Hoare logic
*)
Misc = Hoare

theorem classic_Local_indep:

  [| Y ~= X; G|-{P}. c .{%Z s. s<X> = d} |]
  ==> G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<X> = d}

theorem Local_indep:

  [| Y ~= X; G|-{P}. c .{%Z s. s<X> = d} |]
  ==> G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<X> = d}

theorem weak_Local_indep:

  [| X ~= Y; G|-{P}. c .{%Z s. s<X> = d} |]
  ==> G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<X> = d}

theorem export_Local_invariant:

  G|-{%Z s. Z = s<X>}. LOCAL X:=a IN c .{%Z s. Z = s<X>}

theorem classic_Local_invariant:

  G|-{%Z s. Z = s<X>}. LOCAL X:=a IN c .{%Z s. Z = s<X>}