equal
deleted
inserted
replaced
228 in |
228 in |
229 MetaSimplifier.rewrite_rule thms thm |
229 MetaSimplifier.rewrite_rule thms thm |
230 end |
230 end |
231 *} |
231 *} |
232 |
232 |
233 section {* Does the same as 'subst' in a given theorem *} |
233 section {* Debugging infrastructure for testing tactics *} |
234 |
234 |
|
235 ML {* |
|
236 fun my_print_tac ctxt s thm = |
|
237 let |
|
238 val prems_str = prems_of thm |
|
239 |> map (Syntax.string_of_term ctxt) |
|
240 |> cat_lines |
|
241 val _ = tracing (s ^ "\n" ^ prems_str) |
|
242 in |
|
243 Seq.single thm |
|
244 end |
|
245 |
|
246 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
|
247 *} |
|
248 |
|
249 section {* Infrastructure about definitions *} |
|
250 |
|
251 (* Does the same as 'subst' in a given theorem *) |
235 ML {* |
252 ML {* |
236 fun eqsubst_thm ctxt thms thm = |
253 fun eqsubst_thm ctxt thms thm = |
237 let |
254 let |
238 val goalstate = Goal.init (Thm.cprop_of thm) |
255 val goalstate = Goal.init (Thm.cprop_of thm) |
239 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
256 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
246 in |
263 in |
247 @{thm equal_elim_rule1} OF [rt, thm] |
264 @{thm equal_elim_rule1} OF [rt, thm] |
248 end |
265 end |
249 *} |
266 *} |
250 |
267 |
251 section {* Infrastructure about definitions *} |
|
252 |
|
253 (* expects atomized definitions *) |
268 (* expects atomized definitions *) |
254 ML {* |
269 ML {* |
255 fun add_lower_defs_aux lthy thm = |
270 fun add_lower_defs_aux lthy thm = |
256 let |
271 let |
257 val e1 = @{thm fun_cong} OF [thm]; |
272 val e1 = @{thm fun_cong} OF [thm]; |
272 in |
287 in |
273 map Thm.varifyT defs_all |
288 map Thm.varifyT defs_all |
274 end |
289 end |
275 *} |
290 *} |
276 |
291 |
277 section {* Infrastructure for collecting theorems for calling lifting *} |
292 section {* Infrastructure for collecting theorems for starting the lifting *} |
278 |
293 |
279 ML {* |
294 ML {* |
280 fun lookup_quot_data lthy qty = |
295 fun lookup_quot_data lthy qty = |
281 let |
296 let |
282 val qty_name = fst (dest_Type qty) |
297 val qty_name = fst (dest_Type qty) |
359 else let |
374 else let |
360 val SOME qinfo = quotdata_lookup_thy thy s' |
375 val SOME qinfo = quotdata_lookup_thy thy s' |
361 (* FIXME: check in this case that the rty and qty *) |
376 (* FIXME: check in this case that the rty and qty *) |
362 (* FIXME: correspond to each other *) |
377 (* FIXME: correspond to each other *) |
363 val (s, _) = dest_Const (#rel qinfo) |
378 val (s, _) = dest_Const (#rel qinfo) |
364 (* FIXME: the relation should only be the string *) |
379 (* FIXME: the relation should only be the string *) |
365 (* FIXME: and the type needs to be calculated as below *) |
380 (* FIXME: and the type needs to be calculated as below; *) |
|
381 (* FIXME: maybe one should actually have a term *) |
|
382 (* FIXME: and one needs to force it to have this type *) |
366 in |
383 in |
367 Const (s, rty --> rty --> @{typ bool}) |
384 Const (s, rty --> rty --> @{typ bool}) |
368 end |
385 end |
369 | _ => HOLogic.eq_const dummyT |
386 | _ => HOLogic.eq_const dummyT |
370 (* FIXME: check that the types correspond to each other? *) |
387 (* FIXME: check that the types correspond to each other? *) |
452 | (rt, qt) => |
469 | (rt, qt) => |
453 raise (LIFT_MATCH "regularize (default)") |
470 raise (LIFT_MATCH "regularize (default)") |
454 *} |
471 *} |
455 |
472 |
456 (* |
473 (* |
|
474 FIXME / TODO: needs to be adapted |
|
475 |
457 To prove that the raw theorem implies the regularised one, |
476 To prove that the raw theorem implies the regularised one, |
458 we try in order: |
477 we try in order: |
459 |
478 |
460 - Reflexivity of the relation |
479 - Reflexivity of the relation |
461 - Assumption |
480 - Assumption |
476 assumes b: "b \<longrightarrow> d" |
495 assumes b: "b \<longrightarrow> d" |
477 shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
496 shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
478 using a b by auto |
497 using a b by auto |
479 |
498 |
480 (* version of regularize_tac including debugging information *) |
499 (* version of regularize_tac including debugging information *) |
481 ML {* |
|
482 fun my_print_tac ctxt s thm = |
|
483 let |
|
484 val prems_str = prems_of thm |
|
485 |> map (Syntax.string_of_term ctxt) |
|
486 |> cat_lines |
|
487 val _ = tracing (s ^ "\n" ^ prems_str) |
|
488 in |
|
489 Seq.single thm |
|
490 end |
|
491 |
|
492 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))] |
|
493 *} |
|
494 |
|
495 ML {* |
500 ML {* |
496 fun regularize_tac ctxt rel_eqv rel_refl = |
501 fun regularize_tac ctxt rel_eqv rel_refl = |
497 (ObjectLogic.full_atomize_tac) THEN' |
502 (ObjectLogic.full_atomize_tac) THEN' |
498 REPEAT_ALL_NEW (FIRST' |
503 REPEAT_ALL_NEW (FIRST' |
499 [(K (print_tac "start")) THEN' (K no_tac), |
504 [(K (print_tac "start")) THEN' (K no_tac), |