src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 41287 029a6fc1bfb8
parent 40774 0437dbc127b3
child 41290 e9c9577d88b5
--- a/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 05:15:31 2010 -0800
+++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sun Dec 19 06:34:41 2010 -0800
@@ -30,7 +30,7 @@
 
 definition
   foo_bar_baz_deflF ::
-    "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
+    "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"
 where
   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
@@ -47,13 +47,13 @@
 
 text {* Individual type combinators are projected from the fixed point. *}
 
-definition foo_defl :: "defl \<rightarrow> defl"
+definition foo_defl :: "udom defl \<rightarrow> udom defl"
 where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
 
-definition bar_defl :: "defl \<rightarrow> defl"
+definition bar_defl :: "udom defl \<rightarrow> udom defl"
 where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
-definition baz_defl :: "defl \<rightarrow> defl"
+definition baz_defl :: "udom defl \<rightarrow> udom defl"
 where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
 
 lemma defl_apply_thms:
@@ -103,7 +103,7 @@
 definition prj_foo :: "udom \<rightarrow> 'a foo"
 where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
-definition defl_foo :: "'a foo itself \<Rightarrow> defl"
+definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"
 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
 
 definition
@@ -138,7 +138,7 @@
 definition prj_bar :: "udom \<rightarrow> 'a bar"
 where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
-definition defl_bar :: "'a bar itself \<Rightarrow> defl"
+definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"
 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
 
 definition
@@ -173,7 +173,7 @@
 definition prj_baz :: "udom \<rightarrow> 'a baz"
 where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
 
-definition defl_baz :: "'a baz itself \<Rightarrow> defl"
+definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"
 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
 
 definition