# HG changeset patch
# User paulson
# Date 865000527 -7200
# Node ID 7091ffa99c93ff088a2fbb5d451cff6987bee531
# Parent  11f4884a071a3a864caa6bb944a7a3f7620e51bb
Simplified the calling sequence of CONTEXT_REWRITE_RULE
Eliminated get_rhs, which was calling dest_Trueprop too many times

diff -r 11f4884a071a -r 7091ffa99c93 TFL/rules.new.sml
--- 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)) 
diff -r 11f4884a071a -r 7091ffa99c93 TFL/rules.sig
--- 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 
 
diff -r 11f4884a071a -r 7091ffa99c93 TFL/tfl.sml
--- 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,