# HG changeset patch # User Cezary Kaliszyk # Date 1259141643 -3600 # Node ID e99c0334d8bffb31e458705d0a2a9f7977a5c91e # Parent f7dee6e808eb7fb6f098a41a02a85a2f6d389be0 lambda_prs and cleaning the existing examples. diff -r f7dee6e808eb -r e99c0334d8bf FSet.thy --- a/FSet.thy Wed Nov 25 03:47:07 2009 +0100 +++ b/FSet.thy Wed Nov 25 10:34:03 2009 +0100 @@ -337,155 +337,21 @@ apply (tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) done -ML {* - -fun lambda_prs_conv ctxt quot ctrm = - case (Thm.term_of ctrm) of - (Const (@{const_name "fun_map"}, _) $ y $ z) $ (Abs (_, T, x)) => - let - val _ = tracing "AAA"; - val lty = T; - val rty = fastype_of x; - val thy = ProofContext.theory_of ctxt; - val (lcty, rcty) = (ctyp_of thy lty, ctyp_of thy rty) - val inst = [SOME lcty, NONE, SOME rcty]; - val lpi = Drule.instantiate' inst [] @{thm LAMBDA_PRS}; - val tac = - (compose_tac (false, lpi, 2)) THEN_ALL_NEW - (quotient_tac quot); - val gc = Drule.strip_imp_concl (cprop_of lpi); - val t = Goal.prove_internal [] gc (fn _ => tac 1) - val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t - val te = @{thm eq_reflection} OF [ts] - val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm)); - val _ = tracing (Syntax.string_of_term @{context} (term_of (Thm.lhs_of te))); - val insts = matching_prs (ProofContext.theory_of ctxt) (term_of ctrm) (term_of (Thm.lhs_of te)); - val ti = Drule.instantiate insts te; - val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti))); - in - Conv.rewr_conv (eq_reflection OF [ti]) ctrm - end - | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm - | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm - | _ => Conv.all_conv ctrm -*} - -ML {* -fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => - CONVERSION - (Conv.params_conv ~1 (fn ctxt => - (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv - Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) -*} - -ML {* -val ctrm = @{cterm "((ABS_fset ---> id) ---> id) (\x. id ((REP_fset ---> id) x))"} -val pat = @{cpat "((ABS_fset ---> id) ---> id) (\x. ?f ((REP_fset ---> id) x))"} -*} - -ML {* matching_prs @{theory} (term_of pat) (term_of ctrm); *} - -ML {* - lambda_prs_conv @{context} quot ctrm -*} - - -ML {* -val t = @{thm LAMBDA_PRS[OF FUN_QUOTIENT[OF QUOTIENT_fset IDENTITY_QUOTIENT] IDENTITY_QUOTIENT]} -val te = @{thm eq_reflection} OF [t] -val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te -val tl = Thm.lhs_of ts - *} - -ML {* val inst = matching_prs @{theory} (term_of tl) (term_of ctrm); *} - -ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\(P\('a list \ bool)). - All ((REP_fset ---> id) (\(list\('a list)). - (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \ - True \ (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset list))))))"} *} - -ML {* - lambda_prs_conv @{context} quot trm -*} - - - -(*ML {* val trm = @{cterm "(((ABS_fset ---> id) ---> id) (\(?P\('a list \ bool)). (g (id P)"} *} *) - - - -lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" -apply(tactic {* procedure_tac @{thm list.induct} @{context} 1 *}) -apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) -apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) -apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *}) -apply(tactic {* lambda_prs_tac @{context} quot 1 *}) - - -ML_prf {* Subgoal.focus @{context} 1 (#goal (Isar.goal ())) *} - -apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) - - -thm LAMBDA_PRS -apply(tactic {* EqSubst.eqsubst_tac @{context} [0] @{thms LAMBDA_PRS} 1 *}) - -apply(tactic {* (lambda_prs_tac @{context} quot) 1 *}) - -apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *}) - -apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) -apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) -ML {* lift_thm_fset @{context} @{thm list.induct} *} -ML {* lift_thm_g_fset @{context} @{thm list.induct} @{term "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l"} *} - - - - -thm map_append lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" -apply(tactic {* procedure_tac @{thm map_append} @{context} 1 *}) -apply(tactic {* prepare_tac 1 *}) -thm map_append apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) done - - lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) done -ML {* atomize_thm @{thm fold1.simps(2)} *} -(*ML {* lift_thm_g_fset @{context} @{thm fold1.simps(2)} @{term "FOLD f g (z::'b) (INSERT a x) = - (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"} *}*) - - -*) -ML {* lift_thm_g_fset @{context} @{thm map_append} @{term "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"} *} - - -ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "\x xa a. x = xa \ INSERT a x = INSERT a xa"}) *} - - -ML {* lift_thm_fset @{context} @{thm map_append} *} - - -(* -apply(tactic {* procedure_tac @{thm m1} @{context} 1 *}) -apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *}) -apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *}) -apply(tactic {* clean_tac @{context} quot defs reps_same 1 *}) -apply(tactic {* TRY' (REPEAT_ALL_NEW (allex_prs_tac @{context} quot)) 1 *}) -apply(tactic {* TRY' (REPEAT_ALL_NEW (lambda_prs_tac @{context} quot)) 1 *}) -ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} -apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*}) -apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) -*) - - - -(*ML {* lift_thm_fset @{context} @{thm neq_Nil_conv} *}*) +ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.induct})) *} +ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} +lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" +apply (tactic {* lift_tac_fset @{context} @{thm list.induct} 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) +apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) +done quotient_def fset_rec::"'a \ ('b \ 'b fset \ 'a \ 'a) \ 'b fset \ 'a" @@ -510,67 +376,35 @@ apply (auto simp add: FUN_REL_EQ) sorry - ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} ML {* fun lift_thm_fset lthy t = lift_thm lthy qty "fset" rsp_thms defs t *} ML {* fun lift_thm_g_fset lthy t g = lift_thm_goal lthy qty "fset" rsp_thms defs t g *} +ML {* fun lift_tac_fset lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} -thm list.recs(2) -ML {* lift_thm_fset @{context} @{thm list.recs(2)} *} -ML {* lift_thm_g_fset @{context} @{thm list.recs(2)} @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} +ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.recs(2)})) *} +ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} +lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" +apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) +apply (tactic {* (simp_tac (HOL_ss addsimps + @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id})) 1 *}) +ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *} +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1 *}) +apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) +done + +ML {* val aps = findaps rty (prop_of (atomize_thm @{thm list.cases(2)})) *} +ML {* val app_prs_thms = map (applic_prs @{context} rty qty absrep) aps *} -ML {* val gl = @{term "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"} *} -ML {* val t_a = atomize_thm @{thm list.recs(2)} *} -ML {* val qtrm = atomize_goal @{theory} gl *} -ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (REGULARIZE_trm @{context} (prop_of t_a) qtrm)) *} -ML {* val rg2 = cterm_of @{theory}(my_reg @{context} rel rty (prop_of t_a)) *} - -ML {* val t_r = regularize_goal @{context} t_a rel_eqv rel_refl qtrm *} -ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} - -ML {* val rg = cterm_of @{theory}(Syntax.check_term @{context} (inj_REPABS @{context} ((prop_of t_r), qtrm))) *} -ML {* val rg2 = cterm_of @{theory} (build_repabs_term @{context} t_r consts rty qty) *} -ML {* val t_t = repabs_goal @{context} t_r rty quot rel_refl trans2 rsp_thms qtrm *} -ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} -ML {* - val lthy = @{context} - val (alls, exs) = findallex lthy rty qty (prop_of t_a); - val allthms = map (make_allex_prs_thm lthy quot @{thm FORALL_PRS}) alls - val exthms = map (make_allex_prs_thm lthy quot @{thm EXISTS_PRS}) exs - val t_a = MetaSimplifier.rewrite_rule (allthms @ exthms) t_t - val abs = findabs rty (prop_of t_a); - val aps = findaps rty (prop_of t_a); - val app_prs_thms = map (applic_prs lthy rty qty absrep) aps; - val lam_prs_thms = map (make_simp_prs_thm lthy quot @{thm LAMBDA_PRS}) abs; - val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; - val defs_sym = flat (map (add_lower_defs lthy) defs); - val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; - val t_id = simp_ids lthy t_l; - val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_id; - val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; - val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; - val t_rv = ObjectLogic.rulify t_r - -*} - - - - - - -ML {* map (lift_thm_fset @{context}) @{thms list.cases} *} - - - - -ML {* atomize_thm @{thm m1} *} -ML {* cterm_of @{theory} (atomize_goal @{theory} @{term "IN x EMPTY = False"}) *} -ML {* lift_thm_fset @{context} @{thm m1} *} -(* ML {* lift_thm_g_fset @{context} @{thm m1} @{term "IN x EMPTY = False"}) *} *) - +ML {* map (lift_thm_fset @{context}) @{thms list.cases(2)} *} +lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" +apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) +apply (tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] app_prs_thms) 1 *}) +apply (tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *}) +done lemma list_induct_part: assumes a: "P (x :: 'a list) ([] :: 'a list)" @@ -583,6 +417,7 @@ done + (* Construction site starts here *) @@ -590,7 +425,6 @@ ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset" *} -thm list.recs(2) ML {* val t_a = atomize_thm @{thm list_induct_part} *} @@ -754,26 +588,4 @@ ML {* val t_al = MetaSimplifier.rewrite_rule (allthms) t_d *} ML {* val t_s = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_fset.REPS_same} t_al *} - -ML {* - fun lift_thm_fset_note name thm lthy = - let - val lifted_thm = lift_thm_fset lthy thm; - val (_, lthy2) = note (name, lifted_thm) lthy; - in - lthy2 - end; -*} - -local_setup {* - lift_thm_fset_note @{binding "m1l"} @{thm m1} #> - lift_thm_fset_note @{binding "m2l"} @{thm m2} #> - lift_thm_fset_note @{binding "leqi4l"} @{thm list_eq.intros(4)} #> - lift_thm_fset_note @{binding "leqi5l"} @{thm list_eq.intros(5)} -*} -thm m1l -thm m2l -thm leqi4l -thm leqi5l - end diff -r f7dee6e808eb -r e99c0334d8bf LamEx.thy --- a/LamEx.thy Wed Nov 25 03:47:07 2009 +0100 +++ b/LamEx.thy Wed Nov 25 10:34:03 2009 +0100 @@ -119,18 +119,6 @@ shows "(pi\rLam a t) \ rLam (pi\a) (pi\t)" sorry -lemma fv_var: - shows "fv (Var a) = {a}" -sorry - -lemma fv_app: - shows "fv (App t1 t2) = (fv t1) \ (fv t2)" -sorry - -lemma fv_lam: - shows "fv (Lam a t) = (fv t) - {a}" -sorry - lemma real_alpha: assumes "t = [(a,b)]\s" "a\[b].s" shows "Lam a t = Lam b s" @@ -194,51 +182,48 @@ ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *} ML {* fun lift_tac_lam lthy t = lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same defs *} -lemma "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" +lemma pi_var: "(pi\('x \ 'x) list) \ Var a = Var (pi \ a)" apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *}) done -ML {* val pi_app = lift_thm_lam @{context} @{thm pi_app_com} *} -lemma "(pi\('x \ 'x) list) \ App (x\lam) (xa\lam) = App (pi \ x) (pi \ xa)" +lemma pi_app: "(pi\('x \ 'x) list) \ App (x\lam) (xa\lam) = App (pi \ x) (pi \ xa)" apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *}) done -ML {* val pi_lam = lift_thm_lam @{context} @{thm pi_lam_com} *} -lemma "(pi\('x \ 'x) list) \ Lam (a\name) (x\lam) = Lam (pi \ a) (pi \ x)" + +lemma pi_lam: "(pi\('x \ 'x) list) \ Lam (a\name) (x\lam) = Lam (pi \ a) (pi \ x)" apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *}) done -ML {* val fv_var = lift_thm_lam @{context} @{thm rfv_var} *} -lemma "\a. fv (Var (a\name)) = {a}" +lemma fv_var: "fv (Var (a\name)) = {a}" apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *}) done -ML {* val fv_app = lift_thm_lam @{context} @{thm rfv_app} *} -lemma "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" -(*apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})*) -sorry -ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} -lemma "fv (Lam (a\name) (x\lam)) = fv x - {a}" -(*apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})*) -sorry + +lemma fv_app: "fv (App (x\lam) (xa\lam)) = fv x \ fv xa" +apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *}) +done -ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} -lemma "(a\name) = (b\name) \ Var a = Var b" +lemma fv_lam: "fv (Lam (a\name) (x\lam)) = fv x - {a}" +apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *}) +done + +lemma a1: "(a\name) = (b\name) \ Var a = Var b" apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *}) done -ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} -lemma "\(x\lam) = (xa\lam); (xb\lam) = (xc\lam)\ \ App x xb = App xa xc" + +lemma a2: "\(x\lam) = (xa\lam); (xb\lam) = (xc\lam)\ \ App x xb = App xa xc" apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *}) done -ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} -lemma "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" -(*apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})*) -sorry + +lemma a3: "\(x\lam) = [(a\name, b\name)] \ (xa\lam); a \ fv (Lam b x)\ \ Lam a x = Lam b xa" +apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *}) +done ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} lemma "\(x\lam) = (xa\lam); \(a\name) b\name. \x = Var a; xa = Var b; a = b\ \ P\bool; \(x\lam) (xa\lam) (xb\lam) xc\lam. \x = App x xb; xa = App xa xc; x = xa; xb = xc\ \ P; \(x\lam) (a\name) (b\name) xa\lam. \x = Lam a x; xa = Lam b xa; x = [(a, b)] \ xa; a \ fv (Lam b x)\ \ P\ \ P" -(* apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *}) *) +apply (tactic {* procedure_tac @{thm alpha.cases} @{context} 1 *}) sorry ML {* val alpha_induct = lift_thm_lam @{context} @{thm alpha.induct} *} lemma "\(qx\lam) = (qxa\lam); \(a\name) b\name. a = b \ (qxb\lam \ lam \ bool) (Var a) (Var b); @@ -249,27 +234,10 @@ (* apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *}) *) sorry -lemma "(Var a = Var b) = (a = b)" +lemma var_inject: "(Var a = Var b) = (a = b)" apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *}) done -local_setup {* - Quotient.note (@{binding "pi_var"}, pi_var) #> snd #> - Quotient.note (@{binding "pi_app"}, pi_app) #> snd #> - Quotient.note (@{binding "pi_lam"}, pi_lam) #> snd #> - Quotient.note (@{binding "a1"}, a1) #> snd #> - Quotient.note (@{binding "a2"}, a2) #> snd #> - Quotient.note (@{binding "a3"}, a3) #> snd #> - Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd #> - Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd #> - Quotient.note (@{binding "var_inject"}, var_inject) #> snd -*} - -thm alpha.cases -thm alpha_cases -thm alpha.induct -thm alpha_induct - lemma var_supp: shows "supp (Var a) = ((supp a)::name set)" apply(simp add: supp_def) @@ -354,24 +322,6 @@ ML_prf {* fun r_mk_comb_tac_lam lthy = r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms *} -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) -apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) apply (tactic {* (r_mk_comb_tac_lam @{context}) 1 *}) diff -r f7dee6e808eb -r e99c0334d8bf QuotMain.thy --- a/QuotMain.thy Wed Nov 25 03:47:07 2009 +0100 +++ b/QuotMain.thy Wed Nov 25 10:34:03 2009 +0100 @@ -1649,9 +1649,51 @@ *} ML {* -fun lambda_prs_tac lthy quot = - (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS} - THEN' (RANGE [quotient_tac quot, quotient_tac quot])); +fun lambda_prs_conv1 ctxt quot ctrm = + case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) => + let + val (_, [ty_b, ty_a]) = dest_Type (fastype_of r1); + val (_, [ty_c, ty_d]) = dest_Type (fastype_of a2); + val thy = ProofContext.theory_of ctxt; + val [cty_a, cty_b, cty_c, cty_d] = map (ctyp_of thy) [ty_a, ty_b, ty_c, ty_d] + val tyinst = [SOME cty_a, SOME cty_b, SOME cty_c, SOME cty_d]; + val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)] + val lpi = Drule.instantiate' tyinst tinst @{thm LAMBDA_PRS}; + val tac = + (compose_tac (false, lpi, 2)) THEN_ALL_NEW + (quotient_tac quot); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) + val te = @{thm eq_reflection} OF [t] + val ts = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] te + val tl = Thm.lhs_of ts +(* val _ = tracing (Syntax.string_of_term @{context} (term_of ctrm));*) +(* val _ = tracing (Syntax.string_of_term @{context} (term_of tl));*) + val insts = matching_prs (ProofContext.theory_of ctxt) (term_of tl) (term_of ctrm); + val ti = Drule.eta_contraction_rule (Drule.instantiate insts ts); +(* val _ = tracing (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*) + in + Conv.rewr_conv ti ctrm + end + +*} +ML {* +fun lambda_prs_conv ctxt quot ctrm = + case (term_of ctrm) of + (Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs (_, _, x)) => + (Conv.arg_conv (Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt) + then_conv (lambda_prs_conv1 ctxt quot)) ctrm + | _ $ _ => Conv.comb_conv (lambda_prs_conv ctxt quot) ctrm + | Abs _ => Conv.abs_conv (fn (_, ctxt) => lambda_prs_conv ctxt quot) ctxt ctrm + | _ => Conv.all_conv ctrm +*} + +ML {* +fun lambda_prs_tac ctxt quot = CSUBGOAL (fn (goal, i) => + CONVERSION + (Conv.params_conv ~1 (fn ctxt => + (Conv.prems_conv ~1 (lambda_prs_conv ctxt quot) then_conv + Conv.concl_conv ~1 (lambda_prs_conv ctxt quot))) ctxt) i) *} ML {* @@ -1664,7 +1706,7 @@ val lower = flat (map (add_lower_defs lthy) defs) in TRY' (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN' - TRY' (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN' + TRY' (lambda_prs_tac lthy quot) THEN' TRY' (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN' simp_tac (HOL_ss addsimps [reps_same]) end