# HG changeset patch
# User haftmann
# Date 1192803480 -7200
# Node ID fe9632d914c75267b1f9ee512e6babd5c84ae132
# Parent  b2c19b9964db1ab399a7731e1226b0195db041c4
added examples

diff -r b2c19b9964db -r fe9632d914c7 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Fri Oct 19 16:17:59 2007 +0200
+++ b/src/HOL/ex/NormalForm.thy	Fri Oct 19 16:18:00 2007 +0200
@@ -65,8 +65,9 @@
 lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
 
 lemma "[] @ [] = []" by normalization
+normal_form "map f [x,y,z::'x] = [f x, f y, f z]"
+normal_form "[a, b, c] @ xs = a # b # c # xs"
 lemma "[] @ xs = xs" by normalization
-normal_form "[a, b, c] @ xs = a # b # c # xs"
 normal_form "map f [x,y,z::'x] = [f x, f y, f z]"
 normal_form "map (%f. f True) [id, g, Not] = [True, g True, False]"
 normal_form "map (%f. f True) ([id, g, Not] @ fs) = [True, g True, False] @ map (%f. f True) fs"
@@ -87,7 +88,7 @@
 
 normal_form "[x,y,z] @ [a,b,c] = [x, y, z, a, b ,c]"
 normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]"
-normal_form "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()] = [False, True]"
+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
@@ -107,6 +108,8 @@
 lemma "(if (0\<Colon>nat) \<le> (x\<Colon>nat) then 0\<Colon>nat else x) = 0" by normalization
 lemma "4 = Suc (Suc (Suc (Suc 0)))" by normalization
 lemma "nat 4 = Suc (Suc (Suc (Suc 0)))" by normalization
+lemma "[Suc 0, 0] = [Suc 0, 0]" by normalization
+lemma "max (Suc 0) 0 = Suc 0" by normalization
 
 normal_form "Suc 0 \<in> set ms"
 
@@ -123,3 +126,4 @@
 normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
 
 end
+