src/HOLCF/Dsum.thy
changeset 29549 7187373c6cb1
parent 29548 02a52ae34b7a
parent 29547 f2587922591e
child 29550 67ec51c032cb
child 29667 53103fc8ffa3
     1.1 --- a/src/HOLCF/Dsum.thy	Sun Jan 18 13:53:15 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,251 +0,0 @@
     1.4 -(*  Title:      HOLCF/Dsum.thy
     1.5 -    Author:     Brian Huffman
     1.6 -*)
     1.7 -
     1.8 -header {* The cpo of disjoint sums *}
     1.9 -
    1.10 -theory Dsum
    1.11 -imports Bifinite
    1.12 -begin
    1.13 -
    1.14 -subsection {* Ordering on type @{typ "'a + 'b"} *}
    1.15 -
    1.16 -instantiation "+" :: (sq_ord, sq_ord) sq_ord
    1.17 -begin
    1.18 -
    1.19 -definition
    1.20 -  less_sum_def: "x \<sqsubseteq> y \<equiv> case x of
    1.21 -         Inl a \<Rightarrow> (case y of Inl b \<Rightarrow> a \<sqsubseteq> b | Inr b \<Rightarrow> False) |
    1.22 -         Inr a \<Rightarrow> (case y of Inl b \<Rightarrow> False | Inr b \<Rightarrow> a \<sqsubseteq> b)"
    1.23 -
    1.24 -instance ..
    1.25 -end
    1.26 -
    1.27 -lemma Inl_less_iff [simp]: "Inl x \<sqsubseteq> Inl y = x \<sqsubseteq> y"
    1.28 -unfolding less_sum_def by simp
    1.29 -
    1.30 -lemma Inr_less_iff [simp]: "Inr x \<sqsubseteq> Inr y = x \<sqsubseteq> y"
    1.31 -unfolding less_sum_def by simp
    1.32 -
    1.33 -lemma Inl_less_Inr [simp]: "\<not> Inl x \<sqsubseteq> Inr y"
    1.34 -unfolding less_sum_def by simp
    1.35 -
    1.36 -lemma Inr_less_Inl [simp]: "\<not> Inr x \<sqsubseteq> Inl y"
    1.37 -unfolding less_sum_def by simp
    1.38 -
    1.39 -lemma Inl_mono: "x \<sqsubseteq> y \<Longrightarrow> Inl x \<sqsubseteq> Inl y"
    1.40 -by simp
    1.41 -
    1.42 -lemma Inr_mono: "x \<sqsubseteq> y \<Longrightarrow> Inr x \<sqsubseteq> Inr y"
    1.43 -by simp
    1.44 -
    1.45 -lemma Inl_lessE: "\<lbrakk>Inl a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    1.46 -by (cases x, simp_all)
    1.47 -
    1.48 -lemma Inr_lessE: "\<lbrakk>Inr a \<sqsubseteq> x; \<And>b. \<lbrakk>x = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
    1.49 -by (cases x, simp_all)
    1.50 -
    1.51 -lemmas sum_less_elims = Inl_lessE Inr_lessE
    1.52 -
    1.53 -lemma sum_less_cases:
    1.54 -  "\<lbrakk>x \<sqsubseteq> y;
    1.55 -    \<And>a b. \<lbrakk>x = Inl a; y = Inl b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R;
    1.56 -    \<And>a b. \<lbrakk>x = Inr a; y = Inr b; a \<sqsubseteq> b\<rbrakk> \<Longrightarrow> R\<rbrakk>
    1.57 -      \<Longrightarrow> R"
    1.58 -by (cases x, safe elim!: sum_less_elims, auto)
    1.59 -
    1.60 -subsection {* Sum type is a complete partial order *}
    1.61 -
    1.62 -instance "+" :: (po, po) po
    1.63 -proof
    1.64 -  fix x :: "'a + 'b"
    1.65 -  show "x \<sqsubseteq> x"
    1.66 -    by (induct x, simp_all)
    1.67 -next
    1.68 -  fix x y :: "'a + 'b"
    1.69 -  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> x" thus "x = y"
    1.70 -    by (induct x, auto elim!: sum_less_elims intro: antisym_less)
    1.71 -next
    1.72 -  fix x y z :: "'a + 'b"
    1.73 -  assume "x \<sqsubseteq> y" and "y \<sqsubseteq> z" thus "x \<sqsubseteq> z"
    1.74 -    by (induct x, auto elim!: sum_less_elims intro: trans_less)
    1.75 -qed
    1.76 -
    1.77 -lemma monofun_inv_Inl: "monofun (\<lambda>p. THE a. p = Inl a)"
    1.78 -by (rule monofunI, erule sum_less_cases, simp_all)
    1.79 -
    1.80 -lemma monofun_inv_Inr: "monofun (\<lambda>p. THE b. p = Inr b)"
    1.81 -by (rule monofunI, erule sum_less_cases, simp_all)
    1.82 -
    1.83 -lemma sum_chain_cases:
    1.84 -  assumes Y: "chain Y"
    1.85 -  assumes A: "\<And>A. \<lbrakk>chain A; Y = (\<lambda>i. Inl (A i))\<rbrakk> \<Longrightarrow> R"
    1.86 -  assumes B: "\<And>B. \<lbrakk>chain B; Y = (\<lambda>i. Inr (B i))\<rbrakk> \<Longrightarrow> R"
    1.87 -  shows "R"
    1.88 - apply (cases "Y 0")
    1.89 -  apply (rule A)
    1.90 -   apply (rule ch2ch_monofun [OF monofun_inv_Inl Y])
    1.91 -  apply (rule ext)
    1.92 -  apply (cut_tac j=i in chain_mono [OF Y le0], simp)
    1.93 -  apply (erule Inl_lessE, simp)
    1.94 - apply (rule B)
    1.95 -  apply (rule ch2ch_monofun [OF monofun_inv_Inr Y])
    1.96 - apply (rule ext)
    1.97 - apply (cut_tac j=i in chain_mono [OF Y le0], simp)
    1.98 - apply (erule Inr_lessE, simp)
    1.99 -done
   1.100 -
   1.101 -lemma is_lub_Inl: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inl (S i)) <<| Inl x"
   1.102 - apply (rule is_lubI)
   1.103 -  apply (rule ub_rangeI)
   1.104 -  apply (simp add: is_ub_lub)
   1.105 - apply (frule ub_rangeD [where i=arbitrary])
   1.106 - apply (erule Inl_lessE, simp)
   1.107 - apply (erule is_lub_lub)
   1.108 - apply (rule ub_rangeI)
   1.109 - apply (drule ub_rangeD, simp)
   1.110 -done
   1.111 -
   1.112 -lemma is_lub_Inr: "range S <<| x \<Longrightarrow> range (\<lambda>i. Inr (S i)) <<| Inr x"
   1.113 - apply (rule is_lubI)
   1.114 -  apply (rule ub_rangeI)
   1.115 -  apply (simp add: is_ub_lub)
   1.116 - apply (frule ub_rangeD [where i=arbitrary])
   1.117 - apply (erule Inr_lessE, simp)
   1.118 - apply (erule is_lub_lub)
   1.119 - apply (rule ub_rangeI)
   1.120 - apply (drule ub_rangeD, simp)
   1.121 -done
   1.122 -
   1.123 -instance "+" :: (cpo, cpo) cpo
   1.124 - apply intro_classes
   1.125 - apply (erule sum_chain_cases, safe)
   1.126 -  apply (rule exI)
   1.127 -  apply (rule is_lub_Inl)
   1.128 -  apply (erule cpo_lubI)
   1.129 - apply (rule exI)
   1.130 - apply (rule is_lub_Inr)
   1.131 - apply (erule cpo_lubI)
   1.132 -done
   1.133 -
   1.134 -subsection {* Continuity of @{term Inl}, @{term Inr}, @{term sum_case} *}
   1.135 -
   1.136 -lemma cont2cont_Inl [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inl (f x))"
   1.137 -by (fast intro: contI is_lub_Inl elim: contE)
   1.138 -
   1.139 -lemma cont2cont_Inr [simp]: "cont f \<Longrightarrow> cont (\<lambda>x. Inr (f x))"
   1.140 -by (fast intro: contI is_lub_Inr elim: contE)
   1.141 -
   1.142 -lemma cont_Inl: "cont Inl"
   1.143 -by (rule cont2cont_Inl [OF cont_id])
   1.144 -
   1.145 -lemma cont_Inr: "cont Inr"
   1.146 -by (rule cont2cont_Inr [OF cont_id])
   1.147 -
   1.148 -lemmas ch2ch_Inl [simp] = ch2ch_cont [OF cont_Inl]
   1.149 -lemmas ch2ch_Inr [simp] = ch2ch_cont [OF cont_Inr]
   1.150 -
   1.151 -lemmas lub_Inl = cont2contlubE [OF cont_Inl, symmetric]
   1.152 -lemmas lub_Inr = cont2contlubE [OF cont_Inr, symmetric]
   1.153 -
   1.154 -lemma cont_sum_case1:
   1.155 -  assumes f: "\<And>a. cont (\<lambda>x. f x a)"
   1.156 -  assumes g: "\<And>b. cont (\<lambda>x. g x b)"
   1.157 -  shows "cont (\<lambda>x. case y of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   1.158 -by (induct y, simp add: f, simp add: g)
   1.159 -
   1.160 -lemma cont_sum_case2: "\<lbrakk>cont f; cont g\<rbrakk> \<Longrightarrow> cont (sum_case f g)"
   1.161 -apply (rule contI)
   1.162 -apply (erule sum_chain_cases)
   1.163 -apply (simp add: cont2contlubE [OF cont_Inl, symmetric] contE)
   1.164 -apply (simp add: cont2contlubE [OF cont_Inr, symmetric] contE)
   1.165 -done
   1.166 -
   1.167 -lemma cont2cont_sum_case [simp]:
   1.168 -  assumes f1: "\<And>a. cont (\<lambda>x. f x a)" and f2: "\<And>x. cont (\<lambda>a. f x a)"
   1.169 -  assumes g1: "\<And>b. cont (\<lambda>x. g x b)" and g2: "\<And>x. cont (\<lambda>b. g x b)"
   1.170 -  assumes h: "cont (\<lambda>x. h x)"
   1.171 -  shows "cont (\<lambda>x. case h x of Inl a \<Rightarrow> f x a | Inr b \<Rightarrow> g x b)"
   1.172 -apply (rule cont2cont_app2 [OF cont2cont_lambda _ h])
   1.173 -apply (rule cont_sum_case1 [OF f1 g1])
   1.174 -apply (rule cont_sum_case2 [OF f2 g2])
   1.175 -done
   1.176 -
   1.177 -subsection {* Compactness and chain-finiteness *}
   1.178 -
   1.179 -lemma compact_Inl: "compact a \<Longrightarrow> compact (Inl a)"
   1.180 -apply (rule compactI2)
   1.181 -apply (erule sum_chain_cases, safe)
   1.182 -apply (simp add: lub_Inl)
   1.183 -apply (erule (2) compactD2)
   1.184 -apply (simp add: lub_Inr)
   1.185 -done
   1.186 -
   1.187 -lemma compact_Inr: "compact a \<Longrightarrow> compact (Inr a)"
   1.188 -apply (rule compactI2)
   1.189 -apply (erule sum_chain_cases, safe)
   1.190 -apply (simp add: lub_Inl)
   1.191 -apply (simp add: lub_Inr)
   1.192 -apply (erule (2) compactD2)
   1.193 -done
   1.194 -
   1.195 -lemma compact_Inl_rev: "compact (Inl a) \<Longrightarrow> compact a"
   1.196 -unfolding compact_def
   1.197 -by (drule adm_subst [OF cont_Inl], simp)
   1.198 -
   1.199 -lemma compact_Inr_rev: "compact (Inr a) \<Longrightarrow> compact a"
   1.200 -unfolding compact_def
   1.201 -by (drule adm_subst [OF cont_Inr], simp)
   1.202 -
   1.203 -lemma compact_Inl_iff [simp]: "compact (Inl a) = compact a"
   1.204 -by (safe elim!: compact_Inl compact_Inl_rev)
   1.205 -
   1.206 -lemma compact_Inr_iff [simp]: "compact (Inr a) = compact a"
   1.207 -by (safe elim!: compact_Inr compact_Inr_rev)
   1.208 -
   1.209 -instance "+" :: (chfin, chfin) chfin
   1.210 -apply intro_classes
   1.211 -apply (erule compact_imp_max_in_chain)
   1.212 -apply (case_tac "\<Squnion>i. Y i", simp_all)
   1.213 -done
   1.214 -
   1.215 -instance "+" :: (finite_po, finite_po) finite_po ..
   1.216 -
   1.217 -instance "+" :: (discrete_cpo, discrete_cpo) discrete_cpo
   1.218 -by intro_classes (simp add: less_sum_def split: sum.split)
   1.219 -
   1.220 -subsection {* Sum type is a bifinite domain *}
   1.221 -
   1.222 -instantiation "+" :: (profinite, profinite) profinite
   1.223 -begin
   1.224 -
   1.225 -definition
   1.226 -  approx_sum_def: "approx =
   1.227 -    (\<lambda>n. \<Lambda> x. case x of Inl a \<Rightarrow> Inl (approx n\<cdot>a) | Inr b \<Rightarrow> Inr (approx n\<cdot>b))"
   1.228 -
   1.229 -lemma approx_Inl [simp]: "approx n\<cdot>(Inl x) = Inl (approx n\<cdot>x)"
   1.230 -  unfolding approx_sum_def by simp
   1.231 -
   1.232 -lemma approx_Inr [simp]: "approx n\<cdot>(Inr x) = Inr (approx n\<cdot>x)"
   1.233 -  unfolding approx_sum_def by simp
   1.234 -
   1.235 -instance proof
   1.236 -  fix i :: nat and x :: "'a + 'b"
   1.237 -  show "chain (approx :: nat \<Rightarrow> 'a + 'b \<rightarrow> 'a + 'b)"
   1.238 -    unfolding approx_sum_def
   1.239 -    by (rule ch2ch_LAM, case_tac x, simp_all)
   1.240 -  show "(\<Squnion>i. approx i\<cdot>x) = x"
   1.241 -    by (induct x, simp_all add: lub_Inl lub_Inr)
   1.242 -  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   1.243 -    by (induct x, simp_all)
   1.244 -  have "{x::'a + 'b. approx i\<cdot>x = x} \<subseteq>
   1.245 -        {x::'a. approx i\<cdot>x = x} <+> {x::'b. approx i\<cdot>x = x}"
   1.246 -    by (rule subsetI, case_tac x, simp_all add: InlI InrI)
   1.247 -  thus "finite {x::'a + 'b. approx i\<cdot>x = x}"
   1.248 -    by (rule finite_subset,
   1.249 -        intro finite_Plus finite_fixes_approx)
   1.250 -qed
   1.251 -
   1.252 -end
   1.253 -
   1.254 -end