File Misc.ML

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

Goal "[| 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}";
br classic_Local 1;
by (ALLGOALS Clarsimp_tac);
be conseq12 1;
by (Clarsimp_tac 1);
bd sym 1;
by (Asm_full_simp_tac 1);
qed "classic_Local_indep";

Goal "[| 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}";
br export_s 1;
br hoare_derivs.Local 1;
by (Clarsimp_tac 1);
qed "Local_indep";

Goal "[| 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}";
br weak_Local 1;
by (ALLGOALS Clarsimp_tac);
qed "weak_Local_indep";


Goal "G|-{%Z s. Z = s<X>}. LOCAL X:=a IN c .{%Z s. Z = s<X>}";
br export_s 1;
by (res_inst_tac [("P'","%Z s. s'=s & True"), ("Q'","%Z s. s'<X> = s<X>")] (conseq12) 1);
by  (Clarsimp_tac 2);
br hoare_derivs.Local 1;
by (Clarsimp_tac 1);
br trueI 1;
qed "export_Local_invariant";

Goal "G|-{%Z s. Z = s<X>}. LOCAL X:=a IN c .{%Z s. Z = s<X>}";
br classic_Local 1;
by (Clarsimp_tac 1);
br (trueI RS conseq12) 1;
by (Clarsimp_tac 1);
qed "classic_Local_invariant";