# HG changeset patch
# User huffman
# Date 1294182207 28800
# Node ID cf5f025bc3c7adbf54715de36534653a61a6a4c6
# Parent  44511bf5dcc61edc719b9338b1a5884bdd8a0d1b
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
removed redundant lemma UU_least

diff -r 44511bf5dcc6 -r cf5f025bc3c7 NEWS
--- a/NEWS	Mon Jan 03 17:10:32 2011 +0100
+++ b/NEWS	Tue Jan 04 15:03:27 2011 -0800
@@ -547,6 +547,9 @@
 from e.g. '+\<sharp>' to '\<union>\<sharp>', for consistency with set
 syntax. INCOMPATIBILITY.
 
+* The constant 'UU' has been renamed to 'bottom'. The syntax 'UU' is
+still supported as an input translation.
+
 * Renamed some theorems (the original names are also still available).
   expand_fun_below   ~> fun_below_iff
   below_fun_ext      ~> fun_belowI
diff -r 44511bf5dcc6 -r cf5f025bc3c7 src/HOL/HOLCF/Fixrec.thy
--- a/src/HOL/HOLCF/Fixrec.thy	Mon Jan 03 17:10:32 2011 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy	Tue Jan 04 15:03:27 2011 -0800
@@ -241,7 +241,7 @@
       (@{const_name ONE}, @{const_name match_ONE}),
       (@{const_name TT}, @{const_name match_TT}),
       (@{const_name FF}, @{const_name match_FF}),
-      (@{const_name UU}, @{const_name match_bottom}) ]
+      (@{const_name bottom}, @{const_name match_bottom}) ]
 *}
 
 hide_const (open) succeed fail run
diff -r 44511bf5dcc6 -r cf5f025bc3c7 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 03 17:10:32 2011 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Jan 04 15:03:27 2011 -0800
@@ -42,7 +42,7 @@
   "[x, xs!]"     == "x>>[xs!]"
   "[x!]"         == "x>>nil"
   "[x, xs?]"     == "x>>[xs?]"
-  "[x?]"         == "x>>CONST UU"
+  "[x?]"         == "x>>CONST bottom"
 
 defs
 
diff -r 44511bf5dcc6 -r cf5f025bc3c7 src/HOL/HOLCF/Pcpo.thy
--- a/src/HOL/HOLCF/Pcpo.thy	Mon Jan 03 17:10:32 2011 +0100
+++ b/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:03:27 2011 -0800
@@ -143,32 +143,34 @@
   assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
 begin
 
-definition UU :: 'a where
-  "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
+definition bottom :: "'a"
+  where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)"
 
 notation (xsymbols)
-  UU  ("\<bottom>")
+  bottom ("\<bottom>")
 
-text {* derive the old rule minimal *}
- 
-lemma UU_least: "\<forall>z. \<bottom> \<sqsubseteq> z"
-apply (unfold UU_def)
-apply (rule theI')
+lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
+unfolding bottom_def
+apply (rule the1I2)
 apply (rule ex_ex1I)
 apply (rule least)
 apply (blast intro: below_antisym)
+apply simp
 done
 
-lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
-by (rule UU_least [THEN spec])
+end
+
+text {* Old "UU" syntax: *}
 
-end
+syntax UU :: logic
+
+translations "UU" => "CONST bottom"
 
 text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
 
 setup {*
   Reorient_Proc.add
-    (fn Const(@{const_name UU}, _) => true | _ => false)
+    (fn Const(@{const_name bottom}, _) => true | _ => false)
 *}
 
 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
diff -r 44511bf5dcc6 -r cf5f025bc3c7 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Jan 03 17:10:32 2011 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Jan 04 15:03:27 2011 -0800
@@ -221,7 +221,7 @@
           val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy)
         in Library.foldr mk_ex (vs, conj) end
       val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
-      (* first rules replace "y = UU \/ P" with "rep$y = UU \/ P" *)
+      (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
       val tacs = [
           rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
           rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
@@ -264,8 +264,8 @@
           val (vs, nonlazy) = get_vars args
           fun one_strict v' =
             let
-              val UU = mk_bottom (fastype_of v')
-              val vs' = map (fn v => if v = v' then UU else v) vs
+              val bottom = mk_bottom (fastype_of v')
+              val vs' = map (fn v => if v = v' then bottom else v) vs
               val goal = mk_trp (mk_undef (list_ccomb (con, vs')))
               val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]
             in prove thy con_betas goal (K tacs) end
@@ -461,7 +461,7 @@
           app "_case1" (con1 authentic n c, expvar n)
       fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
       fun when1 n (m, c) =
-          if n = m then arg1 (n, c) else (Constant @{const_syntax UU})
+          if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
       val case_constant = Constant (syntax (case_const dummyT))
       fun case_trans authentic =
           (if authentic then ParsePrintRule else ParseRule)
diff -r 44511bf5dcc6 -r cf5f025bc3c7 src/HOL/HOLCF/Tools/cpodef.ML
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Jan 03 17:10:32 2011 +0100
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Tue Jan 04 15:03:27 2011 -0800
@@ -65,9 +65,9 @@
     let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
     in rule OF [set_def, thm] end
 
-fun fold_UU_mem thm NONE = thm
-  | fold_UU_mem thm (SOME set_def) =
-    let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
+fun fold_bottom_mem thm NONE = thm
+  | fold_bottom_mem thm (SOME set_def) =
+    let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp}
     in rule OF [set_def, thm] end
 
 (* proving class instances *)
@@ -120,12 +120,12 @@
       (type_definition: thm)  (* type_definition Rep Abs A *)
       (set_def: thm option)   (* A == set *)
       (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
-      (UU_mem: thm)           (* UU : set *)
+      (bottom_mem: thm)       (* bottom : set *)
       (thy: theory)
     =
   let
-    val UU_mem' = fold_UU_mem UU_mem set_def
-    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem']
+    val bottom_mem' = fold_bottom_mem bottom_mem set_def
+    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem']
     val (full_tname, Ts) = dest_Type newT
     val lhs_sorts = map (snd o dest_TFree) Ts
     val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
@@ -252,26 +252,26 @@
     val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
       prepare prep_term name typ raw_set opt_morphs thy
 
-    val goal_UU_mem =
-      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set))
+    val goal_bottom_mem =
+      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set))
 
     val goal_admissible =
       HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)))
 
-    fun pcpodef_result UU_mem admissible thy =
+    fun pcpodef_result bottom_mem admissible thy =
       let
-        val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1
+        val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
         val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
           |> add_podef def (SOME name) typ set opt_morphs tac
         val (cpo_info, thy) = thy
           |> prove_cpo name newT morphs type_definition set_def below_def admissible
         val (pcpo_info, thy) = thy
-          |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem
+          |> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem
       in
         ((info, cpo_info, pcpo_info), thy)
       end
   in
-    (goal_UU_mem, goal_admissible, pcpodef_result)
+    (goal_bottom_mem, goal_admissible, pcpodef_result)
   end
   handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name))
diff -r 44511bf5dcc6 -r cf5f025bc3c7 src/HOL/HOLCF/Tools/holcf_library.ML
--- a/src/HOL/HOLCF/Tools/holcf_library.ML	Mon Jan 03 17:10:32 2011 +0100
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Jan 04 15:03:27 2011 -0800
@@ -32,7 +32,7 @@
 
 (*** Basic HOLCF concepts ***)
 
-fun mk_bottom T = Const (@{const_name UU}, T)
+fun mk_bottom T = Const (@{const_name bottom}, T)
 
 fun below_const T = Const (@{const_name below}, [T, T] ---> boolT)
 fun mk_below (t, u) = below_const (fastype_of t) $ t $ u