equal
deleted
inserted
replaced
13 val clean_tac: Proof.context -> int -> tactic |
13 val clean_tac: Proof.context -> int -> tactic |
14 val procedure_tac: Proof.context -> thm -> int -> tactic |
14 val procedure_tac: Proof.context -> thm -> int -> tactic |
15 val lift_tac: Proof.context -> thm list -> int -> tactic |
15 val lift_tac: Proof.context -> thm list -> int -> tactic |
16 val quotient_tac: Proof.context -> int -> tactic |
16 val quotient_tac: Proof.context -> int -> tactic |
17 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic |
17 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic |
18 val lifted_attr: attribute |
18 val lifted_attrib: attribute |
19 end; |
19 end; |
20 |
20 |
21 structure Quotient_Tacs: QUOTIENT_TACS = |
21 structure Quotient_Tacs: QUOTIENT_TACS = |
22 struct |
22 struct |
23 |
23 |
646 in |
646 in |
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 (* The attribute *) |
651 (* An Attribute *) |
652 fun lifted_attr_pre ctxt thm = |
652 (* FIXME: Logic.unvarify needs to be replaced by propper Isar constructions *) |
653 let |
653 fun lifted_attrib_pre context thm = |
654 val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm |
654 let |
655 val glc = Syntax.check_term ctxt gl |
655 val ctxt = Context.proof_of context |
656 in |
656 val goal = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm |
657 (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1)) |
657 val goal_chk = Syntax.check_term ctxt goal |
|
658 val frees = Term.add_free_names goal_chk [] |
|
659 in |
|
660 Goal.prove ctxt frees [] goal_chk |
|
661 (fn x => lift_tac (#context x) [thm] 1) |
658 end; |
662 end; |
659 |
663 |
660 val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t) |
664 val lifted_attrib = Thm.rule_attribute lifted_attrib_pre |
661 |
665 |
662 end; (* structure *) |
666 end; (* structure *) |