equal
deleted
inserted
replaced
324 rtac @{thm ext}, |
324 rtac @{thm ext}, |
325 rtac trans_thm, |
325 rtac trans_thm, |
326 LAMBDA_RES_TAC ctxt, |
326 LAMBDA_RES_TAC ctxt, |
327 res_forall_rsp_tac ctxt, |
327 res_forall_rsp_tac ctxt, |
328 ( |
328 ( |
329 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps res_thms)) |
329 (simp_tac ((Simplifier.context @{context} HOL_ss) addsimps (res_thms @ @{thms ho_all_prs}))) |
330 THEN_ALL_NEW (fn _ => no_tac) |
330 THEN_ALL_NEW (fn _ => no_tac) |
331 ), |
331 ), |
332 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
332 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
333 rtac refl, |
333 rtac refl, |
334 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
334 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
356 apply (atomize(full)) |
356 apply (atomize(full)) |
357 (* APPLY_RSP_TAC *) |
357 (* APPLY_RSP_TAC *) |
358 ML_prf {* val ctxt = @{context} *} |
358 ML_prf {* val ctxt = @{context} *} |
359 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
359 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
360 (* LAMBDA_RES_TAC *) |
360 (* LAMBDA_RES_TAC *) |
361 prefer 2 |
|
362 apply (subst FUN_REL.simps) |
361 apply (subst FUN_REL.simps) |
363 apply (rule allI) |
362 apply (rule allI) |
364 apply (rule allI) |
363 apply (rule allI) |
365 apply (rule impI) |
364 apply (rule impI) |
366 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
365 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
367 apply (auto) |
|
368 done |
366 done |
369 |
367 |
370 prove list_induct_t: trm |
368 prove list_induct_t: trm |
371 apply (simp only: list_induct_tr[symmetric]) |
369 apply (simp only: list_induct_tr[symmetric]) |
372 apply (tactic {* rtac thm 1 *}) |
370 apply (tactic {* rtac thm 1 *}) |
387 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
385 ML {* val m2_t_g = build_repabs_goal @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
388 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
386 ML {* val m2_t = build_repabs_term @{context} m2_r consts @{typ "'a list"} @{typ "'a fset"} *} |
389 prove m2_t_p: m2_t_g |
387 prove m2_t_p: m2_t_g |
390 apply (atomize(full)) |
388 apply (atomize(full)) |
391 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
389 apply (tactic {* REPEAT_ALL_NEW (r_mk_comb_tac_fset @{context}) 1 *}) |
392 apply (auto) |
|
393 done |
390 done |
394 |
391 |
395 prove m2_t: m2_t |
392 prove m2_t: m2_t |
396 apply (simp only: m2_t_p[symmetric]) |
393 apply (simp only: m2_t_p[symmetric]) |
397 apply (tactic {* rtac m2_r 1 *}) |
394 apply (tactic {* rtac m2_r 1 *}) |