Theory Eudoxus
theory Eudoxus
imports Slope
begin
section ‹Eudoxus Reals›
subsection ‹Type Definition›
text ‹Two slopes are said to be equivalent if their difference is bounded.›
definition eudoxus_rel :: "(int ⇒ int) ⇒ (int ⇒ int) ⇒ bool" (infix "∼⇩e" 50) where
"f ∼⇩e g ≡ slope f ∧ slope g ∧ bounded (λn. f n - g n)"
lemma eudoxus_rel_equivp:
"part_equivp eudoxus_rel"
proof (rule part_equivpI)
show "∃x. x ∼⇩e x" unfolding eudoxus_rel_def slope_def bounded_def by fast
show "symp (∼⇩e)" unfolding eudoxus_rel_def by (force intro: sympI dest: bounded_uminus simp: fun_Compl_def)
show "transp (∼⇩e)" unfolding eudoxus_rel_def by (force intro!: transpI dest: bounded_add)
qed
text ‹We define the reals as the set of all equivalence classes of the relation \<^term>‹eudoxus_rel›.›
quotient_type real = "(int ⇒ int)" / partial: eudoxus_rel
by (rule eudoxus_rel_equivp)
lemma real_quot_type: "quot_type (∼⇩e) Abs_real Rep_real"
using Rep_real Abs_real_inverse Rep_real_inverse Rep_real_inject eudoxus_rel_equivp by (auto intro!: quot_type.intro)
lemma slope_refl: "slope f = (f ∼⇩e f)"
unfolding eudoxus_rel_def by (fastforce simp add: bounded_constant)
declare slope_refl[THEN iffD2, simp]
lemmas slope_reflI = slope_refl[THEN iffD1]
lemma slope_induct[consumes 0, case_names slope]:
assumes "⋀f. slope f ⟹ P (abs_real f)"
shows "P x"
using assms by induct force
lemma abs_real_eq_iff: "f ∼⇩e g ⟷ slope f ∧ slope g ∧ abs_real f = abs_real g"
by (metis Quotient_real Quotient_rel slope_refl)
lemma abs_real_eqI[intro]: "f ∼⇩e g ⟹ abs_real f = abs_real g" using abs_real_eq_iff by blast
lemmas eudoxus_rel_sym[sym] = Quotient_symp[OF Quotient_real, THEN sympD]
lemmas eudoxus_rel_trans[trans] = Quotient_transp[OF Quotient_real, THEN transpD]
lemmas rep_real_abs_real_refl = Quotient_rep_abs[OF Quotient_real, OF slope_refl[THEN iffD1], intro!]
lemmas rep_real_iff = Quotient_rel_rep[OF Quotient_real, iff]
declare Quotient_abs_rep[OF Quotient_real, simp]
lemma slope_rep_real: "slope (rep_real x)" by simp
lemma eudoxus_relI:
assumes "slope f" "slope g" "⋀n. n ≥ N ⟹ ¦f n - g n¦ ≤ C"
shows "f ∼⇩e g"
proof -
have C_nonneg: "C ≥ 0" using assms by force
obtain C_f where C_f: "¦f (n + (- n)) - (f n + f (- n))¦ ≤ C_f" "0 ≤ C_f" for n using assms by fast
obtain C_g where C_g: "¦g (n + (- n)) - (g n + g (- n))¦ ≤ C_g" "0 ≤ C_g" for n using assms by fast
have bound: "¦f (- n) - g (- n)¦ ≤ ¦f n - g n¦ + ¦f 0¦ + ¦g 0¦ + C_f + C_g" for n using C_f(1)[of n] C_g(1)[of n] by simp
define C' where "C' = Sup {¦f n - g n¦ | n. n ∈ {0..max 0 N}} + C + ¦f 0¦ + ¦g 0¦ + C_f + C_g"
have *: "bdd_above {¦f n - g n¦ |n. n ∈ {0..max 0 N}}" by simp
have "Sup {¦f n - g n¦ |n. n ∈ {0..max 0 N}} ∈ {¦f n - g n¦ |n. n ∈ {0..max 0 N}}" using C_nonneg by (intro int_Sup_mem[OF _ *]) auto
hence Sup_nonneg: "Sup {¦f n - g n¦ | n. n ∈ {0..max 0 N}} ≥ 0" by fastforce
have *: "¦f n - g n¦ ≤ Sup {¦f n - g n¦ | n. n ∈ {0..max 0 N}} + C" if "n ≥ 0" for n unfolding C'_def using cSup_upper[OF _ *] that C_nonneg Sup_nonneg by (cases "n ≤ N") (fastforce simp add: add.commute add_increasing2 assms(3))+
{
fix n
have "¦f n - g n¦ ≤ C'"
proof (cases "n ≥ 0")
case True
thus ?thesis unfolding C'_def using * C_f C_g by fastforce
next
case False
hence "- n ≥ 0" by simp
hence "¦f (- n) - g (- n)¦ ≤ Sup {¦f n - g n¦ | n. n ∈ {0..max 0 N}} + C" using *[of "- n"] by blast
hence "¦f (- (- n)) - g (- (- n))¦ ≤ C'" unfolding C'_def using bound[of "- n"] by linarith
thus ?thesis by simp
qed
}
thus ?thesis using assms unfolding eudoxus_rel_def by (auto intro: boundedI)
qed
subsection ‹Addition and Subtraction›
text ‹We define addition, subtraction and the additive identity as follows.›
instantiation real :: "{zero, plus, minus, uminus}"
begin
quotient_definition
"0 :: real" is "abs_real (λ_. 0)" .
declare slope_zero[intro!, simp]
lemma zero_iff_bounded: "f ∼⇩e (λ_. 0) ⟷ bounded f" by (metis (no_types, lifting) boundedE boundedI diff_zero eudoxus_rel_def slope_zero bounded_slopeI)
lemma zero_iff_bounded': "x = 0 ⟷ bounded (rep_real x)" by (metis (mono_tags) abs_real_eq_iff id_apply rep_real_abs_real_refl rep_real_iff slope_zero zero_iff_bounded zero_real_def)
lemma zero_def: "0 = abs_real (λ_. 0)" unfolding zero_real_def by simp
definition eudoxus_plus :: "(int ⇒ int) ⇒ (int ⇒ int) ⇒ (int ⇒ int)" (infixl "+⇩e" 60) where
"(f :: int ⇒ int) +⇩e g = (λz. f z + g z)"
declare slope_add[intro, simp]
quotient_definition
"(+) :: (real ⇒ real ⇒ real)" is "(+⇩e)"
proof -
fix x x' y y' assume "x ∼⇩e x'" "y ∼⇩e y'"
hence rel_x: "slope x" "slope x'" "bounded (λz. x z - x' z)" and rel_y: "slope y" "slope y'" "bounded (λz. y z - y' z)" unfolding eudoxus_rel_def by blast+
thus "(x +⇩e y) ∼⇩e (x' +⇩e y')" unfolding eudoxus_rel_def eudoxus_plus_def by (fastforce intro: back_subst[of bounded, OF bounded_add[OF rel_x(3) rel_y(3)]])
qed
lemmas eudoxus_plus_cong = apply_rsp'[OF plus_real.rsp, THEN rel_funD, intro]
lemma abs_real_plus[simp]:
assumes "slope f" "slope g"
shows "abs_real f + abs_real g = abs_real (f +⇩e g)"
using assms unfolding plus_real_def by auto
definition eudoxus_uminus :: "(int ⇒ int) ⇒ (int ⇒ int)" ("-⇩e") where
"-⇩e (f :: int ⇒ int) = (λx. - f x)"
declare slope_uminus'[intro, simp]
quotient_definition
"(uminus) :: (real ⇒ real)" is "-⇩e"
proof -
fix x x' assume "x ∼⇩e x'"
hence rel_x: "slope x" "slope x'" "bounded (λz. x z - x' z)" unfolding eudoxus_rel_def by blast+
thus "-⇩e x ∼⇩e -⇩e x'" unfolding eudoxus_rel_def eudoxus_uminus_def by (fastforce intro: back_subst[of bounded, OF bounded_uminus[OF rel_x(3)]])
qed
lemmas eudoxus_uminus_cong = apply_rsp'[OF uminus_real.rsp, simplified, intro]
lemma abs_real_uminus[simp]:
assumes "slope f"
shows "- abs_real f = abs_real (-⇩e f)"
using assms unfolding uminus_real_def by auto
definition "x - (y::real) = x + - y"
declare slope_minus[intro, simp]
lemma abs_real_minus[simp]:
assumes "slope g" "slope f"
shows "abs_real g - abs_real f = abs_real (g +⇩e (-⇩e f))"
using assms by (simp add: minus_real_def slope_refl eudoxus_uminus_cong)
instance ..
end
text ‹The Eudoxus reals equipped with addition and negation specified as above constitute an Abelian group.›
instance real :: ab_group_add
proof
fix x y z :: real
show "x + y + z = x + (y + z)" by (induct x, induct y, induct z) (simp add: eudoxus_plus_cong eudoxus_plus_def add.assoc)
show "x + y = y + x" by (induct x, induct y) (simp add: eudoxus_plus_def add.commute)
show "0 + x = x" by (induct x) (simp add: zero_real_def eudoxus_plus_def)
show "- x + x = 0" by (induct x) (simp add: eudoxus_uminus_cong, simp add: zero_real_def eudoxus_plus_def eudoxus_uminus_def)
qed (simp add: minus_real_def)
subsection ‹Multiplication›
text ‹We define multiplication as the composition of two slopes.›
instantiation real :: "{one, times}"
begin
quotient_definition
"1 :: real" is "abs_real id" .
declare slope_one[intro!, simp]
lemma one_def: "1 = abs_real id" unfolding one_real_def by simp
definition eudoxus_times :: "(int ⇒ int) ⇒ (int ⇒ int) ⇒ int ⇒ int" (infixl "*⇩e" 60) where
"f *⇩e g = f o g"
declare slope_comp[intro, simp]
declare slope_scale[intro, simp]
quotient_definition
"(*) :: real ⇒ real ⇒ real" is "(*⇩e)"
proof -
fix x x' y y' assume "x ∼⇩e x'" "y ∼⇩e y'"
hence rel_x: "slope x" "slope x'" "bounded (λz. x z - x' z)" and rel_y: "slope y" "slope y'" "bounded (λz. y z - y' z)" unfolding eudoxus_rel_def by blast+
obtain C where x'_bound: "¦x' (m + n) - (x' m + x' n)¦ ≤ C" for m n using rel_x(2) unfolding slope_def by fastforce
obtain A B where x'_lin_bound: "¦x' n¦ ≤ A * ¦n¦ + B" "0 ≤ A" "0 ≤ B" for n using slope_linear_bound[OF rel_x(2)] by blast
obtain C' where y_y'_bound: "¦y z - y' z¦ ≤ C'" for z using rel_y(3) unfolding slope_def by fastforce
have "bounded (λz. x' (y z) - x' (y' z))"
proof (rule boundedI)
fix z
have "¦x' (y z) - x' (y' z)¦ ≤ ¦x' (y z - y' z)¦ + C" using x'_bound[of "y z - y' z" "y' z"] by fastforce
also have "... ≤ A * ¦y z - y' z¦ + B + C" using x'_lin_bound by force
also have "... ≤ A * C' + B + C" using mult_left_mono[OF y_y'_bound x'_lin_bound(2)] by fastforce
finally show "¦x' (y z) - x' (y' z)¦ ≤ A * C' + B + C" by blast
qed
hence "bounded (λz. x (y z) - x' (y' z))" using bounded_add[OF bounded_comp(1)[OF rel_x(3), of y]] by force
thus "(x *⇩e y) ∼⇩e (x' *⇩e y')" unfolding eudoxus_rel_def eudoxus_times_def using rel_x rel_y by simp
qed
lemmas eudoxus_times_cong = apply_rsp'[OF times_real.rsp, THEN rel_funD, intro]
lemmas eudoxus_rel_comp = eudoxus_times_cong[unfolded eudoxus_times_def]
lemma eudoxus_times_commute:
assumes "slope f" "slope g"
shows "(f *⇩e g) ∼⇩e (g *⇩e f)"
unfolding eudoxus_rel_def eudoxus_times_def
using slope_comp slope_comp_commute assms by blast
lemma abs_real_times[simp]:
assumes "slope f" "slope g"
shows "abs_real f * abs_real g = abs_real (f *⇩e g)"
using assms unfolding times_real_def by auto
instance ..
end
lemma neg_one_def: "- 1 = abs_real (-⇩e id)" unfolding one_real_def by (simp add: eudoxus_uminus_def)
lemma slope_neg_one[intro, simp]: "slope (-⇩e id)" using slope_refl by blast
text ‹With the definitions provided above, the Eudoxus reals are a commutative ring with unity.›
instance real :: comm_ring_1
proof
fix x y z :: real
show "x * y * z = x * (y * z)" by (induct x, induct y, induct z) (simp add: eudoxus_times_cong eudoxus_times_def comp_assoc)
show "x * y = y * x" by (induct x, induct y) (force simp add: slope_refl eudoxus_times_commute)
show "1 * x = x" by (induct x) (simp add: one_real_def eudoxus_times_def)
show "(x + y) * z = x * z + y * z" by (induct x, induct y, induct z) (simp add: eudoxus_times_cong eudoxus_plus_cong, simp add: eudoxus_times_def eudoxus_plus_def comp_def)
have "¬bounded (λx. x)" by (metis add.inverse_inverse boundedE_strict less_irrefl neg_less_0_iff_less zabs_def)
thus "(0 :: real) ≠ (1 :: real)" using abs_real_eq_iff[of id "λ_. 0"] unfolding one_real_def zero_real_def eudoxus_rel_def by simp
qed
lemma real_of_nat:
"of_nat n = abs_real ((*) (of_nat n))"
proof (induction n)
case 0
then show ?case by (simp add: zero_real_def)
next
case (Suc n)
then show ?case by (simp add: one_real_def distrib_right eudoxus_plus_def)
qed
lemma real_of_int:
"of_int z = abs_real ((*) z)"
proof (induction z rule: int_induct[where ?k=0])
case base
then show ?case by (simp add: zero_real_def)
next
case (step1 i)
then show ?case by (simp add: one_real_def distrib_right eudoxus_plus_def)
next
case (step2 i)
then show ?case by (simp add: one_real_def eudoxus_plus_def left_diff_distrib eudoxus_uminus_def)
qed
text ‹The Eudoxus reals are a ring of characteristic \<^term>‹0›.›
instance real :: ring_char_0
proof
show "inj (λn. of_nat n :: real)"
proof (intro inj_onI)
fix x y assume "(of_nat x :: real) = of_nat y"
hence "((*) (int x)) ∼⇩e ((*) (int y))" unfolding abs_real_eq_iff real_of_nat using slope_scale by blast
hence "bounded (λz. (int x - int y) * z)" unfolding eudoxus_rel_def by (simp add: left_diff_distrib)
then obtain C where bound: "¦(int x - int y) * z¦ ≤ C" and C_nonneg: "0 ≤ C" for z by blast
hence "¦int x - int y¦ * ¦C + 1¦ ≤ C" using abs_mult by metis
hence *: "¦int x - int y¦ * (C + 1) ≤ C" using C_nonneg by force
thus "x = y" using order_trans[OF mult_right_mono *, of 1] C_nonneg by fastforce
qed
qed
subsection ‹Ordering›
text ‹We call a slope positive, if it tends to infinity. Similarly, we call a slope negative if it tends to negative infinity.›
instantiation real :: "{ord, abs, sgn}"
begin
definition pos :: "(int ⇒ int) ⇒ bool" where
"pos f = (∀C ≥ 0. ∃N. ∀n ≥ N. f n ≥ C)"
definition neg :: "(int ⇒ int) ⇒ bool" where
"neg f = (∀C ≥ 0. ∃N. ∀n ≥ N. f n ≤ -C)"
lemma pos_neg_exclusive: "¬ (pos f ∧ neg f)" unfolding neg_def pos_def by (metis int_one_le_iff_zero_less linorder_not_less nle_le uminus_int_code(1) zero_less_one_class.zero_le_one)
lemma pos_iff_neg_uminus: "pos f = neg (-⇩e f)" unfolding neg_def pos_def eudoxus_uminus_def by simp
lemma neg_iff_pos_uminus: "neg f = pos (-⇩e f)" unfolding neg_def pos_def eudoxus_uminus_def by fastforce
lemma pos_iff:
assumes "slope f"
shows "pos f = infinite (f ` {0..} ∩ {0<..})" (is "?lhs = ?rhs")
proof (rule iffI)
assume pos: ?lhs
{
fix C assume C_nonneg: "0 ≤ (C :: int)"
hence "∃z ≥ 0. (C + 1) ≤ f z" by (metis add_increasing2 nle_le zero_less_one_class.zero_le_one pos pos_def)
hence "∃z ≥ 0. C ≤ f z ∧ 0 < f z" using C_nonneg by fastforce
hence "∃N≥C. ∃z. N = f z ∧ 0 < f z ∧ 0 ≤ z" by blast
}
thus ?rhs by (blast intro!: int_set_infiniteI)
next
assume infinite: ?rhs
then obtain D where D_bound: "¦f (m + n) - (f m + f n)¦ < D" "0 < D" for m n using assms by (fastforce simp: slope_def elim: boundedE_strict)
obtain M where M_bound: "∀m>0. (m + 1) * D ≤ f (m * M)" "0 < M" using slope_positive_lower_bound[OF assms infinite] D_bound(2) by blast
define g where "g = (λz. f ((z div M) * M))"
define E where "E = Sup ((abs o f) ` {z. 0 ≤ z ∧ z < M})"
have E_bound: "¦f (z mod M)¦ ≤ E" for z
proof -
have "(z mod M) ∈ {z. 0 ≤ z ∧ z < M}" by (simp add: M_bound(2))
hence "¦f (z mod M)¦ ∈ (abs o f) ` {z. 0 ≤ z ∧ z < M}" by fastforce
thus "¦f (z mod M)¦ ≤ E" unfolding E_def by (simp add: le_cSup_finite)
qed
hence E_nonneg: "0 ≤ E" by fastforce
have diff_bound: "¦f z - g z¦ ≤ E + D" for z
proof-
let ?d = "z div M" and ?r = "z mod M"
have z_is: "z = ?d * M + ?r" by presburger
hence "¦f z - g z¦ = ¦f (?d * M + ?r) - g (?d * M + ?r)¦" by argo
also have "... = ¦(f (?d*M + ?r) - (f (?d * M) + f ?r)) + (f (?d * M) + f ?r) - g (?d * M + ?r)¦" by auto
also have "... = ¦f ?r + (f (?d*M + ?r) - (f (?d * M) + f ?r))¦" unfolding g_def by force
also have "... ≤ ¦f ?r¦ + D" using D_bound(1)[of "?d * M" "?r"] by linarith
also have "... ≤ E + D" using E_bound by simp
finally show "¦f z - g z¦ ≤ E + D" .
qed
{
fix C assume C_nonneg: "0 ≤ (C :: int)"
define n where "n = (E + D + C) div D"
hence zero_less_n: "n > 0" using D_bound(2) E_nonneg C_nonneg using pos_imp_zdiv_pos_iff by fastforce
have "E + C < E + D + C - (E + D + C) mod D" using diff_strict_left_mono[OF pos_mod_bound[OF D_bound(2)]] by simp
also have "... = n * D" unfolding n_def using div_mod_decomp_int[of "E + D + C" D] by algebra
finally have *: "(n + 1) * D > E + D + C" by (simp add: add.commute distrib_right)
have "C ≤ f m" if "m ≥ n * M" for m
proof -
let ?d = "m div M" and ?r = "m mod M"
have d_pos: "?d > 0" using zero_less_n M_bound that dual_order.trans pos_imp_zdiv_pos_iff by fastforce
have n_le_d: "?d ≥ n" using zdiv_mono1 M_bound that by fastforce
have "E + D + C < (?d + 1) * D" using D_bound n_le_d by (intro *[THEN order.strict_trans2]) simp
also have "... ≤ g m" unfolding g_def using M_bound d_pos by blast
finally have "E + D + C < g m" .
hence "¦f m - g m¦ + C < g m" using diff_bound[of m] by fastforce
thus ?thesis by fastforce
qed
hence "∃N. ∀p≥N. C ≤ f p" using add1_zle_eq by blast
}
thus ?lhs unfolding pos_def by blast
qed
lemma neg_iff:
assumes "slope f"
shows "neg f = infinite (f ` {0..} ∩ {..<0})" (is "?lhs = ?rhs")
proof (rule iffI)
assume ?lhs
hence "infinite ((- f) ` {0..} ∩ {0<..})" using pos_iff[OF slope_uminus'[OF assms]] unfolding neg_def pos_def by fastforce
moreover have "inj (uminus :: int ⇒ int)" by simp
moreover have "(- f) ` {0..} ∩ {0<..} = uminus ` (f ` {0..} ∩ {..<0})" by fastforce
ultimately show ?rhs using finite_imageD by fastforce
next
assume ?rhs
moreover have "inj (uminus :: int ⇒ int)" by simp
moreover have "f ` {0..} ∩ {..<0} = uminus ` ((- f) ` {0..} ∩ {0<..})" by force
ultimately have "infinite ((- f) ` {0..} ∩ {0<..})" using finite_imageD by force
thus ?lhs using pos_iff[OF slope_uminus'[OF assms]] unfolding pos_def neg_def by fastforce
qed
lemma pos_cong:
assumes "f ∼⇩e g"
shows "pos f = pos g"
proof -
{
fix x y assume asm: "pos x" "x ∼⇩e y"
fix D assume D: "0 ≤ D" "∀N. ∃p≥N. ¬ D ≤ y p"
obtain C where bounds: "∀n. ¦x n - y n¦ ≤ C" "0 ≤ C" using asm unfolding eudoxus_rel_def by blast
obtain N where "∀p≥N. C + D ≤ x p" using D bounds asm by (fastforce simp add: pos_def)
hence "∀p≥N. ¦x p - y p¦ + D ≤ x p" by (metis add.commute add_left_mono bounds(1) dual_order.trans)
hence "∀p≥N. D ≤ y p" by force
hence False using D by blast
}
hence "pos x ⟹ pos y" if "x ∼⇩e y" for x y using that unfolding pos_def by metis
thus ?thesis by (metis assms eudoxus_rel_equivp part_equivp_symp)
qed
lemma neg_cong:
assumes "f ∼⇩e g"
shows "neg f = neg g"
proof -
{
fix x y assume asm: "neg x" "x ∼⇩e y"
fix D assume D: "0 ≤ D" "∀N. ∃p≥N. ¬ - D ≥ y p"
obtain C where bounds: "¦x n - y n¦ ≤ C" "0 ≤ C" for n using asm unfolding eudoxus_rel_def by blast
obtain N where "∀p≥N. - (C + D) ≥ x p" using D bounds asm add_increasing2 unfolding neg_def by meson
hence "∀p≥N. - ¦x p - y p¦ - D ≥ x p" using bounds(1)[THEN le_imp_neg_le, THEN diff_right_mono, THEN dual_order.trans] by simp
hence "∀p≥N. - D ≥ y p" by force
hence False using D by blast
}
hence "neg x ⟹ neg y" if "x ∼⇩e y" for x y using that unfolding neg_def by metis
thus ?thesis by (metis assms eudoxus_rel_equivp part_equivp_symp)
qed
lemma pos_iff_nonneg_nonzero:
assumes "slope f"
shows "pos f ⟷ (¬ neg f) ∧ (¬ bounded f)" (is "?lhs ⟷ ?rhs")
proof (rule iffI)
assume pos: ?lhs
then obtain N where "∀n≥N. f n > 0" unfolding pos_def by (metis int_one_le_iff_zero_less zero_less_one_class.zero_le_one)
hence "f (max N m) > 0" for m by simp
hence "¬ neg f" unfolding neg_def by (metis add.inverse_neutral dual_order.refl linorder_not_le max.cobounded2)
thus ?rhs using pos unfolding pos_def bounded_def bdd_above_def by (metis abs_ge_self dual_order.trans gt_ex imageI iso_tuple_UNIV_I order.strict_iff_not)
next
assume nonneg_nonzero: ?rhs
hence finite: "finite (f ` {0..} ∩ {..<0})" using neg_iff assms by blast
moreover have unbounded: "infinite (f ` {0..})" using nonneg_nonzero bounded_iff_finite_range slope_finite_range_iff assms by blast
ultimately have "infinite (f ` {0..} ∩ {0..})" by (metis Compl_atLeast Diff_Diff_Int Diff_eq Diff_infinite_finite)
moreover have "f ` {0..} ∩ {0<..} = f ` {0..} ∩ {0..} - {0}" by force
ultimately show ?lhs unfolding pos_iff[OF assms] by simp
qed
lemma neg_iff_nonpos_nonzero:
assumes "slope f"
shows "neg f ⟷ (¬ pos f) ∧ (¬ bounded f)"
unfolding pos_iff_nonneg_nonzero[OF assms] neg_iff_pos_uminus uminus_apply
eudoxus_uminus_def pos_iff_nonneg_nonzero[OF slope_uminus', OF assms]
by (force simp add: bounded_def bdd_above_def)
text ‹We define the sign of a slope to be \<^term>‹id› if it is positive, \<^term>‹-⇩e id› if it is negative and \<^term>‹(λ_. 0)› otherwise.›
definition eudoxus_sgn :: "(int ⇒ int) ⇒ (int ⇒ int)" where
"eudoxus_sgn f = (if pos f then id else if neg f then -⇩e id else (λ_. 0))"
lemma eudoxus_sgn_iff:
assumes "slope f"
shows "eudoxus_sgn f = (λ_. 0) ⟷ bounded f"
"eudoxus_sgn f = id ⟷ pos f"
"eudoxus_sgn f = (-⇩e id) ⟷ neg f"
using eudoxus_sgn_def neg_one_def one_def zero_def assms neg_iff_nonpos_nonzero pos_iff_nonneg_nonzero by auto
quotient_definition
"(sgn :: real ⇒ real)" is eudoxus_sgn
unfolding eudoxus_sgn_def
using eudoxus_uminus_cong neg_cong pos_cong slope_one slope_refl by fastforce
lemmas eudoxus_sgn_cong = apply_rsp'[OF sgn_real.rsp, intro]
lemma eudoxus_sgn_cong'[cong]:
assumes "f ∼⇩e g"
shows "eudoxus_sgn f = eudoxus_sgn g"
using assms eudoxus_sgn_def neg_cong pos_cong by presburger
lemma sgn_range: "sgn (x :: real) ∈ {-1, 0, 1}" unfolding sgn_real_def zero_def one_def neg_one_def eudoxus_sgn_def by simp
lemma sgn_abs_real_zero_iff:
assumes "slope f"
shows "sgn (abs_real f) = 0 ⟷ (eudoxus_sgn f = (λ_. 0))" (is "?lhs ⟷ ?rhs")
using eudoxus_sgn_cong[OF rep_real_abs_real_refl, OF assms] abs_real_eqI eudoxus_sgn_def neg_one_def one_def zero_def
by (auto simp add: sgn_real_def)
lemma sgn_zero_iff[simp]: "sgn (x :: real) = 0 ⟷ x = 0"
using eudoxus_sgn_iff(1) sgn_abs_real_zero_iff zero_iff_bounded' slope_refl
by (induct x) (metis (mono_tags) rep_real_abs_real_refl rep_real_iff)
lemma sgn_zero[simp]: "sgn (0 :: real) = 0" by simp
lemma sgn_abs_real_one_iff:
assumes "slope f"
shows "sgn (abs_real f) = 1 ⟷ pos f"
using eudoxus_sgn_cong[OF rep_real_abs_real_refl, OF assms] abs_real_eqI eudoxus_sgn_def neg_one_def one_def zero_def
by (auto simp add: sgn_real_def)
lemmas sgn_pos = sgn_abs_real_one_iff[THEN iffD2, simp]
lemma sgn_one[simp]: "sgn (1 :: real) = 1" by (subst one_def) (fastforce simp add: pos_def iff: sgn_abs_real_one_iff)
lemma sgn_abs_real_neg_one_iff:
assumes "slope f"
shows "sgn (abs_real f) = - 1 ⟷ neg f"
using eudoxus_sgn_cong[OF rep_real_abs_real_refl, OF assms] abs_real_eqI eudoxus_sgn_def neg_one_def one_def zero_def pos_neg_exclusive
by (auto simp add: sgn_real_def)
lemmas sgn_neg = sgn_abs_real_neg_one_iff[THEN iffD2, simp]
lemma sgn_neg_one[simp]: "sgn (- 1 :: real) = - 1" by (subst neg_one_def) (fastforce simp add: neg_def eudoxus_uminus_def iff: sgn_abs_real_neg_one_iff)
lemma sgn_plus:
assumes "sgn x = (1 :: real)" "sgn y = 1"
shows "sgn (x + y) = 1"
proof -
have pos: "pos (rep_real x)" "pos (rep_real y)" using assms sgn_abs_real_one_iff[OF slope_rep_real] by simp+
{
fix C :: int assume C_nonneg: "C ≥ 0"
then obtain N M where "∀n≥N. rep_real x n ≥ C" "∀n≥M. rep_real y n ≥ C" using pos unfolding pos_def by presburger
hence "∀n≥ max N M. (rep_real x +⇩e rep_real y) n ≥ C" using C_nonneg unfolding eudoxus_plus_def by fastforce
hence "∃N. ∀n ≥ N. (rep_real x +⇩e rep_real y) n ≥ C" by blast
}
thus ?thesis using pos_def by (simp add: eudoxus_plus_cong plus_real_def)
qed
lemma sgn_times: "sgn ((x :: real) * y) = sgn x * sgn y"
proof (cases "x = 0 ∨ y = 0")
case False
have *: "⟦x ≠ 0; pos (rep_real y)⟧ ⟹ sgn ((x :: real) * y) = sgn x * sgn y" for x y
proof (induct x rule: slope_induct, induct y rule: slope_induct)
case (slope y x)
hence pos_y: "pos y" using pos_cong by blast
show ?case
proof (cases "pos x")
case pos_x: True
{
fix C :: int assume asm: "C ≥ 0"
then obtain N where N: "∀n ≥ N. x n ≥ C" using pos_x unfolding pos_def by blast
then obtain N' where "∀n≥ N'. y n ≥ max 0 N" using pos_y unfolding pos_def by (meson max.cobounded1)
hence "∃N'. ∀n≥ N'. x (y n) ≥ C" using N by force
}
hence "pos (x *⇩e y)" unfolding pos_def eudoxus_times_def by simp
thus ?thesis using pos_x pos_y slope by (simp add: eudoxus_times_def)
next
case _: False
hence neg_x: "neg x" using slope by (metis abs_real_eqI neg_iff_nonpos_nonzero zero_def zero_iff_bounded)
{
fix C :: int assume "C ≥ 0"
then obtain N where N: "∀n ≥ N. x n ≤ - C" using neg_x unfolding neg_def by blast
then obtain N' where "∀n≥ N'. y n ≥ max 0 N" using pos_y unfolding pos_def by (meson max.cobounded1)
hence "∃N'. ∀n≥ N'. x (y n) ≤ -C" using N by force
}
hence "neg (x *⇩e y)" unfolding neg_def eudoxus_times_def by simp
thus ?thesis using neg_x pos_y slope by (simp add: eudoxus_times_def)
qed
qed
moreover have "sgn ((x :: real) * y) = sgn x * sgn y" if neg_x: "neg (rep_real x)" and neg_y: "neg (rep_real y)" for x y
proof -
have pos_uminus_y: "pos (rep_real (- y))" by (metis abs_real_eq_iff eudoxus_uminus_cong map_fun_apply neg_iff_pos_uminus neg_y pos_cong rep_real_abs_real_refl rep_real_iff uminus_real_def)
moreover have "x ≠ 0" using neg_iff_nonpos_nonzero neg_x zero_iff_bounded' by fastforce
ultimately have "sgn (- (x * y)) = - 1" using sgn_neg[OF slope_rep_real neg_x] sgn_pos[OF slope_rep_real pos_uminus_y] * by fastforce
hence "pos (rep_real (x * y))" by (metis eudoxus_uminus_cong map_fun_apply pos_iff_neg_uminus sgn_abs_real_neg_one_iff slope_refl slope_rep_real uminus_real_def)
thus ?thesis using sgn_neg[OF slope_rep_real] sgn_pos[OF slope_rep_real] neg_x neg_y by simp
qed
ultimately show ?thesis using False neg_iff_nonpos_nonzero[OF slope_rep_real] zero_iff_bounded'
by (cases "pos (rep_real x)" ; cases "pos (rep_real y)") (fastforce simp add: mult.commute)+
qed (force)
lemma sgn_uminus: "sgn (- (x :: real)) = - sgn x" by (metis (mono_tags, lifting) mult_minus1 sgn_neg_one sgn_times)
lemma sgn_plus':
assumes "sgn x = (-1 :: real)" "sgn y = -1"
shows "sgn (x + y) = -1"
using assms sgn_uminus[of x] sgn_uminus[of y] sgn_uminus[of "x + y"] sgn_plus[of "- x" "- y"]
by (simp add: equation_minus_iff)
lemma pos_dual_def:
assumes "slope f"
shows "pos f = (∀C ≥ 0. ∃N. ∀n ≤ N. f n ≤ -C)"
proof-
have "pos f = neg (f *⇩e (-⇩e id))" by (metis abs_real_eq_iff abs_real_times add.inverse_inverse assms eudoxus_times_commute mult_minus1_right neg_one_def sgn_abs_real_neg_one_iff sgn_abs_real_one_iff sgn_uminus slope_neg_one)
also have "... = (∀C ≥ 0. ∃N. ∀n ≥ N. (f (- n)) ≤ -C)" unfolding neg_def eudoxus_times_def eudoxus_uminus_def by simp
also have "... = (∀C ≥ 0. ∃N. ∀n ≤ N. f n ≤ -C)" by (metis add.inverse_inverse minus_le_iff)
finally show ?thesis .
qed
lemma neg_dual_def:
assumes "slope f"
shows "neg f = (∀C ≥ 0. ∃N. ∀n ≤ N. f n ≥ C)"
unfolding neg_iff_pos_uminus using assms by (subst pos_dual_def) (auto simp add: eudoxus_uminus_def)
lemma pos_representative:
assumes "slope f" "pos f"
obtains g where "f ∼⇩e g" "⋀n. n ≥ N ⟹ g n ≥ C"
proof -
obtain N' where N': "∀z≥N'. f z ≥ max 0 C" using assms unfolding pos_def by (meson max.cobounded1)
have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
hence "abs_real f * 1 = abs_real (f *⇩e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
hence "f ∼⇩e (f *⇩e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
moreover have "∀z≥N. (f *⇩e (λx. x + N' - N)) z ≥ C" unfolding eudoxus_times_def using N' by simp
ultimately show ?thesis using that by blast
qed
lemma pos_representative':
assumes "slope f" "pos f"
obtains g where "f ∼⇩e g" "⋀n. g n ≥ C ⟹ n ≥ N"
proof -
obtain N' where "∀z ≤ N'. f z ≤ - (max 0 (- C) + 1)" using assms unfolding pos_dual_def[OF assms(1)] by (metis max.cobounded1 add_increasing2 zero_less_one_class.zero_le_one)
hence N': "∀z ≤ N'. f z < min 0 C" by fastforce
have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
hence "abs_real f * 1 = abs_real (f *⇩e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
hence "f ∼⇩e (f *⇩e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
moreover have "∀z<N. (f *⇩e (λx. x + N' - N)) z < C" unfolding eudoxus_times_def using N' by simp
ultimately show ?thesis using that by (meson linorder_not_less)
qed
lemma neg_representative:
assumes "slope f" "neg f"
obtains g where "f ∼⇩e g" "⋀n. n ≥ N ⟹ g n ≤ - C"
proof -
obtain N' where "∀z≥N'. f z ≤ - max 0 C" using assms unfolding neg_def by (meson max.cobounded1)
hence N': "∀z≥N'. f z ≤ min 0 (- C)" by force
have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
hence "abs_real f * 1 = abs_real (f *⇩e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
hence "f ∼⇩e (f *⇩e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
moreover have "∀z≥N. (f *⇩e (λx. x + N' - N)) z ≤ - C" unfolding eudoxus_times_def using N' by simp
ultimately show ?thesis using that by blast
qed
lemma neg_representative':
assumes "slope f" "neg f"
obtains g where "f ∼⇩e g" "⋀n. g n ≤ - C ⟹ n ≥ N"
proof -
obtain N' where "∀z ≤ N'. f z ≥ max 0 (- C) + 1" using assms unfolding neg_dual_def[OF assms(1)] by (metis max.cobounded1 add_increasing2 zero_less_one_class.zero_le_one)
hence N': "∀z ≤ N'. f z > max 0 (- C)" by fastforce
have *: "1 = abs_real (λx. x + N' - N)" "slope (λx. x + N' - N)" unfolding one_def by (intro abs_real_eqI) (auto simp add: eudoxus_rel_def slope_def intro!: boundedI)
hence "abs_real f * 1 = abs_real (f *⇩e (λx. x + N' - N))" using abs_real_times[OF assms(1) *(2)] by simp
hence "f ∼⇩e (f *⇩e (λx. x + N' - N))" using assms * by (metis abs_real_eq_iff eudoxus_times_commute mult.right_neutral)
moreover have "∀z < N. (f *⇩e (λx. x + N' - N)) z > - C" unfolding eudoxus_times_def using N' by simp
ultimately show ?thesis using that by (meson linorder_not_less)
qed
text ‹We call a real \<^term>‹x› less than another real \<^term>‹y›, if their difference is positive.›
definition
"x < (y::real) ≡ sgn (y - x) = 1"
definition
"x ≤ (y::real) ≡ x < y ∨ x = y"
definition
abs_real: "¦x :: real¦ = (if 0 ≤ x then x else - x)"
instance ..
end
instance real :: linorder
proof
fix x y z :: real
show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" unfolding less_eq_real_def less_real_def using sgn_times[of "-1" "x - y"] by fastforce
show "x ≤ x" unfolding less_eq_real_def by blast
show "⟦x ≤ y; y ≤ z⟧ ⟹ x ≤ z" unfolding less_eq_real_def less_real_def using sgn_plus by fastforce
show "⟦x ≤ y; y ≤ x⟧ ⟹ x = y" unfolding less_eq_real_def less_real_def using sgn_times[of "-1" "x - y"] by fastforce
show "x ≤ y ∨ y ≤ x" unfolding less_eq_real_def less_real_def using sgn_times[of "-1" "x - y"] sgn_range by force
qed
lemma real_leI:
assumes "sgn (y - x) ∈ {0 :: real, 1}"
shows "x ≤ y"
using assms unfolding less_eq_real_def less_real_def by force
lemma real_lessI:
assumes "sgn (y - x) = (1 :: real)"
shows "x < y"
using assms unfolding less_real_def by blast
lemma abs_real_leI:
assumes "slope f" "slope g" "⋀z. z ≥ N ⟹ f z ≥ g z"
shows "abs_real f ≥ abs_real g"
proof -
{
assume "abs_real f ≠ abs_real g"
hence "abs_real (f +⇩e -⇩e g) ≠ 0" by (metis abs_real_minus assms(1,2) eq_iff_diff_eq_0)
hence "¬ bounded (f +⇩e -⇩e g)" by (metis abs_real_eqI zero_def zero_iff_bounded)
hence "pos (f +⇩e -⇩e g) ∨ neg (f +⇩e -⇩e g)" using assms eudoxus_plus_cong eudoxus_uminus_cong neg_iff_nonpos_nonzero slope_refl by auto
moreover
{
assume "neg (f +⇩e -⇩e g)"
then obtain N' where "(f +⇩e -⇩e g) z ≤ - 1" if "z ≥ N'" for z unfolding neg_def by fastforce
hence "f z < g z" if "z ≥ N'" for z using that unfolding eudoxus_plus_def eudoxus_uminus_def by fastforce
hence False using assms by (metis linorder_not_less nle_le)
}
ultimately have "abs_real f > abs_real g" using assms by (fastforce intro: real_lessI sgn_pos simp add: eudoxus_plus_def eudoxus_uminus_def)
}
thus ?thesis unfolding less_eq_real_def by argo
qed
lemma abs_real_lessI:
assumes "slope f" "slope g" "⋀z. z ≥ N ⟹ f z ≥ g z" "⋀C. C ≥ 0 ⟹ ∃z. f z ≥ g z + C"
shows "abs_real f > abs_real g"
proof -
{
assume "bounded (f +⇩e -⇩e g)"
then obtain C where "¦f z - g z¦ ≤ C" "C ≥ 0" for z unfolding eudoxus_plus_def eudoxus_uminus_def by auto
moreover obtain z where "f z ≥ g z + (C + 1)" using assms(4)[of "C + 1"] calculation by auto
ultimately have False by (metis abs_le_D1 add.commute dual_order.trans le_diff_eq linorder_not_less zless_add1_eq)
}
moreover have "abs_real f ≥ abs_real g" using assms abs_real_leI by blast
ultimately show ?thesis by (metis abs_real_minus assms(1,2) eq_iff_diff_eq_0 eudoxus_plus_cong eudoxus_sgn_iff(1) eudoxus_uminus_cong order_le_imp_less_or_eq sgn_abs_real_zero_iff sgn_zero slope_refl)
qed
lemma abs_real_lessD:
assumes "slope f" "slope g" "abs_real f > abs_real g"
obtains z where "z ≥ N" "f z > g z"
proof -
{
assume "∃N. ∀z≥N. f z ≤ g z"
then obtain N where "f z ≤ g z" if "z ≥ N" for z by fastforce
hence False using assms abs_real_leI by (metis linorder_not_le)
}
thus ?thesis using that by fastforce
qed
subsection ‹Multiplicative Inverse›
text ‹We now define the multiplicative inverse. We start by constructing a candidate for positive slopes first and then extend it to the entire domain using the choice function \<^term>‹Eps›.›
instantiation real :: "{inverse}"
begin
definition eudoxus_pos_inverse :: "(int ⇒ int) ⇒ (int ⇒ int)" where
"eudoxus_pos_inverse f z = sgn z * Inf ({0..} ∩ {n. f n ≥ ¦z¦})"
lemma eudoxus_pos_inverse:
assumes "slope f" "pos f"
obtains g where "f ∼⇩e g" "slope (eudoxus_pos_inverse g)" "eudoxus_pos_inverse g *⇩e f ∼⇩e id"
proof -
let ?φ = eudoxus_pos_inverse
obtain g where g: "f ∼⇩e g" "g z ≥ 0 ⟹ z > 1" for z using pos_representative'[OF assms] by (metis gt_ex order_less_le_trans)
hence pos_g: "pos g" using assms pos_cong by blast
have slope_g: "slope g" using g unfolding eudoxus_rel_def by simp
have "∃n ≥ 0. g n ≥ ¦z¦" for z using pos_g unfolding pos_def by (metis abs_ge_self order_less_imp_le zero_less_abs_iff)
hence nonempty_φ: "{0..} ∩ {n. ¦z¦ ≤ g n} ≠ {}" for z by blast
have bdd_below_φ: "bdd_below ({0..} ∩ {n. g n ≥ ¦z¦})" for z by simp
have φ_bound: "g n ≥ z ⟹ ?φ g z ≤ n" if "z ≥ 0" "n ≥ 0" for n z unfolding eudoxus_pos_inverse_def using cInf_lower[OF _ bdd_below_φ, of n z] that abs_of_nonneg zsgn_def by simp
hence φ_bound': "?φ g z > n ⟹ g n < z" if "z ≥ 0" "n ≥ 0" for z n using that linorder_not_less by blast
have φ_mem: "z > 0 ⟹ ?φ g z ∈ {0..} ∩ {n. g n ≥ ¦z¦}" for z unfolding eudoxus_pos_inverse_def using int_Inf_mem[OF nonempty_φ bdd_below_φ, of z] by simp
obtain L where "¦g (1 + (z - 1)) - (g 1 + g (z - 1))¦ ≤ L" for z using slope_g by fast
hence *: "¦g z - (g 1 + g (z - 1))¦ ≤ L" for z by simp
hence L: "g z ≤ g (z - 1) + (L + g 1)" for z using abs_le_D1 *[of z] by linarith
let ?γ = "λm n. (g (m + (- n)) - (g m + g (- n))) - (g (n + (- n)) - (g n + g (- n))) + g 0"
obtain c where c: "¦g (m + (- n)) - (g m + g (- n))¦ ≤ c" for m n using slope_g by fast
obtain c' where c': "¦g (n + (- n)) - (g n + g (- n))¦ ≤ c'" for n using slope_g by fast
have "¦?γ m n¦ ≤ ¦g (m + (- n)) - (g m + g (- n))¦ + ¦g (n + (- n)) - (g n + g (- n))¦ + ¦g 0¦" for m n by linarith
hence *: "¦?γ m n¦ ≤ c + c' + ¦g 0¦" for m n using c[of m n] c'[of n] by linarith
define C where "C = 2 * (c + c' + ¦g 0¦)"
have "g (m - (n + p)) - (g m - (g n + g p)) = ?γ (m - n) p + ?γ m n" for m n p by (simp add: algebra_simps)
hence "¦g (m - (n + p)) - (g m - (g n + g p))¦ ≤ (c + c' + ¦g 0¦) + (c + c' + ¦g 0¦)" for m n p using *[of "m - n" p] *[of m n] by simp
hence *: "¦g (m - (n + p)) - (g m - (g n + g p))¦ ≤ C" for m n p unfolding C_def by (metis mult_2)
have C: "g (m - (n + p)) ≤ g m - (g n + g p) + C" "g m - (g n + g p) + (- C) ≤ g (m - (n + p))" for m n p using *[of m n p] abs_le_D1 abs_le_D2 by linarith+
have bounded: "bounded h" if bounded: "bounded (g o h)" for h :: "'a ⇒ int"
proof (rule ccontr)
assume asm: "¬ bounded h"
obtain C where C: "¦g (h z)¦ ≤ C" "C ≥ 0" for z using bounded by fastforce
obtain N where N: "g z ≥ C + 1" if "z ≥ N" for z using C pos_g unfolding pos_def by fastforce
obtain N' where N': "g z ≤ - (C + 1)" if "z ≤ N'" for z using C pos_g unfolding pos_dual_def[OF slope_g] by (meson add_increasing2 linordered_nonzero_semiring_class.zero_le_one)
obtain z where "¦h z¦ > max ¦N¦ ¦N'¦" using asm unfolding bounded_alt_def by (meson leI)
hence "h z ∈ {..N'} ∪ {N..}" by fastforce
hence "g (h z) ∈ {..- (C + 1)} ∪ {C + 1..}" using N N' by blast
hence "¦g (h z)¦ ≥ C + 1" by fastforce
thus False using C(1)[of z] by simp
qed
define D where "D = max ¦- (C + (L + g 1) + (L + g 1))¦ ¦C + L + g 1¦"
{
fix m n :: int
assume asm: "m > 0" "n > 0"
have "g (?φ g m) ≥ m" using φ_mem asm by simp
moreover have "?φ g m > 1" using calculation g asm by simp
moreover have "m > g (?φ g m - 1)" using asm calculation by (intro φ_bound') auto
ultimately have m: "m ∈ {g (?φ g m - 1)<..g (?φ g m)}" by simp
have "g (?φ g n) ≥ n" using φ_mem asm by simp
moreover have "?φ g n > 1" using calculation g asm by simp
moreover have "n > g (?φ g n - 1)" using asm calculation by (intro φ_bound') auto
ultimately have n: "n ∈ {g (?φ g n - 1)<..g (?φ g n)}" by simp
have "g (?φ g (m + n)) ≥ m + n" using φ_mem asm by simp
moreover have "?φ g (m + n) > 1" using calculation g asm by simp
moreover have "(m + n) > g (?φ g (m + n) - 1)" using asm calculation by (intro φ_bound') auto
ultimately have m_n: "m + n ∈ {g (?φ g (m + n) - 1)<..g (?φ g (m + n))}" by simp
have *: "g (?φ g (m + n)) - (g (?φ g m - 1) + g (?φ g n - 1)) > 0" "g (?φ g (m + n) - 1) - (g (?φ g m) + g (?φ g n)) < 0" using m_n m n by simp+
have "g (?φ g (m + n) - (?φ g m + ?φ g n)) ≤ g (?φ g (m + n)) - (g (?φ g m) + g (?φ g n)) + C" using C by blast
also have "... ≤ g (?φ g (m + n) - 1) - g (?φ g m) - g (?φ g n) + (C + L + g 1)" using L by fastforce
finally have upper: "g (?φ g (m + n) - (?φ g m + ?φ g n)) ≤ C + L + g 1" using * by fastforce
have "- (C + (L + g 1) + (L + g 1)) ≤ g (?φ g (m + n)) - g (?φ g m - 1) - g (?φ g n - 1) - (C + (L + g 1) + (L + g 1))" using * by linarith
also have "... ≤ g (?φ g (m + n)) - (g (?φ g m) + g (?φ g n)) + (- C)" using L[THEN le_imp_neg_le, of "?φ g m"] L[THEN le_imp_neg_le, of "?φ g n"] by linarith
also have "... ≤ g (?φ g (m + n) - (?φ g m + ?φ g n))" using C by blast
finally have lower: "- (C + (L + g 1) + (L + g 1)) ≤ g (?φ g (m + n) - (?φ g m + ?φ g n))" .
have "¦g (?φ g (m + n) - (?φ g m + ?φ g n))¦ ≤ D" using upper lower unfolding D_def by simp
}
hence "bounded (g o (λ(m, n). ?φ g (m + n) - (?φ g m + ?φ g n)) o (λ(m, n). (max 1 m, max 1 n)))" by (intro boundedI[of _ D]) auto
hence "bounded ((λ(m, n). ?φ g (m + n) - (?φ g m + ?φ g n)) o (λ(m, n). (max 1 m, max 1 n)))" by (metis (mono_tags, lifting) bounded comp_assoc)
then obtain C where "¦((λ(m, n). ?φ g (m + n) - (?φ g m + ?φ g n)) o (λ(m, n). (max 1 m, max 1 n))) (m, n)¦ ≤ C" for m n by blast
hence "¦?φ g (m + n) - (?φ g m + ?φ g n)¦ ≤ C" if "m ≥ 1" "n ≥ 1" for m n using that[THEN max_absorb2] by (metis (no_types, lifting) comp_apply prod.case)
hence slope: "slope (?φ g)" by (intro slope_odd[of _ C]) (auto simp add: eudoxus_pos_inverse_def)
moreover
{
obtain C where C: "¦g ((?φ g n - 1) + 1) - (g (?φ g n - 1) + g 1)¦ ≤ C" for n using slope_g by fast
have C_bound: "g (?φ g n - 1) ≥ g (?φ g n) - (¦g 1¦ + C)" for n using C[of n] by fastforce
{
fix n :: int
assume asm: "n > 0"
have upper: "g (?φ g n) ≥ n" using φ_mem asm by simp
moreover have "?φ g n > 1" using calculation g asm by simp
moreover have "n > g (?φ g n - 1)" using calculation asm by (intro φ_bound') auto
moreover have "n ≥ g (?φ g n) - (¦g 1¦ + C)" using calculation C_bound[of n] by force
ultimately have "¦g (?φ g n) - n¦ ≤ ¦g 1¦ + C" by simp
}
hence id: "g *⇩e ?φ g ∼⇩e id" using slope_g slope by (intro eudoxus_relI[of _ _ 1 "¦g 1¦ + C"]) (auto simp add: eudoxus_times_def)
}
ultimately show ?thesis using g that eudoxus_rel_trans eudoxus_times_cong slope_reflI eudoxus_times_commute[OF slope slope_g] by metis
qed
definition eudoxus_inverse :: "(int ⇒ int) ⇒ (int ⇒ int)" where
"eudoxus_inverse f = (if ¬ bounded f then SOME g. slope g ∧ (g *⇩e f) ∼⇩e id else (λ_. 0))"
lemma
assumes "slope f"
shows slope_eudoxus_inverse: "slope (eudoxus_inverse f)" (is "?slope") and
eudoxus_inverse_id: "¬ bounded f ⟹ eudoxus_inverse f *⇩e f ∼⇩e id" (is "¬ bounded f ⟹ ?id")
proof -
have *: "⟦slope g; (g *⇩e f) ∼⇩e id⟧ ⟹ ?slope" "⟦slope g; (g *⇩e f) ∼⇩e id; ¬ bounded f⟧ ⟹ ?id" for g
unfolding eudoxus_inverse_def using someI[where ?P="λg. slope g ∧ (g *⇩e f) ∼⇩e id"] by auto
{
assume pos: "pos f"
then obtain g where "slope (eudoxus_pos_inverse g)" "eudoxus_pos_inverse g *⇩e f ∼⇩e id" using eudoxus_pos_inverse[OF assms] by blast
hence ?slope "¬ bounded f ⟹ ?id" using pos pos_iff_nonneg_nonzero[OF assms] * by blast+
}
moreover
{
assume nonpos: "¬ pos f"
{
assume nonzero: "¬ bounded f"
hence uminus_f: "slope (-⇩e f)" "pos (-⇩e f)" using neg_iff_pos_uminus neg_iff_nonpos_nonzero assms slope_refl nonpos by auto
then obtain g where g: "slope (eudoxus_pos_inverse g)" "eudoxus_pos_inverse g *⇩e (-⇩e f) ∼⇩e id" using eudoxus_pos_inverse by metis
hence "-⇩e (eudoxus_pos_inverse g) *⇩e f ∼⇩e id" by (metis (full_types) uminus_f(1) abs_real_eq_iff abs_real_times abs_real_uminus assms(1) eudoxus_times_commute minus_mult_commute rel_funE uminus_real.rsp)
moreover have "slope (-⇩e (eudoxus_pos_inverse g))" using uminus_f eudoxus_uminus_cong slope_refl g by presburger
ultimately have ?slope ?id using * nonzero by blast+
}
moreover have "bounded f ⟹ ?slope" unfolding eudoxus_inverse_def by simp
ultimately have ?slope "¬ bounded f ⟹ ?id" by blast+
}
ultimately show ?slope "¬ bounded f ⟹ ?id" by blast+
qed
quotient_definition
"(inverse :: real ⇒ real)" is eudoxus_inverse
proof -
fix x x' assume asm: "x ∼⇩e x'"
hence slopes: "slope x" "slope x'" unfolding eudoxus_rel_def by blast+
show "eudoxus_inverse x ∼⇩e eudoxus_inverse x'"
proof (cases "bounded x")
case True
hence "bounded x'" by (meson asm eudoxus_rel_sym eudoxus_rel_trans zero_iff_bounded)
then show ?thesis unfolding eudoxus_inverse_def using True slope_zero slope_refl by auto
next
case False
hence "¬ bounded x'" by (meson asm eudoxus_rel_sym eudoxus_rel_trans zero_iff_bounded)
hence inverses: "eudoxus_inverse x *⇩e x ∼⇩e id" "eudoxus_inverse x' *⇩e x' ∼⇩e id" using slopes eudoxus_inverse_id False by blast+
have alt_inverse: "eudoxus_inverse x *⇩e x' ∼⇩e id"
using inverses eudoxus_times_cong[OF slope_reflI, OF slope_eudoxus_inverse asm, OF slopes(1)]
eudoxus_rel_sym eudoxus_rel_trans by blast
have "eudoxus_inverse x ∼⇩e eudoxus_inverse x *⇩e (eudoxus_inverse x' *⇩e x')"
using eudoxus_times_cong[OF slope_reflI, OF slope_eudoxus_inverse inverses(2)[THEN eudoxus_rel_sym], OF slopes(1)]
by (simp add: eudoxus_times_def)
also have "... ∼⇩e eudoxus_inverse x' *⇩e (eudoxus_inverse x *⇩e x')"
using eudoxus_times_commute[OF slope_eudoxus_inverse(1,1), OF slopes, THEN eudoxus_times_cong, OF slope_reflI, OF slopes(2)]
by (simp add: eudoxus_times_def comp_assoc)
also have "... ∼⇩e eudoxus_inverse x' *⇩e id" using alt_inverse eudoxus_times_cong[OF slope_reflI] slope_eudoxus_inverse slopes by blast
also have "... = eudoxus_inverse x'" unfolding eudoxus_times_def by simp
finally show ?thesis .
qed
qed
definition
"x div (y::real) = inverse y * x"
instance ..
end
lemmas eudoxus_inverse_cong = apply_rsp'[OF inverse_real.rsp, intro]
lemma eudoxus_inverse_abs[simp]:
assumes "slope f" "¬ bounded f"
shows "inverse (abs_real f) * abs_real f = 1"
unfolding inverse_real_def using eudoxus_inverse_id[OF assms]
by (metis abs_real_eqI abs_real_times assms(1) eudoxus_inverse_cong map_fun_apply one_def rep_real_abs_real_refl slope_refl)
text ‹The Eudoxus reals are a field, with inverses defined as above.›
instance real :: field
proof
fix x y :: real
show "x ≠ 0 ⟹ inverse x * x = 1" using eudoxus_sgn_iff(1) sgn_abs_real_zero_iff by (induct x rule: slope_induct) force
show "x / y = x * inverse y" unfolding divide_real_def by simp
show "inverse (0 :: real) = 0" unfolding inverse_real_def eudoxus_inverse_def using zero_def zero_iff_bounded' by auto
qed
instantiation real :: distrib_lattice
begin
definition
"(inf :: real ⇒ real ⇒ real) = min"
definition
"(sup :: real ⇒ real ⇒ real) = max"
instance by standard (auto simp: inf_real_def sup_real_def max_min_distrib2)
end
text ‹The ordering on the Eudoxus reals is linear.›
instance real :: linordered_field
proof
fix x y z :: real
show "z + x ≤ z + y" if "x ≤ y"
proof (cases "x = y")
case False
hence "x < y" using that by simp
thus ?thesis
proof (induct x rule: slope_induct, induct y rule: slope_induct, induct z rule: slope_induct)
case (slope h g f)
hence "pos (g +⇩e (-⇩e f))" unfolding less_real_def using sgn_abs_real_one_iff by (force simp add: eudoxus_plus_def eudoxus_uminus_def)
thus ?case by (metis slope(4) less_real_def add_diff_cancel_left nless_le)
qed
qed (force)
show "¦x¦ = (if x < 0 then -x else x)" by (metis abs_real less_eq_real_def not_less_iff_gr_or_eq)
show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)" using sgn_range sgn_zero_iff by (auto simp: less_real_def)
show "⟦x < y; 0 < z⟧ ⟹ z * x < z * y" by (metis (no_types, lifting) diff_zero less_real_def mult.right_neutral right_diff_distrib' sgn_times)
qed
text ‹The Eudoxus reals fulfill the Archimedean property.›
instance real :: archimedean_field
proof
fix x :: real
show "∃z. x ≤ of_int z"
proof (induct x rule: slope_induct)
case (slope y)
then obtain A B where linear_bound: "¦y z¦ ≤ A * ¦z¦ + B" "0 ≤ A" "0 ≤ B" for z using slope_linear_bound by blast
{
fix C assume C_nonneg: "0 ≤ (C :: int)"
{
fix z assume asm: "z ≥ B + C"
have "y z + C ≤ A * ¦z¦ + B + C" using abs_le_D1 linear_bound by auto
also have "... ≤ (A + 1) * ¦z¦" using C_nonneg linear_bound(2,3) asm by (auto simp: distrib_right)
finally have "y z + C ≤ (A + 1) * z" using add_nonneg_nonneg[OF C_nonneg linear_bound(3)] abs_of_nonneg[of z] asm by linarith
}
hence "∃N. ∀x ≥ N. (((*) (A + 1)) +⇩e -⇩e y) x ≥ C" unfolding eudoxus_plus_def eudoxus_uminus_def by fastforce
}
hence "pos (((*) (A + 1)) +⇩e -⇩e y)" unfolding pos_def by blast
hence "pos (rep_real (of_int (A + 1) - abs_real y))" unfolding real_of_int using slope by (simp, subst pos_cong[OF rep_real_abs_real_refl]) (auto simp add: eudoxus_plus_def eudoxus_uminus_def)
hence "abs_real y < of_int (A + 1)" unfolding less_real_def by (metis sgn_pos rep_real_abs_real_refl rep_real_iff slope_rep_real)
thus ?case unfolding less_eq_real_def by blast
qed
qed
subsection ‹Completeness›
text ‹To show that the Eudoxus reals are complete, we first introduce the floor function.›
instantiation real :: floor_ceiling
begin
definition
"(floor :: (real ⇒ int)) = (λx. (SOME z. of_int z ≤ x ∧ x < of_int z + 1))"
instance
proof
fix x :: real
show "of_int ⌊x⌋ ≤ x ∧ x < of_int (⌊x⌋ + 1)" using someI[of "λz. of_int z ≤ x ∧ x < of_int z + 1"] floor_exists by (fastforce simp add: floor_real_def)
qed
end
lemma eudoxus_dense_rational:
fixes x y :: real
assumes "x < y"
obtains m n where "x < (of_int m / of_int n)" "(of_int m / of_int n) < y" "n > 0"
proof -
obtain n :: int where n: "inverse (y - x) < of_int n" "n > 0" by (metis ex_less_of_int antisym_conv3 dual_order.strict_trans of_int_less_iff)
hence *: "inverse (of_int n) < y - x" by (metis assms diff_gt_0_iff_gt inverse_inverse_eq inverse_less_iff_less inverse_positive_iff_positive of_int_0_less_iff)
define m where "m = floor (x * of_int n) + 1"
{
assume "y ≤ of_int m / of_int n"
hence "inverse (of_int n) < of_int m / of_int n - x" using * by linarith
hence "x < (of_int m - 1) / of_int n" by (simp add: diff_divide_distrib inverse_eq_divide)
hence False unfolding m_def using n(2) divide_le_eq linorder_not_less by fastforce
}
moreover have "x < of_int m / of_int n" unfolding m_def by (meson n(2) floor_correct mult_imp_less_div_pos of_int_pos)
ultimately show ?thesis using that n by fastforce
qed
text ‹The Eudoxus reals are a complete field.›
lemma eudoxus_complete:
assumes "S ≠ {}" "bdd_above S"
obtains u :: real where "⋀s. s ∈ S ⟹ s ≤ u" "⋀y. (⋀s. s ∈ S ⟹ s ≤ y) ⟹ u ≤ y"
proof (cases "∃u ∈ S. ∀s ∈ S. s ≤ u")
case False
hence no_greatest_element: "∃y ∈ S. x < y" if "x ∈ S" for x using that by force
define u :: "int ⇒ int" where "u = (λz. sgn z * Sup ((λx. ⌊of_int ¦z¦ * x⌋) ` S))"
have bdd_above_u: "bdd_above ((λx. ⌊of_int ¦z¦ * x⌋) ` S)" for z by (intro bdd_above_image_mono[OF _ assms(2)] monoI) (simp add: floor_mono mult.commute mult_right_mono)
have u_Sup_nonneg: "z ≥ 0 ⟹ ⌊of_int z * s⌋ ≤ u z" and
u_Sup_nonpos: "z ≤ 0 ⟹ - ⌊of_int (- z) * s⌋ ≥ u z" if "s ∈ S" for s z
unfolding u_def using cSup_upper[OF _ bdd_above_u, of "⌊of_int ¦z¦ * s⌋" z] that abs_of_nonpos zsgn_def by force+
have u_mem: "u z ∈ (λx. sgn z * ⌊of_int ¦z¦ * x⌋) ` S" for z unfolding u_def using int_Sup_mem[OF _ bdd_above_u, of z] assms by auto
have slope: "slope u"
proof -
{
fix m n :: int assume asm: "m > 0" "n > 0"
obtain x_m where x_m: "x_m ∈ S" "u m = ⌊of_int m * x_m⌋" using u_mem[of m] asm zsgn_def by auto
obtain x_n where x_n: "x_n ∈ S" "u n = ⌊of_int n * x_n⌋" using u_mem[of n] asm zsgn_def by auto
obtain x_m_n where x_m_n: "x_m_n ∈ S" "u (m + n) = ⌊of_int (m + n) * x_m_n⌋" using u_mem[of "m + n"] asm zsgn_def by auto
define x where "x = max (max x_m x_n) x_m_n"
have x: "x ∈ S" unfolding x_def using x_m x_n x_m_n by linarith
have "x ≥ x_m" "x ≥ x_n" "x ≥ x_m_n" unfolding x_def by linarith+
hence "u m ≤ ⌊of_int m * x⌋" "u n ≤ ⌊of_int n * x⌋" "u (m + n) ≤ ⌊of_int (m + n) * x⌋"
unfolding x_m x_n x_m_n by (meson asm floor_less_cancel linorder_not_less mult_le_cancel_left_pos of_int_0_less_iff add_pos_pos)+
hence "u m = ⌊of_int m * x⌋" "u n = ⌊of_int n * x⌋" "u (m + n) = ⌊of_int m * x + of_int n * x⌋"
using u_Sup_nonneg[OF x(1), of m] u_Sup_nonneg[OF x(1), of n] u_Sup_nonneg[OF x(1), of "m + n"] asm add_pos_pos[OF asm] by (force simp add: distrib_right)+
moreover
{
fix a b :: real
have "a - of_int ⌊a⌋ ∈ {0..<1}" using floor_less_one by fastforce
moreover have "b - of_int ⌊b⌋ ∈ {0..<1}" using floor_less_one by fastforce
ultimately have "(a - of_int ⌊a⌋) + (b - of_int ⌊b⌋) ∈ {0..<2}" unfolding atLeastLessThan_def by simp
hence "(a + b) - (of_int ⌊a⌋ + of_int ⌊b⌋) ∈ {0..<2}" by (simp add: diff_add_eq)
hence "⌊a + b - (of_int ⌊a⌋ + of_int ⌊b⌋)⌋ ∈ {0..<2}" by simp
hence "⌊a + b⌋ - (⌊a⌋ + ⌊b⌋) ∈ {0..<2}" by (metis floor_diff_of_int of_int_add)
}
ultimately have "¦u (m + n) - (u m + u n)¦ ≤ 2" by (metis abs_of_nonneg atLeastLessThan_iff nless_le)
}
moreover have "u z = - u (- z)" for z unfolding u_def by simp
ultimately show ?thesis using slope_odd by blast
qed
{
fix s assume "s ∈ S"
then obtain y where y: "s < y" "y ∈ S" using no_greatest_element by blast
then obtain m n :: int where *: "s < (of_int m / of_int n)" "(of_int m / of_int n) < y" "n > 0" using eudoxus_dense_rational by blast
hence n_nonneg: "n ≥ 0" by simp
{
fix z :: int assume z_nonneg: "z ≥ 0"
have "z * m = ⌊of_int (z * n) * (of_int m / of_int n) :: real⌋" using *(3) by simp (auto simp only: of_int_mult[symmetric] floor_of_int)
also have "... ≤ ⌊of_int (z * n) * y⌋" using *(2) by (meson floor_mono mult_left_mono n_nonneg nless_le of_int_nonneg z_nonneg zero_le_mult_iff)
also have "... ≤ u (z * n)" using u_Sup_nonneg[OF y(2)] mult_nonneg_nonneg[OF z_nonneg n_nonneg] by blast
finally have "u (z * n) ≥ z * m" .
}
hence "abs_real (u *⇩e (*) n) ≥ of_int m" using slope unfolding real_of_int eudoxus_times_def by (intro abs_real_leI[where ?N=0]) (auto simp add: mult.commute)
moreover have "abs_real u * of_int n = abs_real (u *⇩e (*) n)" unfolding real_of_int using slope by (simp add: eudoxus_times_def comp_def)
ultimately have "s ≤ abs_real u" using * by (metis leI mult_imp_div_pos_le of_int_0_less_iff order_le_less_trans order_less_asym)
}
moreover
{
fix y assume asm: "s ≤ y" if "s ∈ S" for s
assume "abs_real u > y"
then obtain m n :: int where *: "y < (of_int m / of_int n)" "(of_int m / of_int n) < abs_real u" "n > 0" using eudoxus_dense_rational by blast
hence "of_int m < abs_real u * of_int n" by (simp add: pos_divide_less_eq)
hence "of_int m < abs_real (u *⇩e (*) n)" unfolding real_of_int using slope by (simp add: eudoxus_times_def comp_def)
moreover have "slope (u *⇩e (*) n)" using slope by (simp add: eudoxus_times_def)
ultimately obtain z where z: "(u *⇩e (*) n) z > m * z" "z ≥ 1" unfolding real_of_int using abs_real_lessD by blast
hence **: "u (n * z) > m * z" by (simp add: eudoxus_times_def comp_def)
obtain x where x: "x ∈ S" "u (n * z) = ⌊of_int (n * z) * x⌋" using u_mem[of "n * z"] zsgn_def[of "n * z"] mult_pos_pos[OF *(3), of z] z(2) by fastforce
have "of_int (n * z) * x ≤ of_int z * of_int n * y" using asm[OF x(1)] using * z by auto
also have "... < of_int z * of_int m" using * z by (simp add: mult.commute pos_less_divide_eq)
finally have "of_int (n * z) * x < of_int (m * z)" by (simp add: mult.commute)
hence False using ** by (metis floor_less_iff less_le_not_le x(2))
}
ultimately show ?thesis using that by force
qed blast
end