# HG changeset patch
# User krauss
# Date 1251115148 -7200
# Node ID 4dc441c71cce8fb8d8183cacdfdd297e39e156d6
# Parent  40a0760a00eab73815e51b840fecfec6e8d5be7e
some examples for giving measures manually

diff -r 40a0760a00ea -r 4dc441c71cce src/HOL/ex/Termination.thy
--- a/src/HOL/ex/Termination.thy	Mon Aug 24 10:44:03 2009 +0200
+++ b/src/HOL/ex/Termination.thy	Mon Aug 24 13:59:08 2009 +0200
@@ -1,5 +1,4 @@
 (* Title:       HOL/ex/Termination.thy
-   ID:          $Id$
    Author:      Lukas Bulwahn, TU Muenchen
    Author:      Alexander Krauss, TU Muenchen
 *)
@@ -10,12 +9,33 @@
 imports Main Multiset
 begin
 
+subsection {* Manually giving termination relations using @{text relation} and
+@{term measure} *}
+
+function sum :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "sum i N = (if i > N then 0 else i + sum (Suc i) N)"
+by pat_completeness auto
+
+termination by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
+
+function foo :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "foo i N = (if i > N 
+              then (if N = 0 then 0 else foo 0 (N - 1))
+              else i + foo (Suc i) N)"
+by pat_completeness auto
+
+termination by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
+
+
+subsection {* @{text lexicographic_order}: Trivial examples *}
+
 text {*
-  The @{text fun} command uses the method @{text lexicographic_order} by default.
+  The @{text fun} command uses the method @{text lexicographic_order} by default,
+  so it is not explicitly invoked.
 *}
 
-subsection {* Trivial examples *}
-
 fun identity :: "nat \<Rightarrow> nat"
 where
   "identity n = n"