author krauss Fri, 30 Oct 2009 01:32:06 +0100 changeset 33351 37ec56ac3fd4 parent 33350 b2b78c5ef771 child 33352 021677ed8eaa child 33356 9157d0f9f00e child 33375 fd3e861f8d31
less verbose termination tactics
```--- 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}```
```--- 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```
```--- 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 *)```