src/HOLCF/Cprod.thy
changeset 16008 861a255cf1e7
parent 15609 d12c459e2325
child 16057 e23a61b3406f
equal deleted inserted replaced
16007:4dcccaa11a13 16008:861a255cf1e7
    11 theory Cprod
    11 theory Cprod
    12 imports Cfun
    12 imports Cfun
    13 begin
    13 begin
    14 
    14 
    15 defaultsort cpo
    15 defaultsort cpo
       
    16 
       
    17 subsection {* Type @{typ unit} is a pcpo *}
       
    18 
       
    19 instance unit :: sq_ord ..
       
    20 
       
    21 defs (overloaded)
       
    22   less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
       
    23 
       
    24 instance unit :: po
       
    25 by intro_classes simp_all
       
    26 
       
    27 instance unit :: cpo
       
    28 by intro_classes (simp add: is_lub_def is_ub_def)
       
    29 
       
    30 instance unit :: pcpo
       
    31 by intro_classes simp
       
    32 
    16 
    33 
    17 subsection {* Ordering on @{typ "'a * 'b"} *}
    34 subsection {* Ordering on @{typ "'a * 'b"} *}
    18 
    35 
    19 instance "*" :: (sq_ord, sq_ord) sq_ord ..
    36 instance "*" :: (sq_ord, sq_ord) sq_ord ..
    20 
    37