TFL/post.sml

     Copyright   1997  University of Cambridge
 
 Postprocessing of TFL definitions
 *)
 
-(*-------------------------------------------------------------------------
-Three postprocessors are applied to the definition:
-    - a wellfoundedness prover (WF_TAC)
-    - a simplifier (tries to eliminate the language of termination expressions)
-    - a termination prover
-*-------------------------------------------------------------------------*)
-
 signature TFL = 
   sig
    structure Prim : TFL_sig
 
    val tgoalw : theory -> thm list -> thm list -> thm list
    val tgoal: theory -> thm list -> thm list
 
-   val WF_TAC : thm list -> tactic
-
-   val simplifier : thm -> thm
-   val std_postprocessor : theory 
+   val std_postprocessor : simpset -> theory 
                            -> {induction:thm, rules:thm, TCs:term list list} 
                            -> {induction:thm, rules:thm, nested_tcs:thm list}
 
    val define_i : theory -> string -> term -> term list
-                  -> theory * (thm * Prim.pattern list)
+                  -> theory * Prim.pattern list
 
    val define   : theory -> string -> string -> string list 
                   -> theory * Prim.pattern list
 
-   val simplify_defn : theory * (string * Prim.pattern list)
+   val simplify_defn : simpset -> theory * (string * Prim.pattern list)
                         -> {rules:thm list, induct:thm, tcs:term list}
 
   (*-------------------------------------------------------------------------
        val function : theory -> term -> {theory:theory, eq_ind : thm}
        val lazyR_def: theory -> term -> {theory:theory, eqns : thm}

 (*---------------------------------------------------------------------------
  * Extract termination goals so that they can be put it into a goalstack, or 
  * have a tactic directly applied to them.
  *--------------------------------------------------------------------------*)
 fun termination_goals rules = 
-    map (Logic.freeze_vars o HOLogic.dest_Trueprop)
+    map (#1 o Type.freeze_thaw o HOLogic.dest_Trueprop)
       (foldr (fn (th,A) => union_term (prems_of th, A)) (rules, []));
 
- (*---------------------------------------------------------------------------
-  * Finds the termination conditions in (highly massaged) definition and 
-  * puts them into a goalstack.
-  *--------------------------------------------------------------------------*)
- fun tgoalw thy defs rules = 
-    let val L = termination_goals rules
-        open USyntax
-        val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
-    in goalw_cterm defs g
-    end;
-
- fun tgoal thy = tgoalw thy [];
-
- (*---------------------------------------------------------------------------
-  * Simple wellfoundedness prover.
-  *--------------------------------------------------------------------------*)
- fun WF_TAC thms = REPEAT(FIRST1(map rtac thms))
- val WFtac = WF_TAC[wf_measure, wf_inv_image, wf_lex_prod, wf_less_than, 
-                    wf_trancl];
-
- val terminator = simp_tac(!simpset addsimps [less_Suc_eq]) 1
-                  THEN TRY(best_tac
-                           (!claset addSDs [not0_implies_Suc]
-                                    addss (!simpset)) 1);
-
- val simpls = [less_eq RS eq_reflection,
-               lex_prod_def, measure_def, inv_image_def];
-
- (*---------------------------------------------------------------------------
-  * Does some standard things with the termination conditions of a definition:
-  * attempts to prove wellfoundedness of the given relation; simplifies the
-  * non-proven termination conditions; and finally attempts to prove the 
-  * simplified termination conditions.
-  *--------------------------------------------------------------------------*)
- val std_postprocessor = Prim.postprocess{WFtac = WFtac,
-                                    terminator = terminator, 
-                                    simplifier = Rules.simpl_conv simpls};
-
- val simplifier = rewrite_rule (simpls @ #simps(rep_ss (!simpset)) @ 
-                                [pred_list_def]);
-
- fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
+(*---------------------------------------------------------------------------
+ * Finds the termination conditions in (highly massaged) definition and 
+ * puts them into a goalstack.
+ *--------------------------------------------------------------------------*)
+fun tgoalw thy defs rules = 
+   let val L = termination_goals rules
+       open USyntax
+       val g = cterm_of (sign_of thy) (HOLogic.mk_Trueprop(list_mk_conj L))
+   in goalw_cterm defs g
+   end;
+
+fun tgoal thy = tgoalw thy [];
+
+(*---------------------------------------------------------------------------
+* Three postprocessors are applied to the definition.  It
+* attempts to prove wellfoundedness of the given relation, simplifies the
+* non-proved termination conditions, and finally attempts to prove the 
+* simplified termination conditions.
+*--------------------------------------------------------------------------*)
+fun std_postprocessor ss =
+  Prim.postprocess
+   {WFtac      = REPEAT (ares_tac [wf_measure, wf_inv_image, wf_lex_prod, 
+				   wf_less_than, wf_trancl] 1),
+    terminator = asm_simp_tac ss 1
+		 THEN TRY(best_tac
+			  (!claset addSDs [not0_implies_Suc] addss ss) 1),
+    simplifier = Rules.simpl_conv ss []};
+
+fun tflcongs thy = Prim.Context.read() @ (#case_congs(Thry.extract_info thy));
 
 
 val concl = #2 o Rules.dest_thm;
 
 (*---------------------------------------------------------------------------
  * Defining a function with an associated termination relation. 
  *---------------------------------------------------------------------------*)
 fun define_i thy fid R eqs = 
   let val dummy = require_thy thy "WF_Rel" "recursive function definitions"
       val {functional,pats} = Prim.mk_functional thy eqs
-      val (thm,thry) = Prim.wfrec_definition0 thy fid R functional
-  in (thry,(thm,pats))
+  in (Prim.wfrec_definition0 thy fid R functional, pats)
   end;
 
 (*lcp's version: takes strings; doesn't return "thm" 
         (whose signature is a draft and therefore useless) *)
 fun define thy fid R eqs = 
   let fun read thy = readtm (sign_of thy) (TVar(("DUMMY",0),[])) 
-      val (thy',(_,pats)) =
-             define_i thy fid (read thy R) (map (read thy) eqs)
-  in  (thy',pats)  end
+  in  define_i thy fid (read thy R) (map (read thy) eqs)  end
   handle Utils.ERR {mesg,...} => error mesg;
 
 (*---------------------------------------------------------------------------
  * Postprocess a definition made by "define". This is a separate stage of 
  * processing from the definition stage.

 val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
 fun mk_meta_eq r = case concl_of r of
      Const("==",_)$_$_ => r
   |   _$(Const("op =",_)$_$_) => r RS eq_reflection
   |   _ => r RS P_imp_P_eq_True
+
+(*Is this the best way to invoke the simplifier??*)
 fun rewrite L = rewrite_rule (map mk_meta_eq (filter(not o id_thm) L))
-fun reducer thl = rewrite (map standard thl @ #simps(rep_ss (!simpset)))
 
 fun join_assums th = 
   let val {sign,...} = rep_thm th
       val tych = cterm_of sign
       val {lhs,rhs} = S.dest_eq(#2 (S.strip_forall (concl th)))

       (R.DISCH_ALL 
          (rewrite (map (R.ASSUME o tych) cntxt) (R.SPEC_ALL th)))
   end
   val gen_all = S.gen_all
 in
-(*---------------------------------------------------------------------------
- * The "reducer" argument is 
- *  (fn thl => rewrite (map standard thl @ #simps(rep_ss (!simpset)))); 
- *---------------------------------------------------------------------------*)
-fun proof_stage theory reducer {f, R, rules, full_pats_TCs, TCs} =
+fun proof_stage ss theory {f, R, rules, full_pats_TCs, TCs} =
   let val dummy = prs "Proving induction theorem..  "
       val ind = Prim.mk_induction theory f R full_pats_TCs
-      val dummy = writeln "Proved induction theorem."
-      val pp = std_postprocessor theory
-      val dummy = prs "Postprocessing..  "
-      val {rules,induction,nested_tcs} = pp{rules=rules,induction=ind,TCs=TCs}
+      val dummy = prs "Proved induction theorem.\nPostprocessing..  "
+      val {rules, induction, nested_tcs} = 
+	  std_postprocessor ss theory {rules=rules, induction=ind, TCs=TCs}
   in
   case nested_tcs
   of [] => (writeln "Postprocessing done.";
             {induction=induction, rules=rules,tcs=[]})
   | L  => let val dummy = prs "Simplifying nested TCs..  "

                U.itlist (fn th => fn (So,Si,St) =>
                      if (id_thm th) then (So, Si, th::St) else
                      if (solved th) then (th::So, Si, St) 
                      else (So, th::Si, St)) nested_tcs ([],[],[])
               val simplified' = map join_assums simplified
-              val induction' = reducer (solved@simplified') induction
-              val rules' = reducer (solved@simplified') rules
+              val rewr = rewrite (solved @ simplified' @ #simps(rep_ss ss))
+              val induction' = rewr induction
+              and rules'     = rewr rules
               val dummy = writeln "Postprocessing done."
           in
           {induction = induction',
                rules = rules',
                  tcs = map (gen_all o S.rhs o #2 o S.strip_forall o concl)

 				  ORELSE' etac conjE));
 
 (*Strip off the outer !P*)
 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
 
-
-fun simplify_defn (thy,(id,pats)) =
+val wf_rel_defs = [lex_prod_def, measure_def, inv_image_def];
+
+fun simplify_defn ss (thy,(id,pats)) =
    let val dummy = deny (id  mem  map ! (stamps_of_thy thy))
                         ("Recursive definition " ^ id ^ 
                          " would clash with the theory of the same name!")
-       val def = freezeT(get_def thy id  RS  meta_eq_to_obj_eq)
+       val def =  freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
+       val ss' = ss addsimps ((less_Suc_eq RS iffD2) :: wf_rel_defs)
        val {theory,rules,TCs,full_pats_TCs,patterns} = 
-                Prim.post_definition (thy,(def,pats))
+                Prim.post_definition ss' (thy,(def,pats))
        val {lhs=f,rhs} = S.dest_eq(concl def)
        val (_,[R,_]) = S.strip_comb rhs
        val {induction, rules, tcs} = 
-             proof_stage theory reducer
+             proof_stage ss' theory 
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
        val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
    in  {induct = meta_outer

         rules = rules', 
         tcs = (termination_goals rules') @ tcs}
    end
   handle Utils.ERR {mesg,func,module} => 
                error (mesg ^ 
-		      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")")
-       |  e => print_exn e;
+		      "\n    (In TFL function " ^ module ^ "." ^ func ^ ")");
 end;
 
 (*---------------------------------------------------------------------------
  *
  *     Definitions with synthesized termination relation temporarily

      val induction = Prim.mk_induction theory f R full_pats_TCs
      val dummy = prs "Induction theorem proved.\n"
  in {theory = theory, 
      eq_ind = standard (induction RS (rules RS conjI))}
  end
- handle    e              => print_exn e
 end;
 
 
 fun lazyR_def theory eqs = 
    let val {rules,theory, ...} = Prim.lazyR_def theory eqs