src/HOLCF/Pcpo.thy
changeset 31024 0fdf666e08bf
parent 29634 2baf1b2f6655
child 31071 845a6acd3bf3
     1.1 --- a/src/HOLCF/Pcpo.thy	Wed Apr 29 13:36:29 2009 -0700
     1.2 +++ b/src/HOLCF/Pcpo.thy	Wed Apr 29 17:15:01 2009 -0700
     1.3 @@ -193,26 +193,14 @@
     1.4  lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
     1.5  by (rule UU_least [THEN spec])
     1.6  
     1.7 -lemma UU_reorient: "(\<bottom> = x) = (x = \<bottom>)"
     1.8 -by auto
     1.9 +text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
    1.10  
    1.11 -ML {*
    1.12 -local
    1.13 -  val meta_UU_reorient = thm "UU_reorient" RS eq_reflection;
    1.14 -  fun reorient_proc sg _ (_ $ t $ u) =
    1.15 -    case u of
    1.16 -        Const("Pcpo.UU",_) => NONE
    1.17 -      | Const("HOL.zero", _) => NONE
    1.18 -      | Const("HOL.one", _) => NONE
    1.19 -      | Const("Numeral.number_of", _) $ _ => NONE
    1.20 -      | _ => SOME meta_UU_reorient;
    1.21 -in
    1.22 -  val UU_reorient_simproc = 
    1.23 -    Simplifier.simproc (the_context ()) "UU_reorient_simproc" ["UU=x"] reorient_proc
    1.24 -end;
    1.25 +setup {*
    1.26 +  ReorientProc.add
    1.27 +    (fn Const(@{const_name UU}, _) => true | _ => false)
    1.28 +*}
    1.29  
    1.30 -Addsimprocs [UU_reorient_simproc];
    1.31 -*}
    1.32 +simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
    1.33  
    1.34  text {* useful lemmas about @{term \<bottom>} *}
    1.35