src/HOL/HOLCF/Cfun.thy
changeset 41430 1aa23e9f2c87
parent 41400 1a7557cc686a
child 41478 18500bd1f47b
equal deleted inserted replaced
41429:cf5f025bc3c7 41430:1aa23e9f2c87
    90 translations
    90 translations
    91   "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
    91   "\<Lambda> _. t" => "CONST Abs_cfun (\<lambda> _. t)"
    92 
    92 
    93 subsection {* Continuous function space is pointed *}
    93 subsection {* Continuous function space is pointed *}
    94 
    94 
    95 lemma UU_cfun: "\<bottom> \<in> cfun"
    95 lemma bottom_cfun: "\<bottom> \<in> cfun"
    96 by (simp add: cfun_def inst_fun_pcpo)
    96 by (simp add: cfun_def inst_fun_pcpo)
    97 
    97 
    98 instance cfun :: (cpo, discrete_cpo) discrete_cpo
    98 instance cfun :: (cpo, discrete_cpo) discrete_cpo
    99 by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
    99 by intro_classes (simp add: below_cfun_def Rep_cfun_inject)
   100 
   100 
   101 instance cfun :: (cpo, pcpo) pcpo
   101 instance cfun :: (cpo, pcpo) pcpo
   102 by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def UU_cfun])
   102 by (rule typedef_pcpo [OF type_definition_cfun below_cfun_def bottom_cfun])
   103 
   103 
   104 lemmas Rep_cfun_strict =
   104 lemmas Rep_cfun_strict =
   105   typedef_Rep_strict [OF type_definition_cfun below_cfun_def UU_cfun]
   105   typedef_Rep_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
   106 
   106 
   107 lemmas Abs_cfun_strict =
   107 lemmas Abs_cfun_strict =
   108   typedef_Abs_strict [OF type_definition_cfun below_cfun_def UU_cfun]
   108   typedef_Abs_strict [OF type_definition_cfun below_cfun_def bottom_cfun]
   109 
   109 
   110 text {* function application is strict in its first argument *}
   110 text {* function application is strict in its first argument *}
   111 
   111 
   112 lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
   112 lemma Rep_cfun_strict1 [simp]: "\<bottom>\<cdot>x = \<bottom>"
   113 by (simp add: Rep_cfun_strict)
   113 by (simp add: Rep_cfun_strict)
   259 lemmas lub_distribs = lub_APP lub_LAM
   259 lemmas lub_distribs = lub_APP lub_LAM
   260 
   260 
   261 text {* strictness *}
   261 text {* strictness *}
   262 
   262 
   263 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
   263 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
   264 apply (rule UU_I)
   264 apply (rule bottomI)
   265 apply (erule subst)
   265 apply (erule subst)
   266 apply (rule minimal [THEN monofun_cfun_arg])
   266 apply (rule minimal [THEN monofun_cfun_arg])
   267 done
   267 done
   268 
   268 
   269 text {* type @{typ "'a -> 'b"} is chain complete *}
   269 text {* type @{typ "'a -> 'b"} is chain complete *}
   362 
   362 
   363 text {* Continuous retractions are strict. *}
   363 text {* Continuous retractions are strict. *}
   364 
   364 
   365 lemma retraction_strict:
   365 lemma retraction_strict:
   366   "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
   366   "\<forall>x. f\<cdot>(g\<cdot>x) = x \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>"
   367 apply (rule UU_I)
   367 apply (rule bottomI)
   368 apply (drule_tac x="\<bottom>" in spec)
   368 apply (drule_tac x="\<bottom>" in spec)
   369 apply (erule subst)
   369 apply (erule subst)
   370 apply (rule monofun_cfun_arg)
   370 apply (rule monofun_cfun_arg)
   371 apply (rule minimal)
   371 apply (rule minimal)
   372 done
   372 done
   404 
   404 
   405 lemma flat_codom:
   405 lemma flat_codom:
   406   "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
   406   "f\<cdot>x = (c::'b::flat) \<Longrightarrow> f\<cdot>\<bottom> = \<bottom> \<or> (\<forall>z. f\<cdot>z = c)"
   407 apply (case_tac "f\<cdot>x = \<bottom>")
   407 apply (case_tac "f\<cdot>x = \<bottom>")
   408 apply (rule disjI1)
   408 apply (rule disjI1)
   409 apply (rule UU_I)
   409 apply (rule bottomI)
   410 apply (erule_tac t="\<bottom>" in subst)
   410 apply (erule_tac t="\<bottom>" in subst)
   411 apply (rule minimal [THEN monofun_cfun_arg])
   411 apply (rule minimal [THEN monofun_cfun_arg])
   412 apply clarify
   412 apply clarify
   413 apply (rule_tac a = "f\<cdot>\<bottom>" in refl [THEN box_equals])
   413 apply (rule_tac a = "f\<cdot>\<bottom>" in refl [THEN box_equals])
   414 apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])
   414 apply (erule minimal [THEN monofun_cfun_arg, THEN flat_eqI])