src/HOL/HOLCF/Porder.thy
changeset 40774 0437dbc127b3
parent 40771 1c6f7d4b110e
child 41182 717404c7d59a
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/Porder.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,336 @@
     1.4 +(*  Title:      HOLCF/Porder.thy
     1.5 +    Author:     Franz Regensburger and Brian Huffman
     1.6 +*)
     1.7 +
     1.8 +header {* Partial orders *}
     1.9 +
    1.10 +theory Porder
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +subsection {* Type class for partial orders *}
    1.15 +
    1.16 +class below =
    1.17 +  fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.18 +begin
    1.19 +
    1.20 +notation
    1.21 +  below (infix "<<" 50)
    1.22 +
    1.23 +notation (xsymbols)
    1.24 +  below (infix "\<sqsubseteq>" 50)
    1.25 +
    1.26 +lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
    1.27 +  by (rule subst)
    1.28 +
    1.29 +lemma eq_below_trans: "\<lbrakk>a = b; b \<sqsubseteq> c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
    1.30 +  by (rule ssubst)
    1.31 +
    1.32 +end
    1.33 +
    1.34 +class po = below +
    1.35 +  assumes below_refl [iff]: "x \<sqsubseteq> x"
    1.36 +  assumes below_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z"
    1.37 +  assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y"
    1.38 +begin
    1.39 +
    1.40 +lemma eq_imp_below: "x = y \<Longrightarrow> x \<sqsubseteq> y"
    1.41 +  by simp
    1.42 +
    1.43 +lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d"
    1.44 +  by (rule below_trans [OF below_trans])
    1.45 +
    1.46 +lemma po_eq_conv: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x"
    1.47 +  by (fast intro!: below_antisym)
    1.48 +
    1.49 +lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
    1.50 +  by (rule below_trans)
    1.51 +
    1.52 +lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
    1.53 +  by auto
    1.54 +
    1.55 +end
    1.56 +
    1.57 +lemmas HOLCF_trans_rules [trans] =
    1.58 +  below_trans
    1.59 +  below_antisym
    1.60 +  below_eq_trans
    1.61 +  eq_below_trans
    1.62 +
    1.63 +context po
    1.64 +begin
    1.65 +
    1.66 +subsection {* Upper bounds *}
    1.67 +
    1.68 +definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55) where
    1.69 +  "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)"
    1.70 +
    1.71 +lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u"
    1.72 +  by (simp add: is_ub_def)
    1.73 +
    1.74 +lemma is_ubD: "\<lbrakk>S <| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
    1.75 +  by (simp add: is_ub_def)
    1.76 +
    1.77 +lemma ub_imageI: "(\<And>x. x \<in> S \<Longrightarrow> f x \<sqsubseteq> u) \<Longrightarrow> (\<lambda>x. f x) ` S <| u"
    1.78 +  unfolding is_ub_def by fast
    1.79 +
    1.80 +lemma ub_imageD: "\<lbrakk>f ` S <| u; x \<in> S\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> u"
    1.81 +  unfolding is_ub_def by fast
    1.82 +
    1.83 +lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x"
    1.84 +  unfolding is_ub_def by fast
    1.85 +
    1.86 +lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x"
    1.87 +  unfolding is_ub_def by fast
    1.88 +
    1.89 +lemma is_ub_empty [simp]: "{} <| u"
    1.90 +  unfolding is_ub_def by fast
    1.91 +
    1.92 +lemma is_ub_insert [simp]: "(insert x A) <| y = (x \<sqsubseteq> y \<and> A <| y)"
    1.93 +  unfolding is_ub_def by fast
    1.94 +
    1.95 +lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y"
    1.96 +  unfolding is_ub_def by (fast intro: below_trans)
    1.97 +
    1.98 +subsection {* Least upper bounds *}
    1.99 +
   1.100 +definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55) where
   1.101 +  "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)"
   1.102 +
   1.103 +definition lub :: "'a set \<Rightarrow> 'a" where
   1.104 +  "lub S = (THE x. S <<| x)"
   1.105 +
   1.106 +end
   1.107 +
   1.108 +syntax
   1.109 +  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3LUB _:_./ _)" [0,0, 10] 10)
   1.110 +
   1.111 +syntax (xsymbols)
   1.112 +  "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10)
   1.113 +
   1.114 +translations
   1.115 +  "LUB x:A. t" == "CONST lub ((%x. t) ` A)"
   1.116 +
   1.117 +context po
   1.118 +begin
   1.119 +
   1.120 +abbreviation
   1.121 +  Lub  (binder "LUB " 10) where
   1.122 +  "LUB n. t n == lub (range t)"
   1.123 +
   1.124 +notation (xsymbols)
   1.125 +  Lub  (binder "\<Squnion> " 10)
   1.126 +
   1.127 +text {* access to some definition as inference rule *}
   1.128 +
   1.129 +lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x"
   1.130 +  unfolding is_lub_def by fast
   1.131 +
   1.132 +lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u"
   1.133 +  unfolding is_lub_def by fast
   1.134 +
   1.135 +lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x"
   1.136 +  unfolding is_lub_def by fast
   1.137 +
   1.138 +lemma is_lub_below_iff: "S <<| x \<Longrightarrow> x \<sqsubseteq> u \<longleftrightarrow> S <| u"
   1.139 +  unfolding is_lub_def is_ub_def by (metis below_trans)
   1.140 +
   1.141 +text {* lubs are unique *}
   1.142 +
   1.143 +lemma is_lub_unique: "\<lbrakk>S <<| x; S <<| y\<rbrakk> \<Longrightarrow> x = y"
   1.144 +  unfolding is_lub_def is_ub_def by (blast intro: below_antisym)
   1.145 +
   1.146 +text {* technical lemmas about @{term lub} and @{term is_lub} *}
   1.147 +
   1.148 +lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M"
   1.149 +  unfolding lub_def by (rule theI [OF _ is_lub_unique])
   1.150 +
   1.151 +lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l"
   1.152 +  by (rule is_lub_unique [OF is_lub_lub])
   1.153 +
   1.154 +lemma is_lub_singleton: "{x} <<| x"
   1.155 +  by (simp add: is_lub_def)
   1.156 +
   1.157 +lemma lub_singleton [simp]: "lub {x} = x"
   1.158 +  by (rule is_lub_singleton [THEN lub_eqI])
   1.159 +
   1.160 +lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y"
   1.161 +  by (simp add: is_lub_def)
   1.162 +
   1.163 +lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y"
   1.164 +  by (rule is_lub_bin [THEN lub_eqI])
   1.165 +
   1.166 +lemma is_lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> S <<| x"
   1.167 +  by (erule is_lubI, erule (1) is_ubD)
   1.168 +
   1.169 +lemma lub_maximal: "\<lbrakk>S <| x; x \<in> S\<rbrakk> \<Longrightarrow> lub S = x"
   1.170 +  by (rule is_lub_maximal [THEN lub_eqI])
   1.171 +
   1.172 +subsection {* Countable chains *}
   1.173 +
   1.174 +definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.175 +  -- {* Here we use countable chains and I prefer to code them as functions! *}
   1.176 +  "chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))"
   1.177 +
   1.178 +lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y"
   1.179 +  unfolding chain_def by fast
   1.180 +
   1.181 +lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)"
   1.182 +  unfolding chain_def by fast
   1.183 +
   1.184 +text {* chains are monotone functions *}
   1.185 +
   1.186 +lemma chain_mono_less: "\<lbrakk>chain Y; i < j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
   1.187 +  by (erule less_Suc_induct, erule chainE, erule below_trans)
   1.188 +
   1.189 +lemma chain_mono: "\<lbrakk>chain Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i \<sqsubseteq> Y j"
   1.190 +  by (cases "i = j", simp, simp add: chain_mono_less)
   1.191 +
   1.192 +lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))"
   1.193 +  by (rule chainI, simp, erule chainE)
   1.194 +
   1.195 +text {* technical lemmas about (least) upper bounds of chains *}
   1.196 +
   1.197 +lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x"
   1.198 +  by (rule is_lubD1 [THEN ub_rangeD])
   1.199 +
   1.200 +lemma is_ub_range_shift:
   1.201 +  "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x"
   1.202 +apply (rule iffI)
   1.203 +apply (rule ub_rangeI)
   1.204 +apply (rule_tac y="S (i + j)" in below_trans)
   1.205 +apply (erule chain_mono)
   1.206 +apply (rule le_add1)
   1.207 +apply (erule ub_rangeD)
   1.208 +apply (rule ub_rangeI)
   1.209 +apply (erule ub_rangeD)
   1.210 +done
   1.211 +
   1.212 +lemma is_lub_range_shift:
   1.213 +  "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x"
   1.214 +  by (simp add: is_lub_def is_ub_range_shift)
   1.215 +
   1.216 +text {* the lub of a constant chain is the constant *}
   1.217 +
   1.218 +lemma chain_const [simp]: "chain (\<lambda>i. c)"
   1.219 +  by (simp add: chainI)
   1.220 +
   1.221 +lemma is_lub_const: "range (\<lambda>x. c) <<| c"
   1.222 +by (blast dest: ub_rangeD intro: is_lubI ub_rangeI)
   1.223 +
   1.224 +lemma lub_const [simp]: "(\<Squnion>i. c) = c"
   1.225 +  by (rule is_lub_const [THEN lub_eqI])
   1.226 +
   1.227 +subsection {* Finite chains *}
   1.228 +
   1.229 +definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.230 +  -- {* finite chains, needed for monotony of continuous functions *}
   1.231 +  "max_in_chain i C \<longleftrightarrow> (\<forall>j. i \<le> j \<longrightarrow> C i = C j)"
   1.232 +
   1.233 +definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" where
   1.234 +  "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))"
   1.235 +
   1.236 +text {* results about finite chains *}
   1.237 +
   1.238 +lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y"
   1.239 +  unfolding max_in_chain_def by fast
   1.240 +
   1.241 +lemma max_in_chainD: "\<lbrakk>max_in_chain i Y; i \<le> j\<rbrakk> \<Longrightarrow> Y i = Y j"
   1.242 +  unfolding max_in_chain_def by fast
   1.243 +
   1.244 +lemma finite_chainI:
   1.245 +  "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> finite_chain C"
   1.246 +  unfolding finite_chain_def by fast
   1.247 +
   1.248 +lemma finite_chainE:
   1.249 +  "\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R"
   1.250 +  unfolding finite_chain_def by fast
   1.251 +
   1.252 +lemma lub_finch1: "\<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> range C <<| C i"
   1.253 +apply (rule is_lubI)
   1.254 +apply (rule ub_rangeI, rename_tac j)
   1.255 +apply (rule_tac x=i and y=j in linorder_le_cases)
   1.256 +apply (drule (1) max_in_chainD, simp)
   1.257 +apply (erule (1) chain_mono)
   1.258 +apply (erule ub_rangeD)
   1.259 +done
   1.260 +
   1.261 +lemma lub_finch2:
   1.262 +  "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)"
   1.263 +apply (erule finite_chainE)
   1.264 +apply (erule LeastI2 [where Q="\<lambda>i. range C <<| C i"])
   1.265 +apply (erule (1) lub_finch1)
   1.266 +done
   1.267 +
   1.268 +lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)"
   1.269 + apply (erule finite_chainE)
   1.270 + apply (rule_tac B="Y ` {..i}" in finite_subset)
   1.271 +  apply (rule subsetI)
   1.272 +  apply (erule rangeE, rename_tac j)
   1.273 +  apply (rule_tac x=i and y=j in linorder_le_cases)
   1.274 +   apply (subgoal_tac "Y j = Y i", simp)
   1.275 +   apply (simp add: max_in_chain_def)
   1.276 +  apply simp
   1.277 + apply simp
   1.278 +done
   1.279 +
   1.280 +lemma finite_range_has_max:
   1.281 +  fixes f :: "nat \<Rightarrow> 'a" and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.282 +  assumes mono: "\<And>i j. i \<le> j \<Longrightarrow> r (f i) (f j)"
   1.283 +  assumes finite_range: "finite (range f)"
   1.284 +  shows "\<exists>k. \<forall>i. r (f i) (f k)"
   1.285 +proof (intro exI allI)
   1.286 +  fix i :: nat
   1.287 +  let ?j = "LEAST k. f k = f i"
   1.288 +  let ?k = "Max ((\<lambda>x. LEAST k. f k = x) ` range f)"
   1.289 +  have "?j \<le> ?k"
   1.290 +  proof (rule Max_ge)
   1.291 +    show "finite ((\<lambda>x. LEAST k. f k = x) ` range f)"
   1.292 +      using finite_range by (rule finite_imageI)
   1.293 +    show "?j \<in> (\<lambda>x. LEAST k. f k = x) ` range f"
   1.294 +      by (intro imageI rangeI)
   1.295 +  qed
   1.296 +  hence "r (f ?j) (f ?k)"
   1.297 +    by (rule mono)
   1.298 +  also have "f ?j = f i"
   1.299 +    by (rule LeastI, rule refl)
   1.300 +  finally show "r (f i) (f ?k)" .
   1.301 +qed
   1.302 +
   1.303 +lemma finite_range_imp_finch:
   1.304 +  "\<lbrakk>chain Y; finite (range Y)\<rbrakk> \<Longrightarrow> finite_chain Y"
   1.305 + apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k")
   1.306 +  apply (erule exE)
   1.307 +  apply (rule finite_chainI, assumption)
   1.308 +  apply (rule max_in_chainI)
   1.309 +  apply (rule below_antisym)
   1.310 +   apply (erule (1) chain_mono)
   1.311 +  apply (erule spec)
   1.312 + apply (rule finite_range_has_max)
   1.313 +  apply (erule (1) chain_mono)
   1.314 + apply assumption
   1.315 +done
   1.316 +
   1.317 +lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)"
   1.318 +  by (rule chainI, simp)
   1.319 +
   1.320 +lemma bin_chainmax:
   1.321 +  "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)"
   1.322 +  unfolding max_in_chain_def by simp
   1.323 +
   1.324 +lemma is_lub_bin_chain:
   1.325 +  "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y"
   1.326 +apply (frule bin_chain)
   1.327 +apply (drule bin_chainmax)
   1.328 +apply (drule (1) lub_finch1)
   1.329 +apply simp
   1.330 +done
   1.331 +
   1.332 +text {* the maximal element in a chain is its lub *}
   1.333 +
   1.334 +lemma lub_chain_maxelem: "\<lbrakk>Y i = c; \<forall>i. Y i \<sqsubseteq> c\<rbrakk> \<Longrightarrow> lub (range Y) = c"
   1.335 +  by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI)
   1.336 +
   1.337 +end
   1.338 +
   1.339 +end