# HG changeset patch
# User huffman
# Date 1241050501 25200
# Node ID 0fdf666e08bf955639a0b63951b111ffde705f74
# Parent  d027411c9a3812da07164750fd59d83b9b130926
reimplement reorientation simproc using theory data

diff -r d027411c9a38 -r 0fdf666e08bf src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Apr 29 13:36:29 2009 -0700
+++ b/src/HOL/HOL.thy	Wed Apr 29 17:15:01 2009 -0700
@@ -1568,6 +1568,56 @@
 setup Coherent.setup
 
 
+subsubsection {* Reorienting equalities *}
+
+ML {*
+signature REORIENT_PROC =
+sig
+  val init : theory -> theory
+  val add : (term -> bool) -> theory -> theory
+  val proc : morphism -> simpset -> cterm -> thm option
+end;
+
+structure ReorientProc : REORIENT_PROC =
+struct
+  structure Data = TheoryDataFun
+  (
+    type T = term -> bool;
+    val empty = (fn _ => false);
+    val copy = I;
+    val extend = I;
+    fun merge _ (m1, m2) = (fn t => m1 t orelse m2 t);
+  )
+
+  val init = Data.init;
+  fun add m = Data.map (fn matches => fn t => matches t orelse m t);
+  val meta_reorient = @{thm eq_commute [THEN eq_reflection]};
+  fun proc phi ss ct =
+    let
+      val ctxt = Simplifier.the_context ss;
+      val thy = ProofContext.theory_of ctxt;
+      val matches = Data.get thy;
+    in
+      case Thm.term_of ct of
+        (_ $ t $ u) => if matches u then NONE else SOME meta_reorient
+      | _ => NONE
+    end;
+end;
+*}
+
+setup ReorientProc.init
+
+setup {*
+  ReorientProc.add
+    (fn Const(@{const_name HOL.zero}, _) => true
+      | Const(@{const_name HOL.one}, _) => true
+      | _ => false)
+*}
+
+simproc_setup reorient_zero ("0 = x") = ReorientProc.proc
+simproc_setup reorient_one ("1 = x") = ReorientProc.proc
+
+
 subsection {* Other simple lemmas and lemma duplicates *}
 
 lemma Let_0 [simp]: "Let 0 f = f 0"
diff -r d027411c9a38 -r 0fdf666e08bf src/HOL/Int.thy
--- a/src/HOL/Int.thy	Wed Apr 29 13:36:29 2009 -0700
+++ b/src/HOL/Int.thy	Wed Apr 29 17:15:01 2009 -0700
@@ -1518,6 +1518,13 @@
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
 
+setup {*
+  ReorientProc.add
+    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
+*}
+
+simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc
+
 
 subsection{*Lemmas About Small Numerals*}
 
diff -r d027411c9a38 -r 0fdf666e08bf src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Apr 29 13:36:29 2009 -0700
+++ b/src/HOL/Nat.thy	Wed Apr 29 17:15:01 2009 -0700
@@ -1274,10 +1274,10 @@
 text{*Special cases where either operand is zero*}
 
 lemma of_nat_0_eq_iff [simp, noatp]: "0 = of_nat n \<longleftrightarrow> 0 = n"
-  by (rule of_nat_eq_iff [of 0, simplified])
+  by (rule of_nat_eq_iff [of 0 n, unfolded of_nat_0])
 
 lemma of_nat_eq_0_iff [simp, noatp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
-  by (rule of_nat_eq_iff [of _ 0, simplified])
+  by (rule of_nat_eq_iff [of m 0, unfolded of_nat_0])
 
 lemma inj_of_nat: "inj of_nat"
   by (simp add: inj_on_def)
diff -r d027411c9a38 -r 0fdf666e08bf src/HOL/Tools/int_arith.ML
--- a/src/HOL/Tools/int_arith.ML	Wed Apr 29 13:36:29 2009 -0700
+++ b/src/HOL/Tools/int_arith.ML	Wed Apr 29 17:15:01 2009 -0700
@@ -6,27 +6,6 @@
 structure Int_Numeral_Simprocs =
 struct
 
-(*reorientation simprules using ==, for the following simproc*)
-val meta_zero_reorient = @{thm zero_reorient} RS eq_reflection
-val meta_one_reorient = @{thm one_reorient} RS eq_reflection
-val meta_number_of_reorient = @{thm number_of_reorient} RS eq_reflection
-
-(*reorientation simplification procedure: reorients (polymorphic) 
-  0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a Int.*)
-fun reorient_proc sg _ (_ $ t $ u) =
-  case u of
-      Const(@{const_name HOL.zero}, _) => NONE
-    | Const(@{const_name HOL.one}, _) => NONE
-    | Const(@{const_name Int.number_of}, _) $ _ => NONE
-    | _ => SOME (case t of
-        Const(@{const_name HOL.zero}, _) => meta_zero_reorient
-      | Const(@{const_name HOL.one}, _) => meta_one_reorient
-      | Const(@{const_name Int.number_of}, _) $ _ => meta_number_of_reorient)
-
-val reorient_simproc = 
-  Arith_Data.prep_simproc ("reorient_simproc", ["0=x", "1=x", "number_of w = x"], reorient_proc);
-
-
 (** Utilities **)
 
 fun mk_number T n = HOLogic.number_of_const T $ HOLogic.mk_numeral n;
@@ -383,7 +362,6 @@
 
 end;
 
-Addsimprocs [Int_Numeral_Simprocs.reorient_simproc];
 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
 Addsimprocs [Int_Numeral_Simprocs.combine_numerals];
 Addsimprocs [Int_Numeral_Simprocs.field_combine_numerals];
diff -r d027411c9a38 -r 0fdf666e08bf src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Wed Apr 29 13:36:29 2009 -0700
+++ b/src/HOLCF/Pcpo.thy	Wed Apr 29 17:15:01 2009 -0700
@@ -193,26 +193,14 @@
 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
 by (rule UU_least [THEN spec])
 
-lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
-by auto
+text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
 
-ML {*
-local
-  val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
-  fun reorient_proc sg _ (_ $ t $ u) =
-    case u of
-        Const("Pcpo.UU",_) => NONE
-      | Const("HOL.zero", _) => NONE
-      | Const("HOL.one", _) => NONE
-      | Const("Numeral.number_of", _) $ _ => NONE
-      | _ => SOME meta_UU_reorient;
-in
-  val UU_reorient_simproc = 
-    Simplifier.simproc (the_context ()) "UU_reorient_simproc" ["UU=x"] reorient_proc
-end;
+setup {*
+  ReorientProc.add
+    (fn Const(@{const_name UU}, _) => true | _ => false)
+*}
 
-Addsimprocs [UU_reorient_simproc];
-*}
+simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
 
 text {* useful lemmas about @{term \<bottom>} *}