# HG changeset patch
# User hoelzl
# Date 1383683022 -3600
# Node ID b01057e722336083373264a4d38f4bf1ced47a49
# Parent 23c0049e7c409e342cc3f720cbde73ff9fef7302
int and nat are conditionally_complete_lattices
diff -r 23c0049e7c40 -r b01057e72233 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy Wed Nov 06 14:50:50 2013 +0100
+++ b/src/HOL/Archimedean_Field.thy Tue Nov 05 21:23:42 2013 +0100
@@ -129,12 +129,8 @@
fix y z assume
"of_int y \<le> x \<and> x < of_int (y + 1)"
"of_int z \<le> x \<and> x < of_int (z + 1)"
- then have
- "of_int y \<le> x" "x < of_int (y + 1)"
- "of_int z \<le> x" "x < of_int (z + 1)"
- by simp_all
- from le_less_trans [OF `of_int y \<le> x` `x < of_int (z + 1)`]
- le_less_trans [OF `of_int z \<le> x` `x < of_int (y + 1)`]
+ with le_less_trans [of "of_int y" "x" "of_int (z + 1)"]
+ le_less_trans [of "of_int z" "x" "of_int (y + 1)"]
show "y = z" by (simp del: of_int_add)
qed
diff -r 23c0049e7c40 -r b01057e72233 src/HOL/Conditionally_Complete_Lattices.thy
--- a/src/HOL/Conditionally_Complete_Lattices.thy Wed Nov 06 14:50:50 2013 +0100
+++ b/src/HOL/Conditionally_Complete_Lattices.thy Tue Nov 05 21:23:42 2013 +0100
@@ -471,4 +471,92 @@
end
+instantiation nat :: conditionally_complete_linorder
+begin
+
+definition "Sup (X::nat set) = Max X"
+definition "Inf (X::nat set) = (LEAST n. n \<in> X)"
+
+lemma bdd_above_nat: "bdd_above X \<longleftrightarrow> finite (X::nat set)"
+proof
+ assume "bdd_above X"
+ then obtain z where "X \<subseteq> {.. z}"
+ by (auto simp: bdd_above_def)
+ then show "finite X"
+ by (rule finite_subset) simp
+qed simp
+
+instance
+proof
+ fix x :: nat and X :: "nat set"
+ { assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
+ by (simp add: Inf_nat_def Least_le) }
+ { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X"
+ unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
+ { assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
+ by (simp add: Sup_nat_def bdd_above_nat) }
+ { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
+ moreover then have "bdd_above X"
+ by (auto simp: bdd_above_def)
+ ultimately show "Sup X \<le> x"
+ by (simp add: Sup_nat_def bdd_above_nat) }
+qed
end
+
+instantiation int :: conditionally_complete_linorder
+begin
+
+definition "Sup (X::int set) = (THE x. x \<in> X \<and> (\<forall>y\<in>X. y \<le> x))"
+definition "Inf (X::int set) = - (Sup (uminus ` X))"
+
+instance
+proof
+ { fix x :: int and X :: "int set" assume "X \<noteq> {}" "bdd_above X"
+ then obtain x y where "X \<subseteq> {..y}" "x \<in> X"
+ by (auto simp: bdd_above_def)
+ then have *: "finite (X \<inter> {x..y})" "X \<inter> {x..y} \<noteq> {}" and "x \<le> y"
+ by (auto simp: subset_eq)
+ have "\<exists>!x\<in>X. (\<forall>y\<in>X. y \<le> x)"
+ proof
+ { fix z assume "z \<in> X"
+ have "z \<le> Max (X \<inter> {x..y})"
+ proof cases
+ assume "x \<le> z" with `z \<in> X` `X \<subseteq> {..y}` *(1) show ?thesis
+ by (auto intro!: Max_ge)
+ next
+ assume "\<not> x \<le> z"
+ then have "z < x" by simp
+ also have "x \<le> Max (X \<inter> {x..y})"
+ using `x \<in> X` *(1) `x \<le> y` by (intro Max_ge) auto
+ finally show ?thesis by simp
+ qed }
+ note le = this
+ 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
+
+ fix z assume *: "z \<in> X \<and> (\<forall>y\<in>X. y \<le> z)"
+ with le have "z \<le> Max (X \<inter> {x..y})"
+ by auto
+ moreover have "Max (X \<inter> {x..y}) \<le> z"
+ using * ex by auto
+ ultimately show "z = Max (X \<inter> {x..y})"
+ by auto
+ qed
+ then have "Sup X \<in> X \<and> (\<forall>y\<in>X. y \<le> Sup X)"
+ unfolding Sup_int_def by (rule theI') }
+ note Sup_int = this
+
+ { fix x :: int and X :: "int set" assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
+ using Sup_int[of X] by auto }
+ note le_Sup = this
+ { fix x :: int and X :: "int set" assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x" then show "Sup X \<le> x"
+ using Sup_int[of X] by (auto simp: bdd_above_def) }
+ note Sup_le = this
+
+ { fix x :: int and X :: "int set" assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
+ using le_Sup[of "-x" "uminus ` X"] by (auto simp: Inf_int_def) }
+ { fix x :: int and X :: "int set" assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X"
+ using Sup_le[of "uminus ` X" "-x"] by (force simp: Inf_int_def) }
+qed
+end
+
+end
diff -r 23c0049e7c40 -r b01057e72233 src/HOL/Real.thy
--- a/src/HOL/Real.thy Wed Nov 06 14:50:50 2013 +0100
+++ b/src/HOL/Real.thy Tue Nov 05 21:23:42 2013 +0100
@@ -924,11 +924,8 @@
subsection{*Supremum of a set of reals*}
-definition
- Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
-
-definition
- Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
+definition "Sup X = (LEAST z::real. \<forall>x\<in>X. x \<le> z)"
+definition "Inf (X::real set) = - Sup (uminus ` X)"
instance
proof
@@ -951,20 +948,10 @@
finally show "Sup X \<le> z" . }
note Sup_least = this
- { fix x z :: real and X :: "real set"
- assume x: "x \<in> X" and [simp]: "bdd_below X"
- have "-x \<le> Sup (uminus ` X)"
- by (rule Sup_upper) (auto simp add: image_iff x)
- then show "Inf X \<le> x"
- by (auto simp add: Inf_real_def) }
-
- { fix z :: real and X :: "real set"
- assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
- have "Sup (uminus ` X) \<le> -z"
- using x z by (force intro: Sup_least)
- then show "z \<le> Inf X"
- by (auto simp add: Inf_real_def) }
-
+ { fix x :: real and X :: "real set" assume x: "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
+ using Sup_upper[of "-x" "uminus ` X"] by (auto simp: Inf_real_def) }
+ { fix z :: real and X :: "real set" assume "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" then show "z \<le> Inf X"
+ using Sup_least[of "uminus ` X" "- z"] by (force simp: Inf_real_def) }
show "\<exists>a b::real. a \<noteq> b"
using zero_neq_one by blast
qed