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 |
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 |
|
465 (* Construction site starts here *) |
415 (* Construction site starts here *) |
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 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
467 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) |
417 apply (tactic {* procedure_tac @{thm list_induct_part} @{context} 1 *}) |
468 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
418 apply (tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) |
469 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
419 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
470 apply (rule FUN_QUOTIENT) |
420 apply (rule FUN_QUOTIENT) |
471 apply (rule FUN_QUOTIENT) |
421 apply (rule FUN_QUOTIENT) |
537 apply (simp only:map_id) |
487 apply (simp only:map_id) |
538 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
488 apply (tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) |
539 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
489 ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} |
540 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
490 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) |
541 apply (tactic {* lambda_prs_tac @{context} quot 1 *}) |
491 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)"} *} |
492 ML_prf {* val t = applic_prs @{context} rty qty absrep @{typ "('b \<Rightarrow> 'c list \<Rightarrow> bool)"} *} |
543 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *}) |
493 apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] [t]) 1 *}) |
544 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
494 apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) |
545 done |
495 done |
546 |
496 |
547 end |
497 end |