# HG changeset patch
# User krauss
# Date 1256862726 -3600
# Node ID 37ec56ac3fd43b578fea01d413f7b6712bbc48aa
# Parent  b2b78c5ef7719c02a5d0ef7e1e3ab315db0e14cd
less verbose termination tactics

diff -r b2b78c5ef771 -r 37ec56ac3fd4 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Oct 30 01:32:06 2009 +0100
@@ -6,8 +6,8 @@
 
 signature LEXICOGRAPHIC_ORDER =
 sig
-  val lex_order_tac : Proof.context -> tactic -> tactic
-  val lexicographic_order_tac : Proof.context -> tactic
+  val lex_order_tac : bool -> Proof.context -> tactic -> tactic
+  val lexicographic_order_tac : bool -> Proof.context -> tactic
   val lexicographic_order : Proof.context -> Proof.method
 
   val setup: theory -> theory
@@ -187,7 +187,7 @@
 
 (** The Main Function **)
 
-fun lex_order_tac ctxt solve_tac (st: thm) =
+fun lex_order_tac quiet ctxt solve_tac (st: thm) =
     let
       val thy = ProofContext.theory_of ctxt
       val ((trueprop $ (wf $ rel)) :: tl) = prems_of st
@@ -198,28 +198,31 @@
 
       (* 2: create table *)
       val table = map (fn t => map (mk_cell thy solve_tac (dest_term t)) measure_funs) tl
-
-      val order = the (search_table table) (* 3: search table *)
-          handle Option => error (no_order_msg ctxt table tl measure_funs)
-
-      val clean_table = map (fn x => map (nth x) order) table
+    in
+      case search_table table of
+        NONE => if quiet then no_tac st else error (no_order_msg ctxt table tl measure_funs)
+      | SOME order =>
+          let 
+            val clean_table = map (fn x => map (nth x) order) table
+            val relation = mk_measures domT (map (nth measure_funs) order)
+            val _ = if not quiet
+              then writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
+              else ()
 
-      val relation = mk_measures domT (map (nth measure_funs) order)
-      val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
-
-    in (* 4: proof reconstruction *)
-      st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
-              THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
-              THEN (rtac @{thm "wf_empty"} 1)
-              THEN EVERY (map prove_row clean_table))
+          in (* 4: proof reconstruction *)
+            st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
+            THEN (REPEAT (rtac @{thm "wf_mlex"} 1))
+            THEN (rtac @{thm "wf_empty"} 1)
+            THEN EVERY (map prove_row clean_table))
+          end
     end
 
-fun lexicographic_order_tac ctxt =
+fun lexicographic_order_tac quiet ctxt =
   TRY (Function_Common.apply_termination_rule ctxt 1)
-  THEN lex_order_tac ctxt
+  THEN lex_order_tac quiet ctxt
     (auto_tac (clasimpset_of ctxt addsimps2 Function_Common.Termination_Simps.get ctxt))
 
-val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
+val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac false
 
 val setup =
   Method.setup @{binding lexicographic_order}
diff -r b2b78c5ef771 -r 37ec56ac3fd4 src/HOL/Tools/Function/scnp_reconstruct.ML
--- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Fri Oct 30 01:32:06 2009 +0100
@@ -39,7 +39,6 @@
 struct
 
 val PROFILE = Function_Common.PROFILE
-fun TRACE x = if ! Function_Common.profile then tracing x else ()
 
 open ScnpSolve
 
@@ -197,7 +196,7 @@
               else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
           in
             rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
-            THEN (if tag_flag then Arith_Data.verbose_arith_tac ctxt 1 else all_tac)
+            THEN (if tag_flag then Arith_Data.arith_tac ctxt 1 else all_tac)
           end
 
         fun steps_tac MAX strict lq lp =
@@ -347,17 +346,13 @@
   end)
 end
 
-
 fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
   let
     val ms_configured = is_some (Multiset_Setup.get (ProofContext.theory_of ctxt))
     val orders' = if ms_configured then orders
                   else filter_out (curry op = MS) orders
     val gp = gen_probl D cs
-(*    val _ = TRACE ("SCNP instance: " ^ makestring gp)*)
     val certificate = generate_certificate use_tags orders' gp
-(*    val _ = TRACE ("Certificate: " ^ makestring certificate)*)
-
   in
     case certificate
      of NONE => err_cont D i
diff -r b2b78c5ef771 -r 37ec56ac3fd4 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 30 01:32:06 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Oct 30 01:32:06 2009 +0100
@@ -1634,7 +1634,7 @@
 val cached_wf_props : (term * bool) list Unsynchronized.ref =
   Unsynchronized.ref []
 
-val termination_tacs = [Lexicographic_Order.lex_order_tac,
+val termination_tacs = [Lexicographic_Order.lex_order_tac true,
                         ScnpReconstruct.sizechange_tac]
 
 (* extended_context -> const_table -> styp -> bool *)