equal
deleted
inserted
replaced
|
1 ML {* |
|
2 fun repeat_eqsubst_thm ctxt thms thm = |
|
3 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) |
|
4 handle _ => thm |
|
5 *} |
|
6 |
|
7 |
|
8 ML {* |
|
9 fun eqsubst_prop ctxt thms t = |
|
10 let |
|
11 val goalstate = Goal.init (cterm_of (ProofContext.theory_of ctxt) t) |
|
12 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
13 NONE => error "eqsubst_prop" |
|
14 | SOME th => cprem_of th 1 |
|
15 in term_of a' end |
|
16 *} |
|
17 |
|
18 ML {* |
|
19 fun repeat_eqsubst_prop ctxt thms t = |
|
20 repeat_eqsubst_prop ctxt thms (eqsubst_prop ctxt thms t) |
|
21 handle _ => t |
|
22 *} |
|
23 |
1 |
24 |
2 text {* tyRel takes a type and builds a relation that a quantifier over this |
25 text {* tyRel takes a type and builds a relation that a quantifier over this |
3 type needs to respect. *} |
26 type needs to respect. *} |
4 ML {* |
27 ML {* |
5 fun tyRel ty rty rel lthy = |
28 fun tyRel ty rty rel lthy = |
442 in |
465 in |
443 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
466 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
444 end |
467 end |
445 *} |
468 *} |
446 |
469 |
|
470 |
|
471 ML {* |
|
472 fun atomize_goal thy gl = |
|
473 let |
|
474 val vars = map Free (Term.add_frees gl []); |
|
475 val all = if fastype_of gl = @{typ bool} then HOLogic.all_const else Term.all; |
|
476 fun lambda_all (var as Free(_, T)) trm = (all T) $ lambda var trm; |
|
477 val glv = fold lambda_all vars gl |
|
478 val gla = (term_of o snd o Thm.dest_equals o cprop_of) (ObjectLogic.atomize (cterm_of thy glv)) |
|
479 val glf = Type.legacy_freeze gla |
|
480 in |
|
481 if fastype_of gl = @{typ bool} then @{term Trueprop} $ glf else glf |
|
482 end |
|
483 *} |
|
484 |
|
485 |
|
486 ML {* atomize_goal @{theory} @{term "x memb [] = False"} *} |
|
487 ML {* atomize_goal @{theory} @{term "x = xa ⟹ a # x = a # xa"} *} |
|
488 |
|
489 |
|
490 |
447 ML {* |
491 ML {* |
448 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
492 fun lift_thm_goal lthy qty qty_name rsp_thms defs rthm goal = |
449 let |
493 let |
450 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty; |
494 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; |
495 val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name; |
482 in |
526 in |
483 lthy2 |
527 lthy2 |
484 end |
528 end |
485 *} |
529 *} |
486 |
530 |
|
531 ML {* |
|
532 fun simp_ids_trm trm = |
|
533 trm |> |
|
534 MetaSimplifier.rewrite false @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id} |
|
535 |> cprop_of |> Thm.dest_equals |> snd |
|
536 |
|
537 *} |