diff -r c770f36f9459 -r e30997c88050 LamEx.thy --- a/LamEx.thy Fri Oct 30 18:31:06 2009 +0100 +++ b/LamEx.thy Fri Oct 30 19:03:53 2009 +0100 @@ -107,7 +107,7 @@ lemma fv_lam: shows "fv (Lam a t) = (fv t) - {a}" -sorry +sorry lemma real_alpha: assumes "t = [(a,b)]\s" "a\[b].s" @@ -179,16 +179,20 @@ ML {* val a2 = lift_thm_lam @{context} @{thm a1} *} ML {* val a3 = lift_thm_lam @{context} @{thm a3} *} +ML {* val alpha_cases = lift_thm_lam @{context} @{thm alpha.cases} *} + 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 "a3"}, a3) #> snd #> + Quotient.note (@{binding "alpha_cases"}, alpha_cases) #> snd *} thm alpha.cases +thm alpha_cases thm rlam.inject thm pi_var @@ -217,114 +221,17 @@ - -lemma get_rid: "(\x. (P x \ Q x)) \ ((\x. P x) \ (\x. Q x))" -apply (auto) -done - -lemma get_rid2: "(c \ a) \ (a \ b \ d) \ (a \ b) \ (c \ d)" -apply (auto) -done - ML {* val t_a = atomize_thm @{thm alpha.cases} *} -prove {* build_regularize_goal t_a rty rel @{context} *} - ML_prf {* fun tac ctxt = - (FIRST' [ - rtac rel_refl, - atac, - rtac @{thm get_rid}, - rtac @{thm get_rid2}, - (fn i => CHANGED (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])]) i)), - (rtac @{thm impI} THEN' (asm_full_simp_tac (Simplifier.context ctxt HOL_ss)) THEN' rtac rel_refl) - ]); - *} - apply (atomize(full)) - apply (tactic {* tac @{context} 1 *}) - apply (rule get_rid) - apply (rule get_rid) - apply (rule get_rid2) - apply (simp) - apply (rule get_rid) - apply (rule get_rid2) - apply (rule get_rid) - apply (rule get_rid2) - apply (rule impI) - apply (simp) - apply (tactic {* tac @{context} 1 *}) - apply (rule get_rid2) - apply (rule impI) - apply (simp) - apply (tactic {* tac @{context} 1 *}) - apply (simp) - apply (rule get_rid2) - apply (rule get_rid) - apply (rule get_rid) - apply (rule get_rid) - apply (rule get_rid2) - apply (rule impI) - apply (simp) - apply (tactic {* tac @{context} 1 *}) - apply (rule get_rid) - apply (rule get_rid2) - - - apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) -ML_prf {* -fun focus_compose t = Subgoal.FOCUS (fn {concl, ...} => - rtac t 1) -*} -thm spec[of _ "x"] - apply (rule allI) - apply (drule_tac x="a2" in spec) - apply (rule impI) - apply (erule impE) - apply (assumption) - apply (rule allI) - apply (drule_tac x="P" in spec) - apply (atomize(full)) - apply (rule allI) - apply (rule allI) - apply (rule allI) - apply (rule impI) - apply (rule get_rid2) - - thm get_rid2 - apply (tactic {* compose_tac (false, @{thm get_rid2}, 0) 1 *}) - - thm spec - - ML_prf {* val t = snd (Subgoal.focus @{context} 1 (Isar.goal ())) *} -ML_prf {* Seq.pull (compose_tac (false, @{thm get_rid}, 2) 1 t) *} - - - thm get_rid - apply (rule allI) - apply (drule spec) - - thm spec - apply (tactic {* compose_tac (false, @{thm get_rid}, 1) 1 *}) - - apply (tactic {* tac @{context} 1 *}) - apply (tactic {* tac @{context} 1 *}) - apply (rule impI) - apply (erule impE) - apply (assumption) - apply (tactic {* tac @{context} 1 *}) - apply (rule impI) - apply (erule impE) - apply (tactic {* tac @{context} 1 *}) - apply (tactic {* tac @{context} 1 *}) - apply (tactic {* tac @{context} 1 *}) - apply (tactic {* tac @{context} 1 *}) - ML {* val t_r = regularize t_a rty rel rel_eqv rel_refl @{context} *} ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} +ML {* val abs = findabs rty (prop_of t_a); *} +ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} ML {* val t_a = simp_allex_prs @{context} quot t_l *} -ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym - +ML {* val defs_sym = add_lower_defs @{context} defs; *} +ML {* val t_d = repeat_eqsubst_thm @{context} defs_sym t_a *} +ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} +ML {* ObjectLogic.rulify t_r *} @@ -358,127 +265,3 @@ (* Simp starts hanging so don't know how to continue *) sorry -(* Not sure if it make sense or if it will be needed *) -lemma abs_fun_rsp: "(op = ===> alpha ===> op = ===> op =) abs_fun abs_fun" -sorry - -(* Should not be needed *) -lemma eq_rsp2: "((op = ===> op =) ===> (op = ===> op =) ===> op =) op = op =" -apply auto -apply (rule ext) -apply auto -apply (rule ext) -apply auto -done - -(* Should not be needed *) -lemma perm_rsp_eq: "(op = ===> (op = ===> op =) ===> op = ===> op =) op \ op \" -apply auto -thm arg_cong2 -apply (rule_tac f="perm x" in arg_cong2) -apply (auto) -apply (rule ext) -apply (auto) -done - -(* Should not be needed *) -lemma fresh_rsp_eq: "(op = ===> (op = ===> op =) ===> op =) fresh fresh" -apply (simp add: FUN_REL.simps) -apply (metis ext) -done - -(* It is just a test, it doesn't seem true... *) -lemma quotient_cheat: "QUOTIENT op = (option_map ABS_lam) (option_map REP_lam)" -sorry - -ML {* val rsp_thms = @{thms abs_fun_rsp OPT_QUOTIENT eq_rsp2 quotient_cheat perm_rsp_eq fresh_rsp_eq} @ rsp_thms *} -ML {* fun lift_thm_lam lthy t = lift_thm lthy qty "lam" rsp_thms defs t *} - -thm a3 -ML {* Toplevel.program (fn () => lift_thm_lam @{context} @{thm a3}) *} -thm a3 -ML {* val t_u1 = eqsubst_thm @{context} @{thms abs_fresh(1)} (atomize_thm @{thm a3}) *} -ML {* val t_u = MetaSimplifier.rewrite_rule @{thms fresh_def supp_def} t_u1 *} - -(* T_U *) - -ML {* val t_a = atomize_thm @{thm rfv_var} *} -ML {* val t_r = regularize t_a rty rel rel_eqv @{context} *} -ML {* val t_t = repabs @{context} t_r consts rty qty quot rel_refl trans2 rsp_thms *} - -ML {* fun r_mk_comb_tac_lam ctxt = - r_mk_comb_tac ctxt rty quot rel_refl trans2 rsp_thms -*} - -instance lam :: fs_name -apply(intro_classes) -sorry - -prove asdf: {* Logic.mk_implies (concl_of t_r, (@{term "Trueprop (\t\rlam\Respects - alpha. - \(a\name) b\name. - \s\rlam\Respects - alpha. - t \ ([(a, - b)] \ s) \ - a = b \ - a - \ {a\name. - infinite - {b\name. Not - (([(a, b)] \ - s) \ - s)}} \ - rLam a - t \ rLam - b s)"})) *} -apply (tactic {* full_simp_tac ((Simplifier.context @{context} HOL_ss) addsimps - [(@{thm equiv_res_forall} OF [rel_eqv]), - (@{thm equiv_res_exists} OF [rel_eqv])]) 1 *}) -apply (rule allI) -apply (drule_tac x="t" in spec) -apply (rule allI) -apply (drule_tac x="a" in spec) -apply (rule allI) -apply (drule_tac x="b" in spec) -apply (rule allI) -apply (drule_tac x="s" in spec) -apply (rule impI) -apply (drule_tac mp) -apply (simp) -apply (simp) -apply (rule impI) -apply (rule a3) -apply (simp) -apply (simp add: abs_fresh(1)) -apply (case_tac "a = b") -apply (simp) -apply (simp) -apply (auto) -apply (unfold fresh_def) -apply (unfold supp_def) -apply (simp) -prefer 2 -apply (simp) -sorry - -ML {* val abs = findabs rty (prop_of t_a) *} -ML {* val simp_lam_prs_thms = map (make_simp_lam_prs_thm @{context} quot) abs *} -ML {* val t_defs_sym = add_lower_defs @{context} defs *} - -ML {* val t_r' = @{thm asdf} OF [t_r] *} -ML {* val t_t = repabs @{context} t_r' consts rty qty quot rel_refl trans2 rsp_thms *} -ML {* val t_l = repeat_eqsubst_thm @{context} simp_lam_prs_thms t_t *} -ML {* val t_a = simp_allex_prs @{context} quot t_l *} -ML {* val t_d = repeat_eqsubst_thm @{context} t_defs_sym t_a *} -ML {* val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d *} -ML {* val tt = MetaSimplifier.rewrite_rule [symmetric @{thm supp_def}, symmetric @{thm fresh_def}] t_r *} -ML {* val rr = @{thm sym} OF @{thms abs_fresh(1)} *} -ML {* val ttt = eqsubst_thm @{context} [rr] tt *} -ML {* ObjectLogic.rulify ttt *} - -lemma - assumes a: "a \ {a\name. infinite {b\name. \ ([(a, b)] \ s) \ s}}" - shows "a \ {a\name. infinite {b\name. [(a, b)] \ s \ s}}" - using a apply simp - sorry (* Not true... *)