Theory RealDef

Up to index of Isabelle/HOL

theory RealDef
imports Rat
`(*  Title       : HOL/RealDef.thy    Author      : Jacques D. Fleuriot, 1998    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4    Additional contributions by Jeremy Avigad    Construction of Cauchy Reals by Brian Huffman, 2010*)header {* Development of the Reals using Cauchy Sequences *}theory RealDefimports Ratbegintext {*  This theory contains a formalization of the real numbers as  equivalence classes of Cauchy sequences of rationals.  See  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative  construction using Dedekind cuts.*}subsection {* Preliminary lemmas *}lemma add_diff_add:  fixes a b c d :: "'a::ab_group_add"  shows "(a + c) - (b + d) = (a - b) + (c - d)"  by simplemma minus_diff_minus:  fixes a b :: "'a::ab_group_add"  shows "- a - - b = - (a - b)"  by simplemma mult_diff_mult:  fixes x y a b :: "'a::ring"  shows "(x * y - a * b) = x * (y - b) + (x - a) * b"  by (simp add: algebra_simps)lemma inverse_diff_inverse:  fixes a b :: "'a::division_ring"  assumes "a ≠ 0" and "b ≠ 0"  shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)"  using assms by (simp add: algebra_simps)lemma obtain_pos_sum:  fixes r :: rat assumes r: "0 < r"  obtains s t where "0 < s" and "0 < t" and "r = s + t"proof    from r show "0 < r/2" by simp    from r show "0 < r/2" by simp    show "r = r/2 + r/2" by simpqedsubsection {* Sequences that converge to zero *}definition  vanishes :: "(nat => rat) => bool"where  "vanishes X = (∀r>0. ∃k. ∀n≥k. ¦X n¦ < r)"lemma vanishesI: "(!!r. 0 < r ==> ∃k. ∀n≥k. ¦X n¦ < r) ==> vanishes X"  unfolding vanishes_def by simplemma vanishesD: "[|vanishes X; 0 < r|] ==> ∃k. ∀n≥k. ¦X n¦ < r"  unfolding vanishes_def by simplemma vanishes_const [simp]: "vanishes (λn. c) <-> c = 0"  unfolding vanishes_def  apply (cases "c = 0", auto)  apply (rule exI [where x="¦c¦"], auto)  donelemma vanishes_minus: "vanishes X ==> vanishes (λn. - X n)"  unfolding vanishes_def by simplemma vanishes_add:  assumes X: "vanishes X" and Y: "vanishes Y"  shows "vanishes (λn. X n + Y n)"proof (rule vanishesI)  fix r :: rat assume "0 < r"  then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"    by (rule obtain_pos_sum)  obtain i where i: "∀n≥i. ¦X n¦ < s"    using vanishesD [OF X s] ..  obtain j where j: "∀n≥j. ¦Y n¦ < t"    using vanishesD [OF Y t] ..  have "∀n≥max i j. ¦X n + Y n¦ < r"  proof (clarsimp)    fix n assume n: "i ≤ n" "j ≤ n"    have "¦X n + Y n¦ ≤ ¦X n¦ + ¦Y n¦" by (rule abs_triangle_ineq)    also have "… < s + t" by (simp add: add_strict_mono i j n)    finally show "¦X n + Y n¦ < r" unfolding r .  qed  thus "∃k. ∀n≥k. ¦X n + Y n¦ < r" ..qedlemma vanishes_diff:  assumes X: "vanishes X" and Y: "vanishes Y"  shows "vanishes (λn. X n - Y n)"unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)lemma vanishes_mult_bounded:  assumes X: "∃a>0. ∀n. ¦X n¦ < a"  assumes Y: "vanishes (λn. Y n)"  shows "vanishes (λn. X n * Y n)"proof (rule vanishesI)  fix r :: rat assume r: "0 < r"  obtain a where a: "0 < a" "∀n. ¦X n¦ < a"    using X by fast  obtain b where b: "0 < b" "r = a * b"  proof    show "0 < r / a" using r a by (simp add: divide_pos_pos)    show "r = a * (r / a)" using a by simp  qed  obtain k where k: "∀n≥k. ¦Y n¦ < b"    using vanishesD [OF Y b(1)] ..  have "∀n≥k. ¦X n * Y n¦ < r"    by (simp add: b(2) abs_mult mult_strict_mono' a k)  thus "∃k. ∀n≥k. ¦X n * Y n¦ < r" ..qedsubsection {* Cauchy sequences *}definition  cauchy :: "(nat => rat) => bool"where  "cauchy X <-> (∀r>0. ∃k. ∀m≥k. ∀n≥k. ¦X m - X n¦ < r)"lemma cauchyI:  "(!!r. 0 < r ==> ∃k. ∀m≥k. ∀n≥k. ¦X m - X n¦ < r) ==> cauchy X"  unfolding cauchy_def by simplemma cauchyD:  "[|cauchy X; 0 < r|] ==> ∃k. ∀m≥k. ∀n≥k. ¦X m - X n¦ < r"  unfolding cauchy_def by simplemma cauchy_const [simp]: "cauchy (λn. x)"  unfolding cauchy_def by simplemma cauchy_add [simp]:  assumes X: "cauchy X" and Y: "cauchy Y"  shows "cauchy (λn. X n + Y n)"proof (rule cauchyI)  fix r :: rat assume "0 < r"  then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"    by (rule obtain_pos_sum)  obtain i where i: "∀m≥i. ∀n≥i. ¦X m - X n¦ < s"    using cauchyD [OF X s] ..  obtain j where j: "∀m≥j. ∀n≥j. ¦Y m - Y n¦ < t"    using cauchyD [OF Y t] ..  have "∀m≥max i j. ∀n≥max i j. ¦(X m + Y m) - (X n + Y n)¦ < r"  proof (clarsimp)    fix m n assume *: "i ≤ m" "j ≤ m" "i ≤ n" "j ≤ n"    have "¦(X m + Y m) - (X n + Y n)¦ ≤ ¦X m - X n¦ + ¦Y m - Y n¦"      unfolding add_diff_add by (rule abs_triangle_ineq)    also have "… < s + t"      by (rule add_strict_mono, simp_all add: i j *)    finally show "¦(X m + Y m) - (X n + Y n)¦ < r" unfolding r .  qed  thus "∃k. ∀m≥k. ∀n≥k. ¦(X m + Y m) - (X n + Y n)¦ < r" ..qedlemma cauchy_minus [simp]:  assumes X: "cauchy X"  shows "cauchy (λn. - X n)"using assms unfolding cauchy_defunfolding minus_diff_minus abs_minus_cancel .lemma cauchy_diff [simp]:  assumes X: "cauchy X" and Y: "cauchy Y"  shows "cauchy (λn. X n - Y n)"using assms unfolding diff_minus by simplemma cauchy_imp_bounded:  assumes "cauchy X" shows "∃b>0. ∀n. ¦X n¦ < b"proof -  obtain k where k: "∀m≥k. ∀n≥k. ¦X m - X n¦ < 1"    using cauchyD [OF assms zero_less_one] ..  show "∃b>0. ∀n. ¦X n¦ < b"  proof (intro exI conjI allI)    have "0 ≤ ¦X 0¦" by simp    also have "¦X 0¦ ≤ Max (abs ` X ` {..k})" by simp    finally have "0 ≤ Max (abs ` X ` {..k})" .    thus "0 < Max (abs ` X ` {..k}) + 1" by simp  next    fix n :: nat    show "¦X n¦ < Max (abs ` X ` {..k}) + 1"    proof (rule linorder_le_cases)      assume "n ≤ k"      hence "¦X n¦ ≤ Max (abs ` X ` {..k})" by simp      thus "¦X n¦ < Max (abs ` X ` {..k}) + 1" by simp    next      assume "k ≤ n"      have "¦X n¦ = ¦X k + (X n - X k)¦" by simp      also have "¦X k + (X n - X k)¦ ≤ ¦X k¦ + ¦X n - X k¦"        by (rule abs_triangle_ineq)      also have "… < Max (abs ` X ` {..k}) + 1"        by (rule add_le_less_mono, simp, simp add: k `k ≤ n`)      finally show "¦X n¦ < Max (abs ` X ` {..k}) + 1" .    qed  qedqedlemma cauchy_mult [simp]:  assumes X: "cauchy X" and Y: "cauchy Y"  shows "cauchy (λn. X n * Y n)"proof (rule cauchyI)  fix r :: rat assume "0 < r"  then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"    by (rule obtain_pos_sum)  obtain a where a: "0 < a" "∀n. ¦X n¦ < a"    using cauchy_imp_bounded [OF X] by fast  obtain b where b: "0 < b" "∀n. ¦Y n¦ < b"    using cauchy_imp_bounded [OF Y] by fast  obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"  proof    show "0 < v/b" using v b(1) by (rule divide_pos_pos)    show "0 < u/a" using u a(1) by (rule divide_pos_pos)    show "r = a * (u/a) + (v/b) * b"      using a(1) b(1) `r = u + v` by simp  qed  obtain i where i: "∀m≥i. ∀n≥i. ¦X m - X n¦ < s"    using cauchyD [OF X s] ..  obtain j where j: "∀m≥j. ∀n≥j. ¦Y m - Y n¦ < t"    using cauchyD [OF Y t] ..  have "∀m≥max i j. ∀n≥max i j. ¦X m * Y m - X n * Y n¦ < r"  proof (clarsimp)    fix m n assume *: "i ≤ m" "j ≤ m" "i ≤ n" "j ≤ n"    have "¦X m * Y m - X n * Y n¦ = ¦X m * (Y m - Y n) + (X m - X n) * Y n¦"      unfolding mult_diff_mult ..    also have "… ≤ ¦X m * (Y m - Y n)¦ + ¦(X m - X n) * Y n¦"      by (rule abs_triangle_ineq)    also have "… = ¦X m¦ * ¦Y m - Y n¦ + ¦X m - X n¦ * ¦Y n¦"      unfolding abs_mult ..    also have "… < a * t + s * b"      by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)    finally show "¦X m * Y m - X n * Y n¦ < r" unfolding r .  qed  thus "∃k. ∀m≥k. ∀n≥k. ¦X m * Y m - X n * Y n¦ < r" ..qedlemma cauchy_not_vanishes_cases:  assumes X: "cauchy X"  assumes nz: "¬ vanishes X"  shows "∃b>0. ∃k. (∀n≥k. b < - X n) ∨ (∀n≥k. b < X n)"proof -  obtain r where "0 < r" and r: "∀k. ∃n≥k. r ≤ ¦X n¦"    using nz unfolding vanishes_def by (auto simp add: not_less)  obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t"    using `0 < r` by (rule obtain_pos_sum)  obtain i where i: "∀m≥i. ∀n≥i. ¦X m - X n¦ < s"    using cauchyD [OF X s] ..  obtain k where "i ≤ k" and "r ≤ ¦X k¦"    using r by fast  have k: "∀n≥k. ¦X n - X k¦ < s"    using i `i ≤ k` by auto  have "X k ≤ - r ∨ r ≤ X k"    using `r ≤ ¦X k¦` by auto  hence "(∀n≥k. t < - X n) ∨ (∀n≥k. t < X n)"    unfolding `r = s + t` using k by auto  hence "∃k. (∀n≥k. t < - X n) ∨ (∀n≥k. t < X n)" ..  thus "∃t>0. ∃k. (∀n≥k. t < - X n) ∨ (∀n≥k. t < X n)"    using t by autoqedlemma cauchy_not_vanishes:  assumes X: "cauchy X"  assumes nz: "¬ vanishes X"  shows "∃b>0. ∃k. ∀n≥k. b < ¦X n¦"using cauchy_not_vanishes_cases [OF assms]by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto)lemma cauchy_inverse [simp]:  assumes X: "cauchy X"  assumes nz: "¬ vanishes X"  shows "cauchy (λn. inverse (X n))"proof (rule cauchyI)  fix r :: rat assume "0 < r"  obtain b i where b: "0 < b" and i: "∀n≥i. b < ¦X n¦"    using cauchy_not_vanishes [OF X nz] by fast  from b i have nz: "∀n≥i. X n ≠ 0" by auto  obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"  proof    show "0 < b * r * b"      by (simp add: `0 < r` b mult_pos_pos)    show "r = inverse b * (b * r * b) * inverse b"      using b by simp  qed  obtain j where j: "∀m≥j. ∀n≥j. ¦X m - X n¦ < s"    using cauchyD [OF X s] ..  have "∀m≥max i j. ∀n≥max i j. ¦inverse (X m) - inverse (X n)¦ < r"  proof (clarsimp)    fix m n assume *: "i ≤ m" "j ≤ m" "i ≤ n" "j ≤ n"    have "¦inverse (X m) - inverse (X n)¦ =          inverse ¦X m¦ * ¦X m - X n¦ * inverse ¦X n¦"      by (simp add: inverse_diff_inverse nz * abs_mult)    also have "… < inverse b * s * inverse b"      by (simp add: mult_strict_mono less_imp_inverse_less                    mult_pos_pos i j b * s)    finally show "¦inverse (X m) - inverse (X n)¦ < r" unfolding r .  qed  thus "∃k. ∀m≥k. ∀n≥k. ¦inverse (X m) - inverse (X n)¦ < r" ..qedlemma vanishes_diff_inverse:  assumes X: "cauchy X" "¬ vanishes X"  assumes Y: "cauchy Y" "¬ vanishes Y"  assumes XY: "vanishes (λn. X n - Y n)"  shows "vanishes (λn. inverse (X n) - inverse (Y n))"proof (rule vanishesI)  fix r :: rat assume r: "0 < r"  obtain a i where a: "0 < a" and i: "∀n≥i. a < ¦X n¦"    using cauchy_not_vanishes [OF X] by fast  obtain b j where b: "0 < b" and j: "∀n≥j. b < ¦Y n¦"    using cauchy_not_vanishes [OF Y] by fast  obtain s where s: "0 < s" and "inverse a * s * inverse b = r"  proof    show "0 < a * r * b"      using a r b by (simp add: mult_pos_pos)    show "inverse a * (a * r * b) * inverse b = r"      using a r b by simp  qed  obtain k where k: "∀n≥k. ¦X n - Y n¦ < s"    using vanishesD [OF XY s] ..  have "∀n≥max (max i j) k. ¦inverse (X n) - inverse (Y n)¦ < r"  proof (clarsimp)    fix n assume n: "i ≤ n" "j ≤ n" "k ≤ n"    have "X n ≠ 0" and "Y n ≠ 0"      using i j a b n by auto    hence "¦inverse (X n) - inverse (Y n)¦ =        inverse ¦X n¦ * ¦X n - Y n¦ * inverse ¦Y n¦"      by (simp add: inverse_diff_inverse abs_mult)    also have "… < inverse a * s * inverse b"      apply (intro mult_strict_mono' less_imp_inverse_less)      apply (simp_all add: a b i j k n mult_nonneg_nonneg)      done    also note `inverse a * s * inverse b = r`    finally show "¦inverse (X n) - inverse (Y n)¦ < r" .  qed  thus "∃k. ∀n≥k. ¦inverse (X n) - inverse (Y n)¦ < r" ..qedsubsection {* Equivalence relation on Cauchy sequences *}definition realrel :: "(nat => rat) => (nat => rat) => bool"  where "realrel = (λX Y. cauchy X ∧ cauchy Y ∧ vanishes (λn. X n - Y n))"lemma realrelI [intro?]:  assumes "cauchy X" and "cauchy Y" and "vanishes (λn. X n - Y n)"  shows "realrel X Y"  using assms unfolding realrel_def by simplemma realrel_refl: "cauchy X ==> realrel X X"  unfolding realrel_def by simplemma symp_realrel: "symp realrel"  unfolding realrel_def  by (rule sympI, clarify, drule vanishes_minus, simp)lemma transp_realrel: "transp realrel"  unfolding realrel_def  apply (rule transpI, clarify)  apply (drule (1) vanishes_add)  apply (simp add: algebra_simps)  donelemma part_equivp_realrel: "part_equivp realrel"  by (fast intro: part_equivpI symp_realrel transp_realrel    realrel_refl cauchy_const)subsection {* The field of real numbers *}quotient_type real = "nat => rat" / partial: realrel  morphisms rep_real Real  by (rule part_equivp_realrel)lemma cr_real_eq: "cr_real = (λx y. cauchy x ∧ Real x = y)"  unfolding cr_real_def realrel_def by simplemma Real_induct [induct type: real]: (* TODO: generate automatically *)  assumes "!!X. cauchy X ==> P (Real X)" shows "P x"proof (induct x)  case (1 X)  hence "cauchy X" by (simp add: realrel_def)  thus "P (Real X)" by (rule assms)qedlemma eq_Real:  "cauchy X ==> cauchy Y ==> Real X = Real Y <-> vanishes (λn. X n - Y n)"  using real.rel_eq_transfer  unfolding cr_real_def fun_rel_def realrel_def by simpdeclare real.forall_transfer [transfer_rule del]lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *)  "(fun_rel (fun_rel cr_real op =) op =)    (transfer_bforall cauchy) transfer_forall"  using Quotient_forall_transfer [OF Quotient_real]  by (simp add: realrel_def)instantiation real :: field_inverse_zerobeginlift_definition zero_real :: "real" is "λn. 0"  by (simp add: realrel_refl)lift_definition one_real :: "real" is "λn. 1"  by (simp add: realrel_refl)lift_definition plus_real :: "real => real => real" is "λX Y n. X n + Y n"  unfolding realrel_def add_diff_add  by (simp only: cauchy_add vanishes_add simp_thms)lift_definition uminus_real :: "real => real" is "λX n. - X n"  unfolding realrel_def minus_diff_minus  by (simp only: cauchy_minus vanishes_minus simp_thms)lift_definition times_real :: "real => real => real" is "λX Y n. X n * Y n"  unfolding realrel_def mult_diff_mult  by (subst (4) mult_commute, simp only: cauchy_mult vanishes_add    vanishes_mult_bounded cauchy_imp_bounded simp_thms)lift_definition inverse_real :: "real => real"  is "λX. if vanishes X then (λn. 0) else (λn. inverse (X n))"proof -  fix X Y assume "realrel X Y"  hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (λn. X n - Y n)"    unfolding realrel_def by simp_all  have "vanishes X <-> vanishes Y"  proof    assume "vanishes X"    from vanishes_diff [OF this XY] show "vanishes Y" by simp  next    assume "vanishes Y"    from vanishes_add [OF this XY] show "vanishes X" by simp  qed  thus "?thesis X Y"    unfolding realrel_def    by (simp add: vanishes_diff_inverse X Y XY)qeddefinition  "x - y = (x::real) + - y"definition  "x / y = (x::real) * inverse y"lemma add_Real:  assumes X: "cauchy X" and Y: "cauchy Y"  shows "Real X + Real Y = Real (λn. X n + Y n)"  using assms plus_real.transfer  unfolding cr_real_eq fun_rel_def by simplemma minus_Real:  assumes X: "cauchy X"  shows "- Real X = Real (λn. - X n)"  using assms uminus_real.transfer  unfolding cr_real_eq fun_rel_def by simplemma diff_Real:  assumes X: "cauchy X" and Y: "cauchy Y"  shows "Real X - Real Y = Real (λn. X n - Y n)"  unfolding minus_real_def diff_minus  by (simp add: minus_Real add_Real X Y)lemma mult_Real:  assumes X: "cauchy X" and Y: "cauchy Y"  shows "Real X * Real Y = Real (λn. X n * Y n)"  using assms times_real.transfer  unfolding cr_real_eq fun_rel_def by simplemma inverse_Real:  assumes X: "cauchy X"  shows "inverse (Real X) =    (if vanishes X then 0 else Real (λn. inverse (X n)))"  using assms inverse_real.transfer zero_real.transfer  unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis)instance proof  fix a b c :: real  show "a + b = b + a"    by transfer (simp add: add_ac realrel_def)  show "(a + b) + c = a + (b + c)"    by transfer (simp add: add_ac realrel_def)  show "0 + a = a"    by transfer (simp add: realrel_def)  show "- a + a = 0"    by transfer (simp add: realrel_def)  show "a - b = a + - b"    by (rule minus_real_def)  show "(a * b) * c = a * (b * c)"    by transfer (simp add: mult_ac realrel_def)  show "a * b = b * a"    by transfer (simp add: mult_ac realrel_def)  show "1 * a = a"    by transfer (simp add: mult_ac realrel_def)  show "(a + b) * c = a * c + b * c"    by transfer (simp add: distrib_right realrel_def)  show "(0::real) ≠ (1::real)"    by transfer (simp add: realrel_def)  show "a ≠ 0 ==> inverse a * a = 1"    apply transfer    apply (simp add: realrel_def)    apply (rule vanishesI)    apply (frule (1) cauchy_not_vanishes, clarify)    apply (rule_tac x=k in exI, clarify)    apply (drule_tac x=n in spec, simp)    done  show "a / b = a * inverse b"    by (rule divide_real_def)  show "inverse (0::real) = 0"    by transfer (simp add: realrel_def)qedendsubsection {* Positive reals *}lift_definition positive :: "real => bool"  is "λX. ∃r>0. ∃k. ∀n≥k. r < X n"proof -  { fix X Y    assume "realrel X Y"    hence XY: "vanishes (λn. X n - Y n)"      unfolding realrel_def by simp_all    assume "∃r>0. ∃k. ∀n≥k. r < X n"    then obtain r i where "0 < r" and i: "∀n≥i. r < X n"      by fast    obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"      using `0 < r` by (rule obtain_pos_sum)    obtain j where j: "∀n≥j. ¦X n - Y n¦ < s"      using vanishesD [OF XY s] ..    have "∀n≥max i j. t < Y n"    proof (clarsimp)      fix n assume n: "i ≤ n" "j ≤ n"      have "¦X n - Y n¦ < s" and "r < X n"        using i j n by simp_all      thus "t < Y n" unfolding r by simp    qed    hence "∃r>0. ∃k. ∀n≥k. r < Y n" using t by fast  } note 1 = this  fix X Y assume "realrel X Y"  hence "realrel X Y" and "realrel Y X"    using symp_realrel unfolding symp_def by auto  thus "?thesis X Y"    by (safe elim!: 1)qedlemma positive_Real:  assumes X: "cauchy X"  shows "positive (Real X) <-> (∃r>0. ∃k. ∀n≥k. r < X n)"  using assms positive.transfer  unfolding cr_real_eq fun_rel_def by simplemma positive_zero: "¬ positive 0"  by transfer autolemma positive_add:  "positive x ==> positive y ==> positive (x + y)"apply transferapply (clarify, rename_tac a b i j)apply (rule_tac x="a + b" in exI, simp)apply (rule_tac x="max i j" in exI, clarsimp)apply (simp add: add_strict_mono)donelemma positive_mult:  "positive x ==> positive y ==> positive (x * y)"apply transferapply (clarify, rename_tac a b i j)apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)apply (rule_tac x="max i j" in exI, clarsimp)apply (rule mult_strict_mono, auto)donelemma positive_minus:  "¬ positive x ==> x ≠ 0 ==> positive (- x)"apply transferapply (simp add: realrel_def)apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)doneinstantiation real :: linordered_field_inverse_zerobegindefinition  "x < y <-> positive (y - x)"definition  "x ≤ (y::real) <-> x < y ∨ x = y"definition  "abs (a::real) = (if a < 0 then - a else a)"definition  "sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"instance proof  fix a b c :: real  show "¦a¦ = (if a < 0 then - a else a)"    by (rule abs_real_def)  show "a < b <-> a ≤ b ∧ ¬ b ≤ a"    unfolding less_eq_real_def less_real_def    by (auto, drule (1) positive_add, simp_all add: positive_zero)  show "a ≤ a"    unfolding less_eq_real_def by simp  show "a ≤ b ==> b ≤ c ==> a ≤ c"    unfolding less_eq_real_def less_real_def    by (auto, drule (1) positive_add, simp add: algebra_simps)  show "a ≤ b ==> b ≤ a ==> a = b"    unfolding less_eq_real_def less_real_def    by (auto, drule (1) positive_add, simp add: positive_zero)  show "a ≤ b ==> c + a ≤ c + b"    unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)    (* FIXME: Procedure int_combine_numerals: c + b - (c + a) ≡ b + - a *)    (* Should produce c + b - (c + a) ≡ b - a *)  show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"    by (rule sgn_real_def)  show "a ≤ b ∨ b ≤ a"    unfolding less_eq_real_def less_real_def    by (auto dest!: positive_minus)  show "a < b ==> 0 < c ==> c * a < c * b"    unfolding less_real_def    by (drule (1) positive_mult, simp add: algebra_simps)qedendinstantiation real :: distrib_latticebegindefinition  "(inf :: real => real => real) = min"definition  "(sup :: real => real => real) = max"instance proofqed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)endlemma of_nat_Real: "of_nat x = Real (λn. of_nat x)"apply (induct x)apply (simp add: zero_real_def)apply (simp add: one_real_def add_Real)donelemma of_int_Real: "of_int x = Real (λn. of_int x)"apply (cases x rule: int_diff_cases)apply (simp add: of_nat_Real diff_Real)donelemma of_rat_Real: "of_rat x = Real (λn. x)"apply (induct x)apply (simp add: Fract_of_int_quotient of_rat_divide)apply (simp add: of_int_Real divide_inverse)apply (simp add: inverse_Real mult_Real)doneinstance real :: archimedean_fieldproof  fix x :: real  show "∃z. x ≤ of_int z"    apply (induct x)    apply (frule cauchy_imp_bounded, clarify)    apply (rule_tac x="ceiling b + 1" in exI)    apply (rule less_imp_le)    apply (simp add: of_int_Real less_real_def diff_Real positive_Real)    apply (rule_tac x=1 in exI, simp add: algebra_simps)    apply (rule_tac x=0 in exI, clarsimp)    apply (rule le_less_trans [OF abs_ge_self])    apply (rule less_le_trans [OF _ le_of_int_ceiling])    apply simp    doneqedinstantiation real :: floor_ceilingbegindefinition [code del]:  "floor (x::real) = (THE z. of_int z ≤ x ∧ x < of_int (z + 1))"instance proof  fix x :: real  show "of_int (floor x) ≤ x ∧ x < of_int (floor x + 1)"    unfolding floor_real_def using floor_exists1 by (rule theI')qedendsubsection {* Completeness *}lemma not_positive_Real:  assumes X: "cauchy X"  shows "¬ positive (Real X) <-> (∀r>0. ∃k. ∀n≥k. X n ≤ r)"unfolding positive_Real [OF X]apply (auto, unfold not_less)apply (erule obtain_pos_sum)apply (drule_tac x=s in spec, simp)apply (drule_tac r=t in cauchyD [OF X], clarify)apply (drule_tac x=k in spec, clarsimp)apply (rule_tac x=n in exI, clarify, rename_tac m)apply (drule_tac x=m in spec, simp)apply (drule_tac x=n in spec, simp)apply (drule spec, drule (1) mp, clarify, rename_tac i)apply (rule_tac x="max i k" in exI, simp)donelemma le_Real:  assumes X: "cauchy X" and Y: "cauchy Y"  shows "Real X ≤ Real Y = (∀r>0. ∃k. ∀n≥k. X n ≤ Y n + r)"unfolding not_less [symmetric, where 'a=real] less_real_defapply (simp add: diff_Real not_positive_Real X Y)apply (simp add: diff_le_eq add_ac)donelemma le_RealI:  assumes Y: "cauchy Y"  shows "∀n. x ≤ of_rat (Y n) ==> x ≤ Real Y"proof (induct x)  fix X assume X: "cauchy X" and "∀n. Real X ≤ of_rat (Y n)"  hence le: "!!m r. 0 < r ==> ∃k. ∀n≥k. X n ≤ Y m + r"    by (simp add: of_rat_Real le_Real)  {    fix r :: rat assume "0 < r"    then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"      by (rule obtain_pos_sum)    obtain i where i: "∀m≥i. ∀n≥i. ¦Y m - Y n¦ < s"      using cauchyD [OF Y s] ..    obtain j where j: "∀n≥j. X n ≤ Y i + t"      using le [OF t] ..    have "∀n≥max i j. X n ≤ Y n + r"    proof (clarsimp)      fix n assume n: "i ≤ n" "j ≤ n"      have "X n ≤ Y i + t" using n j by simp      moreover have "¦Y i - Y n¦ < s" using n i by simp      ultimately show "X n ≤ Y n + r" unfolding r by simp    qed    hence "∃k. ∀n≥k. X n ≤ Y n + r" ..  }  thus "Real X ≤ Real Y"    by (simp add: of_rat_Real le_Real X Y)qedlemma Real_leI:  assumes X: "cauchy X"  assumes le: "∀n. of_rat (X n) ≤ y"  shows "Real X ≤ y"proof -  have "- y ≤ - Real X"    by (simp add: minus_Real X le_RealI of_rat_minus le)  thus ?thesis by simpqedlemma less_RealD:  assumes Y: "cauchy Y"  shows "x < Real Y ==> ∃n. x < of_rat (Y n)"by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y])lemma of_nat_less_two_power:  "of_nat n < (2::'a::linordered_idom) ^ n"apply (induct n)apply simpapply (subgoal_tac "(1::'a) ≤ 2 ^ n")apply (drule (1) add_le_less_mono, simp)apply simpdonelemma complete_real:  fixes S :: "real set"  assumes "∃x. x ∈ S" and "∃z. ∀x∈S. x ≤ z"  shows "∃y. (∀x∈S. x ≤ y) ∧ (∀z. (∀x∈S. x ≤ z) --> y ≤ z)"proof -  obtain x where x: "x ∈ S" using assms(1) ..  obtain z where z: "∀x∈S. x ≤ z" using assms(2) ..  def P ≡ "λx. ∀y∈S. y ≤ of_rat x"  obtain a where a: "¬ P a"  proof    have "of_int (floor (x - 1)) ≤ x - 1" by (rule of_int_floor_le)    also have "x - 1 < x" by simp    finally have "of_int (floor (x - 1)) < x" .    hence "¬ x ≤ of_int (floor (x - 1))" by (simp only: not_le)    then show "¬ P (of_int (floor (x - 1)))"      unfolding P_def of_rat_of_int_eq using x by fast  qed  obtain b where b: "P b"  proof    show "P (of_int (ceiling z))"    unfolding P_def of_rat_of_int_eq    proof      fix y assume "y ∈ S"      hence "y ≤ z" using z by simp      also have "z ≤ of_int (ceiling z)" by (rule le_of_int_ceiling)      finally show "y ≤ of_int (ceiling z)" .    qed  qed  def avg ≡ "λx y :: rat. x/2 + y/2"  def bisect ≡ "λ(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)"  def A ≡ "λn. fst ((bisect ^^ n) (a, b))"  def B ≡ "λn. snd ((bisect ^^ n) (a, b))"  def C ≡ "λn. avg (A n) (B n)"  have A_0 [simp]: "A 0 = a" unfolding A_def by simp  have B_0 [simp]: "B 0 = b" unfolding B_def by simp  have A_Suc [simp]: "!!n. A (Suc n) = (if P (C n) then A n else C n)"    unfolding A_def B_def C_def bisect_def split_def by simp  have B_Suc [simp]: "!!n. B (Suc n) = (if P (C n) then C n else B n)"    unfolding A_def B_def C_def bisect_def split_def by simp  have width: "!!n. B n - A n = (b - a) / 2^n"    apply (simp add: eq_divide_eq)    apply (induct_tac n, simp)    apply (simp add: C_def avg_def algebra_simps)    done  have twos: "!!y r :: rat. 0 < r ==> ∃n. y / 2 ^ n < r"    apply (simp add: divide_less_eq)    apply (subst mult_commute)    apply (frule_tac y=y in ex_less_of_nat_mult)    apply clarify    apply (rule_tac x=n in exI)    apply (erule less_trans)    apply (rule mult_strict_right_mono)    apply (rule le_less_trans [OF _ of_nat_less_two_power])    apply simp    apply assumption    done  have PA: "!!n. ¬ P (A n)"    by (induct_tac n, simp_all add: a)  have PB: "!!n. P (B n)"    by (induct_tac n, simp_all add: b)  have ab: "a < b"    using a b unfolding P_def    apply (clarsimp simp add: not_le)    apply (drule (1) bspec)    apply (drule (1) less_le_trans)    apply (simp add: of_rat_less)    done  have AB: "!!n. A n < B n"    by (induct_tac n, simp add: ab, simp add: C_def avg_def)  have A_mono: "!!i j. i ≤ j ==> A i ≤ A j"    apply (auto simp add: le_less [where 'a=nat])    apply (erule less_Suc_induct)    apply (clarsimp simp add: C_def avg_def)    apply (simp add: add_divide_distrib [symmetric])    apply (rule AB [THEN less_imp_le])    apply simp    done  have B_mono: "!!i j. i ≤ j ==> B j ≤ B i"    apply (auto simp add: le_less [where 'a=nat])    apply (erule less_Suc_induct)    apply (clarsimp simp add: C_def avg_def)    apply (simp add: add_divide_distrib [symmetric])    apply (rule AB [THEN less_imp_le])    apply simp    done  have cauchy_lemma:    "!!X. ∀n. ∀i≥n. A n ≤ X i ∧ X i ≤ B n ==> cauchy X"    apply (rule cauchyI)    apply (drule twos [where y="b - a"])    apply (erule exE)    apply (rule_tac x=n in exI, clarify, rename_tac i j)    apply (rule_tac y="B n - A n" in le_less_trans) defer    apply (simp add: width)    apply (drule_tac x=n in spec)    apply (frule_tac x=i in spec, drule (1) mp)    apply (frule_tac x=j in spec, drule (1) mp)    apply (frule A_mono, drule B_mono)    apply (frule A_mono, drule B_mono)    apply arith    done  have "cauchy A"    apply (rule cauchy_lemma [rule_format])    apply (simp add: A_mono)    apply (erule order_trans [OF less_imp_le [OF AB] B_mono])    done  have "cauchy B"    apply (rule cauchy_lemma [rule_format])    apply (simp add: B_mono)    apply (erule order_trans [OF A_mono less_imp_le [OF AB]])    done  have 1: "∀x∈S. x ≤ Real B"  proof    fix x assume "x ∈ S"    then show "x ≤ Real B"      using PB [unfolded P_def] `cauchy B`      by (simp add: le_RealI)  qed  have 2: "∀z. (∀x∈S. x ≤ z) --> Real A ≤ z"    apply clarify    apply (erule contrapos_pp)    apply (simp add: not_le)    apply (drule less_RealD [OF `cauchy A`], clarify)    apply (subgoal_tac "¬ P (A n)")    apply (simp add: P_def not_le, clarify)    apply (erule rev_bexI)    apply (erule (1) less_trans)    apply (simp add: PA)    done  have "vanishes (λn. (b - a) / 2 ^ n)"  proof (rule vanishesI)    fix r :: rat assume "0 < r"    then obtain k where k: "¦b - a¦ / 2 ^ k < r"      using twos by fast    have "∀n≥k. ¦(b - a) / 2 ^ n¦ < r"    proof (clarify)      fix n assume n: "k ≤ n"      have "¦(b - a) / 2 ^ n¦ = ¦b - a¦ / 2 ^ n"        by simp      also have "… ≤ ¦b - a¦ / 2 ^ k"        using n by (simp add: divide_left_mono mult_pos_pos)      also note k      finally show "¦(b - a) / 2 ^ n¦ < r" .    qed    thus "∃k. ∀n≥k. ¦(b - a) / 2 ^ n¦ < r" ..  qed  hence 3: "Real B = Real A"    by (simp add: eq_Real `cauchy A` `cauchy B` width)  show "∃y. (∀x∈S. x ≤ y) ∧ (∀z. (∀x∈S. x ≤ z) --> y ≤ z)"    using 1 2 3 by (rule_tac x="Real B" in exI, simp)qedsubsection {* Hiding implementation details *}hide_const (open) vanishes cauchy positive Realdeclare Real_induct [induct del]declare Abs_real_induct [induct del]declare Abs_real_cases [cases del]lemmas [transfer_rule del] =  real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer  zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer  times_real.transfer inverse_real.transfer positive.transfersubsection{*More Lemmas*}text {* BH: These lemmas should not be necessary; they should becovered by existing simp rules and simplification procedures. *}lemma real_mult_left_cancel: "(c::real) ≠ 0 ==> (c*a=c*b) = (a=b)"by simp (* redundant with mult_cancel_left *)lemma real_mult_right_cancel: "(c::real) ≠ 0 ==> (a*c=b*c) = (a=b)"by simp (* redundant with mult_cancel_right *)lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"by simp (* solved by linordered_ring_less_cancel_factor simproc *)lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z ≤ y*z) = (x≤y)"by simp (* solved by linordered_ring_le_cancel_factor simproc *)lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x ≤ z*y) = (x≤y)"by simp (* solved by linordered_ring_le_cancel_factor simproc *)subsection {* Embedding numbers into the Reals *}abbreviation  real_of_nat :: "nat => real"where  "real_of_nat ≡ of_nat"abbreviation  real_of_int :: "int => real"where  "real_of_int ≡ of_int"abbreviation  real_of_rat :: "rat => real"where  "real_of_rat ≡ of_rat"consts  (*overloaded constant for injecting other types into "real"*)  real :: "'a => real"defs (overloaded)  real_of_nat_def [code_unfold]: "real == real_of_nat"  real_of_int_def [code_unfold]: "real == real_of_int"declare [[coercion_enabled]]declare [[coercion "real::nat=>real"]]declare [[coercion "real::int=>real"]]declare [[coercion "int"]]declare [[coercion_map map]]declare [[coercion_map "% f g h x. g (h (f x))"]]declare [[coercion_map "% f g (x,y) . (f x, g y)"]]lemma real_eq_of_nat: "real = of_nat"  unfolding real_of_nat_def ..lemma real_eq_of_int: "real = of_int"  unfolding real_of_int_def ..lemma real_of_int_zero [simp]: "real (0::int) = 0"  by (simp add: real_of_int_def) lemma real_of_one [simp]: "real (1::int) = (1::real)"by (simp add: real_of_int_def) lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"by (simp add: real_of_int_def) lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"by (simp add: real_of_int_def) lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"by (simp add: real_of_int_def) lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"by (simp add: real_of_int_def) lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"by (simp add: real_of_int_def of_int_power)lemmas power_real_of_int = real_of_int_power [symmetric]lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"  apply (subst real_eq_of_int)+  apply (rule of_int_setsum)donelemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) =     (PROD x:A. real(f x))"  apply (subst real_eq_of_int)+  apply (rule of_int_setprod)donelemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"by (simp add: real_of_int_def) lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"by (simp add: real_of_int_def) lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"by (simp add: real_of_int_def) lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) ≤ real y) = (x ≤ y)"by (simp add: real_of_int_def) lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"by (simp add: real_of_int_def) lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"by (simp add: real_of_int_def) lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)" by (simp add: real_of_int_def)lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"by (simp add: real_of_int_def)lemma one_less_real_of_int_cancel_iff: "1 < real (i :: int) <-> 1 < i"  unfolding real_of_one[symmetric] real_of_int_less_iff ..lemma one_le_real_of_int_cancel_iff: "1 ≤ real (i :: int) <-> 1 ≤ i"  unfolding real_of_one[symmetric] real_of_int_le_iff ..lemma real_of_int_less_one_cancel_iff: "real (i :: int) < 1 <-> i < 1"  unfolding real_of_one[symmetric] real_of_int_less_iff ..lemma real_of_int_le_one_cancel_iff: "real (i :: int) ≤ 1 <-> i ≤ 1"  unfolding real_of_one[symmetric] real_of_int_le_iff ..lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"by (auto simp add: abs_if)lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"  apply (subgoal_tac "real n + 1 = real (n + 1)")  apply (simp del: real_of_int_add)  apply autodonelemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)"  apply (subgoal_tac "real m + 1 = real (m + 1)")  apply (simp del: real_of_int_add)  apply simpdonelemma real_of_int_div_aux: "(real (x::int)) / (real d) =     real (x div d) + (real (x mod d)) / (real d)"proof -  have "x = (x div d) * d + x mod d"    by auto  then have "real x = real (x div d) * real d + real(x mod d)"    by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym])  then have "real x / real d = ... / real d"    by simp  then show ?thesis    by (auto simp add: add_divide_distrib algebra_simps)qedlemma real_of_int_div: "(d :: int) dvd n ==>    real(n div d) = real n / real d"  apply (subst real_of_int_div_aux)  apply simp  apply (simp add: dvd_eq_mod_eq_0)donelemma real_of_int_div2:  "0 <= real (n::int) / real (x) - real (n div x)"  apply (case_tac "x = 0")  apply simp  apply (case_tac "0 < x")  apply (simp add: algebra_simps)  apply (subst real_of_int_div_aux)  apply simp  apply (subst zero_le_divide_iff)  apply auto  apply (simp add: algebra_simps)  apply (subst real_of_int_div_aux)  apply simp  apply (subst zero_le_divide_iff)  apply autodonelemma real_of_int_div3:  "real (n::int) / real (x) - real (n div x) <= 1"  apply (simp add: algebra_simps)  apply (subst real_of_int_div_aux)  apply (auto simp add: divide_le_eq intro: order_less_imp_le)donelemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" by (insert real_of_int_div2 [of n x], simp)lemma Ints_real_of_int [simp]: "real (x::int) ∈ Ints"unfolding real_of_int_def by (rule Ints_of_int)subsection{*Embedding the Naturals into the Reals*}lemma real_of_nat_zero [simp]: "real (0::nat) = 0"by (simp add: real_of_nat_def)lemma real_of_nat_1 [simp]: "real (1::nat) = 1"by (simp add: real_of_nat_def)lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"by (simp add: real_of_nat_def)lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"by (simp add: real_of_nat_def)(*Not for addsimps: often the LHS is used to represent a positive natural*)lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"by (simp add: real_of_nat_def)lemma real_of_nat_less_iff [iff]:      "(real (n::nat) < real m) = (n < m)"by (simp add: real_of_nat_def)lemma real_of_nat_le_iff [iff]: "(real (n::nat) ≤ real m) = (n ≤ m)"by (simp add: real_of_nat_def)lemma real_of_nat_ge_zero [iff]: "0 ≤ real (n::nat)"by (simp add: real_of_nat_def)lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"by (simp add: real_of_nat_def del: of_nat_Suc)lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"by (simp add: real_of_nat_def of_nat_mult)lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"by (simp add: real_of_nat_def of_nat_power)lemmas power_real_of_nat = real_of_nat_power [symmetric]lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) =     (SUM x:A. real(f x))"  apply (subst real_eq_of_nat)+  apply (rule of_nat_setsum)donelemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) =     (PROD x:A. real(f x))"  apply (subst real_eq_of_nat)+  apply (rule of_nat_setprod)donelemma real_of_card: "real (card A) = setsum (%x.1) A"  apply (subst card_eq_setsum)  apply (subst real_of_nat_setsum)  apply simpdonelemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"by (simp add: real_of_nat_def)lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)"by (simp add: real_of_nat_def)lemma real_of_nat_diff: "n ≤ m ==> real (m - n) = real (m::nat) - real n"by (simp add: add: real_of_nat_def of_nat_diff)lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"by (auto simp: real_of_nat_def)lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) ≤ 0) = (n = 0)"by (simp add: add: real_of_nat_def)lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"by (simp add: add: real_of_nat_def)lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)"  apply (subgoal_tac "real n + 1 = real (Suc n)")  apply simp  apply (auto simp add: real_of_nat_Suc)donelemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)"  apply (subgoal_tac "real m + 1 = real (Suc m)")  apply (simp add: less_Suc_eq_le)  apply (simp add: real_of_nat_Suc)donelemma real_of_nat_div_aux: "(real (x::nat)) / (real d) =     real (x div d) + (real (x mod d)) / (real d)"proof -  have "x = (x div d) * d + x mod d"    by auto  then have "real x = real (x div d) * real d + real(x mod d)"    by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym])  then have "real x / real d = … / real d"    by simp  then show ?thesis    by (auto simp add: add_divide_distrib algebra_simps)qedlemma real_of_nat_div: "(d :: nat) dvd n ==>    real(n div d) = real n / real d"  by (subst real_of_nat_div_aux)    (auto simp add: dvd_eq_mod_eq_0 [symmetric])lemma real_of_nat_div2:  "0 <= real (n::nat) / real (x) - real (n div x)"apply (simp add: algebra_simps)apply (subst real_of_nat_div_aux)apply simpapply (subst zero_le_divide_iff)apply simpdonelemma real_of_nat_div3:  "real (n::nat) / real (x) - real (n div x) <= 1"apply(case_tac "x = 0")apply (simp)apply (simp add: algebra_simps)apply (subst real_of_nat_div_aux)apply simpdonelemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" by (insert real_of_nat_div2 [of n x], simp)lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n"by (simp add: real_of_int_def real_of_nat_def)lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x"  apply (subgoal_tac "real(int(nat x)) = real(nat x)")  apply force  apply (simp only: real_of_int_of_nat_eq)donelemma Nats_real_of_nat [simp]: "real (n::nat) ∈ Nats"unfolding real_of_nat_def by (rule of_nat_in_Nats)lemma Ints_real_of_nat [simp]: "real (n::nat) ∈ Ints"unfolding real_of_nat_def by (rule Ints_of_nat)subsection{* Rationals *}lemma Rats_real_nat[simp]: "real(n::nat) ∈ \<rat>"by (simp add: real_eq_of_nat)lemma Rats_eq_int_div_int:  "\<rat> = { real(i::int)/real(j::int) |i j. j ≠ 0}" (is "_ = ?S")proof  show "\<rat> ⊆ ?S"  proof    fix x::real assume "x : \<rat>"    then obtain r where "x = of_rat r" unfolding Rats_def ..    have "of_rat r : ?S"      by (cases r)(auto simp add:of_rat_rat real_eq_of_int)    thus "x : ?S" using `x = of_rat r` by simp  qednext  show "?S ⊆ \<rat>"  proof(auto simp:Rats_def)    fix i j :: int assume "j ≠ 0"    hence "real i / real j = of_rat(Fract i j)"      by (simp add:of_rat_rat real_eq_of_int)    thus "real i / real j ∈ range of_rat" by blast  qedqedlemma Rats_eq_int_div_nat:  "\<rat> = { real(i::int)/real(n::nat) |i n. n ≠ 0}"proof(auto simp:Rats_eq_int_div_int)  fix i j::int assume "j ≠ 0"  show "EX (i'::int) (n::nat). real i/real j = real i'/real n ∧ 0<n"  proof cases    assume "j>0"    hence "real i/real j = real i/real(nat j) ∧ 0<nat j"      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)    thus ?thesis by blast  next    assume "~ j>0"    hence "real i/real j = real(-i)/real(nat(-j)) ∧ 0<nat(-j)" using `j≠0`      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)    thus ?thesis by blast  qednext  fix i::int and n::nat assume "0 < n"  hence "real i/real n = real i/real(int n) ∧ int n ≠ 0" by simp  thus "∃(i'::int) j::int. real i/real n = real i'/real j ∧ j ≠ 0" by blastqedlemma Rats_abs_nat_div_natE:  assumes "x ∈ \<rat>"  obtains m n :: nat  where "n ≠ 0" and "¦x¦ = real m / real n" and "gcd m n = 1"proof -  from `x ∈ \<rat>` obtain i::int and n::nat where "n ≠ 0" and "x = real i / real n"    by(auto simp add: Rats_eq_int_div_nat)  hence "¦x¦ = real(nat(abs i)) / real n" by simp  then obtain m :: nat where x_rat: "¦x¦ = real m / real n" by blast  let ?gcd = "gcd m n"  from `n≠0` have gcd: "?gcd ≠ 0" by simp  let ?k = "m div ?gcd"  let ?l = "n div ?gcd"  let ?gcd' = "gcd ?k ?l"  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"    by (rule dvd_mult_div_cancel)  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"    by (rule dvd_mult_div_cancel)  from `n≠0` and gcd_l have "?l ≠ 0" by (auto iff del: neq0_conv)  moreover  have "¦x¦ = real ?k / real ?l"  proof -    from gcd have "real ?k / real ?l =        real (?gcd * ?k) / real (?gcd * ?l)" by simp    also from gcd_k and gcd_l have "… = real m / real n" by simp    also from x_rat have "… = ¦x¦" ..    finally show ?thesis ..  qed  moreover  have "?gcd' = 1"  proof -    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"      by (rule gcd_mult_distrib_nat)    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp    with gcd show ?thesis by auto  qed  ultimately show ?thesis ..qedsubsection{*Numerals and Arithmetic*}lemma [code_abbrev]:  "real_of_int (numeral k) = numeral k"  "real_of_int (neg_numeral k) = neg_numeral k"  by simp_alltext{*Collapse applications of @{term real} to @{term number_of}*}lemma real_numeral [simp]:  "real (numeral v :: int) = numeral v"  "real (neg_numeral v :: int) = neg_numeral v"by (simp_all add: real_of_int_def)lemma real_of_nat_numeral [simp]:  "real (numeral v :: nat) = numeral v"by (simp add: real_of_nat_def)declaration {*  K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2]    (* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *)  #> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2]    (* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *)  #> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add},      @{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one},      @{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff},      @{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq},      @{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}]  #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat => real"})  #> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int => real"}))*}subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}lemma real_add_minus_iff [simp]: "(x + - a = (0::real)) = (x=a)" by arithtext {* FIXME: redundant with @{text add_eq_0_iff} below *}lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = -x)"by autolemma real_add_less_0_iff: "(x+y < (0::real)) = (y < -x)"by autolemma real_0_less_add_iff: "((0::real) < x+y) = (-x < y)"by autolemma real_add_le_0_iff: "(x+y ≤ (0::real)) = (y ≤ -x)"by autolemma real_0_le_add_iff: "((0::real) ≤ x+y) = (-x ≤ y)"by autosubsection {* Lemmas about powers *}text {* FIXME: declare this in Rings.thy or not at all *}declare abs_mult_self [simp](* used by Import/HOL/real.imp *)lemma two_realpow_ge_one: "(1::real) ≤ 2 ^ n"by simplemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"apply (induct "n")apply (auto simp add: real_of_nat_Suc)apply (subst mult_2)apply (erule add_less_le_mono)apply (rule two_realpow_ge_one)donetext {* TODO: no longer real-specific; rename and move elsewhere *}lemma realpow_Suc_le_self:  fixes r :: "'a::linordered_semidom"  shows "[| 0 ≤ r; r ≤ 1 |] ==> r ^ Suc n ≤ r"by (insert power_decreasing [of 1 "Suc n" r], simp)text {* TODO: no longer real-specific; rename and move elsewhere *}lemma realpow_minus_mult:  fixes x :: "'a::monoid_mult"  shows "0 < n ==> x ^ (n - 1) * x = x ^ n"by (simp add: power_commutes split add: nat_diff_split)text {* FIXME: declare this [simp] for all types, or not at all *}lemma real_two_squares_add_zero_iff [simp]:  "(x * x + y * y = 0) = ((x::real) = 0 ∧ y = 0)"by (rule sum_squares_eq_zero_iff)text {* FIXME: declare this [simp] for all types, or not at all *}lemma realpow_two_sum_zero_iff [simp]:     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"by (rule sum_power2_eq_zero_iff)lemma real_minus_mult_self_le [simp]: "-(u * u) ≤ (x * (x::real))"by (rule_tac y = 0 in order_trans, auto)lemma realpow_square_minus_le [simp]: "-(u ^ 2) ≤ (x::real) ^ 2"by (auto simp add: power2_eq_square)lemma numeral_power_le_real_of_nat_cancel_iff[simp]:  "(numeral x::real) ^ n ≤ real a <-> (numeral x::nat) ^ n ≤ a"  unfolding real_of_nat_le_iff[symmetric] by simplemma real_of_nat_le_numeral_power_cancel_iff[simp]:  "real a ≤ (numeral x::real) ^ n <-> a ≤ (numeral x::nat) ^ n"  unfolding real_of_nat_le_iff[symmetric] by simplemma numeral_power_le_real_of_int_cancel_iff[simp]:  "(numeral x::real) ^ n ≤ real a <-> (numeral x::int) ^ n ≤ a"  unfolding real_of_int_le_iff[symmetric] by simplemma real_of_int_le_numeral_power_cancel_iff[simp]:  "real a ≤ (numeral x::real) ^ n <-> a ≤ (numeral x::int) ^ n"  unfolding real_of_int_le_iff[symmetric] by simplemma neg_numeral_power_le_real_of_int_cancel_iff[simp]:  "(neg_numeral x::real) ^ n ≤ real a <-> (neg_numeral x::int) ^ n ≤ a"  unfolding real_of_int_le_iff[symmetric] by simplemma real_of_int_le_neg_numeral_power_cancel_iff[simp]:  "real a ≤ (neg_numeral x::real) ^ n <-> a ≤ (neg_numeral x::int) ^ n"  unfolding real_of_int_le_iff[symmetric] by simpsubsection{*Density of the Reals*}lemma real_lbound_gt_zero:     "[| (0::real) < d1; 0 < d2 |] ==> ∃e. 0 < e & e < d1 & e < d2"apply (rule_tac x = " (min d1 d2) /2" in exI)apply (simp add: min_def)donetext{*Similar results are proved in @{text Fields}*}lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)"  by autolemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y"  by autosubsection{*Absolute Value Function for the Reals*}lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"by (simp add: abs_if)(* FIXME: redundant, but used by Integration/RealRandVar.thy in AFP *)lemma abs_le_interval_iff: "(abs x ≤ r) = (-r≤x & x≤(r::real))"by (force simp add: abs_le_iff)lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"by (simp add: abs_if)lemma abs_real_of_nat_cancel [simp]: "abs (real x) = real (x::nat)"by (rule abs_of_nonneg [OF real_of_nat_ge_zero])lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"by simp lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) ≤ abs(x + -l) + abs(y + -m)"by simpsubsection {* Implementation of rational real numbers *}text {* Formal constructor *}definition Ratreal :: "rat => real" where  [code_abbrev, simp]: "Ratreal = of_rat"code_datatype Ratrealtext {* Numerals *}lemma [code_abbrev]:  "(of_rat (of_int a) :: real) = of_int a"  by simplemma [code_abbrev]:  "(of_rat 0 :: real) = 0"  by simplemma [code_abbrev]:  "(of_rat 1 :: real) = 1"  by simplemma [code_abbrev]:  "(of_rat (numeral k) :: real) = numeral k"  by simplemma [code_abbrev]:  "(of_rat (neg_numeral k) :: real) = neg_numeral k"  by simplemma [code_post]:  "(of_rat (0 / r)  :: real) = 0"  "(of_rat (r / 0)  :: real) = 0"  "(of_rat (1 / 1)  :: real) = 1"  "(of_rat (numeral k / 1) :: real) = numeral k"  "(of_rat (neg_numeral k / 1) :: real) = neg_numeral k"  "(of_rat (1 / numeral k) :: real) = 1 / numeral k"  "(of_rat (1 / neg_numeral k) :: real) = 1 / neg_numeral k"  "(of_rat (numeral k / numeral l)  :: real) = numeral k / numeral l"  "(of_rat (numeral k / neg_numeral l)  :: real) = numeral k / neg_numeral l"  "(of_rat (neg_numeral k / numeral l)  :: real) = neg_numeral k / numeral l"  "(of_rat (neg_numeral k / neg_numeral l)  :: real) = neg_numeral k / neg_numeral l"  by (simp_all add: of_rat_divide)text {* Operations *}lemma zero_real_code [code]:  "0 = Ratreal 0"by simplemma one_real_code [code]:  "1 = Ratreal 1"by simpinstantiation real :: equalbegindefinition "HOL.equal (x::real) y <-> x - y = 0"instance proofqed (simp add: equal_real_def)lemma real_equal_code [code]:  "HOL.equal (Ratreal x) (Ratreal y) <-> HOL.equal x y"  by (simp add: equal_real_def equal)lemma [code nbe]:  "HOL.equal (x::real) x <-> True"  by (rule equal_refl)endlemma real_less_eq_code [code]: "Ratreal x ≤ Ratreal y <-> x ≤ y"  by (simp add: of_rat_less_eq)lemma real_less_code [code]: "Ratreal x < Ratreal y <-> x < y"  by (simp add: of_rat_less)lemma real_plus_code [code]: "Ratreal x + Ratreal y = Ratreal (x + y)"  by (simp add: of_rat_add)lemma real_times_code [code]: "Ratreal x * Ratreal y = Ratreal (x * y)"  by (simp add: of_rat_mult)lemma real_uminus_code [code]: "- Ratreal x = Ratreal (- x)"  by (simp add: of_rat_minus)lemma real_minus_code [code]: "Ratreal x - Ratreal y = Ratreal (x - y)"  by (simp add: of_rat_diff)lemma real_inverse_code [code]: "inverse (Ratreal x) = Ratreal (inverse x)"  by (simp add: of_rat_inverse) lemma real_divide_code [code]: "Ratreal x / Ratreal y = Ratreal (x / y)"  by (simp add: of_rat_divide)lemma real_floor_code [code]: "floor (Ratreal x) = floor x"  by (metis Ratreal_def floor_le_iff floor_unique le_floor_iff of_int_floor_le of_rat_of_int_eq real_less_eq_code)text {* Quickcheck *}definition (in term_syntax)  valterm_ratreal :: "rat × (unit => Code_Evaluation.term) => real × (unit => Code_Evaluation.term)" where  [code_unfold]: "valterm_ratreal k = Code_Evaluation.valtermify Ratreal {·} k"notation fcomp (infixl "o>" 60)notation scomp (infixl "o->" 60)instantiation real :: randombegindefinition  "Quickcheck.random i = Quickcheck.random i o-> (λr. Pair (valterm_ratreal r))"instance ..endno_notation fcomp (infixl "o>" 60)no_notation scomp (infixl "o->" 60)instantiation real :: exhaustivebegindefinition  "exhaustive_real f d = Quickcheck_Exhaustive.exhaustive (%r. f (Ratreal r)) d"instance ..endinstantiation real :: full_exhaustivebegindefinition  "full_exhaustive_real f d = Quickcheck_Exhaustive.full_exhaustive (%r. f (valterm_ratreal r)) d"instance ..endinstantiation real :: narrowingbegindefinition  "narrowing = Quickcheck_Narrowing.apply (Quickcheck_Narrowing.cons Ratreal) narrowing"instance ..endsubsection {* Setup for Nitpick *}declaration {*  Nitpick_HOL.register_frac_type @{type_name real}   [(@{const_name zero_real_inst.zero_real}, @{const_name Nitpick.zero_frac}),    (@{const_name one_real_inst.one_real}, @{const_name Nitpick.one_frac}),    (@{const_name plus_real_inst.plus_real}, @{const_name Nitpick.plus_frac}),    (@{const_name times_real_inst.times_real}, @{const_name Nitpick.times_frac}),    (@{const_name uminus_real_inst.uminus_real}, @{const_name Nitpick.uminus_frac}),    (@{const_name inverse_real_inst.inverse_real}, @{const_name Nitpick.inverse_frac}),    (@{const_name ord_real_inst.less_real}, @{const_name Nitpick.less_frac}),    (@{const_name ord_real_inst.less_eq_real}, @{const_name Nitpick.less_eq_frac})]*}lemmas [nitpick_unfold] = inverse_real_inst.inverse_real one_real_inst.one_real    ord_real_inst.less_real ord_real_inst.less_eq_real plus_real_inst.plus_real    times_real_inst.times_real uminus_real_inst.uminus_real    zero_real_inst.zero_realend`