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