File Hoare.ML

(*  Title:      HOL/IMPP/Hoare.ML
    ID:         $Id: Hoare.ML,v 1.36 1999/11/24 13:48:19 oheimb Exp $
    Author:     Tobias Nipkow, complete revision by David von Oheimb
    Copyright   1995, 1999 TUM

Soundness and relative completeness of Hoare rules wrt operational semantics
*)

Addsimps[peek_and_def];


section "validity";

Goalw [triple_valid_def] 
  "|=n:{P}.c.{Q} = (!Z s. P Z s --> (!s'. <c,s> -n-> s' --> Q Z s'))";
by Auto_tac;
qed "triple_valid_def2";

Goal "|=0:{P}. BODY pn .{Q}";
by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
by (Clarsimp_tac 1);
qed "Body_triple_valid_0";

(* only ==> direction required *)
Goal "|=n:{P}. body pn .{Q} = |=Suc n:{P}. BODY pn .{Q}";
by (simp_tac (simpset() addsimps [triple_valid_def2]) 1);
by (Force_tac 1);
qed "Body_triple_valid_Suc";

Goalw [triple_valid_def] "|=Suc n:t --> |=n:t";
by (induct_tac "t" 1);
by (Simp_tac 1);
by (fast_tac (claset() addIs [evaln_Suc]) 1);
qed_spec_mp "triple_valid_Suc";

Goal "||=Suc n:ts ==> ||=n:ts";
by (fast_tac (claset() addIs [triple_valid_Suc]) 1);
qed "triples_valid_Suc";


section "derived rules";

Goal "[| G|-{P'}.c.{Q'}; !Z s. P Z s --> \
\                        (!s'. (!Z'. P' Z' s --> Q' Z' s') --> Q Z s') |] \
\      ==> G|-{P}.c.{Q}";
br hoare_derivs.conseq 1;
by (Blast_tac 1);
qed "conseq12";

Goal "[| G|-{P'}.c.{Q}; !Z s. P Z s --> P' Z s |] ==> G|-{P}.c.{Q}";
be conseq12 1;
by (Fast_tac 1);
qed "conseq1";

Goal "[| G|-{P}.c.{Q'}; !Z s. Q' Z s --> Q Z s |] ==> G|-{P}.c.{Q}";
be conseq12 1;
by (Fast_tac 1);
qed "conseq2";

(*
Goal "G||-ts' ==> !ts. ts<=ts' --> G||-ts";
by                (etac hoare_derivs.induct 1);
by                (ALLGOALS strip_tac);
by                (ALLGOALS (REPEAT o (EVERY'[dtac subset_singletonD,etac disjE,
              		fast_tac (claset() addSIs [hoare_derivs.empty])])));
by                (TRYALL hyp_subst_tac);
by                (EVERY'[Asm_full_simp_tac, rtac hoare_derivs.empty] 1);
bd               subset_insertD 1;
by               (blast_tac (claset() addIs [hoare_derivs.insert]) 1);
by              (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
by             (blast_tac (claset() addIs [hoare_derivs.cut]) 1);
by            (blast_tac (claset() addIs [hoare_derivs.weaken]) 1);
by           (EVERY'[rtac hoare_derivs.conseq,
			Clarify_tac,smp_tac 2,Blast_tac]1);
by          (TRYALL (resolve_tac ((funpow 5 tl) hoare_derivs.intrs) 
		THEN_ALL_NEW atac));
by (defer_tac 1);
qed_spec_mp "weaken";
*)

Goal "[| G Un (%p. {P p}. BODY p .{Q p})``Procs  \
\         ||- (%p. {P p}. body p .{Q p})``Procs; \
\        pn:Procs |] ==> G|-{P pn}. BODY pn .{Q pn}";
bd hoare_derivs.Body 1;
be hoare_derivs.weaken 1;
by (Fast_tac 1);
qed "Body1";

Goal "(insert ({P}. BODY pn .{Q}) G) |-{P}. body pn .{Q} ==> \
\ G|-{P}. BODY pn .{Q}";
br Body1 1;
br  singletonI 2;
by (Clarsimp_tac 1);
qed "BodyN";

Goal "[| !Z s. P Z s --> G|-{%Z s'. s'=s}.c.{%Z'. Q Z} |] ==> G|-{P}.c.{Q}";
br hoare_derivs.conseq 1;
by (Fast_tac 1);
qed "escape";

Goal "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}";
br hoare_derivs.conseq 1;
by (fast_tac (claset() addDs (premises())) 1);
qed "constant";

Goal "G|-{%Z s. P Z s & ~b s}.WHILE b DO c.{P}";
br (hoare_derivs.Loop RS conseq2) 1;
by  (ALLGOALS Simp_tac);
br hoare_derivs.conseq 1;
by (Fast_tac 1);
qed "LoopF";

(*
Goal "[| G'||-ts; G' <= G |] ==> G||-ts";
be hoare_derivs.cut 1;
be hoare_derivs.asm 1;
qed "thin";
*)
Goal "G'||-ts ==> !G. G' <= G --> G||-ts";
by (etac hoare_derivs.induct 1);
by                (ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]));
br		  hoare_derivs.empty 1;
by               (eatac hoare_derivs.insert 1 1);
by              (fast_tac (claset() addIs [hoare_derivs.asm]) 1);
by             (fast_tac (claset() addIs [hoare_derivs.cut]) 1);
by            (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
by           (EVERY'[rtac hoare_derivs.conseq, strip_tac, smp_tac 2,Clarify_tac,
	             smp_tac 1,rtac exI, rtac exI, eatac conjI 1] 1);
by          (EVERY'[rtac hoare_derivs.Body,dtac spec,etac mp,Fast_tac]9); 
by         (ALLGOALS (resolve_tac ((funpow 5 tl) hoare_derivs.intrs)
	              THEN_ALL_NEW Fast_tac));
qed_spec_mp "thin";

Goal "G|-{P}. body pn .{Q} ==> G|-{P}. BODY pn .{Q}";
br BodyN 1;
be thin 1;
by Auto_tac;
qed "weak_Body";

Goal "G||-insert t ts ==> G|-t & G||-ts";
by (fast_tac (claset() addIs [hoare_derivs.weaken]) 1);
qed "derivs_insertD";

Goal "[| finite U; \
\ !p. G |-     {P' p}.c0 p.{Q' p}       --> G |-     {P p}.c0 p.{Q p} |] ==> \
\     G||-(%p. {P' p}.c0 p.{Q' p}) `` U --> G||-(%p. {P p}.c0 p.{Q p}) `` U";
be finite_induct 1;
by (ALLGOALS Clarsimp_tac);
bd derivs_insertD 1;
br hoare_derivs.insert 1;
by  Auto_tac;
qed_spec_mp "finite_pointwise";


section "soundness";

Goalw [hoare_valids_def]
 "G|={P &> b}. c .{P} ==> \
\ G|={P}. WHILE b DO c .{P &> (Not o b)}";
by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
br allI 1;
by (subgoal_tac "!d s s'. <d,s> -n-> s' --> \
\ d = WHILE b DO c --> ||=n:G --> (!Z. P Z s --> P Z s' & ~b s')" 1);
by  (EVERY'[etac thin_rl, Fast_tac] 1);
by (EVERY'[REPEAT o rtac allI, rtac impI] 1);
by ((etac evaln.induct THEN_ALL_NEW Simp_tac) 1);
by  (ALLGOALS Fast_tac);
qed "Loop_sound_lemma";

Goalw [hoare_valids_def]
   "[| G Un (%pn. {P pn}. BODY pn .{Q pn})``Procs \
\        ||=(%pn. {P pn}. body pn .{Q pn})``Procs |] ==> \
\      G||=(%pn. {P pn}. BODY pn .{Q pn})``Procs";
br allI 1;
by (induct_tac "n" 1);
by  (fast_tac (claset() addIs [Body_triple_valid_0]) 1);
by (Clarsimp_tac 1);
bd triples_valid_Suc 1;
by (mp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [ball_Un]) 1);
by (EVERY'[dtac spec, etac impE, etac conjI, atac] 1);
by (fast_tac (claset() addSIs [Body_triple_valid_Suc RS iffD1]) 1);
qed "Body_sound_lemma";

Goal "G||-ts ==> G||=ts";
be hoare_derivs.induct 1;
by                (TRYALL (eresolve_tac [Loop_sound_lemma, Body_sound_lemma]
                          THEN_ALL_NEW atac));
by              (rewtac hoare_valids_def);
by              (Blast_tac 1);
by             (Blast_tac 1);
by            (Blast_tac 1); (* asm *)
by           (Blast_tac 1); (* cut *)
by          (Blast_tac 1); (* weaken *)
by         (ALLGOALS (EVERY'[REPEAT o thin_tac "?x : hoare_derivs", 
	                     Clarsimp_tac, REPEAT o smp_tac 1]));
by         (ALLGOALS (full_simp_tac (simpset() addsimps [triple_valid_def2])));
by         (EVERY'[strip_tac, smp_tac 2, Blast_tac] 1); (* conseq *)
by        (ALLGOALS Clarsimp_tac); (* Skip, Ass, Local *)
by     (EVERY'[dtac evaln_evalc, Fast_tac] 1); (* diverg *)
by     (Force_tac 4); (* Call *)
by   (eresolve_tac evaln_elim_cases 2); (* If *)
by    (etac evaln_WHILE_case 4); (* Loop *)
by     (TRYALL Blast_tac);
qed "hoare_sound";


section "completeness";

Open_locale "struct_ind";

val MGT_def = thm "MGT_def";

(*unused*)
Goalw [MGT_def] "G|-MGT c ==> \
\ G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. c .{%Z s1. Z=s1}";
be conseq12 1;
by Auto_tac;
qed "MGT_alternI";

(* requires com_det, single_stateE *)
Goalw [MGT_def] "G|-{%Z s0. !s1. <c,s0> -c-> s1 --> Z=s1}. \
\ c .{%Z s1. Z=s1} ==> G|-MGT c";
be conseq12 1;
by Auto_tac;
by (case_tac "? t. <c,?s> -c-> t" 1);
by  (fast_tac (claset() addEs [com_det]) 1);
by (force_tac  (claset() addSEs [single_stateE],simpset()) 1);
qed "MGT_alternD";

Goalw [MGT_def] 
 "{}|-(MGT c::state triple) ==> {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::state assn}";
be conseq12 1;
by (clarsimp_tac (claset(), simpset() addsimps 
  [hoare_valids_def,eval_eq,triple_valid_def2]) 1);
qed "MGF_complete";

(* requires com_det, single_stateE, escape (i.e. hoare_derivs.conseq) *)
Goal "!pn. G|-{=}.BODY pn.{->} ==> G|-{=}.c.{->}";
by (induct_tac "c" 1);
be        spec 7;
br       MGT_alternD 6;
by       (rewtac MGT_def);
by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
	     [("P1","%Z' s. s=(setlocs Z newlocs)[Loc Arg ::= fun Z]")]
	     (hoare_derivs.Call RS conseq1), dtac spec, etac conseq12] 7);
by        (TRYALL (etac thin_rl));
br        (hoare_derivs.Skip RS conseq2) 1;
br        (hoare_derivs.Ass RS conseq1) 2;
by        (EVERY'[rtac escape, Clarsimp_tac, res_inst_tac 
	          [("P1","%Z' s. s=(Z[Loc loc::=fun Z])")] 
		  (hoare_derivs.Local RS conseq1), etac conseq12] 3);
by         (EVERY'[etac hoare_derivs.Comp, etac conseq12] 5);
by         ((rtac hoare_derivs.If THEN_ALL_NEW etac conseq12) 6);
by          (EVERY'[rtac (hoare_derivs.Loop RS conseq2), etac conseq12] 8);
by           Auto_tac;
qed "MGF_lemma1";

Goal "[| !!G ts. ts <= G ==> P G ts;\
\ !!G pn. P (insert (mgt_call pn) G) {mgt (body pn)} ==> P G {mgt_call pn};\
\         !!G c. !pn:U. P G {mgt_call pn} ==> P G {mgt c}; \
\         finite U; uG = mgt_call``U |] ==> \
\ !G. G <= uG --> n <= card uG --> card G = card uG - n --> (!c. P G {mgt c})";
by (cut_facts_tac (premises()) 1);
by (induct_tac "n" 1);
by  (ALLGOALS Clarsimp_tac);
bd  card_seteq 1;
by    (Asm_simp_tac 1);
be   finite_imageI 1;
by  (Asm_full_simp_tac 1);
by  (resolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
br  ballI 1;
by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
by  (Fast_tac 1);
by (resolve_tac (tl(tl(premises()))(*MGF_lemma1*)) 1);
br ballI 1;
by (case_tac "mgt_call pn : G" 1);
by  (resolve_tac (premises()(*hoare_derivs.asm*)) 1);
by  (Fast_tac 1);
by (resolve_tac (tl(premises())(*MGT_BodyN*)) 1);
byev[dtac spec 1, etac impE 1, etac impE 2, etac impE 3, etac spec 4];
by   (Fast_tac 1);
be  Suc_leD 1;
bd finite_subset 1;
be  finite_imageI 1;
by (force_tac (claset() addEs [Suc_diff_Suc], simpset()) 1);
qed_spec_mp "nesting_lemma";

Goalw [MGT_def] "insert ({=}.BODY pn.{->}) G|-{=}.body pn.{->} ==> G|-{=}.BODY pn.{->}";
br BodyN 1;
be conseq2 1;
by (Force_tac 1);
qed "MGT_BodyN";

(* requires BodyN, com_det, single_stateE *)
Goal "{}|-MGT c";
by (res_inst_tac [("P","%G ts. G||-ts")] nesting_lemma 1);
be        hoare_derivs.asm 1;
be       MGT_BodyN 1;
br      MGF_lemma1 1;
br      finite 2;
br     le_refl 4;
by    Auto_tac;
qed "MGF";

(* finiteness necessary here *)
(* requires empty, insert, com_det, single_stateE *)
Goal "finite F ==> \
\ F <= range (%pn. {=}.body pn.{->}) --> range (%pn. {=}.BODY pn.{->})||-F";
be finite_induct 1;
by  (ALLGOALS (clarsimp_tac (claset() addSIs [hoare_derivs.empty,
					      hoare_derivs.insert],simpset())));
br MGF_lemma1 1;
br allI 1;
br hoare_derivs.asm 1;
by (Fast_tac 1);
qed_spec_mp "MGF_lemma2_simult";

(* finiteness not really necessary here *)
Goalw [MGT_def]     "[| G Un (%pn. {=}. BODY pn .{->})``Procs \
\                         ||-(%pn. {=}. body pn .{->})``Procs; \
\ finite Procs |] ==>   G ||-(%pn. {=}. BODY pn .{->})``Procs";
br hoare_derivs.Body 1;
be finite_pointwise 1;
ba  2;
by (Clarify_tac 1);
be  conseq2 1;
by Auto_tac;
qed "MGT_Body";

(* requires Body, empty, insert, com_det, single_stateE *)
Goal "{}|-MGT c";
br MGF_lemma1 1;
by (subgoal_tac "{}||-range (%pn. {=}. BODY pn .{->})" 1);
br  allI 1;
be  hoare_derivs.weaken 1;
by  (Simp_tac 1);
br MGT_Body 1;
by  (Simp_tac 1);
br  MGF_lemma2_simult 1;
by   (safe_tac (claset() addSIs [finite_imageI, finite]));
qed "MGF";

(* requires Body+empty+insert/BodyN, com_det, single_stateE *)
bind_thm ("hoare_complete", export (MGF RS MGF_complete)); 

Close_locale "struct_ind";


(*Open_locale "rule_ind";*)


Goal "!s0 s1. <c,s0> -c-> s1 --> {}|-{%(Z::'a) s. s=s0}.c.{%Z s'. s'=s1} ==> \
\ {}|={P}.c.{Q} ==> {}|-{P}.c.{Q::'a assn}";
br hoare_derivs.conseq 1;
by (Clarify_tac 1);
by (case_tac "? s'.  <c,s> -c-> s'" 1);
be  exE 1;
by  (ftac (eval_eq RS iffD1) 1);
be  exE 1;
by  (smp_tac 2 1);
by  (EVERY'[rtac exI, rtac exI, etac conjI] 1);
by  (full_simp_tac (simpset() addsimps [hoare_valids_def,triple_valid_def2]) 1);
by  (smp_tac 3 1);
by  (Blast_tac 1);
br exI 1;
br exI 1;
br conjI 1;
by (res_inst_tac [("Q","%Z s. False")] hoare_derivs.diverg 1);
by (Asm_simp_tac 1);
qed "MGF2_complete";

Goal "G|-{%Z s'. s'=s & C s'}.c.{Q} = (C s --> G|-{%Z s'. s'=s}.c.{Q})";
by (subgoal_tac "!s'. (s'=s & C s') = (s'=s & C s)" 1);
by  (auto_tac (claset() addSIs [constant], simpset()));
qed "const_eq";

(* requires conseq, LoopT, weak_Body *)
Goal "!s0a s1a. <c,s0a> -c-> s1a --> {}|-{%Z s. s = s0a}.c.{%Z s'. s' = s1a}";
by (strip_tac 1);
be evalc.induct 1;
by          (rtac hoare_derivs.Skip 1);
by         (EVERY'[rtac (hoare_derivs.Ass RS conseq1), Fast_tac] 1);
by        (EVERY'[res_inst_tac [("P1","%Z s. s=s0[Loc X::=a s0]"),
	   ("Q'","?Q")] (hoare_derivs.Local RS conseq12),
		 etac conseq12, Force_tac, Clarsimp_tac] 1);
by       (EVERY'[etac hoare_derivs.Comp, Fast_tac] 1);
by      (TRYALL (rtac hoare_derivs.If THEN_ALL_NEW 
	(Full_simp_tac THEN' fast_tac (claset() addSIs [const_eq RS iffD2]))));
by    (EVERY'[rtac (LoopF RS conseq1), Fast_tac] 1);
by   (EVERY'[rtac (hoare_derivs.LoopT RS conseq1), 
	etac conseq1, Clarsimp_tac, atac, 
        atac, Clarsimp_tac] 1);
be  weak_Body 1;
by (EVERY'[res_inst_tac [("P1",
	"%Z s. s=(setlocs s0 newlocs[Loc Arg::=a s0])"),
	   ("Q'","?Q")] (hoare_derivs.Call RS conseq12), 
		 etac conseq12, Force_tac, Clarsimp_tac] 1);
qed "MGF2";

(* requires conseq, LoopT, weak_Body *)
bind_thm ("hoare_complete", export (MGF2 RS MGF2_complete));

(*Close_locale ();*)


Goal "{}|-{P}.c.{Q} = {}|={P}.c.{Q}";
by (fast_tac (claset() addEs [hoare_sound, hoare_complete]) 1);
qed "hoare_eq";


section "unused derived rules";

Goal "G|-{%Z s. False}.c.{Q}";
br hoare_derivs.conseq 1;
by (Fast_tac 1);
qed "falseE";

Goal "G|-{P}.c.{%Z s. True}";
br hoare_derivs.conseq 1;
by (fast_tac (claset() addSIs [falseE]) 1);
qed "trueI";

Goal "[| G|-{P}.c.{Q}; G|-{P'}.c.{Q'} |] \
\       ==> G|-{%Z s. P Z s | P' Z s}.c.{%Z s. Q Z s | Q' Z s}";
br hoare_derivs.conseq 1;
by (fast_tac (claset() addEs [conseq12]) 1);
qed "disj";(*conj non-derivable*)

Goal "(!Z s. P Z s --> Q Z s) ==> G|-{P}. SKIP .{Q}";
br conseq12 1;
br  hoare_derivs.Skip 1;
by (Fast_tac 1);
qed "hoare_SkipI";


section "useful derived rules";

Goal "{t}|-t";
br hoare_derivs.asm 1;
br subset_refl 1;
qed "single_asm";

Goal "[| !!s'. G|-{%Z s. s'=s & P Z s}.c.{Q} |] ==> G|-{P}.c.{Q}";
br hoare_derivs.conseq 1;
by (Clarsimp_tac 1);
by (cut_facts_tac (premises()) 1);
by (Fast_tac 1);
qed "export_s";

Goalw [getlocs_def] "getlocs (st g l) = l";
by (Simp_tac 1);
qed "getlocs_def2";

Goalw [update_def] "s[Loc X::=s<X>] = s";
by (induct_tac "s" 1);
by (simp_tac (simpset() addsimps [getlocs_def2]) 1);
br ext 1;
by (Simp_tac 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 X::=k])<Y> = (if X=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];

(*unused*)
Goalw [hoare_valids_def] 
"!v. G|={%Z s. P Z (s[Loc X::=v]) & s<X> = a (s[Loc X::=v])}. \
\ c .{%Z s. Q Z (s[Loc X::=v])} ==> G|={P}. LOCAL X:=a IN c .{Q}";
by (full_simp_tac (simpset() addsimps [triple_valid_def2]) 1);
by (Clarsimp_tac 1);
by (dres_inst_tac [("x","s<X>")] spec 1);
by (smp_tac 1 1);
bd spec 1;
by (dres_inst_tac [("x","s[Loc X::=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 X::=v]) & s<X> = a (s[Loc X::=v])}. \
\ c .{%Z s. Q Z (s[Loc X::=v])} ==> G|-{P}. LOCAL X:=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 \<and> P Z (s[Loc X::=a s][Loc X::=s'<X>]) \<and> (s[Loc X::=a s])<X> = a (s[Loc X::=a s][Loc X::=s'<X>])")] conseq1 1);
by  (Clarsimp_tac 2);
br hoare_derivs.Local 1;
be spec 1;
*)
qed "classic_Local";

Goal "[| G|-{P}. c .{Q}; !k Z s. Q Z s --> Q Z (s[Loc X::=k]) |] ==> \
\   G|-{%Z s. P Z (s[Loc X::=a s])}. LOCAL X:=a IN c .{Q}";
br export_s 1;
br hoare_derivs.Local 1;
be conseq2 1;
be spec 1;
qed "weak_Local";


Goalw [update_def] "getlocs (s[Glb X::=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')[X::=k]) = getlocs (s'[X::=k])";
by (induct_tac "X" 1);
br ext 2;
by Auto_tac;
qed "getlocs_setlocs_lemma";

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