src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 40774 0437dbc127b3
parent 40771 1c6f7d4b110e
child 41287 029a6fc1bfb8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/ex/Domain_Proofs.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,501 @@
     1.4 +(*  Title:      HOLCF/ex/Domain_Proofs.thy
     1.5 +    Author:     Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Internal domain package proofs done manually *}
     1.9 +
    1.10 +theory Domain_Proofs
    1.11 +imports HOLCF
    1.12 +begin
    1.13 +
    1.14 +(*
    1.15 +
    1.16 +The definitions and proofs below are for the following recursive
    1.17 +datatypes:
    1.18 +
    1.19 +domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
    1.20 +   and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
    1.21 +   and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
    1.22 +
    1.23 +TODO: add another type parameter that is strict,
    1.24 +to show the different handling of LIFTDEFL vs. DEFL.
    1.25 +
    1.26 +*)
    1.27 +
    1.28 +(********************************************************************)
    1.29 +
    1.30 +subsection {* Step 1: Define the new type combinators *}
    1.31 +
    1.32 +text {* Start with the one-step non-recursive version *}
    1.33 +
    1.34 +definition
    1.35 +  foo_bar_baz_deflF ::
    1.36 +    "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
    1.37 +where
    1.38 +  "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). 
    1.39 +    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>t2))
    1.40 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))
    1.41 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"
    1.42 +
    1.43 +lemma foo_bar_baz_deflF_beta:
    1.44 +  "foo_bar_baz_deflF\<cdot>a\<cdot>t =
    1.45 +    ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
    1.46 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
    1.47 +    , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
    1.48 +unfolding foo_bar_baz_deflF_def
    1.49 +by (simp add: split_def)
    1.50 +
    1.51 +text {* Individual type combinators are projected from the fixed point. *}
    1.52 +
    1.53 +definition foo_defl :: "defl \<rightarrow> defl"
    1.54 +where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
    1.55 +
    1.56 +definition bar_defl :: "defl \<rightarrow> defl"
    1.57 +where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
    1.58 +
    1.59 +definition baz_defl :: "defl \<rightarrow> defl"
    1.60 +where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
    1.61 +
    1.62 +lemma defl_apply_thms:
    1.63 +  "foo_defl\<cdot>a = fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))"
    1.64 +  "bar_defl\<cdot>a = fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
    1.65 +  "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
    1.66 +unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
    1.67 +
    1.68 +text {* Unfold rules for each combinator. *}
    1.69 +
    1.70 +lemma foo_defl_unfold:
    1.71 +  "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
    1.72 +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    1.73 +
    1.74 +lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
    1.75 +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    1.76 +
    1.77 +lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(foo_defl\<cdot>a)))\<cdot>DEFL(tr))"
    1.78 +unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
    1.79 +
    1.80 +text "The automation for the previous steps will be quite similar to
    1.81 +how the fixrec package works."
    1.82 +
    1.83 +(********************************************************************)
    1.84 +
    1.85 +subsection {* Step 2: Define types, prove class instances *}
    1.86 +
    1.87 +text {* Use @{text pcpodef} with the appropriate type combinator. *}
    1.88 +
    1.89 +pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
    1.90 +by (rule defl_set_bottom, rule adm_defl_set)
    1.91 +
    1.92 +pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
    1.93 +by (rule defl_set_bottom, rule adm_defl_set)
    1.94 +
    1.95 +pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"
    1.96 +by (rule defl_set_bottom, rule adm_defl_set)
    1.97 +
    1.98 +text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
    1.99 +
   1.100 +instantiation foo :: ("domain") liftdomain
   1.101 +begin
   1.102 +
   1.103 +definition emb_foo :: "'a foo \<rightarrow> udom"
   1.104 +where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
   1.105 +
   1.106 +definition prj_foo :: "udom \<rightarrow> 'a foo"
   1.107 +where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
   1.108 +
   1.109 +definition defl_foo :: "'a foo itself \<Rightarrow> defl"
   1.110 +where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
   1.111 +
   1.112 +definition
   1.113 +  "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
   1.114 +
   1.115 +definition
   1.116 +  "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
   1.117 +
   1.118 +definition
   1.119 +  "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
   1.120 +
   1.121 +instance
   1.122 +apply (rule typedef_liftdomain_class)
   1.123 +apply (rule type_definition_foo)
   1.124 +apply (rule below_foo_def)
   1.125 +apply (rule emb_foo_def)
   1.126 +apply (rule prj_foo_def)
   1.127 +apply (rule defl_foo_def)
   1.128 +apply (rule liftemb_foo_def)
   1.129 +apply (rule liftprj_foo_def)
   1.130 +apply (rule liftdefl_foo_def)
   1.131 +done
   1.132 +
   1.133 +end
   1.134 +
   1.135 +instantiation bar :: ("domain") liftdomain
   1.136 +begin
   1.137 +
   1.138 +definition emb_bar :: "'a bar \<rightarrow> udom"
   1.139 +where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
   1.140 +
   1.141 +definition prj_bar :: "udom \<rightarrow> 'a bar"
   1.142 +where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
   1.143 +
   1.144 +definition defl_bar :: "'a bar itself \<Rightarrow> defl"
   1.145 +where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
   1.146 +
   1.147 +definition
   1.148 +  "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
   1.149 +
   1.150 +definition
   1.151 +  "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
   1.152 +
   1.153 +definition
   1.154 +  "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
   1.155 +
   1.156 +instance
   1.157 +apply (rule typedef_liftdomain_class)
   1.158 +apply (rule type_definition_bar)
   1.159 +apply (rule below_bar_def)
   1.160 +apply (rule emb_bar_def)
   1.161 +apply (rule prj_bar_def)
   1.162 +apply (rule defl_bar_def)
   1.163 +apply (rule liftemb_bar_def)
   1.164 +apply (rule liftprj_bar_def)
   1.165 +apply (rule liftdefl_bar_def)
   1.166 +done
   1.167 +
   1.168 +end
   1.169 +
   1.170 +instantiation baz :: ("domain") liftdomain
   1.171 +begin
   1.172 +
   1.173 +definition emb_baz :: "'a baz \<rightarrow> udom"
   1.174 +where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
   1.175 +
   1.176 +definition prj_baz :: "udom \<rightarrow> 'a baz"
   1.177 +where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>LIFTDEFL('a))\<cdot>y))"
   1.178 +
   1.179 +definition defl_baz :: "'a baz itself \<Rightarrow> defl"
   1.180 +where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
   1.181 +
   1.182 +definition
   1.183 +  "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
   1.184 +
   1.185 +definition
   1.186 +  "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
   1.187 +
   1.188 +definition
   1.189 +  "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
   1.190 +
   1.191 +instance
   1.192 +apply (rule typedef_liftdomain_class)
   1.193 +apply (rule type_definition_baz)
   1.194 +apply (rule below_baz_def)
   1.195 +apply (rule emb_baz_def)
   1.196 +apply (rule prj_baz_def)
   1.197 +apply (rule defl_baz_def)
   1.198 +apply (rule liftemb_baz_def)
   1.199 +apply (rule liftprj_baz_def)
   1.200 +apply (rule liftdefl_baz_def)
   1.201 +done
   1.202 +
   1.203 +end
   1.204 +
   1.205 +text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
   1.206 +
   1.207 +lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
   1.208 +apply (rule typedef_DEFL)
   1.209 +apply (rule defl_foo_def)
   1.210 +done
   1.211 +
   1.212 +lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
   1.213 +apply (rule typedef_DEFL)
   1.214 +apply (rule defl_bar_def)
   1.215 +done
   1.216 +
   1.217 +lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
   1.218 +apply (rule typedef_DEFL)
   1.219 +apply (rule defl_baz_def)
   1.220 +done
   1.221 +
   1.222 +text {* Prove DEFL equations using type combinator unfold lemmas. *}
   1.223 +
   1.224 +lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
   1.225 +unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
   1.226 +by (rule foo_defl_unfold)
   1.227 +
   1.228 +lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
   1.229 +unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
   1.230 +by (rule bar_defl_unfold)
   1.231 +
   1.232 +lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
   1.233 +unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
   1.234 +by (rule baz_defl_unfold)
   1.235 +
   1.236 +(********************************************************************)
   1.237 +
   1.238 +subsection {* Step 3: Define rep and abs functions *}
   1.239 +
   1.240 +text {* Define them all using @{text prj} and @{text emb}! *}
   1.241 +
   1.242 +definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
   1.243 +where "foo_rep \<equiv> prj oo emb"
   1.244 +
   1.245 +definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
   1.246 +where "foo_abs \<equiv> prj oo emb"
   1.247 +
   1.248 +definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
   1.249 +where "bar_rep \<equiv> prj oo emb"
   1.250 +
   1.251 +definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
   1.252 +where "bar_abs \<equiv> prj oo emb"
   1.253 +
   1.254 +definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
   1.255 +where "baz_rep \<equiv> prj oo emb"
   1.256 +
   1.257 +definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
   1.258 +where "baz_abs \<equiv> prj oo emb"
   1.259 +
   1.260 +text {* Prove isomorphism rules. *}
   1.261 +
   1.262 +lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
   1.263 +by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
   1.264 +
   1.265 +lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
   1.266 +by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
   1.267 +
   1.268 +lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
   1.269 +by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
   1.270 +
   1.271 +lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
   1.272 +by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
   1.273 +
   1.274 +lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
   1.275 +by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
   1.276 +
   1.277 +lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
   1.278 +by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
   1.279 +
   1.280 +text {* Prove isodefl rules using @{text isodefl_coerce}. *}
   1.281 +
   1.282 +lemma isodefl_foo_abs:
   1.283 +  "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
   1.284 +by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
   1.285 +
   1.286 +lemma isodefl_bar_abs:
   1.287 +  "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
   1.288 +by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
   1.289 +
   1.290 +lemma isodefl_baz_abs:
   1.291 +  "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
   1.292 +by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
   1.293 +
   1.294 +(********************************************************************)
   1.295 +
   1.296 +subsection {* Step 4: Define map functions, prove isodefl property *}
   1.297 +
   1.298 +text {* Start with the one-step non-recursive version. *}
   1.299 +
   1.300 +text {* Note that the type of the map function depends on which
   1.301 +variables are used in positive and negative positions. *}
   1.302 +
   1.303 +definition
   1.304 +  foo_bar_baz_mapF ::
   1.305 +    "('a \<rightarrow> 'b) \<rightarrow>
   1.306 +     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
   1.307 +     ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
   1.308 +where
   1.309 +  "foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3).
   1.310 +    (
   1.311 +      foo_abs oo
   1.312 +        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
   1.313 +          oo foo_rep
   1.314 +    ,
   1.315 +      bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
   1.316 +    ,
   1.317 +      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
   1.318 +    )))"
   1.319 +
   1.320 +lemma foo_bar_baz_mapF_beta:
   1.321 +  "foo_bar_baz_mapF\<cdot>f\<cdot>d =
   1.322 +    (
   1.323 +      foo_abs oo
   1.324 +        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
   1.325 +          oo foo_rep
   1.326 +    ,
   1.327 +      bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
   1.328 +    ,
   1.329 +      baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
   1.330 +    )"
   1.331 +unfolding foo_bar_baz_mapF_def
   1.332 +by (simp add: split_def)
   1.333 +
   1.334 +text {* Individual map functions are projected from the fixed point. *}
   1.335 +
   1.336 +definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
   1.337 +where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
   1.338 +
   1.339 +definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
   1.340 +where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
   1.341 +
   1.342 +definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
   1.343 +where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
   1.344 +
   1.345 +lemma map_apply_thms:
   1.346 +  "foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))"
   1.347 +  "bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
   1.348 +  "baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
   1.349 +unfolding foo_map_def bar_map_def baz_map_def by simp_all
   1.350 +
   1.351 +text {* Prove isodefl rules for all map functions simultaneously. *}
   1.352 +
   1.353 +lemma isodefl_foo_bar_baz:
   1.354 +  assumes isodefl_d: "isodefl (u_map\<cdot>d) t"
   1.355 +  shows
   1.356 +  "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
   1.357 +  isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
   1.358 +  isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
   1.359 +unfolding map_apply_thms defl_apply_thms
   1.360 + apply (rule parallel_fix_ind)
   1.361 +   apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
   1.362 +  apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
   1.363 + apply (simp only: foo_bar_baz_mapF_beta
   1.364 +                   foo_bar_baz_deflF_beta
   1.365 +                   fst_conv snd_conv)
   1.366 + apply (elim conjE)
   1.367 + apply (intro
   1.368 +  conjI
   1.369 +  isodefl_foo_abs
   1.370 +  isodefl_bar_abs
   1.371 +  isodefl_baz_abs
   1.372 +  domain_isodefl
   1.373 +  isodefl_ID_DEFL isodefl_LIFTDEFL
   1.374 +  isodefl_d
   1.375 + )
   1.376 + apply assumption+
   1.377 +done
   1.378 +
   1.379 +lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
   1.380 +lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
   1.381 +lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
   1.382 +
   1.383 +text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
   1.384 +
   1.385 +lemma foo_map_ID: "foo_map\<cdot>ID = ID"
   1.386 +apply (rule isodefl_DEFL_imp_ID)
   1.387 +apply (subst DEFL_foo)
   1.388 +apply (rule isodefl_foo)
   1.389 +apply (rule isodefl_LIFTDEFL)
   1.390 +done
   1.391 +
   1.392 +lemma bar_map_ID: "bar_map\<cdot>ID = ID"
   1.393 +apply (rule isodefl_DEFL_imp_ID)
   1.394 +apply (subst DEFL_bar)
   1.395 +apply (rule isodefl_bar)
   1.396 +apply (rule isodefl_LIFTDEFL)
   1.397 +done
   1.398 +
   1.399 +lemma baz_map_ID: "baz_map\<cdot>ID = ID"
   1.400 +apply (rule isodefl_DEFL_imp_ID)
   1.401 +apply (subst DEFL_baz)
   1.402 +apply (rule isodefl_baz)
   1.403 +apply (rule isodefl_LIFTDEFL)
   1.404 +done
   1.405 +
   1.406 +(********************************************************************)
   1.407 +
   1.408 +subsection {* Step 5: Define take functions, prove lub-take lemmas *}
   1.409 +
   1.410 +definition
   1.411 +  foo_bar_baz_takeF ::
   1.412 +    "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
   1.413 +     ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
   1.414 +where
   1.415 +  "foo_bar_baz_takeF = (\<Lambda> p.
   1.416 +    ( foo_abs oo
   1.417 +        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
   1.418 +          oo foo_rep
   1.419 +    , bar_abs oo
   1.420 +        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
   1.421 +    , baz_abs oo
   1.422 +        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
   1.423 +    ))"
   1.424 +
   1.425 +lemma foo_bar_baz_takeF_beta:
   1.426 +  "foo_bar_baz_takeF\<cdot>p =
   1.427 +    ( foo_abs oo
   1.428 +        ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
   1.429 +          oo foo_rep
   1.430 +    , bar_abs oo
   1.431 +        u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
   1.432 +    , baz_abs oo
   1.433 +        u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
   1.434 +    )"
   1.435 +unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp)
   1.436 +
   1.437 +definition
   1.438 +  foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
   1.439 +where
   1.440 +  "foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))"
   1.441 +
   1.442 +definition
   1.443 +  bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
   1.444 +where
   1.445 +  "bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
   1.446 +
   1.447 +definition
   1.448 +  baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
   1.449 +where
   1.450 +  "baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
   1.451 +
   1.452 +lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take"
   1.453 +unfolding foo_take_def bar_take_def baz_take_def
   1.454 +by (intro ch2ch_fst ch2ch_snd chain_iterate)+
   1.455 +
   1.456 +lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>"
   1.457 +unfolding foo_take_def bar_take_def baz_take_def
   1.458 +by (simp only: iterate_0 fst_strict snd_strict)+
   1.459 +
   1.460 +lemma take_Suc_thms:
   1.461 +  "foo_take (Suc n) =
   1.462 +    foo_abs oo ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(bar_take n))) oo foo_rep"
   1.463 +  "bar_take (Suc n) =
   1.464 +    bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep"
   1.465 +  "baz_take (Suc n) =
   1.466 +    baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep"
   1.467 +unfolding foo_take_def bar_take_def baz_take_def
   1.468 +by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+
   1.469 +
   1.470 +lemma lub_take_lemma:
   1.471 +  "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
   1.472 +    = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
   1.473 +apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
   1.474 +apply (simp only: map_apply_thms pair_collapse)
   1.475 +apply (simp only: fix_def2)
   1.476 +apply (rule lub_eq)
   1.477 +apply (rule nat.induct)
   1.478 +apply (simp only: iterate_0 Pair_strict take_0_thms)
   1.479 +apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
   1.480 +                  foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
   1.481 +done
   1.482 +
   1.483 +lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
   1.484 +apply (rule trans [OF _ foo_map_ID])
   1.485 +using lub_take_lemma
   1.486 +apply (elim Pair_inject)
   1.487 +apply assumption
   1.488 +done
   1.489 +
   1.490 +lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID"
   1.491 +apply (rule trans [OF _ bar_map_ID])
   1.492 +using lub_take_lemma
   1.493 +apply (elim Pair_inject)
   1.494 +apply assumption
   1.495 +done
   1.496 +
   1.497 +lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID"
   1.498 +apply (rule trans [OF _ baz_map_ID])
   1.499 +using lub_take_lemma
   1.500 +apply (elim Pair_inject)
   1.501 +apply assumption
   1.502 +done
   1.503 +
   1.504 +end