183 apply (cut_tac x=f in Rep_CFun) |
183 apply (cut_tac x=f in Rep_CFun) |
184 apply (simp add: CFun_def) |
184 apply (simp add: CFun_def) |
185 done |
185 done |
186 |
186 |
187 lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono] |
187 lemmas monofun_Rep_CFun = cont_Rep_CFun [THEN cont2mono] |
188 lemmas contlub_Rep_CFun = cont_Rep_CFun [THEN cont2contlub] |
|
189 |
188 |
190 lemmas monofun_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2mono, standard] |
189 lemmas monofun_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2mono, standard] |
191 lemmas contlub_Rep_CFun1 = cont_Rep_CFun1 [THEN cont2contlub, standard] |
|
192 lemmas monofun_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2mono, standard] |
190 lemmas monofun_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2mono, standard] |
193 lemmas contlub_Rep_CFun2 = cont_Rep_CFun2 [THEN cont2contlub, standard] |
|
194 |
191 |
195 text {* contlub, cont properties of @{term Rep_CFun} in each argument *} |
192 text {* contlub, cont properties of @{term Rep_CFun} in each argument *} |
196 |
193 |
197 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))" |
194 lemma contlub_cfun_arg: "chain Y \<Longrightarrow> f\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. f\<cdot>(Y i))" |
198 by (rule contlub_Rep_CFun2 [THEN contlubE]) |
195 by (rule cont_Rep_CFun2 [THEN cont2contlubE]) |
199 |
196 |
200 lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)" |
197 lemma cont_cfun_arg: "chain Y \<Longrightarrow> range (\<lambda>i. f\<cdot>(Y i)) <<| f\<cdot>(\<Squnion>i. Y i)" |
201 by (rule cont_Rep_CFun2 [THEN contE]) |
198 by (rule cont_Rep_CFun2 [THEN contE]) |
202 |
199 |
203 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)" |
200 lemma contlub_cfun_fun: "chain F \<Longrightarrow> (\<Squnion>i. F i)\<cdot>x = (\<Squnion>i. F i\<cdot>x)" |
204 by (rule contlub_Rep_CFun1 [THEN contlubE]) |
201 by (rule cont_Rep_CFun1 [THEN cont2contlubE]) |
205 |
202 |
206 lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x" |
203 lemma cont_cfun_fun: "chain F \<Longrightarrow> range (\<lambda>i. F i\<cdot>x) <<| (\<Squnion>i. F i)\<cdot>x" |
207 by (rule cont_Rep_CFun1 [THEN contE]) |
204 by (rule cont_Rep_CFun1 [THEN contE]) |
208 |
205 |
209 text {* monotonicity of application *} |
206 text {* monotonicity of application *} |
528 lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)" |
525 lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)" |
529 apply (rule monofunI) |
526 apply (rule monofunI) |
530 apply (auto simp add: monofun_cfun_arg) |
527 apply (auto simp add: monofun_cfun_arg) |
531 done |
528 done |
532 |
529 |
533 (*FIXME: long proof*) |
530 lemma cont_strictify2: "cont (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)" |
534 lemma contlub_strictify2: "contlub (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)" |
531 apply (rule contI2) |
535 apply (rule contlubI) |
532 apply (rule monofun_strictify2) |
536 apply (case_tac "(\<Squnion>i. Y i) = \<bottom>") |
533 apply (case_tac "(\<Squnion>i. Y i) = \<bottom>", simp) |
537 apply (drule (1) chain_UU_I) |
534 apply (simp add: contlub_cfun_arg del: if_image_distrib) |
538 apply simp |
535 apply (drule chain_UU_I_inverse2, clarify, rename_tac j) |
539 apply (simp del: if_image_distrib) |
536 apply (rule lub_mono2, rule_tac x=j in exI, simp_all) |
540 apply (simp only: contlub_cfun_arg) |
537 apply (auto dest!: chain_mono_less) |
541 apply (rule lub_equal2) |
538 done |
542 apply (rule chain_mono2 [THEN exE]) |
|
543 apply (erule chain_UU_I_inverse2) |
|
544 apply (assumption) |
|
545 apply (rule_tac x=x in exI, clarsimp) |
|
546 apply (erule chain_monofun) |
|
547 apply (erule monofun_strictify2 [THEN ch2ch_monofun]) |
|
548 done |
|
549 |
|
550 lemmas cont_strictify2 = |
|
551 monocontlub2cont [OF monofun_strictify2 contlub_strictify2, standard] |
|
552 |
539 |
553 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)" |
540 lemma strictify_conv_if: "strictify\<cdot>f\<cdot>x = (if x = \<bottom> then \<bottom> else f\<cdot>x)" |
554 unfolding strictify_def |
541 unfolding strictify_def |
555 by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM) |
542 by (simp add: cont_strictify1 cont_strictify2 cont2cont_LAM) |
556 |
543 |