author | wenzelm |
Thu, 26 May 2016 17:51:22 +0200 | |
changeset 63167 | 0909deb8059b |
parent 62145 | 5b946c81dfbf |
child 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
8177 | 1 |
(* Title: HOL/IMPP/Misc.thy |
41589 | 2 |
Author: David von Oheimb, TUM |
17477 | 3 |
*) |
8177 | 4 |
|
63167 | 5 |
section \<open>Several examples for Hoare logic\<close> |
17477 | 6 |
|
7 |
theory Misc |
|
8 |
imports Hoare |
|
9 |
begin |
|
8177 | 10 |
|
62145 | 11 |
overloading |
12 |
newlocs \<equiv> newlocs |
|
13 |
setlocs \<equiv> setlocs |
|
14 |
getlocs \<equiv> getlocs |
|
15 |
update \<equiv> update |
|
16 |
begin |
|
17 |
||
18 |
definition newlocs :: locals |
|
19 |
where "newlocs == %x. undefined" |
|
20 |
||
21 |
definition setlocs :: "state => locals => state" |
|
22 |
where "setlocs s l' == case s of st g l => st g l'" |
|
23 |
||
24 |
definition getlocs :: "state => locals" |
|
25 |
where "getlocs s == case s of st g l => l" |
|
26 |
||
27 |
definition 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 |
||
33 |
end |
|
17477 | 34 |
|
19803 | 35 |
|
36 |
subsection "state access" |
|
37 |
||
38 |
lemma getlocs_def2: "getlocs (st g l) = l" |
|
39 |
apply (unfold getlocs_def) |
|
40 |
apply simp |
|
41 |
done |
|
42 |
||
43 |
lemma update_Loc_idem2 [simp]: "s[Loc Y::=s<Y>] = s" |
|
44 |
apply (unfold update_def) |
|
45 |
apply (induct_tac s) |
|
46 |
apply (simp add: getlocs_def2) |
|
47 |
done |
|
48 |
||
49 |
lemma update_overwrt [simp]: "s[X::=x][X::=y] = s[X::=y]" |
|
50 |
apply (unfold update_def) |
|
51 |
apply (induct_tac X) |
|
52 |
apply auto |
|
53 |
apply (induct_tac [!] s) |
|
54 |
apply auto |
|
55 |
done |
|
56 |
||
57 |
lemma getlocs_Loc_update [simp]: "(s[Loc Y::=k])<Y'> = (if Y=Y' then k else s<Y'>)" |
|
58 |
apply (unfold update_def) |
|
59 |
apply (induct_tac s) |
|
60 |
apply (simp add: getlocs_def2) |
|
61 |
done |
|
62 |
||
63 |
lemma getlocs_Glb_update [simp]: "getlocs (s[Glb Y::=k]) = getlocs s" |
|
64 |
apply (unfold update_def) |
|
65 |
apply (induct_tac s) |
|
66 |
apply (simp add: getlocs_def2) |
|
67 |
done |
|
68 |
||
69 |
lemma getlocs_setlocs [simp]: "getlocs (setlocs s l) = l" |
|
70 |
apply (unfold setlocs_def) |
|
71 |
apply (induct_tac s) |
|
72 |
apply auto |
|
73 |
apply (simp add: getlocs_def2) |
|
74 |
done |
|
75 |
||
76 |
lemma getlocs_setlocs_lemma: "getlocs (setlocs s (getlocs s')[Y::=k]) = getlocs (s'[Y::=k])" |
|
77 |
apply (induct_tac Y) |
|
78 |
apply (rule_tac [2] ext) |
|
79 |
apply auto |
|
80 |
done |
|
81 |
||
82 |
(*unused*) |
|
83 |
lemma classic_Local_valid: |
|
84 |
"!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}" |
|
86 |
apply (unfold hoare_valids_def) |
|
87 |
apply (simp (no_asm_use) add: triple_valid_def2) |
|
88 |
apply clarsimp |
|
89 |
apply (drule_tac x = "s<Y>" in spec) |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
90 |
apply (tactic "smp_tac @{context} 1 1") |
19803 | 91 |
apply (drule spec) |
92 |
apply (drule_tac x = "s[Loc Y::=a s]" in spec) |
|
93 |
apply (simp (no_asm_use)) |
|
94 |
apply (erule (1) notE impE) |
|
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
95 |
apply (tactic "smp_tac @{context} 1 1") |
19803 | 96 |
apply simp |
97 |
done |
|
98 |
||
99 |
lemma classic_Local: "!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}" |
|
101 |
apply (rule export_s) |
|
102 |
apply (rule hoare_derivs.Local [THEN conseq1]) |
|
103 |
apply (erule spec) |
|
104 |
apply force |
|
105 |
done |
|
106 |
||
107 |
lemma 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}" |
|
109 |
apply (rule classic_Local) |
|
110 |
apply clarsimp |
|
111 |
apply (erule conseq12) |
|
112 |
apply clarsimp |
|
113 |
apply (drule sym) |
|
114 |
apply simp |
|
115 |
done |
|
116 |
||
117 |
lemma 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}" |
|
119 |
apply (rule export_s) |
|
120 |
apply (rule hoare_derivs.Local) |
|
121 |
apply clarsimp |
|
122 |
done |
|
123 |
||
124 |
lemma 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}" |
|
126 |
apply (rule weak_Local) |
|
127 |
apply auto |
|
128 |
done |
|
129 |
||
130 |
||
131 |
lemma export_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}" |
|
132 |
apply (rule export_s) |
|
133 |
apply (rule_tac P' = "%Z s. s'=s & True" and Q' = "%Z s. s'<Y> = s<Y>" in conseq12) |
|
134 |
prefer 2 |
|
135 |
apply clarsimp |
|
136 |
apply (rule hoare_derivs.Local) |
|
137 |
apply clarsimp |
|
138 |
apply (rule trueI) |
|
139 |
done |
|
140 |
||
141 |
lemma classic_Local_invariant: "G|-{%Z s. Z = s<Y>}. LOCAL Y:=a IN c .{%Z s. Z = s<Y>}" |
|
142 |
apply (rule classic_Local) |
|
143 |
apply clarsimp |
|
144 |
apply (rule trueI [THEN conseq12]) |
|
145 |
apply clarsimp |
|
146 |
done |
|
147 |
||
148 |
lemma 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}" |
|
151 |
apply (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]) |
|
154 |
apply (simp (no_asm_simp) add: getlocs_setlocs_lemma) |
|
155 |
apply force |
|
156 |
done |
|
8177 | 157 |
|
158 |
end |