(*  Title:      HOL/IMPP/Misc.ML

    ID:         $Id$

    Author:     David von Oheimb

    Copyright   1999 TUM

*)

section "state access";

Goalw [getlocs_def] "getlocs (st g l) = l";

by (Simp_tac 1);

qed "getlocs_def2";

Goalw [update_def] "s[Loc Y::=s<Y>] = s";

by (induct_tac "s" 1);

by (simp_tac (simpset() addsimps [getlocs_def2]) 1);

qed "update_Loc_idem2";

Addsimps[update_Loc_idem2];

Goalw [update_def] "s[X::=x][X::=y] = s[X::=y]";

by (induct_tac "X" 1);

by  Auto_tac;

by  (ALLGOALS (induct_tac "s"));

by  Auto_tac;

by  (ALLGOALS (rtac ext));

by  Auto_tac;

qed "update_overwrt";

Addsimps[update_overwrt];

Goalw [update_def]"(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)";

by (induct_tac "s" 1);

by (simp_tac (simpset() addsimps [getlocs_def2]) 1);

qed "getlocs_Loc_update";

Addsimps[getlocs_Loc_update];

Goalw [update_def] "getlocs (s[Glb Y::=k]) = getlocs s";

by (induct_tac "s" 1);

by (simp_tac (simpset() addsimps [getlocs_def2]) 1);

qed "getlocs_Glb_update";

Addsimps[getlocs_Glb_update];

Goalw [setlocs_def] "getlocs (setlocs s l) = l";

by (induct_tac "s" 1);

by Auto_tac;

by (simp_tac (simpset() addsimps [getlocs_def2]) 1);

qed "getlocs_setlocs";

Addsimps[getlocs_setlocs];

Goal "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])";

by (induct_tac "Y" 1);

br ext 2;

by Auto_tac;

qed "getlocs_setlocs_lemma";

(*unused*)

Goalw [hoare_valids_def] 

"!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}";

by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);

by (Clarsimp_tac 1);

by (dres_inst_tac [("x","s<Y>")] spec 1);

by (smp_tac 1 1);

bd spec 1;

by (dres_inst_tac [("x","s[Loc Y::=a s]")] spec 1);

by (Full_simp_tac 1);

by (mp_tac 1);

by (smp_tac 1 1);

by (Simp_tac 1);

qed "classic_Local_valid";

Goal "!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}";

br export_s 1;

(*variant 1*)

br (hoare_derivs.Local RS conseq1) 1;

be  spec 1;

by (Force_tac 1);

(*variant 2

by (res_inst_tac [("P'","%Z s. s' = s & P Z (s[Loc Y::=a s][Loc Y::=s'<Y>]) & (s[Loc Y::=a s])<Y> = a (s[Loc Y::=a s][Loc Y::=s'<Y>])")] conseq1 1);

by  (Clarsimp_tac 2);

br hoare_derivs.Local 1;

be spec 1;

*)

qed "classic_Local";

Goal "[| 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}";

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~=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}";

br export_s 1;

br hoare_derivs.Local 1;

by (Clarsimp_tac 1);

qed "Local_indep";

Goal "[| 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}";

br weak_Local 1;

by (ALLGOALS Clarsimp_tac);

qed "weak_Local_indep";

Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";

br export_s 1;

by (res_inst_tac [("P'","%Z s. s'=s & True"), ("Q'","%Z s. s'<Y> = s<Y>")] (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<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";

br classic_Local 1;

by (Clarsimp_tac 1);

br (trueI RS conseq12) 1;

by (Clarsimp_tac 1);

qed "classic_Local_invariant";

Goal "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}";

by (res_inst_tac [("s'1","s'"),("Q'","%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s")] (hoare_derivs.Call RS conseq12) 1);

by  (asm_simp_tac  (simpset() addsimps [getlocs_setlocs_lemma]) 1);

by (Force_tac 1);

qed "Call_invariant";