# HG changeset patch # User paulson # Date 1071674632 -3600 # Node ID 0b5c0b0a3eba92732ad25499d9cb127198091f92 # Parent e616f4bda3a2f3e40af40e152d78e429dccfc454 converted Hyperreal/HyperDef to Isar script diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Complex/NSCA.ML Wed Dec 17 16:23:52 2003 +0100 @@ -785,12 +785,13 @@ Infinitesimal_FreeUltrafilterNat_iff2])); by (dres_inst_tac [("x","m")] spec 1); by (Ultra_tac 1); +by (rename_tac "Z x" 1); by (res_inst_tac [("z","X x")] eq_Abs_complex 1); by (res_inst_tac [("z","Y x")] eq_Abs_complex 1); by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add, complex_mod] delsimps [realpow_Suc])); by (rtac order_le_less_trans 1 THEN assume_tac 2); -by (dres_inst_tac [("t","Ya x")] sym 1); +by (dres_inst_tac [("t","Z x")] sym 1); by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc])); qed "hcomplex_capproxD1"; @@ -805,12 +806,13 @@ Infinitesimal_FreeUltrafilterNat_iff2])); by (dres_inst_tac [("x","m")] spec 1); by (Ultra_tac 1); +by (rename_tac "Z x" 1); by (res_inst_tac [("z","X x")] eq_Abs_complex 1); by (res_inst_tac [("z","Y x")] eq_Abs_complex 1); by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add, complex_mod] delsimps [realpow_Suc])); by (rtac order_le_less_trans 1 THEN assume_tac 2); -by (dres_inst_tac [("t","Ya x")] sym 1); +by (dres_inst_tac [("t","Z x")] sym 1); by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc])); qed "hcomplex_capproxD2"; @@ -894,13 +896,14 @@ \ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite"; by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff, hcmod,HFinite_FreeUltrafilterNat_iff])); +by (rename_tac "Y Z u v" 1); by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); -by (res_inst_tac [("x","2*(u + ua)")] exI 1); +by (res_inst_tac [("x","2*(u + v)")] exI 1); by (Ultra_tac 1); by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1); by (auto_tac (claset(),simpset() addsimps [complex_mod,two_eq_Suc_Suc] delsimps [realpow_Suc])); by (subgoal_tac "0 < u" 1 THEN arith_tac 2); -by (subgoal_tac "0 < ua" 1 THEN arith_tac 2); +by (subgoal_tac "0 < v" 1 THEN arith_tac 2); by (rtac (realpow_two_abs RS subst) 1); by (res_inst_tac [("x1","Y x")] (realpow_two_abs RS subst) 1); by (simp_tac (simpset() addsimps [two_eq_Suc_Suc RS sym]) 1); diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Complex/NSComplex.ML --- a/src/HOL/Complex/NSComplex.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Complex/NSComplex.ML Wed Dec 17 16:23:52 2003 +0100 @@ -36,9 +36,9 @@ by (Auto_tac); qed "hcomplexrel_refl"; -Goalw [hcomplexrel_def] "(x,y): hcomplexrel --> (y,x):hcomplexrel"; -by (auto_tac (claset() addIs [lemma_perm RS subst],simpset())); -qed_spec_mp "hcomplexrel_sym"; +Goalw [hcomplexrel_def] "(x,y): hcomplexrel ==> (y,x):hcomplexrel"; +by (auto_tac (claset(), simpset() addsimps [eq_commute])); +qed "hcomplexrel_sym"; Goalw [hcomplexrel_def] "(x,y): hcomplexrel --> (y,z):hcomplexrel --> (x,z):hcomplexrel"; @@ -659,7 +659,8 @@ "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) = \ \ Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})"; by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); -by (Auto_tac THEN Ultra_tac 1); +by Auto_tac; +by (Ultra_tac 1); qed "hcomplex_of_hypreal"; Goal "inj hcomplex_of_hypreal"; @@ -711,8 +712,8 @@ Goalw [hcomplex_divide_def] "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)"; -by (hypreal_div_undefined_case_tac "y=0" 1); -by (simp_tac (simpset() addsimps [rename_numerals HYPREAL_DIVISION_BY_ZERO, +by (case_tac "y=0" 1); +by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO,HYPREAL_INVERSE_ZERO, HCOMPLEX_INVERSE_ZERO]) 1); by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal_mult, hcomplex_of_hypreal_inverse RS sym])); @@ -1592,7 +1593,8 @@ "hcis (Abs_hypreal(hyprel `` {%n. X n})) = \ \ Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})"; by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); -by (Auto_tac THEN Ultra_tac 1); +by Auto_tac; +by (Ultra_tac 1); qed "hcis"; Goal diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HLog.ML --- a/src/HOL/Hyperreal/HLog.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/HLog.ML Wed Dec 17 16:23:52 2003 +0100 @@ -122,7 +122,8 @@ "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) = \ \ Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); -by (Auto_tac THEN Ultra_tac 1); +by Auto_tac; +by (Ultra_tac 1); qed "hlog"; Goal "( *f* ln) x = hlog (( *f* exp) 1) x"; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HRealAbs.ML --- a/src/HOL/Hyperreal/HRealAbs.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/HRealAbs.ML Wed Dec 17 16:23:52 2003 +0100 @@ -18,15 +18,6 @@ qed "hrabs_number_of"; Addsimps [hrabs_number_of]; -Goalw [hrabs_def] - "abs (Abs_hypreal (hyprel `` {X})) = \ -\ Abs_hypreal(hyprel `` {%n. abs (X n)})"; -by (auto_tac (claset(), - simpset_of HyperDef.thy - addsimps [hypreal_zero_def, hypreal_le,hypreal_minus])); -by (ALLGOALS(Ultra_tac THEN' arith_tac )); -qed "hypreal_hrabs"; - (*------------------------------------------------------------ Properties of the absolute value function over the reals (adapted version of previously proved theorems about abs) diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HRealAbs.thy --- a/src/HOL/Hyperreal/HRealAbs.thy Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/HRealAbs.thy Wed Dec 17 16:23:52 2003 +0100 @@ -6,9 +6,6 @@ HRealAbs = HyperArith + RealArith + -defs - hrabs_def "abs r == if (0::hypreal) <=r then r else -r" - constdefs hypreal_of_nat :: nat => hypreal diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HyperDef.ML --- a/src/HOL/Hyperreal/HyperDef.ML Tue Dec 16 23:24:17 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1257 +0,0 @@ -(* Title : HOL/Real/Hyperreal/Hyper.ML - ID : $Id$ - Author : Jacques D. Fleuriot - Copyright : 1998 University of Cambridge - Description : Ultrapower construction of hyperreals -*) - -(*------------------------------------------------------------------------ - Proof that the set of naturals is not finite - ------------------------------------------------------------------------*) - -(*** based on James' proof that the set of naturals is not finite ***) -Goal "finite (A::nat set) --> (EX n. ALL m. Suc (n + m) ~: A)"; -by (rtac impI 1); -by (eres_inst_tac [("F","A")] finite_induct 1); -by (Blast_tac 1 THEN etac exE 1); -by (res_inst_tac [("x","n + x")] exI 1); -by (rtac allI 1 THEN eres_inst_tac [("x","x + m")] allE 1); -by (auto_tac (claset(), simpset() addsimps add_ac)); -by (auto_tac (claset(), - simpset() addsimps [add_assoc RS sym, - less_add_Suc2 RS less_not_refl2])); -qed_spec_mp "finite_exhausts"; - -Goal "finite (A :: nat set) --> (EX n. n ~:A)"; -by (rtac impI 1 THEN dtac finite_exhausts 1); -by (Blast_tac 1); -qed_spec_mp "finite_not_covers"; - -Goal "~ finite(UNIV:: nat set)"; -by (fast_tac (claset() addSDs [finite_exhausts]) 1); -qed "not_finite_nat"; - -(*------------------------------------------------------------------------ - Existence of free ultrafilter over the naturals and proof of various - properties of the FreeUltrafilterNat- an arbitrary free ultrafilter - ------------------------------------------------------------------------*) - -Goal "EX U. U: FreeUltrafilter (UNIV::nat set)"; -by (rtac (not_finite_nat RS FreeUltrafilter_Ex) 1); -qed "FreeUltrafilterNat_Ex"; - -Goalw [FreeUltrafilterNat_def] - "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)"; -by (rtac (FreeUltrafilterNat_Ex RS exE) 1); -by (rtac someI2 1 THEN ALLGOALS(assume_tac)); -qed "FreeUltrafilterNat_mem"; -Addsimps [FreeUltrafilterNat_mem]; - -Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat"; -by (rtac (FreeUltrafilterNat_Ex RS exE) 1); -by (rtac someI2 1 THEN assume_tac 1); -by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1); -qed "FreeUltrafilterNat_finite"; - -Goal "x: FreeUltrafilterNat ==> ~ finite x"; -by (blast_tac (claset() addDs [FreeUltrafilterNat_finite]) 1); -qed "FreeUltrafilterNat_not_finite"; - -Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat"; -by (rtac (FreeUltrafilterNat_Ex RS exE) 1); -by (rtac someI2 1 THEN assume_tac 1); -by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter, - Ultrafilter_Filter,Filter_empty_not_mem]) 1); -qed "FreeUltrafilterNat_empty"; -Addsimps [FreeUltrafilterNat_empty]; - -Goal "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] \ -\ ==> X Int Y : FreeUltrafilterNat"; -by (cut_facts_tac [FreeUltrafilterNat_mem] 1); -by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter, - Ultrafilter_Filter,mem_FiltersetD1]) 1); -qed "FreeUltrafilterNat_Int"; - -Goal "[| X: FreeUltrafilterNat; X <= Y |] \ -\ ==> Y : FreeUltrafilterNat"; -by (cut_facts_tac [FreeUltrafilterNat_mem] 1); -by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter, - Ultrafilter_Filter,mem_FiltersetD2]) 1); -qed "FreeUltrafilterNat_subset"; - -Goal "X: FreeUltrafilterNat ==> -X ~: FreeUltrafilterNat"; -by (Step_tac 1); -by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); -by Auto_tac; -qed "FreeUltrafilterNat_Compl"; - -Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat"; -by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1); -by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1); -by (auto_tac (claset(), simpset() addsimps [UNIV_diff_Compl])); -qed "FreeUltrafilterNat_Compl_mem"; - -Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)"; -by (blast_tac (claset() addDs [FreeUltrafilterNat_Compl, - FreeUltrafilterNat_Compl_mem]) 1); -qed "FreeUltrafilterNat_Compl_iff1"; - -Goal "(X: FreeUltrafilterNat) = (-X ~: FreeUltrafilterNat)"; -by (auto_tac (claset(), - simpset() addsimps [FreeUltrafilterNat_Compl_iff1 RS sym])); -qed "FreeUltrafilterNat_Compl_iff2"; - -Goal "(UNIV::nat set) : FreeUltrafilterNat"; -by (rtac (FreeUltrafilterNat_mem RS FreeUltrafilter_Ultrafilter RS - Ultrafilter_Filter RS mem_FiltersetD4) 1); -qed "FreeUltrafilterNat_UNIV"; -Addsimps [FreeUltrafilterNat_UNIV]; - -Goal "UNIV : FreeUltrafilterNat"; -by Auto_tac; -qed "FreeUltrafilterNat_Nat_set"; -Addsimps [FreeUltrafilterNat_Nat_set]; - -Goal "{n. P(n) = P(n)} : FreeUltrafilterNat"; -by (Simp_tac 1); -qed "FreeUltrafilterNat_Nat_set_refl"; -AddIs [FreeUltrafilterNat_Nat_set_refl]; - -Goal "{n::nat. P} : FreeUltrafilterNat ==> P"; -by (rtac ccontr 1); -by (Asm_full_simp_tac 1); -qed "FreeUltrafilterNat_P"; - -Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)"; -by (rtac ccontr 1); -by (Asm_full_simp_tac 1); -qed "FreeUltrafilterNat_Ex_P"; - -Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat"; -by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set], simpset())); -qed "FreeUltrafilterNat_all"; - -(*------------------------------------------------------- - Define and use Ultrafilter tactics - -------------------------------------------------------*) -use "fuf.ML"; - -(*------------------------------------------------------- - Now prove one further property of our free ultrafilter - -------------------------------------------------------*) -Goal "X Un Y: FreeUltrafilterNat \ -\ ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat"; -by Auto_tac; -by (Ultra_tac 1); -qed "FreeUltrafilterNat_Un"; - -(*------------------------------------------------------- - Properties of hyprel - -------------------------------------------------------*) - -(** Proving that hyprel is an equivalence relation **) -(** Natural deduction for hyprel **) - -Goalw [hyprel_def] - "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"; -by (Fast_tac 1); -qed "hyprel_iff"; - -Goalw [hyprel_def] - "{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hyprel"; -by (Fast_tac 1); -qed "hyprelI"; - -Goalw [hyprel_def] - "p: hyprel --> (EX X Y. \ -\ p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)"; -by (Fast_tac 1); -qed "hyprelE_lemma"; - -val [major,minor] = goal (the_context ()) - "[| p: hyprel; \ -\ !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\ -\ |] ==> Q |] ==> Q"; -by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1); -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1)); -qed "hyprelE"; - -AddSIs [hyprelI]; -AddSEs [hyprelE]; - -Goalw [hyprel_def] "(x,x): hyprel"; -by (auto_tac (claset(), - simpset() addsimps [FreeUltrafilterNat_Nat_set])); -qed "hyprel_refl"; - -Goal "{n. X n = Y n} = {n. Y n = X n}"; -by Auto_tac; -qed "lemma_perm"; - -Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel"; -by (auto_tac (claset() addIs [lemma_perm RS subst], simpset())); -qed_spec_mp "hyprel_sym"; - -Goalw [hyprel_def] - "(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel"; -by Auto_tac; -by (Ultra_tac 1); -qed_spec_mp "hyprel_trans"; - -Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV hyprel"; -by (auto_tac (claset() addSIs [hyprel_refl] - addSEs [hyprel_sym,hyprel_trans] - delrules [hyprelI,hyprelE], - simpset() addsimps [FreeUltrafilterNat_Nat_set])); -qed "equiv_hyprel"; - -(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) : hyprel) *) -bind_thm ("equiv_hyprel_iff", - [equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff); - -Goalw [hypreal_def,hyprel_def,quotient_def] "hyprel``{x}:hypreal"; -by (Blast_tac 1); -qed "hyprel_in_hypreal"; - -Goal "inj_on Abs_hypreal hypreal"; -by (rtac inj_on_inverseI 1); -by (etac Abs_hypreal_inverse 1); -qed "inj_on_Abs_hypreal"; - -Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff, - hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse]; - -Addsimps [equiv_hyprel RS eq_equiv_class_iff]; -bind_thm ("eq_hyprelD", equiv_hyprel RSN (2,eq_equiv_class)); - -Goal "inj(Rep_hypreal)"; -by (rtac inj_inverseI 1); -by (rtac Rep_hypreal_inverse 1); -qed "inj_Rep_hypreal"; - -Goalw [hyprel_def] "x: hyprel `` {x}"; -by (Step_tac 1); -by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset())); -qed "lemma_hyprel_refl"; - -Addsimps [lemma_hyprel_refl]; - -Goalw [hypreal_def] "{} ~: hypreal"; -by (auto_tac (claset() addSEs [quotientE], simpset())); -qed "hypreal_empty_not_mem"; - -Addsimps [hypreal_empty_not_mem]; - -Goal "Rep_hypreal x ~= {}"; -by (cut_inst_tac [("x","x")] Rep_hypreal 1); -by Auto_tac; -qed "Rep_hypreal_nonempty"; - -Addsimps [Rep_hypreal_nonempty]; - -(*------------------------------------------------------------------------ - hypreal_of_real: the injection from real to hypreal - ------------------------------------------------------------------------*) - -Goal "inj(hypreal_of_real)"; -by (rtac injI 1); -by (rewtac hypreal_of_real_def); -by (dtac (inj_on_Abs_hypreal RS inj_onD) 1); -by (REPEAT (rtac hyprel_in_hypreal 1)); -by (dtac eq_equiv_class 1); -by (rtac equiv_hyprel 1); -by (Fast_tac 1); -by (rtac ccontr 1); -by Auto_tac; -qed "inj_hypreal_of_real"; - -val [prem] = goal (the_context ()) - "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"; -by (res_inst_tac [("x1","z")] - (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1); -by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1); -by (res_inst_tac [("x","x")] prem 1); -by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1); -qed "eq_Abs_hypreal"; - -(**** hypreal_minus: additive inverse on hypreal ****) - -Goalw [congruent_def] - "congruent hyprel (%X. hyprel``{%n. - (X n)})"; -by Safe_tac; -by (ALLGOALS Ultra_tac); -qed "hypreal_minus_congruent"; - -Goalw [hypreal_minus_def] - "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"; -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); -by (simp_tac (simpset() addsimps - [hyprel_in_hypreal RS Abs_hypreal_inverse, - [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1); -qed "hypreal_minus"; - -Goal "- (- z) = (z::hypreal)"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1); -qed "hypreal_minus_minus"; - -Addsimps [hypreal_minus_minus]; - -Goal "inj(%r::hypreal. -r)"; -by (rtac injI 1); -by (dres_inst_tac [("f","uminus")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1); -qed "inj_hypreal_minus"; - -Goalw [hypreal_zero_def] "- 0 = (0::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_minus]) 1); -qed "hypreal_minus_zero"; -Addsimps [hypreal_minus_zero]; - -Goal "(-x = 0) = (x = (0::hypreal))"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_zero_def, hypreal_minus])); -qed "hypreal_minus_zero_iff"; -Addsimps [hypreal_minus_zero_iff]; - - -(**** hyperreal addition: hypreal_add ****) - -Goalw [congruent2_def] - "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})"; -by Safe_tac; -by (ALLGOALS(Ultra_tac)); -qed "hypreal_add_congruent2"; - -Goalw [hypreal_add_def] - "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = \ -\ Abs_hypreal(hyprel``{%n. X n + Y n})"; -by (simp_tac (simpset() addsimps - [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1); -qed "hypreal_add"; - -Goal "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = \ -\ Abs_hypreal(hyprel``{%n. X n - Y n})"; -by (simp_tac (simpset() addsimps - [hypreal_diff_def, hypreal_minus,hypreal_add]) 1); -qed "hypreal_diff"; - -Goal "(z::hypreal) + w = w + z"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); -by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1); -qed "hypreal_add_commute"; - -Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"; -by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); -by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1); -qed "hypreal_add_assoc"; - -(*For AC rewriting*) -Goal "(x::hypreal)+(y+z)=y+(x+z)"; -by(rtac ([hypreal_add_assoc,hypreal_add_commute] MRS - read_instantiate[("f","op +")](thm"mk_left_commute")) 1); -qed "hypreal_add_left_commute"; - -(* hypreal addition is an AC operator *) -bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute, - hypreal_add_left_commute]); - -Goalw [hypreal_zero_def] "(0::hypreal) + z = z"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (asm_full_simp_tac (simpset() addsimps - [hypreal_add]) 1); -qed "hypreal_add_zero_left"; - -Goal "z + (0::hypreal) = z"; -by (simp_tac (simpset() addsimps - [hypreal_add_zero_left,hypreal_add_commute]) 1); -qed "hypreal_add_zero_right"; - -Goalw [hypreal_zero_def] "z + -z = (0::hypreal)"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, hypreal_add]) 1); -qed "hypreal_add_minus"; - -Goal "-z + z = (0::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_add_commute, hypreal_add_minus]) 1); -qed "hypreal_add_minus_left"; - -Addsimps [hypreal_add_minus,hypreal_add_minus_left, - hypreal_add_zero_left,hypreal_add_zero_right]; - -Goal "EX y. (x::hypreal) + y = 0"; -by (fast_tac (claset() addIs [hypreal_add_minus]) 1); -qed "hypreal_minus_ex"; - -Goal "EX! y. (x::hypreal) + y = 0"; -by (auto_tac (claset() addIs [hypreal_add_minus], simpset())); -by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); -qed "hypreal_minus_ex1"; - -Goal "EX! y. y + (x::hypreal) = 0"; -by (auto_tac (claset() addIs [hypreal_add_minus_left], simpset())); -by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); -qed "hypreal_minus_left_ex1"; - -Goal "x + y = (0::hypreal) ==> x = -y"; -by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1); -by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1); -by (Blast_tac 1); -qed "hypreal_add_minus_eq_minus"; - -Goal "EX y::hypreal. x = -y"; -by (cut_inst_tac [("x","x")] hypreal_minus_ex 1); -by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1); -by (Fast_tac 1); -qed "hypreal_as_add_inverse_ex"; - -Goal "-(x + (y::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_minus, hypreal_add, - real_minus_add_distrib])); -qed "hypreal_minus_add_distrib"; -Addsimps [hypreal_minus_add_distrib]; - -Goal "-(y + -(x::hypreal)) = x + -y"; -by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1); -qed "hypreal_minus_distrib1"; - -Goal "((x::hypreal) + y = x + z) = (y = z)"; -by (Step_tac 1); -by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); -qed "hypreal_add_left_cancel"; - -Goal "(y + (x::hypreal)= z + x) = (y = z)"; -by (simp_tac (simpset() addsimps [hypreal_add_commute, - hypreal_add_left_cancel]) 1); -qed "hypreal_add_right_cancel"; - -Goal "z + ((- z) + w) = (w::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); -qed "hypreal_add_minus_cancelA"; - -Goal "(-z) + (z + w) = (w::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); -qed "hypreal_minus_add_cancelA"; - -Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA]; - -(**** hyperreal multiplication: hypreal_mult ****) - -Goalw [congruent2_def] - "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})"; -by Safe_tac; -by (ALLGOALS(Ultra_tac)); -qed "hypreal_mult_congruent2"; - -Goalw [hypreal_mult_def] - "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) = \ -\ Abs_hypreal(hyprel``{%n. X n * Y n})"; -by (simp_tac (simpset() addsimps - [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1); -qed "hypreal_mult"; - -Goal "(z::hypreal) * w = w * z"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); -by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1); -qed "hypreal_mult_commute"; - -Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"; -by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1); -by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1); -qed "hypreal_mult_assoc"; - -Goal "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"; -by(rtac ([hypreal_mult_assoc,hypreal_mult_commute] MRS - read_instantiate[("f","op *")](thm"mk_left_commute")) 1); -qed "hypreal_mult_left_commute"; - -(* hypreal multiplication is an AC operator *) -bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, - hypreal_mult_left_commute]); - -Goalw [hypreal_one_def] "(1::hypreal) * z = z"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1); -qed "hypreal_mult_1"; -Addsimps [hypreal_mult_1]; - -Goal "z * (1::hypreal) = z"; -by (simp_tac (simpset() addsimps [hypreal_mult_commute, - hypreal_mult_1]) 1); -qed "hypreal_mult_1_right"; -Addsimps [hypreal_mult_1_right]; - -Goalw [hypreal_zero_def] "0 * z = (0::hypreal)"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1); -qed "hypreal_mult_0"; -Addsimps [hypreal_mult_0]; - -Goal "z * 0 = (0::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_mult_commute]) 1); -qed "hypreal_mult_0_right"; -Addsimps [hypreal_mult_0_right]; - -Goal "-(x * y) = -x * (y::hypreal)"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_minus, hypreal_mult] - @ real_mult_ac @ real_add_ac)); -qed "hypreal_minus_mult_eq1"; - -Goal "-(x * y) = (x::hypreal) * -y"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_mult] - @ real_mult_ac @ real_add_ac)); -qed "hypreal_minus_mult_eq2"; - -(*Pull negations out*) -Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym]; - -Goal "(- (1::hypreal)) * z = -z"; -by (Simp_tac 1); -qed "hypreal_mult_minus_1"; -Addsimps [hypreal_mult_minus_1]; - -Goal "z * (- (1::hypreal)) = -z"; -by (stac hypreal_mult_commute 1); -by (Simp_tac 1); -qed "hypreal_mult_minus_1_right"; -Addsimps [hypreal_mult_minus_1_right]; - -Goal "(-x) * y = (x::hypreal) * -y"; -by Auto_tac; -qed "hypreal_minus_mult_commute"; - -(*----------------------------------------------------------------------------- - A few more theorems - ----------------------------------------------------------------------------*) -Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"; -by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); -qed "hypreal_add_assoc_cong"; - -Goal "(z::hypreal) + (v + w) = v + (z + w)"; -by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1)); -qed "hypreal_add_assoc_swap"; - -Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"; -by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","w")] eq_Abs_hypreal 1); -by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add, - real_add_mult_distrib]) 1); -qed "hypreal_add_mult_distrib"; - -val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute; - -Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)"; -by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1); -qed "hypreal_add_mult_distrib2"; - - -Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)"; -by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1); -qed "hypreal_diff_mult_distrib"; - -Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)"; -by (simp_tac (simpset() addsimps [hypreal_mult_commute', - hypreal_diff_mult_distrib]) 1); -qed "hypreal_diff_mult_distrib2"; - -(*** one and zero are distinct ***) -Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= (1::hypreal)"; -by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one])); -qed "hypreal_zero_not_eq_one"; - - -(**** multiplicative inverse on hypreal ****) - -Goalw [congruent_def] - "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"; -by (Auto_tac THEN Ultra_tac 1); -qed "hypreal_inverse_congruent"; - -Goalw [hypreal_inverse_def] - "inverse (Abs_hypreal(hyprel``{%n. X n})) = \ -\ Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"; -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); -by (simp_tac (simpset() addsimps - [hyprel_in_hypreal RS Abs_hypreal_inverse, - [equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1); -qed "hypreal_inverse"; - -Goal "inverse 0 = (0::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_inverse, hypreal_zero_def]) 1); -qed "HYPREAL_INVERSE_ZERO"; - -Goal "a / (0::hypreal) = 0"; -by (simp_tac - (simpset() addsimps [hypreal_divide_def, HYPREAL_INVERSE_ZERO]) 1); -qed "HYPREAL_DIVISION_BY_ZERO"; (*NOT for adding to default simpset*) - -fun hypreal_div_undefined_case_tac s i = - case_tac s i THEN - asm_simp_tac - (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO, HYPREAL_INVERSE_ZERO]) i; - -Goal "inverse (inverse (z::hypreal)) = z"; -by (hypreal_div_undefined_case_tac "z=0" 1); -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (asm_full_simp_tac (simpset() addsimps - [hypreal_inverse, hypreal_zero_def]) 1); -qed "hypreal_inverse_inverse"; -Addsimps [hypreal_inverse_inverse]; - -Goalw [hypreal_one_def] "inverse((1::hypreal)) = (1::hypreal)"; -by (full_simp_tac (simpset() addsimps [hypreal_inverse, - real_zero_not_eq_one RS not_sym]) 1); -qed "hypreal_inverse_1"; -Addsimps [hypreal_inverse_1]; - - -(*** existence of inverse ***) - -Goalw [hypreal_one_def,hypreal_zero_def] - "x ~= 0 ==> x*inverse(x) = (1::hypreal)"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1); -by (dtac FreeUltrafilterNat_Compl_mem 1); -by (blast_tac (claset() addSIs [real_mult_inv_right, - FreeUltrafilterNat_subset]) 1); -qed "hypreal_mult_inverse"; - -Goal "x ~= 0 ==> inverse(x)*x = (1::hypreal)"; -by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse, - hypreal_mult_commute]) 1); -qed "hypreal_mult_inverse_left"; - -Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)"; -by Auto_tac; -by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1); -qed "hypreal_mult_left_cancel"; - -Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)"; -by (Step_tac 1); -by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac) 1); -qed "hypreal_mult_right_cancel"; - -Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1); -qed "hypreal_inverse_not_zero"; - -Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left]; - -Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)"; -by (Step_tac 1); -by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); -qed "hypreal_mult_not_0"; - -Goal "x*y = (0::hypreal) ==> x = 0 | y = 0"; -by (auto_tac (claset() addIs [ccontr] addDs [hypreal_mult_not_0], - simpset())); -qed "hypreal_mult_zero_disj"; - -Goal "inverse(-x) = -inverse(x::hypreal)"; -by (hypreal_div_undefined_case_tac "x=0" 1); -by (rtac (hypreal_mult_right_cancel RS iffD1) 1); -by (stac hypreal_mult_inverse_left 2); -by Auto_tac; -qed "hypreal_minus_inverse"; - -Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)"; -by (hypreal_div_undefined_case_tac "x=0" 1); -by (hypreal_div_undefined_case_tac "y=0" 1); -by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1); -by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_mult_assoc RS sym])); -by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_commute])); -by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1); -qed "hypreal_inverse_distrib"; - -(*------------------------------------------------------------------ - Theorems for ordering - ------------------------------------------------------------------*) - -(* prove introduction and elimination rules for hypreal_less *) - -Goalw [hypreal_less_def] - "(P < (Q::hypreal)) = (EX X Y. X : Rep_hypreal(P) & \ -\ Y : Rep_hypreal(Q) & \ -\ {n. X n < Y n} : FreeUltrafilterNat)"; -by (Fast_tac 1); -qed "hypreal_less_iff"; - -Goalw [hypreal_less_def] - "[| {n. X n < Y n} : FreeUltrafilterNat; \ -\ X : Rep_hypreal(P); \ -\ Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)"; -by (Fast_tac 1); -qed "hypreal_lessI"; - - -Goalw [hypreal_less_def] - "!! R1. [| R1 < (R2::hypreal); \ -\ !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \ -\ !!X. X : Rep_hypreal(R1) ==> P; \ -\ !!Y. Y : Rep_hypreal(R2) ==> P |] \ -\ ==> P"; -by Auto_tac; -qed "hypreal_lessE"; - -Goalw [hypreal_less_def] - "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \ -\ X : Rep_hypreal(R1) & \ -\ Y : Rep_hypreal(R2))"; -by (Fast_tac 1); -qed "hypreal_lessD"; - -Goal "~ (R::hypreal) < R"; -by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_less_def])); -by (Ultra_tac 1); -qed "hypreal_less_not_refl"; - -(*** y < y ==> P ***) -bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE); -AddSEs [hypreal_less_irrefl]; - -Goal "!!(x::hypreal). x < y ==> x ~= y"; -by (auto_tac (claset(), simpset() addsimps [hypreal_less_not_refl])); -qed "hypreal_not_refl2"; - -Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3"; -by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1); -by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1); -by (auto_tac (claset() addSIs [exI], simpset() addsimps [hypreal_less_def])); -by (ultra_tac (claset() addIs [order_less_trans], simpset()) 1); -qed "hypreal_less_trans"; - -Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P"; -by (dtac hypreal_less_trans 1 THEN assume_tac 1); -by (asm_full_simp_tac (simpset() addsimps - [hypreal_less_not_refl]) 1); -qed "hypreal_less_asym"; - -(*------------------------------------------------------- - TODO: The following theorem should have been proved - first and then used througout the proofs as it probably - makes many of them more straightforward. - -------------------------------------------------------*) -Goalw [hypreal_less_def] - "(Abs_hypreal(hyprel``{%n. X n}) < \ -\ Abs_hypreal(hyprel``{%n. Y n})) = \ -\ ({n. X n < Y n} : FreeUltrafilterNat)"; -by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset())); -by (Ultra_tac 1); -qed "hypreal_less"; - -(*---------------------------------------------------------------------------- - Trichotomy: the hyperreals are linearly ordered - ---------------------------------------------------------------------------*) - -Goalw [hyprel_def] "EX x. x: hyprel `` {%n. 0}"; -by (res_inst_tac [("x","%n. 0")] exI 1); -by (Step_tac 1); -by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset())); -qed "lemma_hyprel_0_mem"; - -Goalw [hypreal_zero_def]"0 < x | x = 0 | x < (0::hypreal)"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(),simpset() addsimps [hypreal_less_def])); -by (cut_facts_tac [lemma_hyprel_0_mem] 1 THEN etac exE 1); -by (dres_inst_tac [("x","xa")] spec 1); -by (dres_inst_tac [("x","x")] spec 1); -by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1); -by Auto_tac; -by (dres_inst_tac [("x","x")] spec 1); -by (dres_inst_tac [("x","xa")] spec 1); -by Auto_tac; -by (Ultra_tac 1); -by (auto_tac (claset() addIs [real_linear_less2],simpset())); -qed "hypreal_trichotomy"; - -val prems = Goal "[| (0::hypreal) < x ==> P; \ -\ x = 0 ==> P; \ -\ x < 0 ==> P |] ==> P"; -by (cut_inst_tac [("x","x")] hypreal_trichotomy 1); -by (REPEAT (eresolve_tac (disjE::prems) 1)); -qed "hypreal_trichotomyE"; - -(*---------------------------------------------------------------------------- - More properties of < - ----------------------------------------------------------------------------*) - -Goal "((x::hypreal) < y) = (0 < y + -x)"; -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, - hypreal_zero_def,hypreal_minus,hypreal_less])); -by (ALLGOALS(Ultra_tac)); -qed "hypreal_less_minus_iff"; - -Goal "((x::hypreal) < y) = (x + -y < 0)"; -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, - hypreal_zero_def,hypreal_minus,hypreal_less])); -by (ALLGOALS(Ultra_tac)); -qed "hypreal_less_minus_iff2"; - -Goal "((x::hypreal) = y) = (x + - y = 0)"; -by Auto_tac; -by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1); -by Auto_tac; -qed "hypreal_eq_minus_iff"; - -Goal "((x::hypreal) = y) = (0 = y + - x)"; -by Auto_tac; -by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1); -by Auto_tac; -qed "hypreal_eq_minus_iff2"; - -(* 07/00 *) -Goal "(0::hypreal) - x = -x"; -by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); -qed "hypreal_diff_zero"; - -Goal "x - (0::hypreal) = x"; -by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); -qed "hypreal_diff_zero_right"; - -Goal "x - x = (0::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1); -qed "hypreal_diff_self"; - -Addsimps [hypreal_diff_zero, hypreal_diff_zero_right, hypreal_diff_self]; - -Goal "(x = y + z) = (x + -z = (y::hypreal))"; -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc])); -qed "hypreal_eq_minus_iff3"; - -Goal "(x ~= a) = (x + -a ~= (0::hypreal))"; -by (auto_tac (claset() addDs [hypreal_eq_minus_iff RS iffD2], - simpset())); -qed "hypreal_not_eq_minus_iff"; - - -(*** linearity ***) - -Goal "(x::hypreal) < y | x = y | y < x"; -by (stac hypreal_eq_minus_iff2 1); -by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1); -by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1); -by (rtac hypreal_trichotomyE 1); -by Auto_tac; -qed "hypreal_linear"; - -Goal "((w::hypreal) ~= z) = (w P; x = y ==> P; \ -\ y < x ==> P |] ==> P"; -by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1); -by Auto_tac; -qed "hypreal_linear_less2"; - -(*------------------------------------------------------------------------------ - Properties of <= - ------------------------------------------------------------------------------*) -(*------ hypreal le iff reals le a.e ------*) - -Goalw [hypreal_le_def,real_le_def] - "(Abs_hypreal(hyprel``{%n. X n}) <= \ -\ Abs_hypreal(hyprel``{%n. Y n})) = \ -\ ({n. X n <= Y n} : FreeUltrafilterNat)"; -by (auto_tac (claset(),simpset() addsimps [hypreal_less])); -by (ALLGOALS(Ultra_tac)); -qed "hypreal_le"; - -(*---------------------------------------------------------*) -(*---------------------------------------------------------*) -Goalw [hypreal_le_def] - "~(w < z) ==> z <= (w::hypreal)"; -by (assume_tac 1); -qed "hypreal_leI"; - -Goalw [hypreal_le_def] - "z<=w ==> ~(w<(z::hypreal))"; -by (assume_tac 1); -qed "hypreal_leD"; - -bind_thm ("hypreal_leE", make_elim hypreal_leD); - -Goal "(~(w < z)) = (z <= (w::hypreal))"; -by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1); -qed "hypreal_less_le_iff"; - -Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)"; -by (Fast_tac 1); -qed "not_hypreal_leE"; - -Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y"; -by (cut_facts_tac [hypreal_linear] 1); -by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); -qed "hypreal_le_imp_less_or_eq"; - -Goalw [hypreal_le_def] "z z <=(w::hypreal)"; -by (cut_facts_tac [hypreal_linear] 1); -by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1); -qed "hypreal_less_or_eq_imp_le"; - -Goal "(x <= (y::hypreal)) = (x < y | x=y)"; -by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1)); -qed "hypreal_le_eq_less_or_eq"; -val hypreal_le_less = hypreal_le_eq_less_or_eq; - -Goal "w <= (w::hypreal)"; -by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1); -qed "hypreal_le_refl"; - -(* Axiom 'linorder_linear' of class 'linorder': *) -Goal "(z::hypreal) <= w | w <= z"; -by (simp_tac (simpset() addsimps [hypreal_le_less]) 1); -by (cut_facts_tac [hypreal_linear] 1); -by (Blast_tac 1); -qed "hypreal_le_linear"; - -Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)"; -by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, - rtac hypreal_less_or_eq_imp_le, - fast_tac (claset() addIs [hypreal_less_trans])]); -qed "hypreal_le_trans"; - -Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)"; -by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq, - fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]); -qed "hypreal_le_anti_sym"; - -Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)"; -by (rtac not_hypreal_leE 1); -by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1); -qed "not_less_not_eq_hypreal_less"; - -(* Axiom 'order_less_le' of class 'order': *) -Goal "((w::hypreal) < z) = (w <= z & w ~= z)"; -by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1); -by (blast_tac (claset() addIs [hypreal_less_asym]) 1); -qed "hypreal_less_le"; - -Goal "(0 < -R) = (R < (0::hypreal))"; -by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus])); -qed "hypreal_minus_zero_less_iff"; -Addsimps [hypreal_minus_zero_less_iff]; - -Goal "(-R < 0) = ((0::hypreal) < R)"; -by (res_inst_tac [("z","R")] eq_Abs_hypreal 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus])); -by (ALLGOALS(Ultra_tac)); -qed "hypreal_minus_zero_less_iff2"; -Addsimps [hypreal_minus_zero_less_iff2]; - -Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= 0)"; -by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1); -qed "hypreal_minus_zero_le_iff"; -Addsimps [hypreal_minus_zero_le_iff]; - -Goalw [hypreal_le_def] "(-r <= (0::hypreal)) = (0 <= r)"; -by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1); -qed "hypreal_minus_zero_le_iff2"; -Addsimps [hypreal_minus_zero_le_iff2]; - -(*---------------------------------------------------------- - hypreal_of_real preserves field and order properties - -----------------------------------------------------------*) -Goalw [hypreal_of_real_def] - "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2"; -by (simp_tac (simpset() addsimps [hypreal_add, hypreal_add_mult_distrib]) 1); -qed "hypreal_of_real_add"; -Addsimps [hypreal_of_real_add]; - -Goalw [hypreal_of_real_def] - "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2"; -by (simp_tac (simpset() addsimps [hypreal_mult, hypreal_add_mult_distrib2]) 1); -qed "hypreal_of_real_mult"; -Addsimps [hypreal_of_real_mult]; - -Goalw [hypreal_less_def,hypreal_of_real_def] - "(hypreal_of_real z1 < hypreal_of_real z2) = (z1 < z2)"; -by Auto_tac; -by (res_inst_tac [("x","%n. z1")] exI 2); -by (Step_tac 1); -by (res_inst_tac [("x","%n. z2")] exI 3); -by Auto_tac; -by (rtac FreeUltrafilterNat_P 1); -by (Ultra_tac 1); -qed "hypreal_of_real_less_iff"; -Addsimps [hypreal_of_real_less_iff]; - -Goalw [hypreal_le_def,real_le_def] - "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)"; -by Auto_tac; -qed "hypreal_of_real_le_iff"; -Addsimps [hypreal_of_real_le_iff]; - -Goal "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)"; -by (force_tac (claset() addIs [order_antisym, hypreal_of_real_le_iff RS iffD1], - simpset()) 1); -qed "hypreal_of_real_eq_iff"; -Addsimps [hypreal_of_real_eq_iff]; - -Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real r"; -by (auto_tac (claset(),simpset() addsimps [hypreal_minus])); -qed "hypreal_of_real_minus"; -Addsimps [hypreal_of_real_minus]; - -Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real 1 = (1::hypreal)"; -by (Simp_tac 1); -qed "hypreal_of_real_one"; -Addsimps [hypreal_of_real_one]; - -Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real 0 = 0"; -by (Simp_tac 1); -qed "hypreal_of_real_zero"; -Addsimps [hypreal_of_real_zero]; - -Goal "(hypreal_of_real r = 0) = (r = 0)"; -by (auto_tac (claset() addIs [FreeUltrafilterNat_P], - simpset() addsimps [hypreal_of_real_def, - hypreal_zero_def,FreeUltrafilterNat_Nat_set])); -qed "hypreal_of_real_zero_iff"; - -Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"; -by (case_tac "r=0" 1); -by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO, INVERSE_ZERO, - HYPREAL_INVERSE_ZERO]) 1); -by (res_inst_tac [("c1","hypreal_of_real r")] - (hypreal_mult_left_cancel RS iffD1) 1); -by (stac (hypreal_of_real_mult RS sym) 2); -by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero_iff])); -qed "hypreal_of_real_inverse"; -Addsimps [hypreal_of_real_inverse]; - -Goal "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def]) 1); -qed "hypreal_of_real_divide"; -Addsimps [hypreal_of_real_divide]; - - -(*** Division lemmas ***) - -Goal "(0::hypreal)/x = 0"; -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); -qed "hypreal_zero_divide"; - -Goal "x/(1::hypreal) = x"; -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); -qed "hypreal_divide_one"; -Addsimps [hypreal_zero_divide, hypreal_divide_one]; - -Goal "(x::hypreal) * (y/z) = (x*y)/z"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1); -qed "hypreal_times_divide1_eq"; - -Goal "(y/z) * (x::hypreal) = (y*x)/z"; -by (simp_tac (simpset() addsimps [hypreal_divide_def]@hypreal_mult_ac) 1); -qed "hypreal_times_divide2_eq"; - -Addsimps [hypreal_times_divide1_eq, hypreal_times_divide2_eq]; - -Goal "(x::hypreal) / (y/z) = (x*z)/y"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]@ - hypreal_mult_ac) 1); -qed "hypreal_divide_divide1_eq"; - -Goal "((x::hypreal) / y) / z = x/(y*z)"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib, - hypreal_mult_assoc]) 1); -qed "hypreal_divide_divide2_eq"; - -Addsimps [hypreal_divide_divide1_eq, hypreal_divide_divide2_eq]; - -(** As with multiplication, pull minus signs OUT of the / operator **) - -Goal "(-x) / (y::hypreal) = - (x/y)"; -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); -qed "hypreal_minus_divide_eq"; -Addsimps [hypreal_minus_divide_eq]; - -Goal "(x / -(y::hypreal)) = - (x/y)"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1); -qed "hypreal_divide_minus_eq"; -Addsimps [hypreal_divide_minus_eq]; - -Goal "(x+y)/(z::hypreal) = x/z + y/z"; -by (simp_tac (simpset() addsimps [hypreal_divide_def, - hypreal_add_mult_distrib]) 1); -qed "hypreal_add_divide_distrib"; - -Goal "[|(x::hypreal) ~= 0; y ~= 0 |] \ -\ ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)"; -by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_distrib, - hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1); -by (stac hypreal_mult_assoc 1); -by (rtac (hypreal_mult_left_commute RS subst) 1); -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1); -qed "hypreal_inverse_add"; - -Goal "x = -x ==> x = (0::hypreal)"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_zero_def])); -by (Ultra_tac 1); -qed "hypreal_self_eq_minus_self_zero"; - -Goal "(x + x = 0) = (x = (0::hypreal))"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [hypreal_add, hypreal_zero_def])); -qed "hypreal_add_self_zero_cancel"; -Addsimps [hypreal_add_self_zero_cancel]; - -Goal "(x + x + y = y) = (x = (0::hypreal))"; -by Auto_tac; -by (dtac (hypreal_eq_minus_iff RS iffD1) 1); -by (auto_tac (claset(), - simpset() addsimps [hypreal_add_assoc, hypreal_self_eq_minus_self_zero])); -qed "hypreal_add_self_zero_cancel2"; -Addsimps [hypreal_add_self_zero_cancel2]; - -Goal "(x + (x + y) = y) = (x = (0::hypreal))"; -by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1); -qed "hypreal_add_self_zero_cancel2a"; -Addsimps [hypreal_add_self_zero_cancel2a]; - -Goal "(b = -a) = (-b = (a::hypreal))"; -by Auto_tac; -qed "hypreal_minus_eq_swap"; - -Goal "(-b = -a) = (b = (a::hypreal))"; -by (asm_full_simp_tac (simpset() addsimps - [hypreal_minus_eq_swap]) 1); -qed "hypreal_minus_eq_cancel"; -Addsimps [hypreal_minus_eq_cancel]; - -Goalw [hypreal_diff_def] "(x (x (y<=x) = (y'<=x')"; -by (dtac hypreal_less_eqI 1); -by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1); -qed "hypreal_le_eqI"; - -Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')"; -by Safe_tac; -by (ALLGOALS - (asm_full_simp_tac - (simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq]))); -qed "hypreal_eq_eqI"; - - -(*MOVE UP*) -Goal "0 = Abs_hypreal (hyprel `` {%n. 0})"; -by (simp_tac (simpset() addsimps [hypreal_zero_def RS meta_eq_to_obj_eq RS sym]) 1); -qed "hypreal_zero_num"; - -Goal "1 = Abs_hypreal (hyprel `` {%n. 1})"; -by (simp_tac (simpset() addsimps [hypreal_one_def RS meta_eq_to_obj_eq RS sym]) 1); -qed "hypreal_one_num"; - - -(*MOVE UP*) - -Goalw [omega_def] "0 < omega"; -by (auto_tac (claset(),simpset() addsimps [hypreal_less,hypreal_zero_num])); -qed "hypreal_omega_gt_zero"; -Addsimps [hypreal_omega_gt_zero]; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HyperDef.thy --- a/src/HOL/Hyperreal/HyperDef.thy Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/HyperDef.thy Wed Dec 17 16:23:52 2003 +0100 @@ -5,52 +5,55 @@ Description : Construction of hyperreals using ultrafilters *) -HyperDef = Filter + Real + - -consts - - FreeUltrafilterNat :: nat set set ("\\") - -defs - - FreeUltrafilterNat_def - "FreeUltrafilterNat == (@U. U : FreeUltrafilter (UNIV:: nat set))" +theory HyperDef = Filter + Real +files ("fuf.ML"): (*Warning: file fuf.ML refers to the name Hyperdef!*) constdefs - hyprel :: "((nat=>real)*(nat=>real)) set" - "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & + + FreeUltrafilterNat :: "nat set set" ("\\") + "FreeUltrafilterNat == (SOME U. U \ FreeUltrafilter (UNIV:: nat set))" + + hyprel :: "((nat=>real)*(nat=>real)) set" + "hyprel == {p. \X Y. p = ((X::nat=>real),Y) & {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}" -typedef hypreal = "UNIV//hyprel" (quotient_def) +typedef hypreal = "UNIV//hyprel" + by (auto simp add: quotient_def) -instance - hypreal :: {ord, zero, one, plus, times, minus, inverse} +instance hypreal :: ord .. +instance hypreal :: zero .. +instance hypreal :: one .. +instance hypreal :: plus .. +instance hypreal :: times .. +instance hypreal :: minus .. +instance hypreal :: inverse .. -defs - hypreal_zero_def +defs (overloaded) + + hypreal_zero_def: "0 == Abs_hypreal(hyprel``{%n::nat. (0::real)})" - hypreal_one_def + hypreal_one_def: "1 == Abs_hypreal(hyprel``{%n::nat. (1::real)})" - hypreal_minus_def - "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" + hypreal_minus_def: + "- P == Abs_hypreal(\X \ Rep_hypreal(P). hyprel``{%n::nat. - (X n)})" - hypreal_diff_def + hypreal_diff_def: "x - y == x + -(y::hypreal)" - hypreal_inverse_def - "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). + hypreal_inverse_def: + "inverse P == Abs_hypreal(\X \ Rep_hypreal(P). hyprel``{%n. if X n = 0 then 0 else inverse (X n)})" - hypreal_divide_def + hypreal_divide_def: "P / Q::hypreal == P * inverse Q" constdefs - hypreal_of_real :: real => hypreal + hypreal_of_real :: "real => hypreal" "hypreal_of_real r == Abs_hypreal(hyprel``{%n::nat. r})" omega :: hypreal (*an infinite number = [<1,2,3,...>] *) @@ -60,25 +63,1442 @@ "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})" syntax (xsymbols) - omega :: hypreal ("\\") - epsilon :: hypreal ("\\") + omega :: hypreal ("\") + epsilon :: hypreal ("\") defs - hypreal_add_def - "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). + hypreal_add_def: + "P + Q == Abs_hypreal(\X \ Rep_hypreal(P). \Y \ Rep_hypreal(Q). hyprel``{%n::nat. X n + Y n})" - hypreal_mult_def - "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q). + hypreal_mult_def: + "P * Q == Abs_hypreal(\X \ Rep_hypreal(P). \Y \ Rep_hypreal(Q). hyprel``{%n::nat. X n * Y n})" - hypreal_less_def - "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & - Y: Rep_hypreal(Q) & - {n::nat. X n < Y n} : FreeUltrafilterNat" - hypreal_le_def + hypreal_less_def: + "P < (Q::hypreal) == \X Y. X \ Rep_hypreal(P) & + Y \ Rep_hypreal(Q) & + {n::nat. X n < Y n} \ FreeUltrafilterNat" + hypreal_le_def: "P <= (Q::hypreal) == ~(Q < P)" +(*------------------------------------------------------------------------ + Proof that the set of naturals is not finite + ------------------------------------------------------------------------*) + +(*** based on James' proof that the set of naturals is not finite ***) +lemma finite_exhausts [rule_format (no_asm)]: "finite (A::nat set) --> (\n. \m. Suc (n + m) \ A)" +apply (rule impI) +apply (erule_tac F = "A" in finite_induct) +apply (blast , erule exE) +apply (rule_tac x = "n + x" in exI) +apply (rule allI , erule_tac x = "x + m" in allE) +apply (auto simp add: add_ac) +done + +lemma finite_not_covers [rule_format (no_asm)]: "finite (A :: nat set) --> (\n. n \A)" +apply (rule impI , drule finite_exhausts) +apply blast +done + +lemma not_finite_nat: "~ finite(UNIV:: nat set)" +apply (fast dest!: finite_exhausts) +done + +(*------------------------------------------------------------------------ + Existence of free ultrafilter over the naturals and proof of various + properties of the FreeUltrafilterNat- an arbitrary free ultrafilter + ------------------------------------------------------------------------*) + +lemma FreeUltrafilterNat_Ex: "\U. U: FreeUltrafilter (UNIV::nat set)" +apply (rule not_finite_nat [THEN FreeUltrafilter_Ex]) +done + +lemma FreeUltrafilterNat_mem: + "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)" +apply (unfold FreeUltrafilterNat_def) +apply (rule FreeUltrafilterNat_Ex [THEN exE]) +apply (rule someI2) +apply assumption+ +done +declare FreeUltrafilterNat_mem [simp] + +lemma FreeUltrafilterNat_finite: "finite x ==> x \ FreeUltrafilterNat" +apply (unfold FreeUltrafilterNat_def) +apply (rule FreeUltrafilterNat_Ex [THEN exE]) +apply (rule someI2 , assumption) +apply (blast dest: mem_FreeUltrafiltersetD1) +done + +lemma FreeUltrafilterNat_not_finite: "x: FreeUltrafilterNat ==> ~ finite x" +apply (blast dest: FreeUltrafilterNat_finite) +done + +lemma FreeUltrafilterNat_empty: "{} \ FreeUltrafilterNat" +apply (unfold FreeUltrafilterNat_def) +apply (rule FreeUltrafilterNat_Ex [THEN exE]) +apply (rule someI2 , assumption) +apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter Filter_empty_not_mem) +done +declare FreeUltrafilterNat_empty [simp] + +lemma FreeUltrafilterNat_Int: "[| X: FreeUltrafilterNat; Y: FreeUltrafilterNat |] + ==> X Int Y \ FreeUltrafilterNat" +apply (cut_tac FreeUltrafilterNat_mem) +apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1) +done + +lemma FreeUltrafilterNat_subset: "[| X: FreeUltrafilterNat; X <= Y |] + ==> Y \ FreeUltrafilterNat" +apply (cut_tac FreeUltrafilterNat_mem) +apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2) +done + +lemma FreeUltrafilterNat_Compl: "X: FreeUltrafilterNat ==> -X \ FreeUltrafilterNat" +apply (safe) +apply (drule FreeUltrafilterNat_Int , assumption) +apply auto +done + +lemma FreeUltrafilterNat_Compl_mem: "X\ FreeUltrafilterNat ==> -X \ FreeUltrafilterNat" +apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) +apply (safe , drule_tac x = "X" in bspec) +apply (auto simp add: UNIV_diff_Compl) +done + +lemma FreeUltrafilterNat_Compl_iff1: "(X \ FreeUltrafilterNat) = (-X: FreeUltrafilterNat)" +apply (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem) +done + +lemma FreeUltrafilterNat_Compl_iff2: "(X: FreeUltrafilterNat) = (-X \ FreeUltrafilterNat)" +apply (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) +done + +lemma FreeUltrafilterNat_UNIV: "(UNIV::nat set) \ FreeUltrafilterNat" +apply (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4]) +done +declare FreeUltrafilterNat_UNIV [simp] + +lemma FreeUltrafilterNat_Nat_set: "UNIV \ FreeUltrafilterNat" +apply auto +done +declare FreeUltrafilterNat_Nat_set [simp] + +lemma FreeUltrafilterNat_Nat_set_refl: "{n. P(n) = P(n)} \ FreeUltrafilterNat" +apply (simp (no_asm)) +done +declare FreeUltrafilterNat_Nat_set_refl [intro] + +lemma FreeUltrafilterNat_P: "{n::nat. P} \ FreeUltrafilterNat ==> P" +apply (rule ccontr) +apply simp +done + +lemma FreeUltrafilterNat_Ex_P: "{n. P(n)} \ FreeUltrafilterNat ==> \n. P(n)" +apply (rule ccontr) +apply simp +done + +lemma FreeUltrafilterNat_all: "\n. P(n) ==> {n. P(n)} \ FreeUltrafilterNat" +apply (auto intro: FreeUltrafilterNat_Nat_set) +done + +(*------------------------------------------------------- + Define and use Ultrafilter tactics + -------------------------------------------------------*) +use "fuf.ML" + +method_setup fuf = {* + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + fuf_tac (Classical.get_local_claset ctxt, + Simplifier.get_local_simpset ctxt) 1)) *} + "free ultrafilter tactic" + +method_setup ultra = {* + Method.ctxt_args (fn ctxt => + Method.METHOD (fn facts => + ultra_tac (Classical.get_local_claset ctxt, + Simplifier.get_local_simpset ctxt) 1)) *} + "ultrafilter tactic" + + +(*------------------------------------------------------- + Now prove one further property of our free ultrafilter + -------------------------------------------------------*) +lemma FreeUltrafilterNat_Un: "X Un Y: FreeUltrafilterNat + ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat" +apply auto +apply (ultra) +done + +(*------------------------------------------------------- + Properties of hyprel + -------------------------------------------------------*) + +(** Proving that hyprel is an equivalence relation **) +(** Natural deduction for hyprel **) + +lemma hyprel_iff: "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)" +apply (unfold hyprel_def) +apply fast +done + +lemma hyprel_refl: "(x,x): hyprel" +apply (unfold hyprel_def) +apply (auto simp add: FreeUltrafilterNat_Nat_set) +done + +lemma hyprel_sym [rule_format (no_asm)]: "(x,y): hyprel --> (y,x):hyprel" +apply (simp add: hyprel_def eq_commute) +done + +lemma hyprel_trans: + "[|(x,y): hyprel; (y,z):hyprel|] ==> (x,z):hyprel" +apply (unfold hyprel_def) +apply auto +apply (ultra) +done + +lemma equiv_hyprel: "equiv UNIV hyprel" +apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl) +apply (blast intro: hyprel_sym hyprel_trans) +done + +(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) \ hyprel) *) +lemmas equiv_hyprel_iff = + eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp] + +lemma hyprel_in_hypreal: "hyprel``{x}:hypreal" +apply (unfold hypreal_def hyprel_def quotient_def) +apply blast +done + +lemma inj_on_Abs_hypreal: "inj_on Abs_hypreal hypreal" +apply (rule inj_on_inverseI) +apply (erule Abs_hypreal_inverse) +done + +declare inj_on_Abs_hypreal [THEN inj_on_iff, simp] + hyprel_in_hypreal [simp] Abs_hypreal_inverse [simp] + +declare equiv_hyprel [THEN eq_equiv_class_iff, simp] + +declare hyprel_iff [iff] + +lemmas eq_hyprelD = eq_equiv_class [OF _ equiv_hyprel] + +lemma inj_Rep_hypreal: "inj(Rep_hypreal)" +apply (rule inj_on_inverseI) +apply (rule Rep_hypreal_inverse) +done + +lemma lemma_hyprel_refl: "x \ hyprel `` {x}" +apply (unfold hyprel_def) +apply (safe) +apply (auto intro!: FreeUltrafilterNat_Nat_set) +done + +declare lemma_hyprel_refl [simp] + +lemma hypreal_empty_not_mem: "{} \ hypreal" +apply (unfold hypreal_def) +apply (auto elim!: quotientE equalityCE) +done + +declare hypreal_empty_not_mem [simp] + +lemma Rep_hypreal_nonempty: "Rep_hypreal x \ {}" +apply (cut_tac x = "x" in Rep_hypreal) +apply auto +done + +declare Rep_hypreal_nonempty [simp] + +(*------------------------------------------------------------------------ + hypreal_of_real: the injection from real to hypreal + ------------------------------------------------------------------------*) + +lemma inj_hypreal_of_real: "inj(hypreal_of_real)" +apply (rule inj_onI) +apply (unfold hypreal_of_real_def) +apply (drule inj_on_Abs_hypreal [THEN inj_onD]) +apply (rule hyprel_in_hypreal)+ +apply (drule eq_equiv_class) +apply (rule equiv_hyprel) +apply (simp_all add: split: split_if_asm) +done + +lemma eq_Abs_hypreal: + "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P" +apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE]) +apply (drule_tac f = "Abs_hypreal" in arg_cong) +apply (force simp add: Rep_hypreal_inverse) +done + +(**** hypreal_minus: additive inverse on hypreal ****) + +lemma hypreal_minus_congruent: + "congruent hyprel (%X. hyprel``{%n. - (X n)})" +by (force simp add: congruent_def) + +lemma hypreal_minus: + "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})" +apply (unfold hypreal_minus_def) +apply (rule_tac f = "Abs_hypreal" in arg_cong) +apply (simp (no_asm) add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] + UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent]) +done + +lemma hypreal_minus_minus: "- (- z) = (z::hypreal)" +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (simp (no_asm_simp) add: hypreal_minus) +done + +declare hypreal_minus_minus [simp] + +lemma inj_hypreal_minus: "inj(%r::hypreal. -r)" +apply (rule inj_onI) +apply (drule_tac f = "uminus" in arg_cong) +apply (simp add: hypreal_minus_minus) +done + +lemma hypreal_minus_zero: "- 0 = (0::hypreal)" +apply (unfold hypreal_zero_def) +apply (simp (no_asm) add: hypreal_minus) +done +declare hypreal_minus_zero [simp] + +lemma hypreal_minus_zero_iff: "(-x = 0) = (x = (0::hypreal))" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (auto simp add: hypreal_zero_def hypreal_minus) +done +declare hypreal_minus_zero_iff [simp] + + +(**** hyperreal addition: hypreal_add ****) + +lemma hypreal_add_congruent2: + "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})" +apply (unfold congruent2_def) +apply (auto ); +apply ultra +done + +lemma hypreal_add: + "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = + Abs_hypreal(hyprel``{%n. X n + Y n})" +apply (unfold hypreal_add_def) +apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2]) +done + +lemma hypreal_diff: "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = + Abs_hypreal(hyprel``{%n. X n - Y n})" +apply (simp (no_asm) add: hypreal_diff_def hypreal_minus hypreal_add) +done + +lemma hypreal_add_commute: "(z::hypreal) + w = w + z" +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (rule_tac z = "w" in eq_Abs_hypreal) +apply (simp (no_asm_simp) add: real_add_ac hypreal_add) +done + +lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)" +apply (rule_tac z = "z1" in eq_Abs_hypreal) +apply (rule_tac z = "z2" in eq_Abs_hypreal) +apply (rule_tac z = "z3" in eq_Abs_hypreal) +apply (simp (no_asm_simp) add: hypreal_add real_add_assoc) +done + +(*For AC rewriting*) +lemma hypreal_add_left_commute: "(x::hypreal)+(y+z)=y+(x+z)" + apply (rule mk_left_commute [of "op +"]) + apply (rule hypreal_add_assoc) + apply (rule hypreal_add_commute) + done + +(* hypreal addition is an AC operator *) +lemmas hypreal_add_ac = + hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute + +lemma hypreal_add_zero_left: "(0::hypreal) + z = z" +apply (unfold hypreal_zero_def) +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (simp add: hypreal_add) +done + +lemma hypreal_add_zero_right: "z + (0::hypreal) = z" +apply (simp (no_asm) add: hypreal_add_zero_left hypreal_add_commute) +done + +lemma hypreal_add_minus: "z + -z = (0::hypreal)" +apply (unfold hypreal_zero_def) +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (simp add: hypreal_minus hypreal_add) +done + +lemma hypreal_add_minus_left: "-z + z = (0::hypreal)" +apply (simp (no_asm) add: hypreal_add_commute hypreal_add_minus) +done + +declare hypreal_add_minus [simp] hypreal_add_minus_left [simp] + hypreal_add_zero_left [simp] hypreal_add_zero_right [simp] + +lemma hypreal_minus_ex: "\y. (x::hypreal) + y = 0" +apply (fast intro: hypreal_add_minus) +done + +lemma hypreal_minus_ex1: "EX! y. (x::hypreal) + y = 0" +apply (auto intro: hypreal_add_minus) +apply (drule_tac f = "%x. ya+x" in arg_cong) +apply (simp add: hypreal_add_assoc [symmetric]) +apply (simp add: hypreal_add_commute) +done + +lemma hypreal_minus_left_ex1: "EX! y. y + (x::hypreal) = 0" +apply (auto intro: hypreal_add_minus_left) +apply (drule_tac f = "%x. x+ya" in arg_cong) +apply (simp add: hypreal_add_assoc) +apply (simp add: hypreal_add_commute) +done + +lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y" +apply (cut_tac z = "y" in hypreal_add_minus_left) +apply (rule_tac x1 = "y" in hypreal_minus_left_ex1 [THEN ex1E]) +apply blast +done + +lemma hypreal_as_add_inverse_ex: "\y::hypreal. x = -y" +apply (cut_tac x = "x" in hypreal_minus_ex) +apply (erule exE , drule hypreal_add_minus_eq_minus) +apply fast +done + +lemma hypreal_minus_add_distrib: "-(x + (y::hypreal)) = -x + -y" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (rule_tac z = "y" in eq_Abs_hypreal) +apply (auto simp add: hypreal_minus hypreal_add real_minus_add_distrib) +done +declare hypreal_minus_add_distrib [simp] + +lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y" +apply (simp (no_asm) add: hypreal_add_commute) +done + +lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)" +apply (safe) +apply (drule_tac f = "%t.-x + t" in arg_cong) +apply (simp add: hypreal_add_assoc [symmetric]) +done + +lemma hypreal_add_right_cancel: "(y + (x::hypreal)= z + x) = (y = z)" +apply (simp (no_asm) add: hypreal_add_commute hypreal_add_left_cancel) +done + +lemma hypreal_add_minus_cancelA: "z + ((- z) + w) = (w::hypreal)" +apply (simp (no_asm) add: hypreal_add_assoc [symmetric]) +done + +lemma hypreal_minus_add_cancelA: "(-z) + (z + w) = (w::hypreal)" +apply (simp (no_asm) add: hypreal_add_assoc [symmetric]) +done + +declare hypreal_add_minus_cancelA [simp] hypreal_minus_add_cancelA [simp] + +(**** hyperreal multiplication: hypreal_mult ****) + +lemma hypreal_mult_congruent2: + "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})" +apply (unfold congruent2_def) +apply auto +apply (ultra) +done + +lemma hypreal_mult: + "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) = + Abs_hypreal(hyprel``{%n. X n * Y n})" +apply (unfold hypreal_mult_def) +apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_mult_congruent2]) +done + +lemma hypreal_mult_commute: "(z::hypreal) * w = w * z" +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (rule_tac z = "w" in eq_Abs_hypreal) +apply (simp (no_asm_simp) add: hypreal_mult real_mult_ac) +done + +lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)" +apply (rule_tac z = "z1" in eq_Abs_hypreal) +apply (rule_tac z = "z2" in eq_Abs_hypreal) +apply (rule_tac z = "z3" in eq_Abs_hypreal) +apply (simp (no_asm_simp) add: hypreal_mult real_mult_assoc) +done + +lemma hypreal_mult_left_commute: "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)" + apply (rule mk_left_commute [of "op *"]) + apply (rule hypreal_mult_assoc) + apply (rule hypreal_mult_commute) + done + +(* hypreal multiplication is an AC operator *) +lemmas hypreal_mult_ac = + hypreal_mult_assoc hypreal_mult_commute hypreal_mult_left_commute + +lemma hypreal_mult_1: "(1::hypreal) * z = z" +apply (unfold hypreal_one_def) +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (simp add: hypreal_mult) +done +declare hypreal_mult_1 [simp] + +lemma hypreal_mult_1_right: "z * (1::hypreal) = z" +apply (simp (no_asm) add: hypreal_mult_commute hypreal_mult_1) +done +declare hypreal_mult_1_right [simp] + +lemma hypreal_mult_0: "0 * z = (0::hypreal)" +apply (unfold hypreal_zero_def) +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (simp add: hypreal_mult) +done +declare hypreal_mult_0 [simp] + +lemma hypreal_mult_0_right: "z * 0 = (0::hypreal)" +apply (simp (no_asm) add: hypreal_mult_commute) +done +declare hypreal_mult_0_right [simp] + +lemma hypreal_minus_mult_eq1: "-(x * y) = -x * (y::hypreal)" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (rule_tac z = "y" in eq_Abs_hypreal) +apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) +done + +lemma hypreal_minus_mult_eq2: "-(x * y) = (x::hypreal) * -y" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (rule_tac z = "y" in eq_Abs_hypreal) +apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac) +done + +(*Pull negations out*) +declare hypreal_minus_mult_eq2 [symmetric, simp] hypreal_minus_mult_eq1 [symmetric, simp] + +lemma hypreal_mult_minus_1: "(- (1::hypreal)) * z = -z" +apply (simp (no_asm)) +done +declare hypreal_mult_minus_1 [simp] + +lemma hypreal_mult_minus_1_right: "z * (- (1::hypreal)) = -z" +apply (subst hypreal_mult_commute) +apply (simp (no_asm)) +done +declare hypreal_mult_minus_1_right [simp] + +lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y" +apply auto +done + +(*----------------------------------------------------------------------------- + A few more theorems + ----------------------------------------------------------------------------*) +lemma hypreal_add_assoc_cong: "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)" +apply (simp (no_asm_simp) add: hypreal_add_assoc [symmetric]) +done + +lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)" +apply (rule_tac z = "z1" in eq_Abs_hypreal) +apply (rule_tac z = "z2" in eq_Abs_hypreal) +apply (rule_tac z = "w" in eq_Abs_hypreal) +apply (simp (no_asm_simp) add: hypreal_mult hypreal_add real_add_mult_distrib) +done + +lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)" +apply (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib) +done + + +lemma hypreal_diff_mult_distrib: "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)" + +apply (unfold hypreal_diff_def) +apply (simp (no_asm) add: hypreal_add_mult_distrib) +done + +lemma hypreal_diff_mult_distrib2: "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)" +apply (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib) +done + +(*** one and zero are distinct ***) +lemma hypreal_zero_not_eq_one: "0 \ (1::hypreal)" +apply (unfold hypreal_zero_def hypreal_one_def) +apply (auto simp add: real_zero_not_eq_one) +done + + +(**** multiplicative inverse on hypreal ****) + +lemma hypreal_inverse_congruent: + "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})" +apply (unfold congruent_def) +apply (auto , ultra) +done + +lemma hypreal_inverse: + "inverse (Abs_hypreal(hyprel``{%n. X n})) = + Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})" +apply (unfold hypreal_inverse_def) +apply (rule_tac f = "Abs_hypreal" in arg_cong) +apply (simp (no_asm) add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] + UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent]) +done + +lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)" +apply (simp (no_asm) add: hypreal_inverse hypreal_zero_def) +done + +lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0" +apply (simp (no_asm) add: hypreal_divide_def HYPREAL_INVERSE_ZERO) +done + +lemma hypreal_inverse_inverse: "inverse (inverse (z::hypreal)) = z" +apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO) +apply (rule_tac z = "z" in eq_Abs_hypreal) +apply (simp add: hypreal_inverse hypreal_zero_def) +done +declare hypreal_inverse_inverse [simp] + +lemma hypreal_inverse_1: "inverse((1::hypreal)) = (1::hypreal)" +apply (unfold hypreal_one_def) +apply (simp (no_asm_use) add: hypreal_inverse real_zero_not_eq_one [THEN not_sym]) +done +declare hypreal_inverse_1 [simp] + + +(*** existence of inverse ***) + +lemma hypreal_mult_inverse: + "x \ 0 ==> x*inverse(x) = (1::hypreal)" + +apply (unfold hypreal_one_def hypreal_zero_def) +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (simp add: hypreal_inverse hypreal_mult) +apply (drule FreeUltrafilterNat_Compl_mem) +apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset) +done + +lemma hypreal_mult_inverse_left: "x \ 0 ==> inverse(x)*x = (1::hypreal)" +apply (simp (no_asm_simp) add: hypreal_mult_inverse hypreal_mult_commute) +done + +lemma hypreal_mult_left_cancel: "(c::hypreal) \ 0 ==> (c*a=c*b) = (a=b)" +apply auto +apply (drule_tac f = "%x. x*inverse c" in arg_cong) +apply (simp add: hypreal_mult_inverse hypreal_mult_ac) +done + +lemma hypreal_mult_right_cancel: "(c::hypreal) \ 0 ==> (a*c=b*c) = (a=b)" +apply (safe) +apply (drule_tac f = "%x. x*inverse c" in arg_cong) +apply (simp add: hypreal_mult_inverse hypreal_mult_ac) +done + +lemma hypreal_inverse_not_zero: "x \ 0 ==> inverse (x::hypreal) \ 0" +apply (unfold hypreal_zero_def) +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (simp add: hypreal_inverse hypreal_mult) +done + +declare hypreal_mult_inverse [simp] hypreal_mult_inverse_left [simp] + +lemma hypreal_mult_not_0: "[| x \ 0; y \ 0 |] ==> x * y \ (0::hypreal)" +apply (safe) +apply (drule_tac f = "%z. inverse x*z" in arg_cong) +apply (simp add: hypreal_mult_assoc [symmetric]) +done + +lemma hypreal_mult_zero_disj: "x*y = (0::hypreal) ==> x = 0 | y = 0" +apply (auto intro: ccontr dest: hypreal_mult_not_0) +done + +lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)" +apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) +apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1]) +apply (simp add: ); +apply (subst hypreal_mult_inverse_left) +apply auto +done + +lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)" +apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO) +apply (case_tac "y=0", simp add: HYPREAL_INVERSE_ZERO) +apply (frule_tac y = "y" in hypreal_mult_not_0 , assumption) +apply (rule_tac c1 = "x" in hypreal_mult_left_cancel [THEN iffD1]) +apply (auto simp add: hypreal_mult_assoc [symmetric]) +apply (rule_tac c1 = "y" in hypreal_mult_left_cancel [THEN iffD1]) +apply (auto simp add: hypreal_mult_left_commute) +apply (simp (no_asm_simp) add: hypreal_mult_assoc [symmetric]) +done + +(*------------------------------------------------------------------ + Theorems for ordering + ------------------------------------------------------------------*) + +(* prove introduction and elimination rules for hypreal_less *) + +lemma hypreal_less_iff: + "(P < (Q::hypreal)) = (\X Y. X \ Rep_hypreal(P) & + Y \ Rep_hypreal(Q) & + {n. X n < Y n} \ FreeUltrafilterNat)" + +apply (unfold hypreal_less_def) +apply fast +done + +lemma hypreal_lessI: + "[| {n. X n < Y n} \ FreeUltrafilterNat; + X \ Rep_hypreal(P); + Y \ Rep_hypreal(Q) |] ==> P < (Q::hypreal)" +apply (unfold hypreal_less_def) +apply fast +done + + +lemma hypreal_lessE: + "!! R1. [| R1 < (R2::hypreal); + !!X Y. {n. X n < Y n} \ FreeUltrafilterNat ==> P; + !!X. X \ Rep_hypreal(R1) ==> P; + !!Y. Y \ Rep_hypreal(R2) ==> P |] + ==> P" + +apply (unfold hypreal_less_def) +apply auto +done + +lemma hypreal_lessD: + "R1 < (R2::hypreal) ==> (\X Y. {n. X n < Y n} \ FreeUltrafilterNat & + X \ Rep_hypreal(R1) & + Y \ Rep_hypreal(R2))" +apply (unfold hypreal_less_def) +apply fast +done + +lemma hypreal_less_not_refl: "~ (R::hypreal) < R" +apply (rule_tac z = "R" in eq_Abs_hypreal) +apply (auto simp add: hypreal_less_def) +apply (ultra) +done + +(*** y < y ==> P ***) +lemmas hypreal_less_irrefl = hypreal_less_not_refl [THEN notE, standard] +declare hypreal_less_irrefl [elim!] + +lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \ y" +apply (auto simp add: hypreal_less_not_refl) +done + +lemma hypreal_less_trans: "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3" +apply (rule_tac z = "R1" in eq_Abs_hypreal) +apply (rule_tac z = "R2" in eq_Abs_hypreal) +apply (rule_tac z = "R3" in eq_Abs_hypreal) +apply (auto intro!: exI simp add: hypreal_less_def) +apply ultra +done + +lemma hypreal_less_asym: "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P" +apply (drule hypreal_less_trans , assumption) +apply (simp add: hypreal_less_not_refl) +done + +(*------------------------------------------------------- + TODO: The following theorem should have been proved + first and then used througout the proofs as it probably + makes many of them more straightforward. + -------------------------------------------------------*) +lemma hypreal_less: + "(Abs_hypreal(hyprel``{%n. X n}) < + Abs_hypreal(hyprel``{%n. Y n})) = + ({n. X n < Y n} \ FreeUltrafilterNat)" +apply (unfold hypreal_less_def) +apply (auto intro!: lemma_hyprel_refl) +apply (ultra) +done + +(*---------------------------------------------------------------------------- + Trichotomy: the hyperreals are linearly ordered + ---------------------------------------------------------------------------*) + +lemma lemma_hyprel_0_mem: "\x. x: hyprel `` {%n. 0}" + +apply (unfold hyprel_def) +apply (rule_tac x = "%n. 0" in exI) +apply (safe) +apply (auto intro!: FreeUltrafilterNat_Nat_set) +done + +lemma hypreal_trichotomy: "0 < x | x = 0 | x < (0::hypreal)" +apply (unfold hypreal_zero_def) +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (auto simp add: hypreal_less_def) +apply (cut_tac lemma_hyprel_0_mem , erule exE) +apply (drule_tac x = "xa" in spec) +apply (drule_tac x = "x" in spec) +apply (cut_tac x = "x" in lemma_hyprel_refl) +apply auto +apply (drule_tac x = "x" in spec) +apply (drule_tac x = "xa" in spec) +apply auto +apply (ultra) +done + +lemma hypreal_trichotomyE: + "[| (0::hypreal) < x ==> P; + x = 0 ==> P; + x < 0 ==> P |] ==> P" +apply (insert hypreal_trichotomy [of x]) +apply (blast intro: elim:); +done + +(*---------------------------------------------------------------------------- + More properties of < + ----------------------------------------------------------------------------*) + +lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (rule_tac z = "y" in eq_Abs_hypreal) +apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less) +done + +lemma hypreal_less_minus_iff2: "((x::hypreal) < y) = (x + -y < 0)" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (rule_tac z = "y" in eq_Abs_hypreal) +apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less) +done + +lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)" +apply auto +apply (rule_tac x1 = "-y" in hypreal_add_right_cancel [THEN iffD1]) +apply auto +done + +lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)" +apply auto +apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1]) +apply auto +done + +(* 07/00 *) +lemma hypreal_diff_zero: "(0::hypreal) - x = -x" +apply (simp (no_asm) add: hypreal_diff_def) +done + +lemma hypreal_diff_zero_right: "x - (0::hypreal) = x" +apply (simp (no_asm) add: hypreal_diff_def) +done + +lemma hypreal_diff_self: "x - x = (0::hypreal)" +apply (simp (no_asm) add: hypreal_diff_def) +done + +declare hypreal_diff_zero [simp] hypreal_diff_zero_right [simp] hypreal_diff_self [simp] + +lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))" +apply (auto simp add: hypreal_add_assoc) +done + +lemma hypreal_not_eq_minus_iff: "(x \ a) = (x + -a \ (0::hypreal))" +apply (auto dest: hypreal_eq_minus_iff [THEN iffD2]) +done + + +(*** linearity ***) + +lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x" +apply (subst hypreal_eq_minus_iff2) +apply (rule_tac x1 = "x" in hypreal_less_minus_iff [THEN ssubst]) +apply (rule_tac x1 = "y" in hypreal_less_minus_iff2 [THEN ssubst]) +apply (rule hypreal_trichotomyE) +apply auto +done + +lemma hypreal_neq_iff: "((w::hypreal) \ z) = (w P; x = y ==> P; + y < x ==> P |] ==> P" +apply (cut_tac x = "x" and y = "y" in hypreal_linear) +apply auto +done + +(*------------------------------------------------------------------------------ + Properties of <= + ------------------------------------------------------------------------------*) +(*------ hypreal le iff reals le a.e ------*) + +lemma hypreal_le: + "(Abs_hypreal(hyprel``{%n. X n}) <= + Abs_hypreal(hyprel``{%n. Y n})) = + ({n. X n <= Y n} \ FreeUltrafilterNat)" +apply (unfold hypreal_le_def real_le_def) +apply (auto simp add: hypreal_less) +apply (ultra+) +done + +(*---------------------------------------------------------*) +(*---------------------------------------------------------*) +lemma hypreal_leI: + "~(w < z) ==> z <= (w::hypreal)" +apply (unfold hypreal_le_def) +apply assumption +done + +lemma hypreal_leD: + "z<=w ==> ~(w<(z::hypreal))" +apply (unfold hypreal_le_def) +apply assumption +done + +lemma hypreal_less_le_iff: "(~(w < z)) = (z <= (w::hypreal))" +apply (fast intro!: hypreal_leI hypreal_leD) +done + +lemma not_hypreal_leE: "~ z <= w ==> w<(z::hypreal)" +apply (unfold hypreal_le_def) +apply fast +done + +lemma hypreal_le_imp_less_or_eq: "!!(x::hypreal). x <= y ==> x < y | x = y" +apply (unfold hypreal_le_def) +apply (cut_tac hypreal_linear) +apply (fast elim: hypreal_less_irrefl hypreal_less_asym) +done + +lemma hypreal_less_or_eq_imp_le: "z z <=(w::hypreal)" +apply (unfold hypreal_le_def) +apply (cut_tac hypreal_linear) +apply (fast elim: hypreal_less_irrefl hypreal_less_asym) +done + +lemma hypreal_le_eq_less_or_eq: "(x <= (y::hypreal)) = (x < y | x=y)" +by (blast intro!: hypreal_less_or_eq_imp_le dest: hypreal_le_imp_less_or_eq) + +lemmas hypreal_le_less = hypreal_le_eq_less_or_eq + +lemma hypreal_le_refl: "w <= (w::hypreal)" +apply (simp (no_asm) add: hypreal_le_eq_less_or_eq) +done + +(* Axiom 'linorder_linear' of class 'linorder': *) +lemma hypreal_le_linear: "(z::hypreal) <= w | w <= z" +apply (simp (no_asm) add: hypreal_le_less) +apply (cut_tac hypreal_linear) +apply blast +done + +lemma hypreal_le_trans: "[| i <= j; j <= k |] ==> i <= (k::hypreal)" +apply (drule hypreal_le_imp_less_or_eq) +apply (drule hypreal_le_imp_less_or_eq) +apply (rule hypreal_less_or_eq_imp_le) +apply (blast intro: hypreal_less_trans) +done + +lemma hypreal_le_anti_sym: "[| z <= w; w <= z |] ==> z = (w::hypreal)" +apply (drule hypreal_le_imp_less_or_eq) +apply (drule hypreal_le_imp_less_or_eq) +apply (fast elim: hypreal_less_irrefl hypreal_less_asym) +done + +lemma not_less_not_eq_hypreal_less: "[| ~ y < x; y \ x |] ==> x < (y::hypreal)" +apply (rule not_hypreal_leE) +apply (fast dest: hypreal_le_imp_less_or_eq) +done + +(* Axiom 'order_less_le' of class 'order': *) +lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \ z)" +apply (simp (no_asm) add: hypreal_le_def hypreal_neq_iff) +apply (blast intro: hypreal_less_asym) +done + +lemma hypreal_minus_zero_less_iff: "(0 < -R) = (R < (0::hypreal))" +apply (rule_tac z = "R" in eq_Abs_hypreal) +apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) +done +declare hypreal_minus_zero_less_iff [simp] + +lemma hypreal_minus_zero_less_iff2: "(-R < 0) = ((0::hypreal) < R)" +apply (rule_tac z = "R" in eq_Abs_hypreal) +apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus) +done +declare hypreal_minus_zero_less_iff2 [simp] + +lemma hypreal_minus_zero_le_iff: "((0::hypreal) <= -r) = (r <= 0)" +apply (unfold hypreal_le_def) +apply (simp (no_asm) add: hypreal_minus_zero_less_iff2) +done +declare hypreal_minus_zero_le_iff [simp] + +lemma hypreal_minus_zero_le_iff2: "(-r <= (0::hypreal)) = (0 <= r)" +apply (unfold hypreal_le_def) +apply (simp (no_asm) add: hypreal_minus_zero_less_iff2) +done +declare hypreal_minus_zero_le_iff2 [simp] + +(*---------------------------------------------------------- + hypreal_of_real preserves field and order properties + -----------------------------------------------------------*) +lemma hypreal_of_real_add: + "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2" +apply (unfold hypreal_of_real_def) +apply (simp (no_asm) add: hypreal_add hypreal_add_mult_distrib) +done +declare hypreal_of_real_add [simp] + +lemma hypreal_of_real_mult: + "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2" +apply (unfold hypreal_of_real_def) +apply (simp (no_asm) add: hypreal_mult hypreal_add_mult_distrib2) +done +declare hypreal_of_real_mult [simp] + +lemma hypreal_of_real_less_iff: + "(hypreal_of_real z1 < hypreal_of_real z2) = (z1 < z2)" +apply (unfold hypreal_less_def hypreal_of_real_def) +apply auto +apply (rule_tac [2] x = "%n. z1" in exI) +apply (safe) +apply (rule_tac [3] x = "%n. z2" in exI) +apply auto +apply (rule FreeUltrafilterNat_P) +apply (ultra) +done +declare hypreal_of_real_less_iff [simp] + +lemma hypreal_of_real_le_iff: + "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)" +apply (unfold hypreal_le_def real_le_def) +apply auto +done +declare hypreal_of_real_le_iff [simp] + +lemma hypreal_of_real_eq_iff: "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)" +apply (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1]) +done +declare hypreal_of_real_eq_iff [simp] + +lemma hypreal_of_real_minus: "hypreal_of_real (-r) = - hypreal_of_real r" +apply (unfold hypreal_of_real_def) +apply (auto simp add: hypreal_minus) +done +declare hypreal_of_real_minus [simp] + +lemma hypreal_of_real_one: "hypreal_of_real 1 = (1::hypreal)" +apply (unfold hypreal_of_real_def hypreal_one_def) +apply (simp (no_asm)) +done +declare hypreal_of_real_one [simp] + +lemma hypreal_of_real_zero: "hypreal_of_real 0 = 0" +apply (unfold hypreal_of_real_def hypreal_zero_def) +apply (simp (no_asm)) +done +declare hypreal_of_real_zero [simp] + +lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)" +apply (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set) +done + +lemma hypreal_of_real_inverse: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)" +apply (case_tac "r=0") +apply (simp (no_asm_simp) add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO) +apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1]) +apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric]) +done +declare hypreal_of_real_inverse [simp] + +lemma hypreal_of_real_divide: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2" +apply (simp (no_asm) add: hypreal_divide_def real_divide_def) +done +declare hypreal_of_real_divide [simp] + + +(*** Division lemmas ***) + +lemma hypreal_zero_divide: "(0::hypreal)/x = 0" +apply (simp (no_asm) add: hypreal_divide_def) +done + +lemma hypreal_divide_one: "x/(1::hypreal) = x" +apply (simp (no_asm) add: hypreal_divide_def) +done +declare hypreal_zero_divide [simp] hypreal_divide_one [simp] + +lemma hypreal_times_divide1_eq: "(x::hypreal) * (y/z) = (x*y)/z" +apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_assoc) +done + +lemma hypreal_times_divide2_eq: "(y/z) * (x::hypreal) = (y*x)/z" +apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_ac) +done + +declare hypreal_times_divide1_eq [simp] hypreal_times_divide2_eq [simp] + +lemma hypreal_divide_divide1_eq: "(x::hypreal) / (y/z) = (x*z)/y" +apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac) +done + +lemma hypreal_divide_divide2_eq: "((x::hypreal) / y) / z = x/(y*z)" +apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc) +done + +declare hypreal_divide_divide1_eq [simp] hypreal_divide_divide2_eq [simp] + +(** As with multiplication, pull minus signs OUT of the / operator **) + +lemma hypreal_minus_divide_eq: "(-x) / (y::hypreal) = - (x/y)" +apply (simp (no_asm) add: hypreal_divide_def) +done +declare hypreal_minus_divide_eq [simp] + +lemma hypreal_divide_minus_eq: "(x / -(y::hypreal)) = - (x/y)" +apply (simp (no_asm) add: hypreal_divide_def hypreal_minus_inverse) +done +declare hypreal_divide_minus_eq [simp] + +lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z" +apply (simp (no_asm) add: hypreal_divide_def hypreal_add_mult_distrib) +done + +lemma hypreal_inverse_add: "[|(x::hypreal) \ 0; y \ 0 |] + ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)" +apply (simp add: hypreal_inverse_distrib hypreal_add_mult_distrib hypreal_mult_assoc [symmetric]) +apply (subst hypreal_mult_assoc) +apply (rule hypreal_mult_left_commute [THEN subst]) +apply (simp add: hypreal_add_commute) +done + +lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (auto simp add: hypreal_minus hypreal_zero_def) +apply (ultra) +done + +lemma hypreal_add_self_zero_cancel: "(x + x = 0) = (x = (0::hypreal))" +apply (rule_tac z = "x" in eq_Abs_hypreal) +apply (auto simp add: hypreal_add hypreal_zero_def) +done +declare hypreal_add_self_zero_cancel [simp] + +lemma hypreal_add_self_zero_cancel2: "(x + x + y = y) = (x = (0::hypreal))" +apply auto +apply (drule hypreal_eq_minus_iff [THEN iffD1]) +apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero) +done +declare hypreal_add_self_zero_cancel2 [simp] + +lemma hypreal_add_self_zero_cancel2a: "(x + (x + y) = y) = (x = (0::hypreal))" +apply (simp (no_asm) add: hypreal_add_assoc [symmetric]) +done +declare hypreal_add_self_zero_cancel2a [simp] + +lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))" +apply auto +done + +lemma hypreal_minus_eq_cancel: "(-b = -a) = (b = (a::hypreal))" +apply (simp add: hypreal_minus_eq_swap) +done +declare hypreal_minus_eq_cancel [simp] + +lemma hypreal_less_eq_diff: "(x (x (y<=x) = (y'<=x')" +apply (drule hypreal_less_eqI) +apply (simp (no_asm_simp) add: hypreal_le_def) +done + +lemma hypreal_eq_eqI: "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')" +apply safe +apply (simp_all add: hypreal_eq_diff_eq hypreal_diff_eq_eq) +done + +lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})" +apply (simp (no_asm) add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric]) +done + +lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})" +apply (simp (no_asm) add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric]) +done + +lemma hypreal_omega_gt_zero: "0 < omega" +apply (unfold omega_def) +apply (auto simp add: hypreal_less hypreal_zero_num) +done +declare hypreal_omega_gt_zero [simp] + +ML +{* +val hypreal_zero_def = thm "hypreal_zero_def"; +val hypreal_one_def = thm "hypreal_one_def"; +val hypreal_minus_def = thm "hypreal_minus_def"; +val hypreal_diff_def = thm "hypreal_diff_def"; +val hypreal_inverse_def = thm "hypreal_inverse_def"; +val hypreal_divide_def = thm "hypreal_divide_def"; +val hypreal_of_real_def = thm "hypreal_of_real_def"; +val omega_def = thm "omega_def"; +val epsilon_def = thm "epsilon_def"; +val hypreal_add_def = thm "hypreal_add_def"; +val hypreal_mult_def = thm "hypreal_mult_def"; +val hypreal_less_def = thm "hypreal_less_def"; +val hypreal_le_def = thm "hypreal_le_def"; + +val finite_exhausts = thm "finite_exhausts"; +val finite_not_covers = thm "finite_not_covers"; +val not_finite_nat = thm "not_finite_nat"; +val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex"; +val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem"; +val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite"; +val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite"; +val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty"; +val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int"; +val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset"; +val FreeUltrafilterNat_Compl = thm "FreeUltrafilterNat_Compl"; +val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem"; +val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1"; +val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2"; +val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV"; +val FreeUltrafilterNat_Nat_set = thm "FreeUltrafilterNat_Nat_set"; +val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl"; +val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P"; +val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P"; +val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all"; +val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un"; +val hyprel_iff = thm "hyprel_iff"; +val hyprel_refl = thm "hyprel_refl"; +val hyprel_sym = thm "hyprel_sym"; +val hyprel_trans = thm "hyprel_trans"; +val equiv_hyprel = thm "equiv_hyprel"; +val hyprel_in_hypreal = thm "hyprel_in_hypreal"; +val Abs_hypreal_inverse = thm "Abs_hypreal_inverse"; +val inj_on_Abs_hypreal = thm "inj_on_Abs_hypreal"; +val inj_Rep_hypreal = thm "inj_Rep_hypreal"; +val lemma_hyprel_refl = thm "lemma_hyprel_refl"; +val hypreal_empty_not_mem = thm "hypreal_empty_not_mem"; +val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty"; +val inj_hypreal_of_real = thm "inj_hypreal_of_real"; +val eq_Abs_hypreal = thm "eq_Abs_hypreal"; +val hypreal_minus_congruent = thm "hypreal_minus_congruent"; +val hypreal_minus = thm "hypreal_minus"; +val hypreal_minus_minus = thm "hypreal_minus_minus"; +val inj_hypreal_minus = thm "inj_hypreal_minus"; +val hypreal_minus_zero = thm "hypreal_minus_zero"; +val hypreal_minus_zero_iff = thm "hypreal_minus_zero_iff"; +val hypreal_add_congruent2 = thm "hypreal_add_congruent2"; +val hypreal_add = thm "hypreal_add"; +val hypreal_diff = thm "hypreal_diff"; +val hypreal_add_commute = thm "hypreal_add_commute"; +val hypreal_add_assoc = thm "hypreal_add_assoc"; +val hypreal_add_left_commute = thm "hypreal_add_left_commute"; +val hypreal_add_zero_left = thm "hypreal_add_zero_left"; +val hypreal_add_zero_right = thm "hypreal_add_zero_right"; +val hypreal_add_minus = thm "hypreal_add_minus"; +val hypreal_add_minus_left = thm "hypreal_add_minus_left"; +val hypreal_minus_ex = thm "hypreal_minus_ex"; +val hypreal_minus_ex1 = thm "hypreal_minus_ex1"; +val hypreal_minus_left_ex1 = thm "hypreal_minus_left_ex1"; +val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus"; +val hypreal_as_add_inverse_ex = thm "hypreal_as_add_inverse_ex"; +val hypreal_minus_add_distrib = thm "hypreal_minus_add_distrib"; +val hypreal_minus_distrib1 = thm "hypreal_minus_distrib1"; +val hypreal_add_left_cancel = thm "hypreal_add_left_cancel"; +val hypreal_add_right_cancel = thm "hypreal_add_right_cancel"; +val hypreal_add_minus_cancelA = thm "hypreal_add_minus_cancelA"; +val hypreal_minus_add_cancelA = thm "hypreal_minus_add_cancelA"; +val hypreal_mult_congruent2 = thm "hypreal_mult_congruent2"; +val hypreal_mult = thm "hypreal_mult"; +val hypreal_mult_commute = thm "hypreal_mult_commute"; +val hypreal_mult_assoc = thm "hypreal_mult_assoc"; +val hypreal_mult_left_commute = thm "hypreal_mult_left_commute"; +val hypreal_mult_1 = thm "hypreal_mult_1"; +val hypreal_mult_1_right = thm "hypreal_mult_1_right"; +val hypreal_mult_0 = thm "hypreal_mult_0"; +val hypreal_mult_0_right = thm "hypreal_mult_0_right"; +val hypreal_minus_mult_eq1 = thm "hypreal_minus_mult_eq1"; +val hypreal_minus_mult_eq2 = thm "hypreal_minus_mult_eq2"; +val hypreal_mult_minus_1 = thm "hypreal_mult_minus_1"; +val hypreal_mult_minus_1_right = thm "hypreal_mult_minus_1_right"; +val hypreal_minus_mult_commute = thm "hypreal_minus_mult_commute"; +val hypreal_add_assoc_cong = thm "hypreal_add_assoc_cong"; +val hypreal_add_mult_distrib = thm "hypreal_add_mult_distrib"; +val hypreal_add_mult_distrib2 = thm "hypreal_add_mult_distrib2"; +val hypreal_diff_mult_distrib = thm "hypreal_diff_mult_distrib"; +val hypreal_diff_mult_distrib2 = thm "hypreal_diff_mult_distrib2"; +val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one"; +val hypreal_inverse_congruent = thm "hypreal_inverse_congruent"; +val hypreal_inverse = thm "hypreal_inverse"; +val HYPREAL_INVERSE_ZERO = thm "HYPREAL_INVERSE_ZERO"; +val HYPREAL_DIVISION_BY_ZERO = thm "HYPREAL_DIVISION_BY_ZERO"; +val hypreal_inverse_inverse = thm "hypreal_inverse_inverse"; +val hypreal_inverse_1 = thm "hypreal_inverse_1"; +val hypreal_mult_inverse = thm "hypreal_mult_inverse"; +val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left"; +val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel"; +val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel"; +val hypreal_inverse_not_zero = thm "hypreal_inverse_not_zero"; +val hypreal_mult_not_0 = thm "hypreal_mult_not_0"; +val hypreal_mult_zero_disj = thm "hypreal_mult_zero_disj"; +val hypreal_minus_inverse = thm "hypreal_minus_inverse"; +val hypreal_inverse_distrib = thm "hypreal_inverse_distrib"; +val hypreal_less_iff = thm "hypreal_less_iff"; +val hypreal_lessI = thm "hypreal_lessI"; +val hypreal_lessE = thm "hypreal_lessE"; +val hypreal_lessD = thm "hypreal_lessD"; +val hypreal_less_not_refl = thm "hypreal_less_not_refl"; +val hypreal_not_refl2 = thm "hypreal_not_refl2"; +val hypreal_less_trans = thm "hypreal_less_trans"; +val hypreal_less_asym = thm "hypreal_less_asym"; +val hypreal_less = thm "hypreal_less"; +val hypreal_trichotomy = thm "hypreal_trichotomy"; +val hypreal_trichotomyE = thm "hypreal_trichotomyE"; +val hypreal_less_minus_iff = thm "hypreal_less_minus_iff"; +val hypreal_less_minus_iff2 = thm "hypreal_less_minus_iff2"; +val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff"; +val hypreal_eq_minus_iff2 = thm "hypreal_eq_minus_iff2"; +val hypreal_diff_zero = thm "hypreal_diff_zero"; +val hypreal_diff_zero_right = thm "hypreal_diff_zero_right"; +val hypreal_diff_self = thm "hypreal_diff_self"; +val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3"; +val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff"; +val hypreal_linear = thm "hypreal_linear"; +val hypreal_neq_iff = thm "hypreal_neq_iff"; +val hypreal_linear_less2 = thm "hypreal_linear_less2"; +val hypreal_le = thm "hypreal_le"; +val hypreal_leI = thm "hypreal_leI"; +val hypreal_leD = thm "hypreal_leD"; +val hypreal_less_le_iff = thm "hypreal_less_le_iff"; +val not_hypreal_leE = thm "not_hypreal_leE"; +val hypreal_le_imp_less_or_eq = thm "hypreal_le_imp_less_or_eq"; +val hypreal_less_or_eq_imp_le = thm "hypreal_less_or_eq_imp_le"; +val hypreal_le_eq_less_or_eq = thm "hypreal_le_eq_less_or_eq"; +val hypreal_le_refl = thm "hypreal_le_refl"; +val hypreal_le_linear = thm "hypreal_le_linear"; +val hypreal_le_trans = thm "hypreal_le_trans"; +val hypreal_le_anti_sym = thm "hypreal_le_anti_sym"; +val not_less_not_eq_hypreal_less = thm "not_less_not_eq_hypreal_less"; +val hypreal_less_le = thm "hypreal_less_le"; +val hypreal_minus_zero_less_iff = thm "hypreal_minus_zero_less_iff"; +val hypreal_minus_zero_less_iff2 = thm "hypreal_minus_zero_less_iff2"; +val hypreal_minus_zero_le_iff = thm "hypreal_minus_zero_le_iff"; +val hypreal_minus_zero_le_iff2 = thm "hypreal_minus_zero_le_iff2"; +val hypreal_of_real_add = thm "hypreal_of_real_add"; +val hypreal_of_real_mult = thm "hypreal_of_real_mult"; +val hypreal_of_real_less_iff = thm "hypreal_of_real_less_iff"; +val hypreal_of_real_le_iff = thm "hypreal_of_real_le_iff"; +val hypreal_of_real_eq_iff = thm "hypreal_of_real_eq_iff"; +val hypreal_of_real_minus = thm "hypreal_of_real_minus"; +val hypreal_of_real_one = thm "hypreal_of_real_one"; +val hypreal_of_real_zero = thm "hypreal_of_real_zero"; +val hypreal_of_real_zero_iff = thm "hypreal_of_real_zero_iff"; +val hypreal_of_real_inverse = thm "hypreal_of_real_inverse"; +val hypreal_of_real_divide = thm "hypreal_of_real_divide"; +val hypreal_zero_divide = thm "hypreal_zero_divide"; +val hypreal_divide_one = thm "hypreal_divide_one"; +val hypreal_times_divide1_eq = thm "hypreal_times_divide1_eq"; +val hypreal_times_divide2_eq = thm "hypreal_times_divide2_eq"; +val hypreal_divide_divide1_eq = thm "hypreal_divide_divide1_eq"; +val hypreal_divide_divide2_eq = thm "hypreal_divide_divide2_eq"; +val hypreal_minus_divide_eq = thm "hypreal_minus_divide_eq"; +val hypreal_divide_minus_eq = thm "hypreal_divide_minus_eq"; +val hypreal_add_divide_distrib = thm "hypreal_add_divide_distrib"; +val hypreal_inverse_add = thm "hypreal_inverse_add"; +val hypreal_self_eq_minus_self_zero = thm "hypreal_self_eq_minus_self_zero"; +val hypreal_add_self_zero_cancel = thm "hypreal_add_self_zero_cancel"; +val hypreal_add_self_zero_cancel2 = thm "hypreal_add_self_zero_cancel2"; +val hypreal_add_self_zero_cancel2a = thm "hypreal_add_self_zero_cancel2a"; +val hypreal_minus_eq_swap = thm "hypreal_minus_eq_swap"; +val hypreal_minus_eq_cancel = thm "hypreal_minus_eq_cancel"; +val hypreal_less_eq_diff = thm "hypreal_less_eq_diff"; +val hypreal_add_diff_eq = thm "hypreal_add_diff_eq"; +val hypreal_diff_add_eq = thm "hypreal_diff_add_eq"; +val hypreal_diff_diff_eq = thm "hypreal_diff_diff_eq"; +val hypreal_diff_diff_eq2 = thm "hypreal_diff_diff_eq2"; +val hypreal_diff_less_eq = thm "hypreal_diff_less_eq"; +val hypreal_less_diff_eq = thm "hypreal_less_diff_eq"; +val hypreal_diff_le_eq = thm "hypreal_diff_le_eq"; +val hypreal_le_diff_eq = thm "hypreal_le_diff_eq"; +val hypreal_diff_eq_eq = thm "hypreal_diff_eq_eq"; +val hypreal_eq_diff_eq = thm "hypreal_eq_diff_eq"; +val hypreal_less_eqI = thm "hypreal_less_eqI"; +val hypreal_le_eqI = thm "hypreal_le_eqI"; +val hypreal_eq_eqI = thm "hypreal_eq_eqI"; +val hypreal_zero_num = thm "hypreal_zero_num"; +val hypreal_one_num = thm "hypreal_one_num"; +val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero"; +*} + + end diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HyperNat.ML --- a/src/HOL/Hyperreal/HyperNat.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/HyperNat.ML Wed Dec 17 16:23:52 2003 +0100 @@ -48,9 +48,9 @@ by Auto_tac; qed "hypnatrel_refl"; -Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,x):hypnatrel"; -by (auto_tac (claset() addIs [lemma_perm RS subst], simpset())); -qed_spec_mp "hypnatrel_sym"; +Goal "(x,y): hypnatrel ==> (y,x):hypnatrel"; +by (auto_tac (claset(), simpset() addsimps [hypnatrel_def, eq_commute])); +qed "hypnatrel_sym"; Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel"; @@ -950,7 +950,7 @@ Goalw [SHNat_def] "[| EX x. x: P; P <= Nats |] ==> EX Q. P = hypnat_of_nat ` Q"; -by (Best_tac 1); +by (Blast_tac 1); qed "SHNat_hypnat_of_nat_image"; Goalw [SHNat_def] @@ -1215,6 +1215,7 @@ Embedding of the hypernaturals into the hyperreal --------------------------------------------------------------*) +(*WARNING: FRAGILE!*) Goal "(Ya : hyprel ``{%n. f(n)}) = \ \ ({n. f n = Ya n} : FreeUltrafilterNat)"; by Auto_tac; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HyperOrd.thy --- a/src/HOL/Hyperreal/HyperOrd.thy Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/HyperOrd.thy Wed Dec 17 16:23:52 2003 +0100 @@ -7,21 +7,16 @@ theory HyperOrd = HyperDef: +defs (overloaded) + hrabs_def: "abs (r::hypreal) == (if 0 \ r then r else -r)" -method_setup fuf = {* - Method.ctxt_args (fn ctxt => - Method.METHOD (fn facts => - fuf_tac (Classical.get_local_claset ctxt, - Simplifier.get_local_simpset ctxt) 1)) *} - "free ultrafilter tactic" -method_setup ultra = {* - Method.ctxt_args (fn ctxt => - Method.METHOD (fn facts => - ultra_tac (Classical.get_local_claset ctxt, - Simplifier.get_local_simpset ctxt) 1)) *} - "ultrafilter tactic" - +lemma hypreal_hrabs: + "abs (Abs_hypreal (hyprel `` {X})) = + Abs_hypreal(hyprel `` {%n. abs (X n)})" +apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus) +apply (ultra, arith)+ +done instance hypreal :: order by (intro_classes, @@ -344,8 +339,7 @@ Existence of infinite hyperreal number ----------------------------------------------------------------------------*) -lemma Rep_hypreal_omega: "Rep_hypreal(omega) : hypreal" - +lemma Rep_hypreal_omega: "Rep_hypreal(omega) \ hypreal" apply (unfold omega_def) apply (rule Rep_hypreal) done @@ -355,19 +349,19 @@ (* a few lemmas first *) lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | - (EX y. {n::nat. x = real n} = {y})" + (\y. {n::nat. x = real n} = {y})" by (force dest: inj_real_of_nat [THEN injD]) lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) lemma not_ex_hypreal_of_real_eq_omega: - "~ (EX x. hypreal_of_real x = omega)" + "~ (\x. hypreal_of_real x = omega)" apply (unfold omega_def hypreal_of_real_def) apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) done -lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x ~= omega" +lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \ omega" by (cut_tac not_ex_hypreal_of_real_eq_omega, auto) (* existence of infinitesimal number also not *) @@ -377,7 +371,7 @@ by (rule inj_real_of_nat [THEN injD], simp) lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} | - (EX y. {n::nat. x = inverse(real(Suc n))} = {y})" + (\y. {n::nat. x = inverse(real(Suc n))} = {y})" apply (auto simp add: inj_real_of_nat [THEN inj_eq]) done @@ -385,15 +379,15 @@ by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) lemma not_ex_hypreal_of_real_eq_epsilon: - "~ (EX x. hypreal_of_real x = epsilon)" + "~ (\x. hypreal_of_real x = epsilon)" apply (unfold epsilon_def hypreal_of_real_def) apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite]) done -lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x ~= epsilon" +lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \ epsilon" by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto) -lemma hypreal_epsilon_not_zero: "epsilon ~= 0" +lemma hypreal_epsilon_not_zero: "epsilon \ 0" by (unfold epsilon_def hypreal_zero_def, auto) lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" @@ -470,9 +464,20 @@ lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0" by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero) +(*TO BE DELETED*) +ML +{* +val hypreal_add_ac = thms"hypreal_add_ac"; +val hypreal_mult_ac = thms"hypreal_mult_ac"; + +val hypreal_less_irrefl = thm"hypreal_less_irrefl"; +*} ML {* +val hrabs_def = thm "hrabs_def"; +val hypreal_hrabs = thm "hypreal_hrabs"; + val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21"; val hypreal_add_cancel_end = thm"hypreal_add_cancel_end"; val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq"; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/HyperPow.ML --- a/src/HOL/Hyperreal/HyperPow.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/HyperPow.ML Wed Dec 17 16:23:52 2003 +0100 @@ -252,7 +252,7 @@ Goalw [congruent_def] "congruent hyprel \ \ (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"; -by (safe_tac (claset() addSIs [ext])); +by (auto_tac (claset() addSIs [ext], simpset())); by (ALLGOALS(Fuf_tac)); qed "hyperpow_congruent"; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Wed Dec 17 16:23:52 2003 +0100 @@ -223,19 +223,17 @@ by (dtac lemma_skolemize_LIM2 1); by Safe_tac; by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1); -by (asm_full_simp_tac - (simpset() addsimps [starfun, hypreal_minus, - hypreal_of_real_def,hypreal_add]) 1); -by Safe_tac; +by (auto_tac + (claset(), + simpset() addsimps [starfun, hypreal_minus, + hypreal_of_real_def,hypreal_add])); by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1); by (asm_full_simp_tac (simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def, hypreal_minus, hypreal_add]) 1); by (Blast_tac 1); -by (rotate_tac 2 1); -by (dres_inst_tac [("x","r")] spec 1); -by (Clarify_tac 1); +by (dtac spec 1 THEN dtac mp 1 THEN assume_tac 1); by (dtac FreeUltrafilterNat_all 1); by (Ultra_tac 1); qed "NSLIM_LIM"; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/NSA.ML --- a/src/HOL/Hyperreal/NSA.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/NSA.ML Wed Dec 17 16:23:52 2003 +0100 @@ -1967,8 +1967,6 @@ by (dres_inst_tac [("x","u")] spec 1 THEN REPEAT(dtac FreeUltrafilterNat_Compl_mem 1)); by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); - - by (asm_full_simp_tac (simpset() addsimps [lemma_Compl_eq, lemma_Compl_eq2,lemma_Int_eq1]) 1); by (auto_tac (claset() addDs [FreeUltrafilterNat_const_Finite], diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/SEQ.ML --- a/src/HOL/Hyperreal/SEQ.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/SEQ.ML Wed Dec 17 16:23:52 2003 +0100 @@ -127,6 +127,7 @@ mem_infmal_iff RS sym,hypreal_of_real_def, hypreal_minus,hypreal_add, Infinitesimal_FreeUltrafilterNat_iff])); +by (rename_tac "Y" 1); by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1); @@ -814,6 +815,7 @@ by (dtac (mem_infmal_iff RS iffD2) 1); by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_add,Infinitesimal_FreeUltrafilterNat_iff])); +by (rename_tac "Y" 1); by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac); by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); by (dtac (CLAIM "{n. X (f n) + - X (fa n) = Y n} Int \ diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/Star.ML --- a/src/HOL/Hyperreal/Star.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/Star.ML Wed Dec 17 16:23:52 2003 +0100 @@ -193,7 +193,7 @@ -----------------------------------------------------------------------*) Goalw [congruent_def] "congruent hyprel (%X. hyprel``{%n. f (X n)})"; -by Safe_tac; +by Auto_tac; by (ALLGOALS(Fuf_tac)); qed "starfun_congruent"; @@ -407,7 +407,8 @@ "( *f* f) x : *s* A ==> x : *s* {x. f x : A}"; by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); by (auto_tac (claset(),simpset() addsimps [starfun])); -by (dres_inst_tac [("x","%n. f (Xa n)")] bspec 1); +by (rename_tac "X" 1); +by (dres_inst_tac [("x","%n. f (X n)")] bspec 1); by (Auto_tac THEN Fuf_tac 1); qed "starfun_mem_starset"; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/Hyperreal/fuf.ML --- a/src/HOL/Hyperreal/fuf.ML Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/Hyperreal/fuf.ML Wed Dec 17 16:23:52 2003 +0100 @@ -9,6 +9,11 @@ finite intersection property. *) +val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty"; +val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset"; +val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem"; +val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int"; + local exception FUFempty; diff -r e616f4bda3a2 -r 0b5c0b0a3eba src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 16 23:24:17 2003 +0100 +++ b/src/HOL/IsaMakefile Wed Dec 17 16:23:52 2003 +0100 @@ -151,7 +151,7 @@ Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\ Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\ Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\ - Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy Hyperreal/HyperDef.ML\ + Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \ Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\ Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\ Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\