--- a/src/HOL/ex/NormalForm.thy Fri Apr 17 14:29:54 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy Fri Apr 17 14:29:55 2009 +0200
@@ -1,7 +1,6 @@
-(* Authors: Klaus Aehlig, Tobias Nipkow
-*)
+(* Authors: Klaus Aehlig, Tobias Nipkow *)
-header {* Test of normalization function *}
+header {* Testing implementation of normalization by evaluation *}
theory NormalForm
imports Main Rational
@@ -19,18 +18,13 @@
datatype n = Z | S n
-consts
- add :: "n \<Rightarrow> n \<Rightarrow> n"
- add2 :: "n \<Rightarrow> n \<Rightarrow> n"
- mul :: "n \<Rightarrow> n \<Rightarrow> n"
- mul2 :: "n \<Rightarrow> n \<Rightarrow> n"
- exp :: "n \<Rightarrow> n \<Rightarrow> n"
-primrec
- "add Z = id"
- "add (S m) = S o add m"
-primrec
- "add2 Z n = n"
- "add2 (S m) n = S(add2 m n)"
+primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "add Z = id"
+ | "add (S m) = S o add m"
+
+primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "add2 Z n = n"
+ | "add2 (S m) n = S(add2 m n)"
declare add2.simps [code]
lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
@@ -44,15 +38,17 @@
lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
-primrec
- "mul Z = (%n. Z)"
- "mul (S m) = (%n. add (mul m n) n)"
-primrec
- "mul2 Z n = Z"
- "mul2 (S m) n = add2 n (mul2 m n)"
-primrec
- "exp m Z = S Z"
- "exp m (S n) = mul (exp m n) m"
+primrec mul :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "mul Z = (%n. Z)"
+ | "mul (S m) = (%n. add (mul m n) n)"
+
+primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "mul2 Z n = Z"
+ | "mul2 (S m) n = add2 n (mul2 m n)"
+
+primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
+ "exp m Z = S Z"
+ | "exp m (S n) = mul (exp m n) m"
lemma "mul2 (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization
lemma "mul (S(S(S(S(S Z))))) (S(S(S Z))) = S(S(S(S(S(S(S(S(S(S(S(S(S(S(S Z))))))))))))))" by normalization