# HG changeset patch
# User nipkow
# Date 1151581948 -7200
# Node ID 5aa2e37e250ca01d8dee1f11e0945724ef06b58d
# Parent  a0e3f2df9b0e7a842bd62b1c66d0f52f27f95f77
new method "normalization"

diff -r a0e3f2df9b0e -r 5aa2e37e250c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Thu Jun 29 01:08:08 2006 +0200
+++ b/src/HOL/HOL.thy	Thu Jun 29 13:52:28 2006 +0200
@@ -1274,6 +1274,36 @@
 setup evaluation_oracle_setup
 
 
+ML {*
+local
+
+exception Normalization of term;
+
+fun normalization_oracle (thy, Normalization t) = Logic.mk_equals
+  (t, HOLogic.mk_Trueprop (NBE.norm_term thy (HOLogic.dest_Trueprop t)));
+
+fun normalization_conv ct =
+  let val {sign, t, ...} = rep_cterm ct
+  in Thm.invoke_oracle_i sign "HOL.Normalization" (sign, Normalization t) end;
+
+fun normalization_tac i = Tactical.PRIMITIVE (Drule.fconv_rule
+  (Drule.goals_conv (equal i) normalization_conv));
+
+val normalization_meth =
+  Method.no_args (Method.METHOD (fn _ => normalization_tac 1 THEN rtac TrueI 1));
+
+in
+
+val normalization_oracle_setup =
+  Theory.add_oracle ("Normalization", normalization_oracle) #>
+  Method.add_method ("normalization", normalization_meth, "solve goal by normalization");
+
+end;
+*}
+
+setup normalization_oracle_setup
+
+
 subsection {* Other simple lemmas *}
 
 declare disj_absorb [simp] conj_absorb [simp]