1(* Title: HOL/HOLCF/Porder.thy 2 Author: Franz Regensburger and Brian Huffman 3*) 4 5section \<open>Partial orders\<close> 6 7theory Porder 8 imports Main 9begin 10 11declare [[typedef_overloaded]] 12 13 14subsection \<open>Type class for partial orders\<close> 15 16class below = 17 fixes below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 18begin 19 20notation (ASCII) 21 below (infix "<<" 50) 22 23notation 24 below (infix "\<sqsubseteq>" 50) 25 26abbreviation not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "\<notsqsubseteq>" 50) 27 where "not_below x y \<equiv> \<not> below x y" 28 29notation (ASCII) 30 not_below (infix "~<<" 50) 31 32lemma below_eq_trans: "a \<sqsubseteq> b \<Longrightarrow> b = c \<Longrightarrow> a \<sqsubseteq> c" 33 by (rule subst) 34 35lemma eq_below_trans: "a = b \<Longrightarrow> b \<sqsubseteq> c \<Longrightarrow> a \<sqsubseteq> c" 36 by (rule ssubst) 37 38end 39 40class po = below + 41 assumes below_refl [iff]: "x \<sqsubseteq> x" 42 assumes below_trans: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> z" 43 assumes below_antisym: "x \<sqsubseteq> y \<Longrightarrow> y \<sqsubseteq> x \<Longrightarrow> x = y" 44begin 45 46lemma eq_imp_below: "x = y \<Longrightarrow> x \<sqsubseteq> y" 47 by simp 48 49lemma box_below: "a \<sqsubseteq> b \<Longrightarrow> c \<sqsubseteq> a \<Longrightarrow> b \<sqsubseteq> d \<Longrightarrow> c \<sqsubseteq> d" 50 by (rule below_trans [OF below_trans]) 51 52lemma po_eq_conv: "x = y \<longleftrightarrow> x \<sqsubseteq> y \<and> y \<sqsubseteq> x" 53 by (fast intro!: below_antisym) 54 55lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z" 56 by (rule below_trans) 57 58lemma not_below2not_eq: "x \<notsqsubseteq> y \<Longrightarrow> x \<noteq> y" 59 by auto 60 61end 62 63lemmas HOLCF_trans_rules [trans] = 64 below_trans 65 below_antisym 66 below_eq_trans 67 eq_below_trans 68 69context po 70begin 71 72subsection \<open>Upper bounds\<close> 73 74definition is_ub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<|" 55) 75 where "S <| x \<longleftrightarrow> (\<forall>y\<in>S. y \<sqsubseteq> x)" 76 77lemma is_ubI: "(\<And>x. x \<in> S \<Longrightarrow> x \<sqsubseteq> u) \<Longrightarrow> S <| u" 78 by (simp add: is_ub_def) 79 80lemma is_ubD: "\<lbrakk>S <| u; x \<in> S\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" 81 by (simp add: is_ub_def) 82 83lemma ub_imageI: "(\<And>x. x \<in> S \<Longrightarrow> f x \<sqsubseteq> u) \<Longrightarrow> (\<lambda>x. f x) ` S <| u" 84 unfolding is_ub_def by fast 85 86lemma ub_imageD: "\<lbrakk>f ` S <| u; x \<in> S\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> u" 87 unfolding is_ub_def by fast 88 89lemma ub_rangeI: "(\<And>i. S i \<sqsubseteq> x) \<Longrightarrow> range S <| x" 90 unfolding is_ub_def by fast 91 92lemma ub_rangeD: "range S <| x \<Longrightarrow> S i \<sqsubseteq> x" 93 unfolding is_ub_def by fast 94 95lemma is_ub_empty [simp]: "{} <| u" 96 unfolding is_ub_def by fast 97 98lemma is_ub_insert [simp]: "(insert x A) <| y = (x \<sqsubseteq> y \<and> A <| y)" 99 unfolding is_ub_def by fast 100 101lemma is_ub_upward: "\<lbrakk>S <| x; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> S <| y" 102 unfolding is_ub_def by (fast intro: below_trans) 103 104 105subsection \<open>Least upper bounds\<close> 106 107definition is_lub :: "'a set \<Rightarrow> 'a \<Rightarrow> bool" (infix "<<|" 55) 108 where "S <<| x \<longleftrightarrow> S <| x \<and> (\<forall>u. S <| u \<longrightarrow> x \<sqsubseteq> u)" 109 110definition lub :: "'a set \<Rightarrow> 'a" 111 where "lub S = (THE x. S <<| x)" 112 113end 114 115syntax (ASCII) 116 "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3LUB _:_./ _)" [0,0, 10] 10) 117 118syntax 119 "_BLub" :: "[pttrn, 'a set, 'b] \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0,0, 10] 10) 120 121translations 122 "LUB x:A. t" \<rightleftharpoons> "CONST lub ((\<lambda>x. t) ` A)" 123 124context po 125begin 126 127abbreviation Lub (binder "\<Squnion>" 10) 128 where "\<Squnion>n. t n \<equiv> lub (range t)" 129 130notation (ASCII) 131 Lub (binder "LUB " 10) 132 133text \<open>access to some definition as inference rule\<close> 134 135lemma is_lubD1: "S <<| x \<Longrightarrow> S <| x" 136 unfolding is_lub_def by fast 137 138lemma is_lubD2: "\<lbrakk>S <<| x; S <| u\<rbrakk> \<Longrightarrow> x \<sqsubseteq> u" 139 unfolding is_lub_def by fast 140 141lemma is_lubI: "\<lbrakk>S <| x; \<And>u. S <| u \<Longrightarrow> x \<sqsubseteq> u\<rbrakk> \<Longrightarrow> S <<| x" 142 unfolding is_lub_def by fast 143 144lemma is_lub_below_iff: "S <<| x \<Longrightarrow> x \<sqsubseteq> u \<longleftrightarrow> S <| u" 145 unfolding is_lub_def is_ub_def by (metis below_trans) 146 147text \<open>lubs are unique\<close> 148 149lemma is_lub_unique: "S <<| x \<Longrightarrow> S <<| y \<Longrightarrow> x = y" 150 unfolding is_lub_def is_ub_def by (blast intro: below_antisym) 151 152text \<open>technical lemmas about @{term lub} and @{term is_lub}\<close> 153 154lemma is_lub_lub: "M <<| x \<Longrightarrow> M <<| lub M" 155 unfolding lub_def by (rule theI [OF _ is_lub_unique]) 156 157lemma lub_eqI: "M <<| l \<Longrightarrow> lub M = l" 158 by (rule is_lub_unique [OF is_lub_lub]) 159 160lemma is_lub_singleton: "{x} <<| x" 161 by (simp add: is_lub_def) 162 163lemma lub_singleton [simp]: "lub {x} = x" 164 by (rule is_lub_singleton [THEN lub_eqI]) 165 166lemma is_lub_bin: "x \<sqsubseteq> y \<Longrightarrow> {x, y} <<| y" 167 by (simp add: is_lub_def) 168 169lemma lub_bin: "x \<sqsubseteq> y \<Longrightarrow> lub {x, y} = y" 170 by (rule is_lub_bin [THEN lub_eqI]) 171 172lemma is_lub_maximal: "S <| x \<Longrightarrow> x \<in> S \<Longrightarrow> S <<| x" 173 by (erule is_lubI, erule (1) is_ubD) 174 175lemma lub_maximal: "S <| x \<Longrightarrow> x \<in> S \<Longrightarrow> lub S = x" 176 by (rule is_lub_maximal [THEN lub_eqI]) 177 178 179subsection \<open>Countable chains\<close> 180 181definition chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" 182 where \<comment> \<open>Here we use countable chains and I prefer to code them as functions!\<close> 183 "chain Y = (\<forall>i. Y i \<sqsubseteq> Y (Suc i))" 184 185lemma chainI: "(\<And>i. Y i \<sqsubseteq> Y (Suc i)) \<Longrightarrow> chain Y" 186 unfolding chain_def by fast 187 188lemma chainE: "chain Y \<Longrightarrow> Y i \<sqsubseteq> Y (Suc i)" 189 unfolding chain_def by fast 190 191text \<open>chains are monotone functions\<close> 192 193lemma chain_mono_less: "chain Y \<Longrightarrow> i < j \<Longrightarrow> Y i \<sqsubseteq> Y j" 194 by (erule less_Suc_induct, erule chainE, erule below_trans) 195 196lemma chain_mono: "chain Y \<Longrightarrow> i \<le> j \<Longrightarrow> Y i \<sqsubseteq> Y j" 197 by (cases "i = j") (simp_all add: chain_mono_less) 198 199lemma chain_shift: "chain Y \<Longrightarrow> chain (\<lambda>i. Y (i + j))" 200 by (rule chainI, simp, erule chainE) 201 202text \<open>technical lemmas about (least) upper bounds of chains\<close> 203 204lemma is_lub_rangeD1: "range S <<| x \<Longrightarrow> S i \<sqsubseteq> x" 205 by (rule is_lubD1 [THEN ub_rangeD]) 206 207lemma is_ub_range_shift: "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <| x = range S <| x" 208 apply (rule iffI) 209 apply (rule ub_rangeI) 210 apply (rule_tac y="S (i + j)" in below_trans) 211 apply (erule chain_mono) 212 apply (rule le_add1) 213 apply (erule ub_rangeD) 214 apply (rule ub_rangeI) 215 apply (erule ub_rangeD) 216 done 217 218lemma is_lub_range_shift: "chain S \<Longrightarrow> range (\<lambda>i. S (i + j)) <<| x = range S <<| x" 219 by (simp add: is_lub_def is_ub_range_shift) 220 221text \<open>the lub of a constant chain is the constant\<close> 222 223lemma chain_const [simp]: "chain (\<lambda>i. c)" 224 by (simp add: chainI) 225 226lemma is_lub_const: "range (\<lambda>x. c) <<| c" 227by (blast dest: ub_rangeD intro: is_lubI ub_rangeI) 228 229lemma lub_const [simp]: "(\<Squnion>i. c) = c" 230 by (rule is_lub_const [THEN lub_eqI]) 231 232 233subsection \<open>Finite chains\<close> 234 235definition max_in_chain :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool" 236 where \<comment> \<open>finite chains, needed for monotony of continuous functions\<close> 237 "max_in_chain i C \<longleftrightarrow> (\<forall>j. i \<le> j \<longrightarrow> C i = C j)" 238 239definition finite_chain :: "(nat \<Rightarrow> 'a) \<Rightarrow> bool" 240 where "finite_chain C = (chain C \<and> (\<exists>i. max_in_chain i C))" 241 242text \<open>results about finite chains\<close> 243 244lemma max_in_chainI: "(\<And>j. i \<le> j \<Longrightarrow> Y i = Y j) \<Longrightarrow> max_in_chain i Y" 245 unfolding max_in_chain_def by fast 246 247lemma max_in_chainD: "max_in_chain i Y \<Longrightarrow> i \<le> j \<Longrightarrow> Y i = Y j" 248 unfolding max_in_chain_def by fast 249 250lemma finite_chainI: "chain C \<Longrightarrow> max_in_chain i C \<Longrightarrow> finite_chain C" 251 unfolding finite_chain_def by fast 252 253lemma finite_chainE: "\<lbrakk>finite_chain C; \<And>i. \<lbrakk>chain C; max_in_chain i C\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" 254 unfolding finite_chain_def by fast 255 256lemma lub_finch1: "chain C \<Longrightarrow> max_in_chain i C \<Longrightarrow> range C <<| C i" 257 apply (rule is_lubI) 258 apply (rule ub_rangeI, rename_tac j) 259 apply (rule_tac x=i and y=j in linorder_le_cases) 260 apply (drule (1) max_in_chainD, simp) 261 apply (erule (1) chain_mono) 262 apply (erule ub_rangeD) 263 done 264 265lemma lub_finch2: "finite_chain C \<Longrightarrow> range C <<| C (LEAST i. max_in_chain i C)" 266 apply (erule finite_chainE) 267 apply (erule LeastI2 [where Q="\<lambda>i. range C <<| C i"]) 268 apply (erule (1) lub_finch1) 269 done 270 271lemma finch_imp_finite_range: "finite_chain Y \<Longrightarrow> finite (range Y)" 272 apply (erule finite_chainE) 273 apply (rule_tac B="Y ` {..i}" in finite_subset) 274 apply (rule subsetI) 275 apply (erule rangeE, rename_tac j) 276 apply (rule_tac x=i and y=j in linorder_le_cases) 277 apply (subgoal_tac "Y j = Y i", simp) 278 apply (simp add: max_in_chain_def) 279 apply simp 280 apply simp 281 done 282 283lemma finite_range_has_max: 284 fixes f :: "nat \<Rightarrow> 'a" 285 and r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 286 assumes mono: "\<And>i j. i \<le> j \<Longrightarrow> r (f i) (f j)" 287 assumes finite_range: "finite (range f)" 288 shows "\<exists>k. \<forall>i. r (f i) (f k)" 289proof (intro exI allI) 290 fix i :: nat 291 let ?j = "LEAST k. f k = f i" 292 let ?k = "Max ((\<lambda>x. LEAST k. f k = x) ` range f)" 293 have "?j \<le> ?k" 294 proof (rule Max_ge) 295 show "finite ((\<lambda>x. LEAST k. f k = x) ` range f)" 296 using finite_range by (rule finite_imageI) 297 show "?j \<in> (\<lambda>x. LEAST k. f k = x) ` range f" 298 by (intro imageI rangeI) 299 qed 300 hence "r (f ?j) (f ?k)" 301 by (rule mono) 302 also have "f ?j = f i" 303 by (rule LeastI, rule refl) 304 finally show "r (f i) (f ?k)" . 305qed 306 307lemma finite_range_imp_finch: "chain Y \<Longrightarrow> finite (range Y) \<Longrightarrow> finite_chain Y" 308 apply (subgoal_tac "\<exists>k. \<forall>i. Y i \<sqsubseteq> Y k") 309 apply (erule exE) 310 apply (rule finite_chainI, assumption) 311 apply (rule max_in_chainI) 312 apply (rule below_antisym) 313 apply (erule (1) chain_mono) 314 apply (erule spec) 315 apply (rule finite_range_has_max) 316 apply (erule (1) chain_mono) 317 apply assumption 318 done 319 320lemma bin_chain: "x \<sqsubseteq> y \<Longrightarrow> chain (\<lambda>i. if i=0 then x else y)" 321 by (rule chainI) simp 322 323lemma bin_chainmax: "x \<sqsubseteq> y \<Longrightarrow> max_in_chain (Suc 0) (\<lambda>i. if i=0 then x else y)" 324 by (simp add: max_in_chain_def) 325 326lemma is_lub_bin_chain: "x \<sqsubseteq> y \<Longrightarrow> range (\<lambda>i::nat. if i=0 then x else y) <<| y" 327 apply (frule bin_chain) 328 apply (drule bin_chainmax) 329 apply (drule (1) lub_finch1) 330 apply simp 331 done 332 333text \<open>the maximal element in a chain is its lub\<close> 334 335lemma lub_chain_maxelem: "Y i = c \<Longrightarrow> \<forall>i. Y i \<sqsubseteq> c \<Longrightarrow> lub (range Y) = c" 336 by (blast dest: ub_rangeD intro: lub_eqI is_lubI ub_rangeI) 337 338end 339 340end 341