0
|
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;
|