add xsymbol syntax for u type constructor
authorhuffman
Wed Nov 30 00:55:24 2005 +0100 (2005-11-30)
changeset 182905fc309770840
parent 18289 56ddf617d6e8
child 18291 4afdf02d9831
add xsymbol syntax for u type constructor
src/HOLCF/Up.thy
     1.1 --- a/src/HOLCF/Up.thy	Wed Nov 30 00:53:30 2005 +0100
     1.2 +++ b/src/HOLCF/Up.thy	Wed Nov 30 00:55:24 2005 +0100
     1.3 @@ -17,6 +17,9 @@
     1.4  
     1.5  datatype 'a u = Ibottom | Iup 'a
     1.6  
     1.7 +syntax (xsymbols)
     1.8 +  "u" :: "type \<Rightarrow> type" ("(_\<^sub>\<bottom>)" [1000] 999)
     1.9 +
    1.10  consts
    1.11    Ifup :: "('a \<rightarrow> 'b::pcpo) \<Rightarrow> 'a u \<Rightarrow> 'b"
    1.12  
    1.13 @@ -24,7 +27,7 @@
    1.14    "Ifup f Ibottom = \<bottom>"
    1.15    "Ifup f (Iup x) = f\<cdot>x"
    1.16  
    1.17 -subsection {* Ordering on type @{typ "'a u"} *}
    1.18 +subsection {* Ordering on lifted cpo *}
    1.19  
    1.20  instance u :: (sq_ord) sq_ord ..
    1.21  
    1.22 @@ -42,7 +45,7 @@
    1.23  lemma Iup_less [iff]: "(Iup x \<sqsubseteq> Iup y) = (x \<sqsubseteq> y)"
    1.24  by (simp add: less_up_def)
    1.25  
    1.26 -subsection {* Type @{typ "'a u"} is a partial order *}
    1.27 +subsection {* Lifted cpo is a partial order *}
    1.28  
    1.29  lemma refl_less_up: "(x::'a u) \<sqsubseteq> x"
    1.30  by (simp add: less_up_def split: u.split)
    1.31 @@ -61,7 +64,7 @@
    1.32  by intro_classes
    1.33    (assumption | rule refl_less_up antisym_less_up trans_less_up)+
    1.34  
    1.35 -subsection {* Type @{typ "'a u"} is a cpo *}
    1.36 +subsection {* Lifted cpo is a cpo *}
    1.37  
    1.38  lemma is_lub_Iup:
    1.39    "range S <<| x \<Longrightarrow> range (\<lambda>i. Iup (S i)) <<| Iup x"
    1.40 @@ -147,7 +150,7 @@
    1.41  instance u :: (cpo) cpo
    1.42  by intro_classes (rule cpo_up)
    1.43  
    1.44 -subsection {* Type @{typ "'a u"} is pointed *}
    1.45 +subsection {* Lifted cpo is pointed *}
    1.46  
    1.47  lemma least_up: "\<exists>x::'a u. \<forall>y. x \<sqsubseteq> y"
    1.48  apply (rule_tac x = "Ibottom" in exI)