# HG changeset patch
# User haftmann
# Date 1199788657 -3600
# Node ID 263aaf988d444c28711be681ad4c0fcba5811552
# Parent  a141d6bfd3980dd6b07c171613f85294ea29f4c7
normalization conversion

diff -r a141d6bfd398 -r 263aaf988d44 src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Tue Jan 08 11:37:32 2008 +0100
+++ b/src/HOL/Code_Setup.thy	Tue Jan 08 11:37:37 2008 +0100
@@ -145,8 +145,9 @@
 
 method_setup normalization = {*
   Method.no_args (Method.SIMPLE_METHOD'
-    (CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv)
-      THEN' resolve_tac [TrueI, refl]))
+    (fn k => CONVERSION (ObjectLogic.judgment_conv Nbe.norm_conv) k
+    THEN TRYALL (resolve_tac [TrueI])
+  ))
 *} "solve goal by normalization"
 
 end
diff -r a141d6bfd398 -r 263aaf988d44 src/HOL/ex/NormalForm.thy
--- a/src/HOL/ex/NormalForm.thy	Tue Jan 08 11:37:32 2008 +0100
+++ b/src/HOL/ex/NormalForm.thy	Tue Jan 08 11:37:37 2008 +0100
@@ -9,14 +9,13 @@
 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
+lemma "((P | Q) | R) = (P | (Q | R))" by normalization rule
 declare disj_assoc [code func del]
-lemma "0 + (n::nat) = n" by normalization
-lemma "0 + Suc n = Suc n" by normalization
-lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization
+lemma "0 + (n::nat) = n" by normalization rule
+lemma "0 + Suc n = Suc n" by normalization rule
+lemma "Suc n + Suc m = n + Suc (Suc m)" by normalization rule
 lemma "~((0::nat) < (0::nat))" by normalization
 
 datatype n = Z | S n
@@ -40,9 +39,9 @@
 lemma [code]: "add2 n Z = n"
   by(induct n) auto
 
-lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization
-lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
-lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization
+lemma "add2 (add2 n m) k = add2 n (add2 m k)" by normalization rule
+lemma "add2 (add2 (S n) (S m)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization rule
+lemma "add2 (add2 (S n) (add2 (S m) Z)) (S k) = S(S(S(add2 n (add2 m k))))" by normalization rule
 
 primrec
   "mul Z = (%n. Z)"
@@ -59,7 +58,7 @@
 lemma "exp (S(S Z)) (S(S(S(S Z)))) = exp (S(S(S(S Z)))) (S(S Z))" by normalization
 
 lemma "(let ((x,y),(u,v)) = ((Z,Z),(Z,Z)) in add (add x y) (add u v)) = Z" by normalization
-lemma "split (%x y. x) (a, b) = a" by normalization
+lemma "split (%x y. x) (a, b) = a" by normalization rule
 lemma "(%((x,y),(u,v)). add (add x y) (add u v)) ((Z,Z),(Z,Z)) = Z" by normalization
 
 lemma "case Z of Z \<Rightarrow> True | S x \<Rightarrow> False" by normalization
@@ -67,7 +66,7 @@
 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
+lemma "[] @ xs = xs" by normalization rule
 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"
@@ -90,12 +89,11 @@
 normal_form "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f]) = [a, b, c, d, e, f]"
 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
+lemma "last [a, b, c] = c" by normalization rule
 lemma "last ([a, b, c] @ xs) = (if null xs then c else last xs)"
-  by normalization
+  by normalization rule
 
-lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization
+lemma "(2::int) + 3 - 1 + (- k) * 2 = 4 + - k * 2" by normalization rule
 lemma "(-4::int) * 2 = -8" by normalization
 lemma "abs ((-4::int) + 2 * 1) = 2" by normalization
 lemma "(2::int) + 3 = 5" by normalization