src/HOL/Hyperreal/NatStar.ML
changeset 14378 69c4d5997669
parent 14371 c78c7da09519
     1.1 --- a/src/HOL/Hyperreal/NatStar.ML	Thu Feb 05 10:45:28 2004 +0100
     1.2 +++ b/src/HOL/Hyperreal/NatStar.ML	Tue Feb 10 12:02:11 2004 +0100
     1.3 @@ -6,6 +6,9 @@
     1.4                    nat=>nat functions
     1.5  *) 
     1.6  
     1.7 +val hypnat_of_nat_eq = thm"hypnat_of_nat_eq";
     1.8 +val SHNat_eq = thm"SHNat_eq";
     1.9 +
    1.10  Goalw [starsetNat_def] 
    1.11        "*sNat*(UNIV::nat set) = (UNIV::hypnat set)";
    1.12  by (auto_tac (claset(), simpset() addsimps [FreeUltrafilterNat_Nat_set]));
    1.13 @@ -111,28 +114,26 @@
    1.14  by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1));
    1.15  qed "NatStar_subset";
    1.16  
    1.17 -Goalw [starsetNat_def,hypnat_of_nat_def] 
    1.18 -          "a : A ==> hypnat_of_nat a : *sNat* A";
    1.19 +Goal "a : A ==> hypnat_of_nat a : *sNat* A";
    1.20  by (auto_tac (claset() addIs [FreeUltrafilterNat_subset],
    1.21 -         simpset()));
    1.22 +         simpset() addsimps [starsetNat_def,hypnat_of_nat_eq]));
    1.23  qed "NatStar_mem";
    1.24  
    1.25  Goalw [starsetNat_def] "hypnat_of_nat ` A <= *sNat* A";
    1.26 -by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_def]));
    1.27 +by (auto_tac (claset(), simpset() addsimps [hypnat_of_nat_eq]));
    1.28  by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1);
    1.29  qed "NatStar_hypreal_of_real_image_subset";
    1.30  
    1.31  Goal "Nats <= *sNat* (UNIV:: nat set)";
    1.32 -by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_iff,
    1.33 -                          NatStar_hypreal_of_real_image_subset]) 1);
    1.34 +by (auto_tac (claset(), simpset() addsimps [starsetNat_def,SHNat_eq,hypnat_of_nat_eq]));
    1.35  qed "NatStar_SHNat_subset";
    1.36  
    1.37  Goalw [starsetNat_def] 
    1.38       "*sNat* X Int Nats = hypnat_of_nat ` X";
    1.39  by (auto_tac (claset(),
    1.40           simpset() addsimps 
    1.41 -           [hypnat_of_nat_def,SHNat_def]));
    1.42 -by (fold_tac [hypnat_of_nat_def]);
    1.43 +           [hypnat_of_nat_eq,SHNat_eq]));
    1.44 +by (simp_tac (simpset() addsimps [hypnat_of_nat_eq RS sym]) 1);
    1.45  by (rtac imageI 1 THEN rtac ccontr 1);
    1.46  by (dtac bspec 1);
    1.47  by (rtac lemma_hypnatrel_refl 1);
    1.48 @@ -289,7 +290,7 @@
    1.49  
    1.50  Goal "( *fNat2* (%x. k)) z = hypnat_of_nat  k";
    1.51  by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
    1.52 -by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_def]));
    1.53 +by (auto_tac (claset(), simpset() addsimps [starfunNat2, hypnat_of_nat_eq]));
    1.54  qed "starfunNat2_const_fun";
    1.55  
    1.56  Addsimps [starfunNat2_const_fun];
    1.57 @@ -312,13 +313,13 @@
    1.58  
    1.59  Goal "( *fNat* f) (hypnat_of_nat a) = hypreal_of_real (f a)";
    1.60  by (auto_tac (claset(),
    1.61 -      simpset() addsimps [starfunNat,hypnat_of_nat_def,hypreal_of_real_def]));
    1.62 +      simpset() addsimps [starfunNat,hypnat_of_nat_eq,hypreal_of_real_def]));
    1.63  qed "starfunNat_eq";
    1.64  
    1.65  Addsimps [starfunNat_eq];
    1.66  
    1.67  Goal "( *fNat2* f) (hypnat_of_nat a) = hypnat_of_nat (f a)";
    1.68 -by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_def]));
    1.69 +by (auto_tac (claset(), simpset() addsimps [starfunNat2,hypnat_of_nat_eq]));
    1.70  qed "starfunNat2_eq";
    1.71  
    1.72  Addsimps [starfunNat2_eq];
    1.73 @@ -337,7 +338,7 @@
    1.74  by (Step_tac 1);
    1.75  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    1.76  by (auto_tac (claset(),
    1.77 -         simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
    1.78 +         simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
    1.79                               hypreal_less, hypnat_le,hypnat_less]));
    1.80  by (Ultra_tac 1);
    1.81  by Auto_tac;
    1.82 @@ -349,7 +350,7 @@
    1.83  by (Step_tac 1);
    1.84  by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
    1.85  by (auto_tac (claset(),
    1.86 -         simpset() addsimps [starfunNat, hypnat_of_nat_def,hypreal_le,
    1.87 +         simpset() addsimps [starfunNat, hypnat_of_nat_eq,hypreal_le,
    1.88                               hypreal_less, hypnat_le,hypnat_less]));
    1.89  by (Ultra_tac 1);
    1.90  by Auto_tac;
    1.91 @@ -384,12 +385,12 @@
    1.92  Goal "( *fNat* (%n. (X n) ^ m)) N = ( *fNat* X) N pow hypnat_of_nat m";
    1.93  by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
    1.94  by (auto_tac (claset(),
    1.95 -         simpset() addsimps [hyperpow, hypnat_of_nat_def,starfunNat]));
    1.96 +         simpset() addsimps [hyperpow, hypnat_of_nat_eq,starfunNat]));
    1.97  qed "starfunNat_pow2";
    1.98  
    1.99 -Goalw [hypnat_of_nat_def] "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
   1.100 +Goal "( *f* (%r. r ^ n)) R = (R) pow hypnat_of_nat n";
   1.101  by (res_inst_tac [("z","R")] eq_Abs_hypreal 1);
   1.102 -by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun]));
   1.103 +by (auto_tac (claset(), simpset() addsimps [hyperpow,starfun,hypnat_of_nat_eq]));
   1.104  qed "starfun_pow";
   1.105  
   1.106  (*----------------------------------------------------- 
   1.107 @@ -469,7 +470,7 @@
   1.108  qed "starfunNat_n_minus";
   1.109  
   1.110  Goal "( *fNatn* f) (hypnat_of_nat n) = Abs_hypreal(hyprel `` {%i. f i n})";
   1.111 -by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_def]));
   1.112 +by (auto_tac (claset(), simpset() addsimps [starfunNat_n,hypnat_of_nat_eq]));
   1.113  qed "starfunNat_n_eq";
   1.114  Addsimps [starfunNat_n_eq];
   1.115  
   1.116 @@ -477,7 +478,7 @@
   1.117  by Auto_tac;
   1.118  by (rtac ext 1 THEN rtac ccontr 1);
   1.119  by (dres_inst_tac [("x","hypnat_of_nat(x)")] fun_cong 1);
   1.120 -by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_def]));
   1.121 +by (auto_tac (claset(), simpset() addsimps [starfunNat,hypnat_of_nat_eq]));
   1.122  qed "starfun_eq_iff";
   1.123  
   1.124