--- a/src/HOL/Real/Hyperreal/HRealAbs.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HRealAbs.ML Fri Dec 15 17:41:38 2000 +0100
@@ -94,37 +94,15 @@
hypreal_mult,abs_mult]));
qed "hrabs_mult";
-Goal "x~= (0::hypreal) ==> abs(inverse(x)) = inverse(abs(x))";
+Goal "abs(inverse(x)) = inverse(abs(x::hypreal))";
+by (hypreal_div_undefined_case_tac "x=0" 1);
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_hrabs,
- hypreal_inverse,hypreal_zero_def]));
-by (ultra_tac (claset(),simpset() addsimps [abs_inverse]) 1);
-by (arith_tac 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_hrabs,
+ hypreal_inverse,hypreal_zero_def]));
+by (ultra_tac (claset(), simpset() addsimps [abs_inverse]) 1);
qed "hrabs_inverse";
-(* old version of proof:
-Goalw [hrabs_def]
- "x~= (0::hypreal) ==> abs(inverse(x)) = inverse(abs(x))";
-by (auto_tac (claset(),simpset() addsimps [hypreal_minus_inverse]));
-by (ALLGOALS(dtac not_hypreal_leE));
-by (etac hypreal_less_asym 1);
-by (blast_tac (claset() addDs [hypreal_le_imp_less_or_eq,
- hypreal_inverse_gt_zero]) 1);
-by (dtac (hreal_inverse_not_zero RS not_sym) 1);
-by (rtac (hypreal_inverse_less_zero RSN (2,hypreal_less_asym)) 1);
-by (assume_tac 2);
-by (blast_tac (claset() addSDs [hypreal_le_imp_less_or_eq]) 1);
-qed "hrabs_inverse";
-*)
-
-val [prem] = goal thy "y ~= (0::hypreal) ==> \
-\ abs(x*inverse(y)) = abs(x)*inverse(abs(y))";
-by (res_inst_tac [("c1","abs y")] (hypreal_mult_left_cancel RS subst) 1);
-by (simp_tac (simpset() addsimps [(hrabs_not_zero_iff RS sym), prem]) 1);
-by (simp_tac (simpset() addsimps [(hrabs_mult RS sym), prem,
- hrabs_not_zero_iff RS sym] @ hypreal_mult_ac) 1);
-qed "hrabs_mult_inverse";
-
Goal "abs(x+(y::hypreal)) <= abs x + abs y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
--- a/src/HOL/Real/Hyperreal/HyperDef.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML Fri Dec 15 17:41:38 2000 +0100
@@ -88,7 +88,7 @@
Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat";
by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1);
by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1);
-by (auto_tac (claset(),simpset() addsimps [UNIV_diff_Compl]));
+by (auto_tac (claset(), simpset() addsimps [UNIV_diff_Compl]));
qed "FreeUltrafilterNat_Compl_mem";
Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)";
@@ -129,7 +129,7 @@
qed "FreeUltrafilterNat_Ex_P";
Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat";
-by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set],simpset()));
+by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set], simpset()));
qed "FreeUltrafilterNat_all";
(*-------------------------------------------------------
@@ -181,8 +181,8 @@
AddSEs [hyprelE];
Goalw [hyprel_def] "(x,x): hyprel";
-by (auto_tac (claset(),simpset() addsimps
- [FreeUltrafilterNat_Nat_set]));
+by (auto_tac (claset(),
+ simpset() addsimps [FreeUltrafilterNat_Nat_set]));
qed "hyprel_refl";
Goal "{n. X n = Y n} = {n. Y n = X n}";
@@ -190,7 +190,7 @@
qed "lemma_perm";
Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel";
-by (auto_tac (claset() addIs [lemma_perm RS subst],simpset()));
+by (auto_tac (claset() addIs [lemma_perm RS subst], simpset()));
qed_spec_mp "hyprel_sym";
Goalw [hyprel_def]
@@ -232,7 +232,7 @@
Goalw [hyprel_def] "x: hyprel ^^ {x}";
by (Step_tac 1);
-by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
+by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
qed "lemma_hyprel_refl";
Addsimps [lemma_hyprel_refl];
@@ -284,11 +284,11 @@
qed "hypreal_minus_congruent";
Goalw [hypreal_minus_def]
- "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
+ "- (Abs_hypreal(hyprel^^{%n. X n})) = Abs_hypreal(hyprel ^^ {%n. -(X n)})";
by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
by (simp_tac (simpset() addsimps
- [hyprel_in_hypreal RS Abs_hypreal_inverse,
- [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1);
+ [hyprel_in_hypreal RS Abs_hypreal_inverse,
+ [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1);
qed "hypreal_minus";
Goal "- (- z) = (z::hypreal)";
@@ -307,48 +307,17 @@
Goalw [hypreal_zero_def] "-0 = (0::hypreal)";
by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
qed "hypreal_minus_zero";
-
Addsimps [hypreal_minus_zero];
Goal "(-x = 0) = (x = (0::hypreal))";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_zero_def,
- hypreal_minus] @ real_add_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_zero_def, hypreal_minus, eq_commute] @
+ real_add_ac));
qed "hypreal_minus_zero_iff";
Addsimps [hypreal_minus_zero_iff];
-(**** multiplicative inverse on hypreal ****)
-Goalw [congruent_def]
- "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})";
-by (Auto_tac THEN Ultra_tac 1);
-qed "hypreal_inverse_congruent";
-
-Goalw [hypreal_inverse_def]
- "inverse (Abs_hypreal(hyprel^^{%n. X n})) = \
-\ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else inverse(X n)})";
-by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
-by (simp_tac (simpset() addsimps
- [hyprel_in_hypreal RS Abs_hypreal_inverse,
- [equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1);
-qed "hypreal_inverse";
-
-Goal "z ~= 0 ==> inverse (inverse (z::hypreal)) = z";
-by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
-by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps
- [hypreal_inverse,hypreal_zero_def] addsplits [split_if]) 1);
-by (ultra_tac (claset() addDs (map rename_numerals [real_inverse_not_zero]),
- simpset() addsimps [real_inverse_inverse]) 1);
-qed "hypreal_inverse_inverse";
-
-Addsimps [hypreal_inverse_inverse];
-
-Goalw [hypreal_one_def] "inverse(1hr) = 1hr";
-by (full_simp_tac (simpset() addsimps [hypreal_inverse,
- real_zero_not_eq_one RS not_sym]) 1);
-qed "hypreal_inverse_1";
-Addsimps [hypreal_inverse_1];
(**** hyperreal addition: hypreal_add ****)
@@ -417,14 +386,14 @@
qed "hypreal_minus_ex";
Goal "EX! y. (x::hypreal) + y = 0";
-by (auto_tac (claset() addIs [hypreal_add_minus],simpset()));
+by (auto_tac (claset() addIs [hypreal_add_minus], simpset()));
by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
qed "hypreal_minus_ex1";
Goal "EX! y. y + (x::hypreal) = 0";
-by (auto_tac (claset() addIs [hypreal_add_minus_left],simpset()));
+by (auto_tac (claset() addIs [hypreal_add_minus_left], simpset()));
by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
@@ -572,8 +541,7 @@
qed "hypreal_mult_0";
Goal "z * 0 = (0::hypreal)";
-by (simp_tac (simpset() addsimps [hypreal_mult_commute,
- hypreal_mult_0]) 1);
+by (simp_tac (simpset() addsimps [hypreal_mult_commute, hypreal_mult_0]) 1);
qed "hypreal_mult_0_right";
Addsimps [hypreal_mult_0,hypreal_mult_0_right];
@@ -589,8 +557,7 @@
Goal "-(x * y) = (x::hypreal) * -y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_minus,
- hypreal_mult]
+by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_mult]
@ real_mult_ac @ real_add_ac));
qed "hypreal_minus_mult_eq2";
@@ -642,16 +609,62 @@
(*** one and zero are distinct ***)
Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= 1hr";
-by (auto_tac (claset(),simpset() addsimps [real_zero_not_eq_one]));
+by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one]));
qed "hypreal_zero_not_eq_one";
+
+(**** multiplicative inverse on hypreal ****)
+
+Goalw [congruent_def]
+ "congruent hyprel (%X. hyprel^^{%n. if X n = #0 then #0 else inverse(X n)})";
+by (Auto_tac THEN Ultra_tac 1);
+qed "hypreal_inverse_congruent";
+
+Goalw [hypreal_inverse_def]
+ "inverse (Abs_hypreal(hyprel^^{%n. X n})) = \
+\ Abs_hypreal(hyprel ^^ {%n. if X n = #0 then #0 else inverse(X n)})";
+by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
+by (simp_tac (simpset() addsimps
+ [hyprel_in_hypreal RS Abs_hypreal_inverse,
+ [equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1);
+qed "hypreal_inverse";
+
+Goal "inverse 0 = (0::hypreal)";
+by (simp_tac (simpset() addsimps [hypreal_inverse, hypreal_zero_def]) 1);
+qed "HYPREAL_INVERSE_ZERO";
+
+Goal "a / (0::hypreal) = 0";
+by (simp_tac
+ (simpset() addsimps [hypreal_divide_def, HYPREAL_INVERSE_ZERO]) 1);
+qed "HYPREAL_DIVISION_BY_ZERO"; (*NOT for adding to default simpset*)
+
+fun hypreal_div_undefined_case_tac s i =
+ case_tac s i THEN
+ asm_simp_tac
+ (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO, HYPREAL_INVERSE_ZERO]) i;
+
+Goal "inverse (inverse (z::hypreal)) = z";
+by (hypreal_div_undefined_case_tac "z=0" 1);
+by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [hypreal_inverse, hypreal_zero_def]) 1);
+qed "hypreal_inverse_inverse";
+Addsimps [hypreal_inverse_inverse];
+
+Goalw [hypreal_one_def] "inverse(1hr) = 1hr";
+by (full_simp_tac (simpset() addsimps [hypreal_inverse,
+ real_zero_not_eq_one RS not_sym]) 1);
+qed "hypreal_inverse_1";
+Addsimps [hypreal_inverse_1];
+
+
(*** existence of inverse ***)
+
Goalw [hypreal_one_def,hypreal_zero_def]
- "x ~= 0 ==> x*inverse(x) = 1hr";
+ "x ~= 0 ==> x*inverse(x) = 1hr";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse,
- hypreal_mult] addsplits [split_if]) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
by (dtac FreeUltrafilterNat_Compl_mem 1);
by (blast_tac (claset() addSIs [real_mult_inv_right,
FreeUltrafilterNat_subset]) 1);
@@ -662,43 +675,6 @@
hypreal_mult_commute]) 1);
qed "hypreal_mult_inverse_left";
-Goal "x ~= 0 ==> EX y. x * y = 1hr";
-by (fast_tac (claset() addDs [hypreal_mult_inverse]) 1);
-qed "hypreal_inverse_ex";
-
-Goal "x ~= 0 ==> EX y. y * x = 1hr";
-by (fast_tac (claset() addDs [hypreal_mult_inverse_left]) 1);
-qed "hypreal_inverse_left_ex";
-
-Goal "x ~= 0 ==> EX! y. x * y = 1hr";
-by (auto_tac (claset() addIs [hypreal_mult_inverse],simpset()));
-by (dres_inst_tac [("f","%x. ya*x")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
-qed "hypreal_inverse_ex1";
-
-Goal "x ~= 0 ==> EX! y. y * x = 1hr";
-by (auto_tac (claset() addIs [hypreal_mult_inverse_left],simpset()));
-by (dres_inst_tac [("f","%x. x*ya")] arg_cong 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc]) 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
-qed "hypreal_inverse_left_ex1";
-
-Goal "[| y~= 0; x * y = 1hr |] ==> x = inverse y";
-by (forw_inst_tac [("x","y")] hypreal_mult_inverse_left 1);
-by (res_inst_tac [("x1","y")] (hypreal_inverse_left_ex1 RS ex1E) 1);
-by (assume_tac 1);
-by (Blast_tac 1);
-qed "hypreal_mult_inv_inverse";
-
-Goal "x ~= 0 ==> EX y. x = inverse (y::hypreal)";
-by (forw_inst_tac [("x","x")] hypreal_inverse_left_ex 1);
-by (etac exE 1 THEN
- forw_inst_tac [("x","y")] hypreal_mult_inv_inverse 1);
-by (res_inst_tac [("x","y")] exI 2);
-by Auto_tac;
-qed "hypreal_as_inverse_ex";
-
Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)";
by Auto_tac;
by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
@@ -713,13 +689,7 @@
Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (rotate_tac 1 1);
-by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse,
- hypreal_mult] addsplits [split_if]) 1);
-by (dtac FreeUltrafilterNat_Compl_mem 1 THEN Clarify_tac 1);
-by (ultra_tac (claset() addIs [ccontr]
- addDs [rename_numerals real_inverse_not_zero],
- simpset()) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
qed "hypreal_inverse_not_zero";
Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left];
@@ -733,8 +703,8 @@
bind_thm ("hypreal_mult_not_0E",hypreal_mult_not_0 RS notE);
Goal "x*y = (0::hypreal) ==> x = 0 | y = 0";
-by (auto_tac (claset() addIs [ccontr] addDs
- [hypreal_mult_not_0],simpset()));
+by (auto_tac (claset() addIs [ccontr] addDs [hypreal_mult_not_0],
+ simpset()));
qed "hypreal_mult_zero_disj";
Goal "x ~= 0 ==> x * x ~= (0::hypreal)";
@@ -743,26 +713,30 @@
Goal "[| x ~= 0; y ~= 0 |] ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,
- hypreal_mult_not_0]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
by (res_inst_tac [("c1","y")] (hypreal_mult_right_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym,hypreal_mult_not_0]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_not_0] @ hypreal_mult_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_assoc RS sym, hypreal_mult_not_0]));
qed "inverse_mult_eq";
-Goal "x ~= 0 ==> inverse(-x) = -inverse(x::hypreal)";
+Goal "inverse(-x) = -inverse(x::hypreal)";
+by (hypreal_div_undefined_case_tac "x=0" 1);
by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
by (stac hypreal_mult_inverse_left 2);
by Auto_tac;
qed "hypreal_minus_inverse";
-Goal "[| x ~= 0; y ~= 0 |] \
-\ ==> inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
+by (hypreal_div_undefined_case_tac "x=0" 1);
+by (hypreal_div_undefined_case_tac "y=0" 1);
by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc RS sym]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_mult_assoc RS sym]));
by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_left_commute]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_commute]));
by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
qed "hypreal_inverse_distrib";
@@ -805,7 +779,7 @@
Goal "~ (R::hypreal) < R";
by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_less_def]));
by (Ultra_tac 1);
qed "hypreal_less_not_refl";
@@ -814,16 +788,15 @@
AddSEs [hypreal_less_irrefl];
Goal "!!(x::hypreal). x < y ==> x ~= y";
-by (auto_tac (claset(),simpset() addsimps [hypreal_less_not_refl]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_less_not_refl]));
qed "hypreal_not_refl2";
Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSIs [exI],simpset()
- addsimps [hypreal_less_def]));
-by (ultra_tac (claset() addIs [real_less_trans],simpset()) 1);
+by (auto_tac (claset() addSIs [exI], simpset() addsimps [hypreal_less_def]));
+by (ultra_tac (claset() addIs [real_less_trans], simpset()) 1);
qed "hypreal_less_trans";
Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
@@ -841,7 +814,7 @@
"(Abs_hypreal(hyprel^^{%n. X n}) < \
\ Abs_hypreal(hyprel^^{%n. Y n})) = \
\ ({n. X n < Y n} : FreeUltrafilterNat)";
-by (auto_tac (claset() addSIs [lemma_hyprel_refl],simpset()));
+by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset()));
by (Ultra_tac 1);
qed "hypreal_less";
@@ -881,7 +854,7 @@
Goalw [hyprel_def] "EX x. x: hyprel ^^ {%n. #0}";
by (res_inst_tac [("x","%n. #0")] exI 1);
by (Step_tac 1);
-by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set],simpset()));
+by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
qed "lemma_hyprel_0r_mem";
Goalw [hypreal_zero_def]"0 < x | x = 0 | x < (0::hypreal)";
@@ -1140,41 +1113,45 @@
by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
qed "hypreal_of_real_minus";
+(*DON'T insert this or the next one as default simprules.
+ They are used in both orientations and anyway aren't the ones we finally
+ need, which would use binary literals.*)
Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real #1 = 1hr";
by (Step_tac 1);
qed "hypreal_of_real_one";
-Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real #0 = 0";
+Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real #0 = 0";
by (Step_tac 1);
qed "hypreal_of_real_zero";
-Goal "(hypreal_of_real r = 0) = (r = #0)";
+Goal "(hypreal_of_real r = 0) = (r = #0)";
by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
simpset() addsimps [hypreal_of_real_def,
- hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
+ hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
qed "hypreal_of_real_zero_iff";
-Goal "(hypreal_of_real r ~= 0) = (r ~= #0)";
+(*FIXME: delete*)
+Goal "(hypreal_of_real r ~= 0) = (r ~= #0)";
by (full_simp_tac (simpset() addsimps [hypreal_of_real_zero_iff]) 1);
qed "hypreal_of_real_not_zero_iff";
-Goal "r ~= #0 ==> inverse (hypreal_of_real r) = \
-\ hypreal_of_real (inverse r)";
-by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1);
+Goal "inverse (hypreal_of_real r) = hypreal_of_real (inverse r)";
+by (case_tac "r=#0" 1);
+by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO,
+ HYPREAL_INVERSE_ZERO, hypreal_of_real_zero]) 1);
+by (res_inst_tac [("c1","hypreal_of_real r")]
+ (hypreal_mult_left_cancel RS iffD1) 1);
by (etac (hypreal_of_real_not_zero_iff RS iffD2) 1);
by (forward_tac [hypreal_of_real_not_zero_iff RS iffD2] 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_mult RS sym,hypreal_of_real_one]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_one, hypreal_of_real_mult RS sym]));
qed "hypreal_of_real_inverse";
-Goal "hypreal_of_real r ~= 0 ==> inverse (hypreal_of_real r) = \
-\ hypreal_of_real (inverse r)";
-by (etac (hypreal_of_real_not_zero_iff RS iffD1 RS hypreal_of_real_inverse) 1);
-qed "hypreal_of_real_inverse2";
-
Goal "x+x=x*(1hr+1hr)";
by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2]) 1);
qed "hypreal_add_self";
+(*FIXME: DELETE (used in Lim.ML) *)
Goal "(z::hypreal) ~= 0 ==> x*y = (x*inverse(z))*(z*y)";
by (asm_simp_tac (simpset() addsimps hypreal_mult_ac) 1);
qed "lemma_chain";
--- a/src/HOL/Real/Hyperreal/HyperOrd.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/HyperOrd.ML Fri Dec 15 17:41:38 2000 +0100
@@ -77,8 +77,7 @@
Goalw [hypreal_zero_def]
"((0::hypreal) < x) = (-x < x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_less,
- hypreal_minus]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_less, hypreal_minus]));
by (ALLGOALS(Ultra_tac));
qed "hypreal_gt_zero_iff";
@@ -86,8 +85,8 @@
by (res_inst_tac [("z","A")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","B")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","C")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addSIs [exI],simpset() addsimps
- [hypreal_less_def,hypreal_add]));
+by (auto_tac (claset() addSIs [exI],
+ simpset() addsimps [hypreal_less_def,hypreal_add]));
by (Ultra_tac 1);
qed "hypreal_add_less_mono1";
@@ -197,9 +196,9 @@
qed "hypreal_two_not_zero";
Addsimps [hypreal_two_not_zero];
-Goal "x*inverse(1hr + 1hr) + x*inverse(1hr + 1hr) = x";
+Goal "x/(1hr + 1hr) + x/(1hr + 1hr) = x";
by (stac hypreal_add_self 1);
-by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc,
+by (full_simp_tac (simpset() addsimps [hypreal_mult_assoc, hypreal_divide_def,
hypreal_two_not_zero RS hypreal_mult_inverse_left]) 1);
qed "hypreal_sum_of_halves";
@@ -397,9 +396,8 @@
by (ftac hypreal_not_refl2 1);
by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1);
by (rtac (hypreal_minus_zero_less_iff RS iffD1) 1);
-by (dtac (hypreal_minus_inverse RS sym) 1);
-by (auto_tac (claset() addIs [hypreal_inverse_gt_zero],
- simpset()));
+by (stac (hypreal_minus_inverse RS sym) 1);
+by (auto_tac (claset() addIs [hypreal_inverse_gt_zero], simpset()));
qed "hypreal_inverse_less_zero";
(* check why this does not work without 2nd substitution anymore! *)
@@ -426,7 +424,7 @@
Goal "!!(x::hypreal). x < y ==> EX r. x < r & r < y";
by (blast_tac (claset() addSIs [hypreal_less_half_sum,
- hypreal_gt_half_sum]) 1);
+ hypreal_gt_half_sum]) 1);
qed "hypreal_dense";
@@ -453,18 +451,18 @@
Goal "x * x ~= 0 ==> (0::hypreal) < x* x + y*y + z*z";
by (cut_inst_tac [("x1","x")] (hypreal_le_square
RS hypreal_le_imp_less_or_eq) 1);
-by (auto_tac (claset() addSIs
- [hypreal_add_order_le],simpset()));
+by (auto_tac (claset() addSIs [hypreal_add_order_le],
+ simpset()));
qed "hypreal_sum_squares3_gt_zero";
Goal "x * x ~= 0 ==> (0::hypreal) < y*y + x*x + z*z";
by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
+by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
qed "hypreal_sum_squares3_gt_zero2";
Goal "x * x ~= 0 ==> (0::hypreal) < y*y + z*z + x*x";
by (dtac hypreal_sum_squares3_gt_zero 1);
-by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
+by (auto_tac (claset(), simpset() addsimps hypreal_add_ac));
qed "hypreal_sum_squares3_gt_zero3";
@@ -480,28 +478,36 @@
Addsimps [hypreal_three_squares_add_zero_iff];
Addsimps [rename_numerals real_le_square];
+
Goal "(x::hypreal)*x <= x*x + y*y";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_mult,hypreal_add,hypreal_le]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult,hypreal_add,hypreal_le]));
qed "hypreal_self_le_add_pos";
Addsimps [hypreal_self_le_add_pos];
+(*lcp: new lemma unfortunately needed...*)
+Goal "-(x*x) <= (y*y::real)";
+by (rtac order_trans 1);
+by (rtac real_le_square 2);
+by Auto_tac;
+qed "minus_square_le_square";
+
Goal "(x::hypreal)*x <= x*x + y*y + z*z";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
by (auto_tac (claset(),
simpset() addsimps [hypreal_mult, hypreal_add, hypreal_le,
- rename_numerals real_le_add_order]));
+ minus_square_le_square]));
qed "hypreal_self_le_add_pos2";
Addsimps [hypreal_self_le_add_pos2];
-(*---------------------------------------------------------------------------------
+(*----------------------------------------------------------------------------
Embedding of the naturals in the hyperreals
- ---------------------------------------------------------------------------------*)
+ ----------------------------------------------------------------------------*)
Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 0 = 1hr";
by (full_simp_tac (simpset() addsimps
[pnat_one_iff RS sym,real_of_preal_def]) 1);
@@ -608,7 +614,7 @@
Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0";
by (auto_tac (claset(),
- simpset() addsimps [rename_numerals real_of_posnat_inverse_not_zero]));
+ simpset() addsimps [rename_numerals real_of_posnat_not_eq_zero]));
qed "hypreal_epsilon_not_zero";
Addsimps [rename_numerals real_of_posnat_not_eq_zero];
@@ -618,7 +624,7 @@
Goal "ehr = inverse(whr)";
by (asm_full_simp_tac (simpset() addsimps
- [hypreal_inverse,omega_def,epsilon_def]) 1);
+ [hypreal_inverse, omega_def, epsilon_def]) 1);
qed "hypreal_epsilon_inverse_omega";
(*----------------------------------------------------------------
@@ -631,7 +637,7 @@
Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr";
by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,
- hypreal_add_assoc]) 1);
+ hypreal_add_assoc]) 1);
qed "hypreal_of_nat_one";
Goalw [hypreal_of_nat_def]
@@ -687,10 +693,10 @@
by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1);
qed "hypreal_of_nat_Suc";
-Goal "0 < r ==> 0 < r*inverse(1hr+1hr)";
+Goal "0 < r ==> 0 < r/(1hr+1hr)";
by (dtac (hypreal_zero_less_two RS hypreal_inverse_gt_zero
RS hypreal_mult_less_mono1) 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [hypreal_divide_def]));
qed "hypreal_half_gt_zero";
(* this proof is so much simpler than one for reals!! *)
@@ -705,21 +711,19 @@
Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))";
by (auto_tac (claset() addIs [hypreal_inverse_less_swap],simpset()));
by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1);
-by (etac (hypreal_not_refl2 RS not_sym) 1);
by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1);
-by (etac (hypreal_not_refl2 RS not_sym) 1);
-by (auto_tac (claset() addIs [hypreal_inverse_less_swap],
- simpset() addsimps [hypreal_inverse_gt_zero]));
+by (rtac hypreal_inverse_less_swap 1);
+by (auto_tac (claset(), simpset() addsimps [hypreal_inverse_gt_zero]));
qed "hypreal_inverse_less_iff";
Goal "[| 0 < z; x < y |] ==> x * inverse z < y * inverse (z::hypreal)";
by (blast_tac (claset() addSIs [hypreal_mult_less_mono1,
- hypreal_inverse_gt_zero]) 1);
+ hypreal_inverse_gt_zero]) 1);
qed "hypreal_mult_inverse_less_mono1";
Goal "[| 0 < z; x < y |] ==> inverse z * x < inverse (z::hypreal) * y";
by (blast_tac (claset() addSIs [hypreal_mult_less_mono2,
- hypreal_inverse_gt_zero]) 1);
+ hypreal_inverse_gt_zero]) 1);
qed "hypreal_mult_inverse_less_mono2";
Goal "[| (0::hypreal) < z; x*z < y*z |] ==> x < y";
@@ -734,18 +738,14 @@
simpset() addsimps [hypreal_mult_commute]));
qed "hypreal_less_mult_left_cancel";
-Goal "[| 0 < r; (0::hypreal) < ra; \
-\ r < x; ra < y |] \
-\ ==> r*ra < x*y";
+Goal "[| 0 < r; (0::hypreal) < ra; r < x; ra < y |] ==> r*ra < x*y";
by (forw_inst_tac [("R2.0","r")] hypreal_less_trans 1);
by (dres_inst_tac [("z","ra"),("x","r")] hypreal_mult_less_mono1 2);
by (dres_inst_tac [("z","x"),("x","ra")] hypreal_mult_less_mono2 3);
by (auto_tac (claset() addIs [hypreal_less_trans],simpset()));
qed "hypreal_mult_less_gt_zero";
-Goal "[| 0 < r; (0::hypreal) < ra; \
-\ r <= x; ra <= y |] \
-\ ==> r*ra <= x*y";
+Goal "[| 0 < r; (0::hypreal) < ra; r <= x; ra <= y |] ==> r*ra <= x*y";
by (REPEAT(dtac hypreal_le_imp_less_or_eq 1));
by (rtac hypreal_less_or_eq_imp_le 1);
by (auto_tac (claset() addIs [hypreal_mult_less_mono1,
--- a/src/HOL/Real/Hyperreal/Lim.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML Fri Dec 15 17:41:38 2000 +0100
@@ -6,6 +6,7 @@
*)
+(*DELETE?????*)
fun ARITH_PROVE str = prove_goal thy str
(fn prems => [cut_facts_tac prems 1,arith_tac 1]);
@@ -25,7 +26,7 @@
qed "LIM_iff";
Goalw [LIM_def]
- "!!a. [| f -- a --> L; #0 < r |] \
+ "[| f -- a --> L; #0 < r |] \
\ ==> (EX s. #0 < s & (ALL x. (x ~= a \
\ & (abs(x + -a) < s) --> abs(f x + -L) < r)))";
by Auto_tac;
@@ -47,7 +48,7 @@
"[| f -- x --> l; g -- x --> m |] \
\ ==> (%x. f(x) + g(x)) -- x --> (l + m)";
by (Step_tac 1);
-by (REPEAT(dres_inst_tac [("x","r*inverse(#1 + #1)")] spec 1));
+by (REPEAT(dres_inst_tac [("x","r/#2")] spec 1));
by (dtac (rename_numerals (real_zero_less_two RS real_inverse_gt_zero
RSN (2,real_mult_less_mono2))) 1);
by (Asm_full_simp_tac 1);
@@ -130,7 +131,7 @@
(*-------------
LIM_mult_zero
-------------*)
-Goalw [LIM_def] "!!f. [| f -- x --> #0; g -- x --> #0 |] \
+Goalw [LIM_def] "[| f -- x --> #0; g -- x --> #0 |] \
\ ==> (%x. f(x)*g(x)) -- x --> #0";
by (Step_tac 1);
by (dres_inst_tac [("x","#1")] spec 1);
@@ -224,7 +225,7 @@
by (Blast_tac 1);
val lemma_skolemize_LIM2 = result();
-Goal "!!X. ALL n. X n ~= x & \
+Goal "ALL n. X n ~= x & \
\ abs (X n + - x) < inverse (real_of_posnat n) & \
\ r <= abs (f (X n) + - L) ==> \
\ ALL n. abs (X n + - x) < inverse (real_of_posnat n)";
@@ -236,7 +237,7 @@
-------------------*)
Goalw [LIM_def,NSLIM_def,inf_close_def]
- "!!f. f -- x --NS> L ==> f -- x --> L";
+ "f -- x --NS> L ==> f -- x --> L";
by (asm_full_simp_tac
(simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff]) 1);
by (EVERY1[Step_tac, rtac ccontr, Asm_full_simp_tac]);
@@ -337,12 +338,12 @@
(*----------------------------------------------
NSLIM_add_minus
----------------------------------------------*)
-Goal "!!f. [| f -- x --NS> l; g -- x --NS> m |] \
+Goal "[| f -- x --NS> l; g -- x --NS> m |] \
\ ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)";
by (blast_tac (claset() addDs [NSLIM_add,NSLIM_minus]) 1);
qed "NSLIM_add_minus";
-Goal "!!f. [| f -- x --> l; g -- x --> m |] \
+Goal "[| f -- x --> l; g -- x --> m |] \
\ ==> (%x. f(x) + -g(x)) -- x --> (l + -m)";
by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff,
NSLIM_add_minus]) 1);
@@ -352,18 +353,18 @@
NSLIM_inverse
-----------------------------*)
Goalw [NSLIM_def]
- "!!f. [| f -- a --NS> L; \
-\ L ~= #0 \
-\ |] ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
-by (Step_tac 1);
-by (dtac spec 1 THEN auto_tac (claset(),simpset()
- addsimps [hypreal_of_real_not_zero_iff RS sym,
- hypreal_of_real_inverse RS sym]));
-by (forward_tac [inf_close_hypreal_of_real_not_zero] 1
- THEN assume_tac 1);
-by (auto_tac (claset() addSEs [(starfun_inverse2 RS subst),
- inf_close_inverse,hypreal_of_real_HFinite_diff_Infinitesimal],
- simpset()));
+ "[| f -- a --NS> L; L ~= #0 |] \
+\ ==> (%x. inverse(f(x))) -- a --NS> (inverse L)";
+by (Clarify_tac 1);
+by (dtac spec 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_not_zero_iff RS sym,
+ hypreal_of_real_inverse RS sym]));
+by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
+by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
+by (stac (starfun_inverse RS sym) 1);
+by (auto_tac (claset() addSEs [inf_close_inverse],
+ simpset() addsimps [hypreal_of_real_zero_iff]));
qed "NSLIM_inverse";
Goal "[| f -- a --> L; \
@@ -485,18 +486,18 @@
---------------*)
Goalw [isNSCont_def]
- "!!f. [| isNSCont f a; y @= hypreal_of_real a |] \
+ "[| isNSCont f a; y @= hypreal_of_real a |] \
\ ==> (*f* f) y @= hypreal_of_real (f a)";
by (Blast_tac 1);
qed "isNSContD";
Goalw [isNSCont_def,NSLIM_def]
- "!!f. isNSCont f a ==> f -- a --NS> (f a) ";
+ "isNSCont f a ==> f -- a --NS> (f a) ";
by (Blast_tac 1);
qed "isNSCont_NSLIM";
Goalw [isNSCont_def,NSLIM_def]
- "!!f. f -- a --NS> (f a) ==> isNSCont f a";
+ "f -- a --NS> (f a) ==> isNSCont f a";
by (Auto_tac);
by (res_inst_tac [("Q","y = hypreal_of_real a")]
(excluded_middle RS disjE) 1);
@@ -531,14 +532,14 @@
(*----------------------------------------
Standard continuity ==> NS continuity
----------------------------------------*)
-Goal "!!f. isCont f a ==> isNSCont f a";
+Goal "isCont f a ==> isNSCont f a";
by (etac (isNSCont_isCont_iff RS iffD2) 1);
qed "isCont_isNSCont";
(*----------------------------------------
NS continuity ==> Standard continuity
----------------------------------------*)
-Goal "!!f. isNSCont f a ==> isCont f a";
+Goal "isNSCont f a ==> isCont f a";
by (etac (isNSCont_isCont_iff RS iffD1) 1);
qed "isNSCont_isCont";
@@ -587,7 +588,7 @@
(*------------------------
sum continuous
------------------------*)
-Goal "!!f. [| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
+Goal "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) + g(x)) a";
by (auto_tac (claset() addIs [starfun_add_inf_close],simpset() addsimps
[isNSCont_isCont_iff RS sym,isNSCont_def,hypreal_of_real_add]));
qed "isCont_add";
@@ -662,14 +663,14 @@
Addsimps [isCont_rabs];
(****************************************************************
-(* Leave as commented until I add topology theory or remove? *)
-(*------------------------------------------------------------
+(%* Leave as commented until I add topology theory or remove? *%)
+(%*------------------------------------------------------------
Elementary topology proof for a characterisation of
continuity now: a function f is continuous if and only
if the inverse image, {x. f(x) : A}, of any open set A
is always an open set
- ------------------------------------------------------------*)
-Goal "!!A. [| isNSopen A; ALL x. isNSCont f x |] \
+ ------------------------------------------------------------*%)
+Goal "[| isNSopen A; ALL x. isNSCont f x |] \
\ ==> isNSopen {x. f x : A}";
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
by (dtac (mem_monad_inf_close RS inf_close_sym) 1);
@@ -681,7 +682,7 @@
qed "isNSCont_isNSopen";
Goalw [isNSCont_def]
- "!!x. ALL A. isNSopen A --> isNSopen {x. f x : A} \
+ "ALL A. isNSopen A --> isNSopen {x. f x : A} \
\ ==> isNSCont f x";
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
(inf_close_minus_iff RS iffD2)],simpset() addsimps
@@ -700,7 +701,7 @@
isNSopen_isNSCont]) 1);
qed "isNSCont_isNSopen_iff";
-(*------- Standard version of same theorem --------*)
+(%*------- Standard version of same theorem --------*%)
Goal "(ALL x. isCont f x) = \
\ (ALL A. isopen A --> isopen {x. f(x) : A})";
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
@@ -741,7 +742,7 @@
by (Ultra_tac 1);
qed "isUCont_isNSUCont";
-Goal "!!x. ALL s. #0 < s --> \
+Goal "ALL s. #0 < s --> \
\ (EX xa y. abs (xa + - y) < s & \
\ r <= abs (f xa + -f y)) ==> \
\ ALL n::nat. EX xa y. \
@@ -752,7 +753,7 @@
by Auto_tac;
val lemma_LIMu = result();
-Goal "!!x. ALL s. #0 < s --> \
+Goal "ALL s. #0 < s --> \
\ (EX xa y. abs (xa + - y) < s & \
\ r <= abs (f xa + -f y)) ==> \
\ EX X Y. ALL n::nat. \
@@ -807,34 +808,34 @@
Derivatives
------------------------------------------------------------------*)
Goalw [deriv_def]
- "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --> D)";
+ "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --> D)";
by (Blast_tac 1);
qed "DERIV_iff";
Goalw [deriv_def]
- "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --NS> D)";
+ "(DERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --NS> D)";
by (simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
qed "DERIV_NS_iff";
Goalw [deriv_def]
"DERIV f x :> D \
-\ ==> (%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --> D";
+\ ==> (%h. (f(x + h) + - f(x))/h) -- #0 --> D";
by (Blast_tac 1);
qed "DERIVD";
Goalw [deriv_def] "DERIV f x :> D ==> \
-\ (%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --NS> D";
+\ (%h. (f(x + h) + - f(x))/h) -- #0 --NS> D";
by (asm_full_simp_tac (simpset() addsimps [LIM_NSLIM_iff]) 1);
qed "NS_DERIVD";
(* Uniqueness *)
Goalw [deriv_def]
- "!!f. [| DERIV f x :> D; DERIV f x :> E |] ==> D = E";
+ "[| DERIV f x :> D; DERIV f x :> E |] ==> D = E";
by (blast_tac (claset() addIs [LIM_unique]) 1);
qed "DERIV_unique";
Goalw [nsderiv_def]
- "!!f. [| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E";
+ "[| NSDERIV f x :> D; NSDERIV f x :> E |] ==> D = E";
by (cut_facts_tac [Infinitesimal_epsilon,
hypreal_epsilon_not_zero] 1);
by (auto_tac (claset() addSDs [bspec] addSIs
@@ -846,22 +847,22 @@
------------------------------------------------------------------------*)
Goalw [differentiable_def]
- "!!f. f differentiable x ==> EX D. DERIV f x :> D";
+ "f differentiable x ==> EX D. DERIV f x :> D";
by (assume_tac 1);
qed "differentiableD";
Goalw [differentiable_def]
- "!!f. DERIV f x :> D ==> f differentiable x";
+ "DERIV f x :> D ==> f differentiable x";
by (Blast_tac 1);
qed "differentiableI";
Goalw [NSdifferentiable_def]
- "!!f. f NSdifferentiable x ==> EX D. NSDERIV f x :> D";
+ "f NSdifferentiable x ==> EX D. NSDERIV f x :> D";
by (assume_tac 1);
qed "NSdifferentiableD";
Goalw [NSdifferentiable_def]
- "!!f. NSDERIV f x :> D ==> f NSdifferentiable x";
+ "NSDERIV f x :> D ==> f NSdifferentiable x";
by (Blast_tac 1);
qed "NSdifferentiableI";
@@ -870,8 +871,8 @@
-------------------------------------------------------*)
Goalw [LIM_def]
- "((%h. (f(a + h) + - f(a))*inverse(h)) -- #0 --> D) = \
-\ ((%x. (f(x) + -f(a))*inverse(x + -a)) -- a --> D)";
+ "((%h. (f(a + h) + - f(a))/h) -- #0 --> D) = \
+\ ((%x. (f(x) + -f(a)) / (x + -a)) -- a --> D)";
by (Step_tac 1);
by (ALLGOALS(dtac spec));
by (Step_tac 1);
@@ -880,12 +881,12 @@
by (Step_tac 1);
by (dres_inst_tac [("x","x + -a")] spec 1);
by (dres_inst_tac [("x","x + a")] spec 2);
-by (auto_tac (claset(),simpset() addsimps
- real_add_ac));
+by (auto_tac (claset(), simpset() addsimps real_add_ac));
+by (arith_tac 1);
qed "DERIV_LIM_iff";
Goalw [deriv_def] "(DERIV f x :> D) = \
-\ ((%z. (f(z) + -f(x))*inverse(z + -x)) -- x --> D)";
+\ ((%z. (f(z) + -f(x)) / (z + -x)) -- x --> D)";
by (simp_tac (simpset() addsimps [DERIV_LIM_iff]) 1);
qed "DERIV_iff2";
@@ -895,23 +896,26 @@
(*-------------------------------------------
First NSDERIV in terms of NSLIM
-------------------------------------------*)
+
+Addsimps [starfun_Id]; (*???????Star.ML?????*)
(*--- first equivalence ---*)
Goalw [nsderiv_def,NSLIM_def]
- "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))*inverse(h)) -- #0 --NS> D)";
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_zero]));
+ "(NSDERIV f x :> D) = ((%h. (f(x + h) + - f(x))/h) -- #0 --NS> D)";
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero]));
by (dres_inst_tac [("x","xa")] bspec 1);
by (rtac ccontr 3);
by (dres_inst_tac [("x","h")] spec 3);
-by (auto_tac (claset(),simpset() addsimps [mem_infmal_iff,
- starfun_mult RS sym,starfun_inverse_inverse,starfun_add RS sym,
- hypreal_of_real_minus,starfun_lambda_cancel]));
+by (auto_tac (claset(),
+ simpset() addsimps [mem_infmal_iff,
+ starfun_divide RS sym, starfun_add RS sym,
+ hypreal_of_real_minus, starfun_lambda_cancel]));
qed "NSDERIV_NSLIM_iff";
(*--- second equivalence ---*)
Goal "(NSDERIV f x :> D) = \
-\ ((%z. (f(z) + -f(x))*inverse(z + -x)) -- x --NS> D)";
+\ ((%z. (f(z) + -f(x)) / (z + -x)) -- x --NS> D)";
by (full_simp_tac (simpset() addsimps
- [NSDERIV_NSLIM_iff,DERIV_LIM_iff,LIM_NSLIM_iff RS sym]) 1);
+ [NSDERIV_NSLIM_iff, DERIV_LIM_iff, LIM_NSLIM_iff RS sym]) 1);
qed "NSDERIV_NSLIM_iff2";
(* while we're at it! *)
@@ -919,13 +923,28 @@
"(NSDERIV f x :> D) = \
\ (ALL xa. \
\ xa ~= hypreal_of_real x & xa @= hypreal_of_real x --> \
-\ (*f* (%z. (f z - f x) * inverse (z - x))) xa @= hypreal_of_real D)";
-by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff2,
- NSLIM_def]));
+\ (*f* (%z. (f z - f x) / (z - x))) xa @= hypreal_of_real D)";
+by (auto_tac (claset(), simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def]));
qed "NSDERIV_iff2";
Addsimps [inf_close_refl];
+
+(*FIXME: replace both of these by simprocs for cancellation of common factors*)
+Goal "h ~= (0::hypreal) ==> (x/h)*h = x";
+by (asm_simp_tac
+ (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left,
+ hypreal_mult_assoc]) 1);
+qed "hypreal_divide_mult_self_eq";
+Addsimps [hypreal_divide_mult_self_eq];
+
+Goal "h ~= (0::real) ==> (x/h)*h = x";
+by (asm_full_simp_tac
+ (simpset() addsimps [real_divide_def, real_mult_inv_left,
+ real_mult_assoc]) 1);
+qed "real_divide_mult_self_eq";
+Addsimps [real_divide_mult_self_eq];
+
Goal "(NSDERIV f x :> D) ==> \
\ (ALL xa. \
\ xa @= hypreal_of_real x --> \
@@ -940,13 +959,13 @@
inf_close_mult1 1);
by (ALLGOALS(dtac (hypreal_not_eq_minus_iff RS iffD1)));
by (subgoal_tac "(*f* (%z. z - x)) xa ~= (0::hypreal)" 2);
-by (dtac (starfun_inverse2 RS sym) 2);
-by (auto_tac (claset() addDs [hypreal_mult_inverse_left],
- simpset() addsimps [starfun_mult RS sym,
- hypreal_mult_assoc,starfun_add RS sym,real_diff_def,
- starfun_Id,hypreal_of_real_minus,hypreal_diff_def,
- (inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
- Infinitesimal_subset_HFinite RS subsetD]));
+by (rotate_tac ~1 2);
+by (auto_tac (claset(),
+ simpset() addsimps [starfun_divide RS sym,
+ starfun_add RS sym, real_diff_def,
+ hypreal_of_real_minus, hypreal_diff_def,
+ (inf_close_minus_iff RS iffD1) RS (mem_infmal_iff RS iffD2),
+ Infinitesimal_subset_HFinite RS subsetD]));
qed "NSDERIVD5";
Goal "(NSDERIV f x :> D) ==> \
@@ -959,7 +978,7 @@
by (dres_inst_tac [("x","h")] bspec 1);
by (dres_inst_tac [("c","h")] inf_close_mult1 2);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
- simpset() addsimps [hypreal_mult_assoc,hypreal_diff_def]));
+ simpset() addsimps [hypreal_diff_def]));
qed "NSDERIVD4";
Goal "(NSDERIV f x :> D) ==> \
@@ -970,7 +989,7 @@
by (rtac ccontr 1 THEN dres_inst_tac [("x","h")] bspec 1);
by (dres_inst_tac [("c","h")] inf_close_mult1 2);
by (auto_tac (claset() addIs [Infinitesimal_subset_HFinite RS subsetD],
- simpset() addsimps [hypreal_mult_assoc,hypreal_diff_def]));
+ simpset() addsimps [hypreal_mult_assoc, hypreal_diff_def]));
qed "NSDERIVD3";
(*--------------------------------------------------------------
@@ -1036,13 +1055,62 @@
(*-----------------------------------------------------
Sum of functions- proved easily
----------------------------------------------------*)
-Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \
+
+
+Goal "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def,
+ hypreal_of_real_mult, hypreal_of_real_inverse]) 1);
+qed "hypreal_of_real_divide"; (**??????HYPERDEF.ML??????*)
+
+
+(**??????HYPERDEF.ML???after inverse_distrib???*)
+Goal "(x::hypreal) * (y/z) = (x*y)/z";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1);
+qed "hypreal_times_divide1_eq";
+
+Goal "(y/z) * (x::hypreal) = (y*x)/z";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]@hypreal_mult_ac) 1);
+qed "hypreal_times_divide2_eq";
+
+Addsimps [hypreal_times_divide1_eq, hypreal_times_divide2_eq];
+
+Goal "(x::hypreal) / (y/z) = (x*z)/y";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]@
+ hypreal_mult_ac) 1);
+qed "hypreal_divide_divide1_eq";
+
+Goal "((x::hypreal) / y) / z = x/(y*z)";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib,
+ hypreal_mult_assoc]) 1);
+qed "hypreal_divide_divide2_eq";
+
+Addsimps [hypreal_divide_divide1_eq, hypreal_divide_divide2_eq];
+
+(** As with multiplication, pull minus signs OUT of the / operator **)
+
+Goal "(-x) / (y::hypreal) = - (x/y)";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+qed "hypreal_minus_divide_eq";
+Addsimps [hypreal_minus_divide_eq];
+
+Goal "(x / -(y::hypreal)) = - (x/y)";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1);
+qed "hypreal_divide_minus_eq";
+Addsimps [hypreal_divide_minus_eq];
+
+Goal "(x+y)/(z::hypreal) = x/z + y/z";
+by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_add_mult_distrib]) 1);
+qed "hypreal_add_divide_distrib";
+
+
+Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \
\ ==> NSDERIV (%x. f x + g x) x :> Da + Db";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
- NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
-by (auto_tac (claset(),simpset() addsimps [starfun_add RS sym,
- starfun_mult RS sym,hypreal_of_real_minus,hypreal_of_real_add,
- hypreal_minus_add_distrib,hypreal_add_mult_distrib]));
+ NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
+by (auto_tac (claset(),
+ simpset() addsimps [starfun_divide RS sym, starfun_add RS sym,
+ hypreal_of_real_minus, hypreal_of_real_add, hypreal_of_real_divide,
+ hypreal_add_divide_distrib]));
by (thin_tac "xa @= hypreal_of_real #0" 1 THEN dtac inf_close_add 1);
by (auto_tac (claset(),simpset() addsimps hypreal_add_ac));
qed "NSDERIV_add";
@@ -1066,48 +1134,65 @@
real_minus_mult_eq2 RS sym,real_mult_commute]) 1);
val lemma_nsderiv1 = result();
-Goal "[| (x + y) * inverse z = hypreal_of_real D + yb; z ~= 0; \
+(*FIXME: replace both of these by simprocs for cancellation of common factors*)
+Goal "h ~= (0::hypreal) ==> (x*h)/h = x";
+by (asm_simp_tac
+ (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left,
+ hypreal_mult_assoc]) 1);
+qed "hypreal_divide_mult2_self_eq";
+Addsimps [hypreal_divide_mult2_self_eq];
+
+Goal "h ~= (0::real) ==> (x*h)/h = x";
+by (asm_full_simp_tac
+ (simpset() addsimps [real_divide_def, real_mult_inv_left,
+ real_mult_assoc]) 1);
+qed "real_divide_mult2_self_eq";
+Addsimps [real_divide_mult2_self_eq];
+
+Goal "[| (x + y) / z = hypreal_of_real D + yb; z ~= 0; \
\ z : Infinitesimal; yb : Infinitesimal |] \
\ ==> x + y @= 0";
-by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel
- RS iffD2) 1 THEN assume_tac 1);
-by (thin_tac "(x + y) * inverse z = hypreal_of_real D + yb" 1);
-by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2,
- HFinite_add],simpset() addsimps [hypreal_mult_assoc,
- mem_infmal_iff RS sym]));
+by (forw_inst_tac [("c1","z")] (hypreal_mult_right_cancel RS iffD2) 1
+ THEN assume_tac 1);
+by (thin_tac "(x + y) / z = hypreal_of_real D + yb" 1);
+by (auto_tac (claset() addSIs [Infinitesimal_HFinite_mult2, HFinite_add],
+ simpset() addsimps [hypreal_mult_assoc, mem_infmal_iff RS sym]));
by (etac (Infinitesimal_subset_HFinite RS subsetD) 1);
val lemma_nsderiv2 = result();
Goal "[| NSDERIV f x :> Da; NSDERIV g x :> Db |] \
\ ==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))";
-by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
- NSLIM_def]) 1 THEN REPEAT(Step_tac 1));
-by (auto_tac (claset(),simpset() addsimps [starfun_mult RS sym,
- starfun_add RS sym,starfun_lambda_cancel,
- starfun_inverse_inverse,hypreal_of_real_zero,lemma_nsderiv1]));
-by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
+by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def]) 1
+ THEN REPEAT(Step_tac 1));
+by (auto_tac (claset(),
+ simpset() addsimps [starfun_divide RS sym, starfun_mult RS sym,
+ starfun_add RS sym,starfun_lambda_cancel,hypreal_of_real_zero,
+ lemma_nsderiv1]));
+by (simp_tac (simpset() addsimps [hypreal_add_divide_distrib]) 1);
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1));
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
- hypreal_of_real_minus]));
+by (auto_tac (claset(),
+ simpset() delsimps [hypreal_times_divide1_eq]
+ addsimps [hypreal_times_divide1_eq RS sym,
+ hypreal_of_real_minus]));
by (dres_inst_tac [("D","Db")] lemma_nsderiv2 1);
-by (dtac ((inf_close_minus_iff RS iffD2) RS
- (bex_Infinitesimal_iff2 RS iffD2)) 4);
+by (dtac (inf_close_minus_iff RS iffD2 RS (bex_Infinitesimal_iff2 RS iffD2)) 4);
by (auto_tac (claset() addSIs [inf_close_add_mono1],
simpset() addsimps [hypreal_of_real_add,hypreal_add_mult_distrib,
- hypreal_add_mult_distrib2,hypreal_of_real_mult,hypreal_mult_commute,
- hypreal_add_assoc]));
+ hypreal_add_mult_distrib2,hypreal_of_real_mult,hypreal_mult_commute,
+ hypreal_add_assoc]));
by (res_inst_tac [("w1","hypreal_of_real Db * hypreal_of_real (f x)")]
(hypreal_add_commute RS subst) 1);
by (auto_tac (claset() addSIs [Infinitesimal_add_inf_close_self2 RS
- inf_close_sym,Infinitesimal_add,Infinitesimal_mult,
- Infinitesimal_hypreal_of_real_mult,Infinitesimal_hypreal_of_real_mult2 ],
- simpset() addsimps [hypreal_add_assoc RS sym]));
+ inf_close_sym,Infinitesimal_add,Infinitesimal_mult,
+ Infinitesimal_hypreal_of_real_mult,
+ Infinitesimal_hypreal_of_real_mult2 ],
+ simpset() addsimps [hypreal_add_assoc RS sym]));
qed "NSDERIV_mult";
Goal "[| DERIV f x :> Da; DERIV g x :> Db |] \
\ ==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_mult,
- NSDERIV_DERIV_iff RS sym]) 1);
+ NSDERIV_DERIV_iff RS sym]) 1);
qed "DERIV_mult";
(*----------------------------
@@ -1115,9 +1200,10 @@
---------------------------*)
Goal "NSDERIV f x :> D \
\ ==> NSDERIV (%x. c * f x) x :> c*D";
-by (asm_full_simp_tac (simpset() addsimps [NSDERIV_NSLIM_iff,
- real_minus_mult_eq2,real_add_mult_distrib2 RS sym,
- real_mult_assoc] delsimps [real_minus_mult_eq2 RS sym]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
+ real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
+ delsimps [real_times_divide1_eq, real_minus_mult_eq2 RS sym]) 1);
by (etac (NSLIM_const RS NSLIM_mult) 1);
qed "NSDERIV_cmult";
@@ -1127,9 +1213,10 @@
Goalw [deriv_def]
"DERIV f x :> D \
\ ==> DERIV (%x. c * f x) x :> c*D";
-by (asm_full_simp_tac (simpset() addsimps [
- real_minus_mult_eq2,real_add_mult_distrib2 RS sym,
- real_mult_assoc] delsimps [real_minus_mult_eq2 RS sym]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [real_times_divide1_eq RS sym, NSDERIV_NSLIM_iff,
+ real_minus_mult_eq2, real_add_mult_distrib2 RS sym]
+ delsimps [real_times_divide1_eq, real_minus_mult_eq2 RS sym]) 1);
by (etac (LIM_const RS LIM_mult2) 1);
qed "DERIV_cmult";
@@ -1193,6 +1280,13 @@
by (etac (NSdifferentiableI RS incrementI) 1);
qed "incrementI2";
+(*FIXME: replace by simprocs for cancellation of common factors*)
+Goal "h ~= (0::hypreal) ==> h/h = 1hr";
+by (asm_simp_tac
+ (simpset() addsimps [hypreal_divide_def, hypreal_mult_inverse_left]) 1);
+qed "hypreal_divide_self_eq";
+Addsimps [hypreal_divide_self_eq];
+
(* The Increment theorem -- Keisler p. 65 *)
Goal "[| NSDERIV f x :> D; h: Infinitesimal; h ~= 0 |] \
\ ==> EX e: Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h";
@@ -1200,12 +1294,14 @@
by (dtac bspec 1 THEN Auto_tac);
by (dtac (bex_Infinitesimal_iff2 RS iffD2) 1 THEN Step_tac 1);
by (forw_inst_tac [("b1","hypreal_of_real(D) + y")]
- (hypreal_mult_right_cancel RS iffD2) 1);
+ (hypreal_mult_right_cancel RS iffD2) 1);
by (thin_tac "((*f* f) (hypreal_of_real(x) + h) + \
-\ - hypreal_of_real (f x)) * inverse h = hypreal_of_real(D) + y" 2);
+\ - hypreal_of_real (f x)) / h = hypreal_of_real(D) + y" 2);
by (assume_tac 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
- hypreal_add_mult_distrib]));
+by (asm_full_simp_tac (simpset() addsimps [hypreal_times_divide1_eq RS sym]
+ delsimps [hypreal_times_divide1_eq]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_add_mult_distrib]));
qed "increment_thm";
Goal "[| NSDERIV f x :> D; h @= 0; h ~= 0 |] \
@@ -1231,22 +1327,32 @@
the so-called Carathedory derivative. Our main problem is
manipulation of terms.
--------------------------------------------------------------*)
+
+(*???HYPERDEF.ML???*)
+Goal "(0::hypreal)/x = 0";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+qed "hypreal_zero_divide";
+
+Goal "x/1hr = x";
+by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1);
+qed "hypreal_divide_one";
+Addsimps [hypreal_zero_divide, hypreal_divide_one];
+
(* lemmas *)
Goalw [nsderiv_def]
- "!!f. [| NSDERIV g x :> D; \
+ "[| NSDERIV g x :> D; \
\ (*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x);\
\ xa : Infinitesimal;\
\ xa ~= 0 \
\ |] ==> D = #0";
by (dtac bspec 1);
by (Auto_tac);
-by (asm_full_simp_tac (simpset() addsimps
- [hypreal_of_real_zero RS sym]) 1);
+by (asm_full_simp_tac (simpset() addsimps [hypreal_of_real_zero RS sym]) 1);
qed "NSDERIV_zero";
(* can be proved differently using NSLIM_isCont_iff *)
Goalw [nsderiv_def]
- "!!f. [| NSDERIV f x :> D; \
+ "[| NSDERIV f x :> D; \
\ h: Infinitesimal; h ~= 0 \
\ |] ==> (*f* f) (hypreal_of_real(x) + h) + -hypreal_of_real(f x) @= 0";
by (asm_full_simp_tac (simpset() addsimps
@@ -1267,12 +1373,13 @@
\ (*f* g) (hypreal_of_real(x) + xa) ~= hypreal_of_real (g x); \
\ (*f* g) (hypreal_of_real(x) + xa) @= hypreal_of_real (g x) \
\ |] ==> ((*f* f) ((*f* g) (hypreal_of_real(x) + xa)) \
-\ + - hypreal_of_real (f (g x)))* \
-\ inverse ((*f* g) (hypreal_of_real(x) + xa) + \
-\ - hypreal_of_real (g x)) @= hypreal_of_real(Da)";
-by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff2,
- NSLIM_def,starfun_mult RS sym,hypreal_of_real_minus,
- starfun_add RS sym,starfun_inverse3]));
+\ + - hypreal_of_real (f (g x))) \
+\ / ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real (g x)) \
+\ @= hypreal_of_real(Da)";
+by (auto_tac (claset(),
+ simpset() addsimps [NSDERIV_NSLIM_iff2, NSLIM_def, starfun_divide RS sym,
+ hypreal_of_real_minus,
+ starfun_add RS sym]));
qed "NSDERIVD1";
(*--------------------------------------------------------------
@@ -1283,12 +1390,12 @@
h
--------------------------------------------------------------*)
Goal "[| NSDERIV g x :> Db; xa: Infinitesimal; xa ~= 0 |] \
-\ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) * \
-\ inverse xa @= hypreal_of_real(Db)";
-by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff,
- NSLIM_def,starfun_mult RS sym,starfun_inverse_inverse,
- starfun_add RS sym,hypreal_of_real_zero,mem_infmal_iff,
- starfun_lambda_cancel,hypreal_of_real_minus]));
+\ ==> ((*f* g) (hypreal_of_real(x) + xa) + - hypreal_of_real(g x)) / xa \
+\ @= hypreal_of_real(Db)";
+by (auto_tac (claset(),
+ simpset() addsimps [NSDERIV_NSLIM_iff, NSLIM_def, starfun_divide RS sym,
+ starfun_add RS sym, hypreal_of_real_zero, mem_infmal_iff,
+ starfun_lambda_cancel,hypreal_of_real_minus]));
qed "NSDERIVD2";
(*---------------------------------------------
@@ -1301,23 +1408,24 @@
NSLIM_def,hypreal_of_real_zero,mem_infmal_iff RS sym]) 1 THEN Step_tac 1);
by (forw_inst_tac [("f","g")] NSDERIV_inf_close 1);
by (auto_tac (claset(),simpset() addsimps [starfun_add RS sym,
- hypreal_of_real_minus,starfun_inverse_inverse,hypreal_of_real_mult,
- starfun_lambda_cancel2,starfun_o RS sym,starfun_mult RS sym]));
+ hypreal_of_real_minus, hypreal_of_real_mult,
+ starfun_lambda_cancel2,starfun_o RS sym, starfun_divide RS sym]));
by (case_tac "(*f* g) (hypreal_of_real(x) + xa) = hypreal_of_real (g x)" 1);
by (dres_inst_tac [("g","g")] NSDERIV_zero 1);
-by (auto_tac (claset(),simpset()
- addsimps [hypreal_of_real_zero,inf_close_refl]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_divide_def, hypreal_of_real_zero]));
by (res_inst_tac [("z1","(*f* g) (hypreal_of_real(x) + xa) + -hypreal_of_real (g x)"),
("y1","inverse xa")] (lemma_chain RS ssubst) 1);
by (etac (hypreal_not_eq_minus_iff RS iffD1) 1);
by (rtac inf_close_mult_hypreal_of_real 1);
+by (fold_tac [hypreal_divide_def]);
by (blast_tac (claset() addIs [NSDERIVD1,
inf_close_minus_iff RS iffD2]) 1);
by (blast_tac (claset() addIs [NSDERIVD2]) 1);
qed "NSDERIV_chain";
(* standard version *)
-Goal "!!f. [| DERIV f (g x) :> Da; \
+Goal "[| DERIV f (g x) :> Da; \
\ DERIV g x :> Db \
\ |] ==> DERIV (f o g) x :> Da * Db";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff RS sym,
@@ -1329,18 +1437,14 @@
by (auto_tac (claset() addDs [DERIV_chain], simpset() addsimps [o_def]));
qed "DERIV_chain2";
-Goal "[| DERIV f x :> D; D = E |] ==> DERIV f x :> E";
-by (Auto_tac);
-val lemma_DERIV_tac = result();
-
(*------------------------------------------------------------------
Differentiation of natural number powers
------------------------------------------------------------------*)
Goal "NSDERIV (%x. x) x :> #1";
-by (auto_tac (claset(),simpset() addsimps [NSDERIV_NSLIM_iff,
- NSLIM_def,starfun_mult RS sym,starfun_Id,hypreal_of_real_zero,
- starfun_inverse_inverse,hypreal_of_real_one]
- @ real_add_ac));
+by (auto_tac (claset(),
+ simpset() addsimps [NSDERIV_NSLIM_iff,
+ NSLIM_def, starfun_divide RS sym,starfun_Id, hypreal_of_real_zero,
+ hypreal_of_real_one]));
qed "NSDERIV_Id";
Addsimps [NSDERIV_Id];
@@ -1350,6 +1454,8 @@
qed "DERIV_Id";
Addsimps [DERIV_Id];
+bind_thm ("isCont_Id", DERIV_Id RS DERIV_isCont);
+
(*derivative of linear multiplication*)
Goal "DERIV (op * c) x :> c";
by (cut_inst_tac [("c","c"),("x","x")] (DERIV_Id RS DERIV_cmult) 1);
@@ -1381,14 +1487,27 @@
(*---------------------------------------------------------------
Power of -1
---------------------------------------------------------------*)
+
+
+(*FIXME: replace by simprocs for cancellation of common factors*)
+Goal "h ~= (0::hypreal) ==> (h*x)/h = x";
+by (asm_simp_tac
+ (simpset() addsimps [inst "z" "h" hypreal_mult_commute]) 1);
+qed "hypreal_times_divide_self_eq";
+Addsimps [hypreal_times_divide_self_eq];
+
+(*Can't get rid of x ~= #0 because it isn't continuous at zero*)
Goalw [nsderiv_def]
"x ~= #0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))";
by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1);
by (forward_tac [Infinitesimal_add_not_zero] 1);
-by (auto_tac (claset(),simpset() addsimps [starfun_inverse_inverse,
+by (auto_tac (claset(),
+ simpset() addsimps [starfun_inverse_inverse,
hypreal_of_real_inverse RS sym,hypreal_of_real_minus,realpow_two,
- hypreal_of_real_mult] delsimps [hypreal_minus_mult_eq1 RS
- sym,hypreal_minus_mult_eq2 RS sym]));
+ hypreal_of_real_mult,
+ hypreal_of_real_divide]
+ delsimps [hypreal_minus_mult_eq1 RS sym,
+ hypreal_minus_mult_eq2 RS sym]));
by (dtac (hypreal_of_real_not_zero_iff RS iffD2) 1);
by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_add,
inverse_mult_eq RS sym, hypreal_minus_inverse RS sym]
@@ -1437,20 +1556,20 @@
Derivative of quotient
-------------------------------------------------------------*)
Goal "[| DERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \
-\ ==> DERIV (%y. f(y)*inverse(g y)) x :> (d*g(x) \
-\ + -(e*f(x)))*inverse(g(x) ^ 2)";
+\ ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) + -(e*f(x))) / (g(x) ^ 2)";
by (dres_inst_tac [("f","g")] DERIV_inverse_fun 1);
by (dtac DERIV_mult 2);
by (REPEAT(assume_tac 1));
-by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2,
- realpow_inverse,real_minus_mult_eq1] @ real_mult_ac delsimps
- [thm "realpow_Suc",real_minus_mult_eq1 RS sym,
- real_minus_mult_eq2 RS sym]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [real_divide_def, real_add_mult_distrib2,
+ realpow_inverse,real_minus_mult_eq1] @ real_mult_ac
+ delsimps [thm "realpow_Suc", real_minus_mult_eq1 RS sym,
+ real_minus_mult_eq2 RS sym]) 1);
qed "DERIV_quotient";
Goal "[| NSDERIV f x :> d; DERIV g x :> e; g(x) ~= #0 |] \
-\ ==> NSDERIV (%y. f(y)*inverse(g y)) x :> (d*g(x) \
-\ + -(e*f(x)))*inverse(g(x) ^ 2)";
+\ ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) \
+\ + -(e*f(x))) / (g(x) ^ 2)";
by (asm_full_simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,
DERIV_quotient] delsimps [thm "realpow_Suc"]) 1);
qed "NSDERIV_quotient";
@@ -1463,7 +1582,7 @@
\ (EX g. (ALL z. f z - f x = g z * (z - x)) & isCont g x & g x = l)";
by (Step_tac 1);
by (res_inst_tac
- [("x","%z. if z = x then l else (f(z) - f(x)) * inverse (z - x)")] exI 1);
+ [("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1);
by (auto_tac (claset(),simpset() addsimps [real_mult_assoc,
ARITH_PROVE "z ~= x ==> z - x ~= (#0::real)"]));
by (auto_tac (claset(),simpset() addsimps [isCont_iff,DERIV_iff]));
@@ -1480,13 +1599,14 @@
(* How about a NS proof? *)
Goal "(ALL z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l \
\ ==> NSDERIV f x :> l";
-by (auto_tac (claset(),simpset() addsimps [NSDERIV_iff2,starfun_mult
- RS sym]));
-by (rtac (starfun_inverse2 RS subst) 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_mult_assoc,
- starfun_diff RS sym,starfun_Id]));
+by (auto_tac (claset(),
+ simpset() addsimps [NSDERIV_iff2, starfun_mult RS sym,
+ starfun_divide RS sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_mult_assoc,
+ starfun_diff RS sym]));
by (asm_full_simp_tac (simpset() addsimps [hypreal_eq_minus_iff3 RS sym,
- hypreal_diff_def]) 1);
+ hypreal_diff_def]) 1);
by (dtac (CLAIM_SIMP "x ~= y ==> x - y ~= (0::hypreal)" [hypreal_eq_minus_iff3 RS sym,
hypreal_diff_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [isNSCont_def]) 1);
@@ -1545,17 +1665,17 @@
by (induct_tac "no" 2);
by (auto_tac (claset() addIs [real_le_trans],
simpset() addsimps [real_diff_def]));
-by (dtac abs_eqI1 1 THEN Asm_full_simp_tac 1);
-by (dres_inst_tac [("i"," f (no + n)"),("no1","no")] (lemma_f_mono_add
- RSN (2,real_less_le_trans)) 1);
-by (subgoal_tac "0 <= lim g + - g(no + n)" 3);
+by (asm_full_simp_tac (simpset() addsimps [inst "r" "f ?x + ?y" abs_real_def]) 1);
+by (dres_inst_tac [("i"," f (no + n)"),("no1","no")]
+ (lemma_f_mono_add RSN (2,real_less_le_trans)) 1);
+by (subgoal_tac "g(no + n) <= lim g" 3);
by (induct_tac "no" 4);
by (auto_tac (claset() addIs [real_le_trans],
simpset() addsimps [real_diff_def,abs_minus_add_cancel]));
-by (dtac abs_eqI1 2 THEN Asm_full_simp_tac 2);
-by (dres_inst_tac [("i","- g (no + n)"),("no1","no")] (lemma_f_mono_add
- RSN (2,real_less_le_trans)) 2);
-by (auto_tac (claset(),simpset() addsimps [add_commute]));
+by (asm_full_simp_tac (simpset() addsimps [inst "r" "lim g + ?y" abs_real_def]) 2);
+by (cut_inst_tac [("f", "%x. -(g x)"), ("m","n"), ("no","no")]
+ lemma_f_mono_add 2);
+by (auto_tac (claset(), simpset() addsimps [add_commute]));
qed "lemma_nest";
Goal "[| ALL n. f(n) <= f(Suc n); \
@@ -1580,19 +1700,7 @@
qed "nat_Axiom";
-(****************************************************************
-REPLACING THE VERSION IN REALORD.ML
-****************************************************************)
-
-(*NEW VERSION with #2*)
-Goal "x < y ==> x < (x + y) / (#2::real)";
-by Auto_tac;
-qed "real_less_half_sum";
-
-
-(*Replaces "inverse #nn" by #1/#nn *)
-Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide];
-
+(*?????????OBSOLETE????????***)
Goal "((x::real) = y / (#2 * z)) = (#2 * x = y/z)";
by Auto_tac;
by (dres_inst_tac [("f","%u. (#1/#2)*u")] arg_cong 1);
@@ -1711,13 +1819,9 @@
by (subgoal_tac "#0 <= (l + - fst (fn (no + noa)))" 1);
by (subgoal_tac "#0 <= (snd (fn (no + noa)) + - l)" 1);
by (asm_simp_tac (simpset() addsimps [abs_eqI1] @ real_add_ac) 1);
-by (asm_simp_tac (simpset() addsimps real_add_ac) 1);
-by (res_inst_tac [("C","l")] real_le_add_right_cancel 1);
-by (res_inst_tac [("C"," fst (fn (no + noa))")] real_le_add_right_cancel 2);
-by (ALLGOALS(asm_simp_tac (simpset() addsimps real_add_ac)));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps real_add_divide_distrib::real_add_ac)));
qed "lemma_BOLZANO";
-
Goal "((ALL a b c. (a <= b & b <= c & P(a,b) & P(b,c)) --> P(a,c)) & \
\ (ALL x. EX d::real. 0 < d & \
\ (ALL a b. a <= x & x <= b & (b - a) < d --> P(a,b)))) \
@@ -1995,90 +2099,6 @@
(* If f'(x) > 0 then x is locally strictly increasing at the right *)
(*----------------------------------------------------------------------------*)
-
-(**????????????????????????????????????????????????????????????????
- MOVE EARLIER *)
-
-
-(** The next several equations can make the simplifier loop! **)
-
-Goal "(x < - y) = (y < - (x::real))";
-by Auto_tac;
-qed "real_less_minus";
-
-Goal "(- x < y) = (- y < (x::real))";
-by Auto_tac;
-(*or this:
-by (res_inst_tac [("t","x")] (real_minus_minus RS subst) 1);
-by (stac real_minus_less_minus 1);
-by (Simp_tac 1);
-*)
-qed "real_minus_less";
-
-Goal "(x <= - y) = (y <= - (x::real))";
-by Auto_tac;
-qed "real_le_minus";
-
-Goal "(- x <= y) = (- y <= (x::real))";
-by Auto_tac;
-qed "real_minus_le";
-
-Goal "(x = - y) = (y = - (x::real))";
-by Auto_tac;
-qed "real_equation_minus";
-
-Goal "(- x = y) = (- (y::real) = x)";
-by Auto_tac;
-qed "real_minus_equation";
-
-
-(*Distributive laws for literals*)
-Addsimps (map (inst "w" "number_of ?v")
- [real_add_mult_distrib, real_add_mult_distrib2,
- real_diff_mult_distrib, real_diff_mult_distrib2]);
-
-Addsimps (map (inst "x" "number_of ?v")
- [real_less_minus, real_le_minus, real_equation_minus]);
-Addsimps (map (inst "y" "number_of ?v")
- [real_minus_less, real_minus_le, real_minus_equation]);
-
-
-(*move up these rewrites AFTER the rest works*)
-
-Goal "(x+y = (#0::real)) = (y = -x)";
-by Auto_tac;
-qed "real_add_eq_0_iff";
-AddIffs [real_add_eq_0_iff];
-
-Goal "((#0::real) = x+y) = (y = -x)";
-by Auto_tac;
-qed "real_0_eq_add_iff";
-AddIffs [real_0_eq_add_iff];
-
-Goal "(x+y < (#0::real)) = (y < -x)";
-by Auto_tac;
-qed "real_add_less_0_iff";
-AddIffs [real_add_less_0_iff];
-
-Goal "((#0::real) < x+y) = (-x < y)";
-by Auto_tac;
-qed "real_0_less_add_iff";
-AddIffs [real_0_less_add_iff];
-
-Goal "(x+y <= (#0::real)) = (y <= -x)";
-by Auto_tac;
-qed "real_add_le_0_iff";
-AddIffs [real_add_le_0_iff];
-
-Goal "((#0::real) <= x+y) = (-x <= y)";
-by Auto_tac;
-qed "real_0_le_add_iff";
-AddIffs [real_0_le_add_iff];
-
-(*
-Addsimps [symmetric real_diff_def];
-*)
-
Goalw [deriv_def,LIM_def]
"[| DERIV f x :> l; #0 < l |] ==> \
\ EX d. #0 < d & (ALL h. #0 < h & h < d --> f(x) < f(x + h))";
@@ -2093,14 +2113,6 @@
addsplits [split_if_asm]) 1);
qed "DERIV_left_inc";
-Addsimps [real_minus_less_minus] (****************);
-
-
-Goal "-(x-y) = y - (x::real)";
-by (arith_tac 1);
-qed "real_minus_diff_eq";
-Addsimps [real_minus_diff_eq]; (******************************************************************)
-
Goalw [deriv_def,LIM_def]
"[| DERIV f x :> l; l < #0 |] ==> \
\ EX d. #0 < d & (ALL h. #0 < h & h < d --> f(x) < f(x - h))";
@@ -2256,45 +2268,21 @@
(*----------------------------------------------------------------------------*)
-(*????????????????*)
-
+(*????????TO BE OBSOLETE?????????*)
Goal "k~=#0 ==> (k*m) / k = (m::real)";
by (dres_inst_tac [("n","#1")] real_mult_div_cancel1 1);
by (Asm_full_simp_tac 1);
qed "real_mult_div_self1";
Addsimps [real_mult_div_self1];
-(*move up these rewrites AFTER the rest works*)
-Goal "(x-y = (#0::real)) = (x = y)";
-by Auto_tac;
-qed "real_diff_eq_0_iff";
-AddIffs [real_diff_eq_0_iff];
-
-Goal "((#0::real) = x-y) = (x = y)";
-by Auto_tac;
-qed "real_0_eq_diff_iff";
-AddIffs [real_0_eq_diff_iff];
-
-Goal "(x-y < (#0::real)) = (x < y)";
-by Auto_tac;
-qed "real_diff_less_0_iff";
-AddIffs [real_diff_less_0_iff];
-
-Goal "((#0::real) < x-y) = (y < x)";
-by Auto_tac;
-qed "real_0_less_diff_iff";
-AddIffs [real_0_less_diff_iff];
-
-Goal "(x-y <= (#0::real)) = (x <= y)";
-by Auto_tac;
-qed "real_diff_le_0_iff";
-AddIffs [real_diff_le_0_iff];
-
-Goal "((#0::real) <= x-y) = (y <= x)";
-by Auto_tac;
-qed "real_0_le_diff_iff";
-AddIffs [real_0_le_diff_iff];
+(**???FIXME: replace by simproc*??*)
+Goal "h ~= (0::real) ==> (h*x)/h = x";
+by (asm_full_simp_tac
+ (simpset() addsimps [real_divide_mult2_self_eq,
+ real_mult_commute]) 1);
+qed "real_divide_mult3_self_eq";
+Delsimps [real_divide_mult3_self_eq];
Goal "f a - (f b - f a)/(b - a) * a = \
@@ -2305,8 +2293,7 @@
by (arith_tac 1);
by (auto_tac (claset(),
simpset() addsimps [real_diff_mult_distrib2, real_diff_eq_eq,
- eq_commute]));
+ inst "a" "a" eq_commute]));
by (auto_tac (claset(),
- simpset() addsimps [real_diff_mult_distrib2, real_mult_commute]));
+ simpset() addsimps [real_diff_mult_distrib2, real_mult_commute]));
qed "lemma_MVT";
-
--- a/src/HOL/Real/Hyperreal/Lim.thy Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.thy Fri Dec 15 17:41:38 2000 +0100
@@ -7,57 +7,60 @@
Lim = SEQ + RealAbs +
- (*-----------------------------------------------------------------------
- Limits, continuity and differentiation: standard and NS definitions
- -----------------------------------------------------------------------*)
+(*-----------------------------------------------------------------------
+ Limits, continuity and differentiation: standard and NS definitions
+ -----------------------------------------------------------------------*)
+
constdefs
- LIM :: [real=>real,real,real] => bool
- ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
- "f -- a --> L ==
- ALL r. #0 < r -->
- (EX s. #0 < s & (ALL x. (x ~= a & (abs(x + -a) < s)
- --> abs(f x + -L) < r)))"
+ LIM :: [real=>real,real,real] => bool
+ ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
+ "f -- a --> L ==
+ ALL r. #0 < r -->
+ (EX s. #0 < s & (ALL x. (x ~= a & (abs(x + -a) < s)
+ --> abs(f x + -L) < r)))"
- NSLIM :: [real=>real,real,real] => bool
- ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
- "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a &
- x @= hypreal_of_real a --> (*f* f) x @= hypreal_of_real L))"
+ NSLIM :: [real=>real,real,real] => bool
+ ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
+ "f -- a --NS> L == (ALL x. (x ~= hypreal_of_real a &
+ x @= hypreal_of_real a -->
+ (*f* f) x @= hypreal_of_real L))"
- isCont :: [real=>real,real] => bool
- "isCont f a == (f -- a --> (f a))"
+ isCont :: [real=>real,real] => bool
+ "isCont f a == (f -- a --> (f a))"
+
+ (* NS definition dispenses with limit notions *)
+ isNSCont :: [real=>real,real] => bool
+ "isNSCont f a == (ALL y. y @= hypreal_of_real a -->
+ (*f* f) y @= hypreal_of_real (f a))"
- (* NS definition dispenses with limit notions *)
- isNSCont :: [real=>real,real] => bool
- "isNSCont f a == (ALL y. y @= hypreal_of_real a -->
- (*f* f) y @= hypreal_of_real (f a))"
-
- (* differentiation: D is derivative of function f at x *)
- deriv:: [real=>real,real,real] => bool
- ("(DERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
- "DERIV f x :> D == ((%h. (f(x + h) + -f(x))*inverse(h)) -- #0 --> D)"
+ (* differentiation: D is derivative of function f at x *)
+ deriv:: [real=>real,real,real] => bool
+ ("(DERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
+ "DERIV f x :> D == ((%h. (f(x + h) + -f(x))/h) -- #0 --> D)"
- nsderiv :: [real=>real,real,real] => bool
- ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
- "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}.
- ((*f* f)(hypreal_of_real x + h) +
- -hypreal_of_real (f x))*inverse(h) @= hypreal_of_real D)"
+ nsderiv :: [real=>real,real,real] => bool
+ ("(NSDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
+ "NSDERIV f x :> D == (ALL h: Infinitesimal - {0}.
+ ((*f* f)(hypreal_of_real x + h) +
+ - hypreal_of_real (f x))/h @= hypreal_of_real D)"
+
+ differentiable :: [real=>real,real] => bool (infixl 60)
+ "f differentiable x == (EX D. DERIV f x :> D)"
- differentiable :: [real=>real,real] => bool (infixl 60)
- "f differentiable x == (EX D. DERIV f x :> D)"
+ NSdifferentiable :: [real=>real,real] => bool (infixl 60)
+ "f NSdifferentiable x == (EX D. NSDERIV f x :> D)"
- NSdifferentiable :: [real=>real,real] => bool (infixl 60)
- "f NSdifferentiable x == (EX D. NSDERIV f x :> D)"
+ increment :: [real=>real,real,hypreal] => hypreal
+ "increment f x h == (@inc. f NSdifferentiable x &
+ inc = (*f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
- increment :: [real=>real,real,hypreal] => hypreal
- "increment f x h == (@inc. f NSdifferentiable x &
- inc = (*f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
+ isUCont :: (real=>real) => bool
+ "isUCont f == (ALL r. #0 < r -->
+ (EX s. #0 < s & (ALL x y. abs(x + -y) < s
+ --> abs(f x + -f y) < r)))"
- isUCont :: (real=>real) => bool
- "isUCont f == (ALL r. #0 < r -->
- (EX s. #0 < s & (ALL x y. abs(x + -y) < s
- --> abs(f x + -f y) < r)))"
+ isNSUCont :: (real=>real) => bool
+ "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
- isNSUCont :: (real=>real) => bool
- "isNSUCont f == (ALL x y. x @= y --> (*f* f) x @= (*f* f) y)"
end
--- a/src/HOL/Real/Hyperreal/NSA.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NSA.ML Fri Dec 15 17:41:38 2000 +0100
@@ -27,18 +27,18 @@
by (simp_tac (simpset() addsimps [hypreal_of_real_mult]) 1);
qed "SReal_mult";
-Goalw [SReal_def] "[| x: SReal; x ~= 0 |] ==> inverse x : SReal";
-by (blast_tac (claset() addSDs [hypreal_of_real_inverse2]) 1);
+Goalw [SReal_def] "x: SReal ==> inverse x : SReal";
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_inverse]));
qed "SReal_inverse";
Goalw [SReal_def] "x: SReal ==> -x : SReal";
-by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_minus RS sym]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_minus RS sym]));
qed "SReal_minus";
Goal "[| x + y : SReal; y: SReal |] ==> x: SReal";
by (dres_inst_tac [("x","y")] SReal_minus 1);
by (dtac SReal_add 1);
-by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
+by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
qed "SReal_add_cancel";
Goalw [SReal_def] "x: SReal ==> abs x : SReal";
@@ -46,21 +46,21 @@
qed "SReal_hrabs";
Goalw [SReal_def] "hypreal_of_real #1 : SReal";
-by (Auto_tac);
+by (auto_tac (claset() addIs [hypreal_of_real_one RS sym], simpset()));
qed "SReal_hypreal_of_real_one";
Goalw [SReal_def] "hypreal_of_real 0 : SReal";
-by (Auto_tac);
+by (auto_tac (claset() addIs [hypreal_of_real_zero RS sym], simpset()));
qed "SReal_hypreal_of_real_zero";
Goal "1hr : SReal";
by (simp_tac (simpset() addsimps [SReal_hypreal_of_real_one,
- hypreal_of_real_one RS sym]) 1);
+ hypreal_of_real_one RS sym]) 1);
qed "SReal_one";
Goal "0 : SReal";
-by (simp_tac (simpset() addsimps [rename_numerals
- SReal_hypreal_of_real_zero,hypreal_of_real_zero RS sym]) 1);
+by (simp_tac (simpset() addsimps [rename_numerals SReal_hypreal_of_real_zero,
+ hypreal_of_real_zero RS sym]) 1);
qed "SReal_zero";
Goal "1hr + 1hr : SReal";
@@ -69,13 +69,12 @@
Addsimps [SReal_zero,SReal_two];
-Goal "r : SReal ==> r*inverse(1hr + 1hr): SReal";
-by (blast_tac (claset() addSIs [SReal_mult,SReal_inverse,
- SReal_two,hypreal_two_not_zero]) 1);
+Goalw [hypreal_divide_def] "r : SReal ==> r/(1hr + 1hr): SReal";
+by (blast_tac (claset() addSIs [SReal_mult, SReal_inverse, SReal_two]) 1);
qed "SReal_half";
(* in general: move before previous thms!*)
-Goalw [SReal_def] "hypreal_of_real x: SReal";
+Goalw [SReal_def] "hypreal_of_real x: SReal";
by (Blast_tac 1);
qed "SReal_hypreal_of_real";
@@ -84,13 +83,13 @@
(* Infinitesimal ehr not in SReal *)
Goalw [SReal_def] "ehr ~: SReal";
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_of_real_not_eq_epsilon RS not_sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_not_eq_epsilon RS not_sym]));
qed "SReal_epsilon_not_mem";
Goalw [SReal_def] "whr ~: SReal";
-by (auto_tac (claset(),simpset() addsimps
- [hypreal_of_real_not_eq_omega RS not_sym]));
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_not_eq_omega RS not_sym]));
qed "SReal_omega_not_mem";
Goalw [SReal_def] "{x. hypreal_of_real x : SReal} = (UNIV::real set)";
@@ -286,18 +285,15 @@
Goalw [Infinitesimal_def] "0 : Infinitesimal";
by (simp_tac (simpset() addsimps [hrabs_zero]) 1);
qed "Infinitesimal_zero";
-
Addsimps [Infinitesimal_zero];
Goalw [Infinitesimal_def]
- "[| x : Infinitesimal; y : Infinitesimal |] \
-\ ==> (x + y) : Infinitesimal";
+ "[| x : Infinitesimal; y : Infinitesimal |] ==> (x + y) : Infinitesimal";
by (Auto_tac);
by (rtac (hypreal_sum_of_halves RS subst) 1);
by (dtac hypreal_half_gt_zero 1);
by (dtac SReal_half 1);
-by (auto_tac (claset() addSDs [bspec]
- addIs [hrabs_add_less],simpset()));
+by (auto_tac (claset() addSDs [bspec] addIs [hrabs_add_less], simpset()));
qed "Infinitesimal_add";
Goalw [Infinitesimal_def]
@@ -326,22 +322,20 @@
by (ALLGOALS(blast_tac (claset() addSDs [bspec])));
qed "Infinitesimal_mult";
-Goal "[| x : Infinitesimal; y : HFinite |] \
-\ ==> (x * y) : Infinitesimal";
+Goal "[| x : Infinitesimal; y : HFinite |] ==> (x * y) : Infinitesimal";
by (auto_tac (claset() addSDs [HFiniteD],
- simpset() addsimps [Infinitesimal_def]));
+ simpset() addsimps [Infinitesimal_def]));
by (forward_tac [hrabs_less_gt_zero] 1);
by (dtac (hypreal_inverse_gt_zero RSN (2,hypreal_mult_less_mono2)) 1
THEN assume_tac 1);
-by (dtac ((hypreal_not_refl2 RS not_sym) RSN (2,SReal_inverse)) 1
- THEN assume_tac 1);
+by (dtac SReal_inverse 1);
by (dtac SReal_mult 1 THEN assume_tac 1);
by (thin_tac "inverse t : SReal" 1);
-by (auto_tac (claset() addSDs [bspec],simpset() addsimps [hrabs_mult]));
+by (auto_tac (claset() addSDs [bspec], simpset() addsimps [hrabs_mult]));
by (dtac hrabs_mult_less 1 THEN assume_tac 1);
by (dtac (hypreal_not_refl2 RS not_sym) 1);
by (auto_tac (claset() addSDs [hypreal_mult_inverse],
- simpset() addsimps [hrabs_mult] @ hypreal_mult_ac));
+ simpset() addsimps [hrabs_mult] @ hypreal_mult_ac));
qed "Infinitesimal_HFinite_mult";
Goal "[| x : Infinitesimal; y : HFinite |] \
@@ -352,25 +346,20 @@
(*** rather long proof ***)
Goalw [HInfinite_def,Infinitesimal_def]
- "x: HInfinite ==> inverse x: Infinitesimal";
+ "x: HInfinite ==> inverse x: Infinitesimal";
by (Auto_tac);
by (eres_inst_tac [("x","inverse r")] ballE 1);
by (rtac (hrabs_inverse RS ssubst) 1);
-by (etac (((hypreal_inverse_gt_zero RS hypreal_less_trans)
- RS hypreal_not_refl2 RS not_sym) RS (hrabs_not_zero_iff
- RS iffD2)) 1 THEN assume_tac 1);
by (forw_inst_tac [("x1","r"),("R3.0","abs x")]
(hypreal_inverse_gt_zero RS hypreal_less_trans) 1);
by (assume_tac 1);
by (forw_inst_tac [("s","abs x"),("t","0")]
(hypreal_not_refl2 RS not_sym) 1);
by (dtac ((hypreal_inverse_inverse RS sym) RS subst) 1);
-by (rotate_tac 2 1 THEN assume_tac 1);
by (dres_inst_tac [("x","abs x")] hypreal_inverse_gt_zero 1);
by (rtac (hypreal_inverse_less_iff RS ssubst) 1);
by (auto_tac (claset() addSDs [SReal_inverse],
- simpset() addsimps [hypreal_not_refl2 RS not_sym,
- hypreal_less_not_refl]));
+ simpset() addsimps [hypreal_not_refl2 RS not_sym, hypreal_less_not_refl]));
qed "HInfinite_inverse_Infinitesimal";
Goalw [HInfinite_def]
@@ -904,20 +893,20 @@
qed "inf_close_hypreal_of_real_not_zero";
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
-\ ==> x : HFinite - Infinitesimal";
+\ ==> x : HFinite - Infinitesimal";
by (auto_tac (claset() addIs [inf_close_sym RSN (2,inf_close_HFinite)],
simpset() addsimps [mem_infmal_iff]));
by (dtac inf_close_trans3 1 THEN assume_tac 1);
by (blast_tac (claset() addDs [inf_close_sym]) 1);
qed "HFinite_diff_Infinitesimal_inf_close";
-Goal "[| y ~= 0; y: Infinitesimal; \
-\ x*inverse(y) : HFinite \
-\ |] ==> x : Infinitesimal";
+(*The premise y~=0 is essential; otherwise x/y =0 and we lose the
+ HFinite premise.*)
+Goal "[| y ~= 0; y: Infinitesimal; x/y : HFinite |] ==> x : Infinitesimal";
by (dtac Infinitesimal_HFinite_mult2 1);
by (assume_tac 1);
-by (asm_full_simp_tac (simpset()
- addsimps [hypreal_mult_assoc]) 1);
+by (asm_full_simp_tac
+ (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1);
qed "Infinitesimal_ratio";
(*------------------------------------------------------------------
@@ -928,7 +917,7 @@
Uniqueness: Two infinitely close reals are equal
------------------------------------------------------------------*)
-Goal "[|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
+Goal "[|x: SReal; y: SReal|] ==> (x @= y) = (x = y)";
by (auto_tac (claset(),simpset() addsimps [inf_close_refl]));
by (rewrite_goals_tac [inf_close_def]);
by (dres_inst_tac [("x","y")] SReal_minus 1);
@@ -1203,7 +1192,6 @@
Goal "[| x : HFinite; x ~: Infinitesimal |] ==> inverse x : HFinite";
by (cut_inst_tac [("x","inverse x")] HInfinite_HFinite_disj 1);
-by (forward_tac [not_Infinitesimal_not_zero RS hypreal_inverse_inverse] 1);
by (auto_tac (claset() addSDs [HInfinite_inverse_Infinitesimal],simpset()));
qed "HFinite_inverse";
@@ -1215,15 +1203,16 @@
Goal "x ~: Infinitesimal ==> inverse(x) : HFinite";
by (dtac HInfinite_diff_HFinite_Infinitesimal_disj 1);
by (blast_tac (claset() addIs [HFinite_inverse,
- HInfinite_inverse_Infinitesimal,
- Infinitesimal_subset_HFinite RS subsetD]) 1);
+ HInfinite_inverse_Infinitesimal,
+ Infinitesimal_subset_HFinite RS subsetD]) 1);
qed "Infinitesimal_inverse_HFinite";
Goal "x : HFinite - Infinitesimal ==> inverse x : HFinite - Infinitesimal";
by (auto_tac (claset() addIs [Infinitesimal_inverse_HFinite],simpset()));
by (dtac Infinitesimal_HFinite_mult2 1);
-by (auto_tac (claset() addSDs [not_Infinitesimal_not_zero,
- hypreal_mult_inverse],simpset()));
+by (auto_tac (claset() addSDs [not_Infinitesimal_not_zero,
+ hypreal_mult_inverse],
+ simpset()));
qed "HFinite_not_Infinitesimal_inverse";
Goal "[| x @= y; y : HFinite - Infinitesimal |] \
@@ -2075,14 +2064,14 @@
(hypreal_of_real_less_iff RS iffD1) RSN(2,impE)) 1);
by (assume_tac 2);
by (asm_full_simp_tac (simpset() addsimps
- [real_not_refl2 RS not_sym RS hypreal_of_real_inverse RS sym,
+ [hypreal_of_real_inverse RS sym,
rename_numerals real_of_posnat_gt_zero,hypreal_of_real_zero,
hypreal_of_real_of_posnat]) 1);
by (auto_tac (claset() addSDs [reals_Archimedean],
simpset() addsimps [SReal_iff,hypreal_of_real_zero RS sym]));
by (dtac (hypreal_of_real_less_iff RS iffD1) 1);
by (asm_full_simp_tac (simpset() addsimps
- [real_not_refl2 RS not_sym RS hypreal_of_real_inverse RS sym,
+ [hypreal_of_real_inverse RS sym,
rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1);
by (blast_tac (claset() addIs [hypreal_less_trans]) 1);
qed "lemma_Infinitesimal2";
--- a/src/HOL/Real/Hyperreal/NatStar.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/NatStar.ML Fri Dec 15 17:41:38 2000 +0100
@@ -313,11 +313,9 @@
hypreal_minus]));
qed "starfunNat_minus";
-Goal "ALL x. f x ~= 0 ==> \
-\ inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
+Goal "inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset(),simpset() addsimps [starfunNat,
- hypreal_inverse]));
+by (auto_tac (claset(), simpset() addsimps [starfunNat, hypreal_inverse]));
qed "starfunNat_inverse";
(*--------------------------------------------------------
@@ -359,19 +357,6 @@
simpset() addsimps [starfunNat_add RS sym]));
qed "starfunNat_add_inf_close";
-(*-------------------------------------------------------------------
- A few more theorems involving NS extension of real sequences
- See analogous theorems for starfun- NS extension of f::real=>real
- ------------------------------------------------------------------*)
-Goal
- "!!f. (*fNat* f) x ~= 0 ==> \
-\ inverse ((*fNat* f) x) = (*fNat* (%x. inverse (f x))) x";
-by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
-by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
- addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [starfunNat,hypreal_inverse,
- hypreal_zero_def]));
-qed "starfunNat_inverse2";
(*-----------------------------------------------------------------
Example of transfer of a property from reals to hyperreals
--- a/src/HOL/Real/Hyperreal/SEQ.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/SEQ.ML Fri Dec 15 17:41:38 2000 +0100
@@ -26,47 +26,47 @@
(*** LIMSEQ ***)
Goalw [LIMSEQ_def]
- "!!X. X ----> L ==> \
+ "X ----> L ==> \
\ ALL r. #0 < r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r)";
by (Asm_simp_tac 1);
qed "LIMSEQD1";
Goalw [LIMSEQ_def]
- "!!X. [| X ----> L; #0 < r|] ==> \
+ "[| X ----> L; #0 < r|] ==> \
\ EX no. ALL n. no <= n --> abs(X n + -L) < r";
by (Asm_simp_tac 1);
qed "LIMSEQD2";
Goalw [LIMSEQ_def]
- "!!X. ALL r. #0 < r --> (EX no. ALL n. \
+ "ALL r. #0 < r --> (EX no. ALL n. \
\ no <= n --> abs(X n + -L) < r) ==> X ----> L";
by (Asm_simp_tac 1);
qed "LIMSEQI";
Goalw [LIMSEQ_def]
- "!!X. (X ----> L) = \
+ "(X ----> L) = \
\ (ALL r. #0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))";
by (Simp_tac 1);
qed "LIMSEQ_iff";
(*** NSLIMSEQ ***)
Goalw [NSLIMSEQ_def]
- "!!X. X ----NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L";
+ "X ----NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L";
by (Asm_simp_tac 1);
qed "NSLIMSEQD1";
Goalw [NSLIMSEQ_def]
- "!!X. [| X ----NS> L; N: HNatInfinite |] ==> (*fNat* X) N @= hypreal_of_real L";
+ "[| X ----NS> L; N: HNatInfinite |] ==> (*fNat* X) N @= hypreal_of_real L";
by (Asm_simp_tac 1);
qed "NSLIMSEQD2";
Goalw [NSLIMSEQ_def]
- "!!X. ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X ----NS> L";
+ "ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X ----NS> L";
by (Asm_simp_tac 1);
qed "NSLIMSEQI";
Goalw [NSLIMSEQ_def]
- "!!X. (X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
+ "(X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)";
by (Simp_tac 1);
qed "NSLIMSEQ_iff";
@@ -74,7 +74,7 @@
LIMSEQ ==> NSLIMSEQ
---------------------------------------*)
Goalw [LIMSEQ_def,NSLIMSEQ_def]
- "!!X. X ----> L ==> X ----NS> L";
+ "X ----> L ==> X ----NS> L";
by (auto_tac (claset(),simpset() addsimps
[HNatInfinite_FreeUltrafilterNat_iff]));
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
@@ -140,7 +140,7 @@
qed "FreeUltrafilterNat_NSLIMSEQ";
(* thus, the sequence defines an infinite hypernatural! *)
-Goal "!!f. ALL n. n <= f n \
+Goal "ALL n. n <= f n \
\ ==> Abs_hypnat (hypnatrel ^^ {f}) : HNatInfinite";
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]);
@@ -156,7 +156,7 @@
addIs [real_less_irrefl], simpset()));
val lemmaLIM2 = result();
-Goal "!!f. [| #0 < r; ALL n. r <= abs (X (f n) + - L); \
+Goal "[| #0 < r; ALL n. r <= abs (X (f n) + - L); \
\ (*fNat* X) (Abs_hypnat (hypnatrel ^^ {f})) + \
\ - hypreal_of_real L @= 0 |] ==> False";
by (auto_tac (claset(),simpset() addsimps [starfunNat,
@@ -174,7 +174,7 @@
val lemmaLIM3 = result();
Goalw [LIMSEQ_def,NSLIMSEQ_def]
- "!!X. X ----NS> L ==> X ----> L";
+ "X ----NS> L ==> X ----> L";
by (rtac ccontr 1 THEN Asm_full_simp_tac 1);
by (Step_tac 1);
(* skolemization step *)
@@ -203,39 +203,39 @@
qed "LIMSEQ_const";
Goalw [NSLIMSEQ_def]
- "!!X. [| X ----NS> a; Y ----NS> b |] \
+ "[| X ----NS> a; Y ----NS> b |] \
\ ==> (%n. X n + Y n) ----NS> a + b";
by (auto_tac (claset() addIs [inf_close_add],
simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add]));
qed "NSLIMSEQ_add";
-Goal "!!X. [| X ----> a; Y ----> b |] \
+Goal "[| X ----> a; Y ----> b |] \
\ ==> (%n. X n + Y n) ----> a + b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
NSLIMSEQ_add]) 1);
qed "LIMSEQ_add";
Goalw [NSLIMSEQ_def]
- "!!X. [| X ----NS> a; Y ----NS> b |] \
+ "[| X ----NS> a; Y ----NS> b |] \
\ ==> (%n. X n * Y n) ----NS> a * b";
by (auto_tac (claset() addSIs [starfunNat_mult_HFinite_inf_close],
simpset() addsimps [hypreal_of_real_mult]));
qed "NSLIMSEQ_mult";
-Goal "!!X. [| X ----> a; Y ----> b |] \
+Goal "[| X ----> a; Y ----> b |] \
\ ==> (%n. X n * Y n) ----> a * b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
NSLIMSEQ_mult]) 1);
qed "LIMSEQ_mult";
Goalw [NSLIMSEQ_def]
- "!!X. X ----NS> a ==> (%n. -(X n)) ----NS> -a";
+ "X ----NS> a ==> (%n. -(X n)) ----NS> -a";
by (auto_tac (claset() addIs [inf_close_minus],
simpset() addsimps [starfunNat_minus RS sym,
hypreal_of_real_minus]));
qed "NSLIMSEQ_minus";
-Goal "!!X. X ----> a ==> (%n. -(X n)) ----> -a";
+Goal "X ----> a ==> (%n. -(X n)) ----> -a";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
NSLIMSEQ_minus]) 1);
qed "LIMSEQ_minus";
@@ -250,69 +250,61 @@
by (Asm_full_simp_tac 1);
qed "NSLIMSEQ_minus_cancel";
-Goal "!!X. [| X ----NS> a; Y ----NS> b |] \
+Goal "[| X ----NS> a; Y ----NS> b |] \
\ ==> (%n. X n + -Y n) ----NS> a + -b";
by (dres_inst_tac [("X","Y")] NSLIMSEQ_minus 1);
by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_add]));
qed "NSLIMSEQ_add_minus";
-Goal "!!X. [| X ----> a; Y ----> b |] \
+Goal "[| X ----> a; Y ----> b |] \
\ ==> (%n. X n + -Y n) ----> a + -b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
NSLIMSEQ_add_minus]) 1);
qed "LIMSEQ_add_minus";
-goalw SEQ.thy [real_diff_def]
- "!!X. [| X ----> a; Y ----> b |] \
-\ ==> (%n. X n - Y n) ----> a - b";
+Goalw [real_diff_def]
+ "[| X ----> a; Y ----> b |] ==> (%n. X n - Y n) ----> a - b";
by (blast_tac (claset() addIs [LIMSEQ_add_minus]) 1);
qed "LIMSEQ_diff";
-goalw SEQ.thy [real_diff_def]
- "!!X. [| X ----NS> a; Y ----NS> b |] \
-\ ==> (%n. X n - Y n) ----NS> a - b";
+Goalw [real_diff_def]
+ "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n - Y n) ----NS> a - b";
by (blast_tac (claset() addIs [NSLIMSEQ_add_minus]) 1);
qed "NSLIMSEQ_diff";
(*---------------------------------------------------------------
- Proof is exactly same as that of NSLIM_inverse except
- for starfunNat_inverse2 --- would not be the case if we
- had generalised net theorems for example. Not our
- real concern though.
+ Proof is like that of NSLIM_inverse.
--------------------------------------------------------------*)
Goalw [NSLIMSEQ_def]
- "!!X. [| X ----NS> a; a ~= #0 |] \
-\ ==> (%n. inverse(X n)) ----NS> inverse(a)";
-by (Step_tac 1);
-by (dtac bspec 1 THEN auto_tac (claset(),simpset()
- addsimps [hypreal_of_real_not_zero_iff RS sym,
- hypreal_of_real_inverse RS sym]));
-by (forward_tac [inf_close_hypreal_of_real_not_zero] 1
- THEN assume_tac 1);
-by (auto_tac (claset() addSEs [(starfunNat_inverse2 RS subst),
- inf_close_inverse,hypreal_of_real_HFinite_diff_Infinitesimal],
- simpset()));
+ "[| X ----NS> a; a ~= #0 |] ==> (%n. inverse(X n)) ----NS> inverse(a)";
+by (Clarify_tac 1);
+by (dtac bspec 1);
+by (auto_tac (claset(),
+ simpset() addsimps [hypreal_of_real_not_zero_iff RS sym,
+ hypreal_of_real_inverse RS sym]));
+by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 THEN assume_tac 1);
+by (dtac hypreal_of_real_HFinite_diff_Infinitesimal 1);
+by (stac (starfunNat_inverse RS sym) 1);
+by (auto_tac (claset() addSEs [inf_close_inverse],
+ simpset() addsimps [hypreal_of_real_zero_iff]));
qed "NSLIMSEQ_inverse";
+
(*------ Standard version of theorem -------*)
-Goal
- "!!X. [| X ----> a; a ~= #0 |] \
-\ ==> (%n. inverse(X n)) ----> inverse(a)";
+Goal "[| X ----> a; a ~= #0 |] ==> (%n. inverse(X n)) ----> inverse(a)";
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_inverse,
LIMSEQ_NSLIMSEQ_iff]) 1);
qed "LIMSEQ_inverse";
(* trivially proved *)
-Goal
- "!!X. [| X ----NS> a; Y ----NS> b; b ~= #0 |] \
-\ ==> (%n. (X n) * inverse(Y n)) ----NS> a*inverse(b)";
+Goal "[| X ----NS> a; Y ----NS> b; b ~= #0 |] \
+\ ==> (%n. (X n) * inverse(Y n)) ----NS> a*inverse(b)";
by (blast_tac (claset() addDs [NSLIMSEQ_inverse,NSLIMSEQ_mult]) 1);
qed "NSLIMSEQ_mult_inverse";
(* let's give a standard proof of theorem *)
-Goal
- "!!X. [| X ----> a; Y ----> b; b ~= #0 |] \
-\ ==> (%n. (X n) * inverse(Y n)) ----> a*inverse(b)";
+Goal "[| X ----> a; Y ----> b; b ~= #0 |] \
+\ ==> (%n. (X n) * inverse(Y n)) ----> a*inverse(b)";
by (blast_tac (claset() addDs [LIMSEQ_inverse,LIMSEQ_mult]) 1);
qed "LIMSEQ_mult_inverse";
@@ -320,14 +312,12 @@
Uniqueness of limit
----------------------------------------------*)
Goalw [NSLIMSEQ_def]
- "!!X. [| X ----NS> a; X ----NS> b |] \
-\ ==> a = b";
+ "[| X ----NS> a; X ----NS> b |] ==> a = b";
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1));
by (auto_tac (claset() addDs [inf_close_trans3], simpset()));
qed "NSLIMSEQ_unique";
-Goal "!!X. [| X ----> a; X ----> b |] \
-\ ==> a = b";
+Goal "[| X ----> a; X ----> b |] ==> a = b";
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff,
NSLIMSEQ_unique]) 1);
qed "LIMSEQ_unique";
@@ -335,11 +325,11 @@
(*-----------------------------------------------------------------
theorems about nslim and lim
----------------------------------------------------------------*)
-Goalw [lim_def] "!!X. X ----> L ==> lim X = L";
+Goalw [lim_def] "X ----> L ==> lim X = L";
by (blast_tac (claset() addIs [LIMSEQ_unique]) 1);
qed "limI";
-Goalw [nslim_def] "!!X. X ----NS> L ==> nslim X = L";
+Goalw [nslim_def] "X ----NS> L ==> nslim X = L";
by (blast_tac (claset() addIs [NSLIMSEQ_unique]) 1);
qed "nslimI";
@@ -351,37 +341,37 @@
Convergence
-----------------------------------------------------------------*)
Goalw [convergent_def]
- "!!f. convergent X ==> EX L. (X ----> L)";
+ "convergent X ==> EX L. (X ----> L)";
by (assume_tac 1);
qed "convergentD";
Goalw [convergent_def]
- "!!f. (X ----> L) ==> convergent X";
+ "(X ----> L) ==> convergent X";
by (Blast_tac 1);
qed "convergentI";
Goalw [NSconvergent_def]
- "!!f. NSconvergent X ==> EX L. (X ----NS> L)";
+ "NSconvergent X ==> EX L. (X ----NS> L)";
by (assume_tac 1);
qed "NSconvergentD";
Goalw [NSconvergent_def]
- "!!f. (X ----NS> L) ==> NSconvergent X";
+ "(X ----NS> L) ==> NSconvergent X";
by (Blast_tac 1);
qed "NSconvergentI";
Goalw [convergent_def,NSconvergent_def]
- "convergent X = NSconvergent X";
+ "convergent X = NSconvergent X";
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1);
qed "convergent_NSconvergent_iff";
Goalw [NSconvergent_def,nslim_def]
- "NSconvergent X = (X ----NS> nslim X)";
+ "NSconvergent X = (X ----NS> nslim X)";
by (auto_tac (claset() addIs [someI], simpset()));
qed "NSconvergent_NSLIMSEQ_iff";
Goalw [convergent_def,lim_def]
- "convergent X = (X ----> lim X)";
+ "convergent X = (X ----> lim X)";
by (auto_tac (claset() addIs [someI], simpset()));
qed "convergent_LIMSEQ_iff";
@@ -414,20 +404,20 @@
qed "monoseq_Suc";
Goalw [monoseq_def]
- "!!X. ALL m n. m <= n --> X m <= X n ==> monoseq X";
+ "ALL m n. m <= n --> X m <= X n ==> monoseq X";
by (Blast_tac 1);
qed "monoI1";
Goalw [monoseq_def]
- "!!X. ALL m n. m <= n --> X n <= X m ==> monoseq X";
+ "ALL m n. m <= n --> X n <= X m ==> monoseq X";
by (Blast_tac 1);
qed "monoI2";
-Goal "!!X. ALL n. X n <= X (Suc n) ==> monoseq X";
+Goal "ALL n. X n <= X (Suc n) ==> monoseq X";
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
qed "mono_SucI1";
-Goal "!!X. ALL n. X (Suc n) <= X n ==> monoseq X";
+Goal "ALL n. X (Suc n) <= X n ==> monoseq X";
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1);
qed "mono_SucI2";
@@ -435,12 +425,12 @@
Bounded Sequence
------------------------------------------------------------------*)
Goalw [Bseq_def]
- "!!X. Bseq X ==> EX K. #0 < K & (ALL n. abs(X n) <= K)";
+ "Bseq X ==> EX K. #0 < K & (ALL n. abs(X n) <= K)";
by (assume_tac 1);
qed "BseqD";
Goalw [Bseq_def]
- "!!X. [| #0 < K; ALL n. abs(X n) <= K |] \
+ "[| #0 < K; ALL n. abs(X n) <= K |] \
\ ==> Bseq X";
by (Blast_tac 1);
qed "BseqI";
@@ -479,13 +469,13 @@
qed "Bseq_iff1a";
Goalw [NSBseq_def]
- "!!X. [| NSBseq X; N: HNatInfinite |] \
+ "[| NSBseq X; N: HNatInfinite |] \
\ ==> (*fNat* X) N : HFinite";
by (Blast_tac 1);
qed "NSBseqD";
Goalw [NSBseq_def]
- "!!X. ALL N: HNatInfinite. (*fNat* X) N : HFinite \
+ "ALL N: HNatInfinite. (*fNat* X) N : HFinite \
\ ==> NSBseq X";
by (assume_tac 1);
qed "NSBseqI";
@@ -524,21 +514,21 @@
is not what we want (read useless!)
-------------------------------------------------------------------*)
-Goal "!!X. ALL K. #0 < K --> (EX n. K < abs (X n)) \
+Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
\ ==> ALL N. EX n. real_of_posnat N < abs (X n)";
by (Step_tac 1);
by (cut_inst_tac [("n","N")] (rename_numerals real_of_posnat_gt_zero) 1);
by (Blast_tac 1);
val lemmaNSBseq = result();
-Goal "!!X. ALL K. #0 < K --> (EX n. K < abs (X n)) \
+Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \
\ ==> EX f. ALL N. real_of_posnat N < abs (X (f N))";
by (dtac lemmaNSBseq 1);
by (dtac choice 1);
by (Blast_tac 1);
val lemmaNSBseq2 = result();
-Goal "!!X. ALL N. real_of_posnat N < abs (X (f N)) \
+Goal "ALL N. real_of_posnat N < abs (X (f N)) \
\ ==> Abs_hypreal(hyprel^^{X o f}) : HInfinite";
by (auto_tac (claset(),simpset() addsimps
[HInfinite_FreeUltrafilterNat_iff,o_def]));
@@ -615,14 +605,14 @@
-----------------------------------------------------------------------*)
(* easier --- nonstandard version - no existential as usual *)
Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def]
- "!!X. NSconvergent X ==> NSBseq X";
+ "NSconvergent X ==> NSBseq X";
by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS
(inf_close_sym RSN (2,inf_close_HFinite))]) 1);
qed "NSconvergent_NSBseq";
(* standard version - easily now proved using *)
(* equivalence of NS and standard definitions *)
-Goal "!!X. convergent X ==> Bseq X";
+Goal "convergent X ==> Bseq X";
by (asm_full_simp_tac (simpset() addsimps [NSconvergent_NSBseq,
convergent_NSconvergent_iff,Bseq_NSBseq_iff]) 1);
qed "convergent_Bseq";
@@ -650,14 +640,14 @@
(* nonstandard version of premise will be *)
(* handy when we work in NS universe *)
-Goal "!!X. NSBseq X ==> \
+Goal "NSBseq X ==> \
\ EX U. isUb (UNIV::real set) {x. EX n. X n = x} U";
by (asm_full_simp_tac (simpset() addsimps
[Bseq_NSBseq_iff RS sym,Bseq_isUb]) 1);
qed "NSBseq_isUb";
Goal
- "!!X. NSBseq X ==> \
+ "NSBseq X ==> \
\ EX U. isLub (UNIV::real set) {x. EX n. X n = x} U";
by (asm_full_simp_tac (simpset() addsimps
[Bseq_NSBseq_iff RS sym,Bseq_isLub]) 1);
@@ -682,7 +672,7 @@
equivalent nonstandard form if needed!
-------------------------------------------------------------------*)
Goalw [LIMSEQ_def]
- "!!X. ALL n. m <= n --> X n = X m \
+ "ALL n. m <= n --> X n = X m \
\ ==> EX L. (X ----> L)";
by (res_inst_tac [("x","X m")] exI 1);
by (Step_tac 1);
@@ -693,7 +683,7 @@
qed "Bmonoseq_LIMSEQ";
(* Now same theorem in terms of NS limit *)
-Goal "!!X. ALL n. m <= n --> X n = X m \
+Goal "ALL n. m <= n --> X n = X m \
\ ==> EX L. (X ----NS> L)";
by (auto_tac (claset() addSDs [Bmonoseq_LIMSEQ],
simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]));
@@ -737,7 +727,7 @@
------------------------------------------------------------------*)
Goalw [convergent_def]
- "!!X. [| Bseq X; ALL m n. m <= n --> X m <= X n |] \
+ "[| Bseq X; ALL m n. m <= n --> X m <= X n |] \
\ ==> convergent X";
by (forward_tac [Bseq_isLub] 1);
by (Step_tac 1);
@@ -757,7 +747,7 @@
(* NS version of theorem *)
Goalw [convergent_def]
- "!!X. [| NSBseq X; ALL m n. m <= n --> X m <= X n |] \
+ "[| NSBseq X; ALL m n. m <= n --> X m <= X n |] \
\ ==> NSconvergent X";
by (auto_tac (claset() addIs [Bseq_mono_convergent],
simpset() addsimps [convergent_NSconvergent_iff RS sym,
@@ -765,7 +755,7 @@
qed "NSBseq_mono_NSconvergent";
Goalw [convergent_def]
- "!!X. (convergent X) = (convergent (%n. -(X n)))";
+ "(convergent X) = (convergent (%n. -(X n)))";
by (auto_tac (claset() addDs [LIMSEQ_minus], simpset()));
by (dtac LIMSEQ_minus 1 THEN Auto_tac);
qed "convergent_minus_iff";
@@ -778,7 +768,7 @@
**** main mono theorem ****
-------------------------------*)
Goalw [monoseq_def]
- "!!X. [| Bseq X; monoseq X |] ==> convergent X";
+ "[| Bseq X; monoseq X |] ==> convergent X";
by (Step_tac 1);
by (rtac (convergent_minus_iff RS ssubst) 2);
by (dtac (Bseq_minus_iff RS ssubst) 2);
@@ -793,49 +783,34 @@
Goalw [Bseq_def]
"Bseq X = (EX k x. #0 < k & (ALL n. abs(X(n) + -x) <= k))";
by (Step_tac 1);
+by (res_inst_tac [("x","k + abs(x)")] exI 2);
by (res_inst_tac [("x","K")] exI 1);
by (res_inst_tac [("x","0")] exI 1);
by (Auto_tac);
-by (res_inst_tac [("x","k + abs(x)")] exI 1);
-by (Step_tac 1);
-by (dres_inst_tac [("x","n")] spec 2);
-by (ALLGOALS(arith_tac));
+by (ALLGOALS (dres_inst_tac [("x","n")] spec));
+by (ALLGOALS arith_tac);
qed "Bseq_iff2";
(***--- alternative formulation for boundedness ---***)
-Goal "Bseq X = (EX k N. #0 < k & (ALL n. \
-\ abs(X(n) + -X(N)) <= k))";
+Goal "Bseq X = (EX k N. #0 < k & (ALL n. abs(X(n) + -X(N)) <= k))";
by (Step_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Bseq_def]) 1);
by (Step_tac 1);
by (res_inst_tac [("x","K + abs(X N)")] exI 1);
by (Auto_tac);
-by (etac abs_add_pos_gt_zero 1);
+by (arith_tac 1);
by (res_inst_tac [("x","N")] exI 1);
by (Step_tac 1);
-by (res_inst_tac [("j","abs(X n) + abs (X N)")]
- real_le_trans 1);
-by (auto_tac (claset() addIs [abs_triangle_minus_ineq,
- real_add_le_mono1], simpset() addsimps [Bseq_iff2]));
+by (dres_inst_tac [("x","n")] spec 1);
+by (arith_tac 1);
+by (auto_tac (claset(), simpset() addsimps [Bseq_iff2]));
qed "Bseq_iff3";
-val real_not_leE = CLAIM "~ m <= n ==> n < (m::real)";
-
Goalw [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f";
by (res_inst_tac [("x","(abs(k) + abs(K)) + #1")] exI 1);
by (Auto_tac);
-by (arith_tac 1);
-by (case_tac "#0 <= f n" 1);
-by (auto_tac (claset(),simpset() addsimps [abs_eqI1,
- real_not_leE RS abs_minus_eqI2]));
-by (res_inst_tac [("j","abs K")] real_le_trans 1);
-by (res_inst_tac [("j","abs k")] real_le_trans 3);
-by (auto_tac (claset() addSIs [rename_numerals real_le_add_order] addDs
- [real_le_trans], simpset()
- addsimps [abs_ge_zero,rename_numerals real_zero_less_one,abs_eqI1]));
-by (subgoal_tac "k < 0" 1);
-by (rtac (real_not_leE RSN (2,real_le_less_trans)) 2);
-by (auto_tac (claset(),simpset() addsimps [abs_minus_eqI2]));
+by (dres_inst_tac [("x","n")] spec 2);
+by (ALLGOALS arith_tac);
qed "BseqI2";
(*-------------------------------------------------------------------
@@ -844,10 +819,10 @@
(*-------------------------------
Standard def => NS def
-------------------------------*)
-Goal "!!x. Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \
+Goal "Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \
\ ==> {n. M <= x n} : FreeUltrafilterNat";
-by (auto_tac (claset(),simpset() addsimps
- [HNatInfinite_FreeUltrafilterNat_iff]));
+by (auto_tac (claset(),
+ simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff]));
by (dres_inst_tac [("x","M")] spec 1);
by (ultra_tac (claset(),simpset() addsimps [less_imp_le]) 1);
val lemmaCauchy1 = result();
@@ -924,7 +899,7 @@
-------------------------------------------------------*)
(***------------- VARIOUS LEMMAS --------------***)
-Goal "!!X. ALL n. M <= n --> abs (X M + - X n) < (#1::real) \
+Goal "ALL n. M <= n --> abs (X M + - X n) < (#1::real) \
\ ==> ALL n. M <= n --> abs(X n) < #1 + abs(X M)";
by (Step_tac 1);
by (dtac spec 1 THEN Auto_tac);
@@ -1021,6 +996,7 @@
by (res_inst_tac [("x","abs(X m)")] exI 3);
by (auto_tac (claset() addSEs [lemma_Nat_covered],
simpset()));
+by (ALLGOALS arith_tac);
qed "Cauchy_Bseq";
(*------------------------------------------------
@@ -1069,7 +1045,7 @@
starting with the limit comparison property for sequences
-----------------------------------------------------------------*)
Goalw [NSLIMSEQ_def]
- "!!f. [| f ----NS> l; g ----NS> m; \
+ "[| f ----NS> l; g ----NS> m; \
\ EX N. ALL n. N <= n --> f(n) <= g(n) \
\ |] ==> l <= m";
by (Step_tac 1);
@@ -1397,9 +1373,9 @@
-- Show that every sequence contains a monotonic subsequence
Goal "EX f. subseq f & monoseq (%n. s (f n))";
-- Show that a subsequence of a bounded sequence is bounded
-Goal "!!X. Bseq X ==> Bseq (%n. X (f n))";
+Goal "Bseq X ==> Bseq (%n. X (f n))";
-- Show we can take subsequential terms arbitrarily far
up a sequence
-Goal "!!f. subseq f ==> n <= f(n)";
-Goal "!!f. subseq f ==> EX n. N1 <= n & N2 <= f(n)";
+Goal "subseq f ==> n <= f(n)";
+Goal "subseq f ==> EX n. N1 <= n & N2 <= f(n)";
---------------------------------------------------------------***)
--- a/src/HOL/Real/Hyperreal/Star.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Star.ML Fri Dec 15 17:41:38 2000 +0100
@@ -12,7 +12,7 @@
referee for the JCM Paper: let f(x) be least y such
that Q(x,y)
*)
-Goal "!!Q. ALL x. EX y. Q x y ==> EX (f :: nat => nat). ALL x. Q x (f x)";
+Goal "ALL x. EX y. Q x y ==> EX (f :: nat => nat). ALL x. Q x (f x)";
by (res_inst_tac [("x","%x. LEAST y. Q x y")] exI 1);
by (blast_tac (claset() addIs [LeastI]) 1);
qed "no_choice";
@@ -65,7 +65,7 @@
by (Step_tac 1);
qed "set_diff_iff2";
-Goal "!!x. x ~: *s* F ==> x : *s* (- F)";
+Goal "x ~: *s* F ==> x : *s* (- F)";
by (auto_tac (claset(),simpset() addsimps [STAR_Compl]));
qed "STAR_mem_Compl";
@@ -74,12 +74,12 @@
[set_diff_iff2,STAR_Int,STAR_Compl]));
qed "STAR_diff";
-Goalw [starset_def] "!!A. A <= B ==> *s* A <= *s* B";
+Goalw [starset_def] "A <= B ==> *s* A <= *s* B";
by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
qed "STAR_subset";
Goalw [starset_def,hypreal_of_real_def]
- "!!A. a : A ==> hypreal_of_real a : *s* A";
+ "a : A ==> hypreal_of_real a : *s* A";
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],simpset()));
qed "STAR_mem";
@@ -98,7 +98,7 @@
by (Auto_tac);
qed "STAR_hypreal_of_real_Int";
-Goal "!!x. x ~: hypreal_of_real `` A ==> ALL y: A. x ~= hypreal_of_real y";
+Goal "x ~: hypreal_of_real `` A ==> ALL y: A. x ~= hypreal_of_real y";
by (Auto_tac);
qed "lemma_not_hyprealA";
@@ -107,7 +107,7 @@
qed "lemma_Compl_eq";
Goalw [starset_def]
- "!!M. ALL n. (X n) ~: M \
+ "ALL n. (X n) ~: M \
\ ==> Abs_hypreal(hyprel^^{X}) ~: *s* M";
by (Auto_tac THEN rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
by (Auto_tac);
@@ -120,14 +120,14 @@
qed "STAR_singleton";
Addsimps [STAR_singleton];
-Goal "!!x. x ~: F ==> hypreal_of_real x ~: *s* F";
+Goal "x ~: F ==> hypreal_of_real x ~: *s* F";
by (auto_tac (claset(),simpset() addsimps
[starset_def,hypreal_of_real_def]));
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
by (Auto_tac);
qed "STAR_not_mem";
-Goal "!!x. [| x : *s* A; A <= B |] ==> x : *s* B";
+Goal "[| x : *s* A; A <= B |] ==> x : *s* B";
by (blast_tac (claset() addDs [STAR_subset]) 1);
qed "STAR_subset_closed";
@@ -137,7 +137,7 @@
-----------------------------------------------------------------*)
Goalw [starset_n_def,starset_def]
- "!!A. ALL n. (As n = A) ==> *sn* As = *s* A";
+ "ALL n. (As n = A) ==> *sn* As = *s* A";
by (Auto_tac);
qed "starset_n_starset";
@@ -152,7 +152,7 @@
(*----------------------------------------------------------------*)
Goalw [starfun_n_def,starfun_def]
- "!!A. ALL n. (F n = f) ==> *fn* F = *f* f";
+ "ALL n. (F n = f) ==> *fn* F = *f* f";
by (Auto_tac);
qed "starfun_n_starfun";
@@ -181,7 +181,7 @@
by (TRYALL(arith_tac));
qed "hrabs_is_starext_rabs";
-Goal "!!z. [| X: Rep_hypreal z; Y: Rep_hypreal z |] \
+Goal "[| X: Rep_hypreal z; Y: Rep_hypreal z |] \
\ ==> {n. X n = Y n} : FreeUltrafilterNat";
by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
by (Auto_tac THEN Fuf_tac 1);
@@ -224,10 +224,14 @@
(*--------------------------------------------
subtraction: ( *f ) + -( *g ) = *(f + -g)
-------------------------------------------*)
+
+Goal "- (*f* f) x = (*f* (%x. - f x)) x";
+by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
+by (auto_tac (claset(),simpset() addsimps [starfun, hypreal_minus]));
+qed "starfun_minus";
+
Goal "(*f* f) xa + -(*f* g) xa = (*f* (%x. f x + -g x)) xa";
-by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_minus,hypreal_add]));
+by (simp_tac (simpset() addsimps [starfun_minus, starfun_add]) 1);
qed "starfun_add_minus";
Goalw [hypreal_diff_def,real_diff_def]
@@ -260,17 +264,11 @@
Addsimps [starfun_const_fun];
-Goal "- (*f* f) x = (*f* (%x. - f x)) x";
-by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_minus]));
-qed "starfun_minus";
-
(*----------------------------------------------------
the NS extension of the identity function
----------------------------------------------------*)
-Goal "!!x. x @= hypreal_of_real a ==> (*f* (%x. x)) x @= hypreal_of_real a";
+Goal "x @= hypreal_of_real a ==> (*f* (%x. x)) x @= hypreal_of_real a";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun]));
qed "starfun_Idfun_inf_close";
@@ -295,7 +293,7 @@
Any nonstandard extension is in fact the *-function
----------------------------------------------------------------------*)
-Goalw [is_starext_def] "!!f. is_starext F f ==> F = *f* f";
+Goalw [is_starext_def] "is_starext F f ==> F = *f* f";
by (rtac ext 1);
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (dres_inst_tac [("x","x")] spec 1);
@@ -338,7 +336,7 @@
hypreal_of_real_def,hypreal_add]));
qed "starfun_lambda_cancel2";
-Goal "!!f. [| (*f* f) xa @= l; (*f* g) xa @= m; \
+Goal "[| (*f* f) xa @= l; (*f* g) xa @= m; \
\ l: HFinite; m: HFinite \
\ |] ==> (*f* (%x. f x * g x)) xa @= l * m";
by (dtac inf_close_mult_HFinite 1);
@@ -347,7 +345,7 @@
simpset() addsimps [starfun_mult]));
qed "starfun_mult_HFinite_inf_close";
-Goal "!!f. [| (*f* f) xa @= l; (*f* g) xa @= m \
+Goal "[| (*f* f) xa @= l; (*f* g) xa @= m \
\ |] ==> (*f* (%x. f x + g x)) xa @= l + m";
by (auto_tac (claset() addIs [inf_close_add],
simpset() addsimps [starfun_add RS sym]));
@@ -367,61 +365,41 @@
(is_starext_starfun_iff RS iffD1) RS sym) 1);
qed "starfun_rabs_hrabs";
-Goal "!!x. x ~= 0 ==> (*f* inverse) x = inverse(x)";
+Goal "(*f* inverse) x = inverse(x)";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_inverse,hypreal_zero_def]));
-by (dtac FreeUltrafilterNat_Compl_mem 1);
-by (auto_tac (claset() addEs [FreeUltrafilterNat_subset],simpset()));
+by (auto_tac (claset(),
+ simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def]));
qed "starfun_inverse_inverse";
(* more specifically *)
Goal "(*f* inverse) ehr = inverse (ehr)";
-by (rtac (hypreal_epsilon_not_zero RS starfun_inverse_inverse) 1);
+by (rtac starfun_inverse_inverse 1);
qed "starfun_inverse_epsilon";
-Goal "ALL x. f x ~= 0 ==> \
-\ inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
+Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
-by (auto_tac (claset(),simpset() addsimps [starfun,
- hypreal_inverse]));
+by (auto_tac (claset(),
+ simpset() addsimps [starfun, hypreal_inverse]));
qed "starfun_inverse";
-Goal "(*f* f) x ~= 0 ==> \
-\ inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
+Goalw [hypreal_divide_def,real_divide_def]
+ "(*f* f) xa / (*f* g) xa = (*f* (%x. f x / g x)) xa";
+by (simp_tac (simpset() addsimps [starfun_inverse, starfun_mult]) 1);
+qed "starfun_divide";
+
+Goal "inverse ((*f* f) x) = (*f* (%x. inverse (f x))) x";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
- addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [starfun,hypreal_inverse,
- hypreal_zero_def]));
+ addSDs [FreeUltrafilterNat_Compl_mem],
+ simpset() addsimps [starfun, hypreal_inverse, hypreal_zero_def]));
qed "starfun_inverse2";
-Goal "a ~= hypreal_of_real b ==> \
-\ (*f* (%z. inverse (z + -b))) a = inverse(a + -hypreal_of_real b)";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
- addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [starfun,hypreal_of_real_def,hypreal_add,
- hypreal_minus,hypreal_inverse,rename_numerals
- (real_eq_minus_iff2 RS sym)]));
-qed "starfun_inverse3";
-
-Goal
- "!!f. a + hypreal_of_real b ~= 0 ==> \
-\ (*f* (%z. inverse (z + b))) a = inverse(a + hypreal_of_real b)";
-by (res_inst_tac [("z","a")] eq_Abs_hypreal 1);
-by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
- addSDs [FreeUltrafilterNat_Compl_mem],
- simpset() addsimps [starfun,hypreal_of_real_def,hypreal_add,
- hypreal_inverse,hypreal_zero_def]));
-qed "starfun_inverse4";
-
(*-------------------------------------------------------------
General lemma/theorem needed for proofs in elementary
topology of the reals
------------------------------------------------------------*)
Goalw [starset_def]
- "!!A. (*f* f) x : *s* A ==> x : *s* {x. f x : A}";
+ "(*f* f) x : *s* A ==> x : *s* {x. f x : A}";
by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
by (auto_tac (claset(),simpset() addsimps [starfun]));
by (dres_inst_tac [("x","%n. f (Xa n)")] bspec 1);
--- a/src/HOL/Real/RComplete.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/RComplete.ML Fri Dec 15 17:41:38 2000 +0100
@@ -137,10 +137,6 @@
by (Auto_tac);
qed "lemma_le_swap2";
-Goal "[| #0 < (x::real) + (-X) + #1; x < xa |] ==> #0 < xa + (-X) + #1";
-by (Auto_tac);
-qed "lemma_real_complete1";
-
Goal "[| (x::real) + (-X) + #1 <= S; xa < x |] ==> xa + (-X) + #1 <= S";
by (Auto_tac);
qed "lemma_real_complete2";
@@ -183,7 +179,7 @@
by (ftac isLubD2 1 THEN assume_tac 2);
by (Step_tac 1);
by (Blast_tac 1);
-by (dtac lemma_real_complete1 1 THEN REPEAT(assume_tac 1));
+by (arith_tac 1);
by (stac lemma_le_swap2 1);
by (ftac isLubD2 1 THEN assume_tac 2);
by (Blast_tac 1);
--- a/src/HOL/Real/RealArith.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/RealArith.ML Fri Dec 15 17:41:38 2000 +0100
@@ -8,8 +8,45 @@
Also, common factor cancellation
*)
+(*****????????????????***VERY EARLY! (HOL itself)*********)
+Goal "(number_of w = x+y) = (x+y = number_of w)";
+by Auto_tac;
+qed "number_of_add_reorient";
+AddIffs [number_of_add_reorient];
+
+Goal "(number_of w = x-y) = (x-y = number_of w)";
+by Auto_tac;
+qed "number_of_diff_reorient";
+AddIffs [number_of_diff_reorient];
+
+Goal "(number_of w = x*y) = (x*y = number_of w)";
+by Auto_tac;
+qed "number_of_mult_reorient";
+AddIffs [number_of_mult_reorient];
+
+Goal "(number_of w = x div y) = (x div y = number_of w)";
+by Auto_tac;
+qed "number_of_div_reorient";
+AddIffs [number_of_div_reorient];
+
+Goal "(number_of w = x mod y) = (x mod y = number_of w)";
+by Auto_tac;
+qed "number_of_mod_reorient";
+AddIffs [number_of_mod_reorient];
+
+Goal "(number_of w = x/y) = (x/y = number_of w)";
+by Auto_tac;
+qed "number_of_divide_reorient";
+AddIffs [number_of_divide_reorient];
+
+
(** Division and inverse **)
+Goal "#0/x = (#0::real)";
+by (simp_tac (simpset() addsimps [real_divide_def]) 1);
+qed "real_0_divide";
+Addsimps [real_0_divide];
+
Goal "((#0::real) < inverse x) = (#0 < x)";
by (case_tac "x=#0" 1);
by (asm_simp_tac (HOL_ss addsimps [rename_numerals INVERSE_ZERO]) 1);
@@ -63,6 +100,18 @@
qed "real_divide_1";
Addsimps [real_divide_1];
+Goal "(inverse(x::real) = #0) = (x = #0)";
+by (auto_tac (claset(), simpset() addsimps [rename_numerals INVERSE_ZERO]));
+by (rtac ccontr 1);
+by (blast_tac (claset() addDs [rename_numerals real_inverse_not_zero]) 1);
+qed "real_inverse_zero_iff";
+AddIffs [real_inverse_zero_iff];
+
+Goal "(x/y = #0) = (x=#0 | y=(#0::real))";
+by (auto_tac (claset(), simpset() addsimps [real_divide_def]));
+qed "real_divide_eq_0_iff";
+AddIffs [real_divide_eq_0_iff];
+
(**** Factor cancellation theorems for "real" ****)
@@ -74,6 +123,7 @@
Goal "(-y < -x) = ((x::real) < y)";
by (arith_tac 1);
qed "real_minus_less_minus";
+Addsimps [real_minus_less_minus];
Goal "[| i<j; k < (0::real) |] ==> j*k < i*k";
by (rtac (real_minus_less_minus RS iffD1) 1);
@@ -366,9 +416,21 @@
qed "real_divide_eq_eq";
Addsimps [inst "z" "number_of ?w" real_divide_eq_eq];
+Goal "(m/k = n/k) = (k = #0 | m = (n::real))";
+by (case_tac "k=#0" 1);
+by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1);
+by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq,
+ real_mult_eq_cancel2]) 1);
+qed "real_divide_eq_cancel2";
-(** Moved from RealOrd.ML to use #0 **)
+Goal "(k/m = k/n) = (k = #0 | m = (n::real))";
+by (case_tac "m=#0 | n = #0" 1);
+by (auto_tac (claset(),
+ simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq,
+ real_eq_divide_eq, real_mult_eq_cancel1]));
+qed "real_divide_eq_cancel1";
+(*Moved from RealOrd.ML to use #0 *)
Goal "[| #0 < r; #0 < x|] ==> (inverse x < inverse (r::real)) = (r < x)";
by (auto_tac (claset() addIs [real_inverse_less_swap], simpset()));
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1);
@@ -387,3 +449,142 @@
by (res_inst_tac [("x","(min d1 d2)/#2")] exI 1);
by (asm_simp_tac (simpset() addsimps [min_def]) 1);
qed "real_lbound_gt_zero";
+
+
+(*** General rewrites to improve automation, like those for type "int" ***)
+
+(** The next several equations can make the simplifier loop! **)
+
+Goal "(x < - y) = (y < - (x::real))";
+by Auto_tac;
+qed "real_less_minus";
+
+Goal "(- x < y) = (- y < (x::real))";
+by Auto_tac;
+qed "real_minus_less";
+
+Goal "(x <= - y) = (y <= - (x::real))";
+by Auto_tac;
+qed "real_le_minus";
+
+Goal "(- x <= y) = (- y <= (x::real))";
+by Auto_tac;
+qed "real_minus_le";
+
+Goal "(x = - y) = (y = - (x::real))";
+by Auto_tac;
+qed "real_equation_minus";
+
+Goal "(- x = y) = (- (y::real) = x)";
+by Auto_tac;
+qed "real_minus_equation";
+
+
+(*Distributive laws for literals*)
+Addsimps (map (inst "w" "number_of ?v")
+ [real_add_mult_distrib, real_add_mult_distrib2,
+ real_diff_mult_distrib, real_diff_mult_distrib2]);
+
+Addsimps (map (inst "x" "number_of ?v")
+ [real_less_minus, real_le_minus, real_equation_minus]);
+Addsimps (map (inst "y" "number_of ?v")
+ [real_minus_less, real_minus_le, real_minus_equation]);
+
+
+(*** Simprules combining x+y and #0 ***)
+
+Goal "(x+y = (#0::real)) = (y = -x)";
+by Auto_tac;
+qed "real_add_eq_0_iff";
+AddIffs [real_add_eq_0_iff];
+
+(**?????????not needed with re-orientation
+Goal "((#0::real) = x+y) = (y = -x)";
+by Auto_tac;
+qed "real_0_eq_add_iff";
+AddIffs [real_0_eq_add_iff];
+????????*)
+
+Goal "(x+y < (#0::real)) = (y < -x)";
+by Auto_tac;
+qed "real_add_less_0_iff";
+AddIffs [real_add_less_0_iff];
+
+Goal "((#0::real) < x+y) = (-x < y)";
+by Auto_tac;
+qed "real_0_less_add_iff";
+AddIffs [real_0_less_add_iff];
+
+Goal "(x+y <= (#0::real)) = (y <= -x)";
+by Auto_tac;
+qed "real_add_le_0_iff";
+AddIffs [real_add_le_0_iff];
+
+Goal "((#0::real) <= x+y) = (-x <= y)";
+by Auto_tac;
+qed "real_0_le_add_iff";
+AddIffs [real_0_le_add_iff];
+
+
+(*** Simprules combining x-y and #0 ***)
+
+Goal "(x-y = (#0::real)) = (x = y)";
+by Auto_tac;
+qed "real_diff_eq_0_iff";
+AddIffs [real_diff_eq_0_iff];
+
+Goal "((#0::real) = x-y) = (x = y)";
+by Auto_tac;
+qed "real_0_eq_diff_iff";
+AddIffs [real_0_eq_diff_iff];
+
+Goal "(x-y < (#0::real)) = (x < y)";
+by Auto_tac;
+qed "real_diff_less_0_iff";
+AddIffs [real_diff_less_0_iff];
+
+Goal "((#0::real) < x-y) = (y < x)";
+by Auto_tac;
+qed "real_0_less_diff_iff";
+AddIffs [real_0_less_diff_iff];
+
+Goal "(x-y <= (#0::real)) = (x <= y)";
+by Auto_tac;
+qed "real_diff_le_0_iff";
+AddIffs [real_diff_le_0_iff];
+
+Goal "((#0::real) <= x-y) = (y <= x)";
+by Auto_tac;
+qed "real_0_le_diff_iff";
+AddIffs [real_0_le_diff_iff];
+
+(*
+?? still needed ??
+Addsimps [symmetric real_diff_def];
+*)
+
+Goal "-(x-y) = y - (x::real)";
+by (arith_tac 1);
+qed "real_minus_diff_eq";
+Addsimps [real_minus_diff_eq];
+
+
+(*** Density of the Reals ***)
+
+Goal "x < y ==> x < (x+y) / (#2::real)";
+by Auto_tac;
+qed "real_less_half_sum";
+
+Goal "x < y ==> (x+y)/(#2::real) < y";
+by Auto_tac;
+qed "real_gt_half_sum";
+
+Goal "x < y ==> EX r::real. x < r & r < y";
+by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
+qed "real_dense";
+
+
+(*Replaces "inverse #nn" by #1/#nn *)
+Addsimps [inst "x" "number_of ?w" real_inverse_eq_divide];
+
+
--- a/src/HOL/Real/RealOrd.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/RealOrd.ML Fri Dec 15 17:41:38 2000 +0100
@@ -574,26 +574,6 @@
simpset() addsimps [real_le_refl]));
qed "real_mult_self_le2";
-Goal "x < y ==> x < (x + y) * inverse (1r + 1r)";
-by (dres_inst_tac [("C","x")] real_add_less_mono2 1);
-by (dtac (real_add_self RS subst) 1);
-by (dtac (real_zero_less_two RS real_inverse_gt_zero RS
- real_mult_less_mono1) 1);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
-qed "real_less_half_sum";
-
-Goal "x < y ==> (x + y) * inverse (1r + 1r) < y";
-by (dtac real_add_less_mono1 1);
-by (dtac (real_add_self RS subst) 1);
-by (dtac (real_zero_less_two RS real_inverse_gt_zero RS
- real_mult_less_mono1) 1);
-by (asm_full_simp_tac (simpset() addsimps [real_mult_assoc]) 1);
-qed "real_gt_half_sum";
-
-Goal "x < y ==> EX r::real. x < r & r < y";
-by (blast_tac (claset() addSIs [real_less_half_sum, real_gt_half_sum]) 1);
-qed "real_dense";
-
Goal "(EX n. inverse (real_of_posnat n) < r) = (EX n. 1r < r * real_of_posnat n)";
by (Step_tac 1);
by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero
--- a/src/HOL/Real/RealPow.ML Fri Dec 15 12:32:35 2000 +0100
+++ b/src/HOL/Real/RealPow.ML Fri Dec 15 17:41:38 2000 +0100
@@ -6,7 +6,7 @@
*)
Goal "(#0::real) ^ (Suc n) = #0";
-by (Auto_tac);
+by Auto_tac;
qed "realpow_zero";
Addsimps [realpow_zero];
@@ -87,7 +87,7 @@
Goal "#1 ^ n = (#1::real)";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_eq_one";
Addsimps [realpow_eq_one];
@@ -97,18 +97,13 @@
qed "abs_minus_realpow_one";
Addsimps [abs_minus_realpow_one];
-Goal "abs((-#1) ^ n) = (#1::real)";
+Goal "abs((#-1) ^ n) = (#1::real)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps [abs_mult,
abs_minus_cancel,abs_one]));
qed "abs_realpow_minus_one";
Addsimps [abs_realpow_minus_one];
-Goal "abs((#-1) ^ n) = (#1::real)";
-by (rtac (simplify (simpset()) abs_realpow_minus_one) 1);
-qed "abs_realpow_minus_one2";
-Addsimps [abs_realpow_minus_one2];
-
Goal "((r::real) * s) ^ n = (r ^ n) * (s ^ n)";
by (induct_tac "n" 1);
by (auto_tac (claset(),simpset() addsimps real_mult_ac));
@@ -200,33 +195,25 @@
qed "two_realpow_gt";
Addsimps [two_realpow_gt,two_realpow_ge_one];
-Goal "(-#1) ^ (2*n) = (#1::real)";
+Goal "(#-1) ^ (#2*n) = (#1::real)";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_minus_one";
Addsimps [realpow_minus_one];
-Goal "(-#1) ^ (n + n) = (#1::real)";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed "realpow_minus_one2";
-Addsimps [realpow_minus_one2];
-
-Goal "(-#1) ^ Suc (n + n) = -(#1::real)";
-by (induct_tac "n" 1);
-by (Auto_tac);
+Goal "(#-1) ^ Suc (#2*n) = -(#1::real)";
+by Auto_tac;
qed "realpow_minus_one_odd";
Addsimps [realpow_minus_one_odd];
-Goal "(-#1) ^ Suc (Suc (n + n)) = (#1::real)";
-by (induct_tac "n" 1);
-by (Auto_tac);
+Goal "(#-1) ^ Suc (Suc (#2*n)) = (#1::real)";
+by Auto_tac;
qed "realpow_minus_one_even";
Addsimps [realpow_minus_one_even];
Goal "(#0::real) < r & r < (#1::real) --> r ^ Suc n < r ^ n";
by (induct_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "realpow_Suc_less";
Goal "#0 <= r & r < (#1::real) --> r ^ Suc n <= r ^ n";
@@ -237,7 +224,7 @@
Goal "(#0::real) <= #0 ^ n";
by (case_tac "n" 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_zero_le";
Addsimps [realpow_zero_le];
@@ -249,12 +236,12 @@
Goal "[| #0 <= r; r < (#1::real) |] ==> r ^ Suc n <= r ^ n";
by (etac (real_le_imp_less_or_eq RS disjE) 1);
by (rtac realpow_Suc_le2 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_Suc_le3";
Goal "#0 <= r & r < (#1::real) & n < N --> r ^ N <= r ^ n";
by (induct_tac "N" 1);
-by (Auto_tac);
+by Auto_tac;
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_zero2));
by (ALLGOALS(dtac (rename_numerals real_mult_le_mono3)));
by (REPEAT(assume_tac 1));
@@ -272,7 +259,7 @@
Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n <= r";
by (dres_inst_tac [("n","1"),("N","Suc n")]
(real_less_imp_le RS realpow_le_le) 1);
-by (Auto_tac);
+by Auto_tac;
qed "realpow_Suc_le_self";
Goal "[| #0 < r; r < (#1::real) |] ==> r ^ Suc n < #1";
@@ -297,7 +284,7 @@
Goal "(#1::real) < r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
-by (Auto_tac);
+by Auto_tac;
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one));
by (ALLGOALS(dtac (rename_numerals real_mult_self_le)));
by (assume_tac 1);
@@ -308,7 +295,7 @@
Goal "(#1::real) <= r & n < N --> r ^ n <= r ^ N";
by (induct_tac "N" 1);
-by (Auto_tac);
+by Auto_tac;
by (ALLGOALS(forw_inst_tac [("n","na")] realpow_ge_one2));
by (ALLGOALS(dtac (rename_numerals real_mult_self_le2)));
by (assume_tac 1);
@@ -330,13 +317,13 @@
Goal "(#1::real) < r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")]
realpow_ge_ge 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "realpow_Suc_ge_self";
Goal "(#1::real) <= r ==> r <= r ^ Suc n";
by (dres_inst_tac [("n","1"),("N","Suc n")]
realpow_ge_ge2 1);
-by (Auto_tac);
+by Auto_tac;
qed_spec_mp "realpow_Suc_ge_self2";
Goal "[| (#1::real) < r; 0 < n |] ==> r <= r ^ n";