src/HOLCF/Cprod.thy
changeset 31113 15cf300a742f
parent 31076 99fe356cbbc2
child 33399 768b2bb9e66a
     1.1 --- a/src/HOLCF/Cprod.thy	Mon May 11 12:25:20 2009 -0700
     1.2 +++ b/src/HOLCF/Cprod.thy	Mon May 11 12:26:33 2009 -0700
     1.3 @@ -91,10 +91,10 @@
     1.4  by (cut_tac Exh_Cprod2, auto)
     1.5  
     1.6  lemma cfst_cpair [simp]: "cfst\<cdot><x, y> = x"
     1.7 -by (simp add: cpair_eq_pair cfst_def cont_fst)
     1.8 +by (simp add: cpair_eq_pair cfst_def)
     1.9  
    1.10  lemma csnd_cpair [simp]: "csnd\<cdot><x, y> = y"
    1.11 -by (simp add: cpair_eq_pair csnd_def cont_snd)
    1.12 +by (simp add: cpair_eq_pair csnd_def)
    1.13  
    1.14  lemma cfst_strict [simp]: "cfst\<cdot>\<bottom> = \<bottom>"
    1.15  by (simp add: cfst_def)
    1.16 @@ -108,7 +108,7 @@
    1.17  lemmas surjective_pairing_Cprod2 = cpair_cfst_csnd
    1.18  
    1.19  lemma below_cprod: "x \<sqsubseteq> y = (cfst\<cdot>x \<sqsubseteq> cfst\<cdot>y \<and> csnd\<cdot>x \<sqsubseteq> csnd\<cdot>y)"
    1.20 -by (simp add: below_prod_def cfst_def csnd_def cont_fst cont_snd)
    1.21 +by (simp add: below_prod_def cfst_def csnd_def)
    1.22  
    1.23  lemma eq_cprod: "(x = y) = (cfst\<cdot>x = cfst\<cdot>y \<and> csnd\<cdot>x = csnd\<cdot>y)"
    1.24  by (auto simp add: po_eq_conv below_cprod)
    1.25 @@ -133,7 +133,7 @@
    1.26  
    1.27  lemma lub_cprod2: 
    1.28    "chain S \<Longrightarrow> range S <<| <\<Squnion>i. cfst\<cdot>(S i), \<Squnion>i. csnd\<cdot>(S i)>"
    1.29 -apply (simp add: cpair_eq_pair cfst_def csnd_def cont_fst cont_snd)
    1.30 +apply (simp add: cpair_eq_pair cfst_def csnd_def)
    1.31  apply (erule lub_cprod)
    1.32  done
    1.33  
    1.34 @@ -154,38 +154,9 @@
    1.35  
    1.36  subsection {* Product type is a bifinite domain *}
    1.37  
    1.38 -instantiation "*" :: (profinite, profinite) profinite
    1.39 -begin
    1.40 -
    1.41 -definition
    1.42 -  approx_cprod_def:
    1.43 -    "approx = (\<lambda>n. \<Lambda>\<langle>x, y\<rangle>. \<langle>approx n\<cdot>x, approx n\<cdot>y\<rangle>)"
    1.44 -
    1.45 -instance proof
    1.46 -  fix i :: nat and x :: "'a \<times> 'b"
    1.47 -  show "chain (approx :: nat \<Rightarrow> 'a \<times> 'b \<rightarrow> 'a \<times> 'b)"
    1.48 -    unfolding approx_cprod_def by simp
    1.49 -  show "(\<Squnion>i. approx i\<cdot>x) = x"
    1.50 -    unfolding approx_cprod_def
    1.51 -    by (simp add: lub_distribs eta_cfun)
    1.52 -  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.53 -    unfolding approx_cprod_def csplit_def by simp
    1.54 -  have "{x::'a \<times> 'b. approx i\<cdot>x = x} \<subseteq>
    1.55 -        {x::'a. approx i\<cdot>x = x} \<times> {x::'b. approx i\<cdot>x = x}"
    1.56 -    unfolding approx_cprod_def
    1.57 -    by (clarsimp simp add: pair_eq_cpair)
    1.58 -  thus "finite {x::'a \<times> 'b. approx i\<cdot>x = x}"
    1.59 -    by (rule finite_subset,
    1.60 -        intro finite_cartesian_product finite_fixes_approx)
    1.61 -qed
    1.62 -
    1.63 -end
    1.64 -
    1.65 -instance "*" :: (bifinite, bifinite) bifinite ..
    1.66 -
    1.67  lemma approx_cpair [simp]:
    1.68    "approx i\<cdot>\<langle>x, y\<rangle> = \<langle>approx i\<cdot>x, approx i\<cdot>y\<rangle>"
    1.69 -unfolding approx_cprod_def by simp
    1.70 +by (simp add: cpair_eq_pair)
    1.71  
    1.72  lemma cfst_approx: "cfst\<cdot>(approx i\<cdot>p) = approx i\<cdot>(cfst\<cdot>p)"
    1.73  by (cases p rule: cprodE, simp)