# HG changeset patch # User paulson # Date 978600181 -3600 # Node ID 2c6605049646988b471f5add7b5d3c314bf79af0 # Parent a5a6255748c3855f91487f2cf14c6dc4f06fc27c more tidying, especially to remove real_of_posnat diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HRealAbs.ML --- a/src/HOL/Hyperreal/HRealAbs.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HRealAbs.ML Thu Jan 04 10:23:01 2001 +0100 @@ -204,3 +204,52 @@ "abs (hypreal_of_real r) = hypreal_of_real (abs r)"; by (auto_tac (claset(), simpset() addsimps [hypreal_hrabs])); qed "hypreal_of_real_hrabs"; + + +(*---------------------------------------------------------------------------- + Embedding of the naturals in the hyperreals + ----------------------------------------------------------------------------*) + +Goalw [hypreal_of_nat_def] + "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)"; +by (simp_tac (simpset() addsimps [hypreal_of_real_add, real_of_nat_add]) 1); +qed "hypreal_of_nat_add"; + +Goalw [hypreal_of_nat_def] + "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"; +by (auto_tac (claset() addIs [hypreal_add_less_mono1], simpset())); +qed "hypreal_of_nat_less_iff"; +Addsimps [hypreal_of_nat_less_iff RS sym]; + +(*------------------------------------------------------------*) +(* naturals embedded in hyperreals *) +(* is a hyperreal c.f. NS extension *) +(*------------------------------------------------------------*) + +Goalw [hypreal_of_nat_def, hypreal_of_real_def, real_of_nat_def] + "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; +by Auto_tac; +qed "hypreal_of_nat_iff"; + +Goal "inj hypreal_of_nat"; +by (simp_tac (simpset() addsimps [inj_on_def, hypreal_of_nat_def]) 1); +qed "inj_hypreal_of_nat"; + +Goalw [hypreal_of_nat_def] + "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr"; +by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1); +qed "hypreal_of_nat_Suc"; + +(*"neg" is used in rewrite rules for binary comparisons*) +Goal "hypreal_of_nat (number_of v :: nat) = \ +\ (if neg (number_of v) then #0 \ +\ else (number_of v :: hypreal))"; +by (simp_tac (simpset() addsimps [hypreal_of_nat_def]) 1); +qed "hypreal_of_nat_number_of"; +Addsimps [hypreal_of_nat_number_of]; + +Goal "hypreal_of_nat 0 = #0"; +by (simp_tac (simpset() delsimps [numeral_0_eq_0] + addsimps [numeral_0_eq_0 RS sym]) 1); +qed "hypreal_of_nat_zero"; +Addsimps [hypreal_of_nat_zero]; diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HRealAbs.thy --- a/src/HOL/Hyperreal/HRealAbs.thy Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HRealAbs.thy Thu Jan 04 10:23:01 2001 +0100 @@ -9,4 +9,9 @@ defs hrabs_def "abs r == if (0::hypreal) <=r then r else -r" +constdefs + + hypreal_of_nat :: nat => hypreal + "hypreal_of_nat n == hypreal_of_real (real_of_nat n)" + end \ No newline at end of file diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HSeries.ML --- a/src/HOL/Hyperreal/HSeries.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HSeries.ML Thu Jan 04 10:23:01 2001 +0100 @@ -195,7 +195,7 @@ by (simp_tac (HOL_ss addsimps [one_eq_numeral_1 RS sym, hypreal_one_def]) 1); by (auto_tac (claset(), - simpset() addsimps [sumhr, hypreal_diff, real_of_nat_def])); + simpset() addsimps [sumhr, hypreal_diff, real_of_nat_Suc])); qed "sumhr_hypreal_omega_minus_one"; Goalw [hypnat_zero_def, hypnat_omega_def] @@ -211,8 +211,8 @@ \ ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) = \ \ (hypreal_of_nat (na - m) * hypreal_of_real r)"; by (auto_tac (claset() addSDs [sumr_interval_const], - simpset() addsimps [sumhr,hypreal_of_nat_real_of_nat, - hypreal_of_real_def,hypreal_mult])); + simpset() addsimps [sumhr,hypreal_of_nat_def, + hypreal_of_real_def, hypreal_mult])); qed "sumhr_interval_const"; Goalw [hypnat_zero_def] diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HyperBin.ML --- a/src/HOL/Hyperreal/HyperBin.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HyperBin.ML Thu Jan 04 10:23:01 2001 +0100 @@ -172,15 +172,6 @@ hypreal_add_number_of_diff1, hypreal_add_number_of_diff2]; -(*"neg" is used in rewrite rules for binary comparisons*) -Goal "hypreal_of_nat (number_of v :: nat) = \ -\ (if neg (number_of v) then #0 \ -\ else (number_of v :: hypreal))"; -by (simp_tac (simpset() addsimps [hypreal_of_nat_real_of_nat]) 1); -qed "hypreal_of_nat_number_of"; -Addsimps [hypreal_of_nat_number_of]; - - (**** Simprocs for numeric literals ****) (** Combining of literal coefficients in sums of products **) diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HyperDef.ML --- a/src/HOL/Hyperreal/HyperDef.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HyperDef.ML Thu Jan 04 10:23:01 2001 +0100 @@ -1227,49 +1227,6 @@ qed "hypreal_minus_eq_cancel"; Addsimps [hypreal_minus_eq_cancel]; -Goal "x < x + 1hr"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_add, hypreal_one_def,hypreal_less])); -qed "hypreal_less_self_add_one"; -Addsimps [hypreal_less_self_add_one]; - -(*??DELETE MOST OF THE FOLLOWING??*) -Goal "((x::hypreal) + x = y + y) = (x = 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_add])); -by (ALLGOALS(Ultra_tac)); -qed "hypreal_add_self_cancel"; -Addsimps [hypreal_add_self_cancel]; - -Goal "(y = x + - y + x) = (y = (x::hypreal))"; -by Auto_tac; -by (dres_inst_tac [("x1","y")] - (hypreal_add_right_cancel RS iffD2) 1); -by (auto_tac (claset(),simpset() addsimps hypreal_add_ac)); -qed "hypreal_add_self_minus_cancel"; -Addsimps [hypreal_add_self_minus_cancel]; - -Goal "(y = x + (- y + x)) = (y = (x::hypreal))"; -by (asm_full_simp_tac (simpset() addsimps - [hypreal_add_assoc RS sym])1); -qed "hypreal_add_self_minus_cancel2"; -Addsimps [hypreal_add_self_minus_cancel2]; - -(* of course, can prove this by "transfer" as well *) -Goal "z + -x = y + (y + (-x + -z)) = (y = (z::hypreal))"; -by Auto_tac; -by (dres_inst_tac [("x1","z")] - (hypreal_add_right_cancel RS iffD2) 1); -by (asm_full_simp_tac (simpset() addsimps - [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac - delsimps [hypreal_minus_add_distrib]) 1); -by (asm_full_simp_tac (simpset() addsimps - [hypreal_add_assoc RS sym,hypreal_add_right_cancel]) 1); -qed "hypreal_add_self_minus_cancel3"; -Addsimps [hypreal_add_self_minus_cancel3]; - Goalw [hypreal_diff_def] "(x] *) omega_def - "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_posnat n})" + "whr == Abs_hypreal(hyprel^^{%n::nat. real_of_nat (Suc n)})" (* an infinitesimal number = [<1,1/2,1/3,...>] *) epsilon_def - "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_posnat n)})" + "ehr == Abs_hypreal(hyprel^^{%n::nat. inverse (real_of_nat (Suc n))})" hypreal_minus_def "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel^^{%n::nat. - (X n)})" @@ -67,14 +67,6 @@ hypreal_of_real :: real => hypreal "hypreal_of_real r == Abs_hypreal(hyprel^^{%n::nat. r})" - - (* n::nat --> (n+1)::hypreal *) - hypreal_of_posnat :: nat => hypreal - "hypreal_of_posnat n == (hypreal_of_real(real_of_preal - (preal_of_prat(prat_of_pnat(pnat_of_nat n)))))" - - hypreal_of_nat :: nat => hypreal - "hypreal_of_nat n == hypreal_of_posnat n + -1hr" defs diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HyperNat.ML --- a/src/HOL/Hyperreal/HyperNat.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HyperNat.ML Thu Jan 04 10:23:01 2001 +0100 @@ -41,7 +41,7 @@ AddSEs [hypnatrelE]; Goalw [hypnatrel_def] "(x,x): hypnatrel"; -by (Auto_tac); +by Auto_tac; qed "hypnatrel_refl"; Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,x):hypnatrel"; @@ -50,7 +50,7 @@ Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel"; -by (Auto_tac); +by Auto_tac; by (Fuf_tac 1); qed_spec_mp "hypnatrel_trans"; @@ -87,7 +87,7 @@ Goalw [hypnatrel_def] "x: hypnatrel ^^ {x}"; by (Step_tac 1); -by (Auto_tac); +by Auto_tac; qed "lemma_hypnatrel_refl"; Addsimps [lemma_hypnatrel_refl]; @@ -100,7 +100,7 @@ Goal "Rep_hypnat x ~= {}"; by (cut_inst_tac [("x","x")] Rep_hypnat 1); -by (Auto_tac); +by Auto_tac; qed "Rep_hypnat_nonempty"; Addsimps [Rep_hypnat_nonempty]; @@ -117,7 +117,7 @@ by (rtac equiv_hypnatrel 1); by (Fast_tac 1); by (rtac ccontr 1 THEN rotate_tac 1 1); -by (Auto_tac); +by Auto_tac; qed "inj_hypnat_of_nat"; val [prem] = Goal @@ -376,7 +376,7 @@ (*** (hypnat) one and zero are distinct ***) Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= 1hn"; -by (Auto_tac); +by Auto_tac; qed "hypnat_zero_not_eq_one"; Addsimps [hypnat_zero_not_eq_one]; Addsimps [hypnat_zero_not_eq_one RS not_sym]; @@ -404,7 +404,7 @@ qed "hypnat_less_iff"; Goalw [hypnat_less_def] - "!!P. [| {n. X n < Y n} : FreeUltrafilterNat; \ + "[| {n. X n < Y n} : FreeUltrafilterNat; \ \ X : Rep_hypnat(P); \ \ Y : Rep_hypnat(Q) |] ==> P < (Q::hypnat)"; by (Fast_tac 1); @@ -416,11 +416,11 @@ \ !!X. X : Rep_hypnat(R1) ==> P; \ \ !!Y. Y : Rep_hypnat(R2) ==> P |] \ \ ==> P"; -by (Auto_tac); +by Auto_tac; qed "hypnat_lessE"; Goalw [hypnat_less_def] - "!!R1. R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \ + "R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \ \ X : Rep_hypnat(R1) & \ \ Y : Rep_hypnat(R2))"; by (Fast_tac 1); @@ -437,7 +437,7 @@ Goalw [hypnat_less_def,hypnat_zero_def] "~ n<(0::hypnat)"; by (res_inst_tac [("z","n")] eq_Abs_hypnat 1); -by (Auto_tac); +by Auto_tac; by (Fuf_empty_tac 1); qed "hypnat_not_less0"; AddIffs [hypnat_not_less0]; @@ -460,9 +460,9 @@ by (res_inst_tac [("z","R3")] eq_Abs_hypnat 1); by (auto_tac (claset(),simpset() addsimps [hypnat_less_def])); by (res_inst_tac [("x","X")] exI 1); -by (Auto_tac); +by Auto_tac; by (res_inst_tac [("x","Ya")] exI 1); -by (Auto_tac); +by Auto_tac; by (Fuf_tac 1); qed "hypnat_less_trans"; @@ -530,12 +530,12 @@ Goalw [hypnatrel_def] "EX x. x: hypnatrel ^^ {%n. 0}"; by (res_inst_tac [("x","%n. 0")] exI 1); by (Step_tac 1); -by (Auto_tac); +by Auto_tac; qed "lemma_hypnatrel_0_mem"; (* linearity is actually proved further down! *) -Goalw [hypnat_zero_def, - hypnat_less_def]"(0::hypnat) < x | x = 0 | x < 0"; +Goalw [hypnat_zero_def, hypnat_less_def] + "(0::hypnat) < x | x = 0 | x < 0"; by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (Auto_tac ); by (REPEAT(Step_tac 1)); @@ -543,29 +543,28 @@ by (Fuf_tac 1); qed "hypnat_trichotomy"; -Goal "!!x. [| (0::hypnat) < x ==> P; \ -\ x = 0 ==> P; \ -\ x < 0 ==> P |] ==> P"; +Goal "!!P. [| (0::hypnat) < x ==> P; \ +\ x = 0 ==> P; \ +\ x < 0 ==> P |] ==> P"; by (cut_inst_tac [("x","x")] hypnat_trichotomy 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_trichotomyE"; -(*------------------------------------------------------------------------------ +(*---------------------------------------------------------------------------- More properties of < - ------------------------------------------------------------------------------*) + ----------------------------------------------------------------------------*) Goal "!!(A::hypnat). A < B ==> A + C < B + C"; by (res_inst_tac [("z","A")] eq_Abs_hypnat 1); by (res_inst_tac [("z","B")] eq_Abs_hypnat 1); by (res_inst_tac [("z","C")] eq_Abs_hypnat 1); -by (auto_tac (claset(),simpset() addsimps - [hypnat_less_def,hypnat_add])); +by (auto_tac (claset(), simpset() addsimps [hypnat_less_def,hypnat_add])); by (REPEAT(Step_tac 1)); by (Fuf_tac 1); qed "hypnat_add_less_mono1"; Goal "!!(A::hypnat). A < B ==> C + A < C + B"; by (auto_tac (claset() addIs [hypnat_add_less_mono1], - simpset() addsimps [hypnat_add_commute])); + simpset() addsimps [hypnat_add_commute])); qed "hypnat_add_less_mono2"; Goal "!!k l::hypnat. [|i i + k < j + l"; @@ -598,16 +597,27 @@ by (Fuf_tac 1); qed "hypnat_linear"; -Goal - "!!(x::hypnat). [| x < y ==> P; x = y ==> P; \ -\ y < x ==> P |] ==> P"; +Goal "!!(x::hypnat). [| x < y ==> P; x = y ==> P; \ +\ y < x ==> P |] ==> P"; by (cut_inst_tac [("x","x"),("y","y")] hypnat_linear 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_linear_less2"; -(*------------------------------------------------------------------------------ +Goal "((w::hypnat) ~= z) = (w z <= (w::hypnat)"; -by (assume_tac 1); -qed "hypnat_leI"; -Goalw [hypnat_le_def] "!!w. z<=w ==> ~(w<(z::hypnat))"; -by (assume_tac 1); -qed "hypnat_leD"; - -val hypnat_leE = make_elim hypnat_leD; - -Goal "!!w. (~(w < z)) = (z <= (w::hypnat))"; -by (fast_tac (claset() addSIs [hypnat_leI,hypnat_leD]) 1); -qed "hypnat_less_le_iff"; - -Goalw [hypnat_le_def] "!!z. ~ z <= w ==> w<(z::hypnat)"; -by (Fast_tac 1); -qed "not_hypnat_leE"; - -Goalw [hypnat_le_def] "!!z. z < w ==> z <= (w::hypnat)"; +Goalw [hypnat_le_def] "z < w ==> z <= (w::hypnat)"; by (fast_tac (claset() addEs [hypnat_less_asym]) 1); qed "hypnat_less_imp_le"; @@ -647,59 +640,53 @@ by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1); qed "hypnat_le_imp_less_or_eq"; -Goalw [hypnat_le_def] "!!z. z z <=(w::hypnat)"; +Goalw [hypnat_le_def] "z z <=(w::hypnat)"; by (cut_facts_tac [hypnat_linear] 1); -by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1); +by (blast_tac (claset() addDs [hypnat_less_irrefl,hypnat_less_asym]) 1); qed "hypnat_less_or_eq_imp_le"; Goal "(x <= (y::hypnat)) = (x < y | x=y)"; -by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, hypnat_le_imp_less_or_eq] 1)); -qed "hypnat_le_eq_less_or_eq"; +by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, + hypnat_le_imp_less_or_eq] 1)); +qed "hypnat_le_less"; + +(* Axiom 'linorder_linear' of class 'linorder': *) +Goal "(z::hypnat) <= w | w <= z"; +by (simp_tac (simpset() addsimps [hypnat_le_less]) 1); +by (cut_facts_tac [hypnat_linear] 1); +by (Blast_tac 1); +qed "hypnat_le_linear"; Goal "w <= (w::hypnat)"; -by (simp_tac (simpset() addsimps [hypnat_le_eq_less_or_eq]) 1); +by (simp_tac (simpset() addsimps [hypnat_le_less]) 1); qed "hypnat_le_refl"; Addsimps [hypnat_le_refl]; -val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::hypnat)"; -by (dtac hypnat_le_imp_less_or_eq 1); -by (fast_tac (claset() addIs [hypnat_less_trans]) 1); -qed "hypnat_le_less_trans"; - -Goal "!! (i::hypnat). [| i < j; j <= k |] ==> i < k"; -by (dtac hypnat_le_imp_less_or_eq 1); -by (fast_tac (claset() addIs [hypnat_less_trans]) 1); -qed "hypnat_less_le_trans"; - -Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::hypnat)"; +Goal "[| i <= j; j <= k |] ==> i <= (k::hypnat)"; by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq, - rtac hypnat_less_or_eq_imp_le, fast_tac (claset() addIs [hypnat_less_trans])]); + rtac hypnat_less_or_eq_imp_le, + fast_tac (claset() addIs [hypnat_less_trans])]); qed "hypnat_le_trans"; -Goal "!!z. [| z <= w; w <= z |] ==> z = (w::hypnat)"; +Goal "[| z <= w; w <= z |] ==> z = (w::hypnat)"; by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq, fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym])]); qed "hypnat_le_anti_sym"; -Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::hypnat)"; -by (rtac not_hypnat_leE 1); -by (fast_tac (claset() addDs [hypnat_le_imp_less_or_eq]) 1); -qed "not_less_not_eq_hypnat_less"; - -Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y"; +Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y"; by (REPEAT(dtac hypnat_le_imp_less_or_eq 1)); -by (auto_tac (claset() addIs [hypnat_mult_order, - hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl])); +by (auto_tac (claset() addIs [hypnat_mult_order, hypnat_less_imp_le], + simpset() addsimps [hypnat_le_refl])); qed "hypnat_le_mult_order"; Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] "(0::hypnat) < 1hn"; by (res_inst_tac [("x","%n. 0")] exI 1); by (res_inst_tac [("x","%n. 1")] exI 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_zero_less_one"; -Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y"; +Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y"; by (REPEAT(dtac hypnat_le_imp_less_or_eq 1)); by (auto_tac (claset() addIs [hypnat_add_order, hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl])); @@ -752,7 +739,7 @@ Goal "(x::hypnat) < x + 1hn"; by (cut_facts_tac [hypnat_zero_less_one RS hypnat_add_less_mono2] 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_add_one_self_less"; Addsimps [hypnat_add_one_self_less]; @@ -816,7 +803,7 @@ Goalw [hypnat_le_def,le_def] "(z1 <= z2) = (hypnat_of_nat z1 <= hypnat_of_nat z2)"; -by (Auto_tac); +by Auto_tac; qed "hypnat_of_nat_le_iff"; Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat 1 = 1hn"; @@ -837,8 +824,8 @@ by (full_simp_tac (simpset() addsimps [hypnat_of_nat_zero_iff]) 1); qed "hypnat_of_nat_not_zero_iff"; -goalw HyperNat.thy [hypnat_of_nat_def,hypnat_one_def] - "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn"; +Goalw [hypnat_of_nat_def,hypnat_one_def] + "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn"; by (auto_tac (claset(),simpset() addsimps [hypnat_add])); qed "hypnat_of_nat_Suc"; @@ -847,7 +834,7 @@ ---------------------------------------------------------------------------------*) Goal "hypnatrel^^{%n::nat. n} : hypnat"; -by (Auto_tac); +by Auto_tac; qed "hypnat_omega"; Goalw [hypnat_omega_def] "Rep_hypnat(whn) : hypnat"; @@ -867,111 +854,110 @@ Goal "hypnat_of_nat x ~= whn"; by (cut_facts_tac [not_ex_hypnat_of_nat_eq_omega] 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_of_nat_not_eq_omega"; Addsimps [hypnat_of_nat_not_eq_omega RS not_sym]; (*----------------------------------------------------------- - Properties of the set SHNat of embedded natural numbers + Properties of the set SNat of embedded natural numbers (cf. set SReal in NSA.thy/NSA.ML) ----------------------------------------------------------*) -(* Infinite hypernatural not in embedded SHNat *) -Goalw [SHNat_def] "whn ~: SHNat"; -by (Auto_tac); +(* Infinite hypernatural not in embedded SNat *) +Goalw [SHNat_def] "whn ~: SNat"; +by Auto_tac; qed "SHNAT_omega_not_mem"; Addsimps [SHNAT_omega_not_mem]; (*----------------------------------------------------------------------- - Closure laws for members of (embedded) set standard naturals SHNat + Closure laws for members of (embedded) set standard naturals SNat -----------------------------------------------------------------------*) Goalw [SHNat_def] - "!!x. [| x: SHNat; y: SHNat |] ==> x + y: SHNat"; + "!!x::hypnat. [| x: SNat; y: SNat |] ==> x + y: SNat"; by (Step_tac 1); by (res_inst_tac [("x","N + Na")] exI 1); by (simp_tac (simpset() addsimps [hypnat_of_nat_add]) 1); qed "SHNat_add"; Goalw [SHNat_def] - "!!x. [| x: SHNat; y: SHNat |] ==> x - y: SHNat"; + "!!x::hypnat. [| x: SNat; y: SNat |] ==> x - y: SNat"; by (Step_tac 1); by (res_inst_tac [("x","N - Na")] exI 1); by (simp_tac (simpset() addsimps [hypnat_of_nat_minus]) 1); qed "SHNat_minus"; Goalw [SHNat_def] - "!!x. [| x: SHNat; y: SHNat |] ==> x * y: SHNat"; + "!!x::hypnat. [| x: SNat; y: SNat |] ==> x * y: SNat"; by (Step_tac 1); by (res_inst_tac [("x","N * Na")] exI 1); by (simp_tac (simpset() addsimps [hypnat_of_nat_mult]) 1); qed "SHNat_mult"; -Goal "!!x. [| x + y : SHNat; y: SHNat |] ==> x: SHNat"; +Goal"!!x::hypnat. [| x + y : SNat; y: SNat |] ==> x: SNat"; by (dres_inst_tac [("x","x+y")] SHNat_minus 1); -by (Auto_tac); +by Auto_tac; qed "SHNat_add_cancel"; -Goalw [SHNat_def] "hypnat_of_nat x : SHNat"; +Goalw [SHNat_def] "hypnat_of_nat x : SNat"; by (Blast_tac 1); qed "SHNat_hypnat_of_nat"; Addsimps [SHNat_hypnat_of_nat]; -Goal "hypnat_of_nat 1 : SHNat"; +Goal "hypnat_of_nat 1 : SNat"; by (Simp_tac 1); qed "SHNat_hypnat_of_nat_one"; -Goal "hypnat_of_nat 0 : SHNat"; +Goal "hypnat_of_nat 0 : SNat"; by (Simp_tac 1); qed "SHNat_hypnat_of_nat_zero"; -Goal "1hn : SHNat"; +Goal "1hn : SNat"; by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one, hypnat_of_nat_one RS sym]) 1); qed "SHNat_one"; -Goal "0 : SHNat"; +Goal "(0::hypnat) : SNat"; by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_zero, - hypnat_of_nat_zero RS sym]) 1); + hypnat_of_nat_zero RS sym]) 1); qed "SHNat_zero"; Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero, SHNat_one,SHNat_zero]; -Goal "1hn + 1hn : SHNat"; +Goal "1hn + 1hn : SNat"; by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1); qed "SHNat_two"; -Goalw [SHNat_def] "{x. hypnat_of_nat x : SHNat} = (UNIV::nat set)"; -by (Auto_tac); +Goalw [SHNat_def] "{x. hypnat_of_nat x : SNat} = (UNIV::nat set)"; +by Auto_tac; qed "SHNat_UNIV_nat"; -Goalw [SHNat_def] "(x: SHNat) = (EX y. x = hypnat_of_nat y)"; -by (Auto_tac); +Goalw [SHNat_def] "(x: SNat) = (EX y. x = hypnat_of_nat y)"; +by Auto_tac; qed "SHNat_iff"; -Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SHNat"; -by (Auto_tac); +Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SNat"; +by Auto_tac; qed "hypnat_of_nat_image"; -Goalw [SHNat_def] "inv hypnat_of_nat ``SHNat = (UNIV::nat set)"; -by (Auto_tac); +Goalw [SHNat_def] "inv hypnat_of_nat ``SNat = (UNIV::nat set)"; +by Auto_tac; by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1); by (Blast_tac 1); qed "inv_hypnat_of_nat_image"; Goalw [SHNat_def] - "!!P. [| EX x. x: P; P <= SHNat |] ==> \ -\ EX Q. P = hypnat_of_nat `` Q"; + "[| EX x. x: P; P <= SNat |] ==> EX Q. P = hypnat_of_nat `` Q"; by (Best_tac 1); qed "SHNat_hypnat_of_nat_image"; Goalw [SHNat_def] - "SHNat = hypnat_of_nat `` (UNIV::nat set)"; -by (Auto_tac); + "SNat = hypnat_of_nat `` (UNIV::nat set)"; +by Auto_tac; qed "SHNat_hypnat_of_nat_iff"; -Goalw [SHNat_def] "SHNat <= (UNIV::hypnat set)"; -by (Auto_tac); +Goalw [SHNat_def] "SNat <= (UNIV::hypnat set)"; +by Auto_tac; qed "SHNat_subset_UNIV"; Goal "{n. n <= Suc m} = {n. n <= m} Un {n. n = Suc m}"; @@ -990,9 +976,8 @@ qed "lemma_unbounded_set"; Addsimps [lemma_unbounded_set]; -Goalw [SHNat_def,hypnat_of_nat_def, - hypnat_less_def,hypnat_omega_def] - "ALL n: SHNat. n < whn"; +Goalw [SHNat_def,hypnat_of_nat_def, hypnat_less_def,hypnat_omega_def] + "ALL n: SNat. n < whn"; by (Clarify_tac 1); by (auto_tac (claset() addSIs [exI],simpset())); qed "hypnat_omega_gt_SHNat"; @@ -1000,7 +985,7 @@ Goal "hypnat_of_nat n < whn"; by (cut_facts_tac [hypnat_omega_gt_SHNat] 1); by (dres_inst_tac [("x","hypnat_of_nat n")] bspec 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_of_nat_less_whn"; Addsimps [hypnat_of_nat_less_whn]; @@ -1011,13 +996,13 @@ Goal "0 < whn"; by (rtac (hypnat_omega_gt_SHNat RS ballE) 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_zero_less_hypnat_omega"; Addsimps [hypnat_zero_less_hypnat_omega]; Goal "1hn < whn"; by (rtac (hypnat_omega_gt_SHNat RS ballE) 1); -by (Auto_tac); +by Auto_tac; qed "hypnat_one_less_hypnat_omega"; Addsimps [hypnat_one_less_hypnat_omega]; @@ -1025,43 +1010,43 @@ Theorems about infinite hypernatural numbers -- HNatInfinite -------------------------------------------------------------------------*) Goalw [HNatInfinite_def,SHNat_def] "whn : HNatInfinite"; -by (Auto_tac); +by Auto_tac; qed "HNatInfinite_whn"; Addsimps [HNatInfinite_whn]; -Goalw [HNatInfinite_def] "!!x. x: SHNat ==> x ~: HNatInfinite"; +Goalw [HNatInfinite_def] "x: SNat ==> x ~: HNatInfinite"; by (Simp_tac 1); qed "SHNat_not_HNatInfinite"; -Goalw [HNatInfinite_def] "!!x. x ~: HNatInfinite ==> x: SHNat"; +Goalw [HNatInfinite_def] "x ~: HNatInfinite ==> x: SNat"; by (Asm_full_simp_tac 1); qed "not_HNatInfinite_SHNat"; -Goalw [HNatInfinite_def] "!!x. x ~: SHNat ==> x: HNatInfinite"; +Goalw [HNatInfinite_def] "x ~: SNat ==> x: HNatInfinite"; by (Simp_tac 1); qed "not_SHNat_HNatInfinite"; -Goalw [HNatInfinite_def] "!!x. x: HNatInfinite ==> x ~: SHNat"; +Goalw [HNatInfinite_def] "x: HNatInfinite ==> x ~: SNat"; by (Asm_full_simp_tac 1); qed "HNatInfinite_not_SHNat"; -Goal "(x: SHNat) = (x ~: HNatInfinite)"; +Goal "(x: SNat) = (x ~: HNatInfinite)"; by (blast_tac (claset() addSIs [SHNat_not_HNatInfinite, not_HNatInfinite_SHNat]) 1); qed "SHNat_not_HNatInfinite_iff"; -Goal "(x ~: SHNat) = (x: HNatInfinite)"; +Goal "(x ~: SNat) = (x: HNatInfinite)"; by (blast_tac (claset() addSIs [not_SHNat_HNatInfinite, HNatInfinite_not_SHNat]) 1); qed "not_SHNat_HNatInfinite_iff"; -Goal "x : SHNat | x : HNatInfinite"; +Goal "x : SNat | x : HNatInfinite"; by (simp_tac (simpset() addsimps [SHNat_not_HNatInfinite_iff]) 1); qed "SHNat_HNatInfinite_disj"; (*------------------------------------------------------------------- Proof of alternative definition for set of Infinite hypernatural - numbers --- HNatInfinite = {N. ALL n: SHNat. n < N} + numbers --- HNatInfinite = {N. ALL n: SNat. n < N} -------------------------------------------------------------------*) Goal "!!N (xa::nat=>nat). \ \ (ALL N. {n. xa n ~= N} : FreeUltrafilterNat) ==> \ @@ -1078,7 +1063,7 @@ (*** alternative definition ***) Goalw [HNatInfinite_def,SHNat_def,hypnat_of_nat_def] - "HNatInfinite = {N. ALL n:SHNat. n < N}"; + "HNatInfinite = {N. ALL n:SNat. n < N}"; by (Step_tac 1); by (dres_inst_tac [("x","Abs_hypnat \ \ (hypnatrel ^^ {%n. N})")] bspec 2); @@ -1094,8 +1079,8 @@ (*-------------------------------------------------------------------- Alternative definition for HNatInfinite using Free ultrafilter --------------------------------------------------------------------*) -Goal "!!x. x : HNatInfinite ==> EX X: Rep_hypnat x. \ -\ ALL u. {n. u < X n}: FreeUltrafilterNat"; +Goal "x : HNatInfinite ==> EX X: Rep_hypnat x. \ +\ ALL u. {n. u < X n}: FreeUltrafilterNat"; by (auto_tac (claset(),simpset() addsimps [hypnat_less_def, HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def])); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); @@ -1108,26 +1093,25 @@ by (Fuf_tac 1); qed "HNatInfinite_FreeUltrafilterNat"; -Goal "!!x. EX X: Rep_hypnat x. \ -\ ALL u. {n. u < X n}: FreeUltrafilterNat \ -\ ==> x: HNatInfinite"; +Goal "EX X: Rep_hypnat x. ALL u. {n. u < X n}: FreeUltrafilterNat \ +\ ==> x: HNatInfinite"; by (auto_tac (claset(),simpset() addsimps [hypnat_less_def, HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def])); by (rtac exI 1 THEN Auto_tac); qed "FreeUltrafilterNat_HNatInfinite"; -Goal "!!x. (x : HNatInfinite) = (EX X: Rep_hypnat x. \ +Goal "(x : HNatInfinite) = (EX X: Rep_hypnat x. \ \ ALL u. {n. u < X n}: FreeUltrafilterNat)"; by (blast_tac (claset() addIs [HNatInfinite_FreeUltrafilterNat, FreeUltrafilterNat_HNatInfinite]) 1); qed "HNatInfinite_FreeUltrafilterNat_iff"; -Goal "!!x. x : HNatInfinite ==> 1hn < x"; +Goal "x : HNatInfinite ==> 1hn < x"; by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff])); qed "HNatInfinite_gt_one"; Addsimps [HNatInfinite_gt_one]; -Goal "!!x. 0 ~: HNatInfinite"; +Goal "0 ~: HNatInfinite"; by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff])); by (dres_inst_tac [("a","1hn")] equals0D 1); @@ -1135,11 +1119,11 @@ qed "zero_not_mem_HNatInfinite"; Addsimps [zero_not_mem_HNatInfinite]; -Goal "!!x. x : HNatInfinite ==> x ~= 0"; -by (Auto_tac); +Goal "x : HNatInfinite ==> x ~= 0"; +by Auto_tac; qed "HNatInfinite_not_eq_zero"; -Goal "!!x. x : HNatInfinite ==> 1hn <= x"; +Goal "x : HNatInfinite ==> 1hn <= x"; by (blast_tac (claset() addIs [hypnat_less_imp_le, HNatInfinite_gt_one]) 1); qed "HNatInfinite_ge_one"; @@ -1148,7 +1132,7 @@ (*-------------------------------------------------- Closure Rules --------------------------------------------------*) -Goal "!!x. [| x: HNatInfinite; y: HNatInfinite |] \ +Goal "[| x: HNatInfinite; y: HNatInfinite |] \ \ ==> x + y: HNatInfinite"; by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff])); by (dtac bspec 1 THEN assume_tac 1); @@ -1157,16 +1141,14 @@ by (Asm_full_simp_tac 1); qed "HNatInfinite_add"; -Goal "!!x. [| x: HNatInfinite; y: SHNat |] \ -\ ==> x + y: HNatInfinite"; +Goal "[| x: HNatInfinite; y: SNat |] ==> x + y: HNatInfinite"; by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1); by (dres_inst_tac [("x","x + y")] SHNat_minus 1); by (auto_tac (claset(),simpset() addsimps [SHNat_not_HNatInfinite_iff])); qed "HNatInfinite_SHNat_add"; -goal HyperNat.thy "!!x. [| x: HNatInfinite; y: SHNat |] \ -\ ==> x - y: HNatInfinite"; +Goal "[| x: HNatInfinite; y: SNat |] ==> x - y: HNatInfinite"; by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1); by (dres_inst_tac [("x","x - y")] SHNat_add 1); by (subgoal_tac "y <= x" 2); @@ -1176,23 +1158,21 @@ simpset() addsimps [not_SHNat_HNatInfinite_iff,HNatInfinite_iff])); qed "HNatInfinite_SHNat_diff"; -Goal - "!!x. x: HNatInfinite ==> x + 1hn: HNatInfinite"; +Goal "x: HNatInfinite ==> x + 1hn: HNatInfinite"; by (auto_tac (claset() addIs [HNatInfinite_SHNat_add], simpset())); qed "HNatInfinite_add_one"; -Goal - "!!x. x: HNatInfinite ==> x - 1hn: HNatInfinite"; +Goal "x: HNatInfinite ==> x - 1hn: HNatInfinite"; by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1); by (dres_inst_tac [("x","x - 1hn"),("y","1hn")] SHNat_add 1); by (auto_tac (claset(),simpset() addsimps [not_SHNat_HNatInfinite_iff RS sym])); qed "HNatInfinite_minus_one"; -Goal "!!x. x : HNatInfinite ==> EX y. x = y + 1hn"; +Goal "x : HNatInfinite ==> EX y. x = y + 1hn"; by (res_inst_tac [("x","x - 1hn")] exI 1); -by (Auto_tac); +by Auto_tac; qed "HNatInfinite_is_Suc"; (*--------------------------------------------------------------- @@ -1200,23 +1180,21 @@ Obtained using the NS extension of the naturals --------------------------------------------------------------*) -Goalw [HNat_def,starset_def, - hypreal_of_posnat_def,hypreal_of_real_def] - "hypreal_of_posnat N : HNat"; -by (Auto_tac); +Goalw [HNat_def,starset_def, hypreal_of_nat_def,hypreal_of_real_def] + "hypreal_of_nat N : HNat"; +by Auto_tac; by (Ultra_tac 1); -by (res_inst_tac [("x","Suc N")] exI 1); -by (dtac sym 1 THEN auto_tac (claset(),simpset() - addsimps [real_of_preal_real_of_nat_Suc])); -qed "HNat_hypreal_of_posnat"; -Addsimps [HNat_hypreal_of_posnat]; +by (res_inst_tac [("x","N")] exI 1); +by Auto_tac; +qed "HNat_hypreal_of_nat"; +Addsimps [HNat_hypreal_of_nat]; Goalw [HNat_def,starset_def] "[| x: HNat; y: HNat |] ==> x + y: HNat"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl], - simpset() addsimps [hypreal_add])); + simpset() addsimps [hypreal_add])); by (Ultra_tac 1); by (dres_inst_tac [("t","Y xb")] sym 1); by (auto_tac (claset(),simpset() addsimps [real_of_nat_add RS sym])); @@ -1236,10 +1214,10 @@ (*--------------------------------------------------------------- Embedding of the hypernaturals into the hyperreal --------------------------------------------------------------*) -(*** A lemma that should have been derived a long time ago! ***) + Goal "(Ya : hyprel ^^{%n. f(n)}) = \ -\ ({n. f n = Ya n} : FreeUltrafilterNat)"; -by (Auto_tac); +\ ({n. f n = Ya n} : FreeUltrafilterNat)"; +by Auto_tac; qed "lemma_hyprel_FUFN"; Goalw [hypreal_of_hypnat_def] @@ -1255,8 +1233,7 @@ by (rtac injI 1); by (res_inst_tac [("z","x")] eq_Abs_hypnat 1); by (res_inst_tac [("z","y")] eq_Abs_hypnat 1); -by (auto_tac (claset(),simpset() addsimps - [hypreal_of_hypnat,real_of_nat_eq_cancel])); +by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat])); qed "inj_hypreal_of_hypnat"; Goal "(hypreal_of_hypnat n = hypreal_of_hypnat m) = (n = m)"; @@ -1326,7 +1303,7 @@ Addsimps [hypnat_not_all_eq_zero]; Goal "n ~= 0 ==> (n <= 1hn) = (n = 1hn)"; -by (auto_tac (claset(),simpset() addsimps [hypnat_le_eq_less_or_eq])); +by (auto_tac (claset(), simpset() addsimps [hypnat_le_less])); qed "hypnat_le_one_eq_one"; Addsimps [hypnat_le_one_eq_one]; diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HyperNat.thy --- a/src/HOL/Hyperreal/HyperNat.thy Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HyperNat.thy Thu Jan 04 10:23:01 2001 +0100 @@ -21,29 +21,12 @@ "1hn" :: hypnat ("1hn") "whn" :: hypnat ("whn") -defs - - hypnat_zero_def "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})" - hypnat_one_def "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})" - - (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *) - hypnat_omega_def "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})" - - constdefs (* embedding the naturals in the hypernaturals *) hypnat_of_nat :: nat => hypnat "hypnat_of_nat m == Abs_hypnat(hypnatrel^^{%n::nat. m})" - (* set of naturals embedded in the hypernaturals*) - SHNat :: "hypnat set" - "SHNat == {n. EX N. n = hypnat_of_nat N}" - - (* embedding the naturals in the hyperreals*) - SNat :: "hypreal set" - "SNat == {n. EX N. n = hypreal_of_nat N}" - (* hypernaturals as members of the hyperreals; the set is defined as *) (* the nonstandard extension of set of naturals embedded in the reals *) HNat :: "hypreal set" @@ -51,7 +34,7 @@ (* the set of infinite hypernatural numbers *) HNatInfinite :: "hypnat set" - "HNatInfinite == {n. n ~: SHNat}" + "HNatInfinite == {n. n ~: SNat}" (* explicit embedding of the hypernaturals in the hyperreals *) hypreal_of_hypnat :: hypnat => hypreal @@ -59,6 +42,23 @@ hyprel^^{%n::nat. real_of_nat (X n)})" defs + + (** the overloaded constant "SNat" **) + + (* set of naturals embedded in the hyperreals*) + SNat_def "SNat == {n. EX N. n = hypreal_of_nat N}" + + (* set of naturals embedded in the hypernaturals*) + SHNat_def "SNat == {n. EX N. n = hypnat_of_nat N}" + + (** hypernatural arithmetic **) + + hypnat_zero_def "0 == Abs_hypnat(hypnatrel^^{%n::nat. 0})" + hypnat_one_def "1hn == Abs_hypnat(hypnatrel^^{%n::nat. 1})" + + (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *) + hypnat_omega_def "whn == Abs_hypnat(hypnatrel^^{%n::nat. n})" + hypnat_add_def "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q). hypnatrel^^{%n::nat. X n + Y n})" diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HyperOrd.ML --- a/src/HOL/Hyperreal/HyperOrd.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.ML Thu Jan 04 10:23:01 2001 +0100 @@ -102,22 +102,22 @@ qed "hypreal_lt_zero_iff"; Goalw [hypreal_le_def] "((0::hypreal) <= x) = (-x <= x)"; -by (auto_tac (claset(),simpset() addsimps [hypreal_lt_zero_iff RS sym])); +by (auto_tac (claset(), simpset() addsimps [hypreal_lt_zero_iff RS sym])); qed "hypreal_ge_zero_iff"; Goalw [hypreal_le_def] "(x <= (0::hypreal)) = (x <= -x)"; -by (auto_tac (claset(),simpset() addsimps [hypreal_gt_zero_iff RS sym])); +by (auto_tac (claset(), simpset() addsimps [hypreal_gt_zero_iff RS sym])); qed "hypreal_le_zero_iff"; Goalw [hypreal_zero_def] "[| 0 < x; 0 < y |] ==> (0::hypreal) < x + 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_less_def,hypreal_add])); -by (auto_tac (claset() addSIs [exI],simpset() addsimps - [hypreal_less_def,hypreal_add])); -by (ultra_tac (claset() addIs [real_add_order],simpset()) 1); +by (auto_tac (claset(), + simpset() addsimps [hypreal_less_def,hypreal_add])); +by (auto_tac (claset() addSIs [exI], + simpset() addsimps [hypreal_less_def,hypreal_add])); +by (ultra_tac (claset() addIs [real_add_order], simpset()) 1); qed "hypreal_add_order"; Goal "[| 0 < x; 0 <= y |] ==> (0::hypreal) < x + y"; @@ -130,8 +130,8 @@ "[| 0 < x; 0 < y |] ==> (0::hypreal) < x * 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() addSIs [exI],simpset() addsimps - [hypreal_less_def,hypreal_mult])); +by (auto_tac (claset() addSIs [exI], + simpset() addsimps [hypreal_less_def,hypreal_mult])); by (ultra_tac (claset() addIs [rename_numerals real_mult_order], simpset()) 1); qed "hypreal_mult_order"; @@ -142,31 +142,6 @@ by (Asm_full_simp_tac 1); qed "hypreal_mult_less_zero1"; -Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x * y"; -by (REPEAT(dtac order_le_imp_less_or_eq 1)); -by (auto_tac (claset() addIs [hypreal_mult_order, order_less_imp_le], - simpset())); -qed "hypreal_le_mult_order"; - - -Goal "[| x <= 0; y <= 0 |] ==> (0::hypreal) <= x * y"; -by (rtac hypreal_less_or_eq_imp_le 1); -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1); -by Auto_tac; -by (dtac order_le_imp_less_or_eq 1); -by (auto_tac (claset() addDs [hypreal_mult_less_zero1],simpset())); -qed "hypreal_mult_le_zero1"; - -Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::hypreal)"; -by (rtac hypreal_less_or_eq_imp_le 1); -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1); -by Auto_tac; -by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); -by (rtac (hypreal_minus_zero_less_iff RS subst) 1); -by (blast_tac (claset() addDs [hypreal_mult_order] - addIs [hypreal_minus_mult_eq2 RS ssubst]) 1); -qed "hypreal_mult_le_zero"; - Goal "[| 0 < x; y < 0 |] ==> x*y < (0::hypreal)"; by (dtac (hypreal_minus_zero_less_iff RS iffD2) 1); by (dtac hypreal_mult_order 1 THEN assume_tac 1); @@ -181,22 +156,6 @@ simpset() addsimps [real_zero_less_one, FreeUltrafilterNat_Nat_set])); qed "hypreal_zero_less_one"; -Goal "1hr < 1hr + 1hr"; -by (rtac (hypreal_less_minus_iff RS iffD2) 1); -by (full_simp_tac (simpset() addsimps [hypreal_zero_less_one, - hypreal_add_assoc]) 1); -qed "hypreal_one_less_two"; - -Goal "0 < 1hr + 1hr"; -by (rtac ([hypreal_zero_less_one, - hypreal_one_less_two] MRS order_less_trans) 1); -qed "hypreal_zero_less_two"; - -Goal "1hr + 1hr ~= 0"; -by (rtac (hypreal_zero_less_two RS hypreal_not_refl2 RS not_sym) 1); -qed "hypreal_two_not_zero"; -Addsimps [hypreal_two_not_zero]; - Goal "[| 0 <= x; 0 <= y |] ==> (0::hypreal) <= x + y"; by (REPEAT(dtac order_le_imp_less_or_eq 1)); by (auto_tac (claset() addIs [hypreal_add_order, order_less_imp_le], @@ -232,9 +191,9 @@ by (dtac hypreal_add_order 1 THEN assume_tac 1); by (thin_tac "0 < y2 + - z2" 1); by (dres_inst_tac [("C","z1 + z2")] hypreal_add_less_mono1 1); -by (auto_tac (claset(),simpset() addsimps - [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac - delsimps [hypreal_minus_add_distrib])); +by (auto_tac (claset(), + simpset() addsimps [hypreal_minus_add_distrib RS sym] @ hypreal_add_ac + delsimps [hypreal_minus_add_distrib])); qed "hypreal_add_less_mono"; Goal "(q1::hypreal) <= q2 ==> x + q1 <= x + q2"; @@ -322,7 +281,7 @@ Goal "[| (0::hypreal)<=z; x x*z<=y*z"; by (EVERY1 [rtac hypreal_less_or_eq_imp_le, dtac order_le_imp_less_or_eq]); -by (auto_tac (claset() addIs [hypreal_mult_less_mono1],simpset())); +by (auto_tac (claset() addIs [hypreal_mult_less_mono1], simpset())); qed "hypreal_mult_le_less_mono1"; Goal "[| (0::hypreal)<=z; x z*x<=z*y"; @@ -397,12 +356,6 @@ by (blast_tac (claset() addDs [hypreal_mult_zero_disj]) 1); qed "hypreal_mult_is_0"; -Goal "(x*x + y*y = 0) = (x = 0 & y = (0::hypreal))"; -by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_add_nonneg_eq_0_iff, - hypreal_mult_is_0]) 1); -qed "hypreal_squares_add_zero_iff"; -Addsimps [hypreal_squares_add_zero_iff]; - Goal "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"; by (simp_tac (HOL_ss addsimps [hypreal_le_square, hypreal_le_add_order, hypreal_add_nonneg_eq_0_iff, hypreal_mult_is_0]) 1); @@ -435,58 +388,8 @@ (*---------------------------------------------------------------------------- - Embedding of the naturals in the hyperreals + Existence of infinite hyperreal number ----------------------------------------------------------------------------*) -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); -by (fold_tac [real_one_def]); -by (simp_tac (simpset() addsimps [hypreal_of_real_one]) 1); -qed "hypreal_of_posnat_one"; - -Goalw [hypreal_of_posnat_def] "hypreal_of_posnat 1 = 1hr + 1hr"; -by (full_simp_tac (simpset() addsimps - [real_of_preal_def, - rename_numerals (real_one_def RS meta_eq_to_obj_eq), - hypreal_add,hypreal_of_real_def,pnat_two_eq, - hypreal_one_def, real_add, - prat_of_pnat_add RS sym, preal_of_prat_add RS sym] @ - pnat_add_ac) 1); -qed "hypreal_of_posnat_two"; - -(*FIXME: delete this and all posnat*) -Goalw [hypreal_of_posnat_def] - "hypreal_of_posnat n1 + hypreal_of_posnat n2 = \ -\ hypreal_of_posnat (n1 + n2) + 1hr"; -by (full_simp_tac (HOL_ss addsimps [hypreal_of_posnat_one RS sym, - hypreal_of_real_add RS sym,hypreal_of_posnat_def,real_of_preal_add RS sym, - preal_of_prat_add RS sym,prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); -qed "hypreal_of_posnat_add"; - -Goal "hypreal_of_posnat (n + 1) = hypreal_of_posnat n + 1hr"; -by (res_inst_tac [("x1","1hr")] (hypreal_add_right_cancel RS iffD1) 1); -by (rtac (hypreal_of_posnat_add RS subst) 1); -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two,hypreal_add_assoc]) 1); -qed "hypreal_of_posnat_add_one"; - -Goalw [real_of_posnat_def,hypreal_of_posnat_def] - "hypreal_of_posnat n = hypreal_of_real (real_of_posnat n)"; -by (rtac refl 1); -qed "hypreal_of_real_of_posnat"; - -Goalw [hypreal_of_posnat_def] - "(n < m) = (hypreal_of_posnat n < hypreal_of_posnat m)"; -by Auto_tac; -qed "hypreal_of_posnat_less_iff"; - -Addsimps [hypreal_of_posnat_less_iff RS sym]; -(*--------------------------------------------------------------------------------- - Existence of infinite hyperreal number - ---------------------------------------------------------------------------------*) - -Goal "hyprel^^{%n::nat. real_of_posnat n} : hypreal"; -by Auto_tac; -qed "hypreal_omega"; Goalw [omega_def] "Rep_hypreal(whr) : hypreal"; by (rtac Rep_hypreal 1); @@ -496,20 +399,21 @@ (* use assumption that member FreeUltrafilterNat is not finite *) (* a few lemmas first *) -Goal "{n::nat. x = real_of_posnat n} = {} | \ -\ (EX y. {n::nat. x = real_of_posnat n} = {y})"; -by (auto_tac (claset() addDs [inj_real_of_posnat RS injD],simpset())); +Goal "{n::nat. x = real_of_nat n} = {} | \ +\ (EX y. {n::nat. x = real_of_nat n} = {y})"; +by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset())); qed "lemma_omega_empty_singleton_disj"; -Goal "finite {n::nat. x = real_of_posnat n}"; +Goal "finite {n::nat. x = real_of_nat n}"; by (cut_inst_tac [("x","x")] lemma_omega_empty_singleton_disj 1); by Auto_tac; qed "lemma_finite_omega_set"; Goalw [omega_def,hypreal_of_real_def] "~ (EX x. hypreal_of_real x = whr)"; -by (auto_tac (claset(),simpset() addsimps [lemma_finite_omega_set - RS FreeUltrafilterNat_finite])); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_Suc, real_diff_eq_eq RS sym, + lemma_finite_omega_set RS FreeUltrafilterNat_finite])); qed "not_ex_hypreal_of_real_eq_omega"; Goal "hypreal_of_real x ~= whr"; @@ -520,21 +424,25 @@ (* existence of infinitesimal number also not *) (* corresponding to any real number *) -Goal "{n::nat. x = inverse(real_of_posnat n)} = {} | \ -\ (EX y. {n::nat. x = inverse(real_of_posnat n)} = {y})"; -by (Step_tac 1 THEN Step_tac 1); -by (auto_tac (claset() addIs [real_of_posnat_inverse_inj],simpset())); +Goal "inverse (real_of_nat x) = inverse (real_of_nat y) ==> x = y"; +by (rtac (inj_real_of_nat RS injD) 1); +by (Asm_full_simp_tac 1); +qed "real_of_nat_inverse_inj"; + +Goal "{n::nat. x = inverse(real_of_nat(Suc n))} = {} | \ +\ (EX y. {n::nat. x = inverse(real_of_nat(Suc n))} = {y})"; +by (auto_tac (claset(), simpset() addsimps [inj_real_of_nat RS inj_eq])); qed "lemma_epsilon_empty_singleton_disj"; -Goal "finite {n::nat. x = inverse(real_of_posnat n)}"; +Goal "finite {n::nat. x = inverse(real_of_nat(Suc n))}"; by (cut_inst_tac [("x","x")] lemma_epsilon_empty_singleton_disj 1); by Auto_tac; qed "lemma_finite_epsilon_set"; Goalw [epsilon_def,hypreal_of_real_def] "~ (EX x. hypreal_of_real x = ehr)"; -by (auto_tac (claset(),simpset() addsimps [lemma_finite_epsilon_set - RS FreeUltrafilterNat_finite])); +by (auto_tac (claset(), + simpset() addsimps [lemma_finite_epsilon_set RS FreeUltrafilterNat_finite])); qed "not_ex_hypreal_of_real_eq_epsilon"; Goal "hypreal_of_real x ~= ehr"; @@ -543,96 +451,28 @@ qed "hypreal_of_real_not_eq_epsilon"; Goalw [epsilon_def,hypreal_zero_def] "ehr ~= 0"; +by Auto_tac; by (auto_tac (claset(), - simpset() addsimps [rename_numerals real_of_posnat_not_eq_zero])); + simpset() addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym])); qed "hypreal_epsilon_not_zero"; -Addsimps [rename_numerals real_of_posnat_not_eq_zero]; -Goalw [omega_def,hypreal_zero_def] "whr ~= 0"; -by (Simp_tac 1); -qed "hypreal_omega_not_zero"; - Goal "ehr = inverse(whr)"; by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, omega_def, epsilon_def]) 1); qed "hypreal_epsilon_inverse_omega"; -(*---------------------------------------------------------------- - Another embedding of the naturals in the - hyperreals (see hypreal_of_posnat) - ----------------------------------------------------------------*) -Goalw [hypreal_of_nat_def] "hypreal_of_nat 0 = 0"; -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_one]) 1); -qed "hypreal_of_nat_zero"; - -Goalw [hypreal_of_nat_def] "hypreal_of_nat 1 = 1hr"; -by (full_simp_tac (simpset() addsimps [hypreal_of_posnat_two, - hypreal_add_assoc]) 1); -qed "hypreal_of_nat_one"; - -Goalw [hypreal_of_nat_def] - "hypreal_of_nat n1 + hypreal_of_nat n2 = hypreal_of_nat (n1 + n2)"; -by (full_simp_tac (simpset() addsimps hypreal_add_ac) 1); -by (simp_tac (simpset() addsimps [hypreal_of_posnat_add, - hypreal_add_assoc RS sym]) 1); -qed "hypreal_of_nat_add"; - -Goal "hypreal_of_nat 2 = 1hr + 1hr"; -by (simp_tac (simpset() addsimps [hypreal_of_nat_one - RS sym,hypreal_of_nat_add]) 1); -qed "hypreal_of_nat_two"; - -Goalw [hypreal_of_nat_def] - "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"; -by (auto_tac (claset() addIs [hypreal_add_less_mono1],simpset())); -qed "hypreal_of_nat_less_iff"; -Addsimps [hypreal_of_nat_less_iff RS sym]; - -(*------------------------------------------------------------*) -(* naturals embedded in hyperreals *) -(* is a hyperreal c.f. NS extension *) -(*------------------------------------------------------------*) - -Goalw [hypreal_of_nat_def,real_of_nat_def] - "hypreal_of_nat m = Abs_hypreal(hyprel^^{%n. real_of_nat m})"; -by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def, - hypreal_of_real_of_posnat,hypreal_minus,hypreal_one_def,hypreal_add])); -qed "hypreal_of_nat_iff"; - -Goal "inj hypreal_of_nat"; -by (rtac injI 1); -by (auto_tac (claset() addSDs [FreeUltrafilterNat_P], - simpset() addsimps [split_if_mem1, hypreal_of_nat_iff, - real_add_right_cancel,inj_real_of_nat RS injD])); -qed "inj_hypreal_of_nat"; - -Goalw [hypreal_of_nat_def,hypreal_of_real_def,hypreal_of_posnat_def, - real_of_posnat_def,hypreal_one_def,real_of_nat_def] - "hypreal_of_nat n = hypreal_of_real (real_of_nat n)"; -by (simp_tac (simpset() addsimps [hypreal_add,hypreal_minus]) 1); -qed "hypreal_of_nat_real_of_nat"; - -Goal "hypreal_of_posnat (Suc n) = hypreal_of_posnat n + 1hr"; -by (stac (hypreal_of_posnat_add_one RS sym) 1); -by (Simp_tac 1); -qed "hypreal_of_posnat_Suc"; - -Goalw [hypreal_of_nat_def] - "hypreal_of_nat (Suc n) = hypreal_of_nat n + 1hr"; -by (simp_tac (simpset() addsimps [hypreal_of_posnat_Suc] @ hypreal_add_ac) 1); -qed "hypreal_of_nat_Suc"; (* this proof is so much simpler than one for reals!! *) Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::hypreal)"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (res_inst_tac [("z","r")] eq_Abs_hypreal 1); -by (auto_tac (claset(),simpset() addsimps [hypreal_inverse, - hypreal_less,hypreal_zero_def])); -by (ultra_tac (claset() addIs [real_inverse_less_swap],simpset()) 1); +by (auto_tac (claset(), + simpset() addsimps [hypreal_inverse, hypreal_less,hypreal_zero_def])); +by (ultra_tac (claset() addIs [real_inverse_less_swap], simpset()) 1); qed "hypreal_inverse_less_swap"; Goal "[| 0 < r; 0 < x|] ==> (r < x) = (inverse x < inverse (r::hypreal))"; -by (auto_tac (claset() addIs [hypreal_inverse_less_swap],simpset())); +by (auto_tac (claset() addIs [hypreal_inverse_less_swap], simpset())); by (res_inst_tac [("t","r")] (hypreal_inverse_inverse RS subst) 1); by (res_inst_tac [("t","x")] (hypreal_inverse_inverse RS subst) 1); by (rtac hypreal_inverse_less_swap 1); diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HyperPow.ML --- a/src/HOL/Hyperreal/HyperPow.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HyperPow.ML Thu Jan 04 10:23:01 2001 +0100 @@ -3,6 +3,7 @@ Copyright : 1998 University of Cambridge Description : Natural Powers of hyperreals theory +Exponentials on the hyperreals *) Goal "(#0::hypreal) ^ (Suc n) = 0"; @@ -136,15 +137,13 @@ Goal "(#1::hypreal) <= #2 ^ n"; by (res_inst_tac [("y","#1 ^ n")] order_trans 1); by (rtac hrealpow_le 2); -by (auto_tac (claset() addIs [order_less_imp_le], - simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two])); +by Auto_tac; qed "two_hrealpow_ge_one"; Goal "hypreal_of_nat n < #2 ^ n"; by (induct_tac "n" 1); by (auto_tac (claset(), - simpset() addsimps [hypreal_of_nat_Suc,hypreal_of_nat_zero, - hypreal_zero_less_one,hypreal_add_mult_distrib,hypreal_of_nat_one])); + simpset() addsimps [hypreal_of_nat_Suc, hypreal_add_mult_distrib])); by (cut_inst_tac [("n","n")] two_hrealpow_ge_one 1); by (arith_tac 1); qed "two_hrealpow_gt"; @@ -189,9 +188,9 @@ Goal "(x + (y::hypreal)) ^ 2 = \ \ x ^ 2 + y ^ 2 + (hypreal_of_nat 2)*x*y"; -by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib2, - hypreal_add_mult_distrib,hypreal_of_nat_two] - @ hypreal_add_ac @ hypreal_mult_ac) 1); +by (simp_tac (simpset() addsimps + [hypreal_add_mult_distrib2, hypreal_add_mult_distrib, + hypreal_of_nat_zero, hypreal_of_nat_Suc]) 1); qed "hrealpow_sum_square_expand"; (*--------------------------------------------------------------- @@ -391,8 +390,7 @@ Goal "(#1::hypreal) <= #2 pow n"; by (res_inst_tac [("y","#1 pow n")] order_trans 1); by (rtac hyperpow_le 2); -by (auto_tac (claset() addIs [order_less_imp_le], - simpset() addsimps [hypreal_zero_less_one, hypreal_one_less_two])); +by Auto_tac; qed "two_hyperpow_ge_one"; Addsimps [two_hyperpow_ge_one]; @@ -455,7 +453,7 @@ qed "hyperpow_less_le2"; Goal "[| #0 <= r; r < (#1::hypreal); N : HNatInfinite |] \ -\ ==> ALL n:SHNat. r pow N <= r pow n"; +\ ==> ALL n: SNat. r pow N <= r pow n"; by (auto_tac (claset() addSIs [hyperpow_less_le], simpset() addsimps [HNatInfinite_iff])); qed "hyperpow_SHNat_le"; @@ -493,18 +491,16 @@ qed "hyperpow_Suc_le_self2"; Goalw [Infinitesimal_def] - "[| x : Infinitesimal; 0 < N |] ==> (abs x) pow N <= abs x"; + "[| x : Infinitesimal; 0 < N |] ==> abs (x pow N) <= abs x"; by (auto_tac (claset() addSIs [hyperpow_Suc_le_self2], - simpset() addsimps [hyperpow_hrabs RS sym, - hypnat_gt_zero_iff2, hrabs_ge_zero, - hypreal_zero_less_one])); + simpset() addsimps [hyperpow_hrabs RS sym, + hypnat_gt_zero_iff2, hrabs_ge_zero])); qed "lemma_Infinitesimal_hyperpow"; Goal "[| x : Infinitesimal; 0 < N |] ==> x pow N : Infinitesimal"; by (rtac hrabs_le_Infinitesimal 1); -by (dtac Infinitesimal_hrabs 1); -by (auto_tac (claset() addSIs [lemma_Infinitesimal_hyperpow], - simpset() addsimps [hyperpow_hrabs RS sym])); +by (rtac lemma_Infinitesimal_hyperpow 2); +by Auto_tac; qed "Infinitesimal_hyperpow"; Goalw [hypnat_of_nat_def] diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/HyperPow.thy --- a/src/HOL/Hyperreal/HyperPow.thy Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/HyperPow.thy Thu Jan 04 10:23:01 2001 +0100 @@ -6,6 +6,16 @@ HyperPow = HRealAbs + HyperNat + RealPow + +(** First: hypnat is linearly ordered **) + +instance hypnat :: order (hypnat_le_refl,hypnat_le_trans,hypnat_le_anti_sym, + hypnat_less_le) +instance hypnat :: linorder (hypnat_le_linear) + +instance hypnat :: plus_ac0(hypnat_add_commute,hypnat_add_assoc, + hypnat_add_zero_left) + + instance hypreal :: {power} consts hpowr :: "[hypreal,nat] => hypreal" diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Thu Jan 04 10:23:01 2001 +0100 @@ -5,7 +5,6 @@ differentiation of real=>real functions *) - fun ARITH_PROVE str = prove_goal thy str (fn prems => [cut_facts_tac prems 1,arith_tac 1]); @@ -28,12 +27,9 @@ LIM_add ---------------*) Goalw [LIM_def] - "[| f -- x --> l; g -- x --> m |] \ -\ ==> (%x. f(x) + g(x)) -- x --> (l + m)"; -by (Step_tac 1); + "[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"; +by (Clarify_tac 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); by (Clarify_tac 1); by (res_inst_tac [("R1.0","s"),("R2.0","sa")] @@ -189,26 +185,26 @@ Goal "ALL s. #0 < s --> (EX xa. xa ~= x & \ \ abs (xa + - x) < s & r <= abs (f xa + -L)) \ \ ==> ALL n::nat. EX xa. xa ~= x & \ -\ abs(xa + -x) < inverse(real_of_posnat n) & r <= abs(f xa + -L)"; -by (Step_tac 1); +\ abs(xa + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f xa + -L)"; +by (Clarify_tac 1); by (cut_inst_tac [("n1","n")] - (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1); + (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1); by Auto_tac; val lemma_LIM = result(); Goal "ALL s. #0 < s --> (EX xa. xa ~= x & \ \ abs (xa + - x) < s & r <= abs (f xa + -L)) \ \ ==> EX X. ALL n::nat. X n ~= x & \ -\ abs(X n + -x) < inverse(real_of_posnat n) & r <= abs(f (X n) + -L)"; +\ abs(X n + -x) < inverse(real_of_nat(Suc n)) & r <= abs(f (X n) + -L)"; by (dtac lemma_LIM 1); by (dtac choice 1); by (Blast_tac 1); val lemma_skolemize_LIM2 = result(); Goal "ALL n. X n ~= x & \ -\ abs (X n + - x) < inverse (real_of_posnat n) & \ +\ abs (X n + - x) < inverse (real_of_nat(Suc n)) & \ \ r <= abs (f (X n) + - L) ==> \ -\ ALL n. abs (X n + - x) < inverse (real_of_posnat n)"; +\ ALL n. abs (X n + - x) < inverse (real_of_nat(Suc n))"; by (Auto_tac ); val lemma_simp = result(); @@ -217,7 +213,7 @@ -------------------*) Goalw [LIM_def,NSLIM_def,inf_close_def] - "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]); @@ -697,16 +693,17 @@ Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \ \ ==> ALL n::nat. EX z y. \ -\ abs(z + -y) < inverse(real_of_posnat n) & \ +\ abs(z + -y) < inverse(real_of_nat(Suc n)) & \ \ r <= abs(f z + -f y)"; -by (Step_tac 1); -by (cut_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1); +by (Clarify_tac 1); +by (cut_inst_tac [("n1","n")] + (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero) 1); by Auto_tac; val lemma_LIMu = result(); Goal "ALL s. #0 < s --> (EX z y. abs (z + - y) < s & r <= abs (f z + -f y)) \ \ ==> EX X Y. ALL n::nat. \ -\ abs(X n + -(Y n)) < inverse(real_of_posnat n) & \ +\ abs(X n + -(Y n)) < inverse(real_of_nat(Suc n)) & \ \ r <= abs(f (X n) + -f (Y n))"; by (dtac lemma_LIMu 1); by (dtac choice 1); @@ -715,9 +712,9 @@ by (Blast_tac 1); val lemma_skolemize_LIM2u = result(); -Goal "ALL n. abs (X n + -Y n) < inverse (real_of_posnat n) & \ +Goal "ALL n. abs (X n + -Y n) < inverse (real_of_nat(Suc n)) & \ \ r <= abs (f (X n) + - f(Y n)) ==> \ -\ ALL n. abs (X n + - Y n) < inverse (real_of_posnat n)"; +\ ALL n. abs (X n + - Y n) < inverse (real_of_nat(Suc n))"; by (Auto_tac ); val lemma_simpu = result(); @@ -1301,17 +1298,17 @@ Goal "DERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))"; by (induct_tac "n" 1); by (dtac (DERIV_Id RS DERIV_mult) 2); -by (auto_tac (claset(),simpset() addsimps - [real_add_mult_distrib])); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_Suc, real_add_mult_distrib])); by (case_tac "0 < n" 1); by (dres_inst_tac [("x","x")] realpow_minus_mult 1); -by (auto_tac (claset(),simpset() addsimps - [real_mult_assoc,real_add_commute])); +by (auto_tac (claset(), + simpset() addsimps [real_mult_assoc, real_add_commute])); qed "DERIV_pow"; (* NS version *) Goal "NSDERIV (%x. x ^ n) x :> real_of_nat n * (x ^ (n - 1))"; -by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff,DERIV_pow]) 1); +by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1); qed "NSDERIV_pow"; (*--------------------------------------------------------------- diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Thu Jan 04 10:23:01 2001 +0100 @@ -228,13 +228,10 @@ by Auto_tac; qed "HFiniteD"; -Goalw [HFinite_def] "x : HFinite ==> abs x : HFinite"; +Goalw [HFinite_def] "(abs x : HFinite) = (x : HFinite)"; by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent])); -qed "HFinite_hrabs"; - -Goalw [HFinite_def,Bex_def] "x ~: HFinite ==> abs x ~: HFinite"; -by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent])); -qed "not_HFinite_hrabs"; +qed "HFinite_hrabs_iff"; +AddIffs [HFinite_hrabs_iff]; Goal "number_of w : HFinite"; by (rtac (SReal_number_of RS (SReal_subset_HFinite RS subsetD)) 1); @@ -389,23 +386,13 @@ by Auto_tac; qed "not_Infinitesimal_not_zero2"; -Goal "x : Infinitesimal ==> abs x : Infinitesimal"; -by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1); -by Auto_tac; -qed "Infinitesimal_hrabs"; - -Goal "x ~: Infinitesimal ==> abs x ~: Infinitesimal"; -by (res_inst_tac [("x1","x")] (hrabs_disj RS disjE) 1); -by Auto_tac; -qed "not_Infinitesimal_hrabs"; - -Goal "abs x : Infinitesimal ==> x : Infinitesimal"; -by (rtac ccontr 1); -by (blast_tac (claset() addDs [not_Infinitesimal_hrabs]) 1); -qed "hrabs_Infinitesimal_Infinitesimal"; +Goal "(abs x : Infinitesimal) = (x : Infinitesimal)"; +by (auto_tac (claset(), simpset() addsimps [hrabs_def])); +qed "Infinitesimal_hrabs_iff"; +AddIffs [Infinitesimal_hrabs_iff]; Goal "x : HFinite - Infinitesimal ==> abs x : HFinite - Infinitesimal"; -by (fast_tac (set_cs addSEs [HFinite_hrabs,not_Infinitesimal_hrabs]) 1); +by (Blast_tac 1); qed "HFinite_diff_Infinitesimal_hrabs"; Goalw [Infinitesimal_def] @@ -417,8 +404,7 @@ Goal "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal"; by (blast_tac (claset() addDs [order_le_imp_less_or_eq] - addIs [hrabs_Infinitesimal_Infinitesimal, - hrabs_less_Infinitesimal]) 1); + addIs [hrabs_less_Infinitesimal]) 1); qed "hrabs_le_Infinitesimal"; Goalw [Infinitesimal_def] @@ -1091,8 +1077,7 @@ ------------------------------------------------------------------*) Goalw [HFinite_def,HInfinite_def] "HFinite Int HInfinite = {}"; -by (auto_tac (claset() addIs [hypreal_less_irrefl] - addDs [order_less_trans,bspec], +by (auto_tac (claset() addIs [hypreal_less_irrefl] addDs [order_less_trans], simpset())); qed "HFinite_Int_HInfinite_empty"; Addsimps [HFinite_Int_HInfinite_empty]; @@ -1102,15 +1087,10 @@ by Auto_tac; qed "HFinite_not_HInfinite"; -val [prem] = goalw thy [HInfinite_def] "x~: HFinite ==> x: HInfinite"; -by (cut_facts_tac [prem] 1); -by (Clarify_tac 1); -by (auto_tac (claset() addSDs [spec], - simpset() addsimps [HFinite_def,Bex_def])); -by (dtac hypreal_leI 1); -by (dtac order_le_imp_less_or_eq 1); -by (auto_tac (claset() addSDs [SReal_subset_HFinite RS subsetD], - simpset() addsimps [prem,hrabs_idempotent,prem RS not_HFinite_hrabs])); +Goalw [HInfinite_def, HFinite_def] "x~: HFinite ==> x: HInfinite"; +by Auto_tac; +by (dres_inst_tac [("x","r + #1")] bspec 1); +by (auto_tac (claset(), simpset() addsimps [SReal_add])); qed "not_HFinite_HInfinite"; Goal "x : HInfinite | x : HFinite"; @@ -1325,22 +1305,19 @@ simpset())); qed "less_Infinitesimal_less"; -Goal "[| #0 < x; x ~: Infinitesimal|] ==> ALL u: monad x. #0 < u"; -by (Step_tac 1); +Goal "[| #0 < x; x ~: Infinitesimal; u: monad x |] ==> #0 < u"; by (dtac (mem_monad_inf_close RS inf_close_sym) 1); by (etac (bex_Infinitesimal_iff2 RS iffD2 RS bexE) 1); by (dres_inst_tac [("e","-xa")] less_Infinitesimal_less 1); by Auto_tac; qed "Ball_mem_monad_gt_zero"; -Goal "[| x < #0; x ~: Infinitesimal|] ==> ALL u: monad x. u < #0"; -by (Step_tac 1); +Goal "[| x < #0; x ~: Infinitesimal; u: monad x |] ==> u < #0"; by (dtac (mem_monad_inf_close RS inf_close_sym) 1); by (etac (bex_Infinitesimal_iff RS iffD2 RS bexE) 1); by (cut_inst_tac [("x","-x"),("e","xa")] less_Infinitesimal_less 1); by Auto_tac; qed "Ball_mem_monad_less_zero"; -(*??GET RID OF QUANTIFIERS ABOVE??*) Goal "[|#0 < x; x ~: Infinitesimal; x @= y|] ==> #0 < y"; by (blast_tac (claset() addDs [Ball_mem_monad_gt_zero, @@ -1352,16 +1329,14 @@ inf_close_subset_monad]) 1); qed "lemma_inf_close_less_zero"; -Goal "[| x @= y; x < #0; x ~: Infinitesimal |] \ -\ ==> abs x @= abs y"; +Goal "[| x @= y; x < #0; x ~: Infinitesimal |] ==> abs x @= abs y"; by (forward_tac [lemma_inf_close_less_zero] 1); by (REPEAT(assume_tac 1)); by (REPEAT(dtac hrabs_minus_eqI2 1)); by Auto_tac; qed "inf_close_hrabs1"; -Goal "[| x @= y; #0 < x; x ~: Infinitesimal |] \ -\ ==> abs x @= abs y"; +Goal "[| x @= y; #0 < x; x ~: Infinitesimal |] ==> abs x @= abs y"; by (forward_tac [lemma_inf_close_gt_zero] 1); by (REPEAT(assume_tac 1)); by (REPEAT(dtac hrabs_eqI2 1)); @@ -1975,42 +1950,42 @@ (*------------------------------------------------------------------------ Infinitesimals as smaller than 1/n for all n::nat (> 0) ------------------------------------------------------------------------*) -Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real_of_posnat n))"; -by (auto_tac (claset(), - simpset() addsimps [rename_numerals real_of_posnat_gt_zero])); -by (blast_tac (claset() addSDs [rename_numerals reals_Archimedean] + +Goal "(ALL r. #0 < r --> x < r) = (ALL n. x < inverse(real_of_nat (Suc n)))"; +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc_gt_zero])); +by (blast_tac (claset() addSDs [reals_Archimedean] addIs [order_less_trans]) 1); qed "lemma_Infinitesimal"; Goal "(ALL r: SReal. #0 < r --> x < r) = \ -\ (ALL n. x < inverse(hypreal_of_posnat n))"; +\ (ALL n. x < inverse(hypreal_of_nat (Suc n)))"; by (Step_tac 1); -by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_posnat n))")] +by (dres_inst_tac [("x","inverse (hypreal_of_real(real_of_nat (Suc n)))")] bspec 1); by (full_simp_tac (simpset() addsimps [SReal_inverse]) 1); -by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero RS +by (rtac (real_of_nat_Suc_gt_zero RS rename_numerals real_inverse_gt_zero RS (hypreal_of_real_less_iff RS iffD2) RSN(2,impE)) 1); by (assume_tac 2); by (asm_full_simp_tac (simpset() addsimps - [rename_numerals real_of_posnat_gt_zero, hypreal_of_real_zero, - hypreal_of_real_of_posnat]) 1); + [real_of_nat_Suc_gt_zero, hypreal_of_real_zero, hypreal_of_nat_def]) 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 iffD2) 1); by (asm_full_simp_tac (simpset() addsimps - [rename_numerals real_of_posnat_gt_zero,hypreal_of_real_of_posnat])1); + [real_of_nat_Suc_gt_zero, hypreal_of_nat_def])1); by (blast_tac (claset() addIs [order_less_trans]) 1); qed "lemma_Infinitesimal2"; Goalw [Infinitesimal_def] - "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_posnat n)}"; + "Infinitesimal = {x. ALL n. abs x < inverse (hypreal_of_nat (Suc n))}"; by (auto_tac (claset(), simpset() addsimps [lemma_Infinitesimal2])); -qed "Infinitesimal_hypreal_of_posnat_iff"; +qed "Infinitesimal_hypreal_of_nat_iff"; + -(*----------------------------------------------------------------------------- - Actual proof that omega (whr) is an infinite number and +(*--------------------------------------------------------------------------- + Proof that omega (whr) is an infinite number and hence that epsilon (ehr) is an infinitesimal number. - -----------------------------------------------------------------------------*) + ---------------------------------------------------------------------------*) Goal "{n. n < Suc m} = {n. n < m} Un {n. n = m}"; by (auto_tac (claset(), simpset() addsimps [less_Suc_eq])); qed "Suc_Un_eq"; @@ -2024,72 +1999,85 @@ by (auto_tac (claset(), simpset() addsimps [Suc_Un_eq])); qed "finite_nat_segment"; -Goal "finite {n::nat. real_of_posnat n < real_of_posnat m}"; +Goal "finite {n::nat. real_of_nat n < real_of_nat m}"; by (auto_tac (claset() addIs [finite_nat_segment], simpset())); -qed "finite_real_of_posnat_segment"; +qed "finite_real_of_nat_segment"; -Goal "finite {n. real_of_posnat n < u}"; +Goal "finite {n. real_of_nat n < u}"; by (cut_inst_tac [("x","u")] reals_Archimedean2 1); by (Step_tac 1); -by (rtac (finite_real_of_posnat_segment RSN (2,finite_subset)) 1); +by (rtac (finite_real_of_nat_segment RSN (2,finite_subset)) 1); by (auto_tac (claset() addDs [order_less_trans], simpset())); -qed "finite_real_of_posnat_less_real"; +qed "finite_real_of_nat_less_real"; -Goal "{n. real_of_posnat n <= u} = \ -\ {n. real_of_posnat n < u} Un {n. u = real_of_posnat n}"; +Goal "{n. f n <= u} = {n. f n < u} Un {n. u = (f n :: real)}"; by (auto_tac (claset() addDs [order_le_imp_less_or_eq], simpset() addsimps [order_less_imp_le])); qed "lemma_real_le_Un_eq"; -Goal "finite {n. real_of_posnat n <= u}"; -by (auto_tac (claset(), simpset() addsimps - [lemma_real_le_Un_eq,lemma_finite_omega_set, - finite_real_of_posnat_less_real])); -qed "finite_real_of_posnat_le_real"; +Goal "finite {n. real_of_nat n <= u}"; +by (auto_tac (claset(), + simpset() addsimps [lemma_real_le_Un_eq,lemma_finite_omega_set, + finite_real_of_nat_less_real])); +qed "finite_real_of_nat_le_real"; -Goal "finite {n. abs(real_of_posnat n) <= u}"; -by (full_simp_tac (simpset() addsimps [rename_numerals - real_of_posnat_gt_zero,abs_eqI2, - finite_real_of_posnat_le_real]) 1); -qed "finite_rabs_real_of_posnat_le_real"; +Goal "finite {n. abs(real_of_nat n) <= u}"; +by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero, + finite_real_of_nat_le_real]) 1); +qed "finite_rabs_real_of_nat_le_real"; -Goal "{n. abs(real_of_posnat n) <= u} ~: FreeUltrafilterNat"; +Goal "{n. abs(real_of_nat n) <= u} ~: FreeUltrafilterNat"; by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite, - finite_rabs_real_of_posnat_le_real]) 1); -qed "rabs_real_of_posnat_le_real_FreeUltrafilterNat"; + finite_rabs_real_of_nat_le_real]) 1); +qed "rabs_real_of_nat_le_real_FreeUltrafilterNat"; -Goal "{n. u < real_of_posnat n} : FreeUltrafilterNat"; +Goal "{n. u < real_of_nat n} : FreeUltrafilterNat"; by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1); -by (auto_tac (claset(), simpset() addsimps - [CLAIM_SIMP "- {n. u < real_of_posnat n} = \ -\ {n. real_of_posnat n <= u}" - [real_le_def],finite_real_of_posnat_le_real - RS FreeUltrafilterNat_finite])); +by (subgoal_tac "- {n. u < real_of_nat n} = {n. real_of_nat n <= u}" 1); +by (Force_tac 2); +by (asm_full_simp_tac (simpset() addsimps + [finite_real_of_nat_le_real RS FreeUltrafilterNat_finite]) 1); qed "FreeUltrafilterNat_nat_gt_real"; (*-------------------------------------------------------------- - The complement of {n. abs(real_of_posnat n) <= u} = - {n. u < abs (real_of_posnat n)} is in FreeUltrafilterNat + The complement of {n. abs(real_of_nat n) <= u} = + {n. u < abs (real_of_nat n)} is in FreeUltrafilterNat by property of (free) ultrafilters --------------------------------------------------------------*) -Goal "- {n. abs (real_of_posnat n) <= u} = \ -\ {n. u < abs (real_of_posnat n)}"; +Goal "- {n. real_of_nat n <= u} = {n. u < real_of_nat n}"; by (auto_tac (claset() addSDs [order_le_less_trans], simpset() addsimps [not_real_leE])); val lemma = result(); -Goal "{n. u < abs (real_of_posnat n)} : FreeUltrafilterNat"; -by (cut_inst_tac [("u","u")] rabs_real_of_posnat_le_real_FreeUltrafilterNat 1); +Goal "{n. u < abs (real_of_nat n)} : FreeUltrafilterNat"; +by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1); by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem], - simpset() addsimps [lemma])); + simpset() addsimps [lemma])); qed "FreeUltrafilterNat_omega"; (*----------------------------------------------- Omega is a member of HInfinite -----------------------------------------------*) + +Goal "hyprel^^{%n::nat. real_of_nat (Suc n)} : hypreal"; +by Auto_tac; +qed "hypreal_omega"; + + +Goal "{n. u < real_of_nat n} : FreeUltrafilterNat"; +by (cut_inst_tac [("u","u")] rabs_real_of_nat_le_real_FreeUltrafilterNat 1); +by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem], + simpset() addsimps [lemma])); +qed "FreeUltrafilterNat_omega"; + Goalw [omega_def] "whr: HInfinite"; -by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite, - lemma_hyprel_refl,FreeUltrafilterNat_omega], simpset())); +by (auto_tac (claset() addSIs [FreeUltrafilterNat_HInfinite], + simpset())); +by (rtac bexI 1); +by (rtac lemma_hyprel_refl 2); +by Auto_tac; +by (simp_tac (simpset() addsimps [real_of_nat_Suc, real_diff_less_eq RS sym, + FreeUltrafilterNat_omega]) 1); qed "HInfinite_omega"; (*----------------------------------------------- @@ -2118,48 +2106,75 @@ that ALL n. |X n - a| < 1/n. Used in proof of NSLIM => LIM. -----------------------------------------------------------------------*) -Goal "#0 < u ==> finite {n. u < inverse(real_of_posnat n)}"; -by (asm_simp_tac (simpset() addsimps [real_of_posnat_less_inverse_iff]) 1); -by (rtac finite_real_of_posnat_less_real 1); +Goal "0 < u ==> \ +\ (u < inverse (real_of_nat(Suc n))) = (real_of_nat(Suc n) < inverse u)"; +by (asm_full_simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1); +by (stac pos_real_less_divide_eq 1); +by (assume_tac 1); +by (stac pos_real_less_divide_eq 1); +by (simp_tac (simpset() addsimps [real_mult_commute]) 2); +by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); +qed "real_of_nat_less_inverse_iff"; + +Goal "#0 < u ==> finite {n. u < inverse(real_of_nat(Suc n))}"; +by (asm_simp_tac (simpset() addsimps [real_of_nat_less_inverse_iff]) 1); +by (asm_simp_tac (simpset() addsimps [real_of_nat_Suc, + real_less_diff_eq RS sym]) 1); +by (rtac finite_real_of_nat_less_real 1); qed "finite_inverse_real_of_posnat_gt_real"; -Goal "{n. u <= inverse(real_of_posnat n)} = \ -\ {n. u < inverse(real_of_posnat n)} Un {n. u = inverse(real_of_posnat n)}"; +Goal "{n. u <= inverse(real_of_nat(Suc n))} = \ +\ {n. u < inverse(real_of_nat(Suc n))} Un {n. u = inverse(real_of_nat(Suc n))}"; by (auto_tac (claset() addDs [order_le_imp_less_or_eq], simpset() addsimps [order_less_imp_le])); qed "lemma_real_le_Un_eq2"; -Goal "#0 < u ==> finite {n::nat. u = inverse(real_of_posnat n)}"; -by (asm_simp_tac (simpset() addsimps [real_of_posnat_inverse_eq_iff]) 1); -by (auto_tac (claset() addIs [lemma_finite_omega_set RSN - (2,finite_subset)], simpset())); +Goal "(inverse (real_of_nat(Suc n)) <= r) = (#1 <= r * real_of_nat(Suc n))"; +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); +by (simp_tac (simpset() addsimps [real_inverse_eq_divide]) 1); +by (stac pos_real_less_divide_eq 1); +by (simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero]) 1); +by (simp_tac (simpset() addsimps [real_mult_commute]) 1); +qed "real_of_nat_inverse_le_iff"; + +Goal "(u = inverse (real_of_nat(Suc n))) = (real_of_nat(Suc n) = inverse u)"; +by (auto_tac (claset(), + simpset() addsimps [real_inverse_inverse, real_of_nat_Suc_gt_zero, + real_not_refl2 RS not_sym])); +qed "real_of_nat_inverse_eq_iff"; + +Goal "finite {n::nat. u = inverse(real_of_nat(Suc n))}"; +by (asm_simp_tac (simpset() addsimps [real_of_nat_inverse_eq_iff]) 1); +by (cut_inst_tac [("x","inverse u - #1")] lemma_finite_omega_set 1); +by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc, + real_diff_eq_eq RS sym, eq_commute]) 1); qed "lemma_finite_omega_set2"; -Goal "#0 < u ==> finite {n. u <= inverse(real_of_posnat n)}"; +Goal "#0 < u ==> finite {n. u <= inverse(real_of_nat(Suc n))}"; by (auto_tac (claset(), simpset() addsimps [lemma_real_le_Un_eq2,lemma_finite_omega_set2, finite_inverse_real_of_posnat_gt_real])); qed "finite_inverse_real_of_posnat_ge_real"; Goal "#0 < u ==> \ -\ {n. u <= inverse(real_of_posnat n)} ~: FreeUltrafilterNat"; +\ {n. u <= inverse(real_of_nat(Suc n))} ~: FreeUltrafilterNat"; by (blast_tac (claset() addSIs [FreeUltrafilterNat_finite, finite_inverse_real_of_posnat_ge_real]) 1); qed "inverse_real_of_posnat_ge_real_FreeUltrafilterNat"; (*-------------------------------------------------------------- - The complement of {n. u <= inverse(real_of_posnat n)} = - {n. inverse(real_of_posnat n) < u} is in FreeUltrafilterNat + The complement of {n. u <= inverse(real_of_nat(Suc n))} = + {n. inverse(real_of_nat(Suc n)) < u} is in FreeUltrafilterNat by property of (free) ultrafilters --------------------------------------------------------------*) -Goal "- {n. u <= inverse(real_of_posnat n)} = \ -\ {n. inverse(real_of_posnat n) < u}"; +Goal "- {n. u <= inverse(real_of_nat(Suc n))} = \ +\ {n. inverse(real_of_nat(Suc n)) < u}"; by (auto_tac (claset() addSDs [order_le_less_trans], simpset() addsimps [not_real_leE])); val lemma = result(); Goal "#0 < u ==> \ -\ {n. inverse(real_of_posnat n) < u} : FreeUltrafilterNat"; +\ {n. inverse(real_of_nat(Suc n)) < u} : FreeUltrafilterNat"; by (cut_inst_tac [("u","u")] inverse_real_of_posnat_ge_real_FreeUltrafilterNat 1); by (auto_tac (claset() addDs [FreeUltrafilterNat_Compl_mem], simpset() addsimps [lemma])); @@ -2176,7 +2191,7 @@ (*----------------------------------------------------- |X(n) - x| < 1/n ==> [] - hypreal_of_real x|: Infinitesimal -----------------------------------------------------*) -Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \ +Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ \ ==> Abs_hypreal(hyprel^^{X}) + -hypreal_of_real x : Infinitesimal"; by (auto_tac (claset() addSIs [bexI] addDs [rename_numerals FreeUltrafilterNat_inverse_real_of_posnat, @@ -2184,24 +2199,23 @@ addIs [order_less_trans, FreeUltrafilterNat_subset], simpset() addsimps [hypreal_minus, hypreal_of_real_def,hypreal_add, - Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse, - hypreal_of_real_of_posnat])); + Infinitesimal_FreeUltrafilterNat_iff,hypreal_inverse])); qed "real_seq_to_hypreal_Infinitesimal"; -Goal "ALL n. abs(X n + -x) < inverse(real_of_posnat n) \ +Goal "ALL n. abs(X n + -x) < inverse(real_of_nat(Suc n)) \ \ ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x"; by (rtac (inf_close_minus_iff RS ssubst) 1); by (rtac (mem_infmal_iff RS subst) 1); by (etac real_seq_to_hypreal_Infinitesimal 1); qed "real_seq_to_hypreal_inf_close"; -Goal "ALL n. abs(x + -X n) < inverse(real_of_posnat n) \ +Goal "ALL n. abs(x + -X n) < inverse(real_of_nat(Suc n)) \ \ ==> Abs_hypreal(hyprel^^{X}) @= hypreal_of_real x"; by (asm_full_simp_tac (simpset() addsimps [abs_minus_add_cancel, real_seq_to_hypreal_inf_close]) 1); qed "real_seq_to_hypreal_inf_close2"; -Goal "ALL n. abs(X n + -Y n) < inverse(real_of_posnat n) \ +Goal "ALL n. abs(X n + -Y n) < inverse(real_of_nat(Suc n)) \ \ ==> Abs_hypreal(hyprel^^{X}) + \ \ -Abs_hypreal(hyprel^^{Y}) : Infinitesimal"; by (auto_tac (claset() addSIs [bexI] @@ -2211,5 +2225,5 @@ addIs [order_less_trans, FreeUltrafilterNat_subset], simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,hypreal_minus,hypreal_add, - hypreal_inverse,hypreal_of_real_of_posnat])); + hypreal_inverse])); qed "real_seq_to_hypreal_Infinitesimal2"; diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/NatStar.ML --- a/src/HOL/Hyperreal/NatStar.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/NatStar.ML Thu Jan 04 10:23:01 2001 +0100 @@ -122,13 +122,13 @@ by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1); qed "NatStar_hypreal_of_real_image_subset"; -Goal "SHNat <= *sNat* (UNIV:: nat set)"; +Goal "SNat <= *sNat* (UNIV:: nat set)"; by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff, - NatStar_hypreal_of_real_image_subset]) 1); + NatStar_hypreal_of_real_image_subset]) 1); qed "NatStar_SHNat_subset"; Goalw [starsetNat_def] - "*sNat* X Int SHNat = hypnat_of_nat `` X"; + "*sNat* X Int SNat = hypnat_of_nat `` X"; by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def,SHNat_def])); diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/NatStar.thy --- a/src/HOL/Hyperreal/NatStar.thy Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/NatStar.thy Thu Jan 04 10:23:01 2001 +0100 @@ -5,7 +5,7 @@ sets of reals, and nat=>real, nat=>nat functions *) -NatStar = HyperNat + RealPow + HyperPow + +NatStar = RealPow + HyperPow + constdefs diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Thu Jan 04 10:23:01 2001 +0100 @@ -11,14 +11,13 @@ -------------------------------------------------------------------------- *) Goalw [hypnat_omega_def] - "(*fNat* (%n::nat. inverse(real_of_posnat n))) whn : Infinitesimal"; + "(*fNat* (%n::nat. inverse(real_of_nat(Suc n)))) whn : Infinitesimal"; by (auto_tac (claset(), simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat])); by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); by (auto_tac (claset(), - simpset() addsimps (map rename_numerals) - [real_of_posnat_gt_zero,real_inverse_gt_zero,abs_eqI2, - FreeUltrafilterNat_inverse_real_of_posnat])); + simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2, + FreeUltrafilterNat_inverse_real_of_posnat])); qed "SEQ_Infinitesimal"; (*-------------------------------------------------------------------------- @@ -423,45 +422,46 @@ qed "BseqI"; Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \ -\ (EX N. ALL n. abs(X n) <= real_of_posnat N)"; -by (auto_tac (claset(),simpset() addsimps - (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero])); -by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1); -by (blast_tac (claset() addIs [order_le_less_trans, order_less_imp_le]) 1); -by (auto_tac (claset(),simpset() addsimps [real_of_posnat_def])); +\ (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))"; +by Auto_tac; +by (Force_tac 2); +by (cut_inst_tac [("x","K")] reals_Archimedean2 1); +by (Clarify_tac 1); +by (res_inst_tac [("x","n")] exI 1); +by (Clarify_tac 1); +by (dres_inst_tac [("x","na")] spec 1); +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); qed "lemma_NBseq_def"; (* alternative definition for Bseq *) -Goalw [Bseq_def] - "Bseq X = (EX N. ALL n. abs(X n) <= real_of_posnat N)"; +Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) <= real_of_nat(Suc N))"; by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1); qed "Bseq_iff"; Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \ -\ (EX N. ALL n. abs(X n) < real_of_posnat N)"; -by (auto_tac (claset(),simpset() addsimps - (map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero])); -by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1); -by (blast_tac (claset() addIs [order_less_trans, order_le_less_trans]) 1); -by (auto_tac (claset() addIs [order_less_imp_le], - simpset() addsimps [real_of_posnat_def])); +\ (EX N. ALL n. abs(X n) < real_of_nat(Suc N))"; +by (stac lemma_NBseq_def 1); +by Auto_tac; +by (res_inst_tac [("x","Suc N")] exI 1); +by (res_inst_tac [("x","N")] exI 2); +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); +by (blast_tac (claset() addIs [order_less_imp_le]) 2); +by (dres_inst_tac [("x","n")] spec 1); +by (Asm_simp_tac 1); qed "lemma_NBseq_def2"; (* yet another definition for Bseq *) -Goalw [Bseq_def] - "Bseq X = (EX N. ALL n. abs(X n) < real_of_posnat N)"; +Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real_of_nat(Suc N))"; by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1); qed "Bseq_iff1a"; Goalw [NSBseq_def] - "[| NSBseq X; N: HNatInfinite |] \ -\ ==> (*fNat* X) N : HFinite"; + "[| NSBseq X; N: HNatInfinite |] ==> (*fNat* X) N : HFinite"; by (Blast_tac 1); qed "NSBseqD"; Goalw [NSBseq_def] - "ALL N: HNatInfinite. (*fNat* X) N : HFinite \ -\ ==> NSBseq X"; + "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X"; by (assume_tac 1); qed "NSBseqI"; @@ -469,17 +469,16 @@ Standard definition ==> NS definition ----------------------------------------------------------*) (* a few lemmas *) -Goal "ALL n. abs(X n) <= K ==> \ -\ ALL n. abs(X((f::nat=>nat) n)) <= K"; +Goal "ALL n. abs(X n) <= K ==> ALL n. abs(X((f::nat=>nat) n)) <= K"; by (Auto_tac); val lemma_Bseq = result(); Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X"; by (Step_tac 1); by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); -by (auto_tac (claset(),simpset() addsimps [starfunNat, - HFinite_FreeUltrafilterNat_iff, - HNatInfinite_FreeUltrafilterNat_iff])); +by (auto_tac (claset(), + simpset() addsimps [starfunNat, HFinite_FreeUltrafilterNat_iff, + HNatInfinite_FreeUltrafilterNat_iff])); by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]); by (dres_inst_tac [("f","Xa")] lemma_Bseq 1); by (res_inst_tac [("x","K+#1")] exI 1); @@ -500,79 +499,77 @@ -------------------------------------------------------------------*) Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \ -\ ==> ALL N. EX n. real_of_posnat N < abs (X n)"; +\ ==> ALL N. EX n. real_of_nat(Suc N) < abs (X n)"; by (Step_tac 1); -by (cut_inst_tac [("n","N")] (rename_numerals real_of_posnat_gt_zero) 1); +by (cut_inst_tac [("n","N")] real_of_nat_Suc_gt_zero 1); by (Blast_tac 1); val lemmaNSBseq = result(); Goal "ALL K. #0 < K --> (EX n. K < abs (X n)) \ -\ ==> EX f. ALL N. real_of_posnat N < abs (X (f N))"; +\ ==> EX f. ALL N. real_of_nat(Suc N) < abs (X (f N))"; by (dtac lemmaNSBseq 1); by (dtac choice 1); by (Blast_tac 1); val lemmaNSBseq2 = result(); -Goal "ALL N. real_of_posnat N < abs (X (f N)) \ +Goal "ALL N. real_of_nat(Suc N) < abs (X (f N)) \ \ ==> Abs_hypreal(hyprel^^{X o f}) : HInfinite"; -by (auto_tac (claset(),simpset() addsimps - [HInfinite_FreeUltrafilterNat_iff,o_def])); -by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, - Step_tac 1]); +by (auto_tac (claset(), + simpset() addsimps [HInfinite_FreeUltrafilterNat_iff,o_def])); +by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]); by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1); -by (blast_tac (claset() addDs [FreeUltrafilterNat_all, FreeUltrafilterNat_Int] - addIs [order_less_trans, FreeUltrafilterNat_subset]) 1); +by (dtac FreeUltrafilterNat_all 1); +by (etac (FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset) 1); +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); qed "real_seq_to_hypreal_HInfinite"; -(*-------------------------------------------------------------------------------- +(*----------------------------------------------------------------------------- Now prove that we can get out an infinite hypernatural as well defined using the skolem function f::nat=>nat above - --------------------------------------------------------------------------------*) + ----------------------------------------------------------------------------*) -Goal "{n. f n <= Suc u & real_of_posnat n < abs (X (f n))} <= \ -\ {n. f n <= u & real_of_posnat n < abs (X (f n))} \ -\ Un {n. real_of_posnat n < abs (X (Suc u))}"; -by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_imp_le], - simpset() addsimps [less_Suc_eq])); +Goal "{n. f n <= Suc u & real_of_nat(Suc n) < abs (X (f n))} <= \ +\ {n. f n <= u & real_of_nat(Suc n) < abs (X (f n))} \ +\ Un {n. real_of_nat(Suc n) < abs (X (Suc u))}"; +by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset())); val lemma_finite_NSBseq = result(); -Goal "finite {n. f n <= (u::nat) & real_of_posnat n < abs(X(f n))}"; +Goal "finite {n. f n <= (u::nat) & real_of_nat(Suc n) < abs(X(f n))}"; by (induct_tac "u" 1); -by (rtac (CLAIM "{n. f n <= (0::nat) & real_of_posnat n < abs (X (f n))} <= \ -\ {n. real_of_posnat n < abs (X 0)}" - RS finite_subset) 1); -by (rtac finite_real_of_posnat_less_real 1); -by (rtac (lemma_finite_NSBseq RS finite_subset) 1); -by (auto_tac (claset() addIs [finite_real_of_posnat_less_real], simpset())); +by (res_inst_tac [("B","{n. real_of_nat(Suc n) < abs(X 0)}")] finite_subset 1); +by (Force_tac 1); +by (rtac (lemma_finite_NSBseq RS finite_subset) 2); +by (auto_tac (claset() addIs [finite_real_of_nat_less_real], + simpset() addsimps [real_of_nat_Suc, real_less_diff_eq RS sym])); val lemma_finite_NSBseq2 = result(); -Goal "ALL N. real_of_posnat N < abs (X (f N)) \ +Goal "ALL N. real_of_nat(Suc N) < abs (X (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]); +by (auto_tac (claset(), + simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff])); +by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]); by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1); by (asm_full_simp_tac (simpset() addsimps [CLAIM_SIMP "- {n. u < (f::nat=>nat) n} \ \ = {n. f n <= u}" [le_def]]) 1); by (dtac FreeUltrafilterNat_all 1); by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); -by (auto_tac (claset(),simpset() addsimps - [CLAIM "({n. f n <= u} Int {n. real_of_posnat n < abs(X(f n))}) = \ -\ {n. f n <= (u::nat) & real_of_posnat n < abs(X(f n))}", +by (auto_tac (claset(), + simpset() addsimps + [CLAIM "({n. f n <= u} Int {n. real_of_nat(Suc n) < abs(X(f n))}) = \ +\ {n. f n <= (u::nat) & real_of_nat(Suc n) < abs(X(f n))}", lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite])); qed "HNatInfinite_skolem_f"; Goalw [Bseq_def,NSBseq_def] "NSBseq X ==> Bseq X"; by (rtac ccontr 1); -by (auto_tac (claset(),simpset() addsimps [real_le_def])); +by (auto_tac (claset(), simpset() addsimps [real_le_def])); by (dtac lemmaNSBseq2 1 THEN Step_tac 1); by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1); by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1); -by (auto_tac (claset(),simpset() addsimps [starfunNat, - o_def,HFinite_HInfinite_iff])); +by (auto_tac (claset(), + simpset() addsimps [starfunNat, o_def,HFinite_HInfinite_iff])); qed "NSBseq_Bseq"; (*---------------------------------------------------------------------- @@ -805,7 +802,7 @@ 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); +by (ultra_tac (claset(), simpset() addsimps [less_imp_le]) 1); val lemmaCauchy1 = result(); Goal "{n. ALL m n. M <= m & M <= (n::nat) --> abs (X m + - X n) < u} Int \ @@ -821,8 +818,9 @@ by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); by (rtac (inf_close_minus_iff RS iffD2) 1); by (rtac (mem_infmal_iff RS iffD1) 1); -by (auto_tac (claset(),simpset() addsimps [starfunNat, - hypreal_minus,hypreal_add,Infinitesimal_FreeUltrafilterNat_iff])); +by (auto_tac (claset(), + simpset() addsimps [starfunNat, hypreal_minus,hypreal_add, + Infinitesimal_FreeUltrafilterNat_iff])); by (EVERY[rtac bexI 1, Auto_tac]); by (dtac spec 1 THEN Auto_tac); by (dres_inst_tac [("M","M")] lemmaCauchy1 1); @@ -841,17 +839,17 @@ Goalw [Cauchy_def,NSCauchy_def] "NSCauchy X ==> Cauchy X"; by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]); -by (dtac choice 1 THEN auto_tac (claset(),simpset() - addsimps [all_conj_distrib])); -by (dtac choice 1 THEN step_tac (claset() addSDs - [all_conj_distrib RS iffD1]) 1); +by (dtac choice 1 THEN + auto_tac (claset(), simpset() addsimps [all_conj_distrib])); +by (dtac choice 1 THEN + step_tac (claset() addSDs [all_conj_distrib RS iffD1]) 1); by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1)); by (dtac bspec 1 THEN assume_tac 1); by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ^^ {fa})")] bspec 1 - THEN auto_tac (claset(),simpset() addsimps [starfunNat])); + THEN auto_tac (claset(), simpset() addsimps [starfunNat])); by (dtac (inf_close_minus_iff RS iffD1) 1); by (dtac (mem_infmal_iff RS iffD2) 1); -by (auto_tac (claset(),simpset() addsimps [hypreal_minus, +by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_add,Infinitesimal_FreeUltrafilterNat_iff])); by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac); by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); @@ -1076,8 +1074,8 @@ Goal "f ----NS> l ==> (%n. f(Suc n)) ----NS> l"; by (forward_tac [NSconvergentI RS (NSCauchy_NSconvergent_iff RS iffD2)] 1); -by (auto_tac (claset(),simpset() addsimps [NSCauchy_def, - NSLIMSEQ_def,starfunNat_shift_one])); +by (auto_tac (claset(), + simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one])); by (dtac bspec 1 THEN assume_tac 1); by (dtac bspec 1 THEN assume_tac 1); by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1); @@ -1093,8 +1091,8 @@ Goal "(%n. f(Suc n)) ----NS> l ==> f ----NS> l"; by (forward_tac [NSconvergentI RS (NSCauchy_NSconvergent_iff RS iffD2)] 1); -by (auto_tac (claset(),simpset() addsimps [NSCauchy_def, - NSLIMSEQ_def,starfunNat_shift_one])); +by (auto_tac (claset(), + simpset() addsimps [NSCauchy_def, NSLIMSEQ_def,starfunNat_shift_one])); by (dtac bspec 1 THEN assume_tac 1); by (dtac bspec 1 THEN assume_tac 1); by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1); @@ -1181,31 +1179,33 @@ (*-------------------------------------------------------------- Sequence 1/n --> 0 as n --> infinity -------------------------------------------------------------*) -Goal "(%n. inverse(real_of_posnat n)) ----> #0"; + +Goal "(%n. inverse(real_of_nat(Suc n))) ----> #0"; by (rtac LIMSEQ_inverse_zero 1 THEN Step_tac 1); by (cut_inst_tac [("x","y")] reals_Archimedean2 1); by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); -by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1); -by (dtac (real_of_posnat_less_iff RS iffD2) 1); -by (auto_tac (claset() addEs [order_less_trans], simpset())); -qed "LIMSEQ_inverse_real_of_posnat"; +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); +by (subgoal_tac "y < real_of_nat na" 1); +by (Asm_simp_tac 1); +by (blast_tac (claset() addIs [order_less_le_trans]) 1); +qed "LIMSEQ_inverse_real_of_nat"; -Goal "(%n. inverse(real_of_posnat n)) ----NS> #0"; +Goal "(%n. inverse(real_of_nat(Suc n))) ----NS> #0"; by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, - LIMSEQ_inverse_real_of_posnat]) 1); -qed "NSLIMSEQ_inverse_real_of_posnat"; + LIMSEQ_inverse_real_of_nat]) 1); +qed "NSLIMSEQ_inverse_real_of_nat"; (*-------------------------------------------- Sequence r + 1/n --> r as n --> infinity now easily proved --------------------------------------------*) -Goal "(%n. r + inverse(real_of_posnat n)) ----> r"; -by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat] - MRS LIMSEQ_add] 1); -by (Auto_tac); +Goal "(%n. r + inverse(real_of_nat(Suc n))) ----> r"; +by (cut_facts_tac + [ [LIMSEQ_const,LIMSEQ_inverse_real_of_nat] MRS LIMSEQ_add ] 1); +by Auto_tac; qed "LIMSEQ_inverse_real_of_posnat_add"; -Goal "(%n. r + inverse(real_of_posnat n)) ----NS> r"; +Goal "(%n. r + inverse(real_of_nat(Suc n))) ----NS> r"; by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, LIMSEQ_inverse_real_of_posnat_add]) 1); qed "NSLIMSEQ_inverse_real_of_posnat_add"; @@ -1214,24 +1214,24 @@ Also... --------------*) -Goal "(%n. r + -inverse(real_of_posnat n)) ----> r"; -by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat] - MRS LIMSEQ_add_minus] 1); +Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----> r"; +by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_nat] + MRS LIMSEQ_add_minus] 1); by (Auto_tac); qed "LIMSEQ_inverse_real_of_posnat_add_minus"; -Goal "(%n. r + -inverse(real_of_posnat n)) ----NS> r"; +Goal "(%n. r + -inverse(real_of_nat(Suc n))) ----NS> r"; by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, LIMSEQ_inverse_real_of_posnat_add_minus]) 1); qed "NSLIMSEQ_inverse_real_of_posnat_add_minus"; -Goal "(%n. r*( #1 + -inverse(real_of_posnat n))) ----> r"; +Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----> r"; by (cut_inst_tac [("b","#1")] ([LIMSEQ_const, LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1); by (Auto_tac); qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult"; -Goal "(%n. r*( #1 + -inverse(real_of_posnat n))) ----NS> r"; +Goal "(%n. r*( #1 + -inverse(real_of_nat(Suc n)))) ----NS> r"; by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1); qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult"; @@ -1349,8 +1349,9 @@ "X ----NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal"; by (dres_inst_tac [("x","whn")] bspec 1); by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1); -by (auto_tac (claset(),simpset() addsimps [hypnat_omega_def, - mem_infmal_iff RS sym,starfunNat,hypreal_of_real_zero])); +by (auto_tac (claset(), + simpset() addsimps [hypnat_omega_def, mem_infmal_iff RS sym, + starfunNat,hypreal_of_real_zero])); qed "NSLIMSEQ_zero_Infinitesimal_hypreal"; (***--------------------------------------------------------------- @@ -1366,3 +1367,5 @@ Goal "subseq f ==> n <= f(n)"; Goal "subseq f ==> EX n. N1 <= n & N2 <= f(n)"; ---------------------------------------------------------------***) + + diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/Series.ML --- a/src/HOL/Hyperreal/Series.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/Series.ML Thu Jan 04 10:23:01 2001 +0100 @@ -67,8 +67,9 @@ Goal "sumr 0 n (%i. r) = real_of_nat n*r"; by (induct_tac "n" 1); -by (auto_tac (claset(),simpset() addsimps - [real_add_mult_distrib,real_of_nat_zero])); +by (auto_tac (claset(), + simpset() addsimps [real_add_mult_distrib,real_of_nat_zero, + real_of_nat_Suc])); qed "sumr_const"; Addsimps [sumr_const]; @@ -118,10 +119,9 @@ by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2); by (Step_tac 1); by (dres_inst_tac [("x","n")] spec 3); -by (auto_tac (claset() addSDs [le_imp_less_or_eq], - simpset())); -by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, - Suc_diff_n]) 1); +by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset())); +by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, Suc_diff_n, + real_of_nat_Suc]) 1); qed_spec_mp "sumr_interval_const"; Goal "(ALL n. m <= n --> f n = r) & m <= na \ @@ -133,20 +133,14 @@ by (dres_inst_tac [("x","n")] spec 3); by (auto_tac (claset() addSDs [le_imp_less_or_eq], simpset())); -by (asm_simp_tac (simpset() addsimps [Suc_diff_n, - real_add_mult_distrib]) 1); +by (asm_simp_tac (simpset() addsimps [Suc_diff_n, real_add_mult_distrib, + real_of_nat_Suc]) 1); qed_spec_mp "sumr_interval_const2"; -Goal "(m <= n)= (m < Suc n)"; -by (Auto_tac); -qed "le_eq_less_Suc"; - -Goal "(ALL n. m <= n --> #0 <= f n) & m < na \ -\ --> sumr 0 m f <= sumr 0 na f"; -by (induct_tac "na" 1); +Goal "(ALL n. m <= n --> #0 <= f n) & m < k --> sumr 0 m f <= sumr 0 k f"; +by (induct_tac "k" 1); by (Step_tac 1); -by (ALLGOALS(asm_full_simp_tac (simpset() addsimps - [le_eq_less_Suc RS sym]))); +by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le]))); by (ALLGOALS(dres_inst_tac [("x","n")] spec)); by (Step_tac 1); by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); @@ -235,14 +229,14 @@ \ --> (sumr m (m + n) f <= (real_of_nat n * K))"; by (induct_tac "n" 1); by (auto_tac (claset() addIs [real_add_le_mono], - simpset() addsimps [real_add_mult_distrib])); + simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); qed_spec_mp "sumr_bound"; Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \ \ --> (sumr 0 n f <= (real_of_nat n * K))"; by (induct_tac "n" 1); by (auto_tac (claset() addIs [real_add_le_mono], - simpset() addsimps [real_add_mult_distrib])); + simpset() addsimps [real_add_mult_distrib, real_of_nat_Suc])); qed_spec_mp "sumr_bound2"; Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"; @@ -543,14 +537,13 @@ (*------------------------------------------------------------------- The ratio test -------------------------------------------------------------------*) + Goal "[| c <= #0; abs x <= c * abs y |] ==> x = (#0::real)"; by (dtac order_le_imp_less_or_eq 1); -by Auto_tac; -by (dres_inst_tac [("x1","y")] - (abs_ge_zero RS rename_numerals real_mult_le_zero) 1); -by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1); -by (dtac order_trans 1 THEN assume_tac 1); -by (TRYALL(arith_tac)); +by Auto_tac; +by (subgoal_tac "#0 <= c * abs y" 1); +by (arith_tac 2); +by (asm_full_simp_tac (simpset() addsimps [real_0_le_mult_iff]) 1); qed "rabs_ratiotest_lemma"; (* lemmas *) @@ -599,9 +592,9 @@ qed "ratio_test"; -(*----------------------------------------------------------------------------*) -(* Differentiation of finite sum *) -(*----------------------------------------------------------------------------*) +(*--------------------------------------------------------------------------*) +(* Differentiation of finite sum *) +(*--------------------------------------------------------------------------*) Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \ \ --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"; diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Hyperreal/Star.ML --- a/src/HOL/Hyperreal/Star.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Hyperreal/Star.ML Thu Jan 04 10:23:01 2001 +0100 @@ -451,25 +451,28 @@ qed "STAR_starfun_rabs_add_minus"; (*------------------------------------------------------------------- - Another charaterization of Infinitesimal and one of @= relation. + Another characterization of Infinitesimal and one of @= relation. In this theory since hypreal_hrabs proved here. (To Check:) Maybe move both if possible? -------------------------------------------------------------------*) Goal "(x:Infinitesimal) = \ \ (EX X:Rep_hypreal(x). \ -\ ALL m. {n. abs(X n) < inverse(real_of_posnat m)}:FreeUltrafilterNat)"; +\ ALL m. {n. abs(X n) < inverse(real_of_nat(Suc m))} \ +\ : FreeUltrafilterNat)"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl], - simpset() addsimps [Infinitesimal_hypreal_of_posnat_iff, - hypreal_of_real_of_posnat,hypreal_of_real_def,hypreal_inverse, - hypreal_hrabs,hypreal_less])); + simpset() addsimps [Infinitesimal_hypreal_of_nat_iff, + hypreal_of_real_def,hypreal_inverse, + hypreal_hrabs,hypreal_less, hypreal_of_nat_def])); +by (asm_full_simp_tac (simpset() addsimps [real_of_nat_Suc_gt_zero, + real_not_refl2 RS not_sym]) 1) ; by (dres_inst_tac [("x","n")] spec 1); by (Fuf_tac 1); qed "Infinitesimal_FreeUltrafilterNat_iff2"; Goal "(Abs_hypreal(hyprel^^{X}) @= Abs_hypreal(hyprel^^{Y})) = \ \ (ALL m. {n. abs (X n + - Y n) < \ -\ inverse(real_of_posnat m)} : FreeUltrafilterNat)"; +\ inverse(real_of_nat(Suc m))} : FreeUltrafilterNat)"; by (rtac (inf_close_minus_iff RS ssubst) 1); by (rtac (mem_infmal_iff RS subst) 1); by (auto_tac (claset(), @@ -485,8 +488,3 @@ by (dres_inst_tac [("x","Abs_hypreal(hyprel ^^{%n. xa})")] fun_cong 1); by (auto_tac (claset(),simpset() addsimps [starfun])); qed "inj_starfun"; - - - - - diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Real/RComplete.ML --- a/src/HOL/Real/RComplete.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Real/RComplete.ML Thu Jan 04 10:23:01 2001 +0100 @@ -194,51 +194,61 @@ Related: Archimedean property of reals ----------------------------------------------------------------*) -Goal "#0 < x ==> EX n. inverse (real_of_posnat n) < x"; -by (stac real_of_posnat_inverse_Ex_iff 1); -by (EVERY1[rtac ccontr, Asm_full_simp_tac]); -by (fold_tac [real_le_def]); +Goal "#0 < real_of_nat (Suc n)"; +by (res_inst_tac [("y","real_of_nat n")] order_le_less_trans 1); +by (rtac (rename_numerals real_of_nat_ge_zero) 1); +by (simp_tac (simpset() addsimps [real_of_nat_Suc]) 1); +qed "real_of_nat_Suc_gt_zero"; + +Goal "#0 < x ==> EX n. inverse (real_of_nat(Suc n)) < x"; +by (rtac ccontr 1); +by (subgoal_tac "ALL n. x * real_of_nat (Suc n) <= #1" 1); +by (asm_full_simp_tac + (simpset() addsimps [linorder_not_less, real_inverse_eq_divide]) 2); +by (Clarify_tac 2); +by (dres_inst_tac [("x","n")] spec 2); +by (dres_inst_tac [("z","real_of_nat (Suc n)")] + (rotate_prems 1 real_mult_le_le_mono1) 2); +by (rtac real_of_nat_ge_zero 2); +by (asm_full_simp_tac (simpset() + addsimps [real_of_nat_Suc_gt_zero RS real_not_refl2 RS not_sym, + real_mult_commute]) 2); by (subgoal_tac "isUb (UNIV::real set) \ -\ {z. EX n. z = x*(real_of_posnat n)} #1" 1); -by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_posnat n)}" 1); +\ {z. EX n. z = x*(real_of_nat (Suc n))} #1" 1); +by (subgoal_tac "EX X. X : {z. EX n. z = x*(real_of_nat (Suc n))}" 1); by (dtac reals_complete 1); by (auto_tac (claset() addIs [isUbI,setleI],simpset())); -by (subgoal_tac "ALL m. x*(real_of_posnat(Suc m)) <= t" 1); +by (subgoal_tac "ALL m. x*(real_of_nat(Suc m)) <= t" 1); by (asm_full_simp_tac (simpset() addsimps - [real_of_posnat_Suc,real_add_mult_distrib2]) 1); + [real_of_nat_Suc, real_add_mult_distrib2]) 1); by (blast_tac (claset() addIs [isLubD2]) 2); by (asm_full_simp_tac (simpset() addsimps [real_le_diff_eq RS sym, real_diff_def]) 1); by (subgoal_tac "isUb (UNIV::real set) \ -\ {z. EX n. z = x*(real_of_posnat n)} (t + (-x))" 1); +\ {z. EX n. z = x*(real_of_nat (Suc n))} (t + (-x))" 1); by (blast_tac (claset() addSIs [isUbI,setleI]) 2); by (dres_inst_tac [("y","t+(-x)")] isLub_le_isUb 1); -by (dres_inst_tac [("x","-t")] real_add_left_le_mono1 2); -by (auto_tac (claset() addDs [order_le_less_trans, - real_minus_zero_less_iff2 RS iffD2], - simpset() addsimps [real_add_assoc RS sym])); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_Suc,real_add_mult_distrib2])); qed "reals_Archimedean"; -Goal "EX n. (x::real) < real_of_posnat n"; +(*There must be other proofs, e.g. Suc of the largest integer in the + cut representing x*) +Goal "EX n. (x::real) < real_of_nat n"; by (res_inst_tac [("R1.0","x"),("R2.0","#0")] real_linear_less2 1); by (res_inst_tac [("x","0")] exI 1); -by (res_inst_tac [("x","0")] exI 2); +by (res_inst_tac [("x","1")] exI 2); by (auto_tac (claset() addEs [order_less_trans], - simpset() addsimps [real_of_posnat_one,real_zero_less_one])); + simpset() addsimps [real_of_nat_one])); by (ftac ((rename_numerals real_inverse_gt_zero) RS reals_Archimedean) 1); -by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); +by (Step_tac 1 THEN res_inst_tac [("x","Suc n")] exI 1); by (forw_inst_tac [("y","inverse x")] (rename_numerals real_mult_less_mono1) 1); -by (auto_tac (claset(),simpset() addsimps [real_not_refl2 RS not_sym])); -by (dres_inst_tac [("n1","n"),("y","#1")] - (real_of_posnat_gt_zero RS real_mult_less_mono2) 1); +by Auto_tac; +by (dres_inst_tac [("y","#1"),("z","real_of_nat (Suc n)")] + (rotate_prems 1 real_mult_less_mono2) 1); by (auto_tac (claset(), - simpset() addsimps [rename_numerals real_of_posnat_gt_zero, + simpset() addsimps [real_of_nat_Suc_gt_zero, real_not_refl2 RS not_sym, real_mult_assoc RS sym])); qed "reals_Archimedean2"; - - - - - diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Real/RealArith0.ML --- a/src/HOL/Real/RealArith0.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Real/RealArith0.ML Thu Jan 04 10:23:01 2001 +0100 @@ -86,6 +86,11 @@ qed "real_divide_eq_0_iff"; Addsimps [real_divide_eq_0_iff]; +Goal "h ~= (#0::real) ==> h/h = #1"; +by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_inv_left]) 1); +qed "real_divide_self_eq"; +Addsimps [real_divide_self_eq]; + (**** Factor cancellation theorems for "real" ****) @@ -524,6 +529,25 @@ by (asm_simp_tac (simpset() addsimps [min_def]) 1); qed "real_lbound_gt_zero"; +Goal "(inverse x = inverse y) = (x = (y::real))"; +by (case_tac "x=#0 | y=#0" 1); +by (auto_tac (claset(), + simpset() addsimps [real_inverse_eq_divide, + rename_numerals DIVISION_BY_ZERO])); +by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1); +by (Asm_full_simp_tac 1); +qed "real_inverse_eq_iff"; +Addsimps [real_inverse_eq_iff]; + +Goal "(z/x = z/y) = (z = #0 | x = (y::real))"; +by (case_tac "x=#0 | y=#0" 1); +by (auto_tac (claset(), + simpset() addsimps [rename_numerals DIVISION_BY_ZERO])); +by (dres_inst_tac [("f","%u. x*y*u")] arg_cong 1); +by Auto_tac; +qed "real_divide_eq_iff"; +Addsimps [real_divide_eq_iff]; + (*** General rewrites to improve automation, like those for type "int" ***) diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Real/RealDef.thy --- a/src/HOL/Real/RealDef.thy Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Real/RealDef.thy Thu Jan 04 10:23:01 2001 +0100 @@ -23,9 +23,10 @@ consts "1r" :: real ("1r") - (*Overloaded constant: denotes the Real subset of enclosing types such as - hypreal and complex*) - SReal :: "'a set" + (*Overloaded constants denoting the Nat and Real subsets of enclosing + types such as hypreal and complex*) + SNat, SReal :: "'a set" + defs @@ -80,5 +81,6 @@ syntax (symbols) SReal :: "'a set" ("\\") + SNat :: "'a set" ("\\") end diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Real/RealOrd.ML --- a/src/HOL/Real/RealOrd.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Real/RealOrd.ML Thu Jan 04 10:23:01 2001 +0100 @@ -142,24 +142,6 @@ simpset())); qed "real_less_le_mult_order"; -Goal "[| x <= 0; y <= 0 |] ==> (0::real) <= x * y"; -by (rtac real_less_or_eq_imp_le 1); -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1); -by Auto_tac; -by (dtac order_le_imp_less_or_eq 1); -by (auto_tac (claset() addDs [real_mult_less_zero1],simpset())); -qed "real_mult_le_zero1"; - -Goal "[| 0 <= x; y < 0 |] ==> x * y <= (0::real)"; -by (rtac real_less_or_eq_imp_le 1); -by (dtac order_le_imp_less_or_eq 1 THEN etac disjE 1); -by Auto_tac; -by (dtac (real_minus_zero_less_iff RS iffD2) 1); -by (rtac (real_minus_zero_less_iff RS subst) 1); -by (blast_tac (claset() addDs [real_mult_order] - addIs [real_minus_mult_eq2 RS ssubst]) 1); -qed "real_mult_le_zero"; - Goal "[| 0 < x; y < 0 |] ==> x*y < (0::real)"; by (dtac (real_minus_zero_less_iff RS iffD2) 1); by (dtac real_mult_order 1 THEN assume_tac 1); @@ -281,11 +263,6 @@ by (auto_tac (claset(), simpset() addsimps [real_add_assoc])); qed "real_le_minus_iff"; Addsimps [real_le_minus_iff]; - -Goal "0 <= 1r"; -by (rtac (real_zero_less_one RS order_less_imp_le) 1); -qed "real_zero_le_one"; -Addsimps [real_zero_le_one]; Goal "(0::real) <= x*x"; by (res_inst_tac [("R2.0","0"),("R1.0","x")] real_linear_less2 1); @@ -300,19 +277,18 @@ ----------------------------------------------------------------------------*) Goalw [real_of_posnat_def] "real_of_posnat 0 = 1r"; -by (full_simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def]) 1); -by (fold_tac [real_one_def]); -by (rtac refl 1); +by (simp_tac (simpset() addsimps [pnat_one_iff RS sym,real_of_preal_def, + symmetric real_one_def]) 1); qed "real_of_posnat_one"; Goalw [real_of_posnat_def] "real_of_posnat 1 = 1r + 1r"; -by (full_simp_tac (simpset() addsimps [real_of_preal_def,real_one_def, - pnat_two_eq,real_add,prat_of_pnat_add RS sym,preal_of_prat_add RS sym - ] @ pnat_add_ac) 1); +by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def, + pnat_two_eq,real_add,prat_of_pnat_add RS sym, + preal_of_prat_add RS sym] @ pnat_add_ac) 1); qed "real_of_posnat_two"; Goalw [real_of_posnat_def] - "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r"; + "real_of_posnat n1 + real_of_posnat n2 = real_of_posnat (n1 + n2) + 1r"; by (full_simp_tac (simpset() addsimps [real_of_posnat_one RS sym, real_of_posnat_def,real_of_preal_add RS sym,preal_of_prat_add RS sym, prat_of_pnat_add RS sym,pnat_of_nat_add]) 1); @@ -338,40 +314,96 @@ by (etac (inj_pnat_of_nat RS injD) 1); qed "inj_real_of_posnat"; -Goalw [real_of_posnat_def] "0 < real_of_posnat n"; -by (rtac (real_gt_zero_preal_Ex RS iffD2) 1); -by (Blast_tac 1); -qed "real_of_posnat_gt_zero"; +Goalw [real_of_nat_def] "real_of_nat 0 = 0"; +by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1); +qed "real_of_nat_zero"; + +Goalw [real_of_nat_def] "real_of_nat 1 = 1r"; +by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1); +qed "real_of_nat_one"; +Addsimps [real_of_nat_zero, real_of_nat_one]; + +Goalw [real_of_nat_def] + "real_of_nat (m + n) = real_of_nat m + real_of_nat n"; +by (simp_tac (simpset() addsimps + [real_of_posnat_add,real_add_assoc RS sym]) 1); +qed "real_of_nat_add"; -Goal "real_of_posnat n ~= 0"; -by (rtac (real_of_posnat_gt_zero RS real_not_refl2 RS not_sym) 1); -qed "real_of_posnat_not_eq_zero"; -Addsimps[real_of_posnat_not_eq_zero]; +(*Not for addsimps: often the LHS is used to represent a positive natural*) +Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r"; +by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1); +qed "real_of_nat_Suc"; + +Goalw [real_of_nat_def, real_of_posnat_def] + "(real_of_nat n < real_of_nat m) = (n < m)"; +by Auto_tac; +qed "real_of_nat_less_iff"; +AddIffs [real_of_nat_less_iff]; -Goal "1r <= real_of_posnat n"; -by (simp_tac (simpset() addsimps [real_of_posnat_one RS sym]) 1); +Goal "(real_of_nat n <= real_of_nat m) = (n <= m)"; +by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); +qed "real_of_nat_le_iff"; +AddIffs [real_of_nat_le_iff]; + +Goal "inj real_of_nat"; +by (rtac injI 1); +by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD], + simpset() addsimps [real_of_nat_def,real_add_right_cancel])); +qed "inj_real_of_nat"; + +Goal "0 <= real_of_nat n"; by (induct_tac "n" 1); by (auto_tac (claset(), - simpset () addsimps [real_of_posnat_Suc,real_of_posnat_one, - real_of_posnat_gt_zero, order_less_imp_le])); -qed "real_of_posnat_less_one"; -Addsimps [real_of_posnat_less_one]; + simpset () addsimps [real_of_nat_Suc])); +by (dtac real_add_le_less_mono 1); +by (rtac real_zero_less_one 1); +by (asm_full_simp_tac (simpset() addsimps [order_less_imp_le]) 1); +qed "real_of_nat_ge_zero"; +AddIffs [real_of_nat_ge_zero]; + +Goal "real_of_nat (m * n) = real_of_nat m * real_of_nat n"; +by (induct_tac "m" 1); +by (auto_tac (claset(), + simpset() addsimps [real_of_nat_add, real_of_nat_Suc, + real_add_mult_distrib, real_add_commute])); +qed "real_of_nat_mult"; + +Goal "(real_of_nat n = real_of_nat m) = (n = m)"; +by (auto_tac (claset() addDs [inj_real_of_nat RS injD], simpset())); +qed "real_of_nat_eq_cancel"; +Addsimps [real_of_nat_eq_cancel]; -Goal "inverse (real_of_posnat n) ~= 0"; -by (rtac ((real_of_posnat_gt_zero RS - real_not_refl2 RS not_sym) RS real_inverse_not_zero) 1); -qed "real_of_posnat_inverse_not_zero"; -Addsimps [real_of_posnat_inverse_not_zero]; +Goal "n <= m --> real_of_nat (m - n) = real_of_nat m + (-real_of_nat n)"; +by (induct_tac "m" 1); +by (auto_tac (claset(), + simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc, + real_of_nat_zero] @ real_add_ac)); +qed_spec_mp "real_of_nat_minus"; + +Goalw [real_diff_def] + "n < m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n"; +by (auto_tac (claset() addIs [real_of_nat_minus], simpset())); +qed "real_of_nat_diff"; -Goal "inverse (real_of_posnat x) = inverse (real_of_posnat y) ==> x = y"; -by (rtac (inj_real_of_posnat RS injD) 1); -by (res_inst_tac [("n2","x")] - (real_of_posnat_inverse_not_zero RS real_mult_left_cancel RS iffD1) 1); -by (full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS - real_not_refl2 RS not_sym) RS real_mult_inv_left]) 1); -by (asm_full_simp_tac (simpset() addsimps [(real_of_posnat_gt_zero RS - real_not_refl2 RS not_sym)]) 1); -qed "real_of_posnat_inverse_inj"; +Goalw [real_diff_def] + "n <= m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n"; +by (etac real_of_nat_minus 1); +qed "real_of_nat_diff2"; + +Goal "(real_of_nat n = 0) = (n = 0)"; +by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset())); +qed "real_of_nat_zero_iff"; +Addsimps [real_of_nat_zero_iff]; + +Goal "neg z ==> real_of_nat (nat z) = 0"; +by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1); +qed "real_of_nat_neg_int"; +Addsimps [real_of_nat_neg_int]; + + +(*---------------------------------------------------------------------------- + inverse, etc. + ----------------------------------------------------------------------------*) Goal "0 < x ==> 0 < inverse (x::real)"; by (EVERY1[rtac ccontr, dtac real_leI]); @@ -392,40 +424,6 @@ by (auto_tac (claset() addIs [real_inverse_gt_zero], simpset())); qed "real_inverse_less_zero"; -Goal "0 < inverse (real_of_posnat n)"; -by (rtac (real_of_posnat_gt_zero RS real_inverse_gt_zero) 1); -qed "real_of_posnat_inverse_gt_zero"; -Addsimps [real_of_posnat_inverse_gt_zero]; - -Goal "real_of_preal (preal_of_prat (prat_of_pnat (pnat_of_nat N))) = \ -\ real_of_nat (Suc N)"; -by (simp_tac (simpset() addsimps [real_of_nat_def,real_of_posnat_Suc, - real_add_assoc,(real_of_posnat_def RS meta_eq_to_obj_eq) RS sym]) 1); -qed "real_of_preal_real_of_nat_Suc"; - -Goal "x+x = x*(1r+1r)"; -by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1); -qed "real_add_self"; - -Goal "x < x + 1r"; -by (rtac (real_less_sum_gt_0_iff RS iffD1) 1); -by (full_simp_tac (simpset() addsimps [real_zero_less_one, - real_add_assoc, real_add_left_commute]) 1); -qed "real_self_less_add_one"; - -Goal "1r < 1r + 1r"; -by (rtac real_self_less_add_one 1); -qed "real_one_less_two"; - -Goal "0 < 1r + 1r"; -by (rtac ([real_zero_less_one, real_one_less_two] MRS order_less_trans) 1); -qed "real_zero_less_two"; - -Goal "1r + 1r ~= 0"; -by (rtac (real_zero_less_two RS real_not_refl2 RS not_sym) 1); -qed "real_two_not_zero"; -Addsimps [real_two_not_zero]; - Goal "[| (0::real) < z; x < y |] ==> x*z < y*z"; by (rotate_tac 1 1); by (dtac real_less_sum_gt_zero 1); @@ -550,66 +548,6 @@ by (auto_tac (claset() addIs [real_mult_self_le], simpset())); qed "real_mult_self_le2"; -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 - RS real_mult_less_mono1) 1); -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS - real_inverse_gt_zero RS real_mult_less_mono1) 2); -by (auto_tac (claset(), - simpset() addsimps [(real_of_posnat_gt_zero RS - real_not_refl2 RS not_sym), - real_mult_assoc])); -qed "real_of_posnat_inverse_Ex_iff"; - -Goal "(inverse(real_of_posnat n) < r) = (1r < r * real_of_posnat n)"; -by (Step_tac 1); -by (dres_inst_tac [("n1","n")] (real_of_posnat_gt_zero - RS real_mult_less_mono1) 1); -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS - real_inverse_gt_zero RS real_mult_less_mono1) 2); -by (auto_tac (claset(), simpset() addsimps [real_mult_assoc])); -qed "real_of_posnat_inverse_iff"; - -Goal "(inverse (real_of_posnat n) <= r) = (1r <= r * real_of_posnat n)"; -by (Step_tac 1); -by (dres_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS - order_less_imp_le RS real_mult_le_le_mono1) 1); -by (dres_inst_tac [("n3","n")] (real_of_posnat_gt_zero RS - real_inverse_gt_zero RS order_less_imp_le RS - real_mult_le_le_mono1) 2); -by (auto_tac (claset(), simpset() addsimps real_mult_ac)); -qed "real_of_posnat_inverse_le_iff"; - -Goalw [real_of_posnat_def] "(real_of_posnat n < real_of_posnat m) = (n < m)"; -by Auto_tac; -qed "real_of_posnat_less_iff"; - -Addsimps [real_of_posnat_less_iff]; - -Goal "0 < u ==> (u < inverse (real_of_posnat n)) = (real_of_posnat n < inverse u)"; -by (Step_tac 1); -by (res_inst_tac [("n2","n")] (real_of_posnat_gt_zero RS - real_inverse_gt_zero RS real_mult_less_cancel1) 1); -by (res_inst_tac [("x1","u")] ( real_inverse_gt_zero - RS real_mult_less_cancel1) 2); -by (auto_tac (claset(), - simpset() addsimps [real_of_posnat_gt_zero, - real_not_refl2 RS not_sym])); -by (res_inst_tac [("z","u")] real_mult_less_cancel2 1); -by (res_inst_tac [("n1","n")] (real_of_posnat_gt_zero RS - real_mult_less_cancel2) 3); -by (auto_tac (claset(), - simpset() addsimps [real_of_posnat_gt_zero, - real_not_refl2 RS not_sym,real_mult_assoc RS sym])); -qed "real_of_posnat_less_inverse_iff"; - -Goal "0 < u ==> (u = inverse (real_of_posnat n)) = (real_of_posnat n = inverse u)"; -by (auto_tac (claset(), - simpset() addsimps [real_inverse_inverse, real_of_posnat_gt_zero, - real_not_refl2 RS not_sym])); -qed "real_of_posnat_inverse_eq_iff"; - Goal "[| 0 < r; r < x |] ==> inverse x < inverse (r::real)"; by (ftac order_less_trans 1 THEN assume_tac 1); by (ftac real_inverse_gt_zero 1); @@ -625,65 +563,14 @@ not_sym RS real_mult_inv_left,real_mult_assoc RS sym]) 1); qed "real_inverse_less_swap"; -Goal "r < r + inverse (real_of_posnat n)"; -by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); -by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym]) 1); -qed "real_add_inverse_real_of_posnat_less"; -Addsimps [real_add_inverse_real_of_posnat_less]; - -Goal "r <= r + inverse (real_of_posnat n)"; -by (rtac order_less_imp_le 1); -by (Simp_tac 1); -qed "real_add_inverse_real_of_posnat_le"; -Addsimps [real_add_inverse_real_of_posnat_le]; - -Goal "r + (-inverse (real_of_posnat n)) < r"; -by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); -by (full_simp_tac (simpset() addsimps [real_add_assoc RS sym, - real_minus_zero_less_iff2]) 1); -qed "real_add_minus_inverse_real_of_posnat_less"; -Addsimps [real_add_minus_inverse_real_of_posnat_less]; - -Goal "r + (-inverse (real_of_posnat n)) <= r"; -by (rtac order_less_imp_le 1); -by (Simp_tac 1); -qed "real_add_minus_inverse_real_of_posnat_le"; -Addsimps [real_add_minus_inverse_real_of_posnat_le]; - -Goal "0 < r ==> r*(1r + (-inverse (real_of_posnat n))) < r"; -by (simp_tac (simpset() addsimps [real_add_mult_distrib2]) 1); -by (res_inst_tac [("C","-r")] real_less_add_left_cancel 1); -by (auto_tac (claset() addIs [real_mult_order], - simpset() addsimps [real_add_assoc RS sym, - real_minus_zero_less_iff2])); -qed "real_mult_less_self"; - -Goal "0 <= 1r + (-inverse (real_of_posnat n))"; -by (res_inst_tac [("C","inverse (real_of_posnat n)")] real_le_add_right_cancel 1); -by (simp_tac (simpset() addsimps [real_add_assoc, - real_of_posnat_inverse_le_iff]) 1); -qed "real_add_one_minus_inverse_ge_zero"; - -Goal "0 < r ==> 0 <= r*(1r + (-inverse (real_of_posnat n)))"; -by (dtac (real_add_one_minus_inverse_ge_zero RS real_mult_le_less_mono1) 1); -by Auto_tac; -qed "real_mult_add_one_minus_ge_zero"; - Goal "(x*y = 0) = (x = 0 | y = (0::real))"; by Auto_tac; by (blast_tac (claset() addIs [ccontr] addDs [real_mult_not_zero]) 1); qed "real_mult_is_0"; AddIffs [real_mult_is_0]; -Goal "[| 0 <= x * y; 0 < x |] ==> (0::real) <= y"; -by (ftac real_inverse_gt_zero 1); -by (dres_inst_tac [("x","inverse x")] real_less_le_mult_order 1); -by (dtac (real_not_refl2 RS not_sym RS real_mult_inv_left) 2); -by (auto_tac (claset(), - simpset() addsimps [real_mult_assoc RS sym])); -qed "real_mult_ge_zero_cancel"; - -Goal "[|x ~= 0; y ~= 0 |] ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"; +Goal "[| x ~= 0; y ~= 0 |] \ +\ ==> inverse x + inverse y = (x + y) * inverse (x * (y::real))"; by (asm_full_simp_tac (simpset() addsimps [real_inverse_distrib,real_add_mult_distrib, real_mult_assoc RS sym]) 1); @@ -753,90 +640,3 @@ linorder_not_less RS sym])); qed "real_mult_le_zero_iff"; - -(*---------------------------------------------------------------------------- - Another embedding of the naturals in the reals (see real_of_posnat) - ----------------------------------------------------------------------------*) -Goalw [real_of_nat_def] "real_of_nat 0 = 0"; -by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1); -qed "real_of_nat_zero"; - -Goalw [real_of_nat_def] "real_of_nat 1 = 1r"; -by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1); -qed "real_of_nat_one"; -Addsimps [real_of_nat_zero, real_of_nat_one]; - -Goalw [real_of_nat_def] - "real_of_nat (m + n) = real_of_nat m + real_of_nat n"; -by (simp_tac (simpset() addsimps - [real_of_posnat_add,real_add_assoc RS sym]) 1); -qed "real_of_nat_add"; - -Goalw [real_of_nat_def] "real_of_nat (Suc n) = real_of_nat n + 1r"; -by (simp_tac (simpset() addsimps [real_of_posnat_Suc] @ real_add_ac) 1); -qed "real_of_nat_Suc"; -Addsimps [real_of_nat_Suc]; - -Goalw [real_of_nat_def] "(real_of_nat n < real_of_nat m) = (n < m)"; -by Auto_tac; -qed "real_of_nat_less_iff"; - -AddIffs [real_of_nat_less_iff]; - -Goal "inj real_of_nat"; -by (rtac injI 1); -by (auto_tac (claset() addSIs [inj_real_of_posnat RS injD], - simpset() addsimps [real_of_nat_def,real_add_right_cancel])); -qed "inj_real_of_nat"; - -Goalw [real_of_nat_def] "0 <= real_of_nat n"; -by (res_inst_tac [("C","1r")] real_le_add_right_cancel 1); -by (asm_full_simp_tac (simpset() addsimps [real_add_assoc]) 1); -qed "real_of_nat_ge_zero"; -AddIffs [real_of_nat_ge_zero]; - -Goal "real_of_nat (m * n) = real_of_nat m * real_of_nat n"; -by (induct_tac "m" 1); -by (auto_tac (claset(), - simpset() addsimps [real_of_nat_add, - real_add_mult_distrib, real_add_commute])); -qed "real_of_nat_mult"; - -Goal "(real_of_nat n = real_of_nat m) = (n = m)"; -by (auto_tac (claset() addDs [inj_real_of_nat RS injD], - simpset())); -qed "real_of_nat_eq_cancel"; - -Goal "n <= m --> real_of_nat (m - n) = real_of_nat m + (-real_of_nat n)"; -by (induct_tac "m" 1); -by (auto_tac (claset(), - simpset() addsimps [Suc_diff_le, le_Suc_eq, real_of_nat_Suc, - real_of_nat_zero] @ real_add_ac)); -qed_spec_mp "real_of_nat_minus"; - -(* 05/00 *) -Goal "n < m ==> real_of_nat (m - n) = \ -\ real_of_nat m + -real_of_nat n"; -by (auto_tac (claset() addIs [real_of_nat_minus],simpset())); -qed "real_of_nat_minus2"; - -Goalw [real_diff_def] - "n < m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n"; -by (etac real_of_nat_minus2 1); -qed "real_of_nat_diff"; - -Goalw [real_diff_def] - "n <= m ==> real_of_nat (m - n) = real_of_nat m - real_of_nat n"; -by (etac real_of_nat_minus 1); -qed "real_of_nat_diff2"; - -Goal "(real_of_nat n = 0) = (n = 0)"; -by (auto_tac (claset() addIs [inj_real_of_nat RS injD], simpset())); -qed "real_of_nat_zero_iff"; -AddIffs [real_of_nat_zero_iff]; - -Goal "neg z ==> real_of_nat (nat z) = 0"; -by (asm_simp_tac (simpset() addsimps [neg_nat, real_of_nat_zero]) 1); -qed "real_of_nat_neg_int"; -Addsimps [real_of_nat_neg_int]; - diff -r a5a6255748c3 -r 2c6605049646 src/HOL/Real/RealPow.ML --- a/src/HOL/Real/RealPow.ML Thu Jan 04 10:22:33 2001 +0100 +++ b/src/HOL/Real/RealPow.ML Thu Jan 04 10:23:01 2001 +0100 @@ -146,16 +146,15 @@ Goal "(#1::real) <= #2 ^ n"; by (res_inst_tac [("y","#1 ^ n")] order_trans 1); by (rtac realpow_le 2); -by (auto_tac (claset() addIs [order_less_imp_le],simpset())); +by (auto_tac (claset() addIs [order_less_imp_le], simpset())); qed "two_realpow_ge_one"; Goal "real_of_nat n < #2 ^ n"; by (induct_tac "n" 1); -by Auto_tac; +by (auto_tac (claset(), simpset() addsimps [real_of_nat_Suc])); by (stac real_mult_2 1); by (rtac real_add_less_le_mono 1); -by (auto_tac (claset(), - simpset() addsimps [two_realpow_ge_one])); +by (auto_tac (claset(), simpset() addsimps [two_realpow_ge_one])); qed "two_realpow_gt"; Addsimps [two_realpow_gt,two_realpow_ge_one];