lambda_prs and cleaning the existing examples.
--- 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) (\<lambda>x. id ((REP_fset ---> id) x))"}
-val pat = @{cpat "((ABS_fset ---> id) ---> id) (\<lambda>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) (\<lambda>(P\<Colon>('a list \<Rightarrow> bool)).
- All ((REP_fset ---> id) (\<lambda>(list\<Colon>('a list)).
- (ABS_fset ---> id) ((REP_fset ---> id) P) (REP_fset (ABS_fset [])) \<longrightarrow>
- True \<longrightarrow> (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) (\<lambda>(?P\<Colon>('a list \<Rightarrow> bool)). (g (id P)"} *} *)
-
-
-
-lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> 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 "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> 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 "\<forall>x xa a. x = xa \<Longrightarrow> 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 "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> 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 \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> '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
--- 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\<bullet>rLam a t) \<approx> rLam (pi\<bullet>a) (pi\<bullet>t)"
sorry
-lemma fv_var:
- shows "fv (Var a) = {a}"
-sorry
-
-lemma fv_app:
- shows "fv (App t1 t2) = (fv t1) \<union> (fv t2)"
-sorry
-
-lemma fv_lam:
- shows "fv (Lam a t) = (fv t) - {a}"
-sorry
-
lemma real_alpha:
assumes "t = [(a,b)]\<bullet>s" "a\<sharp>[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\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
+lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> 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\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
+lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> 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\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
+
+lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> 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 "\<forall>a. fv (Var (a\<Colon>name)) = {a}"
+lemma fv_var: "fv (Var (a\<Colon>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\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> 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\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
-(*apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})*)
-sorry
+
+lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
+apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})
+done
-ML {* val a1 = lift_thm_lam @{context} @{thm a1} *}
-lemma "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
+lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
+apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})
+done
+
+lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *})
done
-ML {* val a2 = lift_thm_lam @{context} @{thm a2} *}
-lemma "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
+
+lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> 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 "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
-(*apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})*)
-sorry
+
+lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> 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 "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. \<lbrakk>x = Var a; xa = Var b; a = b\<rbrakk> \<Longrightarrow> P\<Colon>bool;
\<And>(x\<Colon>lam) (xa\<Colon>lam) (xb\<Colon>lam) xc\<Colon>lam. \<lbrakk>x = App x xb; xa = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
\<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam. \<lbrakk>x = Lam a x; xa = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
\<Longrightarrow> 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 "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> 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 *})
--- 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