# HG changeset patch # User Cezary Kaliszyk # Date 1259936726 -3600 # Node ID 051bd9e90e9258c2e0b8bd1a2f743d4934980fa6 # Parent 53984a386999b866453d75c07135fbfae1163c05 merged diff -r 53984a386999 -r 051bd9e90e92 LFex.thy --- a/LFex.thy Fri Dec 04 15:20:06 2009 +0100 +++ b/LFex.thy Fri Dec 04 15:25:26 2009 +0100 @@ -67,18 +67,18 @@ apply(auto intro: akind_aty_atrm.intros) done -lemma alpha_EQUIVs: - shows "EQUIV akind" - and "EQUIV aty" - and "EQUIV atrm" +lemma alpha_equivps: + shows "equivp akind" + and "equivp aty" + and "equivp atrm" sorry quotient KIND = kind / akind - by (rule alpha_EQUIVs) + by (rule alpha_equivps) quotient TY = ty / aty and TRM = trm / atrm - by (auto intro: alpha_EQUIVs) + by (auto intro: alpha_equivps) print_quotients @@ -217,10 +217,10 @@ thm kind_ty_trm.induct ML {* - val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} - val rel_refl = map (fn x => @{thm EQUIV_REFL} OF [x]) @{thms alpha_EQUIVs} - (*val trans2 = map (fn x => @{thm equiv_trans2} OF [x]) @{thms alpha_EQUIVs}*) - val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot + val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM} + val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps} + (*val trans2 = map (fn x => @{thm EQUALS_PRS} OF [x]) quot*) + val reps_same = map (fn x => @{thm Quotient_REL_REP} OF [x]) quot val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same *} @@ -258,8 +258,8 @@ ((x5 :: TRM) = x6 \ P3 x5 x6)" using a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 apply - -apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_EQUIVs} 1 *}) -(*apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *}) +apply(tactic {* lift_tac @{context} @{thm akind_aty_atrm.induct} @{thms alpha_equivps} 1 *}) +(*apply(tactic {* regularize_tac @{context} @{thms alpha_equivps} 1 *}) apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *}) apply(tactic {* clean_tac @{context} 1 *}) *) @@ -268,7 +268,7 @@ Profiling: ML_prf {* fun ith i = (#concl (fst (Subgoal.focus @{context} i (#goal (Isar.goal ()))))) *} ML_prf {* profile 2 Seq.list_of ((clean_tac @{context} quot defs 1) (ith 3)) *} -ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_EQUIVs} 1) (ith 1)) *} +ML_prf {* profile 2 Seq.list_of ((regularize_tac @{context} @{thms alpha_equivps} 1) (ith 1)) *} ML_prf {* PolyML.profiling 1 *} ML_prf {* profile 2 Seq.list_of ((all_inj_repabs_tac @{context} quot rel_refl trans2 1) (#goal (Isar.goal ()))) *} *) @@ -298,7 +298,7 @@ \trm1 trm2. \P3 trm1; P3 trm2\ \ P3 (APP trm1 trm2); \ty name trm. \P2 ty; P3 trm\ \ P3 (LAM ty name trm)\ \ P1 mkind \ P2 mty \ P3 mtrm" -apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_EQUIVs} 1 *}) +apply(tactic {* lift_tac @{context} @{thm kind_ty_trm.induct} @{thms alpha_equivps} 1 *}) done print_quotients diff -r 53984a386999 -r 051bd9e90e92 LamEx.thy --- a/LamEx.thy Fri Dec 04 15:20:06 2009 +0100 +++ b/LamEx.thy Fri Dec 04 15:25:26 2009 +0100 @@ -46,12 +46,12 @@ apply(simp) done -lemma alpha_EQUIV: - shows "EQUIV alpha" +lemma alpha_equivp: + shows "equivp alpha" sorry quotient lam = rlam / alpha - apply(rule alpha_EQUIV) + apply(rule alpha_equivp) done print_quotients @@ -281,13 +281,13 @@ lemma "option_map id = id" sorry -lemma OPT_QUOTIENT: - assumes q: "QUOTIENT R Abs Rep" - shows "QUOTIENT (option_rel R) (option_map Abs) (option_map Rep)" - apply (unfold QUOTIENT_def) +lemma option_Quotient: + assumes q: "Quotient R Abs Rep" + shows "Quotient (option_rel R) (option_map Abs) (option_map Rep)" + apply (unfold Quotient_def) apply (auto) using q - apply (unfold QUOTIENT_def) + apply (unfold Quotient_def) apply (case_tac "a :: 'b noption") apply (simp) apply (simp) @@ -297,46 +297,3 @@ (* Simp starts hanging so don't know how to continue *) sorry -lemma real_alpha_pre: - assumes a: "t = [(a,b)]\s" "a\[b].s" - shows "rLam a t \ rLam b s" -sorry - -lemma perm_prs : "(id ---> option_map ABS_lam) ([b].REP_lam s) = [b].s" -sorry - -lemma perm_prs2: "(id ---> option_map ABS_lam) ((id ---> option_map REP_lam) ([b].(s::lam))) = [b].s" -sorry - -lemma real_alpha_lift: - "\t = [(a, b)] \ s; a \ [b].s\ \ Lam a t = Lam b s" -apply (tactic {* procedure_tac @{context} @{thm real_alpha_pre} 1 *}) -prefer 2 -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (tactic {* inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -apply (simp only: perm_prs) -prefer 2 -apply (tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *}) -prefer 3 -apply (tactic {* clean_tac @{context} 1 *}) -apply (simp only: perm_prs) -(*apply (tactic {* regularize_tac @{context} 1 *})*) -sorry -