src/HOL/RealDef.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 47108 2a1953f0d20d
child 47428 45b58fec9024
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28906
diff changeset
     1
(*  Title       : HOL/RealDef.thy
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
     2
    Author      : Jacques D. Fleuriot, 1998
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
     3
    Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
     4
    Additional contributions by Jeremy Avigad
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
     5
    Construction of Cauchy Reals by Brian Huffman, 2010
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
     6
*)
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
     7
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
     8
header {* Development of the Reals using Cauchy Sequences *}
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
     9
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    10
theory RealDef
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    11
imports Rat
15131
c69542757a4d New theory header syntax.
nipkow
parents: 15086
diff changeset
    12
begin
5588
a3ab526bb891 Revised version with Abelian group simprocs
paulson
parents:
diff changeset
    13
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    14
text {*
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    15
  This theory contains a formalization of the real numbers as
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    16
  equivalence classes of Cauchy sequences of rationals.  See
40810
142f890ceef6 use new 'file' antiquotation for reference to Dedekind_Real.thy
huffman
parents: 38857
diff changeset
    17
  @{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative
142f890ceef6 use new 'file' antiquotation for reference to Dedekind_Real.thy
huffman
parents: 38857
diff changeset
    18
  construction using Dedekind cuts.
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    19
*}
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    20
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    21
subsection {* Preliminary lemmas *}
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    22
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    23
lemma add_diff_add:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    24
  fixes a b c d :: "'a::ab_group_add"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    25
  shows "(a + c) - (b + d) = (a - b) + (c - d)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    26
  by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    27
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    28
lemma minus_diff_minus:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    29
  fixes a b :: "'a::ab_group_add"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    30
  shows "- a - - b = - (a - b)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    31
  by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    32
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    33
lemma mult_diff_mult:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    34
  fixes x y a b :: "'a::ring"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    35
  shows "(x * y - a * b) = x * (y - b) + (x - a) * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    36
  by (simp add: algebra_simps)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    37
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    38
lemma inverse_diff_inverse:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    39
  fixes a b :: "'a::division_ring"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    40
  assumes "a \<noteq> 0" and "b \<noteq> 0"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    41
  shows "inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    42
  using assms by (simp add: algebra_simps)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    43
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    44
lemma obtain_pos_sum:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    45
  fixes r :: rat assumes r: "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    46
  obtains s t where "0 < s" and "0 < t" and "r = s + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    47
proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    48
    from r show "0 < r/2" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    49
    from r show "0 < r/2" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    50
    show "r = r/2 + r/2" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    51
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    52
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    53
subsection {* Sequences that converge to zero *}
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    54
19765
dfe940911617 misc cleanup;
wenzelm
parents: 19023
diff changeset
    55
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    56
  vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    57
where
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    58
  "vanishes X = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    59
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    60
lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    61
  unfolding vanishes_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    62
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    63
lemma vanishesD: "\<lbrakk>vanishes X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    64
  unfolding vanishes_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    65
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    66
lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    67
  unfolding vanishes_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    68
  apply (cases "c = 0", auto)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    69
  apply (rule exI [where x="\<bar>c\<bar>"], auto)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    70
  done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    71
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    72
lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n. - X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    73
  unfolding vanishes_def by simp
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
    74
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    75
lemma vanishes_add:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    76
  assumes X: "vanishes X" and Y: "vanishes Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    77
  shows "vanishes (\<lambda>n. X n + Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    78
proof (rule vanishesI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    79
  fix r :: rat assume "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    80
  then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    81
    by (rule obtain_pos_sum)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    82
  obtain i where i: "\<forall>n\<ge>i. \<bar>X n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    83
    using vanishesD [OF X s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    84
  obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    85
    using vanishesD [OF Y t] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    86
  have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    87
  proof (clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    88
    fix n assume n: "i \<le> n" "j \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    89
    have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    90
    also have "\<dots> < s + t" by (simp add: add_strict_mono i j n)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    91
    finally show "\<bar>X n + Y n\<bar> < r" unfolding r .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    92
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    93
  thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    94
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    95
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    96
lemma vanishes_diff:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    97
  assumes X: "vanishes X" and Y: "vanishes Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    98
  shows "vanishes (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
    99
unfolding diff_minus by (intro vanishes_add vanishes_minus X Y)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   100
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   101
lemma vanishes_mult_bounded:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   102
  assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   103
  assumes Y: "vanishes (\<lambda>n. Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   104
  shows "vanishes (\<lambda>n. X n * Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   105
proof (rule vanishesI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   106
  fix r :: rat assume r: "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   107
  obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   108
    using X by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   109
  obtain b where b: "0 < b" "r = a * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   110
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   111
    show "0 < r / a" using r a by (simp add: divide_pos_pos)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   112
    show "r = a * (r / a)" using a by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   113
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   114
  obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   115
    using vanishesD [OF Y b(1)] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   116
  have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   117
    by (simp add: b(2) abs_mult mult_strict_mono' a k)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   118
  thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   119
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   120
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   121
subsection {* Cauchy sequences *}
5588
a3ab526bb891 Revised version with Abelian group simprocs
paulson
parents:
diff changeset
   122
19765
dfe940911617 misc cleanup;
wenzelm
parents: 19023
diff changeset
   123
definition
44278
1220ecb81e8f observe distinction between sets and predicates more properly
haftmann
parents: 43887
diff changeset
   124
  cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool"
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   125
where
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   126
  "cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   127
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   128
lemma cauchyI:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   129
  "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r) \<Longrightarrow> cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   130
  unfolding cauchy_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   131
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   132
lemma cauchyD:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   133
  "\<lbrakk>cauchy X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   134
  unfolding cauchy_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   135
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   136
lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   137
  unfolding cauchy_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   138
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   139
lemma cauchy_add [simp]:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   140
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   141
  shows "cauchy (\<lambda>n. X n + Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   142
proof (rule cauchyI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   143
  fix r :: rat assume "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   144
  then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   145
    by (rule obtain_pos_sum)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   146
  obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   147
    using cauchyD [OF X s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   148
  obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   149
    using cauchyD [OF Y t] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   150
  have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   151
  proof (clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   152
    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   153
    have "\<bar>(X m + Y m) - (X n + Y n)\<bar> \<le> \<bar>X m - X n\<bar> + \<bar>Y m - Y n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   154
      unfolding add_diff_add by (rule abs_triangle_ineq)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   155
    also have "\<dots> < s + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   156
      by (rule add_strict_mono, simp_all add: i j *)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   157
    finally show "\<bar>(X m + Y m) - (X n + Y n)\<bar> < r" unfolding r .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   158
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   159
  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m) - (X n + Y n)\<bar> < r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   160
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   161
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   162
lemma cauchy_minus [simp]:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   163
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   164
  shows "cauchy (\<lambda>n. - X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   165
using assms unfolding cauchy_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   166
unfolding minus_diff_minus abs_minus_cancel .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   167
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   168
lemma cauchy_diff [simp]:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   169
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   170
  shows "cauchy (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   171
using assms unfolding diff_minus by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   172
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   173
lemma cauchy_imp_bounded:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   174
  assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   175
proof -
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   176
  obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m - X n\<bar> < 1"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   177
    using cauchyD [OF assms zero_less_one] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   178
  show "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   179
  proof (intro exI conjI allI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   180
    have "0 \<le> \<bar>X 0\<bar>" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   181
    also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   182
    finally have "0 \<le> Max (abs ` X ` {..k})" .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   183
    thus "0 < Max (abs ` X ` {..k}) + 1" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   184
  next
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   185
    fix n :: nat
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   186
    show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   187
    proof (rule linorder_le_cases)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   188
      assume "n \<le> k"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   189
      hence "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   190
      thus "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   191
    next
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   192
      assume "k \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   193
      have "\<bar>X n\<bar> = \<bar>X k + (X n - X k)\<bar>" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   194
      also have "\<bar>X k + (X n - X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n - X k\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   195
        by (rule abs_triangle_ineq)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   196
      also have "\<dots> < Max (abs ` X ` {..k}) + 1"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   197
        by (rule add_le_less_mono, simp, simp add: k `k \<le> n`)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   198
      finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   199
    qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   200
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   201
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   202
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   203
lemma cauchy_mult [simp]:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   204
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   205
  shows "cauchy (\<lambda>n. X n * Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   206
proof (rule cauchyI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   207
  fix r :: rat assume "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   208
  then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   209
    by (rule obtain_pos_sum)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   210
  obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   211
    using cauchy_imp_bounded [OF X] by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   212
  obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   213
    using cauchy_imp_bounded [OF Y] by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   214
  obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   215
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   216
    show "0 < v/b" using v b(1) by (rule divide_pos_pos)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   217
    show "0 < u/a" using u a(1) by (rule divide_pos_pos)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   218
    show "r = a * (u/a) + (v/b) * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   219
      using a(1) b(1) `r = u + v` by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   220
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   221
  obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   222
    using cauchyD [OF X s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   223
  obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m - Y n\<bar> < t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   224
    using cauchyD [OF Y t] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   225
  have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m - X n * Y n\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   226
  proof (clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   227
    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   228
    have "\<bar>X m * Y m - X n * Y n\<bar> = \<bar>X m * (Y m - Y n) + (X m - X n) * Y n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   229
      unfolding mult_diff_mult ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   230
    also have "\<dots> \<le> \<bar>X m * (Y m - Y n)\<bar> + \<bar>(X m - X n) * Y n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   231
      by (rule abs_triangle_ineq)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   232
    also have "\<dots> = \<bar>X m\<bar> * \<bar>Y m - Y n\<bar> + \<bar>X m - X n\<bar> * \<bar>Y n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   233
      unfolding abs_mult ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   234
    also have "\<dots> < a * t + s * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   235
      by (simp_all add: add_strict_mono mult_strict_mono' a b i j *)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   236
    finally show "\<bar>X m * Y m - X n * Y n\<bar> < r" unfolding r .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   237
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   238
  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m - X n * Y n\<bar> < r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   239
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   240
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   241
lemma cauchy_not_vanishes_cases:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   242
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   243
  assumes nz: "\<not> vanishes X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   244
  shows "\<exists>b>0. \<exists>k. (\<forall>n\<ge>k. b < - X n) \<or> (\<forall>n\<ge>k. b < X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   245
proof -
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   246
  obtain r where "0 < r" and r: "\<forall>k. \<exists>n\<ge>k. r \<le> \<bar>X n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   247
    using nz unfolding vanishes_def by (auto simp add: not_less)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   248
  obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   249
    using `0 < r` by (rule obtain_pos_sum)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   250
  obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m - X n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   251
    using cauchyD [OF X s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   252
  obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   253
    using r by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   254
  have k: "\<forall>n\<ge>k. \<bar>X n - X k\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   255
    using i `i \<le> k` by auto
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   256
  have "X k \<le> - r \<or> r \<le> X k"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   257
    using `r \<le> \<bar>X k\<bar>` by auto
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   258
  hence "(\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   259
    unfolding `r = s + t` using k by auto
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   260
  hence "\<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   261
  thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t < - X n) \<or> (\<forall>n\<ge>k. t < X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   262
    using t by auto
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   263
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   264
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   265
lemma cauchy_not_vanishes:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   266
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   267
  assumes nz: "\<not> vanishes X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   268
  shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   269
using cauchy_not_vanishes_cases [OF assms]
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   270
by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   271
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   272
lemma cauchy_inverse [simp]:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   273
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   274
  assumes nz: "\<not> vanishes X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   275
  shows "cauchy (\<lambda>n. inverse (X n))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   276
proof (rule cauchyI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   277
  fix r :: rat assume "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   278
  obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   279
    using cauchy_not_vanishes [OF X nz] by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   280
  from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   281
  obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   282
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   283
    show "0 < b * r * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   284
      by (simp add: `0 < r` b mult_pos_pos)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   285
    show "r = inverse b * (b * r * b) * inverse b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   286
      using b by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   287
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   288
  obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m - X n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   289
    using cauchyD [OF X s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   290
  have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m) - inverse (X n)\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   291
  proof (clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   292
    fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   293
    have "\<bar>inverse (X m) - inverse (X n)\<bar> =
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   294
          inverse \<bar>X m\<bar> * \<bar>X m - X n\<bar> * inverse \<bar>X n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   295
      by (simp add: inverse_diff_inverse nz * abs_mult)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   296
    also have "\<dots> < inverse b * s * inverse b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   297
      by (simp add: mult_strict_mono less_imp_inverse_less
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   298
                    mult_pos_pos i j b * s)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   299
    finally show "\<bar>inverse (X m) - inverse (X n)\<bar> < r" unfolding r .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   300
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   301
  thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m) - inverse (X n)\<bar> < r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   302
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   303
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   304
subsection {* Equivalence relation on Cauchy sequences *}
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   305
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   306
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   307
  realrel :: "((nat \<Rightarrow> rat) \<times> (nat \<Rightarrow> rat)) set"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   308
where
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   309
  "realrel = {(X, Y). cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n - Y n)}"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   310
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   311
lemma refl_realrel: "refl_on {X. cauchy X} realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   312
  unfolding realrel_def by (rule refl_onI, clarsimp, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   313
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   314
lemma sym_realrel: "sym realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   315
  unfolding realrel_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   316
  by (rule symI, clarify, drule vanishes_minus, simp)
14484
ef8c7c5eb01b new treatment of equivalence classes
paulson
parents: 14476
diff changeset
   317
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   318
lemma trans_realrel: "trans realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   319
  unfolding realrel_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   320
  apply (rule transI, clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   321
  apply (drule (1) vanishes_add)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   322
  apply (simp add: algebra_simps)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   323
  done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   324
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   325
lemma equiv_realrel: "equiv {X. cauchy X} realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   326
  using refl_realrel sym_realrel trans_realrel
40815
6e2d17cc0d1d equivI has replaced equiv.intro
haftmann
parents: 38857
diff changeset
   327
  by (rule equivI)
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   328
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   329
subsection {* The field of real numbers *}
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   330
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   331
typedef (open) real = "{X. cauchy X} // realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   332
  by (fast intro: quotientI cauchy_const)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   333
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   334
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   335
  Real :: "(nat \<Rightarrow> rat) \<Rightarrow> real"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   336
where
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   337
  "Real X = Abs_real (realrel `` {X})"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   338
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   339
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   340
  real_case :: "((nat \<Rightarrow> rat) \<Rightarrow> 'a) \<Rightarrow> real \<Rightarrow> 'a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   341
where
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   342
  "real_case f x = (THE y. \<forall>X\<in>Rep_real x. y = f X)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   343
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   344
lemma Real_induct [induct type: real]:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   345
  "(\<And>X. cauchy X \<Longrightarrow> P (Real X)) \<Longrightarrow> P x"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   346
  unfolding Real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   347
  apply (induct x)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   348
  apply (erule quotientE)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   349
  apply (simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   350
  done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   351
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   352
lemma real_case_1:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   353
  assumes f: "congruent realrel f"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   354
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   355
  shows "real_case f (Real X) = f X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   356
  unfolding real_case_def Real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   357
  apply (subst Abs_real_inverse)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   358
  apply (simp add: quotientI X)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   359
  apply (rule the_equality)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   360
  apply clarsimp
40816
19c492929756 replaced slightly odd locale congruent by plain definition
haftmann
parents: 40815
diff changeset
   361
  apply (erule congruentD [OF f])
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   362
  apply (erule bspec)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   363
  apply simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   364
  apply (rule refl_onD [OF refl_realrel])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   365
  apply (simp add: X)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   366
  done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   367
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   368
lemma real_case_2:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   369
  assumes f: "congruent2 realrel realrel f"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   370
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   371
  shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   372
 apply (subst real_case_1 [OF _ X])
40816
19c492929756 replaced slightly odd locale congruent by plain definition
haftmann
parents: 40815
diff changeset
   373
  apply (rule congruentI)
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   374
  apply (subst real_case_1 [OF _ Y])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   375
   apply (rule congruent2_implies_congruent [OF equiv_realrel f])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   376
   apply (simp add: realrel_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   377
  apply (subst real_case_1 [OF _ Y])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   378
   apply (rule congruent2_implies_congruent [OF equiv_realrel f])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   379
   apply (simp add: realrel_def)
40817
781da1e8808c replaced slightly odd locale congruent2 by plain definition
haftmann
parents: 40816
diff changeset
   380
  apply (erule congruent2D [OF f])
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   381
  apply (rule refl_onD [OF refl_realrel])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   382
  apply (simp add: Y)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   383
  apply (rule real_case_1 [OF _ Y])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   384
  apply (rule congruent2_implies_congruent [OF equiv_realrel f])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   385
  apply (simp add: X)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   386
  done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   387
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   388
lemma eq_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   389
  "cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   390
  unfolding Real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   391
  apply (subst Abs_real_inject)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   392
  apply (simp add: quotientI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   393
  apply (simp add: quotientI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   394
  apply (simp add: eq_equiv_class_iff [OF equiv_realrel])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   395
  apply (simp add: realrel_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   396
  done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   397
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   398
lemma add_respects2_realrel:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   399
  "(\<lambda>X Y. Real (\<lambda>n. X n + Y n)) respects2 realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   400
proof (rule congruent2_commuteI [OF equiv_realrel, unfolded mem_Collect_eq])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   401
  fix X Y show "Real (\<lambda>n. X n + Y n) = Real (\<lambda>n. Y n + X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   402
    by (simp add: add_commute)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   403
next
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   404
  fix X assume X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   405
  fix Y Z assume "(Y, Z) \<in> realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   406
  hence Y: "cauchy Y" and Z: "cauchy Z" and YZ: "vanishes (\<lambda>n. Y n - Z n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   407
    unfolding realrel_def by simp_all
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   408
  show "Real (\<lambda>n. X n + Y n) = Real (\<lambda>n. X n + Z n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   409
  proof (rule eq_Real [THEN iffD2])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   410
    show "cauchy (\<lambda>n. X n + Y n)" using X Y by (rule cauchy_add)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   411
    show "cauchy (\<lambda>n. X n + Z n)" using X Z by (rule cauchy_add)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   412
    show "vanishes (\<lambda>n. (X n + Y n) - (X n + Z n))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   413
      unfolding add_diff_add using YZ by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   414
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   415
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   416
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   417
lemma minus_respects_realrel:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   418
  "(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
40816
19c492929756 replaced slightly odd locale congruent by plain definition
haftmann
parents: 40815
diff changeset
   419
proof (rule congruentI)
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   420
  fix X Y assume "(X, Y) \<in> realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   421
  hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   422
    unfolding realrel_def by simp_all
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   423
  show "Real (\<lambda>n. - X n) = Real (\<lambda>n. - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   424
  proof (rule eq_Real [THEN iffD2])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   425
    show "cauchy (\<lambda>n. - X n)" using X by (rule cauchy_minus)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   426
    show "cauchy (\<lambda>n. - Y n)" using Y by (rule cauchy_minus)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   427
    show "vanishes (\<lambda>n. (- X n) - (- Y n))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   428
      unfolding minus_diff_minus using XY by (rule vanishes_minus)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   429
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   430
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   431
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   432
lemma mult_respects2_realrel:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   433
  "(\<lambda>X Y. Real (\<lambda>n. X n * Y n)) respects2 realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   434
proof (rule congruent2_commuteI [OF equiv_realrel, unfolded mem_Collect_eq])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   435
  fix X Y
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   436
  show "Real (\<lambda>n. X n * Y n) = Real (\<lambda>n. Y n * X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   437
    by (simp add: mult_commute)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   438
next
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   439
  fix X assume X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   440
  fix Y Z assume "(Y, Z) \<in> realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   441
  hence Y: "cauchy Y" and Z: "cauchy Z" and YZ: "vanishes (\<lambda>n. Y n - Z n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   442
    unfolding realrel_def by simp_all
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   443
  show "Real (\<lambda>n. X n * Y n) = Real (\<lambda>n. X n * Z n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   444
  proof (rule eq_Real [THEN iffD2])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   445
    show "cauchy (\<lambda>n. X n * Y n)" using X Y by (rule cauchy_mult)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   446
    show "cauchy (\<lambda>n. X n * Z n)" using X Z by (rule cauchy_mult)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   447
    have "vanishes (\<lambda>n. X n * (Y n - Z n))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   448
      by (intro vanishes_mult_bounded cauchy_imp_bounded X YZ)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   449
    thus "vanishes (\<lambda>n. X n * Y n - X n * Z n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   450
      by (simp add: right_diff_distrib)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   451
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   452
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   453
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   454
lemma vanishes_diff_inverse:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   455
  assumes X: "cauchy X" "\<not> vanishes X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   456
  assumes Y: "cauchy Y" "\<not> vanishes Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   457
  assumes XY: "vanishes (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   458
  shows "vanishes (\<lambda>n. inverse (X n) - inverse (Y n))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   459
proof (rule vanishesI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   460
  fix r :: rat assume r: "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   461
  obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   462
    using cauchy_not_vanishes [OF X] by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   463
  obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   464
    using cauchy_not_vanishes [OF Y] by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   465
  obtain s where s: "0 < s" and "inverse a * s * inverse b = r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   466
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   467
    show "0 < a * r * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   468
      using a r b by (simp add: mult_pos_pos)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   469
    show "inverse a * (a * r * b) * inverse b = r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   470
      using a r b by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   471
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   472
  obtain k where k: "\<forall>n\<ge>k. \<bar>X n - Y n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   473
    using vanishesD [OF XY s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   474
  have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   475
  proof (clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   476
    fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   477
    have "X n \<noteq> 0" and "Y n \<noteq> 0"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   478
      using i j a b n by auto
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   479
    hence "\<bar>inverse (X n) - inverse (Y n)\<bar> =
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   480
        inverse \<bar>X n\<bar> * \<bar>X n - Y n\<bar> * inverse \<bar>Y n\<bar>"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   481
      by (simp add: inverse_diff_inverse abs_mult)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   482
    also have "\<dots> < inverse a * s * inverse b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   483
      apply (intro mult_strict_mono' less_imp_inverse_less)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   484
      apply (simp_all add: a b i j k n mult_nonneg_nonneg)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   485
      done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   486
    also note `inverse a * s * inverse b = r`
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   487
    finally show "\<bar>inverse (X n) - inverse (Y n)\<bar> < r" .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   488
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   489
  thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n) - inverse (Y n)\<bar> < r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   490
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   491
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   492
lemma inverse_respects_realrel:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   493
  "(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   494
    (is "?inv respects realrel")
40816
19c492929756 replaced slightly odd locale congruent by plain definition
haftmann
parents: 40815
diff changeset
   495
proof (rule congruentI)
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   496
  fix X Y assume "(X, Y) \<in> realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   497
  hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   498
    unfolding realrel_def by simp_all
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   499
  have "vanishes X \<longleftrightarrow> vanishes Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   500
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   501
    assume "vanishes X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   502
    from vanishes_diff [OF this XY] show "vanishes Y" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   503
  next
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   504
    assume "vanishes Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   505
    from vanishes_add [OF this XY] show "vanishes X" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   506
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   507
  thus "?inv X = ?inv Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   508
    by (simp add: vanishes_diff_inverse eq_Real X Y XY)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   509
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   510
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   511
instantiation real :: field_inverse_zero
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   512
begin
5588
a3ab526bb891 Revised version with Abelian group simprocs
paulson
parents:
diff changeset
   513
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   514
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   515
  "0 = Real (\<lambda>n. 0)"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   516
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   517
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   518
  "1 = Real (\<lambda>n. 1)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   519
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   520
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   521
  "x + y = real_case (\<lambda>X. real_case (\<lambda>Y. Real (\<lambda>n. X n + Y n)) y) x"
5588
a3ab526bb891 Revised version with Abelian group simprocs
paulson
parents:
diff changeset
   522
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   523
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   524
  "- x = real_case (\<lambda>X. Real (\<lambda>n. - X n)) x"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   525
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   526
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   527
  "x - y = (x::real) + - y"
10606
e3229a37d53f converted rinv to inverse;
bauerg
parents: 9391
diff changeset
   528
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   529
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   530
  "x * y = real_case (\<lambda>X. real_case (\<lambda>Y. Real (\<lambda>n. X n * Y n)) y) x"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   531
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   532
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   533
  "inverse =
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   534
    real_case (\<lambda>X. if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
14484
ef8c7c5eb01b new treatment of equivalence classes
paulson
parents: 14476
diff changeset
   535
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   536
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   537
  "x / y = (x::real) * inverse y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   538
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   539
lemma add_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   540
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   541
  shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   542
  unfolding plus_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   543
  by (rule real_case_2 [OF add_respects2_realrel X Y])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   544
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   545
lemma minus_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   546
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   547
  shows "- Real X = Real (\<lambda>n. - X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   548
  unfolding uminus_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   549
  by (rule real_case_1 [OF minus_respects_realrel X])
5588
a3ab526bb891 Revised version with Abelian group simprocs
paulson
parents:
diff changeset
   550
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   551
lemma diff_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   552
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   553
  shows "Real X - Real Y = Real (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   554
  unfolding minus_real_def diff_minus
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   555
  by (simp add: minus_Real add_Real X Y)
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   556
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   557
lemma mult_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   558
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   559
  shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   560
  unfolding times_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   561
  by (rule real_case_2 [OF mult_respects2_realrel X Y])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   562
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   563
lemma inverse_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   564
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   565
  shows "inverse (Real X) =
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   566
    (if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   567
  unfolding inverse_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   568
  by (rule real_case_1 [OF inverse_respects_realrel X])
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   569
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   570
instance proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   571
  fix a b c :: real
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   572
  show "a + b = b + a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   573
    by (induct a, induct b) (simp add: add_Real add_ac)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   574
  show "(a + b) + c = a + (b + c)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   575
    by (induct a, induct b, induct c) (simp add: add_Real add_ac)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   576
  show "0 + a = a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   577
    unfolding zero_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   578
    by (induct a) (simp add: add_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   579
  show "- a + a = 0"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   580
    unfolding zero_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   581
    by (induct a) (simp add: minus_Real add_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   582
  show "a - b = a + - b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   583
    by (rule minus_real_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   584
  show "(a * b) * c = a * (b * c)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   585
    by (induct a, induct b, induct c) (simp add: mult_Real mult_ac)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   586
  show "a * b = b * a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   587
    by (induct a, induct b) (simp add: mult_Real mult_ac)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   588
  show "1 * a = a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   589
    unfolding one_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   590
    by (induct a) (simp add: mult_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   591
  show "(a + b) * c = a * c + b * c"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   592
    by (induct a, induct b, induct c)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   593
       (simp add: mult_Real add_Real algebra_simps)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   594
  show "(0\<Colon>real) \<noteq> (1\<Colon>real)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   595
    unfolding zero_real_def one_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   596
    by (simp add: eq_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   597
  show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   598
    unfolding zero_real_def one_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   599
    apply (induct a)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   600
    apply (simp add: eq_Real inverse_Real mult_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   601
    apply (rule vanishesI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   602
    apply (frule (1) cauchy_not_vanishes, clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   603
    apply (rule_tac x=k in exI, clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   604
    apply (drule_tac x=n in spec, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   605
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   606
  show "a / b = a * inverse b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   607
    by (rule divide_real_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   608
  show "inverse (0::real) = 0"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   609
    by (simp add: zero_real_def inverse_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   610
qed
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   611
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   612
end
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   613
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   614
subsection {* Positive reals *}
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   615
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   616
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   617
  positive :: "real \<Rightarrow> bool"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   618
where
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   619
  "positive = real_case (\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   620
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   621
lemma bool_congruentI:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   622
  assumes sym: "sym r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   623
  assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   624
  shows "P respects r"
40816
19c492929756 replaced slightly odd locale congruent by plain definition
haftmann
parents: 40815
diff changeset
   625
apply (rule congruentI)
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   626
apply (rule iffI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   627
apply (erule (1) P)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   628
apply (erule (1) P [OF symD [OF sym]])
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   629
done
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   630
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   631
lemma positive_respects_realrel:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   632
  "(\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n) respects realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   633
proof (rule bool_congruentI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   634
  show "sym realrel" by (rule sym_realrel)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   635
next
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   636
  fix X Y assume "(X, Y) \<in> realrel"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   637
  hence XY: "vanishes (\<lambda>n. X n - Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   638
    unfolding realrel_def by simp_all
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   639
  assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   640
  then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   641
    by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   642
  obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   643
    using `0 < r` by (rule obtain_pos_sum)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   644
  obtain j where j: "\<forall>n\<ge>j. \<bar>X n - Y n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   645
    using vanishesD [OF XY s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   646
  have "\<forall>n\<ge>max i j. t < Y n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   647
  proof (clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   648
    fix n assume n: "i \<le> n" "j \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   649
    have "\<bar>X n - Y n\<bar> < s" and "r < X n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   650
      using i j n by simp_all
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   651
    thus "t < Y n" unfolding r by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   652
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   653
  thus "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast
14484
ef8c7c5eb01b new treatment of equivalence classes
paulson
parents: 14476
diff changeset
   654
qed
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   655
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   656
lemma positive_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   657
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   658
  shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   659
unfolding positive_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   660
by (rule real_case_1 [OF positive_respects_realrel X])
23287
063039db59dd define (1::preal); clean up instance declarations
huffman
parents: 23031
diff changeset
   661
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   662
lemma positive_zero: "\<not> positive 0"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   663
unfolding zero_real_def by (auto simp add: positive_Real)
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   664
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   665
lemma positive_add:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   666
  "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   667
apply (induct x, induct y, rename_tac Y X)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   668
apply (simp add: add_Real positive_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   669
apply (clarify, rename_tac a b i j)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   670
apply (rule_tac x="a + b" in exI, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   671
apply (rule_tac x="max i j" in exI, clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   672
apply (simp add: add_strict_mono)
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   673
done
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   674
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   675
lemma positive_mult:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   676
  "positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   677
apply (induct x, induct y, rename_tac Y X)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   678
apply (simp add: mult_Real positive_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   679
apply (clarify, rename_tac a b i j)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   680
apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   681
apply (rule_tac x="max i j" in exI, clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   682
apply (rule mult_strict_mono, auto)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   683
done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   684
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   685
lemma positive_minus:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   686
  "\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive (- x)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   687
apply (induct x, rename_tac X)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   688
apply (simp add: zero_real_def eq_Real minus_Real positive_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   689
apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast)
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   690
done
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   691
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   692
instantiation real :: linordered_field_inverse_zero
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   693
begin
14341
a09441bd4f1e Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents: 14335
diff changeset
   694
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   695
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   696
  "x < y \<longleftrightarrow> positive (y - x)"
14341
a09441bd4f1e Ring_and_Field now requires axiom add_left_imp_eq for semirings.
paulson
parents: 14335
diff changeset
   697
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   698
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   699
  "x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   700
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   701
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   702
  "abs (a::real) = (if a < 0 then - a else a)"
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   703
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   704
definition
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   705
  "sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
14269
502a7c95de73 conversion of some Real theories to Isar scripts
paulson
parents: 13487
diff changeset
   706
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   707
instance proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   708
  fix a b c :: real
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   709
  show "\<bar>a\<bar> = (if a < 0 then - a else a)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   710
    by (rule abs_real_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   711
  show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   712
    unfolding less_eq_real_def less_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   713
    by (auto, drule (1) positive_add, simp_all add: positive_zero)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   714
  show "a \<le> a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   715
    unfolding less_eq_real_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   716
  show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   717
    unfolding less_eq_real_def less_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   718
    by (auto, drule (1) positive_add, simp add: algebra_simps)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   719
  show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   720
    unfolding less_eq_real_def less_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   721
    by (auto, drule (1) positive_add, simp add: positive_zero)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   722
  show "a \<le> b \<Longrightarrow> c + a \<le> c + b"
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46670
diff changeset
   723
    unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46670
diff changeset
   724
    (* FIXME: Procedure int_combine_numerals: c + b - (c + a) \<equiv> b + - a *)
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46670
diff changeset
   725
    (* Should produce c + b - (c + a) \<equiv> b - a *)
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   726
  show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   727
    by (rule sgn_real_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   728
  show "a \<le> b \<or> b \<le> a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   729
    unfolding less_eq_real_def less_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   730
    by (auto dest!: positive_minus)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   731
  show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   732
    unfolding less_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   733
    by (drule (1) positive_mult, simp add: algebra_simps)
23288
3e45b5464d2b remove references to preal-specific theorems
huffman
parents: 23287
diff changeset
   734
qed
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
   735
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   736
end
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   737
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   738
instantiation real :: distrib_lattice
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   739
begin
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   740
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   741
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   742
  "(inf :: real \<Rightarrow> real \<Rightarrow> real) = min"
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   743
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   744
definition
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   745
  "(sup :: real \<Rightarrow> real \<Rightarrow> real) = max"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   746
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   747
instance proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   748
qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   749
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   750
end
25571
c9e39eafc7a0 instantiation target rather than legacy instance
haftmann
parents: 25546
diff changeset
   751
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   752
lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   753
apply (induct x)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   754
apply (simp add: zero_real_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   755
apply (simp add: one_real_def add_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   756
done
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
   757
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   758
lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   759
apply (cases x rule: int_diff_cases)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   760
apply (simp add: of_nat_Real diff_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   761
done
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   762
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   763
lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   764
apply (induct x)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   765
apply (simp add: Fract_of_int_quotient of_rat_divide)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   766
apply (simp add: of_int_Real divide_inverse)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   767
apply (simp add: inverse_Real mult_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   768
done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   769
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   770
instance real :: archimedean_field
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   771
proof
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   772
  fix x :: real
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   773
  show "\<exists>z. x \<le> of_int z"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   774
    apply (induct x)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   775
    apply (frule cauchy_imp_bounded, clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   776
    apply (rule_tac x="ceiling b + 1" in exI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   777
    apply (rule less_imp_le)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   778
    apply (simp add: of_int_Real less_real_def diff_Real positive_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   779
    apply (rule_tac x=1 in exI, simp add: algebra_simps)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   780
    apply (rule_tac x=0 in exI, clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   781
    apply (rule le_less_trans [OF abs_ge_self])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   782
    apply (rule less_le_trans [OF _ le_of_int_ceiling])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   783
    apply simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   784
    done
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   785
qed
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
   786
43732
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   787
instantiation real :: floor_ceiling
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   788
begin
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   789
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   790
definition [code del]:
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   791
  "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))"
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   792
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   793
instance proof
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   794
  fix x :: real
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   795
  show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)"
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   796
    unfolding floor_real_def using floor_exists1 by (rule theI')
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   797
qed
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   798
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   799
end
6b2bdc57155b adding a floor_ceiling type class for different instantiations of floor (changeset from Brian Huffman)
bulwahn
parents: 42311
diff changeset
   800
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   801
subsection {* Completeness *}
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   802
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   803
lemma not_positive_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   804
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   805
  shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   806
unfolding positive_Real [OF X]
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   807
apply (auto, unfold not_less)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   808
apply (erule obtain_pos_sum)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   809
apply (drule_tac x=s in spec, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   810
apply (drule_tac r=t in cauchyD [OF X], clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   811
apply (drule_tac x=k in spec, clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   812
apply (rule_tac x=n in exI, clarify, rename_tac m)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   813
apply (drule_tac x=m in spec, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   814
apply (drule_tac x=n in spec, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   815
apply (drule spec, drule (1) mp, clarify, rename_tac i)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   816
apply (rule_tac x="max i k" in exI, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   817
done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   818
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   819
lemma le_Real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   820
  assumes X: "cauchy X" and Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   821
  shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   822
unfolding not_less [symmetric, where 'a=real] less_real_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   823
apply (simp add: diff_Real not_positive_Real X Y)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   824
apply (simp add: diff_le_eq add_ac)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   825
done
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   826
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   827
lemma le_RealI:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   828
  assumes Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   829
  shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   830
proof (induct x)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   831
  fix X assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   832
  hence le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   833
    by (simp add: of_rat_Real le_Real)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   834
  {
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   835
    fix r :: rat assume "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   836
    then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   837
      by (rule obtain_pos_sum)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   838
    obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m - Y n\<bar> < s"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   839
      using cauchyD [OF Y s] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   840
    obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   841
      using le [OF t] ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   842
    have "\<forall>n\<ge>max i j. X n \<le> Y n + r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   843
    proof (clarsimp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   844
      fix n assume n: "i \<le> n" "j \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   845
      have "X n \<le> Y i + t" using n j by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   846
      moreover have "\<bar>Y i - Y n\<bar> < s" using n i by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   847
      ultimately show "X n \<le> Y n + r" unfolding r by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   848
    qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   849
    hence "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   850
  }
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   851
  thus "Real X \<le> Real Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   852
    by (simp add: of_rat_Real le_Real X Y)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   853
qed
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   854
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   855
lemma Real_leI:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   856
  assumes X: "cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   857
  assumes le: "\<forall>n. of_rat (X n) \<le> y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   858
  shows "Real X \<le> y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   859
proof -
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   860
  have "- y \<le> - Real X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   861
    by (simp add: minus_Real X le_RealI of_rat_minus le)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   862
  thus ?thesis by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   863
qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   864
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   865
lemma less_RealD:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   866
  assumes Y: "cauchy Y"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   867
  shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   868
by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   869
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   870
lemma of_nat_less_two_power:
47108
2a1953f0d20d merged fork with new numeral representation (see NEWS)
huffman
parents: 46670
diff changeset
   871
  "of_nat n < (2::'a::linordered_idom) ^ n"
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   872
apply (induct n)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   873
apply simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   874
apply (subgoal_tac "(1::'a) \<le> 2 ^ n")
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   875
apply (drule (1) add_le_less_mono, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   876
apply simp
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   877
done
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   878
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   879
lemma complete_real:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   880
  fixes S :: "real set"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   881
  assumes "\<exists>x. x \<in> S" and "\<exists>z. \<forall>x\<in>S. x \<le> z"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   882
  shows "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   883
proof -
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   884
  obtain x where x: "x \<in> S" using assms(1) ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   885
  obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) ..
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   886
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   887
  def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   888
  obtain a where a: "\<not> P a"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   889
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   890
    have "of_int (floor (x - 1)) \<le> x - 1" by (rule of_int_floor_le)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   891
    also have "x - 1 < x" by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   892
    finally have "of_int (floor (x - 1)) < x" .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   893
    hence "\<not> x \<le> of_int (floor (x - 1))" by (simp only: not_le)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   894
    then show "\<not> P (of_int (floor (x - 1)))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   895
      unfolding P_def of_rat_of_int_eq using x by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   896
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   897
  obtain b where b: "P b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   898
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   899
    show "P (of_int (ceiling z))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   900
    unfolding P_def of_rat_of_int_eq
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   901
    proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   902
      fix y assume "y \<in> S"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   903
      hence "y \<le> z" using z by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   904
      also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   905
      finally show "y \<le> of_int (ceiling z)" .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   906
    qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   907
  qed
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   908
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   909
  def avg \<equiv> "\<lambda>x y :: rat. x/2 + y/2"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   910
  def bisect \<equiv> "\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   911
  def A \<equiv> "\<lambda>n. fst ((bisect ^^ n) (a, b))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   912
  def B \<equiv> "\<lambda>n. snd ((bisect ^^ n) (a, b))"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   913
  def C \<equiv> "\<lambda>n. avg (A n) (B n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   914
  have A_0 [simp]: "A 0 = a" unfolding A_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   915
  have B_0 [simp]: "B 0 = b" unfolding B_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   916
  have A_Suc [simp]: "\<And>n. A (Suc n) = (if P (C n) then A n else C n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   917
    unfolding A_def B_def C_def bisect_def split_def by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   918
  have B_Suc [simp]: "\<And>n. B (Suc n) = (if P (C n) then C n else B n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   919
    unfolding A_def B_def C_def bisect_def split_def by simp
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   920
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   921
  have width: "\<And>n. B n - A n = (b - a) / 2^n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   922
    apply (simp add: eq_divide_eq)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   923
    apply (induct_tac n, simp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   924
    apply (simp add: C_def avg_def algebra_simps)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   925
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   926
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   927
  have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   928
    apply (simp add: divide_less_eq)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   929
    apply (subst mult_commute)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   930
    apply (frule_tac y=y in ex_less_of_nat_mult)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   931
    apply clarify
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   932
    apply (rule_tac x=n in exI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   933
    apply (erule less_trans)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   934
    apply (rule mult_strict_right_mono)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   935
    apply (rule le_less_trans [OF _ of_nat_less_two_power])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   936
    apply simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   937
    apply assumption
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   938
    done
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
   939
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   940
  have PA: "\<And>n. \<not> P (A n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   941
    by (induct_tac n, simp_all add: a)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   942
  have PB: "\<And>n. P (B n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   943
    by (induct_tac n, simp_all add: b)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   944
  have ab: "a < b"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   945
    using a b unfolding P_def
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   946
    apply (clarsimp simp add: not_le)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   947
    apply (drule (1) bspec)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   948
    apply (drule (1) less_le_trans)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   949
    apply (simp add: of_rat_less)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   950
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   951
  have AB: "\<And>n. A n < B n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   952
    by (induct_tac n, simp add: ab, simp add: C_def avg_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   953
  have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   954
    apply (auto simp add: le_less [where 'a=nat])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   955
    apply (erule less_Suc_induct)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   956
    apply (clarsimp simp add: C_def avg_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   957
    apply (simp add: add_divide_distrib [symmetric])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   958
    apply (rule AB [THEN less_imp_le])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   959
    apply simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   960
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   961
  have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   962
    apply (auto simp add: le_less [where 'a=nat])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   963
    apply (erule less_Suc_induct)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   964
    apply (clarsimp simp add: C_def avg_def)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   965
    apply (simp add: add_divide_distrib [symmetric])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   966
    apply (rule AB [THEN less_imp_le])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   967
    apply simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   968
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   969
  have cauchy_lemma:
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   970
    "\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   971
    apply (rule cauchyI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   972
    apply (drule twos [where y="b - a"])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   973
    apply (erule exE)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   974
    apply (rule_tac x=n in exI, clarify, rename_tac i j)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   975
    apply (rule_tac y="B n - A n" in le_less_trans) defer
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   976
    apply (simp add: width)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   977
    apply (drule_tac x=n in spec)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   978
    apply (frule_tac x=i in spec, drule (1) mp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   979
    apply (frule_tac x=j in spec, drule (1) mp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   980
    apply (frule A_mono, drule B_mono)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   981
    apply (frule A_mono, drule B_mono)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   982
    apply arith
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   983
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   984
  have "cauchy A"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   985
    apply (rule cauchy_lemma [rule_format])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   986
    apply (simp add: A_mono)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   987
    apply (erule order_trans [OF less_imp_le [OF AB] B_mono])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   988
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   989
  have "cauchy B"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   990
    apply (rule cauchy_lemma [rule_format])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   991
    apply (simp add: B_mono)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   992
    apply (erule order_trans [OF A_mono less_imp_le [OF AB]])
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   993
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   994
  have 1: "\<forall>x\<in>S. x \<le> Real B"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   995
  proof
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   996
    fix x assume "x \<in> S"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   997
    then show "x \<le> Real B"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   998
      using PB [unfolded P_def] `cauchy B`
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
   999
      by (simp add: le_RealI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1000
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1001
  have 2: "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1002
    apply clarify
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1003
    apply (erule contrapos_pp)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1004
    apply (simp add: not_le)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1005
    apply (drule less_RealD [OF `cauchy A`], clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1006
    apply (subgoal_tac "\<not> P (A n)")
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1007
    apply (simp add: P_def not_le, clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1008
    apply (erule rev_bexI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1009
    apply (erule (1) less_trans)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1010
    apply (simp add: PA)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1011
    done
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1012
  have "vanishes (\<lambda>n. (b - a) / 2 ^ n)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1013
  proof (rule vanishesI)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1014
    fix r :: rat assume "0 < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1015
    then obtain k where k: "\<bar>b - a\<bar> / 2 ^ k < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1016
      using twos by fast
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1017
    have "\<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1018
    proof (clarify)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1019
      fix n assume n: "k \<le> n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1020
      have "\<bar>(b - a) / 2 ^ n\<bar> = \<bar>b - a\<bar> / 2 ^ n"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1021
        by simp
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1022
      also have "\<dots> \<le> \<bar>b - a\<bar> / 2 ^ k"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1023
        using n by (simp add: divide_left_mono mult_pos_pos)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1024
      also note k
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1025
      finally show "\<bar>(b - a) / 2 ^ n\<bar> < r" .
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1026
    qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1027
    thus "\<exists>k. \<forall>n\<ge>k. \<bar>(b - a) / 2 ^ n\<bar> < r" ..
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1028
  qed
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1029
  hence 3: "Real B = Real A"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1030
    by (simp add: eq_Real `cauchy A` `cauchy B` width)
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1031
  show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)"
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1032
    using 1 2 3 by (rule_tac x="Real B" in exI, simp)
14484
ef8c7c5eb01b new treatment of equivalence classes
paulson
parents: 14476
diff changeset
  1033
qed
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1034
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1035
subsection {* Hiding implementation details *}
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1036
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1037
hide_const (open) vanishes cauchy positive Real real_case
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1038
36795
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1039
declare Real_induct [induct del]
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1040
declare Abs_real_induct [induct del]
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1041
declare Abs_real_cases [cases del]
e05e1283c550 new construction of real numbers using Cauchy sequences
huffman
parents: 36776
diff changeset
  1042
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1043
subsection{*More Lemmas*}
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1044
36776
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1045
text {* BH: These lemmas should not be necessary; they should be
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1046
covered by existing simp rules and simplification procedures. *}
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1047
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1048
lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
36776
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1049
by simp (* redundant with mult_cancel_left *)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1050
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1051
lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
36776
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1052
by simp (* redundant with mult_cancel_right *)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1053
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1054
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)"
36776
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1055
by simp (* solved by linordered_ring_less_cancel_factor simproc *)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1056
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1057
lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)"
36776
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1058
by simp (* solved by linordered_ring_le_cancel_factor simproc *)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1059
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1060
lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)"
36776
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1061
by (rule mult_le_cancel_left_pos)
c137ae7673d3 remove a couple of redundant lemmas; simplify some proofs
huffman
parents: 36414
diff changeset
  1062
(* BH: Why doesn't "simp" prove this one, like it does the last one? *)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1063
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1064
24198
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1065
subsection {* Embedding numbers into the Reals *}
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1066
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1067
abbreviation
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1068
  real_of_nat :: "nat \<Rightarrow> real"
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1069
where
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1070
  "real_of_nat \<equiv> of_nat"
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1071
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1072
abbreviation
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1073
  real_of_int :: "int \<Rightarrow> real"
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1074
where
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1075
  "real_of_int \<equiv> of_int"
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1076
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1077
abbreviation
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1078
  real_of_rat :: "rat \<Rightarrow> real"
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1079
where
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1080
  "real_of_rat \<equiv> of_rat"
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1081
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1082
consts
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1083
  (*overloaded constant for injecting other types into "real"*)
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1084
  real :: "'a => real"
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1085
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1086
defs (overloaded)
31998
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31952
diff changeset
  1087
  real_of_nat_def [code_unfold]: "real == real_of_nat"
2c7a24f74db9 code attributes use common underscore convention
haftmann
parents: 31952
diff changeset
  1088
  real_of_int_def [code_unfold]: "real == real_of_int"
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1089
40939
2c150063cd4d setup subtyping/coercions once in HOL.thy, but enable it only later via configuration option;
wenzelm
parents: 40864
diff changeset
  1090
declare [[coercion_enabled]]
40864
4abaaadfdaf2 moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents: 40826
diff changeset
  1091
declare [[coercion "real::nat\<Rightarrow>real"]]
4abaaadfdaf2 moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents: 40826
diff changeset
  1092
declare [[coercion "real::int\<Rightarrow>real"]]
41022
81d337539d57 moved coercion decl. for int
nipkow
parents: 40939
diff changeset
  1093
declare [[coercion "int"]]
40864
4abaaadfdaf2 moved activation of coercion inference into RealDef and declared function real a coercion.
nipkow
parents: 40826
diff changeset
  1094
41024
ba961a606c67 move coercions to appropriate places
hoelzl
parents: 41022
diff changeset
  1095
declare [[coercion_map map]]
42112
9cb122742f5c Change coercion for RealDef to use function application (not composition)
noschinl
parents: 41920
diff changeset
  1096
declare [[coercion_map "% f g h x. g (h (f x))"]]
41024
ba961a606c67 move coercions to appropriate places
hoelzl
parents: 41022
diff changeset
  1097
declare [[coercion_map "% f g (x,y) . (f x, g y)"]]
ba961a606c67 move coercions to appropriate places
hoelzl
parents: 41022
diff changeset
  1098
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1099
lemma real_eq_of_nat: "real = of_nat"
24198
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1100
  unfolding real_of_nat_def ..
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1101
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1102
lemma real_eq_of_int: "real = of_int"
24198
4031da6d8ba3 adaptions for code generation
haftmann
parents: 24075
diff changeset
  1103
  unfolding real_of_int_def ..
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1104
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1105
lemma real_of_int_zero [simp]: "real (0::int) = 0"  
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1106
by (simp add: real_of_int_def) 
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1107
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1108
lemma real_of_one [simp]: "real (1::int) = (1::real)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1109
by (simp add: real_of_int_def) 
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1110
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1111
lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1112
by (simp add: real_of_int_def) 
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1113
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1114
lemma real_of_int_minus [simp]: "real(-x) = -real (x::int)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1115
by (simp add: real_of_int_def) 
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1116
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1117
lemma real_of_int_diff [simp]: "real(x - y) = real (x::int) - real y"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1118
by (simp add: real_of_int_def) 
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1119
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1120
lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1121
by (simp add: real_of_int_def) 
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1122
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1123
lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n"
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1124
by (simp add: real_of_int_def of_int_power)
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1125
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1126
lemmas power_real_of_int = real_of_int_power [symmetric]
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1127
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1128
lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1129
  apply (subst real_eq_of_int)+
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1130
  apply (rule of_int_setsum)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1131
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1132
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1133
lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) = 
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1134
    (PROD x:A. real(f x))"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1135
  apply (subst real_eq_of_int)+
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1136
  apply (rule of_int_setprod)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1137
done
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1138
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1139
lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1140
by (simp add: real_of_int_def) 
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1141
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1142
lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1143
by (simp add: real_of_int_def) 
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1144
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1145
lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1146
by (simp add: real_of_int_def) 
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1147
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1148
lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1149
by (simp add: real_of_int_def) 
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1150
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1151
lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1152
by (simp add: real_of_int_def) 
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1153
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1154
lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1155
by (simp add: real_of_int_def) 
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1156
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1157
lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)" 
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1158
by (simp add: real_of_int_def)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1159
27668
6eb20b2cecf8 Tuned and simplified proofs
chaieb
parents: 27652
diff changeset
  1160
lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1161
by (simp add: real_of_int_def)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1162
16888
7cb4bcfa058e added list of theorem changes to NEWS
avigad
parents: 16819
diff changeset
  1163
lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
7cb4bcfa058e added list of theorem changes to NEWS
avigad
parents: 16819
diff changeset
  1164
by (auto simp add: abs_if)
7cb4bcfa058e added list of theorem changes to NEWS
avigad
parents: 16819
diff changeset
  1165
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1166
lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1167
  apply (subgoal_tac "real n + 1 = real (n + 1)")
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1168
  apply (simp del: real_of_int_add)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1169
  apply auto
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1170
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1171
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1172
lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1173
  apply (subgoal_tac "real m + 1 = real (m + 1)")
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1174
  apply (simp del: real_of_int_add)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1175
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1176
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1177
46670
e9aa6d151329 removing unnecessary assumptions in RealDef;
bulwahn
parents: 46028
diff changeset
  1178
lemma real_of_int_div_aux: "(real (x::int)) / (real d) = 
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1179
    real (x div d) + (real (x mod d)) / (real d)"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1180
proof -
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1181
  have "x = (x div d) * d + x mod d"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1182
    by auto
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1183
  then have "real x = real (x div d) * real d + real(x mod d)"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1184
    by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym])
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1185
  then have "real x / real d = ... / real d"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1186
    by simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1187
  then show ?thesis
46670
e9aa6d151329 removing unnecessary assumptions in RealDef;
bulwahn
parents: 46028
diff changeset
  1188
    by (auto simp add: add_divide_distrib algebra_simps)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1189
qed
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1190
46670
e9aa6d151329 removing unnecessary assumptions in RealDef;
bulwahn
parents: 46028
diff changeset
  1191
lemma real_of_int_div: "(d :: int) dvd n ==>
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1192
    real(n div d) = real n / real d"
46670
e9aa6d151329 removing unnecessary assumptions in RealDef;
bulwahn
parents: 46028
diff changeset
  1193
  apply (subst real_of_int_div_aux)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1194
  apply simp
30042
31039ee583fa Removed subsumed lemmas
nipkow
parents: 29667
diff changeset
  1195
  apply (simp add: dvd_eq_mod_eq_0)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1196
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1197
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1198
lemma real_of_int_div2:
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1199
  "0 <= real (n::int) / real (x) - real (n div x)"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1200
  apply (case_tac "x = 0")
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1201
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1202
  apply (case_tac "0 < x")
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28952
diff changeset
  1203
  apply (simp add: algebra_simps)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1204
  apply (subst real_of_int_div_aux)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1205
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1206
  apply (subst zero_le_divide_iff)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1207
  apply auto
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28952
diff changeset
  1208
  apply (simp add: algebra_simps)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1209
  apply (subst real_of_int_div_aux)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1210
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1211
  apply (subst zero_le_divide_iff)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1212
  apply auto
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1213
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1214
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1215
lemma real_of_int_div3:
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1216
  "real (n::int) / real (x) - real (n div x) <= 1"
29667
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps;
nipkow
parents: 28952
diff changeset
  1217
  apply (simp add: algebra_simps)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1218
  apply (subst real_of_int_div_aux)
46670
e9aa6d151329 removing unnecessary assumptions in RealDef;
bulwahn
parents: 46028
diff changeset
  1219
  apply (auto simp add: divide_le_eq intro: order_less_imp_le)
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1220
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1221
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1222
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
27964
1e0303048c0b added const Rational
nipkow
parents: 27833
diff changeset
  1223
by (insert real_of_int_div2 [of n x], simp)
1e0303048c0b added const Rational
nipkow
parents: 27833
diff changeset
  1224
35635
90fffd5ff996 add simp rules about Ints, Nats
huffman
parents: 35344
diff changeset
  1225
lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
90fffd5ff996 add simp rules about Ints, Nats
huffman
parents: 35344
diff changeset
  1226
unfolding real_of_int_def by (rule Ints_of_int)
90fffd5ff996 add simp rules about Ints, Nats
huffman
parents: 35344
diff changeset
  1227
27964
1e0303048c0b added const Rational
nipkow
parents: 27833
diff changeset
  1228
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1229
subsection{*Embedding the Naturals into the Reals*}
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1230
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1231
lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1232
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1233
30082
43c5b7bfc791 make more proofs work whether or not One_nat_def is a simp rule
huffman
parents: 30042
diff changeset
  1234
lemma real_of_nat_1 [simp]: "real (1::nat) = 1"
43c5b7bfc791 make more proofs work whether or not One_nat_def is a simp rule
huffman
parents: 30042
diff changeset
  1235
by (simp add: real_of_nat_def)
43c5b7bfc791 make more proofs work whether or not One_nat_def is a simp rule
huffman
parents: 30042
diff changeset
  1236
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1237
lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)"
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1238
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1239
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1240
lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1241
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1242
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1243
(*Not for addsimps: often the LHS is used to represent a positive natural*)
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1244
lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1245
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1246
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1247
lemma real_of_nat_less_iff [iff]: 
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1248
     "(real (n::nat) < real m) = (n < m)"
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1249
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1250
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1251
lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1252
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1253
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1254
lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1255
by (simp add: real_of_nat_def zero_le_imp_of_nat)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1256
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1257
lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1258
by (simp add: real_of_nat_def del: of_nat_Suc)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1259
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1260
lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n"
23431
25ca91279a9b change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
huffman
parents: 23289
diff changeset
  1261
by (simp add: real_of_nat_def of_nat_mult)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1262
35344
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1263
lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n"
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1264
by (simp add: real_of_nat_def of_nat_power)
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1265
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1266
lemmas power_real_of_nat = real_of_nat_power [symmetric]
e0b46cd72414 moved some lemmas from RealPow to RealDef; changed orientation of real_of_int_power
huffman
parents: 35216
diff changeset
  1267
16819
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1268
lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1269
    (SUM x:A. real(f x))"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1270
  apply (subst real_eq_of_nat)+
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1271
  apply (rule of_nat_setsum)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1272
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1273
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1274
lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) = 
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1275
    (PROD x:A. real(f x))"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1276
  apply (subst real_eq_of_nat)+
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1277
  apply (rule of_nat_setprod)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1278
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1279
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1280
lemma real_of_card: "real (card A) = setsum (%x.1) A"
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1281
  apply (subst card_eq_setsum)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1282
  apply (subst real_of_nat_setsum)
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1283
  apply simp
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1284
done
00d8f9300d13 Additions to the Real (and Hyperreal) libraries:
avigad
parents: 16417
diff changeset
  1285
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1286
lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1287
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1288
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 14378
diff changeset
  1289
lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1290
by (simp add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1291
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1292
lemma real_of_nat_diff: "n \<le> m ==> real (m - n) = real (m::nat) - real n"
23438
dd824e86fa8a remove simp attribute from of_nat_diff, for backward compatibility with zdiff_int
huffman
parents: 23431
diff changeset
  1293
by (simp add: add: real_of_nat_def of_nat_diff)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1294
25162
ad4d5365d9d8 went back to >0
nipkow
parents: 25140
diff changeset
  1295
lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)"
25140
273772abbea2 More changes from >0 to ~=0::nat
nipkow
parents: 25134
diff changeset
  1296
by (auto simp: real_of_nat_def)
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1297
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1298
lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1299
by (simp add: add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1300
14365
3d4df8c166ae replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents: 14348
diff changeset
  1301
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0"
14378
69c4d5997669 generic of_nat and of_int functions, and generalization of iszero
paulson
parents: 14369
diff changeset
  1302
by (simp add: add: real_of_nat_def)
14334
6137d24eef79 tweaking of lemmas in RealDef, RealOrd
paulson
parents: 14329
diff changeset
  1303
16819