5 satisfies plus_ac0: + is an AC-operator with zero |
5 satisfies plus_ac0: + is an AC-operator with zero |
6 *) |
6 *) |
7 |
7 |
8 theory HyperOrd = HyperDef: |
8 theory HyperOrd = HyperDef: |
9 |
9 |
10 |
10 defs (overloaded) |
11 method_setup fuf = {* |
11 hrabs_def: "abs (r::hypreal) == (if 0 \<le> r then r else -r)" |
12 Method.ctxt_args (fn ctxt => |
12 |
13 Method.METHOD (fn facts => |
13 |
14 fuf_tac (Classical.get_local_claset ctxt, |
14 lemma hypreal_hrabs: |
15 Simplifier.get_local_simpset ctxt) 1)) *} |
15 "abs (Abs_hypreal (hyprel `` {X})) = |
16 "free ultrafilter tactic" |
16 Abs_hypreal(hyprel `` {%n. abs (X n)})" |
17 |
17 apply (auto simp add: hrabs_def hypreal_zero_def hypreal_le hypreal_minus) |
18 method_setup ultra = {* |
18 apply (ultra, arith)+ |
19 Method.ctxt_args (fn ctxt => |
19 done |
20 Method.METHOD (fn facts => |
|
21 ultra_tac (Classical.get_local_claset ctxt, |
|
22 Simplifier.get_local_simpset ctxt) 1)) *} |
|
23 "ultrafilter tactic" |
|
24 |
|
25 |
20 |
26 instance hypreal :: order |
21 instance hypreal :: order |
27 by (intro_classes, |
22 by (intro_classes, |
28 (assumption | |
23 (assumption | |
29 rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym |
24 rule hypreal_le_refl hypreal_le_trans hypreal_le_anti_sym |
342 |
337 |
343 (*---------------------------------------------------------------------------- |
338 (*---------------------------------------------------------------------------- |
344 Existence of infinite hyperreal number |
339 Existence of infinite hyperreal number |
345 ----------------------------------------------------------------------------*) |
340 ----------------------------------------------------------------------------*) |
346 |
341 |
347 lemma Rep_hypreal_omega: "Rep_hypreal(omega) : hypreal" |
342 lemma Rep_hypreal_omega: "Rep_hypreal(omega) \<in> hypreal" |
348 |
|
349 apply (unfold omega_def) |
343 apply (unfold omega_def) |
350 apply (rule Rep_hypreal) |
344 apply (rule Rep_hypreal) |
351 done |
345 done |
352 |
346 |
353 (* existence of infinite number not corresponding to any real number *) |
347 (* existence of infinite number not corresponding to any real number *) |
354 (* use assumption that member FreeUltrafilterNat is not finite *) |
348 (* use assumption that member FreeUltrafilterNat is not finite *) |
355 (* a few lemmas first *) |
349 (* a few lemmas first *) |
356 |
350 |
357 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | |
351 lemma lemma_omega_empty_singleton_disj: "{n::nat. x = real n} = {} | |
358 (EX y. {n::nat. x = real n} = {y})" |
352 (\<exists>y. {n::nat. x = real n} = {y})" |
359 by (force dest: inj_real_of_nat [THEN injD]) |
353 by (force dest: inj_real_of_nat [THEN injD]) |
360 |
354 |
361 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
355 lemma lemma_finite_omega_set: "finite {n::nat. x = real n}" |
362 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) |
356 by (cut_tac x = x in lemma_omega_empty_singleton_disj, auto) |
363 |
357 |
364 lemma not_ex_hypreal_of_real_eq_omega: |
358 lemma not_ex_hypreal_of_real_eq_omega: |
365 "~ (EX x. hypreal_of_real x = omega)" |
359 "~ (\<exists>x. hypreal_of_real x = omega)" |
366 apply (unfold omega_def hypreal_of_real_def) |
360 apply (unfold omega_def hypreal_of_real_def) |
367 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) |
361 apply (auto simp add: real_of_nat_Suc diff_eq_eq [symmetric] lemma_finite_omega_set [THEN FreeUltrafilterNat_finite]) |
368 done |
362 done |
369 |
363 |
370 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x ~= omega" |
364 lemma hypreal_of_real_not_eq_omega: "hypreal_of_real x \<noteq> omega" |
371 by (cut_tac not_ex_hypreal_of_real_eq_omega, auto) |
365 by (cut_tac not_ex_hypreal_of_real_eq_omega, auto) |
372 |
366 |
373 (* existence of infinitesimal number also not *) |
367 (* existence of infinitesimal number also not *) |
374 (* corresponding to any real number *) |
368 (* corresponding to any real number *) |
375 |
369 |
376 lemma real_of_nat_inverse_inj: "inverse (real (x::nat)) = inverse (real y) ==> x = y" |
370 lemma real_of_nat_inverse_inj: "inverse (real (x::nat)) = inverse (real y) ==> x = y" |
377 by (rule inj_real_of_nat [THEN injD], simp) |
371 by (rule inj_real_of_nat [THEN injD], simp) |
378 |
372 |
379 lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} | |
373 lemma lemma_epsilon_empty_singleton_disj: "{n::nat. x = inverse(real(Suc n))} = {} | |
380 (EX y. {n::nat. x = inverse(real(Suc n))} = {y})" |
374 (\<exists>y. {n::nat. x = inverse(real(Suc n))} = {y})" |
381 apply (auto simp add: inj_real_of_nat [THEN inj_eq]) |
375 apply (auto simp add: inj_real_of_nat [THEN inj_eq]) |
382 done |
376 done |
383 |
377 |
384 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
378 lemma lemma_finite_epsilon_set: "finite {n. x = inverse(real(Suc n))}" |
385 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
379 by (cut_tac x = x in lemma_epsilon_empty_singleton_disj, auto) |
386 |
380 |
387 lemma not_ex_hypreal_of_real_eq_epsilon: |
381 lemma not_ex_hypreal_of_real_eq_epsilon: |
388 "~ (EX x. hypreal_of_real x = epsilon)" |
382 "~ (\<exists>x. hypreal_of_real x = epsilon)" |
389 apply (unfold epsilon_def hypreal_of_real_def) |
383 apply (unfold epsilon_def hypreal_of_real_def) |
390 apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite]) |
384 apply (auto simp add: lemma_finite_epsilon_set [THEN FreeUltrafilterNat_finite]) |
391 done |
385 done |
392 |
386 |
393 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x ~= epsilon" |
387 lemma hypreal_of_real_not_eq_epsilon: "hypreal_of_real x \<noteq> epsilon" |
394 by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto) |
388 by (cut_tac not_ex_hypreal_of_real_eq_epsilon, auto) |
395 |
389 |
396 lemma hypreal_epsilon_not_zero: "epsilon ~= 0" |
390 lemma hypreal_epsilon_not_zero: "epsilon \<noteq> 0" |
397 by (unfold epsilon_def hypreal_zero_def, auto) |
391 by (unfold epsilon_def hypreal_zero_def, auto) |
398 |
392 |
399 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
393 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)" |
400 by (simp add: hypreal_inverse omega_def epsilon_def) |
394 by (simp add: hypreal_inverse omega_def epsilon_def) |
401 |
395 |
468 by (auto dest: order_less_not_sym simp add: hypreal_0_less_mult_iff linorder_not_less [symmetric]) |
462 by (auto dest: order_less_not_sym simp add: hypreal_0_less_mult_iff linorder_not_less [symmetric]) |
469 |
463 |
470 lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0" |
464 lemma hypreal_mult_less_zero2: "[| (0::hypreal) < x; y < 0 |] ==> y*x < 0" |
471 by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero) |
465 by (auto simp add: hypreal_mult_commute hypreal_mult_less_zero) |
472 |
466 |
473 |
467 (*TO BE DELETED*) |
474 ML |
468 ML |
475 {* |
469 {* |
|
470 val hypreal_add_ac = thms"hypreal_add_ac"; |
|
471 val hypreal_mult_ac = thms"hypreal_mult_ac"; |
|
472 |
|
473 val hypreal_less_irrefl = thm"hypreal_less_irrefl"; |
|
474 *} |
|
475 |
|
476 ML |
|
477 {* |
|
478 val hrabs_def = thm "hrabs_def"; |
|
479 val hypreal_hrabs = thm "hypreal_hrabs"; |
|
480 |
476 val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21"; |
481 val hypreal_add_cancel_21 = thm"hypreal_add_cancel_21"; |
477 val hypreal_add_cancel_end = thm"hypreal_add_cancel_end"; |
482 val hypreal_add_cancel_end = thm"hypreal_add_cancel_end"; |
478 val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq"; |
483 val hypreal_minus_diff_eq = thm"hypreal_minus_diff_eq"; |
479 val hypreal_less_swap_iff = thm"hypreal_less_swap_iff"; |
484 val hypreal_less_swap_iff = thm"hypreal_less_swap_iff"; |
480 val hypreal_gt_zero_iff = thm"hypreal_gt_zero_iff"; |
485 val hypreal_gt_zero_iff = thm"hypreal_gt_zero_iff"; |