equal
deleted
inserted
replaced
738 | (Free (_, T), Free (_, T')) => |
738 | (Free (_, T), Free (_, T')) => |
739 if T = T' |
739 if T = T' |
740 then rtrm |
740 then rtrm |
741 else mk_repabs lthy (T, T') rtrm |
741 else mk_repabs lthy (T, T') rtrm |
742 |
742 |
743 | (Const (_, T), Const (_, T')) => |
743 | (_, Const (@{const_name "op ="}, _)) => rtrm |
744 if T = T' |
744 |
|
745 (* FIXME: check here that rtrm is the corresponding definition for teh const *) |
|
746 | (_, Const (_, T')) => |
|
747 let |
|
748 val rty = fastype_of rtrm |
|
749 in |
|
750 if rty = T' |
745 then rtrm |
751 then rtrm |
746 else mk_repabs lthy (T, T') rtrm |
752 else mk_repabs lthy (rty, T') rtrm |
747 |
753 end |
748 | (_, Const (@{const_name "op ="}, _)) => rtrm |
|
749 |
754 |
750 | _ => raise (LIFT_MATCH "injection") |
755 | _ => raise (LIFT_MATCH "injection") |
751 *} |
756 *} |
752 |
757 |
753 section {* RepAbs Injection Tactic *} |
758 section {* RepAbs Injection Tactic *} |
769 ML {* |
774 ML {* |
770 fun quotient_tac ctxt = |
775 fun quotient_tac ctxt = |
771 REPEAT_ALL_NEW (FIRST' |
776 REPEAT_ALL_NEW (FIRST' |
772 [rtac @{thm identity_quotient}, |
777 [rtac @{thm identity_quotient}, |
773 resolve_tac (quotient_rules_get ctxt)]) |
778 resolve_tac (quotient_rules_get ctxt)]) |
|
779 *} |
|
780 |
|
781 (* solver for the simplifier *) |
|
782 ML {* |
|
783 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
784 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
774 *} |
785 *} |
775 |
786 |
776 definition |
787 definition |
777 "QUOT_TRUE x \<equiv> True" |
788 "QUOT_TRUE x \<equiv> True" |
778 |
789 |
1094 The second one is an EqSubst (slow). |
1105 The second one is an EqSubst (slow). |
1095 The rest are a simp_tac and are fast. |
1106 The rest are a simp_tac and are fast. |
1096 *) |
1107 *) |
1097 |
1108 |
1098 ML {* |
1109 ML {* |
1099 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
1100 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
1101 *} |
|
1102 |
|
1103 ML {* |
|
1104 fun clean_tac lthy = |
1110 fun clean_tac lthy = |
1105 let |
1111 let |
1106 val thy = ProofContext.theory_of lthy; |
1112 val thy = ProofContext.theory_of lthy; |
1107 val defs = map (Thm.varifyT o #def) (qconsts_dest thy) |
1113 val defs = map (Thm.varifyT o #def) (qconsts_dest thy) |
1108 val thms1 = @{thms all_prs ex_prs} |
1114 val thms1 = @{thms all_prs ex_prs} |