3 val regularize_tac: Proof.context -> int -> tactic |
3 val regularize_tac: Proof.context -> int -> tactic |
4 val injection_tac: Proof.context -> int -> tactic |
4 val injection_tac: Proof.context -> int -> tactic |
5 val all_injection_tac: Proof.context -> int -> tactic |
5 val all_injection_tac: Proof.context -> int -> tactic |
6 val clean_tac: Proof.context -> int -> tactic |
6 val clean_tac: Proof.context -> int -> tactic |
7 val procedure_tac: Proof.context -> thm -> int -> tactic |
7 val procedure_tac: Proof.context -> thm -> int -> tactic |
8 val lift_tac: Proof.context -> thm -> int -> tactic |
8 val lift_tac: Proof.context -> thm list -> int -> tactic |
9 val quotient_tac: Proof.context -> int -> tactic |
9 val quotient_tac: Proof.context -> int -> tactic |
10 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic |
10 val quot_true_tac: Proof.context -> (term -> term) -> int -> tactic |
11 end; |
11 end; |
12 |
12 |
13 structure Quotient_Tacs: QUOTIENT_TACS = |
13 structure Quotient_Tacs: QUOTIENT_TACS = |
610 end) |
610 end) |
611 |
611 |
612 |
612 |
613 (* Automatic Proofs *) |
613 (* Automatic Proofs *) |
614 |
614 |
615 val msg1 = "Regularize proof failed." |
615 val msg1 = "The regularize proof failed." |
616 val msg2 = cat_lines ["Injection proof failed.", |
616 val msg2 = cat_lines ["The injection proof failed.", |
617 "This is probably due to missing respects lemmas.", |
617 "This is probably due to missing respects lemmas.", |
618 "Try invoking the injection method manually to see", |
618 "Try invoking the injection method manually to see", |
619 "which lemmas are missing."] |
619 "which lemmas are missing."] |
620 val msg3 = "Cleaning proof failed." |
620 val msg3 = "The cleaning proof failed." |
621 |
621 |
622 fun lift_tac ctxt rthm = |
622 fun lift_tac ctxt rthms = |
623 procedure_tac ctxt rthm |
623 let |
624 THEN' RANGE_WARN |
624 fun mk_tac rthm = |
625 [(regularize_tac ctxt, msg1), |
625 procedure_tac ctxt rthm |
626 (all_injection_tac ctxt, msg2), |
626 THEN' RANGE_WARN |
627 (clean_tac ctxt, msg3)] |
627 [(regularize_tac ctxt, msg1), |
|
628 (all_injection_tac ctxt, msg2), |
|
629 (clean_tac ctxt, msg3)] |
|
630 in |
|
631 simp_tac (mk_minimal_ss ctxt) (* unfolding multiple &&& *) |
|
632 THEN' RANGE (map mk_tac rthms) |
|
633 end |
628 |
634 |
629 end; (* structure *) |
635 end; (* structure *) |