409 |
409 |
410 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
410 ML {* fun r_mk_comb_tac_fset lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} |
411 |
411 |
412 |
412 |
413 |
413 |
|
414 |
|
415 ML {* |
|
416 fun lambda_prs_conv1 ctxt quot ctrm = |
|
417 case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => |
|
418 let |
|
419 val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); |
|
420 val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); |
|
421 val thy = ProofContext.theory_of ctxt; |
|
422 val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] |
|
423 val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; |
|
424 val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] |
|
425 val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; |
|
426 val tac = |
|
427 (compose_tac (false, lpi, 2)) THEN_ALL_NEW |
|
428 (quotient_tac quot); |
|
429 val gc = Drule.strip_imp_concl (cprop_of lpi); |
|
430 val t = Goal.prove_internal [] gc (fn _ => tac 1) |
|
431 val te = @{thm eq_reflection} OF [t] |
|
432 val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te |
|
433 val tl = Thm.lhs_of ts |
|
434 val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm)); |
|
435 val _ = tracing (Syntax.string_of_term @{context} (term_of tl)); |
|
436 val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm); |
|
437 val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); |
|
438 (* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) |
|
439 in |
|
440 Conv.rewr_conv ti ctrm |
|
441 end |
|
442 handle _ => Conv.all_conv ctrm |
|
443 |
|
444 *} |
|
445 ML {* |
|
446 fun lambda_prs_conv ctxt quot ctrm = |
|
447 case (term_of ctrm) of |
|
448 (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) => |
|
449 (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt) |
|
450 then_conv (lambda_prs_conv1 ctxt quot)) ctrm |
|
451 | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm |
|
452 | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm |
|
453 | _ => Conv.all_conv ctrm |
|
454 *} |
|
455 |
|
456 ML {* |
|
457 fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => |
|
458 CONVERSION |
|
459 (Conv.params_conv ~1 (fn ctxt => |
|
460 (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv |
|
461 Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) |
|
462 *} |
|
463 |
|
464 |
414 (* Construction site starts here *) |
465 (* Construction site starts here *) |
415 lemma "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
466 lemma "P (x :: 'a list) (EMPTY :: 'a fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
416 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) |
467 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) |
417 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
468 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
418 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
469 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
481 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
532 apply (tactic {* (instantiate_tac @{thm REP_ABS_RSP(1)} @{context} THEN' (RANGE [quotient_tac quot])) 1 *}) |
482 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
533 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
483 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
534 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
484 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
535 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
485 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
536 apply (tactic {* (r_mk_comb_tac_fset @{context}) 1 *}) |
486 apply (tactic {* clean_tac @{context} quot defs reps_same 1 *}) |
537 apply (simp only:map_id) |
|
538 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
|
539 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
|
540 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
|
541 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
|
542 ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'a list \<Rightarrow> bool)"} *} |
|
543 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *}) |
|
544 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
487 done |
545 done |
488 |
546 |
489 end |
547 end |