renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
authorhuffman
Tue Jan 04 15:03:27 2011 -0800 (2011-01-04)
changeset 41429cf5f025bc3c7
parent 41428 44511bf5dcc6
child 41430 1aa23e9f2c87
renamed constant 'UU' to 'bottom', keeping 'UU' as alternative input syntax;
removed redundant lemma UU_least
NEWS
src/HOL/HOLCF/Fixrec.thy
src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
src/HOL/HOLCF/Pcpo.thy
src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/holcf_library.ML
     1.1 --- a/NEWS	Mon Jan 03 17:10:32 2011 +0100
     1.2 +++ b/NEWS	Tue Jan 04 15:03:27 2011 -0800
     1.3 @@ -547,6 +547,9 @@
     1.4  from e.g. '+\<sharp>' to '\<union>\<sharp>', for consistency with set
     1.5  syntax. INCOMPATIBILITY.
     1.6  
     1.7 +* The constant 'UU' has been renamed to 'bottom'. The syntax 'UU' is
     1.8 +still supported as an input translation.
     1.9 +
    1.10  * Renamed some theorems (the original names are also still available).
    1.11    expand_fun_below   ~> fun_below_iff
    1.12    below_fun_ext      ~> fun_belowI
     2.1 --- a/src/HOL/HOLCF/Fixrec.thy	Mon Jan 03 17:10:32 2011 +0100
     2.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Tue Jan 04 15:03:27 2011 -0800
     2.3 @@ -241,7 +241,7 @@
     2.4        (@{const_name ONE}, @{const_name match_ONE}),
     2.5        (@{const_name TT}, @{const_name match_TT}),
     2.6        (@{const_name FF}, @{const_name match_FF}),
     2.7 -      (@{const_name UU}, @{const_name match_bottom}) ]
     2.8 +      (@{const_name bottom}, @{const_name match_bottom}) ]
     2.9  *}
    2.10  
    2.11  hide_const (open) succeed fail run
     3.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Mon Jan 03 17:10:32 2011 +0100
     3.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Tue Jan 04 15:03:27 2011 -0800
     3.3 @@ -42,7 +42,7 @@
     3.4    "[x, xs!]"     == "x>>[xs!]"
     3.5    "[x!]"         == "x>>nil"
     3.6    "[x, xs?]"     == "x>>[xs?]"
     3.7 -  "[x?]"         == "x>>CONST UU"
     3.8 +  "[x?]"         == "x>>CONST bottom"
     3.9  
    3.10  defs
    3.11  
     4.1 --- a/src/HOL/HOLCF/Pcpo.thy	Mon Jan 03 17:10:32 2011 +0100
     4.2 +++ b/src/HOL/HOLCF/Pcpo.thy	Tue Jan 04 15:03:27 2011 -0800
     4.3 @@ -143,32 +143,34 @@
     4.4    assumes least: "\<exists>x. \<forall>y. x \<sqsubseteq> y"
     4.5  begin
     4.6  
     4.7 -definition UU :: 'a where
     4.8 -  "UU = (THE x. \<forall>y. x \<sqsubseteq> y)"
     4.9 +definition bottom :: "'a"
    4.10 +  where "bottom = (THE x. \<forall>y. x \<sqsubseteq> y)"
    4.11  
    4.12  notation (xsymbols)
    4.13 -  UU  ("\<bottom>")
    4.14 +  bottom ("\<bottom>")
    4.15  
    4.16 -text {* derive the old rule minimal *}
    4.17 - 
    4.18 -lemma UU_least: "\<forall>z. \<bottom> \<sqsubseteq> z"
    4.19 -apply (unfold UU_def)
    4.20 -apply (rule theI')
    4.21 +lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
    4.22 +unfolding bottom_def
    4.23 +apply (rule the1I2)
    4.24  apply (rule ex_ex1I)
    4.25  apply (rule least)
    4.26  apply (blast intro: below_antisym)
    4.27 +apply simp
    4.28  done
    4.29  
    4.30 -lemma minimal [iff]: "\<bottom> \<sqsubseteq> x"
    4.31 -by (rule UU_least [THEN spec])
    4.32 +end
    4.33 +
    4.34 +text {* Old "UU" syntax: *}
    4.35  
    4.36 -end
    4.37 +syntax UU :: logic
    4.38 +
    4.39 +translations "UU" => "CONST bottom"
    4.40  
    4.41  text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
    4.42  
    4.43  setup {*
    4.44    Reorient_Proc.add
    4.45 -    (fn Const(@{const_name UU}, _) => true | _ => false)
    4.46 +    (fn Const(@{const_name bottom}, _) => true | _ => false)
    4.47  *}
    4.48  
    4.49  simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
     5.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Mon Jan 03 17:10:32 2011 +0100
     5.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Tue Jan 04 15:03:27 2011 -0800
     5.3 @@ -221,7 +221,7 @@
     5.4            val conj = foldr1 mk_conj (eqn :: map mk_defined nonlazy)
     5.5          in Library.foldr mk_ex (vs, conj) end
     5.6        val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec'))
     5.7 -      (* first rules replace "y = UU \/ P" with "rep$y = UU \/ P" *)
     5.8 +      (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *)
     5.9        val tacs = [
    5.10            rtac (iso_locale RS @{thm iso.casedist_rule}) 1,
    5.11            rewrite_goals_tac [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})],
    5.12 @@ -264,8 +264,8 @@
    5.13            val (vs, nonlazy) = get_vars args
    5.14            fun one_strict v' =
    5.15              let
    5.16 -              val UU = mk_bottom (fastype_of v')
    5.17 -              val vs' = map (fn v => if v = v' then UU else v) vs
    5.18 +              val bottom = mk_bottom (fastype_of v')
    5.19 +              val vs' = map (fn v => if v = v' then bottom else v) vs
    5.20                val goal = mk_trp (mk_undef (list_ccomb (con, vs')))
    5.21                val tacs = [simp_tac (HOL_basic_ss addsimps rules) 1]
    5.22              in prove thy con_betas goal (K tacs) end
    5.23 @@ -461,7 +461,7 @@
    5.24            app "_case1" (con1 authentic n c, expvar n)
    5.25        fun arg1 (n, (con,args)) = List.foldr cabs (expvar n) (argvars n args)
    5.26        fun when1 n (m, c) =
    5.27 -          if n = m then arg1 (n, c) else (Constant @{const_syntax UU})
    5.28 +          if n = m then arg1 (n, c) else (Constant @{const_syntax bottom})
    5.29        val case_constant = Constant (syntax (case_const dummyT))
    5.30        fun case_trans authentic =
    5.31            (if authentic then ParsePrintRule else ParseRule)
     6.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Mon Jan 03 17:10:32 2011 +0100
     6.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Tue Jan 04 15:03:27 2011 -0800
     6.3 @@ -65,9 +65,9 @@
     6.4      let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
     6.5      in rule OF [set_def, thm] end
     6.6  
     6.7 -fun fold_UU_mem thm NONE = thm
     6.8 -  | fold_UU_mem thm (SOME set_def) =
     6.9 -    let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
    6.10 +fun fold_bottom_mem thm NONE = thm
    6.11 +  | fold_bottom_mem thm (SOME set_def) =
    6.12 +    let val rule = @{lemma "A == B ==> bottom : B ==> bottom : A" by simp}
    6.13      in rule OF [set_def, thm] end
    6.14  
    6.15  (* proving class instances *)
    6.16 @@ -120,12 +120,12 @@
    6.17        (type_definition: thm)  (* type_definition Rep Abs A *)
    6.18        (set_def: thm option)   (* A == set *)
    6.19        (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
    6.20 -      (UU_mem: thm)           (* UU : set *)
    6.21 +      (bottom_mem: thm)       (* bottom : set *)
    6.22        (thy: theory)
    6.23      =
    6.24    let
    6.25 -    val UU_mem' = fold_UU_mem UU_mem set_def
    6.26 -    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem']
    6.27 +    val bottom_mem' = fold_bottom_mem bottom_mem set_def
    6.28 +    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem']
    6.29      val (full_tname, Ts) = dest_Type newT
    6.30      val lhs_sorts = map (snd o dest_TFree) Ts
    6.31      val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
    6.32 @@ -252,26 +252,26 @@
    6.33      val (newT, oldT, set, morphs as (Rep_name, Abs_name)) =
    6.34        prepare prep_term name typ raw_set opt_morphs thy
    6.35  
    6.36 -    val goal_UU_mem =
    6.37 -      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set))
    6.38 +    val goal_bottom_mem =
    6.39 +      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name bottom}, oldT), set))
    6.40  
    6.41      val goal_admissible =
    6.42        HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)))
    6.43  
    6.44 -    fun pcpodef_result UU_mem admissible thy =
    6.45 +    fun pcpodef_result bottom_mem admissible thy =
    6.46        let
    6.47 -        val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1
    6.48 +        val tac = Tactic.rtac exI 1 THEN Tactic.rtac bottom_mem 1
    6.49          val ((info as (_, {type_definition, set_def, ...}), below_def), thy) = thy
    6.50            |> add_podef def (SOME name) typ set opt_morphs tac
    6.51          val (cpo_info, thy) = thy
    6.52            |> prove_cpo name newT morphs type_definition set_def below_def admissible
    6.53          val (pcpo_info, thy) = thy
    6.54 -          |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem
    6.55 +          |> prove_pcpo name newT morphs type_definition set_def below_def bottom_mem
    6.56        in
    6.57          ((info, cpo_info, pcpo_info), thy)
    6.58        end
    6.59    in
    6.60 -    (goal_UU_mem, goal_admissible, pcpodef_result)
    6.61 +    (goal_bottom_mem, goal_admissible, pcpodef_result)
    6.62    end
    6.63    handle ERROR msg =>
    6.64      cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name))
     7.1 --- a/src/HOL/HOLCF/Tools/holcf_library.ML	Mon Jan 03 17:10:32 2011 +0100
     7.2 +++ b/src/HOL/HOLCF/Tools/holcf_library.ML	Tue Jan 04 15:03:27 2011 -0800
     7.3 @@ -32,7 +32,7 @@
     7.4  
     7.5  (*** Basic HOLCF concepts ***)
     7.6  
     7.7 -fun mk_bottom T = Const (@{const_name UU}, T)
     7.8 +fun mk_bottom T = Const (@{const_name bottom}, T)
     7.9  
    7.10  fun below_const T = Const (@{const_name below}, [T, T] ---> boolT)
    7.11  fun mk_below (t, u) = below_const (fastype_of t) $ t $ u