src/HOLCF/Sprod.thy
author wenzelm
Sat Oct 17 14:43:18 2009 +0200 (2009-10-17)
changeset 32960 69916a850301
parent 31114 2e9cc546e5b0
child 33504 b4210cc3ac97
permissions -rw-r--r--
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
     1 (*  Title:      HOLCF/Sprod.thy
     2     Author:     Franz Regensburger and Brian Huffman
     3 *)
     4 
     5 header {* The type of strict products *}
     6 
     7 theory Sprod
     8 imports Bifinite
     9 begin
    10 
    11 defaultsort pcpo
    12 
    13 subsection {* Definition of strict product type *}
    14 
    15 pcpodef (Sprod)  ('a, 'b) "**" (infixr "**" 20) =
    16         "{p::'a \<times> 'b. p = \<bottom> \<or> (fst p \<noteq> \<bottom> \<and> snd p \<noteq> \<bottom>)}"
    17 by simp_all
    18 
    19 instance "**" :: ("{finite_po,pcpo}", "{finite_po,pcpo}") finite_po
    20 by (rule typedef_finite_po [OF type_definition_Sprod])
    21 
    22 instance "**" :: ("{chfin,pcpo}", "{chfin,pcpo}") chfin
    23 by (rule typedef_chfin [OF type_definition_Sprod below_Sprod_def])
    24 
    25 syntax (xsymbols)
    26   "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    27 syntax (HTML output)
    28   "**"          :: "[type, type] => type"        ("(_ \<otimes>/ _)" [21,20] 20)
    29 
    30 lemma spair_lemma:
    31   "(strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a) \<in> Sprod"
    32 by (simp add: Sprod_def strictify_conv_if)
    33 
    34 subsection {* Definitions of constants *}
    35 
    36 definition
    37   sfst :: "('a ** 'b) \<rightarrow> 'a" where
    38   "sfst = (\<Lambda> p. fst (Rep_Sprod p))"
    39 
    40 definition
    41   ssnd :: "('a ** 'b) \<rightarrow> 'b" where
    42   "ssnd = (\<Lambda> p. snd (Rep_Sprod p))"
    43 
    44 definition
    45   spair :: "'a \<rightarrow> 'b \<rightarrow> ('a ** 'b)" where
    46   "spair = (\<Lambda> a b. Abs_Sprod
    47              (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a))"
    48 
    49 definition
    50   ssplit :: "('a \<rightarrow> 'b \<rightarrow> 'c) \<rightarrow> ('a ** 'b) \<rightarrow> 'c" where
    51   "ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))"
    52 
    53 syntax
    54   "@stuple" :: "['a, args] => 'a ** 'b"  ("(1'(:_,/ _:'))")
    55 translations
    56   "(:x, y, z:)" == "(:x, (:y, z:):)"
    57   "(:x, y:)"    == "CONST spair\<cdot>x\<cdot>y"
    58 
    59 translations
    60   "\<Lambda>(CONST spair\<cdot>x\<cdot>y). t" == "CONST ssplit\<cdot>(\<Lambda> x y. t)"
    61 
    62 subsection {* Case analysis *}
    63 
    64 lemma Rep_Sprod_spair:
    65   "Rep_Sprod (:a, b:) = (strictify\<cdot>(\<Lambda> b. a)\<cdot>b, strictify\<cdot>(\<Lambda> a. b)\<cdot>a)"
    66 unfolding spair_def
    67 by (simp add: cont_Abs_Sprod Abs_Sprod_inverse spair_lemma)
    68 
    69 lemmas Rep_Sprod_simps =
    70   Rep_Sprod_inject [symmetric] below_Sprod_def
    71   Rep_Sprod_strict Rep_Sprod_spair
    72 
    73 lemma Exh_Sprod:
    74   "z = \<bottom> \<or> (\<exists>a b. z = (:a, b:) \<and> a \<noteq> \<bottom> \<and> b \<noteq> \<bottom>)"
    75 apply (insert Rep_Sprod [of z])
    76 apply (simp add: Rep_Sprod_simps Pair_fst_snd_eq)
    77 apply (simp add: Sprod_def)
    78 apply (erule disjE, simp)
    79 apply (simp add: strictify_conv_if)
    80 apply fast
    81 done
    82 
    83 lemma sprodE [cases type: **]:
    84   "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x y. \<lbrakk>p = (:x, y:); x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"
    85 by (cut_tac z=p in Exh_Sprod, auto)
    86 
    87 lemma sprod_induct [induct type: **]:
    88   "\<lbrakk>P \<bottom>; \<And>x y. \<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> P (:x, y:)\<rbrakk> \<Longrightarrow> P x"
    89 by (cases x, simp_all)
    90 
    91 subsection {* Properties of @{term spair} *}
    92 
    93 lemma spair_strict1 [simp]: "(:\<bottom>, y:) = \<bottom>"
    94 by (simp add: Rep_Sprod_simps strictify_conv_if)
    95 
    96 lemma spair_strict2 [simp]: "(:x, \<bottom>:) = \<bottom>"
    97 by (simp add: Rep_Sprod_simps strictify_conv_if)
    98 
    99 lemma spair_strict_iff [simp]: "((:x, y:) = \<bottom>) = (x = \<bottom> \<or> y = \<bottom>)"
   100 by (simp add: Rep_Sprod_simps strictify_conv_if)
   101 
   102 lemma spair_below_iff:
   103   "((:a, b:) \<sqsubseteq> (:c, d:)) = (a = \<bottom> \<or> b = \<bottom> \<or> (a \<sqsubseteq> c \<and> b \<sqsubseteq> d))"
   104 by (simp add: Rep_Sprod_simps strictify_conv_if)
   105 
   106 lemma spair_eq_iff:
   107   "((:a, b:) = (:c, d:)) =
   108     (a = c \<and> b = d \<or> (a = \<bottom> \<or> b = \<bottom>) \<and> (c = \<bottom> \<or> d = \<bottom>))"
   109 by (simp add: Rep_Sprod_simps strictify_conv_if)
   110 
   111 lemma spair_strict: "x = \<bottom> \<or> y = \<bottom> \<Longrightarrow> (:x, y:) = \<bottom>"
   112 by simp
   113 
   114 lemma spair_strict_rev: "(:x, y:) \<noteq> \<bottom> \<Longrightarrow> x \<noteq> \<bottom> \<and> y \<noteq> \<bottom>"
   115 by simp
   116 
   117 lemma spair_defined: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<noteq> \<bottom>"
   118 by simp
   119 
   120 lemma spair_defined_rev: "(:x, y:) = \<bottom> \<Longrightarrow> x = \<bottom> \<or> y = \<bottom>"
   121 by simp
   122 
   123 lemma spair_eq:
   124   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ((:x, y:) = (:a, b:)) = (x = a \<and> y = b)"
   125 by (simp add: spair_eq_iff)
   126 
   127 lemma spair_inject:
   128   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>; (:x, y:) = (:a, b:)\<rbrakk> \<Longrightarrow> x = a \<and> y = b"
   129 by (rule spair_eq [THEN iffD1])
   130 
   131 lemma inst_sprod_pcpo2: "UU = (:UU,UU:)"
   132 by simp
   133 
   134 subsection {* Properties of @{term sfst} and @{term ssnd} *}
   135 
   136 lemma sfst_strict [simp]: "sfst\<cdot>\<bottom> = \<bottom>"
   137 by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_strict)
   138 
   139 lemma ssnd_strict [simp]: "ssnd\<cdot>\<bottom> = \<bottom>"
   140 by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_strict)
   141 
   142 lemma sfst_spair [simp]: "y \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>(:x, y:) = x"
   143 by (simp add: sfst_def cont_Rep_Sprod Rep_Sprod_spair)
   144 
   145 lemma ssnd_spair [simp]: "x \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>(:x, y:) = y"
   146 by (simp add: ssnd_def cont_Rep_Sprod Rep_Sprod_spair)
   147 
   148 lemma sfst_defined_iff [simp]: "(sfst\<cdot>p = \<bottom>) = (p = \<bottom>)"
   149 by (cases p, simp_all)
   150 
   151 lemma ssnd_defined_iff [simp]: "(ssnd\<cdot>p = \<bottom>) = (p = \<bottom>)"
   152 by (cases p, simp_all)
   153 
   154 lemma sfst_defined: "p \<noteq> \<bottom> \<Longrightarrow> sfst\<cdot>p \<noteq> \<bottom>"
   155 by simp
   156 
   157 lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
   158 by simp
   159 
   160 lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
   161 by (cases p, simp_all)
   162 
   163 lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"
   164 apply (simp add: below_Sprod_def sfst_def ssnd_def cont_Rep_Sprod)
   165 apply (simp only: below_prod_def)
   166 done
   167 
   168 lemma eq_sprod: "(x = y) = (sfst\<cdot>x = sfst\<cdot>y \<and> ssnd\<cdot>x = ssnd\<cdot>y)"
   169 by (auto simp add: po_eq_conv below_sprod)
   170 
   171 lemma spair_below:
   172   "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> (:x, y:) \<sqsubseteq> (:a, b:) = (x \<sqsubseteq> a \<and> y \<sqsubseteq> b)"
   173 apply (cases "a = \<bottom>", simp)
   174 apply (cases "b = \<bottom>", simp)
   175 apply (simp add: below_sprod)
   176 done
   177 
   178 lemma sfst_below_iff: "sfst\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:y, ssnd\<cdot>x:)"
   179 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
   180 apply (simp add: below_sprod)
   181 done
   182 
   183 lemma ssnd_below_iff: "ssnd\<cdot>x \<sqsubseteq> y = x \<sqsubseteq> (:sfst\<cdot>x, y:)"
   184 apply (cases "x = \<bottom>", simp, cases "y = \<bottom>", simp)
   185 apply (simp add: below_sprod)
   186 done
   187 
   188 subsection {* Compactness *}
   189 
   190 lemma compact_sfst: "compact x \<Longrightarrow> compact (sfst\<cdot>x)"
   191 by (rule compactI, simp add: sfst_below_iff)
   192 
   193 lemma compact_ssnd: "compact x \<Longrightarrow> compact (ssnd\<cdot>x)"
   194 by (rule compactI, simp add: ssnd_below_iff)
   195 
   196 lemma compact_spair: "\<lbrakk>compact x; compact y\<rbrakk> \<Longrightarrow> compact (:x, y:)"
   197 by (rule compact_Sprod, simp add: Rep_Sprod_spair strictify_conv_if)
   198 
   199 lemma compact_spair_iff:
   200   "compact (:x, y:) = (x = \<bottom> \<or> y = \<bottom> \<or> (compact x \<and> compact y))"
   201 apply (safe elim!: compact_spair)
   202 apply (drule compact_sfst, simp)
   203 apply (drule compact_ssnd, simp)
   204 apply simp
   205 apply simp
   206 done
   207 
   208 subsection {* Properties of @{term ssplit} *}
   209 
   210 lemma ssplit1 [simp]: "ssplit\<cdot>f\<cdot>\<bottom> = \<bottom>"
   211 by (simp add: ssplit_def)
   212 
   213 lemma ssplit2 [simp]: "\<lbrakk>x \<noteq> \<bottom>; y \<noteq> \<bottom>\<rbrakk> \<Longrightarrow> ssplit\<cdot>f\<cdot>(:x, y:) = f\<cdot>x\<cdot>y"
   214 by (simp add: ssplit_def)
   215 
   216 lemma ssplit3 [simp]: "ssplit\<cdot>spair\<cdot>z = z"
   217 by (cases z, simp_all)
   218 
   219 subsection {* Strict product preserves flatness *}
   220 
   221 instance "**" :: (flat, flat) flat
   222 proof
   223   fix x y :: "'a \<otimes> 'b"
   224   assume "x \<sqsubseteq> y" thus "x = \<bottom> \<or> x = y"
   225     apply (induct x, simp)
   226     apply (induct y, simp)
   227     apply (simp add: spair_below_iff flat_below_iff)
   228     done
   229 qed
   230 
   231 subsection {* Strict product is a bifinite domain *}
   232 
   233 instantiation "**" :: (bifinite, bifinite) bifinite
   234 begin
   235 
   236 definition
   237   approx_sprod_def:
   238     "approx = (\<lambda>n. \<Lambda>(:x, y:). (:approx n\<cdot>x, approx n\<cdot>y:))"
   239 
   240 instance proof
   241   fix i :: nat and x :: "'a \<otimes> 'b"
   242   show "chain (approx :: nat \<Rightarrow> 'a \<otimes> 'b \<rightarrow> 'a \<otimes> 'b)"
   243     unfolding approx_sprod_def by simp
   244   show "(\<Squnion>i. approx i\<cdot>x) = x"
   245     unfolding approx_sprod_def
   246     by (simp add: lub_distribs eta_cfun)
   247   show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   248     unfolding approx_sprod_def
   249     by (simp add: ssplit_def strictify_conv_if)
   250   have "Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x} \<subseteq> {x. approx i\<cdot>x = x}"
   251     unfolding approx_sprod_def
   252     apply (clarify, case_tac x)
   253      apply (simp add: Rep_Sprod_strict)
   254     apply (simp add: Rep_Sprod_spair spair_eq_iff)
   255     done
   256   hence "finite (Rep_Sprod ` {x::'a \<otimes> 'b. approx i\<cdot>x = x})"
   257     using finite_fixes_approx by (rule finite_subset)
   258   thus "finite {x::'a \<otimes> 'b. approx i\<cdot>x = x}"
   259     by (rule finite_imageD, simp add: inj_on_def Rep_Sprod_inject)
   260 qed
   261 
   262 end
   263 
   264 lemma approx_spair [simp]:
   265   "approx i\<cdot>(:x, y:) = (:approx i\<cdot>x, approx i\<cdot>y:)"
   266 unfolding approx_sprod_def
   267 by (simp add: ssplit_def strictify_conv_if)
   268 
   269 end