# HG changeset patch # User paulson # Date 1072200256 -3600 # Node ID 94ac3895822f9b9a099c99827918115bad91e96b # Parent c9c6832f9b22b1a60dbb58a3b782bccf86b25a80 removing real_of_posnat diff -r c9c6832f9b22 -r 94ac3895822f src/HOL/Hyperreal/NthRoot.thy --- a/src/HOL/Hyperreal/NthRoot.thy Tue Dec 23 17:41:52 2003 +0100 +++ b/src/HOL/Hyperreal/NthRoot.thy Tue Dec 23 18:24:16 2003 +0100 @@ -76,7 +76,7 @@ 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) +apply (auto intro: lemma_nth_realpow_isLub_gt_zero) done text{*First result we want*} @@ -108,9 +108,21 @@ apply (auto simp add: real_le_def) done +lemma real_mult_less_self: "0 < r ==> r * (1 + -inverse(real (Suc n))) < r" +apply (simp (no_asm) add: real_add_mult_distrib2) +apply (rule_tac C = "-r" in real_less_add_left_cancel) +apply (auto intro: real_mult_order simp add: real_add_assoc [symmetric] real_minus_zero_less_iff2) +done + +lemma real_mult_add_one_minus_ge_zero: + "0 < r ==> 0 <= r*(1 + -inverse(real (Suc n)))" +apply (simp add: zero_le_mult_iff real_of_nat_inverse_le_iff) +apply (simp add: RealOrd.real_of_nat_Suc) +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" + 0 < a; 0 < n |] ==> ALL k. (u*(1 + -inverse(real (Suc 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) diff -r c9c6832f9b22 -r 94ac3895822f src/HOL/Real/RealOrd.thy --- a/src/HOL/Real/RealOrd.thy Tue Dec 23 17:41:52 2003 +0100 +++ b/src/HOL/Real/RealOrd.thy Tue Dec 23 18:24:16 2003 +0100 @@ -521,119 +521,12 @@ by (simp add: neg_nat real_of_nat_zero) -subsection{*Results About @{term real_of_posnat}: to be Deleted*} - -lemma real_of_posnat_gt_zero: "0 < real_of_posnat n" -apply (unfold real_of_posnat_def) -apply (rule real_gt_zero_preal_Ex [THEN iffD2], blast) -done - -declare real_of_posnat_gt_zero [simp] - -lemmas real_inv_real_of_posnat_gt_zero = real_of_posnat_gt_zero [THEN real_inverse_gt_0, standard] -declare real_inv_real_of_posnat_gt_zero [simp] - -lemmas real_of_posnat_ge_zero = real_of_posnat_gt_zero [THEN order_less_imp_le, standard] -declare real_of_posnat_ge_zero [simp] - -lemma real_of_posnat_not_eq_zero: "real_of_posnat n ~= 0" -by (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym]) -declare real_of_posnat_not_eq_zero [simp] - -declare real_of_posnat_not_eq_zero [THEN real_mult_inv_left, simp] -declare real_of_posnat_not_eq_zero [THEN real_mult_inv_right, simp] - -lemma real_of_posnat_ge_one: "1 <= real_of_posnat n" -apply (simp (no_asm) add: real_of_posnat_one [symmetric]) -apply (induct_tac "n", simp) -apply (simp add: real_of_posnat_Suc real_of_posnat_one order_less_imp_le) -apply (rule add_le_cancel_right [THEN iffD1, of _ "- 1"]) -apply (simp add: add_assoc) -done -declare real_of_posnat_ge_one [simp] - -lemma real_of_posnat_real_inv_not_zero: "inverse(real_of_posnat n) ~= 0" -apply (rule real_inverse_not_zero) -apply (rule real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym]) -done -declare real_of_posnat_real_inv_not_zero [simp] - -lemma real_of_posnat_real_inv_inj: "inverse(real_of_posnat x) = inverse(real_of_posnat y) ==> x = y" -apply (rule inj_real_of_posnat [THEN injD]) -apply (rule real_of_posnat_real_inv_not_zero - [THEN real_mult_left_cancel, THEN iffD1, of x]) -apply (simp add: real_mult_inv_left - real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym]) -done - -lemma real_mult_less_self: "0 < r ==> r*(1 + -inverse(real_of_posnat n)) < r" -apply (simp (no_asm) add: real_add_mult_distrib2) -apply (rule_tac C = "-r" in real_less_add_left_cancel) -apply (auto intro: real_mult_order simp add: real_add_assoc [symmetric] real_minus_zero_less_iff2) -done - -lemma real_of_posnat_inv_Ex_iff: "(EX n. inverse(real_of_posnat n) < r) = (EX n. 1 < r * real_of_posnat n)" -apply safe -apply (drule_tac n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_mono1]) -apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1]) -apply (auto simp add: real_of_posnat_gt_zero [THEN real_not_refl2, THEN not_sym] real_mult_assoc) -done - -lemma real_of_posnat_inv_iff: "(inverse(real_of_posnat n) < r) = (1 < r * real_of_posnat n)" -apply safe -apply (drule_tac n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_mono1]) -apply (drule_tac [2] n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_mono1]) -apply (auto simp add: real_mult_assoc) -done - lemma real_mult_le_le_mono1: "[| (0::real) <=z; x<=y |] ==> z*x<=z*y" by (rule Ring_and_Field.mult_left_mono) lemma real_mult_le_le_mono2: "[| (0::real)<=z; x<=y |] ==> x*z<=y*z" by (rule Ring_and_Field.mult_right_mono) -lemma real_of_posnat_inv_le_iff: "(inverse(real_of_posnat n) <= r) = (1 <= r * real_of_posnat n)" -apply safe -apply (drule_tac n2=n in real_of_posnat_gt_zero [THEN order_less_imp_le, THEN real_mult_le_le_mono1]) -apply (drule_tac [2] n3=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN order_less_imp_le, THEN real_mult_le_le_mono1]) -apply (auto simp add: real_mult_ac) -done - -lemma real_of_posnat_less_iff: - "(real_of_posnat n < real_of_posnat m) = (n < m)" -apply (unfold real_of_posnat_def, auto) -done -declare real_of_posnat_less_iff [simp] - -lemma real_of_posnat_le_iff: "(real_of_posnat n <= real_of_posnat m) = (n <= m)" -by (auto dest: inj_real_of_posnat [THEN injD] simp add: real_le_less le_eq_less_or_eq) -declare real_of_posnat_le_iff [simp] - -lemma real_mult_less_cancel3: "[| (0::real) x x (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse(u))" -apply safe -apply (rule_tac n2=n in real_of_posnat_gt_zero [THEN real_inverse_gt_0, THEN real_mult_less_cancel3]) -apply (rule_tac [2] x1 = u in real_inverse_gt_0 [THEN real_mult_less_cancel3]) -apply (auto simp add: real_not_refl2 [THEN not_sym]) -apply (rule_tac z = u in real_mult_less_cancel4) -apply (rule_tac [3] n1 = n in real_of_posnat_gt_zero [THEN real_mult_less_cancel4]) -apply (auto simp add: real_not_refl2 [THEN not_sym] real_mult_assoc [symmetric]) -done - -lemma real_of_posnat_inv_eq_iff: "0 < u ==> (u = inverse(real_of_posnat n)) = (real_of_posnat n = inverse u)" -by auto - -lemma real_add_one_minus_inv_ge_zero: "0 <= 1 + -inverse(real_of_posnat n)" -apply (rule_tac C = "inverse (real_of_posnat n) " in real_le_add_right_cancel) -apply (simp (no_asm) add: real_add_assoc real_of_posnat_inv_le_iff) -done - (*Used just below and in HahnBanach/Aux.thy*) lemma real_mult_le_less_mono1: "[| (0::real) \ z; x < y |] ==> x*z \ y*z" apply (rule real_less_or_eq_imp_le) @@ -641,9 +534,6 @@ apply (auto intro: real_mult_less_mono1) done -lemma real_mult_add_one_minus_ge_zero: "0 < r ==> 0 <= r*(1 + -inverse(real_of_posnat n))" -by (drule real_add_one_minus_inv_ge_zero [THEN real_mult_le_less_mono1], auto) - lemma real_inverse_unique: "x*y = (1::real) ==> y = inverse x" apply (case_tac "x ~= 0") apply (rule_tac c1 = x in real_mult_left_cancel [THEN iffD1], auto) @@ -857,25 +747,8 @@ val real_of_nat_zero_iff = thm "real_of_nat_zero_iff"; val real_of_nat_neg_int = thm "real_of_nat_neg_int"; -val real_of_posnat_gt_zero = thm "real_of_posnat_gt_zero"; -val real_inv_real_of_posnat_gt_zero = thm "real_inv_real_of_posnat_gt_zero"; -val real_of_posnat_ge_zero = thm "real_of_posnat_ge_zero"; -val real_of_posnat_not_eq_zero = thm "real_of_posnat_not_eq_zero"; -val real_of_posnat_ge_one = thm "real_of_posnat_ge_one"; -val real_of_posnat_real_inv_not_zero = thm "real_of_posnat_real_inv_not_zero"; -val real_of_posnat_real_inv_inj = thm "real_of_posnat_real_inv_inj"; -val real_mult_less_self = thm "real_mult_less_self"; -val real_of_posnat_inv_Ex_iff = thm "real_of_posnat_inv_Ex_iff"; -val real_of_posnat_inv_iff = thm "real_of_posnat_inv_iff"; val real_mult_le_le_mono1 = thm "real_mult_le_le_mono1"; val real_mult_le_le_mono2 = thm "real_mult_le_le_mono2"; -val real_of_posnat_inv_le_iff = thm "real_of_posnat_inv_le_iff"; -val real_of_posnat_less_iff = thm "real_of_posnat_less_iff"; -val real_of_posnat_le_iff = thm "real_of_posnat_le_iff"; -val real_of_posnat_less_inv_iff = thm "real_of_posnat_less_inv_iff"; -val real_of_posnat_inv_eq_iff = thm "real_of_posnat_inv_eq_iff"; -val real_add_one_minus_inv_ge_zero = thm "real_add_one_minus_inv_ge_zero"; -val real_mult_add_one_minus_ge_zero = thm "real_mult_add_one_minus_ge_zero"; val real_inverse_unique = thm "real_inverse_unique"; val real_inverse_gt_one = thm "real_inverse_gt_one"; val real_of_nat_gt_zero_cancel_iff = thm "real_of_nat_gt_zero_cancel_iff";