src/HOLCF/Up.thy
changeset 31076 99fe356cbbc2
parent 29530 9905b660612b
child 33504 b4210cc3ac97
     1.1 --- a/src/HOLCF/Up.thy	Fri May 08 19:28:11 2009 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Fri May 08 16:19:51 2009 -0700
     1.3 @@ -26,11 +26,11 @@
     1.4  
     1.5  subsection {* Ordering on lifted cpo *}
     1.6  
     1.7 -instantiation u :: (cpo) sq_ord
     1.8 +instantiation u :: (cpo) below
     1.9  begin
    1.10  
    1.11  definition
    1.12 -  less_up_def:
    1.13 +  below_up_def:
    1.14      "(op \<sqsubseteq>) \<equiv> (\<lambda>x y. case x of Ibottom \<Rightarrow> True | Iup a \<Rightarrow>
    1.15        (case y of Ibottom \<Rightarrow> False | Iup b \<Rightarrow> a \<sqsubseteq> b))"
    1.16  
    1.17 @@ -38,13 +38,13 @@
    1.18  end
    1.19  
    1.20  lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
    1.21 -by (simp add: less_up_def)
    1.22 +by (simp add: below_up_def)
    1.23  
    1.24 -lemma not_Iup_less [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
    1.25 -by (simp add: less_up_def)
    1.26 +lemma not_Iup_below [iff]: "\<not> Iup x \<sqsubseteq> Ibottom"
    1.27 +by (simp add: below_up_def)
    1.28  
    1.29 -lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
    1.30 -by (simp add: less_up_def)
    1.31 +lemma Iup_below [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
    1.32 +by (simp add: below_up_def)
    1.33  
    1.34  subsection {* Lifted cpo is a partial order *}
    1.35  
    1.36 @@ -52,17 +52,17 @@
    1.37  proof
    1.38    fix x :: "'a u"
    1.39    show "x \<sqsubseteq> x"
    1.40 -    unfolding less_up_def by (simp split: u.split)
    1.41 +    unfolding below_up_def by (simp split: u.split)
    1.42  next
    1.43    fix x y :: "'a u"
    1.44    assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    1.45 -    unfolding less_up_def
    1.46 -    by (auto split: u.split_asm intro: antisym_less)
    1.47 +    unfolding below_up_def
    1.48 +    by (auto split: u.split_asm intro: below_antisym)
    1.49  next
    1.50    fix x y z :: "'a u"
    1.51    assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    1.52 -    unfolding less_up_def
    1.53 -    by (auto split: u.split_asm intro: trans_less)
    1.54 +    unfolding below_up_def
    1.55 +    by (auto split: u.split_asm intro: below_trans)
    1.56  qed
    1.57  
    1.58  lemma u_UNIV: "UNIV = insert Ibottom (range Iup)"
    1.59 @@ -78,7 +78,7 @@
    1.60    "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
    1.61  apply (rule is_lubI)
    1.62  apply (rule ub_rangeI)
    1.63 -apply (subst Iup_less)
    1.64 +apply (subst Iup_below)
    1.65  apply (erule is_ub_lub)
    1.66  apply (case_tac u)
    1.67  apply (drule ub_rangeD)
    1.68 @@ -112,7 +112,7 @@
    1.69  lemma up_lemma4:
    1.70    "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> chain (\<lambda>i. THE a. Iup a = Y (i + j))"
    1.71  apply (rule chainI)
    1.72 -apply (rule Iup_less [THEN iffD1])
    1.73 +apply (rule Iup_below [THEN iffD1])
    1.74  apply (subst up_lemma3, assumption+)+
    1.75  apply (simp add: chainE)
    1.76  done
    1.77 @@ -235,9 +235,9 @@
    1.78  by (simp add: up_def cont_Iup inst_up_pcpo)
    1.79  
    1.80  lemma not_up_less_UU: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
    1.81 -by simp
    1.82 +by simp (* FIXME: remove? *)
    1.83  
    1.84 -lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
    1.85 +lemma up_below [simp]: "up\<cdot>x \<sqsubseteq> up\<cdot>y \<longleftrightarrow> x \<sqsubseteq> y"
    1.86  by (simp add: up_def cont_Iup)
    1.87  
    1.88  lemma upE [cases type: u]: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"