# HG changeset patch
# User wenzelm
# Date 1001697815 -7200
# Node ID 6fc8de600f5869eb751d1183fafb83ff4521c6c7
# Parent  b325c05709d3f8257610bf2bd9634a8664ded5fd
prove: ``strict'' argument;

diff -r b325c05709d3 -r 6fc8de600f58 TFL/post.ML
--- a/TFL/post.ML	Fri Sep 28 19:23:07 2001 +0200
+++ b/TFL/post.ML	Fri Sep 28 19:23:35 2001 +0200
@@ -13,12 +13,9 @@
   val message: string -> unit
   val tgoalw: theory -> thm list -> thm list -> thm list
   val tgoal: theory -> thm list -> thm list
-  val std_postprocessor: claset -> simpset -> thm list -> theory ->
-    {induction: thm, rules: thm, TCs: term list list} ->
-    {induction: thm, rules: thm, nested_tcs: thm list}
-  val define_i: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
+  val define_i: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
     term -> term list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
-  val define: theory -> claset -> simpset -> thm list -> thm list -> xstring ->
+  val define: bool -> theory -> claset -> simpset -> thm list -> thm list -> xstring ->
     string -> string list -> theory * {rules: (thm * int) list, induct: thm, tcs: term list}
   val defer_i: theory -> thm list -> xstring -> term list -> theory * thm
   val defer: theory -> thm list -> xstring -> string list -> theory * thm
@@ -70,8 +67,8 @@
  * non-proved termination conditions, and finally attempts to prove the
  * simplified termination conditions.
  *--------------------------------------------------------------------------*)
-fun std_postprocessor cs ss wfs =
-  Prim.postprocess
+fun std_postprocessor strict cs ss wfs =
+  Prim.postprocess strict
    {wf_tac     = REPEAT (ares_tac wfs 1),
     terminator = asm_simp_tac ss 1
                  THEN TRY (fast_tac (cs addSDs [not0_implies_Suc] addss ss) 1),
@@ -123,13 +120,13 @@
   end
   val gen_all = S.gen_all
 in
-fun proof_stage cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
+fun proof_stage strict cs ss wfs theory {f, R, rules, full_pats_TCs, TCs} =
   let
     val _ = message "Proving induction theorem ..."
     val ind = Prim.mk_induction theory {fconst=f, R=R, SV=[], pat_TCs_list=full_pats_TCs}
     val _ = message "Postprocessing ...";
     val {rules, induction, nested_tcs} =
-      std_postprocessor cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
+      std_postprocessor strict cs ss wfs theory {rules=rules, induction=ind, TCs=TCs}
   in
   case nested_tcs
   of [] => {induction=induction, rules=rules,tcs=[]}
@@ -164,13 +161,13 @@
 (*Strip off the outer !P*)
 val spec'= read_instantiate [("x","P::?'b=>bool")] spec;
 
-fun simplify_defn thy cs ss congs wfs id pats def0 =
+fun simplify_defn strict thy cs ss congs wfs id pats def0 =
    let val def = freezeT def0 RS meta_eq_to_obj_eq
        val {theory,rules,rows,TCs,full_pats_TCs} = Prim.post_definition congs (thy, (def,pats))
        val {lhs=f,rhs} = S.dest_eq (concl def)
        val (_,[R,_]) = S.strip_comb rhs
        val {induction, rules, tcs} =
-             proof_stage cs ss wfs theory
+             proof_stage strict cs ss wfs theory
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
@@ -186,13 +183,13 @@
 (*---------------------------------------------------------------------------
  * Defining a function with an associated termination relation.
  *---------------------------------------------------------------------------*)
-fun define_i thy cs ss congs wfs fid R eqs =
+fun define_i strict thy cs ss congs wfs fid R eqs =
   let val {functional,pats} = Prim.mk_functional thy eqs
       val (thy, def) = Prim.wfrec_definition0 thy (Sign.base_name fid) R functional
-  in (thy, simplify_defn thy cs ss congs wfs fid pats def) end;
+  in (thy, simplify_defn strict thy cs ss congs wfs fid pats def) end;
 
-fun define thy cs ss congs wfs fid R seqs =
-  define_i thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
+fun define strict thy cs ss congs wfs fid R seqs =
+  define_i strict thy cs ss congs wfs fid (read_term thy R) (map (read_term thy) seqs)
     handle U.ERR {mesg,...} => error mesg;
 
 
diff -r b325c05709d3 -r 6fc8de600f58 TFL/rules.ML
--- a/TFL/rules.ML	Fri Sep 28 19:23:07 2001 +0200
+++ b/TFL/rules.ML	Fri Sep 28 19:23:35 2001 +0200
@@ -57,7 +57,7 @@
                              -> thm -> thm * term list
   val RIGHT_ASSOC : thm -> thm
 
-  val prove : cterm * tactic -> thm
+  val prove : bool -> cterm * tactic -> thm
 end;
 
 structure Rules: RULES =
@@ -813,11 +813,13 @@
  end;
 
 
-fun prove (ptm, tac) =
+fun prove strict (ptm, tac) =
   let val result =
-    Library.transform_error (fn () =>
-      Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
-    handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg)
+    if strict then Goals.prove_goalw_cterm [] ptm (fn _ => [tac])
+    else
+      Library.transform_error (fn () =>
+        Goals.prove_goalw_cterm [] ptm (fn _ => [tac])) ()
+      handle ERROR_MESSAGE msg => (warning msg; raise RULES_ERR "prove" msg);
   in #1 (freeze_thaw result) end;
 
 
diff -r b325c05709d3 -r 6fc8de600f58 TFL/tfl.ML
--- a/TFL/tfl.ML	Fri Sep 28 19:23:07 2001 +0200
+++ b/TFL/tfl.ML	Fri Sep 28 19:23:35 2001 +0200
@@ -33,9 +33,9 @@
     patterns : pattern list}
   val mk_induction: theory ->
     {fconst: term, R: term, SV: term list, pat_TCs_list: (term * term list) list} -> thm
-  val postprocess: {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm} -> theory ->
-    {rules: thm, induction: thm, TCs: term list list} ->
-    {rules: thm, induction: thm, nested_tcs: thm list}
+  val postprocess: bool -> {wf_tac: tactic, terminator: tactic, simplifier: cterm -> thm}
+    -> theory -> {rules: thm, induction: thm, TCs: term list list}
+    -> {rules: thm, induction: thm, nested_tcs: thm list}
 end;
 
 structure Prim: PRIM =
@@ -909,14 +909,15 @@
    (R.MP rule tcthm, R.PROVE_HYP tcthm induction)
 
 
-fun postprocess{wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
+fun postprocess strict {wf_tac, terminator, simplifier} theory {rules,induction,TCs} =
 let val tych = Thry.typecheck theory
+    val prove = R.prove strict;
 
    (*---------------------------------------------------------------------
     * Attempt to eliminate WF condition. It's the only assumption of rules
     *---------------------------------------------------------------------*)
    val (rules1,induction1)  =
-       let val thm = R.prove(tych(HOLogic.mk_Trueprop
+       let val thm = prove(tych(HOLogic.mk_Trueprop
                                   (hd(#1(R.dest_thm rules)))),
                              wf_tac)
        in (R.PROVE_HYP thm rules,  R.PROVE_HYP thm induction)
@@ -948,7 +949,7 @@
        elim_tc (R.MATCH_MP Thms.eqT tc_eq) (r,ind)
        handle U.ERR _ =>
         (elim_tc (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
-                  (R.prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
+                  (prove(tych(HOLogic.mk_Trueprop(S.rhs(concl tc_eq))),
                            terminator)))
                  (r,ind)
          handle U.ERR _ =>
@@ -976,7 +977,7 @@
        (R.MATCH_MP Thms.eqT tc_eq
         handle U.ERR _ =>
           (R.MATCH_MP(R.MATCH_MP Thms.rev_eq_mp tc_eq)
-                      (R.prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
+                      (prove(tych(HOLogic.mk_Trueprop (S.rhs(concl tc_eq))),
                                terminator))
             handle U.ERR _ => tc_eq))
       end