1.1 --- a/src/HOL/ex/NormalForm.thy Wed Sep 15 13:44:10 2010 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,131 +0,0 @@
1.4 -(* Authors: Klaus Aehlig, Tobias Nipkow *)
1.5 -
1.6 -header {* Testing implementation of normalization by evaluation *}
1.7 -
1.8 -theory NormalForm
1.9 -imports Complex_Main
1.10 -begin
1.11 -
1.12 -lemma "True" by normalization
1.13 -lemma "p \<longrightarrow> True" by normalization
1.14 -declare disj_assoc [code nbe]
1.15 -lemma "((P | Q) | R) = (P | (Q | R))" by normalization
1.16 -lemma "0 + (n::nat) = n" by normalization
1.17 -lemma "0 + Suc n = Suc n" by normalization
1.18 -lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
1.19 -lemma "~((0::nat) < (0::nat))" by normalization
1.20 -
1.21 -datatype n = Z | S n
1.22 -
1.23 -primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
1.24 - "add Z = id"
1.25 - | "add (S m) = S o add m"
1.26 -
1.27 -primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
1.28 - "add2 Z n = n"
1.29 - | "add2 (S m) n = S(add2 m n)"
1.30 -
1.31 -declare add2.simps [code]
1.32 -lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
1.33 - by (induct n) auto
1.34 -lemma [code]: "add2 n (S m) = S (add2 n m)"
1.35 - by(induct n) auto
1.36 -lemma [code]: "add2 n Z = n"
1.37 - by(induct n) auto
1.38 -
1.39 -lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
1.40 -lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
1.41 -lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
1.42 -
1.43 -primrec mul :: "n \<Rightarrow> n \<Rightarrow> n" where
1.44 - "mul Z = (%n. Z)"
1.45 - | "mul (S m) = (%n. add (mul m n) n)"
1.46 -
1.47 -primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
1.48 - "mul2 Z n = Z"
1.49 - | "mul2 (S m) n = add2 n (mul2 m n)"
1.50 -
1.51 -primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
1.52 - "exp m Z = S Z"
1.53 - | "exp m (S n) = mul (exp m n) m"
1.54 -
1.55 -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
1.56 -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
1.57 -lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
1.58 -
1.59 -lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
1.60 -lemma "split (%x y. x) (a, b) = a" by normalization
1.61 -lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
1.62 -
1.63 -lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
1.64 -
1.65 -lemma "[] @ [] = []" by normalization
1.66 -lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
1.67 -lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
1.68 -lemma "[] @ xs = xs" by normalization
1.69 -lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
1.70 -
1.71 -lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
1.72 - by normalization rule+
1.73 -lemma "rev [a, b, c] = [c, b, a]" by normalization
1.74 -normal_form "rev (a#b#cs) = rev cs @ [b, a]"
1.75 -normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
1.76 -normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
1.77 -normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
1.78 -lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
1.79 - by normalization
1.80 -normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
1.81 -normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
1.82 -lemma "let x = y in [x, x] = [y, y]" by normalization
1.83 -lemma "Let y (%x. [x,x]) = [y, y]" by normalization
1.84 -normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
1.85 -lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
1.86 -normal_form "filter (%x. x) ([True,False,x]@xs)"
1.87 -normal_form "filter Not ([True,False,x]@xs)"
1.88 -
1.89 -lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
1.90 -lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
1.91 -lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
1.92 -
1.93 -lemma "last [a, b, c] = c" by normalization
1.94 -lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization
1.95 -
1.96 -lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
1.97 -lemma "(-4::int) * 2 = -8" by normalization
1.98 -lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
1.99 -lemma "(2::int) + 3 = 5" by normalization
1.100 -lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
1.101 -lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
1.102 -lemma "(2::int) < 3" by normalization
1.103 -lemma "(2::int) <= 3" by normalization
1.104 -lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
1.105 -lemma "4 - 42 * abs (3 + (-7\<Colon>int)) = -164" by normalization
1.106 -lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
1.107 -lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
1.108 -lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
1.109 -lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
1.110 -lemma "max (Suc 0) 0 = Suc 0" by normalization
1.111 -lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
1.112 -normal_form "Suc 0 \<in> set ms"
1.113 -
1.114 -lemma "f = f" by normalization
1.115 -lemma "f x = f x" by normalization
1.116 -lemma "(f o g) x = f (g x)" by normalization
1.117 -lemma "(f o id) x = f x" by normalization
1.118 -normal_form "(\<lambda>x. x)"
1.119 -
1.120 -(* Church numerals: *)
1.121 -
1.122 -normal_form "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
1.123 -normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
1.124 -normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
1.125 -
1.126 -(* handling of type classes in connection with equality *)
1.127 -
1.128 -lemma "map f [x, y] = [f x, f y]" by normalization
1.129 -lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
1.130 -lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
1.131 -lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
1.132 -lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
1.133 -
1.134 -end
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/ex/Normalization_by_Evaluation.thy Wed Sep 15 13:44:10 2010 +0200
2.3 @@ -0,0 +1,131 @@
2.4 +(* Authors: Klaus Aehlig, Tobias Nipkow *)
2.5 +
2.6 +header {* Testing implementation of normalization by evaluation *}
2.7 +
2.8 +theory Normalization_by_Evaluation
2.9 +imports Complex_Main
2.10 +begin
2.11 +
2.12 +lemma "True" by normalization
2.13 +lemma "p \<longrightarrow> True" by normalization
2.14 +declare disj_assoc [code nbe]
2.15 +lemma "((P | Q) | R) = (P | (Q | R))" by normalization
2.16 +lemma "0 + (n::nat) = n" by normalization
2.17 +lemma "0 + Suc n = Suc n" by normalization
2.18 +lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
2.19 +lemma "~((0::nat) < (0::nat))" by normalization
2.20 +
2.21 +datatype n = Z | S n
2.22 +
2.23 +primrec add :: "n \<Rightarrow> n \<Rightarrow> n" where
2.24 + "add Z = id"
2.25 + | "add (S m) = S o add m"
2.26 +
2.27 +primrec add2 :: "n \<Rightarrow> n \<Rightarrow> n" where
2.28 + "add2 Z n = n"
2.29 + | "add2 (S m) n = S(add2 m n)"
2.30 +
2.31 +declare add2.simps [code]
2.32 +lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)"
2.33 + by (induct n) auto
2.34 +lemma [code]: "add2 n (S m) = S (add2 n m)"
2.35 + by(induct n) auto
2.36 +lemma [code]: "add2 n Z = n"
2.37 + by(induct n) auto
2.38 +
2.39 +lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
2.40 +lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
2.41 +lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
2.42 +
2.43 +primrec mul :: "n \<Rightarrow> n \<Rightarrow> n" where
2.44 + "mul Z = (%n. Z)"
2.45 + | "mul (S m) = (%n. add (mul m n) n)"
2.46 +
2.47 +primrec mul2 :: "n \<Rightarrow> n \<Rightarrow> n" where
2.48 + "mul2 Z n = Z"
2.49 + | "mul2 (S m) n = add2 n (mul2 m n)"
2.50 +
2.51 +primrec exp :: "n \<Rightarrow> n \<Rightarrow> n" where
2.52 + "exp m Z = S Z"
2.53 + | "exp m (S n) = mul (exp m n) m"
2.54 +
2.55 +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
2.56 +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
2.57 +lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
2.58 +
2.59 +lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
2.60 +lemma "split (%x y. x) (a, b) = a" by normalization
2.61 +lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
2.62 +
2.63 +lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
2.64 +
2.65 +lemma "[] @ [] = []" by normalization
2.66 +lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
2.67 +lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
2.68 +lemma "[] @ xs = xs" by normalization
2.69 +lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
2.70 +
2.71 +lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
2.72 + by normalization rule+
2.73 +lemma "rev [a, b, c] = [c, b, a]" by normalization
2.74 +value [nbe] "rev (a#b#cs) = rev cs @ [b, a]"
2.75 +value [nbe] "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
2.76 +value [nbe] "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
2.77 +value [nbe] "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
2.78 +lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
2.79 + by normalization
2.80 +value [nbe] "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
2.81 +value [nbe] "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs = P"
2.82 +lemma "let x = y in [x, x] = [y, y]" by normalization
2.83 +lemma "Let y (%x. [x,x]) = [y, y]" by normalization
2.84 +value [nbe] "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
2.85 +lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization
2.86 +value [nbe] "filter (%x. x) ([True,False,x]@xs)"
2.87 +value [nbe] "filter Not ([True,False,x]@xs)"
2.88 +
2.89 +lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization
2.90 +lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
2.91 +lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization
2.92 +
2.93 +lemma "last [a, b, c] = c" by normalization
2.94 +lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization
2.95 +
2.96 +lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
2.97 +lemma "(-4::int) * 2 = -8" by normalization
2.98 +lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
2.99 +lemma "(2::int) + 3 = 5" by normalization
2.100 +lemma "(2::int) + 3 * (- 4) * (- 1) = 14" by normalization
2.101 +lemma "(2::int) + 3 * (- 4) * 1 + 0 = -10" by normalization
2.102 +lemma "(2::int) < 3" by normalization
2.103 +lemma "(2::int) <= 3" by normalization
2.104 +lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
2.105 +lemma "4 - 42 * abs (3 + (-7\<Colon>int)) = -164" by normalization
2.106 +lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
2.107 +lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
2.108 +lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
2.109 +lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
2.110 +lemma "max (Suc 0) 0 = Suc 0" by normalization
2.111 +lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization
2.112 +value [nbe] "Suc 0 \<in> set ms"
2.113 +
2.114 +lemma "f = f" by normalization
2.115 +lemma "f x = f x" by normalization
2.116 +lemma "(f o g) x = f (g x)" by normalization
2.117 +lemma "(f o id) x = f x" by normalization
2.118 +value [nbe] "(\<lambda>x. x)"
2.119 +
2.120 +(* Church numerals: *)
2.121 +
2.122 +value [nbe] "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
2.123 +value [nbe] "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
2.124 +value [nbe] "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
2.125 +
2.126 +(* handling of type classes in connection with equality *)
2.127 +
2.128 +lemma "map f [x, y] = [f x, f y]" by normalization
2.129 +lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
2.130 +lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
2.131 +lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
2.132 +lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
2.133 +
2.134 +end
3.1 --- a/src/HOL/ex/ROOT.ML Wed Sep 15 13:44:10 2010 +0200
3.2 +++ b/src/HOL/ex/ROOT.ML Wed Sep 15 13:44:10 2010 +0200
3.3 @@ -8,7 +8,7 @@
3.4 "Efficient_Nat_examples",
3.5 "FuncSet",
3.6 "Eval_Examples",
3.7 - "NormalForm"
3.8 + "Normalization_by_Evaluation"
3.9 ];
3.10
3.11 use_thys [