src/HOL/Conditionally_Complete_Lattices.thy
 changeset 54281 b01057e72233 parent 54263 c4159fe6fa46 child 56166 9a241bc276cd
```     1.1 --- a/src/HOL/Conditionally_Complete_Lattices.thy	Wed Nov 06 14:50:50 2013 +0100
1.2 +++ b/src/HOL/Conditionally_Complete_Lattices.thy	Tue Nov 05 21:23:42 2013 +0100
1.3 @@ -471,4 +471,92 @@
1.4
1.5  end
1.6
1.7 +instantiation nat :: conditionally_complete_linorder
1.8 +begin
1.9 +
1.10 +definition "Sup (X::nat set) = Max X"
1.11 +definition "Inf (X::nat set) = (LEAST n. n \<in> X)"
1.12 +
1.13 +lemma bdd_above_nat: "bdd_above X \<longleftrightarrow> finite (X::nat set)"
1.14 +proof
1.15 +  assume "bdd_above X"
1.16 +  then obtain z where "X \<subseteq> {.. z}"
1.17 +    by (auto simp: bdd_above_def)
1.18 +  then show "finite X"
1.19 +    by (rule finite_subset) simp
1.20 +qed simp
1.21 +
1.22 +instance
1.23 +proof
1.24 +  fix x :: nat and X :: "nat set"
1.25 +  { assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
1.26 +      by (simp add: Inf_nat_def Least_le) }
1.27 +  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> x \<le> y" then show "x \<le> Inf X"
1.28 +      unfolding Inf_nat_def ex_in_conv[symmetric] by (rule LeastI2_ex) }
1.29 +  { assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
1.30 +      by (simp add: Sup_nat_def bdd_above_nat) }
1.31 +  { assume "X \<noteq> {}" "\<And>y. y \<in> X \<Longrightarrow> y \<le> x"
1.32 +    moreover then have "bdd_above X"
1.33 +      by (auto simp: bdd_above_def)
1.34 +    ultimately show "Sup X \<le> x"
1.35 +      by (simp add: Sup_nat_def bdd_above_nat) }
1.36 +qed
1.37  end
1.38 +
1.39 +instantiation int :: conditionally_complete_linorder
1.40 +begin
1.41 +
1.42 +definition "Sup (X::int set) = (THE x. x \<in> X \<and> (\<forall>y\<in>X. y \<le> x))"
1.43 +definition "Inf (X::int set) = - (Sup (uminus ` X))"
1.44 +
1.45 +instance
1.46 +proof
1.47 +  { fix x :: int and X :: "int set" assume "X \<noteq> {}" "bdd_above X"
1.48 +    then obtain x y where "X \<subseteq> {..y}" "x \<in> X"
1.49 +      by (auto simp: bdd_above_def)
1.50 +    then have *: "finite (X \<inter> {x..y})" "X \<inter> {x..y} \<noteq> {}" and "x \<le> y"
1.51 +      by (auto simp: subset_eq)
1.52 +    have "\<exists>!x\<in>X. (\<forall>y\<in>X. y \<le> x)"
1.53 +    proof
1.54 +      { fix z assume "z \<in> X"
1.55 +        have "z \<le> Max (X \<inter> {x..y})"
1.56 +        proof cases
1.57 +          assume "x \<le> z" with `z \<in> X` `X \<subseteq> {..y}` *(1) show ?thesis
1.58 +            by (auto intro!: Max_ge)
1.59 +        next
1.60 +          assume "\<not> x \<le> z"
1.61 +          then have "z < x" by simp
1.62 +          also have "x \<le> Max (X \<inter> {x..y})"
1.63 +            using `x \<in> X` *(1) `x \<le> y` by (intro Max_ge) auto
1.64 +          finally show ?thesis by simp
1.65 +        qed }
1.66 +      note le = this
1.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
1.68 +
1.69 +      fix z assume *: "z \<in> X \<and> (\<forall>y\<in>X. y \<le> z)"
1.70 +      with le have "z \<le> Max (X \<inter> {x..y})"
1.71 +        by auto
1.72 +      moreover have "Max (X \<inter> {x..y}) \<le> z"
1.73 +        using * ex by auto
1.74 +      ultimately show "z = Max (X \<inter> {x..y})"
1.75 +        by auto
1.76 +    qed
1.77 +    then have "Sup X \<in> X \<and> (\<forall>y\<in>X. y \<le> Sup X)"
1.78 +      unfolding Sup_int_def by (rule theI') }
1.79 +  note Sup_int = this
1.80 +
1.81 +  { fix x :: int and X :: "int set" assume "x \<in> X" "bdd_above X" then show "x \<le> Sup X"
1.82 +      using Sup_int[of X] by auto }
1.83 +  note le_Sup = this
1.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"
1.85 +      using Sup_int[of X] by (auto simp: bdd_above_def) }
1.86 +  note Sup_le = this
1.87 +
1.88 +  { fix x :: int and X :: "int set" assume "x \<in> X" "bdd_below X" then show "Inf X \<le> x"
1.89 +      using le_Sup[of "-x" "uminus ` X"] by (auto simp: Inf_int_def) }
1.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"
1.91 +      using Sup_le[of "uminus ` X" "-x"] by (force simp: Inf_int_def) }
1.92 +qed
1.93 +end
1.94 +
1.95 +end
```