159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
159 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
160 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
161 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
162 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
163 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
164 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) (***) |
165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
165 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
166 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
167 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
168 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
169 apply(tactic {* r_mk_comb_tac_intex @{context} 1*}) |
234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
234 ML_prf {* val aps = find_aps (prop_of (atomize_thm @{thm plus_sym_pre})) (term_of qtm) *} |
235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
235 apply(tactic {* clean_tac @{context} [quot] defs aps 1 *}) |
236 done |
236 done |
237 |
237 |
238 |
238 |
239 (* |
|
240 |
|
241 ML {* |
|
242 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
|
243 (REPEAT1 o FIRST1) |
|
244 [(K (print_tac "start")) THEN' (K no_tac), |
|
245 DT ctxt "1" (rtac trans_thm), |
|
246 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
|
247 DT ctxt "3" (ball_rsp_tac ctxt), |
|
248 DT ctxt "4" (bex_rsp_tac ctxt), |
|
249 DT ctxt "5" (FIRST' (map rtac rsp_thms)), |
|
250 DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
251 DT ctxt "7" (rtac refl), |
|
252 DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
253 DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}), |
|
254 DT ctxt "A" (rtac @{thm ext}), |
|
255 DT ctxt "B" (rtac reflex_thm), |
|
256 DT ctxt "C" (atac), |
|
257 DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))), |
|
258 DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt), |
|
259 DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))] |
|
260 *} |
|
261 |
|
262 ML {* |
|
263 inj_repabs_trm @{context} (reg_atrm, aqtrm) |
|
264 |> Syntax.check_term @{context} |
|
265 *} |
|
266 |
|
267 |
|
268 ML {* val my_goal = cterm_of @{theory} (mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm)) *} |
|
269 ML {* val yr_goal = cterm_of @{theory} (build_repabs_goal @{context} (@{thm testtest} OF [arthm]) consts rty qty) *} |
|
270 |
|
271 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *} |
|
272 apply(tactic {* ObjectLogic.full_atomize_tac 1 *}) |
|
273 apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) |
|
274 done |
|
275 |
|
276 ML {* |
|
277 inj_repabs_trm @{context} (reg_atrm, aqtrm) |
|
278 |> Syntax.string_of_term @{context} |
|
279 |> writeln |
|
280 *} |
|
281 |
|
282 *) |
|
283 |
|
284 |
|