Conversion of HyperNat to Isar format and its declaration as a semiring
authorpaulson
Mon Feb 02 12:23:46 2004 +0100 (2004-02-02)
changeset 14371c78c7da09519
parent 14370 b0064703967b
child 14372 51ddf8963c95
Conversion of HyperNat to Isar format and its declaration as a semiring
src/HOL/Complex/NSComplex.thy
src/HOL/Complex/NSInduct.ML
src/HOL/Complex/ex/NSPrimes.ML
src/HOL/Hyperreal/HLog.ML
src/HOL/Hyperreal/HRealAbs.thy
src/HOL/Hyperreal/HSeries.ML
src/HOL/Hyperreal/HTranscendental.ML
src/HOL/Hyperreal/HyperArith.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.ML
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Hyperreal/HyperOrd.thy
src/HOL/Hyperreal/HyperPow.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Hyperreal/NatStar.ML
src/HOL/Hyperreal/SEQ.ML
src/HOL/Hyperreal/Star.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Jan 29 16:51:17 2004 +0100
     1.2 +++ b/src/HOL/Complex/NSComplex.thy	Mon Feb 02 12:23:46 2004 +0100
     1.3 @@ -6,33 +6,6 @@
     1.4  
     1.5  theory NSComplex = NSInduct:
     1.6  
     1.7 -(* ???MOVE to one of the hyperreal theories: HRealAbs??? *)
     1.8 -lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
     1.9 -apply (induct_tac "m")
    1.10 -apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
    1.11 -done
    1.12 -
    1.13 -lemma hypreal_of_nat_le_iff:
    1.14 -      "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
    1.15 -apply (auto simp add: linorder_not_less [symmetric])
    1.16 -done
    1.17 -declare hypreal_of_nat_le_iff [simp]
    1.18 -
    1.19 -lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
    1.20 -apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
    1.21 -         del: hypreal_of_nat_zero)
    1.22 -done
    1.23 -declare hypreal_of_nat_ge_zero [simp]
    1.24 -
    1.25 -declare hypreal_of_nat_ge_zero [THEN hrabs_eqI1, simp]
    1.26 -
    1.27 -lemma hypreal_of_hypnat_ge_zero: "0 \<le> hypreal_of_hypnat n"
    1.28 -apply (rule_tac z = "n" in eq_Abs_hypnat)
    1.29 -apply (simp (no_asm_simp) add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
    1.30 -done
    1.31 -declare hypreal_of_hypnat_ge_zero [simp]
    1.32 -declare hypreal_of_hypnat_ge_zero [THEN hrabs_eqI1, simp]
    1.33 -
    1.34  constdefs
    1.35      hcomplexrel :: "((nat=>complex)*(nat=>complex)) set"
    1.36      "hcomplexrel == {p. \<exists>X Y. p = ((X::nat=>complex),Y) &
    1.37 @@ -819,13 +792,13 @@
    1.38  
    1.39  lemma hcmod_hcomplex_of_hypreal_of_nat:
    1.40       "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n"
    1.41 -apply auto
    1.42 +apply (simp add: abs_if linorder_not_less) 
    1.43  done
    1.44  declare hcmod_hcomplex_of_hypreal_of_nat [simp]
    1.45  
    1.46  lemma hcmod_hcomplex_of_hypreal_of_hypnat:
    1.47       "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n"
    1.48 -apply auto
    1.49 +apply (simp add: abs_if linorder_not_less) 
    1.50  done
    1.51  declare hcmod_hcomplex_of_hypreal_of_hypnat [simp]
    1.52  
    1.53 @@ -846,8 +819,8 @@
    1.54  done
    1.55  declare hcmod_ge_zero [simp]
    1.56  
    1.57 -lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x"
    1.58 -apply (auto intro: hrabs_eqI1)
    1.59 +lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x" 
    1.60 +apply (simp add: abs_if linorder_not_less) 
    1.61  done
    1.62  declare hrabs_hcmod_cancel [simp]
    1.63  
    1.64 @@ -1817,9 +1790,7 @@
    1.65  val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
    1.66  val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
    1.67  val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
    1.68 -val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
    1.69 -val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
    1.70 -val hypreal_of_hypnat_ge_zero = thm"hypreal_of_hypnat_ge_zero";
    1.71 +
    1.72  val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
    1.73  val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
    1.74  val hcmod_minus = thm"hcmod_minus";
    1.75 @@ -1909,7 +1880,6 @@
    1.76  val hrcis_zero_arg = thm"hrcis_zero_arg";
    1.77  val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
    1.78  val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
    1.79 -val hypreal_of_nat = thm"hypreal_of_nat";
    1.80  val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
    1.81  val NSDeMoivre = thm"NSDeMoivre";
    1.82  val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
     2.1 --- a/src/HOL/Complex/NSInduct.ML	Thu Jan 29 16:51:17 2004 +0100
     2.2 +++ b/src/HOL/Complex/NSInduct.ML	Mon Feb 02 12:23:46 2004 +0100
     2.3 @@ -67,23 +67,6 @@
     2.4  by (Auto_tac);
     2.5  val lemma_hyp = result();
     2.6  
     2.7 -Goal "(EX (v::nat=>nat). ALL (x::nat). P (g v) (f x)) = \
     2.8 -\     (EX (v::nat=>nat). ALL x. EX f': Rep_hypnat(f x). P (g v) (Abs_hypnat(hypnatrel `` {f'})))"; 
     2.9 -by (Auto_tac);
    2.10 -by (ALLGOALS(res_inst_tac [("x","v")] exI));
    2.11 -by (Step_tac 1);
    2.12 -by (ALLGOALS(res_inst_tac [("z","f x")] eq_Abs_hypnat));
    2.13 -by (Auto_tac);
    2.14 -by (rtac bexI 1);
    2.15 -by (dres_inst_tac [("x","x")] spec 3);
    2.16 -by (dtac sym 1);
    2.17 -by (Auto_tac);
    2.18 -by (subgoal_tac 
    2.19 -    "Abs_hypnat (hypnatrel `` {X}) = Abs_hypnat (hypnatrel `` {Y})" 1);
    2.20 -by (Asm_simp_tac 1);
    2.21 -by (Auto_tac);
    2.22 -val lemma_hyp2 = result();
    2.23 -
    2.24  Goalw [hSuc_def] "hSuc m ~= 0";
    2.25  by Auto_tac;
    2.26  qed "hSuc_not_zero";
    2.27 @@ -99,12 +82,6 @@
    2.28  
    2.29  AddIffs [hSuc_not_zero,zero_not_hSuc,hSuc_hSuc_eq];
    2.30  
    2.31 -Goalw [hypnat_le_def] "m <= (n::hypnat) | n <= m";
    2.32 -by (auto_tac (claset() addDs [hypnat_less_trans],simpset()));
    2.33 -qed "hypnat_le_linear";
    2.34 -
    2.35 -val hypnat_less_le = hypnat_less_imp_le;
    2.36 -
    2.37  Goal "c : (S :: nat set) ==> (LEAST n. n : S) : S";
    2.38  by (etac LeastI 1);
    2.39  qed "nonempty_nat_set_Least_mem";
    2.40 @@ -132,7 +109,8 @@
    2.41  by (dres_inst_tac [("x","n - 1")] bspec 1);
    2.42  by (Step_tac 1);
    2.43  by (dres_inst_tac [("x","n - 1")] spec 1);
    2.44 -by (dres_inst_tac [("x","1"),("q1.0","n")] hypnat_add_le_mono1 2);
    2.45 -by (auto_tac (claset(),simpset() addsimps [hypnat_le_def]));
    2.46 +by (dres_inst_tac [("c","1"),("a","n")] add_right_mono 2); 
    2.47 +by (auto_tac ((claset(),simpset() addsimps [linorder_not_less RS sym])
    2.48 +        delIffs [hypnat_neq0_conv]));
    2.49  qed "internal_induct";
    2.50  
     3.1 --- a/src/HOL/Complex/ex/NSPrimes.ML	Thu Jan 29 16:51:17 2004 +0100
     3.2 +++ b/src/HOL/Complex/ex/NSPrimes.ML	Mon Feb 02 12:23:46 2004 +0100
     3.3 @@ -74,7 +74,7 @@
     3.4  
     3.5  Goal "(hypnat_of_nat n <= 0) = (n = 0)";
     3.6  by (stac (hypnat_of_nat_zero RS sym) 1);
     3.7 -by (auto_tac (claset(),simpset() addsimps [hypnat_of_nat_le_iff RS sym]));
     3.8 +by Auto_tac;
     3.9  qed "hypnat_of_nat_le_zero_iff";
    3.10  Addsimps [hypnat_of_nat_le_zero_iff];
    3.11  
    3.12 @@ -107,8 +107,8 @@
    3.13  by Auto_tac;
    3.14  by (rtac exI 1 THEN Auto_tac);
    3.15  by (dres_inst_tac [("x","hypnat_of_nat n")] spec 1);
    3.16 -by (auto_tac (claset(),simpset() addsimps [symmetric hypnat_le_def,
    3.17 -    hypnat_of_nat_zero_iff]));
    3.18 +by (auto_tac (claset(),
    3.19 +     simpset() addsimps [linorder_not_less, hypnat_of_nat_zero_iff]));
    3.20  qed "hypnat_dvd_all_hypnat_of_nat";
    3.21  
    3.22  
     4.1 --- a/src/HOL/Hyperreal/HLog.ML	Thu Jan 29 16:51:17 2004 +0100
     4.2 +++ b/src/HOL/Hyperreal/HLog.ML	Mon Feb 02 12:23:46 2004 +0100
     4.3 @@ -42,8 +42,8 @@
     4.4       "(Abs_hypreal(hyprel `` {X}))/(Abs_hypreal(hyprel `` {Y})) = \
     4.5  \     (Abs_hypreal(hyprel `` {%n. (X n)/(Y n)}))";
     4.6  by (case_tac "Abs_hypreal (hyprel `` {Y}) = 0" 1);
     4.7 -by (auto_tac (claset(),simpset() addsimps [HYPREAL_DIVISION_BY_ZERO,
     4.8 -    hypreal_zero_num,hypreal_inverse,hypreal_mult]));
     4.9 +by (auto_tac (claset(),
    4.10 +  simpset() addsimps [hypreal_zero_num,hypreal_inverse,hypreal_mult]));
    4.11  by (ALLGOALS(ultra_tac (claset(),simpset() addsimps [real_divide_def])));
    4.12  qed "hypreal_divide";
    4.13  
     5.1 --- a/src/HOL/Hyperreal/HRealAbs.thy	Thu Jan 29 16:51:17 2004 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,149 +0,0 @@
     5.4 -(*  Title       : HRealAbs.thy
     5.5 -    Author      : Jacques D. Fleuriot
     5.6 -    Copyright   : 1998  University of Cambridge
     5.7 -    Description : Absolute value function for the hyperreals
     5.8 -*) 
     5.9 -
    5.10 -theory HRealAbs = HyperArith:
    5.11 -
    5.12 -constdefs
    5.13 -
    5.14 -  hypreal_of_nat :: "nat => hypreal"
    5.15 -  "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
    5.16 -
    5.17 -
    5.18 -lemma hrabs_number_of [simp]:
    5.19 -     "abs (number_of v :: hypreal) =
    5.20 -        (if neg (number_of v) then number_of (bin_minus v)
    5.21 -         else number_of v)"
    5.22 -by (simp add: hrabs_def)
    5.23 -
    5.24 -
    5.25 -(*------------------------------------------------------------
    5.26 -   Properties of the absolute value function over the reals
    5.27 -   (adapted version of previously proved theorems about abs)
    5.28 - ------------------------------------------------------------*)
    5.29 -
    5.30 -lemma hrabs_eqI1: "(0::hypreal)<=x ==> abs x = x"
    5.31 -by (simp add: hrabs_def)
    5.32 -
    5.33 -lemma hrabs_eqI2: "(0::hypreal)<x ==> abs x = x"
    5.34 -by (simp add: order_less_imp_le hrabs_eqI1)
    5.35 -
    5.36 -lemma hrabs_minus_eqI2: "x<(0::hypreal) ==> abs x = -x"
    5.37 -by (simp add: linorder_not_less [symmetric] hrabs_def)
    5.38 -
    5.39 -lemma hrabs_minus_eqI1: "x<=(0::hypreal) ==> abs x = -x"
    5.40 -by (auto dest: order_antisym simp add: hrabs_def)
    5.41 -
    5.42 -declare abs_mult [simp]
    5.43 -
    5.44 -lemma hrabs_add_less: "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
    5.45 -apply (unfold hrabs_def)
    5.46 -apply (simp split add: split_if_asm)
    5.47 -done
    5.48 -
    5.49 -lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
    5.50 -by (blast intro!: order_le_less_trans abs_ge_zero)
    5.51 -
    5.52 -lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
    5.53 -by (simp add: hrabs_def)
    5.54 -
    5.55 -lemma hrabs_eq_disj: "abs x = (y::hypreal) ==> x = y | -x = y"
    5.56 -by (simp add: hrabs_def split add: split_if_asm)
    5.57 -
    5.58 -(* Needed in Geom.ML *)
    5.59 -lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
    5.60 -by (simp add: hrabs_def split add: split_if_asm)
    5.61 -
    5.62 -(* Needed in Geom.ML?? *)
    5.63 -lemma hrabs_add_lemma_disj2: "(x::hypreal) + - y + (z + - y) = abs (x + - z) ==> y = z | x = y"
    5.64 -by (simp add: hrabs_def split add: split_if_asm)
    5.65 -
    5.66 -
    5.67 -(*----------------------------------------------------------
    5.68 -    Relating hrabs to abs through embedding of IR into IR*
    5.69 - ----------------------------------------------------------*)
    5.70 -lemma hypreal_of_real_hrabs:
    5.71 -    "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
    5.72 -apply (unfold hypreal_of_real_def)
    5.73 -apply (auto simp add: hypreal_hrabs)
    5.74 -done
    5.75 -
    5.76 -
    5.77 -(*----------------------------------------------------------------------------
    5.78 -             Embedding of the naturals in the hyperreals
    5.79 - ----------------------------------------------------------------------------*)
    5.80 -
    5.81 -lemma hypreal_of_nat_add [simp]:
    5.82 -     "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
    5.83 -by (simp add: hypreal_of_nat_def)
    5.84 -
    5.85 -lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n"
    5.86 -by (simp add: hypreal_of_nat_def)
    5.87 -declare hypreal_of_nat_mult [simp]
    5.88 -
    5.89 -lemma hypreal_of_nat_less_iff:
    5.90 -      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"
    5.91 -apply (simp add: hypreal_of_nat_def)
    5.92 -done
    5.93 -declare hypreal_of_nat_less_iff [symmetric, simp]
    5.94 -
    5.95 -(*------------------------------------------------------------*)
    5.96 -(* naturals embedded in hyperreals                            *)
    5.97 -(* is a hyperreal c.f. NS extension                           *)
    5.98 -(*------------------------------------------------------------*)
    5.99 -
   5.100 -lemma hypreal_of_nat_iff:
   5.101 -     "hypreal_of_nat  m = Abs_hypreal(hyprel``{%n. real m})"
   5.102 -by (simp add: hypreal_of_nat_def hypreal_of_real_def real_of_nat_def)
   5.103 -
   5.104 -lemma inj_hypreal_of_nat: "inj hypreal_of_nat"
   5.105 -by (simp add: inj_on_def hypreal_of_nat_def)
   5.106 -
   5.107 -lemma hypreal_of_nat_Suc:
   5.108 -     "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
   5.109 -by (simp add: hypreal_of_nat_def real_of_nat_Suc)
   5.110 -
   5.111 -(*"neg" is used in rewrite rules for binary comparisons*)
   5.112 -lemma hypreal_of_nat_number_of [simp]:
   5.113 -     "hypreal_of_nat (number_of v :: nat) =
   5.114 -         (if neg (number_of v) then 0
   5.115 -          else (number_of v :: hypreal))"
   5.116 -by (simp add: hypreal_of_nat_def)
   5.117 -
   5.118 -lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
   5.119 -by (simp del: numeral_0_eq_0 add: numeral_0_eq_0 [symmetric])
   5.120 -
   5.121 -lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
   5.122 -by (simp add: hypreal_of_nat_Suc)
   5.123 -
   5.124 -
   5.125 -ML
   5.126 -{*
   5.127 -val hypreal_of_nat_def = thm"hypreal_of_nat_def";
   5.128 -
   5.129 -val hrabs_number_of = thm "hrabs_number_of";
   5.130 -val hrabs_eqI1 = thm "hrabs_eqI1";
   5.131 -val hrabs_eqI2 = thm "hrabs_eqI2";
   5.132 -val hrabs_minus_eqI2 = thm "hrabs_minus_eqI2";
   5.133 -val hrabs_minus_eqI1 = thm "hrabs_minus_eqI1";
   5.134 -val hrabs_add_less = thm "hrabs_add_less";
   5.135 -val hrabs_less_gt_zero = thm "hrabs_less_gt_zero";
   5.136 -val hrabs_disj = thm "hrabs_disj";
   5.137 -val hrabs_eq_disj = thm "hrabs_eq_disj";
   5.138 -val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
   5.139 -val hrabs_add_lemma_disj2 = thm "hrabs_add_lemma_disj2";
   5.140 -val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
   5.141 -val hypreal_of_nat_add = thm "hypreal_of_nat_add";
   5.142 -val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
   5.143 -val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
   5.144 -val hypreal_of_nat_iff = thm "hypreal_of_nat_iff";
   5.145 -val inj_hypreal_of_nat = thm "inj_hypreal_of_nat";
   5.146 -val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
   5.147 -val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
   5.148 -val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
   5.149 -val hypreal_of_nat_one = thm "hypreal_of_nat_one";
   5.150 -*}
   5.151 -
   5.152 -end
     6.1 --- a/src/HOL/Hyperreal/HSeries.ML	Thu Jan 29 16:51:17 2004 +0100
     6.2 +++ b/src/HOL/Hyperreal/HSeries.ML	Mon Feb 02 12:23:46 2004 +0100
     6.3 @@ -213,7 +213,7 @@
     6.4  
     6.5  Goal "sumhr (0, M, f) @= sumhr (0, N, f) \
     6.6  \     ==> abs (sumhr (M, N, f)) @= 0";
     6.7 -by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
     6.8 +by (cut_inst_tac [("x","M"),("y","N")] linorder_less_linear 1);
     6.9  by (auto_tac (claset(), simpset() addsimps [approx_refl]));
    6.10  by (dtac (approx_sym RS (approx_minus_iff RS iffD1)) 1);
    6.11  by (auto_tac (claset() addDs [approx_hrabs],
    6.12 @@ -265,7 +265,7 @@
    6.13                   summable_convergent_sumr_iff, convergent_NSconvergent_iff,
    6.14                   NSCauchy_NSconvergent_iff RS sym, NSCauchy_def,
    6.15                   starfunNat_sumr]));
    6.16 -by (cut_inst_tac [("x","M"),("y","N")] hypnat_linear 1);
    6.17 +by (cut_inst_tac [("x","M"),("y","N")] linorder_less_linear 1);
    6.18  by (auto_tac (claset(), simpset() addsimps [approx_refl]));
    6.19  by (rtac ((approx_minus_iff RS iffD2) RS approx_sym) 1);
    6.20  by (rtac (approx_minus_iff RS iffD2) 2);
     7.1 --- a/src/HOL/Hyperreal/HTranscendental.ML	Thu Jan 29 16:51:17 2004 +0100
     7.2 +++ b/src/HOL/Hyperreal/HTranscendental.ML	Mon Feb 02 12:23:46 2004 +0100
     7.3 @@ -609,7 +609,7 @@
     7.4  Goal "n : HNatInfinite \
     7.5  \     ==> ( *f* sin) (inverse (hypreal_of_hypnat n))/(inverse (hypreal_of_hypnat n)) @= 1";
     7.6  by (rtac STAR_sin_Infinitesimal_divide 1);
     7.7 -by Auto_tac;
     7.8 +by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
     7.9  val lemma_sin_pi = result();
    7.10  
    7.11  Goal "n : HNatInfinite \
    7.12 @@ -626,7 +626,7 @@
    7.13  
    7.14  Goal "N : HNatInfinite \
    7.15  \     ==> hypreal_of_real pi/(hypreal_of_hypnat N) ~= 0";
    7.16 -by Auto_tac;
    7.17 +by (auto_tac (claset(),simpset() addsimps [HNatInfinite_not_eq_zero]));
    7.18  qed "pi_divide_HNatInfinite_not_zero";
    7.19  Addsimps [pi_divide_HNatInfinite_not_zero];
    7.20  
    7.21 @@ -675,8 +675,8 @@
    7.22  
    7.23  Goal "N : HNatInfinite ==> 0 < hypreal_of_hypnat N";
    7.24  by (rtac ccontr 1);
    7.25 -by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat_zero RS sym,
    7.26 -    symmetric hypnat_le_def]));
    7.27 +by (auto_tac (claset(),
    7.28 +   simpset() addsimps [hypreal_of_hypnat_zero RS sym, linorder_not_less]));
    7.29  qed "HNatInfinite_hypreal_of_hypnat_gt_zero";
    7.30  
    7.31  bind_thm ("HNatInfinite_hypreal_of_hypnat_not_eq_zero",
     8.1 --- a/src/HOL/Hyperreal/HyperArith.thy	Thu Jan 29 16:51:17 2004 +0100
     8.2 +++ b/src/HOL/Hyperreal/HyperArith.thy	Mon Feb 02 12:23:46 2004 +0100
     8.3 @@ -1,4 +1,4 @@
     8.4 -(*  Title:      HOL/HyperBin.thy
     8.5 +(*  Title:      HOL/HyperArith.thy
     8.6      ID:         $Id$
     8.7      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     8.8      Copyright   1999  University of Cambridge
     8.9 @@ -6,7 +6,7 @@
    8.10  
    8.11  header{*Binary arithmetic and Simplification for the Hyperreals*}
    8.12  
    8.13 -theory HyperArith = HyperOrd
    8.14 +theory HyperArith = HyperDef
    8.15  files ("hypreal_arith.ML"):
    8.16  
    8.17  subsection{*Binary Arithmetic for the Hyperreals*}
    8.18 @@ -156,10 +156,7 @@
    8.19  by (simp add: hypreal_divide_def hypreal_minus_inverse)
    8.20  
    8.21  
    8.22 -
    8.23 -
    8.24 -(** number_of related to hypreal_of_real.
    8.25 -Could similar theorems be useful for other injections? **)
    8.26 +subsection{*The Function @{term hypreal_of_real}*}
    8.27  
    8.28  lemma number_of_less_hypreal_of_real_iff [simp]:
    8.29       "(number_of w < hypreal_of_real z) = (number_of w < z)"
    8.30 @@ -191,8 +188,114 @@
    8.31  apply (simp (no_asm))
    8.32  done
    8.33  
    8.34 +subsection{*Absolute Value Function for the Hyperreals*}
    8.35 +
    8.36 +lemma hrabs_number_of [simp]:
    8.37 +     "abs (number_of v :: hypreal) =
    8.38 +        (if neg (number_of v) then number_of (bin_minus v)
    8.39 +         else number_of v)"
    8.40 +by (simp add: hrabs_def)
    8.41 +
    8.42 +
    8.43 +declare abs_mult [simp]
    8.44 +
    8.45 +lemma hrabs_add_less: "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
    8.46 +apply (unfold hrabs_def)
    8.47 +apply (simp split add: split_if_asm)
    8.48 +done
    8.49 +
    8.50 +lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
    8.51 +by (blast intro!: order_le_less_trans abs_ge_zero)
    8.52 +
    8.53 +lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
    8.54 +by (simp add: hrabs_def)
    8.55 +
    8.56 +(* Needed in Geom.ML *)
    8.57 +lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
    8.58 +by (simp add: hrabs_def split add: split_if_asm)
    8.59 +
    8.60 +
    8.61 +(*----------------------------------------------------------
    8.62 +    Relating hrabs to abs through embedding of IR into IR*
    8.63 + ----------------------------------------------------------*)
    8.64 +lemma hypreal_of_real_hrabs:
    8.65 +    "abs (hypreal_of_real r) = hypreal_of_real (abs r)"
    8.66 +apply (unfold hypreal_of_real_def)
    8.67 +apply (auto simp add: hypreal_hrabs)
    8.68 +done
    8.69 +
    8.70 +
    8.71 +subsection{*Embedding the Naturals into the Hyperreals*}
    8.72 +
    8.73 +constdefs
    8.74 +
    8.75 +  hypreal_of_nat :: "nat => hypreal"
    8.76 +  "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"
    8.77 +
    8.78 +
    8.79 +lemma hypreal_of_nat_add [simp]:
    8.80 +     "hypreal_of_nat (m + n) = hypreal_of_nat m + hypreal_of_nat n"
    8.81 +by (simp add: hypreal_of_nat_def)
    8.82 +
    8.83 +lemma hypreal_of_nat_mult: "hypreal_of_nat (m * n) = hypreal_of_nat m * hypreal_of_nat n"
    8.84 +by (simp add: hypreal_of_nat_def)
    8.85 +declare hypreal_of_nat_mult [simp]
    8.86 +
    8.87 +lemma hypreal_of_nat_less_iff:
    8.88 +      "(n < m) = (hypreal_of_nat n < hypreal_of_nat m)"
    8.89 +apply (simp add: hypreal_of_nat_def)
    8.90 +done
    8.91 +declare hypreal_of_nat_less_iff [symmetric, simp]
    8.92 +
    8.93 +(*------------------------------------------------------------*)
    8.94 +(* naturals embedded in hyperreals                            *)
    8.95 +(* is a hyperreal c.f. NS extension                           *)
    8.96 +(*------------------------------------------------------------*)
    8.97 +
    8.98 +lemma hypreal_of_nat_iff:
    8.99 +     "hypreal_of_nat  m = Abs_hypreal(hyprel``{%n. real m})"
   8.100 +by (simp add: hypreal_of_nat_def hypreal_of_real_def real_of_nat_def)
   8.101 +
   8.102 +lemma inj_hypreal_of_nat: "inj hypreal_of_nat"
   8.103 +by (simp add: inj_on_def hypreal_of_nat_def)
   8.104 +
   8.105 +lemma hypreal_of_nat_Suc:
   8.106 +     "hypreal_of_nat (Suc n) = hypreal_of_nat n + (1::hypreal)"
   8.107 +by (simp add: hypreal_of_nat_def real_of_nat_Suc)
   8.108 +
   8.109 +(*"neg" is used in rewrite rules for binary comparisons*)
   8.110 +lemma hypreal_of_nat_number_of [simp]:
   8.111 +     "hypreal_of_nat (number_of v :: nat) =
   8.112 +         (if neg (number_of v) then 0
   8.113 +          else (number_of v :: hypreal))"
   8.114 +by (simp add: hypreal_of_nat_def)
   8.115 +
   8.116 +lemma hypreal_of_nat_zero [simp]: "hypreal_of_nat 0 = 0"
   8.117 +by (simp del: numeral_0_eq_0 add: numeral_0_eq_0 [symmetric])
   8.118 +
   8.119 +lemma hypreal_of_nat_one [simp]: "hypreal_of_nat 1 = 1"
   8.120 +by (simp add: hypreal_of_nat_Suc)
   8.121 +
   8.122 +lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})"
   8.123 +apply (induct_tac "m")
   8.124 +apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc)
   8.125 +done
   8.126 +
   8.127 +lemma hypreal_of_nat_le_iff:
   8.128 +      "(hypreal_of_nat n \<le> hypreal_of_nat m) = (n \<le> m)"
   8.129 +apply (auto simp add: linorder_not_less [symmetric])
   8.130 +done
   8.131 +declare hypreal_of_nat_le_iff [simp]
   8.132 +
   8.133 +lemma hypreal_of_nat_ge_zero: "0 \<le> hypreal_of_nat n"
   8.134 +apply (simp (no_asm) add: hypreal_of_nat_zero [symmetric] 
   8.135 +         del: hypreal_of_nat_zero)
   8.136 +done
   8.137 +declare hypreal_of_nat_ge_zero [simp]
   8.138 +
   8.139 +
   8.140  (*
   8.141 -FIXME: we should have this, as for type int, but many proofs would break.
   8.142 +FIXME: we should declare this, as for type int, but many proofs would break.
   8.143  It replaces x+-y by x-y.
   8.144  Addsimps [symmetric hypreal_diff_def]
   8.145  *)
   8.146 @@ -201,6 +304,27 @@
   8.147  {*
   8.148  val hypreal_add_minus_eq_minus = thm "hypreal_add_minus_eq_minus";
   8.149  val hypreal_le_add_order = thm"hypreal_le_add_order";
   8.150 +
   8.151 +val hypreal_of_nat_def = thm"hypreal_of_nat_def";
   8.152 +
   8.153 +val hrabs_number_of = thm "hrabs_number_of";
   8.154 +val hrabs_add_less = thm "hrabs_add_less";
   8.155 +val hrabs_less_gt_zero = thm "hrabs_less_gt_zero";
   8.156 +val hrabs_disj = thm "hrabs_disj";
   8.157 +val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
   8.158 +val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
   8.159 +val hypreal_of_nat_add = thm "hypreal_of_nat_add";
   8.160 +val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
   8.161 +val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
   8.162 +val hypreal_of_nat_iff = thm "hypreal_of_nat_iff";
   8.163 +val inj_hypreal_of_nat = thm "inj_hypreal_of_nat";
   8.164 +val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
   8.165 +val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
   8.166 +val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
   8.167 +val hypreal_of_nat_one = thm "hypreal_of_nat_one";
   8.168 +val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
   8.169 +val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
   8.170 +val hypreal_of_nat = thm"hypreal_of_nat";
   8.171  *}
   8.172  
   8.173  end
     9.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Jan 29 16:51:17 2004 +0100
     9.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Feb 02 12:23:46 2004 +0100
     9.3 @@ -323,22 +323,21 @@
     9.4  done
     9.5  
     9.6  lemma hypreal_add_commute: "(z::hypreal) + w = w + z"
     9.7 -apply (rule_tac z = z in eq_Abs_hypreal)
     9.8 -apply (rule_tac z = w in eq_Abs_hypreal)
     9.9 +apply (rule eq_Abs_hypreal [of z])
    9.10 +apply (rule eq_Abs_hypreal [of w])
    9.11  apply (simp add: add_ac hypreal_add)
    9.12  done
    9.13  
    9.14  lemma hypreal_add_assoc: "((z1::hypreal) + z2) + z3 = z1 + (z2 + z3)"
    9.15 -apply (rule_tac z = z1 in eq_Abs_hypreal)
    9.16 -apply (rule_tac z = z2 in eq_Abs_hypreal)
    9.17 -apply (rule_tac z = z3 in eq_Abs_hypreal)
    9.18 +apply (rule eq_Abs_hypreal [of z1])
    9.19 +apply (rule eq_Abs_hypreal [of z2])
    9.20 +apply (rule eq_Abs_hypreal [of z3])
    9.21  apply (simp add: hypreal_add real_add_assoc)
    9.22  done
    9.23  
    9.24  lemma hypreal_add_zero_left: "(0::hypreal) + z = z"
    9.25 -apply (unfold hypreal_zero_def)
    9.26 -apply (rule_tac z = z in eq_Abs_hypreal)
    9.27 -apply (simp add: hypreal_add)
    9.28 +apply (rule eq_Abs_hypreal [of z])
    9.29 +apply (simp add: hypreal_zero_def hypreal_add)
    9.30  done
    9.31  
    9.32  instance hypreal :: plus_ac0
    9.33 @@ -395,15 +394,15 @@
    9.34  done
    9.35  
    9.36  lemma hypreal_mult_commute: "(z::hypreal) * w = w * z"
    9.37 -apply (rule_tac z = z in eq_Abs_hypreal)
    9.38 -apply (rule_tac z = w in eq_Abs_hypreal)
    9.39 +apply (rule eq_Abs_hypreal [of z])
    9.40 +apply (rule eq_Abs_hypreal [of w])
    9.41  apply (simp add: hypreal_mult mult_ac)
    9.42  done
    9.43  
    9.44  lemma hypreal_mult_assoc: "((z1::hypreal) * z2) * z3 = z1 * (z2 * z3)"
    9.45 -apply (rule_tac z = z1 in eq_Abs_hypreal)
    9.46 -apply (rule_tac z = z2 in eq_Abs_hypreal)
    9.47 -apply (rule_tac z = z3 in eq_Abs_hypreal)
    9.48 +apply (rule eq_Abs_hypreal [of z1])
    9.49 +apply (rule eq_Abs_hypreal [of z2])
    9.50 +apply (rule eq_Abs_hypreal [of z3])
    9.51  apply (simp add: hypreal_mult mult_assoc)
    9.52  done
    9.53  
    9.54 @@ -415,9 +414,9 @@
    9.55  
    9.56  lemma hypreal_add_mult_distrib:
    9.57       "((z1::hypreal) + z2) * w = (z1 * w) + (z2 * w)"
    9.58 -apply (rule_tac z = z1 in eq_Abs_hypreal)
    9.59 -apply (rule_tac z = z2 in eq_Abs_hypreal)
    9.60 -apply (rule_tac z = w in eq_Abs_hypreal)
    9.61 +apply (rule eq_Abs_hypreal [of z1])
    9.62 +apply (rule eq_Abs_hypreal [of z2])
    9.63 +apply (rule eq_Abs_hypreal [of w])
    9.64  apply (simp add: hypreal_mult hypreal_add left_distrib)
    9.65  done
    9.66  
    9.67 @@ -448,7 +447,7 @@
    9.68  lemma hypreal_mult_inverse: 
    9.69       "x \<noteq> 0 ==> x*inverse(x) = (1::hypreal)"
    9.70  apply (unfold hypreal_one_def hypreal_zero_def)
    9.71 -apply (rule_tac z = x in eq_Abs_hypreal)
    9.72 +apply (rule eq_Abs_hypreal [of x])
    9.73  apply (simp add: hypreal_inverse hypreal_mult)
    9.74  apply (drule FreeUltrafilterNat_Compl_mem)
    9.75  apply (blast intro!: right_inverse FreeUltrafilterNat_subset)
    9.76 @@ -616,9 +615,6 @@
    9.77  apply auto
    9.78  done
    9.79  
    9.80 -lemma hypreal_inverse_not_zero: "x \<noteq> 0 ==> inverse (x::hypreal) \<noteq> 0"
    9.81 -  by (rule Ring_and_Field.nonzero_imp_inverse_nonzero)
    9.82 -
    9.83  lemma hypreal_mult_not_0: "[| x \<noteq> 0; y \<noteq> 0 |] ==> x * y \<noteq> (0::hypreal)"
    9.84  by simp
    9.85  
    9.86 @@ -646,7 +642,8 @@
    9.87  by (simp add: Ring_and_Field.inverse_add mult_assoc)
    9.88  
    9.89  
    9.90 -subsection{*@{term hypreal_of_real} Preserves Field and Order Properties*}
    9.91 +subsection{*The Embedding @{term hypreal_of_real} Preserves Field and 
    9.92 +      Order Properties*}
    9.93  
    9.94  lemma hypreal_of_real_add [simp]: 
    9.95       "hypreal_of_real (w + z) = hypreal_of_real w + hypreal_of_real z"
    9.96 @@ -890,13 +887,10 @@
    9.97  val hypreal_zero_not_eq_one = thm "hypreal_zero_not_eq_one";
    9.98  val hypreal_inverse_congruent = thm "hypreal_inverse_congruent";
    9.99  val hypreal_inverse = thm "hypreal_inverse";
   9.100 -val HYPREAL_INVERSE_ZERO = thm "HYPREAL_INVERSE_ZERO";
   9.101 -val HYPREAL_DIVISION_BY_ZERO = thm "HYPREAL_DIVISION_BY_ZERO";
   9.102  val hypreal_mult_inverse = thm "hypreal_mult_inverse";
   9.103  val hypreal_mult_inverse_left = thm "hypreal_mult_inverse_left";
   9.104  val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel";
   9.105  val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel";
   9.106 -val hypreal_inverse_not_zero = thm "hypreal_inverse_not_zero";
   9.107  val hypreal_mult_not_0 = thm "hypreal_mult_not_0";
   9.108  val hypreal_minus_inverse = thm "hypreal_minus_inverse";
   9.109  val hypreal_inverse_distrib = thm "hypreal_inverse_distrib";
    10.1 --- a/src/HOL/Hyperreal/HyperNat.ML	Thu Jan 29 16:51:17 2004 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,1334 +0,0 @@
    10.4 -(*  Title       : HyperNat.ML
    10.5 -    Author      : Jacques D. Fleuriot
    10.6 -    Copyright   : 1998  University of Cambridge
    10.7 -    Description : Explicit construction of hypernaturals using 
    10.8 -                  ultrafilters
    10.9 -*) 
   10.10 -
   10.11 -fun CLAIM_SIMP str thms =
   10.12 -               prove_goal (the_context()) str
   10.13 -               (fn prems => [cut_facts_tac prems 1,
   10.14 -                   auto_tac (claset(),simpset() addsimps thms)]);
   10.15 -fun CLAIM str = CLAIM_SIMP str [];
   10.16 -
   10.17 -(* blast confuses different versions of < *)
   10.18 -DelIffs [order_less_irrefl];
   10.19 -Addsimps [order_less_irrefl];
   10.20 -
   10.21 -(*------------------------------------------------------------------------
   10.22 -                       Properties of hypnatrel
   10.23 - ------------------------------------------------------------------------*)
   10.24 -
   10.25 -(** Proving that hyprel is an equivalence relation       **)
   10.26 -(** Natural deduction for hypnatrel - similar to hyprel! **)
   10.27 -
   10.28 -Goalw [hypnatrel_def]
   10.29 -     "((X,Y): hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)";
   10.30 -by (Fast_tac 1);
   10.31 -qed "hypnatrel_iff";
   10.32 -
   10.33 -Goalw [hypnatrel_def] 
   10.34 -     "{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hypnatrel";
   10.35 -by (Fast_tac 1);
   10.36 -qed "hypnatrelI";
   10.37 -
   10.38 -Goalw [hypnatrel_def]
   10.39 -  "p: hypnatrel --> (EX X Y. \
   10.40 -\                 p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
   10.41 -by (Fast_tac 1);
   10.42 -qed "hypnatrelE_lemma";
   10.43 -
   10.44 -val [major,minor] = Goal
   10.45 -  "[| p: hypnatrel;  \
   10.46 -\     !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat |] \
   10.47 -\            ==> Q |] \
   10.48 -\  ==> Q";
   10.49 -by (cut_facts_tac [major RS (hypnatrelE_lemma RS mp)] 1);
   10.50 -by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
   10.51 -qed "hypnatrelE";
   10.52 -
   10.53 -AddSIs [hypnatrelI];
   10.54 -AddSEs [hypnatrelE];
   10.55 -
   10.56 -Goalw [hypnatrel_def] "(x,x): hypnatrel";
   10.57 -by Auto_tac;
   10.58 -qed "hypnatrel_refl";
   10.59 -
   10.60 -Goal "(x,y): hypnatrel ==> (y,x):hypnatrel";
   10.61 -by (auto_tac (claset(), simpset() addsimps [hypnatrel_def, eq_commute]));
   10.62 -qed "hypnatrel_sym";
   10.63 -
   10.64 -Goalw [hypnatrel_def]
   10.65 -     "(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel";
   10.66 -by Auto_tac;
   10.67 -by (Fuf_tac 1);
   10.68 -qed_spec_mp "hypnatrel_trans";
   10.69 -
   10.70 -Goalw [equiv_def, refl_def, sym_def, trans_def]
   10.71 -     "equiv UNIV hypnatrel";
   10.72 -by (auto_tac (claset() addSIs [hypnatrel_refl] 
   10.73 -                       addSEs [hypnatrel_sym,hypnatrel_trans] 
   10.74 -                       delrules [hypnatrelI,hypnatrelE],
   10.75 -              simpset()));
   10.76 -qed "equiv_hypnatrel";
   10.77 -
   10.78 -val equiv_hypnatrel_iff =
   10.79 -    [UNIV_I, UNIV_I] MRS (equiv_hypnatrel RS eq_equiv_class_iff);
   10.80 -
   10.81 -Goalw  [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel``{x}:hypnat";
   10.82 -by (Blast_tac 1);
   10.83 -qed "hypnatrel_in_hypnat";
   10.84 -
   10.85 -Goal "inj_on Abs_hypnat hypnat";
   10.86 -by (rtac inj_on_inverseI 1);
   10.87 -by (etac Abs_hypnat_inverse 1);
   10.88 -qed "inj_on_Abs_hypnat";
   10.89 -
   10.90 -Addsimps [equiv_hypnatrel_iff,inj_on_Abs_hypnat RS inj_on_iff,
   10.91 -          hypnatrel_iff, hypnatrel_in_hypnat, Abs_hypnat_inverse];
   10.92 -
   10.93 -Addsimps [equiv_hypnatrel RS eq_equiv_class_iff];
   10.94 -val eq_hypnatrelD = equiv_hypnatrel RSN (2,eq_equiv_class);
   10.95 -
   10.96 -Goal "inj(Rep_hypnat)";
   10.97 -by (rtac inj_inverseI 1);
   10.98 -by (rtac Rep_hypnat_inverse 1);
   10.99 -qed "inj_Rep_hypnat";
  10.100 -
  10.101 -Goalw [hypnatrel_def] "x: hypnatrel `` {x}";
  10.102 -by (Step_tac 1);
  10.103 -by Auto_tac;
  10.104 -qed "lemma_hypnatrel_refl";
  10.105 -
  10.106 -Addsimps [lemma_hypnatrel_refl];
  10.107 -
  10.108 -Goalw [hypnat_def] "{} ~: hypnat";
  10.109 -by (auto_tac (claset() addSEs [quotientE],simpset()));
  10.110 -qed "hypnat_empty_not_mem";
  10.111 -
  10.112 -Addsimps [hypnat_empty_not_mem];
  10.113 -
  10.114 -Goal "Rep_hypnat x ~= {}";
  10.115 -by (cut_inst_tac [("x","x")] Rep_hypnat 1);
  10.116 -by Auto_tac;
  10.117 -qed "Rep_hypnat_nonempty";
  10.118 -
  10.119 -Addsimps [Rep_hypnat_nonempty];
  10.120 -
  10.121 -(*------------------------------------------------------------------------
  10.122 -   hypnat_of_nat: the injection from nat to hypnat
  10.123 - ------------------------------------------------------------------------*)
  10.124 -Goal "inj(hypnat_of_nat)";
  10.125 -by (rtac injI 1);
  10.126 -by (rewtac hypnat_of_nat_def);
  10.127 -by (dtac (inj_on_Abs_hypnat RS inj_onD) 1);
  10.128 -by (REPEAT (rtac hypnatrel_in_hypnat 1));
  10.129 -by (dtac eq_equiv_class 1);
  10.130 -by (rtac equiv_hypnatrel 1);
  10.131 -by (Fast_tac 1);
  10.132 -by (rtac ccontr 1 THEN rotate_tac 1 1);
  10.133 -by Auto_tac;
  10.134 -qed "inj_hypnat_of_nat";
  10.135 -
  10.136 -val [prem] = Goal
  10.137 -    "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P";
  10.138 -by (res_inst_tac [("x1","z")] 
  10.139 -    (rewrite_rule [hypnat_def] Rep_hypnat RS quotientE) 1);
  10.140 -by (dres_inst_tac [("f","Abs_hypnat")] arg_cong 1);
  10.141 -by (res_inst_tac [("x","x")] prem 1);
  10.142 -by (asm_full_simp_tac (simpset() addsimps [Rep_hypnat_inverse]) 1);
  10.143 -qed "eq_Abs_hypnat";
  10.144 -
  10.145 -(*-----------------------------------------------------------
  10.146 -   Addition for hyper naturals: hypnat_add 
  10.147 - -----------------------------------------------------------*)
  10.148 -Goalw [congruent2_def]
  10.149 -     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})";
  10.150 -by Safe_tac;
  10.151 -by (ALLGOALS(Fuf_tac));
  10.152 -qed "hypnat_add_congruent2";
  10.153 -
  10.154 -Goalw [hypnat_add_def]
  10.155 -  "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) = \
  10.156 -\  Abs_hypnat(hypnatrel``{%n. X n + Y n})";
  10.157 -by (asm_simp_tac
  10.158 -    (simpset() addsimps [[equiv_hypnatrel, hypnat_add_congruent2] 
  10.159 -     MRS UN_equiv_class2]) 1);
  10.160 -qed "hypnat_add";
  10.161 -
  10.162 -Goal "(z::hypnat) + w = w + z";
  10.163 -by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
  10.164 -by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
  10.165 -by (asm_simp_tac (simpset() addsimps (add_ac @ [hypnat_add])) 1);
  10.166 -qed "hypnat_add_commute";
  10.167 -
  10.168 -Goal "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)";
  10.169 -by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
  10.170 -by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
  10.171 -by (res_inst_tac [("z","z3")] eq_Abs_hypnat 1);
  10.172 -by (asm_simp_tac (simpset() addsimps [hypnat_add,add_assoc]) 1);
  10.173 -qed "hypnat_add_assoc";
  10.174 -
  10.175 -(*For AC rewriting*)
  10.176 -Goal "(x::hypnat)+(y+z)=y+(x+z)";
  10.177 -by(rtac ([hypnat_add_assoc,hypnat_add_commute] MRS
  10.178 -         read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
  10.179 -qed "hypnat_add_left_commute";
  10.180 -
  10.181 -(* hypnat addition is an AC operator *)
  10.182 -val hypnat_add_ac = [hypnat_add_assoc,hypnat_add_commute,
  10.183 -                      hypnat_add_left_commute];
  10.184 -
  10.185 -Goalw [hypnat_zero_def] "(0::hypnat) + z = z";
  10.186 -by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
  10.187 -by (asm_full_simp_tac (simpset() addsimps [hypnat_add]) 1);
  10.188 -qed "hypnat_add_zero_left";
  10.189 -
  10.190 -Goal "z + (0::hypnat) = z";
  10.191 -by (simp_tac (simpset() addsimps 
  10.192 -    [hypnat_add_zero_left,hypnat_add_commute]) 1);
  10.193 -qed "hypnat_add_zero_right";
  10.194 -
  10.195 -Addsimps [hypnat_add_zero_left,hypnat_add_zero_right];
  10.196 -
  10.197 -(*-----------------------------------------------------------
  10.198 -   Subtraction for hyper naturals: hypnat_minus
  10.199 - -----------------------------------------------------------*)
  10.200 -Goalw [congruent2_def]
  10.201 -    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})";
  10.202 -by Safe_tac;
  10.203 -by (ALLGOALS(Fuf_tac));
  10.204 -qed "hypnat_minus_congruent2";
  10.205 - 
  10.206 -Goalw [hypnat_minus_def]
  10.207 -  "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) = \
  10.208 -\  Abs_hypnat(hypnatrel``{%n. X n - Y n})";
  10.209 -by (asm_simp_tac
  10.210 -    (simpset() addsimps [[equiv_hypnatrel, hypnat_minus_congruent2] 
  10.211 -     MRS UN_equiv_class2]) 1);
  10.212 -qed "hypnat_minus";
  10.213 -
  10.214 -Goalw [hypnat_zero_def] "z - z = (0::hypnat)";
  10.215 -by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
  10.216 -by (asm_full_simp_tac (simpset() addsimps [hypnat_minus]) 1);
  10.217 -qed "hypnat_minus_zero";
  10.218 -
  10.219 -Goalw [hypnat_zero_def] "(0::hypnat) - n = 0";
  10.220 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.221 -by (asm_full_simp_tac (simpset() addsimps [hypnat_minus]) 1);
  10.222 -qed "hypnat_diff_0_eq_0";
  10.223 -
  10.224 -Addsimps [hypnat_minus_zero,hypnat_diff_0_eq_0];
  10.225 -
  10.226 -Goalw [hypnat_zero_def] "(m+n = (0::hypnat)) = (m=0 & n=0)";
  10.227 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.228 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.229 -by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
  10.230 -                       addDs [FreeUltrafilterNat_Int],
  10.231 -              simpset() addsimps [hypnat_add] ));
  10.232 -qed "hypnat_add_is_0";
  10.233 -
  10.234 -AddIffs [hypnat_add_is_0];
  10.235 -
  10.236 -Goal "!!i::hypnat. i-j-k = i - (j+k)";
  10.237 -by (res_inst_tac [("z","i")] eq_Abs_hypnat 1);
  10.238 -by (res_inst_tac [("z","j")] eq_Abs_hypnat 1);
  10.239 -by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
  10.240 -by (asm_full_simp_tac (simpset() addsimps 
  10.241 -    [hypnat_minus,hypnat_add,diff_diff_left]) 1);
  10.242 -qed "hypnat_diff_diff_left";
  10.243 -
  10.244 -Goal "!!i::hypnat. i-j-k = i-k-j";
  10.245 -by (simp_tac (simpset() addsimps 
  10.246 -    [hypnat_diff_diff_left, hypnat_add_commute]) 1);
  10.247 -qed "hypnat_diff_commute";
  10.248 -
  10.249 -Goal "!!n::hypnat. (n+m) - n = m";
  10.250 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.251 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.252 -by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
  10.253 -qed "hypnat_diff_add_inverse";
  10.254 -Addsimps [hypnat_diff_add_inverse];
  10.255 -
  10.256 -Goal "!!n::hypnat.(m+n) - n = m";
  10.257 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.258 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.259 -by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
  10.260 -qed "hypnat_diff_add_inverse2";
  10.261 -Addsimps [hypnat_diff_add_inverse2];
  10.262 -
  10.263 -Goal "!!k::hypnat. (k+m) - (k+n) = m - n";
  10.264 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.265 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.266 -by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
  10.267 -by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
  10.268 -qed "hypnat_diff_cancel";
  10.269 -Addsimps [hypnat_diff_cancel];
  10.270 -
  10.271 -Goal "!!m::hypnat. (m+k) - (n+k) = m - n";
  10.272 -val hypnat_add_commute_k = read_instantiate [("w","k")] hypnat_add_commute;
  10.273 -by (asm_simp_tac (simpset() addsimps ([hypnat_add_commute_k])) 1);
  10.274 -qed "hypnat_diff_cancel2";
  10.275 -Addsimps [hypnat_diff_cancel2];
  10.276 -
  10.277 -Goalw [hypnat_zero_def] "!!n::hypnat. n - (n+m) = (0::hypnat)";
  10.278 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.279 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.280 -by (asm_full_simp_tac (simpset() addsimps [hypnat_minus,hypnat_add]) 1);
  10.281 -qed "hypnat_diff_add_0";
  10.282 -Addsimps [hypnat_diff_add_0];
  10.283 -
  10.284 -(*-----------------------------------------------------------
  10.285 -   Multiplication for hyper naturals: hypnat_mult
  10.286 - -----------------------------------------------------------*)
  10.287 -Goalw [congruent2_def]
  10.288 -    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})";
  10.289 -by Safe_tac;
  10.290 -by (ALLGOALS(Fuf_tac));
  10.291 -qed "hypnat_mult_congruent2";
  10.292 -
  10.293 -Goalw [hypnat_mult_def]
  10.294 -  "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) = \
  10.295 -\  Abs_hypnat(hypnatrel``{%n. X n * Y n})";
  10.296 -by (asm_simp_tac
  10.297 -    (simpset() addsimps [[equiv_hypnatrel,hypnat_mult_congruent2] MRS
  10.298 -     UN_equiv_class2]) 1);
  10.299 -qed "hypnat_mult";
  10.300 -
  10.301 -Goal "(z::hypnat) * w = w * z";
  10.302 -by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
  10.303 -by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
  10.304 -by (asm_simp_tac (simpset() addsimps ([hypnat_mult] @ mult_ac)) 1);
  10.305 -qed "hypnat_mult_commute";
  10.306 -
  10.307 -Goal "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)";
  10.308 -by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
  10.309 -by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
  10.310 -by (res_inst_tac [("z","z3")] eq_Abs_hypnat 1);
  10.311 -by (asm_simp_tac (simpset() addsimps [hypnat_mult,mult_assoc]) 1);
  10.312 -qed "hypnat_mult_assoc";
  10.313 -
  10.314 -
  10.315 -Goal "(z1::hypnat) * (z2 * z3) = z2 * (z1 * z3)";
  10.316 -by(rtac ([hypnat_mult_assoc,hypnat_mult_commute] MRS
  10.317 -         read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
  10.318 -qed "hypnat_mult_left_commute";
  10.319 -
  10.320 -(* hypnat multiplication is an AC operator *)
  10.321 -val hypnat_mult_ac = [hypnat_mult_assoc, hypnat_mult_commute, 
  10.322 -                      hypnat_mult_left_commute];
  10.323 -
  10.324 -Goalw [hypnat_one_def] "(1::hypnat) * z = z";
  10.325 -by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
  10.326 -by (asm_full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
  10.327 -qed "hypnat_mult_1";
  10.328 -Addsimps [hypnat_mult_1];
  10.329 -
  10.330 -Goal "z * (1::hypnat) = z";
  10.331 -by (simp_tac (simpset() addsimps [hypnat_mult_commute]) 1);
  10.332 -qed "hypnat_mult_1_right";
  10.333 -Addsimps [hypnat_mult_1_right];
  10.334 -
  10.335 -Goalw [hypnat_zero_def] "(0::hypnat) * z = 0";
  10.336 -by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
  10.337 -by (asm_full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
  10.338 -qed "hypnat_mult_0";
  10.339 -Addsimps [hypnat_mult_0];
  10.340 -
  10.341 -Goal "z * (0::hypnat) = 0";
  10.342 -by (simp_tac (simpset() addsimps [hypnat_mult_commute]) 1);
  10.343 -qed "hypnat_mult_0_right";
  10.344 -Addsimps [hypnat_mult_0_right];
  10.345 -
  10.346 -Goal "!!m::hypnat. (m - n) * k = (m * k) - (n * k)";
  10.347 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.348 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.349 -by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
  10.350 -by (asm_simp_tac (simpset() addsimps [hypnat_mult,
  10.351 -    hypnat_minus,diff_mult_distrib]) 1);
  10.352 -qed "hypnat_diff_mult_distrib" ;
  10.353 -
  10.354 -Goal "!!m::hypnat. k * (m - n) = (k * m) - (k * n)";
  10.355 -val hypnat_mult_commute_k = read_instantiate [("z","k")] hypnat_mult_commute;
  10.356 -by (simp_tac (simpset() addsimps [hypnat_diff_mult_distrib, 
  10.357 -                                  hypnat_mult_commute_k]) 1);
  10.358 -qed "hypnat_diff_mult_distrib2" ;
  10.359 -
  10.360 -(*--------------------------
  10.361 -    A Few more theorems
  10.362 - -------------------------*)
  10.363 -
  10.364 -Goal "(z::hypnat) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
  10.365 -by (asm_simp_tac (simpset() addsimps [hypnat_add_assoc RS sym]) 1);
  10.366 -qed "hypnat_add_assoc_cong";
  10.367 -
  10.368 -Goal "(z::hypnat) + (v + w) = v + (z + w)";
  10.369 -by (REPEAT (ares_tac [hypnat_add_commute RS hypnat_add_assoc_cong] 1));
  10.370 -qed "hypnat_add_assoc_swap";
  10.371 -
  10.372 -Goal "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)";
  10.373 -by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
  10.374 -by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
  10.375 -by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
  10.376 -by (asm_simp_tac (simpset() addsimps [hypnat_mult,hypnat_add,
  10.377 -                                      add_mult_distrib]) 1);
  10.378 -qed "hypnat_add_mult_distrib";
  10.379 -Addsimps [hypnat_add_mult_distrib];
  10.380 -
  10.381 -val hypnat_mult_commute'= read_instantiate [("z","w")] hypnat_mult_commute;
  10.382 -
  10.383 -Goal "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)";
  10.384 -by (simp_tac (simpset() addsimps [hypnat_mult_commute']) 1);
  10.385 -qed "hypnat_add_mult_distrib2";
  10.386 -Addsimps [hypnat_add_mult_distrib2];
  10.387 -
  10.388 -(*** (hypnat) one and zero are distinct ***)
  10.389 -Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= (1::hypnat)";
  10.390 -by Auto_tac;
  10.391 -qed "hypnat_zero_not_eq_one";
  10.392 -Addsimps [hypnat_zero_not_eq_one];
  10.393 -Addsimps [hypnat_zero_not_eq_one RS not_sym];
  10.394 -
  10.395 -Goalw [hypnat_zero_def] "(m*n = (0::hypnat)) = (m=0 | n=0)";
  10.396 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.397 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.398 -by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
  10.399 -    simpset() addsimps [hypnat_mult]));
  10.400 -by (ALLGOALS(Fuf_tac));
  10.401 -qed "hypnat_mult_is_0";
  10.402 -Addsimps [hypnat_mult_is_0];
  10.403 -
  10.404 -(*------------------------------------------------------------------
  10.405 -                   Theorems for ordering 
  10.406 - ------------------------------------------------------------------*)
  10.407 -
  10.408 -(* prove introduction and elimination rules for hypnat_less *)
  10.409 -
  10.410 -Goalw [hypnat_less_def]
  10.411 - "(P < (Q::hypnat)) = (EX X Y. X : Rep_hypnat(P) & \
  10.412 -\                             Y : Rep_hypnat(Q) & \
  10.413 -\                             {n. X n < Y n} : FreeUltrafilterNat)";
  10.414 -by (Fast_tac 1);
  10.415 -qed "hypnat_less_iff";
  10.416 -
  10.417 -Goalw [hypnat_less_def]
  10.418 - "[| {n. X n < Y n} : FreeUltrafilterNat; \
  10.419 -\         X : Rep_hypnat(P); \
  10.420 -\         Y : Rep_hypnat(Q) |] ==> P < (Q::hypnat)";
  10.421 -by (Fast_tac 1);
  10.422 -qed "hypnat_lessI";
  10.423 -
  10.424 -Goalw [hypnat_less_def]
  10.425 -     "!! R1. [| R1 < (R2::hypnat); \
  10.426 -\         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
  10.427 -\         !!X. X : Rep_hypnat(R1) ==> P; \ 
  10.428 -\         !!Y. Y : Rep_hypnat(R2) ==> P |] \
  10.429 -\     ==> P";
  10.430 -by Auto_tac;
  10.431 -qed "hypnat_lessE";
  10.432 -
  10.433 -Goalw [hypnat_less_def]
  10.434 - "R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
  10.435 -\                                  X : Rep_hypnat(R1) & \
  10.436 -\                                  Y : Rep_hypnat(R2))";
  10.437 -by (Fast_tac 1);
  10.438 -qed "hypnat_lessD";
  10.439 -
  10.440 -Goal "~ (R::hypnat) < R";
  10.441 -by (res_inst_tac [("z","R")] eq_Abs_hypnat 1);
  10.442 -by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
  10.443 -by (Fuf_empty_tac 1);
  10.444 -qed "hypnat_less_not_refl";
  10.445 -Addsimps [hypnat_less_not_refl];
  10.446 -
  10.447 -bind_thm("hypnat_less_irrefl",hypnat_less_not_refl RS notE);
  10.448 -
  10.449 -Goalw [hypnat_less_def,hypnat_zero_def] "~ n<(0::hypnat)";
  10.450 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.451 -by Auto_tac;
  10.452 -by (Fuf_empty_tac 1);
  10.453 -qed "hypnat_not_less0";
  10.454 -AddIffs [hypnat_not_less0];
  10.455 -
  10.456 -(* n<(0::hypnat) ==> R *)
  10.457 -bind_thm ("hypnat_less_zeroE", hypnat_not_less0 RS notE);
  10.458 -
  10.459 -Goalw [hypnat_less_def,hypnat_zero_def,hypnat_one_def]
  10.460 -      "(n<(1::hypnat)) = (n=0)";
  10.461 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.462 -by (auto_tac (claset() addSIs [exI] addEs 
  10.463 -    [FreeUltrafilterNat_subset],simpset()));
  10.464 -by (Fuf_tac 1);
  10.465 -qed "hypnat_less_one";
  10.466 -AddIffs [hypnat_less_one];
  10.467 -
  10.468 -Goal "!!(R1::hypnat). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
  10.469 -by (res_inst_tac [("z","R1")] eq_Abs_hypnat 1);
  10.470 -by (res_inst_tac [("z","R2")] eq_Abs_hypnat 1);
  10.471 -by (res_inst_tac [("z","R3")] eq_Abs_hypnat 1);
  10.472 -by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
  10.473 -by (res_inst_tac [("x","X")] exI 1);
  10.474 -by Auto_tac;
  10.475 -by (res_inst_tac [("x","Ya")] exI 1);
  10.476 -by Auto_tac;
  10.477 -by (Fuf_tac 1);
  10.478 -qed "hypnat_less_trans";
  10.479 -
  10.480 -Goal "!! (R1::hypnat). [| R1 < R2; R2 < R1 |] ==> P";
  10.481 -by (dtac hypnat_less_trans 1 THEN assume_tac 1);
  10.482 -by (Asm_full_simp_tac 1);
  10.483 -qed "hypnat_less_asym";
  10.484 -
  10.485 -(*----- hypnat less iff less a.e -----*)
  10.486 -(* See comments in HYPER for corresponding thm *)
  10.487 -
  10.488 -Goalw [hypnat_less_def]
  10.489 -      "(Abs_hypnat(hypnatrel``{%n. X n}) < \
  10.490 -\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
  10.491 -\      ({n. X n < Y n} : FreeUltrafilterNat)";
  10.492 -by (auto_tac (claset() addSIs [lemma_hypnatrel_refl],simpset()));
  10.493 -by (Fuf_tac 1);
  10.494 -qed "hypnat_less";
  10.495 -
  10.496 -Goal "~ m<n --> n+(m-n) = (m::hypnat)";
  10.497 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.498 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  10.499 -by (auto_tac (claset(),simpset() addsimps 
  10.500 -    [hypnat_minus,hypnat_add,hypnat_less]));
  10.501 -by (dtac FreeUltrafilterNat_Compl_mem 1);
  10.502 -by (Fuf_tac 1);
  10.503 -qed_spec_mp "hypnat_add_diff_inverse";
  10.504 -
  10.505 -Goal "n<=m ==> n+(m-n) = (m::hypnat)";
  10.506 -by (asm_full_simp_tac (simpset() addsimps 
  10.507 -    [hypnat_add_diff_inverse, hypnat_le_def]) 1);
  10.508 -qed "hypnat_le_add_diff_inverse";
  10.509 -
  10.510 -Goal "n<=m ==> (m-n)+n = (m::hypnat)";
  10.511 -by (asm_simp_tac (simpset() addsimps [hypnat_le_add_diff_inverse, 
  10.512 -    hypnat_add_commute]) 1);
  10.513 -qed "hypnat_le_add_diff_inverse2";
  10.514 -
  10.515 -(*---------------------------------------------------------------------------------
  10.516 -                    Hyper naturals as a linearly ordered field
  10.517 - ---------------------------------------------------------------------------------*)
  10.518 -Goalw [hypnat_zero_def] 
  10.519 -     "[| (0::hypnat) < x; 0 < y |] ==> 0 < x + y";
  10.520 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  10.521 -by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
  10.522 -by (auto_tac (claset(),simpset() addsimps
  10.523 -   [hypnat_less_def,hypnat_add]));
  10.524 -by (REPEAT(Step_tac 1));
  10.525 -by (Fuf_tac 1);
  10.526 -qed "hypnat_add_order";
  10.527 -
  10.528 -Goalw [hypnat_zero_def] 
  10.529 -      "!!(x::hypnat). [| (0::hypnat) < x; 0 < y |] ==> 0 < x * y";
  10.530 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  10.531 -by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
  10.532 -by (auto_tac (claset(),simpset() addsimps 
  10.533 -    [hypnat_less_def,hypnat_mult]));
  10.534 -by (REPEAT(Step_tac 1));
  10.535 -by (Fuf_tac 1);
  10.536 -qed "hypnat_mult_order";
  10.537 -
  10.538 -(*---------------------------------------------------------------------------------
  10.539 -                   Trichotomy of the hyper naturals
  10.540 -  --------------------------------------------------------------------------------*)
  10.541 -Goalw [hypnatrel_def] "EX x. x: hypnatrel `` {%n. 0}";
  10.542 -by (res_inst_tac [("x","%n. 0")] exI 1);
  10.543 -by (Step_tac 1);
  10.544 -by Auto_tac;
  10.545 -qed "lemma_hypnatrel_0_mem";
  10.546 -
  10.547 -(* linearity is actually proved further down! *)
  10.548 -Goalw [hypnat_zero_def, hypnat_less_def]
  10.549 -     "(0::hypnat) <  x | x = 0 | x < 0";
  10.550 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  10.551 -by (Auto_tac );
  10.552 -by (REPEAT(Step_tac 1));
  10.553 -by (REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
  10.554 -by (Fuf_tac 1);
  10.555 -qed "hypnat_trichotomy";
  10.556 -
  10.557 -Goal "!!P. [| (0::hypnat) < x ==> P; \
  10.558 -\             x = 0 ==> P; \
  10.559 -\             x < 0 ==> P |] ==> P";
  10.560 -by (cut_inst_tac [("x","x")] hypnat_trichotomy 1);
  10.561 -by Auto_tac;
  10.562 -qed "hypnat_trichotomyE";
  10.563 -
  10.564 -(*----------------------------------------------------------------------------
  10.565 -            More properties of <
  10.566 - ----------------------------------------------------------------------------*)
  10.567 -Goal "!!(A::hypnat). A < B ==> A + C < B + C";
  10.568 -by (res_inst_tac [("z","A")] eq_Abs_hypnat 1);
  10.569 -by (res_inst_tac [("z","B")] eq_Abs_hypnat 1);
  10.570 -by (res_inst_tac [("z","C")] eq_Abs_hypnat 1);
  10.571 -by (auto_tac (claset(), simpset() addsimps [hypnat_less_def,hypnat_add]));
  10.572 -by (REPEAT(Step_tac 1));
  10.573 -by (Fuf_tac 1);
  10.574 -qed "hypnat_add_less_mono1";
  10.575 -
  10.576 -Goal "!!(A::hypnat). A < B ==> C + A < C + B";
  10.577 -by (auto_tac (claset() addIs [hypnat_add_less_mono1],
  10.578 -              simpset() addsimps [hypnat_add_commute]));
  10.579 -qed "hypnat_add_less_mono2";
  10.580 -
  10.581 -Goal "!!k l::hypnat. [|i<j;  k<l |] ==> i + k < j + l";
  10.582 -by (etac (hypnat_add_less_mono1 RS hypnat_less_trans) 1);
  10.583 -by (simp_tac (simpset() addsimps [hypnat_add_commute]) 1);
  10.584 -(*j moves to the end because it is free while k, l are bound*)
  10.585 -by (etac hypnat_add_less_mono1 1);
  10.586 -qed "hypnat_add_less_mono";
  10.587 -
  10.588 -(*---------------------------------------
  10.589 -        hypnat_minus_less
  10.590 - ---------------------------------------*)
  10.591 -Goalw [hypnat_less_def,hypnat_zero_def] 
  10.592 -      "((x::hypnat) < y) = ((0::hypnat) < y - x)";
  10.593 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  10.594 -by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
  10.595 -by (auto_tac (claset(),simpset() addsimps 
  10.596 -    [hypnat_minus]));
  10.597 -by (REPEAT(Step_tac 1));
  10.598 -by (REPEAT(Step_tac 2));
  10.599 -by (ALLGOALS(fuf_tac (claset() addDs [sym],simpset())));
  10.600 -
  10.601 -(*** linearity ***)
  10.602 -Goalw [hypnat_less_def] "(x::hypnat) < y | x = y | y < x";
  10.603 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  10.604 -by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
  10.605 -by (Auto_tac );
  10.606 -by (REPEAT(Step_tac 1));
  10.607 -by (REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
  10.608 -by (Fuf_tac 1);
  10.609 -qed "hypnat_linear";
  10.610 -
  10.611 -Goal "!!(x::hypnat). [| x < y ==> P;  x = y ==> P; \
  10.612 -\                       y < x ==> P |] ==> P";
  10.613 -by (cut_inst_tac [("x","x"),("y","y")] hypnat_linear 1);
  10.614 -by Auto_tac;
  10.615 -qed "hypnat_linear_less2";
  10.616 -
  10.617 -Goal "((w::hypnat) ~= z) = (w<z | z<w)";
  10.618 -by (cut_facts_tac [hypnat_linear] 1);
  10.619 -by Auto_tac;
  10.620 -qed "hypnat_neq_iff";
  10.621 -
  10.622 -(* Axiom 'order_less_le' of class 'order': *)
  10.623 -Goal "((w::hypnat) < z) = (w <= z & w ~= z)";
  10.624 -by (simp_tac (simpset() addsimps [hypnat_le_def, hypnat_neq_iff]) 1);
  10.625 -by (blast_tac (claset() addIs [hypnat_less_asym]) 1);
  10.626 -qed "hypnat_less_le";
  10.627 -
  10.628 -(*----------------------------------------------------------------------------
  10.629 -                            Properties of <=
  10.630 - ----------------------------------------------------------------------------*)
  10.631 -
  10.632 -(*------ hypnat le iff nat le a.e ------*)
  10.633 -Goalw [hypnat_le_def,le_def]
  10.634 -      "(Abs_hypnat(hypnatrel``{%n. X n}) <= \
  10.635 -\           Abs_hypnat(hypnatrel``{%n. Y n})) = \
  10.636 -\      ({n. X n <= Y n} : FreeUltrafilterNat)";
  10.637 -by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
  10.638 -    simpset() addsimps [hypnat_less]));
  10.639 -by (Fuf_tac 1 THEN Fuf_empty_tac 1);
  10.640 -qed "hypnat_le";
  10.641 -
  10.642 -(*---------------------------------------------------------*)
  10.643 -(*---------------------------------------------------------*)
  10.644 -
  10.645 -Goalw [hypnat_le_def] "z < w ==> z <= (w::hypnat)";
  10.646 -by (fast_tac (claset() addEs [hypnat_less_asym]) 1);
  10.647 -qed "hypnat_less_imp_le";
  10.648 -
  10.649 -Goalw [hypnat_le_def] "!!(x::hypnat). x <= y ==> x < y | x = y";
  10.650 -by (cut_facts_tac [hypnat_linear] 1);
  10.651 -by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
  10.652 -qed "hypnat_le_imp_less_or_eq";
  10.653 -
  10.654 -Goalw [hypnat_le_def] "z<w | z=w ==> z <=(w::hypnat)";
  10.655 -by (cut_facts_tac [hypnat_linear] 1);
  10.656 -by (blast_tac (claset() addDs [hypnat_less_irrefl,hypnat_less_asym]) 1);
  10.657 -qed "hypnat_less_or_eq_imp_le";
  10.658 -
  10.659 -Goal "(x <= (y::hypnat)) = (x < y | x=y)";
  10.660 -by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, 
  10.661 -                     hypnat_le_imp_less_or_eq] 1));
  10.662 -qed "hypnat_le_less";
  10.663 -
  10.664 -(* Axiom 'linorder_linear' of class 'linorder': *)
  10.665 -Goal "(z::hypnat) <= w | w <= z";
  10.666 -by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
  10.667 -by (cut_facts_tac [hypnat_linear] 1);
  10.668 -by (Blast_tac 1);
  10.669 -qed "hypnat_le_linear";
  10.670 -
  10.671 -Goal "w <= (w::hypnat)";
  10.672 -by (simp_tac (simpset() addsimps [hypnat_le_less]) 1);
  10.673 -qed "hypnat_le_refl";
  10.674 -Addsimps [hypnat_le_refl];
  10.675 -
  10.676 -Goal "[| i <= j; j <= k |] ==> i <= (k::hypnat)";
  10.677 -by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
  10.678 -            rtac hypnat_less_or_eq_imp_le, 
  10.679 -            fast_tac (claset() addIs [hypnat_less_trans])]);
  10.680 -qed "hypnat_le_trans";
  10.681 -
  10.682 -Goal "[| z <= w; w <= z |] ==> z = (w::hypnat)";
  10.683 -by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
  10.684 -            fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym])]);
  10.685 -qed "hypnat_le_anti_sym";
  10.686 -
  10.687 -Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y";
  10.688 -by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
  10.689 -by (auto_tac (claset() addIs [hypnat_mult_order, hypnat_less_imp_le],
  10.690 -              simpset() addsimps [hypnat_le_refl]));
  10.691 -qed "hypnat_le_mult_order";
  10.692 -
  10.693 -Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] 
  10.694 -      "(0::hypnat) < (1::hypnat)";
  10.695 -by (res_inst_tac [("x","%n. 0")] exI 1);
  10.696 -by (res_inst_tac [("x","%n. Suc 0")] exI 1);
  10.697 -by Auto_tac;
  10.698 -qed "hypnat_zero_less_one";
  10.699 -
  10.700 -Goal "[| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y";
  10.701 -by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
  10.702 -by (auto_tac (claset() addIs [hypnat_add_order,
  10.703 -    hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
  10.704 -qed "hypnat_le_add_order";
  10.705 -
  10.706 -Goal "!!(q1::hypnat). q1 <= q2  ==> x + q1 <= x + q2";
  10.707 -by (dtac hypnat_le_imp_less_or_eq 1);
  10.708 -by (Step_tac 1);
  10.709 -by (auto_tac (claset() addSIs [hypnat_le_refl,
  10.710 -    hypnat_less_imp_le,hypnat_add_less_mono1],
  10.711 -    simpset() addsimps [hypnat_add_commute]));
  10.712 -qed "hypnat_add_le_mono2";
  10.713 -
  10.714 -Goal "!!(q1::hypnat). q1 <= q2  ==> q1 + x <= q2 + x";
  10.715 -by (auto_tac (claset() addDs [hypnat_add_le_mono2],
  10.716 -    simpset() addsimps [hypnat_add_commute]));
  10.717 -qed "hypnat_add_le_mono1";
  10.718 -
  10.719 -Goal "!!k l::hypnat. [|i<=j;  k<=l |] ==> i + k <= j + l";
  10.720 -by (etac (hypnat_add_le_mono1 RS hypnat_le_trans) 1);
  10.721 -by (simp_tac (simpset() addsimps [hypnat_add_commute]) 1);
  10.722 -(*j moves to the end because it is free while k, l are bound*)
  10.723 -by (etac hypnat_add_le_mono1 1);
  10.724 -qed "hypnat_add_le_mono";
  10.725 -
  10.726 -Goalw [hypnat_zero_def]
  10.727 -     "!!x::hypnat. [| (0::hypnat) < z; x < y |] ==> x * z < y * z";
  10.728 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  10.729 -by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
  10.730 -by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
  10.731 -by (auto_tac (claset(),simpset() addsimps 
  10.732 -    [hypnat_less,hypnat_mult]));
  10.733 -by (Fuf_tac 1);
  10.734 -qed "hypnat_mult_less_mono1";
  10.735 -
  10.736 -Goal "!!x::hypnat. [| 0 < z; x < y |] ==> z * x < z * y";
  10.737 -by (auto_tac (claset() addIs [hypnat_mult_less_mono1],
  10.738 -              simpset() addsimps [hypnat_mult_commute]));
  10.739 -qed "hypnat_mult_less_mono2";
  10.740 -
  10.741 -Addsimps [hypnat_mult_less_mono2,hypnat_mult_less_mono1];
  10.742 -
  10.743 -Goal "(x::hypnat) <= n + x";
  10.744 -by (res_inst_tac [("x","n")] hypnat_trichotomyE 1);
  10.745 -by (auto_tac (claset() addDs [(hypnat_less_imp_le RS
  10.746 -    hypnat_add_le_mono1)],simpset() addsimps [hypnat_le_refl]));
  10.747 -qed "hypnat_add_self_le";
  10.748 -Addsimps [hypnat_add_self_le];
  10.749 -
  10.750 -Goal "(x::hypnat) < x + (1::hypnat)";
  10.751 -by (cut_facts_tac [hypnat_zero_less_one 
  10.752 -         RS hypnat_add_less_mono2] 1);
  10.753 -by Auto_tac;
  10.754 -qed "hypnat_add_one_self_less";
  10.755 -Addsimps [hypnat_add_one_self_less];
  10.756 -
  10.757 -Goalw [hypnat_le_def] "~ x + (1::hypnat) <= x";
  10.758 -by (Simp_tac 1);
  10.759 -qed "not_hypnat_add_one_le_self";
  10.760 -Addsimps [not_hypnat_add_one_le_self];
  10.761 -
  10.762 -Goal "((0::hypnat) < n) = ((1::hypnat) <= n)";
  10.763 -by (res_inst_tac [("x","n")] hypnat_trichotomyE 1);
  10.764 -by (auto_tac (claset(),simpset() addsimps [hypnat_le_def]));
  10.765 -qed "hypnat_gt_zero_iff";
  10.766 -
  10.767 -Addsimps  [hypnat_le_add_diff_inverse, hypnat_le_add_diff_inverse2,
  10.768 -           hypnat_less_imp_le RS hypnat_le_add_diff_inverse2];
  10.769 -
  10.770 -Goal "(0 < n) = (EX m. n = m + (1::hypnat))";
  10.771 -by (Step_tac 1);
  10.772 -by (res_inst_tac [("x","m")] hypnat_trichotomyE 2);
  10.773 -by (rtac hypnat_less_trans 2);
  10.774 -by (res_inst_tac [("x","n - (1::hypnat)")] exI 1);
  10.775 -by (auto_tac (claset(),simpset() addsimps 
  10.776 -    [hypnat_gt_zero_iff,hypnat_add_commute]));
  10.777 -qed "hypnat_gt_zero_iff2";
  10.778 -
  10.779 -Goalw [hypnat_zero_def] "(0::hypnat) <= n";
  10.780 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  10.781 -by (asm_simp_tac (simpset() addsimps [hypnat_le]) 1);
  10.782 -qed "hypnat_le_zero";
  10.783 -Addsimps [hypnat_le_zero];
  10.784 -
  10.785 -(*------------------------------------------------------------------
  10.786 -     hypnat_of_nat: properties embedding of naturals in hypernaturals
  10.787 - -----------------------------------------------------------------*)
  10.788 -    (** hypnat_of_nat preserves field and order properties **)
  10.789 -
  10.790 -Goalw [hypnat_of_nat_def] 
  10.791 -      "hypnat_of_nat ((z1::nat) + z2) = \
  10.792 -\      hypnat_of_nat z1 + hypnat_of_nat z2";
  10.793 -by (asm_simp_tac (simpset() addsimps [hypnat_add]) 1);
  10.794 -qed "hypnat_of_nat_add";
  10.795 -
  10.796 -Goalw [hypnat_of_nat_def] 
  10.797 -      "hypnat_of_nat ((z1::nat) - z2) = \
  10.798 -\      hypnat_of_nat z1 - hypnat_of_nat z2";
  10.799 -by (asm_simp_tac (simpset() addsimps [hypnat_minus]) 1);
  10.800 -qed "hypnat_of_nat_minus";
  10.801 -
  10.802 -Goalw [hypnat_of_nat_def] 
  10.803 -      "hypnat_of_nat (z1 * z2) = hypnat_of_nat z1 * hypnat_of_nat z2";
  10.804 -by (full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
  10.805 -qed "hypnat_of_nat_mult";
  10.806 -
  10.807 -Goalw [hypnat_less_def,hypnat_of_nat_def] 
  10.808 -      "(z1 < z2) = (hypnat_of_nat z1 < hypnat_of_nat z2)";
  10.809 -by (auto_tac (claset() addSIs [exI] addIs 
  10.810 -   [FreeUltrafilterNat_all],simpset()));
  10.811 -by (rtac FreeUltrafilterNat_P 1 THEN Fuf_tac 1);
  10.812 -qed "hypnat_of_nat_less_iff";
  10.813 -Addsimps [hypnat_of_nat_less_iff RS sym];
  10.814 -
  10.815 -Goalw [hypnat_le_def,le_def] 
  10.816 -      "(z1 <= z2) = (hypnat_of_nat z1 <= hypnat_of_nat z2)";
  10.817 -by Auto_tac;
  10.818 -qed "hypnat_of_nat_le_iff";
  10.819 -
  10.820 -Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat (Suc 0) = (1::hypnat)";
  10.821 -by (Simp_tac 1);
  10.822 -qed "hypnat_of_nat_one";
  10.823 -
  10.824 -Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat 0 = 0";
  10.825 -by (Simp_tac 1);
  10.826 -qed "hypnat_of_nat_zero";
  10.827 -
  10.828 -Goal "(hypnat_of_nat  n = 0) = (n = 0)";
  10.829 -by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
  10.830 -    simpset() addsimps [hypnat_of_nat_def,
  10.831 -    hypnat_zero_def]));
  10.832 -qed "hypnat_of_nat_zero_iff";
  10.833 -
  10.834 -Goal "(hypnat_of_nat  n ~= 0) = (n ~= 0)";
  10.835 -by (full_simp_tac (simpset() addsimps [hypnat_of_nat_zero_iff]) 1);
  10.836 -qed "hypnat_of_nat_not_zero_iff";
  10.837 -
  10.838 -Goalw [hypnat_of_nat_def,hypnat_one_def]
  10.839 -     "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)";
  10.840 -by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
  10.841 -qed "hypnat_of_nat_Suc";
  10.842 -
  10.843 -(*---------------------------------------------------------------------------------
  10.844 -              Existence of infinite hypernatural number
  10.845 - ---------------------------------------------------------------------------------*)
  10.846 -
  10.847 -Goal "hypnatrel``{%n::nat. n} : hypnat";
  10.848 -by Auto_tac;
  10.849 -qed "hypnat_omega";
  10.850 -
  10.851 -Goalw [hypnat_omega_def] "Rep_hypnat(whn) : hypnat";
  10.852 -by (rtac Rep_hypnat 1);
  10.853 -qed "Rep_hypnat_omega";
  10.854 -
  10.855 -(* See Hyper.thy for similar argument*)
  10.856 -(* existence of infinite number not corresponding to any natural number *)
  10.857 -(* use assumption that member FreeUltrafilterNat is not finite       *)
  10.858 -(* a few lemmas first *)
  10.859 -
  10.860 -Goalw [hypnat_omega_def,hypnat_of_nat_def]
  10.861 -      "~ (EX x. hypnat_of_nat x = whn)";
  10.862 -by (auto_tac (claset() addDs [FreeUltrafilterNat_not_finite], 
  10.863 -              simpset()));
  10.864 -qed "not_ex_hypnat_of_nat_eq_omega";
  10.865 -
  10.866 -Goal "hypnat_of_nat x ~= whn";
  10.867 -by (cut_facts_tac [not_ex_hypnat_of_nat_eq_omega] 1);
  10.868 -by Auto_tac;
  10.869 -qed "hypnat_of_nat_not_eq_omega";
  10.870 -Addsimps [hypnat_of_nat_not_eq_omega RS not_sym];
  10.871 -
  10.872 -(*-----------------------------------------------------------
  10.873 -    Properties of the set Nats of embedded natural numbers
  10.874 -              (cf. set Reals in NSA.thy/NSA.ML)
  10.875 - ----------------------------------------------------------*)
  10.876 -
  10.877 -(* Infinite hypernatural not in embedded Nats *)
  10.878 -Goalw [SHNat_def] "whn ~: Nats";
  10.879 -by Auto_tac;
  10.880 -qed "SHNAT_omega_not_mem";
  10.881 -Addsimps [SHNAT_omega_not_mem];
  10.882 -
  10.883 -(*-----------------------------------------------------------------------
  10.884 -     Closure laws for members of (embedded) set standard naturals Nats
  10.885 - -----------------------------------------------------------------------*)
  10.886 -Goalw [SHNat_def] 
  10.887 -     "!!x::hypnat. [| x: Nats; y: Nats |] ==> x + y: Nats";
  10.888 -by (Step_tac 1);
  10.889 -by (res_inst_tac [("x","N + Na")] exI 1);
  10.890 -by (simp_tac (simpset() addsimps [hypnat_of_nat_add]) 1);
  10.891 -qed "SHNat_add";
  10.892 -
  10.893 -Goalw [SHNat_def] 
  10.894 -     "!!x::hypnat. [| x: Nats; y: Nats |] ==> x - y: Nats";
  10.895 -by (Step_tac 1);
  10.896 -by (res_inst_tac [("x","N - Na")] exI 1);
  10.897 -by (simp_tac (simpset() addsimps [hypnat_of_nat_minus]) 1);
  10.898 -qed "SHNat_minus";
  10.899 -
  10.900 -Goalw [SHNat_def] 
  10.901 -     "!!x::hypnat. [| x: Nats; y: Nats |] ==> x * y: Nats";
  10.902 -by (Step_tac 1);
  10.903 -by (res_inst_tac [("x","N * Na")] exI 1);
  10.904 -by (simp_tac (simpset() addsimps [hypnat_of_nat_mult]) 1);
  10.905 -qed "SHNat_mult";
  10.906 -
  10.907 -Goal"!!x::hypnat. [| x + y : Nats; y: Nats |] ==> x: Nats";
  10.908 -by (dres_inst_tac [("x","x+y")] SHNat_minus 1);
  10.909 -by Auto_tac;
  10.910 -qed "SHNat_add_cancel";
  10.911 -
  10.912 -Goalw [SHNat_def] "hypnat_of_nat x : Nats";
  10.913 -by (Blast_tac 1);
  10.914 -qed "SHNat_hypnat_of_nat";
  10.915 -Addsimps [SHNat_hypnat_of_nat];
  10.916 -
  10.917 -Goal "hypnat_of_nat (Suc 0) : Nats";
  10.918 -by (Simp_tac 1);
  10.919 -qed "SHNat_hypnat_of_nat_one";
  10.920 -
  10.921 -Goal "hypnat_of_nat 0 : Nats";
  10.922 -by (Simp_tac 1);
  10.923 -qed "SHNat_hypnat_of_nat_zero";
  10.924 -
  10.925 -Goal "(1::hypnat) : Nats";
  10.926 -by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one,
  10.927 -    hypnat_of_nat_one RS sym]) 1);
  10.928 -qed "SHNat_one";
  10.929 -
  10.930 -Goal "(0::hypnat) : Nats";
  10.931 -by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_zero,
  10.932 -                                  hypnat_of_nat_zero RS sym]) 1);
  10.933 -qed "SHNat_zero";
  10.934 -
  10.935 -Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero,
  10.936 -          SHNat_one,SHNat_zero];
  10.937 -
  10.938 -Goal "(1::hypnat) + (1::hypnat) : Nats";
  10.939 -by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1);
  10.940 -qed "SHNat_two";
  10.941 -
  10.942 -Goalw [SHNat_def] "{x. hypnat_of_nat x : Nats} = (UNIV::nat set)";
  10.943 -by Auto_tac;
  10.944 -qed "SHNat_UNIV_nat";
  10.945 -
  10.946 -Goalw [SHNat_def] "(x: Nats) = (EX y. x = hypnat_of_nat  y)";
  10.947 -by Auto_tac;
  10.948 -qed "SHNat_iff";
  10.949 -
  10.950 -Goalw [SHNat_def] "hypnat_of_nat `(UNIV::nat set) = Nats";
  10.951 -by Auto_tac;
  10.952 -qed "hypnat_of_nat_image";
  10.953 -
  10.954 -Goalw [SHNat_def] "inv hypnat_of_nat `Nats = (UNIV::nat set)";
  10.955 -by Auto_tac;
  10.956 -by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1);
  10.957 -by (Blast_tac 1);
  10.958 -qed "inv_hypnat_of_nat_image";
  10.959 -
  10.960 -Goalw [SHNat_def] 
  10.961 -     "[| EX x. x: P; P <= Nats |] ==> EX Q. P = hypnat_of_nat ` Q";
  10.962 -by (Blast_tac 1);
  10.963 -qed "SHNat_hypnat_of_nat_image";
  10.964 -
  10.965 -Goalw [SHNat_def] 
  10.966 -      "Nats = hypnat_of_nat ` (UNIV::nat set)";
  10.967 -by Auto_tac;
  10.968 -qed "SHNat_hypnat_of_nat_iff";
  10.969 -
  10.970 -Goalw [SHNat_def] "Nats <= (UNIV::hypnat set)";
  10.971 -by Auto_tac;
  10.972 -qed "SHNat_subset_UNIV";
  10.973 -
  10.974 -Goal "{n. n <= Suc m} = {n. n <= m} Un {n. n = Suc m}";
  10.975 -by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
  10.976 -qed "leSuc_Un_eq";
  10.977 -
  10.978 -Goal "finite {n::nat. n <= m}";
  10.979 -by (induct_tac "m" 1);
  10.980 -by (auto_tac (claset(),simpset() addsimps [leSuc_Un_eq]));
  10.981 -qed "finite_nat_le_segment";
  10.982 -
  10.983 -Goal "{n::nat. m < n} : FreeUltrafilterNat";
  10.984 -by (cut_inst_tac [("m2","m")] (finite_nat_le_segment RS 
  10.985 -    FreeUltrafilterNat_finite RS FreeUltrafilterNat_Compl_mem) 1);
  10.986 -by (Fuf_tac 1);
  10.987 -qed "lemma_unbounded_set";
  10.988 -Addsimps [lemma_unbounded_set];
  10.989 -
  10.990 -Goalw [SHNat_def,hypnat_of_nat_def, hypnat_less_def,hypnat_omega_def] 
  10.991 -     "ALL n: Nats. n < whn";
  10.992 -by (Clarify_tac 1);
  10.993 -by (auto_tac (claset() addSIs [exI],simpset()));
  10.994 -qed "hypnat_omega_gt_SHNat";
  10.995 -
  10.996 -Goal "hypnat_of_nat n < whn";
  10.997 -by (cut_facts_tac [hypnat_omega_gt_SHNat] 1);
  10.998 -by (dres_inst_tac [("x","hypnat_of_nat n")] bspec 1);
  10.999 -by Auto_tac;
 10.1000 -qed "hypnat_of_nat_less_whn";
 10.1001 -Addsimps [hypnat_of_nat_less_whn];
 10.1002 -
 10.1003 -Goal "hypnat_of_nat n <= whn";
 10.1004 -by (rtac (hypnat_of_nat_less_whn RS hypnat_less_imp_le) 1);
 10.1005 -qed "hypnat_of_nat_le_whn";
 10.1006 -Addsimps [hypnat_of_nat_le_whn];
 10.1007 -
 10.1008 -Goal "0 < whn";
 10.1009 -by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
 10.1010 -by Auto_tac;
 10.1011 -qed "hypnat_zero_less_hypnat_omega";
 10.1012 -Addsimps [hypnat_zero_less_hypnat_omega];
 10.1013 -
 10.1014 -Goal "(1::hypnat) < whn";
 10.1015 -by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
 10.1016 -by Auto_tac;
 10.1017 -qed "hypnat_one_less_hypnat_omega";
 10.1018 -Addsimps [hypnat_one_less_hypnat_omega];
 10.1019 -
 10.1020 -(*--------------------------------------------------------------------------
 10.1021 -     Theorems about infinite hypernatural numbers -- HNatInfinite
 10.1022 - -------------------------------------------------------------------------*)
 10.1023 -Goalw [HNatInfinite_def,SHNat_def] "whn : HNatInfinite";
 10.1024 -by Auto_tac;
 10.1025 -qed "HNatInfinite_whn";
 10.1026 -Addsimps [HNatInfinite_whn];
 10.1027 -
 10.1028 -Goalw [HNatInfinite_def] "x: Nats ==> x ~: HNatInfinite";
 10.1029 -by (Simp_tac 1);
 10.1030 -qed "SHNat_not_HNatInfinite";
 10.1031 -
 10.1032 -Goalw [HNatInfinite_def] "x ~: HNatInfinite ==> x: Nats";
 10.1033 -by (Asm_full_simp_tac 1);
 10.1034 -qed "not_HNatInfinite_SHNat";
 10.1035 -
 10.1036 -Goalw [HNatInfinite_def] "x ~: Nats ==> x: HNatInfinite";
 10.1037 -by (Simp_tac 1);
 10.1038 -qed "not_SHNat_HNatInfinite";
 10.1039 -
 10.1040 -Goalw [HNatInfinite_def] "x: HNatInfinite ==> x ~: Nats";
 10.1041 -by (Asm_full_simp_tac 1);
 10.1042 -qed "HNatInfinite_not_SHNat";
 10.1043 -
 10.1044 -Goal "(x: Nats) = (x ~: HNatInfinite)";
 10.1045 -by (blast_tac (claset() addSIs [SHNat_not_HNatInfinite,
 10.1046 -    not_HNatInfinite_SHNat]) 1);
 10.1047 -qed "SHNat_not_HNatInfinite_iff";
 10.1048 -
 10.1049 -Goal "(x ~: Nats) = (x: HNatInfinite)";
 10.1050 -by (blast_tac (claset() addSIs [not_SHNat_HNatInfinite,
 10.1051 -    HNatInfinite_not_SHNat]) 1);
 10.1052 -qed "not_SHNat_HNatInfinite_iff";
 10.1053 -
 10.1054 -Goal "x : Nats | x : HNatInfinite";
 10.1055 -by (simp_tac (simpset() addsimps [SHNat_not_HNatInfinite_iff]) 1);
 10.1056 -qed "SHNat_HNatInfinite_disj";
 10.1057 -
 10.1058 -(*-------------------------------------------------------------------
 10.1059 -   Proof of alternative definition for set of Infinite hypernatural 
 10.1060 -   numbers --- HNatInfinite = {N. ALL n: Nats. n < N}
 10.1061 - -------------------------------------------------------------------*)
 10.1062 -Goal "ALL N::nat. {n. f n ~= N} : FreeUltrafilterNat  \
 10.1063 -\     ==> {n. N < f n} : FreeUltrafilterNat";
 10.1064 -by (induct_tac "N" 1);
 10.1065 -by (dres_inst_tac [("x","0")] spec 1);
 10.1066 -by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1
 10.1067 -    THEN dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
 10.1068 -by (Asm_full_simp_tac 1);
 10.1069 -by (dres_inst_tac [("x","Suc n")] spec 1);
 10.1070 -by (fuf_tac (claset() addSDs [Suc_leI],
 10.1071 -             simpset() addsimps [le_eq_less_or_eq]) 1);
 10.1072 -qed "HNatInfinite_FreeUltrafilterNat_lemma";
 10.1073 -
 10.1074 -(*** alternative definition ***)
 10.1075 -Goalw [HNatInfinite_def,SHNat_def,hypnat_of_nat_def] 
 10.1076 -     "HNatInfinite = {N. ALL n:Nats. n < N}";
 10.1077 -by (Step_tac 1);
 10.1078 -by (dres_inst_tac [("x","Abs_hypnat (hypnatrel `` {%n. N})")] bspec 2);
 10.1079 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 10.1080 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 10.1081 -by (auto_tac (claset(),simpset() addsimps [hypnat_less_iff]));
 10.1082 -by (auto_tac (claset() addSIs [exI] 
 10.1083 -                       addEs [HNatInfinite_FreeUltrafilterNat_lemma],
 10.1084 -    simpset() addsimps [FreeUltrafilterNat_Compl_iff1, 
 10.1085 -                 CLAIM "- {n. xa n = N} = {n. xa n ~= N}"]));
 10.1086 -qed "HNatInfinite_iff";
 10.1087 -
 10.1088 -(*--------------------------------------------------------------------
 10.1089 -   Alternative definition for HNatInfinite using Free ultrafilter
 10.1090 - --------------------------------------------------------------------*)
 10.1091 -Goal "x : HNatInfinite ==> EX X: Rep_hypnat x. \
 10.1092 -\                           ALL u. {n. u < X n}:  FreeUltrafilterNat";
 10.1093 -by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
 10.1094 -    HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
 10.1095 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 10.1096 -by (EVERY[Auto_tac, rtac bexI 1, 
 10.1097 -    rtac lemma_hypnatrel_refl 2, Step_tac 1]);
 10.1098 -by (dres_inst_tac [("x","hypnat_of_nat u")] bspec 1);
 10.1099 -by (Simp_tac 1);
 10.1100 -by (auto_tac (claset(),
 10.1101 -    simpset() addsimps [hypnat_of_nat_def]));
 10.1102 -by (Fuf_tac 1);
 10.1103 -qed "HNatInfinite_FreeUltrafilterNat";
 10.1104 -
 10.1105 -Goal "EX X: Rep_hypnat x. ALL u. {n. u < X n}:  FreeUltrafilterNat \
 10.1106 -\     ==> x: HNatInfinite";
 10.1107 -by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
 10.1108 -    HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
 10.1109 -by (rtac exI 1 THEN Auto_tac);
 10.1110 -qed "FreeUltrafilterNat_HNatInfinite";
 10.1111 -
 10.1112 -Goal "(x : HNatInfinite) = (EX X: Rep_hypnat x. \
 10.1113 -\          ALL u. {n. u < X n}:  FreeUltrafilterNat)";
 10.1114 -by (blast_tac (claset() addIs [HNatInfinite_FreeUltrafilterNat,
 10.1115 -    FreeUltrafilterNat_HNatInfinite]) 1);
 10.1116 -qed "HNatInfinite_FreeUltrafilterNat_iff";
 10.1117 -
 10.1118 -Goal "x : HNatInfinite ==> (1::hypnat) < x";
 10.1119 -by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
 10.1120 -qed "HNatInfinite_gt_one";
 10.1121 -Addsimps [HNatInfinite_gt_one];
 10.1122 -
 10.1123 -Goal "0 ~: HNatInfinite";
 10.1124 -by (auto_tac (claset(),simpset() 
 10.1125 -    addsimps [HNatInfinite_iff]));
 10.1126 -by (dres_inst_tac [("a","(1::hypnat)")] equals0D 1);
 10.1127 -by (Asm_full_simp_tac 1);
 10.1128 -qed "zero_not_mem_HNatInfinite";
 10.1129 -Addsimps [zero_not_mem_HNatInfinite];
 10.1130 -
 10.1131 -Goal "x : HNatInfinite ==> x ~= 0";
 10.1132 -by Auto_tac;
 10.1133 -qed "HNatInfinite_not_eq_zero";
 10.1134 -
 10.1135 -Goal "x : HNatInfinite ==> (1::hypnat) <= x";
 10.1136 -by (blast_tac (claset() addIs [hypnat_less_imp_le,
 10.1137 -         HNatInfinite_gt_one]) 1);
 10.1138 -qed "HNatInfinite_ge_one";
 10.1139 -Addsimps [HNatInfinite_ge_one];
 10.1140 -
 10.1141 -(*--------------------------------------------------
 10.1142 -                   Closure Rules
 10.1143 - --------------------------------------------------*)
 10.1144 -Goal "[| x: HNatInfinite; y: HNatInfinite |] \
 10.1145 -\           ==> x + y: HNatInfinite";
 10.1146 -by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
 10.1147 -by (dtac bspec 1 THEN assume_tac 1);
 10.1148 -by (dtac (SHNat_zero RSN (2,bspec)) 1);
 10.1149 -by (dtac hypnat_add_less_mono 1 THEN assume_tac 1);
 10.1150 -by (Asm_full_simp_tac 1);
 10.1151 -qed "HNatInfinite_add";
 10.1152 -
 10.1153 -Goal "[| x: HNatInfinite; y: Nats |] ==> x + y: HNatInfinite";
 10.1154 -by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
 10.1155 -by (dres_inst_tac [("x","x + y")] SHNat_minus 1);
 10.1156 -by (auto_tac (claset(),simpset() addsimps 
 10.1157 -    [SHNat_not_HNatInfinite_iff]));
 10.1158 -qed "HNatInfinite_SHNat_add";
 10.1159 -
 10.1160 -Goal "[| x: HNatInfinite; y: Nats |] ==> x - y: HNatInfinite";
 10.1161 -by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
 10.1162 -by (dres_inst_tac [("x","x - y")] SHNat_add 1);
 10.1163 -by (subgoal_tac "y <= x" 2);
 10.1164 -by (auto_tac (claset() addSDs [hypnat_le_add_diff_inverse2],
 10.1165 -    simpset() addsimps [not_SHNat_HNatInfinite_iff RS sym]));
 10.1166 -by (auto_tac (claset() addSIs [hypnat_less_imp_le],
 10.1167 -    simpset() addsimps [not_SHNat_HNatInfinite_iff,HNatInfinite_iff]));
 10.1168 -qed "HNatInfinite_SHNat_diff";
 10.1169 -
 10.1170 -Goal "x: HNatInfinite ==> x + (1::hypnat): HNatInfinite";
 10.1171 -by (auto_tac (claset() addIs [HNatInfinite_SHNat_add],
 10.1172 -              simpset()));
 10.1173 -qed "HNatInfinite_add_one";
 10.1174 -
 10.1175 -Goal "x: HNatInfinite ==> x - (1::hypnat): HNatInfinite";
 10.1176 -by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
 10.1177 -by (dres_inst_tac [("x","x - (1::hypnat)"),("y","(1::hypnat)")] SHNat_add 1);
 10.1178 -by (auto_tac (claset(),simpset() addsimps 
 10.1179 -    [not_SHNat_HNatInfinite_iff RS sym]));
 10.1180 -qed "HNatInfinite_minus_one";
 10.1181 -
 10.1182 -Goal "x : HNatInfinite ==> EX y. x = y + (1::hypnat)";
 10.1183 -by (res_inst_tac [("x","x - (1::hypnat)")] exI 1);
 10.1184 -by Auto_tac;
 10.1185 -qed "HNatInfinite_is_Suc";
 10.1186 -
 10.1187 -(*---------------------------------------------------------------
 10.1188 -       HNat : the hypernaturals embedded in the hyperreals
 10.1189 -       Obtained using the NS extension of the naturals
 10.1190 - --------------------------------------------------------------*)
 10.1191 - 
 10.1192 -Goalw [HNat_def,starset_def, hypreal_of_nat_def,hypreal_of_real_def] 
 10.1193 -     "hypreal_of_nat N : HNat";
 10.1194 -by Auto_tac;
 10.1195 -by (Ultra_tac 1);
 10.1196 -by (res_inst_tac [("x","N")] exI 1);
 10.1197 -by Auto_tac;  
 10.1198 -qed "HNat_hypreal_of_nat";
 10.1199 -Addsimps [HNat_hypreal_of_nat];
 10.1200 -
 10.1201 -Goalw [HNat_def,starset_def]
 10.1202 -     "[| x: HNat; y: HNat |] ==> x + y: HNat";
 10.1203 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 10.1204 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
 10.1205 -by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
 10.1206 -              simpset() addsimps [hypreal_add]));
 10.1207 -by (Ultra_tac 1);
 10.1208 -by (res_inst_tac [("x","no+noa")] exI 1);
 10.1209 -by Auto_tac;
 10.1210 -qed "HNat_add";
 10.1211 -
 10.1212 -Goalw [HNat_def,starset_def]
 10.1213 -     "[| x: HNat; y: HNat |] ==> x * y: HNat";
 10.1214 -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
 10.1215 -by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
 10.1216 -by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
 10.1217 -              simpset() addsimps [hypreal_mult]));
 10.1218 -by (Ultra_tac 1);
 10.1219 -by (res_inst_tac [("x","no*noa")] exI 1);
 10.1220 -by Auto_tac;
 10.1221 -qed "HNat_mult";
 10.1222 -
 10.1223 -(*---------------------------------------------------------------
 10.1224 -    Embedding of the hypernaturals into the hyperreal
 10.1225 - --------------------------------------------------------------*)
 10.1226 -
 10.1227 -(*WARNING: FRAGILE!*)
 10.1228 -Goal "(Ya : hyprel ``{%n. f(n)}) = \
 10.1229 -\     ({n. f n = Ya n} : FreeUltrafilterNat)";
 10.1230 -by Auto_tac;
 10.1231 -qed "lemma_hyprel_FUFN";
 10.1232 -
 10.1233 -Goalw [hypreal_of_hypnat_def]
 10.1234 -      "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) = \
 10.1235 -\         Abs_hypreal(hyprel `` {%n. real (X n)})";
 10.1236 -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
 10.1237 -by (auto_tac (claset()
 10.1238 -                  addEs [FreeUltrafilterNat_Int RS FreeUltrafilterNat_subset],
 10.1239 -              simpset() addsimps [lemma_hyprel_FUFN]));
 10.1240 -qed "hypreal_of_hypnat";
 10.1241 -
 10.1242 -Goal "inj(hypreal_of_hypnat)";
 10.1243 -by (rtac injI 1);
 10.1244 -by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
 10.1245 -by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
 10.1246 -by (auto_tac (claset(), simpset() addsimps [hypreal_of_hypnat]));
 10.1247 -qed "inj_hypreal_of_hypnat";
 10.1248 -
 10.1249 -Goal "(hypreal_of_hypnat n = hypreal_of_hypnat m) = (n = m)";
 10.1250 -by (auto_tac (claset(),simpset() addsimps [inj_hypreal_of_hypnat RS injD]));
 10.1251 -qed "hypreal_of_hypnat_eq_cancel";
 10.1252 -Addsimps [hypreal_of_hypnat_eq_cancel];
 10.1253 -
 10.1254 -Goal "(hypnat_of_nat n = hypnat_of_nat m) = (n = m)";
 10.1255 -by (auto_tac (claset() addDs [inj_hypnat_of_nat RS injD],
 10.1256 -              simpset()));
 10.1257 -qed "hypnat_of_nat_eq_cancel";
 10.1258 -Addsimps [hypnat_of_nat_eq_cancel];
 10.1259 -
 10.1260 -Goalw [hypnat_zero_def] 
 10.1261 -     "hypreal_of_hypnat 0 = 0";
 10.1262 -by (simp_tac (simpset() addsimps [hypreal_zero_def, hypreal_of_hypnat]) 1);
 10.1263 -qed "hypreal_of_hypnat_zero";
 10.1264 -
 10.1265 -Goalw [hypnat_one_def] 
 10.1266 -     "hypreal_of_hypnat (1::hypnat) = 1";
 10.1267 -by (simp_tac (simpset() addsimps [hypreal_one_def, hypreal_of_hypnat]) 1);
 10.1268 -qed "hypreal_of_hypnat_one";
 10.1269 -
 10.1270 -Goal "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n";
 10.1271 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
 10.1272 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 10.1273 -by (asm_simp_tac (simpset() addsimps
 10.1274 -           [hypreal_of_hypnat, hypreal_add,hypnat_add,real_of_nat_add]) 1);
 10.1275 -qed "hypreal_of_hypnat_add";
 10.1276 -Addsimps [hypreal_of_hypnat_add];
 10.1277 -
 10.1278 -Goal "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n";
 10.1279 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
 10.1280 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 10.1281 -by (asm_simp_tac (simpset() addsimps
 10.1282 -           [hypreal_of_hypnat, hypreal_mult,hypnat_mult,real_of_nat_mult]) 1);
 10.1283 -qed "hypreal_of_hypnat_mult";
 10.1284 -Addsimps [hypreal_of_hypnat_mult];
 10.1285 -
 10.1286 -Goal "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)";
 10.1287 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 10.1288 -by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
 10.1289 -by (asm_simp_tac (simpset() addsimps 
 10.1290 -    [hypreal_of_hypnat,hypreal_less,hypnat_less]) 1);
 10.1291 -qed "hypreal_of_hypnat_less_iff";
 10.1292 -Addsimps [hypreal_of_hypnat_less_iff];
 10.1293 -
 10.1294 -Goal "(hypreal_of_hypnat N = 0) = (N = 0)";
 10.1295 -by (simp_tac (simpset() addsimps [hypreal_of_hypnat_zero RS sym]) 1);
 10.1296 -qed "hypreal_of_hypnat_eq_zero_iff";
 10.1297 -Addsimps [hypreal_of_hypnat_eq_zero_iff];
 10.1298 -
 10.1299 -Goal "ALL n. N <= n ==> N = (0::hypnat)";
 10.1300 -by (dres_inst_tac [("x","0")] spec 1);
 10.1301 -by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
 10.1302 -by (auto_tac (claset(),simpset() addsimps [hypnat_le,hypnat_zero_def]));
 10.1303 -qed "hypnat_eq_zero";
 10.1304 -Addsimps [hypnat_eq_zero];
 10.1305 -
 10.1306 -Goal "~ (ALL n. n = (0::hypnat))";
 10.1307 -by Auto_tac;
 10.1308 -by (res_inst_tac [("x","(1::hypnat)")] exI 1);
 10.1309 -by (Simp_tac 1);
 10.1310 -qed "hypnat_not_all_eq_zero";
 10.1311 -Addsimps [hypnat_not_all_eq_zero];
 10.1312 -
 10.1313 -Goal "n ~= 0 ==> (n <= (1::hypnat)) = (n = (1::hypnat))";
 10.1314 -by (auto_tac (claset(), simpset() addsimps [hypnat_le_less]));
 10.1315 -qed "hypnat_le_one_eq_one";
 10.1316 -Addsimps [hypnat_le_one_eq_one];
 10.1317 -
 10.1318 -
 10.1319 -
 10.1320 -
 10.1321 -(*MOVE UP*)
 10.1322 -Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) : Infinitesimal";
 10.1323 -by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
 10.1324 -by (auto_tac (claset(),simpset() addsimps [hypreal_of_hypnat,hypreal_inverse,
 10.1325 -    HNatInfinite_FreeUltrafilterNat_iff,Infinitesimal_FreeUltrafilterNat_iff2]));
 10.1326 -by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2);
 10.1327 -by Auto_tac;
 10.1328 -by (dres_inst_tac [("x","m + 1")] spec 1);
 10.1329 -by (Ultra_tac 1);
 10.1330 -qed "HNatInfinite_inverse_Infinitesimal";
 10.1331 -Addsimps [HNatInfinite_inverse_Infinitesimal];
 10.1332 -
 10.1333 -Goal "n : HNatInfinite ==> inverse (hypreal_of_hypnat n) ~= 0";
 10.1334 -by (auto_tac (claset() addSIs [hypreal_inverse_not_zero],simpset()));
 10.1335 -qed "HNatInfinite_inverse_not_zero";
 10.1336 -Addsimps [HNatInfinite_inverse_not_zero];
 10.1337 -
    11.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Thu Jan 29 16:51:17 2004 +0100
    11.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Mon Feb 02 12:23:46 2004 +0100
    11.3 @@ -1,83 +1,1070 @@
    11.4  (*  Title       : HyperNat.thy
    11.5      Author      : Jacques D. Fleuriot
    11.6      Copyright   : 1998  University of Cambridge
    11.7 -    Description : Explicit construction of hypernaturals using 
    11.8 -                  ultrafilters
    11.9 -*) 
   11.10 +*)
   11.11  
   11.12 -HyperNat = Star + 
   11.13 +header{*Construction of Hypernaturals using Ultrafilters*}
   11.14 +
   11.15 +theory HyperNat = Star:
   11.16  
   11.17  constdefs
   11.18      hypnatrel :: "((nat=>nat)*(nat=>nat)) set"
   11.19 -    "hypnatrel == {p. EX X Y. p = ((X::nat=>nat),Y) & 
   11.20 -                       {n::nat. X(n) = Y(n)} : FreeUltrafilterNat}"
   11.21 +    "hypnatrel == {p. \<exists>X Y. p = ((X::nat=>nat),Y) &
   11.22 +                       {n::nat. X(n) = Y(n)} \<in> FreeUltrafilterNat}"
   11.23  
   11.24 -typedef hypnat = "UNIV//hypnatrel"              (quotient_def)
   11.25 +typedef hypnat = "UNIV//hypnatrel"
   11.26 +    by (auto simp add: quotient_def)
   11.27  
   11.28 -instance
   11.29 -   hypnat  :: {ord, zero, one, plus, times, minus}
   11.30 +instance hypnat :: ord ..
   11.31 +instance hypnat :: zero ..
   11.32 +instance hypnat :: one ..
   11.33 +instance hypnat :: plus ..
   11.34 +instance hypnat :: times ..
   11.35 +instance hypnat :: minus ..
   11.36  
   11.37 -consts
   11.38 -  whn       :: hypnat
   11.39 +consts whn :: hypnat
   11.40  
   11.41  constdefs
   11.42  
   11.43    (* embedding the naturals in the hypernaturals *)
   11.44 -  hypnat_of_nat   :: nat => hypnat
   11.45 +  hypnat_of_nat   :: "nat => hypnat"
   11.46    "hypnat_of_nat m  == Abs_hypnat(hypnatrel``{%n::nat. m})"
   11.47  
   11.48    (* hypernaturals as members of the hyperreals; the set is defined as  *)
   11.49    (* the nonstandard extension of set of naturals embedded in the reals *)
   11.50    HNat         :: "hypreal set"
   11.51 -  "HNat == *s* {n. EX no::nat. n = real no}"
   11.52 +  "HNat == *s* {n. \<exists>no::nat. n = real no}"
   11.53  
   11.54    (* the set of infinite hypernatural numbers *)
   11.55    HNatInfinite :: "hypnat set"
   11.56 -  "HNatInfinite == {n. n ~: Nats}"
   11.57 +  "HNatInfinite == {n. n \<notin> Nats}"
   11.58  
   11.59 -  (* explicit embedding of the hypernaturals in the hyperreals *)    
   11.60 -  hypreal_of_hypnat :: hypnat => hypreal
   11.61 -  "hypreal_of_hypnat N  == Abs_hypreal(UN X: Rep_hypnat(N). 
   11.62 +  (* explicit embedding of the hypernaturals in the hyperreals *)
   11.63 +  hypreal_of_hypnat :: "hypnat => hypreal"
   11.64 +  "hypreal_of_hypnat N  == Abs_hypreal(\<Union>X \<in> Rep_hypnat(N).
   11.65                                         hyprel``{%n::nat. real (X n)})"
   11.66 -  
   11.67 -defs
   11.68 +
   11.69 +defs (overloaded)
   11.70  
   11.71    (** the overloaded constant "Nats" **)
   11.72 -  
   11.73 +
   11.74    (* set of naturals embedded in the hyperreals*)
   11.75 -  SNat_def             "Nats == {n. EX N. n = hypreal_of_nat N}"  
   11.76 +  SNat_def:  "Nats == {n. \<exists>N. n = hypreal_of_nat N}"
   11.77  
   11.78    (* set of naturals embedded in the hypernaturals*)
   11.79 -  SHNat_def            "Nats == {n. EX N. n = hypnat_of_nat N}"  
   11.80 +  SHNat_def: "Nats == {n. \<exists>N. n = hypnat_of_nat N}"
   11.81  
   11.82    (** hypernatural arithmetic **)
   11.83 -  
   11.84 -  hypnat_zero_def      "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
   11.85 -  hypnat_one_def       "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
   11.86 +
   11.87 +  hypnat_zero_def:  "0 == Abs_hypnat(hypnatrel``{%n::nat. 0})"
   11.88 +  hypnat_one_def:   "1 == Abs_hypnat(hypnatrel``{%n::nat. 1})"
   11.89  
   11.90    (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
   11.91 -  hypnat_omega_def     "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
   11.92 - 
   11.93 -  hypnat_add_def  
   11.94 -  "P + Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
   11.95 +  hypnat_omega_def:  "whn == Abs_hypnat(hypnatrel``{%n::nat. n})"
   11.96 +
   11.97 +  hypnat_add_def:
   11.98 +  "P + Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
   11.99                  hypnatrel``{%n::nat. X n + Y n})"
  11.100  
  11.101 -  hypnat_mult_def  
  11.102 -  "P * Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
  11.103 +  hypnat_mult_def:
  11.104 +  "P * Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
  11.105                  hypnatrel``{%n::nat. X n * Y n})"
  11.106  
  11.107 -  hypnat_minus_def  
  11.108 -  "P - Q == Abs_hypnat(UN X:Rep_hypnat(P). UN Y:Rep_hypnat(Q).
  11.109 +  hypnat_minus_def:
  11.110 +  "P - Q == Abs_hypnat(\<Union>X \<in> Rep_hypnat(P). \<Union>Y \<in> Rep_hypnat(Q).
  11.111                  hypnatrel``{%n::nat. X n - Y n})"
  11.112  
  11.113 -  hypnat_less_def
  11.114 -  "P < (Q::hypnat) == EX X Y. X: Rep_hypnat(P) & 
  11.115 -                               Y: Rep_hypnat(Q) & 
  11.116 -                               {n::nat. X n < Y n} : FreeUltrafilterNat"
  11.117 -  hypnat_le_def
  11.118 -  "P <= (Q::hypnat) == ~(Q < P)" 
  11.119 +  hypnat_le_def:
  11.120 +  "P \<le> (Q::hypnat) == \<exists>X Y. X \<in> Rep_hypnat(P) &
  11.121 +                               Y \<in> Rep_hypnat(Q) &
  11.122 +                               {n::nat. X n \<le> Y n} \<in> FreeUltrafilterNat"
  11.123  
  11.124 -end
  11.125 +  hypnat_less_def: "(x < (y::hypnat)) == (x \<le> y & x \<noteq> y)"
  11.126  
  11.127  
  11.128  
  11.129 +subsection{*Properties of @{term hypnatrel}*}
  11.130 +
  11.131 +text{*Proving that @{term hypnatrel} is an equivalence relation*}
  11.132 +
  11.133 +lemma hypnatrel_iff:
  11.134 +     "((X,Y) \<in> hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)"
  11.135 +apply (unfold hypnatrel_def, fast)
  11.136 +done
  11.137 +
  11.138 +lemma hypnatrel_refl: "(x,x) \<in> hypnatrel"
  11.139 +by (unfold hypnatrel_def, auto)
  11.140 +
  11.141 +lemma hypnatrel_sym: "(x,y) \<in> hypnatrel ==> (y,x) \<in> hypnatrel"
  11.142 +by (auto simp add: hypnatrel_def eq_commute)
  11.143 +
  11.144 +lemma hypnatrel_trans [rule_format (no_asm)]:
  11.145 +     "(x,y) \<in> hypnatrel --> (y,z) \<in> hypnatrel --> (x,z) \<in> hypnatrel"
  11.146 +apply (unfold hypnatrel_def, auto, ultra)
  11.147 +done
  11.148 +
  11.149 +lemma equiv_hypnatrel:
  11.150 +     "equiv UNIV hypnatrel"
  11.151 +apply (simp add: equiv_def refl_def sym_def trans_def hypnatrel_refl)
  11.152 +apply (blast intro: hypnatrel_sym hypnatrel_trans)
  11.153 +done
  11.154 +
  11.155 +(* (hypnatrel `` {x} = hypnatrel `` {y}) = ((x,y) \<in> hypnatrel) *)
  11.156 +lemmas equiv_hypnatrel_iff =
  11.157 +    eq_equiv_class_iff [OF equiv_hypnatrel UNIV_I UNIV_I, simp]
  11.158 +
  11.159 +lemma hypnatrel_in_hypnat [simp]: "hypnatrel``{x}:hypnat"
  11.160 +by (unfold hypnat_def hypnatrel_def quotient_def, blast)
  11.161 +
  11.162 +lemma inj_on_Abs_hypnat: "inj_on Abs_hypnat hypnat"
  11.163 +apply (rule inj_on_inverseI)
  11.164 +apply (erule Abs_hypnat_inverse)
  11.165 +done
  11.166 +
  11.167 +declare inj_on_Abs_hypnat [THEN inj_on_iff, simp]
  11.168 +        Abs_hypnat_inverse [simp]
  11.169 +
  11.170 +declare equiv_hypnatrel [THEN eq_equiv_class_iff, simp]
  11.171 +
  11.172 +declare hypnatrel_iff [iff]
  11.173 +
  11.174 +
  11.175 +lemma inj_Rep_hypnat: "inj(Rep_hypnat)"
  11.176 +apply (rule inj_on_inverseI)
  11.177 +apply (rule Rep_hypnat_inverse)
  11.178 +done
  11.179 +
  11.180 +lemma lemma_hypnatrel_refl: "x \<in> hypnatrel `` {x}"
  11.181 +by (simp add: hypnatrel_def)
  11.182 +
  11.183 +declare lemma_hypnatrel_refl [simp]
  11.184 +
  11.185 +lemma hypnat_empty_not_mem: "{} \<notin> hypnat"
  11.186 +apply (unfold hypnat_def)
  11.187 +apply (auto elim!: quotientE equalityCE)
  11.188 +done
  11.189 +
  11.190 +declare hypnat_empty_not_mem [simp]
  11.191 +
  11.192 +lemma Rep_hypnat_nonempty: "Rep_hypnat x \<noteq> {}"
  11.193 +by (cut_tac x = x in Rep_hypnat, auto)
  11.194 +
  11.195 +declare Rep_hypnat_nonempty [simp]
  11.196 +
  11.197 +subsection{*@{term hypnat_of_nat}:
  11.198 +            the Injection from @{typ nat} to @{typ hypnat}*}
  11.199 +
  11.200 +lemma inj_hypnat_of_nat: "inj(hypnat_of_nat)"
  11.201 +apply (rule inj_onI)
  11.202 +apply (unfold hypnat_of_nat_def)
  11.203 +apply (drule inj_on_Abs_hypnat [THEN inj_onD])
  11.204 +apply (rule hypnatrel_in_hypnat)+
  11.205 +apply (drule eq_equiv_class)
  11.206 +apply (rule equiv_hypnatrel)
  11.207 +apply (simp_all split: split_if_asm)
  11.208 +done
  11.209 +
  11.210 +lemma eq_Abs_hypnat:
  11.211 +    "(!!x. z = Abs_hypnat(hypnatrel``{x}) ==> P) ==> P"
  11.212 +apply (rule_tac x1=z in Rep_hypnat [unfolded hypnat_def, THEN quotientE])
  11.213 +apply (drule_tac f = Abs_hypnat in arg_cong)
  11.214 +apply (force simp add: Rep_hypnat_inverse)
  11.215 +done
  11.216 +
  11.217 +subsection{*Hypernat Addition*}
  11.218 +
  11.219 +lemma hypnat_add_congruent2:
  11.220 +     "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n + Y n})"
  11.221 +apply (unfold congruent2_def, auto, ultra)
  11.222 +done
  11.223 +
  11.224 +lemma hypnat_add:
  11.225 +  "Abs_hypnat(hypnatrel``{%n. X n}) + Abs_hypnat(hypnatrel``{%n. Y n}) =
  11.226 +   Abs_hypnat(hypnatrel``{%n. X n + Y n})"
  11.227 +by (simp add: hypnat_add_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_add_congruent2])
  11.228 +
  11.229 +lemma hypnat_add_commute: "(z::hypnat) + w = w + z"
  11.230 +apply (rule eq_Abs_hypnat [of z])
  11.231 +apply (rule eq_Abs_hypnat [of w])
  11.232 +apply (simp add: add_ac hypnat_add)
  11.233 +done
  11.234 +
  11.235 +lemma hypnat_add_assoc: "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)"
  11.236 +apply (rule eq_Abs_hypnat [of z1])
  11.237 +apply (rule eq_Abs_hypnat [of z2])
  11.238 +apply (rule eq_Abs_hypnat [of z3])
  11.239 +apply (simp add: hypnat_add nat_add_assoc)
  11.240 +done
  11.241 +
  11.242 +lemma hypnat_add_zero_left: "(0::hypnat) + z = z"
  11.243 +apply (rule eq_Abs_hypnat [of z])
  11.244 +apply (simp add: hypnat_zero_def hypnat_add)
  11.245 +done
  11.246 +
  11.247 +instance hypnat :: plus_ac0
  11.248 +  by (intro_classes,
  11.249 +      (assumption |
  11.250 +       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
  11.251 +
  11.252 +
  11.253 +subsection{*Subtraction inverse on @{typ hypreal}*}
  11.254 +
  11.255 +
  11.256 +lemma hypnat_minus_congruent2:
  11.257 +    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n - Y n})"
  11.258 +apply (unfold congruent2_def, auto, ultra)
  11.259 +done
  11.260 +
  11.261 +lemma hypnat_minus:
  11.262 +  "Abs_hypnat(hypnatrel``{%n. X n}) - Abs_hypnat(hypnatrel``{%n. Y n}) =
  11.263 +   Abs_hypnat(hypnatrel``{%n. X n - Y n})"
  11.264 +by (simp add: hypnat_minus_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_minus_congruent2])
  11.265 +
  11.266 +lemma hypnat_minus_zero: "z - z = (0::hypnat)"
  11.267 +apply (rule eq_Abs_hypnat [of z])
  11.268 +apply (simp add: hypnat_zero_def hypnat_minus)
  11.269 +done
  11.270 +
  11.271 +lemma hypnat_diff_0_eq_0: "(0::hypnat) - n = 0"
  11.272 +apply (rule eq_Abs_hypnat [of n])
  11.273 +apply (simp add: hypnat_minus hypnat_zero_def)
  11.274 +done
  11.275 +
  11.276 +declare hypnat_minus_zero [simp] hypnat_diff_0_eq_0 [simp]
  11.277 +
  11.278 +lemma hypnat_add_is_0: "(m+n = (0::hypnat)) = (m=0 & n=0)"
  11.279 +apply (rule eq_Abs_hypnat [of m])
  11.280 +apply (rule eq_Abs_hypnat [of n])
  11.281 +apply (auto intro: FreeUltrafilterNat_subset dest: FreeUltrafilterNat_Int simp add: hypnat_zero_def hypnat_add)
  11.282 +done
  11.283 +
  11.284 +declare hypnat_add_is_0 [iff]
  11.285 +
  11.286 +lemma hypnat_diff_diff_left: "(i::hypnat) - j - k = i - (j+k)"
  11.287 +apply (rule eq_Abs_hypnat [of i])
  11.288 +apply (rule eq_Abs_hypnat [of j])
  11.289 +apply (rule eq_Abs_hypnat [of k])
  11.290 +apply (simp add: hypnat_minus hypnat_add diff_diff_left)
  11.291 +done
  11.292 +
  11.293 +lemma hypnat_diff_commute: "(i::hypnat) - j - k = i-k-j"
  11.294 +by (simp add: hypnat_diff_diff_left hypnat_add_commute)
  11.295 +
  11.296 +lemma hypnat_diff_add_inverse: "((n::hypnat) + m) - n = m"
  11.297 +apply (rule eq_Abs_hypnat [of m])
  11.298 +apply (rule eq_Abs_hypnat [of n])
  11.299 +apply (simp add: hypnat_minus hypnat_add)
  11.300 +done
  11.301 +declare hypnat_diff_add_inverse [simp]
  11.302 +
  11.303 +lemma hypnat_diff_add_inverse2:  "((m::hypnat) + n) - n = m"
  11.304 +apply (rule eq_Abs_hypnat [of m])
  11.305 +apply (rule eq_Abs_hypnat [of n])
  11.306 +apply (simp add: hypnat_minus hypnat_add)
  11.307 +done
  11.308 +declare hypnat_diff_add_inverse2 [simp]
  11.309 +
  11.310 +lemma hypnat_diff_cancel: "((k::hypnat) + m) - (k+n) = m - n"
  11.311 +apply (rule eq_Abs_hypnat [of k])
  11.312 +apply (rule eq_Abs_hypnat [of m])
  11.313 +apply (rule eq_Abs_hypnat [of n])
  11.314 +apply (simp add: hypnat_minus hypnat_add)
  11.315 +done
  11.316 +declare hypnat_diff_cancel [simp]
  11.317 +
  11.318 +lemma hypnat_diff_cancel2: "((m::hypnat) + k) - (n+k) = m - n"
  11.319 +by (simp add: hypnat_add_commute [of _ k])
  11.320 +declare hypnat_diff_cancel2 [simp]
  11.321 +
  11.322 +lemma hypnat_diff_add_0: "(n::hypnat) - (n+m) = (0::hypnat)"
  11.323 +apply (rule eq_Abs_hypnat [of m])
  11.324 +apply (rule eq_Abs_hypnat [of n])
  11.325 +apply (simp add: hypnat_zero_def hypnat_minus hypnat_add)
  11.326 +done
  11.327 +declare hypnat_diff_add_0 [simp]
  11.328 +
  11.329 +
  11.330 +subsection{*Hyperreal Multiplication*}
  11.331 +
  11.332 +lemma hypnat_mult_congruent2:
  11.333 +    "congruent2 hypnatrel (%X Y. hypnatrel``{%n. X n * Y n})"
  11.334 +by (unfold congruent2_def, auto, ultra)
  11.335 +
  11.336 +lemma hypnat_mult:
  11.337 +  "Abs_hypnat(hypnatrel``{%n. X n}) * Abs_hypnat(hypnatrel``{%n. Y n}) =
  11.338 +   Abs_hypnat(hypnatrel``{%n. X n * Y n})"
  11.339 +by (simp add: hypnat_mult_def UN_equiv_class2 [OF equiv_hypnatrel hypnat_mult_congruent2])
  11.340 +
  11.341 +lemma hypnat_mult_commute: "(z::hypnat) * w = w * z"
  11.342 +apply (rule eq_Abs_hypnat [of z])
  11.343 +apply (rule eq_Abs_hypnat [of w])
  11.344 +apply (simp add: hypnat_mult mult_ac)
  11.345 +done
  11.346 +
  11.347 +lemma hypnat_mult_assoc: "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)"
  11.348 +apply (rule eq_Abs_hypnat [of z1])
  11.349 +apply (rule eq_Abs_hypnat [of z2])
  11.350 +apply (rule eq_Abs_hypnat [of z3])
  11.351 +apply (simp add: hypnat_mult mult_assoc)
  11.352 +done
  11.353 +
  11.354 +lemma hypnat_mult_1: "(1::hypnat) * z = z"
  11.355 +apply (rule eq_Abs_hypnat [of z])
  11.356 +apply (simp add: hypnat_mult hypnat_one_def)
  11.357 +done
  11.358 +
  11.359 +lemma hypnat_diff_mult_distrib: "((m::hypnat) - n) * k = (m * k) - (n * k)"
  11.360 +apply (rule eq_Abs_hypnat [of k])
  11.361 +apply (rule eq_Abs_hypnat [of m])
  11.362 +apply (rule eq_Abs_hypnat [of n])
  11.363 +apply (simp add: hypnat_mult hypnat_minus diff_mult_distrib)
  11.364 +done
  11.365 +
  11.366 +lemma hypnat_diff_mult_distrib2: "(k::hypnat) * (m - n) = (k * m) - (k * n)"
  11.367 +by (simp add: hypnat_diff_mult_distrib hypnat_mult_commute [of k])
  11.368 +
  11.369 +lemma hypnat_add_mult_distrib: "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)"
  11.370 +apply (rule eq_Abs_hypnat [of z1])
  11.371 +apply (rule eq_Abs_hypnat [of z2])
  11.372 +apply (rule eq_Abs_hypnat [of w])
  11.373 +apply (simp add: hypnat_mult hypnat_add add_mult_distrib)
  11.374 +done
  11.375 +
  11.376 +lemma hypnat_add_mult_distrib2: "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)"
  11.377 +by (simp add: hypnat_mult_commute [of w] hypnat_add_mult_distrib)
  11.378 +
  11.379 +text{*one and zero are distinct*}
  11.380 +lemma hypnat_zero_not_eq_one: "(0::hypnat) \<noteq> (1::hypnat)"
  11.381 +by (auto simp add: hypnat_zero_def hypnat_one_def)
  11.382 +declare hypnat_zero_not_eq_one [THEN not_sym, simp]
  11.383 +
  11.384 +
  11.385 +text{*The Hypernaturals Form A Semiring*}
  11.386 +instance hypnat :: semiring
  11.387 +proof
  11.388 +  fix i j k :: hypnat
  11.389 +  show "(i + j) + k = i + (j + k)" by (rule hypnat_add_assoc)
  11.390 +  show "i + j = j + i" by (rule hypnat_add_commute)
  11.391 +  show "0 + i = i" by simp
  11.392 +  show "(i * j) * k = i * (j * k)" by (rule hypnat_mult_assoc)
  11.393 +  show "i * j = j * i" by (rule hypnat_mult_commute)
  11.394 +  show "1 * i = i" by (rule hypnat_mult_1)
  11.395 +  show "(i + j) * k = i * k + j * k" by (simp add: hypnat_add_mult_distrib)
  11.396 +  show "0 \<noteq> (1::hypnat)" by (rule hypnat_zero_not_eq_one)
  11.397 +  assume "k+i = k+j"
  11.398 +  hence "(k+i) - k = (k+j) - k" by simp
  11.399 +  thus "i=j" by simp
  11.400 +qed
  11.401 +
  11.402 +
  11.403 +subsection{*Properties of The @{text "\<le>"} Relation*}
  11.404 +
  11.405 +lemma hypnat_le:
  11.406 +      "(Abs_hypnat(hypnatrel``{%n. X n}) \<le> Abs_hypnat(hypnatrel``{%n. Y n})) =
  11.407 +       ({n. X n \<le> Y n} \<in> FreeUltrafilterNat)"
  11.408 +apply (unfold hypnat_le_def)
  11.409 +apply (auto intro!: lemma_hypnatrel_refl, ultra)
  11.410 +done
  11.411 +
  11.412 +lemma hypnat_le_refl: "w \<le> (w::hypnat)"
  11.413 +apply (rule eq_Abs_hypnat [of w])
  11.414 +apply (simp add: hypnat_le)
  11.415 +done
  11.416 +
  11.417 +lemma hypnat_le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::hypnat)"
  11.418 +apply (rule eq_Abs_hypnat [of i])
  11.419 +apply (rule eq_Abs_hypnat [of j])
  11.420 +apply (rule eq_Abs_hypnat [of k])
  11.421 +apply (simp add: hypnat_le, ultra)
  11.422 +done
  11.423 +
  11.424 +lemma hypnat_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::hypnat)"
  11.425 +apply (rule eq_Abs_hypnat [of z])
  11.426 +apply (rule eq_Abs_hypnat [of w])
  11.427 +apply (simp add: hypnat_le, ultra)
  11.428 +done
  11.429 +
  11.430 +(* Axiom 'order_less_le' of class 'order': *)
  11.431 +lemma hypnat_less_le: "((w::hypnat) < z) = (w \<le> z & w \<noteq> z)"
  11.432 +by (simp add: hypnat_less_def)
  11.433 +
  11.434 +instance hypnat :: order
  11.435 +proof qed
  11.436 + (assumption |
  11.437 +  rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+
  11.438 +
  11.439 +(* Axiom 'linorder_linear' of class 'linorder': *)
  11.440 +lemma hypnat_le_linear: "(z::hypnat) \<le> w | w \<le> z"
  11.441 +apply (rule eq_Abs_hypnat [of z])
  11.442 +apply (rule eq_Abs_hypnat [of w])
  11.443 +apply (auto simp add: hypnat_le, ultra)
  11.444 +done
  11.445 +
  11.446 +instance hypnat :: linorder
  11.447 +  by (intro_classes, rule hypnat_le_linear)
  11.448 +
  11.449 +lemma hypnat_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypnat)"
  11.450 +apply (rule eq_Abs_hypnat [of x])
  11.451 +apply (rule eq_Abs_hypnat [of y])
  11.452 +apply (rule eq_Abs_hypnat [of z])
  11.453 +apply (auto simp add: hypnat_le hypnat_add)
  11.454 +done
  11.455 +
  11.456 +lemma hypnat_mult_less_mono2: "[| (0::hypnat)<z; x<y |] ==> z*x<z*y"
  11.457 +apply (rule eq_Abs_hypnat [of x])
  11.458 +apply (rule eq_Abs_hypnat [of y])
  11.459 +apply (rule eq_Abs_hypnat [of z])
  11.460 +apply (simp add: hypnat_zero_def  hypnat_mult linorder_not_le [symmetric])
  11.461 +apply (auto simp add: hypnat_le, ultra)
  11.462 +done
  11.463 +
  11.464 +
  11.465 +subsection{*The Hypernaturals Form an Ordered Semiring*}
  11.466 +
  11.467 +instance hypnat :: ordered_semiring
  11.468 +proof
  11.469 +  fix x y z :: hypnat
  11.470 +  show "0 < (1::hypnat)"
  11.471 +    by (simp add: hypnat_zero_def hypnat_one_def linorder_not_le [symmetric],
  11.472 +        simp add: hypnat_le)
  11.473 +  show "x \<le> y ==> z + x \<le> z + y"
  11.474 +    by (rule hypnat_add_left_mono)
  11.475 +  show "x < y ==> 0 < z ==> z * x < z * y"
  11.476 +    by (simp add: hypnat_mult_less_mono2)
  11.477 +qed
  11.478 +
  11.479 +lemma hypnat_mult_is_0 [simp]: "(m*n = (0::hypnat)) = (m=0 | n=0)"
  11.480 +apply (rule eq_Abs_hypnat [of m])
  11.481 +apply (rule eq_Abs_hypnat [of n])
  11.482 +apply (auto simp add: hypnat_zero_def hypnat_mult, ultra+)
  11.483 +done
  11.484 +
  11.485 +
  11.486 +subsection{*Theorems for Ordering*}
  11.487 +
  11.488 +lemma hypnat_less:
  11.489 +      "(Abs_hypnat(hypnatrel``{%n. X n}) < Abs_hypnat(hypnatrel``{%n. Y n})) =
  11.490 +       ({n. X n < Y n} \<in> FreeUltrafilterNat)"
  11.491 +apply (auto simp add: hypnat_le  linorder_not_le [symmetric])
  11.492 +apply (ultra+)
  11.493 +done
  11.494 +
  11.495 +lemma hypnat_not_less0 [iff]: "~ n < (0::hypnat)"
  11.496 +apply (rule eq_Abs_hypnat [of n])
  11.497 +apply (auto simp add: hypnat_zero_def hypnat_less)
  11.498 +done
  11.499 +
  11.500 +lemma hypnat_less_one [iff]:
  11.501 +      "(n < (1::hypnat)) = (n=0)"
  11.502 +apply (rule eq_Abs_hypnat [of n])
  11.503 +apply (auto simp add: hypnat_zero_def hypnat_one_def hypnat_less)
  11.504 +done
  11.505 +
  11.506 +lemma hypnat_add_diff_inverse: "~ m<n ==> n+(m-n) = (m::hypnat)"
  11.507 +apply (rule eq_Abs_hypnat [of m])
  11.508 +apply (rule eq_Abs_hypnat [of n])
  11.509 +apply (simp add: hypnat_minus hypnat_add hypnat_less split: nat_diff_split, ultra)
  11.510 +done
  11.511 +
  11.512 +lemma hypnat_le_add_diff_inverse [simp]: "n \<le> m ==> n+(m-n) = (m::hypnat)"
  11.513 +by (simp add: hypnat_add_diff_inverse linorder_not_less [symmetric])
  11.514 +
  11.515 +lemma hypnat_le_add_diff_inverse2 [simp]: "n\<le>m ==> (m-n)+n = (m::hypnat)"
  11.516 +by (simp add: hypnat_le_add_diff_inverse hypnat_add_commute)
  11.517 +
  11.518 +declare hypnat_le_add_diff_inverse2 [OF order_less_imp_le]
  11.519 +
  11.520 +lemma hypnat_le0 [iff]: "(0::hypnat) \<le> n"
  11.521 +by (simp add: linorder_not_less [symmetric])
  11.522 +
  11.523 +lemma hypnat_add_self_le [simp]: "(x::hypnat) \<le> n + x"
  11.524 +by (insert add_right_mono [of 0 n x], simp)
  11.525 +
  11.526 +lemma hypnat_add_one_self_less [simp]: "(x::hypnat) < x + (1::hypnat)"
  11.527 +by (insert add_strict_left_mono [OF zero_less_one], auto)
  11.528 +
  11.529 +lemma hypnat_neq0_conv [iff]: "(n \<noteq> 0) = (0 < (n::hypnat))"
  11.530 +by (simp add: order_less_le)
  11.531 +
  11.532 +lemma hypnat_gt_zero_iff: "((0::hypnat) < n) = ((1::hypnat) \<le> n)"
  11.533 +by (auto simp add: linorder_not_less [symmetric])
  11.534 +
  11.535 +lemma hypnat_gt_zero_iff2: "(0 < n) = (\<exists>m. n = m + (1::hypnat))"
  11.536 +apply safe
  11.537 + apply (rule_tac x = "n - (1::hypnat) " in exI)
  11.538 + apply (simp add: hypnat_gt_zero_iff) 
  11.539 +apply (insert add_le_less_mono [OF _ zero_less_one, of 0], auto) 
  11.540 +done
  11.541 +
  11.542 +subsection{*The Embedding @{term hypnat_of_nat} Preserves Ring and 
  11.543 +      Order Properties*}
  11.544 +
  11.545 +lemma hypnat_of_nat_add:
  11.546 +      "hypnat_of_nat ((z::nat) + w) = hypnat_of_nat z + hypnat_of_nat w"
  11.547 +by (simp add: hypnat_of_nat_def hypnat_add)
  11.548 +
  11.549 +lemma hypnat_of_nat_minus:
  11.550 +      "hypnat_of_nat ((z::nat) - w) = hypnat_of_nat z - hypnat_of_nat w"
  11.551 +by (simp add: hypnat_of_nat_def hypnat_minus)
  11.552 +
  11.553 +lemma hypnat_of_nat_mult:
  11.554 +      "hypnat_of_nat (z * w) = hypnat_of_nat z * hypnat_of_nat w"
  11.555 +by (simp add: hypnat_of_nat_def hypnat_mult)
  11.556 +
  11.557 +lemma hypnat_of_nat_less_iff [simp]:
  11.558 +      "(hypnat_of_nat z < hypnat_of_nat w) = (z < w)"
  11.559 +by (simp add: hypnat_less hypnat_of_nat_def)
  11.560 +
  11.561 +lemma hypnat_of_nat_le_iff [simp]:
  11.562 +      "(hypnat_of_nat z \<le> hypnat_of_nat w) = (z \<le> w)"
  11.563 +by (simp add: linorder_not_less [symmetric])
  11.564 +
  11.565 +lemma hypnat_of_nat_one: "hypnat_of_nat (Suc 0) = (1::hypnat)"
  11.566 +by (simp add: hypnat_of_nat_def hypnat_one_def)
  11.567 +
  11.568 +lemma hypnat_of_nat_zero: "hypnat_of_nat 0 = 0"
  11.569 +by (simp add: hypnat_of_nat_def hypnat_zero_def)
  11.570 +
  11.571 +lemma hypnat_of_nat_zero_iff: "(hypnat_of_nat n = 0) = (n = 0)"
  11.572 +by (auto intro: FreeUltrafilterNat_P 
  11.573 +         simp add: hypnat_of_nat_def hypnat_zero_def)
  11.574 +
  11.575 +lemma hypnat_of_nat_Suc:
  11.576 +     "hypnat_of_nat (Suc n) = hypnat_of_nat n + (1::hypnat)"
  11.577 +by (auto simp add: hypnat_add hypnat_of_nat_def hypnat_one_def)
  11.578 +
  11.579 +
  11.580 +subsection{*Existence of an Infinite Hypernatural Number*}
  11.581 +
  11.582 +lemma hypnat_omega: "hypnatrel``{%n::nat. n} \<in> hypnat"
  11.583 +by auto
  11.584 +
  11.585 +lemma Rep_hypnat_omega: "Rep_hypnat(whn) \<in> hypnat"
  11.586 +by (simp add: hypnat_omega_def)
  11.587 +
  11.588 +text{*Existence of infinite number not corresponding to any natural number
  11.589 +follows because member @{term FreeUltrafilterNat} is not finite.
  11.590 +See @{text HyperDef.thy} for similar argument.*}
  11.591 +
  11.592 +lemma not_ex_hypnat_of_nat_eq_omega:
  11.593 +      "~ (\<exists>x. hypnat_of_nat x = whn)"
  11.594 +apply (simp add: hypnat_omega_def hypnat_of_nat_def)
  11.595 +apply (auto dest: FreeUltrafilterNat_not_finite)
  11.596 +done
  11.597 +
  11.598 +lemma hypnat_of_nat_not_eq_omega: "hypnat_of_nat x \<noteq> whn"
  11.599 +by (cut_tac not_ex_hypnat_of_nat_eq_omega, auto)
  11.600 +declare hypnat_of_nat_not_eq_omega [THEN not_sym, simp]
  11.601 +
  11.602 +
  11.603 +subsection{*Properties of the set @{term Nats} of Embedded Natural Numbers*}
  11.604 +
  11.605 +(* Infinite hypernatural not in embedded Nats *)
  11.606 +lemma SHNAT_omega_not_mem [simp]: "whn \<notin> Nats"
  11.607 +by (simp add: SHNat_def)
  11.608 +
  11.609 +(*-----------------------------------------------------------------------
  11.610 +     Closure laws for members of (embedded) set standard naturals Nats
  11.611 + -----------------------------------------------------------------------*)
  11.612 +lemma SHNat_add:
  11.613 +     "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x + y \<in> Nats"
  11.614 +apply (simp add: SHNat_def, safe)
  11.615 +apply (rule_tac x = "N + Na" in exI)
  11.616 +apply (simp add: hypnat_of_nat_add)
  11.617 +done
  11.618 +
  11.619 +lemma SHNat_minus:
  11.620 +     "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x - y \<in> Nats"
  11.621 +apply (simp add: SHNat_def, safe)
  11.622 +apply (rule_tac x = "N - Na" in exI)
  11.623 +apply (simp add: hypnat_of_nat_minus)
  11.624 +done
  11.625 +
  11.626 +lemma SHNat_mult:
  11.627 +     "!!x::hypnat. [| x \<in> Nats; y \<in> Nats |] ==> x * y \<in> Nats"
  11.628 +apply (simp add: SHNat_def, safe)
  11.629 +apply (rule_tac x = "N * Na" in exI)
  11.630 +apply (simp (no_asm) add: hypnat_of_nat_mult)
  11.631 +done
  11.632 +
  11.633 +lemma SHNat_add_cancel: "!!x::hypnat. [| x + y \<in> Nats; y \<in> Nats |] ==> x \<in> Nats"
  11.634 +by (drule_tac x = "x+y" in SHNat_minus, auto)
  11.635 +
  11.636 +lemma SHNat_hypnat_of_nat [simp]: "hypnat_of_nat x \<in> Nats"
  11.637 +by (simp add: SHNat_def, blast)
  11.638 +
  11.639 +lemma SHNat_hypnat_of_nat_one [simp]: "hypnat_of_nat (Suc 0) \<in> Nats"
  11.640 +by simp
  11.641 +
  11.642 +lemma SHNat_hypnat_of_nat_zero [simp]: "hypnat_of_nat 0 \<in> Nats"
  11.643 +by simp
  11.644 +
  11.645 +lemma SHNat_one [simp]: "(1::hypnat) \<in> Nats"
  11.646 +by (simp add: hypnat_of_nat_one [symmetric])
  11.647 +
  11.648 +lemma SHNat_zero [simp]: "(0::hypnat) \<in> Nats"
  11.649 +by (simp add: hypnat_of_nat_zero [symmetric])
  11.650 +
  11.651 +lemma SHNat_iff: "(x \<in> Nats) = (\<exists>y. x = hypnat_of_nat  y)"
  11.652 +by (simp add: SHNat_def)
  11.653 +
  11.654 +lemma SHNat_hypnat_of_nat_iff:
  11.655 +      "Nats = hypnat_of_nat ` (UNIV::nat set)"
  11.656 +by (auto simp add: SHNat_def)
  11.657 +
  11.658 +lemma leSuc_Un_eq: "{n. n \<le> Suc m} = {n. n \<le> m} Un {n. n = Suc m}"
  11.659 +by (auto simp add: le_Suc_eq)
  11.660 +
  11.661 +lemma finite_nat_le_segment: "finite {n::nat. n \<le> m}"
  11.662 +apply (induct_tac "m")
  11.663 +apply (auto simp add: leSuc_Un_eq)
  11.664 +done
  11.665 +
  11.666 +lemma lemma_unbounded_set [simp]: "{n::nat. m < n} \<in> FreeUltrafilterNat"
  11.667 +by (insert finite_nat_le_segment
  11.668 +                [THEN FreeUltrafilterNat_finite, 
  11.669 +                 THEN FreeUltrafilterNat_Compl_mem, of m], ultra)
  11.670 +
  11.671 +(*????hyperdef*)
  11.672 +lemma cofinite_mem_FreeUltrafilterNat: "finite (-X) ==> X \<in> FreeUltrafilterNat"
  11.673 +apply (drule FreeUltrafilterNat_finite)  
  11.674 +apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
  11.675 +done
  11.676 +
  11.677 +lemma Compl_Collect_le: "- {n::nat. N \<le> n} = {n. n < N}"
  11.678 +by (simp add: Collect_neg_eq [symmetric] linorder_not_le) 
  11.679 +
  11.680 +lemma hypnat_omega_gt_SHNat:
  11.681 +     "n \<in> Nats ==> n < whn"
  11.682 +apply (auto simp add: SHNat_def hypnat_of_nat_def hypnat_less_def 
  11.683 +                      hypnat_le_def hypnat_omega_def)
  11.684 + prefer 2 apply (force dest: FreeUltrafilterNat_not_finite)
  11.685 +apply (auto intro!: exI)
  11.686 +apply (rule cofinite_mem_FreeUltrafilterNat)
  11.687 +apply (simp add: Compl_Collect_le finite_nat_segment) 
  11.688 +done
  11.689 +
  11.690 +lemma hypnat_of_nat_less_whn: "hypnat_of_nat n < whn"
  11.691 +by (insert hypnat_omega_gt_SHNat [of "hypnat_of_nat n"], auto)
  11.692 +declare hypnat_of_nat_less_whn [simp]
  11.693 +
  11.694 +lemma hypnat_of_nat_le_whn: "hypnat_of_nat n \<le> whn"
  11.695 +by (rule hypnat_of_nat_less_whn [THEN order_less_imp_le])
  11.696 +declare hypnat_of_nat_le_whn [simp]
  11.697 +
  11.698 +lemma hypnat_zero_less_hypnat_omega [simp]: "0 < whn"
  11.699 +by (simp add: hypnat_omega_gt_SHNat)
  11.700 +
  11.701 +lemma hypnat_one_less_hypnat_omega [simp]: "(1::hypnat) < whn"
  11.702 +by (simp add: hypnat_omega_gt_SHNat)
  11.703 +
  11.704 +
  11.705 +subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
  11.706 +
  11.707 +lemma HNatInfinite_whn: "whn \<in> HNatInfinite"
  11.708 +by (simp add: HNatInfinite_def SHNat_def)
  11.709 +declare HNatInfinite_whn [simp]
  11.710 +
  11.711 +lemma SHNat_not_HNatInfinite: "x \<in> Nats ==> x \<notin> HNatInfinite"
  11.712 +by (simp add: HNatInfinite_def)
  11.713 +
  11.714 +lemma not_HNatInfinite_SHNat: "x \<notin> HNatInfinite ==> x \<in> Nats"
  11.715 +by (simp add: HNatInfinite_def)
  11.716 +
  11.717 +lemma not_SHNat_HNatInfinite: "x \<notin> Nats ==> x \<in> HNatInfinite"
  11.718 +by (simp add: HNatInfinite_def)
  11.719 +
  11.720 +lemma HNatInfinite_not_SHNat: "x \<in> HNatInfinite ==> x \<notin> Nats"
  11.721 +by (simp add: HNatInfinite_def)
  11.722 +
  11.723 +lemma SHNat_not_HNatInfinite_iff: "(x \<in> Nats) = (x \<notin> HNatInfinite)"
  11.724 +by (blast intro!: SHNat_not_HNatInfinite not_HNatInfinite_SHNat)
  11.725 +
  11.726 +lemma not_SHNat_HNatInfinite_iff: "(x \<notin> Nats) = (x \<in> HNatInfinite)"
  11.727 +by (blast intro!: not_SHNat_HNatInfinite HNatInfinite_not_SHNat)
  11.728 +
  11.729 +lemma SHNat_HNatInfinite_disj: "x \<in> Nats | x \<in> HNatInfinite"
  11.730 +by (simp add: SHNat_not_HNatInfinite_iff)
  11.731 +
  11.732 +
  11.733 +subsection{*Alternative Characterization of the Set of Infinite Hypernaturals:
  11.734 +@{term "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"}*}
  11.735 +
  11.736 +(*??delete? similar reasoning in hypnat_omega_gt_SHNat above*)
  11.737 +lemma HNatInfinite_FreeUltrafilterNat_lemma: "\<forall>N::nat. {n. f n \<noteq> N} \<in> FreeUltrafilterNat
  11.738 +      ==> {n. N < f n} \<in> FreeUltrafilterNat"
  11.739 +apply (induct_tac "N")
  11.740 +apply (drule_tac x = 0 in spec)
  11.741 +apply (rule ccontr, drule FreeUltrafilterNat_Compl_mem, drule FreeUltrafilterNat_Int, assumption, simp)
  11.742 +apply (drule_tac x = "Suc n" in spec, ultra)
  11.743 +done
  11.744 +
  11.745 +lemma HNatInfinite_iff: "HNatInfinite = {N. \<forall>n \<in> Nats. n < N}"
  11.746 +apply (unfold HNatInfinite_def SHNat_def hypnat_of_nat_def, safe)
  11.747 +apply (drule_tac [2] x = "Abs_hypnat (hypnatrel `` {%n. N}) " in bspec)
  11.748 +apply (rule_tac z = x in eq_Abs_hypnat)
  11.749 +apply (rule_tac z = n in eq_Abs_hypnat)
  11.750 +apply (auto simp add: hypnat_less)
  11.751 +apply (auto  elim: HNatInfinite_FreeUltrafilterNat_lemma 
  11.752 +           simp add: FreeUltrafilterNat_Compl_iff1 Collect_neg_eq [symmetric])
  11.753 +done
  11.754 +
  11.755 +subsection{*Alternative Characterization of @{term HNatInfinite} using 
  11.756 +Free Ultrafilter*}
  11.757 +
  11.758 +lemma HNatInfinite_FreeUltrafilterNat:
  11.759 +     "x \<in> HNatInfinite 
  11.760 +      ==> \<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat"
  11.761 +apply (rule eq_Abs_hypnat [of x])
  11.762 +apply (auto simp add: HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
  11.763 +apply (rule bexI [OF _ lemma_hypnatrel_refl], clarify) 
  11.764 +apply (drule_tac x = "hypnat_of_nat u" in bspec, simp) 
  11.765 +apply (auto simp add: hypnat_of_nat_def hypnat_less)
  11.766 +done
  11.767 +
  11.768 +lemma FreeUltrafilterNat_HNatInfinite:
  11.769 +     "\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat
  11.770 +      ==> x \<in> HNatInfinite"
  11.771 +apply (rule eq_Abs_hypnat [of x])
  11.772 +apply (auto simp add: hypnat_less HNatInfinite_iff SHNat_iff hypnat_of_nat_def)
  11.773 +apply (drule spec, ultra, auto) 
  11.774 +done
  11.775 +
  11.776 +lemma HNatInfinite_FreeUltrafilterNat_iff:
  11.777 +     "(x \<in> HNatInfinite) = 
  11.778 +      (\<exists>X \<in> Rep_hypnat x. \<forall>u. {n. u < X n}:  FreeUltrafilterNat)"
  11.779 +apply (blast intro: HNatInfinite_FreeUltrafilterNat FreeUltrafilterNat_HNatInfinite)
  11.780 +done
  11.781 +
  11.782 +lemma HNatInfinite_gt_one: "x \<in> HNatInfinite ==> (1::hypnat) < x"
  11.783 +by (auto simp add: HNatInfinite_iff)
  11.784 +declare HNatInfinite_gt_one [simp]
  11.785 +
  11.786 +lemma zero_not_mem_HNatInfinite: "0 \<notin> HNatInfinite"
  11.787 +apply (auto simp add: HNatInfinite_iff)
  11.788 +apply (drule_tac a = " (1::hypnat) " in equals0D)
  11.789 +apply simp
  11.790 +done
  11.791 +declare zero_not_mem_HNatInfinite [simp]
  11.792 +
  11.793 +lemma HNatInfinite_not_eq_zero: "x \<in> HNatInfinite ==> 0 < x"
  11.794 +apply (drule HNatInfinite_gt_one) 
  11.795 +apply (auto simp add: order_less_trans [OF zero_less_one])
  11.796 +done
  11.797 +
  11.798 +lemma HNatInfinite_ge_one [simp]: "x \<in> HNatInfinite ==> (1::hypnat) \<le> x"
  11.799 +by (blast intro: order_less_imp_le HNatInfinite_gt_one)
  11.800 +
  11.801 +
  11.802 +subsection{*Closure Rules*}
  11.803 +
  11.804 +lemma HNatInfinite_add: "[| x \<in> HNatInfinite; y \<in> HNatInfinite |]
  11.805 +            ==> x + y \<in> HNatInfinite"
  11.806 +apply (auto simp add: HNatInfinite_iff)
  11.807 +apply (drule bspec, assumption)
  11.808 +apply (drule bspec [OF _ SHNat_zero])
  11.809 +apply (drule add_strict_mono, assumption, simp)
  11.810 +done
  11.811 +
  11.812 +lemma HNatInfinite_SHNat_add: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x + y \<in> HNatInfinite"
  11.813 +apply (rule ccontr, drule not_HNatInfinite_SHNat)
  11.814 +apply (drule_tac x = "x + y" in SHNat_minus)
  11.815 +apply (auto simp add: SHNat_not_HNatInfinite_iff)
  11.816 +done
  11.817 +
  11.818 +lemma HNatInfinite_SHNat_diff: "[| x \<in> HNatInfinite; y \<in> Nats |] ==> x - y \<in> HNatInfinite"
  11.819 +apply (rule ccontr, drule not_HNatInfinite_SHNat)
  11.820 +apply (drule_tac x = "x - y" in SHNat_add)
  11.821 +apply (subgoal_tac [2] "y \<le> x")
  11.822 +apply (auto dest!: hypnat_le_add_diff_inverse2 simp add: not_SHNat_HNatInfinite_iff [symmetric])
  11.823 +apply (auto intro!: order_less_imp_le simp add: not_SHNat_HNatInfinite_iff HNatInfinite_iff)
  11.824 +done
  11.825 +
  11.826 +lemma HNatInfinite_add_one: "x \<in> HNatInfinite ==> x + (1::hypnat) \<in> HNatInfinite"
  11.827 +by (auto intro: HNatInfinite_SHNat_add)
  11.828 +
  11.829 +lemma HNatInfinite_minus_one: "x \<in> HNatInfinite ==> x - (1::hypnat) \<in> HNatInfinite"
  11.830 +apply (rule ccontr, drule not_HNatInfinite_SHNat)
  11.831 +apply (drule_tac x = "x - (1::hypnat) " and y = " (1::hypnat) " in SHNat_add)
  11.832 +apply (auto simp add: not_SHNat_HNatInfinite_iff [symmetric])
  11.833 +done
  11.834 +
  11.835 +lemma HNatInfinite_is_Suc: "x \<in> HNatInfinite ==> \<exists>y. x = y + (1::hypnat)"
  11.836 +apply (rule_tac x = "x - (1::hypnat) " in exI)
  11.837 +apply auto
  11.838 +done
  11.839 +
  11.840 +
  11.841 +subsection{*@{term HNat}: the Hypernaturals Embedded in the Hyperreals*}
  11.842 +
  11.843 +text{*Obtained using the nonstandard extension of the naturals*}
  11.844 +
  11.845 +lemma HNat_hypreal_of_nat: "hypreal_of_nat N \<in> HNat"
  11.846 +apply (simp add: HNat_def starset_def hypreal_of_nat_def hypreal_of_real_def, auto, ultra)
  11.847 +apply (rule_tac x = N in exI, auto)
  11.848 +done
  11.849 +declare HNat_hypreal_of_nat [simp]
  11.850 +
  11.851 +lemma HNat_add: "[| x \<in> HNat; y \<in> HNat |] ==> x + y \<in> HNat"
  11.852 +apply (simp add: HNat_def starset_def)
  11.853 +apply (rule_tac z = x in eq_Abs_hypreal)
  11.854 +apply (rule_tac z = y in eq_Abs_hypreal)
  11.855 +apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_add, ultra)
  11.856 +apply (rule_tac x = "no+noa" in exI, auto)
  11.857 +done
  11.858 +
  11.859 +lemma HNat_mult:
  11.860 +     "[| x \<in> HNat; y \<in> HNat |] ==> x * y \<in> HNat"
  11.861 +apply (simp add: HNat_def starset_def)
  11.862 +apply (rule_tac z = x in eq_Abs_hypreal)
  11.863 +apply (rule_tac z = y in eq_Abs_hypreal)
  11.864 +apply (auto dest!: bspec intro: lemma_hyprel_refl simp add: hypreal_mult, ultra)
  11.865 +apply (rule_tac x = "no*noa" in exI, auto)
  11.866 +done
  11.867 +
  11.868 +
  11.869 +subsection{*Embedding of the Hypernaturals into the Hyperreals*}
  11.870 +
  11.871 +(*WARNING: FRAGILE!*)
  11.872 +lemma lemma_hyprel_FUFN: "(Ya \<in> hyprel ``{%n. f(n)}) =
  11.873 +      ({n. f n = Ya n} \<in> FreeUltrafilterNat)"
  11.874 +apply auto
  11.875 +done
  11.876 +
  11.877 +lemma hypreal_of_hypnat:
  11.878 +      "hypreal_of_hypnat (Abs_hypnat(hypnatrel``{%n. X n})) =
  11.879 +       Abs_hypreal(hyprel `` {%n. real (X n)})"
  11.880 +apply (simp add: hypreal_of_hypnat_def)
  11.881 +apply (rule_tac f = Abs_hypreal in arg_cong)
  11.882 +apply (auto elim: FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] 
  11.883 +       simp add: lemma_hyprel_FUFN)
  11.884 +done
  11.885 +
  11.886 +lemma inj_hypreal_of_hypnat: "inj(hypreal_of_hypnat)"
  11.887 +apply (rule inj_onI)
  11.888 +apply (rule_tac z = x in eq_Abs_hypnat)
  11.889 +apply (rule_tac z = y in eq_Abs_hypnat)
  11.890 +apply (auto simp add: hypreal_of_hypnat)
  11.891 +done
  11.892 +
  11.893 +declare inj_hypreal_of_hypnat [THEN inj_eq, simp]
  11.894 +declare inj_hypnat_of_nat [THEN inj_eq, simp]
  11.895 +
  11.896 +lemma hypreal_of_hypnat_zero: "hypreal_of_hypnat 0 = 0"
  11.897 +by (simp add: hypnat_zero_def hypreal_zero_def hypreal_of_hypnat)
  11.898 +
  11.899 +lemma hypreal_of_hypnat_one: "hypreal_of_hypnat (1::hypnat) = 1"
  11.900 +by (simp add: hypnat_one_def hypreal_one_def hypreal_of_hypnat)
  11.901 +
  11.902 +lemma hypreal_of_hypnat_add [simp]:
  11.903 +     "hypreal_of_hypnat (m + n) = hypreal_of_hypnat m + hypreal_of_hypnat n"
  11.904 +apply (rule eq_Abs_hypnat [of m])
  11.905 +apply (rule eq_Abs_hypnat [of n])
  11.906 +apply (simp add: hypreal_of_hypnat hypreal_add hypnat_add real_of_nat_add)
  11.907 +done
  11.908 +
  11.909 +lemma hypreal_of_hypnat_mult [simp]:
  11.910 +     "hypreal_of_hypnat (m * n) = hypreal_of_hypnat m * hypreal_of_hypnat n"
  11.911 +apply (rule eq_Abs_hypnat [of m])
  11.912 +apply (rule eq_Abs_hypnat [of n])
  11.913 +apply (simp add: hypreal_of_hypnat hypreal_mult hypnat_mult real_of_nat_mult)
  11.914 +done
  11.915 +
  11.916 +lemma hypreal_of_hypnat_less_iff [simp]:
  11.917 +     "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)"
  11.918 +apply (rule eq_Abs_hypnat [of m])
  11.919 +apply (rule eq_Abs_hypnat [of n])
  11.920 +apply (simp add: hypreal_of_hypnat hypreal_less hypnat_less)
  11.921 +done
  11.922 +
  11.923 +lemma hypreal_of_hypnat_eq_zero_iff: "(hypreal_of_hypnat N = 0) = (N = 0)"
  11.924 +by (simp add: hypreal_of_hypnat_zero [symmetric])
  11.925 +declare hypreal_of_hypnat_eq_zero_iff [simp]
  11.926 +
  11.927 +lemma hypreal_of_hypnat_ge_zero [simp]: "0 \<le> hypreal_of_hypnat n"
  11.928 +apply (rule eq_Abs_hypnat [of n])
  11.929 +apply (simp add: hypreal_of_hypnat hypreal_zero_num hypreal_le)
  11.930 +done
  11.931 +
  11.932 +(*????DELETE??*)
  11.933 +lemma hypnat_eq_zero: "\<forall>n. N \<le> n ==> N = (0::hypnat)"
  11.934 +apply (drule_tac x = 0 in spec)
  11.935 +apply (rule_tac z = N in eq_Abs_hypnat)
  11.936 +apply (auto simp add: hypnat_le hypnat_zero_def)
  11.937 +done
  11.938 +
  11.939 +(*????DELETE??*)
  11.940 +lemma hypnat_not_all_eq_zero: "~ (\<forall>n. n = (0::hypnat))"
  11.941 +by auto
  11.942 +
  11.943 +(*????DELETE??*)
  11.944 +lemma hypnat_le_one_eq_one: "n \<noteq> 0 ==> (n \<le> (1::hypnat)) = (n = (1::hypnat))"
  11.945 +by (auto simp add: order_le_less)
  11.946 +
  11.947 +(*WHERE DO THESE BELONG???*)
  11.948 +lemma HNatInfinite_inverse_Infinitesimal: "n \<in> HNatInfinite ==> inverse (hypreal_of_hypnat n) \<in> Infinitesimal"
  11.949 +apply (rule eq_Abs_hypnat [of n])
  11.950 +apply (auto simp add: hypreal_of_hypnat hypreal_inverse HNatInfinite_FreeUltrafilterNat_iff Infinitesimal_FreeUltrafilterNat_iff2)
  11.951 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
  11.952 +apply (drule_tac x = "m + 1" in spec, ultra)
  11.953 +done
  11.954 +declare HNatInfinite_inverse_Infinitesimal [simp]
  11.955 +
  11.956 +lemma HNatInfinite_inverse_not_zero: "n \<in> HNatInfinite ==> hypreal_of_hypnat n \<noteq> 0"
  11.957 +by (simp add: HNatInfinite_not_eq_zero)
  11.958 +
  11.959 +
  11.960 +
  11.961 +ML
  11.962 +{*
  11.963 +val hypnat_of_nat_def = thm"hypnat_of_nat_def";
  11.964 +val HNat_def = thm"HNat_def";
  11.965 +val HNatInfinite_def = thm"HNatInfinite_def";
  11.966 +val hypreal_of_hypnat_def = thm"hypreal_of_hypnat_def";
  11.967 +val SNat_def = thm"SNat_def";
  11.968 +val SHNat_def = thm"SHNat_def";
  11.969 +val hypnat_zero_def = thm"hypnat_zero_def";
  11.970 +val hypnat_one_def = thm"hypnat_one_def";
  11.971 +val hypnat_omega_def = thm"hypnat_omega_def";
  11.972 +
  11.973 +val hypnatrel_iff = thm "hypnatrel_iff";
  11.974 +val hypnatrel_refl = thm "hypnatrel_refl";
  11.975 +val hypnatrel_sym = thm "hypnatrel_sym";
  11.976 +val hypnatrel_trans = thm "hypnatrel_trans";
  11.977 +val equiv_hypnatrel = thm "equiv_hypnatrel";
  11.978 +val equiv_hypnatrel_iff = thms "equiv_hypnatrel_iff";
  11.979 +val hypnatrel_in_hypnat = thm "hypnatrel_in_hypnat";
  11.980 +val inj_on_Abs_hypnat = thm "inj_on_Abs_hypnat";
  11.981 +val inj_Rep_hypnat = thm "inj_Rep_hypnat";
  11.982 +val lemma_hypnatrel_refl = thm "lemma_hypnatrel_refl";
  11.983 +val hypnat_empty_not_mem = thm "hypnat_empty_not_mem";
  11.984 +val Rep_hypnat_nonempty = thm "Rep_hypnat_nonempty";
  11.985 +val inj_hypnat_of_nat = thm "inj_hypnat_of_nat";
  11.986 +val eq_Abs_hypnat = thm "eq_Abs_hypnat";
  11.987 +val hypnat_add_congruent2 = thm "hypnat_add_congruent2";
  11.988 +val hypnat_add = thm "hypnat_add";
  11.989 +val hypnat_add_commute = thm "hypnat_add_commute";
  11.990 +val hypnat_add_assoc = thm "hypnat_add_assoc";
  11.991 +val hypnat_add_zero_left = thm "hypnat_add_zero_left";
  11.992 +val hypnat_minus_congruent2 = thm "hypnat_minus_congruent2";
  11.993 +val hypnat_minus = thm "hypnat_minus";
  11.994 +val hypnat_minus_zero = thm "hypnat_minus_zero";
  11.995 +val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
  11.996 +val hypnat_add_is_0 = thm "hypnat_add_is_0";
  11.997 +val hypnat_diff_diff_left = thm "hypnat_diff_diff_left";
  11.998 +val hypnat_diff_commute = thm "hypnat_diff_commute";
  11.999 +val hypnat_diff_add_inverse = thm "hypnat_diff_add_inverse";
 11.1000 +val hypnat_diff_add_inverse2 = thm "hypnat_diff_add_inverse2";
 11.1001 +val hypnat_diff_cancel = thm "hypnat_diff_cancel";
 11.1002 +val hypnat_diff_cancel2 = thm "hypnat_diff_cancel2";
 11.1003 +val hypnat_diff_add_0 = thm "hypnat_diff_add_0";
 11.1004 +val hypnat_mult_congruent2 = thm "hypnat_mult_congruent2";
 11.1005 +val hypnat_mult = thm "hypnat_mult";
 11.1006 +val hypnat_mult_commute = thm "hypnat_mult_commute";
 11.1007 +val hypnat_mult_assoc = thm "hypnat_mult_assoc";
 11.1008 +val hypnat_mult_1 = thm "hypnat_mult_1";
 11.1009 +val hypnat_diff_mult_distrib = thm "hypnat_diff_mult_distrib";
 11.1010 +val hypnat_diff_mult_distrib2 = thm "hypnat_diff_mult_distrib2";
 11.1011 +val hypnat_add_mult_distrib = thm "hypnat_add_mult_distrib";
 11.1012 +val hypnat_add_mult_distrib2 = thm "hypnat_add_mult_distrib2";
 11.1013 +val hypnat_zero_not_eq_one = thm "hypnat_zero_not_eq_one";
 11.1014 +val hypnat_le = thm "hypnat_le";
 11.1015 +val hypnat_le_refl = thm "hypnat_le_refl";
 11.1016 +val hypnat_le_trans = thm "hypnat_le_trans";
 11.1017 +val hypnat_le_anti_sym = thm "hypnat_le_anti_sym";
 11.1018 +val hypnat_less_le = thm "hypnat_less_le";
 11.1019 +val hypnat_le_linear = thm "hypnat_le_linear";
 11.1020 +val hypnat_add_left_mono = thm "hypnat_add_left_mono";
 11.1021 +val hypnat_mult_less_mono2 = thm "hypnat_mult_less_mono2";
 11.1022 +val hypnat_mult_is_0 = thm "hypnat_mult_is_0";
 11.1023 +val hypnat_less = thm "hypnat_less";
 11.1024 +val hypnat_not_less0 = thm "hypnat_not_less0";
 11.1025 +val hypnat_less_one = thm "hypnat_less_one";
 11.1026 +val hypnat_add_diff_inverse = thm "hypnat_add_diff_inverse";
 11.1027 +val hypnat_le_add_diff_inverse = thm "hypnat_le_add_diff_inverse";
 11.1028 +val hypnat_le_add_diff_inverse2 = thm "hypnat_le_add_diff_inverse2";
 11.1029 +val hypnat_le0 = thm "hypnat_le0";
 11.1030 +val hypnat_add_self_le = thm "hypnat_add_self_le";
 11.1031 +val hypnat_add_one_self_less = thm "hypnat_add_one_self_less";
 11.1032 +val hypnat_neq0_conv = thm "hypnat_neq0_conv";
 11.1033 +val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
 11.1034 +val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
 11.1035 +val hypnat_of_nat_add = thm "hypnat_of_nat_add";
 11.1036 +val hypnat_of_nat_minus = thm "hypnat_of_nat_minus";
 11.1037 +val hypnat_of_nat_mult = thm "hypnat_of_nat_mult";
 11.1038 +val hypnat_of_nat_less_iff = thm "hypnat_of_nat_less_iff";
 11.1039 +val hypnat_of_nat_le_iff = thm "hypnat_of_nat_le_iff";
 11.1040 +val hypnat_of_nat_one = thm "hypnat_of_nat_one";
 11.1041 +val hypnat_of_nat_zero = thm "hypnat_of_nat_zero";
 11.1042 +val hypnat_of_nat_zero_iff = thm "hypnat_of_nat_zero_iff";
 11.1043 +val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
 11.1044 +val hypnat_omega = thm "hypnat_omega";
 11.1045 +val Rep_hypnat_omega = thm "Rep_hypnat_omega";
 11.1046 +val not_ex_hypnat_of_nat_eq_omega = thm "not_ex_hypnat_of_nat_eq_omega";
 11.1047 +val hypnat_of_nat_not_eq_omega = thm "hypnat_of_nat_not_eq_omega";
 11.1048 +val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
 11.1049 +val SHNat_add = thm "SHNat_add";
 11.1050 +val SHNat_minus = thm "SHNat_minus";
 11.1051 +val SHNat_mult = thm "SHNat_mult";
 11.1052 +val SHNat_add_cancel = thm "SHNat_add_cancel";
 11.1053 +val SHNat_hypnat_of_nat = thm "SHNat_hypnat_of_nat";
 11.1054 +val SHNat_hypnat_of_nat_one = thm "SHNat_hypnat_of_nat_one";
 11.1055 +val SHNat_hypnat_of_nat_zero = thm "SHNat_hypnat_of_nat_zero";
 11.1056 +val SHNat_one = thm "SHNat_one";
 11.1057 +val SHNat_zero = thm "SHNat_zero";
 11.1058 +val SHNat_iff = thm "SHNat_iff";
 11.1059 +val SHNat_hypnat_of_nat_iff = thm "SHNat_hypnat_of_nat_iff";
 11.1060 +val leSuc_Un_eq = thm "leSuc_Un_eq";
 11.1061 +val finite_nat_le_segment = thm "finite_nat_le_segment";
 11.1062 +val lemma_unbounded_set = thm "lemma_unbounded_set";
 11.1063 +val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
 11.1064 +val Compl_Collect_le = thm "Compl_Collect_le";
 11.1065 +val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
 11.1066 +val hypnat_of_nat_less_whn = thm "hypnat_of_nat_less_whn";
 11.1067 +val hypnat_of_nat_le_whn = thm "hypnat_of_nat_le_whn";
 11.1068 +val hypnat_zero_less_hypnat_omega = thm "hypnat_zero_less_hypnat_omega";
 11.1069 +val hypnat_one_less_hypnat_omega = thm "hypnat_one_less_hypnat_omega";
 11.1070 +val HNatInfinite_whn = thm "HNatInfinite_whn";
 11.1071 +val SHNat_not_HNatInfinite = thm "SHNat_not_HNatInfinite";
 11.1072 +val not_HNatInfinite_SHNat = thm "not_HNatInfinite_SHNat";
 11.1073 +val not_SHNat_HNatInfinite = thm "not_SHNat_HNatInfinite";
 11.1074 +val HNatInfinite_not_SHNat = thm "HNatInfinite_not_SHNat";
 11.1075 +val SHNat_not_HNatInfinite_iff = thm "SHNat_not_HNatInfinite_iff";
 11.1076 +val not_SHNat_HNatInfinite_iff = thm "not_SHNat_HNatInfinite_iff";
 11.1077 +val SHNat_HNatInfinite_disj = thm "SHNat_HNatInfinite_disj";
 11.1078 +val HNatInfinite_FreeUltrafilterNat_lemma = thm "HNatInfinite_FreeUltrafilterNat_lemma";
 11.1079 +val HNatInfinite_iff = thm "HNatInfinite_iff";
 11.1080 +val HNatInfinite_FreeUltrafilterNat = thm "HNatInfinite_FreeUltrafilterNat";
 11.1081 +val FreeUltrafilterNat_HNatInfinite = thm "FreeUltrafilterNat_HNatInfinite";
 11.1082 +val HNatInfinite_FreeUltrafilterNat_iff = thm "HNatInfinite_FreeUltrafilterNat_iff";
 11.1083 +val HNatInfinite_gt_one = thm "HNatInfinite_gt_one";
 11.1084 +val zero_not_mem_HNatInfinite = thm "zero_not_mem_HNatInfinite";
 11.1085 +val HNatInfinite_not_eq_zero = thm "HNatInfinite_not_eq_zero";
 11.1086 +val HNatInfinite_ge_one = thm "HNatInfinite_ge_one";
 11.1087 +val HNatInfinite_add = thm "HNatInfinite_add";
 11.1088 +val HNatInfinite_SHNat_add = thm "HNatInfinite_SHNat_add";
 11.1089 +val HNatInfinite_SHNat_diff = thm "HNatInfinite_SHNat_diff";
 11.1090 +val HNatInfinite_add_one = thm "HNatInfinite_add_one";
 11.1091 +val HNatInfinite_minus_one = thm "HNatInfinite_minus_one";
 11.1092 +val HNatInfinite_is_Suc = thm "HNatInfinite_is_Suc";
 11.1093 +val HNat_hypreal_of_nat = thm "HNat_hypreal_of_nat";
 11.1094 +val HNat_add = thm "HNat_add";
 11.1095 +val HNat_mult = thm "HNat_mult";
 11.1096 +val lemma_hyprel_FUFN = thm "lemma_hyprel_FUFN";
 11.1097 +val hypreal_of_hypnat = thm "hypreal_of_hypnat";
 11.1098 +val inj_hypreal_of_hypnat = thm "inj_hypreal_of_hypnat";
 11.1099 +val hypreal_of_hypnat_zero = thm "hypreal_of_hypnat_zero";
 11.1100 +val hypreal_of_hypnat_one = thm "hypreal_of_hypnat_one";
 11.1101 +val hypreal_of_hypnat_add = thm "hypreal_of_hypnat_add";
 11.1102 +val hypreal_of_hypnat_mult = thm "hypreal_of_hypnat_mult";
 11.1103 +val hypreal_of_hypnat_less_iff = thm "hypreal_of_hypnat_less_iff";
 11.1104 +val hypreal_of_hypnat_eq_zero_iff = thm "hypreal_of_hypnat_eq_zero_iff";
 11.1105 +val hypreal_of_hypnat_ge_zero = thm "hypreal_of_hypnat_ge_zero";
 11.1106 +val hypnat_eq_zero = thm "hypnat_eq_zero";
 11.1107 +val hypnat_not_all_eq_zero = thm "hypnat_not_all_eq_zero";
 11.1108 +val hypnat_le_one_eq_one = thm "hypnat_le_one_eq_one";
 11.1109 +val HNatInfinite_inverse_Infinitesimal = thm "HNatInfinite_inverse_Infinitesimal";
 11.1110 +val HNatInfinite_inverse_not_zero = thm "HNatInfinite_inverse_not_zero";
 11.1111 +*}
 11.1112 +
 11.1113 +end
    12.1 --- a/src/HOL/Hyperreal/HyperOrd.thy	Thu Jan 29 16:51:17 2004 +0100
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,9 +0,0 @@
    12.4 -theory HyperOrd = HyperDef:
    12.5 -
    12.6 -
    12.7 -
    12.8 -ML
    12.9 -{*
   12.10 -*}
   12.11 -
   12.12 -end
    13.1 --- a/src/HOL/Hyperreal/HyperPow.thy	Thu Jan 29 16:51:17 2004 +0100
    13.2 +++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Feb 02 12:23:46 2004 +0100
    13.3 @@ -6,23 +6,7 @@
    13.4  
    13.5  header{*Exponentials on the Hyperreals*}
    13.6  
    13.7 -theory HyperPow = HRealAbs + HyperNat + RealPow:
    13.8 -
    13.9 -instance hypnat :: order
   13.10 -  by (intro_classes,
   13.11 -      (assumption | 
   13.12 -       rule hypnat_le_refl hypnat_le_trans hypnat_le_anti_sym hypnat_less_le)+)
   13.13 -
   13.14 -                          
   13.15 -text{*Type @{typ hypnat} is linearly ordered*}
   13.16 -instance hypnat :: linorder 
   13.17 -  by (intro_classes, rule hypnat_le_linear)
   13.18 -
   13.19 -instance hypnat :: plus_ac0
   13.20 -  by (intro_classes,
   13.21 -      (assumption | 
   13.22 -       rule hypnat_add_commute hypnat_add_assoc hypnat_add_zero_left)+)
   13.23 -
   13.24 +theory HyperPow = HyperArith + HyperNat + RealPow:
   13.25  
   13.26  instance hypreal :: power ..
   13.27  
   13.28 @@ -57,12 +41,10 @@
   13.29  done
   13.30  
   13.31  lemma hrabs_hrealpow_minus_one [simp]: "abs(-1 ^ n) = (1::hypreal)"
   13.32 -apply (simp add: power_abs); 
   13.33 -done
   13.34 +by (simp add: power_abs)
   13.35  
   13.36  lemma hrealpow_two_le: "(0::hypreal) \<le> r ^ Suc (Suc 0)"
   13.37 -apply (auto simp add: zero_le_mult_iff)
   13.38 -done
   13.39 +by (auto simp add: zero_le_mult_iff)
   13.40  declare hrealpow_two_le [simp]
   13.41  
   13.42  lemma hrealpow_two_le_add_order:
   13.43 @@ -85,8 +67,7 @@
   13.44  text{*FIXME: DELETE THESE*}
   13.45  lemma hypreal_three_squares_add_zero_iff:
   13.46       "(x*x + y*y + z*z = 0) = (x = 0 & y = 0 & z = (0::hypreal))"
   13.47 -apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff)
   13.48 -apply auto
   13.49 +apply (simp only: zero_le_square hypreal_le_add_order hypreal_add_nonneg_eq_0_iff, auto)
   13.50  done
   13.51  
   13.52  lemma hrealpow_three_squares_add_zero_iff [simp]:
   13.53 @@ -105,24 +86,19 @@
   13.54  lemma two_hrealpow_gt: "hypreal_of_nat n < 2 ^ n"
   13.55  apply (induct_tac "n")
   13.56  apply (auto simp add: hypreal_of_nat_Suc left_distrib)
   13.57 -apply (cut_tac n = "n" in two_hrealpow_ge_one)
   13.58 -apply arith
   13.59 +apply (cut_tac n = n in two_hrealpow_ge_one, arith)
   13.60  done
   13.61  declare two_hrealpow_gt [simp] 
   13.62  
   13.63  lemma hrealpow_minus_one: "-1 ^ (2*n) = (1::hypreal)"
   13.64 -apply (induct_tac "n")
   13.65 -apply auto
   13.66 -done
   13.67 +by (induct_tac "n", auto)
   13.68  
   13.69  lemma double_lemma: "n+n = (2*n::nat)"
   13.70 -apply auto
   13.71 -done
   13.72 +by auto
   13.73  
   13.74  (*ugh: need to get rid fo the n+n*)
   13.75  lemma hrealpow_minus_one2: "-1 ^ (n + n) = (1::hypreal)"
   13.76 -apply (auto simp add: double_lemma hrealpow_minus_one)
   13.77 -done
   13.78 +by (auto simp add: double_lemma hrealpow_minus_one)
   13.79  declare hrealpow_minus_one2 [simp]
   13.80  
   13.81  lemma hrealpow:
   13.82 @@ -163,25 +139,23 @@
   13.83       "congruent hyprel
   13.84       (%X Y. hyprel``{%n. ((X::nat=>real) n ^ (Y::nat=>nat) n)})"
   13.85  apply (unfold congruent_def)
   13.86 -apply (auto intro!: ext)
   13.87 -apply fuf+
   13.88 +apply (auto intro!: ext, fuf+)
   13.89  done
   13.90  
   13.91  lemma hyperpow:
   13.92    "Abs_hypreal(hyprel``{%n. X n}) pow Abs_hypnat(hypnatrel``{%n. Y n}) =
   13.93     Abs_hypreal(hyprel``{%n. X n ^ Y n})"
   13.94  apply (unfold hyperpow_def)
   13.95 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
   13.96 +apply (rule_tac f = Abs_hypreal in arg_cong)
   13.97  apply (auto intro!: lemma_hyprel_refl bexI 
   13.98             simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] equiv_hyprel 
   13.99 -                     hyperpow_congruent)
  13.100 -apply fuf
  13.101 +                     hyperpow_congruent, fuf)
  13.102  done
  13.103  
  13.104  lemma hyperpow_zero: "(0::hypreal) pow (n + (1::hypnat)) = 0"
  13.105  apply (unfold hypnat_one_def)
  13.106  apply (simp (no_asm) add: hypreal_zero_def)
  13.107 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.108 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.109  apply (auto simp add: hyperpow hypnat_add)
  13.110  done
  13.111  declare hyperpow_zero [simp]
  13.112 @@ -189,39 +163,38 @@
  13.113  lemma hyperpow_not_zero [rule_format (no_asm)]:
  13.114       "r \<noteq> (0::hypreal) --> r pow n \<noteq> 0"
  13.115  apply (simp (no_asm) add: hypreal_zero_def)
  13.116 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.117 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.118 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.119 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.120  apply (auto simp add: hyperpow)
  13.121 -apply (drule FreeUltrafilterNat_Compl_mem)
  13.122 -apply ultra
  13.123 +apply (drule FreeUltrafilterNat_Compl_mem, ultra)
  13.124  done
  13.125  
  13.126  lemma hyperpow_inverse:
  13.127       "r \<noteq> (0::hypreal) --> inverse(r pow n) = (inverse r) pow n"
  13.128  apply (simp (no_asm) add: hypreal_zero_def)
  13.129 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.130 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.131 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.132 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.133  apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: hypreal_inverse hyperpow)
  13.134  apply (rule FreeUltrafilterNat_subset)
  13.135  apply (auto dest: realpow_not_zero intro: power_inverse)
  13.136  done
  13.137  
  13.138  lemma hyperpow_hrabs: "abs r pow n = abs (r pow n)"
  13.139 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.140 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.141 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.142 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.143  apply (auto simp add: hypreal_hrabs hyperpow power_abs [symmetric])
  13.144  done
  13.145  
  13.146  lemma hyperpow_add: "r pow (n + m) = (r pow n) * (r pow m)"
  13.147 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.148 -apply (rule_tac z = "m" in eq_Abs_hypnat)
  13.149 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.150 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.151 +apply (rule_tac z = m in eq_Abs_hypnat)
  13.152 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.153  apply (auto simp add: hyperpow hypnat_add hypreal_mult power_add)
  13.154  done
  13.155  
  13.156  lemma hyperpow_one: "r pow (1::hypnat) = r"
  13.157  apply (unfold hypnat_one_def)
  13.158 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.159 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.160  apply (auto simp add: hyperpow)
  13.161  done
  13.162  declare hyperpow_one [simp]
  13.163 @@ -229,38 +202,38 @@
  13.164  lemma hyperpow_two:
  13.165       "r pow ((1::hypnat) + (1::hypnat)) = r * r"
  13.166  apply (unfold hypnat_one_def)
  13.167 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.168 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.169  apply (auto simp add: hyperpow hypnat_add hypreal_mult)
  13.170  done
  13.171  
  13.172  lemma hyperpow_gt_zero: "(0::hypreal) < r ==> 0 < r pow n"
  13.173  apply (simp add: hypreal_zero_def)
  13.174 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.175 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.176 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.177 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.178  apply (auto elim!: FreeUltrafilterNat_subset zero_less_power
  13.179                     simp add: hyperpow hypreal_less hypreal_le)
  13.180  done
  13.181  
  13.182  lemma hyperpow_ge_zero: "(0::hypreal) \<le> r ==> 0 \<le> r pow n"
  13.183  apply (simp add: hypreal_zero_def)
  13.184 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.185 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.186 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.187 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.188  apply (auto elim!: FreeUltrafilterNat_subset zero_le_power 
  13.189              simp add: hyperpow hypreal_le)
  13.190  done
  13.191  
  13.192  lemma hyperpow_le: "[|(0::hypreal) < x; x \<le> y|] ==> x pow n \<le> y pow n"
  13.193  apply (simp add: hypreal_zero_def)
  13.194 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.195 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  13.196 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  13.197 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.198 +apply (rule_tac z = x in eq_Abs_hypreal)
  13.199 +apply (rule_tac z = y in eq_Abs_hypreal)
  13.200  apply (auto simp add: hyperpow hypreal_le hypreal_less)
  13.201 -apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset] , assumption)
  13.202 +apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset], assumption)
  13.203  apply (auto intro: power_mono)
  13.204  done
  13.205  
  13.206  lemma hyperpow_eq_one: "1 pow n = (1::hypreal)"
  13.207 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.208 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.209  apply (auto simp add: hypreal_one_def hyperpow)
  13.210  done
  13.211  declare hyperpow_eq_one [simp]
  13.212 @@ -268,28 +241,24 @@
  13.213  lemma hrabs_hyperpow_minus_one: "abs(-1 pow n) = (1::hypreal)"
  13.214  apply (subgoal_tac "abs ((- (1::hypreal)) pow n) = (1::hypreal) ")
  13.215  apply simp
  13.216 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.217 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.218  apply (auto simp add: hypreal_one_def hyperpow hypreal_minus hypreal_hrabs)
  13.219  done
  13.220  declare hrabs_hyperpow_minus_one [simp]
  13.221  
  13.222  lemma hyperpow_mult: "(r * s) pow n = (r pow n) * (s pow n)"
  13.223 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.224 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.225 -apply (rule_tac z = "s" in eq_Abs_hypreal)
  13.226 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.227 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.228 +apply (rule_tac z = s in eq_Abs_hypreal)
  13.229  apply (auto simp add: hyperpow hypreal_mult power_mult_distrib)
  13.230  done
  13.231  
  13.232  lemma hyperpow_two_le: "(0::hypreal) \<le> r pow ((1::hypnat) + (1::hypnat))"
  13.233 -apply (auto simp add: hyperpow_two zero_le_mult_iff)
  13.234 -done
  13.235 +by (auto simp add: hyperpow_two zero_le_mult_iff)
  13.236  declare hyperpow_two_le [simp]
  13.237  
  13.238 -lemma hrabs_hyperpow_two:
  13.239 -     "abs(x pow (1 + 1)) = x pow (1 + 1)"
  13.240 -apply (simp (no_asm) add: hrabs_eqI1)
  13.241 -done
  13.242 -declare hrabs_hyperpow_two [simp]
  13.243 +lemma hrabs_hyperpow_two [simp]: "abs(x pow (1 + 1)) = x pow (1 + 1)"
  13.244 +by (simp add: hrabs_def hyperpow_two_le)
  13.245  
  13.246  lemma hyperpow_two_hrabs:
  13.247       "abs(x) pow (1 + 1)  = x pow (1 + 1)"
  13.248 @@ -301,8 +270,7 @@
  13.249       "(1::hypreal) < r ==> 1 < r pow (1 + 1)"
  13.250  apply (auto simp add: hyperpow_two)
  13.251  apply (rule_tac y = "1*1" in order_le_less_trans)
  13.252 -apply (rule_tac [2] hypreal_mult_less_mono)
  13.253 -apply auto
  13.254 +apply (rule_tac [2] hypreal_mult_less_mono, auto)
  13.255  done
  13.256  
  13.257  lemma hyperpow_two_ge_one:
  13.258 @@ -312,8 +280,7 @@
  13.259  
  13.260  lemma two_hyperpow_ge_one: "(1::hypreal) \<le> 2 pow n"
  13.261  apply (rule_tac y = "1 pow n" in order_trans)
  13.262 -apply (rule_tac [2] hyperpow_le)
  13.263 -apply auto
  13.264 +apply (rule_tac [2] hyperpow_le, auto)
  13.265  done
  13.266  declare two_hyperpow_ge_one [simp]
  13.267  
  13.268 @@ -322,21 +289,21 @@
  13.269  apply (subgoal_tac " (- ((1::hypreal))) pow ((1 + 1)*n) = (1::hypreal) ")
  13.270  apply simp
  13.271  apply (simp only: hypreal_one_def)
  13.272 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.273 -apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus)
  13.274 +apply (rule eq_Abs_hypnat [of n])
  13.275 +apply (auto simp add: double_lemma hyperpow hypnat_add hypreal_minus
  13.276 +                      left_distrib)
  13.277  done
  13.278  declare hyperpow_minus_one2 [simp]
  13.279  
  13.280  lemma hyperpow_less_le:
  13.281       "[|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
  13.282 -apply (rule_tac z = "n" in eq_Abs_hypnat)
  13.283 -apply (rule_tac z = "N" in eq_Abs_hypnat)
  13.284 -apply (rule_tac z = "r" in eq_Abs_hypreal)
  13.285 +apply (rule_tac z = n in eq_Abs_hypnat)
  13.286 +apply (rule_tac z = N in eq_Abs_hypnat)
  13.287 +apply (rule_tac z = r in eq_Abs_hypreal)
  13.288  apply (auto simp add: hyperpow hypreal_le hypreal_less hypnat_less 
  13.289              hypreal_zero_def hypreal_one_def)
  13.290  apply (erule FreeUltrafilterNat_Int [THEN FreeUltrafilterNat_subset])
  13.291 -apply (erule FreeUltrafilterNat_Int)
  13.292 -apply assumption; 
  13.293 +apply (erule FreeUltrafilterNat_Int, assumption)
  13.294  apply (auto intro: power_decreasing)
  13.295  done
  13.296  
  13.297 @@ -358,14 +325,12 @@
  13.298  declare hyperpow_SReal [simp]
  13.299  
  13.300  lemma hyperpow_zero_HNatInfinite: "N \<in> HNatInfinite ==> (0::hypreal) pow N = 0"
  13.301 -apply (drule HNatInfinite_is_Suc)
  13.302 -apply auto
  13.303 -done
  13.304 +by (drule HNatInfinite_is_Suc, auto)
  13.305  declare hyperpow_zero_HNatInfinite [simp]
  13.306  
  13.307  lemma hyperpow_le_le:
  13.308       "[| (0::hypreal) \<le> r; r \<le> 1; n \<le> N |] ==> r pow N \<le> r pow n"
  13.309 -apply (drule_tac y = "N" in hypnat_le_imp_less_or_eq)
  13.310 +apply (drule order_le_less [of n, THEN iffD1])
  13.311  apply (auto intro: hyperpow_less_le)
  13.312  done
  13.313  
  13.314 @@ -385,14 +350,13 @@
  13.315  lemma Infinitesimal_hyperpow:
  13.316       "[| x \<in> Infinitesimal; 0 < N |] ==> x pow N \<in> Infinitesimal"
  13.317  apply (rule hrabs_le_Infinitesimal)
  13.318 -apply (rule_tac [2] lemma_Infinitesimal_hyperpow)
  13.319 -apply auto
  13.320 +apply (rule_tac [2] lemma_Infinitesimal_hyperpow, auto)
  13.321  done
  13.322  
  13.323  lemma hrealpow_hyperpow_Infinitesimal_iff:
  13.324       "(x ^ n \<in> Infinitesimal) = (x pow (hypnat_of_nat n) \<in> Infinitesimal)"
  13.325  apply (unfold hypnat_of_nat_def)
  13.326 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  13.327 +apply (rule_tac z = x in eq_Abs_hypreal)
  13.328  apply (auto simp add: hrealpow hyperpow)
  13.329  done
  13.330  
  13.331 @@ -400,8 +364,8 @@
  13.332       "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
  13.333  by (force intro!: Infinitesimal_hyperpow
  13.334            simp add: hrealpow_hyperpow_Infinitesimal_iff 
  13.335 -                    hypnat_of_nat_less_iff hypnat_of_nat_zero
  13.336 -          simp del: hypnat_of_nat_less_iff [symmetric])
  13.337 +                    hypnat_of_nat_less_iff [symmetric] hypnat_of_nat_zero
  13.338 +          simp del: hypnat_of_nat_less_iff)
  13.339  
  13.340  ML
  13.341  {*
    14.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu Jan 29 16:51:17 2004 +0100
    14.2 +++ b/src/HOL/Hyperreal/NSA.thy	Mon Feb 02 12:23:46 2004 +0100
    14.3 @@ -5,7 +5,7 @@
    14.4  
    14.5  header{*Infinite Numbers, Infinitesimals, Infinitely Close Relation*}
    14.6  
    14.7 -theory NSA = HRealAbs + RComplete:
    14.8 +theory NSA = HyperArith + RComplete:
    14.9  
   14.10  constdefs
   14.11  
    15.1 --- a/src/HOL/Hyperreal/NatStar.ML	Thu Jan 29 16:51:17 2004 +0100
    15.2 +++ b/src/HOL/Hyperreal/NatStar.ML	Mon Feb 02 12:23:46 2004 +0100
    15.3 @@ -209,7 +209,7 @@
    15.4  \      Abs_hypnat(hypnatrel `` {%n. f (X n)})";
    15.5  by (res_inst_tac [("f","Abs_hypnat")] arg_cong 1);
    15.6  by (simp_tac (simpset() addsimps 
    15.7 -   [hypnatrel_in_hypnat RS Abs_hypnat_inverse,
    15.8 +   [hypnatrel_in_hypnat RS thm"Abs_hypnat_inverse",
    15.9      [equiv_hypnatrel, starfunNat_congruent] MRS UN_equiv_class]) 1);
   15.10  qed "starfunNat2";
   15.11  
   15.12 @@ -406,7 +406,7 @@
   15.13  by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
   15.14  by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
   15.15  by (auto_tac (claset(), 
   15.16 -       simpset() addsimps [starfunNat_real_of_nat, starfun_inverse_inverse]));
   15.17 +       simpset() addsimps [HNatInfinite_not_eq_zero, starfunNat_real_of_nat, starfun_inverse_inverse]));
   15.18  qed "starfunNat_inverse_real_of_nat_eq";
   15.19  
   15.20  (*----------------------------------------------------------
   15.21 @@ -488,6 +488,6 @@
   15.22  \     ==> ( *fNat* (%x. inverse (real x))) N : Infinitesimal";
   15.23  by (res_inst_tac [("f1","inverse")]  (starfun_stafunNat_o2 RS subst) 1);
   15.24  by (subgoal_tac "hypreal_of_hypnat N ~= 0" 1);
   15.25 -by (auto_tac (claset(),simpset() addsimps [starfunNat_real_of_nat]));
   15.26 +by (auto_tac (claset(), simpset() addsimps [HNatInfinite_not_eq_zero, starfunNat_real_of_nat]));
   15.27  qed "starfunNat_inverse_real_of_nat_Infinitesimal";
   15.28  Addsimps [starfunNat_inverse_real_of_nat_Infinitesimal];
    16.1 --- a/src/HOL/Hyperreal/SEQ.ML	Thu Jan 29 16:51:17 2004 +0100
    16.2 +++ b/src/HOL/Hyperreal/SEQ.ML	Mon Feb 02 12:23:46 2004 +0100
    16.3 @@ -4,6 +4,13 @@
    16.4      Description : Theory of sequence and series of real numbers
    16.5  *) 
    16.6  
    16.7 +fun CLAIM_SIMP str thms =
    16.8 +               prove_goal (the_context()) str
    16.9 +               (fn prems => [cut_facts_tac prems 1,
   16.10 +                   auto_tac (claset(),simpset() addsimps thms)]);
   16.11 +
   16.12 +fun CLAIM str = CLAIM_SIMP str [];
   16.13 +
   16.14  (*---------------------------------------------------------------------------
   16.15     Example of an hypersequence (i.e. an extended standard sequence) 
   16.16     whose term with an hypernatural suffix is an infinitesimal i.e. 
    17.1 --- a/src/HOL/Hyperreal/Star.thy	Thu Jan 29 16:51:17 2004 +0100
    17.2 +++ b/src/HOL/Hyperreal/Star.thy	Mon Feb 02 12:23:46 2004 +0100
    17.3 @@ -58,55 +58,44 @@
    17.4  
    17.5  lemma STAR_real_set: "*s*(UNIV::real set) = (UNIV::hypreal set)"
    17.6  
    17.7 -apply (unfold starset_def)
    17.8 -apply auto
    17.9 +apply (unfold starset_def, auto)
   17.10  done
   17.11  declare STAR_real_set [simp]
   17.12  
   17.13  lemma STAR_empty_set: "*s* {} = {}"
   17.14 -apply (unfold starset_def)
   17.15 -apply safe
   17.16 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   17.17 -apply (drule_tac x = "%n. xa n" in bspec)
   17.18 -apply auto
   17.19 +apply (unfold starset_def, safe)
   17.20 +apply (rule_tac z = x in eq_Abs_hypreal)
   17.21 +apply (drule_tac x = "%n. xa n" in bspec, auto)
   17.22  done
   17.23  declare STAR_empty_set [simp]
   17.24  
   17.25  lemma STAR_Un: "*s* (A Un B) = *s* A Un *s* B"
   17.26 -apply (unfold starset_def)
   17.27 -apply auto
   17.28 +apply (unfold starset_def, auto)
   17.29    prefer 3 apply (blast intro: FreeUltrafilterNat_subset)
   17.30   prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
   17.31  apply (drule FreeUltrafilterNat_Compl_mem)
   17.32 -apply (drule bspec , assumption)
   17.33 -apply (rule_tac z = "x" in eq_Abs_hypreal)
   17.34 -apply auto
   17.35 -apply ultra
   17.36 +apply (drule bspec, assumption)
   17.37 +apply (rule_tac z = x in eq_Abs_hypreal, auto, ultra)
   17.38  done
   17.39  
   17.40  lemma STAR_Int: "*s* (A Int B) = *s* A Int *s* B"
   17.41 -apply (unfold starset_def)
   17.42 -apply auto
   17.43 +apply (unfold starset_def, auto)
   17.44  prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset)
   17.45  apply (blast intro: FreeUltrafilterNat_subset)+
   17.46  done
   17.47  
   17.48  lemma STAR_Compl: "*s* -A = -( *s* A)"
   17.49  apply (auto simp add: starset_def)
   17.50 -apply (rule_tac [!] z = "x" in eq_Abs_hypreal)
   17.51 -apply (auto dest!: bspec);
   17.52 -apply ultra
   17.53 -apply (drule FreeUltrafilterNat_Compl_mem)
   17.54 -apply ultra
   17.55 +apply (rule_tac [!] z = x in eq_Abs_hypreal)
   17.56 +apply (auto dest!: bspec, ultra)
   17.57 +apply (drule FreeUltrafilterNat_Compl_mem, ultra)
   17.58  done
   17.59  
   17.60  lemma STAR_mem_Compl: "x \<notin> *s* F ==> x : *s* (- F)"
   17.61 -apply (auto simp add: STAR_Compl)
   17.62 -done
   17.63 +by (auto simp add: STAR_Compl)
   17.64  
   17.65  lemma STAR_diff: "*s* (A - B) = *s* A - *s* B"
   17.66 -apply (auto simp add: Diff_eq STAR_Int STAR_Compl)
   17.67 -done
   17.68 +by (auto simp add: Diff_eq STAR_Int STAR_Compl)
   17.69  
   17.70  lemma STAR_subset: "A <= B ==> *s* A <= *s* B"
   17.71  apply (unfold starset_def)
   17.72 @@ -128,46 +117,40 @@
   17.73  apply (unfold starset_def)
   17.74  apply (auto simp add: hypreal_of_real_def SReal_def)
   17.75  apply (simp add: hypreal_of_real_def [symmetric])
   17.76 -apply (rule imageI , rule ccontr)
   17.77 +apply (rule imageI, rule ccontr)
   17.78  apply (drule bspec)
   17.79  apply (rule lemma_hyprel_refl)
   17.80 -prefer 2 apply (blast intro: FreeUltrafilterNat_subset)
   17.81 -apply auto
   17.82 +prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto)
   17.83  done
   17.84  
   17.85  lemma lemma_not_hyprealA: "x \<notin> hypreal_of_real ` A ==> ALL y: A. x \<noteq> hypreal_of_real y"
   17.86 -apply auto
   17.87 -done
   17.88 +by auto
   17.89  
   17.90  lemma lemma_Compl_eq: "- {n. X n = xa} = {n. X n \<noteq> xa}"
   17.91 -apply auto
   17.92 -done
   17.93 +by auto
   17.94  
   17.95  lemma STAR_real_seq_to_hypreal:
   17.96      "ALL n. (X n) \<notin> M
   17.97            ==> Abs_hypreal(hyprel``{X}) \<notin> *s* M"
   17.98  apply (unfold starset_def)
   17.99 -apply (auto , rule bexI , rule_tac [2] lemma_hyprel_refl)
  17.100 -apply auto
  17.101 +apply (auto, rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
  17.102  done
  17.103  
  17.104  lemma STAR_singleton: "*s* {x} = {hypreal_of_real x}"
  17.105  apply (unfold starset_def)
  17.106  apply (auto simp add: hypreal_of_real_def)
  17.107 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  17.108 +apply (rule_tac z = xa in eq_Abs_hypreal)
  17.109  apply (auto intro: FreeUltrafilterNat_subset)
  17.110  done
  17.111  declare STAR_singleton [simp]
  17.112  
  17.113  lemma STAR_not_mem: "x \<notin> F ==> hypreal_of_real x \<notin> *s* F"
  17.114  apply (auto simp add: starset_def hypreal_of_real_def)
  17.115 -apply (rule bexI , rule_tac [2] lemma_hyprel_refl)
  17.116 -apply auto
  17.117 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, auto)
  17.118  done
  17.119  
  17.120  lemma STAR_subset_closed: "[| x : *s* A; A <= B |] ==> x : *s* B"
  17.121 -apply (blast dest: STAR_subset)
  17.122 -done
  17.123 +by (blast dest: STAR_subset)
  17.124  
  17.125  (*------------------------------------------------------------------
  17.126     Nonstandard extension of a set (defined using a constant
  17.127 @@ -177,8 +160,7 @@
  17.128  lemma starset_n_starset:
  17.129       "ALL n. (As n = A) ==> *sn* As = *s* A"
  17.130  
  17.131 -apply (unfold starset_n_def starset_def)
  17.132 -apply auto
  17.133 +apply (unfold starset_n_def starset_def, auto)
  17.134  done
  17.135  
  17.136  
  17.137 @@ -194,8 +176,7 @@
  17.138  lemma starfun_n_starfun:
  17.139       "ALL n. (F n = f) ==> *fn* F = *f* f"
  17.140  
  17.141 -apply (unfold starfun_n_def starfun_def)
  17.142 -apply auto
  17.143 +apply (unfold starfun_n_def starfun_def, auto)
  17.144  done
  17.145  
  17.146  
  17.147 @@ -212,21 +193,19 @@
  17.148  
  17.149  lemma hrabs_is_starext_rabs: "is_starext abs abs"
  17.150  
  17.151 -apply (unfold is_starext_def)
  17.152 -apply safe
  17.153 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.154 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  17.155 -apply auto
  17.156 -apply (rule bexI , rule_tac [2] lemma_hyprel_refl)
  17.157 -apply (rule bexI , rule_tac [2] lemma_hyprel_refl)
  17.158 +apply (unfold is_starext_def, safe)
  17.159 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.160 +apply (rule_tac z = y in eq_Abs_hypreal, auto)
  17.161 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
  17.162 +apply (rule bexI, rule_tac [2] lemma_hyprel_refl)
  17.163  apply (auto dest!: spec simp add: hypreal_minus hrabs_def hypreal_zero_def hypreal_le_def hypreal_less_def)
  17.164  apply (arith | ultra)+
  17.165  done
  17.166  
  17.167  lemma Rep_hypreal_FreeUltrafilterNat: "[| X: Rep_hypreal z; Y: Rep_hypreal z |]
  17.168        ==> {n. X n = Y n} : FreeUltrafilterNat"
  17.169 -apply (rule_tac z = "z" in eq_Abs_hypreal)
  17.170 -apply (auto , ultra)
  17.171 +apply (rule_tac z = z in eq_Abs_hypreal)
  17.172 +apply (auto, ultra)
  17.173  done
  17.174  
  17.175  (*-----------------------------------------------------------------------
  17.176 @@ -234,44 +213,41 @@
  17.177   -----------------------------------------------------------------------*)
  17.178  
  17.179  lemma starfun_congruent: "congruent hyprel (%X. hyprel``{%n. f (X n)})"
  17.180 -apply (unfold congruent_def)
  17.181 -apply auto
  17.182 -apply ultra
  17.183 -done
  17.184 +by (unfold congruent_def, auto, ultra)
  17.185  
  17.186  lemma starfun:
  17.187        "( *f* f) (Abs_hypreal(hyprel``{%n. X n})) =
  17.188         Abs_hypreal(hyprel `` {%n. f (X n)})"
  17.189  apply (unfold starfun_def)
  17.190 -apply (rule_tac f = "Abs_hypreal" in arg_cong)
  17.191 +apply (rule_tac f = Abs_hypreal in arg_cong)
  17.192  apply (simp add: hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
  17.193                   UN_equiv_class [OF equiv_hyprel starfun_congruent])
  17.194  done
  17.195  
  17.196  (*-------------------------------------------
  17.197 -  multiplication: ( *f ) x ( *g ) = *(f x g)
  17.198 +  multiplication: ( *f) x ( *g) = *(f x g)
  17.199   ------------------------------------------*)
  17.200  lemma starfun_mult: "( *f* f) xa * ( *f* g) xa = ( *f* (%x. f x * g x)) xa"
  17.201 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  17.202 +apply (rule_tac z = xa in eq_Abs_hypreal)
  17.203  apply (auto simp add: starfun hypreal_mult)
  17.204  done
  17.205  declare starfun_mult [symmetric, simp]
  17.206  
  17.207  (*---------------------------------------
  17.208 -  addition: ( *f ) + ( *g ) = *(f + g)
  17.209 +  addition: ( *f) + ( *g) = *(f + g)
  17.210   ---------------------------------------*)
  17.211  lemma starfun_add: "( *f* f) xa + ( *f* g) xa = ( *f* (%x. f x + g x)) xa"
  17.212 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  17.213 +apply (rule_tac z = xa in eq_Abs_hypreal)
  17.214  apply (auto simp add: starfun hypreal_add)
  17.215  done
  17.216  declare starfun_add [symmetric, simp]
  17.217  
  17.218  (*--------------------------------------------
  17.219 -  subtraction: ( *f ) + -( *g ) = *(f + -g)
  17.220 +  subtraction: ( *f) + -( *g) = *(f + -g)
  17.221   -------------------------------------------*)
  17.222  
  17.223  lemma starfun_minus: "- ( *f* f) x = ( *f* (%x. - f x)) x"
  17.224 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.225 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.226  apply (auto simp add: starfun hypreal_minus)
  17.227  done
  17.228  declare starfun_minus [symmetric, simp]
  17.229 @@ -290,12 +266,12 @@
  17.230  declare starfun_diff [symmetric, simp]
  17.231  
  17.232  (*--------------------------------------
  17.233 -  composition: ( *f ) o ( *g ) = *(f o g)
  17.234 +  composition: ( *f) o ( *g) = *(f o g)
  17.235   ---------------------------------------*)
  17.236  
  17.237  lemma starfun_o2: "(%x. ( *f* f) (( *f* g) x)) = *f* (%x. f (g x))"
  17.238  apply (rule ext)
  17.239 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.240 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.241  apply (auto simp add: starfun)
  17.242  done
  17.243  
  17.244 @@ -308,7 +284,7 @@
  17.245    NS extension of constant function
  17.246   --------------------------------------*)
  17.247  lemma starfun_const_fun: "( *f* (%x. k)) xa = hypreal_of_real  k"
  17.248 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  17.249 +apply (rule_tac z = xa in eq_Abs_hypreal)
  17.250  apply (auto simp add: starfun hypreal_of_real_def)
  17.251  done
  17.252  
  17.253 @@ -319,12 +295,12 @@
  17.254   ----------------------------------------------------*)
  17.255  
  17.256  lemma starfun_Idfun_approx: "x @= hypreal_of_real a ==> ( *f* (%x. x)) x @= hypreal_of_real  a"
  17.257 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.258 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.259  apply (auto simp add: starfun)
  17.260  done
  17.261  
  17.262  lemma starfun_Id: "( *f* (%x. x)) x = x"
  17.263 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.264 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.265  apply (auto simp add: starfun)
  17.266  done
  17.267  declare starfun_Id [simp]
  17.268 @@ -335,10 +311,9 @@
  17.269  
  17.270  lemma is_starext_starfun: "is_starext ( *f* f) f"
  17.271  
  17.272 -apply (unfold is_starext_def)
  17.273 -apply auto
  17.274 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.275 -apply (rule_tac z = "y" in eq_Abs_hypreal)
  17.276 +apply (unfold is_starext_def, auto)
  17.277 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.278 +apply (rule_tac z = y in eq_Abs_hypreal)
  17.279  apply (auto intro!: bexI simp add: starfun)
  17.280  done
  17.281  
  17.282 @@ -350,16 +325,14 @@
  17.283  
  17.284  apply (unfold is_starext_def)
  17.285  apply (rule ext)
  17.286 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.287 -apply (drule_tac x = "x" in spec)
  17.288 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.289 +apply (drule_tac x = x in spec)
  17.290  apply (drule_tac x = "( *f* f) x" in spec)
  17.291 -apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun)
  17.292 -apply ultra
  17.293 +apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun, ultra)
  17.294  done
  17.295  
  17.296  lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"
  17.297 -apply (blast intro: is_starfun_starext is_starext_starfun)
  17.298 -done
  17.299 +by (blast intro: is_starfun_starext is_starext_starfun)
  17.300  
  17.301  (*--------------------------------------------------------
  17.302     extented function has same solution as its standard
  17.303 @@ -367,31 +340,28 @@
  17.304     for all real arguments
  17.305   -------------------------------------------------------*)
  17.306  lemma starfun_eq: "( *f* f) (hypreal_of_real a) = hypreal_of_real (f a)"
  17.307 -apply (auto simp add: starfun hypreal_of_real_def)
  17.308 -done
  17.309 +by (auto simp add: starfun hypreal_of_real_def)
  17.310  
  17.311  declare starfun_eq [simp]
  17.312  
  17.313  lemma starfun_approx: "( *f* f) (hypreal_of_real a) @= hypreal_of_real (f a)"
  17.314 -apply auto
  17.315 -done
  17.316 +by auto
  17.317  
  17.318  (* useful for NS definition of derivatives *)
  17.319  lemma starfun_lambda_cancel: "( *f* (%h. f (x + h))) xa  = ( *f* f) (hypreal_of_real  x + xa)"
  17.320 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  17.321 +apply (rule_tac z = xa in eq_Abs_hypreal)
  17.322  apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
  17.323  done
  17.324  
  17.325  lemma starfun_lambda_cancel2: "( *f* (%h. f(g(x + h)))) xa = ( *f* (f o g)) (hypreal_of_real x + xa)"
  17.326 -apply (rule_tac z = "xa" in eq_Abs_hypreal)
  17.327 +apply (rule_tac z = xa in eq_Abs_hypreal)
  17.328  apply (auto simp add: starfun hypreal_of_real_def hypreal_add)
  17.329  done
  17.330  
  17.331  lemma starfun_mult_HFinite_approx: "[| ( *f* f) xa @= l; ( *f* g) xa @= m;
  17.332                    l: HFinite; m: HFinite
  17.333                 |] ==>  ( *f* (%x. f x * g x)) xa @= l * m"
  17.334 -apply (drule approx_mult_HFinite)
  17.335 -apply (assumption)+
  17.336 +apply (drule approx_mult_HFinite, assumption+)
  17.337  apply (auto intro: approx_HFinite [OF _ approx_sym])
  17.338  done
  17.339  
  17.340 @@ -410,30 +380,28 @@
  17.341  (* use the theorem we proved above instead          *)
  17.342  
  17.343  lemma starfun_rabs_hrabs: "*f* abs = abs"
  17.344 -apply (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
  17.345 -done
  17.346 +by (rule hrabs_is_starext_rabs [THEN is_starext_starfun_iff [THEN iffD1], symmetric])
  17.347  
  17.348  lemma starfun_inverse_inverse: "( *f* inverse) x = inverse(x)"
  17.349 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.350 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.351  apply (auto simp add: starfun hypreal_inverse hypreal_zero_def)
  17.352  done
  17.353  declare starfun_inverse_inverse [simp]
  17.354  
  17.355  lemma starfun_inverse: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
  17.356 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.357 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.358  apply (auto simp add: starfun hypreal_inverse)
  17.359  done
  17.360  declare starfun_inverse [symmetric, simp]
  17.361  
  17.362  lemma starfun_divide:
  17.363    "( *f* f) xa  / ( *f* g) xa = ( *f* (%x. f x / g x)) xa"
  17.364 -apply (unfold hypreal_divide_def real_divide_def)
  17.365 -apply auto
  17.366 +apply (unfold hypreal_divide_def real_divide_def, auto)
  17.367  done
  17.368  declare starfun_divide [symmetric, simp]
  17.369  
  17.370  lemma starfun_inverse2: "inverse (( *f* f) x) = ( *f* (%x. inverse (f x))) x"
  17.371 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.372 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.373  apply (auto intro: FreeUltrafilterNat_subset dest!: FreeUltrafilterNat_Compl_mem simp add: starfun hypreal_inverse hypreal_zero_def)
  17.374  done
  17.375  
  17.376 @@ -444,11 +412,11 @@
  17.377  lemma starfun_mem_starset:
  17.378        "( *f* f) x : *s* A ==> x : *s* {x. f x : A}"
  17.379  apply (unfold starset_def)
  17.380 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.381 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.382  apply (auto simp add: starfun)
  17.383  apply (rename_tac "X")
  17.384  apply (drule_tac x = "%n. f (X n) " in bspec)
  17.385 -apply (auto , ultra)
  17.386 +apply (auto, ultra)
  17.387  done
  17.388  
  17.389  (*------------------------------------------------------------
  17.390 @@ -470,21 +438,17 @@
  17.391  lemma STAR_rabs_add_minus:
  17.392     "*s* {x. abs (x + - y) < r} =
  17.393       {x. abs(x + -hypreal_of_real y) < hypreal_of_real r}"
  17.394 -apply (unfold starset_def)
  17.395 -apply safe
  17.396 -apply (rule_tac [!] z = "x" in eq_Abs_hypreal)
  17.397 -apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less)
  17.398 -apply ultra
  17.399 +apply (unfold starset_def, safe)
  17.400 +apply (rule_tac [!] z = x in eq_Abs_hypreal)
  17.401 +apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less, ultra)
  17.402  done
  17.403  
  17.404  lemma STAR_starfun_rabs_add_minus:
  17.405    "*s* {x. abs (f x + - y) < r} =
  17.406         {x. abs(( *f* f) x + -hypreal_of_real y) < hypreal_of_real r}"
  17.407 -apply (unfold starset_def)
  17.408 -apply safe
  17.409 -apply (rule_tac [!] z = "x" in eq_Abs_hypreal)
  17.410 -apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun)
  17.411 -apply ultra
  17.412 +apply (unfold starset_def, safe)
  17.413 +apply (rule_tac [!] z = x in eq_Abs_hypreal)
  17.414 +apply (auto intro!: exI dest!: bspec simp add: hypreal_minus hypreal_of_real_def hypreal_add hypreal_hrabs hypreal_less starfun, ultra)
  17.415  done
  17.416  
  17.417  (*-------------------------------------------------------------------
  17.418 @@ -496,12 +460,11 @@
  17.419        (EX X:Rep_hypreal(x).
  17.420          ALL m. {n. abs(X n) < inverse(real(Suc m))}
  17.421                 : FreeUltrafilterNat)"
  17.422 -apply (rule_tac z = "x" in eq_Abs_hypreal)
  17.423 +apply (rule_tac z = x in eq_Abs_hypreal)
  17.424  apply (auto intro!: bexI lemma_hyprel_refl 
  17.425              simp add: Infinitesimal_hypreal_of_nat_iff hypreal_of_real_def 
  17.426       hypreal_inverse hypreal_hrabs hypreal_less hypreal_of_nat_def)
  17.427 -apply (drule_tac x = "n" in spec)
  17.428 -apply ultra
  17.429 +apply (drule_tac x = n in spec, ultra)
  17.430  done
  17.431  
  17.432  lemma approx_FreeUltrafilterNat_iff: "(Abs_hypreal(hyprel``{X}) @= Abs_hypreal(hyprel``{Y})) =
  17.433 @@ -510,13 +473,12 @@
  17.434  apply (subst approx_minus_iff)
  17.435  apply (rule mem_infmal_iff [THEN subst])
  17.436  apply (auto simp add: hypreal_minus hypreal_add Infinitesimal_FreeUltrafilterNat_iff2)
  17.437 -apply (drule_tac x = "m" in spec)
  17.438 -apply ultra
  17.439 +apply (drule_tac x = m in spec, ultra)
  17.440  done
  17.441  
  17.442  lemma inj_starfun: "inj starfun"
  17.443  apply (rule inj_onI)
  17.444 -apply (rule ext , rule ccontr)
  17.445 +apply (rule ext, rule ccontr)
  17.446  apply (drule_tac x = "Abs_hypreal (hyprel ``{%n. xa}) " in fun_cong)
  17.447  apply (auto simp add: starfun)
  17.448  done
    18.1 --- a/src/HOL/IsaMakefile	Thu Jan 29 16:51:17 2004 +0100
    18.2 +++ b/src/HOL/IsaMakefile	Mon Feb 02 12:23:46 2004 +0100
    18.3 @@ -146,10 +146,9 @@
    18.4    Hyperreal/EvenOdd.ML Hyperreal/EvenOdd.thy \
    18.5    Hyperreal/Fact.ML Hyperreal/Fact.thy\
    18.6    Hyperreal/Filter.ML Hyperreal/Filter.thy\
    18.7 -  Hyperreal/HRealAbs.thy Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
    18.8 -  Hyperreal/HyperArith.thy \
    18.9 -  Hyperreal/HyperDef.thy Hyperreal/HyperNat.ML Hyperreal/HyperNat.thy\
   18.10 -  Hyperreal/HyperOrd.thy Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   18.11 +  Hyperreal/HSeries.ML Hyperreal/HSeries.thy\
   18.12 +  Hyperreal/HyperArith.thy Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy\
   18.13 +  Hyperreal/HyperPow.thy Hyperreal/Hyperreal.thy\
   18.14    Hyperreal/IntFloor.thy Hyperreal/IntFloor.ML\
   18.15    Hyperreal/Lim.ML Hyperreal/Lim.thy  Hyperreal/Log.ML Hyperreal/Log.thy\
   18.16    Hyperreal/MacLaurin.ML Hyperreal/MacLaurin.thy\