src/HOLCF/Sprod.thy
changeset 25914 ff835e25ae87
parent 25881 d80bd899ea95
child 26962 c8b20f615d6c
     1.1 --- a/src/HOLCF/Sprod.thy	Tue Jan 15 02:18:01 2008 +0100
     1.2 +++ b/src/HOLCF/Sprod.thy	Tue Jan 15 02:20:47 2008 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  
     1.5  lemma spair_lemma:
     1.6    "<strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a> \<in> Sprod"
     1.7 -by (simp add: Sprod_def strictify_conv_if cpair_strict)
     1.8 +by (simp add: Sprod_def strictify_conv_if)
     1.9  
    1.10  subsection {* Definitions of constants *}
    1.11  
    1.12 @@ -64,23 +64,23 @@
    1.13  
    1.14  subsection {* Case analysis *}
    1.15  
    1.16 -lemma spair_Abs_Sprod:
    1.17 -  "(:a, b:) = Abs_Sprod <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
    1.18 -apply (unfold spair_def)
    1.19 -apply (simp add: cont_Abs_Sprod spair_lemma)
    1.20 -done
    1.21 +lemma Rep_Sprod_spair:
    1.22 +  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
    1.23 +unfolding spair_def
    1.24 +by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
    1.25 +
    1.26 +lemmas Rep_Sprod_simps =
    1.27 +  Rep_Sprod_inject [symmetric] less_Sprod_def
    1.28 +  Rep_Sprod_strict Rep_Sprod_spair
    1.29  
    1.30  lemma Exh_Sprod2:
    1.31    "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
    1.32 -apply (cases z rule: Abs_Sprod_cases)
    1.33 +apply (insert Rep_Sprod [of z])
    1.34 +apply (simp add: Rep_Sprod_simps eq_cprod)
    1.35  apply (simp add: Sprod_def)
    1.36 -apply (erule disjE)
    1.37 -apply (simp add: Abs_Sprod_strict)
    1.38 -apply (rule disjI2)
    1.39 -apply (rule_tac x="cfst\<cdot>y" in exI)
    1.40 -apply (rule_tac x="csnd\<cdot>y" in exI)
    1.41 -apply (simp add: spair_Abs_Sprod Abs_Sprod_inject spair_lemma)
    1.42 -apply (simp add: surjective_pairing_Cprod2)
    1.43 +apply (erule disjE, simp)
    1.44 +apply (simp add: strictify_conv_if)
    1.45 +apply fast
    1.46  done
    1.47  
    1.48  lemma sprodE [cases type: **]:
    1.49 @@ -94,30 +94,38 @@
    1.50  subsection {* Properties of @{term spair} *}
    1.51  
    1.52  lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
    1.53 -by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)
    1.54 +by (simp add: Rep_Sprod_simps strictify_conv_if)
    1.55  
    1.56  lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
    1.57 -by (simp add: spair_Abs_Sprod strictify_conv_if cpair_strict Abs_Sprod_strict)
    1.58 +by (simp add: Rep_Sprod_simps strictify_conv_if)
    1.59 +
    1.60 +lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
    1.61 +by (simp add: Rep_Sprod_simps strictify_conv_if)
    1.62 +
    1.63 +lemma spair_less_iff:
    1.64 +  "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
    1.65 +by (simp add: Rep_Sprod_simps strictify_conv_if)
    1.66 +
    1.67 +lemma spair_eq_iff:
    1.68 +  "((:a, b:) = (:c, d:)) =
    1.69 +    (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
    1.70 +by (simp add: Rep_Sprod_simps strictify_conv_if)
    1.71  
    1.72  lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
    1.73 -by auto
    1.74 +by simp
    1.75  
    1.76  lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
    1.77 -by (erule contrapos_np, auto)
    1.78 +by simp
    1.79  
    1.80 -lemma spair_defined [simp]:
    1.81 -  "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
    1.82 -by (simp add: spair_Abs_Sprod Abs_Sprod_defined Sprod_def)
    1.83 +lemma spair_defined: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
    1.84 +by simp
    1.85  
    1.86  lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
    1.87 -by (erule contrapos_pp, simp)
    1.88 +by simp
    1.89  
    1.90  lemma spair_eq:
    1.91    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)"
    1.92 -apply (simp add: spair_Abs_Sprod)
    1.93 -apply (simp add: Abs_Sprod_inject [OF _ spair_lemma] Sprod_def)
    1.94 -apply (simp add: strictify_conv_if)
    1.95 -done
    1.96 +by (simp add: spair_eq_iff)
    1.97  
    1.98  lemma spair_inject:
    1.99    "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b"
   1.100 @@ -126,12 +134,6 @@
   1.101  lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
   1.102  by simp
   1.103  
   1.104 -lemma Rep_Sprod_spair:
   1.105 -  "Rep_Sprod (:a, b:) = <strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a>"
   1.106 -apply (unfold spair_def)
   1.107 -apply (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
   1.108 -done
   1.109 -
   1.110  subsection {* Properties of @{term sfst} and @{term ssnd} *}
   1.111  
   1.112  lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
   1.113 @@ -226,4 +228,40 @@
   1.114  apply (simp add: flat_less_iff spair_less)
   1.115  done
   1.116  
   1.117 +subsection {* Strict product is a bifinite domain *}
   1.118 +
   1.119 +instance "**" :: (bifinite, bifinite) approx ..
   1.120 +
   1.121 +defs (overloaded)
   1.122 +  approx_sprod_def:
   1.123 +    "approx \<equiv> \<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:)"
   1.124 +
   1.125 +instance "**" :: (bifinite, bifinite) bifinite
   1.126 +proof
   1.127 +  fix i :: nat and x :: "'a \<otimes> 'b"
   1.128 +  show "chain (\<lambda>i. approx i\<cdot>x)"
   1.129 +    unfolding approx_sprod_def by simp
   1.130 +  show "(\<Squnion>i. approx i\<cdot>x) = x"
   1.131 +    unfolding approx_sprod_def
   1.132 +    by (simp add: lub_distribs eta_cfun)
   1.133 +  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   1.134 +    unfolding approx_sprod_def
   1.135 +    by (simp add: ssplit_def strictify_conv_if)
   1.136 +  have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
   1.137 +    unfolding approx_sprod_def
   1.138 +    apply (clarify, rule_tac p=x in sprodE)
   1.139 +     apply (simp add: Rep_Sprod_strict)
   1.140 +    apply (simp add: Rep_Sprod_spair spair_eq_iff)
   1.141 +    done
   1.142 +  hence "finite (Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x})"
   1.143 +    using finite_fixes_approx by (rule finite_subset)
   1.144 +  thus "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
   1.145 +    by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
   1.146 +qed
   1.147 +
   1.148 +lemma approx_spair [simp]:
   1.149 +  "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
   1.150 +unfolding approx_sprod_def
   1.151 +by (simp add: ssplit_def strictify_conv_if)
   1.152 +
   1.153  end