TFL/rules.ML

 
   val rbeta : thm -> 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 mss_ref : MetaSimplifier.meta_simpset list ref
   val tracing : bool ref
   val CONTEXT_REWRITE_RULE : term * term list * thm * thm list
                              -> thm -> thm * term list
   val RIGHT_ASSOC : thm -> thm
 

 
 (*---------------------------------------------------------------------------
  * Trace information for the rewriter
  *---------------------------------------------------------------------------*)
 val term_ref = ref[] : term list ref
-val mss_ref = ref [] : meta_simpset list ref;
+val mss_ref = ref [] : MetaSimplifier.meta_simpset list ref;
 val thm_ref = ref [] : thm list ref;
 val tracing = ref false;
 
 fun say s = if !tracing then writeln s else ();
 

      val dummy = mss_ref  := []
      val cut_lemma' = cut_lemma RS eq_reflection
      fun prover used mss thm =
      let fun cong_prover mss thm =
          let val dummy = say "cong_prover:"
-             val cntxt = prems_of_mss mss
+             val cntxt = MetaSimplifier.prems_of_mss mss
              val dummy = print_thms "cntxt:" cntxt
              val dummy = say "cong rule:"
              val dummy = say (string_of_thm thm)
              val dummy = thm_ref := (thm :: !thm_ref)
              val dummy = mss_ref := (mss :: !mss_ref)

                  let val tych = cterm_of sign
                      val dummy = print_cterms "To eliminate:" [tych imp]
                      val ants = map tych (Logic.strip_imp_prems imp)
                      val eq = Logic.strip_imp_concl imp
                      val lhs = tych(get_lhs eq)
-                     val mss' = add_prems(mss, map ASSUME ants)
+                     val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants)
                      val lhs_eq_lhs1 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used) mss' lhs
                        handle U.ERR _ => Thm.reflexive lhs
                      val dummy = print_thms "proven:" [lhs_eq_lhs1]
                      val lhs_eq_lhs2 = implies_intr_list ants lhs_eq_lhs1
                      val lhs_eeq_lhs2 = lhs_eq_lhs2 RS meta_eq_to_obj_eq

                   val ants1 = map tych (Logic.strip_imp_prems imp_body1)
                   val eq1 = Logic.strip_imp_concl imp_body1
                   val Q = get_lhs eq1
                   val QeqQ1 = pbeta_reduce (tych Q)
                   val Q1 = #2(D.dest_eq(cconcl QeqQ1))
-                  val mss' = add_prems(mss, map ASSUME ants1)
+                  val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
                   val Q1eeqQ2 = MetaSimplifier.rewrite_cterm (false,true,false) (prover used') mss' Q1
                                 handle U.ERR _ => Thm.reflexive Q1
                   val Q2 = #2 (Logic.dest_equals (#prop(rep_thm Q1eeqQ2)))
                   val Q3 = tych(list_comb(list_mk_aabs(vstrl,Q2),vstrl))
                   val Q2eeqQ3 = Thm.symmetric(pbeta_reduce Q3 RS eq_reflection)

               in if (pbeta_redex Q) (length vlist)
                  then pq_eliminate (thm,sign,vlist,imp_body,Q)
                  else
                  let val tych = cterm_of sign
                      val ants1 = map tych ants
-                     val mss' = add_prems(mss, map ASSUME ants1)
+                     val mss' = MetaSimplifier.add_prems(mss, map ASSUME ants1)
                      val Q_eeq_Q1 = MetaSimplifier.rewrite_cterm
                         (false,true,false) (prover used') mss' (tych Q)
                       handle U.ERR _ => Thm.reflexive (tych Q)
                      val lhs_eeq_lhs2 = implies_intr_list ants1 Q_eeq_Q1
                      val lhs_eq_lhs2 = lhs_eeq_lhs2 RS meta_eq_to_obj_eq

          in Some(eliminate (rename thm)) end
          handle U.ERR _ => None    (* FIXME handle THM as well?? *)
 
         fun restrict_prover mss thm =
           let val dummy = say "restrict_prover:"
-              val cntxt = rev(prems_of_mss mss)
+              val cntxt = rev(MetaSimplifier.prems_of_mss mss)
               val dummy = print_thms "cntxt:" cntxt
               val {prop = Const("==>",_) $ (Const("Trueprop",_) $ A) $ _,
                    sign,...} = rep_thm thm
               fun genl tm = let val vlist = gen_rems (op aconv)
                                            (add_term_frees(tm,[]), globals)

     (if (is_cong thm) then cong_prover else restrict_prover) mss thm
     end
     val ctm = cprop_of th
     val names = add_term_names (term_of ctm, [])
     val th1 = MetaSimplifier.rewrite_cterm(false,true,false)
-      (prover names) (add_congs(mss_of [cut_lemma'], congs)) ctm
+      (prover names) (MetaSimplifier.add_congs(MetaSimplifier.mss_of [cut_lemma'], congs)) ctm
     val th2 = equal_elim th1 th
  in
  (th2, filter (not o restricted) (!tc_list))
  end;