213 in |
213 in |
214 EVERY1 [rtac rule, rtac rthm'] |
214 EVERY1 [rtac rule, rtac rthm'] |
215 end) |
215 end) |
216 *} |
216 *} |
217 |
217 |
|
218 ML {* |
|
219 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
|
220 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
|
221 *} |
|
222 |
|
223 (* FIXME: allex_prs and lambda_prs can be one function *) |
|
224 |
|
225 ML {* |
|
226 fun allex_prs_tac lthy quot = |
|
227 (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]}) |
|
228 THEN' (quotient_tac quot); |
|
229 *} |
|
230 |
|
231 ML {* |
|
232 fun lambda_prs_tac lthy quot = |
|
233 (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} |
|
234 THEN' (RANGE [quotient_tac quot, quotient_tac quot])); |
|
235 *} |
|
236 |
|
237 ML {* |
|
238 fun clean_tac lthy quot defs reps_same = |
|
239 let |
|
240 val lower = flat (map (add_lower_defs lthy) defs) |
|
241 in |
|
242 (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' |
|
243 (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' |
|
244 (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' |
|
245 (simp_tac (HOL_ss addsimps [reps_same])) |
|
246 end |
|
247 *} |
|
248 |
218 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
249 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)" |
219 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
250 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *}) |
220 thm FORALL_PRS |
251 apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
221 prefer 3 |
252 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
222 (* phase 1 *) |
253 apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *}) |
223 apply(subst FORALL_PRS[symmetric]) |
254 done |
224 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
255 |
225 apply(subst FORALL_PRS[symmetric]) |
256 apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
226 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
257 apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) |
227 apply(subst FORALL_PRS[symmetric]) |
|
228 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
229 apply(subst LAMBDA_PRS) |
|
230 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
231 apply(fold id_def) |
|
232 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
233 apply(subst LAMBDA_PRS) |
|
234 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
235 apply(fold id_def) |
|
236 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
237 apply(subst LAMBDA_PRS) |
|
238 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
239 apply(fold id_def) |
|
240 apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *}) |
|
241 (* phase 2 *) |
258 (* phase 2 *) |
242 ML_prf {* |
259 ML_prf {* |
243 val lower = add_lower_defs @{context} @{thm PLUS_def} |
260 val lower = add_lower_defs @{context} @{thm PLUS_def} |
244 *} |
261 *} |
245 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
262 apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*}) |
246 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
263 apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
247 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
264 done |
248 apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*}) |
|
249 (* phase 3 *) |
|
250 apply(subst QUOT_TYPE_I_my_int.REPS_same) |
|
251 apply(rule refl) |
|
252 |
|
253 |
265 |
254 |
266 |
255 |
267 |
256 (* |
268 (* |
257 does not work. |
269 does not work. |