$$$everything.pvs everything : THEORY BEGIN IMPORTING top_derivative, top_sequences, top_limits, top_continuity END everything $$$inverse_continuous_functions.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properties of continuous functions [T1 -> T2] % % Applications of continuity_interval % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% inverse_continuous_functions [ T1, T2 : NONEMPTY_TYPE FROM real ] : THEORY BEGIN ASSUMING % BUG: T1_pred is not correctly expanded % connected_domain : ASSUMPTION % FORALL (x, y : T1), (z : real) : % x <= z AND z <= y IMPLIES T1_pred(z) connected_domain : ASSUMPTION FORALL (x, y : T1), (z : real) : x <= z AND z <= y IMPLIES (EXISTS (u : T1) : z = u) ENDASSUMING IMPORTING continuous_functions_props g : VAR { f : [T1 -> T2] | continuous(f) } %------------------------------------------------------------- % inverse of a continuous, bijective function is continuous %------------------------------------------------------------- inverse_incr : LEMMA bijective?[T1, T2](g) AND strict_increasing(g) IMPLIES continuous(inverse(g)) inverse_decr : LEMMA bijective?[T1, T2](g) AND strict_decreasing(g) IMPLIES continuous(inverse(g)) inverse_continuous : PROPOSITION bijective?[T1, T2](g) IMPLIES continuous(inverse(g)) END inverse_continuous_functions $$$inverse_continuous_functions.prf (|inverse_continuous_functions| (|inverse_incr| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "bijective?") (("" (EXPAND "continuous") (("" (SKOSIMP) (("" (DELETE -1) (("" (REWRITE "continuity_def[T2]") (("" (EXPAND "surjective?") (("" (INST-CP -1 "x0!1") (("" (SKOLEM!) (("" (CASE-REPLACE "inverse(g!1)(x0!1) = x!1") (("1" (DELETE -1) (("1" (SKOLEM!) (("1" (CASE "EXISTS (d : posreal) : FORALL (u : T1) : x0!1 - g!1(u) < d IMPLIES x!1 - u < epsilon!1") (("1" (CASE "EXISTS (d : posreal) : FORALL (u : T1) : g!1(u) - x0!1 < d IMPLIES u - x!1 < epsilon!1") (("1" (SKOSIMP*) (("1" (INST 1 "min(d!1, d!2)") (("1" (SKOSIMP) (("1" (INST -3 "x!2") (("1" (SKOLEM!) (("1" (CASE-REPLACE "inverse(g!1)(x!2) = x!3") (("1" (DELETE -1) (("1" (INST -1 "x!3") (("1" (INST -2 "x!3") (("1" (DELETE -5) (("1" (GRIND :EXCLUDE "min") NIL))))))))) ("2" (REWRITE "bijective_inverse") (("2" (ASSERT) NIL))))))))))))))) ("2" (DELETE -1 -2 2) (("2" (CASE "EXISTS (v : T1) : x!1 + epsilon!1 = v") (("1" (SKOLEM!) (("1" (EXPAND "strict_increasing") (("1" (INST-CP -3 "x!1" "v!1") (("1" (ASSERT) (("1" (ASSERT) (("1" (INST 1 "g!1(v!1) - x0!1") (("1" (SKOSIMP) (("1" (INST -4 "v!1" "u!1") (("1" (ASSERT) NIL))))))))))))))))) ("2" (INST 2 "1") (("2" (SKOSIMP) (("2" (LEMMA "connected_domain") (("2" (INST -1 "x!1" "u!1" "x!1 + epsilon!1") (("2" (ASSERT) NIL))))))))))))))) ("2" (DELETE -1 2) (("2" (CASE "EXISTS (v : T1) : x!1 - epsilon!1 = v") (("1" (SKOLEM!) (("1" (EXPAND "strict_increasing") (("1" (INST-CP -3 "v!1" "x!1") (("1" (ASSERT) (("1" (ASSERT) (("1" (INST 1 "x0!1 - g!1(v!1)") (("1" (SKOSIMP) (("1" (INST -4 "u!1" "v!1") (("1" (ASSERT) NIL))))))))))))))))) ("2" (INST 2 "1") (("2" (SKOSIMP) (("2" (LEMMA "connected_domain") (("2" (INST -1 "u!1" "x!1" "x!1 - epsilon!1") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (REWRITE "bijective_inverse") (("2" (ASSERT) NIL))))))))))))))))))))))))) (|inverse_decr| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "bijective?") (("" (EXPAND "continuous") (("" (SKOSIMP) (("" (DELETE -1) (("" (REWRITE "continuity_def[T2]") (("" (EXPAND "surjective?") (("" (INST-CP -1 "x0!1") (("" (SKOLEM!) (("" (CASE-REPLACE "inverse(g!1)(x0!1) = x!1") (("1" (DELETE -1) (("1" (SKOLEM!) (("1" (CASE "EXISTS (d : posreal) : FORALL (u : T1) : x0!1 - g!1(u) < d IMPLIES u - x!1 < epsilon!1") (("1" (CASE "EXISTS (d : posreal) : FORALL (u : T1) : g!1(u) - x0!1 < d IMPLIES x!1 - u < epsilon!1") (("1" (SKOSIMP*) (("1" (INST 1 "min(d!1, d!2)") (("1" (SKOSIMP) (("1" (INST -3 "x!2") (("1" (SKOLEM!) (("1" (CASE-REPLACE "inverse(g!1)(x!2) = x!3") (("1" (DELETE -1) (("1" (INST -1 "x!3") (("1" (INST -2 "x!3") (("1" (GRIND :EXCLUDE ("min" "strict_decreasing")) NIL))))))) ("2" (REWRITE "bijective_inverse") (("2" (ASSERT) NIL))))))))))))))) ("2" (DELETE -1 -2 2) (("2" (CASE "EXISTS (v : T1) : x!1 - epsilon!1 = v") (("1" (SKOLEM!) (("1" (EXPAND "strict_decreasing") (("1" (INST-CP -3 "v!1" "x!1") (("1" (ASSERT) (("1" (ASSERT) (("1" (INST 1 "g!1(v!1) - x0!1") (("1" (SKOSIMP) (("1" (INST -4 "u!1" "v!1") (("1" (ASSERT) NIL))))))))))))))))) ("2" (INST 2 "1") (("2" (SKOSIMP) (("2" (LEMMA "connected_domain") (("2" (INST -1 "u!1" "x!1" "x!1 - epsilon!1") (("2" (ASSERT) NIL))))))))))))))) ("2" (DELETE -1 2) (("2" (CASE "EXISTS (v : T1) : x!1 + epsilon!1 = v") (("1" (SKOLEM!) (("1" (EXPAND "strict_decreasing") (("1" (INST-CP -3 "x!1" "v!1") (("1" (ASSERT) (("1" (ASSERT) (("1" (INST 1 "x0!1 - g!1(v!1)") (("1" (SKOSIMP) (("1" (INST -4 "v!1" "u!1") (("1" (ASSERT) NIL))))))))))))))))) ("2" (INST 2 "1") (("2" (SKOSIMP) (("2" (LEMMA "connected_domain") (("2" (INST -1 "x!1" "u!1" "x!1 + epsilon!1") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (REWRITE "bijective_inverse") (("2" (ASSERT) NIL))))))))))))))))))))))))) (|inverse_continuous| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "bijective?") (("" (FLATTEN) (("" (USE "inj_monotone[T1]") (("1" (GROUND) (("1" (REWRITE "inverse_incr") NIL) ("2" (REWRITE "inverse_decr") NIL) ("3" (EXPAND "injective?") (("3" (PROPAX) NIL))))) ("2" (LEMMA "connected_domain") (("2" (SKOSIMP) (("2" (INST -1 "x!1" "y!1" "z!1") (("2" (ASSERT) NIL)))))))))))))))))) $$$restriction_continuous.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Restriction of continuous functions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% restriction_continuous[T1 : TYPE FROM real ] : THEORY BEGIN IMPORTING continuous_functions f : VAR [real -> real] restrict_continuous : PROPOSITION continuous(f) IMPLIES continuous[T1](f) END restriction_continuous restriction_continuous2[T1, T2 : TYPE FROM real] : theory BEGIN ASSUMING sub_domain : ASSUMPTION FORALL (x : T1) : EXISTS (y : T2) : x = y ENDASSUMING IMPORTING continuous_functions f : VAR [T2 -> real] sub_dom : LEMMA FORALL (u : T1) : T2_pred(u) restrict2(f) : [T1 -> real] = LAMBDA (u : T1) : f(u) CONVERSION restrict2 restrict_continuous2 : PROPOSITION continuous(f) IMPLIES continuous[T1](f) END restriction_continuous2 $$$restriction_continuous.prf (|restriction_continuous| (|restrict_continuous| "" (SKOSIMP) (("" (EXPAND "continuous") (("" (SKOLEM!) (("" (INST?) (("" (REWRITE "continuity_def[real]") (("" (REWRITE "continuity_def[T1]") (("" (EXPAND "restrict") (("" (SKOLEM!) (("" (INST -1 "epsilon!1") (("" (SKOLEM!) (("" (INST 1 "delta!1") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))))))))))))(|restriction_continuous2| (|sub_dom| "" (LEMMA "sub_domain") (("" (GRIND) NIL))) (|restrict2_TCC1| "" (LEMMA "sub_dom") (("" (PROPAX) NIL))) (|restrict_continuous2| "" (SKOSIMP) (("" (AUTO-REWRITE "sub_dom") (("" (EXPAND "continuous") (("" (SKOLEM!) (("" (INST?) (("" (REWRITE "continuity_def[T2]") (("" (REWRITE "continuity_def[T1]") (("" (EXPAND "restrict2") (("" (SKOLEM!) (("" (INST -1 "epsilon!1") (("" (SKOLEM!) (("" (INST 1 "delta!1") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL)))))))))))))))))))))))))))))) $$$composition_continuous.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Composition of continuous functions % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% composition_continuous [ T1, T2 : TYPE FROM real ] : THEORY BEGIN IMPORTING continuous_functions, real_fun_props f : VAR [T1 -> T2] g : VAR [T2 -> real] x0 : VAR T1 F : VAR { E : setof[real] | subset?(E, T1_pred) } composition_continuous1 : PROPOSITION continuous(f, x0) AND continuous(g, f(x0)) IMPLIES continuous(g o f, x0) composition_continuous2 : PROPOSITION continuous(f, F) AND continuous(g, Im(f, F)) IMPLIES continuous(g o f, F) composition_continuous3 : PROPOSITION continuous(f) AND continuous(g) IMPLIES continuous(g o f) END composition_continuous $$$composition_continuous.prf (|composition_continuous| (|composition_continuous1| "" (GRIND :DEFS NIL :REWRITES ("continuity_def[T1]" "continuity_def[T2]" "o") :IF-MATCH NIL) (("" (INST? -5) (("" (SKOLEM!) (("" (INST -4 "delta!1") (("" (SKOLEM!) (("" (INST 1 "delta!2") (("" (SKOSIMP) (("" (INST -4 "x!1") (("" (INST -5 "f!1(x!1)") (("" (ASSERT) NIL))))))))))))))))))) (|composition_continuous2_TCC1| "" (SKOLEM-TYPEPRED) (("" (FLATTEN) (("" (DELETE -2) (("" (GRIND) NIL))))))) (|composition_continuous2| "" (GRIND :EXCLUDE ("convergence") :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) (("" (DELETE -1 -2) (("" (INST?) (("" (INST?) (("1" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("1" (INST? -6) (("1" (SKOLEM!) (("1" (INST -4 "delta!1") (("1" (SKOLEM!) (("1" (INST 1 "delta!2") (("1" (SKOSIMP) (("1" (INST -4 "x!1") (("1" (INST -6 "f!1(x!1)") (("1" (ASSERT) (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))))))))))) ("2" (INST?) (("2" (ASSERT) NIL))))))))))))))) (|composition_continuous3| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2[T1]")) (("" (REWRITE "composition_continuous2") (("1" (REWRITE "continuity_subset2[T2]") (("1" (DELETE -1 -2 2 3) (("1" (GRIND) NIL))))) ("2" (REWRITE "subset_reflexive") NIL)))))) $$$top_continuity.pvs top_continuity : THEORY BEGIN IMPORTING continuous_functions, composition_continuous, restriction_continuous, restriction_continuous2, continuous_functions_props, inverse_continuous_functions END top_continuity $$$top_limits.pvs top_limits : THEORY BEGIN IMPORTING limit_of_functions, limit_of_composition END top_limits $$$limit_of_composition.pvs limit_of_composition [ T1, T2 : TYPE FROM real ] : THEORY BEGIN IMPORTING limit_of_functions, continuous_functions[T2] f : VAR [T1 -> T2] g : VAR [T2 -> real] x, y : VAR real z : VAR T2 l : VAR real adherence_lemma : LEMMA convergence(f, x, y) IMPLIES adh[T2](fullset[real])(y) adherence_lemma2 : LEMMA convergent(f, x) IMPLIES adh[T2](fullset[real])(lim(f, x)) convergence_composition : PROPOSITION convergence(f, x, y) AND convergence(g, y, l) IMPLIES convergence(g o f, x, l) convergent_composition : PROPOSITION convergent(f, x) AND convergent(g, lim(f, x)) IMPLIES convergent(g o f, x) limit_composition : PROPOSITION convergent(f, x) AND convergent(g, lim(f, x)) IMPLIES lim(g o f, x) = lim(g, lim(f, x)) convergence_comp_continuous : PROPOSITION convergence(f, x, z) AND continuous(g, z) IMPLIES convergence(g o f, x, g(z)) convergent_comp_continuous : PROPOSITION convergent(f, x) AND T2_pred(lim(f, x)) AND continuous(g, lim(f, x)) IMPLIES convergent(g o f, x) limit_comp_continuous : PROPOSITION convergent(f, x) AND T2_pred(lim(f, x)) AND continuous(g, lim(f, x)) IMPLIES lim(g o f, x) = g(lim(f, x)) END limit_of_composition $$$limit_of_composition.prf (|limit_of_composition| (|adherence_lemma| "" (GRIND :EXCLUDE ("convergence" "abs") :REWRITES ("adh[T1]" "adh[T2]" "convergence_def[T1]") :IF-MATCH NIL) (("" (INST? -6) (("" (SKOLEM!) (("" (INST -5 "delta!1") (("" (SKOLEM!) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|adherence_lemma2| "" (SKOSIMP) (("" (USE "lim_fun_lemma[T1]") (("" (FORWARD-CHAIN "adherence_lemma") NIL NIL)) NIL)) NIL) (|convergence_composition| "" (GRIND :EXCLUDE ("convergence" "abs" "adh") :REWRITES ("convergence_def[T2]" "convergence_def[T1]") :IF-MATCH NIL) (("" (DELETE -1 -2 -3 -4 -5 -6 -8) (("" (INST -2 "epsilon!1") (("" (SKOLEM!) (("" (INST -1 "delta!1") (("" (SKOLEM!) (("" (INST 1 "delta!2") (("" (SKOSIMP) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergent_composition| "" (LEMMA "convergence_composition") (("" (GRIND :DEFS NIL :REWRITES ("convergent[T1]" "convergent[T2]")) (("" (REWRITE "lim_fun_def[T1]" :DIR RL) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|limit_composition_TCC1| "" (SKOSIMP) (("" (REWRITE "convergent_composition") NIL NIL)) NIL) (|limit_composition| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "adherence_lemma2" "convergent_composition") (("" (REWRITE "lim_fun_def[T1]") (("" (USE "lim_fun_lemma[T2]") (("" (USE "lim_fun_lemma[T1]" ("f" "f!1")) (("" (FORWARD-CHAIN "convergence_composition") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_comp_continuous| "" (SKOSIMP) (("" (EXPAND "continuous") (("" (FORWARD-CHAIN "convergence_composition") NIL NIL)) NIL)) NIL) (|convergent_comp_continuous| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "lim_fun_lemma[T1]") (("" (USE "convergence_comp_continuous" ("z" "lim(f!1, x!1)")) (("" (ASSERT) (("" (EXPAND "convergent" +) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_comp_continuous_TCC1| "" (SKOSIMP) (("" (REWRITE "convergent_comp_continuous") NIL NIL)) NIL) (|limit_comp_continuous| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "convergent_comp_continuous") (("" (REWRITE "lim_fun_def[T1]") (("" (USE "lim_fun_lemma[T1]") (("" (FORWARD-CHAIN "convergence_comp_continuous") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$chain_rule.pvs chain_rule [ T1, T2 : TYPE FROM real ] : THEORY BEGIN ASSUMING connected_domain1 : ASSUMPTION FORALL (x, y : T1), (z : real) : x <= z AND z <= y IMPLIES T1_pred(z) not_one_element1 : ASSUMPTION FORALL (x : T1) : EXISTS (y : T1) : x /= y connected_domain2 : ASSUMPTION FORALL (x, y : T2), (z : real) : x <= z AND z <= y IMPLIES T2_pred(z) not_one_element2 : ASSUMPTION FORALL (x : T2) : EXISTS (y : T2) : x /= y ENDASSUMING IMPORTING derivative_props, limit_of_composition f : VAR [T1 -> T2] g : VAR [T2 -> real] x : VAR T1 DF, DG : VAR real chain_rule : LEMMA convergence(NQ(f, x), 0, DF) AND convergence(NQ(g, f(x)), 0, DG) IMPLIES convergence(NQ(g o f, x), 0, DG * DF) composition_derivable : LEMMA derivable(f, x) AND derivable(g, f(x)) IMPLIES derivable(g o f, x) composition_derivable2 : LEMMA derivable(f) AND derivable(g) IMPLIES derivable(g o f) deriv_composition : LEMMA derivable(f, x) AND derivable(g, f(x)) IMPLIES deriv(g o f, x) = deriv(g, f(x)) * deriv(f, x) ff : VAR { f | derivable(f) } gg : VAR { g | derivable(g) } deriv_comp_fun : LEMMA deriv(gg o ff) = (deriv(gg) o ff) * deriv(ff) END chain_rule $$$chain_rule.prf (|chain_rule| (|chain_rule_TCC1| "" (LEMMA "connected_domain1") (("" (PROPAX) NIL NIL)) NIL) (|chain_rule_TCC2| "" (LEMMA "not_one_element1") (("" (PROPAX) NIL NIL)) NIL) (|chain_rule_TCC3| "" (SKOSIMP) (("" (LEMMA "connected_domain2") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|chain_rule_TCC4| "" (SKOSIMP) (("" (LEMMA "not_one_element2") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|chain_rule| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC[T1]" "deriv_TCC[T2]" "adherence_fullset[T1]" "adherence_fullset[T2]" "not_one_element1" "not_one_element2" "connected_domain1" "connected_domain2") (("" (USE "derivative_equivalence1[T1]") (("" (GROUND) (("" (FORWARD-CHAIN "derivable_continuous[T1]") (("" (DELETE -2 -3 -4) (("" (EXPAND "continuous") (("" (REWRITE "derivative_equivalence2[T1]") (("" (REWRITE "derivative_equivalence2[T1]") (("" (REWRITE "derivative_equivalence2[T2]") (("" (SKOSIMP*) (("" (INST + "DG!1 * phi!1 + DF!1 * (phi!2 o f!1) + phi!1 * (phi!2 o f!1)") (("" (GROUND) (("1" (USE "convergence_composition" ("f" "f!1" "g" "phi!2" "x" "x!1")) (("1" (ASSERT) (("1" (DELETE -4 -5 -6) (("1" (AUTO-REWRITE-THEORY "limit_of_functions[T1]" :EXCLUDE ("convergence" "convergence_def" "convergent" "convergent_in_domain" "lim" "limit_in_domain" "lim_fun_lemma" "lim_fun_def") :ALWAYS? T) (("1" (GRIND :DEFS NIL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -4) (("2" (SKOLEM!) (("2" (INST -1 "y!1") (("2" (INST -2 "f!1(y!1)") (("2" (GRIND) (("2" (CASE-REPLACE "f!1(y!1) * phi!2(f!1(y!1)) + f!1(y!1) * DG!1 - f!1(x!1) * DG!1 - phi!2(f!1(y!1)) * f!1(x!1) = (f!1(y!1) - f!1(x!1)) * (phi!2(f!1(y!1)) + DG!1)") (("1" (REPLACE -2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -1 -2 2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|composition_derivable_TCC1| "" (SKOSIMP) (("" (LEMMA "connected_domain2") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|composition_derivable_TCC2| "" (SKOSIMP) (("" (LEMMA "not_one_element2") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|composition_derivable| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "chain_rule") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|composition_derivable2_TCC1| "" (SKOSIMP) (("" (LEMMA "connected_domain2") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|composition_derivable2_TCC2| "" (SKOSIMP) (("" (LEMMA "not_one_element2") (("" (PROPAX) NIL NIL)) NIL)) NIL) (|composition_derivable2| "" (EXPAND "derivable") (("" (SKOSIMP*) (("" (REWRITE "composition_derivable") (("1" (INST?) NIL NIL) ("2" (INST? -2) NIL NIL)) NIL)) NIL)) NIL) (|deriv_composition_TCC1| "" (SKOSIMP) (("" (REWRITE "composition_derivable") NIL NIL)) NIL) (|deriv_composition| "" (SKOSIMP) (("" (FORWARD-CHAIN "composition_derivable") (("" (AUTO-REWRITE "deriv_TCC[T1]" "deriv_TCC[T2]" ("deriv[T1]" "derivable[T1]" "deriv[T2]" "derivable[T2]") ("lim_fun_lemma[(A[T1](x!1))]" "lim_fun_lemma[(A[T2](f!1(x!1)))]")) (("" (ASSERT) (("" (REWRITE "lim_fun_def[(A[T1](x!1))]") (("" (REWRITE "chain_rule") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|gg_TCC1| "" (LEMMA "connected_domain2") (("" (PROPAX) NIL NIL)) NIL) (|gg_TCC2| "" (LEMMA "not_one_element2") (("" (PROPAX) NIL NIL)) NIL) (|deriv_comp_fun_TCC1| "" (SKOSIMP) (("" (REWRITE "composition_derivable2") NIL NIL)) NIL) (|deriv_comp_fun| "" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (EXPAND "derivable") (("" (AUTO-REWRITE "composition_derivable2") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "*") (("" (EXPAND "o" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_composition") (("1" (INST? -1) NIL NIL) ("2" (INST? -2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$monotone_subsequence.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % From any sequence one can extract % % an increasing or a decreasing sub-sequence % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% monotone_subsequence : THEORY BEGIN IMPORTING sequence_props u, s : VAR sequence[real] i, j, n : VAR nat %--------------------------------------------------- % If all the suffixes of v have a minimal element % then v contains an increasing sub-sequence %--------------------------------------------------- has_minimum(u, n) : bool = EXISTS i : n <= i AND FORALL j : n <= j IMPLIES u(i) <= u(j) minimum_prefix : LEMMA EXISTS i : FORALL j : j <= n IMPLIES u(i) <= u(j) minimum_suffix : LEMMA has_minimum(u, n) IMPLIES has_minimum(u, 0) v : VAR { u | FORALL n : has_minimum(u, n) } %--- a minimum of the elements n, n+1, .... ---% mini(v, n) : nat = epsilon! i : n <= i AND FORALL j : n <= j IMPLIES v(i) <= v(j) min_prop : LEMMA n <= mini(v, n) AND FORALL j : n <= j IMPLIES v(mini(v, n)) <= v(j) min_prop1 : COROLLARY n <= mini(v, n) min_prop2 : COROLLARY n <= i IMPLIES v(mini(v, n)) <= v(i) %--- subsequence ---% h(v)(i) : RECURSIVE nat = IF i = 0 THEN mini(v, 0) ELSE mini(v, h(v)(i - 1) + 1) ENDIF MEASURE i hseq(v) : sequence[real] = LAMBDA i : v(h(v)(i)) h_increasing : LEMMA strict_increasing(h(v)) hseq_extraction : LEMMA subseq(hseq(v), v) hseq_increasing : LEMMA increasing(hseq(v)) %------------------------------------------------------ % If a sequence has no minimal element it contains a % (strictly) decreasing sub-sequence %------------------------------------------------------ w : VAR { u | not has_minimum(u, 0) } no_minimum : LEMMA not has_minimum(w, n) pick(w, n) : nat = epsilon! i : n <= i AND w(i) < w(n) pick_prop : LEMMA n <= pick(w, n) AND w(pick(w, n)) < w(n) pick_prop1 : COROLLARY n < pick(w, n) pick_prop2 : COROLLARY w(pick(w, n)) < w(n) %--- subsequence ---% g(w)(i) : RECURSIVE nat = IF i = 0 THEN pick(w, 0) ELSE pick(w, g(w)(i - 1)) ENDIF MEASURE i gseq(w) : sequence[real] = LAMBDA i : w(g(w)(i)) g_increasing : LEMMA strict_increasing(g(w)) gseq_extraction : LEMMA subseq(gseq(w), w) gseq_decreasing : LEMMA strict_decreasing(gseq(w)) %------------------------ % Suffix starting at n %------------------------ suffix(u, n) : sequence[real] = LAMBDA i : u(n+i) suffix_subseq : LEMMA subseq(suffix(u, n), u) suffix_hasmin : LEMMA has_minimum(suffix(u, n), 0) IFF has_minimum(u, n) %---------------- % Main theorem %---------------- monotone_subsequence : THEOREM EXISTS s : subseq(s, u) AND (increasing(s) OR decreasing(s)) END monotone_subsequence $$$monotone_subsequence.prf (|monotone_subsequence| (|minimum_prefix| "" (SKOLEM + (_ "u!1")) (("" (INDUCT "n") (("1" (REDUCE) NIL NIL) ("2" (SKOSIMP*) (("2" (INST + "IF u!1(i!1) <= u!1(j!1+1) THEN i!1 ELSE j!1+1 ENDIF") (("2" (SKOSIMP) (("2" (INST - "j!2") (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|minimum_suffix| "" (GRIND :IF-MATCH NIL) (("" (USE "minimum_prefix" ("n" "n!1")) (("" (SKOLEM!) (("" (INST + "IF u!1(i!2) <= u!1(i!1) THEN i!2 ELSE i!1 ENDIF") (("" (SKOLEM!) (("" (INST - "j!1") (("" (INST - "j!1") (("" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|min_prop| "" (SKOLEM!) (("" (NAME-REPLACE "m" "mini(v!1, n!1)" :HIDE? NIL) (("" (EXPAND "mini") (("" (USE "epsilon_ax[nat]") (("" (BETA) (("" (REPLACE -2) (("" (DELETE -2) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (TYPEPRED "v!1") (("2" (INST?) (("2" (EXPAND "has_minimum") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|min_prop1| "" (SKOLEM!) (("" (USE "min_prop") (("" (FLATTEN) NIL NIL)) NIL)) NIL) (|min_prop2| "" (SKOSIMP) (("" (USE "min_prop") (("" (REDUCE) NIL NIL)) NIL)) NIL) (|h_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|h_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL))) (|h_increasing| "" (SKOLEM!) (("" (REWRITE "strict_incr_condition") (("" (SKOLEM!) (("" (EXPAND "h" 1 2) (("" (USE "min_prop1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|hseq_extraction| "" (SKOLEM!) (("" (EXPAND* "hseq" "subseq") (("" (INST + "h(v!1)") (("1" (ASSERT) NIL NIL) ("2" (REWRITE "h_increasing") NIL NIL)) NIL)) NIL)) NIL) (|hseq_increasing| "" (SKOLEM!) (("" (REWRITE "incr_condition") (("" (SKOLEM!) (("" (EXPAND "hseq") (("" (NAME-REPLACE "k" "h(v!1)(i!1)" :HIDE? NIL) (("" (EXPAND "h" -1) (("" (SMASH) (("1" (USE "min_prop2" ("i" "h(v!1)(1 + i!1)")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (USE "min_prop2" ("i" "h(v!1)(1 + i!1)")) (("2" (ASSERT) (("2" (USE "h_increasing") (("2" (EXPAND "strict_increasing") (("2" (INST - "i!1 - 1" "1 + i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|no_minimum| "" (SKOLEM-TYPEPRED) (("" (FORWARD-CHAIN "minimum_suffix") NIL NIL)) NIL) (|pick_prop| "" (SKOLEM!) (("" (NAME-REPLACE "k" "pick(w!1, n!1)" :HIDE? NIL) (("" (EXPAND "pick") (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (i : nat) : n!1 <= i AND w!1(i) < w!1(n!1)")) (("" (REPLACE -2) (("" (ASSERT) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (DELETE -1 2) (("2" (USE "no_minimum" ("n" "n!1")) (("2" (EXPAND "has_minimum") (("2" (INST?) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|pick_prop1| "" (SKOLEM!) (("" (USE "pick_prop") (("" (GROUND) NIL))))) (|pick_prop2| "" (SKOLEM!) (("" (USE "pick_prop") (("" (FLATTEN) (("" (PROPAX) NIL))))))) (|g_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|g_TCC2| "" (ASSERT) NIL) (|g_increasing| "" (SKOLEM!) (("" (REWRITE "strict_incr_condition") (("" (SKOLEM!) (("" (EXPAND "g" 1 2) (("" (REWRITE "pick_prop1") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|gseq_extraction| "" (SKOLEM!) (("" (EXPAND* "subseq" "gseq") (("" (INST + "g(w!1)") (("1" (ASSERT) NIL NIL) ("2" (REWRITE "g_increasing") NIL NIL)) NIL)) NIL)) NIL) (|gseq_decreasing| "" (SKOLEM!) (("" (REWRITE "strict_decr_condition") (("" (SKOLEM!) (("" (EXPAND "gseq") (("" (EXPAND "g" 1 1) (("" (REWRITE "pick_prop2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|suffix_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST + "LAMBDA i : i+n!1") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|suffix_hasmin| "" (GRIND :IF-MATCH NIL) (("1" (INST? +) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST - "j!1 - n!1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST + "i!1 - n!1") (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|monotone_subsequence| "" (SKOSIMP) (("" (AUTO-REWRITE "strict_decr_to_decr[nat]" "gseq_decreasing") (("" (CASE "FORALL n : has_minimum(u!1, n)") (("1" (ASSERT) (("1" (INST + "hseq(u!1)") (("1" (GROUND) (("1" (REWRITE "hseq_extraction") NIL NIL) ("2" (REWRITE "hseq_increasing") NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REWRITE "suffix_hasmin" :DIR RL) (("2" (ASSERT) (("2" (INST + "gseq(suffix(u!1, n!1))") (("2" (GROUND) (("2" (USE "gseq_extraction") (("2" (USE "suffix_subseq") (("2" (FORWARD-CHAIN "transitive_subseq") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$real_fun_props.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Defines several properties of functions [T -> real] % % -> increasing/decreasing functions % % -> upper/lower bound % % -> maximum/minimum of a function % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_fun_props [T : TYPE FROM real] : THEORY BEGIN IMPORTING real_fun_ops f : VAR [T -> real] x, y : VAR T a, z : VAR real E : VAR setof[real] %--------------------------------------- % Increasing and decreasing functions %--------------------------------------- increasing(f) : bool = FORALL x, y : x <= y IMPLIES f(x) <= f(y) decreasing(f) : bool = FORALL x, y : x <= y IMPLIES f(y) <= f(x) strict_increasing(f) : bool = FORALL x, y : x < y IMPLIES f(x) < f(y) strict_decreasing(f) : bool = FORALL x, y : x < y IMPLIES f(y) < f(x) %------------------- % Easy properties %------------------- strict_incr_to_incr : LEMMA strict_increasing(f) IMPLIES increasing(f) strict_decr_to_decr : LEMMA strict_decreasing(f) IMPLIES decreasing(f) incr_opposite : LEMMA increasing(- f) IFF decreasing(f) decr_opposite : LEMMA decreasing(- f) IFF increasing(f) strict_incr_opposite : LEMMA strict_increasing(- f) IFF strict_decreasing(f) strict_decr_opposite : LEMMA strict_decreasing(- f) IFF strict_increasing(f) %----------------------- % Constant functions %----------------------- constant(f) : bool = FORALL x, y : f(x) = f(y) constant_to_incr : LEMMA constant(f) IMPLIES increasing(f) constant_to_decr : LEMMA constant(f) IMPLIES decreasing(f) constant_opposite : LEMMA constant(- f) IFF constant(f) %-------------------------------------------------------- % Image of a function % redefined from function_image to avoid conversions %-------------------------------------------------------- Im(f) : setof[real] = { z | EXISTS x : z = f(x) } Im(f, E) : setof[real] = { z | EXISTS x : E(x) AND z = f(x) } %--------------------- % Bounded functions %--------------------- bounded_above?(f) : bool = EXISTS a: FORALL x: f(x) <= a bounded_below?(f) : bool = EXISTS a: FORALL x: a <= f(x) bounded?(f) : bool = bounded_above?(f) AND bounded_below?(f) %------------------------ % Relation to opposite %------------------------ bounded_above_opposite : LEMMA bounded_above?(- f) IFF bounded_below?(f) bounded_below_opposite : LEMMA bounded_below?(- f) IFF bounded_above?(f) %----------------------------------- % Maximum / minimum of a function %----------------------------------- is_maximum(x, f) : bool = FORALL y : f(y) <= f(x) is_minimum(x, f) : bool = FORALL y : f(x) <= f(y) %------------------------ % Relation with bounds %------------------------ max_bounded : LEMMA is_maximum(x, f) IMPLIES bounded_above?(f) min_bounded : LEMMA is_minimum(x, f) IMPLIES bounded_below?(f) %--------------------------- % Relation with opposites %--------------------------- max_opposite : LEMMA is_maximum(x, - f) IFF is_minimum(x, f) min_opposite : LEMMA is_minimum(x, - f) IFF is_maximum(x, f) END real_fun_props $$$real_fun_props.prf (|real_fun_props| (|strict_incr_to_incr| "" (GRIND :IF-MATCH NIL) (("" (INST -3 "x!1" "y!1") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|strict_decr_to_decr| "" (GRIND :IF-MATCH NIL) (("" (INST -3 "x!1" "y!1") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|incr_opposite| "" (GRIND) NIL NIL) (|decr_opposite| "" (GRIND) NIL NIL) (|strict_incr_opposite| "" (GRIND) NIL NIL) (|strict_decr_opposite| "" (GRIND) NIL NIL) (|constant_to_incr| "" (GRIND :IF-MATCH ALL) NIL NIL) (|constant_to_decr| "" (GRIND :IF-MATCH ALL) NIL NIL) (|constant_opposite| "" (GRIND :IF-MATCH ALL) NIL NIL) (|bounded_above_opposite| "" (GRIND :IF-MATCH NIL) (("1" (INST + "-a!1") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST + "-a!1") (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_below_opposite| "" (GRIND :IF-MATCH NIL) (("1" (INST + "-a!1") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST + "-a!1") (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|max_bounded| "" (GRIND :IF-MATCH NIL) (("" (INST? +) NIL NIL)) NIL) (|min_bounded| "" (GRIND :IF-MATCH NIL) (("" (INST? +) NIL NIL)) NIL) (|max_opposite| "" (GRIND :IF-MATCH NIL) (("1" (INST -3 "y!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|min_opposite| "" (AUTO-REWRITE "negneg_function[T]") (("" (SKOLEM!) (("" (REWRITE "max_opposite" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) $$$real_fun_supinf.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Sup and Inf of bounded functions % % (require nonempty domain) % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_fun_supinf [ T : NONEMPTY_TYPE FROM real ] : THEORY BEGIN IMPORTING real_fun_props, real_facts f : VAR [T -> real] x : VAR T a : VAR real epsilon : VAR posreal %--------------- % Sup and Inf %--------------- g : VAR { f | bounded_above?(f) } h : VAR { f | bounded_below?(f) } nonempty_image: JUDGEMENT Im(f) HAS_TYPE (nonempty?[real]) bounded_above_image: JUDGEMENT Im(g) HAS_TYPE (bounded_above?) bounded_below_image: JUDGEMENT Im(h) HAS_TYPE (bounded_below?) sup(g) : real = lub(Im(g)) inf(h) : real = glb(Im(h)) %-------------- % Properties %-------------- supfun_is_bound : LEMMA g(x) <= sup(g) supfun_is_sup : LEMMA FORALL epsilon : EXISTS x : sup(g) - epsilon < g(x) supfun_is_sup2 : LEMMA sup(g) <= a IFF FORALL x : g(x) <= a inffun_is_bound : LEMMA inf(h) <= h(x) inffun_is_inf : LEMMA FORALL epsilon : EXISTS x : h(x) < inf(h) + epsilon inffun_is_inf2 : LEMMA a <= inf(h) IFF FORALL x : a <= h(x) supfun_opposite : LEMMA sup(- h) = - inf(h) inffun_opposite : LEMMA inf(- g) = - sup(g) %-------------------------------------- % Relations with maximum and minimum %-------------------------------------- max_upper_bound : LEMMA is_maximum(x, f) IFF bounded_above?(f) AND sup(f) = f(x) min_lower_bound : LEMMA is_minimum(x, f) IFF bounded_below?(f) AND inf(f) = f(x) END real_fun_supinf $$$real_fun_supinf.prf (|real_fun_supinf| (|nonempty_image| "" (GRIND) (("" (INST - "f!1(epsilon! x: true)") (("" (INST?) NIL NIL)) NIL)) NIL) (|bounded_above_image| "" (GRIND :IF-MATCH NIL) (("" (INST + "a!1") (("" (REDUCE :IF-MATCH NIL) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|bounded_below_image| "" (GRIND :IF-MATCH NIL) (("" (INST + "a!1") (("" (REDUCE :IF-MATCH NIL) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|supfun_is_bound| "" (SKOLEM!) (("" (EXPAND "sup") (("" (REWRITE "lub_is_bound") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|supfun_is_sup| "" (SKOSIMP) (("" (EXPAND "sup") (("" (USE "adherence_sup") (("" (AUTO-REWRITE "Im") (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|supfun_is_sup2| "" (SKOLEM!) (("" (EXPAND "sup") (("" (REWRITE "lub_is_lub") (("" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|inffun_is_bound| "" (SKOLEM!) (("" (EXPAND "inf") (("" (REWRITE "glb_is_bound") (("" (DELETE 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|inffun_is_inf| "" (SKOSIMP) (("" (EXPAND "inf") (("" (USE "adherence_inf") (("" (AUTO-REWRITE "Im") (("" (APPLY (THEN (REDUCE :IF-MATCH NIL) (INST?) (ASSERT))) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|inffun_is_inf2| "" (SKOLEM!) (("" (EXPAND "inf") (("" (REWRITE "glb_is_glb") (("" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (INST?) NIL NIL)) NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|supfun_opposite_TCC1| "" (SKOLEM!) (("" (REWRITE "bounded_above_opposite[T]") NIL NIL)) NIL) (|supfun_opposite| "" (SKOLEM!) (("" (AUTO-REWRITE "supfun_opposite_TCC1" "-") (("" (USE "supfun_is_sup2") (("" (USE "inffun_is_inf2" ("a" "- sup(- h!1)")) (("" (GROUND) (("1" (SKOLEM!) (("1" (USE "inffun_is_bound") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (USE "supfun_is_bound" ("g" "-h!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inffun_opposite_TCC1| "" (SKOLEM!) (("" (REWRITE "bounded_below_opposite[T]") NIL NIL)) NIL) (|inffun_opposite| "" (SKOLEM!) (("" (AUTO-REWRITE "inffun_opposite_TCC1" "-") (("" (USE "inffun_is_inf2") (("" (USE "supfun_is_sup2" ("a" "- inf(- g!1)")) (("" (GROUND) (("1" (SKOLEM!) (("1" (USE "supfun_is_bound") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (USE "inffun_is_bound" ("h" "-g!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|max_upper_bound| "" (SKOLEM!) (("" (SPLIT) (("1" (FLATTEN) (("1" (FORWARD-CHAIN "max_bounded[T]") (("1" (ASSERT) (("1" (USE "supfun_is_bound") (("1" (EXPAND "is_maximum") (("1" (USE "supfun_is_sup2" ("g" "f!1")) (("1" (GROUND) NIL))))))))))))) ("2" (FLATTEN) (("2" (ASSERT) (("2" (EXPAND "is_maximum") (("2" (REPLACE -2 + RL) (("2" (LEMMA "supfun_is_bound" ("g" "f!1")) (("2" (PROPAX) NIL))))))))))))))) (|min_lower_bound| "" (SKOLEM!) (("" (SPLIT) (("1" (FLATTEN) (("1" (FORWARD-CHAIN "min_bounded[T]") (("1" (ASSERT) (("1" (USE "inffun_is_bound") (("1" (EXPAND "is_minimum") (("1" (USE "inffun_is_inf2" ("h" "f!1")) (("1" (GROUND) NIL))))))))))))) ("2" (FLATTEN) (("2" (ASSERT) (("2" (EXPAND "is_minimum") (("2" (REPLACE -2 + RL) (("2" (LEMMA "inffun_is_bound" ("h" "f!1")) (("2" (PROPAX) NIL)))))))))))))))) $$$sequence_props.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Properties of real sequences % % -> condition for increasing / decreasing % % -> subsequences % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% sequence_props : THEORY BEGIN IMPORTING real_fun_supinf u, v, w : VAR sequence[real] i, j : VAR nat a, x : VAR real %-------------------------------------------------- % Conditions for increasing/decreasing sequences %-------------------------------------------------- incr_condition : LEMMA increasing(u) IFF FORALL i : u(i) <= u(i+1) decr_condition : LEMMA decreasing(u) IFF FORALL i : u(i+1) <= u(i) strict_incr_condition : LEMMA strict_increasing(u) IFF FORALL i : u(i) < u(i+1) strict_decr_condition : LEMMA strict_decreasing(u) IFF FORALL i : u(i+1) < u(i) %------------------------------------------------------- % Increasing sequences of natural numbers % used for extracting a sub-sequence from a sequence %------------------------------------------------------- extraction : TYPE = { f : [nat -> nat] | strict_increasing(f) } f, g : VAR extraction extract_incr1 : LEMMA f(i) < f(j) IFF i < j extract_incr2 : LEMMA i <= j IMPLIES f(i) <= f(j) extract_incr3 : LEMMA i <= f(i) unbounded_extract1 : LEMMA EXISTS j : i <= f(j) unbounded_extract2 : LEMMA EXISTS j : i < f(j) extract_composition : LEMMA strict_increasing(g o f) %----------------- % Sub-sequences %----------------- subseq(u, v) : bool = EXISTS f : FORALL i : u(i) = v(f(i)) reflexive_subseq : LEMMA subseq(u, u) transitive_subseq : LEMMA subseq(u, v) AND subseq(v, w) IMPLIES subseq(u, w) %----------------------------------------- % Properties inherited by subsequences %----------------------------------------- incr_subseq : LEMMA increasing(v) AND subseq(u, v) IMPLIES increasing(u) decr_subseq : LEMMA decreasing(v) AND subseq(u, v) IMPLIES decreasing(u) strict_incr_subseq : LEMMA strict_increasing(v) AND subseq(u, v) IMPLIES strict_increasing(u) strict_decr_subseq : LEMMA strict_increasing(v) AND subseq(u, v) IMPLIES strict_increasing(u) bounded_above_subseq : LEMMA bounded_above?(v) AND subseq(u, v) IMPLIES bounded_above?(u) bounded_below_subseq : LEMMA bounded_below?(v) AND subseq(u, v) IMPLIES bounded_below?(u) bounded_subseq : LEMMA bounded?(v) AND subseq(u, v) IMPLIES bounded?(u) END sequence_props $$$sequence_props.prf (|sequence_props| (|incr_condition| "" (SKOLEM!) (("" (EXPAND "increasing") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|decr_condition| "" (SKOLEM!) (("" (EXPAND "decreasing") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|strict_incr_condition| "" (SKOLEM!) (("" (EXPAND "strict_increasing") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|strict_decr_condition| "" (SKOLEM!) (("" (EXPAND "strict_decreasing") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|extract_incr1| "" (GRIND :IF-MATCH NIL) (("1" (INST -1 "j!1" "i!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|extract_incr2| "" (SKOSIMP) (("" (USE "extract_incr1" ("i" "j!1" "j" "i!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|extract_incr3| "" (SKOLEM 1 ("f!1" _)) (("" (INDUCT "i") (("1" (ASSERT) NIL NIL) ("2" (SKOSIMP) (("2" (USE "extract_incr1" ("i" "j!1" "j" "j!1+1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|unbounded_extract1| "" (SKOLEM!) (("" (INST?) (("" (REWRITE "extract_incr3") NIL NIL)) NIL)) NIL) (|unbounded_extract2| "" (SKOSIMP) (("" (USE "unbounded_extract1" ("f" "f!1")) (("" (SKOLEM!) (("" (INST 1 "j!1+1") (("" (USE "extract_incr1" ("i" "j!1" "j" "j!1+1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|extract_composition| "" (AUTO-REWRITE "strict_increasing" "o") (("" (GRIND) NIL NIL)) NIL) (|reflexive_subseq| "" (SKOLEM!) (("" (EXPAND "subseq") (("" (INST 1 "I") (("1" (EXPAND "I") (("1" (PROPAX) NIL NIL)) NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|transitive_subseq| "" (EXPAND "subseq") (("" (SKOSIMP*) (("" (INST 1 "f!2 o f!1") (("1" (GRIND) NIL NIL) ("2" (REWRITE "extract_composition") NIL NIL)) NIL)) NIL)) NIL) (|incr_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST-CP -5 "x!1") (("" (INST -5 "y!1") (("" (REPLACE*) (("" (INST? -4) (("" (ASSERT) (("" (INST -3 "x!1" "y!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|decr_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST-CP -5 "x!1") (("" (INST -5 "y!1") (("" (INST -3 "x!1" "y!1") (("" (INST -4 "f!1(x!1)" "f!1(y!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|strict_incr_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST-CP -5 "x!1") (("" (INST -5 "y!1") (("" (INST -3 "x!1" "y!1") (("" (INST -4 "f!1(x!1)" "f!1(y!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|strict_decr_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST-CP -5 "x!1") (("" (INST -5 "y!1") (("" (INST -3 "x!1" "y!1") (("" (INST -4 "f!1(x!1)" "f!1(y!1)") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_above_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST? +) (("" (SKOLEM!) (("" (INST? -4) (("" (INST? -3) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_below_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST? +) (("" (SKOLEM!) (("" (INST? -4) (("" (INST? -3) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_subseq| "" (EXPAND "bounded?") (("" (SKOSIMP) (("" (FORWARD-CHAIN "bounded_above_subseq") (("" (FORWARD-CHAIN "bounded_below_subseq") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$convergence_sequences.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Definition and properties of % % convergent sequences of reals % % -> limit of a sequence, % % -> point of accumulation % % -> cauchy criterion % % -> Bolzano-Weierstrass theorem % % -> completeness of the reals % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% convergence_sequences : THEORY BEGIN IMPORTING sequence_props, absolute_value, monotone_subsequence u, u1, u2 : VAR sequence[real] l, l1, l2 : VAR real a, b, c, x : VAR real epsilon : VAR posreal i, j, n, m : VAR nat %-------------------- % Convergence to l %-------------------- convergence(u, l) : bool = FORALL epsilon : EXISTS n : FORALL i : i >= n IMPLIES abs(u(i) - l) < epsilon %------------------------- % Point of accumulation %------------------------- accumulation(u, a) : bool = FORALL epsilon, n : EXISTS i : i >= n AND abs(u(i) - a) < epsilon %-------------------- % Cauchy sequence %-------------------- cauchy(u) : bool = FORALL epsilon : EXISTS n : FORALL i, j : i >= n AND j >= n IMPLIES abs(u(i) - u(j)) < epsilon %----------------------- % The limit is unique %----------------------- unique_limit : PROPOSITION convergence(u, l1) AND convergence(u, l2) IMPLIES l1 = l2 %--------------------------------- % Limit of convergent sequences %--------------------------------- convergent(u) : bool = EXISTS l : convergence(u, l) v : VAR (convergent) limit(v) : real = epsilon(LAMBDA l : convergence(v, l)) limit_lemma : LEMMA convergence(v, limit(v)) limit_def : PROPOSITION limit(v) = l IFF convergence(v, l) %-------------------------------------------------------- % A subsequence of a convergent sequence is convergent %-------------------------------------------------------- convergence_subsequence : PROPOSITION convergence(u1, l) AND subseq(u2, u1) IMPLIES convergence(u2, l) %---------------------------------------- % The limit is a point of accumulation %---------------------------------------- limit_accumulation : PROPOSITION convergence(u, l) IMPLIES accumulation(u, l) %------------------------------------------------------------------ % a is a point of accumulation iff a sub-sequence converges to a %------------------------------------------------------------------ %--- extraction ---% g(u, a)(n) : RECURSIVE nat = IF n = 0 THEN 0 ELSE epsilon! i : g(u, a)(n - 1) < i AND abs(u(i) - a) < 1/n ENDIF MEASURE n %--- property of g when a is an accumulation point of a ---% g_prop : LEMMA accumulation(u, a) IMPLIES FORALL n : g(u, a)(n) < g(u, a)(n+1) AND abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1) g_increasing : COROLLARY accumulation(u, a) IMPLIES strict_increasing(g(u, a)) g_convergence : COROLLARY accumulation(u, a) IMPLIES FORALL n : abs(u(g(u, a)(n + 1)) - a) < 1/(n + 1) %--- main theorem ---% accumulation_subsequence : THEOREM accumulation(u, a) IFF EXISTS u1 : subseq(u1, u) AND convergence(u1, a) %------------------------------------------------------------- % a point of accumulation of a Cauchy sequence is its limit %------------------------------------------------------------- cauchy_accumulation : THEOREM cauchy(u) AND accumulation(u, a) IMPLIES convergence(u, a) cauchy_subsequence : COROLLARY cauchy(u) AND subseq(u1, u) AND convergence(u1, l) IMPLIES convergence(u, l) %---------------------------------------------- % Monotone, bounded sequences are convergent %---------------------------------------------- v1 : VAR { u | bounded_above?(u) } v2 : VAR { u | bounded_below?(u) } increasing_bounded_convergence : PROPOSITION increasing(v1) IMPLIES convergence(v1, sup(v1)) decreasing_bounded_convergence : PROPOSITION decreasing(v2) IMPLIES convergence(v2, inf(v2)) %-------------------------------------------------- % Bolzano-Weierstrass theorem: % a bounded sequence has a point of accumulation %-------------------------------------------------- %--- bounded sequence ---% w : VAR { u | bounded_above?(u) AND bounded_below?(u) } %--- Bolzano/Weirstrass theorem ---% bolzano_weierstrass1 : COROLLARY EXISTS a : inf(w) <= a AND a <= sup(w) AND accumulation(w, a) bolzano_weierstrass2 : COROLLARY EXISTS a : accumulation(w, a) bolzano_weierstrass3 : COROLLARY EXISTS u : subseq(u, w) AND convergent(u) bolzano_weierstrass4 : COROLLARY (FORALL i : a <= u(i) AND u(i) <= b) IMPLIES (EXISTS c : a <= c AND c <= b AND accumulation(u, c)) %-------------------------------- % A Cauchy sequence is bounded %-------------------------------- prefix_bounded1 : LEMMA EXISTS a : FORALL i : i <= n IMPLIES u(i) <= a prefix_bounded2 : LEMMA EXISTS a : FORALL i : i <= n IMPLIES a <= u(i) cauchy_bounded : PROPOSITION cauchy(u) IMPLIES bounded_above?(u) AND bounded_below?(u) %-------------------------------------------------- % Completeness : a Cauchy sequence is convergent %-------------------------------------------------- convergence_cauchy1 : LEMMA convergent(u) IMPLIES cauchy(u) convergence_cauchy2 : LEMMA cauchy(u) IMPLIES convergent(u) convergence_cauchy : THEOREM convergent(u) IFF cauchy(u) END convergence_sequences $$$convergence_sequences.prf (|convergence_sequences| (|unique_limit| "" (SKOSIMP) (("" (EXPAND "convergence") (("" (REWRITE "null_distance") (("" (NAME "eps" "abs(l1!1 - l2!1)/3") (("" (ASSERT) (("" (INST -2 "eps") (("" (INST -3 "eps") (("" (SKOLEM!) (("" (SKOLEM!) (("" (INST -2 "n!1+n!2") (("" (INST -3 "n!1+n!2") (("" (ASSERT) (("" (LEMMA "triangle2") (("" (INST -1 "eps" "eps" "l1!1" "u!1(n!1+n!2)" "l2!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_lemma| "" (SKOLEM-TYPEPRED) (("" (NAME-REPLACE "ll" "limit(v!1)" :HIDE? NIL) (("" (EXPAND "limit") (("" (EXPAND "convergent") (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (l: real): convergence(v!1, l)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_def| "" (SKOLEM!) (("" (USE "limit_lemma") (("" (GROUND) (("" (USE "unique_limit") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_subsequence| "" (GRIND :DEFS NIL :REWRITES ("subseq" "convergence") :IF-MATCH NIL) (("" (DELETE -1 -2 -3 -4) (("" (INST -1 "epsilon!1") (("" (SKOLEM!) (("" (INST 1 "n!1") (("" (SKOSIMP) (("" (INST? -2) (("" (REPLACE -2) (("" (INST?) (("" (ASSERT) (("" (USE "extract_incr3") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_accumulation| "" (GRIND :DEFS NIL :REWRITES ("convergence" "accumulation") :IF-MATCH NIL) (("" (INST?) (("" (SKOLEM!) (("" (INST -5 "n!1+n!2") (("" (INST 1 "n!1+n!2") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|g_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL) (|g_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL) (|g_TCC3| "" (SKOSIMP*) NIL NIL) (|g_prop| "" (SKOSIMP*) (("" (EXPAND "accumulation") (("" (NAME-REPLACE "y" "g(u!1, a!1)(n!1 + 1)" :HIDE? NIL) (("" (EXPAND "g" -1) (("" (ASSERT) (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (i: nat): g(u!1, a!1)(n!1) < i AND abs(u!1(i) - a!1) < 1 / (1 + n!1)")) (("" (REPLACE -2) (("" (ASSERT) (("" (SPLIT -1) (("1" (PROPAX) NIL NIL) ("2" (INST -2 "1/(1+n!1)" "g(u!1, a!1)(n!1) + 1") (("2" (SKOSIMP) (("2" (INST 1 "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|g_increasing| "" (SKOSIMP) (("" (REWRITE "strict_incr_condition") (("" (SKOLEM!) (("" (FORWARD-CHAIN "g_prop") (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|g_convergence| "" (SKOSIMP*) (("" (FORWARD-CHAIN "g_prop") (("" (INST -1 "n!1") (("" (FLATTEN) NIL NIL)) NIL)) NIL)) NIL) (|accumulation_subsequence| "" (SKOLEM!) (("" (PROP) (("1" (INST 1 "LAMBDA (i : nat) : u!1(g(u!1, a!1)(i))") (("1" (SPLIT) (("1" (FORWARD-CHAIN "g_increasing") (("1" (EXPAND "subseq") (("1" (INST 1 "g(u!1, a!1)") (("1" (SKOLEM!) NIL NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "g_convergence") (("2" (EXPAND "convergence") (("2" (SKOLEM!) (("2" (LEMMA "archimedean2" ("x" "epsilon!1")) (("2" (SKOLEM!) (("2" (INST 1 "a!2") (("2" (SKOSIMP) (("2" (ASSERT) (("2" (INST -2 "i!1 - 1") (("2" (ASSERT) (("2" (CASE "1/i!1 <= 1/a!2") (("1" (ASSERT) NIL NIL) ("2" (REWRITE "both_sides_div_pos_le2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GRIND :DEFS NIL :REWRITES ("subseq" "convergence" "accumulation") :IF-MATCH NIL) (("2" (INST? -6) (("2" (SKOLEM!) (("2" (INST -5 "n!1 + n!2") (("2" (INST -6 "n!1+n!2") (("2" (INST?) (("2" (ASSERT) (("2" (ASSERT) (("2" (USE "extract_incr3") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cauchy_accumulation| "" (GRIND :DEFS NIL :REWRITES ("cauchy" "accumulation" "convergence") :IF-MATCH NIL) (("" (INST -4 "epsilon!1/2") (("" (SKOLEM!) (("" (INST -5 "epsilon!1/2" "n!1") (("" (SKOSIMP) (("" (INST 1 "i!1") (("" (SKOSIMP) (("" (INST -4 "i!1" "i!2") (("" (ASSERT) (("" (LEMMA "triangle2") (("" (ASSERT) (("" (INST -1 "epsilon!1/2" "epsilon!1/2" "u!1(i!2)" "u!1(i!1)" "a!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cauchy_subsequence| "" (SKOSIMP) (("" (REWRITE "cauchy_accumulation" 1) (("" (REWRITE "accumulation_subsequence") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|increasing_bounded_convergence| "" (SKOSIMP) (("" (ASSERT) (("" (GRIND :DEFS NIL :IF-MATCH NIL :REWRITES ("increasing" "convergence")) (("" (USE "supfun_is_sup[nat]") (("" (SKOLEM!) (("" (INST 1 "x!1") (("" (SKOSIMP) (("" (INST -4 "x!1" "i!1") (("" (ASSERT) (("" (USE "supfun_is_bound" ("x" "i!1")) (("" (ASSERT) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|decreasing_bounded_convergence| "" (SKOSIMP) (("" (ASSERT) (("" (GRIND :DEFS NIL :IF-MATCH NIL :REWRITES ("decreasing" "convergence")) (("" (USE "inffun_is_inf[nat]") (("" (SKOLEM!) (("" (INST 1 "x!1") (("" (SKOSIMP) (("" (INST -4 "x!1" "i!1") (("" (ASSERT) (("" (USE "inffun_is_bound" ("x" "i!1")) (("" (ASSERT) (("" (EXPAND "abs") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bolzano_weierstrass1| "" (SKOLEM!) (("" (USE "monotone_subsequence") (("" (SKOSIMP) (("" (USE* "bounded_above_subseq" "bounded_below_subseq") (("" (ASSERT) (("" (EXPAND "subseq") (("" (SKOLEM!) (("" (AUTO-REWRITE "supfun_is_sup2[nat]" "inffun_is_inf2[nat]" "supfun_is_bound[nat]" "inffun_is_bound[nat]" "accumulation_subsequence") (("" (GROUND) (("1" (FORWARD-CHAIN "increasing_bounded_convergence") (("1" (INST? +) (("1" (GROUND) (("1" (INST - "0") (("1" (USE "supfun_is_bound" ("g" "s!1")) (("1" (USE "inffun_is_bound" ("h" "w!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST?) (("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "decreasing_bounded_convergence") (("2" (INST? +) (("2" (GROUND) (("1" (SKOLEM!) (("1" (INST?) (("1" (REPLACE -5) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST - "0") (("2" (USE "inffun_is_bound" ("h" "s!1")) (("2" (USE "supfun_is_bound" ("g" "w!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("3" (INST?) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bolzano_weierstrass2| "" (SKOLEM!) (("" (USE "bolzano_weierstrass1") (("" (SKOSIMP) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|bolzano_weierstrass3| "" (SKOSIMP) (("" (USE "bolzano_weierstrass1") (("" (SKOSIMP) (("" (REWRITE "accumulation_subsequence") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (EXPAND "convergent") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bolzano_weierstrass4| "" (SKOSIMP) (("" (CASE "bounded_above?(u!1) AND bounded_below?(u!1)") (("1" (GROUND) (("1" (CASE "a!1 <= inf(u!1) AND sup(u!1) <= b!1") (("1" (GROUND) (("1" (USE "bolzano_weierstrass1") (("1" (SKOSIMP) (("1" (INST + "a!2") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (GROUND) (("1" (REWRITE "inffun_is_inf2[nat]") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "supfun_is_sup2[nat]") (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND :IF-MATCH NIL) (("1" (INST + "a!1") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (INST + "b!1") (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_bounded1| "" (SKOLEM 1 (_ "u!1")) (("" (INDUCT "n") (("1" (INST 1 "u!1(0)") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST 1 "max(a!1, u!1(j!1+1))") (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prefix_bounded2| "" (SKOLEM 1 (_ "u!1")) (("" (INDUCT "n") (("1" (INST 1 "u!1(0)") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (INST 1 "min(a!1, u!1(j!1+1))") (("2" (SKOSIMP) (("2" (INST -1 "i!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|cauchy_bounded| "" (SKOSIMP) (("" (EXPAND "cauchy") (("" (INST - "1") (("" (SKOLEM!) (("" (INST - "n!1" _) (("" (AUTO-REWRITE "bounded_above?" "bounded_below?" "abs") (("" (GROUND) (("1" (USE "prefix_bounded1" ("n" "n!1")) (("1" (SKOLEM!) (("1" (INST + "a!1 + 1") (("1" (SKOLEM!) (("1" (INST-CP - "n!1") (("1" (INST - "x!1") (("1" (INST - "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "prefix_bounded2" ("n" "n!1")) (("2" (SKOLEM!) (("2" (INST + "a!1 - 1") (("2" (SKOLEM!) (("2" (INST-CP - "n!1") (("2" (INST - "x!1") (("2" (INST - "x!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_cauchy1| "" (GRIND :DEFS NIL :REWRITES ("convergent" "convergence" "cauchy") :IF-MATCH NIL) (("" (DELETE -1 -2 -3) (("" (INST -1 "epsilon!1/2") (("" (SKOLEM!) (("" (INST? 1) (("" (SKOSIMP) (("" (INST-CP -1 "i!1") (("" (INST -1 "j!1") (("" (ASSERT) (("" (REWRITE "diff_abs_commute" -1) (("" (REWRITE "diff_abs_commute" -2) (("" (LEMMA "triangle2") (("" (INST -1 "epsilon!1/2" "epsilon!1/2" "u!1(j!1)" "l!1" "u!1(i!1)") (("" (ASSERT) (("" (REWRITE "diff_abs_commute" +) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_cauchy2| "" (SKOSIMP) (("" (USE "bolzano_weierstrass2") (("1" (SKOLEM!) (("1" (EXPAND "convergent") (("1" (INST?) (("1" (REWRITE "cauchy_accumulation") NIL NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "cauchy_bounded") NIL NIL)) NIL)) NIL) (|convergence_cauchy| "" (SKOLEM!) (("" (PROP) (("1" (REWRITE "convergence_cauchy1") NIL NIL) ("2" (REWRITE "convergence_cauchy2") NIL NIL)) NIL)) NIL)) $$$convergence_ops.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Limits and operations on sequences of reals %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% convergence_ops : THEORY BEGIN IMPORTING convergence_sequences, epsilon_lemmas s, s1, s2 : VAR sequence[real] s3 : VAR sequence[nzreal] a : VAR real l, l1, l2 : VAR real n, N : VAR nat %--------------------------------- % limits of sum, product, etc. %--------------------------------- limit_sum : PROPOSITION convergence(s1, l1) AND convergence(s2, l2) IMPLIES convergence(s1 + s2, l1 + l2) limit_opposite : PROPOSITION convergence(s1, l1) IMPLIES convergence(-s1, -l1) limit_diff : PROPOSITION convergence(s1, l1) AND convergence(s2, l2) IMPLIES convergence(s1 - s2, l1 - l2) limit_prod : PROPOSITION convergence(s1, l1) AND convergence(s2, l2) IMPLIES convergence(s1 * s2, l1 * l2) limit_const : PROPOSITION convergence(const(a), a) limit_scal : PROPOSITION convergence(s1, l1) IMPLIES convergence(a * s1, a * l1) limit_inv : PROPOSITION convergence(s3, l2) AND l2 /= 0 IMPLIES convergence(1 / s3, 1 / l2) limit_div : PROPOSITION convergence(s1, l1) AND convergence(s3, l2) AND l2 /= 0 IMPLIES convergence(s1 / s3, l1 / l2) limit_abs : PROPOSITION convergence(s1, l1) IMPLIES convergence(abs(s1), abs(l1)) limit_order : PROPOSITION convergence(s1, l1) and convergence(s2, l2) AND (FORALL n : s1(n) <= s2(n)) IMPLIES l1 <= l2 %------------- % Squeezing %------------- squeezing_variant : PROPOSITION convergence(s1, l) and convergence(s2, l) AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) and s(n) <= s2(n)) IMPLIES convergence(s, l) squeezing_const1 : PROPOSITION convergence(s1, l) AND (FORALL n : N <= n IMPLIES l <= s(n) AND s(n) <= s1(n)) IMPLIES convergence(s, l) squeezing_const2 : PROPOSITION convergence(s1, l) AND (FORALL n : N <= n IMPLIES s1(n) <= s(n) AND s(n) <= l) IMPLIES convergence(s, l) squeezing : PROPOSITION convergence(s1, l) and convergence(s2, l) AND (FORALL n : s1(n) <= s(n) and s(n) <= s2(n)) IMPLIES convergence(s, l) abs_convergence : COROLLARY convergence(s, 0) IFF convergence(abs(s), 0) %---------------------------------- % Same properties with convergent %---------------------------------- convergent_sum : PROPOSITION convergent(s1) AND convergent(s2) IMPLIES convergent(s1 + s2) convergent_opposite : PROPOSITION convergent(s1) IMPLIES convergent(-s1) convergent_diff : PROPOSITION convergent(s1) AND convergent(s2) IMPLIES convergent(s1 - s2) convergent_prod : PROPOSITION convergent(s1) AND convergent(s2) IMPLIES convergent(s1 * s2) convergent_const : PROPOSITION convergent(const(a)) convergent_scal : PROPOSITION convergent(s1) IMPLIES convergent(a * s1) convergent_inv : PROPOSITION convergent(s3) AND limit(s3) /= 0 IMPLIES convergent(1 / s3) convergent_div : PROPOSITION convergent(s1) AND convergent(s3) AND limit(s3) /= 0 IMPLIES convergent(s1 / s3) convergent_abs : PROPOSITION convergent(s1) IMPLIES convergent(abs(s1)) %--------------------------------- % Types of convergent sequences %--------------------------------- v1, v2 : VAR (convergent) u : VAR { s3 | convergent(s3) } convergent_nz(u) : bool = limit(u) /= 0 v3 : VAR (convergent_nz) %-------------- % Judgements %-------------- constant_seq1: JUDGEMENT const(a) HAS_TYPE (convergent) constant_seq2: JUDGEMENT const(b: nzreal) HAS_TYPE (convergent_nz) conv_seq_plus: JUDGEMENT +(v1, v2) HAS_TYPE (convergent) conv_seq_minus: JUDGEMENT -(v1, v2) HAS_TYPE (convergent) conv_seq_times: JUDGEMENT *(v1, v2) HAS_TYPE (convergent) conv_seq_scal: JUDGEMENT *(a, v1) HAS_TYPE (convergent) conv_seq_opposite: JUDGEMENT -(v1) HAS_TYPE (convergent) conv_seq_abs: JUDGEMENT abs(v1) HAS_TYPE (convergent) conv_seq_div1: JUDGEMENT /(v1, v3) HAS_TYPE (convergent) conv_seq_div2: JUDGEMENT /(a, v3) HAS_TYPE (convergent) %----------------------------- % Combinations of sequences %----------------------------- lim_sum : PROPOSITION limit(v1 + v2) = limit(v1) + limit(v2) lim_opposite : PROPOSITION limit(- v1) = - limit(v1) lim_diff : PROPOSITION limit(v1 - v2) = limit(v1) - limit(v2) lim_prod : PROPOSITION limit(v1 * v2) = limit(v1) * limit(v2) lim_inv : PROPOSITION limit(1 / v3) = 1 / limit(v3) lim_div : PROPOSITION limit(v1 / v3) = limit(v1) / limit(v3) lim_const : PROPOSITION limit(const(a)) = a lim_scal : PROPOSITION limit(a * v1) = a * limit(v1) lim_abs : PROPOSITION limit(abs(v1)) = abs(limit(v1)) %--------------------------------------------------- % Expansion of convergence (for computing limits) %--------------------------------------------------- limit_equiv : LEMMA convergence(s, l) IFF convergent(s) AND limit(s) = l END convergence_ops $$$convergence_ops.prf (|convergence_ops| (|limit_sum| "" (EXPAND "convergence") (("" (SKOSIMP*) (("" (INST -1 "epsilon!1/2") (("" (INST -2 "epsilon!1/2") (("" (SKOLEM!) (("" (SKOLEM!) (("" (INST 1 "n!1 + n!2") (("" (SKOSIMP) (("" (INST -1 "i!1") (("" (INST -2 "i!1") (("" (ASSERT) (("" (EXPAND "+") (("" (LEMMA "sum_abs" ("x" "s1!1(i!1) - l1!1" "y" "s2!1(i!1) - l2!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_opposite| "" (EXPAND "convergence") (("" (SKOSIMP*) (("" (INST -1 "epsilon!1") (("" (EXPAND "-") (("" (SKOLEM!) (("" (INST? 1) (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (LEMMA "neg_abs" ("x" "s1!1(i!1) - l1!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_diff| "" (SKOSIMP) (("" (REWRITE "diff_function") (("" (LEMMA "limit_sum" ("s1" "s1!1" "s2" "- s2!1" "l1" "l1!1" "l2" "-l2!1")) (("" (ASSERT) (("" (REWRITE "limit_opposite") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|limit_prod| "" (EXPAND "convergence") (("" (SKOSIMP*) (("" (LEMMA "prod_epsilon") (("" (INST -1 "epsilon!1" "l1!1" "l2!1") (("" (SKOLEM!) (("" (INST -2 "e1!1") (("" (INST -3 "e2!1") (("" (SKOLEM!) (("" (SKOLEM!) (("" (INST 1 "n!1 + n!2") (("" (SKOSIMP) (("" (INST -2 "i!1") (("" (INST -3 "i!1") (("" (ASSERT) (("" (EXPAND "*" 1 1) (("" (LEMMA "prod_bound") (("" (INST -1 "e1!1" "e2!1" "s1!1(i!1)" "s2!1(i!1)" "l1!1" "l2!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_const| "" (SKOLEM!) (("" (GRIND :IF-MATCH NIL) NIL NIL)) NIL) (|limit_scal| "" (SKOSIMP) (("" (REWRITE "scal_function") (("" (REWRITE "limit_prod") (("" (REWRITE "limit_const") NIL NIL)) NIL)) NIL)) NIL) (|limit_inv| "" (EXPAND "convergence") (("" (SKOSIMP*) (("" (ASSERT) (("" (LEMMA "inv_epsilon" ("y1" "l2!1" "e" "epsilon!1")) (("" (ASSERT) (("" (SKOSIMP) (("" (INST -3 "e1!1") (("" (SKOLEM!) (("" (INST 2 "n!1") (("" (SKOSIMP) (("" (INST -3 "i!1") (("" (ASSERT) (("" (EXPAND "/") (("" (ASSERT) (("" (LEMMA "inv_bound") (("" (INST -1 "e1!1" "s3!1(i!1)" "l2!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_div| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "div_function") (("" (USE "limit_prod" ("l2" "1/l2!1")) (("" (ASSERT) (("" (REWRITE "limit_inv") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_abs| "" (EXPAND "convergence") (("" (SKOSIMP*) (("" (INST -1 "epsilon!1") (("" (SKOLEM!) (("" (INST 1 "n!1") (("" (SKOSIMP) (("" (INST -1 "i!1") (("" (ASSERT) (("" (EXPAND "abs" 1 2) (("" (EXPAND "abs" 1 1) (("" (LIFT-IF) (("" (LEMMA "diff_abs" ("x" "s1!1(i!1)" "y" "l1!1")) (("" (LEMMA "diff_abs" ("x" "l1!1" "y" "s1!1(i!1)")) (("" (REWRITE "diff_abs_commute" -1) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_order| "" (SKOSIMP) (("" (EXPAND "convergence") (("" (CASE "l2!1 < l1!1") (("1" (NAME "eps" "(l1!1 - l2!1) / 2") (("1" (ASSERT) (("1" (INST -3 "eps") (("1" (INST -4 "eps") (("1" (SKOLEM!) (("1" (SKOLEM!) (("1" (INST -3 "n!1+n!2") (("1" (INST -4 "n!1+n!2") (("1" (INST -5 "n!1+n!2") (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|squeezing_variant| "" (EXPAND "convergence") (("" (SKOSIMP*) (("" (INST -1 "epsilon!1") (("" (INST -2 "epsilon!1") (("" (SKOLEM!) (("" (SKOLEM!) (("" (INST 1 "N!1 + n!1 + n!2") (("" (SKOSIMP) (("" (INST -1 "i!1") (("" (INST -2 "i!1") (("" (INST -3 "i!1") (("" (ASSERT) (("" (FLATTEN) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (SPLIT 1) (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|squeezing_const1| "" (SKOSIMP) (("" (AUTO-REWRITE "limit_const" "const") (("" (LEMMA "squeezing_variant") (("" (INST -1 "N!1" "l!1" "s!1" "l!1" "s1!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|squeezing_const2| "" (SKOSIMP) (("" (AUTO-REWRITE "limit_const" "const") (("" (LEMMA "squeezing_variant") (("" (INST -1 "N!1" "l!1" "s!1" "s1!1" "l!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|squeezing| "" (SKOSIMP) (("" (USE "squeezing_variant" ("s1" "s1!1" "s2" "s2!1" "s" "s!1" "N" "0")) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|abs_convergence| "" (SKOLEM!) (("" (PROP) (("1" (FORWARD-CHAIN "limit_abs") (("1" (EXPAND "abs" -1 2) (("1" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (FORWARD-CHAIN "limit_opposite") (("2" (ASSERT) (("2" (LEMMA "squeezing" ("s1" "- abs(s!1)" "s2" "abs(s!1)" "s" "s!1" "l" "0")) (("2" (ASSERT) (("2" (SKOLEM!) (("2" (DELETE -1 -2 2) (("2" (EXPAND "-") (("2" (EXPAND "abs") (("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergent_sum| "" (GRIND :EXCLUDE "convergence" :REWRITES ("limit_sum") :IF-MATCH NIL) (("" (INST + "l!1 + l!2") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|convergent_opposite| "" (LEMMA "limit_opposite") (("" (AUTO-REWRITE "convergent") (("" (REDUCE :IF-MATCH NIL) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|convergent_diff| "" (LEMMA "limit_diff") (("" (GRIND :EXCLUDE "convergence") NIL NIL)) NIL) (|convergent_prod| "" (LEMMA "limit_prod") (("" (GRIND :EXCLUDE "convergence") NIL NIL)) NIL) (|convergent_const| "" (LEMMA "limit_const") (("" (GRIND :EXCLUDE "convergence") NIL NIL)) NIL) (|convergent_scal| "" (LEMMA "limit_scal") (("" (GRIND :EXCLUDE "convergence") NIL NIL)) NIL) (|convergent_inv| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "convergent") (("" (SKOLEM!) (("" (USE "limit_inv") (("" (ASSERT) (("" (REWRITE "limit_def" -2 :DIR RL) (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergent_div| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (USE "limit_div") (("" (ASSERT) (("" (REWRITE "limit_def" -3 :DIR RL) (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergent_abs| "" (LEMMA "limit_abs") (("" (AUTO-REWRITE "convergent") (("" (REDUCE :IF-MATCH NIL) (("" (REDUCE) NIL NIL)) NIL)) NIL)) NIL) (|convergent_nz_TCC1| "" (SUBTYPE-TCC) NIL NIL) (|constant_seq1| "" (LEMMA "convergent_const") (("" (PROPAX) NIL NIL)) NIL) (|constant_seq2| "" (SKOLEM!) (("" (USE "limit_const") (("" (AUTO-REWRITE "limit_def" "convergent_nz" "const") (("" (ASSERT) (("" (USE "unique_limit" ("l2" "0")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|conv_seq_plus| "" (SKOLEM!) (("" (REWRITE "convergent_sum") NIL NIL)) NIL) (|conv_seq_minus| "" (SKOLEM!) (("" (REWRITE "convergent_diff") NIL NIL)) NIL) (|conv_seq_times| "" (SKOLEM!) (("" (REWRITE "convergent_prod") NIL NIL)) NIL) (|conv_seq_scal| "" (SKOLEM!) (("" (REWRITE "convergent_scal") NIL NIL)) NIL) (|conv_seq_opposite| "" (SKOLEM!) (("" (REWRITE "convergent_opposite") NIL NIL)) NIL) (|conv_seq_abs| "" (SKOLEM!) (("" (REWRITE "convergent_abs") NIL NIL)) NIL) (|conv_seq_div1| "" (AUTO-REWRITE "convergent_div" "convergent_nz") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|conv_seq_div2| "" (SKOLEM!) (("" (REWRITE "scaldiv_function") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|lim_sum| "" (AUTO-REWRITE "limit_def" "limit_sum" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|lim_opposite| "" (AUTO-REWRITE "limit_def" "limit_opposite" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|lim_diff| "" (AUTO-REWRITE "limit_def" "limit_diff" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|lim_prod| "" (AUTO-REWRITE "limit_def" "limit_prod" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|lim_inv_TCC1| "" (AUTO-REWRITE "convergent_nz") (("" (REDUCE) NIL NIL)) NIL) (|lim_inv_TCC2| "" (SUBTYPE-TCC) NIL NIL) (|lim_inv| "" (AUTO-REWRITE "limit_def" "limit_lemma" "convergent_nz") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REWRITE "limit_inv") NIL NIL)) NIL)) NIL)) NIL) (|lim_div| "" (AUTO-REWRITE "limit_def" "limit_lemma" "convergent_nz") (("" (SKOLEM-TYPEPRED) (("" (ASSERT) (("" (REWRITE "limit_div") NIL NIL)) NIL)) NIL)) NIL) (|lim_const| "" (SKOLEM!) (("" (REWRITE "limit_def") (("" (REWRITE "limit_const") NIL NIL)) NIL)) NIL) (|lim_scal| "" (AUTO-REWRITE "limit_def" "limit_scal" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|lim_abs| "" (AUTO-REWRITE "limit_def" "limit_lemma" "limit_abs") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_equiv| "" (SKOLEM!) (("" (GROUND) (("1" (GRIND :EXCLUDE ("convergence")) NIL NIL) ("2" (REWRITE "limit_def") (("2" (EXPAND "convergent") (("2" (INST?) NIL NIL)) NIL)) NIL) ("3" (REWRITE "limit_def") NIL NIL)) NIL)) NIL)) $$$top_sequences.pvs top_sequences : THEORY BEGIN IMPORTING convergence_ops, convergence_sequences END top_sequences $$$continuity_props.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Properties of continuous functions % % in relation with sequences, limits % % and points of accumulation % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% continuity_props[T : TYPE FROM real] : THEORY BEGIN IMPORTING continuous_functions, top_sequences f : VAR [T -> real] u : VAR sequence[T] l, a : VAR T %-------------------------------------------- % u is convergent to l and f is continuous %-------------------------------------------- continuity_limit : PROPOSITION convergence(u, l) AND continuous(f, l) IMPLIES convergence(f o u, f(l)) %-------------------------------------------- % point of accumulation %-------------------------------------------- continuity_accumulation : PROPOSITION accumulation(u, a) AND continuous(f, a) IMPLIES accumulation(f o u, f(a)) END continuity_props $$$continuity_props.prf (|continuity_props| (|continuity_limit| "" (GRIND :EXCLUDE ("abs" "continuous") :REWRITES ("continuity_def[T]") :IF-MATCH NIL) (("" (INST -5 "epsilon!1") (("" (SKOLEM!) (("" (INST -4 "delta!1") (("" (SKOLEM!) (("" (INST 1 "n!1") (("" (SKOSIMP) (("" (INST?) (("" (INST?) (("" (ASSERT) NIL))))))))))))))))))) (|continuity_accumulation| "" (GRIND :EXCLUDE ("abs" "continuous") :REWRITES ("continuity_def[T]") :IF-MATCH NIL) (("" (INST -6 "epsilon!1") (("" (SKOLEM!) (("" (INST -5 "delta!1" "n!1") (("" (SKOSIMP) (("" (INST -7 "u!1(i!1)") (("" (INST?) (("" (ASSERT) NIL)))))))))))))))) $$$continuity_interval.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % continuous functions on a closed interval % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% continuity_interval [ a : real, b : {x : real | a <= x }] : THEORY BEGIN %----------------------------- % Interval [a, b] as a type %----------------------------- x : VAR real J : NONEMPTY_TYPE = { x | a <= x AND x <= b} f : VAR [J -> real] u : VAR sequence[J] c : VAR J n, i : VAR nat IMPORTING continuity_props %----------------------------------------------- % Reformulation of Bolzano/Weirstrass theorem %----------------------------------------------- bolz_weier : PROPOSITION EXISTS c : accumulation(u, c) %------------------------------------- % If f is continuous, it is bounded %------------------------------------- unbounded_sequence : LEMMA bounded_above?(f) or EXISTS u : FORALL n : f(u(n)) > n bounded_from_above : PROPOSITION continuous(f) IMPLIES bounded_above?(f) bounded_from_below : PROPOSITION continuous(f) IMPLIES bounded_below?(f) %-------------------------------------- % f has a maximum and a minimum in J %-------------------------------------- max_extraction : LEMMA continuous(f) IMPLIES EXISTS u : FORALL n : sup(f) - f(u(n)) < 1/(n+1) sup_is_reached : PROPOSITION continuous(f) IMPLIES EXISTS c : f(c) = sup(f) maximum_exists : PROPOSITION continuous(f) IMPLIES EXISTS c : is_maximum(c, f) inf_is_reached : PROPOSITION continuous(f) IMPLIES EXISTS c : f(c) = inf(f) minimum_exists : PROPOSITION continuous(f) IMPLIES EXISTS c : is_minimum(c, f) %------------------------------- % Intermediate value theorem %------------------------------- intermediate_value1 : PROPOSITION continuous(f) AND f(a) < x AND x < f(b) IMPLIES EXISTS c : f(c) = x intermediate_value2 : PROPOSITION continuous(f) AND f(a) <= x AND x <= f(b) IMPLIES EXISTS c : f(c) = x intermediate_value3 : PROPOSITION continuous(f) AND f(b) < x AND x < f(a) IMPLIES EXISTS c : f(c) = x intermediate_value4 : PROPOSITION continuous(f) AND f(b) <= x AND x <= f(a) IMPLIES EXISTS c : f(c) = x END continuity_interval $$$continuity_interval.prf (|continuity_interval| (J_TCC1 "" (INST 1 "a") (("" (ASSERT) NIL NIL)) NIL) (|bolz_weier| "" (SKOLEM!) (("" (LEMMA "bolzano_weierstrass4") (("" (INST -1 "a" "b" "u!1") (("" (PROP) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|unbounded_sequence| "" (SKOSIMP) (("" (EXPAND "bounded_above?") (("" (INST 2 "lambda (n : nat) : epsilon! (x : J) : f!1(x) > n") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "epsilon_ax[J]") (("" (GROUND) (("" (INST? 2) (("" (DELETE 3) (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_from_above| "" (SKOSIMP) (("" (USE "unbounded_sequence") (("" (ASSERT) (("" (SKOLEM!) (("" (USE "bolz_weier") (("" (SKOLEM!) (("" (EXPAND "continuous") (("" (INST? -3) (("" (FORWARD-CHAIN "continuity_accumulation[J]") (("" (DELETE -2 -4 1) (("" (EXPAND "accumulation") (("" (EXPAND "o") (("" (CASE "EXISTS (m : nat) : f!1(c!1) + 1 < m") (("1" (SKOLEM!) (("1" (INST -2 "1" "m!1") (("1" (SKOSIMP) (("1" (INST?) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -) (("2" (USE "axiom_of_archimedes") (("2" (SKOLEM!) (("2" (INST 1 "IF i!1 < 0 THEN 0 ELSE i!1 ENDIF") (("1" (LIFT-IF) (("1" (ASSERT) NIL NIL)) NIL) ("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|bounded_from_below| "" (SKOSIMP) (("" (LEMMA "bounded_from_above" ("f" "-f!1")) (("" (REWRITE "bounded_above_opposite[J]") (("" (ASSERT) (("" (REWRITE "opp_fun_continuous[J]") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|max_extraction_TCC1| "" (LEMMA "bounded_from_above") (("" (PROPAX) NIL NIL)) NIL) (|max_extraction| "" (SKOSIMP) (("" (FORWARD-CHAIN "bounded_from_above") (("" (ASSERT) (("" (INST 1 "LAMBDA (n : nat) : epsilon! (x : J) : sup(f!1) - f!1(x) < 1 / (1 + n)") (("" (BETA) (("" (SKOLEM!) (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (x: J): sup(f!1) - f!1(x) < 1 / (1 + n!1)")) (("" (ASSERT) (("" (DELETE 2) (("" (LEMMA "supfun_is_sup[J]" ("g" "f!1" "epsilon" "1/(1+n!1)")) (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sup_is_reached| "" (SKOSIMP) (("" (FORWARD-CHAIN "bounded_from_above") (("" (ASSERT) (("" (FORWARD-CHAIN "max_extraction") (("" (SKOLEM!) (("" (USE "bolz_weier") (("" (SKOLEM!) (("" (EXPAND "continuous") (("" (INST? -4) (("" (FORWARD-CHAIN "continuity_accumulation[J]") (("" (DELETE -2 -4 -5) (("" (INST? 1) (("" (EXPAND "accumulation") (("" (EXPAND "o") (("" (USE "supfun_is_bound[J]") (("" (NAME "eps" "sup(f!1) - f!1(c!1)") (("" (ASSERT) (("" (USE "archimedean2" ("x" "eps/2")) (("" (SKOLEM!) (("" (INST -4 "eps/2" "a!1") (("" (SKOSIMP) (("" (INST -6 "i!1") (("" (CASE "1 / (1 + i!1) < 1 / a!1") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (REWRITE "both_sides_div_pos_lt2" 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|maximum_exists| "" (SKOSIMP) (("" (FORWARD-CHAIN "sup_is_reached") (("" (SKOLEM!) (("" (INST?) (("" (REWRITE "max_upper_bound[J]") (("" (ASSERT) (("" (REWRITE "bounded_from_above") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inf_is_reached_TCC1| "" (LEMMA "bounded_from_below") (("" (PROPAX) NIL NIL)) NIL) (|inf_is_reached| "" (SKOSIMP) (("" (USE "sup_is_reached" ("f" "-f!1")) (("" (SPLIT) (("1" (SKOLEM!) (("1" (REWRITE "supfun_opposite[J]") (("1" (EXPAND "-") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "bounded_from_below") NIL NIL)) NIL)) NIL) ("2" (REWRITE "opp_fun_continuous[J]") NIL NIL)) NIL)) NIL)) NIL) (|minimum_exists| "" (SKOSIMP) (("" (USE "maximum_exists" ("f" "-f!1")) (("" (SPLIT) (("1" (SKOLEM!) (("1" (REWRITE "max_opposite[J]") (("1" (INST?) NIL NIL)) NIL)) NIL) ("2" (REWRITE "opp_fun_continuous[J]") NIL NIL)) NIL)) NIL)) NIL) (|intermediate_value1_TCC1| "" (SKOSIMP) (("" (ASSERT) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|intermediate_value1_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL) (|intermediate_value1| "" (SKOSIMP) (("" (NAME "E" "{y:real| a <= y AND y <= b AND f!1(y) < x!1}") (("1" (CASE "nonempty?(E) AND bounded_above?(E)") (("1" (ASSERT) (("1" (GROUND) (("1" (CASE "a <= lub(E) AND lub(E) <= b") (("1" (ASSERT) (("1" (GROUND) (("1" (HIDE -1 -2 -3 -4) (("1" (EXPAND "continuous") (("1" (INST - "lub(E)") (("1" (INST + "lub(E)") (("1" (AUTO-REWRITE "abs" "subset_fullset[real]") (("1" (CASE "x!1 < f!1(lub(E))") (("1" (ASSERT) (("1" (REWRITE "continuity_def[J]") (("1" (INST - "f!1(lub(E)) - x!1") (("1" (SKOLEM!) (("1" (USE "adherence_sup" ("epsilon" "delta!1")) (("1" (SKOLEM-TYPEPRED) (("1" (REPLACE -4 -1 RL) (("1" (ASSERT) (("1" (USE "lub_is_bound" ("U" "E" "x" "x!2")) (("1" (GROUND) (("1" (INST - "x!2") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NAME "F" "{y:real | lub(E) < y AND y <= b}") (("2" (EXPAND* "continuous" "convergence") (("2" (USE "subset_convergence2[J]" ("E1" "F")) (("1" (GROUND) (("1" (DELETE -4) (("1" (USE "convergence_lower_bound[J]" ("b" "x!1")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (REPLACE -3 -1 RL) (("1" (ASSERT) (("1" (USE "lub_is_bound" ("U" "E" "x" "x!2")) (("1" (ASSERT) NIL NIL) ("2" (REPLACE -4 + RL) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 + RL) (("2" (EXPAND "adh") (("2" (SKOSIMP) (("2" (CASE "b < lub(E) + e!1") (("1" (ASSERT) (("1" (INST + "b") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST + "lub(E) + e!1/2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 -4 -5 -6 2) (("2" (GROUND) (("1" (REWRITE "lub_is_bound") (("1" (REPLACE -1 + RL) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "lub_is_lub") (("2" (SKOLEM-TYPEPRED) (("2" (REPLACE -2 - RL) (("2" (ASSERT) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 2) (("2" (GRIND :IF-MATCH NIL) (("1" (INST + "b") (("1" (SKOLEM!) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST - "a") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|intermediate_value2_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL) (|intermediate_value2| "" (SKOSIMP) (("" (USE "intermediate_value1") (("" (ASSERT) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (INST 2 "a") (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST 2 "b") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|intermediate_value3_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL) (|intermediate_value3| "" (SKOSIMP) (("" (LEMMA "intermediate_value1" ("f" "-f!1" "x" "-x!1")) (("" (AUTO-REWRITE "opp_fun_continuous[J]" "-") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|intermediate_value4| "" (SKOSIMP) (("" (USE "intermediate_value3") (("" (ASSERT) (("" (SPLIT) (("1" (PROPAX) NIL NIL) ("2" (INST 2 "b") (("2" (ASSERT) NIL NIL)) NIL) ("3" (INST 2 "a") (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$continuous_functions_props.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properties of continuous functions [T1 -> T2] % % Applications of continuity_interval % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% continuous_functions_props[ T : TYPE FROM real] : THEORY BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) ENDASSUMING IMPORTING continuity_interval f : VAR [T -> real] a, b, c, d : VAR T sub_interval : LEMMA FORALL (c : T), (d : {x : T | c <= x}), (u : J[c, d]) : T_pred(u) %---------------------------------------- % Restriction to a sub-interval of T1 %---------------------------------------- R(f, (c : T), (d : {x : T | c <= x})) : [J[c,d] -> real] = LAMBDA (u : J[c, d]) : f(u) %----------------------------------------------------- % If f is continuous, its restriction is continuous %----------------------------------------------------- g : VAR { f | continuous(f) } continuous_in_subintervals : LEMMA a <= b IMPLIES continuous(R(g, a, b)) %------------------------------ % Intermediate value theorem %------------------------------ x, y, z : VAR real intermediate1 : PROPOSITION a <= b AND g(a) <= x AND x <= g(b) IMPLIES EXISTS c : a <= c AND c <= b AND g(c) = x intermediate2 : PROPOSITION a <= b AND g(b) <= x AND x <= g(a) IMPLIES EXISTS c : a <= c AND c <= b AND g(c) = x %---------------------------------- % Max and minimum in an interval %---------------------------------- max_in_interval : PROPOSITION a <= b IMPLIES EXISTS c : a <= c AND c <= b AND (FORALL d : a <= d AND d <= b IMPLIES g(d) <= g(c)) min_in_interval : PROPOSITION a <= b IMPLIES EXISTS c : a <= c AND c <= b AND (FORALL d : a <= d AND d <= b IMPLIES g(c) <= g(d)) %--------------------------------------------------------- % Injective, continuous functions are strictly monotone %--------------------------------------------------------- inj_continuous : LEMMA injective?(g) AND a <= b AND b <= c IMPLIES (g(a) <= g(b) AND g(b) <= g(c)) OR (g(c) <= g(b) AND g(b) <= g(a)) inj_monotone : PROPOSITION injective?(g) IFF strict_increasing(g) OR strict_decreasing(g) END continuous_functions_props $$$continuous_functions_props.prf (|continuous_functions_props| (|sub_interval_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|sub_interval| "" (SKOLEM!) (("" (LEMMA "connected_domain" ("x" "c!1" "y" "d!1" "z" "u!1")) (("" (ASSERT) NIL))))) (R_TCC1 "" (SKOLEM-TYPEPRED) (("" (USE "connected_domain" ("z" "u!1")) (("" (ASSERT) NIL))))) (|continuous_in_subintervals| "" (SKOSIMP :PREDS? T) (("" (AUTO-REWRITE "sub_interval") (("" (EXPAND "continuous") (("" (SKOLEM!) (("" (INST -3 "x0!1") (("" (REWRITE "continuity_def[J[a!1,b!1]]") (("" (REWRITE "continuity_def[T]") (("" (SKOLEM!) (("" (INST -3 "epsilon!1") (("" (SKOLEM!) (("" (INST 1 "delta!1") (("" (SKOSIMP) (("" (INST -3 "x!1") (("" (EXPAND "R") (("" (ASSERT) NIL))))))))))))))))))))))))))))) (|intermediate1| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "sub_interval") (("" (LEMMA "intermediate_value2[a!1, b!1]") (("" (INST -1 "R(g!1, a!1, b!1)" "x!1") (("" (REWRITE "continuous_in_subintervals") (("" (EXPAND "R") (("" (SKOLEM!) (("" (INST 1 "c!1") (("" (ASSERT) NIL))))))))))))))))))) (|intermediate2| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "sub_interval") (("" (LEMMA "intermediate_value4[a!1, b!1]") (("" (INST -1 "R(g!1, a!1, b!1)" "x!1") (("" (REWRITE "continuous_in_subintervals") (("" (EXPAND "R") (("" (SKOLEM!) (("" (INST 1 "c!1") (("" (ASSERT) NIL))))))))))))))))))) (|max_in_interval| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "sub_interval") (("" (LEMMA "maximum_exists[a!1, b!1]") (("" (INST -1 "R(g!1, a!1, b!1)") (("" (SPLIT) (("1" (GRIND :IF-MATCH NIL) (("1" (INST 1 "c!1") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (REWRITE "continuous_in_subintervals") NIL))))))))))))) (|min_in_interval| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "sub_interval") (("" (LEMMA "minimum_exists[a!1, b!1]") (("" (INST -1 "R(g!1, a!1, b!1)") (("" (SPLIT) (("1" (GRIND :IF-MATCH NIL) (("1" (INST 1 "c!1") (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (REWRITE "continuous_in_subintervals") NIL))))))))))))) (|inj_continuous| "" (SKOSIMP) (("" (EXPAND "injective?") (("" (ASSERT) (("" (CASE "g!1(a!1) <= g!1(c!1)") (("1" (GROUND) (("1" (LEMMA "intermediate1" ("g" "g!1" "a" "b!1" "b" "c!1" "x" "g!1(a!1)")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST -5 "a!1" "c!2") (("1" (ASSERT) NIL))))))))) ("2" (LEMMA "intermediate1" ("g" "g!1" "a" "a!1" "b" "b!1" "x" "g!1(c!1)")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST -5 "c!1" "c!2") (("2" (ASSERT) NIL))))))))))) ("2" (GROUND) (("1" (LEMMA "intermediate2" ("g" "g!1" "a" "a!1" "b" "b!1" "x" "g!1(c!1)")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST -4 "c!1" "c!2") (("1" (ASSERT) NIL))))))))) ("2" (LEMMA "intermediate2" ("g" "g!1" "a" "b!1" "b" "c!1" "x" "g!1(a!1)")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST -4 "c!2" "a!1") (("2" (ASSERT) NIL))))))))))))))))))) (|inj_monotone| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "strict_increasing") (("1" (EXPAND "strict_decreasing") (("1" (SKOSIMP*) (("1" (ASSERT) (("1" (EXPAND "injective?") (("1" (INST-CP -1 "x!1" "y!1") (("1" (INST -1 "x!2" "y!2") (("1" (ASSERT) (("1" (CASE "x!1 <= x!2") (("1" (LEMMA "inj_continuous" ("g" "g!1" "a" "x!1" "b" "x!2" "c" "y!2")) (("1" (ASSERT) (("1" (LEMMA "inj_continuous" ("g" "g!1" "a" "x!1" "b" "y!1" "c" "y!2")) (("1" (LEMMA "inj_continuous" ("g" "g!1" "a" "x!1" "b" "y!2" "c" "y!1")) (("1" (ASSERT) NIL))))))))) ("2" (LEMMA "inj_continuous" ("g" "g!1" "a" "x!2" "b" "x!1" "c" "y!1")) (("2" (ASSERT) (("2" (LEMMA "inj_continuous" ("g" "g!1" "a" "x!2" "b" "y!2" "c" "y!1")) (("2" (LEMMA "inj_continuous" ("g" "g!1" "a" "x!2" "b" "y!1" "c" "y!2")) (("2" (ASSERT) NIL))))))))))))))))))))))))))) ("2" (GRIND :IF-MATCH NIL) (("2" (INST-CP -3 "x1!1" "x2!1") (("2" (INST -3 "x2!1" "x1!1") (("2" (ASSERT) NIL))))))) ("3" (GRIND :IF-MATCH NIL) (("3" (INST-CP -3 "x1!1" "x2!1") (("3" (INST -3 "x2!1" "x1!1") (("3" (ASSERT) NIL)))))))))))) $$$derivative_props.pvs derivative_props [ T : TYPE FROM real ] : THEORY BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) not_one_element : ASSUMPTION FORALL (x : T) : EXISTS (y : T) : x /= y ENDASSUMING IMPORTING derivatives, continuous_functions_props f : VAR [T -> real] x, y, a, b, c : VAR T D : VAR real %-------------------------------------------- % Equivalent definitions of differentiation %-------------------------------------------- derivative_equivalence1 : LEMMA (derivable(f, x) AND deriv(f, x) = D) IFF convergence(NQ(f, x), 0, D) derivative_equivalence2 : LEMMA convergence(NQ(f, x), 0, D) IFF (EXISTS (phi : [T -> real]) : convergence(phi, x, 0) AND FORALL y : f(y) - f(x) = (y - x) * (D + phi(y))) derivative_equivalence2bug : LEMMA convergence(NQ(f, x), 0, D) IFF (EXISTS (phi : [T -> real]) : convergence(phi, x, 0) AND FORALL y : f(y) - f(x) = (y - x) * (D + phi(y))) %-------------------------------------- % Derivative at max and minimum of f % (in an interval ]a, b[) %-------------------------------------- deriv_maximum : PROPOSITION a < c AND c < b AND derivable(f, c) AND (FORALL x : a < x AND x < b IMPLIES f(x) <= f(c)) IMPLIES deriv(f, c) = 0 deriv_minimum : PROPOSITION a < c AND c < b AND derivable(f, c) AND (FORALL x : a < x AND x < b IMPLIES f(c) <= f(x)) IMPLIES deriv(f, c) = 0 %------------------------------------ % f constant on [a, b] %------------------------------------ deriv_constant1 : LEMMA a < c AND c < b AND (FORALL x : a < x AND x < b IMPLIES f(x) = f(c)) IMPLIES convergence(NQ(f, c), 0, 0) deriv_constant2 : LEMMA a < c AND c < b AND (FORALL x : a < x AND x < b IMPLIES f(x) = f(c)) IMPLIES derivable(f, c) AND deriv(f, c) = 0 %----------------------- % Mean value theorem %----------------------- mean_value_aux : LEMMA derivable(f) AND a < b AND f(a) = f(b) IMPLIES EXISTS c : a < c AND c < b AND deriv(f, c) = 0 mean_value : THEOREM derivable(f) AND a < b IMPLIES EXISTS c : a < c AND c < b AND deriv(f, c) * (b - a) = f(b) - f(a) %------------------------------------------ % Applications of the mean value theorem %------------------------------------------ g : VAR deriv_fun[T] nonneg_derivative : PROPOSITION increasing(g) IFF (FORALL x : deriv(g, x) >= 0) nonpos_derivative : PROPOSITION decreasing(g) IFF (FORALL x : deriv(g, x) <= 0) positive_derivative : PROPOSITION (FORALL x : deriv(g, x) > 0) IMPLIES strict_increasing(g) negative_derivative : PROPOSITION (FORALL x : deriv(g, x) < 0) IMPLIES strict_decreasing(g) null_derivative : PROPOSITION constant(g) IFF (FORALL x : deriv(g, x) = 0) END derivative_props $$$derivative_props.prf (|derivative_props| (|derivative_equivalence1_TCC1| "" (LEMMA "connected_domain") (("" (PROPAX) NIL NIL)) NIL) (|derivative_equivalence1_TCC2| "" (LEMMA "not_one_element") (("" (PROPAX) NIL NIL)) NIL) (|derivative_equivalence1| "" (SKOLEM!) (("" (REWRITE "convergence_equiv[(A[T](x!1))]") (("" (EXPAND "derivable") (("" (EXPAND "deriv") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|derivative_equivalence2| "" (GRIND :EXCLUDE ("abs" "adh") :REWRITES ("deriv_TCC[T]" "adherence_fullset[T]") :IF-MATCH NIL) (("1" (INST + "LAMBDA y : IF y=x!1 THEN 0 ELSE NQ(f!1, x!1)(y - x!1) - D!1 ENDIF") (("1" (SPLIT) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST - "epsilon!1") (("1" (SKOLEM!) (("1" (INST + "delta!1") (("1" (AUTO-REWRITE "abs") (("1" (SKOSIMP) (("1" (SMASH) (("1" (INST - "x!2 - x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -) (("2" (REDUCE) (("2" (AUTO-REWRITE "times_div2" "div_distributes_minus") (("2" (ASSERT) (("2" (USE "div_cancel3" ("y" "f!1(y!1) - f!1(x!1)")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST? -5) (("2" (SKOLEM!) (("2" (INST + "delta!1") (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) (("2" (INST - "x!1 + x!2") (("2" (INST - "x!1+x!2") (("2" (ASSERT) (("2" (USE "commutative_mult" ("x" "phi!1(x!1 + x!2)" "y" "x!1")) (("2" (REPLACE -1) (("2" (ASSERT) (("2" (REPLACE -9) (("2" (REWRITE "div_distributes" :DIR RL) (("2" (ASSERT) (("2" (CASE "FORALL (a:real), (c: nzreal): (a * c)/ c = a") (("1" (REWRITE -1 +) NIL NIL) ("2" (ASSERT :FNUMS 1) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|derivative_equivalence2bug| "" (GRIND :EXCLUDE ("abs" "adh") :REWRITES ("deriv_TCC[T]" "adherence_fullset[T]") :IF-MATCH NIL) (("1" (INST + "LAMBDA y : IF y=x!1 THEN 0 ELSE NQ(f!1, x!1)(y - x!1) - D!1 ENDIF") (("1" (SPLIT) (("1" (ASSERT) (("1" (SKOLEM!) (("1" (INST - "epsilon!1") (("1" (SKOLEM!) (("1" (INST + "delta!1") (("1" (AUTO-REWRITE "abs") (("1" (SKOSIMP) (("1" (SMASH) (("1" (INST - "x!2 - x!1") (("1" (ASSERT) NIL))))))))))))))))))) ("2" (DELETE -) (("2" (REDUCE) (("2" (AUTO-REWRITE "times_div2" "div_distributes_minus") (("2" (ASSERT) (("2" (USE "div_cancel3" ("y" "f!1(y!1) - f!1(x!1)")) (("2" (GROUND) NIL))))))))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))))) ("2" (INST? -5) (("2" (SKOLEM!) (("2" (INST + "delta!1") (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) (("2" (INST - "x!1 + x!2") (("2" (INST - "x!1+x!2") (("2" (ASSERT) (("2" (USE "commutative_mult" ("x" "phi!1(x!1 + x!2)" "y" "x!1")) (("2" (REPLACE -1) (("2" (ASSERT) (("2" (REPLACE -9) (("2" (REWRITE "div_distributes" :DIR RL) (("2" (ASSERT) (("2" (CASE "FORALL (a:real), (c: nzreal): (a * c)/ c = a") (("1" (ASSERT) NIL) ("2" (ASSERT :FNUMS 1) NIL))))))))))))))))))))))))))))))))) (|deriv_maximum| "" (SKOSIMP*) (("" (AUTO-REWRITE "deriv_TCC[T]") (("" (EXPAND "deriv") (("" (EXPAND "derivable") (("" (ASSERT) (("" (REWRITE "lim_fun_def[(A[T](c!1))]") (("" (EXPAND "convergent") (("" (SKOLEM!) (("" (CASE "l!1 <= 0 AND 0 <= l!1") (("1" (GROUND) NIL NIL) ("2" (DELETE 2) (("2" (EXPAND "convergence") (("2" (SPLIT) (("1" (NAME "E" "{ x : real| 0 < x AND x < b!1 - c!1}") (("1" (CASE "adh[(A[T](c!1))](E)(0)") (("1" (ASSERT) (("1" (USE "convergence_upper_bound[(A[T](c!1))]" ("f" "NQ(f!1, c!1)" "E" "E")) (("1" (GROUND) (("1" (USE "subset_convergence2[(A[T](c!1))]" ("E1" "E" "E2" "fullset[real]")) (("1" (ASSERT) (("1" (REWRITE "subset_fullset") NIL NIL)) NIL)) NIL) ("2" (REPLACE -2 + RL) (("2" (DELETE -1 -2 -3 -4 -5 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST? -4) (("2" (ASSERT) (("2" (REWRITE "div_mult_pos_le1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 -4 -5 2) (("2" (GRIND :EXCLUDE "abs" :IF-MATCH NIL) (("2" (INST 1 "min(e!1/2, (b!1-c!1)/2)") (("1" (GRIND) NIL NIL) ("2" (USE "connected_domain" ("x" "c!1" "y" "b!1")) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (NAME "E" "{ x : real | a!1 - c!1 < x AND x < 0}") (("2" (CASE "adh[(A[T](c!1))](E)(0)") (("1" (ASSERT) (("1" (USE "convergence_lower_bound[(A[T](c!1))]" ("f" "NQ(f!1, c!1)" "E" "E")) (("1" (GROUND) (("1" (USE "subset_convergence2[(A[T](c!1))]" ("E1" "E" "E2" "fullset[real]")) (("1" (ASSERT) (("1" (REWRITE "subset_fullset") NIL NIL)) NIL)) NIL) ("2" (REPLACE -2 + RL) (("2" (DELETE -1 -2 -3 -4 -5 2) (("2" (GRIND :IF-MATCH NIL) (("2" (INST? -4) (("2" (ASSERT) (("2" (REWRITE "div_mult_neg_le2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -3 -4 -5 2) (("2" (GRIND :EXCLUDE "abs" :IF-MATCH NIL) (("2" (INST 1 "max(-e!1/2, (a!1 - c!1)/2)") (("1" (GRIND) NIL NIL) ("2" (USE "connected_domain" ("x" "a!1" "y" "c!1")) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_minimum| "" (SKOSIMP) (("" (USE "deriv_maximum" ("f" "-f!1")) (("" (AUTO-REWRITE "opposite_derivable[T]" "deriv_opposite[T]") (("" (ASSERT) (("" (DELETE -1 -2 -3 2) (("" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_constant1| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC[T]" "A[T]") (("" (EXPAND "convergence") (("" (LEMMA "convergence_locally_constant" ("f" "NQ(f!1, c!1)" "E" "{x:real| abs(x) < min(c!1 - a!1, b!1 - c!1)}" "b" "0" "a" "0")) (("1" (GROUND) (("1" (GRIND :EXCLUDE ("min" "abs" "NQ" "adh") :IF-MATCH NIL) (("1" (INST? -4) (("1" (SKOLEM!) (("1" (INST 1 "min(delta!1, min(c!1 - a!1, b!1 - c!1))") (("1" (SKOSIMP) (("1" (INST? -4) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE -3 -4 -7) (("2" (EXPAND "min") (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) (("2" (INST -5 "c!1 + x!1") (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3 2) (("2" (LEMMA "deriv_TCC[T]" ("x" "c!1")) (("2" (GRIND :EXCLUDE ("abs" "min") :IF-MATCH NIL) (("2" (INST -3 "min(e!1, min(c!1 - a!1, b!1 - c!1))") (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_constant2| "" (SKOSIMP) (("" (REWRITE "derivative_equivalence1") (("" (FORWARD-CHAIN "deriv_constant1") NIL NIL)) NIL)) NIL) (|mean_value_aux_TCC1| "" (SKOSIMP*) (("" (EXPAND "derivable" -) (("" (INST?) NIL NIL)) NIL)) NIL) (|mean_value_aux| "" (SKOSIMP) (("" (CASE "FORALL (x : T) : a!1 <= x AND x <= b!1 IMPLIES f!1(x) = f!1(a!1)") (("1" (CASE "T_pred((a!1 + b!1)/2)") (("1" (INST 1 "(a!1 + b!1)/2") (("1" (ASSERT) (("1" (USE "deriv_constant2" ("a" "a!1" "b" "b!1" "c" "(a!1 + b!1)/2")) (("1" (GROUND) (("1" (SKOSIMP) (("1" (INST-CP -4 "(a!1+b!1)/2") (("1" (INST -4 "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (USE "connected_domain" ("x" "a!1" "y" "b!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (FORWARD-CHAIN "derivable_continuous2[T]") (("2" (CASE "f!1(x!1) < f!1(a!1)") (("1" (USE "min_in_interval[T]" ("a" "a!1" "b" "b!1")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (EXPAND "derivable") (("1" (INST -8 "c!1") (("1" (USE "deriv_minimum" ("a" "a!1" "b" "b!1" "c" "c!1")) (("1" (INST-CP -4 "x!1") (("1" (ASSERT) (("1" (INST 2 "c!1") (("1" (GROUND) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "connected_domain") (("2" (PROPAX) NIL NIL)) NIL)) NIL) ("2" (USE "max_in_interval[T]" ("a" "a!1" "b" "b!1")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST-CP -3 "x!1") (("1" (ASSERT) (("1" (EXPAND "derivable") (("1" (INST -8 "c!1") (("1" (USE "deriv_maximum" ("a" "a!1" "b" "b!1" "c" "c!1")) (("1" (INST 3 "c!1") (("1" (GROUND) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "connected_domain") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|mean_value_TCC1| "" (SKOSIMP*) (("" (EXPAND "derivable" -) (("" (INST?) NIL NIL)) NIL)) NIL) (|mean_value| "" (SKOSIMP) (("" (NAME-REPLACE "C" "b!1 - a!1" :HIDE? NIL) (("" (NAME-REPLACE "B" "f!1(b!1) - f!1(a!1)" :HIDE? NIL) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "derivatives[T]" :EXCLUDE ("derivable" "deriv") :ALWAYS? T) (("" (USE "mean_value_aux" ("f" "f!1 - (B/C) * (I[T] - const(a!1))")) (("" (GROUND) (("1" (SKOSIMP) (("1" (INST?) (("1" (EXPAND "derivable") (("1" (INST -6 "c!1") (("1" (ASSERT) (("1" (REWRITE "deriv_diff[T]") (("1" (CASE-REPLACE "deriv(f!1, c!1)= B/C") (("1" (REWRITE "div_cancel2") NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3 2) (("2" (GRIND) (("2" (CASE "(B/C) * (b!1 - a!1) = B") (("1" (ASSERT) NIL NIL) ("2" (REPLACE -2 1) (("2" (REWRITE "div_cancel2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nonneg_derivative_TCC1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable" -) (("" (INST?) NIL NIL)) NIL)) NIL) (|nonneg_derivative| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (EXPAND "increasing") (("" (PROP) (("1" (SKOSIMP*) (("1" (EXPAND "deriv") (("1" (USE "limit_ge1[(A[T](x!1))]") (("1" (GROUND) (("1" (EXPAND "derivable") (("1" (INST? -2) NIL NIL)) NIL) ("2" (DELETE -2 2) (("2" (GRIND :IF-MATCH NIL) (("2" (REWRITE "pos_div_ge") (("2" (GROUND) (("1" (INST -2 "x!1 + x!2" "x!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST -2 "x!1" "x!1+x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (USE "mean_value" ("a" "x!1" "b" "y!1")) (("2" (GROUND) (("2" (SKOSIMP) (("2" (INST?) (("2" (LEMMA "pos_times_ge" ("x" "deriv(g!1, c!1)" "y" "y!1 - x!1")) (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|nonpos_derivative| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (EXPAND "decreasing") (("" (PROP) (("1" (SKOSIMP*) (("1" (EXPAND "deriv") (("1" (USE "limit_le1[(A[T](x!1))]") (("1" (GROUND) (("1" (EXPAND "derivable") (("1" (INST? -2) NIL NIL)) NIL) ("2" (DELETE -2 2) (("2" (GRIND :IF-MATCH NIL) (("2" (REWRITE "neg_div_le") (("2" (GROUND) (("1" (INST -2 "x!1 + x!2" "x!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST -2 "x!1" "x!1+x!2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (USE "mean_value" ("a" "x!1" "b" "y!1")) (("2" (GROUND) (("2" (SKOSIMP) (("2" (INST?) (("2" (LEMMA "neg_times_le" ("x" "deriv(g!1, c!1)" "y" "y!1 - x!1")) (("1" (ASSERT) NIL NIL) ("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|positive_derivative| "" (EXPAND "strict_increasing") (("" (SKOSIMP* :PREDS? T) (("" (USE "mean_value" ("b" "y!1")) (("" (ASSERT) (("" (SKOSIMP) (("" (INST?) (("" (LEMMA "pos_times_gt" ("x" "deriv(g!1, c!1)" "y" "y!1 - x!1")) (("1" (ASSERT) NIL NIL) ("2" (EXPAND "derivable" -) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|negative_derivative| "" (EXPAND "strict_decreasing") (("" (SKOSIMP* :PREDS? T) (("" (USE "mean_value" ("a" "x!1")) (("" (ASSERT) (("" (SKOSIMP) (("" (INST?) (("" (LEMMA "neg_times_lt" ("x" "deriv(g!1, c!1)" "y" "y!1 - x!1")) (("1" (ASSERT) NIL NIL) ("2" (EXPAND "derivable" -) (("2" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|null_derivative| "" (APPLY (REPEAT* (THEN (SKOLEM!) (PROP)))) (("1" (AUTO-REWRITE "const_derivable2[T]" "deriv_const[T]") (("1" (CASE-REPLACE "g!1 = const(g!1(x!1))") (("1" (ASSERT) NIL NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (CASE "FORALL (x, y : T) : x < y IMPLIES g!1(x) = g!1(y)") (("1" (DELETE -2) (("1" (EXPAND "constant") (("1" (SKOSIMP) (("1" (INST-CP - "x!1" "y!1") (("1" (INST - "y!1" "x!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP) (("2" (USE "mean_value" ("b" "y!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$continuous_functions.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Continuous functions [ T -> real] % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% continuous_functions [ T : TYPE FROM real ] : THEORY BEGIN IMPORTING limit_of_functions f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] u : VAR real x, x0 : VAR T epsilon, delta : VAR posreal %-------------------- % Continuity at x0 %-------------------- continuous(f, x0) : bool = convergence(f, x0, f(x0)) %--- equivalent definitions ---% continuity_def : PROPOSITION continuous(f, x0) IFF FORALL epsilon : EXISTS delta : FORALL x : abs(x - x0) < delta IMPLIES abs(f(x) - f(x0)) < epsilon continuity_def2 : PROPOSITION continuous(f, x0) IFF convergent(f, x0) %------------------------------------------ % Operations preserving continuity at x0 %------------------------------------------ sum_continuous : PROPOSITION continuous(f1, x0) and continuous(f2, x0) implies continuous(f1 + f2, x0) diff_continuous : PROPOSITION continuous(f1, x0) and continuous(f2, x0) implies continuous(f1 - f2, x0) prod_continuous : PROPOSITION continuous(f1, x0) and continuous(f2, x0) implies continuous(f1 * f2, x0) const_continuous : PROPOSITION continuous(const(u), x0) scal_continuous : PROPOSITION continuous(f, x0) implies continuous(u * f, x0) opp_continuous : PROPOSITION continuous(f, x0) implies continuous(- f, x0) div_continuous : PROPOSITION continuous(f, x0) and continuous(g, x0) implies continuous(f/g, x0) inv_continuous : PROPOSITION continuous(g, x0) implies continuous(1/g, x0) identity_continuous : PROPOSITION continuous(I[T], x0) %--------------------------------------------- % Continuity of f in a subset of its domain %--------------------------------------------- E : VAR { S : setof[real] | subset?(S, T_pred) } F : VAR setof[real] continuous(f, E) : bool = FORALL (y : (E)) : convergence(f, E, y, f(y)) continuity_subset : PROPOSITION subset?(F, E) AND continuous(f, E) IMPLIES continuous(f, F) %--- Operation preserving continuity in E ---% sum_set_continuous : PROPOSITION continuous(f1, E) and continuous(f2, E) implies continuous(f1 + f2, E) diff_set_continuous : PROPOSITION continuous(f1, E) and continuous(f2, E) implies continuous(f1 - f2, E) prod_set_continuous : PROPOSITION continuous(f1, E) and continuous(f2, E) implies continuous(f1 * f2, E) const_set_continuous : PROPOSITION continuous(const(u), E) scal_set_continuous : PROPOSITION continuous(f, E) implies continuous(u * f, E) opp_set_continuous : PROPOSITION continuous(f, E) implies continuous(- f, E) div_set_continuous : PROPOSITION continuous(f, E) and continuous(g, E) implies continuous(f/g, E) inv_set_continuous : PROPOSITION continuous(g, E) implies continuous(1/g, E) identity_set_continuous : PROPOSITION continuous(I[T], E) %--------------------------------- % Continuity of f in its domain %--------------------------------- continuous(f) : bool = FORALL x0 : continuous(f, x0) continuous_def2 : PROPOSITION continuous(f) IFF continuous(f, T_pred) continuity_subset2 : PROPOSITION continuous(f) IMPLIES continuous(f, E) %--- Properties ---% continuous_fun: TYPE+ = { f | continuous(f) } nz_continuous_fun: TYPE = { g | continuous(g) } h, h1, h2: VAR continuous_fun h3: VAR nz_continuous_fun sum_fun_continuous : JUDGEMENT +(h1, h2) HAS_TYPE continuous_fun diff_fun_continuous : JUDGEMENT -(h1, h2) HAS_TYPE continuous_fun prod_fun_continuous : JUDGEMENT *(h1, h2) HAS_TYPE continuous_fun const_fun_continuous : JUDGEMENT const(u) HAS_TYPE continuous_fun scal_fun_continuous : JUDGEMENT *(u, h) HAS_TYPE continuous_fun opp_fun_continuous : JUDGEMENT -(h) HAS_TYPE continuous_fun div_fun_continuous : JUDGEMENT /(h, h3) HAS_TYPE continuous_fun id_fun_continuous : JUDGEMENT I[T] HAS_TYPE continuous_fun inv_fun_continuous : PROPOSITION continuous(1/h3) END continuous_functions $$$continuous_functions.prf (|continuous_functions| (|continuity_def| "" (AUTO-REWRITE ("adherence_fullset[T]" "convergence_def[T]" "continuous")) (("" (ASSERT) NIL NIL)) NIL) (|continuity_def2| "" (SKOLEM!) (("" (REWRITE "convergent_in_domain[T]") (("" (EXPAND "continuous") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|sum_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "sum_fun_convergent[T]")) NIL NIL) (|diff_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "diff_fun_convergent[T]")) NIL NIL) (|prod_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "prod_fun_convergent[T]")) NIL NIL) (|const_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "const_fun_convergent[T]" "adherence_fullset[T]")) NIL NIL) (|scal_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "scal_fun_convergent[T]")) NIL NIL) (|opp_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "opposite_fun_convergent[T]")) NIL NIL) (|div_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("cv_div[T]")) NIL NIL) (|inv_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("cv_inv[T]")) NIL NIL) (|identity_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "adherence_fullset[T]" "convergent_identity[T]")) NIL NIL) (|continuous_TCC1| "" (GRIND) NIL NIL) (|continuity_subset_TCC1| "" (GRIND :EXCLUDE "continuous") NIL NIL) (|continuity_subset| "" (SKOSIMP) (("" (EXPAND "continuous") (("" (SKOLEM-TYPEPRED) (("" (INST?) (("1" (FORWARD-CHAIN "subset_convergence[T]") (("1" (INST?) (("1" (ASSERT) NIL NIL) ("2" (TYPEPRED "E!1") (("2" (DELETE -4 2) (("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (REWRITE "member_adherent[T]") (("3" (DELETE -3 2 3) (("3" (TYPEPRED "E!1") (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|sum_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_sum[T]")) NIL NIL) (|diff_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_diff[T]")) NIL NIL) (|prod_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_prod[T]")) NIL NIL) (|const_set_continuous| "" (GRIND :EXCLUDE ("convergence" "adh") :REWRITES ("convergence_const[T]" "member_adherent[T]")) NIL NIL) (|scal_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_scal[T]")) NIL NIL) (|opp_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_opposite[T]")) NIL NIL) (|div_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_div[T]")) NIL NIL) (|inv_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_inv[T]")) NIL NIL) (|identity_set_continuous| "" (GRIND :EXCLUDE ("convergence" "adh") :REWRITES ("convergence_identity[T]" "member_adherent[T]")) NIL NIL) (|continuous_def2_TCC1| "" (GRIND) NIL NIL) (|continuous_def2| "" (GRIND :EXCLUDE "abs" :IF-MATCH NIL) NIL NIL) (|continuity_subset2| "" (SKOLEM-TYPEPRED) (("" (FLATTEN) (("" (REWRITE "continuous_def2") (("" (FORWARD-CHAIN "continuity_subset") (("" (REWRITE "subset_reflexive") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|continuous_fun_TCC1| "" (INST + "I[T]") (("" (REWRITE "continuous_def2") (("" (REWRITE "identity_set_continuous") (("" (REWRITE "subset_reflexive") NIL NIL)) NIL)) NIL)) NIL) (|sum_fun_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2" "sum_set_continuous" "subset_reflexive")) NIL NIL) (|diff_fun_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2" "diff_set_continuous" "subset_reflexive")) NIL NIL) (|prod_fun_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2" "prod_set_continuous" "subset_reflexive")) NIL NIL) (|const_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("const_continuous")) NIL NIL)) NIL) (|scal_fun_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2" "scal_set_continuous" "subset_reflexive")) NIL NIL) (|opp_fun_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2" "opp_set_continuous" "subset_reflexive")) NIL NIL) (|div_fun_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2" "div_set_continuous" "subset_reflexive")) NIL NIL) (|id_fun_continuous| "" (EXPAND "continuous") (("" (SKOLEM!) (("" (REWRITE "identity_continuous") NIL NIL)) NIL)) NIL) (|inv_fun_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuous_def2" "inv_set_continuous" "subset_reflexive")) NIL NIL)) $$$absolute_value.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properites of absolute value %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% absolute_value : THEORY BEGIN x, y : VAR real z : VAR nzreal null_abs : PROPOSITION abs(x) = 0 IFF x = 0 null_abs2 : PROPOSITION abs(0) = 0 positive_abs : PROPOSITION abs(z) > 0 diff_abs : PROPOSITION abs(x) - abs(y) <= abs(x - y) % sum_abs is triangle in prelude % sum_abs : PROPOSITION abs(x + y) <= abs(x) + abs(y) neg_abs : PROPOSITION abs(- x) = abs(x) % prod_abs is abs_mult in prelude % prod_abs : PROPOSITION abs(x * y) = abs(x) * abs(y) inverse_abs : PROPOSITION abs(1/z) = 1/abs(z) divide_abs : PROPOSITION abs(x/z) = abs(x)/abs(z) abs_abs : PROPOSITION abs(abs(x)) = abs(x) abs_square : PROPOSITION abs(x * x) = x * x %--- abs(x - y) as distance between x and y ---% t, a, b : VAR real diff_abs_commute : PROPOSITION abs(x - y) = abs(y - x) null_distance : PROPOSITION x = y IFF abs(x - y) = 0 triangle2 : PROPOSITION abs(x - t) < a AND abs(x - y) < b IMPLIES abs(t - y) < a + b END absolute_value $$$absolute_value.prf (|absolute_value| (|null_abs| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (ASSERT) NIL))))) ("2" (REPLACE -1) (("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))))) (|null_abs2| "" (EXPAND "abs") (("" (PROPAX) NIL))) (|positive_abs| "" (SKOLEM!) (("" (ASSERT) NIL))) (|diff_abs| "" (SKOLEM!) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))))) (|sum_abs| "" (LEMMA "triangle") (("" (PROPAX) NIL))) (|neg_abs| "" (SKOLEM!) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (ASSERT) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))))) (|prod_abs| "" (LEMMA "abs_mult") (("" (PROPAX) NIL))) (|inverse_abs| "" (SKOLEM!) (("" (EXPAND "abs") (("" (CASE "1 / z!1 < 0") (("1" (ASSERT) (("1" (REWRITE "quotient_neg_lt") (("1" (ASSERT) NIL))))) ("2" (ASSERT) (("2" (REWRITE "quotient_neg_lt") (("2" (ASSERT) NIL))))))))))) (|divide_abs| "" (SKOLEM!) (("" (LEMMA "times_div1" ("x" "x!1" "y" "1" "n0z" "z!1")) (("" (ASSERT) (("" (REPLACE -1 + RL) (("" (REWRITE "prod_abs") (("" (REWRITE "inverse_abs") (("" (ASSERT) NIL))))))))))))) (|abs_abs| "" (SKOLEM!) (("" (EXPAND "abs" 1 1) (("" (LIFT-IF) (("" (GROUND) NIL))))))) (|abs_square| "" (SKOLEM!) (("" (REWRITE "prod_abs") (("" (GRIND) NIL))))) (|diff_abs_commute| "" (SKOLEM!) (("" (LEMMA "neg_abs" ("x" "x!1 - y!1")) (("" (ASSERT) NIL))))) (|null_distance| "" (SKOLEM!) (("" (REWRITE "null_abs") (("" (GROUND) NIL))))) (|triangle2| "" (SKOSIMP) (("" (REWRITE "diff_abs_commute") (("" (LEMMA "sum_abs" ("x" "t!1 - x!1" "y" "x!1 - y!1")) (("" (ASSERT) NIL)))))))) $$$real_facts.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Properties of real numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_facts : THEORY BEGIN %---------------------------------------- % More properties of archimedean field %---------------------------------------- archimedean2 : THEOREM FORALL (x : posreal) : EXISTS (a : posnat) : 1/a < x archimedean3 : THEOREM FORALL (x : nonneg_real) : (FORALL (a : posnat) : x <= 1/a) implies x = 0 %------------------------------------------------- % Every real is between two successive integers %------------------------------------------------- nat_interval : LEMMA FORALL (x : nonneg_real) : EXISTS (a : nat) : a <= x and x < a + 1 int_interval : PROPOSITION FORALL (x : real) : EXISTS (a : integer) : a <= x and x < a +1 %--------------------------------------- % Short cuts for lub and glb of sets %--------------------------------------- U: VAR (bounded_above?) V: VAR (bounded_below?) x, y: VAR real epsilon: VAR posreal lub_is_bound: LEMMA FORALL (x: (U)): x <= lub(U) lub_is_lub: LEMMA lub(U) <= y IFF FORALL (x: (U)): x <= y adherence_sup: LEMMA FORALL epsilon: EXISTS (x: (U)): lub(U) - epsilon < x glb_is_bound: LEMMA FORALL (x: (V)): glb(V) <= x glb_is_glb: LEMMA y <= glb(V) IFF FORALL (x: (V)): y <= x adherence_inf: LEMMA FORALL epsilon: EXISTS (x: (V)): x < glb(V) + epsilon END real_facts $$$real_facts.prf (|real_facts| (|archimedean2| "" (SKOLEM!) (("" (LEMMA "axiom_of_archimedes" ("x" "1/x!1")) (("" (SKOLEM!) (("" (ASSERT) (("" (INST 1 "i!1") (("" (REWRITE "div_mult_pos_lt1") (("" (REWRITE "div_mult_pos_lt1") (("" (ASSERT) NIL))))))))))))))) (|archimedean3| "" (SKOSIMP) (("" (CASE "x!1 > 0") (("1" (LEMMA "archimedean2" ("x" "x!1")) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (PROPAX) NIL))) ("2" (ASSERT) NIL))))) (|nat_interval| "" (SKOLEM!) (("" (LEMMA "wf_nat") (("" (EXPAND "well_founded?") (("" (INST -1 "lambda (b : nat) : x!1 < b") (("" (BETA) (("" (SPLIT) (("1" (SKOLEM!) (("1" (TYPEPRED "y!1") (("1" (INST -2 "y!1 - 1") (("1" (ASSERT) NIL) ("2" (INST 2 "y!1 - 1") (("2" (ASSERT) NIL))))))))) ("2" (LEMMA "axiom_of_archimedes" ("x" "x!1")) (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))))) (|int_interval| "" (SKOLEM!) (("" (CASE "x!1 >= 0") (("1" (LEMMA "nat_interval" ("x" "x!1")) (("1" (SKOSIMP) (("1" (INST 1 "a!1") (("1" (ASSERT) NIL))))) ("2" (PROPAX) NIL))) ("2" (LEMMA "nat_interval" ("x" "- x!1")) (("1" (SKOSIMP) (("1" (CASE "a!1 = -x!1") (("1" (INST 2 "- a!1") (("1" (ASSERT) NIL))) ("2" (INST 3 "-a!1 - 1") (("2" (ASSERT) NIL))))))) ("2" (ASSERT) NIL))))))) (|lub_is_bound| "" (SKOLEM!) (("" (TYPEPRED "lub(U!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|lub_is_lub| "" (SKOLEM!) (("" (TYPEPRED "lub(U!1)") (("" (GRIND :IF-MATCH NIL) (("1" (INST? -3) (("1" (INST? -2) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (INST? -2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|adherence_sup| "" (SKOLEM!) (("" (USE "lub_is_lub" ("y" "lub(U!1) - epsilon!1")) (("" (ASSERT) (("" (SKOLEM!) (("" (INST + "x!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|glb_is_bound| "" (SKOLEM!) (("" (TYPEPRED "glb(V!1)") (("" (GRIND) NIL NIL)) NIL)) NIL) (|glb_is_glb| "" (SKOLEM!) (("" (TYPEPRED "glb(V!1)") (("" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST? -2) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|adherence_inf| "" (SKOLEM!) (("" (USE "glb_is_glb" ("y" "glb(V!1) + epsilon!1")) (("" (ASSERT) (("" (SKOLEM!) (("" (INST + "x!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$epsilon_lemmas.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Lemmas used for limits of product and inverse %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% epsilon_lemmas : THEORY BEGIN x1, x2, y1, y2 : VAR real e, e1, e2 : VAR posreal IMPORTING real_facts, absolute_value %--- Lemmas for product ---% prod_bound : LEMMA abs(x1 - y1) < e1 AND abs(x2 - y2) < e2 IMPLIES abs(x1 * x2 - y1 * y2) < e1 * e2 + abs(y1) * e2 + abs(y2) * e1 prod_epsilon : LEMMA EXISTS e1, e2 : e1 * e2 + abs(y1) * e2 + abs(y2) * e1 < e %--- Lemmas for inverse ---% inv_bound : LEMMA abs(x1 - y1) < e1 and e1 < abs(y1) and x1 /= 0 and y1 /= 0 IMPLIES abs(1/x1 - 1/y1) < e1 / (abs(y1) * (abs(y1) - e1)) inv_epsilon1 : LEMMA y1 /= 0 IMPLIES EXISTS e1 : e1 < abs(y1) and e1 < e * (abs(y1) - e1) inv_epsilon : LEMMA y1 /= 0 IMPLIES EXISTS e1 : e1 < abs(y1) and e1 / (abs(y1) * (abs(y1) - e1)) < e END epsilon_lemmas $$$epsilon_lemmas.prf (|epsilon_lemmas| (|prod_bound| "" (SKOSIMP) (("" (LEMMA "sum_abs") (("" (INST -1 "(x1!1 - y1!1) * x2!1" "(x2!1 - y2!1) * y1!1") (("" (AUTO-REWRITE "prod_abs") (("" (DO-REWRITE) (("" (ASSERT) (("" (CASE "abs(x2!1 - y2!1) * abs(y1!1) <= e2!1 * abs(y1!1)") (("1" (CASE "abs(x1!1 - y1!1) * abs(x2!1) < e1!1 * (abs(y2!1) + e2!1)") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (REWRITE "lt_times_lt_pos1" 1) (("2" (LEMMA "diff_abs") (("2" (INST -1 "x2!1" "y2!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (REWRITE "le_times_le_pos" 1) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_epsilon| "" (SKOLEM!) (("" (CASE "EXISTS (u, v, w : posreal) : u * v <= e!1/3 and abs(y1!1) * v < e!1/3 and abs(y2!1) * w < e!1/3") (("1" (SKOSIMP) (("1" (INST 1 "min(u!1, w!1)" "v!1") (("1" (CASE "min(u!1, w!1) * v!1 <= u!1 * v!1 and abs(y2!1) * min(u!1, w!1) <= abs(y2!1) * w!1") (("1" (FLATTEN) (("1" (ASSERT) NIL NIL)) NIL) ("2" (DELETE -1 -2 -3 2) (("2" (SPLIT) (("1" (REWRITE "both_sides_times_pos_le1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (REWRITE "le_times_le_pos") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (NAME "f" "e!1/3") (("2" (REPLACE -1) (("2" (CASE "FORALL (x : nonneg_real) : x * (f / (x+1)) < f") (("1" (INST-CP -1 "abs(y1!1)") (("1" (INST -1 "abs(y2!1)") (("1" (INST 1 "abs(y1!1) + 1" "f / (abs(y1!1) + 1)" "f / (abs(y2!1) + 1)") (("1" (SPLIT) (("1" (REWRITE "div_cancel1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (PROPAX) NIL NIL) ("3" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (SKOLEM!) (("2" (REWRITE "times_div1") (("2" (REWRITE "div_mult_pos_lt1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inv_bound_TCC1| "" (SKOSIMP) (("" (REWRITE "zero_times3") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|inv_bound| "" (SKOSIMP) (("" (ASSERT) (("" (LEMMA "null_abs" ("x" "x1!1")) (("" (REPLACE 1) (("" (GROUND) (("" (AUTO-REWRITE "zero_times3") (("" (CASE "abs(1 / x1!1 - 1 / y1!1) = abs(x1!1 - y1!1) / (abs(y1!1) * abs(x1!1))") (("1" (LEMMA "lt_div_lt_pos2") (("1" (INST - "abs(x1!1 - y1!1)" "abs(y1!1) * (abs(y1!1) - e1!1)" "abs(y1!1) * abs(x1!1)" "e1!1") (("1" (SPLIT) (("1" (ASSERT) NIL NIL) ("2" (PROPAX) NIL NIL) ("3" (DELETE -1 5) (("3" (REWRITE "both_sides_times_pos_le2") (("3" (USE "diff_abs" ("x" "y1!1" "y" "x1!1")) (("3" (REWRITE "diff_abs_commute" -2) (("3" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 5) (("2" (CASE "abs(y1!1) * (abs(y1!1) - e1!1) > 0") (("1" (ASSERT) NIL NIL) ("2" (DELETE 2) (("2" (REWRITE "pos_times_gt") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 5 -1) (("2" (AUTO-REWRITE "minus_div1" "divide_abs" "prod_abs") (("2" (ASSERT) (("2" (REWRITE "diff_abs_commute" 1) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inv_epsilon1| "" (SKOSIMP) (("" (LEMMA "null_abs" ("x" "y1!1")) (("" (ASSERT) (("" (CASE "EXISTS (c : posreal) : c < e!1 / (1 + e!1)") (("1" (SKOLEM!) (("1" (INST 3 "abs(y1!1) * c!1") (("1" (SPLIT) (("1" (LEMMA "both_sides_times_pos_lt2" ("pz" "abs(y1!1)" "x" "c!1" "y" "1")) (("1" (ASSERT) (("1" (CASE "e!1 / (1 + e!1) < (1 + e!1) / (1 + e!1)") (("1" (REWRITE "div_simp") (("1" (ASSERT) NIL NIL)) NIL) ("2" (REWRITE "both_sides_div_pos_lt1") NIL NIL)) NIL)) NIL)) NIL) ("2" (LEMMA "both_sides_times_pos_lt2") (("2" (INST -1 "abs(y1!1)" "c!1" "e!1 * (1 - c!1)") (("2" (ASSERT) (("2" (DELETE 2) (("2" (REWRITE "div_mult_pos_lt2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "pos_times_gt") NIL NIL)) NIL)) NIL) ("2" (DELETE 2 3 4) (("2" (INST 1 "e!1 / (2 + e!1)") (("2" (REWRITE "both_sides_div_pos_lt2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|inv_epsilon_TCC1| "" (SKOSIMP*) (("" (REWRITE "zero_times3") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|inv_epsilon| "" (SKOSIMP) (("" (LEMMA "null_abs" ("x" "y1!1")) (("" (ASSERT) (("" (LEMMA "inv_epsilon1" ("y1" "y1!1" "e" "e!1 * abs(y1!1)")) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST 3 "e1!1") (("1" (ASSERT) (("1" (REWRITE "div_mult_pos_lt1") (("1" (DELETE -2 4) (("1" (LEMMA "posreal_mult_closed" ("x" "abs(y1!1)" "y" "abs(y1!1) - e1!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "posreal_mult_closed") NIL NIL)) NIL)) NIL)) NIL)) NIL)) $$$real_fun_ops.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Operations on functions : [ T -> real] % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_fun_ops [ T : TYPE ] : THEORY BEGIN f1, f2 : VAR [T -> real] f3 : VAR [T -> nzreal] a : VAR real x : VAR T %------------------------------------------ % Conversion : real to constant function % (Already there in PVS2.3 prelude: K_conversion) % (Removed from PVS2.3.1 prelude) %------------------------------------------ const(a) : [T -> real] = LAMBDA x : a CONVERSION const %-------------- % Operations %-------------- +(f1, f2) : [T -> real] = LAMBDA x : f1(x) + f2(x); -(f1) : [T -> real] = LAMBDA x : -f1(x); *(f1, f2) : [T -> real] = LAMBDA x : f1(x) * f2(x); *(a, f1) : [T -> real] = LAMBDA x : a * f1(x); -(f1, f2) : [T -> real] = LAMBDA x : f1(x) - f2(x); /(f1, f3) : [T -> real] = LAMBDA x : f1(x) / f3(x); /(a, f3) : [T -> real] = LAMBDA x : a / f3(x); inv(f3) : [T -> real] = 1 / f3; abs(f1) : [T -> nonneg_real] = LAMBDA x : abs(f1(x)); %------------------ % Rewrite rules %------------------ diff_function : PROPOSITION f1 - f2 = f1 + (- f2) div_function : PROPOSITION f1 / f3 = f1 * (1 /f3) scal_function : PROPOSITION a * f1 = const(a) * f1 scaldiv_function : PROPOSITION a / f3 = const(a) / f3 negneg_function : PROPOSITION - (- f1) = f1 END real_fun_ops $$$real_fun_ops.prf (|real_fun_ops| (|diff_function| "" (SKOLEM!) (("" (AUTO-REWRITE-THEORY "real_fun_ops") (("" (APPLY-EXTENSIONALITY) NIL))))) (|div_function| "" (SKOLEM!) (("" (AUTO-REWRITE-THEORY "real_fun_ops") (("" (APPLY-EXTENSIONALITY) NIL))))) (|scal_function| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|scaldiv_function| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (GRIND) NIL NIL)) NIL)) NIL) (|negneg_function| "" (SKOLEM!) (("" (AUTO-REWRITE "-") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL)))))) $$$convergence_functions.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % General convergence of functions [T -> real] % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% convergence_functions [T : TYPE FROM real] : THEORY BEGIN IMPORTING real_fun_ops, epsilon_lemmas epsilon, delta : VAR posreal e, e1, e2 : VAR posreal E, E1, E2 : VAR setof[real] f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] l, l1, l2, a, b, z : VAR real x, y : VAR T %--------------------------- % Reals adherent to a set %--------------------------- adh(E) : setof[real] = { z | FORALL e : EXISTS x : E(x) AND abs(x - z) < e } member_adherent : LEMMA E(x) IMPLIES adh(E)(x) adherence_subset1 : LEMMA subset?(E1, E2) AND adh(E1)(z) IMPLIES adh(E2)(z) adherence_subset2 : LEMMA subset?(E1, E2) IMPLIES subset?(adh(E1), adh(E2)) adherence_prop1 : LEMMA FORALL e, E, (a : (adh(E))) : EXISTS x : E(x) AND abs(x - a) < e adherence_prop2 : LEMMA FORALL e1, e2, E, (a : (adh(E))) : EXISTS x : E(x) AND abs(x - a) < e1 AND abs(x - a) < e2 %------------------------------------------------------ % Definition of convergence and immediate properties %------------------------------------------------------ convergence(f, E, a, l) : bool = adh(E)(a) AND FORALL epsilon : EXISTS delta : FORALL x : E(x) AND abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon convergence_unicity : PROPOSITION FORALL E, f, a, l1, l2 : convergence(f, E, a, l1) AND convergence(f, E, a, l2) IMPLIES l1 = l2 subset_convergence : PROPOSITION subset?(E1, E2) IMPLIES FORALL f, (a : (adh(E1))), l : convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l) subset_convergence2 : PROPOSITION FORALL E1, E2, f, (a : (adh(E1))), l : subset?(E1, E2) AND convergence(f, E2, a, l) IMPLIES convergence(f, E1, a, l) convergence_in_domain : PROPOSITION FORALL f, x, l : E(x) AND convergence(f, E, x, l) IMPLIES l = f(x) %---------------------------------- % Limits and function operations %---------------------------------- convergence_sum : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 + f2, E, a, l1 + l2) convergence_opposite : PROPOSITION FORALL E, f1, a, l1 : convergence(f1, E, a, l1) IMPLIES convergence(- f1, E, a, - l1) convergence_diff : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 - f2, E, a, l1 - l2) convergence_prod : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) IMPLIES convergence(f1 * f2, E, a, l1 * l2) convergence_const : PROPOSITION FORALL E, (a : (adh(E))), b : convergence(const(b), E, a, b) convergence_scal : PROPOSITION FORALL E, f1, a, l1, b : convergence(f1, E, a, l1) IMPLIES convergence(b * f1, E, a, b * l1) convergence_inv : PROPOSITION FORALL E, g, a, l1: convergence(g, E, a, l1) AND l1 /= 0 IMPLIES convergence(1/g, E, a, 1/l1) convergence_div : PROPOSITION FORALL E, f, g, a, l1, l2 : convergence(f, E, a, l1) AND convergence(g, E, a, l2) AND l2 /= 0 IMPLIES convergence(f/g, E, a, l1/l2) %--------------------- % Identity function %--------------------- convergence_identity : PROPOSITION FORALL E, (a : (adh(E))) : convergence(I[T], E, a, a) %----------------------------- % Limit preserve order %----------------------------- convergence_order : PROPOSITION FORALL E, f1, f2, a, l1, l2 : convergence(f1, E, a, l1) AND convergence(f2, E, a, l2) AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x)) IMPLIES l1 <= l2 %------------------------------------------- % Bounds on function are bounds on limits %------------------------------------------- convergence_lower_bound : COROLLARY FORALL E, f, b, a, l : convergence(f, E, a, l) AND (FORALL x : E(x) IMPLIES b <= f(x)) IMPLIES b <= l convergence_upper_bound : COROLLARY FORALL E, f, b, a, l : convergence(f, E, a, l) AND (FORALL x : E(x) IMPLIES f(x) <= b) IMPLIES l <= b %-------------------------- % Function constant on E %-------------------------- convergence_locally_constant : PROPOSITION FORALL E, f, b, (a : (adh(E))) : (FORALL x : E(x) IMPLIES f(x) = b) IMPLIES convergence(f, E, a, b) %------------- % Squeezing %------------- convergence_squeezing : PROPOSITION FORALL f1, f2, f, a, l : convergence(f1, E, a, l) AND convergence(f2, E, a, l) AND (FORALL x : E(x) IMPLIES f1(x) <= f(x) AND f(x) <= f2(x)) IMPLIES convergence(f, E, a, l) END convergence_functions $$$convergence_functions.prf (|convergence_functions| (|member_adherent| "" (GRIND :DEFS NIL :REWRITES ("adh" "null_abs2")) NIL NIL) (|adherence_subset1| "" (GRIND :IF-MATCH NIL :DEFS NIL :REWRITES ("subset?" "member" "adh")) (("" (INST? -5) (("" (SKOSIMP) (("" (INST? -4) (("" (INST? 1) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|adherence_subset2| "" (EXPAND "subset?" 1 2) (("" (EXPAND "member") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "adherence_subset1") NIL NIL)) NIL)) NIL)) NIL) (|adherence_prop1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "adh") (("" (INST?) NIL NIL)) NIL)) NIL) (|adherence_prop2| "" (SKOLEM!) (("" (USE "adherence_prop1" ("e" "min(e1!1, e2!1)" "E" "E!1")) (("" (SKOSIMP) (("" (INST?) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_unicity| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (DELETE -1 -2 -3 -4) (("" (REWRITE "null_distance") (("" (NAME "eps" "abs(l1!1 - l2!1)") (("" (ASSERT) (("" (INST -2 "eps/2") (("" (INST -3 "eps/2") (("" (SKOSIMP*) (("" (LEMMA "adherence_prop2" ("E" "E!1" "e1" "delta!1" "e2" "delta!2" "a" "a!1")) (("" (SKOSIMP) (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (DELETE -2 -3 1) (("" (USE "triangle2" ("y" "l2!1" "b" "eps/2")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|subset_convergence| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (INST? -7) (("" (SKOLEM!) (("" (INST 1 "delta!1") (("" (SKOSIMP) (("" (INST? -5) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|subset_convergence2| "" (SKOSIMP) (("" (FORWARD-CHAIN "subset_convergence") (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|convergence_in_domain| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (REWRITE "null_distance") (("" (ASSERT) (("" (INST -5 "abs(l!1 - f!1(x!1))") (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) (("" (REWRITE "null_abs2") (("" (ASSERT) (("" (REWRITE "diff_abs_commute" -) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_sum| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (DELETE -1 -2 -3 -4 -5 -6) (("" (INST -1 "epsilon!1/2") (("" (INST -2 "epsilon!1/2") (("" (SKOSIMP*) (("" (INST 1 "min(delta!1, delta!2)") (("" (SKOSIMP) (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (LEMMA "sum_abs" ("x" "f1!1(x!1) - l1!1" "y" "f2!1(x!1) - l2!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_opposite| "" (GRIND :IF-MATCH NIL :EXCLUDE ("abs" "adh")) (("" (DELETE -1 -2 -3 -4 -5) (("" (INST -1 "epsilon!1") (("" (SKOLEM!) (("" (INST 1 "delta!1") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (LEMMA "neg_abs" ("x" "f1!1(x!1) - l1!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_diff| "" (SKOSIMP) (("" (REWRITE "diff_function") (("" (USE "convergence_sum" ("f2" "-f2!1" "l2" "-l2!1")) (("" (ASSERT) (("" (REWRITE "convergence_opposite") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_prod| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (DELETE -1 -2 -3 -4 -5 -6) (("" (LEMMA "prod_epsilon" ("y1" "l1!1" "y2" "l2!1" "e" "epsilon!1")) (("" (SKOLEM!) (("" (INST -2 "e1!1") (("" (INST -3 "e2!1") (("" (SKOSIMP*) (("" (INST 1 "min(delta!1, delta!2)") (("" (SKOSIMP) (("" (INST?) (("" (INST?) (("" (ASSERT) (("" (LEMMA "prod_bound") (("" (INST -1 "e1!1" "e2!1" "f1!1(x!1)" "f2!1(x!1)" "l1!1" "l2!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_const| "" (GRIND) NIL NIL) (|convergence_scal| "" (SKOSIMP) (("" (REWRITE "scal_function") (("" (REWRITE "convergence_prod") (("" (REWRITE "convergence_const") (("" (EXPAND "convergence" -) (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_inv| "" (GRIND :IF-MATCH NIL :EXCLUDE ("abs" "adh")) (("" (DELETE -1 -2 -3 -4 -5) (("" (LEMMA "inv_epsilon" ("y1" "l1!1" "e" "epsilon!1")) (("" (ASSERT) (("" (SKOSIMP) (("" (INST? -3) (("" (SKOLEM!) (("" (INST 2 "delta!1") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (LEMMA "inv_bound" ("e1" "e1!1" "x1" "g!1(x!1)" "y1" "l1!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_div| "" (SKOSIMP) (("" (REWRITE "div_function") (("" (ASSERT) (("" (USE "convergence_prod" ("l2" "1/l2!1")) (("" (ASSERT) (("" (REWRITE "convergence_inv") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_identity| "" (GRIND :EXCLUDE ("adh" "abs")) NIL NIL) (|convergence_order| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (DELETE -1 -2 -3 -4) (("" (CASE "l2!1 < l1!1") (("1" (NAME "eps" "(l1!1 - l2!1)/2") (("1" (ASSERT) (("1" (INST -3 "eps") (("1" (INST -4 "eps") (("1" (SKOSIMP*) (("1" (LEMMA "adherence_prop2" ("e1" "delta!1" "e2" "delta!2" "E" "E!1" "a" "a!1")) (("1" (SKOSIMP) (("1" (INST?) (("1" (INST?) (("1" (INST?) (("1" (ASSERT) (("1" (DELETE -2 -3) (("1" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|convergence_lower_bound| "" (SKOSIMP) (("" (USE "convergence_const" ("b" "b!1")) (("1" (USE "convergence_order" ("f2" "f!1")) (("1" (AUTO-REWRITE "const") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "convergence") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_upper_bound| "" (SKOSIMP) (("" (USE "convergence_const" ("b" "b!1")) (("1" (USE "convergence_order" ("f1" "f!1")) (("1" (AUTO-REWRITE "const") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (EXPAND "convergence") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_locally_constant| "" (GRIND :IF-MATCH NIL :EXCLUDE ("abs" "adh")) (("" (INST 1 "epsilon!1") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (EXPAND "abs") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_squeezing| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (DELETE -1 -2 -3 -4 -5) (("" (INST -1 "epsilon!1/2") (("" (INST -2 "epsilon!1/2") (("" (SKOSIMP*) (("" (INST 1 "min(delta!1, delta!2)") (("" (SKOSIMP) (("" (INST?) (("" (INST?) (("" (INST?) (("" (GROUND) (("" (DELETE -6) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$limit_of_functions.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Limit of a functions [T -> real] at a point a % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% limit_of_functions [ T : TYPE FROM real ] : THEORY BEGIN IMPORTING convergence_functions %------------------------------------------------ % Subtype of reals where the limit makes sense %------------------------------------------------ a, b, l, l1, l2 : VAR real c : VAR (adh[T](fullset[real])) f, f1, f2 : VAR [ T -> real] g : VAR [T -> nzreal] epsilon, delta : VAR posreal x : VAR T %--------------------------------------------------- % Convergence of f at a point a towards a limit l %--------------------------------------------------- convergence(f, a, l) : bool = convergence(f, fullset[real], a, l) convergence_def : LEMMA FORALL f, a, l : convergence(f, a, l) IFF adh[T](fullset[real])(a) AND FORALL epsilon : EXISTS delta : FORALL x : abs(x - a) < delta IMPLIES abs(f(x) - l) < epsilon adherence_fullset : LEMMA adh[T](fullset[real])(x) cv_unique : PROPOSITION convergence(f, a, l1) AND convergence(f, a, l2) IMPLIES l1 = l2 cv_in_domain : PROPOSITION convergence(f, x, l) IMPLIES l = f(x) %------------------------------------------- % convergence and operations on functions %------------------------------------------- cv_sum : PROPOSITION convergence(f1, a, l1) AND convergence(f2, a, l2) IMPLIES convergence(f1 + f2, a, l1 + l2) cv_diff : PROPOSITION convergence(f1, a, l1) AND convergence(f2, a, l2) IMPLIES convergence(f1 - f2, a, l1 - l2) cv_prod : PROPOSITION convergence(f1, a, l1) AND convergence(f2, a, l2) IMPLIES convergence(f1 * f2, a, l1 * l2) cv_const : PROPOSITION convergence(const(b), c, b) cv_scal : PROPOSITION convergence(f, a, l) IMPLIES convergence(b * f, a, b * l) cv_opp : PROPOSITION convergence(f, a, l) IMPLIES convergence(- f, a, - l) cv_div : PROPOSITION convergence(f, a, l1) AND convergence(g, a, l2) AND l2 /= 0 IMPLIES convergence(f / g, a, l1 / l2) cv_inv : PROPOSITION convergence(g, a, l) AND l /= 0 IMPLIES convergence(1 / g, a, 1 / l) cv_identity : PROPOSITION convergence(I[T], c, c) %------------------------- % f is convergent at a %------------------------- convergent(f, a) : bool = EXISTS l : convergence(f, a, l) lim(f, (x0 : {a | convergent(f, a)})) : real = epsilon(LAMBDA l : convergence(f, x0, l)) lim_fun_lemma : LEMMA FORALL f, (x0 : {a | convergent(f, a)}) : convergence(f, x0, lim(f, x0)) lim_fun_def : LEMMA FORALL f, l, (x0 : {a | convergent(f, a)}) : lim(f, x0) = l IFF convergence(f, x0, l) convergence_equiv : LEMMA convergence(f, a, l) IFF convergent(f, a) AND lim(f, a) = l convergent_in_domain : LEMMA convergent(f, x) IFF convergence(f, x, f(x)) limit_in_domain : LEMMA convergent(f, x) IMPLIES lim(f, x) = f(x) %------------------------------------------ % Operations preserving convergence at a %------------------------------------------ sum_fun_convergent : LEMMA convergent(f1, a) AND convergent(f2, a) IMPLIES convergent(f1 + f2, a) opposite_fun_convergent : LEMMA convergent(f, a) IMPLIES convergent(- f, a) diff_fun_convergent : LEMMA convergent(f1, a) AND convergent(f2, a) IMPLIES convergent(f1 - f2, a) prod_fun_convergent : LEMMA convergent(f1, a) AND convergent(f2, a) IMPLIES convergent(f1 * f2, a) const_fun_convergent : LEMMA convergent(const(b), c) scal_fun_convergent : LEMMA convergent(f, a) IMPLIES convergent(b * f, a) inv_fun_convergent : LEMMA convergent(g, a) AND lim(g, a) /= 0 IMPLIES convergent(1/g, a) div_fun_convergent : LEMMA convergent(f, a) AND convergent(g, a) AND lim(g, a) /= 0 IMPLIES convergent(f / g, a) convergent_identity : LEMMA convergent(I[T], c) %---------------------------- % Same things with lim(a) %---------------------------- limit_sum_fun : LEMMA convergent(f1, a) AND convergent(f2, a) IMPLIES lim(f1 + f2, a) = lim(f1, a) + lim(f2, a) limit_opposite_fun : LEMMA convergent(f, a) IMPLIES lim(- f, a) = - lim(f, a) limit_diff_fun : LEMMA convergent(f1, a) AND convergent(f2, a) IMPLIES lim(f1 - f2, a) = lim(f1, a) - lim(f2, a) limit_prod_fun : LEMMA convergent(f1, a) AND convergent(f2, a) IMPLIES lim(f1 * f2, a) = lim(f1, a) * lim(f2, a) limit_const_fun : LEMMA lim(const(b), c) = b limit_scal_fun : LEMMA convergent(f, a) IMPLIES lim(b * f, a) = b * lim(f, a) limit_inv_fun : LEMMA convergent(g, a) AND lim(g, a) /= 0 IMPLIES lim(1/g, a) = 1/lim(g, a) limit_div_fun : LEMMA convergent(f, a) AND convergent(g, a) AND lim(g, a) /= 0 IMPLIES lim(f / g, a) = lim(f, a)/lim(g, a) limit_identity : LEMMA lim(I[T], c) = c %-------------------- % Bounds on limits %-------------------- E : VAR setof[real] limit_le1 : LEMMA convergent(f, a) AND (FORALL x : f(x) <= b) IMPLIES lim(f, a) <= b limit_ge1 : LEMMA convergent(f, a) AND (FORALL x : f(x) >= b) IMPLIES lim(f, a) >= b limit_order1 : LEMMA convergent(f1, a) AND convergent(f2, a) AND (FORALL x : f1(x) <= f2(x)) IMPLIES lim(f1, a) <= lim(f2, a) limit_le2 : LEMMA convergent(f, a) AND adh[T](E)(a) AND (FORALL x : E(x) IMPLIES f(x) <= b) IMPLIES lim(f, a) <= b limit_ge2 : LEMMA convergent(f, a) AND adh[T](E)(a) AND (FORALL x : E(x) IMPLIES f(x) >= b) IMPLIES lim(f, a) >= b limit_order2: LEMMA convergent(f1, a) AND convergent(f2, a) AND adh[T](E)(a) AND (FORALL x : E(x) IMPLIES f1(x) <= f2(x)) IMPLIES lim(f1, a) <= lim(f2, a) END limit_of_functions $$$limit_of_functions.prf (|limit_of_functions| (|convergence_def| "" (EXPAND "convergence") (("" (EXPAND "convergence") (("" (EXPAND "fullset") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL) (|adherence_fullset| "" (AUTO-REWRITE "fullset" "member_adherent[T]") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|cv_unique| "" (SKOSIMP) (("" (EXPAND "convergence") (("" (USE "convergence_unicity[T]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|cv_in_domain| "" (SKOSIMP) (("" (EXPAND "convergence") (("" (USE "convergence_in_domain[T]") (("" (EXPAND "fullset") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|cv_sum| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_sum[T]") NIL NIL)) NIL) (|cv_diff| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_diff[T]") NIL NIL)) NIL) (|cv_prod| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_prod[T]") NIL NIL)) NIL) (|cv_const| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_const[T]") NIL NIL)) NIL) (|cv_scal| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_scal[T]") NIL NIL)) NIL) (|cv_opp| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_opposite[T]") NIL NIL)) NIL) (|cv_div| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_div[T]") NIL NIL)) NIL) (|cv_inv| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_inv[T]") NIL NIL)) NIL) (|cv_identity| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_identity[T]") NIL NIL)) NIL) (|lim_fun_lemma| "" (SKOLEM!) (("" (NAME-REPLACE "ll" "lim(f!1, x0!1)" :HIDE? NIL) (("" (EXPAND "lim" -) (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (l: real): convergence(f!1, x0!1, l)")) (("" (ASSERT) (("" (TYPEPRED "x0!1") (("" (EXPAND "convergent") (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|lim_fun_def| "" (SKOLEM!) (("" (USE "lim_fun_lemma") (("" (GROUND) (("" (USE "cv_unique" ("l2" "lim(f!1, x0!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|convergence_equiv| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "convergent") (("1" (INST?) NIL NIL)) NIL) ("2" (REWRITE "lim_fun_def") (("2" (EXPAND "convergent") (("2" (INST?) NIL NIL)) NIL)) NIL) ("3" (REWRITE "lim_fun_def") NIL NIL)) NIL)) NIL) (|convergent_in_domain| "" (GRIND :EXCLUDE "convergence") (("" (FORWARD-CHAIN "cv_in_domain") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_in_domain| "" (SKOSIMP) (("" (REWRITE "lim_fun_def") (("" (REWRITE "convergent_in_domain") NIL NIL)) NIL)) NIL) (|sum_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "l!1 + l!2") (("" (REWRITE "cv_sum") NIL NIL)) NIL)) NIL)) NIL) (|opposite_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "cv_opp") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|diff_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "l!1 - l!2") (("" (REWRITE "cv_diff") NIL NIL)) NIL)) NIL)) NIL) (|prod_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "l!1 * l!2") (("" (REWRITE "cv_prod") NIL NIL)) NIL)) NIL)) NIL) (|const_fun_convergent| "" (EXPAND "convergent") (("" (SKOLEM!) (("" (INST?) (("" (REWRITE "cv_const") NIL NIL)) NIL)) NIL)) NIL) (|scal_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "b!1 * l!1") (("" (REWRITE "cv_scal") NIL NIL)) NIL)) NIL)) NIL) (|inv_fun_convergent| "" (SKOSIMP) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergent") (("" (SKOSIMP) (("" (ASSERT) (("" (INST 2 "1/l!1") (("" (REWRITE "cv_inv") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|div_fun_convergent| "" (SKOSIMP) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (ASSERT) (("" (INST 2 "l!1 / l!2") (("" (REWRITE "cv_div") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|convergent_identity| "" (SKOLEM!) (("" (EXPAND "convergent") (("" (USE "cv_identity") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|limit_sum_fun_TCC1| "" (SKOSIMP) (("" (REWRITE "sum_fun_convergent") NIL NIL)) NIL) (|limit_sum_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "sum_fun_convergent" ("cv_sum")) (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_opposite_fun_TCC1| "" (LEMMA "opposite_fun_convergent") (("" (PROPAX) NIL NIL)) NIL) (|limit_opposite_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "opposite_fun_convergent" ("cv_opp")) (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_diff_fun_TCC1| "" (SKOSIMP) (("" (REWRITE "diff_fun_convergent") NIL NIL)) NIL) (|limit_diff_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "diff_fun_convergent" ("cv_diff")) (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_prod_fun_TCC1| "" (SKOSIMP) (("" (REWRITE "prod_fun_convergent") NIL NIL)) NIL) (|limit_prod_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "prod_fun_convergent" ("cv_prod")) (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_const_fun_TCC1| "" (LEMMA "const_fun_convergent") (("" (PROPAX) NIL NIL)) NIL) (|limit_const_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "const_fun_convergent" ("cv_const")) (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_scal_fun_TCC1| "" (LEMMA "scal_fun_convergent") (("" (PROPAX) NIL NIL)) NIL) (|limit_scal_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "scal_fun_convergent" "cv_scal") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_inv_fun_TCC1| "" (SKOSIMP) (("" (REWRITE "inv_fun_convergent") NIL NIL)) NIL) (|limit_inv_fun| "" (SKOSIMP) (("" (ASSERT) (("" (DELETE 1) (("" (AUTO-REWRITE "lim_fun_def" "lim_fun_lemma" "inv_fun_convergent" ("cv_inv")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|limit_div_fun_TCC1| "" (SKOSIMP) (("" (REWRITE "div_fun_convergent") NIL NIL)) NIL) (|limit_div_fun| "" (SKOSIMP) (("" (ASSERT) (("" (DELETE 1) (("" (AUTO-REWRITE "lim_fun_def" "lim_fun_lemma" "div_fun_convergent" "cv_div") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|limit_identity_TCC1| "" (LEMMA "convergent_identity") (("" (PROPAX) NIL NIL)) NIL) (|limit_identity| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "convergent_identity" "cv_identity") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|limit_le1| "" (SKOSIMP) (("" (ASSERT) (("" (NAME-REPLACE "ll" "lim(f!1, a!1)" :HIDE? NIL) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergence") (("" (USE "convergence_upper_bound[T]") (("" (GROUND) (("" (DELETE -1 -2 2) (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_ge1| "" (SKOSIMP) (("" (ASSERT) (("" (NAME-REPLACE "ll" "lim(f!1, a!1)" :HIDE? NIL) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergence") (("" (USE "convergence_lower_bound[T]" ("b" "b!1")) (("" (GROUND) (("" (DELETE -1 -2 2) (("" (GRIND :IF-MATCH NIL) (("" (INST?) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_order1| "" (SKOSIMP) (("" (ASSERT) (("" (NAME-REPLACE "ll1" "lim(f1!1, a!1)" :HIDE? NIL) (("" (NAME-REPLACE "ll2" "lim(f2!1, a!1)" :HIDE? NIL) (("" (REWRITE "lim_fun_def") (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergence") (("" (USE "convergence_order[T]" ("l1" "ll1" "l2" "ll2")) (("" (GROUND) (("" (EXPAND "fullset" +) (("" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_le2| "" (SKOSIMP) (("" (ASSERT) (("" (NAME-REPLACE "ll" "lim(f!1, a!1)" :HIDE? NIL) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergence") (("" (USE "subset_convergence2[T]" ("E1" "E!1")) (("" (GROUND) (("1" (DELETE -2 -3) (("1" (USE "convergence_upper_bound[T]") (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "subset_fullset") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_ge2| "" (SKOSIMP) (("" (ASSERT) (("" (NAME-REPLACE "ll" "lim(f!1, a!1)" :HIDE? NIL) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergence") (("" (USE "subset_convergence2[T]" ("E1" "E!1")) (("" (GROUND) (("1" (DELETE -2 -3) (("1" (USE "convergence_lower_bound[T]" ("b" "b!1")) (("1" (GROUND) (("1" (DELETE -1 -2 2) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REWRITE "subset_fullset") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|limit_order2| "" (SKOSIMP) (("" (ASSERT) (("" (NAME-REPLACE "ll1" "lim(f1!1, a!1)" :HIDE? NIL) (("" (NAME-REPLACE "ll2" "lim(f2!1, a!1)" :HIDE? NIL) (("" (REWRITE "lim_fun_def") (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergence") (("" (USE "subset_convergence2[T]" ("E1" "E!1")) (("" (USE "subset_convergence2[T]" ("E1" "E!1" "f" "f1!1")) (("" (REWRITE "subset_fullset") (("" (GROUND) (("" (DELETE -3 -4 -5 -6) (("" (FORWARD-CHAIN "convergence_order[T]") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) $$$derivatives.pvs derivatives [ T : TYPE FROM real ] : THEORY BEGIN ASSUMING connected_domain : ASSUMPTION FORALL (x, y : T), (z : real) : x <= z AND z <= y IMPLIES T_pred(z) not_one_element : ASSUMPTION FORALL (x : T) : EXISTS (y : T) : x /= y ENDASSUMING IMPORTING limit_of_functions, continuous_functions f, f1, f2 : VAR [T -> real] g : VAR [T -> nzreal] x : VAR T u : VAR nzreal b : VAR real l, l1, l2 : VAR real %------------------- % Newton Quotient %------------------- A(x) : setof[nzreal] = { u | T_pred(x + u) } NQ(f, x)(h : (A(x))) : real = (f(x + h) - f(x)) / h deriv_TCC : LEMMA FORALL x : adh[(A(x))](fullset[real])(0) %---------------------------- % Differentiable functions %---------------------------- derivable(f, x) : bool = convergent(NQ(f, x), 0) derivable(f) : bool = FORALL x : derivable(f, x) %-------------------------------------- % Derivable functions are continuous %-------------------------------------- continuous_lim : LEMMA convergence(LAMBDA (h : (A(x))) : f(x + h), 0, f(x)) IFF continuous(f, x) deriv_continuous : LEMMA convergence(NQ(f, x), 0, l) IMPLIES continuous(f, x) derivable_continuous : PROPOSITION derivable(f, x) IMPLIES continuous(f, x) derivable_continuous2 : PROPOSITION derivable(f) IMPLIES continuous(f) %--------------------- % Properties of NQ %--------------------- sum_NQ : LEMMA NQ(f1 + f2, x) = NQ(f1, x) + NQ(f2, x) opposite_NQ : LEMMA NQ(- f, x) = - NQ(f, x) diff_NQ : LEMMA NQ(f1 - f2, x) = NQ(f1, x) - NQ(f2, x) scal_NQ : LEMMA NQ(b * f, x) = b * NQ(f, x) const_NQ : LEMMA NQ(const(b), x) = const(0) identity_NQ : LEMMA NQ(I[T], x) = const(1) prod_NQ : LEMMA FORALL (h : (A(x))): NQ(f1 * f2, x)(h) = NQ(f1, x)(h) * f2(x) + NQ(f2, x)(h) * f1(x + h) limit_prod_NQ : LEMMA convergence(NQ(f1, x), 0, l1) AND convergence(NQ(f2, x), 0, l2) IMPLIES convergence(NQ(f1 * f2, x), 0, f2(x) * l1 + f1(x) * l2) inv_NQ : LEMMA FORALL (h : (A(x))) : NQ(1/g, x)(h) = - NQ(g, x)(h) / (g(x) * g(x + h)) limit_inv_NQ : LEMMA convergence(NQ(g, x), 0, l1) IMPLIES convergence(NQ(1/g, x), 0, - l1 / (g(x) * g(x))) %--------------------------------------- % Operations preserving derivability %--------------------------------------- sum_derivable : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES derivable(f1 + f2, x) opposite_derivable : LEMMA derivable(f, x) IMPLIES derivable(- f, x) diff_derivable : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES derivable(f1 - f2, x) prod_derivable : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES derivable(f1 * f2, x) scal_derivable : LEMMA derivable(f, x) IMPLIES derivable(b * f, x) const_derivable : LEMMA derivable(const(b), x) inv_derivable : LEMMA derivable(g, x) IMPLIES derivable(1/g, x) div_derivable : LEMMA derivable(f, x) AND derivable(g, x) IMPLIES derivable(f / g, x) identity_derivable : LEMMA derivable(I, x) sum_derivable2 : LEMMA derivable(f1) AND derivable(f2) IMPLIES derivable(f1 + f2) opposite_derivable2 : LEMMA derivable(f) IMPLIES derivable(- f) diff_derivable2 : LEMMA derivable(f1) AND derivable(f2) IMPLIES derivable(f1 - f2) prod_derivable2 : LEMMA derivable(f1) AND derivable(f2) IMPLIES derivable(f1 * f2) scal_derivable2 : LEMMA derivable(f) IMPLIES derivable(b * f) const_derivable2 : LEMMA derivable(const(b)) inv_derivable2 : LEMMA derivable(g) IMPLIES derivable(1/g) div_derivable2 : LEMMA derivable(f) AND derivable(g) IMPLIES derivable(f / g) identity_derivable2 : LEMMA derivable(I) %-------------- % Derivative %-------------- deriv(f, (x0 : { x | derivable(f, x) })) : real = lim(NQ(f, x0), 0) deriv_sum : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES deriv(f1 + f2, x) = deriv(f1, x) + deriv(f2, x) deriv_opposite : LEMMA derivable(f, x) IMPLIES deriv(- f, x) = - deriv(f, x) deriv_diff : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES deriv(f1 - f2, x) = deriv(f1, x) - deriv(f2, x) deriv_prod : LEMMA derivable(f1, x) AND derivable(f2, x) IMPLIES deriv(f1 * f2, x) = deriv(f1, x) * f2(x) + deriv(f2, x) * f1(x) deriv_const : LEMMA deriv(const(b), x) = 0 deriv_scal : LEMMA derivable(f, x) IMPLIES deriv(b * f, x) = b * deriv(f, x) deriv_inv : LEMMA derivable(g, x) IMPLIES deriv(1/g, x) = - deriv(g, x) / (g(x) * g(x)) deriv_div : LEMMA derivable(f, x) AND derivable(g, x) IMPLIES deriv(f / g, x) = (deriv(f, x) * g(x) - deriv(g, x) * f(x)) / (g(x) * g(x)) deriv_identity : LEMMA deriv(I[T], x) = 1 %----------------------------------- % Type of derivable functions %----------------------------------- deriv_fun : TYPE = { f | derivable(f) } nz_deriv_fun : TYPE = { g | derivable(g) } ff, ff1, ff2 : VAR deriv_fun gg : VAR nz_deriv_fun derivable_cont: JUDGEMENT deriv_fun SUBTYPE_OF continuous_fun[T] nz_derivable_cont: JUDGEMENT nz_deriv_fun SUBTYPE_OF nz_continuous_fun[T] derivable_sum: JUDGEMENT +(ff1, ff2) HAS_TYPE deriv_fun derivable_diff: JUDGEMENT -(ff1, ff2) HAS_TYPE deriv_fun derivable_prod: JUDGEMENT *(ff1, ff2) HAS_TYPE deriv_fun derivable_scal: JUDGEMENT *(b, ff) HAS_TYPE deriv_fun derivable_opp: JUDGEMENT -(ff) HAS_TYPE deriv_fun derivable_div: JUDGEMENT /(ff, gg) HAS_TYPE deriv_fun derivable_inv: JUDGEMENT /(b, gg) HAS_TYPE deriv_fun derivable_const: JUDGEMENT const(b) HAS_TYPE deriv_fun derivable_id: JUDGEMENT I[T] HAS_TYPE deriv_fun %------------------------ % Derivative function %------------------------ deriv(ff) : [T -> real] = LAMBDA x : deriv(ff, x) deriv_sum_fun : LEMMA deriv(ff1 + ff2) = deriv(ff1) + deriv(ff2) deriv_opp_fun : LEMMA deriv(- ff) = - deriv(ff) deriv_diff_fun : LEMMA deriv(ff1 - ff2) = deriv(ff1) - deriv(ff2) deriv_prod_fun : LEMMA deriv(ff1 * ff2) = deriv(ff1) * ff2 + deriv(ff2) * ff1 deriv_scal_fun : LEMMA deriv(b * ff) = b * deriv(ff) deriv_inv_fun : LEMMA deriv(1 / gg) = - deriv(gg) / (gg * gg) deriv_scaldiv_fun : LEMMA deriv(b / gg) = - (b * deriv(gg)) / (gg * gg) deriv_div_fun : LEMMA deriv(ff / gg) = (deriv(ff) * gg - deriv(gg) * ff) / (gg * gg) deriv_const_fun : LEMMA deriv(const(b)) = const(0) deriv_id_fun : LEMMA deriv(I) = const(1) END derivatives $$$derivatives.prf (|derivatives| (NQ_TCC1 "" (GRIND) NIL NIL) (|deriv_TCC| "" (AUTO-REWRITE "A") (("" (SKOLEM!) (("" (EXPAND "adh") (("" (EXPAND "fullset") (("" (LEMMA "not_one_element" ("x" "x!1")) (("" (SKOSIMP*) (("" (CASE "abs(y!1 - x!1) < e!1") (("1" (INST? 2) (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST 3 "if x!1 < y!1 then e!1/2 else -e!1/2 endif") (("1" (GRIND) NIL NIL) ("2" (USE "connected_domain" ("x" "y!1" "y" "x!1")) (("2" (GRIND) NIL NIL)) NIL) ("3" (USE "connected_domain" ("x" "x!1" "y" "y!1")) (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|continuous_lim| "" (GRIND :EXCLUDE ("abs" "adh") :REWRITES ("deriv_TCC" "adherence_fullset[T]") :IF-MATCH NIL) (("1" (INST? -4) (("1" (SKOLEM!) (("1" (INST + "delta!1") (("1" (SKOSIMP) (("1" (INST - "x!2 - x!1") (("1" (ASSERT) NIL NIL) ("2" (DELETE -5) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST? -4) (("2" (SKOLEM!) (("2" (INST + "delta!1") (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_continuous| "" (SKOSIMP) (("" (REWRITE "continuous_lim" :DIR RL) (("" (CASE-REPLACE "(LAMBDA (h: (A(x!1))): f!1(h + x!1)) = const(f!1(x!1)) + I[(A(x!1))] * NQ(f!1, x!1)") (("1" (DELETE -1) (("1" (AUTO-REWRITE-THEORY "limit_of_functions[(A(x!1))]" :EXCLUDE ("convergence" "convergence_def" "convergent" "lim" "lim_fun_lemma" "lim_fun_def") :ALWAYS? T) (("1" (AUTO-REWRITE "deriv_TCC") (("1" (GRIND :DEFS NIL) NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL)) NIL) ("3" (DELETE -1 2) (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|derivable_continuous| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "deriv_continuous") NIL NIL)) NIL)) NIL)) NIL) (|derivable_continuous2| "" (EXPAND "derivable") (("" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES "derivable_continuous") NIL NIL)) NIL)) NIL) (|sum_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|opposite_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|diff_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|scal_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|const_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|identity_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL NIL)) NIL)) NIL) (|prod_NQ| "" (GRIND) NIL NIL) (|limit_prod_NQ| "" (AUTO-REWRITE "deriv_TCC") (("" (SKOSIMP) (("" (NAME "F" "LAMBDA (h : (A(x!1))) : f1!1(x!1 + h)") (("1" (CASE-REPLACE "NQ(f1!1 * f2!1, x!1) = f2!1(x!1) * NQ(f1!1, x!1) + F * NQ(f2!1, x!1)") (("1" (AUTO-REWRITE-THEORY "limit_of_functions[(A(x!1))]" :EXCLUDE ("convergence" "convergence_def" "convergent" "lim" "lim_fun_def") :ALWAYS? T) (("1" (FORWARD-CHAIN "deriv_continuous" -3) (("1" (USE "continuous_lim") (("1" (REPLACE*) (("1" (GRIND :DEFS NIL) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 -3 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (DELETE 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 -2 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|inv_NQ| "" (GRIND) NIL NIL) (|limit_inv_NQ| "" (AUTO-REWRITE "deriv_TCC") (("" (SKOSIMP) (("" (NAME "F" "LAMBDA (h : (A(x!1))) : g!1(x!1 + h)") (("1" (CASE-REPLACE "NQ(1/g!1, x!1) = - NQ(g!1, x!1) / (g!1(x!1) * F)") (("1" (REWRITE "cv_div[(A(x!1))]") (("1" (REWRITE "cv_opp[(A(x!1))]") NIL NIL) ("2" (REWRITE "cv_scal[(A(x!1))]") (("2" (USE "continuous_lim" ("f" "g!1")) (("2" (GROUND) (("2" (FORWARD-CHAIN "deriv_continuous") NIL NIL)) NIL)) NIL)) NIL) ("3" (REPLACE -2 1 RL) (("3" (DELETE -1 -2 -3 2) (("3" (GRIND :REWRITES "zero_times3") NIL NIL)) NIL)) NIL)) NIL) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL NIL) ("2" (DELETE 2) (("2" (GRIND :REWRITES "zero_times3") NIL NIL)) NIL) ("3" (DELETE 2) (("3" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("3" (REPLACE -1 + RL) (("3" (DELETE -1 -2 2) (("3" (GRIND :REWRITES "zero_times3") NIL NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|sum_derivable| "" (AUTO-REWRITE "derivable" "sum_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "sum_fun_convergent[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|opposite_derivable| "" (AUTO-REWRITE "derivable" "opposite_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "opposite_fun_convergent[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|diff_derivable| "" (AUTO-REWRITE "derivable" "diff_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "diff_fun_convergent[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|prod_derivable| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (USE "limit_prod_NQ") (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|scal_derivable| "" (AUTO-REWRITE "derivable" "scal_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "scal_fun_convergent[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|const_derivable| "" (SKOLEM!) (("" (AUTO-REWRITE "derivable" "const_NQ" "deriv_TCC") (("" (ASSERT) (("" (LEMMA "const_fun_convergent[(A(x!1))]") (("" (INST - "0" "0") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|inv_derivable| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (USE "limit_inv_NQ") (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|div_derivable| "" (SKOSIMP) (("" (REWRITE "div_function[T]") (("" (REWRITE "prod_derivable") (("" (REWRITE "inv_derivable") NIL NIL)) NIL)) NIL)) NIL) (|identity_derivable| "" (SKOLEM!) (("" (AUTO-REWRITE "derivable" "identity_NQ" "deriv_TCC") (("" (ASSERT) (("" (USE "const_fun_convergent[(A(x!1))]" ("b" "1" "c" "0")) NIL NIL)) NIL)) NIL)) NIL) (|sum_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "sum_derivable") NIL NIL)) NIL) (|opposite_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "opposite_derivable") NIL NIL)) NIL) (|diff_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "diff_derivable") NIL NIL)) NIL) (|prod_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "prod_derivable") NIL NIL)) NIL) (|scal_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "scal_derivable") NIL NIL)) NIL) (|const_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "const_derivable") NIL NIL)) NIL) (|inv_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "inv_derivable") NIL NIL)) NIL) (|div_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "div_derivable") NIL NIL)) NIL) (|identity_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "identity_derivable") NIL NIL)) NIL) (|deriv_TCC1| "" (AUTO-REWRITE "derivable") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|deriv_sum_TCC1| "" (SKOSIMP) (("" (REWRITE "sum_derivable") NIL NIL)) NIL) (|deriv_sum| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "sum_derivable" "derivable" "deriv" "sum_NQ" "limit_sum_fun[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|deriv_opposite_TCC1| "" (LEMMA "opposite_derivable") (("" (PROPAX) NIL NIL)) NIL) (|deriv_opposite| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "opposite_derivable" "derivable" "deriv" "opposite_NQ" "limit_opposite_fun[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|deriv_diff_TCC1| "" (SKOSIMP) (("" (REWRITE "diff_derivable") NIL NIL)) NIL) (|deriv_diff| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "diff_derivable" "derivable" "deriv" "diff_NQ" "limit_diff_fun[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|deriv_prod_TCC1| "" (SKOSIMP) (("" (REWRITE "prod_derivable") NIL NIL)) NIL) (|deriv_prod| "" (SKOSIMP) (("" (USE "prod_derivable") (("" (ASSERT) (("" (AUTO-REWRITE "deriv" "deriv_TCC" "derivable" ("lim_fun_def[(A(x!1))]" "lim_fun_lemma[(A(x!1))]")) (("" (ASSERT) (("" (USE "limit_prod_NQ" ("l1" "lim(NQ(f1!1, x!1), 0)" "l2" "lim(NQ(f2!1, x!1), 0)")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_const_TCC1| "" (LEMMA "const_derivable") (("" (PROPAX) NIL NIL)) NIL) (|deriv_const| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "const_derivable" "derivable" "deriv" "const_NQ") (("" (ASSERT) (("" (USE "limit_const_fun[(A(x!1))]" ("b" "0" "c" "0")) NIL NIL)) NIL)) NIL)) NIL) (|deriv_scal_TCC1| "" (LEMMA "scal_derivable") (("" (PROPAX) NIL NIL)) NIL) (|deriv_scal| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "scal_derivable" "derivable" "deriv" "scal_NQ" "limit_scal_fun[(A(x!1))]") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|deriv_inv_TCC1| "" (LEMMA "inv_derivable") (("" (PROPAX) NIL NIL)) NIL) (|deriv_inv| "" (SKOSIMP) (("" (FORWARD-CHAIN "inv_derivable") (("" (ASSERT) (("" (AUTO-REWRITE "deriv" "deriv_TCC" "derivable" ("lim_fun_def[(A(x!1))]" "lim_fun_lemma[(A(x!1))]")) (("" (ASSERT) (("" (USE "limit_inv_NQ" ("l1" "lim(NQ(g!1, x!1), 0)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_div_TCC1| "" (SKOSIMP) (("" (REWRITE "div_derivable") NIL NIL)) NIL) (|deriv_div| "" (GRIND :DEFS NIL :REWRITES ("inv_derivable" "deriv_inv" "deriv_prod" "div_function[T]" "/")) NIL NIL) (|deriv_identity_TCC1| "" (LEMMA "identity_derivable") (("" (PROPAX) NIL NIL)) NIL) (|deriv_identity| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "identity_derivable" "derivable" "deriv" "identity_NQ") (("" (USE "limit_const_fun[(A(x!1))]" ("b" "1" "c" "0")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|derivable_cont| "" (SKOLEM!) (("" (REWRITE "derivable_continuous2") NIL NIL)) NIL) (|nz_derivable_cont| "" (SKOLEM!) (("" (REWRITE "derivable_continuous2") NIL NIL)) NIL) (|derivable_sum| "" (SKOLEM!) (("" (REWRITE "sum_derivable2") NIL NIL)) NIL) (|derivable_diff| "" (SKOLEM!) (("" (REWRITE "diff_derivable2") NIL NIL)) NIL) (|derivable_prod| "" (SKOLEM!) (("" (REWRITE "prod_derivable2") NIL NIL)) NIL) (|derivable_scal| "" (SKOLEM!) (("" (REWRITE "scal_derivable2") NIL NIL)) NIL) (|derivable_opp| "" (SKOLEM!) (("" (REWRITE "opposite_derivable2") NIL NIL)) NIL) (|derivable_div| "" (SKOLEM!) (("" (REWRITE "div_derivable2") NIL NIL)) NIL) (|derivable_inv| "" (SKOLEM!) (("" (CASE-REPLACE "b!1 / gg!1 = b!1 * (1 / gg!1)") (("1" (REWRITE "scal_derivable2") (("1" (REWRITE "inv_derivable2") NIL NIL)) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|derivable_const| "" (SKOLEM!) (("" (REWRITE "const_derivable2") NIL NIL)) NIL) (|derivable_id| "" (LEMMA "identity_derivable2") (("" (PROPAX) NIL NIL)) NIL) (|deriv_TCC2| "" (AUTO-REWRITE "derivable" "deriv_TCC") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) (("" (INST?) NIL NIL)) NIL)) NIL)) NIL) (|deriv_sum_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "+" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_sum") (("1" (INST?) NIL NIL) ("2" (INST? -2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_opp_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "-" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_opposite") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_diff_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "-" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_diff") (("1" (INST?) NIL NIL) ("2" (INST? -2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_prod_fun| "" (AUTO-REWRITE "*" "+") (("" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "deriv") (("" (REWRITE "deriv_prod") (("1" (INST?) NIL NIL) ("2" (INST? -2) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_scal_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "*" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_scal") (("" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_inv_fun_TCC1| "" (SKOSIMP) (("" (EXPAND "*") (("" (REWRITE "zero_times3") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|deriv_inv_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (EXPAND "/" 1 2) (("1" (EXPAND "-" +) (("1" (EXPAND "*" +) (("1" (EXPAND "deriv") (("1" (REWRITE "deriv_inv") (("1" (INST?) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -) (("2" (GRIND :REWRITES "zero_times3") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_scaldiv_fun| "" (SKOLEM!) (("" (CASE-REPLACE "b!1 / gg!1 = b!1 * (1/gg!1)") (("1" (REWRITE "deriv_scal_fun") (("1" (REWRITE "deriv_inv_fun") (("1" (DELETE -) (("1" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (AUTO-REWRITE-THEORY "real_fun_ops[T]") (("1" (ASSERT) NIL NIL)) NIL) ("2" (GRIND :REWRITES "zero_times3") NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_div_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (INST?) (("1" (INST?) (("1" (EXPAND "/" 1 2) (("1" (EXPAND "-" +) (("1" (EXPAND "*") (("1" (EXPAND "deriv") (("1" (REWRITE "deriv_div") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -) (("2" (GRIND :REWRITES "zero_times3") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|deriv_const_fun| "" (SKOLEM!) (("" (AUTO-REWRITE "deriv_const" "const_derivable" "const") (("" (EXPAND "deriv") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) NIL) (|deriv_id_fun| "" (AUTO-REWRITE "I" "const" "deriv_identity" "identity_derivable") (("" (EXPAND "deriv") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL NIL)) NIL)) NIL)) $$$top_derivative.pvs top_derivative : THEORY BEGIN IMPORTING derivatives, derivative_props, chain_rule END top_derivative