|
1 (* Title: drule |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1993 University of Cambridge |
|
5 |
|
6 Derived rules and other operations on theorems and theories |
|
7 *) |
|
8 |
|
9 infix 0 RS RSN RL RLN COMP; |
|
10 |
|
11 signature DRULE = |
|
12 sig |
|
13 structure Thm : THM |
|
14 local open Thm in |
|
15 val asm_rl: thm |
|
16 val assume_ax: theory -> string -> thm |
|
17 val COMP: thm * thm -> thm |
|
18 val compose: thm * int * thm -> thm list |
|
19 val cterm_instantiate: (Sign.cterm*Sign.cterm)list -> thm -> thm |
|
20 val cut_rl: thm |
|
21 val equal_abs_elim: Sign.cterm -> thm -> thm |
|
22 val equal_abs_elim_list: Sign.cterm list -> thm -> thm |
|
23 val eq_sg: Sign.sg * Sign.sg -> bool |
|
24 val eq_thm: thm * thm -> bool |
|
25 val eq_thm_sg: thm * thm -> bool |
|
26 val flexpair_abs_elim_list: Sign.cterm list -> thm -> thm |
|
27 val forall_intr_list: Sign.cterm list -> thm -> thm |
|
28 val forall_intr_frees: thm -> thm |
|
29 val forall_elim_list: Sign.cterm list -> thm -> thm |
|
30 val forall_elim_var: int -> thm -> thm |
|
31 val forall_elim_vars: int -> thm -> thm |
|
32 val implies_elim_list: thm -> thm list -> thm |
|
33 val implies_intr_list: Sign.cterm list -> thm -> thm |
|
34 val print_cterm: Sign.cterm -> unit |
|
35 val print_ctyp: Sign.ctyp -> unit |
|
36 val print_goals: int -> thm -> unit |
|
37 val print_sg: Sign.sg -> unit |
|
38 val print_theory: theory -> unit |
|
39 val pprint_sg: Sign.sg -> pprint_args -> unit |
|
40 val pprint_theory: theory -> pprint_args -> unit |
|
41 val print_thm: thm -> unit |
|
42 val prth: thm -> thm |
|
43 val prthq: thm Sequence.seq -> thm Sequence.seq |
|
44 val prths: thm list -> thm list |
|
45 val read_instantiate: (string*string)list -> thm -> thm |
|
46 val read_instantiate_sg: Sign.sg -> (string*string)list -> thm -> thm |
|
47 val reflexive_thm: thm |
|
48 val revcut_rl: thm |
|
49 val rewrite_goal_rule: (meta_simpset -> thm -> thm option) -> meta_simpset -> |
|
50 int -> thm -> thm |
|
51 val rewrite_goals_rule: thm list -> thm -> thm |
|
52 val rewrite_rule: thm list -> thm -> thm |
|
53 val RS: thm * thm -> thm |
|
54 val RSN: thm * (int * thm) -> thm |
|
55 val RL: thm list * thm list -> thm list |
|
56 val RLN: thm list * (int * thm list) -> thm list |
|
57 val show_hyps: bool ref |
|
58 val size_of_thm: thm -> int |
|
59 val standard: thm -> thm |
|
60 val string_of_thm: thm -> string |
|
61 val symmetric_thm: thm |
|
62 val pprint_thm: thm -> pprint_args -> unit |
|
63 val transitive_thm: thm |
|
64 val triv_forall_equality: thm |
|
65 val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) |
|
66 val zero_var_indexes: thm -> thm |
|
67 end |
|
68 end; |
|
69 |
|
70 functor DruleFun (structure Logic: LOGIC and Thm: THM) : DRULE = |
|
71 struct |
|
72 structure Thm = Thm; |
|
73 structure Sign = Thm.Sign; |
|
74 structure Type = Sign.Type; |
|
75 structure Pretty = Sign.Syntax.Pretty |
|
76 local open Thm |
|
77 in |
|
78 |
|
79 (**** More derived rules and operations on theorems ****) |
|
80 |
|
81 (*** Find the type (sort) associated with a (T)Var or (T)Free in a term |
|
82 Used for establishing default types (of variables) and sorts (of |
|
83 type variables) when reading another term. |
|
84 Index -1 indicates that a (T)Free rather than a (T)Var is wanted. |
|
85 ***) |
|
86 |
|
87 fun types_sorts thm = |
|
88 let val {prop,hyps,...} = rep_thm thm; |
|
89 val big = list_comb(prop,hyps); (* bogus term! *) |
|
90 val vars = map dest_Var (term_vars big); |
|
91 val frees = map dest_Free (term_frees big); |
|
92 val tvars = term_tvars big; |
|
93 val tfrees = term_tfrees big; |
|
94 fun typ(a,i) = if i<0 then assoc(frees,a) else assoc(vars,(a,i)); |
|
95 fun sort(a,i) = if i<0 then assoc(tfrees,a) else assoc(tvars,(a,i)); |
|
96 in (typ,sort) end; |
|
97 |
|
98 (** Standardization of rules **) |
|
99 |
|
100 (*Generalization over a list of variables, IGNORING bad ones*) |
|
101 fun forall_intr_list [] th = th |
|
102 | forall_intr_list (y::ys) th = |
|
103 let val gth = forall_intr_list ys th |
|
104 in forall_intr y gth handle THM _ => gth end; |
|
105 |
|
106 (*Generalization over all suitable Free variables*) |
|
107 fun forall_intr_frees th = |
|
108 let val {prop,sign,...} = rep_thm th |
|
109 in forall_intr_list |
|
110 (map (Sign.cterm_of sign) (sort atless (term_frees prop))) |
|
111 th |
|
112 end; |
|
113 |
|
114 (*Replace outermost quantified variable by Var of given index. |
|
115 Could clash with Vars already present.*) |
|
116 fun forall_elim_var i th = |
|
117 let val {prop,sign,...} = rep_thm th |
|
118 in case prop of |
|
119 Const("all",_) $ Abs(a,T,_) => |
|
120 forall_elim (Sign.cterm_of sign (Var((a,i), T))) th |
|
121 | _ => raise THM("forall_elim_var", i, [th]) |
|
122 end; |
|
123 |
|
124 (*Repeat forall_elim_var until all outer quantifiers are removed*) |
|
125 fun forall_elim_vars i th = |
|
126 forall_elim_vars i (forall_elim_var i th) |
|
127 handle THM _ => th; |
|
128 |
|
129 (*Specialization over a list of cterms*) |
|
130 fun forall_elim_list cts th = foldr (uncurry forall_elim) (rev cts, th); |
|
131 |
|
132 (* maps [A1,...,An], B to [| A1;...;An |] ==> B *) |
|
133 fun implies_intr_list cAs th = foldr (uncurry implies_intr) (cAs,th); |
|
134 |
|
135 (* maps [| A1;...;An |] ==> B and [A1,...,An] to B *) |
|
136 fun implies_elim_list impth ths = foldl (uncurry implies_elim) (impth,ths); |
|
137 |
|
138 (*Reset Var indexes to zero, renaming to preserve distinctness*) |
|
139 fun zero_var_indexes th = |
|
140 let val {prop,sign,...} = rep_thm th; |
|
141 val vars = term_vars prop |
|
142 val bs = foldl add_new_id ([], map (fn Var((a,_),_)=>a) vars) |
|
143 val inrs = add_term_tvars(prop,[]); |
|
144 val nms' = rev(foldl add_new_id ([], map (#1 o #1) inrs)); |
|
145 val tye = map (fn ((v,rs),a) => (v, TVar((a,0),rs))) (inrs ~~ nms') |
|
146 val ctye = map (fn (v,T) => (v,Sign.ctyp_of sign T)) tye; |
|
147 fun varpairs([],[]) = [] |
|
148 | varpairs((var as Var(v,T)) :: vars, b::bs) = |
|
149 let val T' = typ_subst_TVars tye T |
|
150 in (Sign.cterm_of sign (Var(v,T')), |
|
151 Sign.cterm_of sign (Var((b,0),T'))) :: varpairs(vars,bs) |
|
152 end |
|
153 | varpairs _ = raise TERM("varpairs", []); |
|
154 in instantiate (ctye, varpairs(vars,rev bs)) th end; |
|
155 |
|
156 |
|
157 (*Standard form of object-rule: no hypotheses, Frees, or outer quantifiers; |
|
158 all generality expressed by Vars having index 0.*) |
|
159 fun standard th = |
|
160 let val {maxidx,...} = rep_thm th |
|
161 in varifyT (zero_var_indexes (forall_elim_vars(maxidx+1) |
|
162 (forall_intr_frees(implies_intr_hyps th)))) |
|
163 end; |
|
164 |
|
165 (*Assume a new formula, read following the same conventions as axioms. |
|
166 Generalizes over Free variables, |
|
167 creates the assumption, and then strips quantifiers. |
|
168 Example is [| ALL x:?A. ?P(x) |] ==> [| ?P(?a) |] |
|
169 [ !(A,P,a)[| ALL x:A. P(x) |] ==> [| P(a) |] ] *) |
|
170 fun assume_ax thy sP = |
|
171 let val sign = sign_of thy |
|
172 val prop = Logic.close_form (Sign.term_of (Sign.read_cterm sign |
|
173 (sP, propT))) |
|
174 in forall_elim_vars 0 (assume (Sign.cterm_of sign prop)) end; |
|
175 |
|
176 (*Resolution: exactly one resolvent must be produced.*) |
|
177 fun tha RSN (i,thb) = |
|
178 case Sequence.chop (2, biresolution false [(false,tha)] i thb) of |
|
179 ([th],_) => th |
|
180 | ([],_) => raise THM("RSN: no unifiers", i, [tha,thb]) |
|
181 | _ => raise THM("RSN: multiple unifiers", i, [tha,thb]); |
|
182 |
|
183 (*resolution: P==>Q, Q==>R gives P==>R. *) |
|
184 fun tha RS thb = tha RSN (1,thb); |
|
185 |
|
186 (*For joining lists of rules*) |
|
187 fun thas RLN (i,thbs) = |
|
188 let val resolve = biresolution false (map (pair false) thas) i |
|
189 fun resb thb = Sequence.list_of_s (resolve thb) handle THM _ => [] |
|
190 in flat (map resb thbs) end; |
|
191 |
|
192 fun thas RL thbs = thas RLN (1,thbs); |
|
193 |
|
194 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R |
|
195 with no lifting or renaming! Q may contain ==> or meta-quants |
|
196 ALWAYS deletes premise i *) |
|
197 fun compose(tha,i,thb) = |
|
198 Sequence.list_of_s (bicompose false (false,tha,0) i thb); |
|
199 |
|
200 (*compose Q and [Q1,Q2,...,Qk]==>R to [Q2,...,Qk]==>R getting unique result*) |
|
201 fun tha COMP thb = |
|
202 case compose(tha,1,thb) of |
|
203 [th] => th |
|
204 | _ => raise THM("COMP", 1, [tha,thb]); |
|
205 |
|
206 (*Instantiate theorem th, reading instantiations under signature sg*) |
|
207 fun read_instantiate_sg sg sinsts th = |
|
208 let val ts = types_sorts th; |
|
209 val instpair = Sign.read_insts sg ts ts sinsts |
|
210 in instantiate instpair th end; |
|
211 |
|
212 (*Instantiate theorem th, reading instantiations under theory of th*) |
|
213 fun read_instantiate sinsts th = |
|
214 read_instantiate_sg (#sign (rep_thm th)) sinsts th; |
|
215 |
|
216 |
|
217 (*Left-to-right replacements: tpairs = [...,(vi,ti),...]. |
|
218 Instantiates distinct Vars by terms, inferring type instantiations. *) |
|
219 local |
|
220 fun add_types ((ct,cu), (sign,tye)) = |
|
221 let val {sign=signt, t=t, T= T, ...} = Sign.rep_cterm ct |
|
222 and {sign=signu, t=u, T= U, ...} = Sign.rep_cterm cu |
|
223 val sign' = Sign.merge(sign, Sign.merge(signt, signu)) |
|
224 val tye' = Type.unify (#tsig(Sign.rep_sg sign')) ((T,U), tye) |
|
225 handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u]) |
|
226 in (sign', tye') end; |
|
227 in |
|
228 fun cterm_instantiate ctpairs0 th = |
|
229 let val (sign,tye) = foldr add_types (ctpairs0, (#sign(rep_thm th),[])) |
|
230 val tsig = #tsig(Sign.rep_sg sign); |
|
231 fun instT(ct,cu) = let val inst = subst_TVars tye |
|
232 in (Sign.cfun inst ct, Sign.cfun inst cu) end |
|
233 fun ctyp2 (ix,T) = (ix, Sign.ctyp_of sign T) |
|
234 in instantiate (map ctyp2 tye, map instT ctpairs0) th end |
|
235 handle TERM _ => |
|
236 raise THM("cterm_instantiate: incompatible signatures",0,[th]) |
|
237 | TYPE _ => raise THM("cterm_instantiate: types", 0, [th]) |
|
238 end; |
|
239 |
|
240 |
|
241 (*** Printing of theorems ***) |
|
242 |
|
243 (*If false, hypotheses are printed as dots*) |
|
244 val show_hyps = ref true; |
|
245 |
|
246 fun pretty_thm th = |
|
247 let val {sign, hyps, prop,...} = rep_thm th |
|
248 val hsymbs = if null hyps then [] |
|
249 else if !show_hyps then |
|
250 [Pretty.brk 2, |
|
251 Pretty.lst("[","]") (map (Sign.pretty_term sign) hyps)] |
|
252 else Pretty.str" [" :: map (fn _ => Pretty.str".") hyps @ |
|
253 [Pretty.str"]"]; |
|
254 in Pretty.blk(0, Sign.pretty_term sign prop :: hsymbs) end; |
|
255 |
|
256 val string_of_thm = Pretty.string_of o pretty_thm; |
|
257 |
|
258 val pprint_thm = Pretty.pprint o Pretty.quote o pretty_thm; |
|
259 |
|
260 |
|
261 (** Top-level commands for printing theorems **) |
|
262 val print_thm = writeln o string_of_thm; |
|
263 |
|
264 fun prth th = (print_thm th; th); |
|
265 |
|
266 (*Print and return a sequence of theorems, separated by blank lines. *) |
|
267 fun prthq thseq = |
|
268 (Sequence.prints (fn _ => print_thm) 100000 thseq; |
|
269 thseq); |
|
270 |
|
271 (*Print and return a list of theorems, separated by blank lines. *) |
|
272 fun prths ths = (print_list_ln print_thm ths; ths); |
|
273 |
|
274 (*Other printing commands*) |
|
275 val print_cterm = writeln o Sign.string_of_cterm; |
|
276 val print_ctyp = writeln o Sign.string_of_ctyp; |
|
277 fun pretty_sg sg = |
|
278 Pretty.lst ("{", "}") (map (Pretty.str o !) (#stamps (Sign.rep_sg sg))); |
|
279 |
|
280 val pprint_sg = Pretty.pprint o pretty_sg; |
|
281 |
|
282 val pprint_theory = pprint_sg o sign_of; |
|
283 |
|
284 val print_sg = writeln o Pretty.string_of o pretty_sg; |
|
285 val print_theory = print_sg o sign_of; |
|
286 |
|
287 |
|
288 (** Print thm A1,...,An/B in "goal style" -- premises as numbered subgoals **) |
|
289 |
|
290 fun prettyprints es = writeln(Pretty.string_of(Pretty.blk(0,es))); |
|
291 |
|
292 fun print_goals maxgoals th : unit = |
|
293 let val {sign, hyps, prop,...} = rep_thm th; |
|
294 fun printgoals (_, []) = () |
|
295 | printgoals (n, A::As) = |
|
296 let val prettyn = Pretty.str(" " ^ string_of_int n ^ ". "); |
|
297 val prettyA = Sign.pretty_term sign A |
|
298 in prettyprints[prettyn,prettyA]; |
|
299 printgoals (n+1,As) |
|
300 end; |
|
301 fun prettypair(t,u) = |
|
302 Pretty.blk(0, [Sign.pretty_term sign t, Pretty.str" =?=", Pretty.brk 1, |
|
303 Sign.pretty_term sign u]); |
|
304 fun printff [] = () |
|
305 | printff tpairs = |
|
306 writeln("\nFlex-flex pairs:\n" ^ |
|
307 Pretty.string_of(Pretty.lst("","") (map prettypair tpairs))) |
|
308 val (tpairs,As,B) = Logic.strip_horn(prop); |
|
309 val ngoals = length As |
|
310 in |
|
311 writeln (Sign.string_of_term sign B); |
|
312 if ngoals=0 then writeln"No subgoals!" |
|
313 else if ngoals>maxgoals |
|
314 then (printgoals (1, take(maxgoals,As)); |
|
315 writeln("A total of " ^ string_of_int ngoals ^ " subgoals...")) |
|
316 else printgoals (1, As); |
|
317 printff tpairs |
|
318 end; |
|
319 |
|
320 |
|
321 (** theorem equality test is exported and used by BEST_FIRST **) |
|
322 |
|
323 (*equality of signatures means exact identity -- by ref equality*) |
|
324 fun eq_sg (sg1,sg2) = (#stamps(Sign.rep_sg sg1) = #stamps(Sign.rep_sg sg2)); |
|
325 |
|
326 (*equality of theorems uses equality of signatures and |
|
327 the a-convertible test for terms*) |
|
328 fun eq_thm (th1,th2) = |
|
329 let val {sign=sg1, hyps=hyps1, prop=prop1, ...} = rep_thm th1 |
|
330 and {sign=sg2, hyps=hyps2, prop=prop2, ...} = rep_thm th2 |
|
331 in eq_sg (sg1,sg2) andalso |
|
332 aconvs(hyps1,hyps2) andalso |
|
333 prop1 aconv prop2 |
|
334 end; |
|
335 |
|
336 (*Do the two theorems have the same signature?*) |
|
337 fun eq_thm_sg (th1,th2) = eq_sg(#sign(rep_thm th1), #sign(rep_thm th2)); |
|
338 |
|
339 (*Useful "distance" function for BEST_FIRST*) |
|
340 val size_of_thm = size_of_term o #prop o rep_thm; |
|
341 |
|
342 |
|
343 (*** Meta-Rewriting Rules ***) |
|
344 |
|
345 |
|
346 val reflexive_thm = |
|
347 let val cx = Sign.cterm_of Sign.pure (Var(("x",0),TVar(("'a",0),["logic"]))) |
|
348 in Thm.reflexive cx end; |
|
349 |
|
350 val symmetric_thm = |
|
351 let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT) |
|
352 in standard(Thm.implies_intr_hyps(Thm.symmetric(Thm.assume xy))) end; |
|
353 |
|
354 val transitive_thm = |
|
355 let val xy = Sign.read_cterm Sign.pure ("x::'a::logic == y",propT) |
|
356 val yz = Sign.read_cterm Sign.pure ("y::'a::logic == z",propT) |
|
357 val xythm = Thm.assume xy and yzthm = Thm.assume yz |
|
358 in standard(Thm.implies_intr yz (Thm.transitive xythm yzthm)) end; |
|
359 |
|
360 |
|
361 (** Below, a "conversion" has type sign->term->thm **) |
|
362 |
|
363 (*In [A1,...,An]==>B, rewrite the selected A's only -- for rewrite_goals_tac*) |
|
364 fun goals_conv pred cv sign = |
|
365 let val triv = reflexive o Sign.cterm_of sign |
|
366 fun gconv i t = |
|
367 let val (A,B) = Logic.dest_implies t |
|
368 val thA = if (pred i) then (cv sign A) else (triv A) |
|
369 in combination (combination (triv implies) thA) |
|
370 (gconv (i+1) B) |
|
371 end |
|
372 handle TERM _ => triv t |
|
373 in gconv 1 end; |
|
374 |
|
375 (*Use a conversion to transform a theorem*) |
|
376 fun fconv_rule cv th = |
|
377 let val {sign,prop,...} = rep_thm th |
|
378 in equal_elim (cv sign prop) th end; |
|
379 |
|
380 (*rewriting conversion*) |
|
381 fun rew_conv prover mss sign t = |
|
382 rewrite_cterm mss prover (Sign.cterm_of sign t); |
|
383 |
|
384 (*Rewrite a theorem*) |
|
385 fun rewrite_rule thms = fconv_rule (rew_conv (K(K None)) (Thm.mss_of thms)); |
|
386 |
|
387 (*Rewrite the subgoals of a proof state (represented by a theorem) *) |
|
388 fun rewrite_goals_rule thms = |
|
389 fconv_rule (goals_conv (K true) (rew_conv (K(K None)) (Thm.mss_of thms))); |
|
390 |
|
391 (*Rewrite the subgoal of a proof state (represented by a theorem) *) |
|
392 fun rewrite_goal_rule prover mss i = |
|
393 fconv_rule (goals_conv (fn j => j=i) (rew_conv prover mss)); |
|
394 |
|
395 |
|
396 (** Derived rules mainly for METAHYPS **) |
|
397 |
|
398 (*Given the term "a", takes (%x.t)==(%x.u) to t[a/x]==u[a/x]*) |
|
399 fun equal_abs_elim ca eqth = |
|
400 let val {sign=signa, t=a, ...} = Sign.rep_cterm ca |
|
401 and combth = combination eqth (reflexive ca) |
|
402 val {sign,prop,...} = rep_thm eqth |
|
403 val (abst,absu) = Logic.dest_equals prop |
|
404 val cterm = Sign.cterm_of (Sign.merge (sign,signa)) |
|
405 in transitive (symmetric (beta_conversion (cterm (abst$a)))) |
|
406 (transitive combth (beta_conversion (cterm (absu$a)))) |
|
407 end |
|
408 handle THM _ => raise THM("equal_abs_elim", 0, [eqth]); |
|
409 |
|
410 (*Calling equal_abs_elim with multiple terms*) |
|
411 fun equal_abs_elim_list cts th = foldr (uncurry equal_abs_elim) (rev cts, th); |
|
412 |
|
413 local |
|
414 open Logic |
|
415 val alpha = TVar(("'a",0), []) (* type ?'a::{} *) |
|
416 fun err th = raise THM("flexpair_inst: ", 0, [th]) |
|
417 fun flexpair_inst def th = |
|
418 let val {prop = Const _ $ t $ u, sign,...} = rep_thm th |
|
419 val cterm = Sign.cterm_of sign |
|
420 fun cvar a = cterm(Var((a,0),alpha)) |
|
421 val def' = cterm_instantiate [(cvar"t", cterm t), (cvar"u", cterm u)] |
|
422 def |
|
423 in equal_elim def' th |
|
424 end |
|
425 handle THM _ => err th | bind => err th |
|
426 in |
|
427 val flexpair_intr = flexpair_inst (symmetric flexpair_def) |
|
428 and flexpair_elim = flexpair_inst flexpair_def |
|
429 end; |
|
430 |
|
431 (*Version for flexflex pairs -- this supports lifting.*) |
|
432 fun flexpair_abs_elim_list cts = |
|
433 flexpair_intr o equal_abs_elim_list cts o flexpair_elim; |
|
434 |
|
435 |
|
436 (*** Some useful meta-theorems ***) |
|
437 |
|
438 (*The rule V/V, obtains assumption solving for eresolve_tac*) |
|
439 val asm_rl = trivial(Sign.read_cterm Sign.pure ("PROP ?psi",propT)); |
|
440 |
|
441 (*Meta-level cut rule: [| V==>W; V |] ==> W *) |
|
442 val cut_rl = trivial(Sign.read_cterm Sign.pure |
|
443 ("PROP ?psi ==> PROP ?theta", propT)); |
|
444 |
|
445 (*Generalized elim rule for one conclusion; cut_rl with reversed premises: |
|
446 [| PROP V; PROP V ==> PROP W |] ==> PROP W *) |
|
447 val revcut_rl = |
|
448 let val V = Sign.read_cterm Sign.pure ("PROP V", propT) |
|
449 and VW = Sign.read_cterm Sign.pure ("PROP V ==> PROP W", propT); |
|
450 in standard (implies_intr V |
|
451 (implies_intr VW |
|
452 (implies_elim (assume VW) (assume V)))) |
|
453 end; |
|
454 |
|
455 (* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*) |
|
456 val triv_forall_equality = |
|
457 let val V = Sign.read_cterm Sign.pure ("PROP V", propT) |
|
458 and QV = Sign.read_cterm Sign.pure ("!!x::'a. PROP V", propT) |
|
459 and x = Sign.read_cterm Sign.pure ("x", TFree("'a",["logic"])); |
|
460 in standard (equal_intr (implies_intr QV (forall_elim x (assume QV))) |
|
461 (implies_intr V (forall_intr x (assume V)))) |
|
462 end; |
|
463 |
|
464 end |
|
465 end; |