src/HOL/HOLCF/Lift.thy
changeset 55417 01fbfb60c33e
parent 51717 9e7d1c139569
child 55642 63beb38e9258
     1.1 --- a/src/HOL/HOLCF/Lift.thy	Wed Feb 12 08:35:57 2014 +0100
     1.2 +++ b/src/HOL/HOLCF/Lift.thy	Wed Feb 12 08:37:06 2014 +0100
     1.3 @@ -71,23 +71,23 @@
     1.4      by (induct x) auto
     1.5  qed
     1.6  
     1.7 -subsection {* Continuity of @{const lift_case} *}
     1.8 +subsection {* Continuity of @{const case_lift} *}
     1.9  
    1.10 -lemma lift_case_eq: "lift_case \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
    1.11 +lemma case_lift_eq: "case_lift \<bottom> f x = fup\<cdot>(\<Lambda> y. f (undiscr y))\<cdot>(Rep_lift x)"
    1.12  apply (induct x, unfold lift.cases)
    1.13  apply (simp add: Rep_lift_strict)
    1.14  apply (simp add: Def_def Abs_lift_inverse)
    1.15  done
    1.16  
    1.17 -lemma cont2cont_lift_case [simp]:
    1.18 -  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. lift_case \<bottom> (f x) (g x))"
    1.19 -unfolding lift_case_eq by (simp add: cont_Rep_lift)
    1.20 +lemma cont2cont_case_lift [simp]:
    1.21 +  "\<lbrakk>\<And>y. cont (\<lambda>x. f x y); cont g\<rbrakk> \<Longrightarrow> cont (\<lambda>x. case_lift \<bottom> (f x) (g x))"
    1.22 +unfolding case_lift_eq by (simp add: cont_Rep_lift)
    1.23  
    1.24  subsection {* Further operations *}
    1.25  
    1.26  definition
    1.27    flift1 :: "('a \<Rightarrow> 'b::pcpo) \<Rightarrow> ('a lift \<rightarrow> 'b)"  (binder "FLIFT " 10)  where
    1.28 -  "flift1 = (\<lambda>f. (\<Lambda> x. lift_case \<bottom> f x))"
    1.29 +  "flift1 = (\<lambda>f. (\<Lambda> x. case_lift \<bottom> f x))"
    1.30  
    1.31  translations
    1.32    "\<Lambda>(XCONST Def x). t" => "CONST flift1 (\<lambda>x. t)"