19829

1 
(* ID: $Id$


2 
Authors: Klaus Aehlig, Tobias Nipkow

20807

3 
*)

19829

4 

21059

5 
header {* Test of normalization function *}

19829

6 


7 
theory NormalForm

25165

8 
imports Main "~~/src/HOL/Real/Rational"

19829

9 
begin


10 

28350

11 
lemma [code nbe]:


12 
"x = x \<longleftrightarrow> True" by rule+


13 


14 
lemma [code nbe]:


15 
"eq_class.eq (x::bool) x \<longleftrightarrow> True" unfolding eq by rule+


16 


17 
lemma [code nbe]:


18 
"eq_class.eq (x::nat) x \<longleftrightarrow> True" unfolding eq by rule+


19 

21117

20 
lemma "True" by normalization

19971

21 
lemma "p \<longrightarrow> True" by normalization

28350

22 
declare disj_assoc [code nbe]


23 
lemma "((P  Q)  R) = (P  (Q  R))" by normalization

22845

24 
declare disj_assoc [code func del]

28350

25 
lemma "0 + (n::nat) = n" by normalization


26 
lemma "0 + Suc n = Suc n" by normalization


27 
lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization

19971

28 
lemma "~((0::nat) < (0::nat))" by normalization


29 

19829

30 
datatype n = Z  S n

28350

31 


32 
lemma [code nbe]:


33 
"eq_class.eq (x::n) x \<longleftrightarrow> True" unfolding eq by rule+


34 

19829

35 
consts

20842

36 
add :: "n \<Rightarrow> n \<Rightarrow> n"


37 
add2 :: "n \<Rightarrow> n \<Rightarrow> n"


38 
mul :: "n \<Rightarrow> n \<Rightarrow> n"


39 
mul2 :: "n \<Rightarrow> n \<Rightarrow> n"


40 
exp :: "n \<Rightarrow> n \<Rightarrow> n"

19829

41 
primrec

20842

42 
"add Z = id"


43 
"add (S m) = S o add m"

19829

44 
primrec

20842

45 
"add2 Z n = n"


46 
"add2 (S m) n = S(add2 m n)"

19829

47 

28143

48 
declare add2.simps [code]

19829

49 
lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)"

28143

50 
by (induct n) auto

20842

51 
lemma [code]: "add2 n (S m) = S (add2 n m)"


52 
by(induct n) auto

19829

53 
lemma [code]: "add2 n Z = n"

20842

54 
by(induct n) auto

19971

55 

28350

56 
lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization


57 
lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization


58 
lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization

19829

59 


60 
primrec

20842

61 
"mul Z = (%n. Z)"


62 
"mul (S m) = (%n. add (mul m n) n)"

19829

63 
primrec

20842

64 
"mul2 Z n = Z"


65 
"mul2 (S m) n = add2 n (mul2 m n)"

19829

66 
primrec

20842

67 
"exp m Z = S Z"


68 
"exp m (S n) = mul (exp m n) m"

19829

69 

19971

70 
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


71 
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


72 
lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization


73 


74 
lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization

28350

75 
lemma "split (%x y. x) (a, b) = a" by normalization

19971

76 
lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization


77 


78 
lemma "case Z of Z \<Rightarrow> True  S x \<Rightarrow> False" by normalization

19829

79 

20842

80 
lemma "[] @ [] = []" by normalization

28350

81 
lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization


82 
lemma "[a, b, c] @ xs = a # b # c # xs" by normalization


83 
lemma "[] @ xs = xs" by normalization


84 
lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization


85 


86 
lemma [code nbe]:


87 
"eq_class.eq (x :: 'a\<Colon>eq list) x \<longleftrightarrow> True" unfolding eq by rule+


88 

25934

89 
lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization rule+

28350

90 
lemma "rev [a, b, c] = [c, b, a]" by normalization

26739

91 
normal_form "rev (a#b#cs) = rev cs @ [b, a]"

19829

92 
normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"


93 
normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"


94 
normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"

25934

95 
lemma "map (%x. case x of None \<Rightarrow> False  Some y \<Rightarrow> True) [None, Some ()] = [False, True]"


96 
by normalization

19829

97 
normal_form "case xs of [] \<Rightarrow> True  x#xs \<Rightarrow> False"

25934

98 
normal_form "map (%x. case x of None \<Rightarrow> False  Some y \<Rightarrow> True) xs = P"

28350

99 
lemma "let x = y in [x, x] = [y, y]" by normalization


100 
lemma "Let y (%x. [x,x]) = [y, y]" by normalization

19829

101 
normal_form "case n of Z \<Rightarrow> True  S x \<Rightarrow> False"

28350

102 
lemma "(%(x,y). add x y) (S z,S z) = S (add z (S z))" by normalization

19829

103 
normal_form "filter (%x. x) ([True,False,x]@xs)"


104 
normal_form "filter Not ([True,False,x]@xs)"


105 

28350

106 
lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b, c]" by normalization


107 
lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization

25100

108 
lemma "map (%x. case x of None \<Rightarrow> False  Some y \<Rightarrow> True) [None, Some ()] = [False, True]" by normalization

19829

109 

28350

110 
lemma "last [a, b, c] = c" by normalization


111 
lemma "last ([a, b, c] @ xs) = last (c # xs)" by normalization

19829

112 

28350

113 
lemma [code nbe]:


114 
"eq_class.eq (x :: int) x \<longleftrightarrow> True" unfolding eq by rule+


115 


116 
lemma "(2::int) + 3  1 + ( k) * 2 = 4 +  k * 2" by normalization

20842

117 
lemma "(4::int) * 2 = 8" by normalization


118 
lemma "abs ((4::int) + 2 * 1) = 2" by normalization


119 
lemma "(2::int) + 3 = 5" by normalization


120 
lemma "(2::int) + 3 * ( 4) * ( 1) = 14" by normalization


121 
lemma "(2::int) + 3 * ( 4) * 1 + 0 = 10" by normalization


122 
lemma "(2::int) < 3" by normalization


123 
lemma "(2::int) <= 3" by normalization


124 
lemma "abs ((4::int) + 2 * 1) = 2" by normalization


125 
lemma "4  42 * abs (3 + (7\<Colon>int)) = 164" by normalization


126 
lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization

22394

127 
lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization


128 
lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization

25100

129 
lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization


130 
lemma "max (Suc 0) 0 = Suc 0" by normalization

25187

131 
lemma "(42::rat) / 1704 = 1 / 284 + 3 / 142" by normalization

21059

132 
normal_form "Suc 0 \<in> set ms"

20922

133 

28350

134 
lemma "f = f" by normalization


135 
lemma "f x = f x" by normalization


136 
lemma "(f o g) x = f (g x)" by normalization


137 
lemma "(f o id) x = f x" by normalization

25934

138 
normal_form "(\<lambda>x. x)"

21987

139 

23396

140 
(* Church numerals: *)


141 


142 
normal_form "(%m n f x. m f (n f x)) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"


143 
normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"


144 
normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"


145 

19829

146 
end
