--- a/src/HOL/ex/NormalForm.thy Tue Sep 08 18:31:26 2009 +0200
+++ b/src/HOL/ex/NormalForm.thy Wed Sep 09 11:31:20 2009 +0200
@@ -4,8 +4,17 @@
theory NormalForm
imports Main Rational
+uses "~~/src/Tools/nbe.ML"
begin
+setup {*
+ Nbe.add_const_alias @{thm equals_alias_cert}
+*}
+
+method_setup normalization = {*
+ Scan.succeed (K (SIMPLE_METHOD' (CONVERSION Nbe.norm_conv THEN' (fn k => TRY (rtac TrueI k)))))
+*} "solve goal by normalization"
+
lemma "True" by normalization
lemma "p \<longrightarrow> True" by normalization
declare disj_assoc [code nbe]
@@ -120,4 +129,13 @@
normal_form "(%m n f x. m (n f) x) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
normal_form "(%m n. n m) (%f x. f(f(f(x)))) (%f x. f(f(f(x))))"
+(* handling of type classes in connection with equality *)
+
+lemma "map f [x, y] = [f x, f y]" by normalization
+lemma "(map f [x, y], w) = ([f x, f y], w)" by normalization
+lemma "map f [x, y] = [f x \<Colon> 'a\<Colon>semigroup_add, f y]" by normalization
+lemma "map f [x \<Colon> 'a\<Colon>semigroup_add, y] = [f x, f y]" by normalization
+lemma "(map f [x \<Colon> 'a\<Colon>semigroup_add, y], w \<Colon> 'b\<Colon>finite) = ([f x, f y], w)" by normalization
+
+
end