add constant unit_when
authorhuffman
Wed Nov 30 00:53:30 2005 +0100 (2005-11-30)
changeset 1828956ddf617d6e8
parent 18288 feb79a6b274b
child 18290 5fc309770840
add constant unit_when
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Wed Nov 30 00:46:08 2005 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Wed Nov 30 00:53:30 2005 +0100
     1.3 @@ -29,8 +29,18 @@
     1.4  instance unit :: pcpo
     1.5  by intro_classes simp
     1.6  
     1.7 +constdefs
     1.8 +  unit_when :: "'a \<rightarrow> unit \<rightarrow> 'a"
     1.9 +  "unit_when \<equiv> \<Lambda> a _. a"
    1.10  
    1.11 -subsection {* Type @{typ "'a * 'b"} is a partial order *}
    1.12 +translations
    1.13 +  "\<Lambda>(). t" == "unit_when\<cdot>t"
    1.14 +
    1.15 +lemma unit_when [simp]: "unit_when\<cdot>a\<cdot>u = a"
    1.16 +by (simp add: unit_when_def)
    1.17 +
    1.18 +
    1.19 +subsection {* Product type is a partial order *}
    1.20  
    1.21  instance "*" :: (sq_ord, sq_ord) sq_ord ..
    1.22  
    1.23 @@ -79,7 +89,7 @@
    1.24  lemma monofun_snd: "monofun snd"
    1.25  by (simp add: monofun_def less_cprod_def)
    1.26  
    1.27 -subsection {* Type @{typ "'a * 'b"} is a cpo *}
    1.28 +subsection {* Product type is a cpo *}
    1.29  
    1.30  lemma lub_cprod: 
    1.31    "chain S \<Longrightarrow> range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    1.32 @@ -112,7 +122,7 @@
    1.33  instance "*" :: (cpo, cpo) cpo
    1.34  by intro_classes (rule cpo_cprod)
    1.35  
    1.36 -subsection {* Type @{typ "'a * 'b"} is pointed *}
    1.37 +subsection {* Product type is pointed *}
    1.38  
    1.39  lemma minimal_cprod: "(\<bottom>, \<bottom>) \<sqsubseteq> p"
    1.40  by (simp add: less_cprod_def)