src/HOLCF/Cprod.thy
changeset 25784 71157f7e671e
parent 25131 2c8caac48ade
child 25815 c7b1e7b7087b
     1.1 --- a/src/HOLCF/Cprod.thy	Wed Jan 02 18:28:15 2008 +0100
     1.2 +++ b/src/HOLCF/Cprod.thy	Wed Jan 02 18:29:03 2008 +0100
     1.3 @@ -15,15 +15,19 @@
     1.4  
     1.5  subsection {* Type @{typ unit} is a pcpo *}
     1.6  
     1.7 -instance unit :: sq_ord ..
     1.8 +instantiation unit :: sq_ord
     1.9 +begin
    1.10  
    1.11 -defs (overloaded)
    1.12 +definition
    1.13    less_unit_def [simp]: "x \<sqsubseteq> (y::unit) \<equiv> True"
    1.14  
    1.15 +instance ..
    1.16 +end
    1.17 +
    1.18  instance unit :: po
    1.19  by intro_classes simp_all
    1.20  
    1.21 -instance unit :: cpo
    1.22 +instance unit :: dcpo
    1.23  by intro_classes (simp add: is_lub_def is_ub_def)
    1.24  
    1.25  instance unit :: pcpo
    1.26 @@ -42,29 +46,31 @@
    1.27  
    1.28  subsection {* Product type is a partial order *}
    1.29  
    1.30 -instance "*" :: (sq_ord, sq_ord) sq_ord ..
    1.31 +instantiation "*" :: (sq_ord, sq_ord) sq_ord
    1.32 +begin
    1.33  
    1.34 -defs (overloaded)
    1.35 +definition
    1.36    less_cprod_def: "(op \<sqsubseteq>) \<equiv> \<lambda>p1 p2. (fst p1 \<sqsubseteq> fst p2 \<and> snd p1 \<sqsubseteq> snd p2)"
    1.37  
    1.38 -lemma refl_less_cprod: "(p::'a * 'b) \<sqsubseteq> p"
    1.39 -by (simp add: less_cprod_def)
    1.40 +instance ..
    1.41 +end
    1.42  
    1.43 -lemma antisym_less_cprod: "\<lbrakk>(p1::'a * 'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p1\<rbrakk> \<Longrightarrow> p1 = p2"
    1.44 -apply (unfold less_cprod_def)
    1.45 -apply (rule injective_fst_snd)
    1.46 -apply (fast intro: antisym_less)
    1.47 -apply (fast intro: antisym_less)
    1.48 -done
    1.49 -
    1.50 -lemma trans_less_cprod: "\<lbrakk>(p1::'a*'b) \<sqsubseteq> p2; p2 \<sqsubseteq> p3\<rbrakk> \<Longrightarrow> p1 \<sqsubseteq> p3"
    1.51 -apply (unfold less_cprod_def)
    1.52 -apply (fast intro: trans_less)
    1.53 -done
    1.54 -
    1.55 -instance "*" :: (cpo, cpo) po
    1.56 -by intro_classes
    1.57 -  (assumption | rule refl_less_cprod antisym_less_cprod trans_less_cprod)+
    1.58 +instance "*" :: (po, po) po
    1.59 +proof
    1.60 +  fix x :: "'a \<times> 'b"
    1.61 +  show "x \<sqsubseteq> x"
    1.62 +    unfolding less_cprod_def by simp
    1.63 +next
    1.64 +  fix x y :: "'a \<times> 'b"
    1.65 +  assume "x \<sqsubseteq> y" "y \<sqsubseteq> x" thus "x = y"
    1.66 +    unfolding less_cprod_def Pair_fst_snd_eq
    1.67 +    by (fast intro: antisym_less)
    1.68 +next
    1.69 +  fix x y z :: "'a \<times> 'b"
    1.70 +  assume "x \<sqsubseteq> y" "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    1.71 +    unfolding less_cprod_def
    1.72 +    by (fast intro: trans_less)
    1.73 +qed
    1.74  
    1.75  
    1.76  subsection {* Monotonicity of @{text "(_,_)"}, @{term fst}, @{term snd} *}
    1.77 @@ -91,36 +97,70 @@
    1.78  
    1.79  subsection {* Product type is a cpo *}
    1.80  
    1.81 -lemma lub_cprod: 
    1.82 -  "chain S \<Longrightarrow> range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    1.83 +lemma lub_cprod:
    1.84 +  fixes S :: "nat \<Rightarrow> ('a::cpo \<times> 'b::cpo)"
    1.85 +  assumes S: "chain S"
    1.86 +  shows "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
    1.87  apply (rule is_lubI)
    1.88  apply (rule ub_rangeI)
    1.89  apply (rule_tac t = "S i" in surjective_pairing [THEN ssubst])
    1.90  apply (rule monofun_pair)
    1.91  apply (rule is_ub_thelub)
    1.92 -apply (erule monofun_fst [THEN ch2ch_monofun])
    1.93 +apply (rule ch2ch_monofun [OF monofun_fst S])
    1.94  apply (rule is_ub_thelub)
    1.95 -apply (erule monofun_snd [THEN ch2ch_monofun])
    1.96 +apply (rule ch2ch_monofun [OF monofun_snd S])
    1.97  apply (rule_tac t = "u" in surjective_pairing [THEN ssubst])
    1.98  apply (rule monofun_pair)
    1.99  apply (rule is_lub_thelub)
   1.100 -apply (erule monofun_fst [THEN ch2ch_monofun])
   1.101 +apply (rule ch2ch_monofun [OF monofun_fst S])
   1.102  apply (erule monofun_fst [THEN ub2ub_monofun])
   1.103  apply (rule is_lub_thelub)
   1.104 -apply (erule monofun_snd [THEN ch2ch_monofun])
   1.105 +apply (rule ch2ch_monofun [OF monofun_snd S])
   1.106  apply (erule monofun_snd [THEN ub2ub_monofun])
   1.107  done
   1.108  
   1.109 +lemma directed_lub_cprod:
   1.110 +  fixes S :: "('a::dcpo \<times> 'b::dcpo) set"
   1.111 +  assumes S: "directed S"
   1.112 +  shows "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
   1.113 +apply (rule is_lubI)
   1.114 +apply (rule is_ubI)
   1.115 +apply (rule_tac t=x in surjective_pairing [THEN ssubst])
   1.116 +apply (rule monofun_pair)
   1.117 +apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_fst S] imageI])
   1.118 +apply (erule is_ub_thelub' [OF dir2dir_monofun [OF monofun_snd S] imageI])
   1.119 +apply (rule_tac t=u in surjective_pairing [THEN ssubst])
   1.120 +apply (rule monofun_pair)
   1.121 +apply (rule is_lub_thelub')
   1.122 +apply (rule dir2dir_monofun [OF monofun_fst S])
   1.123 +apply (erule ub2ub_monofun' [OF monofun_fst])
   1.124 +apply (rule is_lub_thelub')
   1.125 +apply (rule dir2dir_monofun [OF monofun_snd S])
   1.126 +apply (erule ub2ub_monofun' [OF monofun_snd])
   1.127 +done
   1.128 +
   1.129  lemma thelub_cprod:
   1.130 -  "chain S \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   1.131 +  "chain (S::nat \<Rightarrow> 'a::cpo \<times> 'b::cpo)
   1.132 +    \<Longrightarrow> lub (range S) = (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   1.133  by (rule lub_cprod [THEN thelubI])
   1.134  
   1.135 -lemma cpo_cprod:
   1.136 -  "chain (S::nat \<Rightarrow> 'a::cpo * 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x"
   1.137 -by (rule exI, erule lub_cprod)
   1.138 +instance "*" :: (cpo, cpo) cpo
   1.139 +proof
   1.140 +  fix S :: "nat \<Rightarrow> ('a \<times> 'b)"
   1.141 +  assume "chain S"
   1.142 +  hence "range S <<| (\<Squnion>i. fst (S i), \<Squnion>i. snd (S i))"
   1.143 +    by (rule lub_cprod)
   1.144 +  thus "\<exists>x. range S <<| x" ..
   1.145 +qed
   1.146  
   1.147 -instance "*" :: (cpo, cpo) cpo
   1.148 -by intro_classes (rule cpo_cprod)
   1.149 +instance "*" :: (dcpo, dcpo) dcpo
   1.150 +proof
   1.151 +  fix S :: "('a \<times> 'b) set"
   1.152 +  assume "directed S"
   1.153 +  hence "S <<| (\<Squnion>x\<in>S. fst x, \<Squnion>x\<in>S. snd x)"
   1.154 +    by (rule directed_lub_cprod)
   1.155 +  thus "\<exists>x. S <<| x" ..
   1.156 +qed
   1.157  
   1.158  subsection {* Product type is pointed *}
   1.159