add bifinite instances
authorhuffman
Mon Jan 14 21:16:06 2008 +0100 (2008-01-14)
changeset 2591025533eb2b914
parent 25909 6b96b9392873
child 25911 cc3f00949986
add bifinite instances
src/HOLCF/Cprod.thy
     1.1 --- a/src/HOLCF/Cprod.thy	Mon Jan 14 21:15:20 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon Jan 14 21:16:06 2008 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* The cpo of cartesian products *}
     1.5  
     1.6  theory Cprod
     1.7 -imports Cfun
     1.8 +imports Bifinite
     1.9  begin
    1.10  
    1.11  defaultsort cpo
    1.12 @@ -230,6 +230,9 @@
    1.13  lemma cpair_eq_pair: "<x, y> = (x, y)"
    1.14  by (simp add: cpair_def cont_pair1 cont_pair2)
    1.15  
    1.16 +lemma pair_eq_cpair: "(x, y) = <x, y>"
    1.17 +by (simp add: cpair_def cont_pair1 cont_pair2)
    1.18 +
    1.19  lemma inject_cpair: "<a,b> = <aa,ba> \<Longrightarrow> a = aa \<and> b = ba"
    1.20  by (simp add: cpair_eq_pair)
    1.21  
    1.22 @@ -270,10 +273,10 @@
    1.23  lemma csnd_strict [simp]: "csnd\<cdot>\<bottom> = \<bottom>"
    1.24  by (simp add: inst_cprod_pcpo2)
    1.25  
    1.26 -lemma surjective_pairing_Cprod2: "<cfst\<cdot>p, csnd\<cdot>p> = p"
    1.27 -apply (unfold cfst_def csnd_def)
    1.28 -apply (simp add: cont_fst cont_snd cpair_eq_pair)
    1.29 -done
    1.30 +lemma cpair_cfst_csnd: "\<langle>cfst\<cdot>p, csnd\<cdot>p\<rangle> = p"
    1.31 +by (cases p rule: cprodE, simp)
    1.32 +
    1.33 +lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd
    1.34  
    1.35  lemma less_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
    1.36  by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd)
    1.37 @@ -325,8 +328,47 @@
    1.38  by (simp add: csplit_def)
    1.39  
    1.40  lemma csplit3 [simp]: "csplit\<cdot>cpair\<cdot>z = z"
    1.41 -by (simp add: csplit_def surjective_pairing_Cprod2)
    1.42 +by (simp add: csplit_def cpair_cfst_csnd)
    1.43  
    1.44  lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2
    1.45  
    1.46 +subsection {* Product type is a bifinite domain *}
    1.47 +
    1.48 +instance "*" :: (bifinite_cpo, bifinite_cpo) approx ..
    1.49 +
    1.50 +defs (overloaded)
    1.51 +  approx_cprod_def:
    1.52 +    "approx \<equiv> \<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>"
    1.53 +
    1.54 +instance "*" :: (bifinite_cpo, bifinite_cpo) bifinite_cpo
    1.55 +proof
    1.56 +  fix i :: nat and x :: "'a \<times> 'b"
    1.57 +  show "chain (\<lambda>i. approx i\<cdot>x)"
    1.58 +    unfolding approx_cprod_def by simp
    1.59 +  show "(\<Squnion>i. approx i\<cdot>x) = x"
    1.60 +    unfolding approx_cprod_def
    1.61 +    by (simp add: lub_distribs eta_cfun)
    1.62 +  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.63 +    unfolding approx_cprod_def csplit_def by simp
    1.64 +  have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
    1.65 +        {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
    1.66 +    unfolding approx_cprod_def
    1.67 +    by (clarsimp simp add: pair_eq_cpair)
    1.68 +  thus "finite {x::'a \<times> 'b. approx i\<cdot>x = x}"
    1.69 +    by (rule finite_subset,
    1.70 +        intro finite_cartesian_product finite_fixes_approx)
    1.71 +qed
    1.72 +
    1.73 +instance "*" :: (bifinite, bifinite) bifinite ..
    1.74 +
    1.75 +lemma approx_cpair [simp]:
    1.76 +  "approx i\<cdot>\<langle>x, y\<rangle> = \<langle>approx i\<cdot>x, approx i\<cdot>y\<rangle>"
    1.77 +unfolding approx_cprod_def by simp
    1.78 +
    1.79 +lemma cfst_approx: "cfst\<cdot>(approx i\<cdot>p) = approx i\<cdot>(cfst\<cdot>p)"
    1.80 +by (cases p rule: cprodE, simp)
    1.81 +
    1.82 +lemma csnd_approx: "csnd\<cdot>(approx i\<cdot>p) = approx i\<cdot>(csnd\<cdot>p)"
    1.83 +by (cases p rule: cprodE, simp)
    1.84 +
    1.85  end