src/HOL/Hyperreal/NSA.ML
changeset 14336 8f731d3cd65b
parent 14334 6137d24eef79
child 14365 3d4df8c166ae
     1.1 --- a/src/HOL/Hyperreal/NSA.ML	Thu Jan 01 21:47:07 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/NSA.ML	Sat Jan 03 16:09:39 2004 +0100
     1.3 @@ -216,7 +216,7 @@
     1.4  
     1.5  Goalw [HFinite_def] "[|x : HFinite; y : HFinite|] ==> x*y : HFinite";
     1.6  by (Asm_full_simp_tac 1);
     1.7 -by (blast_tac (claset() addSIs [SReal_mult,hrabs_mult_less]) 1);
     1.8 +by (blast_tac (claset() addSIs [SReal_mult,abs_mult_less]) 1);
     1.9  qed "HFinite_mult";
    1.10  
    1.11  Goalw [HFinite_def] "(-x : HFinite) = (x : HFinite)";
    1.12 @@ -243,7 +243,7 @@
    1.13  qed "HFiniteD";
    1.14  
    1.15  Goalw [HFinite_def] "(abs x : HFinite) = (x : HFinite)";
    1.16 -by (auto_tac (claset(), simpset() addsimps [hrabs_idempotent]));
    1.17 +by Auto_tac;
    1.18  qed "HFinite_hrabs_iff";
    1.19  AddIffs [HFinite_hrabs_iff];
    1.20  
    1.21 @@ -284,7 +284,7 @@
    1.22  qed "InfinitesimalD";
    1.23  
    1.24  Goalw [Infinitesimal_def] "0 : Infinitesimal";
    1.25 -by (simp_tac (simpset() addsimps [hrabs_zero]) 1);
    1.26 +by (Simp_tac 1);
    1.27  qed "Infinitesimal_zero";
    1.28  AddIffs [Infinitesimal_zero];
    1.29  
    1.30 @@ -424,9 +424,7 @@
    1.31  
    1.32  Goalw [Infinitesimal_def]
    1.33        "[| e : Infinitesimal; abs x < e |] ==> x : Infinitesimal";
    1.34 -by (auto_tac (claset() addSDs [bspec], simpset()));
    1.35 -by (dres_inst_tac [("x","e")] (hrabs_ge_self RS order_le_less_trans) 1);
    1.36 -by (fast_tac (claset() addIs [order_less_trans]) 1);
    1.37 +by (auto_tac (claset(), simpset() addsimps [abs_less_iff]));
    1.38  qed "hrabs_less_Infinitesimal";
    1.39  
    1.40  Goal "[| e : Infinitesimal; abs x <= e |] ==> x : Infinitesimal";
    1.41 @@ -438,10 +436,7 @@
    1.42        "[| e : Infinitesimal; \
    1.43  \         e' : Infinitesimal; \
    1.44  \         e' < x ; x < e |] ==> x : Infinitesimal";
    1.45 -by (auto_tac (claset() addSDs [bspec], simpset()));
    1.46 -by (dres_inst_tac [("x","e")] (hrabs_ge_self RS order_le_less_trans) 1);
    1.47 -by (dtac (hrabs_interval_iff RS iffD1) 1);
    1.48 -by (fast_tac(claset() addIs [order_less_trans,hrabs_interval_iff RS iffD2]) 1);
    1.49 +by (auto_tac (claset(), simpset() addsimps [abs_less_iff]));
    1.50  qed "Infinitesimal_interval";
    1.51  
    1.52  Goal "[| e : Infinitesimal; e' : Infinitesimal; \
    1.53 @@ -819,7 +814,7 @@
    1.54  
    1.55  Goalw [Infinitesimal_def]
    1.56       "[| x: Reals; y: Infinitesimal; 0 < x |] ==> y < x";
    1.57 -by (rtac (hrabs_ge_self RS order_le_less_trans) 1);
    1.58 +by (rtac (abs_ge_self RS order_le_less_trans) 1);
    1.59  by Auto_tac;
    1.60  qed "Infinitesimal_less_SReal";
    1.61  
    1.62 @@ -991,15 +986,14 @@
    1.63  Goal "x: HFinite ==> EX u. isUb Reals {s. s: Reals & s < x} u";
    1.64  by (dtac HFiniteD 1 THEN Step_tac 1);
    1.65  by (rtac exI 1 THEN rtac isUbI 1 THEN assume_tac 2);
    1.66 -by (auto_tac (claset() addIs [order_less_imp_le,setleI,isUbI,
    1.67 -    order_less_trans], simpset() addsimps [hrabs_interval_iff]));
    1.68 +by (auto_tac (claset() addIs [setleI,isUbI], simpset() addsimps [abs_less_iff]));
    1.69  qed "lemma_st_part_ub";
    1.70  
    1.71  Goal "x: HFinite ==> EX y. y: {s. s: Reals & s < x}";
    1.72  by (dtac HFiniteD 1 THEN Step_tac 1);
    1.73  by (dtac SReal_minus 1);
    1.74  by (res_inst_tac [("x","-t")] exI 1);
    1.75 -by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
    1.76 +by (auto_tac (claset(), simpset() addsimps [abs_less_iff]));
    1.77  qed "lemma_st_part_nonempty";
    1.78  
    1.79  Goal "{s. s: Reals & s < x} <= Reals";
    1.80 @@ -1135,8 +1129,8 @@
    1.81  by (ftac lemma_st_part2a 4);
    1.82  by Auto_tac;
    1.83  by (REPEAT(dtac order_le_imp_less_or_eq 1));
    1.84 -by (auto_tac (claset() addDs [lemma_st_part_not_eq1,
    1.85 -    lemma_st_part_not_eq2], simpset() addsimps [hrabs_interval_iff2]));
    1.86 +by (auto_tac (claset() addDs [lemma_st_part_not_eq1, lemma_st_part_not_eq2],
    1.87 +         simpset() addsimps [abs_less_iff]));
    1.88  qed "lemma_st_part_major";
    1.89  
    1.90  Goal "[| x: HFinite; \
    1.91 @@ -1490,7 +1484,7 @@
    1.92  by (dres_inst_tac [("x","hypreal_of_real y + -hypreal_of_real x")] bspec 1);
    1.93  by (auto_tac (claset(),
    1.94                simpset() addsimps [hypreal_add_commute,
    1.95 -                                  hrabs_interval_iff,
    1.96 +                                  abs_less_iff,
    1.97                                    SReal_add, SReal_minus]));
    1.98  qed "Infinitesimal_add_hypreal_of_real_less";
    1.99  
   1.100 @@ -1900,28 +1894,27 @@
   1.101  Goalw [HFinite_def]
   1.102      "x : HFinite ==> EX X: Rep_hypreal x. \
   1.103  \    EX u. {n. abs (X n) < u}:  FreeUltrafilterNat";
   1.104 -by (auto_tac (claset(), simpset() addsimps
   1.105 -    [hrabs_interval_iff]));
   1.106 +by (auto_tac (claset(), simpset() addsimps [abs_less_iff, inst "a" "x" minus_less_iff]));
   1.107  by (auto_tac (claset(), simpset() addsimps
   1.108      [hypreal_less_def,SReal_iff,hypreal_minus,
   1.109       hypreal_of_real_def]));
   1.110  by (dtac FreeUltrafilterNat_Rep_hypreal 1 THEN assume_tac 1);
   1.111 -by (res_inst_tac [("x","Y")] bexI 1 THEN assume_tac 2);
   1.112 +by (rename_tac "Z" 1);
   1.113 +by (res_inst_tac [("x","Z")] bexI 1 THEN assume_tac 2);
   1.114  by (res_inst_tac [("x","y")] exI 1);
   1.115 -by (Ultra_tac 1 THEN arith_tac 1);
   1.116 +by (Ultra_tac 1);
   1.117  qed "HFinite_FreeUltrafilterNat";
   1.118  
   1.119  Goalw [HFinite_def]
   1.120       "EX X: Rep_hypreal x. \
   1.121  \      EX u. {n. abs (X n) < u}: FreeUltrafilterNat\
   1.122  \      ==>  x : HFinite";
   1.123 -by (auto_tac (claset(), simpset() addsimps
   1.124 -    [hrabs_interval_iff]));
   1.125 +by (auto_tac (claset(), simpset() addsimps [abs_less_iff, inst "a" "x" minus_less_iff]));
   1.126  by (res_inst_tac [("x","hypreal_of_real u")] bexI 1);
   1.127 -by (auto_tac (claset() addSIs [exI], simpset() addsimps
   1.128 -    [hypreal_less_def,SReal_iff,hypreal_minus,
   1.129 -     hypreal_of_real_def]));
   1.130 -by (ALLGOALS(Ultra_tac THEN' arith_tac));
   1.131 +by (auto_tac (claset() addSIs [exI], 
   1.132 +   simpset() addsimps
   1.133 +    [hypreal_less_def,SReal_iff,hypreal_minus, hypreal_of_real_def]));
   1.134 +by (ALLGOALS Ultra_tac);
   1.135  qed "FreeUltrafilterNat_HFinite";
   1.136  
   1.137  Goal "(x : HFinite) = (EX X: Rep_hypreal x. \
   1.138 @@ -2026,7 +2019,7 @@
   1.139  Goalw [Infinitesimal_def]
   1.140            "x : Infinitesimal ==> EX X: Rep_hypreal x. \
   1.141  \          ALL u. 0 < u --> {n. abs (X n) < u}:  FreeUltrafilterNat";
   1.142 -by (auto_tac (claset(), simpset() addsimps [hrabs_interval_iff]));
   1.143 +by (auto_tac (claset(), simpset() addsimps [abs_less_iff, inst "a" "x" minus_less_iff]));
   1.144  by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
   1.145  by (EVERY[Auto_tac, rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]);
   1.146  by (dtac (hypreal_of_real_less_iff RS iffD2) 1);
   1.147 @@ -2035,7 +2028,7 @@
   1.148  by (auto_tac (claset(),
   1.149                simpset() addsimps [hypreal_less_def, hypreal_minus,
   1.150                                    hypreal_of_real_def]));
   1.151 -by (Ultra_tac 1 THEN arith_tac 1);
   1.152 +by (Ultra_tac 1);
   1.153  qed "Infinitesimal_FreeUltrafilterNat";
   1.154  
   1.155  Goalw [Infinitesimal_def]
   1.156 @@ -2043,7 +2036,7 @@
   1.157  \           ALL u. 0 < u --> {n. abs (X n) < u} : FreeUltrafilterNat \
   1.158  \     ==> x : Infinitesimal";
   1.159  by (auto_tac (claset(),
   1.160 -              simpset() addsimps [hrabs_interval_iff,abs_interval_iff]));
   1.161 +              simpset() addsimps [abs_less_iff,abs_interval_iff, inst "a" "x" minus_less_iff]));
   1.162  by (auto_tac (claset(),
   1.163                simpset() addsimps [SReal_iff]));
   1.164  by (auto_tac (claset() addSIs [exI]