src/HOL/HOLCF/ex/Domain_Proofs.thy
 changeset 41292 2b7bc8d9fd6e parent 41290 e9c9577d88b5 child 41436 480978f80eae
equal inserted replaced
41291:752d81c2ce25 41292:2b7bc8d9fd6e
`    15 `
`    15 `
`    16 domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")`
`    16 domain 'a foo = Foo1 | Foo2 (lazy 'a) (lazy "'a bar")`
`    17    and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")`
`    17    and 'a bar = Bar (lazy "'a baz \<rightarrow> tr")`
`    18    and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")`
`    18    and 'a baz = Baz (lazy "'a foo convex_pd \<rightarrow> tr")`
`    19 `
`    19 `
`    23 *)`
`    20 *)`
`    24 `
`    21 `
`    25 (********************************************************************)`
`    22 (********************************************************************)`
`    26 `
`    23 `
`    27 subsection {* Step 1: Define the new type combinators *}`
`    24 subsection {* Step 1: Define the new type combinators *}`
`    31 definition`
`    28 definition`
`    32   foo_bar_baz_deflF ::`
`    29   foo_bar_baz_deflF ::`
`    33     "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"`
`    30     "udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl \<rightarrow> udom defl \<times> udom defl \<times> udom defl"`
`    34 where`
`    31 where`
`    35   "foo_bar_baz_deflF = (\<Lambda> a. Abs_cfun (\<lambda>(t1, t2, t3). `
`    32   "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))`
`    33     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>t2)))`
`    37     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>t3)\<cdot>DEFL(tr))`
`    34     , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>t3))\<cdot>DEFL(tr)))`
`    38     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(convex_defl\<cdot>t1))\<cdot>DEFL(tr)))))"`
`    35     , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>t1)))\<cdot>DEFL(tr))))))"`
`    39 `
`    36 `
`    40 lemma foo_bar_baz_deflF_beta:`
`    37 lemma foo_bar_baz_deflF_beta:`
`    41   "foo_bar_baz_deflF\<cdot>a\<cdot>t =`
`    38   "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))))`
`    39     ( ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(fst (snd t)))))`
`    43     , u_defl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(snd (snd t)))\<cdot>DEFL(tr))`
`    40     , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<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)))"`
`    41     , u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(convex_defl\<cdot>(fst t))))\<cdot>DEFL(tr))))"`
`    45 unfolding foo_bar_baz_deflF_def`
`    42 unfolding foo_bar_baz_deflF_def`
`    46 by (simp add: split_def)`
`    43 by (simp add: split_def)`
`    47 `
`    44 `
`    48 text {* Individual type combinators are projected from the fixed point. *}`
`    45 text {* Individual type combinators are projected from the fixed point. *}`
`    49 `
`    46 `
`    63 unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all`
`    60 unfolding foo_defl_def bar_defl_def baz_defl_def by simp_all`
`    64 `
`    61 `
`    65 text {* Unfold rules for each combinator. *}`
`    62 text {* Unfold rules for each combinator. *}`
`    66 `
`    63 `
`    67 lemma foo_defl_unfold:`
`    64 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)))"`
`    65   "foo_defl\<cdot>a = ssum_defl\<cdot>DEFL(one)\<cdot>(sprod_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>a))\<cdot>(u_defl\<cdot>(pdefl\<cdot>(bar_defl\<cdot>a))))"`
`    69 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)`
`    66 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)`
`    70 `
`    67 `
`    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))"`
`    68 lemma bar_defl_unfold: "bar_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<cdot>(baz_defl\<cdot>a)))\<cdot>DEFL(tr)))"`
`    72 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)`
`    69 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)`
`    73 `
`    70 `
`    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))"`
`    71 lemma baz_defl_unfold: "baz_defl\<cdot>a = u_defl\<cdot>(pdefl\<cdot>(sfun_defl\<cdot>(u_defl\<cdot>(pdefl\<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)`
`    72 unfolding defl_apply_thms by (subst fix_eq, simp add: foo_bar_baz_deflF_beta)`
`    76 `
`    73 `
`    77 text "The automation for the previous steps will be quite similar to`
`    74 text "The automation for the previous steps will be quite similar to`
`    78 how the fixrec package works."`
`    75 how the fixrec package works."`
`    79 `
`    76 `
`    81 `
`    78 `
`    82 subsection {* Step 2: Define types, prove class instances *}`
`    79 subsection {* Step 2: Define types, prove class instances *}`
`    83 `
`    80 `
`    84 text {* Use @{text pcpodef} with the appropriate type combinator. *}`
`    81 text {* Use @{text pcpodef} with the appropriate type combinator. *}`
`    85 `
`    82 `
`    86 pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>LIFTDEFL('a))"`
`    83 pcpodef (open) 'a foo = "defl_set (foo_defl\<cdot>DEFL('a))"`
`    87 by (rule defl_set_bottom, rule adm_defl_set)`
`    84 by (rule defl_set_bottom, rule adm_defl_set)`
`    88 `
`    85 `
`    89 pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>LIFTDEFL('a))"`
`    86 pcpodef (open) 'a bar = "defl_set (bar_defl\<cdot>DEFL('a))"`
`    90 by (rule defl_set_bottom, rule adm_defl_set)`
`    87 by (rule defl_set_bottom, rule adm_defl_set)`
`    91 `
`    88 `
`    92 pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>LIFTDEFL('a))"`
`    89 pcpodef (open) 'a baz = "defl_set (baz_defl\<cdot>DEFL('a))"`
`    93 by (rule defl_set_bottom, rule adm_defl_set)`
`    90 by (rule defl_set_bottom, rule adm_defl_set)`
`    94 `
`    91 `
`    95 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}`
`    92 text {* Prove rep instance using lemma @{text typedef_rep_class}. *}`
`    96 `
`    93 `
`    97 instantiation foo :: ("domain") liftdomain`
`    94 instantiation foo :: ("domain") "domain"`
`    98 begin`
`    95 begin`
`    99 `
`    96 `
`   100 definition emb_foo :: "'a foo \<rightarrow> udom"`
`    97 definition emb_foo :: "'a foo \<rightarrow> udom"`
`   101 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"`
`    98 where "emb_foo \<equiv> (\<Lambda> x. Rep_foo x)"`
`   102 `
`    99 `
`   103 definition prj_foo :: "udom \<rightarrow> 'a foo"`
`   100 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))"`
`   101 where "prj_foo \<equiv> (\<Lambda> y. Abs_foo (cast\<cdot>(foo_defl\<cdot>DEFL('a))\<cdot>y))"`
`   105 `
`   102 `
`   106 definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"`
`   103 definition defl_foo :: "'a foo itself \<Rightarrow> udom defl"`
`   107 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>LIFTDEFL('a)"`
`   104 where "defl_foo \<equiv> \<lambda>a. foo_defl\<cdot>DEFL('a)"`
`   108 `
`   105 `
`   109 definition`
`   106 definition`
`   110   "(liftemb :: 'a foo u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"`
`   107   "(liftemb :: 'a foo u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"`
`   111 `
`   108 `
`   112 definition`
`   109 definition`
`   113   "(liftprj :: udom \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj oo u_prj"`
`   110   "(liftprj :: udom u \<rightarrow> 'a foo u) \<equiv> u_map\<cdot>prj"`
`   114 `
`   111 `
`   115 definition`
`   112 definition`
`   116   "liftdefl \<equiv> \<lambda>(t::'a foo itself). u_defl\<cdot>DEFL('a foo)"`
`   113   "liftdefl \<equiv> \<lambda>(t::'a foo itself). pdefl\<cdot>DEFL('a foo)"`
`   117 `
`   114 `
`   118 instance`
`   115 instance`
`   119 apply (rule typedef_liftdomain_class)`
`   116 apply (rule typedef_domain_class)`
`   120 apply (rule type_definition_foo)`
`   117 apply (rule type_definition_foo)`
`   121 apply (rule below_foo_def)`
`   118 apply (rule below_foo_def)`
`   122 apply (rule emb_foo_def)`
`   119 apply (rule emb_foo_def)`
`   123 apply (rule prj_foo_def)`
`   120 apply (rule prj_foo_def)`
`   124 apply (rule defl_foo_def)`
`   121 apply (rule defl_foo_def)`
`   127 apply (rule liftdefl_foo_def)`
`   124 apply (rule liftdefl_foo_def)`
`   128 done`
`   125 done`
`   129 `
`   126 `
`   130 end`
`   127 end`
`   131 `
`   128 `
`   132 instantiation bar :: ("domain") liftdomain`
`   129 instantiation bar :: ("domain") "domain"`
`   133 begin`
`   130 begin`
`   134 `
`   131 `
`   135 definition emb_bar :: "'a bar \<rightarrow> udom"`
`   132 definition emb_bar :: "'a bar \<rightarrow> udom"`
`   136 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"`
`   133 where "emb_bar \<equiv> (\<Lambda> x. Rep_bar x)"`
`   137 `
`   134 `
`   138 definition prj_bar :: "udom \<rightarrow> 'a bar"`
`   135 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))"`
`   136 where "prj_bar \<equiv> (\<Lambda> y. Abs_bar (cast\<cdot>(bar_defl\<cdot>DEFL('a))\<cdot>y))"`
`   140 `
`   137 `
`   141 definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"`
`   138 definition defl_bar :: "'a bar itself \<Rightarrow> udom defl"`
`   142 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>LIFTDEFL('a)"`
`   139 where "defl_bar \<equiv> \<lambda>a. bar_defl\<cdot>DEFL('a)"`
`   143 `
`   140 `
`   144 definition`
`   141 definition`
`   145   "(liftemb :: 'a bar u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"`
`   142   "(liftemb :: 'a bar u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"`
`   146 `
`   143 `
`   147 definition`
`   144 definition`
`   148   "(liftprj :: udom \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj oo u_prj"`
`   145   "(liftprj :: udom u \<rightarrow> 'a bar u) \<equiv> u_map\<cdot>prj"`
`   149 `
`   146 `
`   150 definition`
`   147 definition`
`   151   "liftdefl \<equiv> \<lambda>(t::'a bar itself). u_defl\<cdot>DEFL('a bar)"`
`   148   "liftdefl \<equiv> \<lambda>(t::'a bar itself). pdefl\<cdot>DEFL('a bar)"`
`   152 `
`   149 `
`   153 instance`
`   150 instance`
`   154 apply (rule typedef_liftdomain_class)`
`   151 apply (rule typedef_domain_class)`
`   155 apply (rule type_definition_bar)`
`   152 apply (rule type_definition_bar)`
`   156 apply (rule below_bar_def)`
`   153 apply (rule below_bar_def)`
`   157 apply (rule emb_bar_def)`
`   154 apply (rule emb_bar_def)`
`   158 apply (rule prj_bar_def)`
`   155 apply (rule prj_bar_def)`
`   159 apply (rule defl_bar_def)`
`   156 apply (rule defl_bar_def)`
`   162 apply (rule liftdefl_bar_def)`
`   159 apply (rule liftdefl_bar_def)`
`   163 done`
`   160 done`
`   164 `
`   161 `
`   165 end`
`   162 end`
`   166 `
`   163 `
`   167 instantiation baz :: ("domain") liftdomain`
`   164 instantiation baz :: ("domain") "domain"`
`   168 begin`
`   165 begin`
`   169 `
`   166 `
`   170 definition emb_baz :: "'a baz \<rightarrow> udom"`
`   167 definition emb_baz :: "'a baz \<rightarrow> udom"`
`   171 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"`
`   168 where "emb_baz \<equiv> (\<Lambda> x. Rep_baz x)"`
`   172 `
`   169 `
`   173 definition prj_baz :: "udom \<rightarrow> 'a baz"`
`   170 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))"`
`   171 where "prj_baz \<equiv> (\<Lambda> y. Abs_baz (cast\<cdot>(baz_defl\<cdot>DEFL('a))\<cdot>y))"`
`   175 `
`   172 `
`   176 definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"`
`   173 definition defl_baz :: "'a baz itself \<Rightarrow> udom defl"`
`   177 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>LIFTDEFL('a)"`
`   174 where "defl_baz \<equiv> \<lambda>a. baz_defl\<cdot>DEFL('a)"`
`   178 `
`   175 `
`   179 definition`
`   176 definition`
`   180   "(liftemb :: 'a baz u \<rightarrow> udom) \<equiv> u_emb oo u_map\<cdot>emb"`
`   177   "(liftemb :: 'a baz u \<rightarrow> udom u) \<equiv> u_map\<cdot>emb"`
`   181 `
`   178 `
`   182 definition`
`   179 definition`
`   183   "(liftprj :: udom \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj oo u_prj"`
`   180   "(liftprj :: udom u \<rightarrow> 'a baz u) \<equiv> u_map\<cdot>prj"`
`   184 `
`   181 `
`   185 definition`
`   182 definition`
`   186   "liftdefl \<equiv> \<lambda>(t::'a baz itself). u_defl\<cdot>DEFL('a baz)"`
`   183   "liftdefl \<equiv> \<lambda>(t::'a baz itself). pdefl\<cdot>DEFL('a baz)"`
`   187 `
`   184 `
`   188 instance`
`   185 instance`
`   189 apply (rule typedef_liftdomain_class)`
`   186 apply (rule typedef_domain_class)`
`   190 apply (rule type_definition_baz)`
`   187 apply (rule type_definition_baz)`
`   191 apply (rule below_baz_def)`
`   188 apply (rule below_baz_def)`
`   192 apply (rule emb_baz_def)`
`   189 apply (rule emb_baz_def)`
`   193 apply (rule prj_baz_def)`
`   190 apply (rule prj_baz_def)`
`   194 apply (rule defl_baz_def)`
`   191 apply (rule defl_baz_def)`
`   199 `
`   196 `
`   200 end`
`   197 end`
`   201 `
`   198 `
`   202 text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}`
`   199 text {* Prove DEFL rules using lemma @{text typedef_DEFL}. *}`
`   203 `
`   200 `
`   204 lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>LIFTDEFL('a)"`
`   201 lemma DEFL_foo: "DEFL('a foo) = foo_defl\<cdot>DEFL('a)"`
`   205 apply (rule typedef_DEFL)`
`   202 apply (rule typedef_DEFL)`
`   206 apply (rule defl_foo_def)`
`   203 apply (rule defl_foo_def)`
`   207 done`
`   204 done`
`   208 `
`   205 `
`   209 lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>LIFTDEFL('a)"`
`   206 lemma DEFL_bar: "DEFL('a bar) = bar_defl\<cdot>DEFL('a)"`
`   210 apply (rule typedef_DEFL)`
`   207 apply (rule typedef_DEFL)`
`   211 apply (rule defl_bar_def)`
`   208 apply (rule defl_bar_def)`
`   212 done`
`   209 done`
`   213 `
`   210 `
`   214 lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>LIFTDEFL('a)"`
`   211 lemma DEFL_baz: "DEFL('a baz) = baz_defl\<cdot>DEFL('a)"`
`   215 apply (rule typedef_DEFL)`
`   212 apply (rule typedef_DEFL)`
`   216 apply (rule defl_baz_def)`
`   213 apply (rule defl_baz_def)`
`   217 done`
`   214 done`
`   218 `
`   215 `
`   219 text {* Prove DEFL equations using type combinator unfold lemmas. *}`
`   216 text {* Prove DEFL equations using type combinator unfold lemmas. *}`
`   346 unfolding foo_map_def bar_map_def baz_map_def by simp_all`
`   343 unfolding foo_map_def bar_map_def baz_map_def by simp_all`
`   347 `
`   344 `
`   348 text {* Prove isodefl rules for all map functions simultaneously. *}`
`   345 text {* Prove isodefl rules for all map functions simultaneously. *}`
`   349 `
`   346 `
`   350 lemma isodefl_foo_bar_baz:`
`   347 lemma isodefl_foo_bar_baz:`
`   351   assumes isodefl_d: "isodefl (u_map\<cdot>d) t"`
`   348   assumes isodefl_d: "isodefl d t"`
`   352   shows`
`   349   shows`
`   353   "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>`
`   350   "isodefl (foo_map\<cdot>d) (foo_defl\<cdot>t) \<and>`
`   354   isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>`
`   351   isodefl (bar_map\<cdot>d) (bar_defl\<cdot>t) \<and>`
`   355   isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"`
`   352   isodefl (baz_map\<cdot>d) (baz_defl\<cdot>t)"`
`   356 unfolding map_apply_thms defl_apply_thms`
`   353 unfolding map_apply_thms defl_apply_thms`
`   381 `
`   378 `
`   382 lemma foo_map_ID: "foo_map\<cdot>ID = ID"`
`   379 lemma foo_map_ID: "foo_map\<cdot>ID = ID"`
`   383 apply (rule isodefl_DEFL_imp_ID)`
`   380 apply (rule isodefl_DEFL_imp_ID)`
`   384 apply (subst DEFL_foo)`
`   381 apply (subst DEFL_foo)`
`   385 apply (rule isodefl_foo)`
`   382 apply (rule isodefl_foo)`
`   386 apply (rule isodefl_LIFTDEFL)`
`   383 apply (rule isodefl_ID_DEFL)`
`   387 done`
`   384 done`
`   388 `
`   385 `
`   389 lemma bar_map_ID: "bar_map\<cdot>ID = ID"`
`   386 lemma bar_map_ID: "bar_map\<cdot>ID = ID"`
`   390 apply (rule isodefl_DEFL_imp_ID)`
`   387 apply (rule isodefl_DEFL_imp_ID)`
`   391 apply (subst DEFL_bar)`
`   388 apply (subst DEFL_bar)`
`   392 apply (rule isodefl_bar)`
`   389 apply (rule isodefl_bar)`
`   393 apply (rule isodefl_LIFTDEFL)`
`   390 apply (rule isodefl_ID_DEFL)`
`   394 done`
`   391 done`
`   395 `
`   392 `
`   396 lemma baz_map_ID: "baz_map\<cdot>ID = ID"`
`   393 lemma baz_map_ID: "baz_map\<cdot>ID = ID"`
`   397 apply (rule isodefl_DEFL_imp_ID)`
`   394 apply (rule isodefl_DEFL_imp_ID)`
`   398 apply (subst DEFL_baz)`
`   395 apply (subst DEFL_baz)`
`   399 apply (rule isodefl_baz)`
`   396 apply (rule isodefl_baz)`
`   400 apply (rule isodefl_LIFTDEFL)`
`   397 apply (rule isodefl_ID_DEFL)`
`   401 done`
`   398 done`
`   402 `
`   399 `
`   403 (********************************************************************)`
`   400 (********************************************************************)`
`   404 `
`   401 `
`   405 subsection {* Step 5: Define take functions, prove lub-take lemmas *}`
`   402 subsection {* Step 5: Define take functions, prove lub-take lemmas *}`