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