1135 The first one is implemented as a conversion (fast). |
1135 The first one is implemented as a conversion (fast). |
1136 The second one is an EqSubst (slow). |
1136 The second one is an EqSubst (slow). |
1137 The rest are a simp_tac and are fast. |
1137 The rest are a simp_tac and are fast. |
1138 *) |
1138 *) |
1139 |
1139 |
|
1140 ML {* fun OF1 thm1 thm2 = thm2 RS thm1 *} |
|
1141 ML {* |
|
1142 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss) |
|
1143 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac |
|
1144 *} |
|
1145 |
1140 ML {* |
1146 ML {* |
1141 fun clean_tac lthy = |
1147 fun clean_tac lthy = |
1142 let |
1148 let |
1143 val thy = ProofContext.theory_of lthy; |
1149 val thy = ProofContext.theory_of lthy; |
1144 val quotients = quotient_rules_get lthy |
1150 val defs = map (Thm.varifyT o #def) (qconsts_dest thy) |
1145 val defs = map (Thm.varifyT o #def) (qconsts_dest thy); |
1151 val thms = @{thms eq_reflection[OF fun_map.simps]} |
1146 val absrep = map (fn x => @{thm Quotient_abs_rep} OF [x]) quotients |
1152 @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep} |
1147 val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quotients |
1153 @ defs |
1148 val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps |
1154 val simp_ctxt = HOL_basic_ss addsimps thms addSolver quotient_solver |
1149 (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ absrep @ reps_same @ defs) |
|
1150 in |
1155 in |
1151 EVERY' [ |
1156 EVERY' [ |
1152 (* (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) ----> f *) |
1157 (* (rep1 ---> abs2) (\<lambda>x. rep2 (f (abs1 x))) ----> f *) |
1153 (* \<forall>x\<in>Respects R. (abs ---> id) f ----> \<forall>x. f *) |
1158 (* Ball (Respects R) ((abs ---> id) f) ----> All f *) |
1154 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
1159 NDT lthy "a" (TRY o lambda_allex_prs_tac lthy), |
1155 |
1160 |
1156 (* NewConst ----> (rep ---> abs) oldConst *) |
1161 (* NewConst -----> (rep ---> abs) oldConst *) |
1157 (* Abs (Rep x) ----> x *) |
1162 (* abs (rep x) -----> x *) |
1158 (* id_simps; fun_map.simps *) |
1163 (* R (Rep x) (Rep y) -----> x = y *) |
|
1164 (* id_simps; fun_map.simps *) |
1159 NDT lthy "c" (TRY o simp_tac simp_ctxt), |
1165 NDT lthy "c" (TRY o simp_tac simp_ctxt), |
1160 |
1166 |
1161 (* final step *) |
1167 (* final step *) |
1162 NDT lthy "d" (TRY o rtac refl) |
1168 NDT lthy "d" (TRY o rtac refl) |
1163 ] |
1169 ] |