--- 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