1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOLCF/Bifinite.thy Mon Jan 14 19:26:01 2008 +0100
1.3 @@ -0,0 +1,198 @@
1.4 +(* Title: HOLCF/Bifinite.thy
1.5 + ID: $Id$
1.6 + Author: Brian Huffman
1.7 +*)
1.8 +
1.9 +header {* Bifinite domains and approximation *}
1.10 +
1.11 +theory Bifinite
1.12 +imports Cfun
1.13 +begin
1.14 +
1.15 +subsection {* Bifinite domains *}
1.16 +
1.17 +axclass approx < pcpo
1.18 +
1.19 +consts approx :: "nat \<Rightarrow> 'a::approx \<rightarrow> 'a"
1.20 +
1.21 +axclass bifinite < approx
1.22 + chain_approx_app: "chain (\<lambda>i. approx i\<cdot>x)"
1.23 + lub_approx_app [simp]: "(\<Squnion>i. approx i\<cdot>x) = x"
1.24 + approx_idem: "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
1.25 + finite_fixes_approx: "finite {x. approx i\<cdot>x = x}"
1.26 +
1.27 +lemma finite_range_imp_finite_fixes:
1.28 + "finite {x. \<exists>y. x = f y} \<Longrightarrow> finite {x. f x = x}"
1.29 +apply (subgoal_tac "{x. f x = x} \<subseteq> {x. \<exists>y. x = f y}")
1.30 +apply (erule (1) finite_subset)
1.31 +apply (clarify, erule subst, rule exI, rule refl)
1.32 +done
1.33 +
1.34 +lemma chain_approx [simp]:
1.35 + "chain (approx :: nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a)"
1.36 +apply (rule chainI)
1.37 +apply (rule less_cfun_ext)
1.38 +apply (rule chainE)
1.39 +apply (rule chain_approx_app)
1.40 +done
1.41 +
1.42 +lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda>(x::'a::bifinite). x)"
1.43 +by (rule ext_cfun, simp add: contlub_cfun_fun)
1.44 +
1.45 +lemma approx_less: "approx i\<cdot>x \<sqsubseteq> (x::'a::bifinite)"
1.46 +apply (subgoal_tac "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)", simp)
1.47 +apply (rule is_ub_thelub, simp)
1.48 +done
1.49 +
1.50 +lemma approx_strict [simp]: "approx i\<cdot>(\<bottom>::'a::bifinite) = \<bottom>"
1.51 +by (rule UU_I, rule approx_less)
1.52 +
1.53 +lemma approx_approx1:
1.54 + "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>(x::'a::bifinite)"
1.55 +apply (rule antisym_less)
1.56 +apply (rule monofun_cfun_arg [OF approx_less])
1.57 +apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
1.58 +apply (rule monofun_cfun_arg)
1.59 +apply (rule monofun_cfun_fun)
1.60 +apply (erule chain_mono3 [OF chain_approx])
1.61 +done
1.62 +
1.63 +lemma approx_approx2:
1.64 + "j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>(x::'a::bifinite)"
1.65 +apply (rule antisym_less)
1.66 +apply (rule approx_less)
1.67 +apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
1.68 +apply (rule monofun_cfun_fun)
1.69 +apply (erule chain_mono3 [OF chain_approx])
1.70 +done
1.71 +
1.72 +lemma approx_approx [simp]:
1.73 + "approx i\<cdot>(approx j\<cdot>x) = approx (min i j)\<cdot>(x::'a::bifinite)"
1.74 +apply (rule_tac x=i and y=j in linorder_le_cases)
1.75 +apply (simp add: approx_approx1 min_def)
1.76 +apply (simp add: approx_approx2 min_def)
1.77 +done
1.78 +
1.79 +lemma idem_fixes_eq_range:
1.80 + "\<forall>x. f (f x) = f x \<Longrightarrow> {x. f x = x} = {y. \<exists>x. y = f x}"
1.81 +by (auto simp add: eq_sym_conv)
1.82 +
1.83 +lemma finite_approx: "finite {y::'a::bifinite. \<exists>x. y = approx n\<cdot>x}"
1.84 +using finite_fixes_approx by (simp add: idem_fixes_eq_range)
1.85 +
1.86 +lemma finite_range_approx:
1.87 + "finite (range (\<lambda>x::'a::bifinite. approx n\<cdot>x))"
1.88 +by (simp add: image_def finite_approx)
1.89 +
1.90 +lemma compact_approx [simp]:
1.91 + fixes x :: "'a::bifinite"
1.92 + shows "compact (approx n\<cdot>x)"
1.93 +proof (rule compactI2)
1.94 + fix Y::"nat \<Rightarrow> 'a"
1.95 + assume Y: "chain Y"
1.96 + have "finite_chain (\<lambda>i. approx n\<cdot>(Y i))"
1.97 + proof (rule finite_range_imp_finch)
1.98 + show "chain (\<lambda>i. approx n\<cdot>(Y i))"
1.99 + using Y by simp
1.100 + have "range (\<lambda>i. approx n\<cdot>(Y i)) \<subseteq> {x. approx n\<cdot>x = x}"
1.101 + by clarsimp
1.102 + thus "finite (range (\<lambda>i. approx n\<cdot>(Y i)))"
1.103 + using finite_fixes_approx by (rule finite_subset)
1.104 + qed
1.105 + hence "\<exists>j. (\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)"
1.106 + by (simp add: finite_chain_def maxinch_is_thelub Y)
1.107 + then obtain j where j: "(\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)" ..
1.108 +
1.109 + assume "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
1.110 + hence "approx n\<cdot>(approx n\<cdot>x) \<sqsubseteq> approx n\<cdot>(\<Squnion>i. Y i)"
1.111 + by (rule monofun_cfun_arg)
1.112 + hence "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. approx n\<cdot>(Y i))"
1.113 + by (simp add: contlub_cfun_arg Y)
1.114 + hence "approx n\<cdot>x \<sqsubseteq> approx n\<cdot>(Y j)"
1.115 + using j by simp
1.116 + hence "approx n\<cdot>x \<sqsubseteq> Y j"
1.117 + using approx_less by (rule trans_less)
1.118 + thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" ..
1.119 +qed
1.120 +
1.121 +lemma bifinite_compact_eq_approx:
1.122 + fixes x :: "'a::bifinite"
1.123 + assumes x: "compact x"
1.124 + shows "\<exists>i. approx i\<cdot>x = x"
1.125 +proof -
1.126 + have chain: "chain (\<lambda>i. approx i\<cdot>x)" by simp
1.127 + have less: "x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by simp
1.128 + obtain i where i: "x \<sqsubseteq> approx i\<cdot>x"
1.129 + using compactD2 [OF x chain less] ..
1.130 + with approx_less have "approx i\<cdot>x = x"
1.131 + by (rule antisym_less)
1.132 + thus "\<exists>i. approx i\<cdot>x = x" ..
1.133 +qed
1.134 +
1.135 +lemma bifinite_compact_iff:
1.136 + "compact (x::'a::bifinite) = (\<exists>n. approx n\<cdot>x = x)"
1.137 + apply (rule iffI)
1.138 + apply (erule bifinite_compact_eq_approx)
1.139 + apply (erule exE)
1.140 + apply (erule subst)
1.141 + apply (rule compact_approx)
1.142 +done
1.143 +
1.144 +lemma approx_induct:
1.145 + assumes adm: "adm P" and P: "\<And>n x. P (approx n\<cdot>x)"
1.146 + shows "P (x::'a::bifinite)"
1.147 +proof -
1.148 + have "P (\<Squnion>n. approx n\<cdot>x)"
1.149 + by (rule admD [OF adm], simp, simp add: P)
1.150 + thus "P x" by simp
1.151 +qed
1.152 +
1.153 +lemma bifinite_less_ext:
1.154 + fixes x y :: "'a::bifinite"
1.155 + shows "(\<And>i. approx i\<cdot>x \<sqsubseteq> approx i\<cdot>y) \<Longrightarrow> x \<sqsubseteq> y"
1.156 +apply (subgoal_tac "(\<Squnion>i. approx i\<cdot>x) \<sqsubseteq> (\<Squnion>i. approx i\<cdot>y)", simp)
1.157 +apply (rule lub_mono [rule_format], simp, simp, simp)
1.158 +done
1.159 +
1.160 +subsection {* Instance for continuous function space *}
1.161 +
1.162 +lemma finite_range_lemma:
1.163 + fixes h :: "'a::cpo \<rightarrow> 'b::cpo"
1.164 + fixes k :: "'c::cpo \<rightarrow> 'd::cpo"
1.165 + shows "\<lbrakk>finite {y. \<exists>x. y = h\<cdot>x}; finite {y. \<exists>x. y = k\<cdot>x}\<rbrakk>
1.166 + \<Longrightarrow> finite {g. \<exists>f. g = (\<Lambda> x. k\<cdot>(f\<cdot>(h\<cdot>x)))}"
1.167 + apply (rule_tac f="\<lambda>g. {(h\<cdot>x, y) |x y. y = g\<cdot>x}" in finite_imageD)
1.168 + apply (rule_tac B="Pow ({y. \<exists>x. y = h\<cdot>x} \<times> {y. \<exists>x. y = k\<cdot>x})"
1.169 + in finite_subset)
1.170 + apply (rule image_subsetI)
1.171 + apply (clarsimp, fast)
1.172 + apply simp
1.173 + apply (rule inj_onI)
1.174 + apply (clarsimp simp add: expand_set_eq)
1.175 + apply (rule ext_cfun, simp)
1.176 + apply (drule_tac x="h\<cdot>x" in spec)
1.177 + apply (drule_tac x="k\<cdot>(f\<cdot>(h\<cdot>x))" in spec)
1.178 + apply (drule iffD1, fast)
1.179 + apply clarsimp
1.180 +done
1.181 +
1.182 +instance "->" :: (bifinite, bifinite) approx ..
1.183 +
1.184 +defs (overloaded)
1.185 + approx_cfun_def:
1.186 + "approx \<equiv> \<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
1.187 +
1.188 +instance "->" :: (bifinite, bifinite) bifinite
1.189 + apply (intro_classes, unfold approx_cfun_def)
1.190 + apply simp
1.191 + apply (simp add: lub_distribs eta_cfun)
1.192 + apply simp
1.193 + apply simp
1.194 + apply (rule finite_range_imp_finite_fixes)
1.195 + apply (intro finite_range_lemma finite_approx)
1.196 +done
1.197 +
1.198 +lemma approx_cfun: "approx n\<cdot>f\<cdot>x = approx n\<cdot>(f\<cdot>(approx n\<cdot>x))"
1.199 +by (simp add: approx_cfun_def)
1.200 +
1.201 +end