# HG changeset patch # User huffman # Date 1133308524 -3600 # Node ID 5fc3097708402d6ef066ab84eb9de339a259ab1a # Parent 56ddf617d6e80338713d182119fdbed66f3f9685 add xsymbol syntax for u type constructor diff -r 56ddf617d6e8 -r 5fc309770840 src/HOLCF/Up.thy --- a/src/HOLCF/Up.thy Wed Nov 30 00:53:30 2005 +0100 +++ b/src/HOLCF/Up.thy Wed Nov 30 00:55:24 2005 +0100 @@ -17,6 +17,9 @@ datatype 'a u = Ibottom | Iup 'a +syntax (xsymbols) + "u" :: "type \ type" ("(_\<^sub>\)" [1000] 999) + consts Ifup :: "('a \ 'b::pcpo) \ 'a u \ 'b" @@ -24,7 +27,7 @@ "Ifup f Ibottom = \" "Ifup f (Iup x) = f\x" -subsection {* Ordering on type @{typ "'a u"} *} +subsection {* Ordering on lifted cpo *} instance u :: (sq_ord) sq_ord .. @@ -42,7 +45,7 @@ lemma Iup_less [iff]: "(Iup x \ Iup y) = (x \ y)" by (simp add: less_up_def) -subsection {* Type @{typ "'a u"} is a partial order *} +subsection {* Lifted cpo is a partial order *} lemma refl_less_up: "(x::'a u) \ x" by (simp add: less_up_def split: u.split) @@ -61,7 +64,7 @@ by intro_classes (assumption | rule refl_less_up antisym_less_up trans_less_up)+ -subsection {* Type @{typ "'a u"} is a cpo *} +subsection {* Lifted cpo is a cpo *} lemma is_lub_Iup: "range S <<| x \ range (\i. Iup (S i)) <<| Iup x" @@ -147,7 +150,7 @@ instance u :: (cpo) cpo by intro_classes (rule cpo_up) -subsection {* Type @{typ "'a u"} is pointed *} +subsection {* Lifted cpo is pointed *} lemma least_up: "\x::'a u. \y. x \ y" apply (rule_tac x = "Ibottom" in exI)