diff -r c2860c37e574 -r aa2581752afb src/HOL/IMPP/Misc.thy
--- a/src/HOL/IMPP/Misc.thy	Wed Jun 07 01:06:53 2006 +0200
+++ b/src/HOL/IMPP/Misc.thy	Wed Jun 07 01:51:22 2006 +0200
@@ -18,6 +18,134 @@
                                Glb gn => (case s of st g l => st (g(gn:=v)) l)
                              | Loc ln => (case s of st g l => st g (l(ln:=v)))"
 
-ML {* use_legacy_bindings (the_context ()) *}
+
+subsection "state access"
+
+lemma getlocs_def2: "getlocs (st g l) = l"
+apply (unfold getlocs_def)
+apply simp
+done
+
+lemma update_Loc_idem2 [simp]: "s[Loc Y::=s<Y>] = s"
+apply (unfold update_def)
+apply (induct_tac s)
+apply (simp add: getlocs_def2)
+done
+
+lemma update_overwrt [simp]: "s[X::=x][X::=y] = s[X::=y]"
+apply (unfold update_def)
+apply (induct_tac X)
+apply  auto
+apply  (induct_tac [!] s)
+apply  auto
+done
+
+lemma getlocs_Loc_update [simp]: "(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)"
+apply (unfold update_def)
+apply (induct_tac s)
+apply (simp add: getlocs_def2)
+done
+
+lemma getlocs_Glb_update [simp]: "getlocs (s[Glb Y::=k]) = getlocs s"
+apply (unfold update_def)
+apply (induct_tac s)
+apply (simp add: getlocs_def2)
+done
+
+lemma getlocs_setlocs [simp]: "getlocs (setlocs s l) = l"
+apply (unfold setlocs_def)
+apply (induct_tac s)
+apply auto
+apply (simp add: getlocs_def2)
+done
+
+lemma getlocs_setlocs_lemma: "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])"
+apply (induct_tac Y)
+apply (rule_tac [2] ext)
+apply auto
+done
+
+(*unused*)
+lemma classic_Local_valid: 
+"!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}"
+apply (unfold hoare_valids_def)
+apply (simp (no_asm_use) add: triple_valid_def2)
+apply clarsimp
+apply (drule_tac x = "s<Y>" in spec)
+apply (tactic "smp_tac 1 1")
+apply (drule spec)
+apply (drule_tac x = "s[Loc Y::=a s]" in spec)
+apply (simp (no_asm_use))
+apply (erule (1) notE impE)
+apply (tactic "smp_tac 1 1")
+apply simp
+done
+
+lemma classic_Local: "!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}"
+apply (rule export_s)
+(*variant 1*)
+apply (rule hoare_derivs.Local [THEN conseq1])
+apply (erule spec)
+apply force
+(*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);
+*)
+done
+
+lemma classic_Local_indep: "[| 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}"
+apply (rule classic_Local)
+apply clarsimp
+apply (erule conseq12)
+apply clarsimp
+apply (drule sym)
+apply simp
+done
+
+lemma Local_indep: "[| 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}"
+apply (rule export_s)
+apply (rule hoare_derivs.Local)
+apply clarsimp
+done
+
+lemma weak_Local_indep: "[| 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}"
+apply (rule weak_Local)
+apply auto
+done
+
+
+lemma export_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
+apply (rule export_s)
+apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s'<Y> = s<Y>" in conseq12)
+prefer 2
+apply  clarsimp
+apply (rule hoare_derivs.Local)
+apply clarsimp
+apply (rule trueI)
+done
+
+lemma classic_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}"
+apply (rule classic_Local)
+apply clarsimp
+apply (rule trueI [THEN conseq12])
+apply clarsimp
+done
+
+lemma Call_invariant: "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}"
+apply (rule_tac s'1 = "s'" and
+  Q' = "%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s" in
+  hoare_derivs.Call [THEN conseq12])
+apply  (simp (no_asm_simp) add: getlocs_setlocs_lemma)
+apply force
+done
 
 end