Quelle Archimedean_Field.thy Sprache: Isabelle

(*  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 \ {}"
    and bdd: "\x. x\S \ \x\ \ a"
  shows "\Inf S\ \ a"
proof -
  have "Sup (uminus ` S) = - (Inf S)"
  proof (rule antisym)
    have "\x. x \ S \ bdd_above (uminus ` S)"
      using bdd by (force simp: abs_le_iff bdd_above_def)
  then show "- (Inf S) \ Sup (uminus ` S)"
    by (meson cInf_greatest [OF \<open>S \<noteq> {}\<close>] cSUP_upper minus_le_iff)
  next
    have *: "\x. x \ S \ Inf S \ x"
      by (meson abs_le_iff bdd bdd_below_def cInf_lower minus_le_iff)
    show "Sup (uminus ` S) \ - 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 \ {}"
    and b: "\x\S. \x - l\ \ e"
  shows "\Sup S - l\ \ e"
proof -
  have *: "\x - l\ \ e \ l - e \ x \ x \ 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 \ {}"
    and b: "\x\S. \x - l\ \ e"
  shows "\Inf S - l\ \ e"
proof -
  have *: "\x - l\ \ e \ l - e \ x \ x \ 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: "\z. x \ of_int z"

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

lemma ex_of_int_less: "\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: "\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 "\ \ of_int (int (nat z))"
    by simp
  also have "\ = of_nat (nat z)"
    by (simp only: of_int_of_nat_eq)
  finally show ?thesis ..
qed

lemma real_arch_simple: "\n. x \ of_nat n"
  for x :: "'a::archimedean_field"
proof -
  obtain n where "x < of_nat n"
    using reals_Archimedean2 ..
  then have "x \ 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 "\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 "\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 "\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 "\ P 0" and "\n. P n"
  shows "\n. \ P n \ 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 "\ P n"
    by (rule not_less_Least)
  then have "\ P n \ 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 "\z. of_int z \ x \ x < of_int (z + 1)"
proof (cases "0 \ x")
  case True
  then have "\ x < of_nat 0"
    by simp
  then have "\n. \ x < of_nat n \ x < of_nat (Suc n)"
    using reals_Archimedean2 by (rule exists_least_lemma)
  then obtain n where "\ x < of_nat n \ x < of_nat (Suc n)" ..
  then have "of_int (int n) \ x \ x < of_int (int n + 1)"
    by simp
  then show ?thesis ..
next
  case False
  then have "\ - x \ of_nat 0"
    by simp
  then have "\n. \ - x \ of_nat n \ - x \ of_nat (Suc n)"
    using real_arch_simple by (rule exists_least_lemma)
  then obtain n where "\ - x \ of_nat n \ - x \ of_nat (Suc n)" ..
  then have "of_int (- int n - 1) \ x \ x < of_int (- int n - 1 + 1)"
    by simp
  then show ?thesis ..
qed

lemma floor_exists1: "\!z. of_int z \ x \ x < of_int (z + 1)"
  for x :: "'a::archimedean_field"
proof (rule ex_ex1I)
  show "\z. of_int z \ x \ x < of_int (z + 1)"
    by (rule floor_exists)
next
  fix y z
  assume "of_int y \ x \ x < of_int (y + 1)"
    and "of_int z \ x \ 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 \ int" (\(\open_block notation=\mixfix floor\\\_\)\)
  assumes floor_correct: "of_int \x\ \ x \ x < of_int (\x\ + 1)"

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

lemma floor_eq_iff: "\x\ = a \ of_int a \ x \ x < of_int a + 1"
  using floor_correct floor_unique by auto

lemma of_int_floor_le [simp]: "of_int \x\ \ x"
  using floor_correct ..

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

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

lemma less_floor_iff: "z < \x\ \ of_int z + 1 \ x"
  using le_floor_iff [of "z + 1" x] by auto

lemma floor_le_iff: "\x\ \ z \ x < of_int z + 1"
  by (simp add: not_less [symmetric] less_floor_iff)

lemma floor_split[linarith_split]: "P \t\ \ (\i. of_int i \ t \ t < of_int i + 1 \ P i)"
  by (metis floor_correct floor_unique less_floor_iff not_le order_refl)

lemma floor_eq_imp_diff_1: "\x\ = \y\ \ \x-y\ < 1"
  unfolding floor_eq_iff by linarith

lemma floor_mono:
  assumes "x \ y"
  shows "\x\ \ \y\"
  using assms le_floor_iff of_int_floor_le order.trans by blast

lemma floor_less_cancel: "\x\ < \y\ \ x < y"
  by (auto simp add: not_le [symmetric] floor_mono)

lemma floor_of_int [simp]: "\of_int z\ = z"
  by (rule floor_unique) simp_all

lemma floor_of_nat [simp]: "\of_nat n\ = int n"
  using floor_of_int [of "of_nat n"] by simp

lemma le_floor_add: "\x\ + \y\ \ \x + y\"
  by (simp only: le_floor_iff of_int_add add_mono of_int_floor_le)

text \<open>Floor with numerals.\<close>

lemma floor_zero [simp]: "\0\ = 0"
  using floor_of_int [of 0] by simp

lemma floor_one [simp]: "\1\ = 1"
  using floor_of_int [of 1] by simp

lemma floor_numeral [simp]: "\numeral v\ = numeral v"
  using floor_of_int [of "numeral v"] by simp

lemma floor_neg_numeral [simp]: "\- numeral v\ = - numeral v"
  using floor_of_int [of "- numeral v"] by simp

lemma zero_le_floor [simp]: "0 \ \x\ \ 0 \ x"
  by (simp add: le_floor_iff)

lemma one_le_floor [simp]: "1 \ \x\ \ 1 \ x"
  by (simp add: le_floor_iff)

lemma numeral_le_floor [simp]: "numeral v \ \x\ \ numeral v \ x"
  by (simp add: le_floor_iff)

lemma neg_numeral_le_floor [simp]: "- numeral v \ \x\ \ - numeral v \ x"
  by (simp add: le_floor_iff)

lemma zero_less_floor [simp]: "0 < \x\ \ 1 \ x"
  by (simp add: less_floor_iff)

lemma one_less_floor [simp]: "1 < \x\ \ 2 \ x"
  by (simp add: less_floor_iff)

lemma numeral_less_floor [simp]: "numeral v < \x\ \ numeral v + 1 \ x"
  by (simp add: less_floor_iff)

lemma neg_numeral_less_floor [simp]: "- numeral v < \x\ \ - numeral v + 1 \ x"
  by (simp add: less_floor_iff)

lemma floor_le_zero [simp]: "\x\ \ 0 \ x < 1"
  by (simp add: floor_le_iff)

lemma floor_le_one [simp]: "\x\ \ 1 \ x < 2"
  by (simp add: floor_le_iff)

lemma floor_le_numeral [simp]: "\x\ \ numeral v \ x < numeral v + 1"
  by (simp add: floor_le_iff)

lemma floor_le_neg_numeral [simp]: "\x\ \ - numeral v \ x < - numeral v + 1"
  by (simp add: floor_le_iff)

lemma floor_less_zero [simp]: "\x\ < 0 \ x < 0"
  by (simp add: floor_less_iff)

lemma floor_less_one [simp]: "\x\ < 1 \ x < 1"
  by (simp add: floor_less_iff)

lemma floor_less_numeral [simp]: "\x\ < numeral v \ x < numeral v"
  by (simp add: floor_less_iff)

lemma floor_less_neg_numeral [simp]: "\x\ < - numeral v \ x < - numeral v"
  by (simp add: floor_less_iff)

lemma le_mult_floor_Ints:
  assumes "0 \ a" "a \ Ints"
  shows "of_int (\a\ * \b\) \ (of_int\a * b\ :: 'a :: linordered_idom)"
  by (metis Ints_cases assms floor_less_iff floor_of_int linorder_not_less mult_left_mono of_int_floor_le of_int_less_iff of_int_mult)

text \<open>Addition and subtraction of integers.\<close>

lemma floor_add_int: "\x\ + z = \x + of_int z\"
  using floor_correct [of x] by (simp add: floor_unique[symmetric])

lemma int_add_floor: "z + \x\ = \of_int z + x\"
  using floor_correct [of x] by (simp add: floor_unique[symmetric])

lemma one_add_floor: "\x\ + 1 = \x + 1\"
  using floor_add_int [of x 1] by simp

lemma floor_diff_of_int [simp]: "\x - of_int z\ = \x\ - z"
  using floor_add_int [of x "- z"] by (simp add: algebra_simps)

lemma floor_uminus_of_int [simp]: "\- (of_int z)\ = - z"
  by (metis floor_diff_of_int [of 0] diff_0 floor_zero)

lemma floor_diff_numeral [simp]: "\x - numeral v\ = \x\ - numeral v"
  using floor_diff_of_int [of x "numeral v"] by simp

lemma floor_diff_one [simp]: "\x - 1\ = \x\ - 1"
  using floor_diff_of_int [of x 1] by simp

lemma le_mult_floor:
  assumes "0 \ a" and "0 \ b"
  shows "\a\ * \b\ \ \a * b\"
proof -
  have "of_int \a\ \ a" and "of_int \b\ \ b"
    by (auto intro: of_int_floor_le)
  then have "of_int (\a\ * \b\) \ a * b"
    using assms by (auto intro!: mult_mono)
  also have "a * b < of_int (\a * b\ + 1)"
    using floor_correct[of "a * b"] by auto
  finally show ?thesis
    unfolding of_int_less_iff by simp
qed

lemma floor_divide_of_int_eq: "\of_int k / of_int l\ = k div l"
  for k l :: int
proof (cases "l = 0")
  case True
  then show ?thesis by simp
next
  case False
  have *: "\of_int (k mod l) / of_int l :: 'a\ = 0"
  proof (cases "l > 0")
    case True
    then show ?thesis
      by (auto intro: floor_unique)
  next
    case False
    obtain r where "r = - l"
      by blast
    then have l: "l = - r"
      by simp
    with \<open>l \<noteq> 0\<close> False have "r > 0"
      by simp
    with l show ?thesis
      using pos_mod_bound [of r]
      by (auto simp add: zmod_zminus2_eq_if less_le field_simps intro: floor_unique)
  qed
  have "(of_int k :: 'a) = of_int (k div l * l + k mod l)"
    by simp
  also have "\ = (of_int (k div l) + of_int (k mod l) / of_int l) * of_int l"
    using False by (simp only: of_int_add) (simp add: field_simps)
  finally have "(of_int k / of_int l :: 'a) = \ / of_int l"
    by simp
  then have "(of_int k / of_int l :: 'a) = of_int (k div l) + of_int (k mod l) / of_int l"
    using False by (simp only:) (simp add: field_simps)
  then have "\of_int k / of_int l :: 'a\ = \of_int (k div l) + of_int (k mod l) / of_int l :: 'a\"
    by simp
  then have "\of_int k / of_int l :: 'a\ = \of_int (k mod l) / of_int l + of_int (k div l) :: 'a\"
    by (simp add: ac_simps)
  then have "\of_int k / of_int l :: 'a\ = \of_int (k mod l) / of_int l :: 'a\ + k div l"
    by (simp add: floor_add_int)
  with * show ?thesis
    by simp
qed

lemma floor_divide_of_nat_eq: "\of_nat m / of_nat n\ = of_nat (m div n)"
  for m n :: nat
    by (metis floor_divide_of_int_eq of_int_of_nat_eq linordered_euclidean_semiring_class.of_nat_div)

lemma floor_divide_lower:
  fixes q :: "'a::floor_ceiling"
  shows "q > 0 \ of_int \p / q\ * q \ p"
  using of_int_floor_le pos_le_divide_eq by blast

lemma floor_divide_upper:
  fixes q :: "'a::floor_ceiling"
  shows "q > 0 \ p < (of_int \p / q\ + 1) * q"
  by (meson floor_eq_iff pos_divide_less_eq)

subsection \<open>Ceiling function\<close>

definition ceiling :: "'a::floor_ceiling \ int" (\(\open_block notation=\mixfix ceiling\\\_\)\)
  where "\x\ = - \- x\"

lemma ceiling_correct: "of_int \x\ - 1 < x \ x \ of_int \x\"
  unfolding ceiling_def using floor_correct [of "- x"]
  by (simp add: le_minus_iff)

lemma ceiling_unique: "of_int z - 1 < x \ x \ of_int z \ \x\ = z"
  unfolding ceiling_def using floor_unique [of "- z" "- x"] by simp

lemma ceiling_eq_iff: "\x\ = a \ of_int a - 1 < x \ x \ of_int a"
using ceiling_correct ceiling_unique by auto

lemma le_of_int_ceiling [simp]: "x \ of_int \x\"
  using ceiling_correct ..

lemma ceiling_le_iff: "\x\ \ z \ x \ of_int z"
  unfolding ceiling_def using le_floor_iff [of "- z" "- x"] by auto

lemma less_ceiling_iff: "z < \x\ \ of_int z < x"
  by (simp add: not_le [symmetric] ceiling_le_iff)

lemma ceiling_less_iff: "\x\ < z \ x \ of_int z - 1"
  using ceiling_le_iff [of x "z - 1"] by simp

lemma le_ceiling_iff: "z \ \x\ \ of_int z - 1 < x"
  by (simp add: not_less [symmetric] ceiling_less_iff)

lemma ceiling_mono: "x \ y \ \x\ \ \y\"
  unfolding ceiling_def by (simp add: floor_mono)

lemma ceiling_less_cancel: "\x\ < \y\ \ x < y"
  by (auto simp add: not_le [symmetric] ceiling_mono)

lemma ceiling_of_int [simp]: "\of_int z\ = z"
  by (rule ceiling_unique) simp_all

lemma ceiling_of_nat [simp]: "\of_nat n\ = int n"
  using ceiling_of_int [of "of_nat n"] by simp

lemma ceiling_add_le: "\x + y\ \ \x\ + \y\"
  by (simp only: ceiling_le_iff of_int_add add_mono le_of_int_ceiling)

lemma mult_ceiling_le:
  assumes "0 \ a" and "0 \ b"
  shows "\a * b\ \ \a\ * \b\"
  by (metis assms ceiling_le_iff ceiling_mono le_of_int_ceiling mult_mono of_int_mult)

lemma mult_ceiling_le_Ints:
  assumes "0 \ a" "a \ Ints"
  shows "(of_int \a * b\ :: 'a :: linordered_idom) \ of_int(\a\ * \b\)"
  by (metis Ints_cases assms ceiling_le_iff ceiling_of_int le_of_int_ceiling mult_left_mono of_int_le_iff of_int_mult)

lemma finite_int_segment:
  fixes a :: "'a::floor_ceiling"
  shows "finite {x \ \. a \ x \ x \ b}"
proof -
  have "finite {ceiling a..floor b}"
    by simp
  moreover have "{x \ \. a \ x \ x \ b} = of_int ` {ceiling a..floor b}"
    by (auto simp: le_floor_iff ceiling_le_iff elim!: Ints_cases)
  ultimately show ?thesis
    by simp
qed

corollary finite_abs_int_segment:
  fixes a :: "'a::floor_ceiling"
  shows "finite {k \ \. \k\ \ a}"
  using finite_int_segment [of "-a" a] by (auto simp add: abs_le_iff conj_commute minus_le_iff)

subsubsection \<open>Ceiling with numerals.\<close>

lemma ceiling_zero [simp]: "\0\ = 0"
  using ceiling_of_int [of 0] by simp

lemma ceiling_one [simp]: "\1\ = 1"
  using ceiling_of_int [of 1] by simp

lemma ceiling_numeral [simp]: "\numeral v\ = numeral v"
  using ceiling_of_int [of "numeral v"] by simp

lemma ceiling_neg_numeral [simp]: "\- numeral v\ = - numeral v"
  using ceiling_of_int [of "- numeral v"] by simp

lemma ceiling_le_zero [simp]: "\x\ \ 0 \ x \ 0"
  by (simp add: ceiling_le_iff)

lemma ceiling_le_one [simp]: "\x\ \ 1 \ x \ 1"
  by (simp add: ceiling_le_iff)

lemma ceiling_le_numeral [simp]: "\x\ \ numeral v \ x \ numeral v"
  by (simp add: ceiling_le_iff)

lemma ceiling_le_neg_numeral [simp]: "\x\ \ - numeral v \ x \ - numeral v"
  by (simp add: ceiling_le_iff)

lemma ceiling_less_zero [simp]: "\x\ < 0 \ x \ -1"
  by (simp add: ceiling_less_iff)

lemma ceiling_less_one [simp]: "\x\ < 1 \ x \ 0"
  by (simp add: ceiling_less_iff)

lemma ceiling_less_numeral [simp]: "\x\ < numeral v \ x \ numeral v - 1"
  by (simp add: ceiling_less_iff)

lemma ceiling_less_neg_numeral [simp]: "\x\ < - numeral v \ x \ - numeral v - 1"
  by (simp add: ceiling_less_iff)

lemma zero_le_ceiling [simp]: "0 \ \x\ \ -1 < x"
  by (simp add: le_ceiling_iff)

lemma one_le_ceiling [simp]: "1 \ \x\ \ 0 < x"
  by (simp add: le_ceiling_iff)

lemma numeral_le_ceiling [simp]: "numeral v \ \x\ \ numeral v - 1 < x"
  by (simp add: le_ceiling_iff)

lemma neg_numeral_le_ceiling [simp]: "- numeral v \ \x\ \ - numeral v - 1 < x"
  by (simp add: le_ceiling_iff)

lemma zero_less_ceiling [simp]: "0 < \x\ \ 0 < x"
  by (simp add: less_ceiling_iff)

lemma one_less_ceiling [simp]: "1 < \x\ \ 1 < x"
  by (simp add: less_ceiling_iff)

lemma numeral_less_ceiling [simp]: "numeral v < \x\ \ numeral v < x"
  by (simp add: less_ceiling_iff)

lemma neg_numeral_less_ceiling [simp]: "- numeral v < \x\ \ - numeral v < x"
  by (simp add: less_ceiling_iff)

lemma ceiling_altdef: "\x\ = (if x = of_int \x\ then \x\ else \x\ + 1)"
  by (intro ceiling_unique; simp, linarith?)

lemma floor_le_ceiling [simp]: "\x\ \ \x\"
  by (simp add: ceiling_altdef)

subsubsection \<open>Addition and subtraction of integers.\<close>

lemma ceiling_add_of_int [simp]: "\x + of_int z\ = \x\ + z"
  using ceiling_correct [of x] by (simp add: ceiling_def)

lemma ceiling_add_numeral [simp]: "\x + numeral v\ = \x\ + numeral v"
  using ceiling_add_of_int [of x "numeral v"] by simp

lemma ceiling_add_one [simp]: "\x + 1\ = \x\ + 1"
  using ceiling_add_of_int [of x 1] by simp

lemma ceiling_diff_of_int [simp]: "\x - of_int z\ = \x\ - z"
  using ceiling_add_of_int [of x "- z"] by (simp add: algebra_simps)

lemma ceiling_diff_numeral [simp]: "\x - numeral v\ = \x\ - numeral v"
  using ceiling_diff_of_int [of x "numeral v"] by simp

lemma ceiling_diff_one [simp]: "\x - 1\ = \x\ - 1"
  using ceiling_diff_of_int [of x 1] by simp

lemma ceiling_split[linarith_split]: "P \t\ \ (\i. of_int i - 1 < t \ t \ of_int i \ P i)"
  by (auto simp add: ceiling_unique ceiling_correct)

lemma ceiling_eq_imp_diff_1: "\x\ = \y\ \ \x-y\ < 1"
  unfolding ceiling_eq_iff by linarith

lemma ceiling_diff_floor_le_1: "\x\ - \x\ \ 1"
  by (simp add: ceiling_altdef)

lemma floor_eq_ceiling_imp_diff_2: "\x\ = \y\ \ \x-y\ < 2"
  unfolding floor_eq_iff by linarith

lemma nat_approx_posE:
  fixes e:: "'a::{archimedean_field,floor_ceiling}"
  assumes "0 < e"
  obtains n :: nat where "1 / of_nat(Suc n) < e"
proof
  have "(1::'a) / of_nat (Suc (nat \1/e\)) < 1 / of_int (\1/e\)"
  proof (rule divide_strict_left_mono)
    show "(of_int \1 / e\::'a) < of_nat (Suc (nat \1 / e\))"
      using assms by (simp add: field_simps)
    show "(0::'a) < of_nat (Suc (nat \1 / e\)) * of_int \1 / e\"
      using assms by (auto simp: zero_less_mult_iff pos_add_strict)
  qed auto
  also have "1 / of_int (\1/e\) \ 1 / (1/e)"
    by (rule divide_left_mono) (auto simp: \<open>0 < e\<close> ceiling_correct)
  also have "\ = e" by simp
  finally show  "1 / of_nat (Suc (nat \1 / e\)) < e"
    by metis
qed

lemma ceiling_divide_upper:
  fixes q :: "'a::floor_ceiling"
  shows "q > 0 \ p \ of_int (ceiling (p / q)) * q"
  by (meson divide_le_eq le_of_int_ceiling)

lemma ceiling_divide_lower:
  fixes q :: "'a::floor_ceiling"
  shows "q > 0 \ (of_int \p / q\ - 1) * q < p"
  by (meson ceiling_eq_iff pos_less_divide_eq)

subsection \<open>Negation\<close>

lemma floor_minus: "\- x\ = - \x\"
  unfolding ceiling_def by simp

lemma ceiling_minus: "\- x\ = - \x\"
  unfolding ceiling_def by simp

subsection \<open>Natural numbers\<close>

lemma of_nat_floor: "r\0 \ of_nat (nat \r\) \ r"
  by simp

lemma of_nat_ceiling: "of_nat (nat \r\) \ r"
  by (cases "r\0") auto

lemma of_nat_int_floor [simp]: "x\0 \ of_nat (nat\x\) = of_int \x\"
  by auto

lemma of_nat_int_ceiling [simp]: "x\0 \ of_nat (nat \x\) = of_int \x\"
  by auto

subsection \<open>Frac Function\<close>

definition frac :: "'a \ 'a::floor_ceiling"
  where "frac x \ x - of_int \x\"

lemma frac_lt_1: "frac x < 1"
  by (simp add: frac_def) linarith

lemma frac_eq_0_iff [simp]: "frac x = 0 \ x \ \"
  by (simp add: frac_def) (metis Ints_cases Ints_of_int floor_of_int )

lemma frac_ge_0 [simp]: "frac x \ 0"
  unfolding frac_def by linarith

lemma frac_gt_0_iff [simp]: "frac x > 0 \ x \ \"
  by (metis frac_eq_0_iff frac_ge_0 le_less less_irrefl)

lemma frac_of_int [simp]: "frac (of_int z) = 0"
  by (simp add: frac_def)

lemma frac_frac [simp]: "frac (frac x) = frac x"
  by (simp add: frac_def)

lemma floor_add: "\x + y\ = (if frac x + frac y < 1 then \x\ + \y\ else (\x\ + \y\) + 1)"
proof -
  have "x + y < 1 + (of_int \x\ + of_int \y\) \ \x + y\ = \x\ + \y\"
    by (metis add.commute floor_unique le_floor_add le_floor_iff of_int_add)
  moreover
  have "\ x + y < 1 + (of_int \x\ + of_int \y\) \ \x + y\ = 1 + (\x\ + \y\)"
    apply (simp add: floor_eq_iff)
    apply (auto simp add: algebra_simps)
    apply linarith
    done
  ultimately show ?thesis by (auto simp add: frac_def algebra_simps)
qed

lemma floor_add2[simp]: "x \ \ \ y \ \ \ \x + y\ = \x\ + \y\"
by (metis add.commute add.left_neutral frac_lt_1 floor_add frac_eq_0_iff)

lemma frac_add:
  "frac (x + y) = (if frac x + frac y < 1 then frac x + frac y else (frac x + frac y) - 1)"
  by (simp add: frac_def floor_add)

lemma frac_unique_iff: "frac x = a \ x - a \ \ \ 0 \ a \ a < 1"
  for x :: "'a::floor_ceiling"
  by (auto simp: Ints_def frac_def algebra_simps floor_unique; linarith)

lemma frac_eq: "frac x = x \ 0 \ x \ x < 1"
  by (simp add: frac_unique_iff)

lemma frac_eq_id [simp]: "x \ {0..<1} \ frac x = x"
  by (simp add: frac_eq)

lemma frac_in_Ints_iff [simp]: "frac x \ \ \ x \ \"
  by (metis frac_eq_0_iff frac_frac)

lemma frac_neg: "frac (- x) = (if x \ \ then 0 else 1 - frac x)"
  for x :: "'a::floor_ceiling"
  unfolding frac_unique_iff using frac_lt_1 [of x]
  apply (simp add: frac_def)
  by (metis Ints_of_int floor_eq_iff nless_le)

lemma frac_1_eq: "frac (x+1) = frac x"
  by (simp add: frac_def)

subsection \<open>Fractional part arithmetic\<close>
text \<open>Many thanks to Stepan Holub\<close>

lemma frac_non_zero: "frac x \ 0 \ frac (-x) = 1 - frac x"
  using frac_eq_0_iff frac_neg by metis

lemma frac_add_simps [simp]:
   "frac (frac a + b) = frac (a + b)"
   "frac (a + frac b) = frac (a + b)"
  by (simp_all add: frac_add)

lemma frac_neg_frac:  "frac (- frac x) = frac (-x)"
  unfolding frac_neg frac_frac by force

lemma frac_diff_simp: "frac (y - frac x) = frac (y - x)"
    unfolding diff_conv_add_uminus frac_add frac_neg_frac..

lemma frac_diff: "frac (a - b) = frac (frac a + (- frac b))"
  unfolding frac_add_simps(1)
  unfolding ab_group_add_class.ab_diff_conv_add_uminus[symmetric] frac_diff_simp..

lemma frac_diff_pos: "frac x \ frac y \ frac (y - x) = frac y - frac x"
  unfolding diff_conv_add_uminus frac_add frac_neg
  using frac_lt_1 by force

lemma frac_diff_neg: assumes "frac y < frac x"
  shows "frac (y - x) = frac y + 1 - frac x"
proof-
  have "x \ \"
    unfolding frac_gt_0_iff[symmetric]
    using assms frac_ge_0[of y] by order
  have "frac y + (1 + - frac x) < 1"
    using frac_lt_1[of x] assms by fastforce
  show ?thesis
    unfolding diff_conv_add_uminus frac_add frac_neg
    if_not_P[OF \<open>x \<notin> \<int>\<close>] if_P[OF \<open>frac y + (1 + - frac x) < 1\<close>]
    by simp
qed

lemma frac_diff_eq: assumes "frac y = frac x"
  shows "frac (y - x) = 0"
  by (simp add: assms frac_diff_pos)

lemma frac_diff_zero: assumes "frac (x - y) = 0"
  shows "frac x = frac y"
  using frac_add_simps(1)[of "x - y" y, symmetric]
  unfolding assms add.group_left_neutral diff_add_cancel.

lemma frac_neg_eq_iff: "frac (-x) = frac (-y) \ frac x = frac y"
  using add.inverse_inverse frac_neg_frac by metis

lemma frac_eqE:
  assumes "frac x = frac y"
  obtains n where "x = y + of_int n"
  by (rule that[of "floor x - floor y"]) (use assms in \<open>auto simp: frac_def\<close>)

lemma frac_add_of_int_right [simp]: "frac (x + of_int n) = frac x"
  by (auto simp: frac_def)

lemma frac_add_of_int_left [simp]: "frac (of_int n + x) = frac x"
  by (auto simp: frac_def)

lemma frac_add_int_right: "y \ \ \ frac (x + y) = frac x"
  by (elim Ints_cases) auto

lemma frac_add_int_left: "x \ \ \ frac (x + y) = frac y"
  by (elim Ints_cases) auto

lemma bij_betw_frac: "bij_betw frac {x..
  unfolding bij_betw_def
proof
  show "inj_on frac {x..
  proof
    fix a b assume *: "a \ {x.. {x..
    then obtain n where n: "a = b + of_int n"
      by (elim frac_eqE)
    have "\of_int n\ = \a - b\"
      using n by (simp add: algebra_simps)
    also have "\ < 1"
      using * by auto
    finally have "n = 0"
      by (simp flip: of_int_abs)
    with n show "a = b"
      by auto
  qed
next
  show "frac ` {x..
  proof (intro equalityI subsetI)
    fix t :: 'a assume t: "t \ {0..<1}"
    have "t = frac (if t \ frac x then x + t - frac x else x + t - frac x + 1)"
      using frac_eq[of t] t by (auto simp: frac_def)
    moreover have "(if t \ frac x then x + t - frac x else x + t - frac x + 1) \ {x..
      using frac_lt_1[of x] frac_ge_0[of x] t by (auto simp del: frac_ge_0)
    ultimately show "t \ frac ` {x..
      by blast
  qed (auto intro: frac_lt_1)
qed

subsection \<open>Rounding to the nearest integer\<close>

definition round :: "'a::floor_ceiling \ int"
  where "round x = \x + 1/2\"

lemma round_eq_imp_diff_1: "round x = round y \ \x-y\ < 1"
  unfolding round_def
  using floor_eq_imp_diff_1 by fastforce

lemma of_int_round_ge: "of_int (round x) \ x - 1/2"
  and of_int_round_le: "of_int (round x) \ x + 1/2"
  and of_int_round_abs_le: "\of_int (round x) - x\ \ 1/2"
  and of_int_round_gt: "of_int (round x) > x - 1/2"
proof -
  from floor_correct[of "x + 1/2"] have "x + 1/2 < of_int (round x) + 1"
    by (simp add: round_def)
  from add_strict_right_mono[OF this, of "-1"] show A: "of_int (round x) > x - 1/2"
    by simp
  then show "of_int (round x) \ x - 1/2"
    by simp
  from floor_correct[of "x + 1/2"] show "of_int (round x) \ x + 1/2"
    by (simp add: round_def)
  with A show "\of_int (round x) - x\ \ 1/2"
    by linarith
qed

lemma round_of_int [simp]: "round (of_int n) = n"
  unfolding round_def by (subst floor_eq_iff) force

lemma round_0 [simp]: "round 0 = 0"
  using round_of_int[of 0] by simp

lemma round_1 [simp]: "round 1 = 1"
  using round_of_int[of 1] by simp

lemma round_numeral [simp]: "round (numeral n) = numeral n"
  using round_of_int[of "numeral n"] by simp

lemma round_neg_numeral [simp]: "round (-numeral n) = -numeral n"
  using round_of_int[of "-numeral n"] by simp

lemma round_of_nat [simp]: "round (of_nat n) = of_nat n"
  using round_of_int[of "int n"] by simp

lemma round_mono: "x \ y \ round x \ round y"
  unfolding round_def by (intro floor_mono) simp

lemma round_unique: "of_int y > x - 1/2 \ of_int y \ x + 1/2 \ round x = y"
  unfolding round_def
proof (rule floor_unique)
  assume "x - 1 / 2 < of_int y"
  from add_strict_left_mono[OF this, of 1] show "x + 1 / 2 < of_int y + 1"
    by simp
qed

lemma round_unique': "\x - of_int n\ < 1/2 \ round x = n"
  by (subst (asm) abs_less_iff, rule round_unique) (simp_all add: field_simps)

lemma round_altdef: "round x = (if frac x \ 1/2 then \x\ else \x\)"
  by (cases "frac x \ 1/2")
    (rule round_unique, ((simp add: frac_def field_simps ceiling_altdef; linarith)+)[2])+

lemma floor_le_round: "\x\ \ round x"
  unfolding round_def by (intro floor_mono) simp

lemma ceiling_ge_round: "\x\ \ round x"
  unfolding round_altdef by simp

lemma round_diff_minimal: "\z - of_int (round z)\ \ \z - of_int m\"
  for z :: "'a::floor_ceiling"
proof (cases "of_int m \ z")
  case True
  then have "\z - of_int (round z)\ \ \of_int \z\ - z\"
    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith
  also have "of_int \z\ - z \ 0"
    by linarith
  with True have "\of_int \z\ - z\ \ \z - of_int m\"
    by (simp add: ceiling_le_iff)
  finally show ?thesis .
next
  case False
  then have "\z - of_int (round z)\ \ \of_int \z\ - z\"
    unfolding round_altdef by (simp add: field_simps ceiling_altdef frac_def) linarith
  also have "z - of_int \z\ \ 0"
    by linarith
  with False have "\of_int \z\ - z\ \ \z - of_int m\"
    by (simp add: le_floor_iff)
  finally show ?thesis .
qed

bundle floor_ceiling_syntax
begin
notation floor  (\<open>(\<open>open_block notation=\<open>mixfix floor\<close>\<close>\<lfloor>_\<rfloor>)\<close>)
  and ceiling  (\<open>(\<open>open_block notation=\<open>mixfix ceiling\<close>\<close>\<lceil>_\<rceil>)\<close>)
end

end

quality97%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.