|
1 |
|
2 text {* tyRel takes a type and builds a relation that a quantifier over this |
|
3 type needs to respect. *} |
|
4 ML {* |
|
5 fun tyRel ty rty rel lthy = |
|
6 if Sign.typ_instance (ProofContext.theory_of lthy) (ty, rty) |
|
7 then rel |
|
8 else (case ty of |
|
9 Type (s, tys) => |
|
10 let |
|
11 val tys_rel = map (fn ty => ty --> ty --> @{typ bool}) tys; |
|
12 val ty_out = ty --> ty --> @{typ bool}; |
|
13 val tys_out = tys_rel ---> ty_out; |
|
14 in |
|
15 (case (maps_lookup (ProofContext.theory_of lthy) s) of |
|
16 SOME (info) => list_comb (Const (#relfun info, tys_out), |
|
17 map (fn ty => tyRel ty rty rel lthy) tys) |
|
18 | NONE => HOLogic.eq_const ty |
|
19 ) |
|
20 end |
|
21 | _ => HOLogic.eq_const ty) |
|
22 *} |
|
23 |
|
24 (* |
|
25 ML {* cterm_of @{theory} |
|
26 (tyRel @{typ "'a \<Rightarrow> 'a list \<Rightarrow> 't \<Rightarrow> 't"} (Logic.varifyT @{typ "'a list"}) |
|
27 @{term "f::('a list \<Rightarrow> 'a list \<Rightarrow> bool)"} @{context}) |
|
28 *} |
|
29 *) |
|
30 |
|
31 |
|
32 ML {* |
|
33 fun mk_babs ty ty' = Const (@{const_name "Babs"}, [ty' --> @{typ bool}, ty] ---> ty) |
|
34 fun mk_ball ty = Const (@{const_name "Ball"}, [ty, ty] ---> @{typ bool}) |
|
35 fun mk_bex ty = Const (@{const_name "Bex"}, [ty, ty] ---> @{typ bool}) |
|
36 fun mk_resp ty = Const (@{const_name Respects}, [[ty, ty] ---> @{typ bool}, ty] ---> @{typ bool}) |
|
37 *} |
|
38 |
|
39 (* applies f to the subterm of an abstractions, otherwise to the given term *) |
|
40 ML {* |
|
41 fun apply_subt f trm = |
|
42 case trm of |
|
43 Abs (x, T, t) => |
|
44 let |
|
45 val (x', t') = Term.dest_abs (x, T, t) |
|
46 in |
|
47 Term.absfree (x', T, f t') |
|
48 end |
|
49 | _ => f trm |
|
50 *} |
|
51 |
|
52 |
|
53 |
|
54 (* FIXME: if there are more than one quotient, then you have to look up the relation *) |
|
55 ML {* |
|
56 fun my_reg lthy rel rty trm = |
|
57 case trm of |
|
58 Abs (x, T, t) => |
|
59 if (needs_lift rty T) then |
|
60 let |
|
61 val rrel = tyRel T rty rel lthy |
|
62 in |
|
63 (mk_babs (fastype_of trm) T) $ (mk_resp T $ rrel) $ (apply_subt (my_reg lthy rel rty) trm) |
|
64 end |
|
65 else |
|
66 Abs(x, T, (apply_subt (my_reg lthy rel rty) t)) |
|
67 | Const (@{const_name "All"}, ty) $ (t as Abs (x, T, _)) => |
|
68 let |
|
69 val ty1 = domain_type ty |
|
70 val ty2 = domain_type ty1 |
|
71 val rrel = tyRel T rty rel lthy |
|
72 in |
|
73 if (needs_lift rty T) then |
|
74 (mk_ball ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
|
75 else |
|
76 Const (@{const_name "All"}, ty) $ apply_subt (my_reg lthy rel rty) t |
|
77 end |
|
78 | Const (@{const_name "Ex"}, ty) $ (t as Abs (x, T, _)) => |
|
79 let |
|
80 val ty1 = domain_type ty |
|
81 val ty2 = domain_type ty1 |
|
82 val rrel = tyRel T rty rel lthy |
|
83 in |
|
84 if (needs_lift rty T) then |
|
85 (mk_bex ty1) $ (mk_resp ty2 $ rrel) $ (apply_subt (my_reg lthy rel rty) t) |
|
86 else |
|
87 Const (@{const_name "Ex"}, ty) $ apply_subt (my_reg lthy rel rty) t |
|
88 end |
|
89 | Const (@{const_name "op ="}, ty) $ t => |
|
90 if needs_lift rty (fastype_of t) then |
|
91 (tyRel (fastype_of t) rty rel lthy) $ t (* FIXME: t should be regularised too *) |
|
92 else Const (@{const_name "op ="}, ty) $ (my_reg lthy rel rty t) |
|
93 | t1 $ t2 => (my_reg lthy rel rty t1) $ (my_reg lthy rel rty t2) |
|
94 | _ => trm |
|
95 *} |
|
96 |
|
97 (* For polymorphic types we need to find the type of the Relation term. *) |
|
98 (* TODO: we assume that the relation is a Constant. Is this always true? *) |
|
99 ML {* |
|
100 fun my_reg_inst lthy rel rty trm = |
|
101 case rel of |
|
102 Const (n, _) => Syntax.check_term lthy |
|
103 (my_reg lthy (Const (n, dummyT)) (Logic.varifyT rty) trm) |
|
104 *} |
|
105 |
|
106 (* |
|
107 ML {* |
|
108 val r = Free ("R", dummyT); |
|
109 val t = (my_reg_inst @{context} r @{typ "'a list"} @{term "\<forall>(x::'b list). P x"}); |
|
110 val t2 = Syntax.check_term @{context} t; |
|
111 cterm_of @{theory} t2 |
|
112 *} |
|
113 *) |
|
114 |
|
115 text {* Assumes that the given theorem is atomized *} |
|
116 ML {* |
|
117 fun build_regularize_goal thm rty rel lthy = |
|
118 Logic.mk_implies |
|
119 ((prop_of thm), |
|
120 (my_reg_inst lthy rel rty (prop_of thm))) |
|
121 *} |
|
122 |
|
123 ML {* |
|
124 fun regularize thm rty rel rel_eqv rel_refl lthy = |
|
125 let |
|
126 val goal = build_regularize_goal thm rty rel lthy; |
|
127 fun tac ctxt = |
|
128 (ObjectLogic.full_atomize_tac) THEN' |
|
129 REPEAT_ALL_NEW (FIRST' [ |
|
130 rtac rel_refl, |
|
131 atac, |
|
132 rtac @{thm universal_twice}, |
|
133 (rtac @{thm impI} THEN' atac), |
|
134 rtac @{thm implication_twice}, |
|
135 EqSubst.eqsubst_tac ctxt [0] |
|
136 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
137 (@{thm equiv_res_exists} OF [rel_eqv])], |
|
138 (* For a = b \<longrightarrow> a \<approx> b *) |
|
139 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
140 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
141 ]); |
|
142 val cthm = Goal.prove lthy [] [] goal |
|
143 (fn {context, ...} => tac context 1); |
|
144 in |
|
145 cthm OF [thm] |
|
146 end |
|
147 *} |
|
148 |
|
149 (*consts Rl :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" |
|
150 axioms Rl_eq: "EQUIV Rl" |
|
151 |
|
152 quotient ql = "'a list" / "Rl" |
|
153 by (rule Rl_eq) |
|
154 ML {* |
|
155 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "'a list"}) (Logic.varifyT @{typ "'a ql"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}); |
|
156 ctyp_of @{theory} (exchange_ty @{context} (Logic.varifyT @{typ "nat \<times> nat"}) (Logic.varifyT @{typ "int"}) @{typ "nat list \<Rightarrow> (nat \<times> nat) list"}) |
|
157 *} |
|
158 *) |
|
159 |
|
160 ML {* |
|
161 (* returns all subterms where two types differ *) |
|
162 fun diff (T, S) Ds = |
|
163 case (T, S) of |
|
164 (TVar v, TVar u) => if v = u then Ds else (T, S)::Ds |
|
165 | (TFree x, TFree y) => if x = y then Ds else (T, S)::Ds |
|
166 | (Type (a, Ts), Type (b, Us)) => |
|
167 if a = b then diffs (Ts, Us) Ds else (T, S)::Ds |
|
168 | _ => (T, S)::Ds |
|
169 and diffs (T::Ts, U::Us) Ds = diffs (Ts, Us) (diff (T, U) Ds) |
|
170 | diffs ([], []) Ds = Ds |
|
171 | diffs _ _ = error "Unequal length of type arguments" |
|
172 |
|
173 *} |
|
174 |
|
175 ML {* |
|
176 fun build_repabs_term lthy thm consts rty qty = |
|
177 let |
|
178 (* TODO: The rty and qty stored in the quotient_info should |
|
179 be varified, so this will soon not be needed *) |
|
180 val rty = Logic.varifyT rty; |
|
181 val qty = Logic.varifyT qty; |
|
182 |
|
183 fun mk_abs tm = |
|
184 let |
|
185 val ty = fastype_of tm |
|
186 in Syntax.check_term lthy ((get_fun_OLD absF (rty, qty) lthy ty) $ tm) end |
|
187 fun mk_repabs tm = |
|
188 let |
|
189 val ty = fastype_of tm |
|
190 in Syntax.check_term lthy ((get_fun_OLD repF (rty, qty) lthy ty) $ (mk_abs tm)) end |
|
191 |
|
192 fun is_lifted_const (Const (x, _)) = member (op =) consts x |
|
193 | is_lifted_const _ = false; |
|
194 |
|
195 fun build_aux lthy tm = |
|
196 case tm of |
|
197 Abs (a as (_, vty, _)) => |
|
198 let |
|
199 val (vs, t) = Term.dest_abs a; |
|
200 val v = Free(vs, vty); |
|
201 val t' = lambda v (build_aux lthy t) |
|
202 in |
|
203 if (not (needs_lift rty (fastype_of tm))) then t' |
|
204 else mk_repabs ( |
|
205 if not (needs_lift rty vty) then t' |
|
206 else |
|
207 let |
|
208 val v' = mk_repabs v; |
|
209 (* TODO: I believe 'beta' is not needed any more *) |
|
210 val t1 = (* Envir.beta_norm *) (t' $ v') |
|
211 in |
|
212 lambda v t1 |
|
213 end) |
|
214 end |
|
215 | x => |
|
216 case Term.strip_comb tm of |
|
217 (Const(@{const_name Respects}, _), _) => tm |
|
218 | (opp, tms0) => |
|
219 let |
|
220 val tms = map (build_aux lthy) tms0 |
|
221 val ty = fastype_of tm |
|
222 in |
|
223 if (is_lifted_const opp andalso needs_lift rty ty) then |
|
224 mk_repabs (list_comb (opp, tms)) |
|
225 else if ((Term.is_Free opp) andalso (length tms > 0) andalso (needs_lift rty ty)) then |
|
226 mk_repabs (list_comb (opp, tms)) |
|
227 else if tms = [] then opp |
|
228 else list_comb(opp, tms) |
|
229 end |
|
230 in |
|
231 repeat_eqsubst_prop lthy @{thms id_def_sym} |
|
232 (build_aux lthy (Thm.prop_of thm)) |
|
233 end |
|
234 *} |
|
235 |
|
236 text {* Builds provable goals for regularized theorems *} |
|
237 ML {* |
|
238 fun build_repabs_goal ctxt thm cons rty qty = |
|
239 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) |
|
240 *} |
|
241 |
|
242 ML {* |
|
243 fun repabs lthy thm consts rty qty quot_thm reflex_thm trans_thm rsp_thms = |
|
244 let |
|
245 val rt = build_repabs_term lthy thm consts rty qty; |
|
246 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
|
247 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
|
248 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
|
249 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
|
250 in |
|
251 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
|
252 end |
|
253 *} |
|
254 |
|
255 |
|
256 (* TODO: Check if it behaves properly with varifyed rty *) |
|
257 ML {* |
|
258 fun findabs_all rty tm = |
|
259 case tm of |
|
260 Abs(_, T, b) => |
|
261 let |
|
262 val b' = subst_bound ((Free ("x", T)), b); |
|
263 val tys = findabs_all rty b' |
|
264 val ty = fastype_of tm |
|
265 in if needs_lift rty ty then (ty :: tys) else tys |
|
266 end |
|
267 | f $ a => (findabs_all rty f) @ (findabs_all rty a) |
|
268 | _ => []; |
|
269 fun findabs rty tm = distinct (op =) (findabs_all rty tm) |
|
270 *} |
|
271 |
|
272 |
|
273 (* Currently useful only for LAMBDA_PRS *) |
|
274 ML {* |
|
275 fun make_simp_prs_thm lthy quot_thm thm typ = |
|
276 let |
|
277 val (_, [lty, rty]) = dest_Type typ; |
|
278 val thy = ProofContext.theory_of lthy; |
|
279 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
280 val inst = [SOME lcty, NONE, SOME rcty]; |
|
281 val lpi = Drule.instantiate' inst [] thm; |
|
282 val tac = |
|
283 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
|
284 (quotient_tac quot_thm); |
|
285 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
286 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
|
287 in |
|
288 MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t |
|
289 end |
|
290 *} |
|
291 |
|
292 ML {* |
|
293 fun findallex_all rty qty tm = |
|
294 case tm of |
|
295 Const (@{const_name All}, T) $ (s as (Abs(_, _, b))) => |
|
296 let |
|
297 val (tya, tye) = findallex_all rty qty s |
|
298 in if needs_lift rty T then |
|
299 ((T :: tya), tye) |
|
300 else (tya, tye) end |
|
301 | Const (@{const_name Ex}, T) $ (s as (Abs(_, _, b))) => |
|
302 let |
|
303 val (tya, tye) = findallex_all rty qty s |
|
304 in if needs_lift rty T then |
|
305 (tya, (T :: tye)) |
|
306 else (tya, tye) end |
|
307 | Abs(_, T, b) => |
|
308 findallex_all rty qty (subst_bound ((Free ("x", T)), b)) |
|
309 | f $ a => |
|
310 let |
|
311 val (a1, e1) = findallex_all rty qty f; |
|
312 val (a2, e2) = findallex_all rty qty a; |
|
313 in (a1 @ a2, e1 @ e2) end |
|
314 | _ => ([], []); |
|
315 *} |
|
316 |
|
317 ML {* |
|
318 fun findallex lthy rty qty tm = |
|
319 let |
|
320 val (a, e) = findallex_all rty qty tm; |
|
321 val (ad, ed) = (map domain_type a, map domain_type e); |
|
322 val (au, eu) = (distinct (op =) ad, distinct (op =) ed); |
|
323 val (rty, qty) = (Logic.varifyT rty, Logic.varifyT qty) |
|
324 in |
|
325 (map (exchange_ty lthy rty qty) au, map (exchange_ty lthy rty qty) eu) |
|
326 end |
|
327 *} |
|
328 |
|
329 ML {* |
|
330 fun make_allex_prs_thm lthy quot_thm thm typ = |
|
331 let |
|
332 val (_, [lty, rty]) = dest_Type typ; |
|
333 val thy = ProofContext.theory_of lthy; |
|
334 val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) |
|
335 val inst = [NONE, SOME lcty]; |
|
336 val lpi = Drule.instantiate' inst [] thm; |
|
337 val tac = |
|
338 (compose_tac (false, lpi, 1)) THEN_ALL_NEW |
|
339 (quotient_tac quot_thm); |
|
340 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
341 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
|
342 val t_noid = MetaSimplifier.rewrite_rule |
|
343 [@{thm eq_reflection} OF @{thms id_apply}] t; |
|
344 val t_sym = @{thm "HOL.sym"} OF [t_noid]; |
|
345 val t_eq = @{thm "eq_reflection"} OF [t_sym] |
|
346 in |
|
347 t_eq |
|
348 end |
|
349 *} |
|
350 |
|
351 ML {* |
|
352 fun lift_thm lthy qty qty_name rsp_thms defs rthm = |
|
353 let |
|
354 val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm)) |
|
355 |
|
356 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
|
357 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
|
358 val consts = lookup_quot_consts defs; |
|
359 val t_a = atomize_thm rthm; |
|
360 |
|
361 val _ = tracing ("raw atomized theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) |
|
362 |
|
363 val t_r = regularize t_a rty rel rel_eqv rel_refl lthy; |
|
364 |
|
365 val _ = tracing ("regularised theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) |
|
366 |
|
367 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
|
368 |
|
369 val _ = tracing ("rep/abs injected theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_t)) |
|
370 |
|
371 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
|
372 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
|
373 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
|
374 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
|
375 |
|
376 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_a)) |
|
377 |
|
378 val abs = findabs rty (prop_of t_a); |
|
379 val aps = findaps rty (prop_of t_a); |
|
380 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
|
381 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
|
382 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
|
383 |
|
384 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_l)) |
|
385 |
|
386 val defs_sym = flat (map (add_lower_defs lthy) defs); |
|
387 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
|
388 val t_id = simp_ids lthy t_l; |
|
389 |
|
390 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_id)) |
|
391 |
|
392 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
|
393 |
|
394 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d0)) |
|
395 |
|
396 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
|
397 |
|
398 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_d)) |
|
399 |
|
400 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
|
401 |
|
402 val _ = tracing ("??:\n" ^ Syntax.string_of_term lthy (prop_of t_r)) |
|
403 |
|
404 val t_rv = ObjectLogic.rulify t_r |
|
405 |
|
406 val _ = tracing ("lifted theorem:\n" ^ Syntax.string_of_term lthy (prop_of t_rv)) |
|
407 in |
|
408 Thm.varifyT t_rv |
|
409 end |
|
410 *} |
|
411 |
|
412 ML {* |
|
413 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = |
|
414 let |
|
415 val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; |
|
416 val (_, lthy2) = note (name, lifted_thm) lthy; |
|
417 in |
|
418 lthy2 |
|
419 end |
|
420 *} |
|
421 |
|
422 |
|
423 ML {* |
|
424 fun regularize_goal lthy thm rel_eqv rel_refl qtrm = |
|
425 let |
|
426 val reg_trm = mk_REGULARIZE_goal lthy (prop_of thm) qtrm; |
|
427 fun tac lthy = regularize_tac lthy rel_eqv rel_refl; |
|
428 val cthm = Goal.prove lthy [] [] reg_trm |
|
429 (fn {context, ...} => tac context 1); |
|
430 in |
|
431 cthm OF [thm] |
|
432 end |
|
433 *} |
|
434 |
|
435 ML {* |
|
436 fun repabs_goal lthy thm rty quot_thm reflex_thm trans_thm rsp_thms qtrm = |
|
437 let |
|
438 val rg = Syntax.check_term lthy (mk_inj_REPABS_goal lthy ((prop_of thm), qtrm)); |
|
439 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
|
440 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
|
441 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
|
442 in |
|
443 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
|
444 end |
|
445 *} |
|
446 |
|
447 ML {* |
|
448 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
|
449 let |
|
450 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
|
451 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
|
452 val t_a = atomize_thm rthm; |
|
453 val goal_a = atomize_goal (ProofContext.theory_of lthy) goal; |
|
454 val t_r = regularize_goal lthy t_a rel_eqv rel_refl goal_a; |
|
455 val t_t = repabs_goal lthy t_r rty quot rel_refl trans2 rsp_thms goal_a; |
|
456 val (alls, exs) = findallex lthy rty qty (prop_of t_a); |
|
457 val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls |
|
458 val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs |
|
459 val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t |
|
460 val abs = findabs rty (prop_of t_a); |
|
461 val aps = findaps rty (prop_of t_a); |
|
462 val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; |
|
463 val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; |
|
464 val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; |
|
465 val defs_sym = flat (map (add_lower_defs lthy) defs); |
|
466 val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; |
|
467 val t_id = simp_ids lthy t_l; |
|
468 val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; |
|
469 val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; |
|
470 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
|
471 val t_rv = ObjectLogic.rulify t_r |
|
472 in |
|
473 Thm.varifyT t_rv |
|
474 end |
|
475 *} |
|
476 |
|
477 ML {* |
|
478 fun lift_thm_goal_note lthy qty qty_name rsp_thms defs thm name goal = |
|
479 let |
|
480 val lifted_thm = lift_thm_goal lthy qty qty_name rsp_thms defs thm goal; |
|
481 val (_, lthy2) = note (name, lifted_thm) lthy; |
|
482 in |
|
483 lthy2 |
|
484 end |
|
485 *} |
|
486 |