src/HOL/Hyperreal/NthRoot.thy
author paulson
Thu Jul 29 16:14:42 2004 +0200 (2004-07-29)
changeset 15085 5693a977a767
parent 14767 d2b071e65e4c
child 15131 c69542757a4d
permissions -rw-r--r--
removed some [iff] declarations from RealDef.thy, concerning inequalities
     1 (*  Title       : NthRoot.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 1998  University of Cambridge
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     6 
     7 header{*Existence of Nth Root*}
     8 
     9 theory NthRoot = SEQ + HSeries:
    10 
    11 text {*
    12   Various lemmas needed for this result. We follow the proof given by
    13   John Lindsay Orr (\texttt{jorr@math.unl.edu}) in his Analysis
    14   Webnotes available at \url{http://www.math.unl.edu/~webnotes}.
    15 
    16   Lemmas about sequences of reals are used to reach the result.
    17 *}
    18 
    19 lemma lemma_nth_realpow_non_empty:
    20      "[| (0::real) < a; 0 < n |] ==> \<exists>s. s : {x. x ^ n <= a & 0 < x}"
    21 apply (case_tac "1 <= a")
    22 apply (rule_tac x = 1 in exI)
    23 apply (drule_tac [2] linorder_not_le [THEN iffD1])
    24 apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc], simp) 
    25 apply (force intro!: realpow_Suc_le_self simp del: realpow_Suc)
    26 done
    27 
    28 text{*Used only just below*}
    29 lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
    30 by (insert power_increasing [of 1 n r], simp)
    31 
    32 lemma lemma_nth_realpow_isUb_ex:
    33      "[| (0::real) < a; 0 < n |]  
    34       ==> \<exists>u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u"
    35 apply (case_tac "1 <= a")
    36 apply (rule_tac x = a in exI)
    37 apply (drule_tac [2] linorder_not_le [THEN iffD1])
    38 apply (rule_tac [2] x = 1 in exI)
    39 apply (rule_tac [!] setleI [THEN isUbI], safe)
    40 apply (simp_all (no_asm))
    41 apply (rule_tac [!] ccontr)
    42 apply (drule_tac [!] linorder_not_le [THEN iffD1])
    43 apply (drule realpow_ge_self2, assumption)
    44 apply (drule_tac n = n in realpow_less)
    45 apply (assumption+)
    46 apply (drule real_le_trans, assumption)
    47 apply (drule_tac y = "y ^ n" in order_less_le_trans, assumption, simp) 
    48 apply (drule_tac n = n in zero_less_one [THEN realpow_less], auto)
    49 done
    50 
    51 lemma nth_realpow_isLub_ex:
    52      "[| (0::real) < a; 0 < n |]  
    53       ==> \<exists>u. isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u"
    54 by (blast intro: lemma_nth_realpow_isUb_ex lemma_nth_realpow_non_empty reals_complete)
    55 
    56  
    57 subsection{*First Half -- Lemmas First*}
    58 
    59 lemma lemma_nth_realpow_seq:
    60      "isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u  
    61            ==> u + inverse(real (Suc k)) ~: {x. x ^ n <= a & 0 < x}"
    62 apply (safe, drule isLubD2, blast)
    63 apply (simp add: linorder_not_less [symmetric])
    64 done
    65 
    66 lemma lemma_nth_realpow_isLub_gt_zero:
    67      "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u;  
    68          0 < a; 0 < n |] ==> 0 < u"
    69 apply (drule lemma_nth_realpow_non_empty, auto)
    70 apply (drule_tac y = s in isLub_isUb [THEN isUbD])
    71 apply (auto intro: order_less_le_trans)
    72 done
    73 
    74 lemma lemma_nth_realpow_isLub_ge:
    75      "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u;  
    76          0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real (Suc k))) ^ n"
    77 apply safe
    78 apply (frule lemma_nth_realpow_seq, safe)
    79 apply (auto elim: order_less_asym simp add: linorder_not_less [symmetric]
    80             iff: real_0_less_add_iff) --{*legacy iff rule!*}
    81 apply (simp add: linorder_not_less)
    82 apply (rule order_less_trans [of _ 0])
    83 apply (auto intro: lemma_nth_realpow_isLub_gt_zero)
    84 done
    85 
    86 text{*First result we want*}
    87 lemma realpow_nth_ge:
    88      "[| (0::real) < a; 0 < n;  
    89      isLub (UNIV::real set)  
    90      {x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n"
    91 apply (frule lemma_nth_realpow_isLub_ge, safe)
    92 apply (rule LIMSEQ_inverse_real_of_nat_add [THEN LIMSEQ_pow, THEN LIMSEQ_le_const])
    93 apply (auto simp add: real_of_nat_def)
    94 done
    95 
    96 subsection{*Second Half*}
    97 
    98 lemma less_isLub_not_isUb:
    99      "[| isLub (UNIV::real set) S u; x < u |]  
   100            ==> ~ isUb (UNIV::real set) S x"
   101 apply safe
   102 apply (drule isLub_le_isUb, assumption)
   103 apply (drule order_less_le_trans, auto)
   104 done
   105 
   106 lemma not_isUb_less_ex:
   107      "~ isUb (UNIV::real set) S u ==> \<exists>x \<in> S. u < x"
   108 apply (rule ccontr, erule swap)
   109 apply (rule setleI [THEN isUbI])
   110 apply (auto simp add: linorder_not_less [symmetric])
   111 done
   112 
   113 lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r"
   114 apply (simp (no_asm) add: right_distrib)
   115 apply (rule add_less_cancel_left [of "-r", THEN iffD1])
   116 apply (auto intro: mult_pos
   117             simp add: add_assoc [symmetric] neg_less_0_iff_less)
   118 done
   119 
   120 lemma real_mult_add_one_minus_ge_zero:
   121      "0 < r ==>  0 <= r*(1 + -inverse(real (Suc n)))"
   122 by (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff real_0_le_add_iff)
   123 
   124 lemma lemma_nth_realpow_isLub_le:
   125      "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u;  
   126        0 < a; 0 < n |] ==> ALL k. (u*(1 + -inverse(real (Suc k)))) ^ n <= a"
   127 apply safe
   128 apply (frule less_isLub_not_isUb [THEN not_isUb_less_ex])
   129 apply (rule_tac n = k in real_mult_less_self)
   130 apply (blast intro: lemma_nth_realpow_isLub_gt_zero, safe)
   131 apply (drule_tac n = k in
   132         lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero], assumption+)
   133 apply (blast intro: order_trans order_less_imp_le power_mono) 
   134 done
   135 
   136 text{*Second result we want*}
   137 lemma realpow_nth_le:
   138      "[| (0::real) < a; 0 < n;  
   139      isLub (UNIV::real set)  
   140      {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a"
   141 apply (frule lemma_nth_realpow_isLub_le, safe)
   142 apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult
   143                 [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2])
   144 apply (auto simp add: real_of_nat_def)
   145 done
   146 
   147 text{*The theorem at last!*}
   148 lemma realpow_nth: "[| (0::real) < a; 0 < n |] ==> \<exists>r. r ^ n = a"
   149 apply (frule nth_realpow_isLub_ex, auto)
   150 apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym)
   151 done
   152 
   153 (* positive only *)
   154 lemma realpow_pos_nth: "[| (0::real) < a; 0 < n |] ==> \<exists>r. 0 < r & r ^ n = a"
   155 apply (frule nth_realpow_isLub_ex, auto)
   156 apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym lemma_nth_realpow_isLub_gt_zero)
   157 done
   158 
   159 lemma realpow_pos_nth2: "(0::real) < a  ==> \<exists>r. 0 < r & r ^ Suc n = a"
   160 by (blast intro: realpow_pos_nth)
   161 
   162 (* uniqueness of nth positive root *)
   163 lemma realpow_pos_nth_unique:
   164      "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a"
   165 apply (auto intro!: realpow_pos_nth)
   166 apply (cut_tac x = r and y = y in linorder_less_linear, auto)
   167 apply (drule_tac x = r in realpow_less)
   168 apply (drule_tac [4] x = y in realpow_less, auto)
   169 done
   170 
   171 ML
   172 {*
   173 val nth_realpow_isLub_ex = thm"nth_realpow_isLub_ex";
   174 val realpow_nth_ge = thm"realpow_nth_ge";
   175 val less_isLub_not_isUb = thm"less_isLub_not_isUb";
   176 val not_isUb_less_ex = thm"not_isUb_less_ex";
   177 val realpow_nth_le = thm"realpow_nth_le";
   178 val realpow_nth = thm"realpow_nth";
   179 val realpow_pos_nth = thm"realpow_pos_nth";
   180 val realpow_pos_nth2 = thm"realpow_pos_nth2";
   181 val realpow_pos_nth_unique = thm"realpow_pos_nth_unique";
   182 *}
   183 
   184 end