src/HOL/Archimedean_Field.thy

tuned signature;

(*  Title:      HOL/Archimedean_Field.thy
    Author:     Brian Huffman
*)

section \<open>Archimedean Fields, Floor and Ceiling Functions\<close>

theory Archimedean_Field
imports Main
begin

lemma cInf_abs_ge:
  fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set"
  assumes "S \<noteq> {}"
    and bdd: "\<And>x. x\<in>S \<Longrightarrow> \<bar>x\<bar> \<le> a"
  shows "\<bar>Inf S\<bar> \<le> a"
proof -
  have "Sup (uminus ` S) = - (Inf S)"
  proof (rule antisym)
    show "- (Inf S) \<le> Sup (uminus ` S)"
      apply (subst minus_le_iff)
      apply (rule cInf_greatest [OF \<open>S \<noteq> {}\<close>])
      apply (subst minus_le_iff)
      apply (rule cSup_upper)
       apply force
      using bdd
      apply (force simp: abs_le_iff bdd_above_def)
      done
  next
    have *: "\<And>x. x \<in> S \<Longrightarrow> Inf S \<le> x"
      by (meson abs_le_iff bdd bdd_below_def cInf_lower minus_le_iff)
    show "Sup (uminus ` S) \<le> - Inf S"
      using \<open>S \<noteq> {}\<close> by (force intro: * cSup_least)
  qed
  with cSup_abs_le [of "uminus ` S"] assms show ?thesis
    by fastforce
qed

lemma cSup_asclose:
  fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set"
  assumes S: "S \<noteq> {}"
    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
  shows "\<bar>Sup S - l\<bar> \<le> e"
proof -
  have *: "\<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" for x l e :: 'a
    by arith
  have "bdd_above S"
    using b by (auto intro!: bdd_aboveI[of _ "l + e"])
  with S b show ?thesis
    unfolding * by (auto intro!: cSup_upper2 cSup_least)
qed

lemma cInf_asclose:
  fixes S :: "'a::{linordered_idom,conditionally_complete_linorder} set"
  assumes S: "S \<noteq> {}"
    and b: "\<forall>x\<in>S. \<bar>x - l\<bar> \<le> e"
  shows "\<bar>Inf S - l\<bar> \<le> e"
proof -
  have *: "\<bar>x - l\<bar> \<le> e \<longleftrightarrow> l - e \<le> x \<and> x \<le> l + e" for x l e :: 'a
    by arith
  have "bdd_below S"
    using b by (auto intro!: bdd_belowI[of _ "l - e"])
  with S b show ?thesis
    unfolding * by (auto intro!: cInf_lower2 cInf_greatest)
qed


subsection \<open>Class of Archimedean fields\<close>

text \<open>Archimedean fields have no infinite elements.\<close>

class archimedean_field = linordered_field +
  assumes ex_le_of_int: "\<exists>z. x \<le> of_int z"

lemma ex_less_of_int: "\<exists>z. x < of_int z"
  for x :: "'a::archimedean_field"
proof -
  from ex_le_of_int obtain z where "x \<le> of_int z" ..
  then have "x < of_int (z + 1)" by simp
  then show ?thesis ..
qed

lemma ex_of_int_less: "\<exists>z. of_int z < x"
  for x :: "'a::archimedean_field"
proof -
  from ex_less_of_int obtain z where "- x < of_int z" ..
  then have "of_int (- z) < x" by simp
  then show ?thesis ..
qed

lemma reals_Archimedean2: "\<exists>n. x < of_nat n"
  for x :: "'a::archimedean_field"
proof -
  obtain z where "x < of_int z"
    using ex_less_of_int ..
  also have "\<dots> \<le> of_int (int (nat z))"
    by simp
  also have "\<dots> = of_nat (nat z)"
    by (simp only: of_int_of_nat_eq)
  finally show ?thesis ..
qed

lemma real_arch_simple: "\<exists>n. x \<le> of_nat n"
  for x :: "'a::archimedean_field"
proof -
  obtain n where "x < of_nat n"
    using reals_Archimedean2 ..
  then have "x \<le> of_nat n"
    by simp
  then show ?thesis ..
qed

text \<open>Archimedean fields have no infinitesimal elements.\<close>

lemma reals_Archimedean:
  fixes x :: "'a::archimedean_field"
  assumes "0 < x"
  shows "\<exists>n. inverse (of_nat (Suc n)) < x"
proof -
  from \<open>0 < x\<close> have "0 < inverse x"
    by (rule positive_imp_inverse_positive)
  obtain n where "inverse x < of_nat n"
    using reals_Archimedean2 ..
  then obtain m where "inverse x < of_nat (Suc m)"
    using \<open>0 < inverse x\<close> by (cases n) (simp_all del: of_nat_Suc)
  then have "inverse (of_nat (Suc m)) < inverse (inverse x)"
    using \<open>0 < inverse x\<close> by (rule less_imp_inverse_less)
  then have "inverse (of_nat (Suc m)) < x"
    using \<open>0 < x\<close> by (simp add: nonzero_inverse_inverse_eq)
  then show ?thesis ..
qed

lemma ex_inverse_of_nat_less:
  fixes x :: "'a::archimedean_field"
  assumes "0 < x"
  shows "\<exists>n>0. inverse (of_nat n) < x"
  using reals_Archimedean [OF \<open>0 < x\<close>] by auto

lemma ex_less_of_nat_mult:
  fixes x :: "'a::archimedean_field"
  assumes "0 < x"
  shows "\<exists>n. y < of_nat n * x"
proof -
  obtain n where "y / x < of_nat n"
    using reals_Archimedean2 ..
  with \<open>0 < x\<close> have "y < of_nat n * x"
    by (simp add: pos_divide_less_eq)
  then show ?thesis ..
qed


subsection \<open>Existence and uniqueness of floor function\<close>

lemma exists_least_lemma:
  assumes "\<not> P 0" and "\<exists>n. P n"
  shows "\<exists>n. \<not> P n \<and> P (Suc n)"
proof -
  from \<open>\<exists>n. P n\<close> have "P (Least P)"
    by (rule LeastI_ex)
  with \<open>\<not> P 0\<close> obtain n where "Least P = Suc n"
    by (cases "Least P") auto
  then have "n < Least P"
    by simp
  then have "\<not> P n"
    by (rule not_less_Least)
  then have "\<not> P n \<and> P (Suc n)"
    using \<open>P (Least P)\<close> \<open>Least P = Suc n\<close> by simp
  then show ?thesis ..
qed

lemma floor_exists:
  fixes x :: "'a::archimedean_field"
  shows "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
proof (cases "0 \<le> x")
  case True
  then have "\<not> x < of_nat 0"
    by simp
  then have "\<exists>n. \<not> x < of_nat n \<and> x < of_nat (Suc n)"
    using reals_Archimedean2 by (rule exists_least_lemma)
  then obtain n where "\<not> x < of_nat n \<and> x < of_nat (Suc n)" ..
  then have "of_int (int n) \<le> x \<and> x < of_int (int n + 1)"
    by simp
  then show ?thesis ..
next
  case False
  then have "\<not> - x \<le> of_nat 0"
    by simp
  then have "\<exists>n. \<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)"
    using real_arch_simple by (rule exists_least_lemma)
  then obtain n where "\<not> - x \<le> of_nat n \<and> - x \<le> of_nat (Suc n)" ..
  then have "of_int (- int n - 1) \<le> x \<and> x < of_int (- int n - 1 + 1)"
    by simp
  then show ?thesis ..
qed

lemma floor_exists1: "\<exists>!z. of_int z \<le> x \<and> x < of_int (z + 1)"
  for x :: "'a::archimedean_field"
proof (rule ex_ex1I)
  show "\<exists>z. of_int z \<le> x \<and> x < of_int (z + 1)"
    by (rule floor_exists)
next
  fix y z
  assume "of_int y \<le> x \<and> x < of_int (y + 1)"
    and "of_int z \<le> x \<and> x < of_int (z + 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


subsection \<open>Floor function\<close>

class floor_ceiling = archimedean_field +
  fixes floor :: "'a \<Rightarrow> int"  ("\<lfloor>_\<rfloor>")
  assumes floor_correct: "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)"

lemma floor_unique: "of_int z \<le> x \<Longrightarrow> x < of_int z + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = z"
  using floor_correct [of x] floor_exists1 [of x] by auto

lemma floor_eq_iff: "\<lfloor>x\<rfloor> = a \<longleftrightarrow> of_int a \<le> x \<and> x < of_int a + 1"
using floor_correct floor_unique by auto

lemma of_int_floor_le [simp]: "of_int \<lfloor>x\<rfloor> \<le> x"
  using floor_correct ..

lemma le_floor_iff: "z \<le> \<lfloor>x\<rfloor> \<longleftrightarrow> of_int z \<le> x"
proof
  assume "z \<le> \<lfloor>x\<rfloor>"
  then have "(of_int z :: 'a) \<le> of_int \<lfloor>x\<rfloor>" by simp
  also have "of_int \<lfloor>x\<rfloor> \<le> x" by (rule of_int_floor_le)
  finally show "of_int z \<le> x" .
next
  assume "of_int z \<le> x"
  also have "x < of_int (\<lfloor>x\<rfloor> + 1)" using floor_correct ..
  finally show "z \<le> \<lfloor>x\<rfloor>" by (simp del: of_int_add)
qed

lemma floor_less_iff: "\<lfloor>x\<rfloor> < z \<longleftrightarrow> x < of_int z"
  by (simp add: not_le [symmetric] le_floor_iff)