src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 41287 029a6fc1bfb8
parent 40774 0437dbc127b3
child 41290 e9c9577d88b5
equal deleted 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