--- 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 \<Rightarrow> name set"
@@ -29,6 +30,8 @@
| a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2"
| a3: "\<lbrakk>t \<approx> ([(a,b)]\<bullet>s); a \<notin> rfv (rLam b t)\<rbrakk> \<Longrightarrow> rLam a t \<approx> 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 \<Rightarrow> 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 \<approx> rVar b \<Longrightarrow> (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 \<Rightarrow> 'b) \<Rightarrow> ('a noption) \<Rightarrow> ('b noption)"
where
--- 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