2 Author: Amine Chaieb and L C Paulson, University of Cambridge |
2 Author: Amine Chaieb and L C Paulson, University of Cambridge |
3 Author: Johannes Hölzl, TU München |
3 Author: Johannes Hölzl, TU München |
4 Author: Luke S. Serafin, Carnegie Mellon University |
4 Author: Luke S. Serafin, Carnegie Mellon University |
5 *) |
5 *) |
6 |
6 |
7 section {* Conditionally-complete Lattices *} |
7 section \<open>Conditionally-complete Lattices\<close> |
8 |
8 |
9 theory Conditionally_Complete_Lattices |
9 theory Conditionally_Complete_Lattices |
10 imports Main |
10 imports Main |
11 begin |
11 begin |
12 |
12 |
164 by (auto simp: bdd_below_def intro: le_infI1 le_infI2) |
164 by (auto simp: bdd_below_def intro: le_infI1 le_infI2) |
165 |
165 |
166 end |
166 end |
167 |
167 |
168 |
168 |
169 text {* |
169 text \<open> |
170 |
170 |
171 To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and |
171 To avoid name classes with the @{class complete_lattice}-class we prefix @{const Sup} and |
172 @{const Inf} in theorem names with c. |
172 @{const Inf} in theorem names with c. |
173 |
173 |
174 *} |
174 \<close> |
175 |
175 |
176 class conditionally_complete_lattice = lattice + Sup + Inf + |
176 class conditionally_complete_lattice = lattice + Sup + Inf + |
177 assumes cInf_lower: "x \<in> X \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> x" |
177 assumes cInf_lower: "x \<in> X \<Longrightarrow> bdd_below X \<Longrightarrow> Inf X \<le> x" |
178 and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" |
178 and cInf_greatest: "X \<noteq> {} \<Longrightarrow> (\<And>x. x \<in> X \<Longrightarrow> z \<le> x) \<Longrightarrow> z \<le> Inf X" |
179 assumes cSup_upper: "x \<in> X \<Longrightarrow> bdd_above X \<Longrightarrow> x \<le> Sup X" |
179 assumes cSup_upper: "x \<in> X \<Longrightarrow> bdd_above X \<Longrightarrow> x \<le> Sup X" |
424 shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and> |
424 shows "\<exists>c. a \<le> c \<and> c \<le> b \<and> (\<forall>x. a \<le> x \<and> x < c \<longrightarrow> P x) \<and> |
425 (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)" |
425 (\<forall>d. (\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x) \<longrightarrow> d \<le> c)" |
426 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto) |
426 proof (rule exI [where x = "Sup {d. \<forall>x. a \<le> x & x < d --> P x}"], auto) |
427 show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
427 show "a \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
428 by (rule cSup_upper, auto simp: bdd_above_def) |
428 by (rule cSup_upper, auto simp: bdd_above_def) |
429 (metis `a < b` `\<not> P b` linear less_le) |
429 (metis \<open>a < b\<close> \<open>\<not> P b\<close> linear less_le) |
430 next |
430 next |
431 show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b" |
431 show "Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c} \<le> b" |
432 apply (rule cSup_least) |
432 apply (rule cSup_least) |
433 apply auto |
433 apply auto |
434 apply (metis less_le_not_le) |
434 apply (metis less_le_not_le) |
435 apply (metis `a<b` `~ P b` linear less_le) |
435 apply (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le) |
436 done |
436 done |
437 next |
437 next |
438 fix x |
438 fix x |
439 assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
439 assume x: "a \<le> x" and lt: "x < Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
440 show "P x" |
440 show "P x" |
445 next |
445 next |
446 fix d |
446 fix d |
447 assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x" |
447 assume 0: "\<forall>x. a \<le> x \<and> x < d \<longrightarrow> P x" |
448 thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
448 thus "d \<le> Sup {d. \<forall>c. a \<le> c \<and> c < d \<longrightarrow> P c}" |
449 by (rule_tac cSup_upper, auto simp: bdd_above_def) |
449 by (rule_tac cSup_upper, auto simp: bdd_above_def) |
450 (metis `a<b` `~ P b` linear less_le) |
450 (metis \<open>a<b\<close> \<open>~ P b\<close> linear less_le) |
451 qed |
451 qed |
452 |
452 |
453 end |
453 end |
454 |
454 |
455 instance complete_linorder < conditionally_complete_linorder |
455 instance complete_linorder < conditionally_complete_linorder |
536 have "\<exists>!x\<in>X. (\<forall>y\<in>X. y \<le> x)" |
536 have "\<exists>!x\<in>X. (\<forall>y\<in>X. y \<le> x)" |
537 proof |
537 proof |
538 { fix z assume "z \<in> X" |
538 { fix z assume "z \<in> X" |
539 have "z \<le> Max (X \<inter> {x..y})" |
539 have "z \<le> Max (X \<inter> {x..y})" |
540 proof cases |
540 proof cases |
541 assume "x \<le> z" with `z \<in> X` `X \<subseteq> {..y}` *(1) show ?thesis |
541 assume "x \<le> z" with \<open>z \<in> X\<close> \<open>X \<subseteq> {..y}\<close> *(1) show ?thesis |
542 by (auto intro!: Max_ge) |
542 by (auto intro!: Max_ge) |
543 next |
543 next |
544 assume "\<not> x \<le> z" |
544 assume "\<not> x \<le> z" |
545 then have "z < x" by simp |
545 then have "z < x" by simp |
546 also have "x \<le> Max (X \<inter> {x..y})" |
546 also have "x \<le> Max (X \<inter> {x..y})" |
547 using `x \<in> X` *(1) `x \<le> y` by (intro Max_ge) auto |
547 using \<open>x \<in> X\<close> *(1) \<open>x \<le> y\<close> by (intro Max_ge) auto |
548 finally show ?thesis by simp |
548 finally show ?thesis by simp |
549 qed } |
549 qed } |
550 note le = this |
550 note le = this |
551 with Max_in[OF *] show ex: "Max (X \<inter> {x..y}) \<in> X \<and> (\<forall>z\<in>X. z \<le> Max (X \<inter> {x..y}))" by auto |
551 with Max_in[OF *] show ex: "Max (X \<inter> {x..y}) \<in> X \<and> (\<forall>z\<in>X. z \<le> Max (X \<inter> {x..y}))" by auto |
552 |
552 |