--- a/src/HOL/ex/NormalForm.thy Tue Oct 31 09:29:06 2006 +0100
+++ b/src/HOL/ex/NormalForm.thy Tue Oct 31 09:29:08 2006 +0100
@@ -8,6 +8,8 @@
imports Main
begin
+lemma "True" by normalization
+lemma "x = x" by normalization
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code func]
lemma "((P | Q) | R) = (P | (Q | R))" by normalization
@@ -64,15 +66,17 @@
lemma "[] @ [] = []" by normalization
lemma "[] @ xs = xs" by normalization
-lemma "[a \<Colon> 'd, b, c] @ xs = a # b # c # xs" by normalization
+lemma "[a, b, c] @ xs = a # b # c # xs" by normalization
lemma "[%a::'x. a, %b. b, c] @ xs = (%x. x) # (%x. x) # c # xs" by normalization
-lemma "[%a::'x. a, %b. b, c] @ [u,v] = [%x. x, %x. x, c, u, v]" by normalization
+lemma "[%a::'x. a, %b. b, c] @ [u, v] = [%x. x, %x. x, c, u, v]" by normalization
lemma "map f [x,y,z::'x] = [f x, f y, f z]" by normalization
-normal_form "map (%f. f True) [id,g,Not]"
-normal_form "map (%f. f True) ([id,g,Not] @ fs)"
-lemma "rev[a,b,c] = [c, b, a]" by normalization
-normal_form "rev(a#b#cs)"
-lemma "map map [f,g,h] = [map f, map g, map h]" by normalization
+lemma "map (%f. f True) [id, g, Not] = [True, g True, False]" by normalization
+lemma "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs" by normalization
+lemma "rev [a, b, c] = [c, b, a]" by normalization
+(*normal_form "rev (a#b#cs)"
+normal_form "rev cs @ [b, a]"*)
+(*lemma "rev (a#b#cs) = rev cs @ [b, a]" by normalization*)
+lemma "map map [f, g, h] = [map f, map g, map h]" by normalization
normal_form "map (%F. F [a,b,c::'x]) (map map [f,g,h])"
normal_form "map (%F. F ([a,b,c] @ ds)) (map map ([f,g,h]@fs))"
normal_form "map (%F. F [Z,S Z,S(S Z)]) (map map [S,add (S Z),mul (S(S Z)),id])"
@@ -87,10 +91,11 @@
normal_form "filter Not ([True,False,x]@xs)"
lemma "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]" by normalization
-normal_form "%(xs, ys). xs @ ys"
-normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])"
+lemma "(%(xs, ys). xs @ ys) = split op @" by normalization
+lemma "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]" by normalization
normal_form "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
-normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
+lemma "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
+ by normalization
lemma "last [a, b, c] = c"
by normalization