12 imports SEQ |
12 imports SEQ |
13 begin |
13 begin |
14 |
14 |
15 text{*Standard and Nonstandard Definitions*} |
15 text{*Standard and Nonstandard Definitions*} |
16 |
16 |
17 constdefs |
17 definition |
18 LIM :: "[real=>real,real,real] => bool" |
18 LIM :: "[real=>real,real,real] => bool" |
19 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
19 ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) |
20 "f -- a --> L == |
20 "f -- a --> L = |
21 \<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s |
21 (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s |
22 --> \<bar>f x + -L\<bar> < r" |
22 --> \<bar>f x + -L\<bar> < r)" |
23 |
23 |
24 NSLIM :: "[real=>real,real,real] => bool" |
24 NSLIM :: "[real=>real,real,real] => bool" |
25 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
25 ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) |
26 "f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a & |
26 "f -- a --NS> L = (\<forall>x. (x \<noteq> hypreal_of_real a & |
27 x @= hypreal_of_real a --> |
27 x @= hypreal_of_real a --> |
28 ( *f* f) x @= hypreal_of_real L))" |
28 ( *f* f) x @= hypreal_of_real L))" |
29 |
29 |
30 isCont :: "[real=>real,real] => bool" |
30 isCont :: "[real=>real,real] => bool" |
31 "isCont f a == (f -- a --> (f a))" |
31 "isCont f a = (f -- a --> (f a))" |
32 |
32 |
33 isNSCont :: "[real=>real,real] => bool" |
33 isNSCont :: "[real=>real,real] => bool" |
34 --{*NS definition dispenses with limit notions*} |
34 --{*NS definition dispenses with limit notions*} |
35 "isNSCont f a == (\<forall>y. y @= hypreal_of_real a --> |
35 "isNSCont f a = (\<forall>y. y @= hypreal_of_real a --> |
36 ( *f* f) y @= hypreal_of_real (f a))" |
36 ( *f* f) y @= hypreal_of_real (f a))" |
37 |
37 |
38 deriv:: "[real=>real,real,real] => bool" |
38 deriv:: "[real=>real,real,real] => bool" |
39 --{*Differentiation: D is derivative of function f at x*} |
39 --{*Differentiation: D is derivative of function f at x*} |
40 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
40 ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
41 "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)" |
41 "DERIV f x :> D = ((%h. (f(x + h) + -f x)/h) -- 0 --> D)" |
42 |
42 |
43 nsderiv :: "[real=>real,real,real] => bool" |
43 nsderiv :: "[real=>real,real,real] => bool" |
44 ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
44 ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) |
45 "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}. |
45 "NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal - {0}. |
46 (( *f* f)(hypreal_of_real x + h) + |
46 (( *f* f)(hypreal_of_real x + h) + |
47 - hypreal_of_real (f x))/h @= hypreal_of_real D)" |
47 - hypreal_of_real (f x))/h @= hypreal_of_real D)" |
48 |
48 |
49 differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60) |
49 differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60) |
50 "f differentiable x == (\<exists>D. DERIV f x :> D)" |
50 "f differentiable x = (\<exists>D. DERIV f x :> D)" |
51 |
51 |
52 NSdifferentiable :: "[real=>real,real] => bool" |
52 NSdifferentiable :: "[real=>real,real] => bool" |
53 (infixl "NSdifferentiable" 60) |
53 (infixl "NSdifferentiable" 60) |
54 "f NSdifferentiable x == (\<exists>D. NSDERIV f x :> D)" |
54 "f NSdifferentiable x = (\<exists>D. NSDERIV f x :> D)" |
55 |
55 |
56 increment :: "[real=>real,real,hypreal] => hypreal" |
56 increment :: "[real=>real,real,hypreal] => hypreal" |
57 "increment f x h == (@inc. f NSdifferentiable x & |
57 "increment f x h = (@inc. f NSdifferentiable x & |
58 inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))" |
58 inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))" |
59 |
59 |
60 isUCont :: "(real=>real) => bool" |
60 isUCont :: "(real=>real) => bool" |
61 "isUCont f == \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r" |
61 "isUCont f = (\<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r)" |
62 |
62 |
63 isNSUCont :: "(real=>real) => bool" |
63 isNSUCont :: "(real=>real) => bool" |
64 "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)" |
64 "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)" |
65 |
65 |
66 |
66 |
67 consts |
67 consts |
68 Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" |
68 Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" |
69 --{*Used in the proof of the Bolzano theorem*} |
|
70 |
|
71 |
|
72 primrec |
69 primrec |
73 "Bolzano_bisect P a b 0 = (a,b)" |
70 "Bolzano_bisect P a b 0 = (a,b)" |
74 "Bolzano_bisect P a b (Suc n) = |
71 "Bolzano_bisect P a b (Suc n) = |
75 (let (x,y) = Bolzano_bisect P a b n |
72 (let (x,y) = Bolzano_bisect P a b n |
76 in if P(x, (x+y)/2) then ((x+y)/2, y) |
73 in if P(x, (x+y)/2) then ((x+y)/2, y) |
2370 then have |
2367 then have |
2371 "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> \<bar>f (x+c) + -L\<bar> < r" by simp |
2368 "\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> (a-c) & \<bar>x + -(a-c)\<bar> < s --> \<bar>f (x+c) + -L\<bar> < r" by simp |
2372 thus ?thesis by (fold LIM_def) |
2369 thus ?thesis by (fold LIM_def) |
2373 qed |
2370 qed |
2374 |
2371 |
2375 |
|
2376 |
|
2377 ML |
|
2378 {* |
|
2379 val LIM_def = thm"LIM_def"; |
|
2380 val NSLIM_def = thm"NSLIM_def"; |
|
2381 val isCont_def = thm"isCont_def"; |
|
2382 val isNSCont_def = thm"isNSCont_def"; |
|
2383 val deriv_def = thm"deriv_def"; |
|
2384 val nsderiv_def = thm"nsderiv_def"; |
|
2385 val differentiable_def = thm"differentiable_def"; |
|
2386 val NSdifferentiable_def = thm"NSdifferentiable_def"; |
|
2387 val increment_def = thm"increment_def"; |
|
2388 val isUCont_def = thm"isUCont_def"; |
|
2389 val isNSUCont_def = thm"isNSUCont_def"; |
|
2390 |
|
2391 val half_gt_zero_iff = thm "half_gt_zero_iff"; |
|
2392 val half_gt_zero = thms "half_gt_zero"; |
|
2393 val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq"; |
|
2394 val LIM_eq = thm "LIM_eq"; |
|
2395 val LIM_D = thm "LIM_D"; |
|
2396 val LIM_const = thm "LIM_const"; |
|
2397 val LIM_add = thm "LIM_add"; |
|
2398 val LIM_minus = thm "LIM_minus"; |
|
2399 val LIM_add_minus = thm "LIM_add_minus"; |
|
2400 val LIM_diff = thm "LIM_diff"; |
|
2401 val LIM_const_not_eq = thm "LIM_const_not_eq"; |
|
2402 val LIM_const_eq = thm "LIM_const_eq"; |
|
2403 val LIM_unique = thm "LIM_unique"; |
|
2404 val LIM_mult_zero = thm "LIM_mult_zero"; |
|
2405 val LIM_self = thm "LIM_self"; |
|
2406 val LIM_equal = thm "LIM_equal"; |
|
2407 val LIM_trans = thm "LIM_trans"; |
|
2408 val LIM_NSLIM = thm "LIM_NSLIM"; |
|
2409 val NSLIM_LIM = thm "NSLIM_LIM"; |
|
2410 val LIM_NSLIM_iff = thm "LIM_NSLIM_iff"; |
|
2411 val NSLIM_mult = thm "NSLIM_mult"; |
|
2412 val LIM_mult2 = thm "LIM_mult2"; |
|
2413 val NSLIM_add = thm "NSLIM_add"; |
|
2414 val LIM_add2 = thm "LIM_add2"; |
|
2415 val NSLIM_const = thm "NSLIM_const"; |
|
2416 val LIM_const2 = thm "LIM_const2"; |
|
2417 val NSLIM_minus = thm "NSLIM_minus"; |
|
2418 val LIM_minus2 = thm "LIM_minus2"; |
|
2419 val NSLIM_add_minus = thm "NSLIM_add_minus"; |
|
2420 val LIM_add_minus2 = thm "LIM_add_minus2"; |
|
2421 val NSLIM_inverse = thm "NSLIM_inverse"; |
|
2422 val LIM_inverse = thm "LIM_inverse"; |
|
2423 val NSLIM_zero = thm "NSLIM_zero"; |
|
2424 val LIM_zero2 = thm "LIM_zero2"; |
|
2425 val NSLIM_zero_cancel = thm "NSLIM_zero_cancel"; |
|
2426 val LIM_zero_cancel = thm "LIM_zero_cancel"; |
|
2427 val NSLIM_not_zero = thm "NSLIM_not_zero"; |
|
2428 val NSLIM_const_not_eq = thm "NSLIM_const_not_eq"; |
|
2429 val NSLIM_const_eq = thm "NSLIM_const_eq"; |
|
2430 val NSLIM_unique = thm "NSLIM_unique"; |
|
2431 val LIM_unique2 = thm "LIM_unique2"; |
|
2432 val NSLIM_mult_zero = thm "NSLIM_mult_zero"; |
|
2433 val LIM_mult_zero2 = thm "LIM_mult_zero2"; |
|
2434 val NSLIM_self = thm "NSLIM_self"; |
|
2435 val isNSContD = thm "isNSContD"; |
|
2436 val isNSCont_NSLIM = thm "isNSCont_NSLIM"; |
|
2437 val NSLIM_isNSCont = thm "NSLIM_isNSCont"; |
|
2438 val isNSCont_NSLIM_iff = thm "isNSCont_NSLIM_iff"; |
|
2439 val isNSCont_LIM_iff = thm "isNSCont_LIM_iff"; |
|
2440 val isNSCont_isCont_iff = thm "isNSCont_isCont_iff"; |
|
2441 val isCont_isNSCont = thm "isCont_isNSCont"; |
|
2442 val isNSCont_isCont = thm "isNSCont_isCont"; |
|
2443 val NSLIM_h_iff = thm "NSLIM_h_iff"; |
|
2444 val NSLIM_isCont_iff = thm "NSLIM_isCont_iff"; |
|
2445 val LIM_isCont_iff = thm "LIM_isCont_iff"; |
|
2446 val isCont_iff = thm "isCont_iff"; |
|
2447 val isCont_add = thm "isCont_add"; |
|
2448 val isCont_mult = thm "isCont_mult"; |
|
2449 val isCont_o = thm "isCont_o"; |
|
2450 val isCont_o2 = thm "isCont_o2"; |
|
2451 val isNSCont_minus = thm "isNSCont_minus"; |
|
2452 val isCont_minus = thm "isCont_minus"; |
|
2453 val isCont_inverse = thm "isCont_inverse"; |
|
2454 val isNSCont_inverse = thm "isNSCont_inverse"; |
|
2455 val isCont_diff = thm "isCont_diff"; |
|
2456 val isCont_const = thm "isCont_const"; |
|
2457 val isNSCont_const = thm "isNSCont_const"; |
|
2458 val isNSUContD = thm "isNSUContD"; |
|
2459 val isUCont_isCont = thm "isUCont_isCont"; |
|
2460 val isUCont_isNSUCont = thm "isUCont_isNSUCont"; |
|
2461 val isNSUCont_isUCont = thm "isNSUCont_isUCont"; |
|
2462 val DERIV_iff = thm "DERIV_iff"; |
|
2463 val DERIV_NS_iff = thm "DERIV_NS_iff"; |
|
2464 val DERIV_D = thm "DERIV_D"; |
|
2465 val NS_DERIV_D = thm "NS_DERIV_D"; |
|
2466 val DERIV_unique = thm "DERIV_unique"; |
|
2467 val NSDeriv_unique = thm "NSDeriv_unique"; |
|
2468 val differentiableD = thm "differentiableD"; |
|
2469 val differentiableI = thm "differentiableI"; |
|
2470 val NSdifferentiableD = thm "NSdifferentiableD"; |
|
2471 val NSdifferentiableI = thm "NSdifferentiableI"; |
|
2472 val LIM_I = thm "LIM_I"; |
|
2473 val DERIV_LIM_iff = thm "DERIV_LIM_iff"; |
|
2474 val DERIV_iff2 = thm "DERIV_iff2"; |
|
2475 val NSDERIV_NSLIM_iff = thm "NSDERIV_NSLIM_iff"; |
|
2476 val NSDERIV_NSLIM_iff2 = thm "NSDERIV_NSLIM_iff2"; |
|
2477 val NSDERIV_iff2 = thm "NSDERIV_iff2"; |
|
2478 val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff"; |
|
2479 val NSDERIVD5 = thm "NSDERIVD5"; |
|
2480 val NSDERIVD4 = thm "NSDERIVD4"; |
|
2481 val NSDERIVD3 = thm "NSDERIVD3"; |
|
2482 val NSDERIV_DERIV_iff = thm "NSDERIV_DERIV_iff"; |
|
2483 val NSDERIV_isNSCont = thm "NSDERIV_isNSCont"; |
|
2484 val DERIV_isCont = thm "DERIV_isCont"; |
|
2485 val NSDERIV_const = thm "NSDERIV_const"; |
|
2486 val DERIV_const = thm "DERIV_const"; |
|
2487 val NSDERIV_add = thm "NSDERIV_add"; |
|
2488 val DERIV_add = thm "DERIV_add"; |
|
2489 val NSDERIV_mult = thm "NSDERIV_mult"; |
|
2490 val DERIV_mult = thm "DERIV_mult"; |
|
2491 val NSDERIV_cmult = thm "NSDERIV_cmult"; |
|
2492 val DERIV_cmult = thm "DERIV_cmult"; |
|
2493 val NSDERIV_minus = thm "NSDERIV_minus"; |
|
2494 val DERIV_minus = thm "DERIV_minus"; |
|
2495 val NSDERIV_add_minus = thm "NSDERIV_add_minus"; |
|
2496 val DERIV_add_minus = thm "DERIV_add_minus"; |
|
2497 val NSDERIV_diff = thm "NSDERIV_diff"; |
|
2498 val DERIV_diff = thm "DERIV_diff"; |
|
2499 val incrementI = thm "incrementI"; |
|
2500 val incrementI2 = thm "incrementI2"; |
|
2501 val increment_thm = thm "increment_thm"; |
|
2502 val increment_thm2 = thm "increment_thm2"; |
|
2503 val increment_approx_zero = thm "increment_approx_zero"; |
|
2504 val NSDERIV_zero = thm "NSDERIV_zero"; |
|
2505 val NSDERIV_approx = thm "NSDERIV_approx"; |
|
2506 val NSDERIVD1 = thm "NSDERIVD1"; |
|
2507 val NSDERIVD2 = thm "NSDERIVD2"; |
|
2508 val NSDERIV_chain = thm "NSDERIV_chain"; |
|
2509 val DERIV_chain = thm "DERIV_chain"; |
|
2510 val DERIV_chain2 = thm "DERIV_chain2"; |
|
2511 val NSDERIV_Id = thm "NSDERIV_Id"; |
|
2512 val DERIV_Id = thm "DERIV_Id"; |
|
2513 val isCont_Id = thms "isCont_Id"; |
|
2514 val DERIV_cmult_Id = thm "DERIV_cmult_Id"; |
|
2515 val NSDERIV_cmult_Id = thm "NSDERIV_cmult_Id"; |
|
2516 val DERIV_pow = thm "DERIV_pow"; |
|
2517 val NSDERIV_pow = thm "NSDERIV_pow"; |
|
2518 val NSDERIV_inverse = thm "NSDERIV_inverse"; |
|
2519 val DERIV_inverse = thm "DERIV_inverse"; |
|
2520 val DERIV_inverse_fun = thm "DERIV_inverse_fun"; |
|
2521 val NSDERIV_inverse_fun = thm "NSDERIV_inverse_fun"; |
|
2522 val DERIV_quotient = thm "DERIV_quotient"; |
|
2523 val NSDERIV_quotient = thm "NSDERIV_quotient"; |
|
2524 val CARAT_DERIV = thm "CARAT_DERIV"; |
|
2525 val CARAT_NSDERIV = thm "CARAT_NSDERIV"; |
|
2526 val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3"; |
|
2527 val starfun_if_eq = thm "starfun_if_eq"; |
|
2528 val CARAT_DERIVD = thm "CARAT_DERIVD"; |
|
2529 val f_inc_g_dec_Beq_f = thm "f_inc_g_dec_Beq_f"; |
|
2530 val f_inc_g_dec_Beq_g = thm "f_inc_g_dec_Beq_g"; |
|
2531 val f_inc_imp_le_lim = thm "f_inc_imp_le_lim"; |
|
2532 val lim_uminus = thm "lim_uminus"; |
|
2533 val g_dec_imp_lim_le = thm "g_dec_imp_lim_le"; |
|
2534 val Bolzano_bisect_le = thm "Bolzano_bisect_le"; |
|
2535 val Bolzano_bisect_fst_le_Suc = thm "Bolzano_bisect_fst_le_Suc"; |
|
2536 val Bolzano_bisect_Suc_le_snd = thm "Bolzano_bisect_Suc_le_snd"; |
|
2537 val eq_divide_2_times_iff = thm "eq_divide_2_times_iff"; |
|
2538 val Bolzano_bisect_diff = thm "Bolzano_bisect_diff"; |
|
2539 val Bolzano_nest_unique = thms "Bolzano_nest_unique"; |
|
2540 val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect"; |
|
2541 val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect"; |
|
2542 val lemma_BOLZANO2 = thm "lemma_BOLZANO2"; |
|
2543 val IVT = thm "IVT"; |
|
2544 val IVT2 = thm "IVT2"; |
|
2545 val IVT_objl = thm "IVT_objl"; |
|
2546 val IVT2_objl = thm "IVT2_objl"; |
|
2547 val isCont_bounded = thm "isCont_bounded"; |
|
2548 val isCont_has_Ub = thm "isCont_has_Ub"; |
|
2549 val isCont_eq_Ub = thm "isCont_eq_Ub"; |
|
2550 val isCont_eq_Lb = thm "isCont_eq_Lb"; |
|
2551 val isCont_Lb_Ub = thm "isCont_Lb_Ub"; |
|
2552 val DERIV_left_inc = thm "DERIV_left_inc"; |
|
2553 val DERIV_left_dec = thm "DERIV_left_dec"; |
|
2554 val DERIV_local_max = thm "DERIV_local_max"; |
|
2555 val DERIV_local_min = thm "DERIV_local_min"; |
|
2556 val DERIV_local_const = thm "DERIV_local_const"; |
|
2557 val Rolle = thm "Rolle"; |
|
2558 val MVT = thm "MVT"; |
|
2559 val DERIV_isconst_end = thm "DERIV_isconst_end"; |
|
2560 val DERIV_isconst1 = thm "DERIV_isconst1"; |
|
2561 val DERIV_isconst2 = thm "DERIV_isconst2"; |
|
2562 val DERIV_isconst_all = thm "DERIV_isconst_all"; |
|
2563 val DERIV_const_ratio_const = thm "DERIV_const_ratio_const"; |
|
2564 val DERIV_const_ratio_const2 = thm "DERIV_const_ratio_const2"; |
|
2565 val real_average_minus_first = thm "real_average_minus_first"; |
|
2566 val real_average_minus_second = thm "real_average_minus_second"; |
|
2567 val DERIV_const_average = thm "DERIV_const_average"; |
|
2568 val isCont_inj_range = thm "isCont_inj_range"; |
|
2569 val isCont_inverse_function = thm "isCont_inverse_function"; |
|
2570 *} |
|
2571 |
|
2572 |
|
2573 end |
2372 end |