# HG changeset patch # User huffman # Date 1200341766 -3600 # Node ID 25533eb2b914c16516368229e62ab6c71d14d15d # Parent 6b96b93928738d9598cf344c83fa1d45f401e334 add bifinite instances diff -r 6b96b9392873 -r 25533eb2b914 src/HOLCF/Cprod.thy --- a/src/HOLCF/Cprod.thy Mon Jan 14 21:15:20 2008 +0100 +++ b/src/HOLCF/Cprod.thy Mon Jan 14 21:16:06 2008 +0100 @@ -8,7 +8,7 @@ header {* The cpo of cartesian products *} theory Cprod -imports Cfun +imports Bifinite begin defaultsort cpo @@ -230,6 +230,9 @@ lemma cpair_eq_pair: " = (x, y)" by (simp add: cpair_def cont_pair1 cont_pair2) +lemma pair_eq_cpair: "(x, y) = " +by (simp add: cpair_def cont_pair1 cont_pair2) + lemma inject_cpair: " = \ a = aa \ b = ba" by (simp add: cpair_eq_pair) @@ -270,10 +273,10 @@ lemma csnd_strict [simp]: "csnd\\ = \" by (simp add: inst_cprod_pcpo2) -lemma surjective_pairing_Cprod2: "p, csnd\p> = p" -apply (unfold cfst_def csnd_def) -apply (simp add: cont_fst cont_snd cpair_eq_pair) -done +lemma cpair_cfst_csnd: "\cfst\p, csnd\p\ = p" +by (cases p rule: cprodE, simp) + +lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd lemma less_cprod: "x \ y = (cfst\x \ cfst\y \ csnd\x \ csnd\y)" by (simp add: less_cprod_def cfst_def csnd_def cont_fst cont_snd) @@ -325,8 +328,47 @@ by (simp add: csplit_def) lemma csplit3 [simp]: "csplit\cpair\z = z" -by (simp add: csplit_def surjective_pairing_Cprod2) +by (simp add: csplit_def cpair_cfst_csnd) lemmas Cprod_rews = cfst_cpair csnd_cpair csplit2 +subsection {* Product type is a bifinite domain *} + +instance "*" :: (bifinite_cpo, bifinite_cpo) approx .. + +defs (overloaded) + approx_cprod_def: + "approx \ \n. \\x, y\. \approx n\x, approx n\y\" + +instance "*" :: (bifinite_cpo, bifinite_cpo) bifinite_cpo +proof + fix i :: nat and x :: "'a \ 'b" + show "chain (\i. approx i\x)" + unfolding approx_cprod_def by simp + show "(\i. approx i\x) = x" + unfolding approx_cprod_def + by (simp add: lub_distribs eta_cfun) + show "approx i\(approx i\x) = approx i\x" + unfolding approx_cprod_def csplit_def by simp + have "{x::'a \ 'b. approx i\x = x} \ + {x::'a. approx i\x = x} \ {x::'b. approx i\x = x}" + unfolding approx_cprod_def + by (clarsimp simp add: pair_eq_cpair) + thus "finite {x::'a \ 'b. approx i\x = x}" + by (rule finite_subset, + intro finite_cartesian_product finite_fixes_approx) +qed + +instance "*" :: (bifinite, bifinite) bifinite .. + +lemma approx_cpair [simp]: + "approx i\\x, y\ = \approx i\x, approx i\y\" +unfolding approx_cprod_def by simp + +lemma cfst_approx: "cfst\(approx i\p) = approx i\(cfst\p)" +by (cases p rule: cprodE, simp) + +lemma csnd_approx: "csnd\(approx i\p) = approx i\(csnd\p)" +by (cases p rule: cprodE, simp) + end