19829
|
1 |
(* ID: $Id$
|
|
2 |
Authors: Klaus Aehlig, Tobias Nipkow
|
|
3 |
|
|
4 |
Test of normalization function
|
|
5 |
*)
|
|
6 |
|
|
7 |
theory NormalForm
|
|
8 |
imports Main
|
|
9 |
begin
|
|
10 |
|
|
11 |
normal_form "True \<longrightarrow> p"
|
|
12 |
|
|
13 |
(* FIXME Eventually the code generator should be able to handle this
|
|
14 |
by re-generating the existing code for "or":
|
|
15 |
|
|
16 |
declare disj_assoc[code]
|
|
17 |
|
|
18 |
normal_form "(P | Q) | R"
|
|
19 |
|
|
20 |
*)
|
|
21 |
|
|
22 |
|
|
23 |
datatype n = Z | S n
|
|
24 |
consts
|
|
25 |
add :: "n \<Rightarrow> n \<Rightarrow> n"
|
|
26 |
add2 :: "n \<Rightarrow> n \<Rightarrow> n"
|
|
27 |
mul :: "n \<Rightarrow> n \<Rightarrow> n"
|
|
28 |
mul2 :: "n \<Rightarrow> n \<Rightarrow> n"
|
|
29 |
exp :: "n \<Rightarrow> n \<Rightarrow> n"
|
|
30 |
primrec
|
|
31 |
"add Z = id"
|
|
32 |
"add (S m) = S o add m"
|
|
33 |
primrec
|
|
34 |
"add2 Z n = n"
|
|
35 |
"add2 (S m) n = S(add2 m n)"
|
|
36 |
|
|
37 |
lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"
|
|
38 |
by(induct n, auto)
|
|
39 |
lemma [code]: "add2 n (S m) = S(add2 n m)"
|
|
40 |
by(induct n, auto)
|
|
41 |
lemma [code]: "add2 n Z = n"
|
|
42 |
by(induct n, auto)
|
|
43 |
|
|
44 |
normal_form "add2 (add2 n m) k"
|
|
45 |
normal_form "add2 (add2 (S n) (S m)) (S k)"
|
|
46 |
normal_form "add2 (add2 (S n)(add2 (S m) Z)) (S k)"
|
|
47 |
|
|
48 |
primrec
|
|
49 |
"mul Z = (%n. Z)"
|
|
50 |
"mul (S m) = (%n. add (mul m n) n)"
|
|
51 |
primrec
|
|
52 |
"mul2 Z n = Z"
|
|
53 |
"mul2 (S m) n = add2 n (mul2 m n)"
|
|
54 |
primrec
|
|
55 |
"exp m Z = S Z"
|
|
56 |
"exp m (S n) = mul (exp m n) m"
|
|
57 |
|
|
58 |
normal_form "mul2 (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
|
|
59 |
normal_form "mul (S(S(S(S(S(S(S Z))))))) (S(S(S(S(S Z)))))"
|
|
60 |
normal_form "exp (S(S Z)) (S(S(S(S(S Z)))))"
|
|
61 |
|
|
62 |
normal_form "[] @ []"
|
|
63 |
normal_form "[] @ xs"
|
|
64 |
normal_form "[] @ (xs:: 'b list)"
|
|
65 |
normal_form "[a::'d,b,c] @ xs"
|
|
66 |
normal_form "[%a::'x. a, %b. b, c] @ xs"
|
|
67 |
normal_form "[%a::'x. a, %b. b, c] @ [u,v]"
|
|
68 |
normal_form "map f (xs::'c list)"
|
|
69 |
normal_form "map f [x,y,z::'x]"
|
|
70 |
normal_form "map (%f. f True) [id,g,Not]"
|
|
71 |
normal_form "map (%f. f True) ([id,g,Not] @ fs)"
|
|
72 |
normal_form "rev[a,b,c]"
|
|
73 |
normal_form "rev(a#b#cs)"
|
|
74 |
normal_form "map map [f,g,h]"
|
|
75 |
normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
|
|
76 |
normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
|
|
77 |
normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
|
|
78 |
normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
|
|
79 |
normal_form "case xs of [] \<Rightarrow> True | x#xs \<Rightarrow> False"
|
|
80 |
normal_form "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False"
|
|
81 |
normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) xs"
|
|
82 |
normal_form "let x = y::'x in [x,x]"
|
|
83 |
normal_form "Let y (%x. [x,x])"
|
|
84 |
normal_form "case n of Z \<Rightarrow> True | S x \<Rightarrow> False"
|
|
85 |
normal_form "(%(x,y). add x y) (S z,S z)"
|
|
86 |
normal_form "filter (%x. x) ([True,False,x]@xs)"
|
|
87 |
normal_form "filter Not ([True,False,x]@xs)"
|
|
88 |
|
|
89 |
normal_form "0 + (n::nat)"
|
|
90 |
normal_form "0 + Suc(n)"
|
|
91 |
normal_form "0::nat"
|
|
92 |
normal_form "Suc(n) + Suc m"
|
|
93 |
normal_form "[] @ xs"
|
|
94 |
normal_form "(x#xs) @ ys"
|
|
95 |
normal_form "[x,y,z] @ [a,b,c]"
|
|
96 |
normal_form "%(xs, ys). xs @ ys"
|
|
97 |
normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])"
|
|
98 |
normal_form "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
|
|
99 |
normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
|
|
100 |
|
|
101 |
normal_form "case n of None \<Rightarrow> True | Some((x,y),(u,v)) \<Rightarrow> False"
|
|
102 |
normal_form "let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)"
|
|
103 |
normal_form "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z))"
|
|
104 |
normal_form "last[a,b,c]"
|
|
105 |
normal_form "last([a,b,c]@xs)"
|
|
106 |
normal_form " (0::nat) < (0::nat)"
|
|
107 |
|
|
108 |
(* FIXME
|
|
109 |
won't work since it relies on
|
|
110 |
polymorphically used ad-hoc overloaded function:
|
|
111 |
normal_form "max 0 (0::nat)"
|
|
112 |
*)
|
|
113 |
|
|
114 |
text {*
|
|
115 |
Numerals still take their time\<dots>
|
|
116 |
*}
|
|
117 |
|
|
118 |
end
|