converted Hyperreal/HyperDef to Isar script
authorpaulson
Wed Dec 17 16:23:52 2003 +0100 (2003-12-17)
changeset 142990b5c0b0a3eba
parent 14298 e616f4bda3a2
child 14300 bf8b8c9425c3
converted Hyperreal/HyperDef to Isar script
src/HOL/Complex/NSCA.ML
src/HOL/Complex/NSComplex.ML
src/HOL/Hyperreal/HLog.ML
src/HOL/Hyperreal/HRealAbs.ML
src/HOL/Hyperreal/HRealAbs.thy
src/HOL/Hyperreal/HyperDef.ML
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Hyperreal/HyperOrd.thy
src/HOL/Hyperreal/HyperPow.ML
src/HOL/Hyperreal/Lim.ML
src/HOL/Hyperreal/NSA.ML
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/Star.ML
src/HOL/Hyperreal/fuf.ML
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Complex/NSCA.ML	Tue Dec 16 23:24:17 2003 +0100
     1.2 +++ b/src/HOL/Complex/NSCA.ML	Wed Dec 17 16:23:52 2003 +0100
     1.3 @@ -785,12 +785,13 @@
     1.4      Infinitesimal_FreeUltrafilterNat_iff2]));
     1.5  by (dres_inst_tac [("x","m")] spec 1);
     1.6  by (Ultra_tac 1);
     1.7 +by (rename_tac "Z x" 1);
     1.8  by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
     1.9  by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    1.10  by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
    1.11      complex_mod] delsimps [realpow_Suc]));
    1.12  by (rtac order_le_less_trans 1 THEN assume_tac 2);
    1.13 -by (dres_inst_tac [("t","Ya x")] sym 1);
    1.14 +by (dres_inst_tac [("t","Z x")] sym 1);
    1.15  by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc]));
    1.16  qed "hcomplex_capproxD1";
    1.17  
    1.18 @@ -805,12 +806,13 @@
    1.19      Infinitesimal_FreeUltrafilterNat_iff2]));
    1.20  by (dres_inst_tac [("x","m")] spec 1);
    1.21  by (Ultra_tac 1);
    1.22 +by (rename_tac "Z x" 1);
    1.23  by (res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.24  by (res_inst_tac [("z","Y x")] eq_Abs_complex 1);
    1.25  by (auto_tac (claset(),simpset() addsimps [complex_minus,complex_add,
    1.26      complex_mod] delsimps [realpow_Suc]));
    1.27  by (rtac order_le_less_trans 1 THEN assume_tac 2);
    1.28 -by (dres_inst_tac [("t","Ya x")] sym 1);
    1.29 +by (dres_inst_tac [("t","Z x")] sym 1);
    1.30  by (auto_tac (claset(),simpset() addsimps [abs_eqI1] delsimps [realpow_Suc]));
    1.31  qed "hcomplex_capproxD2";
    1.32  
    1.33 @@ -894,13 +896,14 @@
    1.34  \     |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : CFinite";
    1.35  by (auto_tac (claset(),simpset() addsimps [CFinite_hcmod_iff,
    1.36      hcmod,HFinite_FreeUltrafilterNat_iff]));
    1.37 +by (rename_tac "Y Z u v" 1);
    1.38  by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
    1.39 -by (res_inst_tac [("x","2*(u + ua)")] exI 1);
    1.40 +by (res_inst_tac [("x","2*(u + v)")] exI 1);
    1.41  by (Ultra_tac 1);
    1.42  by (dtac sym 1 THEN res_inst_tac [("z","X x")] eq_Abs_complex 1);
    1.43  by (auto_tac (claset(),simpset() addsimps [complex_mod,two_eq_Suc_Suc] delsimps [realpow_Suc]));
    1.44  by (subgoal_tac "0 < u" 1 THEN arith_tac 2);
    1.45 -by (subgoal_tac "0 < ua" 1 THEN arith_tac 2);
    1.46 +by (subgoal_tac "0 < v" 1 THEN arith_tac 2);
    1.47  by (rtac (realpow_two_abs RS subst) 1);
    1.48  by (res_inst_tac [("x1","Y x")] (realpow_two_abs RS subst) 1);
    1.49  by (simp_tac (simpset() addsimps [two_eq_Suc_Suc RS sym]) 1);
     2.1 --- a/src/HOL/Complex/NSComplex.ML	Tue Dec 16 23:24:17 2003 +0100
     2.2 +++ b/src/HOL/Complex/NSComplex.ML	Wed Dec 17 16:23:52 2003 +0100
     2.3 @@ -36,9 +36,9 @@
     2.4  by (Auto_tac);
     2.5  qed "hcomplexrel_refl";
     2.6  
     2.7 -Goalw [hcomplexrel_def] "(x,y): hcomplexrel --> (y,x):hcomplexrel";
     2.8 -by (auto_tac (claset() addIs [lemma_perm RS subst],simpset()));
     2.9 -qed_spec_mp "hcomplexrel_sym";
    2.10 +Goalw [hcomplexrel_def] "(x,y): hcomplexrel ==> (y,x):hcomplexrel";
    2.11 +by (auto_tac (claset(), simpset() addsimps [eq_commute]));
    2.12 +qed "hcomplexrel_sym";
    2.13  
    2.14  Goalw [hcomplexrel_def]
    2.15        "(x,y): hcomplexrel --> (y,z):hcomplexrel --> (x,z):hcomplexrel";
    2.16 @@ -659,7 +659,8 @@
    2.17    "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) = \
    2.18  \     Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})";
    2.19  by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
    2.20 -by (Auto_tac THEN Ultra_tac 1);
    2.21 +by Auto_tac;
    2.22 +by (Ultra_tac 1);
    2.23  qed "hcomplex_of_hypreal";
    2.24  
    2.25  Goal "inj hcomplex_of_hypreal";
    2.26 @@ -711,8 +712,8 @@
    2.27  
    2.28  Goalw [hcomplex_divide_def]
    2.29    "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)";
    2.30 -by (hypreal_div_undefined_case_tac "y=0" 1);
    2.31 -by (simp_tac (simpset() addsimps [rename_numerals HYPREAL_DIVISION_BY_ZERO,
    2.32 +by (case_tac "y=0" 1);
    2.33 +by (asm_simp_tac (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO,HYPREAL_INVERSE_ZERO,
    2.34      HCOMPLEX_INVERSE_ZERO]) 1);
    2.35  by (auto_tac (claset(),simpset() addsimps [hcomplex_of_hypreal_mult,
    2.36      hcomplex_of_hypreal_inverse RS sym]));
    2.37 @@ -1592,7 +1593,8 @@
    2.38    "hcis (Abs_hypreal(hyprel `` {%n. X n})) = \
    2.39  \     Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})";
    2.40  by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1);
    2.41 -by (Auto_tac THEN Ultra_tac 1);
    2.42 +by Auto_tac;
    2.43 +by (Ultra_tac 1);
    2.44  qed "hcis";
    2.45  
    2.46  Goal 
     3.1 --- a/src/HOL/Hyperreal/HLog.ML	Tue Dec 16 23:24:17 2003 +0100
     3.2 +++ b/src/HOL/Hyperreal/HLog.ML	Wed Dec 17 16:23:52 2003 +0100
     3.3 @@ -122,7 +122,8 @@
     3.4       "hlog (Abs_hypreal(hyprel `` {X})) (Abs_hypreal(hyprel `` {Y})) = \
     3.5  \     Abs_hypreal(hyprel `` {%n. log (X n) (Y n)})";
     3.6  by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
     3.7 -by (Auto_tac THEN Ultra_tac 1);
     3.8 +by Auto_tac;
     3.9 +by (Ultra_tac 1);
    3.10  qed "hlog";
    3.11  
    3.12  Goal "( *f* ln) x = hlog (( *f* exp) 1) x";
     4.1 --- a/src/HOL/Hyperreal/HRealAbs.ML	Tue Dec 16 23:24:17 2003 +0100
     4.2 +++ b/src/HOL/Hyperreal/HRealAbs.ML	Wed Dec 17 16:23:52 2003 +0100
     4.3 @@ -18,15 +18,6 @@
     4.4  qed "hrabs_number_of";
     4.5  Addsimps [hrabs_number_of];
     4.6  
     4.7 -Goalw [hrabs_def]
     4.8 -     "abs (Abs_hypreal (hyprel `` {X})) = \
     4.9 -\     Abs_hypreal(hyprel `` {%n. abs (X n)})";
    4.10 -by (auto_tac (claset(),
    4.11 -              simpset_of HyperDef.thy 
    4.12 -                  addsimps [hypreal_zero_def, hypreal_le,hypreal_minus]));
    4.13 -by (ALLGOALS(Ultra_tac THEN' arith_tac ));
    4.14 -qed "hypreal_hrabs";
    4.15 -
    4.16  (*------------------------------------------------------------
    4.17     Properties of the absolute value function over the reals
    4.18     (adapted version of previously proved theorems about abs)
     5.1 --- a/src/HOL/Hyperreal/HRealAbs.thy	Tue Dec 16 23:24:17 2003 +0100
     5.2 +++ b/src/HOL/Hyperreal/HRealAbs.thy	Wed Dec 17 16:23:52 2003 +0100
     5.3 @@ -6,9 +6,6 @@
     5.4  
     5.5  HRealAbs = HyperArith + RealArith + 
     5.6  
     5.7 -defs
     5.8 -    hrabs_def "abs r  == if (0::hypreal) <=r then r else -r" 
     5.9 -
    5.10  constdefs
    5.11    
    5.12    hypreal_of_nat :: nat => hypreal                   
     6.1 --- a/src/HOL/Hyperreal/HyperDef.ML	Tue Dec 16 23:24:17 2003 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,1257 +0,0 @@
     6.4 -(*  Title       : HOL/Real/Hyperreal/Hyper.ML
     6.5 -    ID          : $Id$
     6.6 -    Author      : Jacques D. Fleuriot
     6.7 -    Copyright   : 1998  University of Cambridge
     6.8 -    Description : Ultrapower construction of hyperreals
     6.9 -*) 
    6.10 -
    6.11 -(*------------------------------------------------------------------------
    6.12 -             Proof that the set of naturals is not finite
    6.13 - ------------------------------------------------------------------------*)
    6.14 -
    6.15 -(*** based on James' proof that the set of naturals is not finite ***)
    6.16 -Goal "finite (A::nat set) --> (EX n. ALL m. Suc (n + m) ~: A)";
    6.17 -by (rtac impI 1);
    6.18 -by (eres_inst_tac [("F","A")] finite_induct 1);
    6.19 -by (Blast_tac 1 THEN etac exE 1);
    6.20 -by (res_inst_tac [("x","n + x")] exI 1);
    6.21 -by (rtac allI 1 THEN eres_inst_tac [("x","x + m")] allE 1);
    6.22 -by (auto_tac (claset(), simpset() addsimps add_ac));
    6.23 -by (auto_tac (claset(),
    6.24 -	      simpset() addsimps [add_assoc RS sym,
    6.25 -				  less_add_Suc2 RS less_not_refl2]));
    6.26 -qed_spec_mp "finite_exhausts";
    6.27 -
    6.28 -Goal "finite (A :: nat set) --> (EX n. n ~:A)";
    6.29 -by (rtac impI 1 THEN dtac finite_exhausts 1);
    6.30 -by (Blast_tac 1);
    6.31 -qed_spec_mp "finite_not_covers";
    6.32 -
    6.33 -Goal "~ finite(UNIV:: nat set)";
    6.34 -by (fast_tac (claset() addSDs [finite_exhausts]) 1);
    6.35 -qed "not_finite_nat";
    6.36 -
    6.37 -(*------------------------------------------------------------------------
    6.38 -   Existence of free ultrafilter over the naturals and proof of various 
    6.39 -   properties of the FreeUltrafilterNat- an arbitrary free ultrafilter
    6.40 - ------------------------------------------------------------------------*)
    6.41 -
    6.42 -Goal "EX U. U: FreeUltrafilter (UNIV::nat set)";
    6.43 -by (rtac (not_finite_nat RS FreeUltrafilter_Ex) 1);
    6.44 -qed "FreeUltrafilterNat_Ex";
    6.45 -
    6.46 -Goalw [FreeUltrafilterNat_def] 
    6.47 -     "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)";
    6.48 -by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    6.49 -by (rtac someI2 1 THEN ALLGOALS(assume_tac));
    6.50 -qed "FreeUltrafilterNat_mem";
    6.51 -Addsimps [FreeUltrafilterNat_mem];
    6.52 -
    6.53 -Goalw [FreeUltrafilterNat_def] "finite x ==> x ~: FreeUltrafilterNat";
    6.54 -by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    6.55 -by (rtac someI2 1 THEN assume_tac 1);
    6.56 -by (blast_tac (claset() addDs [mem_FreeUltrafiltersetD1]) 1);
    6.57 -qed "FreeUltrafilterNat_finite";
    6.58 -
    6.59 -Goal "x: FreeUltrafilterNat ==> ~ finite x";
    6.60 -by (blast_tac (claset() addDs [FreeUltrafilterNat_finite]) 1);
    6.61 -qed "FreeUltrafilterNat_not_finite";
    6.62 -
    6.63 -Goalw [FreeUltrafilterNat_def] "{} ~: FreeUltrafilterNat";
    6.64 -by (rtac (FreeUltrafilterNat_Ex RS exE) 1);
    6.65 -by (rtac someI2 1 THEN assume_tac 1);
    6.66 -by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    6.67 -			       Ultrafilter_Filter,Filter_empty_not_mem]) 1);
    6.68 -qed "FreeUltrafilterNat_empty";
    6.69 -Addsimps [FreeUltrafilterNat_empty];
    6.70 -
    6.71 -Goal "[| X: FreeUltrafilterNat;  Y: FreeUltrafilterNat |]  \
    6.72 -\     ==> X Int Y : FreeUltrafilterNat";
    6.73 -by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
    6.74 -by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    6.75 -			       Ultrafilter_Filter,mem_FiltersetD1]) 1);
    6.76 -qed "FreeUltrafilterNat_Int";
    6.77 -
    6.78 -Goal "[| X: FreeUltrafilterNat;  X <= Y |] \
    6.79 -\     ==> Y : FreeUltrafilterNat";
    6.80 -by (cut_facts_tac [FreeUltrafilterNat_mem] 1);
    6.81 -by (blast_tac (claset() addDs [FreeUltrafilter_Ultrafilter,
    6.82 -			       Ultrafilter_Filter,mem_FiltersetD2]) 1);
    6.83 -qed "FreeUltrafilterNat_subset";
    6.84 -
    6.85 -Goal "X: FreeUltrafilterNat ==> -X ~: FreeUltrafilterNat";
    6.86 -by (Step_tac 1);
    6.87 -by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
    6.88 -by Auto_tac;
    6.89 -qed "FreeUltrafilterNat_Compl";
    6.90 -
    6.91 -Goal "X~: FreeUltrafilterNat ==> -X : FreeUltrafilterNat";
    6.92 -by (cut_facts_tac [FreeUltrafilterNat_mem RS (FreeUltrafilter_iff RS iffD1)] 1);
    6.93 -by (Step_tac 1 THEN dres_inst_tac [("x","X")] bspec 1);
    6.94 -by (auto_tac (claset(), simpset() addsimps [UNIV_diff_Compl]));
    6.95 -qed "FreeUltrafilterNat_Compl_mem";
    6.96 -
    6.97 -Goal "(X ~: FreeUltrafilterNat) = (-X: FreeUltrafilterNat)";
    6.98 -by (blast_tac (claset() addDs [FreeUltrafilterNat_Compl,
    6.99 -			       FreeUltrafilterNat_Compl_mem]) 1);
   6.100 -qed "FreeUltrafilterNat_Compl_iff1";
   6.101 -
   6.102 -Goal "(X: FreeUltrafilterNat) = (-X ~: FreeUltrafilterNat)";
   6.103 -by (auto_tac (claset(),
   6.104 -	      simpset() addsimps [FreeUltrafilterNat_Compl_iff1 RS sym]));
   6.105 -qed "FreeUltrafilterNat_Compl_iff2";
   6.106 -
   6.107 -Goal "(UNIV::nat set) : FreeUltrafilterNat";
   6.108 -by (rtac (FreeUltrafilterNat_mem RS FreeUltrafilter_Ultrafilter RS 
   6.109 -          Ultrafilter_Filter RS mem_FiltersetD4) 1);
   6.110 -qed "FreeUltrafilterNat_UNIV";
   6.111 -Addsimps [FreeUltrafilterNat_UNIV];
   6.112 -
   6.113 -Goal "UNIV : FreeUltrafilterNat";
   6.114 -by Auto_tac;
   6.115 -qed "FreeUltrafilterNat_Nat_set";
   6.116 -Addsimps [FreeUltrafilterNat_Nat_set];
   6.117 -
   6.118 -Goal "{n. P(n) = P(n)} : FreeUltrafilterNat";
   6.119 -by (Simp_tac 1);
   6.120 -qed "FreeUltrafilterNat_Nat_set_refl";
   6.121 -AddIs [FreeUltrafilterNat_Nat_set_refl];
   6.122 -
   6.123 -Goal "{n::nat. P} : FreeUltrafilterNat ==> P";
   6.124 -by (rtac ccontr 1);
   6.125 -by (Asm_full_simp_tac 1);
   6.126 -qed "FreeUltrafilterNat_P";
   6.127 -
   6.128 -Goal "{n. P(n)} : FreeUltrafilterNat ==> EX n. P(n)";
   6.129 -by (rtac ccontr 1);
   6.130 -by (Asm_full_simp_tac 1);
   6.131 -qed "FreeUltrafilterNat_Ex_P";
   6.132 -
   6.133 -Goal "ALL n. P(n) ==> {n. P(n)} : FreeUltrafilterNat";
   6.134 -by (auto_tac (claset() addIs [FreeUltrafilterNat_Nat_set], simpset()));
   6.135 -qed "FreeUltrafilterNat_all";
   6.136 -
   6.137 -(*-------------------------------------------------------
   6.138 -     Define and use Ultrafilter tactics
   6.139 - -------------------------------------------------------*)
   6.140 -use "fuf.ML";
   6.141 -
   6.142 -(*-------------------------------------------------------
   6.143 -  Now prove one further property of our free ultrafilter
   6.144 - -------------------------------------------------------*)
   6.145 -Goal "X Un Y: FreeUltrafilterNat \
   6.146 -\     ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat";
   6.147 -by Auto_tac;
   6.148 -by (Ultra_tac 1);
   6.149 -qed "FreeUltrafilterNat_Un";
   6.150 -
   6.151 -(*-------------------------------------------------------
   6.152 -   Properties of hyprel
   6.153 - -------------------------------------------------------*)
   6.154 -
   6.155 -(** Proving that hyprel is an equivalence relation **)
   6.156 -(** Natural deduction for hyprel **)
   6.157 -
   6.158 -Goalw [hyprel_def]
   6.159 -   "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)";
   6.160 -by (Fast_tac 1);
   6.161 -qed "hyprel_iff";
   6.162 -
   6.163 -Goalw [hyprel_def] 
   6.164 -     "{n. X n = Y n}: FreeUltrafilterNat  ==> (X,Y): hyprel";
   6.165 -by (Fast_tac 1);
   6.166 -qed "hyprelI";
   6.167 -
   6.168 -Goalw [hyprel_def]
   6.169 -  "p: hyprel --> (EX X Y. \
   6.170 -\                 p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
   6.171 -by (Fast_tac 1);
   6.172 -qed "hyprelE_lemma";
   6.173 -
   6.174 -val [major,minor] = goal (the_context ())
   6.175 -  "[| p: hyprel;  \
   6.176 -\     !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\
   6.177 -\                    |] ==> Q |] ==> Q";
   6.178 -by (cut_facts_tac [major RS (hyprelE_lemma RS mp)] 1);
   6.179 -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
   6.180 -qed "hyprelE";
   6.181 -
   6.182 -AddSIs [hyprelI];
   6.183 -AddSEs [hyprelE];
   6.184 -
   6.185 -Goalw [hyprel_def] "(x,x): hyprel";
   6.186 -by (auto_tac (claset(),
   6.187 -              simpset() addsimps [FreeUltrafilterNat_Nat_set]));
   6.188 -qed "hyprel_refl";
   6.189 -
   6.190 -Goal "{n. X n = Y n} = {n. Y n = X n}";
   6.191 -by Auto_tac;
   6.192 -qed "lemma_perm";
   6.193 -
   6.194 -Goalw [hyprel_def] "(x,y): hyprel --> (y,x):hyprel";
   6.195 -by (auto_tac (claset() addIs [lemma_perm RS subst], simpset()));
   6.196 -qed_spec_mp "hyprel_sym";
   6.197 -
   6.198 -Goalw [hyprel_def]
   6.199 -      "(x,y): hyprel --> (y,z):hyprel --> (x,z):hyprel";
   6.200 -by Auto_tac;
   6.201 -by (Ultra_tac 1);
   6.202 -qed_spec_mp "hyprel_trans";
   6.203 -
   6.204 -Goalw [equiv_def, refl_def, sym_def, trans_def] "equiv UNIV hyprel";
   6.205 -by (auto_tac (claset() addSIs [hyprel_refl] 
   6.206 -                       addSEs [hyprel_sym,hyprel_trans] 
   6.207 -                       delrules [hyprelI,hyprelE],
   6.208 -	      simpset() addsimps [FreeUltrafilterNat_Nat_set]));
   6.209 -qed "equiv_hyprel";
   6.210 -
   6.211 -(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) : hyprel) *)
   6.212 -bind_thm ("equiv_hyprel_iff",
   6.213 -    	  [equiv_hyprel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
   6.214 -
   6.215 -Goalw  [hypreal_def,hyprel_def,quotient_def] "hyprel``{x}:hypreal";
   6.216 -by (Blast_tac 1);
   6.217 -qed "hyprel_in_hypreal";
   6.218 -
   6.219 -Goal "inj_on Abs_hypreal hypreal";
   6.220 -by (rtac inj_on_inverseI 1);
   6.221 -by (etac Abs_hypreal_inverse 1);
   6.222 -qed "inj_on_Abs_hypreal";
   6.223 -
   6.224 -Addsimps [equiv_hyprel_iff,inj_on_Abs_hypreal RS inj_on_iff,
   6.225 -          hyprel_iff, hyprel_in_hypreal, Abs_hypreal_inverse];
   6.226 -
   6.227 -Addsimps [equiv_hyprel RS eq_equiv_class_iff];
   6.228 -bind_thm ("eq_hyprelD", equiv_hyprel RSN (2,eq_equiv_class));
   6.229 -
   6.230 -Goal "inj(Rep_hypreal)";
   6.231 -by (rtac inj_inverseI 1);
   6.232 -by (rtac Rep_hypreal_inverse 1);
   6.233 -qed "inj_Rep_hypreal";
   6.234 -
   6.235 -Goalw [hyprel_def] "x: hyprel `` {x}";
   6.236 -by (Step_tac 1);
   6.237 -by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
   6.238 -qed "lemma_hyprel_refl";
   6.239 -
   6.240 -Addsimps [lemma_hyprel_refl];
   6.241 -
   6.242 -Goalw [hypreal_def] "{} ~: hypreal";
   6.243 -by (auto_tac (claset() addSEs [quotientE], simpset()));
   6.244 -qed "hypreal_empty_not_mem";
   6.245 -
   6.246 -Addsimps [hypreal_empty_not_mem];
   6.247 -
   6.248 -Goal "Rep_hypreal x ~= {}";
   6.249 -by (cut_inst_tac [("x","x")] Rep_hypreal 1);
   6.250 -by Auto_tac;
   6.251 -qed "Rep_hypreal_nonempty";
   6.252 -
   6.253 -Addsimps [Rep_hypreal_nonempty];
   6.254 -
   6.255 -(*------------------------------------------------------------------------
   6.256 -   hypreal_of_real: the injection from real to hypreal
   6.257 - ------------------------------------------------------------------------*)
   6.258 -
   6.259 -Goal "inj(hypreal_of_real)";
   6.260 -by (rtac injI 1);
   6.261 -by (rewtac hypreal_of_real_def);
   6.262 -by (dtac (inj_on_Abs_hypreal RS inj_onD) 1);
   6.263 -by (REPEAT (rtac hyprel_in_hypreal 1));
   6.264 -by (dtac eq_equiv_class 1);
   6.265 -by (rtac equiv_hyprel 1);
   6.266 -by (Fast_tac 1);
   6.267 -by (rtac ccontr 1);
   6.268 -by Auto_tac;
   6.269 -qed "inj_hypreal_of_real";
   6.270 -
   6.271 -val [prem] = goal (the_context ())
   6.272 -    "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P";
   6.273 -by (res_inst_tac [("x1","z")] 
   6.274 -    (rewrite_rule [hypreal_def] Rep_hypreal RS quotientE) 1);
   6.275 -by (dres_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   6.276 -by (res_inst_tac [("x","x")] prem 1);
   6.277 -by (asm_full_simp_tac (simpset() addsimps [Rep_hypreal_inverse]) 1);
   6.278 -qed "eq_Abs_hypreal";
   6.279 -
   6.280 -(**** hypreal_minus: additive inverse on hypreal ****)
   6.281 -
   6.282 -Goalw [congruent_def]
   6.283 -  "congruent hyprel (%X. hyprel``{%n. - (X n)})";
   6.284 -by Safe_tac;
   6.285 -by (ALLGOALS Ultra_tac);
   6.286 -qed "hypreal_minus_congruent";
   6.287 -
   6.288 -Goalw [hypreal_minus_def]
   6.289 -   "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})";
   6.290 -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   6.291 -by (simp_tac (simpset() addsimps 
   6.292 -      [hyprel_in_hypreal RS Abs_hypreal_inverse,
   6.293 -       [equiv_hyprel, hypreal_minus_congruent] MRS UN_equiv_class]) 1);
   6.294 -qed "hypreal_minus";
   6.295 -
   6.296 -Goal "- (- z) = (z::hypreal)";
   6.297 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.298 -by (asm_simp_tac (simpset() addsimps [hypreal_minus]) 1);
   6.299 -qed "hypreal_minus_minus";
   6.300 -
   6.301 -Addsimps [hypreal_minus_minus];
   6.302 -
   6.303 -Goal "inj(%r::hypreal. -r)";
   6.304 -by (rtac injI 1);
   6.305 -by (dres_inst_tac [("f","uminus")] arg_cong 1);
   6.306 -by (asm_full_simp_tac (simpset() addsimps [hypreal_minus_minus]) 1);
   6.307 -qed "inj_hypreal_minus";
   6.308 -
   6.309 -Goalw [hypreal_zero_def] "- 0 = (0::hypreal)";
   6.310 -by (simp_tac (simpset() addsimps [hypreal_minus]) 1);
   6.311 -qed "hypreal_minus_zero";
   6.312 -Addsimps [hypreal_minus_zero];
   6.313 -
   6.314 -Goal "(-x = 0) = (x = (0::hypreal))"; 
   6.315 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.316 -by (auto_tac (claset(), simpset() addsimps [hypreal_zero_def, hypreal_minus]));
   6.317 -qed "hypreal_minus_zero_iff";
   6.318 -Addsimps [hypreal_minus_zero_iff];
   6.319 -
   6.320 -
   6.321 -(**** hyperreal addition: hypreal_add  ****)
   6.322 -
   6.323 -Goalw [congruent2_def]
   6.324 -    "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})";
   6.325 -by Safe_tac;
   6.326 -by (ALLGOALS(Ultra_tac));
   6.327 -qed "hypreal_add_congruent2";
   6.328 -
   6.329 -Goalw [hypreal_add_def]
   6.330 -  "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) = \
   6.331 -\  Abs_hypreal(hyprel``{%n. X n + Y n})";
   6.332 -by (simp_tac (simpset() addsimps 
   6.333 -         [[equiv_hyprel, hypreal_add_congruent2] MRS UN_equiv_class2]) 1);
   6.334 -qed "hypreal_add";
   6.335 -
   6.336 -Goal "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) = \
   6.337 -\     Abs_hypreal(hyprel``{%n. X n - Y n})";
   6.338 -by (simp_tac (simpset() addsimps 
   6.339 -         [hypreal_diff_def, hypreal_minus,hypreal_add]) 1);
   6.340 -qed "hypreal_diff";
   6.341 -
   6.342 -Goal "(z::hypreal) + w = w + z";
   6.343 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.344 -by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   6.345 -by (asm_simp_tac (simpset() addsimps (real_add_ac @ [hypreal_add])) 1);
   6.346 -qed "hypreal_add_commute";
   6.347 -
   6.348 -Goal "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)";
   6.349 -by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   6.350 -by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   6.351 -by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   6.352 -by (asm_simp_tac (simpset() addsimps [hypreal_add, real_add_assoc]) 1);
   6.353 -qed "hypreal_add_assoc";
   6.354 -
   6.355 -(*For AC rewriting*)
   6.356 -Goal "(x::hypreal)+(y+z)=y+(x+z)";
   6.357 -by(rtac ([hypreal_add_assoc,hypreal_add_commute] MRS
   6.358 -         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
   6.359 -qed "hypreal_add_left_commute";
   6.360 -
   6.361 -(* hypreal addition is an AC operator *)
   6.362 -bind_thms ("hypreal_add_ac", [hypreal_add_assoc,hypreal_add_commute,
   6.363 -                      hypreal_add_left_commute]);
   6.364 -
   6.365 -Goalw [hypreal_zero_def] "(0::hypreal) + z = z";
   6.366 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.367 -by (asm_full_simp_tac (simpset() addsimps 
   6.368 -    [hypreal_add]) 1);
   6.369 -qed "hypreal_add_zero_left";
   6.370 -
   6.371 -Goal "z + (0::hypreal) = z";
   6.372 -by (simp_tac (simpset() addsimps 
   6.373 -    [hypreal_add_zero_left,hypreal_add_commute]) 1);
   6.374 -qed "hypreal_add_zero_right";
   6.375 -
   6.376 -Goalw [hypreal_zero_def] "z + -z = (0::hypreal)";
   6.377 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.378 -by (asm_full_simp_tac (simpset() addsimps [hypreal_minus, hypreal_add]) 1);
   6.379 -qed "hypreal_add_minus";
   6.380 -
   6.381 -Goal "-z + z = (0::hypreal)";
   6.382 -by (simp_tac (simpset() addsimps [hypreal_add_commute, hypreal_add_minus]) 1);
   6.383 -qed "hypreal_add_minus_left";
   6.384 -
   6.385 -Addsimps [hypreal_add_minus,hypreal_add_minus_left,
   6.386 -          hypreal_add_zero_left,hypreal_add_zero_right];
   6.387 -
   6.388 -Goal "EX y. (x::hypreal) + y = 0";
   6.389 -by (fast_tac (claset() addIs [hypreal_add_minus]) 1);
   6.390 -qed "hypreal_minus_ex";
   6.391 -
   6.392 -Goal "EX! y. (x::hypreal) + y = 0";
   6.393 -by (auto_tac (claset() addIs [hypreal_add_minus], simpset()));
   6.394 -by (dres_inst_tac [("f","%x. ya+x")] arg_cong 1);
   6.395 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   6.396 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   6.397 -qed "hypreal_minus_ex1";
   6.398 -
   6.399 -Goal "EX! y. y + (x::hypreal) = 0";
   6.400 -by (auto_tac (claset() addIs [hypreal_add_minus_left], simpset()));
   6.401 -by (dres_inst_tac [("f","%x. x+ya")] arg_cong 1);
   6.402 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc]) 1);
   6.403 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   6.404 -qed "hypreal_minus_left_ex1";
   6.405 -
   6.406 -Goal "x + y = (0::hypreal) ==> x = -y";
   6.407 -by (cut_inst_tac [("z","y")] hypreal_add_minus_left 1);
   6.408 -by (res_inst_tac [("x1","y")] (hypreal_minus_left_ex1 RS ex1E) 1);
   6.409 -by (Blast_tac 1);
   6.410 -qed "hypreal_add_minus_eq_minus";
   6.411 -
   6.412 -Goal "EX y::hypreal. x = -y";
   6.413 -by (cut_inst_tac [("x","x")] hypreal_minus_ex 1);
   6.414 -by (etac exE 1 THEN dtac hypreal_add_minus_eq_minus 1);
   6.415 -by (Fast_tac 1);
   6.416 -qed "hypreal_as_add_inverse_ex";
   6.417 -
   6.418 -Goal "-(x + (y::hypreal)) = -x + -y";
   6.419 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.420 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.421 -by (auto_tac (claset(),
   6.422 -              simpset() addsimps [hypreal_minus, hypreal_add,
   6.423 -                                  real_minus_add_distrib]));
   6.424 -qed "hypreal_minus_add_distrib";
   6.425 -Addsimps [hypreal_minus_add_distrib];
   6.426 -
   6.427 -Goal "-(y + -(x::hypreal)) = x + -y";
   6.428 -by (simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
   6.429 -qed "hypreal_minus_distrib1";
   6.430 -
   6.431 -Goal "((x::hypreal) + y = x + z) = (y = z)";
   6.432 -by (Step_tac 1);
   6.433 -by (dres_inst_tac [("f","%t.-x + t")] arg_cong 1);
   6.434 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   6.435 -qed "hypreal_add_left_cancel";
   6.436 -
   6.437 -Goal "(y + (x::hypreal)= z + x) = (y = z)";
   6.438 -by (simp_tac (simpset() addsimps [hypreal_add_commute,
   6.439 -                                  hypreal_add_left_cancel]) 1);
   6.440 -qed "hypreal_add_right_cancel";
   6.441 -
   6.442 -Goal "z + ((- z) + w) = (w::hypreal)";
   6.443 -by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   6.444 -qed "hypreal_add_minus_cancelA";
   6.445 -
   6.446 -Goal "(-z) + (z + w) = (w::hypreal)";
   6.447 -by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   6.448 -qed "hypreal_minus_add_cancelA";
   6.449 -
   6.450 -Addsimps [hypreal_add_minus_cancelA, hypreal_minus_add_cancelA];
   6.451 -
   6.452 -(**** hyperreal multiplication: hypreal_mult  ****)
   6.453 -
   6.454 -Goalw [congruent2_def]
   6.455 -    "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})";
   6.456 -by Safe_tac;
   6.457 -by (ALLGOALS(Ultra_tac));
   6.458 -qed "hypreal_mult_congruent2";
   6.459 -
   6.460 -Goalw [hypreal_mult_def]
   6.461 -  "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) = \
   6.462 -\  Abs_hypreal(hyprel``{%n. X n * Y n})";
   6.463 -by (simp_tac (simpset() addsimps 
   6.464 -      [[equiv_hyprel, hypreal_mult_congruent2] MRS UN_equiv_class2]) 1);
   6.465 -qed "hypreal_mult";
   6.466 -
   6.467 -Goal "(z::hypreal) * w = w * z";
   6.468 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.469 -by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   6.470 -by (asm_simp_tac (simpset() addsimps ([hypreal_mult] @ real_mult_ac)) 1);
   6.471 -qed "hypreal_mult_commute";
   6.472 -
   6.473 -Goal "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)";
   6.474 -by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   6.475 -by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   6.476 -by (res_inst_tac [("z","z3")] eq_Abs_hypreal 1);
   6.477 -by (asm_simp_tac (simpset() addsimps [hypreal_mult,real_mult_assoc]) 1);
   6.478 -qed "hypreal_mult_assoc";
   6.479 -
   6.480 -Goal "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)";
   6.481 -by(rtac ([hypreal_mult_assoc,hypreal_mult_commute] MRS
   6.482 -         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
   6.483 -qed "hypreal_mult_left_commute";
   6.484 -
   6.485 -(* hypreal multiplication is an AC operator *)
   6.486 -bind_thms ("hypreal_mult_ac", [hypreal_mult_assoc, hypreal_mult_commute, 
   6.487 -                       hypreal_mult_left_commute]);
   6.488 -
   6.489 -Goalw [hypreal_one_def] "(1::hypreal) * z = z";
   6.490 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.491 -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
   6.492 -qed "hypreal_mult_1";
   6.493 -Addsimps [hypreal_mult_1];
   6.494 -
   6.495 -Goal "z * (1::hypreal) = z";
   6.496 -by (simp_tac (simpset() addsimps [hypreal_mult_commute,
   6.497 -    hypreal_mult_1]) 1);
   6.498 -qed "hypreal_mult_1_right";
   6.499 -Addsimps [hypreal_mult_1_right];
   6.500 -
   6.501 -Goalw [hypreal_zero_def] "0 * z = (0::hypreal)";
   6.502 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.503 -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult]) 1);
   6.504 -qed "hypreal_mult_0";
   6.505 -Addsimps [hypreal_mult_0];
   6.506 -
   6.507 -Goal "z * 0 = (0::hypreal)";
   6.508 -by (simp_tac (simpset() addsimps [hypreal_mult_commute]) 1);
   6.509 -qed "hypreal_mult_0_right";
   6.510 -Addsimps [hypreal_mult_0_right];
   6.511 -
   6.512 -Goal "-(x * y) = -x * (y::hypreal)";
   6.513 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.514 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.515 -by (auto_tac (claset(),
   6.516 -	      simpset() addsimps [hypreal_minus, hypreal_mult] 
   6.517 -                                 @ real_mult_ac @ real_add_ac));
   6.518 -qed "hypreal_minus_mult_eq1";
   6.519 -
   6.520 -Goal "-(x * y) = (x::hypreal) * -y";
   6.521 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.522 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.523 -by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_mult] 
   6.524 -                                           @ real_mult_ac @ real_add_ac));
   6.525 -qed "hypreal_minus_mult_eq2";
   6.526 -
   6.527 -(*Pull negations out*)
   6.528 -Addsimps [hypreal_minus_mult_eq2 RS sym, hypreal_minus_mult_eq1 RS sym];
   6.529 -
   6.530 -Goal "(- (1::hypreal)) * z = -z";
   6.531 -by (Simp_tac 1);
   6.532 -qed "hypreal_mult_minus_1";
   6.533 -Addsimps [hypreal_mult_minus_1];
   6.534 -
   6.535 -Goal "z * (- (1::hypreal)) = -z";
   6.536 -by (stac hypreal_mult_commute 1);
   6.537 -by (Simp_tac 1);
   6.538 -qed "hypreal_mult_minus_1_right";
   6.539 -Addsimps [hypreal_mult_minus_1_right];
   6.540 -
   6.541 -Goal "(-x) * y = (x::hypreal) * -y";
   6.542 -by Auto_tac;
   6.543 -qed "hypreal_minus_mult_commute";
   6.544 -
   6.545 -(*-----------------------------------------------------------------------------
   6.546 -    A few more theorems
   6.547 - ----------------------------------------------------------------------------*)
   6.548 -Goal "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
   6.549 -by (asm_simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
   6.550 -qed "hypreal_add_assoc_cong";
   6.551 -
   6.552 -Goal "(z::hypreal) + (v + w) = v + (z + w)";
   6.553 -by (REPEAT (ares_tac [hypreal_add_commute RS hypreal_add_assoc_cong] 1));
   6.554 -qed "hypreal_add_assoc_swap";
   6.555 -
   6.556 -Goal "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)";
   6.557 -by (res_inst_tac [("z","z1")] eq_Abs_hypreal 1);
   6.558 -by (res_inst_tac [("z","z2")] eq_Abs_hypreal 1);
   6.559 -by (res_inst_tac [("z","w")] eq_Abs_hypreal 1);
   6.560 -by (asm_simp_tac (simpset() addsimps [hypreal_mult,hypreal_add,
   6.561 -     real_add_mult_distrib]) 1);
   6.562 -qed "hypreal_add_mult_distrib";
   6.563 -
   6.564 -val hypreal_mult_commute'= read_instantiate [("z","w")] hypreal_mult_commute;
   6.565 -
   6.566 -Goal "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)";
   6.567 -by (simp_tac (simpset() addsimps [hypreal_mult_commute',hypreal_add_mult_distrib]) 1);
   6.568 -qed "hypreal_add_mult_distrib2";
   6.569 -
   6.570 -
   6.571 -Goalw [hypreal_diff_def] "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)";
   6.572 -by (simp_tac (simpset() addsimps [hypreal_add_mult_distrib]) 1);
   6.573 -qed "hypreal_diff_mult_distrib";
   6.574 -
   6.575 -Goal "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)";
   6.576 -by (simp_tac (simpset() addsimps [hypreal_mult_commute', 
   6.577 -				  hypreal_diff_mult_distrib]) 1);
   6.578 -qed "hypreal_diff_mult_distrib2";
   6.579 -
   6.580 -(*** one and zero are distinct ***)
   6.581 -Goalw [hypreal_zero_def,hypreal_one_def] "0 ~= (1::hypreal)";
   6.582 -by (auto_tac (claset(), simpset() addsimps [real_zero_not_eq_one]));
   6.583 -qed "hypreal_zero_not_eq_one";
   6.584 -
   6.585 -
   6.586 -(**** multiplicative inverse on hypreal ****)
   6.587 -
   6.588 -Goalw [congruent_def]
   6.589 -  "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})";
   6.590 -by (Auto_tac THEN Ultra_tac 1);
   6.591 -qed "hypreal_inverse_congruent";
   6.592 -
   6.593 -Goalw [hypreal_inverse_def]
   6.594 -      "inverse (Abs_hypreal(hyprel``{%n. X n})) = \
   6.595 -\      Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})";
   6.596 -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
   6.597 -by (simp_tac (simpset() addsimps 
   6.598 -   [hyprel_in_hypreal RS Abs_hypreal_inverse,
   6.599 -    [equiv_hyprel, hypreal_inverse_congruent] MRS UN_equiv_class]) 1);
   6.600 -qed "hypreal_inverse";
   6.601 -
   6.602 -Goal "inverse 0 = (0::hypreal)";
   6.603 -by (simp_tac (simpset() addsimps [hypreal_inverse, hypreal_zero_def]) 1);
   6.604 -qed "HYPREAL_INVERSE_ZERO";
   6.605 -
   6.606 -Goal "a / (0::hypreal) = 0";
   6.607 -by (simp_tac
   6.608 -    (simpset() addsimps [hypreal_divide_def, HYPREAL_INVERSE_ZERO]) 1);
   6.609 -qed "HYPREAL_DIVISION_BY_ZERO";  (*NOT for adding to default simpset*)
   6.610 -
   6.611 -fun hypreal_div_undefined_case_tac s i =
   6.612 -  case_tac s i THEN 
   6.613 -  asm_simp_tac 
   6.614 -       (simpset() addsimps [HYPREAL_DIVISION_BY_ZERO, HYPREAL_INVERSE_ZERO]) i;
   6.615 -
   6.616 -Goal "inverse (inverse (z::hypreal)) = z";
   6.617 -by (hypreal_div_undefined_case_tac "z=0" 1);
   6.618 -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1);
   6.619 -by (asm_full_simp_tac (simpset() addsimps 
   6.620 -                       [hypreal_inverse, hypreal_zero_def]) 1);
   6.621 -qed "hypreal_inverse_inverse";
   6.622 -Addsimps [hypreal_inverse_inverse];
   6.623 -
   6.624 -Goalw [hypreal_one_def] "inverse((1::hypreal)) = (1::hypreal)";
   6.625 -by (full_simp_tac (simpset() addsimps [hypreal_inverse,
   6.626 -                                       real_zero_not_eq_one RS not_sym]) 1);
   6.627 -qed "hypreal_inverse_1";
   6.628 -Addsimps [hypreal_inverse_1];
   6.629 -
   6.630 -
   6.631 -(*** existence of inverse ***)
   6.632 -
   6.633 -Goalw [hypreal_one_def,hypreal_zero_def] 
   6.634 -     "x ~= 0 ==> x*inverse(x) = (1::hypreal)";
   6.635 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.636 -by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
   6.637 -by (dtac FreeUltrafilterNat_Compl_mem 1);
   6.638 -by (blast_tac (claset() addSIs [real_mult_inv_right,
   6.639 -    FreeUltrafilterNat_subset]) 1);
   6.640 -qed "hypreal_mult_inverse";
   6.641 -
   6.642 -Goal "x ~= 0 ==> inverse(x)*x = (1::hypreal)";
   6.643 -by (asm_simp_tac (simpset() addsimps [hypreal_mult_inverse,
   6.644 -				      hypreal_mult_commute]) 1);
   6.645 -qed "hypreal_mult_inverse_left";
   6.646 -
   6.647 -Goal "(c::hypreal) ~= 0 ==> (c*a=c*b) = (a=b)";
   6.648 -by Auto_tac;
   6.649 -by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
   6.650 -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac)  1);
   6.651 -qed "hypreal_mult_left_cancel";
   6.652 -    
   6.653 -Goal "(c::hypreal) ~= 0 ==> (a*c=b*c) = (a=b)";
   6.654 -by (Step_tac 1);
   6.655 -by (dres_inst_tac [("f","%x. x*inverse c")] arg_cong 1);
   6.656 -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_inverse] @ hypreal_mult_ac)  1);
   6.657 -qed "hypreal_mult_right_cancel";
   6.658 -
   6.659 -Goalw [hypreal_zero_def] "x ~= 0 ==> inverse (x::hypreal) ~= 0";
   6.660 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.661 -by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse, hypreal_mult]) 1);
   6.662 -qed "hypreal_inverse_not_zero";
   6.663 -
   6.664 -Addsimps [hypreal_mult_inverse,hypreal_mult_inverse_left];
   6.665 -
   6.666 -Goal "[| x ~= 0; y ~= 0 |] ==> x * y ~= (0::hypreal)";
   6.667 -by (Step_tac 1);
   6.668 -by (dres_inst_tac [("f","%z. inverse x*z")] arg_cong 1);
   6.669 -by (asm_full_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   6.670 -qed "hypreal_mult_not_0";
   6.671 -
   6.672 -Goal "x*y = (0::hypreal) ==> x = 0 | y = 0";
   6.673 -by (auto_tac (claset() addIs [ccontr] addDs [hypreal_mult_not_0],
   6.674 -              simpset()));
   6.675 -qed "hypreal_mult_zero_disj";
   6.676 -
   6.677 -Goal "inverse(-x) = -inverse(x::hypreal)";
   6.678 -by (hypreal_div_undefined_case_tac "x=0" 1);
   6.679 -by (rtac (hypreal_mult_right_cancel RS iffD1) 1);
   6.680 -by (stac hypreal_mult_inverse_left 2);
   6.681 -by Auto_tac;
   6.682 -qed "hypreal_minus_inverse";
   6.683 -
   6.684 -Goal "inverse(x*y) = inverse(x)*inverse(y::hypreal)";
   6.685 -by (hypreal_div_undefined_case_tac "x=0" 1);
   6.686 -by (hypreal_div_undefined_case_tac "y=0" 1);
   6.687 -by (forw_inst_tac [("y","y")] hypreal_mult_not_0 1 THEN assume_tac 1);
   6.688 -by (res_inst_tac [("c1","x")] (hypreal_mult_left_cancel RS iffD1) 1);
   6.689 -by (auto_tac (claset(), simpset() addsimps [hypreal_mult_assoc RS sym]));
   6.690 -by (res_inst_tac [("c1","y")] (hypreal_mult_left_cancel RS iffD1) 1);
   6.691 -by (auto_tac (claset(), simpset() addsimps [hypreal_mult_left_commute]));
   6.692 -by (asm_simp_tac (simpset() addsimps [hypreal_mult_assoc RS sym]) 1);
   6.693 -qed "hypreal_inverse_distrib";
   6.694 -
   6.695 -(*------------------------------------------------------------------
   6.696 -                   Theorems for ordering 
   6.697 - ------------------------------------------------------------------*)
   6.698 -
   6.699 -(* prove introduction and elimination rules for hypreal_less *)
   6.700 -
   6.701 -Goalw [hypreal_less_def]
   6.702 - "(P < (Q::hypreal)) = (EX X Y. X : Rep_hypreal(P) & \
   6.703 -\                             Y : Rep_hypreal(Q) & \
   6.704 -\                             {n. X n < Y n} : FreeUltrafilterNat)";
   6.705 -by (Fast_tac 1);
   6.706 -qed "hypreal_less_iff";
   6.707 -
   6.708 -Goalw [hypreal_less_def]
   6.709 - "[| {n. X n < Y n} : FreeUltrafilterNat; \
   6.710 -\         X : Rep_hypreal(P); \
   6.711 -\         Y : Rep_hypreal(Q) |] ==> P < (Q::hypreal)";
   6.712 -by (Fast_tac 1);
   6.713 -qed "hypreal_lessI";
   6.714 -
   6.715 -
   6.716 -Goalw [hypreal_less_def]
   6.717 -     "!! R1. [| R1 < (R2::hypreal); \
   6.718 -\         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
   6.719 -\         !!X. X : Rep_hypreal(R1) ==> P; \ 
   6.720 -\         !!Y. Y : Rep_hypreal(R2) ==> P |] \
   6.721 -\     ==> P";
   6.722 -by Auto_tac;
   6.723 -qed "hypreal_lessE";
   6.724 -
   6.725 -Goalw [hypreal_less_def]
   6.726 - "R1 < (R2::hypreal) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
   6.727 -\                                  X : Rep_hypreal(R1) & \
   6.728 -\                                  Y : Rep_hypreal(R2))";
   6.729 -by (Fast_tac 1);
   6.730 -qed "hypreal_lessD";
   6.731 -
   6.732 -Goal "~ (R::hypreal) < R";
   6.733 -by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   6.734 -by (auto_tac (claset(), simpset() addsimps [hypreal_less_def]));
   6.735 -by (Ultra_tac 1);
   6.736 -qed "hypreal_less_not_refl";
   6.737 -
   6.738 -(*** y < y ==> P ***)
   6.739 -bind_thm("hypreal_less_irrefl",hypreal_less_not_refl RS notE);
   6.740 -AddSEs [hypreal_less_irrefl];
   6.741 -
   6.742 -Goal "!!(x::hypreal). x < y ==> x ~= y";
   6.743 -by (auto_tac (claset(), simpset() addsimps [hypreal_less_not_refl]));
   6.744 -qed "hypreal_not_refl2";
   6.745 -
   6.746 -Goal "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   6.747 -by (res_inst_tac [("z","R1")] eq_Abs_hypreal 1);
   6.748 -by (res_inst_tac [("z","R2")] eq_Abs_hypreal 1);
   6.749 -by (res_inst_tac [("z","R3")] eq_Abs_hypreal 1);
   6.750 -by (auto_tac (claset() addSIs [exI], simpset() addsimps [hypreal_less_def]));
   6.751 -by (ultra_tac (claset() addIs [order_less_trans], simpset()) 1);
   6.752 -qed "hypreal_less_trans";
   6.753 -
   6.754 -Goal "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P";
   6.755 -by (dtac hypreal_less_trans 1 THEN assume_tac 1);
   6.756 -by (asm_full_simp_tac (simpset() addsimps 
   6.757 -    [hypreal_less_not_refl]) 1);
   6.758 -qed "hypreal_less_asym";
   6.759 -
   6.760 -(*-------------------------------------------------------
   6.761 -  TODO: The following theorem should have been proved 
   6.762 -  first and then used througout the proofs as it probably 
   6.763 -  makes many of them more straightforward. 
   6.764 - -------------------------------------------------------*)
   6.765 -Goalw [hypreal_less_def]
   6.766 -      "(Abs_hypreal(hyprel``{%n. X n}) < \
   6.767 -\           Abs_hypreal(hyprel``{%n. Y n})) = \
   6.768 -\      ({n. X n < Y n} : FreeUltrafilterNat)";
   6.769 -by (auto_tac (claset() addSIs [lemma_hyprel_refl], simpset()));
   6.770 -by (Ultra_tac 1);
   6.771 -qed "hypreal_less";
   6.772 -
   6.773 -(*----------------------------------------------------------------------------
   6.774 -		 Trichotomy: the hyperreals are linearly ordered
   6.775 -  ---------------------------------------------------------------------------*)
   6.776 -
   6.777 -Goalw [hyprel_def] "EX x. x: hyprel `` {%n. 0}";
   6.778 -by (res_inst_tac [("x","%n. 0")] exI 1);
   6.779 -by (Step_tac 1);
   6.780 -by (auto_tac (claset() addSIs [FreeUltrafilterNat_Nat_set], simpset()));
   6.781 -qed "lemma_hyprel_0_mem";
   6.782 -
   6.783 -Goalw [hypreal_zero_def]"0 <  x | x = 0 | x < (0::hypreal)";
   6.784 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.785 -by (auto_tac (claset(),simpset() addsimps [hypreal_less_def]));
   6.786 -by (cut_facts_tac [lemma_hyprel_0_mem] 1 THEN etac exE 1);
   6.787 -by (dres_inst_tac [("x","xa")] spec 1);
   6.788 -by (dres_inst_tac [("x","x")] spec 1);
   6.789 -by (cut_inst_tac [("x","x")] lemma_hyprel_refl 1);
   6.790 -by Auto_tac;
   6.791 -by (dres_inst_tac [("x","x")] spec 1);
   6.792 -by (dres_inst_tac [("x","xa")] spec 1);
   6.793 -by Auto_tac;
   6.794 -by (Ultra_tac 1);
   6.795 -by (auto_tac (claset() addIs [real_linear_less2],simpset()));
   6.796 -qed "hypreal_trichotomy";
   6.797 -
   6.798 -val prems = Goal "[| (0::hypreal) < x ==> P; \
   6.799 -\                 x = 0 ==> P; \
   6.800 -\                 x < 0 ==> P |] ==> P";
   6.801 -by (cut_inst_tac [("x","x")] hypreal_trichotomy 1);
   6.802 -by (REPEAT (eresolve_tac (disjE::prems) 1));
   6.803 -qed "hypreal_trichotomyE";
   6.804 -
   6.805 -(*----------------------------------------------------------------------------
   6.806 -            More properties of <
   6.807 - ----------------------------------------------------------------------------*)
   6.808 -
   6.809 -Goal "((x::hypreal) < y) = (0 < y + -x)";
   6.810 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.811 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.812 -by (auto_tac (claset(),simpset() addsimps [hypreal_add,
   6.813 -    hypreal_zero_def,hypreal_minus,hypreal_less]));
   6.814 -by (ALLGOALS(Ultra_tac));
   6.815 -qed "hypreal_less_minus_iff"; 
   6.816 -
   6.817 -Goal "((x::hypreal) < y) = (x + -y < 0)";
   6.818 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   6.819 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
   6.820 -by (auto_tac (claset(),simpset() addsimps [hypreal_add,
   6.821 -    hypreal_zero_def,hypreal_minus,hypreal_less]));
   6.822 -by (ALLGOALS(Ultra_tac));
   6.823 -qed "hypreal_less_minus_iff2";
   6.824 -
   6.825 -Goal "((x::hypreal) = y) = (x + - y = 0)";
   6.826 -by Auto_tac;
   6.827 -by (res_inst_tac [("x1","-y")] (hypreal_add_right_cancel RS iffD1) 1);
   6.828 -by Auto_tac;
   6.829 -qed "hypreal_eq_minus_iff"; 
   6.830 -
   6.831 -Goal "((x::hypreal) = y) = (0 = y + - x)";
   6.832 -by Auto_tac;
   6.833 -by (res_inst_tac [("x1","-x")] (hypreal_add_right_cancel RS iffD1) 1);
   6.834 -by Auto_tac;
   6.835 -qed "hypreal_eq_minus_iff2"; 
   6.836 -
   6.837 -(* 07/00 *)
   6.838 -Goal "(0::hypreal) - x = -x";
   6.839 -by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
   6.840 -qed "hypreal_diff_zero";
   6.841 -
   6.842 -Goal "x - (0::hypreal) = x";
   6.843 -by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
   6.844 -qed "hypreal_diff_zero_right";
   6.845 -
   6.846 -Goal "x - x = (0::hypreal)";
   6.847 -by (simp_tac (simpset() addsimps [hypreal_diff_def]) 1);
   6.848 -qed "hypreal_diff_self";
   6.849 -
   6.850 -Addsimps [hypreal_diff_zero, hypreal_diff_zero_right, hypreal_diff_self];
   6.851 -
   6.852 -Goal "(x = y + z) = (x + -z = (y::hypreal))";
   6.853 -by (auto_tac (claset(),simpset() addsimps [hypreal_add_assoc]));
   6.854 -qed "hypreal_eq_minus_iff3";
   6.855 -
   6.856 -Goal "(x ~= a) = (x + -a ~= (0::hypreal))";
   6.857 -by (auto_tac (claset() addDs [hypreal_eq_minus_iff RS iffD2],
   6.858 -              simpset())); 
   6.859 -qed "hypreal_not_eq_minus_iff";
   6.860 -
   6.861 -
   6.862 -(*** linearity ***)
   6.863 -
   6.864 -Goal "(x::hypreal) < y | x = y | y < x";
   6.865 -by (stac hypreal_eq_minus_iff2 1);
   6.866 -by (res_inst_tac [("x1","x")] (hypreal_less_minus_iff RS ssubst) 1);
   6.867 -by (res_inst_tac [("x1","y")] (hypreal_less_minus_iff2 RS ssubst) 1);
   6.868 -by (rtac hypreal_trichotomyE 1);
   6.869 -by Auto_tac;
   6.870 -qed "hypreal_linear";
   6.871 -
   6.872 -Goal "((w::hypreal) ~= z) = (w<z | z<w)";
   6.873 -by (cut_facts_tac [hypreal_linear] 1);
   6.874 -by (Blast_tac 1);
   6.875 -qed "hypreal_neq_iff";
   6.876 -
   6.877 -Goal "!!(x::hypreal). [| x < y ==> P;  x = y ==> P; \
   6.878 -\          y < x ==> P |] ==> P";
   6.879 -by (cut_inst_tac [("x","x"),("y","y")] hypreal_linear 1);
   6.880 -by Auto_tac;
   6.881 -qed "hypreal_linear_less2";
   6.882 -
   6.883 -(*------------------------------------------------------------------------------
   6.884 -                            Properties of <=
   6.885 - ------------------------------------------------------------------------------*)
   6.886 -(*------ hypreal le iff reals le a.e ------*)
   6.887 -
   6.888 -Goalw [hypreal_le_def,real_le_def]
   6.889 -      "(Abs_hypreal(hyprel``{%n. X n}) <= \
   6.890 -\           Abs_hypreal(hyprel``{%n. Y n})) = \
   6.891 -\      ({n. X n <= Y n} : FreeUltrafilterNat)";
   6.892 -by (auto_tac (claset(),simpset() addsimps [hypreal_less]));
   6.893 -by (ALLGOALS(Ultra_tac));
   6.894 -qed "hypreal_le";
   6.895 -
   6.896 -(*---------------------------------------------------------*)
   6.897 -(*---------------------------------------------------------*)
   6.898 -Goalw [hypreal_le_def] 
   6.899 -     "~(w < z) ==> z <= (w::hypreal)";
   6.900 -by (assume_tac 1);
   6.901 -qed "hypreal_leI";
   6.902 -
   6.903 -Goalw [hypreal_le_def] 
   6.904 -      "z<=w ==> ~(w<(z::hypreal))";
   6.905 -by (assume_tac 1);
   6.906 -qed "hypreal_leD";
   6.907 -
   6.908 -bind_thm ("hypreal_leE", make_elim hypreal_leD);
   6.909 -
   6.910 -Goal "(~(w < z)) = (z <= (w::hypreal))";
   6.911 -by (fast_tac (claset() addSIs [hypreal_leI,hypreal_leD]) 1);
   6.912 -qed "hypreal_less_le_iff";
   6.913 -
   6.914 -Goalw [hypreal_le_def] "~ z <= w ==> w<(z::hypreal)";
   6.915 -by (Fast_tac 1);
   6.916 -qed "not_hypreal_leE";
   6.917 -
   6.918 -Goalw [hypreal_le_def] "!!(x::hypreal). x <= y ==> x < y | x = y";
   6.919 -by (cut_facts_tac [hypreal_linear] 1);
   6.920 -by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
   6.921 -qed "hypreal_le_imp_less_or_eq";
   6.922 -
   6.923 -Goalw [hypreal_le_def] "z<w | z=w ==> z <=(w::hypreal)";
   6.924 -by (cut_facts_tac [hypreal_linear] 1);
   6.925 -by (fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym]) 1);
   6.926 -qed "hypreal_less_or_eq_imp_le";
   6.927 -
   6.928 -Goal "(x <= (y::hypreal)) = (x < y | x=y)";
   6.929 -by (REPEAT(ares_tac [iffI, hypreal_less_or_eq_imp_le, hypreal_le_imp_less_or_eq] 1));
   6.930 -qed "hypreal_le_eq_less_or_eq";
   6.931 -val hypreal_le_less = hypreal_le_eq_less_or_eq;
   6.932 -
   6.933 -Goal "w <= (w::hypreal)";
   6.934 -by (simp_tac (simpset() addsimps [hypreal_le_eq_less_or_eq]) 1);
   6.935 -qed "hypreal_le_refl";
   6.936 -
   6.937 -(* Axiom 'linorder_linear' of class 'linorder': *)
   6.938 -Goal "(z::hypreal) <= w | w <= z";
   6.939 -by (simp_tac (simpset() addsimps [hypreal_le_less]) 1);
   6.940 -by (cut_facts_tac [hypreal_linear] 1);
   6.941 -by (Blast_tac 1);
   6.942 -qed "hypreal_le_linear";
   6.943 -
   6.944 -Goal "[| i <= j; j <= k |] ==> i <= (k::hypreal)";
   6.945 -by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
   6.946 -            rtac hypreal_less_or_eq_imp_le, 
   6.947 -            fast_tac (claset() addIs [hypreal_less_trans])]);
   6.948 -qed "hypreal_le_trans";
   6.949 -
   6.950 -Goal "[| z <= w; w <= z |] ==> z = (w::hypreal)";
   6.951 -by (EVERY1 [dtac hypreal_le_imp_less_or_eq, dtac hypreal_le_imp_less_or_eq,
   6.952 -            fast_tac (claset() addEs [hypreal_less_irrefl,hypreal_less_asym])]);
   6.953 -qed "hypreal_le_anti_sym";
   6.954 -
   6.955 -Goal "[| ~ y < x; y ~= x |] ==> x < (y::hypreal)";
   6.956 -by (rtac not_hypreal_leE 1);
   6.957 -by (fast_tac (claset() addDs [hypreal_le_imp_less_or_eq]) 1);
   6.958 -qed "not_less_not_eq_hypreal_less";
   6.959 -
   6.960 -(* Axiom 'order_less_le' of class 'order': *)
   6.961 -Goal "((w::hypreal) < z) = (w <= z & w ~= z)";
   6.962 -by (simp_tac (simpset() addsimps [hypreal_le_def, hypreal_neq_iff]) 1);
   6.963 -by (blast_tac (claset() addIs [hypreal_less_asym]) 1);
   6.964 -qed "hypreal_less_le";
   6.965 -
   6.966 -Goal "(0 < -R) = (R < (0::hypreal))";
   6.967 -by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   6.968 -by (auto_tac (claset(),
   6.969 -       simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
   6.970 -qed "hypreal_minus_zero_less_iff";
   6.971 -Addsimps [hypreal_minus_zero_less_iff];
   6.972 -
   6.973 -Goal "(-R < 0) = ((0::hypreal) < R)";
   6.974 -by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   6.975 -by (auto_tac (claset(),
   6.976 -         simpset() addsimps [hypreal_zero_def, hypreal_less,hypreal_minus]));
   6.977 -by (ALLGOALS(Ultra_tac));
   6.978 -qed "hypreal_minus_zero_less_iff2";
   6.979 -Addsimps [hypreal_minus_zero_less_iff2];
   6.980 -
   6.981 -Goalw [hypreal_le_def] "((0::hypreal) <= -r) = (r <= 0)";
   6.982 -by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1);
   6.983 -qed "hypreal_minus_zero_le_iff";
   6.984 -Addsimps [hypreal_minus_zero_le_iff];
   6.985 -
   6.986 -Goalw [hypreal_le_def] "(-r <= (0::hypreal)) = (0 <= r)";
   6.987 -by (simp_tac (simpset() addsimps [hypreal_minus_zero_less_iff2]) 1);
   6.988 -qed "hypreal_minus_zero_le_iff2";
   6.989 -Addsimps [hypreal_minus_zero_le_iff2];
   6.990 -
   6.991 -(*----------------------------------------------------------
   6.992 -  hypreal_of_real preserves field and order properties
   6.993 - -----------------------------------------------------------*)
   6.994 -Goalw [hypreal_of_real_def] 
   6.995 -     "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2";
   6.996 -by (simp_tac (simpset() addsimps [hypreal_add, hypreal_add_mult_distrib]) 1);
   6.997 -qed "hypreal_of_real_add";
   6.998 -Addsimps [hypreal_of_real_add];
   6.999 -
  6.1000 -Goalw [hypreal_of_real_def] 
  6.1001 -     "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2";
  6.1002 -by (simp_tac (simpset() addsimps [hypreal_mult, hypreal_add_mult_distrib2]) 1);
  6.1003 -qed "hypreal_of_real_mult";
  6.1004 -Addsimps [hypreal_of_real_mult];
  6.1005 -
  6.1006 -Goalw [hypreal_less_def,hypreal_of_real_def] 
  6.1007 -     "(hypreal_of_real z1 <  hypreal_of_real z2) = (z1 < z2)";
  6.1008 -by Auto_tac;
  6.1009 -by (res_inst_tac [("x","%n. z1")] exI 2);
  6.1010 -by (Step_tac 1); 
  6.1011 -by (res_inst_tac [("x","%n. z2")] exI 3);
  6.1012 -by Auto_tac;
  6.1013 -by (rtac FreeUltrafilterNat_P 1);
  6.1014 -by (Ultra_tac 1);
  6.1015 -qed "hypreal_of_real_less_iff";
  6.1016 -Addsimps [hypreal_of_real_less_iff];
  6.1017 -
  6.1018 -Goalw [hypreal_le_def,real_le_def] 
  6.1019 -     "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)";
  6.1020 -by Auto_tac;
  6.1021 -qed "hypreal_of_real_le_iff";
  6.1022 -Addsimps [hypreal_of_real_le_iff];
  6.1023 -
  6.1024 -Goal "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)";
  6.1025 -by (force_tac (claset() addIs [order_antisym, hypreal_of_real_le_iff RS iffD1],
  6.1026 -               simpset()) 1); 
  6.1027 -qed "hypreal_of_real_eq_iff";
  6.1028 -Addsimps [hypreal_of_real_eq_iff];
  6.1029 -
  6.1030 -Goalw [hypreal_of_real_def] "hypreal_of_real (-r) = - hypreal_of_real  r";
  6.1031 -by (auto_tac (claset(),simpset() addsimps [hypreal_minus]));
  6.1032 -qed "hypreal_of_real_minus";
  6.1033 -Addsimps [hypreal_of_real_minus];
  6.1034 -
  6.1035 -Goalw [hypreal_of_real_def,hypreal_one_def] "hypreal_of_real 1 = (1::hypreal)";
  6.1036 -by (Simp_tac 1); 
  6.1037 -qed "hypreal_of_real_one";
  6.1038 -Addsimps [hypreal_of_real_one];
  6.1039 -
  6.1040 -Goalw [hypreal_of_real_def,hypreal_zero_def] "hypreal_of_real 0 = 0";
  6.1041 -by (Simp_tac 1); 
  6.1042 -qed "hypreal_of_real_zero";
  6.1043 -Addsimps [hypreal_of_real_zero];
  6.1044 -
  6.1045 -Goal "(hypreal_of_real r = 0) = (r = 0)";
  6.1046 -by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
  6.1047 -    simpset() addsimps [hypreal_of_real_def,
  6.1048 -                        hypreal_zero_def,FreeUltrafilterNat_Nat_set]));
  6.1049 -qed "hypreal_of_real_zero_iff";
  6.1050 -
  6.1051 -Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)";
  6.1052 -by (case_tac "r=0" 1);
  6.1053 -by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO, INVERSE_ZERO, 
  6.1054 -                              HYPREAL_INVERSE_ZERO]) 1);
  6.1055 -by (res_inst_tac [("c1","hypreal_of_real r")] 
  6.1056 -    (hypreal_mult_left_cancel RS iffD1) 1);
  6.1057 -by (stac (hypreal_of_real_mult RS sym) 2); 
  6.1058 -by (auto_tac (claset(), simpset() addsimps [hypreal_of_real_zero_iff]));
  6.1059 -qed "hypreal_of_real_inverse";
  6.1060 -Addsimps [hypreal_of_real_inverse];
  6.1061 -
  6.1062 -Goal "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2";
  6.1063 -by (simp_tac (simpset() addsimps [hypreal_divide_def, real_divide_def]) 1);
  6.1064 -qed "hypreal_of_real_divide"; 
  6.1065 -Addsimps [hypreal_of_real_divide];
  6.1066 -
  6.1067 -
  6.1068 -(*** Division lemmas ***)
  6.1069 -
  6.1070 -Goal "(0::hypreal)/x = 0";
  6.1071 -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); 
  6.1072 -qed "hypreal_zero_divide";
  6.1073 -
  6.1074 -Goal "x/(1::hypreal) = x";
  6.1075 -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); 
  6.1076 -qed "hypreal_divide_one";
  6.1077 -Addsimps [hypreal_zero_divide, hypreal_divide_one];
  6.1078 -
  6.1079 -Goal "(x::hypreal) * (y/z) = (x*y)/z";
  6.1080 -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_mult_assoc]) 1); 
  6.1081 -qed "hypreal_times_divide1_eq";
  6.1082 -
  6.1083 -Goal "(y/z) * (x::hypreal) = (y*x)/z";
  6.1084 -by (simp_tac (simpset() addsimps [hypreal_divide_def]@hypreal_mult_ac) 1); 
  6.1085 -qed "hypreal_times_divide2_eq";
  6.1086 -
  6.1087 -Addsimps [hypreal_times_divide1_eq, hypreal_times_divide2_eq];
  6.1088 -
  6.1089 -Goal "(x::hypreal) / (y/z) = (x*z)/y";
  6.1090 -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib]@
  6.1091 -                                 hypreal_mult_ac) 1); 
  6.1092 -qed "hypreal_divide_divide1_eq";
  6.1093 -
  6.1094 -Goal "((x::hypreal) / y) / z = x/(y*z)";
  6.1095 -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_inverse_distrib, 
  6.1096 -                                  hypreal_mult_assoc]) 1); 
  6.1097 -qed "hypreal_divide_divide2_eq";
  6.1098 -
  6.1099 -Addsimps [hypreal_divide_divide1_eq, hypreal_divide_divide2_eq];
  6.1100 -
  6.1101 -(** As with multiplication, pull minus signs OUT of the / operator **)
  6.1102 -
  6.1103 -Goal "(-x) / (y::hypreal) = - (x/y)";
  6.1104 -by (simp_tac (simpset() addsimps [hypreal_divide_def]) 1); 
  6.1105 -qed "hypreal_minus_divide_eq";
  6.1106 -Addsimps [hypreal_minus_divide_eq];
  6.1107 -
  6.1108 -Goal "(x / -(y::hypreal)) = - (x/y)";
  6.1109 -by (simp_tac (simpset() addsimps [hypreal_divide_def, hypreal_minus_inverse]) 1); 
  6.1110 -qed "hypreal_divide_minus_eq";
  6.1111 -Addsimps [hypreal_divide_minus_eq];
  6.1112 -
  6.1113 -Goal "(x+y)/(z::hypreal) = x/z + y/z";
  6.1114 -by (simp_tac (simpset() addsimps [hypreal_divide_def, 
  6.1115 -                                  hypreal_add_mult_distrib]) 1); 
  6.1116 -qed "hypreal_add_divide_distrib";
  6.1117 -
  6.1118 -Goal "[|(x::hypreal) ~= 0;  y ~= 0 |]  \
  6.1119 -\     ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)";
  6.1120 -by (asm_full_simp_tac (simpset() addsimps [hypreal_inverse_distrib,
  6.1121 -                    hypreal_add_mult_distrib,hypreal_mult_assoc RS sym]) 1);
  6.1122 -by (stac hypreal_mult_assoc 1);
  6.1123 -by (rtac (hypreal_mult_left_commute RS subst) 1);
  6.1124 -by (asm_full_simp_tac (simpset() addsimps [hypreal_add_commute]) 1);
  6.1125 -qed "hypreal_inverse_add";
  6.1126 -
  6.1127 -Goal "x = -x ==> x = (0::hypreal)";
  6.1128 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  6.1129 -by (auto_tac (claset(), simpset() addsimps [hypreal_minus, hypreal_zero_def]));
  6.1130 -by (Ultra_tac 1);
  6.1131 -qed "hypreal_self_eq_minus_self_zero";
  6.1132 -
  6.1133 -Goal "(x + x = 0) = (x = (0::hypreal))";
  6.1134 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  6.1135 -by (auto_tac (claset(), simpset() addsimps [hypreal_add, hypreal_zero_def]));
  6.1136 -qed "hypreal_add_self_zero_cancel";
  6.1137 -Addsimps [hypreal_add_self_zero_cancel];
  6.1138 -
  6.1139 -Goal "(x + x + y = y) = (x = (0::hypreal))";
  6.1140 -by Auto_tac;
  6.1141 -by (dtac (hypreal_eq_minus_iff RS iffD1) 1);
  6.1142 -by (auto_tac (claset(), 
  6.1143 -     simpset() addsimps [hypreal_add_assoc, hypreal_self_eq_minus_self_zero]));
  6.1144 -qed "hypreal_add_self_zero_cancel2";
  6.1145 -Addsimps [hypreal_add_self_zero_cancel2];
  6.1146 -
  6.1147 -Goal "(x + (x + y) = y) = (x = (0::hypreal))";
  6.1148 -by (simp_tac (simpset() addsimps [hypreal_add_assoc RS sym]) 1);
  6.1149 -qed "hypreal_add_self_zero_cancel2a";
  6.1150 -Addsimps [hypreal_add_self_zero_cancel2a];
  6.1151 -
  6.1152 -Goal "(b = -a) = (-b = (a::hypreal))";
  6.1153 -by Auto_tac;
  6.1154 -qed "hypreal_minus_eq_swap";
  6.1155 -
  6.1156 -Goal "(-b = -a) = (b = (a::hypreal))";
  6.1157 -by (asm_full_simp_tac (simpset() addsimps 
  6.1158 -    [hypreal_minus_eq_swap]) 1);
  6.1159 -qed "hypreal_minus_eq_cancel";
  6.1160 -Addsimps [hypreal_minus_eq_cancel];
  6.1161 -
  6.1162 -Goalw [hypreal_diff_def] "(x<y) = (x-y < (0::hypreal))";
  6.1163 -by (rtac hypreal_less_minus_iff2 1);
  6.1164 -qed "hypreal_less_eq_diff";
  6.1165 -
  6.1166 -(*** Subtraction laws ***)
  6.1167 -
  6.1168 -Goal "x + (y - z) = (x + y) - (z::hypreal)";
  6.1169 -by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
  6.1170 -qed "hypreal_add_diff_eq";
  6.1171 -
  6.1172 -Goal "(x - y) + z = (x + z) - (y::hypreal)";
  6.1173 -by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
  6.1174 -qed "hypreal_diff_add_eq";
  6.1175 -
  6.1176 -Goal "(x - y) - z = x - (y + (z::hypreal))";
  6.1177 -by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
  6.1178 -qed "hypreal_diff_diff_eq";
  6.1179 -
  6.1180 -Goal "x - (y - z) = (x + z) - (y::hypreal)";
  6.1181 -by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
  6.1182 -qed "hypreal_diff_diff_eq2";
  6.1183 -
  6.1184 -Goal "(x-y < z) = (x < z + (y::hypreal))";
  6.1185 -by (stac hypreal_less_eq_diff 1);
  6.1186 -by (res_inst_tac [("y1", "z")] (hypreal_less_eq_diff RS ssubst) 1);
  6.1187 -by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
  6.1188 -qed "hypreal_diff_less_eq";
  6.1189 -
  6.1190 -Goal "(x < z-y) = (x + (y::hypreal) < z)";
  6.1191 -by (stac hypreal_less_eq_diff 1);
  6.1192 -by (res_inst_tac [("y1", "z-y")] (hypreal_less_eq_diff RS ssubst) 1);
  6.1193 -by (simp_tac (simpset() addsimps hypreal_diff_def::hypreal_add_ac) 1);
  6.1194 -qed "hypreal_less_diff_eq";
  6.1195 -
  6.1196 -Goalw [hypreal_le_def] "(x-y <= z) = (x <= z + (y::hypreal))";
  6.1197 -by (simp_tac (simpset() addsimps [hypreal_less_diff_eq]) 1);
  6.1198 -qed "hypreal_diff_le_eq";
  6.1199 -
  6.1200 -Goalw [hypreal_le_def] "(x <= z-y) = (x + (y::hypreal) <= z)";
  6.1201 -by (simp_tac (simpset() addsimps [hypreal_diff_less_eq]) 1);
  6.1202 -qed "hypreal_le_diff_eq";
  6.1203 -
  6.1204 -Goalw [hypreal_diff_def] "(x-y = z) = (x = z + (y::hypreal))";
  6.1205 -by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
  6.1206 -qed "hypreal_diff_eq_eq";
  6.1207 -
  6.1208 -Goalw [hypreal_diff_def] "(x = z-y) = (x + (y::hypreal) = z)";
  6.1209 -by (auto_tac (claset(), simpset() addsimps [hypreal_add_assoc]));
  6.1210 -qed "hypreal_eq_diff_eq";
  6.1211 -
  6.1212 -(*This list of rewrites simplifies (in)equalities by bringing subtractions
  6.1213 -  to the top and then moving negative terms to the other side.  
  6.1214 -  Use with hypreal_add_ac*)
  6.1215 -val hypreal_compare_rls = 
  6.1216 -  [symmetric hypreal_diff_def,
  6.1217 -   hypreal_add_diff_eq, hypreal_diff_add_eq, hypreal_diff_diff_eq, 
  6.1218 -   hypreal_diff_diff_eq2, 
  6.1219 -   hypreal_diff_less_eq, hypreal_less_diff_eq, hypreal_diff_le_eq, 
  6.1220 -   hypreal_le_diff_eq, hypreal_diff_eq_eq, hypreal_eq_diff_eq];
  6.1221 -
  6.1222 -
  6.1223 -(** For the cancellation simproc.
  6.1224 -    The idea is to cancel like terms on opposite sides by subtraction **)
  6.1225 -
  6.1226 -Goal "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')";
  6.1227 -by (stac hypreal_less_eq_diff 1);
  6.1228 -by (res_inst_tac [("y1", "y")] (hypreal_less_eq_diff RS ssubst) 1);
  6.1229 -by (Asm_simp_tac 1);
  6.1230 -qed "hypreal_less_eqI";
  6.1231 -
  6.1232 -Goal "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')";
  6.1233 -by (dtac hypreal_less_eqI 1);
  6.1234 -by (asm_simp_tac (simpset() addsimps [hypreal_le_def]) 1);
  6.1235 -qed "hypreal_le_eqI";
  6.1236 -
  6.1237 -Goal "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')";
  6.1238 -by Safe_tac;
  6.1239 -by (ALLGOALS
  6.1240 -    (asm_full_simp_tac
  6.1241 -     (simpset() addsimps [hypreal_eq_diff_eq, hypreal_diff_eq_eq])));
  6.1242 -qed "hypreal_eq_eqI";
  6.1243 -
  6.1244 -
  6.1245 -(*MOVE UP*)
  6.1246 -Goal "0 = Abs_hypreal (hyprel `` {%n. 0})";
  6.1247 -by (simp_tac (simpset() addsimps [hypreal_zero_def RS meta_eq_to_obj_eq RS sym]) 1);
  6.1248 -qed "hypreal_zero_num";
  6.1249 -
  6.1250 -Goal "1 = Abs_hypreal (hyprel `` {%n. 1})";
  6.1251 -by (simp_tac (simpset() addsimps [hypreal_one_def RS meta_eq_to_obj_eq RS sym]) 1);
  6.1252 -qed "hypreal_one_num";
  6.1253 -
  6.1254 -
  6.1255 -(*MOVE UP*)
  6.1256 -
  6.1257 -Goalw [omega_def] "0 < omega";
  6.1258 -by (auto_tac (claset(),simpset() addsimps [hypreal_less,hypreal_zero_num]));
  6.1259 -qed "hypreal_omega_gt_zero";
  6.1260 -Addsimps [hypreal_omega_gt_zero];
     7.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Tue Dec 16 23:24:17 2003 +0100
     7.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Dec 17 16:23:52 2003 +0100
     7.3 @@ -5,52 +5,55 @@
     7.4      Description : Construction of hyperreals using ultrafilters
     7.5  *)
     7.6  
     7.7 -HyperDef = Filter + Real +
     7.8 -
     7.9 -consts
    7.10 -
    7.11 -    FreeUltrafilterNat   :: nat set set    ("\\<U>")
    7.12 -
    7.13 -defs
    7.14 -
    7.15 -    FreeUltrafilterNat_def
    7.16 -    "FreeUltrafilterNat    ==   (@U. U : FreeUltrafilter (UNIV:: nat set))"
    7.17 +theory HyperDef = Filter + Real
    7.18 +files ("fuf.ML"):  (*Warning: file fuf.ML refers to the name Hyperdef!*)
    7.19  
    7.20  
    7.21  constdefs
    7.22 -    hyprel :: "((nat=>real)*(nat=>real)) set"
    7.23 -    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) &
    7.24 +
    7.25 +  FreeUltrafilterNat   :: "nat set set"    ("\\<U>")
    7.26 +    "FreeUltrafilterNat == (SOME U. U \<in> FreeUltrafilter (UNIV:: nat set))"
    7.27 +
    7.28 +  hyprel :: "((nat=>real)*(nat=>real)) set"
    7.29 +    "hyprel == {p. \<exists>X Y. p = ((X::nat=>real),Y) &
    7.30                     {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
    7.31  
    7.32 -typedef hypreal = "UNIV//hyprel"   (quotient_def)
    7.33 +typedef hypreal = "UNIV//hyprel" 
    7.34 +    by (auto simp add: quotient_def) 
    7.35  
    7.36 -instance
    7.37 -   hypreal  :: {ord, zero, one, plus, times, minus, inverse}
    7.38 +instance hypreal :: ord ..
    7.39 +instance hypreal :: zero ..
    7.40 +instance hypreal :: one ..
    7.41 +instance hypreal :: plus ..
    7.42 +instance hypreal :: times ..
    7.43 +instance hypreal :: minus ..
    7.44 +instance hypreal :: inverse ..
    7.45  
    7.46 -defs
    7.47  
    7.48 -  hypreal_zero_def
    7.49 +defs (overloaded)
    7.50 +
    7.51 +  hypreal_zero_def:
    7.52    "0 == Abs_hypreal(hyprel``{%n::nat. (0::real)})"
    7.53  
    7.54 -  hypreal_one_def
    7.55 +  hypreal_one_def:
    7.56    "1 == Abs_hypreal(hyprel``{%n::nat. (1::real)})"
    7.57  
    7.58 -  hypreal_minus_def
    7.59 -  "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    7.60 +  hypreal_minus_def:
    7.61 +  "- P == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    7.62  
    7.63 -  hypreal_diff_def
    7.64 +  hypreal_diff_def:
    7.65    "x - y == x + -(y::hypreal)"
    7.66  
    7.67 -  hypreal_inverse_def
    7.68 -  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P).
    7.69 +  hypreal_inverse_def:
    7.70 +  "inverse P == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P).
    7.71                      hyprel``{%n. if X n = 0 then 0 else inverse (X n)})"
    7.72  
    7.73 -  hypreal_divide_def
    7.74 +  hypreal_divide_def:
    7.75    "P / Q::hypreal == P * inverse Q"
    7.76  
    7.77  constdefs
    7.78  
    7.79 -  hypreal_of_real  :: real => hypreal
    7.80 +  hypreal_of_real  :: "real => hypreal"
    7.81    "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
    7.82  
    7.83    omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
    7.84 @@ -60,25 +63,1442 @@
    7.85    "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
    7.86  
    7.87  syntax (xsymbols)
    7.88 -  omega   :: hypreal   ("\\<omega>")
    7.89 -  epsilon :: hypreal   ("\\<epsilon>")
    7.90 +  omega   :: hypreal   ("\<omega>")
    7.91 +  epsilon :: hypreal   ("\<epsilon>")
    7.92  
    7.93  
    7.94  defs
    7.95  
    7.96 -  hypreal_add_def
    7.97 -  "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    7.98 +  hypreal_add_def:
    7.99 +  "P + Q == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). \<Union>Y \<in> Rep_hypreal(Q).
   7.100                  hyprel``{%n::nat. X n + Y n})"
   7.101  
   7.102 -  hypreal_mult_def
   7.103 -  "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
   7.104 +  hypreal_mult_def:
   7.105 +  "P * Q == Abs_hypreal(\<Union>X \<in> Rep_hypreal(P). \<Union>Y \<in> Rep_hypreal(Q).
   7.106                  hyprel``{%n::nat. X n * Y n})"
   7.107  
   7.108 -  hypreal_less_def
   7.109 -  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) &
   7.110 -                               Y: Rep_hypreal(Q) &
   7.111 -                               {n::nat. X n < Y n} : FreeUltrafilterNat"
   7.112 -  hypreal_le_def
   7.113 +  hypreal_less_def:
   7.114 +  "P < (Q::hypreal) == \<exists>X Y. X \<in> Rep_hypreal(P) &
   7.115 +                               Y \<in> Rep_hypreal(Q) &
   7.116 +                               {n::nat. X n < Y n} \<in> FreeUltrafilterNat"
   7.117 +  hypreal_le_def:
   7.118    "P <= (Q::hypreal) == ~(Q < P)"
   7.119  
   7.120 +(*------------------------------------------------------------------------
   7.121 +             Proof that the set of naturals is not finite
   7.122 + ------------------------------------------------------------------------*)
   7.123 +
   7.124 +(*** based on James' proof that the set of naturals is not finite ***)
   7.125 +lemma finite_exhausts [rule_format (no_asm)]: "finite (A::nat set) --> (\<exists>n. \<forall>m. Suc (n + m) \<notin> A)"
   7.126 +apply (rule impI)
   7.127 +apply (erule_tac F = "A" in finite_induct)
   7.128 +apply (blast , erule exE)
   7.129 +apply (rule_tac x = "n + x" in exI)
   7.130 +apply (rule allI , erule_tac x = "x + m" in allE)
   7.131 +apply (auto simp add: add_ac)
   7.132 +done
   7.133 +
   7.134 +lemma finite_not_covers [rule_format (no_asm)]: "finite (A :: nat set) --> (\<exists>n. n \<notin>A)"
   7.135 +apply (rule impI , drule finite_exhausts)
   7.136 +apply blast
   7.137 +done
   7.138 +
   7.139 +lemma not_finite_nat: "~ finite(UNIV:: nat set)"
   7.140 +apply (fast dest!: finite_exhausts)
   7.141 +done
   7.142 +
   7.143 +(*------------------------------------------------------------------------
   7.144 +   Existence of free ultrafilter over the naturals and proof of various 
   7.145 +   properties of the FreeUltrafilterNat- an arbitrary free ultrafilter
   7.146 + ------------------------------------------------------------------------*)
   7.147 +
   7.148 +lemma FreeUltrafilterNat_Ex: "\<exists>U. U: FreeUltrafilter (UNIV::nat set)"
   7.149 +apply (rule not_finite_nat [THEN FreeUltrafilter_Ex])
   7.150 +done
   7.151 +
   7.152 +lemma FreeUltrafilterNat_mem: 
   7.153 +     "FreeUltrafilterNat: FreeUltrafilter(UNIV:: nat set)"
   7.154 +apply (unfold FreeUltrafilterNat_def)
   7.155 +apply (rule FreeUltrafilterNat_Ex [THEN exE])
   7.156 +apply (rule someI2)
   7.157 +apply assumption+
   7.158 +done
   7.159 +declare FreeUltrafilterNat_mem [simp]
   7.160 +
   7.161 +lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat"
   7.162 +apply (unfold FreeUltrafilterNat_def)
   7.163 +apply (rule FreeUltrafilterNat_Ex [THEN exE])
   7.164 +apply (rule someI2 , assumption)
   7.165 +apply (blast dest: mem_FreeUltrafiltersetD1)
   7.166 +done
   7.167 +
   7.168 +lemma FreeUltrafilterNat_not_finite: "x: FreeUltrafilterNat ==> ~ finite x"
   7.169 +apply (blast dest: FreeUltrafilterNat_finite)
   7.170 +done
   7.171 +
   7.172 +lemma FreeUltrafilterNat_empty: "{} \<notin> FreeUltrafilterNat"
   7.173 +apply (unfold FreeUltrafilterNat_def)
   7.174 +apply (rule FreeUltrafilterNat_Ex [THEN exE])
   7.175 +apply (rule someI2 , assumption)
   7.176 +apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter Filter_empty_not_mem)
   7.177 +done
   7.178 +declare FreeUltrafilterNat_empty [simp]
   7.179 +
   7.180 +lemma FreeUltrafilterNat_Int: "[| X: FreeUltrafilterNat;  Y: FreeUltrafilterNat |]   
   7.181 +      ==> X Int Y \<in> FreeUltrafilterNat"
   7.182 +apply (cut_tac FreeUltrafilterNat_mem)
   7.183 +apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1)
   7.184 +done
   7.185 +
   7.186 +lemma FreeUltrafilterNat_subset: "[| X: FreeUltrafilterNat;  X <= Y |]  
   7.187 +      ==> Y \<in> FreeUltrafilterNat"
   7.188 +apply (cut_tac FreeUltrafilterNat_mem)
   7.189 +apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2)
   7.190 +done
   7.191 +
   7.192 +lemma FreeUltrafilterNat_Compl: "X: FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat"
   7.193 +apply (safe)
   7.194 +apply (drule FreeUltrafilterNat_Int , assumption)
   7.195 +apply auto
   7.196 +done
   7.197 +
   7.198 +lemma FreeUltrafilterNat_Compl_mem: "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
   7.199 +apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]])
   7.200 +apply (safe , drule_tac x = "X" in bspec)
   7.201 +apply (auto simp add: UNIV_diff_Compl)
   7.202 +done
   7.203 +
   7.204 +lemma FreeUltrafilterNat_Compl_iff1: "(X \<notin> FreeUltrafilterNat) = (-X: FreeUltrafilterNat)"
   7.205 +apply (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem)
   7.206 +done
   7.207 +
   7.208 +lemma FreeUltrafilterNat_Compl_iff2: "(X: FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)"
   7.209 +apply (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric])
   7.210 +done
   7.211 +
   7.212 +lemma FreeUltrafilterNat_UNIV: "(UNIV::nat set) \<in> FreeUltrafilterNat"
   7.213 +apply (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
   7.214 +done
   7.215 +declare FreeUltrafilterNat_UNIV [simp]
   7.216 +
   7.217 +lemma FreeUltrafilterNat_Nat_set: "UNIV \<in> FreeUltrafilterNat"
   7.218 +apply auto
   7.219 +done
   7.220 +declare FreeUltrafilterNat_Nat_set [simp]
   7.221 +
   7.222 +lemma FreeUltrafilterNat_Nat_set_refl: "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
   7.223 +apply (simp (no_asm))
   7.224 +done
   7.225 +declare FreeUltrafilterNat_Nat_set_refl [intro]
   7.226 +
   7.227 +lemma FreeUltrafilterNat_P: "{n::nat. P} \<in> FreeUltrafilterNat ==> P"
   7.228 +apply (rule ccontr)
   7.229 +apply simp
   7.230 +done
   7.231 +
   7.232 +lemma FreeUltrafilterNat_Ex_P: "{n. P(n)} \<in> FreeUltrafilterNat ==> \<exists>n. P(n)"
   7.233 +apply (rule ccontr)
   7.234 +apply simp
   7.235 +done
   7.236 +
   7.237 +lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat"
   7.238 +apply (auto intro: FreeUltrafilterNat_Nat_set)
   7.239 +done
   7.240 +
   7.241 +(*-------------------------------------------------------
   7.242 +     Define and use Ultrafilter tactics
   7.243 + -------------------------------------------------------*)
   7.244 +use "fuf.ML"
   7.245 +
   7.246 +method_setup fuf = {*
   7.247 +    Method.ctxt_args (fn ctxt =>
   7.248 +        Method.METHOD (fn facts =>
   7.249 +            fuf_tac (Classical.get_local_claset ctxt,
   7.250 +                     Simplifier.get_local_simpset ctxt) 1)) *}
   7.251 +    "free ultrafilter tactic"
   7.252 +
   7.253 +method_setup ultra = {*
   7.254 +    Method.ctxt_args (fn ctxt =>
   7.255 +        Method.METHOD (fn facts =>
   7.256 +            ultra_tac (Classical.get_local_claset ctxt,
   7.257 +                       Simplifier.get_local_simpset ctxt) 1)) *}
   7.258 +    "ultrafilter tactic"
   7.259 +
   7.260 +
   7.261 +(*-------------------------------------------------------
   7.262 +  Now prove one further property of our free ultrafilter
   7.263 + -------------------------------------------------------*)
   7.264 +lemma FreeUltrafilterNat_Un: "X Un Y: FreeUltrafilterNat  
   7.265 +      ==> X: FreeUltrafilterNat | Y: FreeUltrafilterNat"
   7.266 +apply auto
   7.267 +apply (ultra)
   7.268 +done
   7.269 +
   7.270 +(*-------------------------------------------------------
   7.271 +   Properties of hyprel
   7.272 + -------------------------------------------------------*)
   7.273 +
   7.274 +(** Proving that hyprel is an equivalence relation **)
   7.275 +(** Natural deduction for hyprel **)
   7.276 +
   7.277 +lemma hyprel_iff: "((X,Y): hyprel) = ({n. X n = Y n}: FreeUltrafilterNat)"
   7.278 +apply (unfold hyprel_def)
   7.279 +apply fast
   7.280 +done
   7.281 +
   7.282 +lemma hyprel_refl: "(x,x): hyprel"
   7.283 +apply (unfold hyprel_def)
   7.284 +apply (auto simp add: FreeUltrafilterNat_Nat_set)
   7.285 +done
   7.286 +
   7.287 +lemma hyprel_sym [rule_format (no_asm)]: "(x,y): hyprel --> (y,x):hyprel"
   7.288 +apply (simp add: hyprel_def eq_commute) 
   7.289 +done
   7.290 +
   7.291 +lemma hyprel_trans: 
   7.292 +      "[|(x,y): hyprel; (y,z):hyprel|] ==> (x,z):hyprel"
   7.293 +apply (unfold hyprel_def)
   7.294 +apply auto
   7.295 +apply (ultra)
   7.296 +done
   7.297 +
   7.298 +lemma equiv_hyprel: "equiv UNIV hyprel"
   7.299 +apply (simp add: equiv_def refl_def sym_def trans_def hyprel_refl)
   7.300 +apply (blast intro: hyprel_sym hyprel_trans) 
   7.301 +done
   7.302 +
   7.303 +(* (hyprel `` {x} = hyprel `` {y}) = ((x,y) \<in> hyprel) *)
   7.304 +lemmas equiv_hyprel_iff =
   7.305 +    eq_equiv_class_iff [OF equiv_hyprel UNIV_I UNIV_I, simp] 
   7.306 +
   7.307 +lemma hyprel_in_hypreal: "hyprel``{x}:hypreal"
   7.308 +apply (unfold hypreal_def hyprel_def quotient_def)
   7.309 +apply blast
   7.310 +done
   7.311 +
   7.312 +lemma inj_on_Abs_hypreal: "inj_on Abs_hypreal hypreal"
   7.313 +apply (rule inj_on_inverseI)
   7.314 +apply (erule Abs_hypreal_inverse)
   7.315 +done
   7.316 +
   7.317 +declare inj_on_Abs_hypreal [THEN inj_on_iff, simp] 
   7.318 +        hyprel_in_hypreal [simp] Abs_hypreal_inverse [simp]
   7.319 +
   7.320 +declare equiv_hyprel [THEN eq_equiv_class_iff, simp]
   7.321 +
   7.322 +declare hyprel_iff [iff]
   7.323 +
   7.324 +lemmas eq_hyprelD = eq_equiv_class [OF _ equiv_hyprel]
   7.325 +
   7.326 +lemma inj_Rep_hypreal: "inj(Rep_hypreal)"
   7.327 +apply (rule inj_on_inverseI)
   7.328 +apply (rule Rep_hypreal_inverse)
   7.329 +done
   7.330 +
   7.331 +lemma lemma_hyprel_refl: "x \<in> hyprel `` {x}"
   7.332 +apply (unfold hyprel_def)
   7.333 +apply (safe)
   7.334 +apply (auto intro!: FreeUltrafilterNat_Nat_set)
   7.335 +done
   7.336 +
   7.337 +declare lemma_hyprel_refl [simp]
   7.338 +
   7.339 +lemma hypreal_empty_not_mem: "{} \<notin> hypreal"
   7.340 +apply (unfold hypreal_def)
   7.341 +apply (auto elim!: quotientE equalityCE)
   7.342 +done
   7.343 +
   7.344 +declare hypreal_empty_not_mem [simp]
   7.345 +
   7.346 +lemma Rep_hypreal_nonempty: "Rep_hypreal x \<noteq> {}"
   7.347 +apply (cut_tac x = "x" in Rep_hypreal)
   7.348 +apply auto
   7.349 +done
   7.350 +
   7.351 +declare Rep_hypreal_nonempty [simp]
   7.352 +
   7.353 +(*------------------------------------------------------------------------
   7.354 +   hypreal_of_real: the injection from real to hypreal
   7.355 + ------------------------------------------------------------------------*)
   7.356 +
   7.357 +lemma inj_hypreal_of_real: "inj(hypreal_of_real)"
   7.358 +apply (rule inj_onI)
   7.359 +apply (unfold hypreal_of_real_def)
   7.360 +apply (drule inj_on_Abs_hypreal [THEN inj_onD])
   7.361 +apply (rule hyprel_in_hypreal)+
   7.362 +apply (drule eq_equiv_class)
   7.363 +apply (rule equiv_hyprel)
   7.364 +apply (simp_all add: split: split_if_asm) 
   7.365 +done
   7.366 +
   7.367 +lemma eq_Abs_hypreal:
   7.368 +    "(!!x y. z = Abs_hypreal(hyprel``{x}) ==> P) ==> P"
   7.369 +apply (rule_tac x1=z in Rep_hypreal [unfolded hypreal_def, THEN quotientE])
   7.370 +apply (drule_tac f = "Abs_hypreal" in arg_cong)
   7.371 +apply (force simp add: Rep_hypreal_inverse)
   7.372 +done
   7.373 +
   7.374 +(**** hypreal_minus: additive inverse on hypreal ****)
   7.375 +
   7.376 +lemma hypreal_minus_congruent: 
   7.377 +  "congruent hyprel (%X. hyprel``{%n. - (X n)})"
   7.378 +by (force simp add: congruent_def)
   7.379 +
   7.380 +lemma hypreal_minus: 
   7.381 +   "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
   7.382 +apply (unfold hypreal_minus_def)
   7.383 +apply (rule_tac f = "Abs_hypreal" in arg_cong)
   7.384 +apply (simp (no_asm) add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
   7.385 +               UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
   7.386 +done
   7.387 +
   7.388 +lemma hypreal_minus_minus: "- (- z) = (z::hypreal)"
   7.389 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.390 +apply (simp (no_asm_simp) add: hypreal_minus)
   7.391 +done
   7.392 +
   7.393 +declare hypreal_minus_minus [simp]
   7.394 +
   7.395 +lemma inj_hypreal_minus: "inj(%r::hypreal. -r)"
   7.396 +apply (rule inj_onI)
   7.397 +apply (drule_tac f = "uminus" in arg_cong)
   7.398 +apply (simp add: hypreal_minus_minus)
   7.399 +done
   7.400 +
   7.401 +lemma hypreal_minus_zero: "- 0 = (0::hypreal)"
   7.402 +apply (unfold hypreal_zero_def)
   7.403 +apply (simp (no_asm) add: hypreal_minus)
   7.404 +done
   7.405 +declare hypreal_minus_zero [simp]
   7.406 +
   7.407 +lemma hypreal_minus_zero_iff: "(-x = 0) = (x = (0::hypreal))"
   7.408 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.409 +apply (auto simp add: hypreal_zero_def hypreal_minus)
   7.410 +done
   7.411 +declare hypreal_minus_zero_iff [simp]
   7.412 +
   7.413 +
   7.414 +(**** hyperreal addition: hypreal_add  ****)
   7.415 +
   7.416 +lemma hypreal_add_congruent2: 
   7.417 +    "congruent2 hyprel (%X Y. hyprel``{%n. X n + Y n})"
   7.418 +apply (unfold congruent2_def)
   7.419 +apply (auto ); 
   7.420 +apply ultra
   7.421 +done
   7.422 +
   7.423 +lemma hypreal_add: 
   7.424 +  "Abs_hypreal(hyprel``{%n. X n}) + Abs_hypreal(hyprel``{%n. Y n}) =  
   7.425 +   Abs_hypreal(hyprel``{%n. X n + Y n})"
   7.426 +apply (unfold hypreal_add_def)
   7.427 +apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_add_congruent2])
   7.428 +done
   7.429 +
   7.430 +lemma hypreal_diff: "Abs_hypreal(hyprel``{%n. X n}) - Abs_hypreal(hyprel``{%n. Y n}) =  
   7.431 +      Abs_hypreal(hyprel``{%n. X n - Y n})"
   7.432 +apply (simp (no_asm) add: hypreal_diff_def hypreal_minus hypreal_add)
   7.433 +done
   7.434 +
   7.435 +lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
   7.436 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.437 +apply (rule_tac z = "w" in eq_Abs_hypreal)
   7.438 +apply (simp (no_asm_simp) add: real_add_ac hypreal_add)
   7.439 +done
   7.440 +
   7.441 +lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
   7.442 +apply (rule_tac z = "z1" in eq_Abs_hypreal)
   7.443 +apply (rule_tac z = "z2" in eq_Abs_hypreal)
   7.444 +apply (rule_tac z = "z3" in eq_Abs_hypreal)
   7.445 +apply (simp (no_asm_simp) add: hypreal_add real_add_assoc)
   7.446 +done
   7.447 +
   7.448 +(*For AC rewriting*)
   7.449 +lemma hypreal_add_left_commute: "(x::hypreal)+(y+z)=y+(x+z)"
   7.450 +  apply (rule mk_left_commute [of "op +"])
   7.451 +  apply (rule hypreal_add_assoc)
   7.452 +  apply (rule hypreal_add_commute)
   7.453 +  done
   7.454 +
   7.455 +(* hypreal addition is an AC operator *)
   7.456 +lemmas hypreal_add_ac =
   7.457 +       hypreal_add_assoc hypreal_add_commute hypreal_add_left_commute
   7.458 +
   7.459 +lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
   7.460 +apply (unfold hypreal_zero_def)
   7.461 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.462 +apply (simp add: hypreal_add)
   7.463 +done
   7.464 +
   7.465 +lemma hypreal_add_zero_right: "z + (0::hypreal) = z"
   7.466 +apply (simp (no_asm) add: hypreal_add_zero_left hypreal_add_commute)
   7.467 +done
   7.468 +
   7.469 +lemma hypreal_add_minus: "z + -z = (0::hypreal)"
   7.470 +apply (unfold hypreal_zero_def)
   7.471 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.472 +apply (simp add: hypreal_minus hypreal_add)
   7.473 +done
   7.474 +
   7.475 +lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
   7.476 +apply (simp (no_asm) add: hypreal_add_commute hypreal_add_minus)
   7.477 +done
   7.478 +
   7.479 +declare hypreal_add_minus [simp] hypreal_add_minus_left [simp]
   7.480 +    hypreal_add_zero_left [simp] hypreal_add_zero_right [simp] 
   7.481 +
   7.482 +lemma hypreal_minus_ex: "\<exists>y. (x::hypreal) + y = 0"
   7.483 +apply (fast intro: hypreal_add_minus)
   7.484 +done
   7.485 +
   7.486 +lemma hypreal_minus_ex1: "EX! y. (x::hypreal) + y = 0"
   7.487 +apply (auto intro: hypreal_add_minus)
   7.488 +apply (drule_tac f = "%x. ya+x" in arg_cong)
   7.489 +apply (simp add: hypreal_add_assoc [symmetric])
   7.490 +apply (simp add: hypreal_add_commute)
   7.491 +done
   7.492 +
   7.493 +lemma hypreal_minus_left_ex1: "EX! y. y + (x::hypreal) = 0"
   7.494 +apply (auto intro: hypreal_add_minus_left)
   7.495 +apply (drule_tac f = "%x. x+ya" in arg_cong)
   7.496 +apply (simp add: hypreal_add_assoc)
   7.497 +apply (simp add: hypreal_add_commute)
   7.498 +done
   7.499 +
   7.500 +lemma hypreal_add_minus_eq_minus: "x + y = (0::hypreal) ==> x = -y"
   7.501 +apply (cut_tac z = "y" in hypreal_add_minus_left)
   7.502 +apply (rule_tac x1 = "y" in hypreal_minus_left_ex1 [THEN ex1E])
   7.503 +apply blast
   7.504 +done
   7.505 +
   7.506 +lemma hypreal_as_add_inverse_ex: "\<exists>y::hypreal. x = -y"
   7.507 +apply (cut_tac x = "x" in hypreal_minus_ex)
   7.508 +apply (erule exE , drule hypreal_add_minus_eq_minus)
   7.509 +apply fast
   7.510 +done
   7.511 +
   7.512 +lemma hypreal_minus_add_distrib: "-(x + (y::hypreal)) = -x + -y"
   7.513 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.514 +apply (rule_tac z = "y" in eq_Abs_hypreal)
   7.515 +apply (auto simp add: hypreal_minus hypreal_add real_minus_add_distrib)
   7.516 +done
   7.517 +declare hypreal_minus_add_distrib [simp]
   7.518 +
   7.519 +lemma hypreal_minus_distrib1: "-(y + -(x::hypreal)) = x + -y"
   7.520 +apply (simp (no_asm) add: hypreal_add_commute)
   7.521 +done
   7.522 +
   7.523 +lemma hypreal_add_left_cancel: "((x::hypreal) + y = x + z) = (y = z)"
   7.524 +apply (safe)
   7.525 +apply (drule_tac f = "%t.-x + t" in arg_cong)
   7.526 +apply (simp add: hypreal_add_assoc [symmetric])
   7.527 +done
   7.528 +
   7.529 +lemma hypreal_add_right_cancel: "(y + (x::hypreal)= z + x) = (y = z)"
   7.530 +apply (simp (no_asm) add: hypreal_add_commute hypreal_add_left_cancel)
   7.531 +done
   7.532 +
   7.533 +lemma hypreal_add_minus_cancelA: "z + ((- z) + w) = (w::hypreal)"
   7.534 +apply (simp (no_asm) add: hypreal_add_assoc [symmetric])
   7.535 +done
   7.536 +
   7.537 +lemma hypreal_minus_add_cancelA: "(-z) + (z + w) = (w::hypreal)"
   7.538 +apply (simp (no_asm) add: hypreal_add_assoc [symmetric])
   7.539 +done
   7.540 +
   7.541 +declare hypreal_add_minus_cancelA [simp] hypreal_minus_add_cancelA [simp]
   7.542 +
   7.543 +(**** hyperreal multiplication: hypreal_mult  ****)
   7.544 +
   7.545 +lemma hypreal_mult_congruent2: 
   7.546 +    "congruent2 hyprel (%X Y. hyprel``{%n. X n * Y n})"
   7.547 +apply (unfold congruent2_def)
   7.548 +apply auto
   7.549 +apply (ultra)
   7.550 +done
   7.551 +
   7.552 +lemma hypreal_mult: 
   7.553 +  "Abs_hypreal(hyprel``{%n. X n}) * Abs_hypreal(hyprel``{%n. Y n}) =  
   7.554 +   Abs_hypreal(hyprel``{%n. X n * Y n})"
   7.555 +apply (unfold hypreal_mult_def)
   7.556 +apply (simp add: UN_equiv_class2 [OF equiv_hyprel hypreal_mult_congruent2])
   7.557 +done
   7.558 +
   7.559 +lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
   7.560 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.561 +apply (rule_tac z = "w" in eq_Abs_hypreal)
   7.562 +apply (simp (no_asm_simp) add: hypreal_mult real_mult_ac)
   7.563 +done
   7.564 +
   7.565 +lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
   7.566 +apply (rule_tac z = "z1" in eq_Abs_hypreal)
   7.567 +apply (rule_tac z = "z2" in eq_Abs_hypreal)
   7.568 +apply (rule_tac z = "z3" in eq_Abs_hypreal)
   7.569 +apply (simp (no_asm_simp) add: hypreal_mult real_mult_assoc)
   7.570 +done
   7.571 +
   7.572 +lemma hypreal_mult_left_commute: "(z1::hypreal) * (z2 * z3) = z2 * (z1 * z3)"
   7.573 +  apply (rule mk_left_commute [of "op *"])
   7.574 +  apply (rule hypreal_mult_assoc)
   7.575 +  apply (rule hypreal_mult_commute)
   7.576 +  done
   7.577 +
   7.578 +(* hypreal multiplication is an AC operator *)
   7.579 +lemmas hypreal_mult_ac =
   7.580 +       hypreal_mult_assoc hypreal_mult_commute hypreal_mult_left_commute
   7.581 +
   7.582 +lemma hypreal_mult_1: "(1::hypreal) * z = z"
   7.583 +apply (unfold hypreal_one_def)
   7.584 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.585 +apply (simp add: hypreal_mult)
   7.586 +done
   7.587 +declare hypreal_mult_1 [simp]
   7.588 +
   7.589 +lemma hypreal_mult_1_right: "z * (1::hypreal) = z"
   7.590 +apply (simp (no_asm) add: hypreal_mult_commute hypreal_mult_1)
   7.591 +done
   7.592 +declare hypreal_mult_1_right [simp]
   7.593 +
   7.594 +lemma hypreal_mult_0: "0 * z = (0::hypreal)"
   7.595 +apply (unfold hypreal_zero_def)
   7.596 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.597 +apply (simp add: hypreal_mult)
   7.598 +done
   7.599 +declare hypreal_mult_0 [simp]
   7.600 +
   7.601 +lemma hypreal_mult_0_right: "z * 0 = (0::hypreal)"
   7.602 +apply (simp (no_asm) add: hypreal_mult_commute)
   7.603 +done
   7.604 +declare hypreal_mult_0_right [simp]
   7.605 +
   7.606 +lemma hypreal_minus_mult_eq1: "-(x * y) = -x * (y::hypreal)"
   7.607 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.608 +apply (rule_tac z = "y" in eq_Abs_hypreal)
   7.609 +apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac)
   7.610 +done
   7.611 +
   7.612 +lemma hypreal_minus_mult_eq2: "-(x * y) = (x::hypreal) * -y"
   7.613 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.614 +apply (rule_tac z = "y" in eq_Abs_hypreal)
   7.615 +apply (auto simp add: hypreal_minus hypreal_mult real_mult_ac real_add_ac)
   7.616 +done
   7.617 +
   7.618 +(*Pull negations out*)
   7.619 +declare hypreal_minus_mult_eq2 [symmetric, simp] hypreal_minus_mult_eq1 [symmetric, simp]
   7.620 +
   7.621 +lemma hypreal_mult_minus_1: "(- (1::hypreal)) * z = -z"
   7.622 +apply (simp (no_asm))
   7.623 +done
   7.624 +declare hypreal_mult_minus_1 [simp]
   7.625 +
   7.626 +lemma hypreal_mult_minus_1_right: "z * (- (1::hypreal)) = -z"
   7.627 +apply (subst hypreal_mult_commute)
   7.628 +apply (simp (no_asm))
   7.629 +done
   7.630 +declare hypreal_mult_minus_1_right [simp]
   7.631 +
   7.632 +lemma hypreal_minus_mult_commute: "(-x) * y = (x::hypreal) * -y"
   7.633 +apply auto
   7.634 +done
   7.635 +
   7.636 +(*-----------------------------------------------------------------------------
   7.637 +    A few more theorems
   7.638 + ----------------------------------------------------------------------------*)
   7.639 +lemma hypreal_add_assoc_cong: "(z::hypreal) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   7.640 +apply (simp (no_asm_simp) add: hypreal_add_assoc [symmetric])
   7.641 +done
   7.642 +
   7.643 +lemma hypreal_add_mult_distrib: "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
   7.644 +apply (rule_tac z = "z1" in eq_Abs_hypreal)
   7.645 +apply (rule_tac z = "z2" in eq_Abs_hypreal)
   7.646 +apply (rule_tac z = "w" in eq_Abs_hypreal)
   7.647 +apply (simp (no_asm_simp) add: hypreal_mult hypreal_add real_add_mult_distrib)
   7.648 +done
   7.649 +
   7.650 +lemma hypreal_add_mult_distrib2: "(w::hypreal) * (z1 + z2) = (w * z1) + (w * z2)"
   7.651 +apply (simp add: hypreal_mult_commute [of w] hypreal_add_mult_distrib)
   7.652 +done
   7.653 +
   7.654 +
   7.655 +lemma hypreal_diff_mult_distrib: "((z1::hypreal) - z2) * w = (z1 * w) - (z2 * w)"
   7.656 +
   7.657 +apply (unfold hypreal_diff_def)
   7.658 +apply (simp (no_asm) add: hypreal_add_mult_distrib)
   7.659 +done
   7.660 +
   7.661 +lemma hypreal_diff_mult_distrib2: "(w::hypreal) * (z1 - z2) = (w * z1) - (w * z2)"
   7.662 +apply (simp add: hypreal_mult_commute [of w] hypreal_diff_mult_distrib)
   7.663 +done
   7.664 +
   7.665 +(*** one and zero are distinct ***)
   7.666 +lemma hypreal_zero_not_eq_one: "0 \<noteq> (1::hypreal)"
   7.667 +apply (unfold hypreal_zero_def hypreal_one_def)
   7.668 +apply (auto simp add: real_zero_not_eq_one)
   7.669 +done
   7.670 +
   7.671 +
   7.672 +(**** multiplicative inverse on hypreal ****)
   7.673 +
   7.674 +lemma hypreal_inverse_congruent: 
   7.675 +  "congruent hyprel (%X. hyprel``{%n. if X n = 0 then 0 else inverse(X n)})"
   7.676 +apply (unfold congruent_def)
   7.677 +apply (auto , ultra)
   7.678 +done
   7.679 +
   7.680 +lemma hypreal_inverse: 
   7.681 +      "inverse (Abs_hypreal(hyprel``{%n. X n})) =  
   7.682 +       Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
   7.683 +apply (unfold hypreal_inverse_def)
   7.684 +apply (rule_tac f = "Abs_hypreal" in arg_cong)
   7.685 +apply (simp (no_asm) add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
   7.686 +           UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
   7.687 +done
   7.688 +
   7.689 +lemma HYPREAL_INVERSE_ZERO: "inverse 0 = (0::hypreal)"
   7.690 +apply (simp (no_asm) add: hypreal_inverse hypreal_zero_def)
   7.691 +done
   7.692 +
   7.693 +lemma HYPREAL_DIVISION_BY_ZERO: "a / (0::hypreal) = 0"
   7.694 +apply (simp (no_asm) add: hypreal_divide_def HYPREAL_INVERSE_ZERO)
   7.695 +done
   7.696 +
   7.697 +lemma hypreal_inverse_inverse: "inverse (inverse (z::hypreal)) = z"
   7.698 +apply (case_tac "z=0", simp add: HYPREAL_INVERSE_ZERO)
   7.699 +apply (rule_tac z = "z" in eq_Abs_hypreal)
   7.700 +apply (simp add: hypreal_inverse hypreal_zero_def)
   7.701 +done
   7.702 +declare hypreal_inverse_inverse [simp]
   7.703 +
   7.704 +lemma hypreal_inverse_1: "inverse((1::hypreal)) = (1::hypreal)"
   7.705 +apply (unfold hypreal_one_def)
   7.706 +apply (simp (no_asm_use) add: hypreal_inverse real_zero_not_eq_one [THEN not_sym])
   7.707 +done
   7.708 +declare hypreal_inverse_1 [simp]
   7.709 +
   7.710 +
   7.711 +(*** existence of inverse ***)
   7.712 +
   7.713 +lemma hypreal_mult_inverse: 
   7.714 +     "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
   7.715 +
   7.716 +apply (unfold hypreal_one_def hypreal_zero_def)
   7.717 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.718 +apply (simp add: hypreal_inverse hypreal_mult)
   7.719 +apply (drule FreeUltrafilterNat_Compl_mem)
   7.720 +apply (blast intro!: real_mult_inv_right FreeUltrafilterNat_subset)
   7.721 +done
   7.722 +
   7.723 +lemma hypreal_mult_inverse_left: "x \<noteq> 0 ==> inverse(x)*x = (1::hypreal)"
   7.724 +apply (simp (no_asm_simp) add: hypreal_mult_inverse hypreal_mult_commute)
   7.725 +done
   7.726 +
   7.727 +lemma hypreal_mult_left_cancel: "(c::hypreal) \<noteq> 0 ==> (c*a=c*b) = (a=b)"
   7.728 +apply auto
   7.729 +apply (drule_tac f = "%x. x*inverse c" in arg_cong)
   7.730 +apply (simp add: hypreal_mult_inverse hypreal_mult_ac)
   7.731 +done
   7.732 +    
   7.733 +lemma hypreal_mult_right_cancel: "(c::hypreal) \<noteq> 0 ==> (a*c=b*c) = (a=b)"
   7.734 +apply (safe)
   7.735 +apply (drule_tac f = "%x. x*inverse c" in arg_cong)
   7.736 +apply (simp add: hypreal_mult_inverse hypreal_mult_ac)
   7.737 +done
   7.738 +
   7.739 +lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0"
   7.740 +apply (unfold hypreal_zero_def)
   7.741 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.742 +apply (simp add: hypreal_inverse hypreal_mult)
   7.743 +done
   7.744 +
   7.745 +declare hypreal_mult_inverse [simp] hypreal_mult_inverse_left [simp]
   7.746 +
   7.747 +lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)"
   7.748 +apply (safe)
   7.749 +apply (drule_tac f = "%z. inverse x*z" in arg_cong)
   7.750 +apply (simp add: hypreal_mult_assoc [symmetric])
   7.751 +done
   7.752 +
   7.753 +lemma hypreal_mult_zero_disj: "x*y = (0::hypreal) ==> x = 0 | y = 0"
   7.754 +apply (auto intro: ccontr dest: hypreal_mult_not_0)
   7.755 +done
   7.756 +
   7.757 +lemma hypreal_minus_inverse: "inverse(-x) = -inverse(x::hypreal)"
   7.758 +apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO)
   7.759 +apply (rule hypreal_mult_right_cancel [of "-x", THEN iffD1]) 
   7.760 +apply (simp add: ); 
   7.761 +apply (subst hypreal_mult_inverse_left)
   7.762 +apply auto
   7.763 +done
   7.764 +
   7.765 +lemma hypreal_inverse_distrib: "inverse(x*y) = inverse(x)*inverse(y::hypreal)"
   7.766 +apply (case_tac "x=0", simp add: HYPREAL_INVERSE_ZERO)
   7.767 +apply (case_tac "y=0", simp add: HYPREAL_INVERSE_ZERO)
   7.768 +apply (frule_tac y = "y" in hypreal_mult_not_0 , assumption)
   7.769 +apply (rule_tac c1 = "x" in hypreal_mult_left_cancel [THEN iffD1])
   7.770 +apply (auto simp add: hypreal_mult_assoc [symmetric])
   7.771 +apply (rule_tac c1 = "y" in hypreal_mult_left_cancel [THEN iffD1])
   7.772 +apply (auto simp add: hypreal_mult_left_commute)
   7.773 +apply (simp (no_asm_simp) add: hypreal_mult_assoc [symmetric])
   7.774 +done
   7.775 +
   7.776 +(*------------------------------------------------------------------
   7.777 +                   Theorems for ordering 
   7.778 + ------------------------------------------------------------------*)
   7.779 +
   7.780 +(* prove introduction and elimination rules for hypreal_less *)
   7.781 +
   7.782 +lemma hypreal_less_iff: 
   7.783 + "(P < (Q::hypreal)) = (\<exists>X Y. X \<in> Rep_hypreal(P) &  
   7.784 +                              Y \<in> Rep_hypreal(Q) &  
   7.785 +                              {n. X n < Y n} \<in> FreeUltrafilterNat)"
   7.786 +
   7.787 +apply (unfold hypreal_less_def)
   7.788 +apply fast
   7.789 +done
   7.790 +
   7.791 +lemma hypreal_lessI: 
   7.792 + "[| {n. X n < Y n} \<in> FreeUltrafilterNat;  
   7.793 +          X \<in> Rep_hypreal(P);  
   7.794 +          Y \<in> Rep_hypreal(Q) |] ==> P < (Q::hypreal)"
   7.795 +apply (unfold hypreal_less_def)
   7.796 +apply fast
   7.797 +done
   7.798 +
   7.799 +
   7.800 +lemma hypreal_lessE: 
   7.801 +     "!! R1. [| R1 < (R2::hypreal);  
   7.802 +          !!X Y. {n. X n < Y n} \<in> FreeUltrafilterNat ==> P;  
   7.803 +          !!X. X \<in> Rep_hypreal(R1) ==> P;   
   7.804 +          !!Y. Y \<in> Rep_hypreal(R2) ==> P |]  
   7.805 +      ==> P"
   7.806 +
   7.807 +apply (unfold hypreal_less_def)
   7.808 +apply auto
   7.809 +done
   7.810 +
   7.811 +lemma hypreal_lessD: 
   7.812 + "R1 < (R2::hypreal) ==> (\<exists>X Y. {n. X n < Y n} \<in> FreeUltrafilterNat &  
   7.813 +                                   X \<in> Rep_hypreal(R1) &  
   7.814 +                                   Y \<in> Rep_hypreal(R2))"
   7.815 +apply (unfold hypreal_less_def)
   7.816 +apply fast
   7.817 +done
   7.818 +
   7.819 +lemma hypreal_less_not_refl: "~ (R::hypreal) < R"
   7.820 +apply (rule_tac z = "R" in eq_Abs_hypreal)
   7.821 +apply (auto simp add: hypreal_less_def)
   7.822 +apply (ultra)
   7.823 +done
   7.824 +
   7.825 +(*** y < y ==> P ***)
   7.826 +lemmas hypreal_less_irrefl = hypreal_less_not_refl [THEN notE, standard]
   7.827 +declare hypreal_less_irrefl [elim!]
   7.828 +
   7.829 +lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
   7.830 +apply (auto simp add: hypreal_less_not_refl)
   7.831 +done
   7.832 +
   7.833 +lemma hypreal_less_trans: "!!(R1::hypreal). [| R1 < R2; R2 < R3 |] ==> R1 < R3"
   7.834 +apply (rule_tac z = "R1" in eq_Abs_hypreal)
   7.835 +apply (rule_tac z = "R2" in eq_Abs_hypreal)
   7.836 +apply (rule_tac z = "R3" in eq_Abs_hypreal)
   7.837 +apply (auto intro!: exI simp add: hypreal_less_def)
   7.838 +apply ultra
   7.839 +done
   7.840 +
   7.841 +lemma hypreal_less_asym: "!! (R1::hypreal). [| R1 < R2; R2 < R1 |] ==> P"
   7.842 +apply (drule hypreal_less_trans , assumption)
   7.843 +apply (simp add: hypreal_less_not_refl)
   7.844 +done
   7.845 +
   7.846 +(*-------------------------------------------------------
   7.847 +  TODO: The following theorem should have been proved 
   7.848 +  first and then used througout the proofs as it probably 
   7.849 +  makes many of them more straightforward. 
   7.850 + -------------------------------------------------------*)
   7.851 +lemma hypreal_less: 
   7.852 +      "(Abs_hypreal(hyprel``{%n. X n}) <  
   7.853 +            Abs_hypreal(hyprel``{%n. Y n})) =  
   7.854 +       ({n. X n < Y n} \<in> FreeUltrafilterNat)"
   7.855 +apply (unfold hypreal_less_def)
   7.856 +apply (auto intro!: lemma_hyprel_refl)
   7.857 +apply (ultra)
   7.858 +done
   7.859 +
   7.860 +(*----------------------------------------------------------------------------
   7.861 +		 Trichotomy: the hyperreals are linearly ordered
   7.862 +  ---------------------------------------------------------------------------*)
   7.863 +
   7.864 +lemma lemma_hyprel_0_mem: "\<exists>x. x: hyprel `` {%n. 0}"
   7.865 +
   7.866 +apply (unfold hyprel_def)
   7.867 +apply (rule_tac x = "%n. 0" in exI)
   7.868 +apply (safe)
   7.869 +apply (auto intro!: FreeUltrafilterNat_Nat_set)
   7.870 +done
   7.871 +
   7.872 +lemma hypreal_trichotomy: "0 <  x | x = 0 | x < (0::hypreal)"
   7.873 +apply (unfold hypreal_zero_def)
   7.874 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.875 +apply (auto simp add: hypreal_less_def)
   7.876 +apply (cut_tac lemma_hyprel_0_mem , erule exE)
   7.877 +apply (drule_tac x = "xa" in spec)
   7.878 +apply (drule_tac x = "x" in spec)
   7.879 +apply (cut_tac x = "x" in lemma_hyprel_refl)
   7.880 +apply auto
   7.881 +apply (drule_tac x = "x" in spec)
   7.882 +apply (drule_tac x = "xa" in spec)
   7.883 +apply auto
   7.884 +apply (ultra)
   7.885 +done
   7.886 +
   7.887 +lemma hypreal_trichotomyE:
   7.888 +     "[| (0::hypreal) < x ==> P;  
   7.889 +         x = 0 ==> P;  
   7.890 +         x < 0 ==> P |] ==> P"
   7.891 +apply (insert hypreal_trichotomy [of x])
   7.892 +apply (blast intro: elim:); 
   7.893 +done
   7.894 +
   7.895 +(*----------------------------------------------------------------------------
   7.896 +            More properties of <
   7.897 + ----------------------------------------------------------------------------*)
   7.898 +
   7.899 +lemma hypreal_less_minus_iff: "((x::hypreal) < y) = (0 < y + -x)"
   7.900 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.901 +apply (rule_tac z = "y" in eq_Abs_hypreal)
   7.902 +apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less)
   7.903 +done
   7.904 +
   7.905 +lemma hypreal_less_minus_iff2: "((x::hypreal) < y) = (x + -y < 0)"
   7.906 +apply (rule_tac z = "x" in eq_Abs_hypreal)
   7.907 +apply (rule_tac z = "y" in eq_Abs_hypreal)
   7.908 +apply (auto simp add: hypreal_add hypreal_zero_def hypreal_minus hypreal_less)
   7.909 +done
   7.910 +
   7.911 +lemma hypreal_eq_minus_iff: "((x::hypreal) = y) = (x + - y = 0)"
   7.912 +apply auto
   7.913 +apply (rule_tac x1 = "-y" in hypreal_add_right_cancel [THEN iffD1])
   7.914 +apply auto
   7.915 +done
   7.916 +
   7.917 +lemma hypreal_eq_minus_iff2: "((x::hypreal) = y) = (0 = y + - x)"
   7.918 +apply auto
   7.919 +apply (rule_tac x1 = "-x" in hypreal_add_right_cancel [THEN iffD1])
   7.920 +apply auto
   7.921 +done
   7.922 +
   7.923 +(* 07/00 *)
   7.924 +lemma hypreal_diff_zero: "(0::hypreal) - x = -x"
   7.925 +apply (simp (no_asm) add: hypreal_diff_def)
   7.926 +done
   7.927 +
   7.928 +lemma hypreal_diff_zero_right: "x - (0::hypreal) = x"
   7.929 +apply (simp (no_asm) add: hypreal_diff_def)
   7.930 +done
   7.931 +
   7.932 +lemma hypreal_diff_self: "x - x = (0::hypreal)"
   7.933 +apply (simp (no_asm) add: hypreal_diff_def)
   7.934 +done
   7.935 +
   7.936 +declare hypreal_diff_zero [simp] hypreal_diff_zero_right [simp] hypreal_diff_self [simp]
   7.937 +
   7.938 +lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + -z = (y::hypreal))"
   7.939 +apply (auto simp add: hypreal_add_assoc)
   7.940 +done
   7.941 +
   7.942 +lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x + -a \<noteq> (0::hypreal))"
   7.943 +apply (auto dest: hypreal_eq_minus_iff [THEN iffD2])
   7.944 +done
   7.945 +
   7.946 +
   7.947 +(*** linearity ***)
   7.948 +
   7.949 +lemma hypreal_linear: "(x::hypreal) < y | x = y | y < x"
   7.950 +apply (subst hypreal_eq_minus_iff2)
   7.951 +apply (rule_tac x1 = "x" in hypreal_less_minus_iff [THEN ssubst])
   7.952 +apply (rule_tac x1 = "y" in hypreal_less_minus_iff2 [THEN ssubst])
   7.953 +apply (rule hypreal_trichotomyE)
   7.954 +apply auto
   7.955 +done
   7.956 +
   7.957 +lemma hypreal_neq_iff: "((w::hypreal) \<noteq> z) = (w<z | z<w)"
   7.958 +apply (cut_tac hypreal_linear)
   7.959 +apply blast
   7.960 +done
   7.961 +
   7.962 +lemma hypreal_linear_less2: "!!(x::hypreal). [| x < y ==> P;  x = y ==> P;  
   7.963 +           y < x ==> P |] ==> P"
   7.964 +apply (cut_tac x = "x" and y = "y" in hypreal_linear)
   7.965 +apply auto
   7.966 +done
   7.967 +
   7.968 +(*------------------------------------------------------------------------------
   7.969 +                            Properties of <=
   7.970 + ------------------------------------------------------------------------------*)
   7.971 +(*------ hypreal le iff reals le a.e ------*)
   7.972 +
   7.973 +lemma hypreal_le: 
   7.974 +      "(Abs_hypreal(hyprel``{%n. X n}) <=  
   7.975 +            Abs_hypreal(hyprel``{%n. Y n})) =  
   7.976 +       ({n. X n <= Y n} \<in> FreeUltrafilterNat)"
   7.977 +apply (unfold hypreal_le_def real_le_def)
   7.978 +apply (auto simp add: hypreal_less)
   7.979 +apply (ultra+)
   7.980 +done
   7.981 +
   7.982 +(*---------------------------------------------------------*)
   7.983 +(*---------------------------------------------------------*)
   7.984 +lemma hypreal_leI: 
   7.985 +     "~(w < z) ==> z <= (w::hypreal)"
   7.986 +apply (unfold hypreal_le_def)
   7.987 +apply assumption
   7.988 +done
   7.989 +
   7.990 +lemma hypreal_leD: 
   7.991 +      "z<=w ==> ~(w<(z::hypreal))"
   7.992 +apply (unfold hypreal_le_def)
   7.993 +apply assumption
   7.994 +done
   7.995 +
   7.996 +lemma hypreal_less_le_iff: "(~(w < z)) = (z <= (w::hypreal))"
   7.997 +apply (fast intro!: hypreal_leI hypreal_leD)
   7.998 +done
   7.999 +
  7.1000 +lemma not_hypreal_leE: "~ z <= w ==> w<(z::hypreal)"
  7.1001 +apply (unfold hypreal_le_def)
  7.1002 +apply fast
  7.1003 +done
  7.1004 +
  7.1005 +lemma hypreal_le_imp_less_or_eq: "!!(x::hypreal). x <= y ==> x < y | x = y"
  7.1006 +apply (unfold hypreal_le_def)
  7.1007 +apply (cut_tac hypreal_linear)
  7.1008 +apply (fast elim: hypreal_less_irrefl hypreal_less_asym)
  7.1009 +done
  7.1010 +
  7.1011 +lemma hypreal_less_or_eq_imp_le: "z<w | z=w ==> z <=(w::hypreal)"
  7.1012 +apply (unfold hypreal_le_def)
  7.1013 +apply (cut_tac hypreal_linear)
  7.1014 +apply (fast elim: hypreal_less_irrefl hypreal_less_asym)
  7.1015 +done
  7.1016 +
  7.1017 +lemma hypreal_le_eq_less_or_eq: "(x <= (y::hypreal)) = (x < y | x=y)"
  7.1018 +by (blast intro!: hypreal_less_or_eq_imp_le dest: hypreal_le_imp_less_or_eq) 
  7.1019 +
  7.1020 +lemmas hypreal_le_less = hypreal_le_eq_less_or_eq
  7.1021 +
  7.1022 +lemma hypreal_le_refl: "w <= (w::hypreal)"
  7.1023 +apply (simp (no_asm) add: hypreal_le_eq_less_or_eq)
  7.1024 +done
  7.1025 +
  7.1026 +(* Axiom 'linorder_linear' of class 'linorder': *)
  7.1027 +lemma hypreal_le_linear: "(z::hypreal) <= w | w <= z"
  7.1028 +apply (simp (no_asm) add: hypreal_le_less)
  7.1029 +apply (cut_tac hypreal_linear)
  7.1030 +apply blast
  7.1031 +done
  7.1032 +
  7.1033 +lemma hypreal_le_trans: "[| i <= j; j <= k |] ==> i <= (k::hypreal)"
  7.1034 +apply (drule hypreal_le_imp_less_or_eq) 
  7.1035 +apply (drule hypreal_le_imp_less_or_eq) 
  7.1036 +apply (rule hypreal_less_or_eq_imp_le) 
  7.1037 +apply (blast intro: hypreal_less_trans) 
  7.1038 +done
  7.1039 +
  7.1040 +lemma hypreal_le_anti_sym: "[| z <= w; w <= z |] ==> z = (w::hypreal)"
  7.1041 +apply (drule hypreal_le_imp_less_or_eq) 
  7.1042 +apply (drule hypreal_le_imp_less_or_eq) 
  7.1043 +apply (fast elim: hypreal_less_irrefl hypreal_less_asym)
  7.1044 +done
  7.1045 +
  7.1046 +lemma not_less_not_eq_hypreal_less: "[| ~ y < x; y \<noteq> x |] ==> x < (y::hypreal)"
  7.1047 +apply (rule not_hypreal_leE)
  7.1048 +apply (fast dest: hypreal_le_imp_less_or_eq)
  7.1049 +done
  7.1050 +
  7.1051 +(* Axiom 'order_less_le' of class 'order': *)
  7.1052 +lemma hypreal_less_le: "((w::hypreal) < z) = (w <= z & w \<noteq> z)"
  7.1053 +apply (simp (no_asm) add: hypreal_le_def hypreal_neq_iff)
  7.1054 +apply (blast intro: hypreal_less_asym)
  7.1055 +done
  7.1056 +
  7.1057 +lemma hypreal_minus_zero_less_iff: "(0 < -R) = (R < (0::hypreal))"
  7.1058 +apply (rule_tac z = "R" in eq_Abs_hypreal)
  7.1059 +apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus)
  7.1060 +done
  7.1061 +declare hypreal_minus_zero_less_iff [simp]
  7.1062 +
  7.1063 +lemma hypreal_minus_zero_less_iff2: "(-R < 0) = ((0::hypreal) < R)"
  7.1064 +apply (rule_tac z = "R" in eq_Abs_hypreal)
  7.1065 +apply (auto simp add: hypreal_zero_def hypreal_less hypreal_minus)
  7.1066 +done
  7.1067 +declare hypreal_minus_zero_less_iff2 [simp]
  7.1068 +
  7.1069 +lemma hypreal_minus_zero_le_iff: "((0::hypreal) <= -r) = (r <= 0)"
  7.1070 +apply (unfold hypreal_le_def)
  7.1071 +apply (simp (no_asm) add: hypreal_minus_zero_less_iff2)
  7.1072 +done
  7.1073 +declare hypreal_minus_zero_le_iff [simp]
  7.1074 +
  7.1075 +lemma hypreal_minus_zero_le_iff2: "(-r <= (0::hypreal)) = (0 <= r)"
  7.1076 +apply (unfold hypreal_le_def)
  7.1077 +apply (simp (no_asm) add: hypreal_minus_zero_less_iff2)
  7.1078 +done
  7.1079 +declare hypreal_minus_zero_le_iff2 [simp]
  7.1080 +
  7.1081 +(*----------------------------------------------------------
  7.1082 +  hypreal_of_real preserves field and order properties
  7.1083 + -----------------------------------------------------------*)
  7.1084 +lemma hypreal_of_real_add: 
  7.1085 +     "hypreal_of_real (z1 + z2) = hypreal_of_real z1 + hypreal_of_real z2"
  7.1086 +apply (unfold hypreal_of_real_def)
  7.1087 +apply (simp (no_asm) add: hypreal_add hypreal_add_mult_distrib)
  7.1088 +done
  7.1089 +declare hypreal_of_real_add [simp]
  7.1090 +
  7.1091 +lemma hypreal_of_real_mult: 
  7.1092 +     "hypreal_of_real (z1 * z2) = hypreal_of_real z1 * hypreal_of_real z2"
  7.1093 +apply (unfold hypreal_of_real_def)
  7.1094 +apply (simp (no_asm) add: hypreal_mult hypreal_add_mult_distrib2)
  7.1095 +done
  7.1096 +declare hypreal_of_real_mult [simp]
  7.1097 +
  7.1098 +lemma hypreal_of_real_less_iff: 
  7.1099 +     "(hypreal_of_real z1 <  hypreal_of_real z2) = (z1 < z2)"
  7.1100 +apply (unfold hypreal_less_def hypreal_of_real_def)
  7.1101 +apply auto
  7.1102 +apply (rule_tac [2] x = "%n. z1" in exI)
  7.1103 +apply (safe)
  7.1104 +apply (rule_tac [3] x = "%n. z2" in exI)
  7.1105 +apply auto
  7.1106 +apply (rule FreeUltrafilterNat_P)
  7.1107 +apply (ultra)
  7.1108 +done
  7.1109 +declare hypreal_of_real_less_iff [simp]
  7.1110 +
  7.1111 +lemma hypreal_of_real_le_iff: 
  7.1112 +     "(hypreal_of_real z1 <= hypreal_of_real z2) = (z1 <= z2)"
  7.1113 +apply (unfold hypreal_le_def real_le_def)
  7.1114 +apply auto
  7.1115 +done
  7.1116 +declare hypreal_of_real_le_iff [simp]
  7.1117 +
  7.1118 +lemma hypreal_of_real_eq_iff: "(hypreal_of_real z1 = hypreal_of_real z2) = (z1 = z2)"
  7.1119 +apply (force intro: order_antisym hypreal_of_real_le_iff [THEN iffD1])
  7.1120 +done
  7.1121 +declare hypreal_of_real_eq_iff [simp]
  7.1122 +
  7.1123 +lemma hypreal_of_real_minus: "hypreal_of_real (-r) = - hypreal_of_real  r"
  7.1124 +apply (unfold hypreal_of_real_def)
  7.1125 +apply (auto simp add: hypreal_minus)
  7.1126 +done
  7.1127 +declare hypreal_of_real_minus [simp]
  7.1128 +
  7.1129 +lemma hypreal_of_real_one: "hypreal_of_real 1 = (1::hypreal)"
  7.1130 +apply (unfold hypreal_of_real_def hypreal_one_def)
  7.1131 +apply (simp (no_asm))
  7.1132 +done
  7.1133 +declare hypreal_of_real_one [simp]
  7.1134 +
  7.1135 +lemma hypreal_of_real_zero: "hypreal_of_real 0 = 0"
  7.1136 +apply (unfold hypreal_of_real_def hypreal_zero_def)
  7.1137 +apply (simp (no_asm))
  7.1138 +done
  7.1139 +declare hypreal_of_real_zero [simp]
  7.1140 +
  7.1141 +lemma hypreal_of_real_zero_iff: "(hypreal_of_real r = 0) = (r = 0)"
  7.1142 +apply (auto intro: FreeUltrafilterNat_P simp add: hypreal_of_real_def hypreal_zero_def FreeUltrafilterNat_Nat_set)
  7.1143 +done
  7.1144 +
  7.1145 +lemma hypreal_of_real_inverse: "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"
  7.1146 +apply (case_tac "r=0")
  7.1147 +apply (simp (no_asm_simp) add: DIVISION_BY_ZERO INVERSE_ZERO HYPREAL_INVERSE_ZERO)
  7.1148 +apply (rule_tac c1 = "hypreal_of_real r" in hypreal_mult_left_cancel [THEN iffD1])
  7.1149 +apply (auto simp add: hypreal_of_real_zero_iff hypreal_of_real_mult [symmetric])
  7.1150 +done
  7.1151 +declare hypreal_of_real_inverse [simp]
  7.1152 +
  7.1153 +lemma hypreal_of_real_divide: "hypreal_of_real (z1 / z2) = hypreal_of_real z1 / hypreal_of_real z2"
  7.1154 +apply (simp (no_asm) add: hypreal_divide_def real_divide_def)
  7.1155 +done
  7.1156 +declare hypreal_of_real_divide [simp]
  7.1157 +
  7.1158 +
  7.1159 +(*** Division lemmas ***)
  7.1160 +
  7.1161 +lemma hypreal_zero_divide: "(0::hypreal)/x = 0"
  7.1162 +apply (simp (no_asm) add: hypreal_divide_def)
  7.1163 +done
  7.1164 +
  7.1165 +lemma hypreal_divide_one: "x/(1::hypreal) = x"
  7.1166 +apply (simp (no_asm) add: hypreal_divide_def)
  7.1167 +done
  7.1168 +declare hypreal_zero_divide [simp] hypreal_divide_one [simp]
  7.1169 +
  7.1170 +lemma hypreal_times_divide1_eq: "(x::hypreal) * (y/z) = (x*y)/z"
  7.1171 +apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_assoc)
  7.1172 +done
  7.1173 +
  7.1174 +lemma hypreal_times_divide2_eq: "(y/z) * (x::hypreal) = (y*x)/z"
  7.1175 +apply (simp (no_asm) add: hypreal_divide_def hypreal_mult_ac)
  7.1176 +done
  7.1177 +
  7.1178 +declare hypreal_times_divide1_eq [simp] hypreal_times_divide2_eq [simp]
  7.1179 +
  7.1180 +lemma hypreal_divide_divide1_eq: "(x::hypreal) / (y/z) = (x*z)/y"
  7.1181 +apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_ac)
  7.1182 +done
  7.1183 +
  7.1184 +lemma hypreal_divide_divide2_eq: "((x::hypreal) / y) / z = x/(y*z)"
  7.1185 +apply (simp (no_asm) add: hypreal_divide_def hypreal_inverse_distrib hypreal_mult_assoc)
  7.1186 +done
  7.1187 +
  7.1188 +declare hypreal_divide_divide1_eq [simp] hypreal_divide_divide2_eq [simp]
  7.1189 +
  7.1190 +(** As with multiplication, pull minus signs OUT of the / operator **)
  7.1191 +
  7.1192 +lemma hypreal_minus_divide_eq: "(-x) / (y::hypreal) = - (x/y)"
  7.1193 +apply (simp (no_asm) add: hypreal_divide_def)
  7.1194 +done
  7.1195 +declare hypreal_minus_divide_eq [simp]
  7.1196 +
  7.1197 +lemma hypreal_divide_minus_eq: "(x / -(y::hypreal)) = - (x/y)"
  7.1198 +apply (simp (no_asm) add: hypreal_divide_def hypreal_minus_inverse)
  7.1199 +done
  7.1200 +declare hypreal_divide_minus_eq [simp]
  7.1201 +
  7.1202 +lemma hypreal_add_divide_distrib: "(x+y)/(z::hypreal) = x/z + y/z"
  7.1203 +apply (simp (no_asm) add: hypreal_divide_def hypreal_add_mult_distrib)
  7.1204 +done
  7.1205 +
  7.1206 +lemma hypreal_inverse_add: "[|(x::hypreal) \<noteq> 0;  y \<noteq> 0 |]   
  7.1207 +      ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)"
  7.1208 +apply (simp add: hypreal_inverse_distrib hypreal_add_mult_distrib hypreal_mult_assoc [symmetric])
  7.1209 +apply (subst hypreal_mult_assoc)
  7.1210 +apply (rule hypreal_mult_left_commute [THEN subst])
  7.1211 +apply (simp add: hypreal_add_commute)
  7.1212 +done
  7.1213 +
  7.1214 +lemma hypreal_self_eq_minus_self_zero: "x = -x ==> x = (0::hypreal)"
  7.1215 +apply (rule_tac z = "x" in eq_Abs_hypreal)
  7.1216 +apply (auto simp add: hypreal_minus hypreal_zero_def)
  7.1217 +apply (ultra)
  7.1218 +done
  7.1219 +
  7.1220 +lemma hypreal_add_self_zero_cancel: "(x + x = 0) = (x = (0::hypreal))"
  7.1221 +apply (rule_tac z = "x" in eq_Abs_hypreal)
  7.1222 +apply (auto simp add: hypreal_add hypreal_zero_def)
  7.1223 +done
  7.1224 +declare hypreal_add_self_zero_cancel [simp]
  7.1225 +
  7.1226 +lemma hypreal_add_self_zero_cancel2: "(x + x + y = y) = (x = (0::hypreal))"
  7.1227 +apply auto
  7.1228 +apply (drule hypreal_eq_minus_iff [THEN iffD1])
  7.1229 +apply (auto simp add: hypreal_add_assoc hypreal_self_eq_minus_self_zero)
  7.1230 +done
  7.1231 +declare hypreal_add_self_zero_cancel2 [simp]
  7.1232 +
  7.1233 +lemma hypreal_add_self_zero_cancel2a: "(x + (x + y) = y) = (x = (0::hypreal))"
  7.1234 +apply (simp (no_asm) add: hypreal_add_assoc [symmetric])
  7.1235 +done
  7.1236 +declare hypreal_add_self_zero_cancel2a [simp]
  7.1237 +
  7.1238 +lemma hypreal_minus_eq_swap: "(b = -a) = (-b = (a::hypreal))"
  7.1239 +apply auto
  7.1240 +done
  7.1241 +
  7.1242 +lemma hypreal_minus_eq_cancel: "(-b = -a) = (b = (a::hypreal))"
  7.1243 +apply (simp add: hypreal_minus_eq_swap)
  7.1244 +done
  7.1245 +declare hypreal_minus_eq_cancel [simp]
  7.1246 +
  7.1247 +lemma hypreal_less_eq_diff: "(x<y) = (x-y < (0::hypreal))"
  7.1248 +apply (unfold hypreal_diff_def)
  7.1249 +apply (rule hypreal_less_minus_iff2)
  7.1250 +done
  7.1251 +
  7.1252 +(*** Subtraction laws ***)
  7.1253 +
  7.1254 +lemma hypreal_add_diff_eq: "x + (y - z) = (x + y) - (z::hypreal)"
  7.1255 +apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  7.1256 +done
  7.1257 +
  7.1258 +lemma hypreal_diff_add_eq: "(x - y) + z = (x + z) - (y::hypreal)"
  7.1259 +apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  7.1260 +done
  7.1261 +
  7.1262 +lemma hypreal_diff_diff_eq: "(x - y) - z = x - (y + (z::hypreal))"
  7.1263 +apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  7.1264 +done
  7.1265 +
  7.1266 +lemma hypreal_diff_diff_eq2: "x - (y - z) = (x + z) - (y::hypreal)"
  7.1267 +apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  7.1268 +done
  7.1269 +
  7.1270 +lemma hypreal_diff_less_eq: "(x-y < z) = (x < z + (y::hypreal))"
  7.1271 +apply (subst hypreal_less_eq_diff)
  7.1272 +apply (rule_tac y1 = "z" in hypreal_less_eq_diff [THEN ssubst])
  7.1273 +apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  7.1274 +done
  7.1275 +
  7.1276 +lemma hypreal_less_diff_eq: "(x < z-y) = (x + (y::hypreal) < z)"
  7.1277 +apply (subst hypreal_less_eq_diff)
  7.1278 +apply (rule_tac y1 = "z-y" in hypreal_less_eq_diff [THEN ssubst])
  7.1279 +apply (simp (no_asm) add: hypreal_diff_def hypreal_add_ac)
  7.1280 +done
  7.1281 +
  7.1282 +lemma hypreal_diff_le_eq: "(x-y <= z) = (x <= z + (y::hypreal))"
  7.1283 +apply (unfold hypreal_le_def)
  7.1284 +apply (simp (no_asm) add: hypreal_less_diff_eq)
  7.1285 +done
  7.1286 +
  7.1287 +lemma hypreal_le_diff_eq: "(x <= z-y) = (x + (y::hypreal) <= z)"
  7.1288 +apply (unfold hypreal_le_def)
  7.1289 +apply (simp (no_asm) add: hypreal_diff_less_eq)
  7.1290 +done
  7.1291 +
  7.1292 +lemma hypreal_diff_eq_eq: "(x-y = z) = (x = z + (y::hypreal))"
  7.1293 +apply (unfold hypreal_diff_def)
  7.1294 +apply (auto simp add: hypreal_add_assoc)
  7.1295 +done
  7.1296 +
  7.1297 +lemma hypreal_eq_diff_eq: "(x = z-y) = (x + (y::hypreal) = z)"
  7.1298 +apply (unfold hypreal_diff_def)
  7.1299 +apply (auto simp add: hypreal_add_assoc)
  7.1300 +done
  7.1301 +
  7.1302 +
  7.1303 +(** For the cancellation simproc.
  7.1304 +    The idea is to cancel like terms on opposite sides by subtraction **)
  7.1305 +
  7.1306 +lemma hypreal_less_eqI: "(x::hypreal) - y = x' - y' ==> (x<y) = (x'<y')"
  7.1307 +apply (subst hypreal_less_eq_diff)
  7.1308 +apply (rule_tac y1 = "y" in hypreal_less_eq_diff [THEN ssubst])
  7.1309 +apply (simp (no_asm_simp))
  7.1310 +done
  7.1311 +
  7.1312 +lemma hypreal_le_eqI: "(x::hypreal) - y = x' - y' ==> (y<=x) = (y'<=x')"
  7.1313 +apply (drule hypreal_less_eqI)
  7.1314 +apply (simp (no_asm_simp) add: hypreal_le_def)
  7.1315 +done
  7.1316 +
  7.1317 +lemma hypreal_eq_eqI: "(x::hypreal) - y = x' - y' ==> (x=y) = (x'=y')"
  7.1318 +apply safe
  7.1319 +apply (simp_all add: hypreal_eq_diff_eq hypreal_diff_eq_eq)
  7.1320 +done
  7.1321 +
  7.1322 +lemma hypreal_zero_num: "0 = Abs_hypreal (hyprel `` {%n. 0})"
  7.1323 +apply (simp (no_asm) add: hypreal_zero_def [THEN meta_eq_to_obj_eq, symmetric])
  7.1324 +done
  7.1325 +
  7.1326 +lemma hypreal_one_num: "1 = Abs_hypreal (hyprel `` {%n. 1})"
  7.1327 +apply (simp (no_asm) add: hypreal_one_def [THEN meta_eq_to_obj_eq, symmetric])
  7.1328 +done
  7.1329 +
  7.1330 +lemma hypreal_omega_gt_zero: "0 < omega"
  7.1331 +apply (unfold omega_def)
  7.1332 +apply (auto simp add: hypreal_less hypreal_zero_num)
  7.1333 +done
  7.1334 +declare hypreal_omega_gt_zero [simp]
  7.1335 +
  7.1336 +ML
  7.1337 +{*
  7.1338 +val hypreal_zero_def = thm "hypreal_zero_def";
  7.1339 +val hypreal_one_def = thm "hypreal_one_def";
  7.1340 +val hypreal_minus_def = thm "hypreal_minus_def";
  7.1341 +val hypreal_diff_def = thm "hypreal_diff_def";
  7.1342 +val hypreal_inverse_def = thm "hypreal_inverse_def";
  7.1343 +val hypreal_divide_def = thm "hypreal_divide_def";
  7.1344 +val hypreal_of_real_def = thm "hypreal_of_real_def";
  7.1345 +val omega_def = thm "omega_def";
  7.1346 +val epsilon_def = thm "epsilon_def";
  7.1347 +val hypreal_add_def = thm "hypreal_add_def";
  7.1348 +val hypreal_mult_def = thm "hypreal_mult_def";
  7.1349 +val hypreal_less_def = thm "hypreal_less_def";
  7.1350 +val hypreal_le_def = thm "hypreal_le_def";
  7.1351 +
  7.1352 +val finite_exhausts = thm "finite_exhausts";
  7.1353 +val finite_not_covers = thm "finite_not_covers";
  7.1354 +val not_finite_nat = thm "not_finite_nat";
  7.1355 +val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex";
  7.1356 +val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem";
  7.1357 +val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite";
  7.1358 +val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite";
  7.1359 +val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty";
  7.1360 +val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int";
  7.1361 +val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset";
  7.1362 +val FreeUltrafilterNat_Compl = thm "FreeUltrafilterNat_Compl";
  7.1363 +val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem";
  7.1364 +val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1";
  7.1365 +val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2";
  7.1366 +val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV";
  7.1367 +val FreeUltrafilterNat_Nat_set = thm "FreeUltrafilterNat_Nat_set";
  7.1368 +val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl";
  7.1369 +val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P";
  7.1370 +val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
  7.1371 +val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all";
  7.1372 +val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un";
  7.1373 +val hyprel_iff = thm "hyprel_iff";
  7.1374 +val hyprel_refl = thm "hyprel_refl";
  7.1375 +val hyprel_sym = thm "hyprel_sym";
  7.1376 +val hyprel_trans = thm "hyprel_trans";
  7.1377 +val equiv_hyprel = thm "equiv_hyprel";
  7.1378 +val hyprel_in_hypreal = thm "hyprel_in_hypreal";
  7.1379 +val Abs_hypreal_inverse = thm "Abs_hypreal_inverse";
  7.1380 +val inj_on_Abs_hypreal = thm "inj_on_Abs_hypreal";
  7.1381 +val inj_Rep_hypreal = thm "inj_Rep_hypreal";
  7.1382 +val lemma_hyprel_refl = thm "lemma_hyprel_refl";
  7.1383 +val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
  7.1384 +val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
  7.1385 +val inj_hypreal_of_real = thm "inj_hypreal_of_real";
  7.1386 +val eq_Abs_hypreal = thm "eq_Abs_hypreal";
  7.1387 +val hypreal_minus_congruent = thm "hypreal_minus_congruent";
  7.1388 +val hypreal_minus = thm "hypreal_minus";
  7.1389 +val hypreal_minus_minus = thm "hypreal_minus_minus";
  7.1390 +val inj_hypreal_minus = thm "inj_hypreal_minus";
  7.1391 +val hypreal_minus_zero = thm "hypreal_minus_zero";
  7.1392 +val hypreal_minus_zero_iff = thm "hypreal_minus_zero_iff";
  7.1393 +val hypreal_add_congruent2 = thm "hypreal_add_congruent2";
  7.1394 +val hypreal_add = thm "hypreal_add";
  7.1395 +val hypreal_diff = thm "hypreal_diff";
  7.1396 +val hypreal_add_commute = thm "hypreal_add_commute";
  7.1397 +val hypreal_add_assoc = thm "hypreal_add_assoc";
  7.1398 +val hypreal_add_left_commute = thm "hypreal_add_left_commute";
  7.1399 +val hypreal_add_zero_left = thm "hypreal_add_zero_left";
  7.1400 +val hypreal_add_zero_right = thm "hypreal_add_zero_right";
  7.1401 +val hypreal_add_minus = thm "hypreal_add_minus";
  7.1402 +val hypreal_add_minus_left = thm "hypreal_add_minus_left";
  7.1403 +val hypreal_minus_ex = thm "hypreal_minus_ex";
  7.1404 +val hypreal_minus_ex1 = thm "hypreal_minus_ex1";
  7.1405 +val hypreal_minus_left_ex1 = thm "hypreal_minus_left_ex1";
  7.1406 +val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
  7.1407 +val hypreal_as_add_inverse_ex = thm "hypreal_as_add_inverse_ex";
  7.1408 +val hypreal_minus_add_distrib = thm "hypreal_minus_add_distrib";
  7.1409 +val hypreal_minus_distrib1 = thm "hypreal_minus_distrib1";
  7.1410 +val hypreal_add_left_cancel = thm "hypreal_add_left_cancel";
  7.1411 +val hypreal_add_right_cancel = thm "hypreal_add_right_cancel";
  7.1412 +val hypreal_add_minus_cancelA = thm "hypreal_add_minus_cancelA";
  7.1413 +val hypreal_minus_add_cancelA = thm "hypreal_minus_add_cancelA";
  7.1414 +val hypreal_mult_congruent2 = thm "hypreal_mult_congruent2";
  7.1415 +val hypreal_mult = thm "hypreal_mult";
  7.1416 +val hypreal_mult_commute = thm "hypreal_mult_commute";
  7.1417 +val hypreal_mult_assoc = thm "hypreal_mult_assoc";
  7.1418 +val hypreal_mult_left_commute = thm "hypreal_mult_left_commute";
  7.1419 +val hypreal_mult_1 = thm "hypreal_mult_1";
  7.1420 +val hypreal_mult_1_right = thm "hypreal_mult_1_right";
  7.1421 +val hypreal_mult_0 = thm "hypreal_mult_0";
  7.1422 +val hypreal_mult_0_right = thm "hypreal_mult_0_right";
  7.1423 +val hypreal_minus_mult_eq1 = thm "hypreal_minus_mult_eq1";
  7.1424 +val hypreal_minus_mult_eq2 = thm "hypreal_minus_mult_eq2";
  7.1425 +val hypreal_mult_minus_1 = thm "hypreal_mult_minus_1";
  7.1426 +val hypreal_mult_minus_1_right = thm "hypreal_mult_minus_1_right";
  7.1427 +val hypreal_minus_mult_commute = thm "hypreal_minus_mult_commute";
  7.1428 +val hypreal_add_assoc_cong = thm "hypreal_add_assoc_cong";
  7.1429 +val hypreal_add_mult_distrib = thm "hypreal_add_mult_distrib";
  7.1430 +val hypreal_add_mult_distrib2 = thm "hypreal_add_mult_distrib2";
  7.1431 +val hypreal_diff_mult_distrib = thm "hypreal_diff_mult_distrib";
  7.1432 +val hypreal_diff_mult_distrib2 = thm "hypreal_diff_mult_distrib2";
  7.1433 +val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one";
  7.1434 +val hypreal_inverse_congruent = thm "hypreal_inverse_congruent";
  7.1435 +val hypreal_inverse = thm "hypreal_inverse";
  7.1436 +val HYPREAL_INVERSE_ZERO = thm "HYPREAL_INVERSE_ZERO";
  7.1437 +val HYPREAL_DIVISION_BY_ZERO = thm "HYPREAL_DIVISION_BY_ZERO";
  7.1438 +val hypreal_inverse_inverse = thm "hypreal_inverse_inverse";
  7.1439 +val hypreal_inverse_1 = thm "hypreal_inverse_1";
  7.1440 +val hypreal_mult_inverse = thm "hypreal_mult_inverse";
  7.1441 +val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left";
  7.1442 +val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel";
  7.1443 +val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel";
  7.1444 +val hypreal_inverse_not_zero = thm "hypreal_inverse_not_zero";
  7.1445 +val hypreal_mult_not_0 = thm "hypreal_mult_not_0";
  7.1446 +val hypreal_mult_zero_disj = thm "hypreal_mult_zero_disj";
  7.1447 +val hypreal_minus_inverse = thm "hypreal_minus_inverse";
  7.1448 +val hypreal_inverse_distrib = thm "hypreal_inverse_distrib";
  7.1449 +val hypreal_less_iff = thm "hypreal_less_iff";
  7.1450 +val hypreal_lessI = thm "hypreal_lessI";
  7.1451 +val hypreal_lessE = thm "hypreal_lessE";
  7.1452 +val hypreal_lessD = thm "hypreal_lessD";
  7.1453 +val hypreal_less_not_refl = thm "hypreal_less_not_refl";
  7.1454 +val hypreal_not_refl2 = thm "hypreal_not_refl2";
  7.1455 +val hypreal_less_trans = thm "hypreal_less_trans";
  7.1456 +val hypreal_less_asym = thm "hypreal_less_asym";
  7.1457 +val hypreal_less = thm "hypreal_less";
  7.1458 +val hypreal_trichotomy = thm "hypreal_trichotomy";
  7.1459 +val hypreal_trichotomyE = thm "hypreal_trichotomyE";
  7.1460 +val hypreal_less_minus_iff = thm "hypreal_less_minus_iff";
  7.1461 +val hypreal_less_minus_iff2 = thm "hypreal_less_minus_iff2";
  7.1462 +val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff";
  7.1463 +val hypreal_eq_minus_iff2 = thm "hypreal_eq_minus_iff2";
  7.1464 +val hypreal_diff_zero = thm "hypreal_diff_zero";
  7.1465 +val hypreal_diff_zero_right = thm "hypreal_diff_zero_right";
  7.1466 +val hypreal_diff_self = thm "hypreal_diff_self";
  7.1467 +val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3";
  7.1468 +val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff";
  7.1469 +val hypreal_linear = thm "hypreal_linear";
  7.1470 +val hypreal_neq_iff = thm "hypreal_neq_iff";
  7.1471 +val hypreal_linear_less2 = thm "hypreal_linear_less2";
  7.1472 +val hypreal_le = thm "hypreal_le";
  7.1473 +val hypreal_leI = thm "hypreal_leI";
  7.1474 +val hypreal_leD = thm "hypreal_leD";
  7.1475 +val hypreal_less_le_iff = thm "hypreal_less_le_iff";
  7.1476 +val not_hypreal_leE = thm "not_hypreal_leE";
  7.1477 +val hypreal_le_imp_less_or_eq = thm "hypreal_le_imp_less_or_eq";
  7.1478 +val hypreal_less_or_eq_imp_le = thm "hypreal_less_or_eq_imp_le";
  7.1479 +val hypreal_le_eq_less_or_eq = thm "hypreal_le_eq_less_or_eq";
  7.1480 +val hypreal_le_refl = thm "hypreal_le_refl";
  7.1481 +val hypreal_le_linear = thm "hypreal_le_linear";
  7.1482 +val hypreal_le_trans = thm "hypreal_le_trans";
  7.1483 +val hypreal_le_anti_sym = thm "hypreal_le_anti_sym";
  7.1484 +val not_less_not_eq_hypreal_less = thm "not_less_not_eq_hypreal_less";
  7.1485 +val hypreal_less_le = thm "hypreal_less_le";
  7.1486 +val hypreal_minus_zero_less_iff = thm "hypreal_minus_zero_less_iff";
  7.1487 +val hypreal_minus_zero_less_iff2 = thm "hypreal_minus_zero_less_iff2";
  7.1488 +val hypreal_minus_zero_le_iff = thm "hypreal_minus_zero_le_iff";
  7.1489 +val hypreal_minus_zero_le_iff2 = thm "hypreal_minus_zero_le_iff2";
  7.1490 +val hypreal_of_real_add = thm "hypreal_of_real_add";
  7.1491 +val hypreal_of_real_mult = thm "hypreal_of_real_mult";
  7.1492 +val hypreal_of_real_less_iff = thm "hypreal_of_real_less_iff";
  7.1493 +val hypreal_of_real_le_iff = thm "hypreal_of_real_le_iff";
  7.1494 +val hypreal_of_real_eq_iff = thm "hypreal_of_real_eq_iff";
  7.1495 +val hypreal_of_real_minus = thm "hypreal_of_real_minus";
  7.1496 +val hypreal_of_real_one = thm "hypreal_of_real_one";
  7.1497 +val hypreal_of_real_zero = thm "hypreal_of_real_zero";
  7.1498 +val hypreal_of_real_zero_iff = thm "hypreal_of_real_zero_iff";
  7.1499 +val hypreal_of_real_inverse = thm "hypreal_of_real_inverse";
  7.1500 +val hypreal_of_real_divide = thm "hypreal_of_real_divide";
  7.1501 +val hypreal_zero_divide = thm "hypreal_zero_divide";
  7.1502 +val hypreal_divide_one = thm "hypreal_divide_one";
  7.1503 +val hypreal_times_divide1_eq = thm "hypreal_times_divide1_eq";
  7.1504 +val hypreal_times_divide2_eq = thm "hypreal_times_divide2_eq";
  7.1505 +val hypreal_divide_divide1_eq = thm "hypreal_divide_divide1_eq";
  7.1506 +val hypreal_divide_divide2_eq = thm "hypreal_divide_divide2_eq";
  7.1507 +val hypreal_minus_divide_eq = thm "hypreal_minus_divide_eq";
  7.1508 +val hypreal_divide_minus_eq = thm "hypreal_divide_minus_eq";
  7.1509 +val hypreal_add_divide_distrib = thm "hypreal_add_divide_distrib";
  7.1510 +val hypreal_inverse_add = thm "hypreal_inverse_add";
  7.1511 +val hypreal_self_eq_minus_self_zero = thm "hypreal_self_eq_minus_self_zero";
  7.1512 +val hypreal_add_self_zero_cancel = thm "hypreal_add_self_zero_cancel";
  7.1513 +val hypreal_add_self_zero_cancel2 = thm "hypreal_add_self_zero_cancel2";
  7.1514 +val hypreal_add_self_zero_cancel2a = thm "hypreal_add_self_zero_cancel2a";
  7.1515 +val hypreal_minus_eq_swap = thm "hypreal_minus_eq_swap";
  7.1516 +val hypreal_minus_eq_cancel = thm "hypreal_minus_eq_cancel";
  7.1517 +val hypreal_less_eq_diff = thm "hypreal_less_eq_diff";
  7.1518 +val hypreal_add_diff_eq = thm "hypreal_add_diff_eq";
  7.1519 +val hypreal_diff_add_eq = thm "hypreal_diff_add_eq";
  7.1520 +val hypreal_diff_diff_eq = thm "hypreal_diff_diff_eq";
  7.1521 +val hypreal_diff_diff_eq2 = thm "hypreal_diff_diff_eq2";
  7.1522 +val hypreal_diff_less_eq = thm "hypreal_diff_less_eq";
  7.1523 +val hypreal_less_diff_eq = thm "hypreal_less_diff_eq";
  7.1524 +val hypreal_diff_le_eq = thm "hypreal_diff_le_eq";
  7.1525 +val hypreal_le_diff_eq = thm "hypreal_le_diff_eq";
  7.1526 +val hypreal_diff_eq_eq = thm "hypreal_diff_eq_eq";
  7.1527 +val hypreal_eq_diff_eq = thm "hypreal_eq_diff_eq";
  7.1528 +val hypreal_less_eqI = thm "hypreal_less_eqI";
  7.1529 +val hypreal_le_eqI = thm "hypreal_le_eqI";
  7.1530 +val hypreal_eq_eqI = thm "hypreal_eq_eqI";
  7.1531 +val hypreal_zero_num = thm "hypreal_zero_num";
  7.1532 +val hypreal_one_num = thm "hypreal_one_num";
  7.1533 +val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
  7.1534 +*}
  7.1535 +
  7.1536 +
  7.1537  end
     8.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Tue Dec 16 23:24:17 2003 +0100
     8.2 +++ b/src/HOL/Hyperreal/HyperNat.ML	Wed Dec 17 16:23:52 2003 +0100
     8.3 @@ -48,9 +48,9 @@
     8.4  by Auto_tac;
     8.5  qed "hypnatrel_refl";
     8.6  
     8.7 -Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,x):hypnatrel";
     8.8 -by (auto_tac (claset() addIs [lemma_perm RS subst], simpset()));
     8.9 -qed_spec_mp "hypnatrel_sym";
    8.10 +Goal "(x,y): hypnatrel ==> (y,x):hypnatrel";
    8.11 +by (auto_tac (claset(), simpset() addsimps [hypnatrel_def, eq_commute]));
    8.12 +qed "hypnatrel_sym";
    8.13  
    8.14  Goalw [hypnatrel_def]
    8.15       "(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel";
    8.16 @@ -950,7 +950,7 @@
    8.17  
    8.18  Goalw [SHNat_def] 
    8.19       "[| EX x. x: P; P <= Nats |] ==> EX Q. P = hypnat_of_nat ` Q";
    8.20 -by (Best_tac 1); 
    8.21 +by (Blast_tac 1);
    8.22  qed "SHNat_hypnat_of_nat_image";
    8.23  
    8.24  Goalw [SHNat_def] 
    8.25 @@ -1215,6 +1215,7 @@
    8.26      Embedding of the hypernaturals into the hyperreal
    8.27   --------------------------------------------------------------*)
    8.28  
    8.29 +(*WARNING: FRAGILE!*)
    8.30  Goal "(Ya : hyprel ``{%n. f(n)}) = \
    8.31  \     ({n. f n = Ya n} : FreeUltrafilterNat)";
    8.32  by Auto_tac;
     9.1 --- a/src/HOL/Hyperreal/HyperOrd.thy	Tue Dec 16 23:24:17 2003 +0100
     9.2 +++ b/src/HOL/Hyperreal/HyperOrd.thy	Wed Dec 17 16:23:52 2003 +0100
     9.3 @@ -7,21 +7,16 @@
     9.4  
     9.5  theory HyperOrd = HyperDef:
     9.6  
     9.7 +defs (overloaded)
     9.8 +  hrabs_def:  "abs (r::hypreal) == (if 0 \<le> r then r else -r)"
     9.9  
    9.10 -method_setup fuf = {*
    9.11 -    Method.ctxt_args (fn ctxt =>
    9.12 -        Method.METHOD (fn facts =>
    9.13 -            fuf_tac (Classical.get_local_claset ctxt,
    9.14 -                     Simplifier.get_local_simpset ctxt) 1)) *}
    9.15 -    "free ultrafilter tactic"
    9.16  
    9.17 -method_setup ultra = {*
    9.18 -    Method.ctxt_args (fn ctxt =>
    9.19 -        Method.METHOD (fn facts =>
    9.20 -            ultra_tac (Classical.get_local_claset ctxt,
    9.21 -                       Simplifier.get_local_simpset ctxt) 1)) *}
    9.22 -    "ultrafilter tactic"
    9.23 -
    9.24 +lemma hypreal_hrabs:
    9.25 +     "abs (Abs_hypreal (hyprel `` {X})) = 
    9.26 +      Abs_hypreal(hyprel `` {%n. abs (X n)})"
    9.27 +apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus)
    9.28 +apply (ultra, arith)+
    9.29 +done
    9.30  
    9.31  instance hypreal :: order
    9.32    by (intro_classes,
    9.33 @@ -344,8 +339,7 @@
    9.34                 Existence of infinite hyperreal number
    9.35   ----------------------------------------------------------------------------*)
    9.36  
    9.37 -lemma Rep_hypreal_omega: "Rep_hypreal(omega) : hypreal"
    9.38 -
    9.39 +lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal"
    9.40  apply (unfold omega_def)
    9.41  apply (rule Rep_hypreal)
    9.42  done
    9.43 @@ -355,19 +349,19 @@
    9.44  (* a few lemmas first *)
    9.45  
    9.46  lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} |  
    9.47 -      (EX y. {n::nat. x = real n} = {y})"
    9.48 +      (\<exists>y. {n::nat. x = real n} = {y})"
    9.49  by (force dest: inj_real_of_nat [THEN injD])
    9.50  
    9.51  lemma lemma_finite_omega_set: "finite {n::nat. x = real n}"
    9.52  by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto)
    9.53  
    9.54  lemma not_ex_hypreal_of_real_eq_omega: 
    9.55 -      "~ (EX x. hypreal_of_real x = omega)"
    9.56 +      "~ (\<exists>x. hypreal_of_real x = omega)"
    9.57  apply (unfold omega_def hypreal_of_real_def)
    9.58  apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite])
    9.59  done
    9.60  
    9.61 -lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x ~= omega"
    9.62 +lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega"
    9.63  by (cut_tac not_ex_hypreal_of_real_eq_omega, auto)
    9.64  
    9.65  (* existence of infinitesimal number also not *)
    9.66 @@ -377,7 +371,7 @@
    9.67  by (rule inj_real_of_nat [THEN injD], simp)
    9.68  
    9.69  lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} |  
    9.70 -      (EX y. {n::nat. x = inverse(real(Suc n))} = {y})"
    9.71 +      (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})"
    9.72  apply (auto simp add: inj_real_of_nat [THEN inj_eq])
    9.73  done
    9.74  
    9.75 @@ -385,15 +379,15 @@
    9.76  by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto)
    9.77  
    9.78  lemma not_ex_hypreal_of_real_eq_epsilon: 
    9.79 -      "~ (EX x. hypreal_of_real x = epsilon)"
    9.80 +      "~ (\<exists>x. hypreal_of_real x = epsilon)"
    9.81  apply (unfold epsilon_def hypreal_of_real_def)
    9.82  apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite])
    9.83  done
    9.84  
    9.85 -lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x ~= epsilon"
    9.86 +lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon"
    9.87  by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto)
    9.88  
    9.89 -lemma hypreal_epsilon_not_zero: "epsilon ~= 0"
    9.90 +lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0"
    9.91  by (unfold epsilon_def hypreal_zero_def, auto)
    9.92  
    9.93  lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
    9.94 @@ -470,9 +464,20 @@
    9.95  lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0"
    9.96  by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero)
    9.97  
    9.98 +(*TO BE DELETED*)
    9.99 +ML
   9.100 +{*
   9.101 +val hypreal_add_ac = thms"hypreal_add_ac";
   9.102 +val hypreal_mult_ac = thms"hypreal_mult_ac";
   9.103 +
   9.104 +val hypreal_less_irrefl = thm"hypreal_less_irrefl";
   9.105 +*}
   9.106  
   9.107  ML
   9.108  {*
   9.109 +val hrabs_def = thm "hrabs_def";
   9.110 +val hypreal_hrabs = thm "hypreal_hrabs";
   9.111 +
   9.112  val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21";
   9.113  val hypreal_add_cancel_end = thm"hypreal_add_cancel_end";
   9.114  val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq";
    10.1 --- a/src/HOL/Hyperreal/HyperPow.ML	Tue Dec 16 23:24:17 2003 +0100
    10.2 +++ b/src/HOL/Hyperreal/HyperPow.ML	Wed Dec 17 16:23:52 2003 +0100
    10.3 @@ -252,7 +252,7 @@
    10.4  Goalw [congruent_def]
    10.5       "congruent hyprel \
    10.6  \    (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})";
    10.7 -by (safe_tac (claset() addSIs [ext]));
    10.8 +by (auto_tac (claset() addSIs [ext], simpset()));
    10.9  by (ALLGOALS(Fuf_tac));
   10.10  qed "hyperpow_congruent";
   10.11  
    11.1 --- a/src/HOL/Hyperreal/Lim.ML	Tue Dec 16 23:24:17 2003 +0100
    11.2 +++ b/src/HOL/Hyperreal/Lim.ML	Wed Dec 17 16:23:52 2003 +0100
    11.3 @@ -223,19 +223,17 @@
    11.4  by (dtac lemma_skolemize_LIM2 1);
    11.5  by Safe_tac;
    11.6  by (dres_inst_tac [("x","Abs_hypreal(hyprel``{X})")] spec 1);
    11.7 -by (asm_full_simp_tac
    11.8 -    (simpset() addsimps [starfun, hypreal_minus, 
    11.9 -                         hypreal_of_real_def,hypreal_add]) 1);
   11.10 -by Safe_tac;
   11.11 +by (auto_tac
   11.12 +    (claset(),
   11.13 +     simpset() addsimps [starfun, hypreal_minus, 
   11.14 +                         hypreal_of_real_def,hypreal_add]));
   11.15  by (dtac (lemma_simp RS real_seq_to_hypreal_Infinitesimal) 1);
   11.16  by (asm_full_simp_tac
   11.17      (simpset() addsimps 
   11.18         [Infinitesimal_FreeUltrafilterNat_iff,hypreal_of_real_def,
   11.19          hypreal_minus, hypreal_add]) 1);
   11.20  by (Blast_tac 1); 
   11.21 -by (rotate_tac 2 1);
   11.22 -by (dres_inst_tac [("x","r")] spec 1);
   11.23 -by (Clarify_tac 1);
   11.24 +by (dtac spec 1 THEN dtac mp 1 THEN assume_tac 1);
   11.25  by (dtac FreeUltrafilterNat_all 1);
   11.26  by (Ultra_tac 1);
   11.27  qed "NSLIM_LIM";
    12.1 --- a/src/HOL/Hyperreal/NSA.ML	Tue Dec 16 23:24:17 2003 +0100
    12.2 +++ b/src/HOL/Hyperreal/NSA.ML	Wed Dec 17 16:23:52 2003 +0100
    12.3 @@ -1967,8 +1967,6 @@
    12.4  by (dres_inst_tac [("x","u")] spec 1 THEN
    12.5      REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
    12.6  by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
    12.7 -
    12.8 -
    12.9  by (asm_full_simp_tac (simpset() addsimps [lemma_Compl_eq,
   12.10      lemma_Compl_eq2,lemma_Int_eq1]) 1);
   12.11  by (auto_tac (claset() addDs [FreeUltrafilterNat_const_Finite],
    13.1 --- a/src/HOL/Hyperreal/SEQ.ML	Tue Dec 16 23:24:17 2003 +0100
    13.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Wed Dec 17 16:23:52 2003 +0100
    13.3 @@ -127,6 +127,7 @@
    13.4      mem_infmal_iff RS sym,hypreal_of_real_def,
    13.5      hypreal_minus,hypreal_add,
    13.6      Infinitesimal_FreeUltrafilterNat_iff]));
    13.7 +by (rename_tac "Y" 1);
    13.8  by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1);
    13.9  by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   13.10  by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1);
   13.11 @@ -814,6 +815,7 @@
   13.12  by (dtac (mem_infmal_iff RS iffD2) 1);
   13.13  by (auto_tac (claset(), simpset() addsimps [hypreal_minus,
   13.14      hypreal_add,Infinitesimal_FreeUltrafilterNat_iff]));
   13.15 +by (rename_tac "Y" 1);
   13.16  by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac);
   13.17  by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
   13.18  by (dtac (CLAIM "{n. X (f n) + - X (fa n) = Y n} Int \
    14.1 --- a/src/HOL/Hyperreal/Star.ML	Tue Dec 16 23:24:17 2003 +0100
    14.2 +++ b/src/HOL/Hyperreal/Star.ML	Wed Dec 17 16:23:52 2003 +0100
    14.3 @@ -193,7 +193,7 @@
    14.4   -----------------------------------------------------------------------*) 
    14.5  
    14.6  Goalw [congruent_def] "congruent hyprel (%X. hyprel``{%n. f (X n)})";
    14.7 -by Safe_tac;
    14.8 +by Auto_tac;
    14.9  by (ALLGOALS(Fuf_tac));
   14.10  qed "starfun_congruent";
   14.11  
   14.12 @@ -407,7 +407,8 @@
   14.13        "( *f* f) x : *s* A ==> x : *s* {x. f x : A}";
   14.14  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   14.15  by (auto_tac (claset(),simpset() addsimps [starfun]));
   14.16 -by (dres_inst_tac [("x","%n. f (Xa n)")] bspec 1);
   14.17 +by (rename_tac "X" 1);
   14.18 +by (dres_inst_tac [("x","%n. f (X n)")] bspec 1);
   14.19  by (Auto_tac THEN Fuf_tac 1);
   14.20  qed "starfun_mem_starset";
   14.21  
    15.1 --- a/src/HOL/Hyperreal/fuf.ML	Tue Dec 16 23:24:17 2003 +0100
    15.2 +++ b/src/HOL/Hyperreal/fuf.ML	Wed Dec 17 16:23:52 2003 +0100
    15.3 @@ -9,6 +9,11 @@
    15.4  finite intersection property.
    15.5  *)
    15.6  
    15.7 +val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty";
    15.8 +val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset";
    15.9 +val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem";
   15.10 +val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int";
   15.11 +
   15.12  local
   15.13  
   15.14  exception FUFempty;
    16.1 --- a/src/HOL/IsaMakefile	Tue Dec 16 23:24:17 2003 +0100
    16.2 +++ b/src/HOL/IsaMakefile	Wed Dec 17 16:23:52 2003 +0100
    16.3 @@ -151,7 +151,7 @@
    16.4    Hyperreal/Filter.ML Hyperreal/Filter.thy Hyperreal/HRealAbs.ML\
    16.5    Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
    16.6    Hyperreal/HyperArith0.ML Hyperreal/HyperArith0.thy Hyperreal/HyperArith.thy\
    16.7 -  Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy Hyperreal/HyperDef.ML\
    16.8 +  Hyperreal/HyperBin.ML Hyperreal/HyperBin.thy \
    16.9    Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
   16.10    Hyperreal/HyperOrd.thy Hyperreal/HyperPow.ML\
   16.11    Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\