# HG changeset patch # User Cezary Kaliszyk # Date 1257170276 -3600 # Node ID 22c199522befae9d25b7e9f56979cc1a1edd5d48 # Parent 93ea455b29f1222b51f3486e3f4aa7a563033241 Optimization diff -r 93ea455b29f1 -r 22c199522bef LamEx.thy --- a/LamEx.thy Mon Nov 02 11:51:50 2009 +0100 +++ b/LamEx.thy Mon Nov 02 14:57:56 2009 +0100 @@ -11,6 +11,7 @@ | rApp "rlam" "rlam" | rLam "name" "rlam" +print_theorems function rfv :: "rlam \ name set" @@ -29,6 +30,8 @@ | a2: "\t1 \ t2; s1 \ s2\ \ rApp t1 s1 \ rApp t2 s2" | a3: "\t \ ([(a,b)]\s); a \ rfv (rLam b t)\ \ rLam a t \ rLam b s" +print_theorems + quotient lam = rlam / alpha sorry @@ -176,7 +179,7 @@ ML {* val fv_lam = lift_thm_lam @{context} @{thm rfv_lam} *} ML {* val a1 = lift_thm_lam @{context} @{thm a1} *} -ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} +ML {* val a2 = lift_thm_lam @{context} @{thm a2} *} ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} @@ -240,6 +243,7 @@ *} apply (tactic {* tac @{context} 1 *}) *) ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} + (*ML {* val rt = build_repabs_term @{context} t_r consts rty qty val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); @@ -279,39 +283,60 @@ ML {* val abs = findabs rty (prop_of (atomize_thm @{thm alpha.induct})) *} ML {* val aps = findaps rty (prop_of (atomize_thm @{thm alpha.induct})) *} - -ML {* - - -*} - ML {* val aps = @{typ "LamEx.rlam \ bool"} :: aps; *} +ML {* val thm = + @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]]]} *} +ML {* val t_a = simp_allex_prs quot [thm] t_t *} ML {* val simp_app_prs_thms = map (make_simp_prs_thm @{context} quot @{thm APP_PRS}) aps *} ML {* val simp_lam_prs_thms = map (make_simp_prs_thm @{context} quot @{thm LAMBDA_PRS}) abs *} -ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_t *} -ML {* val t_a = simp_allex_prs @{context} quot t_l *} -ML {* val thm = - @{thm FORALL_PRS[OF FUN_QUOTIENT[OF QUOTIENT_lam FUN_QUOTIENT[OF QUOTIENT_lam IDENTITY_QUOTIENT]], symmetric]} *} -ML {* val t_a1 = eqsubst_thm @{context} [thm] t_a *} + +ML {* val t_l = repeat_eqsubst_thm @{context} (simp_app_prs_thms @ simp_lam_prs_thms) t_a *} ML {* val defs_sym = add_lower_defs @{context} defs; *} -ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a1 *} +ML {* val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym *} +ML t_l +ML {* val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l *} +ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_d0 *} ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} ML {* val t_r1 = repeat_eqsubst_thm @{context} @{thms fun_map.simps} t_r *} -ML {* val t_r2 = repeat_eqsubst_thm @{context} @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} -ML {* val t_r3 = repeat_eqsubst_thm @{context} @{thms id_apply} t_r2 *} - +ML {* val t_r2 = MetaSimplifier.rewrite_rule @{thms QUOT_TYPE_I_lam.thm10} t_r1 *} +ML {* val t_r3 = MetaSimplifier.rewrite_rule @{thms eq_reflection[OF id_apply]} t_r2 *} ML {* val alpha_induct = ObjectLogic.rulify t_r3 *} local_setup {* Quotient.note (@{binding "alpha_induct"}, alpha_induct) #> snd *} +thm alpha_induct +thm alpha.induct + +lemma rvar_inject: "rVar a \ rVar b \ (a = b)" +apply (rule alpha.cases) +apply (assumption) +apply (assumption) +apply (simp_all) +apply (cases "a = b") +apply (simp_all) +apply (cases "ba = b") +apply (simp_all) + + +lemma var_inject_test: + fixes a b + assumes a: "Var a = Var b" + shows "(a = b)" + using a apply (cases "a = b") + apply (simp_all) + apply (rule_tac x="Var a" and xa = "Var b" in alpha_cases) + apply (rule a) + + lemma - assumes a: "(a::lam) = b" - shows "False" - using a - apply (rule alpha_induct) - + assumes a: "(x::lam) = y" + shows "P x y" + apply (induct rule: alpha_induct) + apply (rule a) +thm alpha.induct +thm alpha_induct fun option_map::"('a \ 'b) \ ('a noption) \ ('b noption)" where diff -r 93ea455b29f1 -r 22c199522bef QuotMain.thy --- a/QuotMain.thy Mon Nov 02 11:51:50 2009 +0100 +++ b/QuotMain.thy Mon Nov 02 14:57:56 2009 +0100 @@ -760,9 +760,9 @@ ML {* fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = (FIRST' [ - rtac @{thm FUN_QUOTIENT}, +(* rtac @{thm FUN_QUOTIENT}, rtac quot_thm, - rtac @{thm IDENTITY_QUOTIENT}, + rtac @{thm IDENTITY_QUOTIENT},*) rtac trans_thm, LAMBDA_RES_TAC ctxt, res_forall_rsp_tac ctxt, @@ -873,23 +873,22 @@ val tac = (compose_tac (false, lpi, 2)) THEN_ALL_NEW (quotient_tac quot_thm); - val t = Goal.prove lthy [] [] (concl_of lpi) (fn _ => tac 1); + val gc = Drule.strip_imp_concl (cprop_of lpi); + val t = Goal.prove_internal [] gc (fn _ => tac 1) in MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] t end *} ML {* - fun simp_allex_prs lthy quot thm = + fun simp_allex_prs quot thms thm = let - val rwf = @{thm FORALL_PRS} OF [quot]; - val rwfs = @{thm "HOL.sym"} OF [rwf]; - val rwe = @{thm EXISTS_PRS} OF [quot]; - val rwes = @{thm "HOL.sym"} OF [rwe] + val ts = [@{thm FORALL_PRS} OF [quot], @{thm EXISTS_PRS} OF [quot]] @ thms + val sym_ts = map (fn x => @{thm "HOL.sym"} OF [x]) ts; + val eq_ts = map (fn x => @{thm "eq_reflection"} OF [x]) sym_ts in - (simp_allex_prs lthy quot (eqsubst_thm lthy [rwfs, rwes] thm)) + MetaSimplifier.rewrite_rule eq_ts thm end - handle _ => thm *} ML {* @@ -940,10 +939,12 @@ val aps = findaps rty (prop_of t_a); val app_prs_thms = map (make_simp_prs_thm lthy quot @{thm APP_PRS}) 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_t; - val t_a = simp_allex_prs lthy quot t_l; + val t_a = simp_allex_prs quot [] t_t; + val t_l = repeat_eqsubst_thm lthy (lam_prs_thms @ app_prs_thms) t_a; val defs_sym = add_lower_defs lthy defs; - val t_d = repeat_eqsubst_thm lthy defs_sym t_a; + val defs_sym_eq = map (fn x => eq_reflection OF [x]) defs_sym; + val t_d0 = MetaSimplifier.rewrite_rule defs_sym_eq t_l; + val t_d = repeat_eqsubst_thm lthy defs_sym t_d0; val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; in ObjectLogic.rulify t_r