1(* Title: HOL/IMPP/Misc.thy 2 Author: David von Oheimb, TUM 3*) 4 5section \<open>Several examples for Hoare logic\<close> 6 7theory Misc 8imports Hoare 9begin 10 11overloading 12 newlocs \<equiv> newlocs 13 setlocs \<equiv> setlocs 14 getlocs \<equiv> getlocs 15 update \<equiv> update 16begin 17 18definition newlocs :: locals 19 where "newlocs == %x. undefined" 20 21definition setlocs :: "state => locals => state" 22 where "setlocs s l' == case s of st g l => st g l'" 23 24definition getlocs :: "state => locals" 25 where "getlocs s == case s of st g l => l" 26 27definition update :: "state => vname => val => state" 28 where "update s vn v == 29 case vn of 30 Glb gn => (case s of st g l => st (g(gn:=v)) l) 31 | Loc ln => (case s of st g l => st g (l(ln:=v)))" 32 33end 34 35 36subsection "state access" 37 38lemma getlocs_def2: "getlocs (st g l) = l" 39apply (unfold getlocs_def) 40apply simp 41done 42 43lemma update_Loc_idem2 [simp]: "s[Loc Y::=s<Y>] = s" 44apply (unfold update_def) 45apply (induct_tac s) 46apply (simp add: getlocs_def2) 47done 48 49lemma update_overwrt [simp]: "s[X::=x][X::=y] = s[X::=y]" 50apply (unfold update_def) 51apply (induct_tac X) 52apply auto 53apply (induct_tac [!] s) 54apply auto 55done 56 57lemma getlocs_Loc_update [simp]: "(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)" 58apply (unfold update_def) 59apply (induct_tac s) 60apply (simp add: getlocs_def2) 61done 62 63lemma getlocs_Glb_update [simp]: "getlocs (s[Glb Y::=k]) = getlocs s" 64apply (unfold update_def) 65apply (induct_tac s) 66apply (simp add: getlocs_def2) 67done 68 69lemma getlocs_setlocs [simp]: "getlocs (setlocs s l) = l" 70apply (unfold setlocs_def) 71apply (induct_tac s) 72apply auto 73apply (simp add: getlocs_def2) 74done 75 76lemma getlocs_setlocs_lemma: "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])" 77apply (induct_tac Y) 78apply (rule_tac [2] ext) 79apply auto 80done 81 82(*unused*) 83lemma classic_Local_valid: 84"\<forall>v. G|={%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. 85 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|={P}. LOCAL Y:=a IN c .{Q}" 86apply (unfold hoare_valids_def) 87apply (simp (no_asm_use) add: triple_valid_def2) 88apply clarsimp 89apply (drule_tac x = "s<Y>" in spec) 90apply (tactic "smp_tac \<^context> 1 1") 91apply (drule spec) 92apply (drule_tac x = "s[Loc Y::=a s]" in spec) 93apply (simp (no_asm_use)) 94apply (erule (1) notE impE) 95apply (tactic "smp_tac \<^context> 1 1") 96apply simp 97done 98 99lemma classic_Local: "\<forall>v. G|-{%Z s. P Z (s[Loc Y::=v]) & s<Y> = a (s[Loc Y::=v])}. 100 c .{%Z s. Q Z (s[Loc Y::=v])} ==> G|-{P}. LOCAL Y:=a IN c .{Q}" 101apply (rule export_s) 102apply (rule hoare_derivs.Local [THEN conseq1]) 103apply (erule spec) 104apply force 105done 106 107lemma classic_Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> 108 G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}" 109apply (rule classic_Local) 110apply clarsimp 111apply (erule conseq12) 112apply clarsimp 113apply (drule sym) 114apply simp 115done 116 117lemma Local_indep: "[| Y~=Y'; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> 118 G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}" 119apply (rule export_s) 120apply (rule hoare_derivs.Local) 121apply clarsimp 122done 123 124lemma weak_Local_indep: "[| Y'~=Y; G|-{P}. c .{%Z s. s<Y'> = d} |] ==> 125 G|-{%Z s. P Z (s[Loc Y::=a s])}. LOCAL Y:=a IN c .{%Z s. s<Y'> = d}" 126apply (rule weak_Local) 127apply auto 128done 129 130 131lemma export_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}" 132apply (rule export_s) 133apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s'<Y> = s<Y>" in conseq12) 134prefer 2 135apply clarsimp 136apply (rule hoare_derivs.Local) 137apply clarsimp 138apply (rule trueI) 139done 140 141lemma classic_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}" 142apply (rule classic_Local) 143apply clarsimp 144apply (rule trueI [THEN conseq12]) 145apply clarsimp 146done 147 148lemma Call_invariant: "G|-{P}. BODY pn .{%Z s. Q Z (setlocs s (getlocs s')[X::=s<Res>])} ==> 149 G|-{%Z s. s'=s & I Z (getlocs (s[X::=k Z])) & P Z (setlocs s newlocs[Loc Arg::=a s])}. 150 X:=CALL pn (a) .{%Z s. I Z (getlocs (s[X::=k Z])) & Q Z s}" 151apply (rule_tac s'1 = "s'" and 152 Q' = "%Z s. I Z (getlocs (s[X::=k Z])) = I Z (getlocs (s'[X::=k Z])) & Q Z s" in 153 hoare_derivs.Call [THEN conseq12]) 154apply (simp (no_asm_simp) add: getlocs_setlocs_lemma) 155apply force 156done 157 158end 159