reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
authorhuffman
Mon Jun 30 22:16:47 2008 +0200 (2008-06-30)
changeset 27402253a06dfadce
parent 27401 4edc81f93e35
child 27403 0fb81286c88f
reuse proofs from Deflation.thy; clean up proof of finite_range_cfun_lemma
src/HOLCF/Bifinite.thy
     1.1 --- a/src/HOLCF/Bifinite.thy	Mon Jun 30 21:52:17 2008 +0200
     1.2 +++ b/src/HOLCF/Bifinite.thy	Mon Jun 30 22:16:47 2008 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Bifinite domains and approximation *}
     1.5  
     1.6  theory Bifinite
     1.7 -imports Cfun
     1.8 +imports Deflation
     1.9  begin
    1.10  
    1.11  subsection {* Omega-profinite and bifinite domains *}
    1.12 @@ -20,40 +20,45 @@
    1.13  
    1.14  class bifinite = profinite + pcpo
    1.15  
    1.16 -lemma finite_range_imp_finite_fixes:
    1.17 -  "finite {x. \<exists>y. x = f y} \<Longrightarrow> finite {x. f x = x}"
    1.18 -apply (subgoal_tac "{x. f x = x} \<subseteq> {x. \<exists>y. x = f y}")
    1.19 -apply (erule (1) finite_subset)
    1.20 -apply (clarify, erule subst, rule exI, rule refl)
    1.21 -done
    1.22 +lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x"
    1.23 +proof -
    1.24 +  have "chain (\<lambda>i. approx i\<cdot>x)" by simp
    1.25 +  hence "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)" by (rule is_ub_thelub)
    1.26 +  thus "approx i\<cdot>x \<sqsubseteq> x" by simp
    1.27 +qed
    1.28 +
    1.29 +lemma finite_deflation_approx: "finite_deflation (approx i)"
    1.30 +proof
    1.31 +  fix x :: 'a
    1.32 +  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
    1.33 +    by (rule approx_idem)
    1.34 +  show "approx i\<cdot>x \<sqsubseteq> x"
    1.35 +    by (rule approx_less)
    1.36 +  show "finite {x. approx i\<cdot>x = x}"
    1.37 +    by (rule finite_fixes_approx)
    1.38 +qed
    1.39 +
    1.40 +interpretation approx: finite_deflation ["approx i"]
    1.41 +by (rule finite_deflation_approx)
    1.42 +
    1.43 +lemma deflation_approx: "deflation (approx i)"
    1.44 +by (rule approx.deflation_axioms)
    1.45  
    1.46  lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
    1.47  by (rule ext_cfun, simp add: contlub_cfun_fun)
    1.48  
    1.49 -lemma approx_less: "approx i\<cdot>x \<sqsubseteq> x"
    1.50 -apply (subgoal_tac "approx i\<cdot>x \<sqsubseteq> (\<Squnion>i. approx i\<cdot>x)", simp)
    1.51 -apply (rule is_ub_thelub, simp)
    1.52 -done
    1.53 -
    1.54  lemma approx_strict [simp]: "approx i\<cdot>\<bottom> = \<bottom>"
    1.55  by (rule UU_I, rule approx_less)
    1.56  
    1.57  lemma approx_approx1:
    1.58    "i \<le> j \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx i\<cdot>x"
    1.59 -apply (rule antisym_less)
    1.60 -apply (rule monofun_cfun_arg [OF approx_less])
    1.61 -apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
    1.62 -apply (rule monofun_cfun_arg)
    1.63 -apply (rule monofun_cfun_fun)
    1.64 +apply (rule deflation_less_comp1 [OF deflation_approx deflation_approx])
    1.65  apply (erule chain_mono [OF chain_approx])
    1.66  done
    1.67  
    1.68  lemma approx_approx2:
    1.69    "j \<le> i \<Longrightarrow> approx i\<cdot>(approx j\<cdot>x) = approx j\<cdot>x"
    1.70 -apply (rule antisym_less)
    1.71 -apply (rule approx_less)
    1.72 -apply (rule sq_ord_eq_less_trans [OF approx_idem [symmetric]])
    1.73 -apply (rule monofun_cfun_fun)
    1.74 +apply (rule deflation_less_comp2 [OF deflation_approx deflation_approx])
    1.75  apply (erule chain_mono [OF chain_approx])
    1.76  done
    1.77  
    1.78 @@ -64,50 +69,17 @@
    1.79  apply (simp add: approx_approx2 min_def)
    1.80  done
    1.81  
    1.82 -lemma idem_fixes_eq_range:
    1.83 -  "\<forall>x. f (f x) = f x \<Longrightarrow> {x. f x = x} = {y. \<exists>x. y = f x}"
    1.84 -by (auto simp add: eq_sym_conv)
    1.85 +lemma finite_image_approx: "finite ((\<lambda>x. approx n\<cdot>x) ` A)"
    1.86 +by (rule approx.finite_image)
    1.87  
    1.88 -lemma finite_approx: "finite {y. \<exists>x. y = approx n\<cdot>x}"
    1.89 -using finite_fixes_approx by (simp add: idem_fixes_eq_range)
    1.90 -
    1.91 -lemma finite_image_approx: "finite ((\<lambda>x. approx n\<cdot>x) ` A)"
    1.92 -by (rule finite_subset [OF _ finite_fixes_approx [where i=n]]) auto
    1.93 -
    1.94 -lemma finite_range_approx: "finite (range (\<lambda>x. approx n\<cdot>x))"
    1.95 -by (rule finite_image_approx)
    1.96 +lemma finite_range_approx: "finite (range (\<lambda>x. approx i\<cdot>x))"
    1.97 +by (rule approx.finite_range)
    1.98  
    1.99  lemma compact_approx [simp]: "compact (approx n\<cdot>x)"
   1.100 -proof (rule compactI2)
   1.101 -  fix Y::"nat \<Rightarrow> 'a"
   1.102 -  assume Y: "chain Y"
   1.103 -  have "finite_chain (\<lambda>i. approx n\<cdot>(Y i))"
   1.104 -  proof (rule finite_range_imp_finch)
   1.105 -    show "chain (\<lambda>i. approx n\<cdot>(Y i))"
   1.106 -      using Y by simp
   1.107 -    have "range (\<lambda>i. approx n\<cdot>(Y i)) \<subseteq> {x. approx n\<cdot>x = x}"
   1.108 -      by clarsimp
   1.109 -    thus "finite (range (\<lambda>i. approx n\<cdot>(Y i)))"
   1.110 -      using finite_fixes_approx by (rule finite_subset)
   1.111 -  qed
   1.112 -  hence "\<exists>j. (\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)"
   1.113 -    by (simp add: finite_chain_def maxinch_is_thelub Y)
   1.114 -  then obtain j where j: "(\<Squnion>i. approx n\<cdot>(Y i)) = approx n\<cdot>(Y j)" ..
   1.115 -
   1.116 -  assume "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. Y i)"
   1.117 -  hence "approx n\<cdot>(approx n\<cdot>x) \<sqsubseteq> approx n\<cdot>(\<Squnion>i. Y i)"
   1.118 -    by (rule monofun_cfun_arg)
   1.119 -  hence "approx n\<cdot>x \<sqsubseteq> (\<Squnion>i. approx n\<cdot>(Y i))"
   1.120 -    by (simp add: contlub_cfun_arg Y)
   1.121 -  hence "approx n\<cdot>x \<sqsubseteq> approx n\<cdot>(Y j)"
   1.122 -    using j by simp
   1.123 -  hence "approx n\<cdot>x \<sqsubseteq> Y j"
   1.124 -    using approx_less by (rule trans_less)
   1.125 -  thus "\<exists>j. approx n\<cdot>x \<sqsubseteq> Y j" ..
   1.126 -qed
   1.127 +by (rule approx.compact)
   1.128  
   1.129  lemma profinite_compact_eq_approx: "compact x \<Longrightarrow> \<exists>i. approx i\<cdot>x = x"
   1.130 -by (rule admD2) simp_all
   1.131 +by (rule admD2, simp_all)
   1.132  
   1.133  lemma profinite_compact_iff: "compact x \<longleftrightarrow> (\<exists>n. approx n\<cdot>x = x)"
   1.134   apply (rule iffI)
   1.135 @@ -133,25 +105,34 @@
   1.136  
   1.137  subsection {* Instance for continuous function space *}
   1.138  
   1.139 -lemma finite_range_lemma:
   1.140 -  fixes h :: "'a::cpo \<rightarrow> 'b::cpo"
   1.141 -  fixes k :: "'c::cpo \<rightarrow> 'd::cpo"
   1.142 -  shows "\<lbrakk>finite {y. \<exists>x. y = h\<cdot>x}; finite {y. \<exists>x. y = k\<cdot>x}\<rbrakk>
   1.143 -    \<Longrightarrow> finite {g. \<exists>f. g = (\<Lambda> x. k\<cdot>(f\<cdot>(h\<cdot>x)))}"
   1.144 - apply (rule_tac f="\<lambda>g. {(h\<cdot>x, y) |x y. y = g\<cdot>x}" in finite_imageD)
   1.145 -  apply (rule_tac B="Pow ({y. \<exists>x. y = h\<cdot>x} \<times> {y. \<exists>x. y = k\<cdot>x})"
   1.146 -           in finite_subset)
   1.147 -   apply (rule image_subsetI)
   1.148 -   apply (clarsimp, fast)
   1.149 -  apply simp
   1.150 - apply (rule inj_onI)
   1.151 - apply (clarsimp simp add: expand_set_eq)
   1.152 - apply (rule ext_cfun, simp)
   1.153 - apply (drule_tac x="h\<cdot>x" in spec)
   1.154 - apply (drule_tac x="k\<cdot>(f\<cdot>(h\<cdot>x))" in spec)
   1.155 - apply (drule iffD1, fast)
   1.156 - apply clarsimp
   1.157 -done
   1.158 +lemma finite_range_cfun_lemma:
   1.159 +  assumes a: "finite (range (\<lambda>x. a\<cdot>x))"
   1.160 +  assumes b: "finite (range (\<lambda>y. b\<cdot>y))"
   1.161 +  shows "finite (range (\<lambda>f. \<Lambda> x. b\<cdot>(f\<cdot>(a\<cdot>x))))"  (is "finite (range ?h)")
   1.162 +proof (rule finite_imageD)
   1.163 +  let ?f = "\<lambda>g. range (\<lambda>x. (a\<cdot>x, g\<cdot>x))"
   1.164 +  show "finite (?f ` range ?h)"
   1.165 +  proof (rule finite_subset)
   1.166 +    let ?B = "Pow (range (\<lambda>x. a\<cdot>x) \<times> range (\<lambda>y. b\<cdot>y))"
   1.167 +    show "?f ` range ?h \<subseteq> ?B"
   1.168 +      by clarsimp
   1.169 +    show "finite ?B"
   1.170 +      by (simp add: a b)
   1.171 +  qed
   1.172 +  show "inj_on ?f (range ?h)"
   1.173 +  proof (rule inj_onI, rule ext_cfun, clarsimp)
   1.174 +    fix x f g
   1.175 +    assume "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) = range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   1.176 +    hence "range (\<lambda>x. (a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x)))) \<subseteq> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   1.177 +      by (rule equalityD1)
   1.178 +    hence "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) \<in> range (\<lambda>x. (a\<cdot>x, b\<cdot>(g\<cdot>(a\<cdot>x))))"
   1.179 +      by (simp add: subset_eq)
   1.180 +    then obtain y where "(a\<cdot>x, b\<cdot>(f\<cdot>(a\<cdot>x))) = (a\<cdot>y, b\<cdot>(g\<cdot>(a\<cdot>y)))"
   1.181 +      by (rule rangeE)
   1.182 +    thus "b\<cdot>(f\<cdot>(a\<cdot>x)) = b\<cdot>(g\<cdot>(a\<cdot>x))"
   1.183 +      by clarsimp
   1.184 +  qed
   1.185 +qed
   1.186  
   1.187  instantiation "->" :: (profinite, profinite) profinite
   1.188  begin
   1.189 @@ -160,15 +141,26 @@
   1.190    approx_cfun_def:
   1.191      "approx = (\<lambda>n. \<Lambda> f x. approx n\<cdot>(f\<cdot>(approx n\<cdot>x)))"
   1.192  
   1.193 -instance
   1.194 - apply (intro_classes, unfold approx_cfun_def)
   1.195 -    apply simp
   1.196 -   apply (simp add: lub_distribs eta_cfun)
   1.197 -  apply simp
   1.198 - apply simp
   1.199 - apply (rule finite_range_imp_finite_fixes)
   1.200 - apply (intro finite_range_lemma finite_approx)
   1.201 -done
   1.202 +instance proof
   1.203 +  show "chain (approx :: nat \<Rightarrow> ('a \<rightarrow> 'b) \<rightarrow> ('a \<rightarrow> 'b))"
   1.204 +    unfolding approx_cfun_def by simp
   1.205 +next
   1.206 +  fix x :: "'a \<rightarrow> 'b"
   1.207 +  show "(\<Squnion>i. approx i\<cdot>x) = x"
   1.208 +    unfolding approx_cfun_def
   1.209 +    by (simp add: lub_distribs eta_cfun)
   1.210 +next
   1.211 +  fix i :: nat and x :: "'a \<rightarrow> 'b"
   1.212 +  show "approx i\<cdot>(approx i\<cdot>x) = approx i\<cdot>x"
   1.213 +    unfolding approx_cfun_def by simp
   1.214 +next
   1.215 +  fix i :: nat
   1.216 +  show "finite {x::'a \<rightarrow> 'b. approx i\<cdot>x = x}"
   1.217 +    apply (rule finite_range_imp_finite_fixes)
   1.218 +    apply (simp add: approx_cfun_def)
   1.219 +    apply (intro finite_range_cfun_lemma finite_range_approx)
   1.220 +    done
   1.221 +qed
   1.222  
   1.223  end
   1.224