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 end; |
19 end; |
19 |
20 |
20 structure Quotient_Tacs: QUOTIENT_TACS = |
21 structure Quotient_Tacs: QUOTIENT_TACS = |
21 struct |
22 struct |
22 |
23 |
645 in |
646 in |
646 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
647 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
647 THEN' RANGE (map mk_tac rthms) |
648 THEN' RANGE (map mk_tac rthms) |
648 end |
649 end |
649 |
650 |
|
651 (* The attribute *) |
|
652 fun lifted_attr_pre ctxt thm = |
|
653 let |
|
654 val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm |
|
655 val glc = Syntax.check_term ctxt gl |
|
656 in |
|
657 (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1)) |
|
658 end; |
|
659 |
|
660 val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t) |
|
661 |
650 end; (* structure *) |
662 end; (* structure *) |