# File Misc.ML

    (*  Title:      HOL/IMPP/Misc.ML
        ID:         $Id: Misc.ML,v 1.4 2004/12/01 17:11:19 nipkow Exp $
        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);
    by (rtac 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);
    by (dtac 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}";
    by (rtac export_s 1);
    (*variant 1*)
    by (rtac (hoare_derivs.Local RS conseq1) 1);
    by (etac 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);
    by (rtac hoare_derivs.Local 1);
    by (etac 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}";
    by (rtac classic_Local 1);
    by (ALLGOALS Clarsimp_tac);
    by (etac conseq12 1);
    by (Clarsimp_tac 1);
    by (dtac 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}";
    by (rtac export_s 1);
    by (rtac 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}";
    by (rtac 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>}";
    by (rtac 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);
    by (rtac hoare_derivs.Local 1);
    by (Clarsimp_tac 1);
    by (rtac trueI 1);
    qed "export_Local_invariant";

    Goal "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}";
    by (rtac classic_Local 1);
    by (Clarsimp_tac 1);
    by (rtac (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";