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 |
656 in |
657 in |
657 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
658 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
658 THEN' RANGE (map mk_tac rthms) |
659 THEN' RANGE (map mk_tac rthms) |
659 end |
660 end |
660 |
661 |
|
662 (* The attribute *) |
|
663 fun lifted_attr_pre ctxt thm = |
|
664 let |
|
665 val gl = (quotient_lift_all ctxt o Logic.unvarify o prop_of) thm |
|
666 val glc = Syntax.check_term ctxt gl |
|
667 in |
|
668 (Goal.prove ctxt (Term.add_free_names glc []) [] glc (fn x => lift_tac (#context x) [thm] 1)) |
|
669 end; |
|
670 |
|
671 val lifted_attr = Thm.rule_attribute (fn ctxt => fn t => lifted_attr_pre (Context.proof_of ctxt) t) |
|
672 |
661 end; (* structure *) |
673 end; (* structure *) |