1465
|
1 |
(* Title: HOL/Hoare/Hoare.ML
|
1335
|
2 |
ID: $Id$
|
1465
|
3 |
Author: Norbert Galm & Tobias Nipkow
|
1335
|
4 |
Copyright 1995 TUM
|
|
5 |
|
|
6 |
The verification condition generation tactics.
|
|
7 |
*)
|
|
8 |
|
|
9 |
open Hoare;
|
|
10 |
|
|
11 |
(*** Hoare rules ***)
|
|
12 |
|
1558
|
13 |
val SkipRule = prove_goalw thy [Spec_def,Skip_def]
|
1335
|
14 |
"(!!s.p(s) ==> q(s)) ==> Spec p Skip q"
|
1875
|
15 |
(fn prems => [fast_tac (!claset addIs prems) 1]);
|
1335
|
16 |
|
1558
|
17 |
val AssignRule = prove_goalw thy [Spec_def,Assign_def]
|
1335
|
18 |
"(!!s. p s ==> q(%x.if x=v then e s else s x)) ==> Spec p (Assign v e) q"
|
1875
|
19 |
(fn prems => [fast_tac (!claset addIs prems) 1]);
|
1335
|
20 |
|
1558
|
21 |
val SeqRule = prove_goalw thy [Spec_def,Seq_def]
|
1335
|
22 |
"[| Spec p c (%s.q s); Spec (%s.q s) c' r |] ==> Spec p (Seq c c') r"
|
1875
|
23 |
(fn prems => [cut_facts_tac prems 1, Fast_tac 1]);
|
1335
|
24 |
|
1558
|
25 |
val IfRule = prove_goalw thy [Spec_def,Cond_def]
|
1335
|
26 |
"[| !!s. p s ==> (b s --> q s) & (~b s --> q' s); \
|
|
27 |
\ Spec (%s.q s) c r; Spec (%s.q' s) c' r |] \
|
|
28 |
\ ==> Spec p (Cond b c c') r"
|
|
29 |
(fn [prem1,prem2,prem3] =>
|
|
30 |
[REPEAT (rtac allI 1),
|
|
31 |
REPEAT (rtac impI 1),
|
1465
|
32 |
dtac prem1 1,
|
1335
|
33 |
cut_facts_tac [prem2,prem3] 1,
|
1875
|
34 |
fast_tac (!claset addIs [prem1]) 1]);
|
1335
|
35 |
|
1558
|
36 |
val strenthen_pre = prove_goalw thy [Spec_def]
|
1335
|
37 |
"[| !!s. p s ==> p' s; Spec p' c q |] ==> Spec p c q"
|
|
38 |
(fn [prem1,prem2] =>[cut_facts_tac [prem2] 1,
|
1875
|
39 |
fast_tac (!claset addIs [prem1]) 1]);
|
1335
|
40 |
|
1558
|
41 |
val [iter_0,iter_Suc] = nat_recs Iter_def;
|
1335
|
42 |
|
1558
|
43 |
val lemma = prove_goalw thy [Spec_def,While_def]
|
1335
|
44 |
"[| Spec (%s.inv s & b s) c inv; !!s. [| inv s; ~b s |] ==> q s |] \
|
|
45 |
\ ==> Spec inv (While b inv c) q"
|
|
46 |
(fn [prem1,prem2] =>
|
|
47 |
[REPEAT(rtac allI 1), rtac impI 1, etac exE 1, rtac mp 1, atac 2,
|
|
48 |
etac thin_rl 1, res_inst_tac[("x","s")]spec 1,
|
|
49 |
res_inst_tac[("x","s'")]spec 1, nat_ind_tac "n" 1,
|
|
50 |
simp_tac (!simpset addsimps [iter_0]) 1,
|
1875
|
51 |
fast_tac (!claset addIs [prem2]) 1,
|
1558
|
52 |
simp_tac (!simpset addsimps [iter_Suc,Seq_def]) 1,
|
1875
|
53 |
cut_facts_tac [prem1] 1, fast_tac (!claset addIs [prem2]) 1]);
|
1335
|
54 |
|
|
55 |
val WhileRule = lemma RSN (2,strenthen_pre);
|
|
56 |
|
|
57 |
|
|
58 |
(*** meta_spec used in StateElimTac ***)
|
|
59 |
|
|
60 |
val meta_spec = prove_goal HOL.thy
|
|
61 |
"(!!s x. PROP P s x) ==> (!!s. PROP P s (x s))"
|
|
62 |
(fn prems => [resolve_tac prems 1]);
|
|
63 |
|
|
64 |
|
|
65 |
(**************************************************************************************************)
|
|
66 |
(*** Funktion zum Generieren eines Theorems durch Umbennenen von Namen von Lambda-Abstraktionen ***)
|
|
67 |
(*** in einem bestehenden Theorem. Bsp.: "!a.?P(a) ==> ?P(?x)" aus "!x.?P(x) ==> ?P(?x)" ***)
|
|
68 |
(**************************************************************************************************)
|
|
69 |
|
|
70 |
(* rename_abs:term (von:string,nach:string,trm:term) benennt in trm alle Lambda-Abstraktionen
|
|
71 |
mit Namen von in nach um *)
|
|
72 |
|
1465
|
73 |
fun rename_abs (von,nach,Abs (s,t,trm)) =if von=s
|
|
74 |
then Abs (nach,t,rename_abs (von,nach,trm))
|
|
75 |
else Abs (s,t,rename_abs (von,nach,trm))
|
|
76 |
| rename_abs (von,nach,trm1 $ trm2) =rename_abs (von,nach,trm1) $ rename_abs (von,nach,trm2)
|
|
77 |
| rename_abs (_,_,trm) =trm;
|
1335
|
78 |
|
|
79 |
(* ren_abs_thm:thm (von:string,nach:string,theorem:thm) benennt in theorem alle Lambda-Abstraktionen
|
|
80 |
mit Namen von in nach um. Vorgehen:
|
1465
|
81 |
- Term t zu thoerem bestimmen
|
|
82 |
- Term t' zu t durch Umbenennen der Namen generieren
|
|
83 |
- Certified Term ct' zu t' erstellen
|
|
84 |
- Thoerem ct'==ct' anlegen
|
|
85 |
- Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct'
|
|
86 |
abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *)
|
1335
|
87 |
|
1465
|
88 |
fun ren_abs_thm (von,nach,theorem) =
|
|
89 |
equal_elim
|
|
90 |
(
|
|
91 |
reflexive (
|
|
92 |
cterm_of
|
|
93 |
(#sign (rep_thm theorem))
|
|
94 |
(rename_abs (von,nach,#prop (rep_thm theorem)))
|
|
95 |
)
|
|
96 |
)
|
|
97 |
theorem;
|
1335
|
98 |
|
|
99 |
|
|
100 |
(**************************************************************************************************)
|
|
101 |
(*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***)
|
|
102 |
(*** - Umbenennen von Lambda-Abstraktionen im Theorem ***)
|
|
103 |
(*** - Instanziieren von freien Variablen im Theorem ***)
|
|
104 |
(*** - Composing des Subgoals mit dem Theorem ***)
|
|
105 |
(**************************************************************************************************)
|
|
106 |
|
|
107 |
(* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden
|
|
108 |
- insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *)
|
|
109 |
|
1465
|
110 |
fun comp_inst_ren_tac rens insts theorem i =
|
|
111 |
let
|
|
112 |
fun compose_inst_ren_tac [] insts theorem i =
|
|
113 |
compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i
|
|
114 |
| compose_inst_ren_tac ((von,nach)::rl) insts theorem i =
|
|
115 |
compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i
|
|
116 |
in
|
|
117 |
compose_inst_ren_tac rens insts theorem i
|
|
118 |
end;
|
1335
|
119 |
|
|
120 |
|
|
121 |
(**************************************************************************************************)
|
|
122 |
(*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen ***)
|
|
123 |
(*** Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1" ***)
|
|
124 |
(**************************************************************************************************)
|
|
125 |
|
|
126 |
(* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen
|
|
127 |
aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an.
|
1465
|
128 |
Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a")
|
|
129 |
wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *)
|
1335
|
130 |
|
1465
|
131 |
fun pvars_of_term (name,trm) =
|
|
132 |
let
|
|
133 |
fun add_vars (name,Free (s,t) $ trm,vl) =if name=s
|
|
134 |
then if trm mem vl
|
|
135 |
then vl
|
|
136 |
else trm::vl
|
|
137 |
else add_vars (name,trm,vl)
|
|
138 |
| add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl)
|
|
139 |
| add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl))
|
|
140 |
| add_vars (_,_,vl) =vl
|
|
141 |
in
|
|
142 |
add_vars (name,trm,[])
|
|
143 |
end;
|
1335
|
144 |
|
|
145 |
(* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i
|
1465
|
146 |
- v::vl:(term) list Liste der zu eliminierenden Programmvariablen
|
|
147 |
- meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird
|
|
148 |
z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
|
|
149 |
- namexAll:string Name von ^ (hier "x")
|
|
150 |
- varx:term Term zu ^ (hier Var(("x",0),...))
|
|
151 |
- varP:term Term zu ^ (hier Var(("P",0),...))
|
|
152 |
- type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...)
|
1335
|
153 |
|
|
154 |
Vorgehen:
|
1465
|
155 |
- eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu:
|
|
156 |
- Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt
|
|
157 |
z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich
|
|
158 |
meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))"
|
|
159 |
- Instanziierungen in meta_spec:
|
|
160 |
varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert
|
|
161 |
varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a":
|
|
162 |
- zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.":
|
|
163 |
trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable)
|
|
164 |
- substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs:
|
|
165 |
trm1 = "s(Suc(0)) = xs ==> xs = 1"
|
|
166 |
- abstrahiere ueber xs:
|
|
167 |
trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1"
|
|
168 |
- abstrahiere ueber restliche Vorkommen von s:
|
|
169 |
trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1"
|
|
170 |
- instanziiere varP mit trm3
|
1335
|
171 |
*)
|
|
172 |
|
1465
|
173 |
fun VarsElimTac ([],_,_,_,_,_) i =all_tac
|
|
174 |
| VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i =
|
|
175 |
STATE (
|
|
176 |
fn state =>
|
|
177 |
comp_inst_ren_tac
|
|
178 |
[(namexAll,pvar2pvarID v)]
|
|
179 |
[(
|
|
180 |
cterm_of (#sign (rep_thm state)) varx,
|
|
181 |
cterm_of (#sign (rep_thm state)) (
|
|
182 |
Abs ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v)
|
|
183 |
)
|
|
184 |
),(
|
|
185 |
cterm_of (#sign (rep_thm state)) varP,
|
|
186 |
cterm_of (#sign (rep_thm state)) (
|
|
187 |
let
|
|
188 |
val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i);
|
|
189 |
val (sname,trm0) = variant_abs ("s",dummyT,trm);
|
|
190 |
val xsname = variant_name ("xs",trm0);
|
|
191 |
val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0)
|
|
192 |
val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1))
|
|
193 |
in
|
|
194 |
Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2))
|
|
195 |
end
|
|
196 |
)
|
|
197 |
)]
|
|
198 |
meta_spec i
|
|
199 |
)
|
|
200 |
THEN
|
|
201 |
(VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i);
|
1335
|
202 |
|
|
203 |
(* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i
|
|
204 |
|
|
205 |
zur Erinnerung:
|
1465
|
206 |
- das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)",
|
|
207 |
d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_)
|
1335
|
208 |
- meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))"
|
|
209 |
*)
|
|
210 |
|
1465
|
211 |
fun StateElimTac i =
|
|
212 |
STATE (
|
|
213 |
fn state =>
|
|
214 |
let
|
|
215 |
val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i);
|
|
216 |
val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $
|
|
217 |
(_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec)
|
|
218 |
in
|
|
219 |
VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i
|
|
220 |
end
|
|
221 |
);
|
1335
|
222 |
|
|
223 |
|
|
224 |
|
|
225 |
(*** tactics for verification condition generation ***)
|
|
226 |
|
|
227 |
(* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall
|
|
228 |
von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann
|
|
229 |
generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen
|
|
230 |
Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *)
|
|
231 |
|
|
232 |
fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false)
|
|
233 |
and HoareRuleTac i pre_cond =
|
|
234 |
STATE(fn state =>
|
1465
|
235 |
((WlpTac i) THEN (HoareRuleTac i pre_cond))
|
1335
|
236 |
ORELSE
|
1465
|
237 |
(FIRST[rtac SkipRule i,
|
|
238 |
rtac AssignRule i,
|
|
239 |
EVERY[rtac IfRule i,
|
1335
|
240 |
HoareRuleTac (i+2) false,
|
|
241 |
HoareRuleTac (i+1) false],
|
1465
|
242 |
EVERY[rtac WhileRule i,
|
1335
|
243 |
Asm_full_simp_tac (i+2),
|
|
244 |
HoareRuleTac (i+1) true]]
|
1465
|
245 |
THEN
|
1335
|
246 |
(if pre_cond then (Asm_full_simp_tac i) else (atac i))
|
1465
|
247 |
)
|
|
248 |
);
|
1335
|
249 |
|
|
250 |
val HoareTac1 =
|
|
251 |
EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac];
|
|
252 |
|
|
253 |
val hoare_tac = SELECT_GOAL (HoareTac1);
|
|
254 |
|