# 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