--- a/LFex.thy Sat Nov 28 07:44:17 2009 +0100
+++ b/LFex.thy Sat Nov 28 08:04:23 2009 +0100
@@ -226,72 +226,7 @@
apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
prefer 2
ML_prf {* val quot = @{thms QUOTIENT_KIND QUOTIENT_TY QUOTIENT_TRM} *}
-ML_prf {*
-fun make_inst lhs t =
- let
- val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
- val _ $ (Abs (_, _, g)) = t;
- fun mk_abs i t =
- if incr_boundvars i u aconv t then Bound i
- else (case t of
- t1 $ t2 => mk_abs i t1 $ mk_abs i t2
- | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')
- | Bound j => if i = j then error "make_inst" else t
- | _ => t);
- in (f, Abs ("x", T, mk_abs 0 g)) end;
-*}
-
-ML_prf {*
-fun lambda_prs_conv1 ctxt quot_thms 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_thms);
- 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 @{thms id_simps} te
- val tl = Thm.lhs_of ts;
- val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
- val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
-(* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
- in
-(* Conv.all_conv ctrm*)
- Conv.rewr_conv ti ctrm
- end
-(* TODO: We can add a proper error message... *)
- handle Bind => Conv.all_conv ctrm
-
-*}
-
-(* quot stands for the QUOTIENT theorems: *)
-(* could be potentially all of them *)
-ML_prf {*
-fun lambda_prs_conv ctxt quot ctrm =
- case (term_of ctrm) of
- (Const (@{const_name "fun_map"}, _) $ _ $ _) $ (Abs _) =>
- (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_prf {*
-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)
-*}
+(*apply(tactic {* clean_tac @{context} quot defs aps 1 *}) *)
apply (tactic {* lambda_prs_tac @{context} quot 1 *})
ML_prf {* val lower = flat (map (add_lower_defs @{context}) defs) *}
ML_prf {* val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower *}
--- a/QuotMain.thy Sat Nov 28 07:44:17 2009 +0100
+++ b/QuotMain.thy Sat Nov 28 08:04:23 2009 +0100
@@ -1066,6 +1066,19 @@
It proves the QUOTIENT assumptions by calling quotient_tac
*)
ML {*
+fun make_inst lhs t =
+ let
+ val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+ val _ $ (Abs (_, _, g)) = t;
+ fun mk_abs i t =
+ if incr_boundvars i u aconv t then Bound i
+ else (case t of
+ t1 $ t2 => mk_abs i t1 $ mk_abs i t2
+ | Abs (s, T, t') => Abs (s, T, mk_abs (i+1) t')
+ | Bound j => if i = j then error "make_inst" else t
+ | _ => t);
+ in (f, Abs ("x", T, mk_abs 0 g)) end;
+
fun lambda_prs_conv1 ctxt quot_thms ctrm =
case (term_of ctrm) of ((Const (@{const_name "fun_map"}, _) $ r1 $ a2) $ (Abs _)) =>
let
@@ -1083,21 +1096,16 @@
val t = Goal.prove_internal [] gc (fn _ => tac 1)
val te = @{thm eq_reflection} OF [t]
val ts = MetaSimplifier.rewrite_rule @{thms id_simps} 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)));*)
+ val tl = Thm.lhs_of ts;
+ val (insp, inst) = make_inst (term_of tl) (term_of ctrm);
+ val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts;
+(* val _ = writeln (Syntax.string_of_term @{context} (term_of (cprop_of ti)));*)
in
Conv.rewr_conv ti ctrm
end
-(* TODO: We can add a proper error message... *)
- handle Bind => Conv.all_conv ctrm
-
*}
-(* quot stands for the QUOTIENT theorems: *)
+(* quot stands for the QUOTIENT theorems: *)
(* could be potentially all of them *)
ML {*
fun lambda_prs_conv ctxt quot ctrm =
@@ -1122,15 +1130,18 @@
fun clean_tac lthy quot defs aps =
let
val lower = flat (map (add_lower_defs lthy) defs)
+ val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} 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
+ val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower)
val aps_thms = map (applic_prs lthy absrep) aps
in
- EVERY' [TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
- lambda_prs_tac lthy quot,
+ EVERY' [lambda_prs_tac lthy quot,
+ TRY o simp_tac simp_ctxt,
+ TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
- TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower),
- simp_tac (HOL_ss addsimps reps_same)]
+ rtac refl]
end
*}