# HG changeset patch
# User haftmann
# Date 1162283348 -3600
# Node ID e8657a20a52f926b48d1f9081555e73b98ca4113
# Parent  be58cded79da615db379cc74130a4fe4a47db983
*** empty log message ***

diff -r be58cded79da -r e8657a20a52f src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Tue Oct 31 09:29:06 2006 +0100
+++ b/src/HOL/ex/CodeEval.thy	Tue Oct 31 09:29:08 2006 +0100
@@ -180,8 +180,8 @@
 
 subsection {* Small examples *}
 
+ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *}
 ML {* Eval.term "[]::nat list" *}
-ML {* Eval.term "(Suc 2 + Suc 0) * Suc 3" *}
 ML {* Eval.term "fst ([]::nat list, Suc 0) = []" *}
 
 text {* a fancy datatype *}
diff -r be58cded79da -r e8657a20a52f src/HOL/ex/NormalForm.thy
--- 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