src/HOL/Real/Hyperreal/HyperNat.ML
changeset 10045 c76b73e16711
child 10201 b52140d1a7bc
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/HyperNat.ML	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,1338 @@
     1.4 +(*  Title       : HyperNat.ML
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Explicit construction of hypernaturals using 
     1.8 +                  ultrafilters
     1.9 +*) 
    1.10 +       
    1.11 +(*------------------------------------------------------------------------
    1.12 +                       Properties of hypnatrel
    1.13 + ------------------------------------------------------------------------*)
    1.14 +
    1.15 +(** Proving that hyprel is an equivalence relation       **)
    1.16 +(** Natural deduction for hypnatrel - similar to hyprel! **)
    1.17 +
    1.18 +Goalw [hypnatrel_def]
    1.19 +   "((X,Y): hypnatrel) = ({n. X n = Y n}: FreeUltrafilterNat)";
    1.20 +by (Fast_tac 1);
    1.21 +qed "hypnatrel_iff";
    1.22 +
    1.23 +Goalw [hypnatrel_def] 
    1.24 +     "{n. X n = Y n}: FreeUltrafilterNat ==> (X,Y): hypnatrel";
    1.25 +by (Fast_tac 1);
    1.26 +qed "hypnatrelI";
    1.27 +
    1.28 +Goalw [hypnatrel_def]
    1.29 +  "p: hypnatrel --> (EX X Y. \
    1.30 +\                 p = (X,Y) & {n. X n = Y n} : FreeUltrafilterNat)";
    1.31 +by (Fast_tac 1);
    1.32 +qed "hypnatrelE_lemma";
    1.33 +
    1.34 +val [major,minor] = goal thy
    1.35 +  "[| p: hypnatrel;  \
    1.36 +\     !!X Y. [| p = (X,Y); {n. X n = Y n}: FreeUltrafilterNat\
    1.37 +\            |] ==> Q |] ==> Q";
    1.38 +by (cut_facts_tac [major RS (hypnatrelE_lemma RS mp)] 1);
    1.39 +by (REPEAT (eresolve_tac [asm_rl,exE,conjE,minor] 1));
    1.40 +qed "hypnatrelE";
    1.41 +
    1.42 +AddSIs [hypnatrelI];
    1.43 +AddSEs [hypnatrelE];
    1.44 +
    1.45 +Goalw [hypnatrel_def] "(x,x): hypnatrel";
    1.46 +by (Auto_tac);
    1.47 +qed "hypnatrel_refl";
    1.48 +
    1.49 +Goalw [hypnatrel_def] "(x,y): hypnatrel --> (y,x):hypnatrel";
    1.50 +by (auto_tac (claset() addIs [lemma_perm RS subst],simpset()));
    1.51 +qed_spec_mp "hypnatrel_sym";
    1.52 +
    1.53 +Goalw [hypnatrel_def]
    1.54 +      "(x,y): hypnatrel --> (y,z):hypnatrel --> (x,z):hypnatrel";
    1.55 +by (Auto_tac);
    1.56 +by (Fuf_tac 1);
    1.57 +qed_spec_mp "hypnatrel_trans";
    1.58 +
    1.59 +Goalw [equiv_def, refl_def, sym_def, trans_def]
    1.60 +    "equiv {x::nat=>nat. True} hypnatrel";
    1.61 +by (auto_tac (claset() addSIs [hypnatrel_refl] addSEs 
    1.62 +    [hypnatrel_sym,hypnatrel_trans] delrules [hypnatrelI,hypnatrelE],
    1.63 +    simpset()));
    1.64 +qed "equiv_hypnatrel";
    1.65 +
    1.66 +val equiv_hypnatrel_iff =
    1.67 +    [TrueI, TrueI] MRS 
    1.68 +    ([CollectI, CollectI] MRS 
    1.69 +    (equiv_hypnatrel RS eq_equiv_class_iff));
    1.70 +
    1.71 +Goalw  [hypnat_def,hypnatrel_def,quotient_def] "hypnatrel^^{x}:hypnat";
    1.72 +by (Blast_tac 1);
    1.73 +qed "hypnatrel_in_hypnat";
    1.74 +
    1.75 +Goal "inj_on Abs_hypnat hypnat";
    1.76 +by (rtac inj_on_inverseI 1);
    1.77 +by (etac Abs_hypnat_inverse 1);
    1.78 +qed "inj_on_Abs_hypnat";
    1.79 +
    1.80 +Addsimps [equiv_hypnatrel_iff,inj_on_Abs_hypnat RS inj_on_iff,
    1.81 +          hypnatrel_iff, hypnatrel_in_hypnat, Abs_hypnat_inverse];
    1.82 +
    1.83 +Addsimps [equiv_hypnatrel RS eq_equiv_class_iff];
    1.84 +val eq_hypnatrelD = equiv_hypnatrel RSN (2,eq_equiv_class);
    1.85 +
    1.86 +Goal "inj(Rep_hypnat)";
    1.87 +by (rtac inj_inverseI 1);
    1.88 +by (rtac Rep_hypnat_inverse 1);
    1.89 +qed "inj_Rep_hypnat";
    1.90 +
    1.91 +Goalw [hypnatrel_def] "x: hypnatrel ^^ {x}";
    1.92 +by (Step_tac 1);
    1.93 +by (Auto_tac);
    1.94 +qed "lemma_hypnatrel_refl";
    1.95 +
    1.96 +Addsimps [lemma_hypnatrel_refl];
    1.97 +
    1.98 +Goalw [hypnat_def] "{} ~: hypnat";
    1.99 +by (auto_tac (claset() addSEs [quotientE],simpset()));
   1.100 +qed "hypnat_empty_not_mem";
   1.101 +
   1.102 +Addsimps [hypnat_empty_not_mem];
   1.103 +
   1.104 +Goal "Rep_hypnat x ~= {}";
   1.105 +by (cut_inst_tac [("x","x")] Rep_hypnat 1);
   1.106 +by (Auto_tac);
   1.107 +qed "Rep_hypnat_nonempty";
   1.108 +
   1.109 +Addsimps [Rep_hypnat_nonempty];
   1.110 +
   1.111 +(*------------------------------------------------------------------------
   1.112 +   hypnat_of_nat: the injection from nat to hypnat
   1.113 + ------------------------------------------------------------------------*)
   1.114 +Goal "inj(hypnat_of_nat)";
   1.115 +by (rtac injI 1);
   1.116 +by (rewtac hypnat_of_nat_def);
   1.117 +by (dtac (inj_on_Abs_hypnat RS inj_onD) 1);
   1.118 +by (REPEAT (rtac hypnatrel_in_hypnat 1));
   1.119 +by (dtac eq_equiv_class 1);
   1.120 +by (rtac equiv_hypnatrel 1);
   1.121 +by (Fast_tac 1);
   1.122 +by (rtac ccontr 1 THEN rotate_tac 1 1);
   1.123 +by (Auto_tac);
   1.124 +qed "inj_hypnat_of_nat";
   1.125 +
   1.126 +val [prem] = goal thy
   1.127 +    "(!!x. z = Abs_hypnat(hypnatrel^^{x}) ==> P) ==> P";
   1.128 +by (res_inst_tac [("x1","z")] 
   1.129 +    (rewrite_rule [hypnat_def] Rep_hypnat RS quotientE) 1);
   1.130 +by (dres_inst_tac [("f","Abs_hypnat")] arg_cong 1);
   1.131 +by (res_inst_tac [("x","x")] prem 1);
   1.132 +by (asm_full_simp_tac (simpset() addsimps [Rep_hypnat_inverse]) 1);
   1.133 +qed "eq_Abs_hypnat";
   1.134 +
   1.135 +(*-----------------------------------------------------------
   1.136 +   Addition for hyper naturals: hypnat_add 
   1.137 + -----------------------------------------------------------*)
   1.138 +Goalw [congruent2_def]
   1.139 +    "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n + Y n})";
   1.140 +by (safe_tac (claset()));
   1.141 +by (ALLGOALS(Fuf_tac));
   1.142 +qed "hypnat_add_congruent2";
   1.143 +
   1.144 +Goalw [hypnat_add_def]
   1.145 +  "Abs_hypnat(hypnatrel^^{%n. X n}) + Abs_hypnat(hypnatrel^^{%n. Y n}) = \
   1.146 +\  Abs_hypnat(hypnatrel^^{%n. X n + Y n})";
   1.147 +by (asm_simp_tac
   1.148 +    (simpset() addsimps [[equiv_hypnatrel, hypnat_add_congruent2] 
   1.149 +     MRS UN_equiv_class2]) 1);
   1.150 +qed "hypnat_add";
   1.151 +
   1.152 +Goal "(z::hypnat) + w = w + z";
   1.153 +by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.154 +by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
   1.155 +by (asm_simp_tac (simpset() addsimps (add_ac @ [hypnat_add])) 1);
   1.156 +qed "hypnat_add_commute";
   1.157 +
   1.158 +Goal "((z1::hypnat) + z2) + z3 = z1 + (z2 + z3)";
   1.159 +by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
   1.160 +by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
   1.161 +by (res_inst_tac [("z","z3")] eq_Abs_hypnat 1);
   1.162 +by (asm_simp_tac (simpset() addsimps [hypnat_add,add_assoc]) 1);
   1.163 +qed "hypnat_add_assoc";
   1.164 +
   1.165 +(*For AC rewriting*)
   1.166 +Goal "(x::hypnat)+(y+z)=y+(x+z)";
   1.167 +by (rtac (hypnat_add_commute RS trans) 1);
   1.168 +by (rtac (hypnat_add_assoc RS trans) 1);
   1.169 +by (rtac (hypnat_add_commute RS arg_cong) 1);
   1.170 +qed "hypnat_add_left_commute";
   1.171 +
   1.172 +(* hypnat addition is an AC operator *)
   1.173 +val hypnat_add_ac = [hypnat_add_assoc,hypnat_add_commute,
   1.174 +                      hypnat_add_left_commute];
   1.175 +
   1.176 +Goalw [hypnat_zero_def] "(0::hypnat) + z = z";
   1.177 +by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.178 +by (asm_full_simp_tac (simpset() addsimps 
   1.179 +    [hypnat_add]) 1);
   1.180 +qed "hypnat_add_zero_left";
   1.181 +
   1.182 +Goal "z + (0::hypnat) = z";
   1.183 +by (simp_tac (simpset() addsimps 
   1.184 +    [hypnat_add_zero_left,hypnat_add_commute]) 1);
   1.185 +qed "hypnat_add_zero_right";
   1.186 +
   1.187 +Addsimps [hypnat_add_zero_left,hypnat_add_zero_right];
   1.188 +
   1.189 +(*-----------------------------------------------------------
   1.190 +   Subtraction for hyper naturals: hypnat_minus
   1.191 + -----------------------------------------------------------*)
   1.192 +Goalw [congruent2_def]
   1.193 +    "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n - Y n})";
   1.194 +by (safe_tac (claset()));
   1.195 +by (ALLGOALS(Fuf_tac));
   1.196 +qed "hypnat_minus_congruent2";
   1.197 + 
   1.198 +Goalw [hypnat_minus_def]
   1.199 +  "Abs_hypnat(hypnatrel^^{%n. X n}) - Abs_hypnat(hypnatrel^^{%n. Y n}) = \
   1.200 +\  Abs_hypnat(hypnatrel^^{%n. X n - Y n})";
   1.201 +by (asm_simp_tac
   1.202 +    (simpset() addsimps [[equiv_hypnatrel, hypnat_minus_congruent2] 
   1.203 +     MRS UN_equiv_class2]) 1);
   1.204 +qed "hypnat_minus";
   1.205 +
   1.206 +Goalw [hypnat_zero_def] "z - z = (0::hypnat)";
   1.207 +by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.208 +by (asm_full_simp_tac (simpset() addsimps [hypnat_minus]) 1);
   1.209 +qed "hypnat_minus_zero";
   1.210 +
   1.211 +Goalw [hypnat_zero_def] "(0::hypnat) - n = 0";
   1.212 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.213 +by (asm_full_simp_tac (simpset() addsimps [hypnat_minus]) 1);
   1.214 +qed "hypnat_diff_0_eq_0";
   1.215 +
   1.216 +Addsimps [hypnat_minus_zero,hypnat_diff_0_eq_0];
   1.217 +
   1.218 +Goalw [hypnat_zero_def] "(m+n = (0::hypnat)) = (m=0 & n=0)";
   1.219 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.220 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.221 +by (auto_tac (claset() addIs [FreeUltrafilterNat_subset]
   1.222 +    addDs [FreeUltrafilterNat_Int],
   1.223 +    simpset() addsimps [hypnat_add] ));
   1.224 +qed "hypnat_add_is_0";
   1.225 +
   1.226 +AddIffs [hypnat_add_is_0];
   1.227 +
   1.228 +Goal "!!i::hypnat. i-j-k = i - (j+k)";
   1.229 +by (res_inst_tac [("z","i")] eq_Abs_hypnat 1);
   1.230 +by (res_inst_tac [("z","j")] eq_Abs_hypnat 1);
   1.231 +by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
   1.232 +by (asm_full_simp_tac (simpset() addsimps 
   1.233 +    [hypnat_minus,hypnat_add,diff_diff_left]) 1);
   1.234 +qed "hypnat_diff_diff_left";
   1.235 +
   1.236 +Goal "!!i::hypnat. i-j-k = i-k-j";
   1.237 +by (simp_tac (simpset() addsimps 
   1.238 +    [hypnat_diff_diff_left, hypnat_add_commute]) 1);
   1.239 +qed "hypnat_diff_commute";
   1.240 +
   1.241 +Goal "!!n::hypnat. (n+m) - n = m";
   1.242 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.243 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.244 +by (asm_full_simp_tac (simpset() addsimps 
   1.245 +    [hypnat_minus,hypnat_add]) 1);
   1.246 +qed "hypnat_diff_add_inverse";
   1.247 +Addsimps [hypnat_diff_add_inverse];
   1.248 +
   1.249 +Goal "!!n::hypnat.(m+n) - n = m";
   1.250 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.251 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.252 +by (asm_full_simp_tac (simpset() addsimps 
   1.253 +    [hypnat_minus,hypnat_add]) 1);
   1.254 +qed "hypnat_diff_add_inverse2";
   1.255 +Addsimps [hypnat_diff_add_inverse2];
   1.256 +
   1.257 +Goal "!!k::hypnat. (k+m) - (k+n) = m - n";
   1.258 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.259 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.260 +by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
   1.261 +by (asm_full_simp_tac (simpset() addsimps 
   1.262 +    [hypnat_minus,hypnat_add]) 1);
   1.263 +qed "hypnat_diff_cancel";
   1.264 +Addsimps [hypnat_diff_cancel];
   1.265 +
   1.266 +Goal "!!m::hypnat. (m+k) - (n+k) = m - n";
   1.267 +val hypnat_add_commute_k = read_instantiate [("w","k")] hypnat_add_commute;
   1.268 +by (asm_simp_tac (simpset() addsimps ([hypnat_add_commute_k])) 1);
   1.269 +qed "hypnat_diff_cancel2";
   1.270 +Addsimps [hypnat_diff_cancel2];
   1.271 +
   1.272 +Goalw [hypnat_zero_def] "!!n::hypnat. n - (n+m) = (0::hypnat)";
   1.273 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.274 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.275 +by (asm_full_simp_tac (simpset() addsimps 
   1.276 +    [hypnat_minus,hypnat_add]) 1);
   1.277 +qed "hypnat_diff_add_0";
   1.278 +Addsimps [hypnat_diff_add_0];
   1.279 +
   1.280 +(*-----------------------------------------------------------
   1.281 +   Multiplication for hyper naturals: hypnat_mult
   1.282 + -----------------------------------------------------------*)
   1.283 +Goalw [congruent2_def]
   1.284 +    "congruent2 hypnatrel (%X Y. hypnatrel^^{%n. X n * Y n})";
   1.285 +by (safe_tac (claset()));
   1.286 +by (ALLGOALS(Fuf_tac));
   1.287 +qed "hypnat_mult_congruent2";
   1.288 +
   1.289 +Goalw [hypnat_mult_def]
   1.290 +  "Abs_hypnat(hypnatrel^^{%n. X n}) * Abs_hypnat(hypnatrel^^{%n. Y n}) = \
   1.291 +\  Abs_hypnat(hypnatrel^^{%n. X n * Y n})";
   1.292 +by (asm_simp_tac
   1.293 +    (simpset() addsimps [[equiv_hypnatrel,hypnat_mult_congruent2] MRS
   1.294 +     UN_equiv_class2]) 1);
   1.295 +qed "hypnat_mult";
   1.296 +
   1.297 +Goal "(z::hypnat) * w = w * z";
   1.298 +by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.299 +by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
   1.300 +by (asm_simp_tac (simpset() addsimps ([hypnat_mult] @ mult_ac)) 1);
   1.301 +qed "hypnat_mult_commute";
   1.302 +
   1.303 +Goal "((z1::hypnat) * z2) * z3 = z1 * (z2 * z3)";
   1.304 +by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
   1.305 +by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
   1.306 +by (res_inst_tac [("z","z3")] eq_Abs_hypnat 1);
   1.307 +by (asm_simp_tac (simpset() addsimps [hypnat_mult,mult_assoc]) 1);
   1.308 +qed "hypnat_mult_assoc";
   1.309 +
   1.310 +qed_goal "hypnat_mult_left_commute" thy
   1.311 +    "(z1::hypnat) * (z2 * z3) = z2 * (z1 * z3)"
   1.312 + (fn _ => [rtac (hypnat_mult_commute RS trans) 1, rtac (hypnat_mult_assoc RS trans) 1,
   1.313 +           rtac (hypnat_mult_commute RS arg_cong) 1]);
   1.314 +
   1.315 +(* hypnat multiplication is an AC operator *)
   1.316 +val hypnat_mult_ac = [hypnat_mult_assoc, hypnat_mult_commute, 
   1.317 +                       hypnat_mult_left_commute];
   1.318 +
   1.319 +Goalw [hypnat_one_def] "1hn * z = z";
   1.320 +by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.321 +by (asm_full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
   1.322 +qed "hypnat_mult_1";
   1.323 +Addsimps [hypnat_mult_1];
   1.324 +
   1.325 +Goal "z * 1hn = z";
   1.326 +by (simp_tac (simpset() addsimps [hypnat_mult_commute]) 1);
   1.327 +qed "hypnat_mult_1_right";
   1.328 +Addsimps [hypnat_mult_1_right];
   1.329 +
   1.330 +Goalw [hypnat_zero_def] "(0::hypnat) * z = 0";
   1.331 +by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.332 +by (asm_full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
   1.333 +qed "hypnat_mult_0";
   1.334 +Addsimps [hypnat_mult_0];
   1.335 +
   1.336 +Goal "z * (0::hypnat) = 0";
   1.337 +by (simp_tac (simpset() addsimps [hypnat_mult_commute]) 1);
   1.338 +qed "hypnat_mult_0_right";
   1.339 +Addsimps [hypnat_mult_0_right];
   1.340 +
   1.341 +Goal "!!m::hypnat. (m - n) * k = (m * k) - (n * k)";
   1.342 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.343 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.344 +by (res_inst_tac [("z","k")] eq_Abs_hypnat 1);
   1.345 +by (asm_simp_tac (simpset() addsimps [hypnat_mult,
   1.346 +    hypnat_minus,diff_mult_distrib]) 1);
   1.347 +qed "hypnat_diff_mult_distrib" ;
   1.348 +
   1.349 +Goal "!!m::hypnat. k * (m - n) = (k * m) - (k * n)";
   1.350 +val hypnat_mult_commute_k = read_instantiate [("z","k")] hypnat_mult_commute;
   1.351 +by (simp_tac (simpset() addsimps [hypnat_diff_mult_distrib, 
   1.352 +    hypnat_mult_commute_k]) 1);
   1.353 +qed "hypnat_diff_mult_distrib2" ;
   1.354 +
   1.355 +(*--------------------------
   1.356 +    A Few more theorems
   1.357 + -------------------------*)
   1.358 +qed_goal "hypnat_add_assoc_cong" thy
   1.359 +    "!!z. (z::hypnat) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
   1.360 + (fn _ => [(asm_simp_tac (simpset() addsimps [hypnat_add_assoc RS sym]) 1)]);
   1.361 +
   1.362 +qed_goal "hypnat_add_assoc_swap" thy 
   1.363 +          "(z::hypnat) + (v + w) = v + (z + w)"
   1.364 + (fn _ => [(REPEAT (ares_tac [hypnat_add_commute RS hypnat_add_assoc_cong] 1))]);
   1.365 +
   1.366 +Goal "((z1::hypnat) + z2) * w = (z1 * w) + (z2 * w)";
   1.367 +by (res_inst_tac [("z","z1")] eq_Abs_hypnat 1);
   1.368 +by (res_inst_tac [("z","z2")] eq_Abs_hypnat 1);
   1.369 +by (res_inst_tac [("z","w")] eq_Abs_hypnat 1);
   1.370 +by (asm_simp_tac (simpset() addsimps [hypnat_mult,hypnat_add,
   1.371 +     add_mult_distrib]) 1);
   1.372 +qed "hypnat_add_mult_distrib";
   1.373 +Addsimps [hypnat_add_mult_distrib];
   1.374 +
   1.375 +val hypnat_mult_commute'= read_instantiate [("z","w")] hypnat_mult_commute;
   1.376 +
   1.377 +Goal "(w::hypnat) * (z1 + z2) = (w * z1) + (w * z2)";
   1.378 +by (simp_tac (simpset() addsimps [hypnat_mult_commute']) 1);
   1.379 +qed "hypnat_add_mult_distrib2";
   1.380 +Addsimps [hypnat_add_mult_distrib2];
   1.381 +
   1.382 +(*** (hypnat) one and zero are distinct ***)
   1.383 +Goalw [hypnat_zero_def,hypnat_one_def] "(0::hypnat) ~= 1hn";
   1.384 +by (Auto_tac);
   1.385 +qed "hypnat_zero_not_eq_one";
   1.386 +Addsimps [hypnat_zero_not_eq_one];
   1.387 +Addsimps [hypnat_zero_not_eq_one RS not_sym];
   1.388 +
   1.389 +Goalw [hypnat_zero_def] "(m*n = (0::hypnat)) = (m=0 | n=0)";
   1.390 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.391 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.392 +by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   1.393 +    simpset() addsimps [hypnat_mult]));
   1.394 +by (ALLGOALS(Fuf_tac));
   1.395 +qed "hypnat_mult_is_0";
   1.396 +Addsimps [hypnat_mult_is_0];
   1.397 +
   1.398 +(*------------------------------------------------------------------
   1.399 +                   Theorems for ordering 
   1.400 + ------------------------------------------------------------------*)
   1.401 +
   1.402 +(* prove introduction and elimination rules for hypnat_less *)
   1.403 +
   1.404 +Goalw [hypnat_less_def]
   1.405 + "P < (Q::hypnat) = (EX X Y. X : Rep_hypnat(P) & \
   1.406 +\                             Y : Rep_hypnat(Q) & \
   1.407 +\                             {n. X n < Y n} : FreeUltrafilterNat)";
   1.408 +by (Fast_tac 1);
   1.409 +qed "hypnat_less_iff";
   1.410 +
   1.411 +Goalw [hypnat_less_def]
   1.412 + "!!P. [| {n. X n < Y n} : FreeUltrafilterNat; \
   1.413 +\         X : Rep_hypnat(P); \
   1.414 +\         Y : Rep_hypnat(Q) |] ==> P < (Q::hypnat)";
   1.415 +by (Fast_tac 1);
   1.416 +qed "hypnat_lessI";
   1.417 +
   1.418 +Goalw [hypnat_less_def]
   1.419 +     "!! R1. [| R1 < (R2::hypnat); \
   1.420 +\         !!X Y. {n. X n < Y n} : FreeUltrafilterNat ==> P; \
   1.421 +\         !!X. X : Rep_hypnat(R1) ==> P; \ 
   1.422 +\         !!Y. Y : Rep_hypnat(R2) ==> P |] \
   1.423 +\     ==> P";
   1.424 +by (Auto_tac);
   1.425 +qed "hypnat_lessE";
   1.426 +
   1.427 +Goalw [hypnat_less_def]
   1.428 + "!!R1. R1 < (R2::hypnat) ==> (EX X Y. {n. X n < Y n} : FreeUltrafilterNat & \
   1.429 +\                                  X : Rep_hypnat(R1) & \
   1.430 +\                                  Y : Rep_hypnat(R2))";
   1.431 +by (Fast_tac 1);
   1.432 +qed "hypnat_lessD";
   1.433 +
   1.434 +Goal "~ (R::hypnat) < R";
   1.435 +by (res_inst_tac [("z","R")] eq_Abs_hypnat 1);
   1.436 +by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
   1.437 +by (Fuf_empty_tac 1);
   1.438 +qed "hypnat_less_not_refl";
   1.439 +Addsimps [hypnat_less_not_refl];
   1.440 +
   1.441 +bind_thm("hypnat_less_irrefl",hypnat_less_not_refl RS notE);
   1.442 +
   1.443 +qed_goal "hypnat_not_refl2" thy 
   1.444 +    "!!(x::hypnat). x < y ==> x ~= y" (fn _ => [Auto_tac]);
   1.445 +
   1.446 +Goalw [hypnat_less_def,hypnat_zero_def] "~ n<(0::hypnat)";
   1.447 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.448 +by (Auto_tac);
   1.449 +by (Fuf_empty_tac 1);
   1.450 +qed "hypnat_not_less0";
   1.451 +AddIffs [hypnat_not_less0];
   1.452 +
   1.453 +(* n<(0::hypnat) ==> R *)
   1.454 +bind_thm ("hypnat_less_zeroE", hypnat_not_less0 RS notE);
   1.455 +
   1.456 +Goalw [hypnat_less_def,hypnat_zero_def,hypnat_one_def]
   1.457 +      "(n<1hn) = (n=0)";
   1.458 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.459 +by (auto_tac (claset() addSIs [exI] addEs 
   1.460 +    [FreeUltrafilterNat_subset],simpset()));
   1.461 +by (Fuf_tac 1);
   1.462 +qed "hypnat_less_one";
   1.463 +AddIffs [hypnat_less_one];
   1.464 +
   1.465 +Goal "!!(R1::hypnat). [| R1 < R2; R2 < R3 |] ==> R1 < R3";
   1.466 +by (res_inst_tac [("z","R1")] eq_Abs_hypnat 1);
   1.467 +by (res_inst_tac [("z","R2")] eq_Abs_hypnat 1);
   1.468 +by (res_inst_tac [("z","R3")] eq_Abs_hypnat 1);
   1.469 +by (auto_tac (claset(),simpset() addsimps [hypnat_less_def]));
   1.470 +by (res_inst_tac [("x","X")] exI 1);
   1.471 +by (Auto_tac);
   1.472 +by (res_inst_tac [("x","Ya")] exI 1);
   1.473 +by (Auto_tac);
   1.474 +by (Fuf_tac 1);
   1.475 +qed "hypnat_less_trans";
   1.476 +
   1.477 +Goal "!! (R1::hypnat). [| R1 < R2; R2 < R1 |] ==> P";
   1.478 +by (dtac hypnat_less_trans 1 THEN assume_tac 1);
   1.479 +by (Asm_full_simp_tac 1);
   1.480 +qed "hypnat_less_asym";
   1.481 +
   1.482 +(*----- hypnat less iff less a.e -----*)
   1.483 +(* See comments in HYPER for corresponding thm *)
   1.484 +
   1.485 +Goalw [hypnat_less_def]
   1.486 +      "(Abs_hypnat(hypnatrel^^{%n. X n}) < \
   1.487 +\           Abs_hypnat(hypnatrel^^{%n. Y n})) = \
   1.488 +\      ({n. X n < Y n} : FreeUltrafilterNat)";
   1.489 +by (auto_tac (claset() addSIs [lemma_hypnatrel_refl],simpset()));
   1.490 +by (Fuf_tac 1);
   1.491 +qed "hypnat_less";
   1.492 +
   1.493 +Goal "~ m<n --> n+(m-n) = (m::hypnat)";
   1.494 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.495 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
   1.496 +by (auto_tac (claset(),simpset() addsimps 
   1.497 +    [hypnat_minus,hypnat_add,hypnat_less]));
   1.498 +by (dtac FreeUltrafilterNat_Compl_mem 1);
   1.499 +by (Fuf_tac 1);
   1.500 +qed_spec_mp "hypnat_add_diff_inverse";
   1.501 +
   1.502 +Goal "n<=m ==> n+(m-n) = (m::hypnat)";
   1.503 +by (asm_full_simp_tac (simpset() addsimps 
   1.504 +    [hypnat_add_diff_inverse, hypnat_le_def]) 1);
   1.505 +qed "hypnat_le_add_diff_inverse";
   1.506 +
   1.507 +Goal "n<=m ==> (m-n)+n = (m::hypnat)";
   1.508 +by (asm_simp_tac (simpset() addsimps [hypnat_le_add_diff_inverse, 
   1.509 +    hypnat_add_commute]) 1);
   1.510 +qed "hypnat_le_add_diff_inverse2";
   1.511 +
   1.512 +(*---------------------------------------------------------------------------------
   1.513 +                    Hyper naturals as a linearly ordered field
   1.514 + ---------------------------------------------------------------------------------*)
   1.515 +Goalw [hypnat_zero_def] 
   1.516 +     "[| (0::hypnat) < x; 0 < y |] ==> 0 < x + y";
   1.517 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.518 +by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
   1.519 +by (auto_tac (claset(),simpset() addsimps
   1.520 +   [hypnat_less_def,hypnat_add]));
   1.521 +by (REPEAT(Step_tac 1));
   1.522 +by (Fuf_tac 1);
   1.523 +qed "hypnat_add_order";
   1.524 +
   1.525 +Goalw [hypnat_zero_def] 
   1.526 +      "!!(x::hypnat). [| (0::hypnat) < x; 0 < y |] ==> 0 < x * y";
   1.527 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.528 +by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
   1.529 +by (auto_tac (claset(),simpset() addsimps 
   1.530 +    [hypnat_less_def,hypnat_mult]));
   1.531 +by (REPEAT(Step_tac 1));
   1.532 +by (Fuf_tac 1);
   1.533 +qed "hypnat_mult_order";
   1.534 +
   1.535 +(*---------------------------------------------------------------------------------
   1.536 +                   Trichotomy of the hyper naturals
   1.537 +  --------------------------------------------------------------------------------*)
   1.538 +Goalw [hypnatrel_def] "EX x. x: hypnatrel ^^ {%n. 0}";
   1.539 +by (res_inst_tac [("x","%n. 0")] exI 1);
   1.540 +by (Step_tac 1);
   1.541 +by (Auto_tac);
   1.542 +qed "lemma_hypnatrel_0_mem";
   1.543 +
   1.544 +(* linearity is actually proved further down! *)
   1.545 +Goalw [hypnat_zero_def,
   1.546 +       hypnat_less_def]"(0::hypnat) <  x | x = 0 | x < 0";
   1.547 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.548 +by (Auto_tac );
   1.549 +by (REPEAT(Step_tac 1));
   1.550 +by (REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
   1.551 +by (Fuf_tac 1);
   1.552 +qed "hypnat_trichotomy";
   1.553 +
   1.554 +Goal "!!x. [| (0::hypnat) < x ==> P; \
   1.555 +\                 x = 0 ==> P; \
   1.556 +\                 x < 0 ==> P |] ==> P";
   1.557 +by (cut_inst_tac [("x","x")] hypnat_trichotomy 1);
   1.558 +by (Auto_tac);
   1.559 +qed "hypnat_trichotomyE";
   1.560 +
   1.561 +(*------------------------------------------------------------------------------
   1.562 +            More properties of <
   1.563 + ------------------------------------------------------------------------------*)
   1.564 +Goal "!!(A::hypnat). A < B ==> A + C < B + C";
   1.565 +by (res_inst_tac [("z","A")] eq_Abs_hypnat 1);
   1.566 +by (res_inst_tac [("z","B")] eq_Abs_hypnat 1);
   1.567 +by (res_inst_tac [("z","C")] eq_Abs_hypnat 1);
   1.568 +by (auto_tac (claset(),simpset() addsimps 
   1.569 +    [hypnat_less_def,hypnat_add]));
   1.570 +by (REPEAT(Step_tac 1));
   1.571 +by (Fuf_tac 1);
   1.572 +qed "hypnat_add_less_mono1";
   1.573 +
   1.574 +Goal "!!(A::hypnat). A < B ==> C + A < C + B";
   1.575 +by (auto_tac (claset() addIs [hypnat_add_less_mono1],
   1.576 +    simpset() addsimps [hypnat_add_commute]));
   1.577 +qed "hypnat_add_less_mono2";
   1.578 +
   1.579 +Goal "!!k l::hypnat. [|i<j;  k<l |] ==> i + k < j + l";
   1.580 +by (etac (hypnat_add_less_mono1 RS hypnat_less_trans) 1);
   1.581 +by (simp_tac (simpset() addsimps [hypnat_add_commute]) 1);
   1.582 +(*j moves to the end because it is free while k, l are bound*)
   1.583 +by (etac hypnat_add_less_mono1 1);
   1.584 +qed "hypnat_add_less_mono";
   1.585 +
   1.586 +(*---------------------------------------
   1.587 +        hypnat_minus_less
   1.588 + ---------------------------------------*)
   1.589 +Goalw [hypnat_less_def,hypnat_zero_def] 
   1.590 +      "((x::hypnat) < y) = ((0::hypnat) < y - x)";
   1.591 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.592 +by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
   1.593 +by (auto_tac (claset(),simpset() addsimps 
   1.594 +    [hypnat_minus]));
   1.595 +by (REPEAT(Step_tac 1));
   1.596 +by (REPEAT(Step_tac 2));
   1.597 +by (ALLGOALS(fuf_tac (claset() addDs [sym],simpset())));
   1.598 +
   1.599 +(*** linearity ***)
   1.600 +Goalw [hypnat_less_def] "(x::hypnat) < y | x = y | y < x";
   1.601 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.602 +by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
   1.603 +by (Auto_tac );
   1.604 +by (REPEAT(Step_tac 1));
   1.605 +by (REPEAT(dtac FreeUltrafilterNat_Compl_mem 1));
   1.606 +by (Fuf_tac 1);
   1.607 +qed "hypnat_linear";
   1.608 +
   1.609 +Goal
   1.610 +    "!!(x::hypnat). [| x < y ==> P;  x = y ==> P; \
   1.611 +\          y < x ==> P |] ==> P";
   1.612 +by (cut_inst_tac [("x","x"),("y","y")] hypnat_linear 1);
   1.613 +by (Auto_tac);
   1.614 +qed "hypnat_linear_less2";
   1.615 +
   1.616 +(*------------------------------------------------------------------------------
   1.617 +                            Properties of <=
   1.618 + ------------------------------------------------------------------------------*)
   1.619 +(*------ hypnat le iff nat le a.e ------*)
   1.620 +Goalw [hypnat_le_def,le_def]
   1.621 +      "(Abs_hypnat(hypnatrel^^{%n. X n}) <= \
   1.622 +\           Abs_hypnat(hypnatrel^^{%n. Y n})) = \
   1.623 +\      ({n. X n <= Y n} : FreeUltrafilterNat)";
   1.624 +by (auto_tac (claset() addSDs [FreeUltrafilterNat_Compl_mem],
   1.625 +    simpset() addsimps [hypnat_less]));
   1.626 +by (Fuf_tac 1 THEN Fuf_empty_tac 1);
   1.627 +qed "hypnat_le";
   1.628 +
   1.629 +(*---------------------------------------------------------*)
   1.630 +(*---------------------------------------------------------*)
   1.631 +Goalw [hypnat_le_def] "!!w. ~(w < z) ==> z <= (w::hypnat)";
   1.632 +by (assume_tac 1);
   1.633 +qed "hypnat_leI";
   1.634 +
   1.635 +Goalw [hypnat_le_def] "!!w. z<=w ==> ~(w<(z::hypnat))";
   1.636 +by (assume_tac 1);
   1.637 +qed "hypnat_leD";
   1.638 +
   1.639 +val hypnat_leE = make_elim hypnat_leD;
   1.640 +
   1.641 +Goal "!!w. (~(w < z)) = (z <= (w::hypnat))";
   1.642 +by (fast_tac (claset() addSIs [hypnat_leI,hypnat_leD]) 1);
   1.643 +qed "hypnat_less_le_iff";
   1.644 +
   1.645 +Goalw [hypnat_le_def] "!!z. ~ z <= w ==> w<(z::hypnat)";
   1.646 +by (Fast_tac 1);
   1.647 +qed "not_hypnat_leE";
   1.648 +
   1.649 +Goalw [hypnat_le_def] "!!z. z < w ==> z <= (w::hypnat)";
   1.650 +by (fast_tac (claset() addEs [hypnat_less_asym]) 1);
   1.651 +qed "hypnat_less_imp_le";
   1.652 +
   1.653 +Goalw [hypnat_le_def] "!!(x::hypnat). x <= y ==> x < y | x = y";
   1.654 +by (cut_facts_tac [hypnat_linear] 1);
   1.655 +by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
   1.656 +qed "hypnat_le_imp_less_or_eq";
   1.657 +
   1.658 +Goalw [hypnat_le_def] "!!z. z<w | z=w ==> z <=(w::hypnat)";
   1.659 +by (cut_facts_tac [hypnat_linear] 1);
   1.660 +by (fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym]) 1);
   1.661 +qed "hypnat_less_or_eq_imp_le";
   1.662 +
   1.663 +Goal "(x <= (y::hypnat)) = (x < y | x=y)";
   1.664 +by (REPEAT(ares_tac [iffI, hypnat_less_or_eq_imp_le, hypnat_le_imp_less_or_eq] 1));
   1.665 +qed "hypnat_le_eq_less_or_eq";
   1.666 +
   1.667 +Goal "w <= (w::hypnat)";
   1.668 +by (simp_tac (simpset() addsimps [hypnat_le_eq_less_or_eq]) 1);
   1.669 +qed "hypnat_le_refl";
   1.670 +Addsimps [hypnat_le_refl];
   1.671 +
   1.672 +val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::hypnat)";
   1.673 +by (dtac hypnat_le_imp_less_or_eq 1);
   1.674 +by (fast_tac (claset() addIs [hypnat_less_trans]) 1);
   1.675 +qed "hypnat_le_less_trans";
   1.676 +
   1.677 +Goal "!! (i::hypnat). [| i < j; j <= k |] ==> i < k";
   1.678 +by (dtac hypnat_le_imp_less_or_eq 1);
   1.679 +by (fast_tac (claset() addIs [hypnat_less_trans]) 1);
   1.680 +qed "hypnat_less_le_trans";
   1.681 +
   1.682 +Goal "!!i. [| i <= j; j <= k |] ==> i <= (k::hypnat)";
   1.683 +by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
   1.684 +            rtac hypnat_less_or_eq_imp_le, fast_tac (claset() addIs [hypnat_less_trans])]);
   1.685 +qed "hypnat_le_trans";
   1.686 +
   1.687 +Goal "!!z. [| z <= w; w <= z |] ==> z = (w::hypnat)";
   1.688 +by (EVERY1 [dtac hypnat_le_imp_less_or_eq, dtac hypnat_le_imp_less_or_eq,
   1.689 +            fast_tac (claset() addEs [hypnat_less_irrefl,hypnat_less_asym])]);
   1.690 +qed "hypnat_le_anti_sym";
   1.691 +
   1.692 +Goal "!!x. [| ~ y < x; y ~= x |] ==> x < (y::hypnat)";
   1.693 +by (rtac not_hypnat_leE 1);
   1.694 +by (fast_tac (claset() addDs [hypnat_le_imp_less_or_eq]) 1);
   1.695 +qed "not_less_not_eq_hypnat_less";
   1.696 +
   1.697 +Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x * y";
   1.698 +by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
   1.699 +by (auto_tac (claset() addIs [hypnat_mult_order,
   1.700 +    hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
   1.701 +qed "hypnat_le_mult_order";
   1.702 +
   1.703 +Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] 
   1.704 +      "(0::hypnat) < 1hn";
   1.705 +by (res_inst_tac [("x","%n. 0")] exI 1);
   1.706 +by (res_inst_tac [("x","%n. 1")] exI 1);
   1.707 +by (Auto_tac);
   1.708 +qed "hypnat_zero_less_one";
   1.709 +
   1.710 +Goal "!!x. [| (0::hypnat) <= x; 0 <= y |] ==> 0 <= x + y";
   1.711 +by (REPEAT(dtac hypnat_le_imp_less_or_eq 1));
   1.712 +by (auto_tac (claset() addIs [hypnat_add_order,
   1.713 +    hypnat_less_imp_le],simpset() addsimps [hypnat_le_refl]));
   1.714 +qed "hypnat_le_add_order";
   1.715 +
   1.716 +Goal "!!(q1::hypnat). q1 <= q2  ==> x + q1 <= x + q2";
   1.717 +by (dtac hypnat_le_imp_less_or_eq 1);
   1.718 +by (Step_tac 1);
   1.719 +by (auto_tac (claset() addSIs [hypnat_le_refl,
   1.720 +    hypnat_less_imp_le,hypnat_add_less_mono1],
   1.721 +    simpset() addsimps [hypnat_add_commute]));
   1.722 +qed "hypnat_add_le_mono2";
   1.723 +
   1.724 +Goal "!!(q1::hypnat). q1 <= q2  ==> q1 + x <= q2 + x";
   1.725 +by (auto_tac (claset() addDs [hypnat_add_le_mono2],
   1.726 +    simpset() addsimps [hypnat_add_commute]));
   1.727 +qed "hypnat_add_le_mono1";
   1.728 +
   1.729 +Goal "!!k l::hypnat. [|i<=j;  k<=l |] ==> i + k <= j + l";
   1.730 +by (etac (hypnat_add_le_mono1 RS hypnat_le_trans) 1);
   1.731 +by (simp_tac (simpset() addsimps [hypnat_add_commute]) 1);
   1.732 +(*j moves to the end because it is free while k, l are bound*)
   1.733 +by (etac hypnat_add_le_mono1 1);
   1.734 +qed "hypnat_add_le_mono";
   1.735 +
   1.736 +Goalw [hypnat_zero_def]
   1.737 +     "!!x::hypnat. [| (0::hypnat) < z; x < y |] ==> x * z < y * z";
   1.738 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
   1.739 +by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
   1.740 +by (res_inst_tac [("z","z")] eq_Abs_hypnat 1);
   1.741 +by (auto_tac (claset(),simpset() addsimps 
   1.742 +    [hypnat_less,hypnat_mult]));
   1.743 +by (Fuf_tac 1);
   1.744 +qed "hypnat_mult_less_mono1";
   1.745 +
   1.746 +Goal "!!x::hypnat. [| 0 < z; x < y |] ==> z * x < z * y";
   1.747 +by (auto_tac (claset() addIs [hypnat_mult_less_mono1],
   1.748 +              simpset() addsimps [hypnat_mult_commute]));
   1.749 +qed "hypnat_mult_less_mono2";
   1.750 +
   1.751 +Addsimps [hypnat_mult_less_mono2,hypnat_mult_less_mono1];
   1.752 +
   1.753 +Goal "(x::hypnat) <= n + x";
   1.754 +by (res_inst_tac [("x","n")] hypnat_trichotomyE 1);
   1.755 +by (auto_tac (claset() addDs [(hypnat_less_imp_le RS
   1.756 +    hypnat_add_le_mono1)],simpset() addsimps [hypnat_le_refl]));
   1.757 +qed "hypnat_add_self_le";
   1.758 +Addsimps [hypnat_add_self_le];
   1.759 +
   1.760 +Goal "(x::hypnat) < x + 1hn";
   1.761 +by (cut_facts_tac [hypnat_zero_less_one 
   1.762 +         RS hypnat_add_less_mono2] 1);
   1.763 +by (Auto_tac);
   1.764 +qed "hypnat_add_one_self_less";
   1.765 +Addsimps [hypnat_add_one_self_less];
   1.766 +
   1.767 +Goalw [hypnat_le_def] "~ x + 1hn <= x";
   1.768 +by (Simp_tac 1);
   1.769 +qed "not_hypnat_add_one_le_self";
   1.770 +Addsimps [not_hypnat_add_one_le_self];
   1.771 +
   1.772 +Goal "((0::hypnat) < n) = (1hn <= n)";
   1.773 +by (res_inst_tac [("x","n")] hypnat_trichotomyE 1);
   1.774 +by (auto_tac (claset(),simpset() addsimps [hypnat_le_def]));
   1.775 +qed "hypnat_gt_zero_iff";
   1.776 +
   1.777 +Addsimps  [hypnat_le_add_diff_inverse, hypnat_le_add_diff_inverse2,
   1.778 +           hypnat_less_imp_le RS hypnat_le_add_diff_inverse2];
   1.779 +
   1.780 +Goal "(0 < n) = (EX m. n = m + 1hn)";
   1.781 +by (Step_tac 1);
   1.782 +by (res_inst_tac [("x","m")] hypnat_trichotomyE 2);
   1.783 +by (rtac hypnat_less_trans 2);
   1.784 +by (res_inst_tac [("x","n - 1hn")] exI 1);
   1.785 +by (auto_tac (claset(),simpset() addsimps 
   1.786 +    [hypnat_gt_zero_iff,hypnat_add_commute]));
   1.787 +qed "hypnat_gt_zero_iff2";
   1.788 +
   1.789 +Goalw [hypnat_zero_def] "(0::hypnat) <= n";
   1.790 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
   1.791 +by (asm_simp_tac (simpset() addsimps [hypnat_le]) 1);
   1.792 +qed "hypnat_le_zero";
   1.793 +Addsimps [hypnat_le_zero];
   1.794 +
   1.795 +(*------------------------------------------------------------------
   1.796 +     hypnat_of_nat: properties embedding of naturals in hypernaturals
   1.797 + -----------------------------------------------------------------*)
   1.798 +    (** hypnat_of_nat preserves field and order properties **)
   1.799 +
   1.800 +Goalw [hypnat_of_nat_def] 
   1.801 +      "hypnat_of_nat ((z1::nat) + z2) = \
   1.802 +\      hypnat_of_nat z1 + hypnat_of_nat z2";
   1.803 +by (asm_simp_tac (simpset() addsimps [hypnat_add]) 1);
   1.804 +qed "hypnat_of_nat_add";
   1.805 +
   1.806 +Goalw [hypnat_of_nat_def] 
   1.807 +      "hypnat_of_nat ((z1::nat) - z2) = \
   1.808 +\      hypnat_of_nat z1 - hypnat_of_nat z2";
   1.809 +by (asm_simp_tac (simpset() addsimps [hypnat_minus]) 1);
   1.810 +qed "hypnat_of_nat_minus";
   1.811 +
   1.812 +Goalw [hypnat_of_nat_def] 
   1.813 +      "hypnat_of_nat (z1 * z2) = hypnat_of_nat z1 * hypnat_of_nat z2";
   1.814 +by (full_simp_tac (simpset() addsimps [hypnat_mult]) 1);
   1.815 +qed "hypnat_of_nat_mult";
   1.816 +
   1.817 +Goalw [hypnat_less_def,hypnat_of_nat_def] 
   1.818 +      "(z1 < z2) = (hypnat_of_nat z1 < hypnat_of_nat z2)";
   1.819 +by (auto_tac (claset() addSIs [exI] addIs 
   1.820 +   [FreeUltrafilterNat_all],simpset()));
   1.821 +by (rtac FreeUltrafilterNat_P 1 THEN Fuf_tac 1);
   1.822 +qed "hypnat_of_nat_less_iff";
   1.823 +Addsimps [hypnat_of_nat_less_iff RS sym];
   1.824 +
   1.825 +Goalw [hypnat_le_def,le_def] 
   1.826 +      "(z1 <= z2) = (hypnat_of_nat z1 <= hypnat_of_nat z2)";
   1.827 +by (Auto_tac);
   1.828 +qed "hypnat_of_nat_le_iff";
   1.829 +
   1.830 +Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat  1 = 1hn";
   1.831 +by (Simp_tac 1);
   1.832 +qed "hypnat_of_nat_one";
   1.833 +
   1.834 +Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat  0 = 0";
   1.835 +by (Simp_tac 1);
   1.836 +qed "hypnat_of_nat_zero";
   1.837 +
   1.838 +Goal "(hypnat_of_nat  n = 0) = (n = 0)";
   1.839 +by (auto_tac (claset() addIs [FreeUltrafilterNat_P],
   1.840 +    simpset() addsimps [hypnat_of_nat_def,
   1.841 +    hypnat_zero_def]));
   1.842 +qed "hypnat_of_nat_zero_iff";
   1.843 +
   1.844 +Goal "(hypnat_of_nat  n ~= 0) = (n ~= 0)";
   1.845 +by (full_simp_tac (simpset() addsimps [hypnat_of_nat_zero_iff]) 1);
   1.846 +qed "hypnat_of_nat_not_zero_iff";
   1.847 +
   1.848 +goalw HyperNat.thy [hypnat_of_nat_def,hypnat_one_def]
   1.849 +      "hypnat_of_nat (Suc n) = hypnat_of_nat n + 1hn";
   1.850 +by (auto_tac (claset(),simpset() addsimps [hypnat_add]));
   1.851 +qed "hypnat_of_nat_Suc";
   1.852 +
   1.853 +(*---------------------------------------------------------------------------------
   1.854 +              Existence of infinite hypernatural number
   1.855 + ---------------------------------------------------------------------------------*)
   1.856 +
   1.857 +Goal "hypnatrel^^{%n::nat. n} : hypnat";
   1.858 +by (Auto_tac);
   1.859 +qed "hypnat_omega";
   1.860 +
   1.861 +Goalw [hypnat_omega_def] "Rep_hypnat(whn) : hypnat";
   1.862 +by (rtac Rep_hypnat 1);
   1.863 +qed "Rep_hypnat_omega";
   1.864 +
   1.865 +(* See Hyper.thy for similar argument*)
   1.866 +(* existence of infinite number not corresponding to any natural number *)
   1.867 +(* use assumption that member FreeUltrafilterNat is not finite       *)
   1.868 +(* a few lemmas first *)
   1.869 +
   1.870 +Goalw [hypnat_omega_def,hypnat_of_nat_def]
   1.871 +      "~ (EX x. hypnat_of_nat x = whn)";
   1.872 +by (auto_tac (claset() addDs [FreeUltrafilterNat_not_finite], 
   1.873 +              simpset()));
   1.874 +qed "not_ex_hypnat_of_nat_eq_omega";
   1.875 +
   1.876 +Goal "hypnat_of_nat x ~= whn";
   1.877 +by (cut_facts_tac [not_ex_hypnat_of_nat_eq_omega] 1);
   1.878 +by (Auto_tac);
   1.879 +qed "hypnat_of_nat_not_eq_omega";
   1.880 +Addsimps [hypnat_of_nat_not_eq_omega RS not_sym];
   1.881 +
   1.882 +(*-----------------------------------------------------------
   1.883 +    Properties of the set SHNat of embedded natural numbers
   1.884 +              (cf. set SReal in NSA.thy/NSA.ML)
   1.885 + ----------------------------------------------------------*)
   1.886 +
   1.887 +(* Infinite hypernatural not in embedded SHNat *)
   1.888 +Goalw [SHNat_def] "whn ~: SHNat";
   1.889 +by (Auto_tac);
   1.890 +qed "SHNAT_omega_not_mem";
   1.891 +Addsimps [SHNAT_omega_not_mem];
   1.892 +
   1.893 +(*-----------------------------------------------------------------------
   1.894 +     Closure laws for members of (embedded) set standard naturals SHNat
   1.895 + -----------------------------------------------------------------------*)
   1.896 +Goalw [SHNat_def] 
   1.897 +      "!!x. [| x: SHNat; y: SHNat |] ==> x + y: SHNat";
   1.898 +by (Step_tac 1);
   1.899 +by (res_inst_tac [("x","N + Na")] exI 1);
   1.900 +by (simp_tac (simpset() addsimps [hypnat_of_nat_add]) 1);
   1.901 +qed "SHNat_add";
   1.902 +
   1.903 +Goalw [SHNat_def] 
   1.904 +      "!!x. [| x: SHNat; y: SHNat |] ==> x - y: SHNat";
   1.905 +by (Step_tac 1);
   1.906 +by (res_inst_tac [("x","N - Na")] exI 1);
   1.907 +by (simp_tac (simpset() addsimps [hypnat_of_nat_minus]) 1);
   1.908 +qed "SHNat_minus";
   1.909 +
   1.910 +Goalw [SHNat_def] 
   1.911 +      "!!x. [| x: SHNat; y: SHNat |] ==> x * y: SHNat";
   1.912 +by (Step_tac 1);
   1.913 +by (res_inst_tac [("x","N * Na")] exI 1);
   1.914 +by (simp_tac (simpset() addsimps [hypnat_of_nat_mult]) 1);
   1.915 +qed "SHNat_mult";
   1.916 +
   1.917 +Goal "!!x. [| x + y : SHNat; y: SHNat |] ==> x: SHNat";
   1.918 +by (dres_inst_tac [("x","x+y")] SHNat_minus 1);
   1.919 +by (Auto_tac);
   1.920 +qed "SHNat_add_cancel";
   1.921 +
   1.922 +Goalw [SHNat_def] "hypnat_of_nat x : SHNat";
   1.923 +by (Blast_tac 1);
   1.924 +qed "SHNat_hypnat_of_nat";
   1.925 +Addsimps [SHNat_hypnat_of_nat];
   1.926 +
   1.927 +Goal "hypnat_of_nat 1 : SHNat";
   1.928 +by (Simp_tac 1);
   1.929 +qed "SHNat_hypnat_of_nat_one";
   1.930 +
   1.931 +Goal "hypnat_of_nat 0 : SHNat";
   1.932 +by (Simp_tac 1);
   1.933 +qed "SHNat_hypnat_of_nat_zero";
   1.934 +
   1.935 +Goal "1hn : SHNat";
   1.936 +by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_one,
   1.937 +    hypnat_of_nat_one RS sym]) 1);
   1.938 +qed "SHNat_one";
   1.939 +
   1.940 +Goal "0 : SHNat";
   1.941 +by (simp_tac (simpset() addsimps [SHNat_hypnat_of_nat_zero,
   1.942 +    hypnat_of_nat_zero RS sym]) 1);
   1.943 +qed "SHNat_zero";
   1.944 +
   1.945 +Addsimps [SHNat_hypnat_of_nat_one,SHNat_hypnat_of_nat_zero,
   1.946 +          SHNat_one,SHNat_zero];
   1.947 +
   1.948 +Goal "1hn + 1hn : SHNat";
   1.949 +by (rtac ([SHNat_one,SHNat_one] MRS SHNat_add) 1);
   1.950 +qed "SHNat_two";
   1.951 +
   1.952 +Goalw [SHNat_def] "{x. hypnat_of_nat x : SHNat} = (UNIV::nat set)";
   1.953 +by (Auto_tac);
   1.954 +qed "SHNat_UNIV_nat";
   1.955 +
   1.956 +Goalw [SHNat_def] "(x: SHNat) = (EX y. x = hypnat_of_nat  y)";
   1.957 +by (Auto_tac);
   1.958 +qed "SHNat_iff";
   1.959 +
   1.960 +Goalw [SHNat_def] "hypnat_of_nat ``(UNIV::nat set) = SHNat";
   1.961 +by (Auto_tac);
   1.962 +qed "hypnat_of_nat_image";
   1.963 +
   1.964 +Goalw [SHNat_def] "inv hypnat_of_nat ``SHNat = (UNIV::nat set)";
   1.965 +by (Auto_tac);
   1.966 +by (rtac (inj_hypnat_of_nat RS inv_f_f RS subst) 1);
   1.967 +by (Blast_tac 1);
   1.968 +qed "inv_hypnat_of_nat_image";
   1.969 +
   1.970 +Goalw [SHNat_def] 
   1.971 +      "!!P. [| EX x. x: P; P <= SHNat |] ==> \
   1.972 +\           EX Q. P = hypnat_of_nat `` Q";
   1.973 +by (Best_tac 1); 
   1.974 +qed "SHNat_hypnat_of_nat_image";
   1.975 +
   1.976 +Goalw [SHNat_def] 
   1.977 +      "SHNat = hypnat_of_nat `` (UNIV::nat set)";
   1.978 +by (Auto_tac);
   1.979 +qed "SHNat_hypnat_of_nat_iff";
   1.980 +
   1.981 +Goalw [SHNat_def] "SHNat <= (UNIV::hypnat set)";
   1.982 +by (Auto_tac);
   1.983 +qed "SHNat_subset_UNIV";
   1.984 +
   1.985 +Goal "{n. n <= Suc m} = {n. n <= m} Un {n. n = Suc m}";
   1.986 +by (auto_tac (claset(),simpset() addsimps [le_Suc_eq]));
   1.987 +qed "leSuc_Un_eq";
   1.988 +
   1.989 +Goal "finite {n::nat. n <= m}";
   1.990 +by (nat_ind_tac "m" 1);
   1.991 +by (auto_tac (claset(),simpset() addsimps [leSuc_Un_eq]));
   1.992 +qed "finite_nat_le_segment";
   1.993 +
   1.994 +Goal "{n::nat. m < n} : FreeUltrafilterNat";
   1.995 +by (cut_inst_tac [("m2","m")] (finite_nat_le_segment RS 
   1.996 +    FreeUltrafilterNat_finite RS FreeUltrafilterNat_Compl_mem) 1);
   1.997 +by (Fuf_tac 1);
   1.998 +qed "lemma_unbounded_set";
   1.999 +Addsimps [lemma_unbounded_set];
  1.1000 +
  1.1001 +Goalw [SHNat_def,hypnat_of_nat_def,
  1.1002 +           hypnat_less_def,hypnat_omega_def] 
  1.1003 +           "ALL n: SHNat. n < whn";
  1.1004 +by (Clarify_tac 1);
  1.1005 +by (auto_tac (claset() addSIs [exI],simpset()));
  1.1006 +qed "hypnat_omega_gt_SHNat";
  1.1007 +
  1.1008 +Goal "hypnat_of_nat n < whn";
  1.1009 +by (cut_facts_tac [hypnat_omega_gt_SHNat] 1);
  1.1010 +by (dres_inst_tac [("x","hypnat_of_nat n")] bspec 1);
  1.1011 +by (Auto_tac);
  1.1012 +qed "hypnat_of_nat_less_whn";
  1.1013 +Addsimps [hypnat_of_nat_less_whn];
  1.1014 +
  1.1015 +Goal "hypnat_of_nat n <= whn";
  1.1016 +by (rtac (hypnat_of_nat_less_whn RS hypnat_less_imp_le) 1);
  1.1017 +qed "hypnat_of_nat_le_whn";
  1.1018 +Addsimps [hypnat_of_nat_le_whn];
  1.1019 +
  1.1020 +Goal "0 < whn";
  1.1021 +by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
  1.1022 +by (Auto_tac);
  1.1023 +qed "hypnat_zero_less_hypnat_omega";
  1.1024 +Addsimps [hypnat_zero_less_hypnat_omega];
  1.1025 +
  1.1026 +Goal "1hn < whn";
  1.1027 +by (rtac (hypnat_omega_gt_SHNat RS ballE) 1);
  1.1028 +by (Auto_tac);
  1.1029 +qed "hypnat_one_less_hypnat_omega";
  1.1030 +Addsimps [hypnat_one_less_hypnat_omega];
  1.1031 +
  1.1032 +(*--------------------------------------------------------------------------
  1.1033 +     Theorems about infinite hypernatural numbers -- HNatInfinite
  1.1034 + -------------------------------------------------------------------------*)
  1.1035 +Goalw [HNatInfinite_def,SHNat_def] "whn : HNatInfinite";
  1.1036 +by (Auto_tac);
  1.1037 +qed "HNatInfinite_whn";
  1.1038 +Addsimps [HNatInfinite_whn];
  1.1039 +
  1.1040 +Goalw [HNatInfinite_def] "!!x. x: SHNat ==> x ~: HNatInfinite";
  1.1041 +by (Simp_tac 1);
  1.1042 +qed "SHNat_not_HNatInfinite";
  1.1043 +
  1.1044 +Goalw [HNatInfinite_def] "!!x. x ~: HNatInfinite ==> x: SHNat";
  1.1045 +by (Asm_full_simp_tac 1);
  1.1046 +qed "not_HNatInfinite_SHNat";
  1.1047 +
  1.1048 +Goalw [HNatInfinite_def] "!!x. x ~: SHNat ==> x: HNatInfinite";
  1.1049 +by (Simp_tac 1);
  1.1050 +qed "not_SHNat_HNatInfinite";
  1.1051 +
  1.1052 +Goalw [HNatInfinite_def] "!!x. x: HNatInfinite ==> x ~: SHNat";
  1.1053 +by (Asm_full_simp_tac 1);
  1.1054 +qed "HNatInfinite_not_SHNat";
  1.1055 +
  1.1056 +Goal "(x: SHNat) = (x ~: HNatInfinite)";
  1.1057 +by (blast_tac (claset() addSIs [SHNat_not_HNatInfinite,
  1.1058 +    not_HNatInfinite_SHNat]) 1);
  1.1059 +qed "SHNat_not_HNatInfinite_iff";
  1.1060 +
  1.1061 +Goal "(x ~: SHNat) = (x: HNatInfinite)";
  1.1062 +by (blast_tac (claset() addSIs [not_SHNat_HNatInfinite,
  1.1063 +    HNatInfinite_not_SHNat]) 1);
  1.1064 +qed "not_SHNat_HNatInfinite_iff";
  1.1065 +
  1.1066 +Goal "x : SHNat | x : HNatInfinite";
  1.1067 +by (simp_tac (simpset() addsimps [SHNat_not_HNatInfinite_iff]) 1);
  1.1068 +qed "SHNat_HNatInfinite_disj";
  1.1069 +
  1.1070 +(*-------------------------------------------------------------------
  1.1071 +   Proof of alternative definition for set of Infinite hypernatural 
  1.1072 +   numbers --- HNatInfinite = {N. ALL n: SHNat. n < N}
  1.1073 + -------------------------------------------------------------------*)
  1.1074 +Goal "!!N (xa::nat=>nat). \
  1.1075 +\         (ALL N. {n. xa n ~= N} : FreeUltrafilterNat) ==> \
  1.1076 +\         ({n. N < xa n} : FreeUltrafilterNat)";
  1.1077 +by (nat_ind_tac "N" 1);
  1.1078 +by (dres_inst_tac [("x","0")] spec 1);
  1.1079 +by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1
  1.1080 +    THEN dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1);
  1.1081 +by (Asm_full_simp_tac 1);
  1.1082 +by (dres_inst_tac [("x","Suc N")] spec 1);
  1.1083 +by (fuf_tac (claset() addSDs [Suc_leI],simpset() addsimps 
  1.1084 +    [le_eq_less_or_eq]) 1);
  1.1085 +qed "HNatInfinite_FreeUltrafilterNat_lemma";
  1.1086 +
  1.1087 +(*** alternative definition ***)
  1.1088 +Goalw [HNatInfinite_def,SHNat_def,hypnat_of_nat_def] 
  1.1089 +      "HNatInfinite = {N. ALL n:SHNat. n < N}";
  1.1090 +by (Step_tac 1);
  1.1091 +by (dres_inst_tac [("x","Abs_hypnat \
  1.1092 +\        (hypnatrel ^^ {%n. N})")] bspec 2);
  1.1093 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  1.1094 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  1.1095 +by (auto_tac (claset(),simpset() addsimps [hypnat_less_iff]));
  1.1096 +by (auto_tac (claset() addSIs [exI] addEs 
  1.1097 +    [HNatInfinite_FreeUltrafilterNat_lemma],
  1.1098 +    simpset() addsimps [FreeUltrafilterNat_Compl_iff1, 
  1.1099 +     CLAIM "- {n. xa n = N} = {n. xa n ~= N}"]));
  1.1100 +qed "HNatInfinite_iff";
  1.1101 +
  1.1102 +(*--------------------------------------------------------------------
  1.1103 +   Alternative definition for HNatInfinite using Free ultrafilter
  1.1104 + --------------------------------------------------------------------*)
  1.1105 +Goal "!!x. x : HNatInfinite ==> EX X: Rep_hypnat x. \
  1.1106 +\          ALL u. {n. u < X n}:  FreeUltrafilterNat";
  1.1107 +by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
  1.1108 +    HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
  1.1109 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  1.1110 +by (EVERY[Auto_tac, rtac bexI 1, 
  1.1111 +    rtac lemma_hypnatrel_refl 2, Step_tac 1]);
  1.1112 +by (dres_inst_tac [("x","hypnat_of_nat u")] bspec 1);
  1.1113 +by (Simp_tac 1);
  1.1114 +by (auto_tac (claset(),
  1.1115 +    simpset() addsimps [hypnat_of_nat_def]));
  1.1116 +by (Fuf_tac 1);
  1.1117 +qed "HNatInfinite_FreeUltrafilterNat";
  1.1118 +
  1.1119 +Goal "!!x. EX X: Rep_hypnat x. \
  1.1120 +\          ALL u. {n. u < X n}:  FreeUltrafilterNat \
  1.1121 +\          ==> x: HNatInfinite";
  1.1122 +by (auto_tac (claset(),simpset() addsimps [hypnat_less_def,
  1.1123 +    HNatInfinite_iff,SHNat_iff,hypnat_of_nat_def]));
  1.1124 +by (rtac exI 1 THEN Auto_tac);
  1.1125 +qed "FreeUltrafilterNat_HNatInfinite";
  1.1126 +
  1.1127 +Goal "!!x. (x : HNatInfinite) = (EX X: Rep_hypnat x. \
  1.1128 +\          ALL u. {n. u < X n}:  FreeUltrafilterNat)";
  1.1129 +by (blast_tac (claset() addIs [HNatInfinite_FreeUltrafilterNat,
  1.1130 +    FreeUltrafilterNat_HNatInfinite]) 1);
  1.1131 +qed "HNatInfinite_FreeUltrafilterNat_iff";
  1.1132 +
  1.1133 +Goal "!!x. x : HNatInfinite ==> 1hn < x";
  1.1134 +by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
  1.1135 +qed "HNatInfinite_gt_one";
  1.1136 +Addsimps [HNatInfinite_gt_one];
  1.1137 +
  1.1138 +Goal "!!x. 0 ~: HNatInfinite";
  1.1139 +by (auto_tac (claset(),simpset() 
  1.1140 +    addsimps [HNatInfinite_iff]));
  1.1141 +by (dres_inst_tac [("a","1hn")] equals0D 1);
  1.1142 +by (Asm_full_simp_tac 1);
  1.1143 +qed "zero_not_mem_HNatInfinite";
  1.1144 +Addsimps [zero_not_mem_HNatInfinite];
  1.1145 +
  1.1146 +Goal "!!x. x : HNatInfinite ==> x ~= 0";
  1.1147 +by (Auto_tac);
  1.1148 +qed "HNatInfinite_not_eq_zero";
  1.1149 +
  1.1150 +Goal "!!x. x : HNatInfinite ==> 1hn <= x";
  1.1151 +by (blast_tac (claset() addIs [hypnat_less_imp_le,
  1.1152 +         HNatInfinite_gt_one]) 1);
  1.1153 +qed "HNatInfinite_ge_one";
  1.1154 +Addsimps [HNatInfinite_ge_one];
  1.1155 +
  1.1156 +(*--------------------------------------------------
  1.1157 +                   Closure Rules
  1.1158 + --------------------------------------------------*)
  1.1159 +Goal "!!x. [| x: HNatInfinite; y: HNatInfinite |] \
  1.1160 +\           ==> x + y: HNatInfinite";
  1.1161 +by (auto_tac (claset(),simpset() addsimps [HNatInfinite_iff]));
  1.1162 +by (dtac bspec 1 THEN assume_tac 1);
  1.1163 +by (dtac (SHNat_zero RSN (2,bspec)) 1);
  1.1164 +by (dtac hypnat_add_less_mono 1 THEN assume_tac 1);
  1.1165 +by (Asm_full_simp_tac 1);
  1.1166 +qed "HNatInfinite_add";
  1.1167 +
  1.1168 +Goal "!!x. [| x: HNatInfinite; y: SHNat |] \
  1.1169 +\                       ==> x + y: HNatInfinite";
  1.1170 +by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
  1.1171 +by (dres_inst_tac [("x","x + y")] SHNat_minus 1);
  1.1172 +by (auto_tac (claset(),simpset() addsimps 
  1.1173 +    [SHNat_not_HNatInfinite_iff]));
  1.1174 +qed "HNatInfinite_SHNat_add";
  1.1175 +
  1.1176 +goal HyperNat.thy "!!x. [| x: HNatInfinite; y: SHNat |] \
  1.1177 +\                       ==> x - y: HNatInfinite";
  1.1178 +by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
  1.1179 +by (dres_inst_tac [("x","x - y")] SHNat_add 1);
  1.1180 +by (subgoal_tac "y <= x" 2);
  1.1181 +by (auto_tac (claset() addSDs [hypnat_le_add_diff_inverse2],
  1.1182 +    simpset() addsimps [not_SHNat_HNatInfinite_iff RS sym]));
  1.1183 +by (auto_tac (claset() addSIs [hypnat_less_imp_le],
  1.1184 +    simpset() addsimps [not_SHNat_HNatInfinite_iff,HNatInfinite_iff]));
  1.1185 +qed "HNatInfinite_SHNat_diff";
  1.1186 +
  1.1187 +Goal 
  1.1188 +     "!!x. x: HNatInfinite ==> x + 1hn: HNatInfinite";
  1.1189 +by (auto_tac (claset() addIs [HNatInfinite_SHNat_add],
  1.1190 +              simpset()));
  1.1191 +qed "HNatInfinite_add_one";
  1.1192 +
  1.1193 +Goal 
  1.1194 +     "!!x. x: HNatInfinite ==> x - 1hn: HNatInfinite";
  1.1195 +by (rtac ccontr 1 THEN dtac not_HNatInfinite_SHNat 1);
  1.1196 +by (dres_inst_tac [("x","x - 1hn"),("y","1hn")] SHNat_add 1);
  1.1197 +by (auto_tac (claset(),simpset() addsimps 
  1.1198 +    [not_SHNat_HNatInfinite_iff RS sym]));
  1.1199 +qed "HNatInfinite_minus_one";
  1.1200 +
  1.1201 +Goal "!!x. x : HNatInfinite ==> EX y. x = y + 1hn";
  1.1202 +by (res_inst_tac [("x","x - 1hn")] exI 1);
  1.1203 +by (Auto_tac);
  1.1204 +qed "HNatInfinite_is_Suc";
  1.1205 +
  1.1206 +(*---------------------------------------------------------------
  1.1207 +       HNat : the hypernaturals embedded in the hyperreals
  1.1208 +       Obtained using the NS extension of the naturals
  1.1209 + --------------------------------------------------------------*)
  1.1210 + 
  1.1211 +Goalw [HNat_def,starset_def,
  1.1212 +         hypreal_of_posnat_def,hypreal_of_real_def] 
  1.1213 +         "hypreal_of_posnat N : HNat";
  1.1214 +by (Auto_tac);
  1.1215 +by (Ultra_tac 1);
  1.1216 +by (res_inst_tac [("x","Suc N")] exI 1);
  1.1217 +by (dtac sym 1 THEN auto_tac (claset(),simpset() 
  1.1218 +    addsimps [real_of_preal_real_of_nat_Suc]));
  1.1219 +qed "HNat_hypreal_of_posnat";
  1.1220 +Addsimps [HNat_hypreal_of_posnat];
  1.1221 +
  1.1222 +Goalw [HNat_def,starset_def]
  1.1223 +     "[| x: HNat; y: HNat |] ==> x + y: HNat";
  1.1224 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1.1225 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1.1226 +by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
  1.1227 +    simpset() addsimps [hypreal_add]));
  1.1228 +by (Ultra_tac 1);
  1.1229 +by (dres_inst_tac [("t","Y xb")] sym 1);
  1.1230 +by (auto_tac (claset(),simpset() addsimps [real_of_nat_add RS sym]));
  1.1231 +qed "HNat_add";
  1.1232 +
  1.1233 +Goalw [HNat_def,starset_def]
  1.1234 +     "[| x: HNat; y: HNat |] ==> x * y: HNat";
  1.1235 +by (res_inst_tac [("z","x")] eq_Abs_hypreal 1);
  1.1236 +by (res_inst_tac [("z","y")] eq_Abs_hypreal 1);
  1.1237 +by (auto_tac (claset() addSDs [bspec] addIs [lemma_hyprel_refl],
  1.1238 +    simpset() addsimps [hypreal_mult]));
  1.1239 +by (Ultra_tac 1);
  1.1240 +by (dres_inst_tac [("t","Y xb")] sym 1);
  1.1241 +by (auto_tac (claset(),simpset() addsimps [real_of_nat_mult RS sym]));
  1.1242 +qed "HNat_mult";
  1.1243 +
  1.1244 +(*---------------------------------------------------------------
  1.1245 +    Embedding of the hypernaturals into the hyperreal
  1.1246 + --------------------------------------------------------------*)
  1.1247 +(*** A lemma that should have been derived a long time ago! ***)
  1.1248 +Goal "(Ya : hyprel ^^{%n. f(n)}) = \
  1.1249 +\         ({n. f n = Ya n} : FreeUltrafilterNat)";
  1.1250 +by (Auto_tac);
  1.1251 +qed "lemma_hyprel_FUFN";
  1.1252 +
  1.1253 +Goalw [hypreal_of_hypnat_def]
  1.1254 +      "hypreal_of_hypnat (Abs_hypnat(hypnatrel^^{%n. X n})) = \
  1.1255 +\         Abs_hypreal(hyprel ^^ {%n. real_of_nat (X n)})";
  1.1256 +by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1);
  1.1257 +by (auto_tac (claset() addEs [FreeUltrafilterNat_Int RS
  1.1258 +    FreeUltrafilterNat_subset],simpset() addsimps 
  1.1259 +    [lemma_hyprel_FUFN]));
  1.1260 +qed "hypreal_of_hypnat";
  1.1261 +
  1.1262 +Goal "inj(hypreal_of_hypnat)";
  1.1263 +by (rtac injI 1);
  1.1264 +by (res_inst_tac [("z","x")] eq_Abs_hypnat 1);
  1.1265 +by (res_inst_tac [("z","y")] eq_Abs_hypnat 1);
  1.1266 +by (auto_tac (claset(),simpset() addsimps 
  1.1267 +    [hypreal_of_hypnat,real_of_nat_eq_cancel]));
  1.1268 +qed "inj_hypreal_of_hypnat";
  1.1269 +
  1.1270 +Goal "(hypreal_of_hypnat n = hypreal_of_hypnat m) = (n = m)";
  1.1271 +by (auto_tac (claset(),simpset() addsimps [inj_hypreal_of_hypnat RS injD]));
  1.1272 +qed "hypreal_of_hypnat_eq_cancel";
  1.1273 +Addsimps [hypreal_of_hypnat_eq_cancel];
  1.1274 +
  1.1275 +Goal "(hypnat_of_nat n = hypnat_of_nat m) = (n = m)";
  1.1276 +by (auto_tac (claset() addDs [inj_hypnat_of_nat RS injD],
  1.1277 +              simpset()));
  1.1278 +qed "hypnat_of_nat_eq_cancel";
  1.1279 +Addsimps [hypnat_of_nat_eq_cancel];
  1.1280 +
  1.1281 +Goalw [hypreal_zero_def,hypnat_zero_def] 
  1.1282 +           "hypreal_of_hypnat  0 = 0";
  1.1283 +by (simp_tac (simpset() addsimps [hypreal_of_hypnat,
  1.1284 +    real_of_nat_zero]) 1);
  1.1285 +qed "hypreal_of_hypnat_zero";
  1.1286 +
  1.1287 +Goalw [hypreal_one_def,hypnat_one_def] 
  1.1288 +           "hypreal_of_hypnat  1hn = 1hr";
  1.1289 +by (simp_tac (simpset() addsimps [hypreal_of_hypnat,
  1.1290 +    real_of_nat_one]) 1);
  1.1291 +qed "hypreal_of_hypnat_one";
  1.1292 +
  1.1293 +Goal "hypreal_of_hypnat n1 + hypreal_of_hypnat n2 = hypreal_of_hypnat (n1 + n2)";
  1.1294 +by (res_inst_tac [("z","n1")] eq_Abs_hypnat 1);
  1.1295 +by (res_inst_tac [("z","n2")] eq_Abs_hypnat 1);
  1.1296 +by (asm_simp_tac (simpset() addsimps [hypreal_of_hypnat,
  1.1297 +        hypreal_add,hypnat_add,real_of_nat_add]) 1);
  1.1298 +qed "hypreal_of_hypnat_add";
  1.1299 +
  1.1300 +Goal "hypreal_of_hypnat n1 * hypreal_of_hypnat n2 = hypreal_of_hypnat (n1 * n2)";
  1.1301 +by (res_inst_tac [("z","n1")] eq_Abs_hypnat 1);
  1.1302 +by (res_inst_tac [("z","n2")] eq_Abs_hypnat 1);
  1.1303 +by (asm_simp_tac (simpset() addsimps [hypreal_of_hypnat,
  1.1304 +        hypreal_mult,hypnat_mult,real_of_nat_mult]) 1);
  1.1305 +qed "hypreal_of_hypnat_mult";
  1.1306 +
  1.1307 +Goal "(hypreal_of_hypnat n < hypreal_of_hypnat m) = (n < m)";
  1.1308 +by (res_inst_tac [("z","n")] eq_Abs_hypnat 1);
  1.1309 +by (res_inst_tac [("z","m")] eq_Abs_hypnat 1);
  1.1310 +by (asm_simp_tac (simpset() addsimps 
  1.1311 +    [hypreal_of_hypnat,hypreal_less,hypnat_less]) 1);
  1.1312 +qed "hypreal_of_hypnat_less_iff";
  1.1313 +Addsimps [hypreal_of_hypnat_less_iff];
  1.1314 +
  1.1315 +Goal "(hypreal_of_hypnat N = 0) = (N = 0)";
  1.1316 +by (simp_tac (simpset() addsimps [hypreal_of_hypnat_zero RS sym]) 1);
  1.1317 +qed "hypreal_of_hypnat_eq_zero_iff";
  1.1318 +Addsimps [hypreal_of_hypnat_eq_zero_iff];
  1.1319 +
  1.1320 +Goal "ALL n. N <= n ==> N = (0::hypnat)";
  1.1321 +by (dres_inst_tac [("x","0")] spec 1);
  1.1322 +by (res_inst_tac [("z","N")] eq_Abs_hypnat 1);
  1.1323 +by (auto_tac (claset(),simpset() addsimps [hypnat_le,hypnat_zero_def]));
  1.1324 +qed "hypnat_eq_zero";
  1.1325 +Addsimps [hypnat_eq_zero];
  1.1326 +
  1.1327 +Goal "~ (ALL n. n = (0::hypnat))";
  1.1328 +by Auto_tac;
  1.1329 +by (res_inst_tac [("x","1hn")] exI 1);
  1.1330 +by (Simp_tac 1);
  1.1331 +qed "hypnat_not_all_eq_zero";
  1.1332 +Addsimps [hypnat_not_all_eq_zero];
  1.1333 +
  1.1334 +Goal "n ~= 0 ==> (n <= 1hn) = (n = 1hn)";
  1.1335 +by (auto_tac (claset(),simpset() addsimps [hypnat_le_eq_less_or_eq]));
  1.1336 +qed "hypnat_le_one_eq_one";
  1.1337 +Addsimps [hypnat_le_one_eq_one];
  1.1338 +
  1.1339 +
  1.1340 +
  1.1341 +