src/HOLCF/Up.thy
changeset 25787 398dec10518e
parent 25785 dbe118fe3180
child 25788 30cbe0764599
     1.1 --- a/src/HOLCF/Up.thy	Wed Jan 02 18:57:40 2008 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Wed Jan 02 19:41:12 2008 +0100
     1.3 @@ -29,13 +29,17 @@
     1.4  
     1.5  subsection {* Ordering on lifted cpo *}
     1.6  
     1.7 -instance u :: (sq_ord) sq_ord ..
     1.8 +instantiation u :: (cpo) sq_ord
     1.9 +begin
    1.10  
    1.11 -defs (overloaded)
    1.12 +definition
    1.13    less_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 +instance ..
    1.18 +end
    1.19 +
    1.20  lemma minimal_up [iff]: "Ibottom \<sqsubseteq> z"
    1.21  by (simp add: less_up_def)
    1.22  
    1.23 @@ -47,22 +51,22 @@
    1.24  
    1.25  subsection {* Lifted cpo is a partial order *}
    1.26  
    1.27 -lemma refl_less_up: "(x::'a u) \<sqsubseteq> x"
    1.28 -by (simp add: less_up_def split: u.split)
    1.29 -
    1.30 -lemma antisym_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> x\<rbrakk> \<Longrightarrow> x = y"
    1.31 -apply (simp add: less_up_def split: u.split_asm)
    1.32 -apply (erule (1) antisym_less)
    1.33 -done
    1.34 -
    1.35 -lemma trans_less_up: "\<lbrakk>(x::'a u) \<sqsubseteq> y; y \<sqsubseteq> z\<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    1.36 -apply (simp add: less_up_def split: u.split_asm)
    1.37 -apply (erule (1) trans_less)
    1.38 -done
    1.39 -
    1.40  instance u :: (cpo) po
    1.41 -by intro_classes
    1.42 -  (assumption | rule refl_less_up antisym_less_up trans_less_up)+
    1.43 +proof
    1.44 +  fix x :: "'a u"
    1.45 +  show "x \<sqsubseteq> x"
    1.46 +    unfolding less_up_def by (simp split: u.split)
    1.47 +next
    1.48 +  fix x y :: "'a u"
    1.49 +  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    1.50 +    unfolding less_up_def
    1.51 +    by (auto split: u.split_asm intro: antisym_less)
    1.52 +next
    1.53 +  fix x y z :: "'a u"
    1.54 +  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    1.55 +    unfolding less_up_def
    1.56 +    by (auto split: u.split_asm intro: trans_less)
    1.57 +qed
    1.58  
    1.59  subsection {* Lifted cpo is a cpo *}
    1.60