1.1 --- a/src/HOLCF/ex/Domain_Proofs.thy Sat Nov 27 14:34:54 2010 -0800
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,501 +0,0 @@
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