src/HOL/HOLCF/Cfun.thy
changeset 41430 1aa23e9f2c87
parent 41400 1a7557cc686a
child 41478 18500bd1f47b
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Tue Jan 04 15:03:27 2011 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Tue Jan 04 15:32:56 2011 -0800
     1.3 @@ -92,20 +92,20 @@
     1.4  
     1.5  subsection {* Continuous function space is pointed *}
     1.6  
     1.7 -lemma UU_cfun: "\<bottom> \<in> cfun"
     1.8 +lemma bottom_cfun: "\<bottom> \<in> cfun"
     1.9  by (simp add: cfun_def inst_fun_pcpo)
    1.10  
    1.11  instance cfun :: (cpo, discrete_cpo) discrete_cpo
    1.12  by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
    1.13  
    1.14  instance cfun :: (cpo, pcpo) pcpo
    1.15 -by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
    1.16 +by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun])
    1.17  
    1.18  lemmas Rep_cfun_strict =
    1.19 -  typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
    1.20 +  typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
    1.21  
    1.22  lemmas Abs_cfun_strict =
    1.23 -  typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
    1.24 +  typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
    1.25  
    1.26  text {* function application is strict in its first argument *}
    1.27  
    1.28 @@ -261,7 +261,7 @@
    1.29  text {* strictness *}
    1.30  
    1.31  lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
    1.32 -apply (rule UU_I)
    1.33 +apply (rule bottomI)
    1.34  apply (erule subst)
    1.35  apply (rule minimal [THEN monofun_cfun_arg])
    1.36  done
    1.37 @@ -364,7 +364,7 @@
    1.38  
    1.39  lemma retraction_strict:
    1.40    "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
    1.41 -apply (rule UU_I)
    1.42 +apply (rule bottomI)
    1.43  apply (drule_tac x="\<bottom>" in spec)
    1.44  apply (erule subst)
    1.45  apply (rule monofun_cfun_arg)
    1.46 @@ -406,7 +406,7 @@
    1.47    "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
    1.48  apply (case_tac "f\<cdot>x = \<bottom>")
    1.49  apply (rule disjI1)
    1.50 -apply (rule UU_I)
    1.51 +apply (rule bottomI)
    1.52  apply (erule_tac t="\<bottom>" in subst)
    1.53  apply (rule minimal [THEN monofun_cfun_arg])
    1.54  apply clarify