238 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
238 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
239 ]); |
239 ]); |
240 *} |
240 *} |
241 apply (tactic {* tac @{context} 1 *}) *) |
241 apply (tactic {* tac @{context} 1 *}) *) |
242 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
242 ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} |
|
243 ML {* |
|
244 val rt = build_repabs_term @{context} t_r consts rty qty |
|
245 val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); |
|
246 *} |
|
247 prove rg |
|
248 apply(atomize(full)) |
|
249 ML_prf {* |
|
250 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
|
251 (FIRST' [ |
|
252 rtac trans_thm, |
|
253 LAMBDA_RES_TAC ctxt, |
|
254 res_forall_rsp_tac ctxt, |
|
255 res_exists_rsp_tac ctxt, |
|
256 ( |
|
257 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
|
258 THEN_ALL_NEW (fn _ => no_tac) |
|
259 ), |
|
260 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
261 rtac refl, |
|
262 (* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) |
|
263 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
264 Cong_Tac.cong_tac @{thm cong}, |
|
265 rtac @{thm ext}, |
|
266 rtac reflex_thm, |
|
267 atac, |
|
268 ( |
|
269 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
270 THEN_ALL_NEW (fn _ => no_tac) |
|
271 ), |
|
272 WEAK_LAMBDA_RES_TAC ctxt |
|
273 ]); |
|
274 fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms |
|
275 *} |
|
276 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
277 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
278 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
279 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
280 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
281 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
282 prefer 2 |
|
283 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
284 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
285 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
286 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
287 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
288 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
289 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
290 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
291 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
292 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
293 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
294 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
295 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
296 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
297 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
298 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
299 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
300 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
301 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
302 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
303 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
304 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
305 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
306 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
307 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_lam @{context}) 1 *}) |
|
308 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
309 apply (tactic {* r_mk_comb_tac_lam @{context} 1 *}) |
|
310 |
|
311 |
243 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
312 ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} |
244 |
313 |
245 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
314 ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
246 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
315 ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} |
247 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *} |
316 ML {* val aps = @{typ "LamEx.rlam \<Rightarrow> bool"} :: aps; *} |