src/HOLCF/Lift.thy
changeset 31076 99fe356cbbc2
parent 30607 c3d1590debd8
child 32149 ef59550a55d3
     1.1 --- a/src/HOLCF/Lift.thy	Fri May 08 19:28:11 2009 +0100
     1.2 +++ b/src/HOLCF/Lift.thy	Fri May 08 16:19:51 2009 -0700
     1.3 @@ -70,11 +70,11 @@
     1.4  lemma DefE2: "\<lbrakk>x = Def s; x = \<bottom>\<rbrakk> \<Longrightarrow> R"
     1.5    by simp
     1.6  
     1.7 -lemma Def_inject_less_eq: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
     1.8 -by (simp add: less_lift_def Def_def Abs_lift_inverse lift_def)
     1.9 +lemma Def_below_Def: "Def x \<sqsubseteq> Def y \<longleftrightarrow> x = y"
    1.10 +by (simp add: below_lift_def Def_def Abs_lift_inverse lift_def)
    1.11  
    1.12 -lemma Def_less_is_eq [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
    1.13 -by (induct y, simp, simp add: Def_inject_less_eq)
    1.14 +lemma Def_below_iff [simp]: "Def x \<sqsubseteq> y \<longleftrightarrow> Def x = y"
    1.15 +by (induct y, simp, simp add: Def_below_Def)
    1.16  
    1.17  
    1.18  subsection {* Lift is flat *}
    1.19 @@ -134,7 +134,7 @@
    1.20    "(\<And>x. f x \<sqsubseteq> g x) \<Longrightarrow> (FLIFT x. f x) \<sqsubseteq> (FLIFT x. g x)"
    1.21  apply (rule monofunE [where f=flift1])
    1.22  apply (rule cont2mono [OF cont_flift1])
    1.23 -apply (simp add: less_fun_ext)
    1.24 +apply (simp add: below_fun_ext)
    1.25  done
    1.26  
    1.27  lemma cont2cont_flift1 [simp]:
    1.28 @@ -216,7 +216,7 @@
    1.29      apply (rule is_lubI)
    1.30       apply (rule ub_rangeI, simp)
    1.31      apply (drule ub_rangeD)
    1.32 -    apply (erule rev_trans_less)
    1.33 +    apply (erule rev_below_trans)
    1.34      apply simp
    1.35      apply (rule lessI)
    1.36      done