src/HOLCF/Ssum.thy
changeset 25915 f1bce5261dec
parent 25882 c58e380d9f7d
child 26046 1624b3304bb9
equal deleted inserted replaced
25914:ff835e25ae87 25915:f1bce5261dec
    97 by (rule sinr_eq [THEN iffD1])
    97 by (rule sinr_eq [THEN iffD1])
    98 
    98 
    99 text {* Strictness *}
    99 text {* Strictness *}
   100 
   100 
   101 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
   101 lemma sinl_strict [simp]: "sinl\<cdot>\<bottom> = \<bottom>"
   102 by (simp add: sinl_Abs_Ssum Abs_Ssum_strict cpair_strict)
   102 by (simp add: sinl_Abs_Ssum Abs_Ssum_strict)
   103 
   103 
   104 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
   104 lemma sinr_strict [simp]: "sinr\<cdot>\<bottom> = \<bottom>"
   105 by (simp add: sinr_Abs_Ssum Abs_Ssum_strict cpair_strict)
   105 by (simp add: sinr_Abs_Ssum Abs_Ssum_strict)
   106 
   106 
   107 lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
   107 lemma sinl_defined_iff [simp]: "(sinl\<cdot>x = \<bottom>) = (x = \<bottom>)"
   108 by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
   108 by (cut_tac sinl_eq [of "x" "\<bottom>"], simp)
   109 
   109 
   110 lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
   110 lemma sinr_defined_iff [simp]: "(sinr\<cdot>x = \<bottom>) = (x = \<bottom>)"
   212 apply (rule_tac p=x in ssumE, simp)
   212 apply (rule_tac p=x in ssumE, simp)
   213 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
   213 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
   214 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
   214 apply (rule_tac p=y in ssumE, simp_all add: flat_less_iff)
   215 done
   215 done
   216 
   216 
       
   217 subsection {* Strict sum is a bifinite domain *}
       
   218 
       
   219 instance "++" :: (bifinite, bifinite) approx ..
       
   220 
       
   221 defs (overloaded)
       
   222   approx_ssum_def:
       
   223     "approx \<equiv> \<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y))"
       
   224 
       
   225 lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
       
   226 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
       
   227 
       
   228 lemma approx_sinr [simp]: "approx i\<cdot>(sinr\<cdot>x) = sinr\<cdot>(approx i\<cdot>x)"
       
   229 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
       
   230 
       
   231 instance "++" :: (bifinite, bifinite) bifinite
       
   232 proof
       
   233   fix i :: nat and x :: "'a \<oplus> 'b"
       
   234   show "chain (\<lambda>i. approx i\<cdot>x)"
       
   235     unfolding approx_ssum_def by simp
       
   236   show "(\<Squnion>i. approx i\<cdot>x) = x"
       
   237     unfolding approx_ssum_def
       
   238     by (simp add: lub_distribs eta_cfun)
       
   239   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
       
   240     by (cases x, simp add: approx_ssum_def, simp, simp)
       
   241   have "{x::'a \<oplus> 'b. approx i\<cdot>x = x} \<subseteq>
       
   242         (\<lambda>x. sinl\<cdot>x) ` {x. approx i\<cdot>x = x} \<union>
       
   243         (\<lambda>x. sinr\<cdot>x) ` {x. approx i\<cdot>x = x}"
       
   244     by (rule subsetI, rule_tac p=x in ssumE2, simp, simp)
       
   245   thus "finite {x::'a \<oplus> 'b. approx i\<cdot>x = x}"
       
   246     by (rule finite_subset,
       
   247         intro finite_UnI finite_imageI finite_fixes_approx)
       
   248 qed
       
   249 
   217 end
   250 end