equal
deleted
inserted
replaced
8 val quotient_tac: Proof.context -> int -> tactic |
8 val quotient_tac: Proof.context -> int -> tactic |
9 end; |
9 end; |
10 |
10 |
11 structure Quotient_Tacs: QUOTIENT_TACS = |
11 structure Quotient_Tacs: QUOTIENT_TACS = |
12 struct |
12 struct |
|
13 |
|
14 open Quotient_Info; |
|
15 open Quotient_Type; |
|
16 open Quotient_Term; |
|
17 |
13 |
18 |
14 (* Since HOL_basic_ss is too "big" for us, *) |
19 (* Since HOL_basic_ss is too "big" for us, *) |
15 (* we need to set up our own minimal simpset. *) |
20 (* we need to set up our own minimal simpset. *) |
16 fun mk_minimal_ss ctxt = |
21 fun mk_minimal_ss ctxt = |
17 Simplifier.context ctxt empty_ss |
22 Simplifier.context ctxt empty_ss |
561 val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, |
566 val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, |
562 "", "does not match with original theorem", rtrm_str] |
567 "", "does not match with original theorem", rtrm_str] |
563 in |
568 in |
564 error msg |
569 error msg |
565 end |
570 end |
566 |
|
567 open Quotient_Term; |
|
568 |
571 |
569 fun procedure_inst ctxt rtrm qtrm = |
572 fun procedure_inst ctxt rtrm qtrm = |
570 let |
573 let |
571 val thy = ProofContext.theory_of ctxt |
574 val thy = ProofContext.theory_of ctxt |
572 val rtrm' = HOLogic.dest_Trueprop rtrm |
575 val rtrm' = HOLogic.dest_Trueprop rtrm |
613 THEN' RANGE_WARN |
616 THEN' RANGE_WARN |
614 [(regularize_tac ctxt, msg1), |
617 [(regularize_tac ctxt, msg1), |
615 (all_inj_repabs_tac ctxt, msg2), |
618 (all_inj_repabs_tac ctxt, msg2), |
616 (clean_tac ctxt, msg3)] |
619 (clean_tac ctxt, msg3)] |
617 |
620 |
618 |
621 end; (* structure *) |
619 |
|
620 end; |
|