83 - Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct' |
84 - Nach der Regel "[|P==Q; P|] ==> Q" wird aus "ct'==ct'" und theorem das Theorem zu ct' |
84 abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *) |
85 abgeleitet (ist moeglich, da t' mit t unifiziert werden kann, da nur Umnbenennungen) *) |
85 |
86 |
86 fun ren_abs_thm (von,nach,theorem) = |
87 fun ren_abs_thm (von,nach,theorem) = |
87 equal_elim |
88 equal_elim |
88 ( |
89 (reflexive (cterm_of (#sign (rep_thm theorem)) |
89 reflexive ( |
90 (rename_abs (von,nach,#prop (rep_thm theorem))))) |
90 cterm_of |
|
91 (#sign (rep_thm theorem)) |
|
92 (rename_abs (von,nach,#prop (rep_thm theorem))) |
|
93 ) |
|
94 ) |
|
95 theorem; |
91 theorem; |
96 |
92 |
97 |
93 |
98 (**************************************************************************************************) |
94 (****************************************************************************) |
99 (*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***) |
95 (*** Taktik zum Anwenden eines Theorems theorem auf ein Subgoal i durch ***) |
100 (*** - Umbenennen von Lambda-Abstraktionen im Theorem ***) |
96 (*** - Umbenennen von Lambda-Abstraktionen im Theorem ***) |
101 (*** - Instanziieren von freien Variablen im Theorem ***) |
97 (*** - Instanziieren von freien Variablen im Theorem ***) |
102 (*** - Composing des Subgoals mit dem Theorem ***) |
98 (*** - Composing des Subgoals mit dem Theorem ***) |
103 (**************************************************************************************************) |
99 (****************************************************************************) |
104 |
100 |
105 (* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden |
101 (* - rens:(string*string) list, d.h. es koennen verschiedene Lambda-Abstraktionen umbenannt werden |
106 - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *) |
102 - insts:(cterm*cterm) list, d.h. es koennen verschiedene Variablen instanziiert werden *) |
107 |
103 |
108 fun comp_inst_ren_tac rens insts theorem i = |
104 fun comp_inst_ren_tac rens insts theorem i = |
109 let |
105 let fun compose_inst_ren_tac [] insts theorem i = |
110 fun compose_inst_ren_tac [] insts theorem i = |
106 compose_tac (false, |
111 compose_tac (false,cterm_instantiate insts theorem,nprems_of theorem) i |
107 cterm_instantiate insts theorem,nprems_of theorem) i |
112 | compose_inst_ren_tac ((von,nach)::rl) insts theorem i = |
108 | compose_inst_ren_tac ((von,nach)::rl) insts theorem i = |
113 compose_inst_ren_tac rl insts (ren_abs_thm (von,nach,theorem)) i |
109 compose_inst_ren_tac rl insts |
114 in |
110 (ren_abs_thm (von,nach,theorem)) i |
115 compose_inst_ren_tac rens insts theorem i |
111 in compose_inst_ren_tac rens insts theorem i end; |
116 end; |
112 |
117 |
113 |
118 |
114 (*************************************************************** *********) |
119 (**************************************************************************************************) |
|
120 (*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen ***) |
115 (*** Taktik zum Eliminieren des Zustandes waehrend Hoare-Beweisen ***) |
121 (*** Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1" ***) |
116 (*** Bsp.: "!!s. s(Suc(0))=0 --> s(Suc(0))+1=1" wird zu "!!s b. b=0 --> b+1=1" ***) |
122 (**************************************************************************************************) |
117 (****************************************************************************) |
123 |
118 |
124 (* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen |
119 (* pvars_of_term:term list (name:string,trm:term) gibt die Liste aller Programm-Variablen |
125 aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an. |
120 aus trm zurueck. name gibt dabei den Namen der Zustandsvariablen an. |
126 Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a") |
121 Bsp.: bei name="s" und dem Term "s(Suc(Suc(0)))=s(0)" (entspricht "c=a") |
127 wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *) |
122 wird [0,Suc(Suc(0))] geliefert (Liste ist i.A. unsortiert) *) |
128 |
123 |
129 fun pvars_of_term (name,trm) = |
124 fun pvars_of_term (name,trm) = |
130 let |
125 let fun add_vars (name,Free (s,t) $ trm,vl) = |
131 fun add_vars (name,Free (s,t) $ trm,vl) =if name=s |
126 if name=s then if trm mem vl then vl else trm::vl |
132 then if trm mem vl |
127 else add_vars (name,trm,vl) |
133 then vl |
128 | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl) |
134 else trm::vl |
129 | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl)) |
135 else add_vars (name,trm,vl) |
130 | add_vars (_,_,vl) =vl |
136 | add_vars (name,Abs (s,t,trm),vl) =add_vars (name,trm,vl) |
131 in add_vars (name,trm,[]) end; |
137 | add_vars (name,trm1 $ trm2,vl) =add_vars (name,trm2,add_vars (name,trm1,vl)) |
132 |
138 | add_vars (_,_,vl) =vl |
|
139 in |
|
140 add_vars (name,trm,[]) |
|
141 end; |
|
142 |
133 |
143 (* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i |
134 (* VarsElimTac: Taktik zum Eliminieren von bestimmten Programmvariablen aus dem Subgoal i |
144 - v::vl:(term) list Liste der zu eliminierenden Programmvariablen |
135 - v::vl:(term) list Liste der zu eliminierenden Programmvariablen |
145 - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird |
136 - meta_spec:thm Theorem, welches zur Entfernung der Variablen benutzt wird |
146 z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" |
137 z.B.: "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" |
147 - namexAll:string Name von ^ (hier "x") |
138 - namexAll:string Name von ^ (hier "x") |
148 - varx:term Term zu ^ (hier Var(("x",0),...)) |
139 - varx:term Term zu ^ (hier Var(("x",0),...)) |
149 - varP:term Term zu ^ (hier Var(("P",0),...)) |
140 - varP:term Term zu ^ (hier Var(("P",0),...)) |
150 - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...) |
141 - type_pvar:typ Typ der Programmvariablen (d.h. 'a bei 'a prog, z.B.: nat, bool, ...) |
151 |
142 |
152 Vorgehen: |
143 Vorgehen: |
153 - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu: |
144 - eliminiere jede pvar durch Anwendung von comp_inst_ren_tac. Dazu: |
154 - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt |
145 - Unbenennung in meta_spec: namexAll wird in den Namen der Prog.-Var. umbenannt |
155 z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich |
146 z.B.: fuer die Prog.-Var. mit Namen "a" ergibt sich |
156 meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))" |
147 meta_spec zu "(!! s a.PROP P(s,a)) ==> (!! s.PROP P(s,x(s)))" |
157 - Instanziierungen in meta_spec: |
148 - Instanziierungen in meta_spec: |
158 varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert |
149 varx wird mit "%s:(type_pvar) state.s(pvar)" instanziiert |
159 varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a": |
150 varP wird entsprechend instanziiert. Beispiel fuer Prog.-Var. "a": |
160 - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.": |
151 - zu Subgoal "!!s.s(Suc(0)) = s(0) ==> s(0) = 1" bestimme Term ohne "!!s.": |
161 trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable) |
152 trm0 = "s(Suc(0)) = s(0) ==> s(0) = 1" (s ist hier freie Variable) |
162 - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs: |
153 - substituiere alle Vorkommen von s(pvar) durch eine freie Var. xs: |
163 trm1 = "s(Suc(0)) = xs ==> xs = 1" |
154 trm1 = "s(Suc(0)) = xs ==> xs = 1" |
164 - abstrahiere ueber xs: |
155 - abstrahiere ueber xs: |
165 trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1" |
156 trm2 = "%xs.s(Suc(0)) = xs ==> xs = 1" |
166 - abstrahiere ueber restliche Vorkommen von s: |
157 - abstrahiere ueber restliche Vorkommen von s: |
167 trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1" |
158 trm3 = "%s xs.s(Suc(0)) = xs ==> xs = 1" |
168 - instanziiere varP mit trm3 |
159 - instanziiere varP mit trm3 |
169 *) |
160 *) |
170 |
161 |
171 fun VarsElimTac ([],_,_,_,_,_) i =all_tac |
162 (* StateElimTac: tactic to eliminate all program variable from subgoal i |
172 | VarsElimTac (v::vl,meta_spec,namexAll,varx,varP,type_pvar) i = |
163 - applies to subgoals of the form "!!s:('a) state.P(s)", |
173 STATE ( |
164 i.e. the term Const("all",_) $ Abs ("s",pvar --> 'a,_) |
174 fn state => |
165 - meta_spec has the form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" |
175 comp_inst_ren_tac |
|
176 [(namexAll,pvar2pvarID v)] |
|
177 [( |
|
178 cterm_of (#sign (rep_thm state)) varx, |
|
179 cterm_of (#sign (rep_thm state)) ( |
|
180 Abs ("s",Type ("nat",[]) --> type_pvar,Bound 0 $ v) |
|
181 ) |
|
182 ),( |
|
183 cterm_of (#sign (rep_thm state)) varP, |
|
184 cterm_of (#sign (rep_thm state)) ( |
|
185 let |
|
186 val (_,_,_ $ Abs (_,_,trm),_) = dest_state (state,i); |
|
187 val (sname,trm0) = variant_abs ("s",dummyT,trm); |
|
188 val xsname = variant_name ("xs",trm0); |
|
189 val trm1 = subst_term (Free (sname,dummyT) $ v,Syntax.free xsname,trm0) |
|
190 val trm2 = Abs ("xs",type_pvar,abstract_over (Syntax.free xsname,trm1)) |
|
191 in |
|
192 Abs ("s",Type ("nat",[]) --> type_pvar,abstract_over (Free (sname,dummyT),trm2)) |
|
193 end |
|
194 ) |
|
195 )] |
|
196 meta_spec i |
|
197 ) |
|
198 THEN |
|
199 (VarsElimTac (vl,meta_spec,namexAll,varx,varP,type_pvar) i); |
|
200 |
|
201 (* StateElimTac: Taktik zum Eliminieren aller Programmvariablen aus dem Subgoal i |
|
202 |
|
203 zur Erinnerung: |
|
204 - das Subgoal hat vor Anwendung dieser Taktik die Form "!!s:('a) state.P(s)", |
|
205 d.h. den Term Const("all",_) $ Abs ("s",pvar --> 'a,_) |
|
206 - meta_spec hat die Form "(!!s x.PROP P(s,x)) ==> (!!s.PROP P(s,x(s)))" |
|
207 *) |
166 *) |
208 |
167 |
209 fun StateElimTac i = |
168 val StateElimTac = SUBGOAL (fn (Bi,i) => |
210 STATE ( |
169 let val Const _ $ Abs (_,Type ("fun",[_,type_pvar]),trm) = Bi |
211 fn state => |
170 val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $ |
212 let |
171 (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = |
213 val (_,_,_ $ Abs (_,Type ("fun",[_,type_pvar]),trm),_) = dest_state (state,i); |
172 #prop (rep_thm meta_spec) |
214 val _ $ (_ $ Abs (_,_,_ $ Abs (namexAll,_,_))) $ |
173 fun vtac v i st = st |> |
215 (_ $ Abs (_,_,varP $ _ $ (varx $ _))) = #prop (rep_thm meta_spec) |
174 let val cterm = cterm_of (#sign (rep_thm st)) |
216 in |
175 val (_,_,_ $ Abs (_,_,trm),_) = dest_state (st,i); |
217 VarsElimTac (pvars_of_term (variant_abs ("s",dummyT,trm)),meta_spec,namexAll,varx,varP,type_pvar) i |
176 val (sname,trm0) = variant_abs ("s",dummyT,trm); |
218 end |
177 val xsname = variant_name ("xs",trm0); |
219 ); |
178 val trm1 = subst_term (Free (sname,dummyT) $ v, |
220 |
179 Syntax.free xsname,trm0) |
|
180 val trm2 = Abs ("xs", type_pvar, |
|
181 abstract_over (Syntax.free xsname,trm1)) |
|
182 in |
|
183 comp_inst_ren_tac |
|
184 [(namexAll,pvar2pvarID v)] |
|
185 [(cterm varx, |
|
186 cterm (Abs ("s",Type ("nat",[]) --> type_pvar, |
|
187 Bound 0 $ v))), |
|
188 (cterm varP, |
|
189 cterm (Abs ("s", Type ("nat",[]) --> type_pvar, |
|
190 abstract_over (Free (sname,dummyT),trm2))))] |
|
191 meta_spec i |
|
192 end |
|
193 fun vars_tac [] i = all_tac |
|
194 | vars_tac (v::vl) i = vtac v i THEN vars_tac vl i |
|
195 in |
|
196 vars_tac (pvars_of_term (variant_abs ("s",dummyT,trm))) i |
|
197 end); |
221 |
198 |
222 |
199 |
223 (*** tactics for verification condition generation ***) |
200 (*** tactics for verification condition generation ***) |
224 |
201 |
225 (* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall |
202 (* pre_cond:bool gibt an, ob das Subgoal von der Form Spec(?Q,c,p) ist oder nicht. Im Fall |
226 von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann |
203 von pre_cond=false besteht die Vorbedingung nur nur aus einer scheme-Variable. Die dann |
227 generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen |
204 generierte Verifikationsbedingung hat die Form "!!s.?Q --> ...". "?Q" kann deshalb zu gegebenen |
228 Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *) |
205 Zeitpunkt mittels "rtac impI" und "atac" gebunden werden, die Bedingung loest sich dadurch auf. *) |
229 |
206 |
230 fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false) |
207 fun WlpTac i = (rtac SeqRule i) THEN (HoareRuleTac (i+1) false) |
231 and HoareRuleTac i pre_cond = |
208 and HoareRuleTac i pre_cond st = st |> |
232 STATE(fn state => |
209 (*abstraction over st prevents looping*) |
233 ((WlpTac i) THEN (HoareRuleTac i pre_cond)) |
210 ( (WlpTac i THEN HoareRuleTac i pre_cond) |
234 ORELSE |
211 ORELSE |
235 (FIRST[rtac SkipRule i, |
212 (FIRST[rtac SkipRule i, |
236 rtac AssignRule i, |
213 rtac AssignRule i, |
237 EVERY[rtac IfRule i, |
214 EVERY[rtac IfRule i, |
238 HoareRuleTac (i+2) false, |
215 HoareRuleTac (i+2) false, |
239 HoareRuleTac (i+1) false], |
216 HoareRuleTac (i+1) false], |
240 EVERY[rtac WhileRule i, |
217 EVERY[rtac WhileRule i, |
241 Asm_full_simp_tac (i+2), |
218 Asm_full_simp_tac (i+2), |
242 HoareRuleTac (i+1) true]] |
219 HoareRuleTac (i+1) true]] |
243 THEN |
220 THEN |
244 (if pre_cond then (Asm_full_simp_tac i) else (atac i)) |
221 (if pre_cond then (Asm_full_simp_tac i) else (atac i))) ); |
245 ) |
222 |
246 ); |
223 val hoare_tac = |
247 |
224 SELECT_GOAL |
248 val HoareTac1 = |
225 (EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]); |
249 EVERY[HoareRuleTac 1 true, ALLGOALS StateElimTac, prune_params_tac]; |
226 |
250 |
|
251 val hoare_tac = SELECT_GOAL (HoareTac1); |
|
252 |
|