Structure limTheory
signature limTheory =
sig
type thm = Thm.thm
(* Definitions *)
val contl : thm
val differentiable : thm
val diffl : thm
val tends_real_real : thm
(* Theorems *)
val CONTL_LIM : thm
val CONT_ADD : thm
val CONT_ATTAINS : thm
val CONT_ATTAINS2 : thm
val CONT_ATTAINS_ALL : thm
val CONT_BOUNDED : thm
val CONT_COMPOSE : thm
val CONT_CONST : thm
val CONT_DIV : thm
val CONT_HASSUP : thm
val CONT_INJ_LEMMA : thm
val CONT_INJ_LEMMA2 : thm
val CONT_INJ_RANGE : thm
val CONT_INV : thm
val CONT_INVERSE : thm
val CONT_MUL : thm
val CONT_NEG : thm
val CONT_SUB : thm
val DIFF_ADD : thm
val DIFF_CARAT : thm
val DIFF_CHAIN : thm
val DIFF_CMUL : thm
val DIFF_CONST : thm
val DIFF_CONT : thm
val DIFF_DIV : thm
val DIFF_INV : thm
val DIFF_INVERSE : thm
val DIFF_INVERSE_LT : thm
val DIFF_INVERSE_OPEN : thm
val DIFF_ISCONST : thm
val DIFF_ISCONST_ALL : thm
val DIFF_ISCONST_END : thm
val DIFF_LCONST : thm
val DIFF_LDEC : thm
val DIFF_LINC : thm
val DIFF_LMAX : thm
val DIFF_LMIN : thm
val DIFF_MUL : thm
val DIFF_NEG : thm
val DIFF_POW : thm
val DIFF_SUB : thm
val DIFF_SUM : thm
val DIFF_UNIQ : thm
val DIFF_X : thm
val DIFF_XM1 : thm
val INTERVAL_ABS : thm
val INTERVAL_CLEMMA : thm
val INTERVAL_LEMMA : thm
val IVT : thm
val IVT2 : thm
val LIM : thm
val LIM_ADD : thm
val LIM_CONST : thm
val LIM_DIV : thm
val LIM_EQUAL : thm
val LIM_INV : thm
val LIM_MUL : thm
val LIM_NEG : thm
val LIM_NULL : thm
val LIM_SUB : thm
val LIM_TRANSFORM : thm
val LIM_UNIQ : thm
val LIM_X : thm
val MVT : thm
val MVT_LEMMA : thm
val ROLLE : thm
val lim_grammars : type_grammar.grammar * term_grammar.grammar
(*
[seq] Parent theory of "lim"
[contl] Definition
|- !f x. f contl x = ((\h. f (x + h)) -> f x) 0
[differentiable] Definition
|- !f x. f differentiable x = ?l. (f diffl l) x
[diffl] Definition
|- !f l x. (f diffl l) x = ((\h. (f (x + h) - f x) / h) -> l) 0
[tends_real_real] Definition
|- !f l x0. (f -> l) x0 = (f tends l) (mtop mr1,tendsto (mr1,x0))
[CONTL_LIM] Theorem
|- !f x. f contl x = (f -> f x) x
[CONT_ADD] Theorem
|- !f g x. f contl x /\ g contl x ==> (\x. f x + g x) contl x
[CONT_ATTAINS] Theorem
|- !f a b.
a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==>
?M.
(!x. a <= x /\ x <= b ==> f x <= M) /\ ?x. a <= x /\ x <= b /\ (f x = M)
[CONT_ATTAINS2] Theorem
|- !f a b.
a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==>
?M.
(!x. a <= x /\ x <= b ==> M <= f x) /\ ?x. a <= x /\ x <= b /\ (f x = M)
[CONT_ATTAINS_ALL] Theorem
|- !f a b.
a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==>
?L M.
L <= M /\
(!y. L <= y /\ y <= M ==> ?x. a <= x /\ x <= b /\ (f x = y)) /\
!x. a <= x /\ x <= b ==> L <= f x /\ f x <= M
[CONT_BOUNDED] Theorem
|- !f a b.
a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==>
?M. !x. a <= x /\ x <= b ==> f x <= M
[CONT_COMPOSE] Theorem
|- !f g x. f contl x /\ g contl f x ==> (\x. g (f x)) contl x
[CONT_CONST] Theorem
|- !k x. (\x. k) contl x
[CONT_DIV] Theorem
|- !f g x. f contl x /\ g contl x /\ ~(g x = 0) ==> (\x. f x / g x) contl x
[CONT_HASSUP] Theorem
|- !f a b.
a <= b /\ (!x. a <= x /\ x <= b ==> f contl x) ==>
?M.
(!x. a <= x /\ x <= b ==> f x <= M) /\
!N. N < M ==> ?x. a <= x /\ x <= b /\ N < f x
[CONT_INJ_LEMMA] Theorem
|- !f g x d.
0 < d /\ (!z. abs (z - x) <= d ==> (g (f z) = z)) /\
(!z. abs (z - x) <= d ==> f contl z) ==>
~ !z. abs (z - x) <= d ==> f z <= f x
[CONT_INJ_LEMMA2] Theorem
|- !f g x d.
0 < d /\ (!z. abs (z - x) <= d ==> (g (f z) = z)) /\
(!z. abs (z - x) <= d ==> f contl z) ==>
~ !z. abs (z - x) <= d ==> f x <= f z
[CONT_INJ_RANGE] Theorem
|- !f g x d.
0 < d /\ (!z. abs (z - x) <= d ==> (g (f z) = z)) /\
(!z. abs (z - x) <= d ==> f contl z) ==>
?e. 0 < e /\ !y. abs (y - f x) <= e ==> ?z. abs (z - x) <= d /\ (f z = y)
[CONT_INV] Theorem
|- !f x. f contl x /\ ~(f x = 0) ==> (\x. inv (f x)) contl x
[CONT_INVERSE] Theorem
|- !f g x d.
0 < d /\ (!z. abs (z - x) <= d ==> (g (f z) = z)) /\
(!z. abs (z - x) <= d ==> f contl z) ==>
g contl f x
[CONT_MUL] Theorem
|- !f g x. f contl x /\ g contl x ==> (\x. f x * g x) contl x
[CONT_NEG] Theorem
|- !f x. f contl x ==> (\x. ~f x) contl x
[CONT_SUB] Theorem
|- !f g x. f contl x /\ g contl x ==> (\x. f x - g x) contl x
[DIFF_ADD] Theorem
|- !f g l m x.
(f diffl l) x /\ (g diffl m) x ==> ((\x. f x + g x) diffl (l + m)) x
[DIFF_CARAT] Theorem
|- !f l x.
(f diffl l) x =
?g. (!z. f z - f x = g z * (z - x)) /\ g contl x /\ (g x = l)
[DIFF_CHAIN] Theorem
|- !f g l m x.
(f diffl l) (g x) /\ (g diffl m) x ==> ((\x. f (g x)) diffl (l * m)) x
[DIFF_CMUL] Theorem
|- !f c l x. (f diffl l) x ==> ((\x. c * f x) diffl (c * l)) x
[DIFF_CONST] Theorem
|- !k x. ((\x. k) diffl 0) x
[DIFF_CONT] Theorem
|- !f l x. (f diffl l) x ==> f contl x
[DIFF_DIV] Theorem
|- !f g l m x.
(f diffl l) x /\ (g diffl m) x /\ ~(g x = 0) ==>
((\x. f x / g x) diffl ((l * g x - m * f x) / g x pow 2)) x
[DIFF_INV] Theorem
|- !f l x.
(f diffl l) x /\ ~(f x = 0) ==> ((\x. inv (f x)) diffl ~(l / f x pow 2)) x
[DIFF_INVERSE] Theorem
|- !f g l x d.
0 < d /\ (!z. abs (z - x) <= d ==> (g (f z) = z)) /\
(!z. abs (z - x) <= d ==> f contl z) /\ (f diffl l) x /\ ~(l = 0) ==>
(g diffl inv l) (f x)
[DIFF_INVERSE_LT] Theorem
|- !f g l x d.
0 < d /\ (!z. abs (z - x) < d ==> (g (f z) = z)) /\
(!z. abs (z - x) < d ==> f contl z) /\ (f diffl l) x /\ ~(l = 0) ==>
(g diffl inv l) (f x)
[DIFF_INVERSE_OPEN] Theorem
|- !f g l a x b.
a < x /\ x < b /\ (!z. a < z /\ z < b ==> (g (f z) = z) /\ f contl z) /\
(f diffl l) x /\ ~(l = 0) ==>
(g diffl inv l) (f x)
[DIFF_ISCONST] Theorem
|- !f a b.
a < b /\ (!x. a <= x /\ x <= b ==> f contl x) /\
(!x. a < x /\ x < b ==> (f diffl 0) x) ==>
!x. a <= x /\ x <= b ==> (f x = f a)
[DIFF_ISCONST_ALL] Theorem
|- !f. (!x. (f diffl 0) x) ==> !x y. f x = f y
[DIFF_ISCONST_END] Theorem
|- !f a b.
a < b /\ (!x. a <= x /\ x <= b ==> f contl x) /\
(!x. a < x /\ x < b ==> (f diffl 0) x) ==>
(f b = f a)
[DIFF_LCONST] Theorem
|- !f x l.
(f diffl l) x /\ (?d. 0 < d /\ !y. abs (x - y) < d ==> (f y = f x)) ==>
(l = 0)
[DIFF_LDEC] Theorem
|- !f x l.
(f diffl l) x /\ l < 0 ==>
?d. 0 < d /\ !h. 0 < h /\ h < d ==> f x < f (x - h)
[DIFF_LINC] Theorem
|- !f x l.
(f diffl l) x /\ 0 < l ==>
?d. 0 < d /\ !h. 0 < h /\ h < d ==> f x < f (x + h)
[DIFF_LMAX] Theorem
|- !f x l.
(f diffl l) x /\ (?d. 0 < d /\ !y. abs (x - y) < d ==> f y <= f x) ==>
(l = 0)
[DIFF_LMIN] Theorem
|- !f x l.
(f diffl l) x /\ (?d. 0 < d /\ !y. abs (x - y) < d ==> f x <= f y) ==>
(l = 0)
[DIFF_MUL] Theorem
|- !f g l m x.
(f diffl l) x /\ (g diffl m) x ==>
((\x. f x * g x) diffl (l * g x + m * f x)) x
[DIFF_NEG] Theorem
|- !f l x. (f diffl l) x ==> ((\x. ~f x) diffl ~l) x
[DIFF_POW] Theorem
|- !n x. ((\x. x pow n) diffl (& n * x pow (n - 1))) x
[DIFF_SUB] Theorem
|- !f g l m x.
(f diffl l) x /\ (g diffl m) x ==> ((\x. f x - g x) diffl (l - m)) x
[DIFF_SUM] Theorem
|- !f f' m n x.
(!r. m <= r /\ r < m + n ==> ((\x. f r x) diffl f' r x) x) ==>
((\x. sum (m,n) (\n. f n x)) diffl sum (m,n) (\r. f' r x)) x
[DIFF_UNIQ] Theorem
|- !f l m x. (f diffl l) x /\ (f diffl m) x ==> (l = m)
[DIFF_X] Theorem
|- !x. ((\x. x) diffl 1) x
[DIFF_XM1] Theorem
|- !x. ~(x = 0) ==> ((\x. inv x) diffl ~(inv x pow 2)) x
[INTERVAL_ABS] Theorem
|- !x z d. x - d <= z /\ z <= x + d = abs (z - x) <= d
[INTERVAL_CLEMMA] Theorem
|- !a b x.
a < x /\ x < b ==> ?d. 0 < d /\ !y. abs (y - x) <= d ==> a < y /\ y < b
[INTERVAL_LEMMA] Theorem
|- !a b x.
a < x /\ x < b ==> ?d. 0 < d /\ !y. abs (x - y) < d ==> a <= y /\ y <= b
[IVT] Theorem
|- !f a b y.
a <= b /\ (f a <= y /\ y <= f b) /\
(!x. a <= x /\ x <= b ==> f contl x) ==>
?x. a <= x /\ x <= b /\ (f x = y)
[IVT2] Theorem
|- !f a b y.
a <= b /\ (f b <= y /\ y <= f a) /\
(!x. a <= x /\ x <= b ==> f contl x) ==>
?x. a <= x /\ x <= b /\ (f x = y)
[LIM] Theorem
|- !f y0 x0.
(f -> y0) x0 =
!e.
0 < e ==>
?d.
0 < d /\
!x. 0 < abs (x - x0) /\ abs (x - x0) < d ==> abs (f x - y0) < e
[LIM_ADD] Theorem
|- !f g l m x. (f -> l) x /\ (g -> m) x ==> ((\x. f x + g x) -> l + m) x
[LIM_CONST] Theorem
|- !k x. ((\x. k) -> k) x
[LIM_DIV] Theorem
|- !f g l m x.
(f -> l) x /\ (g -> m) x /\ ~(m = 0) ==> ((\x. f x / g x) -> l / m) x
[LIM_EQUAL] Theorem
|- !f g l x0. (!x. ~(x = x0) ==> (f x = g x)) ==> ((f -> l) x0 = (g -> l) x0)
[LIM_INV] Theorem
|- !f l x. (f -> l) x /\ ~(l = 0) ==> ((\x. inv (f x)) -> inv l) x
[LIM_MUL] Theorem
|- !f g l m x. (f -> l) x /\ (g -> m) x ==> ((\x. f x * g x) -> l * m) x
[LIM_NEG] Theorem
|- !f l x. (f -> l) x = ((\x. ~f x) -> ~l) x
[LIM_NULL] Theorem
|- !f l x. (f -> l) x = ((\x. f x - l) -> 0) x
[LIM_SUB] Theorem
|- !f g l m x. (f -> l) x /\ (g -> m) x ==> ((\x. f x - g x) -> l - m) x
[LIM_TRANSFORM] Theorem
|- !f g x0 l. ((\x. f x - g x) -> 0) x0 /\ (g -> l) x0 ==> (f -> l) x0
[LIM_UNIQ] Theorem
|- !f l m x. (f -> l) x /\ (f -> m) x ==> (l = m)
[LIM_X] Theorem
|- !x0. ((\x. x) -> x0) x0
[MVT] Theorem
|- !f a b.
a < b /\ (!x. a <= x /\ x <= b ==> f contl x) /\
(!x. a < x /\ x < b ==> f differentiable x) ==>
?l z. a < z /\ z < b /\ (f diffl l) z /\ (f b - f a = (b - a) * l)
[MVT_LEMMA] Theorem
|- !f a b.
(\x. f x - (f b - f a) / (b - a) * x) a =
(\x. f x - (f b - f a) / (b - a) * x) b
[ROLLE] Theorem
|- !f a b.
a < b /\ (f a = f b) /\ (!x. a <= x /\ x <= b ==> f contl x) /\
(!x. a < x /\ x < b ==> f differentiable x) ==>
?z. a < z /\ z < b /\ (f diffl 0) z
*)
end
HOL 4, Kananaskis-3