# HG changeset patch
# User krauss
# Date 1162973334 -3600
# Node ID 8e75fb38522c3ac24aa77faafe6c7afa91f71192
# Parent  d4fbe2c87ef1f83f87c6e05ef0763d3565b11ff2
Made "termination by lexicographic_order" the default for "fun" definitions.

diff -r d4fbe2c87ef1 -r 8e75fb38522c NEWS
--- a/NEWS	Wed Nov 08 02:13:02 2006 +0100
+++ b/NEWS	Wed Nov 08 09:08:54 2006 +0100
@@ -476,6 +476,22 @@
 
 *** HOL ***
 
+* Automated termination proofs "by lexicographic_order" are now
+included in the abbreviated function command "fun". No explicit
+"termination" command is necessary anymore.
+INCOMPATIBILITY: If a "fun"-definition cannot be proved terminating by
+a lexicographic size order, then the command fails. Use the expanded
+version "function" for these cases.
+
+* New method "lexicographic_order" automatically synthesizes
+termination relations as lexicographic combinations of size measures. 
+Usage for (function package) termination proofs:
+
+termination 
+by lexicographic_order
+
+Contributed by Lukas Bulwahn.
+
 * Records: generalised field-update to take a function on the field 
 rather than the new value: r(|A := x|) is translated to A_update (K x) r
 The K-combinator that is internally used is called K_record.
diff -r d4fbe2c87ef1 -r 8e75fb38522c src/HOL/Tools/function_package/fundef_datatype.ML
--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 08 02:13:02 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Nov 08 09:08:54 2006 +0100
@@ -192,7 +192,7 @@
     lthy
       |> FundefPackage.add_fundef fixes statements FundefCommon.fun_config
       ||> by_pat_completeness_simp
-      (*|-> termination_by_lexicographic_order*) |> snd
+      |-> termination_by_lexicographic_order
 
 
 val funP =
diff -r d4fbe2c87ef1 -r 8e75fb38522c src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 02:13:02 2006 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Nov 08 09:08:54 2006 +0100
@@ -73,7 +73,8 @@
         |> LocalTheory.note ((qualify "termination", []), [termination]) |> snd
         |> LocalTheory.note ((qualify "cases", []), [cases]) |> snd
         |> LocalTheory.note ((qualify "pinduct", [Attrib.internal (InductAttrib.induct_set "")]), simple_pinducts) |> snd
-        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec)))
+        |> LocalTheory.declaration (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* save in target *)
+        |> Context.proof_map (add_fundef_data defname (fundef_data, mutual_info, (fixes,spec))) (* also save in local context *)
     end (* FIXME: Add cases for induct and cases thm *)
 
 
diff -r d4fbe2c87ef1 -r 8e75fb38522c src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Wed Nov 08 02:13:02 2006 +0100
+++ b/src/HOL/ex/Fundefs.thy	Wed Nov 08 09:08:54 2006 +0100
@@ -29,8 +29,8 @@
 
 
 text {* Now termination: *}
-termination fib
-  by (auto_term "less_than")
+(*termination fib
+  by (auto_term "less_than")*)
 
 thm fib.simps
 thm fib.induct
@@ -42,8 +42,6 @@
 where
   "add 0 y = y"
 | "add (Suc x) y = Suc (add x y)"
-termination
-  by (auto_term "measure fst")
 
 thm add.simps
 thm add.induct -- {* Note the curried induction predicate *}
@@ -51,10 +49,11 @@
 
 section {* Nested recursion *}
 
-fun nz :: "nat \<Rightarrow> nat"
+function nz :: "nat \<Rightarrow> nat"
 where
   "nz 0 = 0"
 | "nz (Suc x) = nz (nz x)"
+by pat_completeness auto
 
 lemma nz_is_zero: -- {* A lemma we need to prove termination *}
   assumes trm: "nz_dom x"
@@ -72,9 +71,10 @@
 text {* Here comes McCarthy's 91-function *}
 
 
-fun f91 :: "nat => nat"
+function f91 :: "nat => nat"
 where
   "f91 n = (if 100 < n then n - 10 else f91 (f91 (n + 11)))"
+by pat_completeness auto
 
 (* Prove a lemma before attempting a termination proof *)
 lemma f91_estimate: 
@@ -112,10 +112,6 @@
 | "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
                                     else gcd2 (x - y) (Suc y))"
 
-
-termination 
-  by (auto_term "(measure (%x. x)) <*lex*> (measure (%x. x))")
-
 thm gcd2.simps
 thm gcd2.induct
 
@@ -132,9 +128,7 @@
   apply (case_tac x, case_tac a, auto)
   apply (case_tac ba, auto)
   done
-
-termination 
-  by (auto_term "measure (\<lambda>(x,y). x + y)")
+termination by lexicographic_order
 
 thm gcd3.simps
 thm gcd3.induct
@@ -164,7 +158,7 @@
     with c2 show "P" .
   qed
 qed presburger+ -- {* solve compatibility with presburger *}
-termination by (auto_term "{}")
+termination by lexicographic_order
 
 thm ev.simps
 thm ev.induct
@@ -180,18 +174,15 @@
 | "evn (Suc n) = od n"
 | "od (Suc n) = evn n"
 
-thm evn.psimps
-thm od.psimps
+thm evn.simps
+thm od.simps
 
 thm evn_od.pinduct
 thm evn_od.termination
 thm evn_od.domintros
 
-termination
-  by (auto_term "measure (sum_case (%n. n) (%n. n))")
 
-thm evn.simps
-thm od.simps
+
 
 
 end