# HG changeset patch
# User huffman
# Date 1120753321 -7200
# Node ID 9ffd706ae402187e4e3c66dee3784929e89b04a7
# Parent  b70bac29b11d50a74c8a3df61edd3568c0426ea8
add UU_reorient_simproc

diff -r b70bac29b11d -r 9ffd706ae402 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Jul 07 18:20:08 2005 +0200
+++ b/src/HOLCF/Pcpo.thy	Thu Jul 07 18:22:01 2005 +0200
@@ -203,6 +203,25 @@
 lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
 by (rule UU_least [THEN spec])
 
+lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
+by auto
+
+ML_setup {*
+local
+  val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
+  fun is_UU (Const ("Pcpo.UU",_)) = true
+    | is_UU _ = false;
+  fun reorient_proc sg _ (_ $ t $ u) =
+    if is_UU u then NONE else SOME meta_UU_reorient;
+in
+  val UU_reorient_simproc = 
+    Simplifier.simproc (the_context ())
+      "UU_reorient_simproc" ["UU=x"] reorient_proc
+end;
+
+Addsimprocs [UU_reorient_simproc];
+*}
+
 text {* useful lemmas about @{term \<bottom>} *}
 
 lemma eq_UU_iff: "(x = \<bottom>) = (x \<sqsubseteq> \<bottom>)"