261 rtac @{thm IDENTITY_QUOTIENT} |
261 rtac @{thm IDENTITY_QUOTIENT} |
262 ]) |
262 ]) |
263 *} |
263 *} |
264 |
264 |
265 ML {* |
265 ML {* |
266 fun LAMBDA_RES_TAC ctxt = |
266 fun LAMBDA_RES_TAC ctxt i st = |
267 case (term_of o #concl o fst) (Subgoal.focus ctxt 1 (Isar.goal ())) of |
267 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
268 (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) => |
268 (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) => |
269 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
269 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
270 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
270 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
271 | _ => fn _ => no_tac |
271 | _ => fn _ => no_tac) i st |
272 *} |
272 *} |
273 |
273 |
274 |
274 |
275 ML {* |
275 ML {* |
276 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm = |
276 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm res_thms = |
277 (FIRST' [ |
277 (FIRST' [ |
278 rtac @{thm FUN_QUOTIENT}, |
278 rtac @{thm FUN_QUOTIENT}, |
279 rtac quot_thm, |
279 rtac quot_thm, |
280 rtac @{thm IDENTITY_QUOTIENT}, |
280 rtac @{thm IDENTITY_QUOTIENT}, |
281 rtac @{thm ext}, |
281 rtac @{thm ext}, |
282 rtac trans_thm, |
282 rtac trans_thm, |
283 LAMBDA_RES_TAC ctxt, |
283 LAMBDA_RES_TAC ctxt, |
284 res_forall_rsp_tac ctxt, |
284 res_forall_rsp_tac ctxt, |
|
285 ( |
|
286 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps res_thms)) |
|
287 THEN_ALL_NEW (fn _ => no_tac) |
|
288 ), |
285 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
289 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
286 rtac refl, |
290 rtac refl, |
287 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
291 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
288 rtac reflex_thm, |
292 rtac reflex_thm, |
289 atac, |
293 atac, |
294 ]) |
298 ]) |
295 *} |
299 *} |
296 |
300 |
297 ML {* |
301 ML {* |
298 fun r_mk_comb_tac_fset ctxt = |
302 fun r_mk_comb_tac_fset ctxt = |
299 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} |
303 r_mk_comb_tac ctxt @{thm QUOTIENT_fset} @{thm list_eq_refl} @{thm QUOT_TYPE_I_fset.R_trans2} @{thms ho_memb_rsp ho_cons_rsp} |
300 *} |
304 *} |
301 |
305 |
302 |
306 |
303 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
307 ML {* val thm = @{thm list_induct_r} OF [atomize_thm @{thm list_induct_hol4}] *} |
304 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
308 ML {* val trm_r = build_repabs_goal @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
305 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
309 ML {* val trm = build_repabs_term @{context} thm consts @{typ "'a list"} @{typ "'a fset"} *} |
306 |
310 |
307 |
311 ML {* trm_r *} |
308 prove list_induct_tr: trm_r |
312 prove list_induct_tr: trm_r |
309 apply (atomize(full)) |
313 apply (atomize(full)) |
310 (* APPLY_RSP_TAC *) |
314 (* APPLY_RSP_TAC *) |
|
315 ML_prf {* val ctxt = @{context} *} |
311 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
316 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
312 (* LAMBDA_RES_TAC *) |
317 (* LAMBDA_RES_TAC *) |
313 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
318 prefer 2 |
314 (* MK_COMB_TAC *) |
|
315 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
316 (* MK_COMB_TAC *) |
|
317 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
318 (* REFL_TAC *) |
|
319 apply (simp) |
|
320 (* MK_COMB_TAC *) |
|
321 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
322 (* MK_COMB_TAC *) |
|
323 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
324 (* REFL_TAC *) |
|
325 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
326 (* APPLY_RSP_TAC *) |
|
327 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
328 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
329 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
330 (* MK_COMB_TAC *) |
|
331 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
332 (* MK_COMB_TAC *) |
|
333 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
334 (* REFL_TAC *) |
|
335 apply (simp) |
|
336 (* APPLY_RSP *) |
|
337 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
338 (* MK_COMB_TAC *) |
|
339 apply (tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) |
|
340 (* REFL_TAC *) |
|
341 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
342 (* W(C (curry op THEN) (G... *) |
|
343 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
|
344 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
345 (* CONS respects *) |
|
346 apply (rule ho_cons_rsp) |
|
347 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
348 apply (subst FUN_REL.simps) |
319 apply (subst FUN_REL.simps) |
349 apply (rule allI) |
320 apply (rule allI) |
350 apply (rule allI) |
321 apply (rule allI) |
351 apply (rule impI) |
322 apply (rule impI) |
352 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
323 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
324 apply (auto) |
353 done |
325 done |
354 |
326 |
355 prove list_induct_t: trm |
327 prove list_induct_t: trm |
356 apply (simp only: list_induct_tr[symmetric]) |
328 apply (simp only: list_induct_tr[symmetric]) |
357 apply (tactic {* rtac thm 1 *}) |
329 apply (tactic {* rtac thm 1 *}) |
372 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
344 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
373 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
345 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
374 prove m2_t_p: m2_t_g |
346 prove m2_t_p: m2_t_g |
375 apply (atomize(full)) |
347 apply (atomize(full)) |
376 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
348 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
377 prefer 2 |
|
378 apply (subst FUN_REL.simps) |
|
379 apply (rule allI) |
|
380 apply (rule allI) |
|
381 apply (rule impI) |
|
382 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
383 prefer 2 |
|
384 apply (subst FUN_REL.simps) |
|
385 apply (rule allI) |
|
386 apply (rule allI) |
|
387 apply (rule impI) |
|
388 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
389 apply (subst FUN_REL.simps) |
|
390 apply (rule allI) |
|
391 apply (rule allI) |
|
392 apply (rule impI) |
|
393 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
|
394 apply (rule ho_memb_rsp) |
|
395 apply (rule ho_cons_rsp) |
|
396 apply (rule ho_memb_rsp) |
|
397 apply (auto) |
349 apply (auto) |
398 done |
350 done |
399 |
351 |
400 prove m2_t: m2_t |
352 prove m2_t: m2_t |
401 apply (simp only: m2_t_p[symmetric]) |
353 apply (simp only: m2_t_p[symmetric]) |