# HG changeset patch # User paulson # Date 1072197712 -3600 # Node ID c9c6832f9b22b1a60dbb58a3b782bccf86b25a80 # Parent 27724f528f82a77ffdf7ca79affe7e8db6aaccb6 converting Hyperreal/NthRoot to Isar diff -r 27724f528f82 -r c9c6832f9b22 src/HOL/Hyperreal/NthRoot.ML --- a/src/HOL/Hyperreal/NthRoot.ML Tue Dec 23 16:53:33 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,169 +0,0 @@ -(* Title : NthRoot.ML - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Existence of nth root. Adapted from - http://www.math.unl.edu/~webnotes -*) - -(*---------------------------------------------------------------------- - Existence of nth root - Various lemmas needed for this result. We follow the proof - given by John Lindsay Orr (jorr@math.unl.edu) in his Analysis - Webnotes available on the www at http://www.math.unl.edu/~webnotes - Lemmas about sequences of reals are used to reach the result. - ---------------------------------------------------------------------*) - -Goal "[| (0::real) < a; 0 < n |] \ -\ ==> EX s. s : {x. x ^ n <= a & 0 < x}"; -by (case_tac "1 <= a" 1); -by (res_inst_tac [("x","1")] exI 1); -by (dtac not_real_leE 2); -by (dtac (less_not_refl2 RS not0_implies_Suc) 2); -by (auto_tac (claset() addSIs [realpow_Suc_le_self], - simpset() addsimps [real_zero_less_one])); -qed "lemma_nth_realpow_non_empty"; - -Goal "[| (0::real) < a; 0 < n |] \ -\ ==> EX u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u"; -by (case_tac "1 <= a" 1); -by (res_inst_tac [("x","a")] exI 1); -by (dtac not_real_leE 2); -by (res_inst_tac [("x","1")] exI 2); -by (ALLGOALS(rtac (setleI RS isUbI))); -by Safe_tac; -by (ALLGOALS Simp_tac); -by (ALLGOALS(rtac ccontr)); -by (ALLGOALS(dtac not_real_leE)); -by (dtac realpow_ge_self2 1 THEN assume_tac 1); -by (dres_inst_tac [("n","n")] realpow_less 1); -by (REPEAT(assume_tac 1)); -by (dtac real_le_trans 1 THEN assume_tac 1); -by (dres_inst_tac [("y","y ^ n")] order_less_le_trans 1); -by (assume_tac 1 THEN etac real_less_irrefl 1); -by (dres_inst_tac [("n","n")] ((real_zero_less_one) RS realpow_less) 1); -by (Auto_tac); -qed "lemma_nth_realpow_isUb_ex"; - -Goal "[| (0::real) < a; 0 < n |] \ -\ ==> EX u. isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u"; -by (blast_tac (claset() addIs [lemma_nth_realpow_isUb_ex, - lemma_nth_realpow_non_empty,reals_complete]) 1); -qed "nth_realpow_isLub_ex"; - -(*--------------------------------------------- - First Half -- lemmas first - --------------------------------------------*) -Goal "isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u \ -\ ==> u + inverse(real_of_posnat k) ~: {x. x ^ n <= a & 0 < x}"; -by (Step_tac 1 THEN dtac isLubD2 1 THEN Blast_tac 1); -by (asm_full_simp_tac (simpset() addsimps [real_le_def]) 1); -val lemma_nth_realpow_seq = result(); - -Goal "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; \ -\ 0 < a; 0 < n |] ==> 0 < u"; -by (dtac lemma_nth_realpow_non_empty 1 THEN Auto_tac); -by (dres_inst_tac [("y","s")] (isLub_isUb RS isUbD) 1); -by (auto_tac (claset() addIs [order_less_le_trans],simpset())); -val lemma_nth_realpow_isLub_gt_zero = result(); - -Goal "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; \ -\ 0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real_of_posnat k)) ^ n"; -by (Step_tac 1); -by (ftac lemma_nth_realpow_seq 1 THEN Step_tac 1); -by (auto_tac (claset() addEs [real_less_asym], - simpset() addsimps [real_le_def])); -by (fold_tac [real_le_def]); -by (rtac real_less_trans 1); -by (auto_tac (claset() addIs [real_inv_real_of_posnat_gt_zero, - lemma_nth_realpow_isLub_gt_zero],simpset())); -val lemma_nth_realpow_isLub_ge = result(); - -(*----------------------- - First result we want - ----------------------*) -Goal "[| (0::real) < a; 0 < n; \ -\ isLub (UNIV::real set) \ -\ {x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n"; -by (ftac lemma_nth_realpow_isLub_ge 1 THEN Step_tac 1); -by (rtac (LIMSEQ_inverse_real_of_nat_add RS LIMSEQ_pow - RS LIMSEQ_le_const) 1); -by (auto_tac (claset(),simpset() addsimps [real_of_nat_def, - real_of_posnat_Suc])); -qed "realpow_nth_ge"; - -(*--------------------------------------------- - Second Half - --------------------------------------------*) - -Goal "[| isLub (UNIV::real set) S u; x < u |] \ -\ ==> ~ isUb (UNIV::real set) S x"; -by (Step_tac 1); -by (dtac isLub_le_isUb 1); -by (assume_tac 1); -by (dtac order_less_le_trans 1); -by (auto_tac (claset(),simpset() - addsimps [real_less_not_refl])); -qed "less_isLub_not_isUb"; - -Goal "~ isUb (UNIV::real set) S u \ -\ ==> EX x: S. u < x"; -by (rtac ccontr 1 THEN etac swap 1); -by (rtac (setleI RS isUbI) 1); -by (auto_tac (claset(),simpset() addsimps [real_le_def])); -qed "not_isUb_less_ex"; - -Goal "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; \ -\ 0 < a; 0 < n |] ==> ALL k. (u*(1 + -inverse(real_of_posnat k))) ^ n <= a"; -by (Step_tac 1); -by (forward_tac [less_isLub_not_isUb RS not_isUb_less_ex] 1); -by (res_inst_tac [("n","k")] real_mult_less_self 1); -by (blast_tac (claset() addIs [lemma_nth_realpow_isLub_gt_zero]) 1); -by (Step_tac 1); -by (dres_inst_tac [("n","k")] (lemma_nth_realpow_isLub_gt_zero RS - real_mult_add_one_minus_ge_zero) 1); -by (dtac (conjI RS realpow_le2) 3); -by (rtac (CLAIM "x < y ==> (x::real) <= y") 3); -by (auto_tac (claset() addIs [real_le_trans],simpset())); -val lemma_nth_realpow_isLub_le = result(); - -(*----------------------- - Second result we want - ----------------------*) -Goal "[| (0::real) < a; 0 < n; \ -\ isLub (UNIV::real set) \ -\ {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a"; -by (ftac lemma_nth_realpow_isLub_le 1 THEN Step_tac 1); -by (rtac (LIMSEQ_inverse_real_of_nat_add_minus_mult RS LIMSEQ_pow - RS LIMSEQ_le_const2) 1); -by (auto_tac (claset(),simpset() addsimps [real_of_nat_def,real_of_posnat_Suc])); -qed "realpow_nth_le"; - -(*----------- The theorem at last! -----------*) -Goal "[| (0::real) < a; 0 < n |] ==> EX r. r ^ n = a"; -by (ftac nth_realpow_isLub_ex 1 THEN Auto_tac); -by (auto_tac (claset() addIs [realpow_nth_le, - realpow_nth_ge,real_le_anti_sym],simpset())); -qed "realpow_nth"; - -(* positive only *) -Goal "[| (0::real) < a; 0 < n |] ==> EX r. 0 < r & r ^ n = a"; -by (ftac nth_realpow_isLub_ex 1 THEN Auto_tac); -by (auto_tac (claset() addIs [realpow_nth_le, - realpow_nth_ge,real_le_anti_sym, - lemma_nth_realpow_isLub_gt_zero],simpset())); -qed "realpow_pos_nth"; - -Goal "(0::real) < a ==> EX r. 0 < r & r ^ Suc n = a"; -by (blast_tac (claset() addIs [realpow_pos_nth]) 1); -qed "realpow_pos_nth2"; - -(* uniqueness of nth positive root *) -Goal "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a"; -by (auto_tac (claset() addSIs [realpow_pos_nth],simpset())); -by (cut_inst_tac [("x","r"),("y","y")] linorder_less_linear 1); -by (Auto_tac); -by (dres_inst_tac [("x","r")] realpow_less 1); -by (dres_inst_tac [("x","y")] realpow_less 4); -by (auto_tac (claset(),simpset() addsimps [real_less_not_refl])); -qed "realpow_pos_nth_unique"; - diff -r 27724f528f82 -r c9c6832f9b22 src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Tue Dec 23 16:53:33 2003 +0100 +++ b/src/HOL/Hyperreal/NthRoot.thy Tue Dec 23 17:41:52 2003 +0100 @@ -5,4 +5,171 @@ http://www.math.unl.edu/~webnotes *) -NthRoot = SEQ + HSeries +header{*Existence of Nth Root*} + +theory NthRoot = SEQ + HSeries: + +text{*Various lemmas needed for this result. We follow the proof + given by John Lindsay Orr (jorr@math.unl.edu) in his Analysis + Webnotes available on the www at http://www.math.unl.edu/~webnotes + Lemmas about sequences of reals are used to reach the result.*} + +lemma lemma_nth_realpow_non_empty: + "[| (0::real) < a; 0 < n |] ==> \s. s : {x. x ^ n <= a & 0 < x}" +apply (case_tac "1 <= a") +apply (rule_tac x = "1" in exI) +apply (drule_tac [2] not_real_leE) +apply (drule_tac [2] less_not_refl2 [THEN not0_implies_Suc]) +apply (auto intro!: realpow_Suc_le_self simp add: real_zero_less_one) +done + +lemma lemma_nth_realpow_isUb_ex: + "[| (0::real) < a; 0 < n |] + ==> \u. isUb (UNIV::real set) {x. x ^ n <= a & 0 < x} u" +apply (case_tac "1 <= a") +apply (rule_tac x = "a" in exI) +apply (drule_tac [2] not_real_leE) +apply (rule_tac [2] x = "1" in exI) +apply (rule_tac [!] setleI [THEN isUbI]) +apply safe +apply (simp_all (no_asm)) +apply (rule_tac [!] ccontr) +apply (drule_tac [!] not_real_leE) +apply (drule realpow_ge_self2 , assumption) +apply (drule_tac n = "n" in realpow_less) +apply (assumption+) +apply (drule real_le_trans , assumption) +apply (drule_tac y = "y ^ n" in order_less_le_trans) +apply (assumption , erule real_less_irrefl) +apply (drule_tac n = "n" in real_zero_less_one [THEN realpow_less]) +apply auto +done + +lemma nth_realpow_isLub_ex: + "[| (0::real) < a; 0 < n |] + ==> \u. isLub (UNIV::real set) {x. x ^ n <= a & 0 < x} u" +apply (blast intro: lemma_nth_realpow_isUb_ex lemma_nth_realpow_non_empty reals_complete) +done + +subsection{*First Half -- Lemmas First*} + +lemma lemma_nth_realpow_seq: + "isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u + ==> u + inverse(real (Suc k)) ~: {x. x ^ n <= a & 0 < x}" +apply (safe , drule isLubD2 , blast) +apply (simp add: real_le_def) +done + +lemma lemma_nth_realpow_isLub_gt_zero: + "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; + 0 < a; 0 < n |] ==> 0 < u" +apply (drule lemma_nth_realpow_non_empty , auto) +apply (drule_tac y = "s" in isLub_isUb [THEN isUbD]) +apply (auto intro: order_less_le_trans) +done + +lemma lemma_nth_realpow_isLub_ge: + "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; + 0 < a; 0 < n |] ==> ALL k. a <= (u + inverse(real (Suc k))) ^ n" +apply (safe) +apply (frule lemma_nth_realpow_seq , safe) +apply (auto elim: real_less_asym simp add: real_le_def) +apply (simp add: real_le_def [symmetric]) +apply (rule order_less_trans [of _ 0]) +apply (auto intro: real_inv_real_of_posnat_gt_zero lemma_nth_realpow_isLub_gt_zero) +done + +text{*First result we want*} +lemma realpow_nth_ge: + "[| (0::real) < a; 0 < n; + isLub (UNIV::real set) + {x. x ^ n <= a & 0 < x} u |] ==> a <= u ^ n" +apply (frule lemma_nth_realpow_isLub_ge , safe) +apply (rule LIMSEQ_inverse_real_of_nat_add [THEN LIMSEQ_pow, THEN LIMSEQ_le_const]) +apply (auto simp add: real_of_nat_def real_of_posnat_Suc) +done + +subsection{*Second Half*} + +lemma less_isLub_not_isUb: + "[| isLub (UNIV::real set) S u; x < u |] + ==> ~ isUb (UNIV::real set) S x" +apply (safe) +apply (drule isLub_le_isUb) +apply assumption +apply (drule order_less_le_trans) +apply (auto simp add: real_less_not_refl) +done + +lemma not_isUb_less_ex: + "~ isUb (UNIV::real set) S u ==> \x \ S. u < x" +apply (rule ccontr , erule swap) +apply (rule setleI [THEN isUbI]) +apply (auto simp add: real_le_def) +done + +lemma lemma_nth_realpow_isLub_le: + "[| isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u; + 0 < a; 0 < n |] ==> ALL k. (u*(1 + -inverse(real_of_posnat k))) ^ n <= a" +apply (safe) +apply (frule less_isLub_not_isUb [THEN not_isUb_less_ex]) +apply (rule_tac n = "k" in real_mult_less_self) +apply (blast intro: lemma_nth_realpow_isLub_gt_zero) +apply (safe) +apply (drule_tac n = "k" in lemma_nth_realpow_isLub_gt_zero [THEN real_mult_add_one_minus_ge_zero]) +apply (drule_tac [3] conjI [THEN realpow_le2]) +apply (rule_tac [3] order_less_imp_le) +apply (auto intro: order_trans) +done + +text{*Second result we want*} +lemma realpow_nth_le: + "[| (0::real) < a; 0 < n; + isLub (UNIV::real set) + {x. x ^ n <= a & 0 < x} u |] ==> u ^ n <= a" +apply (frule lemma_nth_realpow_isLub_le , safe) +apply (rule LIMSEQ_inverse_real_of_nat_add_minus_mult [THEN LIMSEQ_pow, THEN LIMSEQ_le_const2]) +apply (auto simp add: real_of_nat_def real_of_posnat_Suc) +done + +(*----------- The theorem at last! -----------*) +lemma realpow_nth: "[| (0::real) < a; 0 < n |] ==> \r. r ^ n = a" +apply (frule nth_realpow_isLub_ex , auto) +apply (auto intro: realpow_nth_le realpow_nth_ge real_le_anti_sym) +done + +(* positive only *) +lemma realpow_pos_nth: "[| (0::real) < a; 0 < n |] ==> \r. 0 < r & r ^ n = a" +apply (frule nth_realpow_isLub_ex , auto) +apply (auto intro: realpow_nth_le realpow_nth_ge real_le_anti_sym lemma_nth_realpow_isLub_gt_zero) +done + +lemma realpow_pos_nth2: "(0::real) < a ==> \r. 0 < r & r ^ Suc n = a" +apply (blast intro: realpow_pos_nth) +done + +(* uniqueness of nth positive root *) +lemma realpow_pos_nth_unique: + "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a" +apply (auto intro!: realpow_pos_nth) +apply (cut_tac x = "r" and y = "y" in linorder_less_linear) +apply auto +apply (drule_tac x = "r" in realpow_less) +apply (drule_tac [4] x = "y" in realpow_less) +apply (auto simp add: real_less_not_refl) +done + +ML +{* +val nth_realpow_isLub_ex = thm"nth_realpow_isLub_ex"; +val realpow_nth_ge = thm"realpow_nth_ge"; +val less_isLub_not_isUb = thm"less_isLub_not_isUb"; +val not_isUb_less_ex = thm"not_isUb_less_ex"; +val realpow_nth_le = thm"realpow_nth_le"; +val realpow_nth = thm"realpow_nth"; +val realpow_pos_nth = thm"realpow_pos_nth"; +val realpow_pos_nth2 = thm"realpow_pos_nth2"; +val realpow_pos_nth_unique = thm"realpow_pos_nth_unique"; +*} + +end diff -r 27724f528f82 -r c9c6832f9b22 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 23 16:53:33 2003 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 23 17:41:52 2003 +0100 @@ -158,8 +158,7 @@ Hyperreal/Lim.ML Hyperreal/Lim.thy Hyperreal/Log.ML Hyperreal/Log.thy\ Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\ Hyperreal/NatStar.ML Hyperreal/NatStar.thy\ - Hyperreal/NSA.ML Hyperreal/NSA.thy\ - Hyperreal/NthRoot.ML Hyperreal/NthRoot.thy\ + Hyperreal/NSA.ML Hyperreal/NSA.thy Hyperreal/NthRoot.thy\ Hyperreal/Poly.ML Hyperreal/Poly.thy\ Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\ Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\