src/HOL/HOLCF/ex/Domain_Proofs.thy
changeset 40774 0437dbc127b3
parent 40771 1c6f7d4b110e
child 41287 029a6fc1bfb8
equal deleted inserted replaced
40773:6c12f5e24e34 40774:0437dbc127b3
       
     1 (*  Title:      HOLCF/ex/Domain_Proofs.thy
       
     2     Author:     Brian Huffman
       
     3 *)
       
     4 
       
     5 header {* Internal domain package proofs done manually *}
       
     6 
       
     7 theory Domain_Proofs
       
     8 imports HOLCF
       
     9 begin
       
    10 
       
    11 (*
       
    12 
       
    13 The definitions and proofs below are for the following recursive
       
    14 datatypes:
       
    15 
       
    16 domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")
       
    17    and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")
       
    18    and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")
       
    19 
       
    20 TODO: add another type parameter that is strict,
       
    21 to show the different handling of LIFTDEFL vs. DEFL.
       
    22 
       
    23 *)
       
    24 
       
    25 (********************************************************************)
       
    26 
       
    27 subsection {* Step 1: Define the new type combinators *}
       
    28 
       
    29 text {* Start with the one-step non-recursive version *}
       
    30 
       
    31 definition
       
    32   foo_bar_baz_deflF ::
       
    33     "defl \<rightarrow> defl \<times> defl \<times> defl \<rightarrow> defl \<times> defl \<times> defl"
       
    34 where
       
    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))
       
    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)))))"
       
    39 
       
    40 lemma foo_bar_baz_deflF_beta:
       
    41   "foo_bar_baz_deflF\<cdot>a\<cdot>t =
       
    42     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(fst (snd t))))
       
    43     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))
       
    44     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>(fst t)))\<cdot>DEFL(tr)))"
       
    45 unfolding foo_bar_baz_deflF_def
       
    46 by (simp add: split_def)
       
    47 
       
    48 text {* Individual type combinators are projected from the fixed point. *}
       
    49 
       
    50 definition foo_defl :: "defl \<rightarrow> defl"
       
    51 where "foo_defl = (\<Lambda> a. fst (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
       
    52 
       
    53 definition bar_defl :: "defl \<rightarrow> defl"
       
    54 where "bar_defl = (\<Lambda> a. fst (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
       
    55 
       
    56 definition baz_defl :: "defl \<rightarrow> defl"
       
    57 where "baz_defl = (\<Lambda> a. snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a))))"
       
    58 
       
    59 lemma defl_apply_thms:
       
    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)))"
       
    62   "baz_defl\<cdot>a = snd (snd (fix\<cdot>(foo_bar_baz_deflF\<cdot>a)))"
       
    63 unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all
       
    64 
       
    65 text {* Unfold rules for each combinator. *}
       
    66 
       
    67 lemma foo_defl_unfold:
       
    68   "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>a\<cdot>(u_defl\<cdot>(bar_defl\<cdot>a)))"
       
    69 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
       
    70 
       
    71 lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(baz_defl\<cdot>a))\<cdot>DEFL(tr))"
       
    72 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
       
    73 
       
    74 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))"
       
    75 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)
       
    76 
       
    77 text "The automation for the previous steps will be quite similar to
       
    78 how the fixrec package works."
       
    79 
       
    80 (********************************************************************)
       
    81 
       
    82 subsection {* Step 2: Define types, prove class instances *}
       
    83 
       
    84 text {* Use @{text pcpodef} with the appropriate type combinator. *}
       
    85 
       
    86 pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"
       
    87 by (rule defl_set_bottom, rule adm_defl_set)
       
    88 
       
    89 pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"
       
    90 by (rule defl_set_bottom, rule adm_defl_set)
       
    91 
       
    92 pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"
       
    93 by (rule defl_set_bottom, rule adm_defl_set)
       
    94 
       
    95 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
       
    96 
       
    97 instantiation foo :: ("domain") liftdomain
       
    98 begin
       
    99 
       
   100 definition emb_foo :: "'a foo \<rightarrow> udom"
       
   101 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"
       
   102 
       
   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))"
       
   105 
       
   106 definition defl_foo :: "'a foo itself \<Rightarrow> defl"
       
   107 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"
       
   108 
       
   109 definition
       
   110   "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
       
   111 
       
   112 definition
       
   113   "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
       
   114 
       
   115 definition
       
   116   "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"
       
   117 
       
   118 instance
       
   119 apply (rule typedef_liftdomain_class)
       
   120 apply (rule type_definition_foo)
       
   121 apply (rule below_foo_def)
       
   122 apply (rule emb_foo_def)
       
   123 apply (rule prj_foo_def)
       
   124 apply (rule defl_foo_def)
       
   125 apply (rule liftemb_foo_def)
       
   126 apply (rule liftprj_foo_def)
       
   127 apply (rule liftdefl_foo_def)
       
   128 done
       
   129 
       
   130 end
       
   131 
       
   132 instantiation bar :: ("domain") liftdomain
       
   133 begin
       
   134 
       
   135 definition emb_bar :: "'a bar \<rightarrow> udom"
       
   136 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"
       
   137 
       
   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))"
       
   140 
       
   141 definition defl_bar :: "'a bar itself \<Rightarrow> defl"
       
   142 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"
       
   143 
       
   144 definition
       
   145   "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
       
   146 
       
   147 definition
       
   148   "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
       
   149 
       
   150 definition
       
   151   "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"
       
   152 
       
   153 instance
       
   154 apply (rule typedef_liftdomain_class)
       
   155 apply (rule type_definition_bar)
       
   156 apply (rule below_bar_def)
       
   157 apply (rule emb_bar_def)
       
   158 apply (rule prj_bar_def)
       
   159 apply (rule defl_bar_def)
       
   160 apply (rule liftemb_bar_def)
       
   161 apply (rule liftprj_bar_def)
       
   162 apply (rule liftdefl_bar_def)
       
   163 done
       
   164 
       
   165 end
       
   166 
       
   167 instantiation baz :: ("domain") liftdomain
       
   168 begin
       
   169 
       
   170 definition emb_baz :: "'a baz \<rightarrow> udom"
       
   171 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"
       
   172 
       
   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))"
       
   175 
       
   176 definition defl_baz :: "'a baz itself \<Rightarrow> defl"
       
   177 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"
       
   178 
       
   179 definition
       
   180   "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> udom_emb u_approx oo u_map\<cdot>emb"
       
   181 
       
   182 definition
       
   183   "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo udom_prj u_approx"
       
   184 
       
   185 definition
       
   186   "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"
       
   187 
       
   188 instance
       
   189 apply (rule typedef_liftdomain_class)
       
   190 apply (rule type_definition_baz)
       
   191 apply (rule below_baz_def)
       
   192 apply (rule emb_baz_def)
       
   193 apply (rule prj_baz_def)
       
   194 apply (rule defl_baz_def)
       
   195 apply (rule liftemb_baz_def)
       
   196 apply (rule liftprj_baz_def)
       
   197 apply (rule liftdefl_baz_def)
       
   198 done
       
   199 
       
   200 end
       
   201 
       
   202 text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}
       
   203 
       
   204 lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"
       
   205 apply (rule typedef_DEFL)
       
   206 apply (rule defl_foo_def)
       
   207 done
       
   208 
       
   209 lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"
       
   210 apply (rule typedef_DEFL)
       
   211 apply (rule defl_bar_def)
       
   212 done
       
   213 
       
   214 lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"
       
   215 apply (rule typedef_DEFL)
       
   216 apply (rule defl_baz_def)
       
   217 done
       
   218 
       
   219 text {* Prove DEFL equations using type combinator unfold lemmas. *}
       
   220 
       
   221 lemma DEFL_foo': "DEFL('a foo) = DEFL(one \<oplus> 'a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
       
   222 unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
       
   223 by (rule foo_defl_unfold)
       
   224 
       
   225 lemma DEFL_bar': "DEFL('a bar) = DEFL(('a baz \<rightarrow> tr)\<^sub>\<bottom>)"
       
   226 unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
       
   227 by (rule bar_defl_unfold)
       
   228 
       
   229 lemma DEFL_baz': "DEFL('a baz) = DEFL(('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>)"
       
   230 unfolding DEFL_foo DEFL_bar DEFL_baz domain_defl_simps
       
   231 by (rule baz_defl_unfold)
       
   232 
       
   233 (********************************************************************)
       
   234 
       
   235 subsection {* Step 3: Define rep and abs functions *}
       
   236 
       
   237 text {* Define them all using @{text prj} and @{text emb}! *}
       
   238 
       
   239 definition foo_rep :: "'a foo \<rightarrow> one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>)"
       
   240 where "foo_rep \<equiv> prj oo emb"
       
   241 
       
   242 definition foo_abs :: "one \<oplus> ('a\<^sub>\<bottom> \<otimes> ('a bar)\<^sub>\<bottom>) \<rightarrow> 'a foo"
       
   243 where "foo_abs \<equiv> prj oo emb"
       
   244 
       
   245 definition bar_rep :: "'a bar \<rightarrow> ('a baz \<rightarrow> tr)\<^sub>\<bottom>"
       
   246 where "bar_rep \<equiv> prj oo emb"
       
   247 
       
   248 definition bar_abs :: "('a baz \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a bar"
       
   249 where "bar_abs \<equiv> prj oo emb"
       
   250 
       
   251 definition baz_rep :: "'a baz \<rightarrow> ('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom>"
       
   252 where "baz_rep \<equiv> prj oo emb"
       
   253 
       
   254 definition baz_abs :: "('a foo convex_pd \<rightarrow> tr)\<^sub>\<bottom> \<rightarrow> 'a baz"
       
   255 where "baz_abs \<equiv> prj oo emb"
       
   256 
       
   257 text {* Prove isomorphism rules. *}
       
   258 
       
   259 lemma foo_abs_iso: "foo_rep\<cdot>(foo_abs\<cdot>x) = x"
       
   260 by (rule domain_abs_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
       
   261 
       
   262 lemma foo_rep_iso: "foo_abs\<cdot>(foo_rep\<cdot>x) = x"
       
   263 by (rule domain_rep_iso [OF DEFL_foo' foo_abs_def foo_rep_def])
       
   264 
       
   265 lemma bar_abs_iso: "bar_rep\<cdot>(bar_abs\<cdot>x) = x"
       
   266 by (rule domain_abs_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
       
   267 
       
   268 lemma bar_rep_iso: "bar_abs\<cdot>(bar_rep\<cdot>x) = x"
       
   269 by (rule domain_rep_iso [OF DEFL_bar' bar_abs_def bar_rep_def])
       
   270 
       
   271 lemma baz_abs_iso: "baz_rep\<cdot>(baz_abs\<cdot>x) = x"
       
   272 by (rule domain_abs_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
       
   273 
       
   274 lemma baz_rep_iso: "baz_abs\<cdot>(baz_rep\<cdot>x) = x"
       
   275 by (rule domain_rep_iso [OF DEFL_baz' baz_abs_def baz_rep_def])
       
   276 
       
   277 text {* Prove isodefl rules using @{text isodefl_coerce}. *}
       
   278 
       
   279 lemma isodefl_foo_abs:
       
   280   "isodefl d t \<Longrightarrow> isodefl (foo_abs oo d oo foo_rep) t"
       
   281 by (rule isodefl_abs_rep [OF DEFL_foo' foo_abs_def foo_rep_def])
       
   282 
       
   283 lemma isodefl_bar_abs:
       
   284   "isodefl d t \<Longrightarrow> isodefl (bar_abs oo d oo bar_rep) t"
       
   285 by (rule isodefl_abs_rep [OF DEFL_bar' bar_abs_def bar_rep_def])
       
   286 
       
   287 lemma isodefl_baz_abs:
       
   288   "isodefl d t \<Longrightarrow> isodefl (baz_abs oo d oo baz_rep) t"
       
   289 by (rule isodefl_abs_rep [OF DEFL_baz' baz_abs_def baz_rep_def])
       
   290 
       
   291 (********************************************************************)
       
   292 
       
   293 subsection {* Step 4: Define map functions, prove isodefl property *}
       
   294 
       
   295 text {* Start with the one-step non-recursive version. *}
       
   296 
       
   297 text {* Note that the type of the map function depends on which
       
   298 variables are used in positive and negative positions. *}
       
   299 
       
   300 definition
       
   301   foo_bar_baz_mapF ::
       
   302     "('a \<rightarrow> 'b) \<rightarrow>
       
   303      ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz) \<rightarrow>
       
   304      ('a foo \<rightarrow> 'b foo) \<times> ('a bar \<rightarrow> 'b bar) \<times> ('b baz \<rightarrow> 'a baz)"
       
   305 where
       
   306   "foo_bar_baz_mapF = (\<Lambda> f. Abs_cfun (\<lambda>(d1, d2, d3).
       
   307     (
       
   308       foo_abs oo
       
   309         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>d2))
       
   310           oo foo_rep
       
   311     ,
       
   312       bar_abs oo u_map\<cdot>(cfun_map\<cdot>d3\<cdot>ID) oo bar_rep
       
   313     ,
       
   314       baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>d1)\<cdot>ID) oo baz_rep
       
   315     )))"
       
   316 
       
   317 lemma foo_bar_baz_mapF_beta:
       
   318   "foo_bar_baz_mapF\<cdot>f\<cdot>d =
       
   319     (
       
   320       foo_abs oo
       
   321         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>f)\<cdot>(u_map\<cdot>(fst (snd d))))
       
   322           oo foo_rep
       
   323     ,
       
   324       bar_abs oo u_map\<cdot>(cfun_map\<cdot>(snd (snd d))\<cdot>ID) oo bar_rep
       
   325     ,
       
   326       baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst d))\<cdot>ID) oo baz_rep
       
   327     )"
       
   328 unfolding foo_bar_baz_mapF_def
       
   329 by (simp add: split_def)
       
   330 
       
   331 text {* Individual map functions are projected from the fixed point. *}
       
   332 
       
   333 definition foo_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a foo \<rightarrow> 'b foo)"
       
   334 where "foo_map = (\<Lambda> f. fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
       
   335 
       
   336 definition bar_map :: "('a \<rightarrow> 'b) \<rightarrow> ('a bar \<rightarrow> 'b bar)"
       
   337 where "bar_map = (\<Lambda> f. fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
       
   338 
       
   339 definition baz_map :: "('a \<rightarrow> 'b) \<rightarrow> ('b baz \<rightarrow> 'a baz)"
       
   340 where "baz_map = (\<Lambda> f. snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))))"
       
   341 
       
   342 lemma map_apply_thms:
       
   343   "foo_map\<cdot>f = fst (fix\<cdot>(foo_bar_baz_mapF\<cdot>f))"
       
   344   "bar_map\<cdot>f = fst (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
       
   345   "baz_map\<cdot>f = snd (snd (fix\<cdot>(foo_bar_baz_mapF\<cdot>f)))"
       
   346 unfolding foo_map_def bar_map_def baz_map_def by simp_all
       
   347 
       
   348 text {* Prove isodefl rules for all map functions simultaneously. *}
       
   349 
       
   350 lemma isodefl_foo_bar_baz:
       
   351   assumes isodefl_d: "isodefl (u_map\<cdot>d) t"
       
   352   shows
       
   353   "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>
       
   354   isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>
       
   355   isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"
       
   356 unfolding map_apply_thms defl_apply_thms
       
   357  apply (rule parallel_fix_ind)
       
   358    apply (intro adm_conj adm_isodefl cont2cont_fst cont2cont_snd cont_id)
       
   359   apply (simp only: fst_strict snd_strict isodefl_bottom simp_thms)
       
   360  apply (simp only: foo_bar_baz_mapF_beta
       
   361                    foo_bar_baz_deflF_beta
       
   362                    fst_conv snd_conv)
       
   363  apply (elim conjE)
       
   364  apply (intro
       
   365   conjI
       
   366   isodefl_foo_abs
       
   367   isodefl_bar_abs
       
   368   isodefl_baz_abs
       
   369   domain_isodefl
       
   370   isodefl_ID_DEFL isodefl_LIFTDEFL
       
   371   isodefl_d
       
   372  )
       
   373  apply assumption+
       
   374 done
       
   375 
       
   376 lemmas isodefl_foo = isodefl_foo_bar_baz [THEN conjunct1]
       
   377 lemmas isodefl_bar = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct1]
       
   378 lemmas isodefl_baz = isodefl_foo_bar_baz [THEN conjunct2, THEN conjunct2]
       
   379 
       
   380 text {* Prove map ID lemmas, using isodefl_DEFL_imp_ID *}
       
   381 
       
   382 lemma foo_map_ID: "foo_map\<cdot>ID = ID"
       
   383 apply (rule isodefl_DEFL_imp_ID)
       
   384 apply (subst DEFL_foo)
       
   385 apply (rule isodefl_foo)
       
   386 apply (rule isodefl_LIFTDEFL)
       
   387 done
       
   388 
       
   389 lemma bar_map_ID: "bar_map\<cdot>ID = ID"
       
   390 apply (rule isodefl_DEFL_imp_ID)
       
   391 apply (subst DEFL_bar)
       
   392 apply (rule isodefl_bar)
       
   393 apply (rule isodefl_LIFTDEFL)
       
   394 done
       
   395 
       
   396 lemma baz_map_ID: "baz_map\<cdot>ID = ID"
       
   397 apply (rule isodefl_DEFL_imp_ID)
       
   398 apply (subst DEFL_baz)
       
   399 apply (rule isodefl_baz)
       
   400 apply (rule isodefl_LIFTDEFL)
       
   401 done
       
   402 
       
   403 (********************************************************************)
       
   404 
       
   405 subsection {* Step 5: Define take functions, prove lub-take lemmas *}
       
   406 
       
   407 definition
       
   408   foo_bar_baz_takeF ::
       
   409     "('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz) \<rightarrow>
       
   410      ('a foo \<rightarrow> 'a foo) \<times> ('a bar \<rightarrow> 'a bar) \<times> ('a baz \<rightarrow> 'a baz)"
       
   411 where
       
   412   "foo_bar_baz_takeF = (\<Lambda> p.
       
   413     ( foo_abs oo
       
   414         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
       
   415           oo foo_rep
       
   416     , bar_abs oo
       
   417         u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
       
   418     , baz_abs oo
       
   419         u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
       
   420     ))"
       
   421 
       
   422 lemma foo_bar_baz_takeF_beta:
       
   423   "foo_bar_baz_takeF\<cdot>p =
       
   424     ( foo_abs oo
       
   425         ssum_map\<cdot>ID\<cdot>(sprod_map\<cdot>(u_map\<cdot>ID)\<cdot>(u_map\<cdot>(fst (snd p))))
       
   426           oo foo_rep
       
   427     , bar_abs oo
       
   428         u_map\<cdot>(cfun_map\<cdot>(snd (snd p))\<cdot>ID) oo bar_rep
       
   429     , baz_abs oo
       
   430         u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(fst p))\<cdot>ID) oo baz_rep
       
   431     )"
       
   432 unfolding foo_bar_baz_takeF_def by (rule beta_cfun, simp)
       
   433 
       
   434 definition
       
   435   foo_take :: "nat \<Rightarrow> 'a foo \<rightarrow> 'a foo"
       
   436 where
       
   437   "foo_take = (\<lambda>n. fst (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>))"
       
   438 
       
   439 definition
       
   440   bar_take :: "nat \<Rightarrow> 'a bar \<rightarrow> 'a bar"
       
   441 where
       
   442   "bar_take = (\<lambda>n. fst (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
       
   443 
       
   444 definition
       
   445   baz_take :: "nat \<Rightarrow> 'a baz \<rightarrow> 'a baz"
       
   446 where
       
   447   "baz_take = (\<lambda>n. snd (snd (iterate n\<cdot>foo_bar_baz_takeF\<cdot>\<bottom>)))"
       
   448 
       
   449 lemma chain_take_thms: "chain foo_take" "chain bar_take" "chain baz_take"
       
   450 unfolding foo_take_def bar_take_def baz_take_def
       
   451 by (intro ch2ch_fst ch2ch_snd chain_iterate)+
       
   452 
       
   453 lemma take_0_thms: "foo_take 0 = \<bottom>" "bar_take 0 = \<bottom>" "baz_take 0 = \<bottom>"
       
   454 unfolding foo_take_def bar_take_def baz_take_def
       
   455 by (simp only: iterate_0 fst_strict snd_strict)+
       
   456 
       
   457 lemma take_Suc_thms:
       
   458   "foo_take (Suc n) =
       
   459     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"
       
   460   "bar_take (Suc n) =
       
   461     bar_abs oo u_map\<cdot>(cfun_map\<cdot>(baz_take n)\<cdot>ID) oo bar_rep"
       
   462   "baz_take (Suc n) =
       
   463     baz_abs oo u_map\<cdot>(cfun_map\<cdot>(convex_map\<cdot>(foo_take n))\<cdot>ID) oo baz_rep"
       
   464 unfolding foo_take_def bar_take_def baz_take_def
       
   465 by (simp only: iterate_Suc foo_bar_baz_takeF_beta fst_conv snd_conv)+
       
   466 
       
   467 lemma lub_take_lemma:
       
   468   "(\<Squnion>n. foo_take n, \<Squnion>n. bar_take n, \<Squnion>n. baz_take n)
       
   469     = (foo_map\<cdot>(ID::'a \<rightarrow> 'a), bar_map\<cdot>(ID::'a \<rightarrow> 'a), baz_map\<cdot>(ID::'a \<rightarrow> 'a))"
       
   470 apply (simp only: lub_Pair [symmetric] ch2ch_Pair chain_take_thms)
       
   471 apply (simp only: map_apply_thms pair_collapse)
       
   472 apply (simp only: fix_def2)
       
   473 apply (rule lub_eq)
       
   474 apply (rule nat.induct)
       
   475 apply (simp only: iterate_0 Pair_strict take_0_thms)
       
   476 apply (simp only: iterate_Suc Pair_fst_snd_eq fst_conv snd_conv
       
   477                   foo_bar_baz_mapF_beta take_Suc_thms simp_thms)
       
   478 done
       
   479 
       
   480 lemma lub_foo_take: "(\<Squnion>n. foo_take n) = ID"
       
   481 apply (rule trans [OF _ foo_map_ID])
       
   482 using lub_take_lemma
       
   483 apply (elim Pair_inject)
       
   484 apply assumption
       
   485 done
       
   486 
       
   487 lemma lub_bar_take: "(\<Squnion>n. bar_take n) = ID"
       
   488 apply (rule trans [OF _ bar_map_ID])
       
   489 using lub_take_lemma
       
   490 apply (elim Pair_inject)
       
   491 apply assumption
       
   492 done
       
   493 
       
   494 lemma lub_baz_take: "(\<Squnion>n. baz_take n) = ID"
       
   495 apply (rule trans [OF _ baz_map_ID])
       
   496 using lub_take_lemma
       
   497 apply (elim Pair_inject)
       
   498 apply assumption
       
   499 done
       
   500 
       
   501 end