# HG changeset patch # User paulson # Date 976898498 -3600 # Node ID 36625483213f1d5c2b1f0ab341357e70b533eb35 # Parent 06f390008ceb649fef155f7973576bbe5177e329 further round of tidying diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/HRealAbs.ML --- 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); diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/HyperDef.ML --- 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"; diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/HyperOrd.ML --- 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, diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/Lim.ML --- 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"; - diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/Lim.thy --- 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 diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/NSA.ML --- 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"; diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/NatStar.ML --- 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 diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/SEQ.ML --- 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 (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)"; ---------------------------------------------------------------***) diff -r 06f390008ceb -r 36625483213f src/HOL/Real/Hyperreal/Star.ML --- 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); diff -r 06f390008ceb -r 36625483213f src/HOL/Real/RComplete.ML --- 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); diff -r 06f390008ceb -r 36625483213f src/HOL/Real/RealArith.ML --- 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 < 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]; + + diff -r 06f390008ceb -r 36625483213f src/HOL/Real/RealOrd.ML --- 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 diff -r 06f390008ceb -r 36625483213f src/HOL/Real/RealPow.ML --- 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";