247 ML {* val reg_atrm = prop_of (@{thm testtest} OF [arthm]) *} |
247 ML {* val reg_atrm = prop_of (@{thm testtest} OF [arthm]) *} |
248 |
248 |
249 ML {* |
249 ML {* |
250 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
250 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
251 (REPEAT1 o FIRST1) |
251 (REPEAT1 o FIRST1) |
252 [rtac trans_thm, |
252 [(K (print_tac "start")) THEN' (K no_tac), |
253 LAMBDA_RES_TAC ctxt, |
253 DT ctxt "1" (rtac trans_thm), |
254 ball_rsp_tac ctxt, |
254 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
255 bex_rsp_tac ctxt, |
255 DT ctxt "3" (ball_rsp_tac ctxt), |
256 FIRST' (map rtac rsp_thms), |
256 DT ctxt "4" (bex_rsp_tac ctxt), |
257 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
257 DT ctxt "5" (FIRST' (map rtac rsp_thms)), |
258 rtac refl, |
258 DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
259 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
259 DT ctxt "7" (rtac refl), |
260 Cong_Tac.cong_tac @{thm cong}, |
260 DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
261 rtac @{thm ext}, |
261 DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}), |
262 rtac reflex_thm, |
262 DT ctxt "A" (rtac @{thm ext}), |
263 atac, |
263 DT ctxt "B" (rtac reflex_thm), |
264 SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})), |
264 DT ctxt "C" (atac), |
265 WEAK_LAMBDA_RES_TAC ctxt, |
265 DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
266 CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))] |
266 DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), |
|
267 DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] |
267 *} |
268 *} |
268 |
269 |
269 ML {* |
270 ML {* |
270 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
271 val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"} |
271 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
272 val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int" |
272 val consts = lookup_quot_consts defs |
273 val consts = lookup_quot_consts defs |
|
274 *} |
|
275 |
|
276 ML {* cprem_of *} |
|
277 |
|
278 ML {* |
|
279 (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) |
|
280 |> Syntax.check_term @{context}) |
273 *} |
281 *} |
274 |
282 |
275 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} |
283 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} |
276 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
284 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
277 (* does not work *) |
285 (* does not work *) |