equal
deleted
inserted
replaced
647 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
647 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
648 THEN' RANGE (map mk_tac rthms) |
648 THEN' RANGE (map mk_tac rthms) |
649 end |
649 end |
650 |
650 |
651 (* An Attribute which automatically constructs the qthm *) |
651 (* An Attribute which automatically constructs the qthm *) |
652 (* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *) |
|
653 fun lifted_attrib_aux context thm = |
652 fun lifted_attrib_aux context thm = |
654 let |
653 let |
655 val ctxt = Context.proof_of context |
654 val ctxt = Context.proof_of context |
656 val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm |
655 val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt |
657 val goal_chk = Syntax.check_term ctxt goal |
656 val goal = (quotient_lift_all ctxt o prop_of) thm' |
658 val frees = Term.add_free_names goal_chk [] |
657 val nthm = Goal.prove ctxt [] [] goal (fn x => lift_tac ctxt [thm] 1) |
659 in |
658 val [nthm1] = ProofContext.export ctxt' ctxt [nthm] |
660 Goal.prove ctxt frees [] goal_chk |
659 in |
661 (fn x => lift_tac (#context x) [thm] 1) |
660 nthm1 |
662 end; |
661 end; |
663 |
662 |
664 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux |
663 val lifted_attrib = Thm.rule_attribute lifted_attrib_aux |
665 |
664 |
666 end; (* structure *) |
665 end; (* structure *) |