Simplified the calling sequence of CONTEXT_REWRITE_RULE
Eliminated get_rhs, which was calling dest_Trueprop too many times
--- a/TFL/rules.new.sml Fri May 30 15:30:52 1997 +0200
+++ b/TFL/rules.new.sml Fri May 30 15:55:27 1997 +0200
@@ -442,13 +442,11 @@
fun dest_equal(Const ("==",_) $
- (Const ("Trueprop",_) $ lhs)
- $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
+ (Const ("Trueprop",_) $ lhs)
+ $ (Const ("Trueprop",_) $ rhs)) = {lhs=lhs, rhs=rhs}
| dest_equal(Const ("==",_) $ lhs $ rhs) = {lhs=lhs, rhs=rhs}
| dest_equal tm = S.dest_eq tm;
-
-fun get_rhs tm = #rhs(dest_equal (HOLogic.dest_Trueprop tm));
fun get_lhs tm = #lhs(dest_equal (HOLogic.dest_Trueprop tm));
fun variants FV vlist =
@@ -654,7 +652,7 @@
val restricted = U.can(S.find_term
(U.holds(fn c => (#Name(S.dest_const c)="cut"))))
-fun CONTEXT_REWRITE_RULE(func,R){thms=[cut_lemma],congs,th} =
+fun CONTEXT_REWRITE_RULE(func,R){cut_lemma, congs, th} =
let val tc_list = ref[]: term list ref
val dummy = term_ref := []
val dummy = thm_ref := []
@@ -690,7 +688,6 @@
val dummy = assert (forall (op aconv)
(ListPair.zip (vlist, args)))
"assertion failed in CONTEXT_REWRITE_RULE"
-(* val fbvs1 = variants (S.free_vars imp) fbvs *)
val imp_body1 = subst_free (ListPair.zip (args, vstrl))
imp_body
val tych = cterm_of sign
@@ -702,7 +699,7 @@
val mss' = add_prems(mss, map ASSUME ants1)
val Q1eeqQ2 = rewrite_cterm (false,true) mss' prover Q1
handle _ => reflexive Q1
- val Q2 = get_rhs(HOLogic.dest_Trueprop(#prop(rep_thm Q1eeqQ2)))
+ val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
val Q2eeqQ3 = symmetric(pbeta_reduce Q3 RS eq_reflection)
val thA = transitive(QeqQ1 RS eq_reflection) Q1eeqQ2
@@ -775,14 +772,16 @@
| _ => [S.list_mk_conj(map cncl rcontext)]
val TC = genl(S.list_mk_imp(antl, A))
val dummy = print_cterms "func:\n" [cterm_of sign func]
- val dummy = print_cterms "TC:\n" [cterm_of sign (HOLogic.mk_Trueprop TC)]
+ val dummy = print_cterms "TC:\n"
+ [cterm_of sign (HOLogic.mk_Trueprop TC)]
val dummy = tc_list := (TC :: !tc_list)
val nestedp = nested TC
- val dummy = if nestedp then say "nested\n" else say "not_nested\n"
+ val dummy = if nestedp then say"nested\n" else say"not_nested\n"
val dummy = term_ref := ([func,TC]@(!term_ref))
val th' = if nestedp then raise RULES_ERR{func = "solver",
mesg = "nested function"}
- else let val cTC = cterm_of sign (HOLogic.mk_Trueprop TC)
+ else let val cTC = cterm_of sign
+ (HOLogic.mk_Trueprop TC)
in case rcontext of
[] => SPEC_ALL(ASSUME cTC)
| _ => MP (SPEC_ALL (ASSUME cTC))
--- a/TFL/rules.sig Fri May 30 15:30:52 1997 +0200
+++ b/TFL/rules.sig Fri May 30 15:55:27 1997 +0200
@@ -50,14 +50,12 @@
val simpl_conv : thm list -> cterm -> thm
(* For debugging my isabelle solver in the conditional rewriter *)
-(*
val term_ref : term list ref
val thm_ref : thm list ref
val mss_ref : meta_simpset list ref
val tracing :bool ref
-*)
val CONTEXT_REWRITE_RULE : term * term
- -> {thms:thm list,congs: thm list, th:thm}
+ -> {cut_lemma:thm, congs: thm list, th:thm}
-> thm * term list
val RIGHT_ASSOC : thm -> thm
--- a/TFL/tfl.sml Fri May 30 15:30:52 1997 +0200
+++ b/TFL/tfl.sml Fri May 30 15:55:27 1997 +0200
@@ -426,9 +426,9 @@
val (case_rewrites,context_congs) = extraction_thms theory
val corollaries' = map(R.simplify case_rewrites) corollaries
fun xtract th = R.CONTEXT_REWRITE_RULE(f,R)
- {thms = [(R.ISPECL o map tych)[f,R] Thms.CUT_LEMMA],
- congs = context_congs,
- th = th}
+ {cut_lemma = R.ISPECL (map tych [f,R]) Thms.CUT_LEMMA,
+ congs = context_congs,
+ th = th}
val (rules, TCs) = ListPair.unzip (map xtract corollaries')
val rules0 = map (R.simplify [Thms.CUT_DEF]) rules
val mk_cond_rule = R.FILTER_DISCH_ALL(not o S.aconv WFR)
@@ -464,9 +464,9 @@
val corollaries = map (U.C R.SPEC corollary' o tych) given_pats
val corollaries' = map (R.simplify case_rewrites) corollaries
fun extract th = R.CONTEXT_REWRITE_RULE(f,R1)
- {thms = [(R.ISPECL o map tych)[f,R1] Thms.CUT_LEMMA],
- congs = context_congs,
- th = th}
+ {cut_lemma = R.ISPECL (map tych [f,R1]) Thms.CUT_LEMMA,
+ congs = context_congs,
+ th = th}
in {proto_def=proto_def,
WFR=WFR,
pats=pats,