src/HOL/HOLCF/ex/Domain_Proofs.thy
 changeset 41287 029a6fc1bfb8 parent 40774 0437dbc127b3 child 41290 e9c9577d88b5
equal inserted replaced
41286:3d7685a4a5ff 41287:029a6fc1bfb8
`    28 `
`    28 `
`    29 text {* Start with the one-step non-recursive version *}`
`    29 text {* Start with the one-step non-recursive version *}`
`    30 `
`    30 `
`    31 definition`
`    31 definition`
`    32   foo_bar_baz_deflF ::`
`    32   foo_bar_baz_deflF ::`
`    33     "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"`
`    33     "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"`
`    34 where`
`    34 where`
`    35   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). `
`    35   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). `
`    36     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))`
`    36     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))`
`    37     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))`
`    37     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))`
`    38     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"`
`    38     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"`
`    45 unfolding foo_bar_baz_deflF_def`
`    45 unfolding foo_bar_baz_deflF_def`
`    46 by (simp add: split_def)`
`    46 by (simp add: split_def)`
`    47 `
`    47 `
`    48 text {* Individual type combinators are projected from the fixed point. *}`
`    48 text {* Individual type combinators are projected from the fixed point. *}`
`    49 `
`    49 `
`    50 definition foo_defl :: "defl \<rightarrow> defl"`
`    50 definition foo_defl :: "udom defl \<rightarrow> udom defl"`
`    51 where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"`
`    51 where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"`
`    52 `
`    52 `
`    53 definition bar_defl :: "defl \<rightarrow> defl"`
`    53 definition bar_defl :: "udom defl \<rightarrow> udom defl"`
`    54 where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"`
`    54 where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"`
`    55 `
`    55 `
`    56 definition baz_defl :: "defl \<rightarrow> defl"`
`    56 definition baz_defl :: "udom defl \<rightarrow> udom defl"`
`    57 where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"`
`    57 where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"`
`    58 `
`    58 `
`    59 lemma defl_apply_thms:`
`    59 lemma defl_apply_thms:`
`    60   "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"`
`    60   "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"`
`    61   "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"`
`    61   "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"`
`   101 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"`
`   101 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"`
`   102 `
`   102 `
`   103 definition prj_foo :: "udom \<rightarrow> 'a foo"`
`   103 definition prj_foo :: "udom \<rightarrow> 'a foo"`
`   104 where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"`
`   104 where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"`
`   105 `
`   105 `
`   106 definition defl_foo :: "'a foo itself \<Rightarrow> defl"`
`   106 definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"`
`   107 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"`
`   107 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"`
`   108 `
`   108 `
`   109 definition`
`   109 definition`
`   110   "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"`
`   110   "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"`
`   111 `
`   111 `
`   136 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"`
`   136 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"`
`   137 `
`   137 `
`   138 definition prj_bar :: "udom \<rightarrow> 'a bar"`
`   138 definition prj_bar :: "udom \<rightarrow> 'a bar"`
`   139 where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"`
`   139 where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"`
`   140 `
`   140 `
`   141 definition defl_bar :: "'a bar itself \<Rightarrow> defl"`
`   141 definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"`
`   142 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"`
`   142 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"`
`   143 `
`   143 `
`   144 definition`
`   144 definition`
`   145   "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"`
`   145   "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"`
`   146 `
`   146 `
`   171 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"`
`   171 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"`
`   172 `
`   172 `
`   173 definition prj_baz :: "udom \<rightarrow> 'a baz"`
`   173 definition prj_baz :: "udom \<rightarrow> 'a baz"`
`   174 where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"`
`   174 where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"`
`   175 `
`   175 `
`   176 definition defl_baz :: "'a baz itself \<Rightarrow> defl"`
`   176 definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"`
`   177 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"`
`   177 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"`
`   178 `
`   178 `
`   179 definition`
`   179 definition`
`   180   "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"`
`   180   "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"`
`   181 `
`   181 `