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```