new lemmas
authorhuffman
Mon May 11 12:25:20 2009 -0700 (2009-05-11)
changeset 311124dcda8ca5d59
parent 31099 03314c427b34
child 31113 15cf300a742f
new lemmas
src/HOLCF/Product_Cpo.thy
     1.1 --- a/src/HOLCF/Product_Cpo.thy	Tue May 05 17:09:18 2009 +0200
     1.2 +++ b/src/HOLCF/Product_Cpo.thy	Mon May 11 12:25:20 2009 -0700
     1.3 @@ -78,6 +78,10 @@
     1.4    "\<lbrakk>x1 \<sqsubseteq> x2; y1 \<sqsubseteq> y2\<rbrakk> \<Longrightarrow> (x1, y1) \<sqsubseteq> (x2, y2)"
     1.5  by simp
     1.6  
     1.7 +lemma ch2ch_Pair [simp]:
     1.8 +  "chain X \<Longrightarrow> chain Y \<Longrightarrow> chain (\<lambda>i. (X i, Y i))"
     1.9 +by (rule chainI, simp add: chainE)
    1.10 +
    1.11  text {* @{term fst} and @{term snd} are monotone *}
    1.12  
    1.13  lemma monofun_fst: "monofun fst"
    1.14 @@ -86,28 +90,47 @@
    1.15  lemma monofun_snd: "monofun snd"
    1.16  by (simp add: monofun_def below_prod_def)
    1.17  
    1.18 +lemmas ch2ch_fst [simp] = ch2ch_monofun [OF monofun_fst]
    1.19 +
    1.20 +lemmas ch2ch_snd [simp] = ch2ch_monofun [OF monofun_snd]
    1.21 +
    1.22 +lemma prod_chain_cases:
    1.23 +  assumes "chain Y"
    1.24 +  obtains A B
    1.25 +  where "chain A" and "chain B" and "Y = (\<lambda>i. (A i, B i))"
    1.26 +proof
    1.27 +  from `chain Y` show "chain (\<lambda>i. fst (Y i))" by (rule ch2ch_fst)
    1.28 +  from `chain Y` show "chain (\<lambda>i. snd (Y i))" by (rule ch2ch_snd)
    1.29 +  show "Y = (\<lambda>i. (fst (Y i), snd (Y i)))" by simp
    1.30 +qed
    1.31 +
    1.32  subsection {* Product type is a cpo *}
    1.33  
    1.34  lemma is_lub_Pair:
    1.35 -  "\<lbrakk>range X <<| x; range Y <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (X i, Y i)) <<| (x, y)"
    1.36 +  "\<lbrakk>range A <<| x; range B <<| y\<rbrakk> \<Longrightarrow> range (\<lambda>i. (A i, B i)) <<| (x, y)"
    1.37  apply (rule is_lubI [OF ub_rangeI])
    1.38 -apply (simp add: below_prod_def is_ub_lub)
    1.39 +apply (simp add: is_ub_lub)
    1.40  apply (frule ub2ub_monofun [OF monofun_fst])
    1.41  apply (drule ub2ub_monofun [OF monofun_snd])
    1.42  apply (simp add: below_prod_def is_lub_lub)
    1.43  done
    1.44  
    1.45 +lemma thelub_Pair:
    1.46 +  "\<lbrakk>chain (A::nat \<Rightarrow> 'a::cpo); chain (B::nat \<Rightarrow> 'b::cpo)\<rbrakk>
    1.47 +    \<Longrightarrow> (\<Squnion>i. (A i, B i)) = (\<Squnion>i. A i, \<Squnion>i. B i)"
    1.48 +by (fast intro: thelubI is_lub_Pair elim: thelubE)
    1.49 +
    1.50  lemma lub_cprod:
    1.51    fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
    1.52    assumes S: "chain S"
    1.53    shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    1.54  proof -
    1.55 -  have "chain (\<lambda>i. fst (S i))"
    1.56 -    using monofun_fst S by (rule ch2ch_monofun)
    1.57 +  from `chain S` have "chain (\<lambda>i. fst (S i))"
    1.58 +    by (rule ch2ch_fst)
    1.59    hence 1: "range (\<lambda>i. fst (S i)) <<| (\<Squnion>i. fst (S i))"
    1.60      by (rule cpo_lubI)
    1.61 -  have "chain (\<lambda>i. snd (S i))"
    1.62 -    using monofun_snd S by (rule ch2ch_monofun)
    1.63 +  from `chain S` have "chain (\<lambda>i. snd (S i))"
    1.64 +    by (rule ch2ch_snd)
    1.65    hence 2: "range (\<lambda>i. snd (S i)) <<| (\<Squnion>i. snd (S i))"
    1.66      by (rule cpo_lubI)
    1.67    show "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"