Use conversions instead of simplifier. tuned
--- a/src/HOL/Tools/function_package/context_tree.ML Tue Mar 04 13:35:45 2008 +0100
+++ b/src/HOL/Tools/function_package/context_tree.ML Wed Mar 05 12:24:52 2008 +0100
@@ -104,8 +104,9 @@
fun mk_branch ctx t =
let
val (ctx', fixes, impl) = dest_all_all_ctx ctx t
+ val assms = Logic.strip_imp_prems impl
in
- (ctx', fixes, Logic.strip_imp_prems impl, rhs_of (Logic.strip_imp_concl impl))
+ (ctx', fixes, assms, rhs_of (Logic.strip_imp_concl impl))
end
fun find_cong_rule ctx fvar h ((r,dep)::rs) t =
@@ -231,40 +232,37 @@
snd o traverse_help ([], []) tr []
end
-val is_refl = op aconv o Logic.dest_equals o prop_of
-
fun rewrite_by_tree thy h ih x tr =
let
- fun rewrite_help fix f_as h_as x (Leaf t) = (reflexive (cterm_of thy t), x)
- | rewrite_help fix f_as h_as x (RCall (_ $ arg, st)) =
+ fun rewrite_help _ _ x (Leaf t) = (reflexive (cterm_of thy t), x)
+ | rewrite_help fix h_as x (RCall (_ $ arg, st)) =
let
- val (inner, (lRi,ha)::x') = rewrite_help fix f_as h_as x st
+ val (inner, (lRi,ha)::x') = rewrite_help fix h_as x st (* "a' = a" *)
- (* Need not use the simplifier here. Can use primitive steps! *)
- val rew_ha = if is_refl inner then I else simplify (HOL_basic_ss addsimps [inner])
-
- val h_a_eq_h_a' = combination (reflexive (cterm_of thy h)) inner
val iha = import_thm thy (fix, h_as) ha (* (a', h a') : G *)
- |> rew_ha
-
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.comb_conv (Conv.arg_conv (K inner))))
+ (* (a, h a) : G *)
val inst_ih = instantiate' [] [SOME (cterm_of thy arg)] ih
- val eq = implies_elim (implies_elim inst_ih lRi) iha
+ val eq = implies_elim (implies_elim inst_ih lRi) iha (* h a = f a *)
- val h_a'_eq_f_a' = eq RS eq_reflection
- val result = transitive h_a_eq_h_a' h_a'_eq_f_a'
+ val h_a'_eq_h_a = combination (reflexive (cterm_of thy h)) inner
+ val h_a_eq_f_a = eq RS eq_reflection
+ val result = transitive h_a'_eq_h_a h_a_eq_f_a
in
(result, x')
end
- | rewrite_help fix f_as h_as x (Cong (crule, deps, branches)) =
+ | rewrite_help fix h_as x (Cong (crule, deps, branches)) =
let
fun sub_step lu i x =
let
val ((fixes, assumes), st) = nth branches i
- val used = fold_rev (cons o lu) (IntGraph.imm_succs deps i) []
- val used_rev = map (fn u_eq => (u_eq RS sym) RS eq_reflection) used
- val assumes' = map (simplify (HOL_basic_ss addsimps (filter_out is_refl used_rev))) assumes
+ val used = map lu (IntGraph.imm_succs deps i)
+ |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
+ |> filter_out Thm.is_reflexive
+
+ val assumes' = map (simplify (HOL_basic_ss addsimps used)) assumes
- val (subeq, x') = rewrite_help (fix @ fixes) (f_as @ assumes) (h_as @ assumes') x st
+ val (subeq, x') = rewrite_help (fix @ fixes) (h_as @ assumes') x st
val subeq_exp = export_thm thy (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
in
(subeq_exp, x')
@@ -275,7 +273,7 @@
(fold_rev (curry op COMP) subthms crule, x')
end
in
- rewrite_help [] [] [] x tr
+ rewrite_help [] [] x tr
end
end
--- a/src/HOL/Tools/function_package/fundef_core.ML Tue Mar 04 13:35:45 2008 +0100
+++ b/src/HOL/Tools/function_package/fundef_core.ML Wed Mar 05 12:24:52 2008 +0100
@@ -295,15 +295,16 @@
fun mk_replacement_lemma thy h ih_elim clause =
let
val ClauseInfo {cdata=ClauseContext {qs, lhs, rhs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
+ local open Conv in
+ val ih_conv = arg1_conv o arg_conv o arg_conv
+ end
- val ih_elim_case = full_simplify (HOL_basic_ss addsimps [case_hyp]) ih_elim
+ val ih_elim_case = Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_elim
val Ris = map (fn RCInfo {llRI, ...} => llRI) RCs
val h_assums = map (fn RCInfo {h_assum, ...} => assume (cterm_of thy (subst_bounds (rev qs, h_assum)))) RCs
- val ih_elim_case_inst = instantiate' [] [NONE, SOME (cterm_of thy h)] ih_elim_case (* Should be done globally *)
-
- val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case_inst (Ris ~~ h_assums) tree
+ val (eql, _) = FundefCtxTree.rewrite_by_tree thy h ih_elim_case (Ris ~~ h_assums) tree
val replace_lemma = (eql RS meta_eq_to_obj_eq)
|> implies_intr (cprop_of case_hyp)
@@ -418,6 +419,7 @@
val ihyp_thm = assume ihyp |> forall_elim_vars 0
val ih_intro = ihyp_thm RS (f_def RS ex1_implies_ex)
val ih_elim = ihyp_thm RS (f_def RS ex1_implies_un)
+ |> instantiate' [] [NONE, SOME (cterm_of thy h)]
val _ = Output.debug (K "Proving Replacement lemmas...")
val repLemmas = map (mk_replacement_lemma thy h ih_elim) clauses
@@ -575,6 +577,9 @@
val acc_subset_induct = @{thm Orderings.predicate1I} RS @{thm Accessible_Part.accp_subset_induct}
+
+val binder_conv = Conv.arg_conv oo Conv.abs_conv
+
fun mk_partial_induct_rule thy globals R complete_thm clauses =
let
val Globals {domT, x, z, a, P, D, ...} = globals
@@ -603,12 +608,14 @@
fun prove_case clause =
let
- val ClauseInfo {cdata = ClauseContext {qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
+ val ClauseInfo {cdata = ClauseContext {ctxt, qs, cqs, ags, gs, lhs, case_hyp, ...}, RCs,
qglr = (oqs, _, _, _), ...} = clause
- val replace_x_ss = HOL_basic_ss addsimps [case_hyp]
- val lhs_D = simplify replace_x_ss x_D (* lhs : D *)
- val sih = full_simplify replace_x_ss aihyp
+ val case_hyp_conv = K (case_hyp RS eq_reflection)
+ local open Conv in
+ val lhs_D = fconv_rule (arg_conv (arg_conv (case_hyp_conv))) x_D
+ val sih = fconv_rule (binder_conv (K (arg1_conv (arg_conv (arg_conv case_hyp_conv)))) ctxt) aihyp
+ end
fun mk_Prec (RCInfo {llRI, RIvs, CCas, rcarg, ...}) =
sih |> forall_elim (cterm_of thy rcarg)
@@ -632,7 +639,7 @@
|> fold Thm.elim_implies P_recs
val res = cterm_of thy (HOLogic.mk_Trueprop (P $ x))
- |> Simplifier.rewrite replace_x_ss
+ |> Conv.arg_conv (Conv.arg_conv case_hyp_conv)
|> symmetric (* P lhs == P x *)
|> (fn eql => equal_elim eql P_lhs) (* "P x" *)
|> implies_intr (cprop_of case_hyp)
@@ -720,7 +727,7 @@
val used = map (fn (ctx,thm) => FundefCtxTree.export_thm thy ctx thm) (u @ sub)
val hyp = HOLogic.mk_Trueprop (R' $ arg $ lhs)
- |> fold_rev (curry Logic.mk_implies o prop_of) used
+ |> fold_rev (curry Logic.mk_implies o prop_of) used (* additional hyps *)
|> FundefCtxTree.export_term (fixes, assumes)
|> fold_rev (curry Logic.mk_implies o prop_of) ags
|> fold_rev mk_forall_rename (map fst oqs ~~ qs)
@@ -729,25 +736,18 @@
val thm = assume hyp
|> fold forall_elim cqs
|> fold Thm.elim_implies ags
- |> FundefCtxTree.import_thm thy (fixes, assumes) (* "(arg, lhs) : R'" *)
- |> fold Thm.elim_implies used
-
- val acc = thm COMP ih_case
+ |> FundefCtxTree.import_thm thy (fixes, assumes)
+ |> fold Thm.elim_implies used (* "(arg, lhs) : R'" *)
- val z_eq_arg = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_eq (z, arg)))
-
- val arg_eq_z = (assume z_eq_arg) RS sym
-
- val z_acc = simplify (HOL_basic_ss addsimps [arg_eq_z]) acc (* fragile, slow... *)
- |> implies_intr (cprop_of case_hyp)
- |> implies_intr z_eq_arg
+ val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
- val z_eq_arg = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (z, arg))))
- val x_eq_lhs = assume (cterm_of thy (HOLogic.mk_Trueprop (mk_eq (x, lhs))))
-
- val ethm = (z_acc OF [z_eq_arg, x_eq_lhs])
+ val acc = thm COMP ih_case
+ val z_acc_local = acc
+ |> Conv.fconv_rule (Conv.arg_conv (Conv.arg_conv (K (symmetric (z_eq_arg RS eq_reflection)))))
+
+ val ethm = z_acc_local
|> FundefCtxTree.export_thm thy (fixes,
- z_eq_arg :: x_eq_lhs :: ags @ assumes)
+ z_eq_arg :: case_hyp :: ags @ assumes)
|> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
val sub' = sub @ [(([],[]), acc)]
--- a/src/HOL/Tools/function_package/mutual.ML Tue Mar 04 13:35:45 2008 +0100
+++ b/src/HOL/Tools/function_package/mutual.ML Wed Mar 05 12:24:52 2008 +0100
@@ -168,8 +168,6 @@
end
-fun beta_reduce thm = Thm.equal_elim (Thm.beta_conversion true (cprop_of thm)) thm
-
fun in_context ctxt (f, pre_qs, pre_gs, pre_args, pre_rhs) F =
let
val thy = ProofContext.theory_of ctxt
@@ -222,7 +220,7 @@
val xs = map_index (fn (i,T) => cterm_of thy (Free ("x" ^ string_of_int i, T))) caTs (* FIXME: Bind xs properly *)
in
fold (fn x => fn thm => combination thm (reflexive x)) xs thm
- |> beta_reduce
+ |> Conv.fconv_rule (Thm.beta_conversion true)
|> fold_rev forall_intr xs
|> forall_elim_vars 0
end