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