diff -r 05072ae0d435 -r 36a59e5d0039 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Wed Sep 13 00:38:38 2006 +0200
+++ b/src/HOL/ex/Fundefs.thy	Wed Sep 13 12:05:50 2006 +0200
@@ -6,26 +6,31 @@
 *)
 
 theory Fundefs 
-imports Main
+imports Main "../FundefDebug"
 begin
 
+
 section {* Very basic *}
 
-consts fib :: "nat \<Rightarrow> nat"
-function
+ML "trace_simp := false"
+
+fun fib :: "nat \<Rightarrow> nat"
+where
   "fib 0 = 1"
-  "fib (Suc 0) = 1"
-  "fib (Suc (Suc n)) = fib n + fib (Suc n)"
-by pat_completeness  -- {* shows that the patterns are complete *}
-  auto  -- {* shows that the patterns are compatible *}
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc n)) = fib n + fib (Suc n)"
+
 
 text {* we get partial simp and induction rules: *}
 thm fib.psimps
-thm pinduct
+thm fib.pinduct
 
 text {* There is also a cases rule to distinguish cases along the definition *}
 thm fib.cases
 
+thm fib.domintros
+
+
 text {* Now termination: *}
 termination fib
   by (auto_term "less_than")
@@ -36,34 +41,30 @@
 
 section {* Currying *}
 
-consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-function
+fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
   "add 0 y = y"
-  "add (Suc x) y = Suc (add x y)"
-thm add_rel.cases
-
-by pat_completeness auto
+| "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 *}
 
 
 section {* Nested recursion *}
 
-consts nz :: "nat \<Rightarrow> nat"
-function
+fun nz :: "nat \<Rightarrow> nat"
+where
   "nz 0 = 0"
-  "nz (Suc x) = nz (nz x)"
-by pat_completeness auto
+| "nz (Suc x) = nz (nz x)"
+
 
 lemma nz_is_zero: -- {* A lemma we need to prove termination *}
   assumes trm: "x \<in> nz_dom"
   shows "nz x = 0"
 using trm
-apply induct 
-apply auto
-done
+by induct auto
 
 termination nz
   apply (auto_term "less_than") -- {* Oops, it left us something to prove *}
@@ -74,10 +75,10 @@
 
 text {* Here comes McCarthy's 91-function *}
 
-consts f91 :: "nat => nat"
-function 
+fun 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: 
@@ -85,7 +86,6 @@
   shows "n < f91 n + 11"
 using trm by induct auto
 
-(* Now go for termination *)
 termination
 proof
   let ?R = "measure (%x. 101 - x)"
@@ -109,15 +109,16 @@
 no automatic splitting takes place. But the following definition of
 gcd is ok, although patterns overlap: *}
 
-consts gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-function
+fun gcd2 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
   "gcd2 x 0 = x"
-  "gcd2 0 y = y"
-  "gcd2 (Suc x) (Suc y) = (if x < y then gcd2 (Suc x) (y - x)
-                                else gcd2 (x - y) (Suc y))"
-by pat_completeness auto
+| "gcd2 0 y = y"
+| "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 (\<lambda>(x,y). x + y)")
+  by (auto_term "(measure (%x. x)) <*lex*> (measure (%x. x))")
 
 thm gcd2.simps
 thm gcd2.induct
@@ -127,8 +128,8 @@
 
 text {* We can reformulate the above example using guarded patterns *}
 
-consts gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-function
+function gcd3 :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
   "gcd3 x 0 = x"
   "gcd3 0 y = y"
   "x < y \<Longrightarrow> gcd3 (Suc x) (Suc y) = gcd3 (Suc x) (y - x)"
@@ -136,6 +137,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)")
 
@@ -143,10 +145,10 @@
 thm gcd3.induct
 
 
+text {* General patterns allow even strange definitions: *}
 
-text {* General patterns allow even strange definitions: *}
-consts ev :: "nat \<Rightarrow> bool"
-function
+function ev :: "nat \<Rightarrow> bool"
+where
   "ev (2 * n) = True"
   "ev (2 * n + 1) = False"
 proof -  -- {* completeness is more difficult here \dots *}
@@ -166,7 +168,7 @@
     with divmod have "x = 2 * (x div 2) + 1" by simp
     with c2 show "P" .
   qed
-qed presburger+   -- {* solve compatibility with presburger *}
+qed presburger+ -- {* solve compatibility with presburger *}
 termination by (auto_term "{}")
 
 thm ev.simps
@@ -176,18 +178,12 @@
 
 section {* Mutual Recursion *}
 
-
-consts
-  evn :: "nat \<Rightarrow> bool"
-  od :: "nat \<Rightarrow> bool"
-
-function
+fun evn od :: "nat \<Rightarrow> bool"
+where
   "evn 0 = True"
-  "evn (Suc n) = od n"
-and
-  "od 0 = False"
-  "od (Suc n) = evn n"
-  by pat_completeness auto
+| "od 0 = False"
+| "evn (Suc n) = od n"
+| "od (Suc n) = evn n"
 
 thm evn.psimps
 thm od.psimps