int and nat are conditionally_complete_lattices
authorhoelzl
Tue Nov 05 21:23:42 2013 +0100 (2013-11-05)
changeset 54281b01057e72233
parent 54280 23c0049e7c40
child 54282 32b5c4821d9d
int and nat are conditionally_complete_lattices
src/HOL/Archimedean_Field.thy
src/HOL/Conditionally_Complete_Lattices.thy
src/HOL/Real.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Wed Nov 06 14:50:50 2013 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Tue Nov 05 21:23:42 2013 +0100
     1.3 @@ -129,12 +129,8 @@
     1.4    fix y z assume
     1.5      "of_int y \<le> x \<and> x < of_int (y + 1)"
     1.6      "of_int z \<le> x \<and> x < of_int (z + 1)"
     1.7 -  then have
     1.8 -    "of_int y \<le> x" "x < of_int (y + 1)"
     1.9 -    "of_int z \<le> x" "x < of_int (z + 1)"
    1.10 -    by simp_all
    1.11 -  from le_less_trans [OF `of_int y \<le> x` `x < of_int (z + 1)`]
    1.12 -       le_less_trans [OF `of_int z \<le> x` `x < of_int (y + 1)`]
    1.13 +  with le_less_trans [of "of_int y" "x" "of_int (z + 1)"]
    1.14 +       le_less_trans [of "of_int z" "x" "of_int (y + 1)"]
    1.15    show "y = z" by (simp del: of_int_add)
    1.16  qed
    1.17  
     2.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Nov 06 14:50:50 2013 +0100
     2.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 21:23:42 2013 +0100
     2.3 @@ -471,4 +471,92 @@
     2.4  
     2.5  end
     2.6  
     2.7 +instantiation nat :: conditionally_complete_linorder
     2.8 +begin
     2.9 +
    2.10 +definition "Sup (X::nat set) = Max X"
    2.11 +definition "Inf (X::nat set) = (LEAST n. n \<in> X)"
    2.12 +
    2.13 +lemma bdd_above_nat: "bdd_above X \<longleftrightarrow> finite (X::nat set)"
    2.14 +proof
    2.15 +  assume "bdd_above X"
    2.16 +  then obtain z where "X \<subseteq> {.. z}"
    2.17 +    by (auto simp: bdd_above_def)
    2.18 +  then show "finite X"
    2.19 +    by (rule finite_subset) simp
    2.20 +qed simp
    2.21 +
    2.22 +instance
    2.23 +proof
    2.24 +  fix x :: nat and X :: "nat set"
    2.25 +  { assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
    2.26 +      by (simp add: Inf_nat_def Least_le) }
    2.27 +  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X"
    2.28 +      unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
    2.29 +  { assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
    2.30 +      by (simp add: Sup_nat_def bdd_above_nat) }
    2.31 +  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x" 
    2.32 +    moreover then have "bdd_above X"
    2.33 +      by (auto simp: bdd_above_def)
    2.34 +    ultimately show "Sup X \<le> x"
    2.35 +      by (simp add: Sup_nat_def bdd_above_nat) }
    2.36 +qed
    2.37  end
    2.38 +
    2.39 +instantiation int :: conditionally_complete_linorder
    2.40 +begin
    2.41 +
    2.42 +definition "Sup (X::int set) = (THE x. x \<in> X \<and> (\<forall>y\<in>X. y \<le> x))"
    2.43 +definition "Inf (X::int set) = - (Sup (uminus ` X))"
    2.44 +
    2.45 +instance
    2.46 +proof
    2.47 +  { fix x :: int and X :: "int set" assume "X \<noteq> {}" "bdd_above X"
    2.48 +    then obtain x y where "X \<subseteq> {..y}" "x \<in> X"
    2.49 +      by (auto simp: bdd_above_def)
    2.50 +    then have *: "finite (X \<inter> {x..y})" "X \<inter> {x..y} \<noteq> {}" and "x \<le> y"
    2.51 +      by (auto simp: subset_eq)
    2.52 +    have "\<exists>!x\<in>X. (\<forall>y\<in>X. y \<le> x)"
    2.53 +    proof
    2.54 +      { fix z assume "z \<in> X"
    2.55 +        have "z \<le> Max (X \<inter> {x..y})"
    2.56 +        proof cases
    2.57 +          assume "x \<le> z" with `z \<in> X` `X \<subseteq> {..y}` *(1) show ?thesis
    2.58 +            by (auto intro!: Max_ge)
    2.59 +        next
    2.60 +          assume "\<not> x \<le> z"
    2.61 +          then have "z < x" by simp
    2.62 +          also have "x \<le> Max (X \<inter> {x..y})"
    2.63 +            using `x \<in> X` *(1) `x \<le> y` by (intro Max_ge) auto
    2.64 +          finally show ?thesis by simp
    2.65 +        qed }
    2.66 +      note le = this
    2.67 +      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
    2.68 +
    2.69 +      fix z assume *: "z \<in> X \<and> (\<forall>y\<in>X. y \<le> z)"
    2.70 +      with le have "z \<le> Max (X \<inter> {x..y})"
    2.71 +        by auto
    2.72 +      moreover have "Max (X \<inter> {x..y}) \<le> z"
    2.73 +        using * ex by auto
    2.74 +      ultimately show "z = Max (X \<inter> {x..y})"
    2.75 +        by auto
    2.76 +    qed
    2.77 +    then have "Sup X \<in> X \<and> (\<forall>y\<in>X. y \<le> Sup X)"
    2.78 +      unfolding Sup_int_def by (rule theI') }
    2.79 +  note Sup_int = this
    2.80 +
    2.81 +  { fix x :: int and X :: "int set" assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
    2.82 +      using Sup_int[of X] by auto }
    2.83 +  note le_Sup = this
    2.84 +  { 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"
    2.85 +      using Sup_int[of X] by (auto simp: bdd_above_def) }
    2.86 +  note Sup_le = this
    2.87 +
    2.88 +  { fix x :: int and X :: "int set" assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
    2.89 +      using le_Sup[of "-x" "uminus ` X"] by (auto simp: Inf_int_def) }
    2.90 +  { 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"
    2.91 +      using Sup_le[of "uminus ` X" "-x"] by (force simp: Inf_int_def) }
    2.92 +qed
    2.93 +end
    2.94 +
    2.95 +end
     3.1 --- a/src/HOL/Real.thy	Wed Nov 06 14:50:50 2013 +0100
     3.2 +++ b/src/HOL/Real.thy	Tue Nov 05 21:23:42 2013 +0100
     3.3 @@ -924,11 +924,8 @@
     3.4  
     3.5  subsection{*Supremum of a set of reals*}
     3.6  
     3.7 -definition
     3.8 -  Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z"
     3.9 -
    3.10 -definition
    3.11 -  Inf_real_def: "Inf (X::real set) \<equiv> - Sup (uminus ` X)"
    3.12 +definition "Sup X = (LEAST z::real. \<forall>x\<in>X. x \<le> z)"
    3.13 +definition "Inf (X::real set) = - Sup (uminus ` X)"
    3.14  
    3.15  instance
    3.16  proof
    3.17 @@ -951,20 +948,10 @@
    3.18      finally show "Sup X \<le> z" . }
    3.19    note Sup_least = this
    3.20  
    3.21 -  { fix x z :: real and X :: "real set"
    3.22 -    assume x: "x \<in> X" and [simp]: "bdd_below X"
    3.23 -    have "-x \<le> Sup (uminus ` X)"
    3.24 -      by (rule Sup_upper) (auto simp add: image_iff x)
    3.25 -    then show "Inf X \<le> x" 
    3.26 -      by (auto simp add: Inf_real_def) }
    3.27 -
    3.28 -  { fix z :: real and X :: "real set"
    3.29 -    assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x"
    3.30 -    have "Sup (uminus ` X) \<le> -z"
    3.31 -      using x z by (force intro: Sup_least)
    3.32 -    then show "z \<le> Inf X" 
    3.33 -        by (auto simp add: Inf_real_def) }
    3.34 -
    3.35 +  { fix x :: real and X :: "real set" assume x: "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
    3.36 +      using Sup_upper[of "-x" "uminus ` X"] by (auto simp: Inf_real_def) }
    3.37 +  { 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"
    3.38 +      using Sup_least[of "uminus ` X" "- z"] by (force simp: Inf_real_def) }
    3.39    show "\<exists>a b::real. a \<noteq> b"
    3.40      using zero_neq_one by blast
    3.41  qed