%Patch files loaded: patch2 version 2.414 $$$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?(g) AND strict_increasing(g) IMPLIES continuous(inverse(g)) inverse_decr : LEMMA bijective?(g) AND strict_decreasing(g) IMPLIES continuous(inverse(g)) inverse_continuous : PROPOSITION bijective?(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))))))))))))))) (|adherence_lemma2| "" (SKOSIMP) (("" (USE "lim_fun_lemma[T1]") (("" (FORWARD-CHAIN "adherence_lemma") 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))))))))))))))))))))) (|convergent_composition| "" (LEMMA "convergence_composition") (("" (GRIND :DEFS NIL :REWRITES ("convergent[T1]" "convergent[T2]")) (("" (REWRITE "lim_fun_def[T1]" :DIR RL) (("" (INST?) NIL))))))) (|limit_composition_TCC1| "" (LEMMA "convergent_composition") (("" (PROPAX) NIL))) (|limit_composition_TCC2| "" (SKOSIMP) NIL) (|limit_composition_TCC3| "" (SKOSIMP) 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))))))))))))) (|convergence_comp_continuous| "" (SKOSIMP) (("" (EXPAND "continuous") (("" (FORWARD-CHAIN "convergence_composition") 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))))))))))))) (|limit_comp_continuous_TCC1| "" (LEMMA "convergent_comp_continuous") (("" (PROPAX) NIL))) (|limit_comp_continuous_TCC2| "" (SKOSIMP) NIL) (|limit_comp_continuous_TCC3| "" (SKOSIMP) 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)))))))))))) $$$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))) (|chain_rule_TCC2| "" (LEMMA "not_one_element1") (("" (PROPAX) NIL))) (|chain_rule_TCC3| "" (SKOSIMP) (("" (LEMMA "connected_domain2") (("" (PROPAX) NIL))))) (|chain_rule_TCC4| "" (SKOSIMP) (("" (LEMMA "not_one_element2") (("" (PROPAX) NIL))))) (|chain_rule| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC[T1]" "deriv_TCC[T2]" "adherence_fullset[T1]" "adherence_fullset[T2]") (("" (USE "derivative_equivalence1[T1]") (("1" (REPLACE -2) (("1" (PROP) (("1" (FORWARD-CHAIN "derivable_continuous[T1]") (("1" (DELETE -2 -3) (("1" (EXPAND "continuous") (("1" (REWRITE "derivative_equivalence2[T1]") (("1" (REWRITE "derivative_equivalence2[T1]") (("1" (REWRITE "derivative_equivalence2[T2]") (("1" (SKOSIMP*) (("1" (INST 1 "DG!1 * phi!1 + DF!1 * (phi!2 o f!1) + phi!1 * (phi!2 o f!1)") (("1" (PROP) (("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))))))))) ("2" (DELETE -1 -2 -4) (("2" (SKOLEM!) (("2" (INST -1 "y!1") (("2" (INST -2 "f!1(y!1)") (("2" (GRIND) NIL))))))))))))))) ("2" (LEMMA "not_one_element2") (("2" (PROPAX) NIL))) ("3" (LEMMA "connected_domain2") (("3" (PROPAX) NIL))))) ("2" (LEMMA "not_one_element1") (("2" (PROPAX) NIL))) ("3" (LEMMA "connected_domain1") (("3" (PROPAX) NIL))))) ("2" (LEMMA "not_one_element1") (("2" (PROPAX) NIL))) ("3" (LEMMA "connected_domain1") (("3" (PROPAX) NIL))))))))))))))) ("2" (LEMMA "not_one_element1") (("2" (PROPAX) NIL))) ("3" (LEMMA "connected_domain1") (("3" (PROPAX) NIL))))))))) (|composition_derivable_TCC1| "" (SKOSIMP) (("" (LEMMA "connected_domain2") (("" (PROPAX) NIL))))) (|composition_derivable_TCC2| "" (SKOSIMP) (("" (LEMMA "not_one_element2") (("" (PROPAX) NIL))))) (|composition_derivable| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "chain_rule") (("" (INST?) NIL))))))))) (|composition_derivable2_TCC1| "" (SKOSIMP) (("" (LEMMA "connected_domain2") (("" (PROPAX) NIL))))) (|composition_derivable2_TCC2| "" (SKOSIMP) (("" (LEMMA "not_one_element2") (("" (PROPAX) NIL))))) (|composition_derivable2| "" (EXPAND "derivable") (("" (SKOSIMP*) (("" (REWRITE "composition_derivable") (("1" (INST?) NIL) ("2" (INST? -2) NIL))))))) (|deriv_composition_TCC1| "" (LEMMA "composition_derivable") (("" (PROPAX) NIL))) (|deriv_composition_TCC2| "" (SKOSIMP) NIL) (|deriv_composition_TCC3| "" (SKOSIMP) 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)))]")) (("1" (ASSERT) (("1" (REWRITE "lim_fun_def[(A[T1](x!1))]") (("1" (REWRITE "chain_rule") NIL) ("2" (SKOSIMP) NIL))))) ("2" (SKOSIMP) NIL))))))) (|gg_TCC1| "" (LEMMA "connected_domain2") (("" (PROPAX) NIL))) (|gg_TCC2| "" (LEMMA "not_one_element2") (("" (PROPAX) NIL))) (|deriv_comp_fun_TCC1| "" (SKOSIMP) (("" (REWRITE "composition_derivable2") NIL))) (|deriv_comp_fun_TCC2| "" (SKOSIMP) (("" (ASSERT) 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) ("2" (INST? -2) 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 1 (_ "u!1")) (("" (INDUCT "n") (("1" (INST?) (("1" (SKOSIMP) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (INST 1 "IF u!1(i!1) <= u!1(j!1+1) THEN i!1 ELSE j!1+1 ENDIF") (("2" (SKOSIMP) (("2" (INST -1 "j!2") (("2" (LIFT-IF) (("2" (GROUND) NIL))))))))))))))) (|minimum_suffix| "" (GRIND :IF-MATCH NIL) (("" (USE "minimum_prefix" ("n" "n!1")) (("" (SKOLEM!) (("" (INST 1 "IF u!1(i!2) <= u!1(i!1) THEN i!2 ELSE i!1 ENDIF") (("" (SKOLEM!) (("" (INST -1 "j!1") (("" (INST -5 "j!1") (("" (LIFT-IF) (("" (GROUND) NIL))))))))))))))))) (|min_prop| "" (SKOLEM!) (("" (NAME-REPLACE "m" "mini(v!1, n!1)" :HIDE? NIL) (("" (EXPAND "mini") (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (i: nat): n!1 <= i AND FORALL (j: nat): n!1 <= j IMPLIES v!1(i) <= v!1(j)")) (("" (REPLACE -2) (("" (ASSERT) (("" (SPLIT) (("1" (PROPAX) NIL) ("2" (TYPEPRED "v!1") (("2" (INST?) (("2" (EXPAND "has_minimum") (("2" (PROPAX) NIL))))))))))))))))))))) (|min_prop1| "" (SKOLEM!) (("" (USE "min_prop") (("" (FLATTEN) (("" (PROPAX) NIL))))))) (|min_prop2| "" (SKOSIMP) (("" (USE "min_prop") (("" (FLATTEN) (("" (INST?) (("" (ASSERT) 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))))))))))) (|hseq_extraction| "" (SKOLEM!) (("" (EXPAND "subseq") (("" (EXPAND "hseq") (("" (INST 1 "h(v!1)") (("1" (ASSERT) NIL) ("2" (REWRITE "h_increasing") NIL))))))))) (|hseq_increasing| "" (SKOLEM!) (("" (REWRITE "incr_condition") (("" (SKOLEM!) (("" (EXPAND "hseq") (("" (NAME-REPLACE "k" "h(v!1)(i!1)" :HIDE? NIL) (("" (EXPAND "h" -1) (("" (LIFT-IF) (("" (PROP) (("1" (USE "min_prop2" ("i" "h(v!1)(1 + i!1)")) (("1" (ASSERT) NIL))) ("2" (ASSERT) (("2" (USE "min_prop2" ("i" "h(v!1)(1 + i!1)")) (("2" (ASSERT) (("2" (USE "h_increasing") (("2" (EXPAND "strict_increasing") (("2" (INST -1 "i!1 - 1" "1 + i!1") (("2" (ASSERT) NIL))))))))))))))))))))))))))))) (|no_minimum| "" (SKOLEM-TYPEPRED) (("" (FORWARD-CHAIN "minimum_suffix") 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) ("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))))))))))))))))))))))))))))) (|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))))))))) (|gseq_extraction| "" (SKOLEM!) (("" (EXPAND "subseq") (("" (EXPAND "gseq") (("" (INST 1 "g(w!1)") (("1" (ASSERT) NIL) ("2" (REWRITE "g_increasing") NIL))))))))) (|gseq_decreasing| "" (SKOLEM!) (("" (REWRITE "strict_decr_condition") (("" (SKOLEM!) (("" (EXPAND "gseq") (("" (EXPAND "g" 1 1) (("" (REWRITE "pick_prop2") NIL))))))))))) (|suffix_subseq| "" (GRIND :IF-MATCH NIL) (("" (INST 1 "LAMBDA i : i+n!1") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (ASSERT) NIL))))))) (|suffix_hasmin| "" (GRIND :IF-MATCH NIL) (("1" (INST? 1) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST -3 "j!1 - n!1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))) ("2" (INST 1 "i!1 - n!1") (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))) (|monotone_subsequence| "" (SKOSIMP) (("" (CASE "FORALL n : has_minimum(u!1, n)") (("1" (ASSERT) (("1" (INST 1 "hseq(u!1)") (("1" (PROP) (("1" (REWRITE "hseq_extraction") NIL) ("2" (REWRITE "hseq_increasing") NIL))))))) ("2" (SKOLEM!) (("2" (REWRITE "suffix_hasmin" :DIR RL) (("2" (ASSERT) (("2" (INST 2 "gseq(suffix(u!1, n!1))") (("2" (PROP) (("1" (USE "gseq_extraction") (("1" (USE "suffix_subseq") (("1" (FORWARD-CHAIN "transitive_subseq") NIL))))) ("2" (REWRITE "strict_decr_to_decr[nat]") (("2" (REWRITE "gseq_decreasing") NIL)))))))))))))))))) $$$real_sets.pvs %%%%%%%%%%%%%%%%%%%%%%%%%% % Sets of real numbers % bounds and extrema %%%%%%%%%%%%%%%%%%%%%%%%%% real_sets : THEORY BEGIN IMPORTING real_facts E, E1, E2 : VAR setof[real] S, S1, S2 : VAR (nonempty?[real]) a, b, c, x, y, z : VAR real epsilon : VAR posreal %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Sets bounded from above %%%%%%%%%%%%%%%%%%%%%%%%%%%%% %----------------------- % Definition and type %----------------------- above_bounded(E) : bool = EXISTS a : upper_bound?(a, E) sup_set : TYPE = { S | above_bounded(S) } U, U1, U2 : VAR sup_set %------------------------------------------------- % Existence and uniqueness of least upper bound %------------------------------------------------- sup_exists : LEMMA EXISTS a : least_upper_bound?(a, U) sup_is_unique : LEMMA least_upper_bound?(a, S) and least_upper_bound?(b, S) implies a = b %--------------------- % Definition of sup %--------------------- sup(U) : real = epsilon(LAMBDA x : least_upper_bound?(x, U)) sup_lemma : LEMMA least_upper_bound?(sup(U), U) sup_def : THEOREM sup(U) = x IFF least_upper_bound?(x, U) %--------------------- % Easy consequences %--------------------- sup_is_bound : COROLLARY member(x, U) implies x <= sup(U) sup_is_sup : COROLLARY upper_bound?(x, U) IFF sup(U) <= x %--------------------- % Inclusion and sup %--------------------- upper_bound_subset : LEMMA subset?(E1, E2) and upper_bound?(a, E2) implies upper_bound?(a, E1) subset_above_bounded : COROLLARY subset?(E, U) implies above_bounded(E) sup_of_subset : COROLLARY subset?(U1, U2) implies sup(U1) <= sup(U2) %----------------------------- % sup(U) is adherent to U %----------------------------- adherence_sup : THEOREM FORALL epsilon : EXISTS x : member(x, U) and sup(U) - epsilon < x %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Sets bounded from below %%%%%%%%%%%%%%%%%%%%%%%%%%%%% %----------------------- % Definition and type %----------------------- below_bounded(E) : bool = EXISTS a : lower_bound?(a, E) inf_set : TYPE = { S | below_bounded(S) } V, V1, V2 : VAR inf_set %------------------------------------------------- % Existence and uniqueness of greatest lower bound %------------------------------------------------- inf_exists : LEMMA EXISTS a : greatest_lower_bound?(a, V) inf_is_unique : LEMMA greatest_lower_bound?(a, S) and greatest_lower_bound?(b, S) implies a = b %--------------------- % Definition of inf %--------------------- inf(V) : real = epsilon(LAMBDA x : greatest_lower_bound?(x, V)) inf_lemma : LEMMA greatest_lower_bound?(inf(V), V) inf_def : THEOREM inf(V) = x IFF greatest_lower_bound?(x, V) %--------------------- % Easy consequences %--------------------- inf_is_bound : COROLLARY member(x, V) implies inf(V) <= x inf_is_inf : COROLLARY lower_bound?(x, V) IFF x <= inf(V) %--------------------- % Inclusion and inf %--------------------- lower_bound_subset : LEMMA subset?(E1, E2) and lower_bound?(a, E2) implies lower_bound?(a, E1) subset_below_bounded : COROLLARY subset?(E, V) implies below_bounded(E) inf_of_subset : COROLLARY subset?(V1, V2) implies inf(V2) <= inf(V1) %----------------------------- % inf(V) is adherent to V %----------------------------- adherence_inf : THEOREM FORALL epsilon : EXISTS x : member(x, V) and x < inf(V) + epsilon %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Relations between inf, sup and set of opposites %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% below_negset : PROPOSITION below_bounded(E) IFF above_bounded(negset(E)) above_negset : PROPOSITION above_bounded(E) IFF below_bounded(negset(E)) JUDGEMENT negset HAS_TYPE [sup_set -> inf_set] JUDGEMENT negset HAS_TYPE [inf_set -> sup_set] inf_negset : PROPOSITION inf(V) = - sup(negset(V)) sup_negset : PROPOSITION sup(U) = - inf(negset(U)) END real_sets $$$real_sets.prf (|real_sets| (|sup_exists| "" (SKOLEM-TYPEPRED) (("" (EXPAND "above_bounded") (("" (ASSERT) (("" (USE "real_complete1") (("" (PROP) NIL))))))))) (|sup_is_unique| "" (SKOSIMP) (("" (EXPAND "least_upper_bound?") (("" (FLATTEN) (("" (INST -2 "b!1") (("" (INST -4 "a!1") (("" (ASSERT) (("" (ASSERT) NIL))))))))))))) (|sup_lemma| "" (SKOLEM!) (("" (USE "sup_exists") (("" (EXPAND "sup") (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (x: real): least_upper_bound?(x, U!1)")) (("" (ASSERT) NIL))))))))) (|sup_def| "" (SKOLEM!) (("" (PROP) (("1" (USE "sup_lemma") (("1" (ASSERT) NIL))) ("2" (USE "sup_lemma") (("2" (USE "sup_is_unique") (("2" (ASSERT) NIL))))))))) (|sup_is_bound| "" (SKOSIMP) (("" (LEMMA "sup_lemma" ("U" "U!1")) (("" (EXPAND "least_upper_bound?") (("" (FLATTEN) (("" (EXPAND "upper_bound?" -1) (("" (INST?) (("" (ASSERT) NIL))))))))))))) (|sup_is_sup| "" (SKOLEM!) (("" (LEMMA "sup_lemma" ("U" "U!1")) (("" (EXPAND "least_upper_bound?") (("" (PROP) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (DELETE -3) (("2" (EXPAND "upper_bound?") (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) (|upper_bound_subset| "" (SKOSIMP) (("" (EXPAND "subset?") (("" (EXPAND "upper_bound?") (("" (SKOSIMP) (("" (INST -1 "x!1") (("" (INST -2 "x!1") (("" (ASSERT) NIL))))))))))))) (|subset_above_bounded| "" (SKOSIMP) (("" (TYPEPRED "U!1") (("" (EXPAND "above_bounded") (("" (SKOLEM!) (("" (INST?) (("" (FORWARD-CHAIN "upper_bound_subset") NIL))))))))))) (|sup_of_subset| "" (SKOSIMP) (("" (REWRITE "sup_is_sup" :DIR RL) (("" (USE "upper_bound_subset") (("" (ASSERT) (("" (REWRITE "sup_is_sup" 1) NIL))))))))) (|adherence_sup| "" (SKOSIMP*) (("" (LEMMA "sup_is_sup" ("U" "U!1" "x" "sup(U!1) - epsilon!1")) (("" (ASSERT) (("" (PROP) (("" (EXPAND "upper_bound?") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL))))))))))))))) (|inf_exists| "" (SKOLEM-TYPEPRED) (("" (EXPAND "below_bounded") (("" (ASSERT) (("" (USE "real_complete2") (("" (PROP) NIL))))))))) (|inf_is_unique| "" (SKOSIMP) (("" (EXPAND "greatest_lower_bound?") (("" (FLATTEN) (("" (INST -2 "b!1") (("" (INST -4 "a!1") (("" (ASSERT) (("" (ASSERT) NIL))))))))))))) (|inf_lemma| "" (SKOLEM!) (("" (USE "inf_exists") (("" (EXPAND "inf") (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (x: real): greatest_lower_bound?(x, V!1)")) (("" (ASSERT) NIL))))))))) (|inf_def| "" (SKOLEM!) (("" (PROP) (("1" (USE "inf_lemma") (("1" (ASSERT) NIL))) ("2" (USE "inf_lemma") (("2" (USE "inf_is_unique") (("2" (ASSERT) NIL))))))))) (|inf_is_bound| "" (SKOSIMP) (("" (LEMMA "inf_lemma" ("V" "V!1")) (("" (EXPAND "greatest_lower_bound?") (("" (FLATTEN) (("" (EXPAND "lower_bound?" -1) (("" (INST?) (("" (ASSERT) NIL))))))))))))) (|inf_is_inf| "" (SKOLEM!) (("" (LEMMA "inf_lemma" ("V" "V!1")) (("" (EXPAND "greatest_lower_bound?") (("" (PROP) (("1" (INST?) (("1" (ASSERT) NIL))) ("2" (DELETE -3) (("2" (EXPAND "lower_bound?") (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))))) (|lower_bound_subset| "" (SKOSIMP) (("" (EXPAND "subset?") (("" (EXPAND "lower_bound?") (("" (SKOSIMP) (("" (INST -1 "x!1") (("" (INST -2 "x!1") (("" (ASSERT) NIL))))))))))))) (|subset_below_bounded| "" (SKOSIMP) (("" (TYPEPRED "V!1") (("" (EXPAND "below_bounded") (("" (SKOLEM!) (("" (INST?) (("" (FORWARD-CHAIN "lower_bound_subset") NIL))))))))))) (|inf_of_subset| "" (SKOSIMP) (("" (REWRITE "inf_is_inf" :DIR RL) (("" (USE "lower_bound_subset") (("" (ASSERT) (("" (REWRITE "inf_is_inf" 1) NIL))))))))) (|adherence_inf| "" (SKOLEM!) (("" (LEMMA "inf_is_inf" ("V" "V!1" "x" "inf(V!1) + epsilon!1")) (("" (ASSERT) (("" (PROP) (("" (EXPAND "lower_bound?") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) NIL))))))))))))))) (|below_negset| "" (GRIND :DEFS NIL :REWRITES ("below_bounded" "above_bounded") :IF-MATCH NIL) (("1" (INST 1 "- a!1") (("1" (REWRITE "lower_to_upper") NIL))) ("2" (INST 1 "- a!1") (("2" (REWRITE "lower_to_upper") NIL))))) (|above_negset| "" (SKOLEM!) (("" (AUTO-REWRITE "below_negset" "neg_neg") (("" (ASSERT) NIL))))) (|negset_TCC1| "" (SKOLEM-TYPEPRED) (("" (REWRITE "above_negset") NIL))) (|negset_TCC2| "" (SKOLEM-TYPEPRED) (("" (REWRITE "below_negset") NIL))) (|inf_negset| "" (SKOLEM!) (("" (NAME-REPLACE "zzz" "sup(negset(V!1))" :HIDE? NIL) (("" (REWRITE "inf_def") (("" (REWRITE "sup_def") (("" (REWRITE "glb_to_lub") (("" (ASSERT) NIL))))))))))) (|sup_negset| "" (SKOLEM!) (("" (NAME-REPLACE "zzz" "inf(negset(U!1))" :HIDE? NIL) (("" (REWRITE "inf_def") (("" (REWRITE "sup_def") (("" (REWRITE "glb_to_lub") (("" (REWRITE "neg_neg") 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_sets, 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 %--------------------- above_bounded(f) : bool = above_bounded(Im(f)) below_bounded(f) : bool = below_bounded(Im(f)) bounded(f) : bool = above_bounded(f) AND below_bounded(f) %---------------------- % Direct definitions %---------------------- above_bounded_def : LEMMA above_bounded(f) IFF EXISTS a : FORALL x : f(x) <= a below_bounded_def : LEMMA below_bounded(f) IFF EXISTS a : FORALL x : a <= f(x) %------------------------ % Relation to opposite %------------------------ above_bounded_opposite : LEMMA above_bounded(- f) IFF below_bounded(f) below_bounded_opposite : LEMMA below_bounded(- f) IFF above_bounded(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 above_bounded(f) min_bounded : LEMMA is_minimum(x, f) IMPLIES below_bounded(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))))) (|strict_decr_to_decr| "" (GRIND :IF-MATCH NIL) (("" (INST -3 "x!1" "y!1") (("" (ASSERT) NIL))))) (|incr_opposite| "" (GRIND) NIL) (|decr_opposite| "" (GRIND) NIL) (|strict_incr_opposite| "" (GRIND) NIL) (|strict_decr_opposite| "" (GRIND) NIL) (|constant_to_incr| "" (GRIND :IF-MATCH ALL) NIL) (|constant_to_decr| "" (GRIND :IF-MATCH ALL) NIL) (|constant_opposite| "" (GRIND :IF-MATCH ALL) NIL) (|above_bounded_def| "" (GRIND :IF-MATCH NIL) (("1" (INST? 1) (("1" (SKOLEM!) (("1" (INST? -2) (("1" (ASSERT) (("1" (INST?) NIL))))))))) ("2" (INST? 1) (("2" (SKOSIMP*) (("2" (INST? -3) (("2" (ASSERT) NIL))))))))) (|below_bounded_def| "" (GRIND :IF-MATCH NIL) (("1" (INST? 1) (("1" (SKOLEM!) (("1" (INST -2 "f!1(x!1)") (("1" (ASSERT) (("1" (INST?) NIL))))))))) ("2" (INST? 1) (("2" (SKOSIMP*) (("2" (INST? -3) (("2" (ASSERT) NIL))))))))) (|above_bounded_opposite| "" (GRIND :DEFS NIL :REWRITES ("above_bounded_def" "below_bounded_def" "-") :IF-MATCH NIL) (("1" (INST 1 "-a!1") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))))) ("2" (INST 1 "-a!1") (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL))))))))) (|below_bounded_opposite| "" (AUTO-REWRITE "negneg_function[T]") (("" (SKOLEM!) (("" (REWRITE "above_bounded_opposite" :DIR RL) (("" (ASSERT) NIL))))))) (|max_bounded| "" (GRIND :DEFS NIL :REWRITES ("is_maximum" "above_bounded_def") :IF-MATCH NIL) (("" (INST? 1) NIL))) (|min_bounded| "" (GRIND :DEFS NIL :REWRITES ("is_minimum" "below_bounded_def") :IF-MATCH NIL) (("" (INST? 1) NIL))) (|max_opposite| "" (GRIND :IF-MATCH NIL) (("1" (INST -3 "y!1") (("1" (ASSERT) NIL))) ("2" (INST?) (("2" (ASSERT) NIL))))) (|min_opposite| "" (AUTO-REWRITE "negneg_function[T]") (("" (SKOLEM!) (("" (REWRITE "max_opposite" :DIR RL) (("" (ASSERT) 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 f : VAR [T -> real] x : VAR T a : VAR real epsilon : VAR posreal %--------------- % Sup and Inf %--------------- g : VAR { f | above_bounded(f) } h : VAR { f | below_bounded(f) } sup(g) : real = sup(Im(g)) inf(h) : real = inf(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 above_bounded(f) AND sup(f) = f(x) min_lower_bound : LEMMA is_minimum(x, f) IFF below_bounded(f) AND inf(f) = f(x) END real_fun_supinf $$$real_fun_supinf.prf (|real_fun_supinf| (|sup_TCC1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "above_bounded" -) (("" (ASSERT) (("" (DELETE -) (("" (GRIND) (("" (INST -1 "g!1(epsilon! (x : T) : true)") (("" (INST?) NIL))))))))))))) (|inf_TCC1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "below_bounded" -) (("" (ASSERT) (("" (DELETE -) (("" (GRIND) (("" (INST -1 "h!1(epsilon! (x : T) : true)") (("" (INST?) NIL))))))))))))) (|supfun_is_bound| "" (SKOLEM!) (("" (EXPAND "sup") (("" (REWRITE "sup_is_bound") (("1" (DELETE 2) (("1" (GRIND) NIL))) ("2" (REWRITE "sup_TCC1") NIL))))))) (|supfun_is_sup| "" (SKOSIMP) (("" (EXPAND "sup") (("" (USE "adherence_sup") (("1" (SKOSIMP) (("1" (EXPAND "member") (("1" (EXPAND "Im" -1) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (REWRITE "sup_TCC1") NIL))))))) (|supfun_is_sup2| "" (SKOLEM!) (("" (EXPAND "sup") (("" (REWRITE "sup_is_sup" :DIR RL) (("1" (GRIND :IF-MATCH NIL) (("1" (INST?) (("1" (ASSERT) (("1" (INST?) NIL))))) ("2" (INST?) NIL))) ("2" (REWRITE "sup_TCC1") NIL))))))) (|inffun_is_bound| "" (SKOLEM!) (("" (EXPAND "inf") (("" (REWRITE "inf_is_bound") (("1" (DELETE 2) (("1" (GRIND) NIL))) ("2" (REWRITE "inf_TCC1") NIL))))))) (|inffun_is_inf| "" (SKOSIMP) (("" (EXPAND "inf") (("" (USE "adherence_inf") (("1" (SKOSIMP) (("1" (EXPAND "member") (("1" (EXPAND "Im" -1) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))))))))) ("2" (REWRITE "inf_TCC1") NIL))))))) (|inffun_is_inf2| "" (SKOLEM!) (("" (EXPAND "inf") (("" (REWRITE "inf_is_inf" :DIR RL) (("1" (GRIND :IF-MATCH NIL) (("1" (INST -2 "h!1(x!1)") (("1" (ASSERT) (("1" (INST?) NIL))))) ("2" (INST?) NIL))) ("2" (REWRITE "inf_TCC1") NIL))))))) (|supfun_opposite_TCC1| "" (SKOLEM!) (("" (REWRITE "above_bounded_opposite[T]") NIL))) (|supfun_opposite| "" (SKOLEM!) (("" (AUTO-REWRITE "supfun_opposite_TCC1") (("" (USE "supfun_is_sup2") (("" (GROUND) (("1" (USE "inffun_is_inf2" ("a" "- sup(- h!1)")) (("1" (GROUND) (("1" (DELETE -1 -2 2 3) (("1" (SKOLEM!) (("1" (USE "supfun_is_bound" ("g" "-h!1")) (("1" (EXPAND "-" -1 1) (("1" (ASSERT) NIL))))))))))))) ("2" (DELETE 2 3) (("2" (SKOLEM!) (("2" (EXPAND "-") (("2" (USE "inffun_is_bound") (("2" (ASSERT) NIL))))))))))))))))) (|inffun_opposite_TCC1| "" (SKOLEM!) (("" (REWRITE "below_bounded_opposite[T]") NIL))) (|inffun_opposite| "" (SKOLEM!) (("" (AUTO-REWRITE "inffun_opposite_TCC1") (("" (USE "inffun_is_inf2") (("" (GROUND) (("1" (USE "supfun_is_sup2" ("a" "- inf(- g!1)")) (("1" (GROUND) (("1" (DELETE -1 -2 2 3) (("1" (SKOLEM!) (("1" (USE "inffun_is_bound" ("h" "-g!1")) (("1" (EXPAND "-" -1 2) (("1" (ASSERT) NIL))))))))))))) ("2" (DELETE 2 3) (("2" (SKOLEM!) (("2" (EXPAND "-") (("2" (USE "supfun_is_bound") (("2" (ASSERT) 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) above_bounded_subseq : LEMMA above_bounded(v) AND subseq(u, v) IMPLIES above_bounded(u) below_bounded_subseq : LEMMA below_bounded(v) AND subseq(u, v) IMPLIES below_bounded(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))))) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL))))))))))))))) (|decr_condition| "" (SKOLEM!) (("" (EXPAND "decreasing") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL))))))))))))))) (|strict_incr_condition| "" (SKOLEM!) (("" (EXPAND "strict_increasing") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL))))))))))))))) (|strict_decr_condition| "" (SKOLEM!) (("" (EXPAND "strict_decreasing") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (INDUCT "y") (("1" (SKOSIMP) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (INST -1 "x!1") (("2" (INST -3 "j!1") (("2" (ASSERT) NIL))))))))))))))) (|extract_incr1| "" (GRIND :IF-MATCH NIL) (("1" (INST -1 "j!1" "i!1") (("1" (ASSERT) NIL))) ("2" (INST?) (("2" (ASSERT) NIL))))) (|extract_incr2| "" (SKOSIMP) (("" (USE "extract_incr1" ("i" "j!1" "j" "i!1")) (("" (ASSERT) NIL))))) (|extract_incr3| "" (SKOLEM 1 ("f!1" _)) (("" (INDUCT "i") (("1" (ASSERT) NIL) ("2" (SKOSIMP) (("2" (USE "extract_incr1" ("i" "j!1" "j" "j!1+1")) (("2" (ASSERT) NIL))))))))) (|unbounded_extract1| "" (SKOLEM!) (("" (INST?) (("" (REWRITE "extract_incr3") 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))))))))))) (|extract_composition| "" (AUTO-REWRITE "strict_increasing" "o") (("" (GRIND) NIL))) (|reflexive_subseq| "" (SKOLEM!) (("" (EXPAND "subseq") (("" (INST 1 "I") (("1" (EXPAND "I") (("1" (PROPAX) NIL))) ("2" (GRIND) NIL))))))) (|transitive_subseq| "" (EXPAND "subseq") (("" (SKOSIMP*) (("" (INST 1 "f!2 o f!1") (("1" (GRIND) NIL) ("2" (REWRITE "extract_composition") 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))))))))))))))) (|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) (("" (ASSERT) 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))))))))))) (|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))))))))))) (|above_bounded_subseq| "" (GRIND :EXCLUDE "above_bounded" :REWRITES ("above_bounded_def[nat]") :IF-MATCH NIL) (("" (INST? 1) (("" (SKOLEM!) (("" (INST? -4) (("" (INST? -3) (("" (ASSERT) NIL))))))))))) (|below_bounded_subseq| "" (GRIND :EXCLUDE "below_bounded" :REWRITES ("below_bounded_def[nat]") :IF-MATCH NIL) (("" (INST? 1) (("" (SKOLEM!) (("" (INST? -4) (("" (INST? -3) (("" (ASSERT) NIL))))))))))) (|bounded_subseq| "" (EXPAND "bounded") (("" (SKOSIMP) (("" (FORWARD-CHAIN "above_bounded_subseq") (("" (FORWARD-CHAIN "below_bounded_subseq") (("" (ASSERT) 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 | above_bounded(u) } v2 : VAR { u | below_bounded(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 | above_bounded(u) AND below_bounded(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 above_bounded(u) AND below_bounded(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))))))))))))))))))))))))))))) (|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))))))))))) (|limit_def| "" (SKOLEM!) (("" (USE "limit_lemma") (("" (GROUND) (("" (USE "unique_limit") (("" (ASSERT) 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))))))))))))))))))))))) (|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))))))))))) (|g_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|g_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL))) (|g_TCC3| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|g_prop_TCC1| "" (SKOSIMP*) (("" (ASSERT) 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) ("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))))))))))))))))))))))))) (|g_increasing| "" (SKOSIMP) (("" (REWRITE "strict_incr_condition") (("" (SKOLEM!) (("" (FORWARD-CHAIN "g_prop") (("" (INST?) (("" (GROUND) NIL))))))))))) (|g_convergence_TCC1| "" (SKOSIMP*) (("" (ASSERT) NIL))) (|g_convergence| "" (SKOSIMP*) (("" (FORWARD-CHAIN "g_prop") (("" (INST -1 "n!1") (("" (FLATTEN) (("" (PROPAX) 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))))))) ("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) ("2" (REWRITE "both_sides_div_pos_le2") 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))))))))))))))))))))))) (|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))))))))))))))))))))))))) (|cauchy_subsequence| "" (SKOSIMP) (("" (REWRITE "cauchy_accumulation" 1) (("" (REWRITE "accumulation_subsequence") (("" (INST?) (("" (ASSERT) 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))))))))))))))))))))))))))) (|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))))))))))))))))))))))))) (|bolzano_weierstrass1_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|bolzano_weierstrass1_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL))) (|bolzano_weierstrass1| "" (SKOLEM!) (("" (USE "monotone_subsequence") (("" (SKOSIMP) (("" (USE "above_bounded_subseq") (("" (USE "below_bounded_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) (("1" (GROUND) (("1" (INST -5 "0") (("1" (USE "supfun_is_bound[nat]") (("1" (USE "inffun_is_bound" ("h" "w!1")) (("1" (ASSERT) NIL))))))) ("2" (SKOLEM!) (("2" (INST?) (("2" (REPLACE*) (("2" (ASSERT) NIL))))))) ("3" (INST?) (("3" (ASSERT) NIL))))))))) ("2" (FORWARD-CHAIN "decreasing_bounded_convergence") (("2" (INST? 1) (("2" (GROUND) (("1" (SKOLEM!) (("1" (INST?) (("1" (REPLACE -5) (("1" (ASSERT) NIL))))))) ("2" (INST -5 "0") (("2" (USE "inffun_is_bound[nat]") (("2" (USE "supfun_is_bound" ("g" "w!1")) (("2" (ASSERT) NIL))))))) ("3" (INST?) (("3" (ASSERT) NIL))))))))))))))))))))))))))))) (|bolzano_weierstrass2| "" (SKOLEM!) (("" (USE "bolzano_weierstrass1") (("" (SKOSIMP) (("" (INST?) NIL))))))) (|bolzano_weierstrass3| "" (SKOSIMP) (("" (USE "bolzano_weierstrass1") (("" (SKOSIMP) (("" (REWRITE "accumulation_subsequence") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (EXPAND "convergent") (("" (INST?) NIL))))))))))))))))) (|bolzano_weierstrass4| "" (SKOSIMP) (("" (CASE "above_bounded(u!1)") (("1" (CASE "below_bounded(u!1)") (("1" (ASSERT) (("1" (CASE "a!1 <= inf(u!1)") (("1" (CASE "sup(u!1) <= b!1") (("1" (USE "bolzano_weierstrass1") (("1" (SKOSIMP) (("1" (INST 1 "a!2") (("1" (ASSERT) NIL))))))) ("2" (REWRITE "supfun_is_sup2[nat]") (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL))))))))) ("2" (REWRITE "inffun_is_inf2[nat]") (("2" (SKOLEM!) (("2" (INST?) (("2" (ASSERT) NIL))))))))))) ("2" (REWRITE "below_bounded_def[nat]") (("2" (INST 1 "a!1") (("2" (SKOLEM!) (("2" (INST?) (("2" (FLATTEN) (("2" (PROPAX) NIL))))))))))))) ("2" (REWRITE "above_bounded_def[nat]") (("2" (INST 1 "b!1") (("2" (SKOLEM!) (("2" (INST?) (("2" (FLATTEN) (("2" (PROPAX) NIL))))))))))))))) (|prefix_bounded1| "" (SKOLEM 1 (_ "u!1")) (("" (INDUCT "n") (("1" (INST 1 "u!1(0)") (("1" (SKOSIMP) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (INST 1 "max(a!1, u!1(j!1+1))") (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))) (|prefix_bounded2| "" (SKOLEM 1 (_ "u!1")) (("" (INDUCT "n") (("1" (INST 1 "u!1(0)") (("1" (SKOSIMP) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP*) (("2" (INST 1 "min(a!1, u!1(j!1+1))") (("2" (SKOSIMP) (("2" (INST -1 "i!1") (("2" (ASSERT) NIL))))))))))))) (|cauchy_bounded| "" (SKOSIMP) (("" (EXPAND "cauchy") (("" (INST -1 "1") (("" (SKOLEM!) (("" (INST -1 "n!1" _) (("" (ASSERT) (("" (SPLIT) (("1" (REWRITE "above_bounded_def[nat]") (("1" (USE "prefix_bounded1" ("n" "n!1")) (("1" (SKOLEM!) (("1" (INST 1 "a!1+1") (("1" (SKOLEM!) (("1" (INST-CP -1 "n!1") (("1" (INST -1 "x!1") (("1" (INST -3 "x!1") (("1" (ASSERT) (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (ASSERT) NIL))))))))))))))))))))))) ("2" (REWRITE "below_bounded_def[nat]") (("2" (USE "prefix_bounded2" ("n" "n!1")) (("2" (SKOLEM!) (("2" (INST 1 "a!1 - 1") (("2" (SKOLEM!) (("2" (INST-CP -1 "n!1") (("2" (INST -1 "x!1") (("2" (INST -3 "x!1") (("2" (ASSERT) (("2" (ASSERT) 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))))))))))))))))))))))))))))))) (|convergence_cauchy2| "" (SKOSIMP) (("" (USE "bolzano_weierstrass2") (("1" (SKOLEM!) (("1" (EXPAND "convergent") (("1" (INST?) (("1" (REWRITE "cauchy_accumulation") NIL))))))) ("2" (REWRITE "cauchy_bounded") NIL))))) (|convergence_cauchy| "" (SKOLEM!) (("" (PROP) (("1" (REWRITE "convergence_cauchy1") NIL) ("2" (REWRITE "convergence_cauchy2") 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(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(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) %-------------------------------------------------- % Constant sequence: redefined for type checking % (because judgements don't work) %-------------------------------------------------- seq : [real -> (convergent)] = const_fun[nat] JUDGEMENT seq HAS_TYPE [nzreal -> (convergent_nz)] limit_const_seq : LEMMA convergence(seq(a), a) %-------------- % Judgements %-------------- JUDGEMENT +, -, * HAS_TYPE [(convergent), (convergent) -> (convergent)] JUDGEMENT * HAS_TYPE [real, (convergent) -> (convergent)] JUDGEMENT -, abs HAS_TYPE [(convergent) -> (convergent)] JUDGEMENT / HAS_TYPE [(convergent), (convergent_nz) -> (convergent)] JUDGEMENT / HAS_TYPE [real, (convergent_nz) -> (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(seq(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))))))))))))))))))))))))))) (|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))))))))))))))))))))) (|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))))))))) (|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))))))))))))))))))))))))))))))))))) (|limit_const| "" (EXPAND "convergence") (("" (EXPAND "const_fun") (("" (SKOSIMP*) (("" (INST 1 "0") (("" (REWRITE "null_abs2") (("" (ASSERT) NIL))))))))))) (|limit_scal| "" (SKOSIMP) (("" (REWRITE "scal_function") (("" (REWRITE "limit_prod") (("" (REWRITE "limit_const") NIL))))))) (|limit_inv_TCC1| "" (SKOSIMP) 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))))))))))))))))))))))))))))))))) (|limit_div_TCC1| "" (SKOSIMP) NIL) (|limit_div| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "div_function") (("" (USE "limit_prod" ("l2" "1/l2!1")) (("" (ASSERT) (("" (REWRITE "limit_inv") 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))))))))))))))))))))))))))))) (|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))))))))))))))))))))))))) ("2" (ASSERT) 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))) ("2" (FLATTEN) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))) (|squeezing_const1| "" (SKOSIMP) (("" (AUTO-REWRITE "limit_const") (("" (LEMMA "squeezing_variant") (("" (INST -1 "N!1" "l!1" "s!1" "l!1" "s1!1") (("" (ASSERT) (("" (EXPAND "const_fun") (("" (PROPAX) NIL))))))))))))) (|squeezing_const2| "" (SKOSIMP) (("" (AUTO-REWRITE "limit_const") (("" (LEMMA "squeezing_variant") (("" (INST -1 "N!1" "l!1" "s!1" "s1!1" "l!1") (("" (ASSERT) (("" (EXPAND "const_fun") (("" (PROPAX) NIL))))))))))))) (|squeezing| "" (SKOSIMP) (("" (USE "squeezing_variant" ("s1" "s1!1" "s2" "s2!1" "s" "s!1" "N" "0")) (("" (ASSERT) NIL))))) (|abs_convergence| "" (SKOLEM!) (("" (PROP) (("1" (FORWARD-CHAIN "limit_abs") (("1" (EXPAND "abs" -1 2) (("1" (PROPAX) 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))))))))))))))))))))))))) (|convergent_sum| "" (GRIND :EXCLUDE "convergence" :REWRITES ("limit_sum") :IF-MATCH NIL) (("" (INST + "l!1 + l!2") (("" (ASSERT) NIL))))) (|convergent_opposite| "" (LEMMA "limit_opposite") (("" (GRIND :EXCLUDE "convergence") NIL))) (|convergent_diff| "" (LEMMA "limit_diff") (("" (GRIND :EXCLUDE "convergence") NIL))) (|convergent_prod| "" (LEMMA "limit_prod") (("" (GRIND :EXCLUDE "convergence") NIL))) (|convergent_const| "" (LEMMA "limit_const") (("" (GRIND :EXCLUDE "convergence") NIL))) (|convergent_scal| "" (LEMMA "limit_scal") (("" (GRIND :EXCLUDE "convergence") NIL))) (|convergent_inv| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "convergent") (("" (SKOLEM!) (("" (USE "limit_inv") (("" (ASSERT) (("" (REWRITE "limit_def" -2 :DIR RL) (("" (ASSERT) (("" (INST?) NIL))))))))))))))))) (|convergent_div| "" (SKOSIMP) (("" (ASSERT) (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (USE "limit_div") (("" (ASSERT) (("" (REWRITE "limit_def" -3 :DIR RL) (("" (ASSERT) (("" (INST?) NIL))))))))))))))))) (|convergent_abs| "" (LEMMA "limit_abs") (("" (GRIND :EXCLUDE ("convergence" "abs")) NIL))) (|convergent_nz_TCC1| "" (SKOLEM!) (("" (ASSERT) NIL))) (|seq_TCC1| "" (SKOLEM!) (("" (REWRITE "convergent_const") NIL))) (|seq_TCC2| "" (SKOLEM!) (("" (PROP) (("1" (GRIND) NIL) ("2" (EXPAND "convergent_nz") (("2" (FLATTEN) (("2" (REWRITE "limit_def") (("2" (EXPAND "seq") (("2" (USE "limit_const") (("2" (USE "unique_limit" ("l2" "0")) (("2" (GROUND) NIL))))))))))))))))) (|limit_const_seq| "" (EXPAND "seq") (("" (LEMMA "limit_const") (("" (PROPAX) NIL))))) (|plus_TCC1| "" (SKOLEM!) (("" (REWRITE "convergent_sum") NIL))) (|difference_TCC1| "" (SKOLEM!) (("" (REWRITE "convergent_diff") NIL))) (|times_TCC1| "" (SKOLEM!) (("" (REWRITE "convergent_prod") NIL))) (|times_TCC2| "" (SKOLEM!) (("" (REWRITE "convergent_scal") NIL))) (|difference_TCC2| "" (SKOLEM!) (("" (REWRITE "convergent_opposite") NIL))) (|abs_TCC1| "" (SKOLEM!) (("" (REWRITE "convergent_abs") NIL))) (|divide_TCC1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "convergent_nz") (("" (FLATTEN) (("" (REWRITE "convergent_div") NIL))))))) (|divide_TCC2| "" (SKOLEM-TYPEPRED) (("" (EXPAND "convergent_nz") (("" (REWRITE "scaldiv_function") (("" (REWRITE "convergent_div") (("" (REWRITE "convergent_const") NIL))))))))) (|lim_sum| "" (AUTO-REWRITE "limit_def" "limit_sum" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|lim_opposite| "" (AUTO-REWRITE "limit_def" "limit_opposite" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|lim_diff| "" (AUTO-REWRITE "limit_def" "limit_diff" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|lim_prod| "" (AUTO-REWRITE "limit_def" "limit_prod" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|lim_inv_TCC1| "" (SKOLEM-TYPEPRED) NIL) (|lim_inv_TCC2| "" (SKOLEM-TYPEPRED) (("" (EXPAND "convergent_nz") (("" (PROPAX) NIL))))) (|lim_inv| "" (AUTO-REWRITE "limit_def" "limit_lemma" "lim_inv_TCC1" "lim_inv_TCC2") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "limit_inv") NIL))))))) (|lim_div| "" (AUTO-REWRITE "limit_def" "limit_lemma" "lim_inv_TCC1" "lim_inv_TCC2") (("" (SKOLEM!) (("" (ASSERT) (("" (REWRITE "limit_div") NIL))))))) (|lim_const| "" (SKOLEM!) (("" (REWRITE "limit_def") (("" (EXPAND "seq") (("" (REWRITE "limit_const") NIL))))))) (|lim_scal| "" (AUTO-REWRITE "limit_def" "limit_scal" "limit_lemma") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|lim_abs| "" (AUTO-REWRITE "limit_def" "limit_lemma" "limit_abs") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|limit_equiv| "" (SKOLEM!) (("" (GROUND) (("1" (GRIND :EXCLUDE ("convergence")) NIL) ("2" (REWRITE "limit_def") (("2" (EXPAND "convergent") (("2" (INST?) NIL))))) ("3" (REWRITE "limit_def") 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 above_bounded(f) or EXISTS u : FORALL n : f(u(n)) > n bounded_from_above : PROPOSITION continuous(f) IMPLIES above_bounded(f) bounded_from_below : PROPOSITION continuous(f) IMPLIES below_bounded(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))) (|bolz_weier| "" (SKOLEM!) (("" (LEMMA "bolzano_weierstrass4") (("" (INST -1 "a" "b" "u!1") (("" (PROP) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (DELETE 2) (("2" (GRIND) NIL))))))))))) (|unbounded_sequence| "" (SKOSIMP) (("" (REWRITE "above_bounded_def[J]") (("" (INST 2 "lambda (n : nat) : epsilon! (x : J) : f!1(x) > n") (("" (SKOSIMP) (("" (BETA) (("" (LEMMA "epsilon_ax" ("p" "LAMBDA (x : J) : f!1(x) > n!1")) (("" (ASSERT) (("" (INST? 2) (("" (DELETE 3) (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) 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))))))))) ("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))) ("2" (GROUND) NIL))))))))))))))))))))))))))))))))))) (|bounded_from_below| "" (SKOSIMP) (("" (LEMMA "bounded_from_above" ("f" "-f!1")) (("" (REWRITE "above_bounded_opposite[J]") (("" (ASSERT) (("" (REWRITE "opp_fun_continuous[J]") NIL))))))))) (|max_extraction_TCC1| "" (LEMMA "bounded_from_above") (("" (PROPAX) NIL))) (|max_extraction_TCC2| "" (SKOSIMP*) (("" (ASSERT) 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))))))))))))))))))))))))) (|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))))) ("2" (REWRITE "both_sides_div_pos_lt2" 1) (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))))))))))) (|maximum_exists| "" (SKOSIMP) (("" (FORWARD-CHAIN "sup_is_reached") (("" (SKOLEM!) (("" (INST?) (("" (REWRITE "max_upper_bound[J]") (("" (ASSERT) (("" (REWRITE "bounded_from_above") NIL))))))))))))) (|inf_is_reached_TCC1| "" (LEMMA "bounded_from_below") (("" (PROPAX) 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))))) ("2" (REWRITE "bounded_from_below") NIL))))) ("2" (REWRITE "opp_fun_continuous[J]") NIL))))))) (|minimum_exists| "" (SKOSIMP) (("" (USE "maximum_exists" ("f" "-f!1")) (("" (SPLIT) (("1" (SKOLEM!) (("1" (REWRITE "max_opposite[J]") (("1" (INST?) NIL))))) ("2" (REWRITE "opp_fun_continuous[J]") NIL))))))) (|intermediate_value1_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|intermediate_value1_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL))) (|intermediate_value1| "" (SKOSIMP) (("" (NAME "E" "{y:real| a <= y AND y <= b AND f!1(y) < x!1}") (("1" (CASE "member(a, E) AND upper_bound?(b, E)") (("1" (FLATTEN) (("1" (CASE "nonempty?(E) AND above_bounded(E)") (("1" (FLATTEN) (("1" (ASSERT) (("1" (CASE "a <= sup(E) AND sup(E) <= b") (("1" (FLATTEN) (("1" (ASSERT) (("1" (HIDE -1 -2 -3 -4 -5 -6) (("1" (INST 1 "sup(E)") (("1" (CASE "x!1 < f!1(sup(E))") (("1" (ASSERT) (("1" (EXPAND "continuous") (("1" (INST -3 "sup(E)") (("1" (REWRITE "continuity_def[J]") (("1" (INST -3 "f!1(sup(E)) - x!1") (("1" (SKOLEM!) (("1" (USE "adherence_sup" ("epsilon" "delta!1")) (("1" (SKOSIMP) (("1" (FORWARD-CHAIN "sup_is_bound") (("1" (REPLACE -5 -2 RL) (("1" (EXPAND "member") (("1" (FLATTEN) (("1" (ASSERT) (("1" (INST -8 "x!2") (("1" (EXPAND "abs") (("1" (PROPAX) NIL))))))))))))))))))))))))))))))) ("2" (NAME "F" "{y:real | sup(E) < y AND y <= b}") (("2" (EXPAND "continuous") (("2" (INST -3 "sup(E)") (("2" (EXPAND "continuous") (("2" (EXPAND "convergence") (("2" (CASE "adh[J](F)(sup(E))") (("1" (ASSERT) (("1" (HIDE -1) (("1" (USE "subset_convergence2[J]" ("E1" "F")) (("1" (ASSERT) (("1" (SPLIT) (("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 "sup_is_bound" ("x" "x!2")) (("1" (ASSERT) (("1" (REPLACE -4 1 RL) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))))))))))))))))) ("2" (REPLACE -1 1 RL) (("2" (DELETE -1 -2 -3 -4 -5 2 3) (("2" (GRIND :DEFS NIL :THEORIES "sets[real]") NIL))))))))))))))) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 -3 -4) (("2" (EXPAND "adh") (("2" (SKOSIMP) (("2" (CASE "b < sup(E) + e!1") (("1" (INST 1 "b") (("1" (ASSERT) (("1" (EXPAND "abs") (("1" (ASSERT) NIL))))))) ("2" (ASSERT) (("2" (INST 2 "sup(E) + e!1/2") (("2" (ASSERT) (("2" (EXPAND "abs") (("2" (ASSERT) NIL))))))))))))))))))))))))))))))))))))))))) ("2" (SPLIT) (("1" (REWRITE "sup_is_bound") NIL) ("2" (REWRITE "sup_is_sup" :DIR RL) NIL))))))))) ("2" (DELETE -3 -4 -5 -6 2) (("2" (GRIND :DEFS NIL :THEORIES "sets[real]" :REWRITES ("above_bounded")) NIL))))))) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 -4 2) (("2" (GRIND) NIL))))))) ("2" (SKOSIMP) (("2" (ASSERT) NIL))))))) (|intermediate_value2_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|intermediate_value2| "" (SKOSIMP) (("" (USE "intermediate_value1") (("" (ASSERT) (("" (SPLIT) (("1" (PROPAX) NIL) ("2" (INST 2 "a") (("2" (ASSERT) NIL))) ("3" (INST 2 "b") (("3" (ASSERT) NIL))))))))))) (|intermediate_value3_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|intermediate_value3_TCC2| "" (SKOSIMP) (("" (ASSERT) NIL))) (|intermediate_value3| "" (SKOSIMP) (("" (LEMMA "intermediate_value1" ("f" "-f!1" "x" "-x!1")) (("" (FORWARD-CHAIN "opp_fun_continuous[J]") (("" (ASSERT) (("" (EXPAND "-" -2) (("" (SKOLEM!) (("" (INST?) (("" (ASSERT) NIL))))))))))))))) (|intermediate_value4_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|intermediate_value4| "" (SKOSIMP) (("" (USE "intermediate_value3") (("" (ASSERT) (("" (SPLIT) (("1" (PROPAX) NIL) ("2" (INST 2 "b") (("2" (ASSERT) NIL))) ("3" (INST 2 "a") (("3" (ASSERT) 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 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))) (|derivative_equivalence1_TCC2| "" (LEMMA "not_one_element") (("" (PROPAX) NIL))) (|derivative_equivalence1| "" (SKOLEM!) (("" (REWRITE "convergence_equiv[(A[T](x!1))]") (("1" (EXPAND "derivable") (("1" (EXPAND "deriv") (("1" (PROPAX) NIL))))) ("2" (SKOSIMP) NIL))))) (|derivative_equivalence2| "" (GRIND :EXCLUDE ("abs" "adh") :REWRITES ("deriv_TCC[T]" "adherence_fullset[T]") :IF-MATCH NIL) (("1" (INST 1 "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 -3 "epsilon!1") (("1" (SKOLEM!) (("1" (INST 1 "delta!1") (("1" (SKOSIMP) (("1" (LIFT-IF) (("1" (GROUND) (("1" (EXPAND "abs" +) (("1" (ASSERT) NIL))) ("2" (INST -4 "x!2 - x!1") (("2" (ASSERT) NIL))))))))))))))))))) ("2" (DELETE -) (("2" (GRIND) (("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 1 "delta!1") (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) (("2" (INST -7 "x!1 + x!2") (("2" (INST -8 "x!1+x!2") (("2" (ASSERT) NIL))))))))))))))))) (|deriv_maximum_TCC1| "" (SKOSIMP) NIL) (|deriv_maximum| "" (SKOSIMP*) (("" (AUTO-REWRITE "deriv_TCC[T]") (("" (EXPAND "deriv") (("" (EXPAND "derivable") (("" (ASSERT) (("" (REWRITE "lim_fun_def[(A[T](c!1))]") (("1" (EXPAND "convergent") (("1" (SKOLEM!) (("1" (CASE "l!1 <= 0 AND 0 <= l!1") (("1" (GROUND) 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))) ("2" (SKOSIMP) 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))))))))))))) ("2" (SKOSIMP) 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) ("2" (USE "connected_domain" ("x" "c!1" "y" "b!1")) (("2" (GRIND) 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))) ("2" (SKOSIMP) 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))))))))))))) ("2" (ASSERT) (("2" (SKOSIMP) 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) ("2" (USE "connected_domain" ("x" "a!1" "y" "c!1")) (("2" (GRIND) NIL))))))))))))))))))))))))))) ("2" (SKOSIMP) NIL))))))))))))) (|deriv_minimum_TCC1| "" (SKOSIMP) 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))))))))))))))) (|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))))) ("2" (DELETE -3 -4 -7) (("2" (EXPAND "min") (("2" (SMASH) NIL))))))))))))) ("2" (DELETE 2) (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) (("2" (INST -5 "c!1 + x!1") (("2" (GRIND) 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))))) ("2" (DELETE 2) (("2" (GRIND) NIL))))))))))) ("3" (SKOSIMP) NIL))))))))) (|deriv_constant2| "" (SKOSIMP) (("" (REWRITE "derivative_equivalence1") (("" (FORWARD-CHAIN "deriv_constant1") NIL))))) (|mean_value_aux_TCC1| "" (SKOSIMP*) (("" (EXPAND "derivable" -) (("" (INST?) 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))))))))))))))) ("2" (USE "connected_domain" ("x" "a!1" "y" "b!1")) (("2" (ASSERT) 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" (ASSERT) (("1" (ASSERT) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))))))))))))))))))))))) ("2" (LEMMA "connected_domain") (("2" (PROPAX) 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))))))))))))))))))))))) ("2" (LEMMA "connected_domain") (("2" (PROPAX) NIL))))))))))))))) (|mean_value_TCC1| "" (SKOSIMP*) (("" (EXPAND "derivable" -) (("" (INST?) 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_fun[T](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) ("2" (ASSERT) NIL))))))))))))))) ("2" (DELETE -3 2) (("2" (GRIND) (("2" (CASE "(B/C) * (b!1 - a!1) = B") (("1" (ASSERT) NIL) ("2" (REPLACE -2 1) (("2" (REWRITE "div_cancel2") NIL))))))))))))))))))))))) (|nonneg_derivative_TCC1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable" -) (("" (INST?) 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))) ("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))) ("2" (INST -2 "x!1" "x!1+x!2") (("2" (ASSERT) NIL))))))))))))) ("2" (SKOSIMP) NIL))))))) ("2" (SKOSIMP) (("2" (USE "mean_value" ("a" "x!1" "b" "y!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (LEMMA "pos_times_ge" ("x" "deriv(g!1, c!1)" "y" "y!1 - x!1")) (("1" (ASSERT) NIL) ("2" (INST?) 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))) ("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))) ("2" (INST -2 "x!1" "x!1+x!2") (("2" (ASSERT) NIL))))))))))))) ("2" (SKOSIMP) NIL))))))) ("2" (SKOSIMP) (("2" (USE "mean_value" ("a" "x!1" "b" "y!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (LEMMA "neg_times_le" ("x" "deriv(g!1, c!1)" "y" "y!1 - x!1")) (("1" (ASSERT) NIL) ("2" (INST?) 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) ("2" (EXPAND "derivable" -) (("2" (INST?) 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) ("2" (EXPAND "derivable" -) (("2" (INST?) NIL))))))))))))))))) (|null_derivative| "" (SKOLEM!) (("" (PROP) (("1" (SKOLEM!) (("1" (AUTO-REWRITE "constant_derivable[T]" "deriv_constant[T]") (("1" (CASE-REPLACE "g!1 = Const(g!1(x!1))") (("1" (ASSERT) NIL) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) 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))))))))))) ("2" (SKOSIMP) (("2" (USE "mean_value" ("b" "y!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) 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(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(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 ---% sum_fun_continuous : PROPOSITION continuous(f1) and continuous(f2) implies continuous(f1 + f2) diff_fun_continuous : PROPOSITION continuous(f1) and continuous(f2) implies continuous(f1 - f2) prod_fun_continuous : PROPOSITION continuous(f1) and continuous(f2) implies continuous(f1 * f2) const_fun_continuous : PROPOSITION continuous(u) scal_fun_continuous : PROPOSITION continuous(f) implies continuous(u * f) opp_fun_continuous : PROPOSITION continuous(f) implies continuous(- f) div_fun_continuous : PROPOSITION continuous(f) and continuous(g) implies continuous(f/g) inv_fun_continuous : PROPOSITION continuous(g) implies continuous(1/g) id_fun_continuous : PROPOSITION continuous(I[T]) %--------------------------------- % Type of continuous functions %--------------------------------- continuous_fun : TYPE = { f | continuous(f) } nz_continuous_fun : TYPE = { g | continuous(g) } JUDGEMENT nz_continuous_fun SUBTYPE_OF continuous_fun JUDGEMENT +, -, * HAS_TYPE [continuous_fun, continuous_fun -> continuous_fun] JUDGEMENT * HAS_TYPE [real, continuous_fun -> continuous_fun] JUDGEMENT - HAS_TYPE [continuous_fun -> continuous_fun] JUDGEMENT / HAS_TYPE [continuous_fun, nz_continuous_fun -> continuous_fun] JUDGEMENT / HAS_TYPE [real, nz_continuous_fun -> continuous_fun] END continuous_functions $$$continuous_functions.prf (|continuous_functions| (|continuity_def| "" (AUTO-REWRITE ("adherence_fullset[T]" "convergence_def[T]" "continuous")) (("" (ASSERT) NIL))) (|continuity_def2| "" (SKOLEM!) (("" (REWRITE "convergent_in_domain[T]") (("" (EXPAND "continuous") (("" (PROPAX) NIL))))))) (|sum_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "sum_fun_convergent[T]")) NIL) (|diff_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "diff_fun_convergent[T]")) NIL) (|prod_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "prod_fun_convergent[T]")) NIL) (|const_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "const_fun_convergent[T]" "adherence_fullset[T]")) NIL) (|scal_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "scal_fun_convergent[T]")) NIL) (|opp_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "opposite_fun_convergent[T]")) NIL) (|div_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("cv_div[T]")) NIL) (|inv_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("cv_inv[T]")) NIL) (|identity_continuous| "" (GRIND :DEFS NIL :REWRITES ("continuity_def2" "adherence_fullset[T]" "convergent_identity[T]")) NIL) (|continuous_TCC1| "" (GRIND) NIL) (|continuity_subset_TCC1| "" (GRIND :EXCLUDE "continuous") NIL) (|continuity_subset| "" (SKOSIMP) (("" (EXPAND "continuous") (("" (SKOLEM-TYPEPRED) (("" (INST?) (("1" (FORWARD-CHAIN "subset_convergence[T]") (("1" (INST?) (("1" (ASSERT) NIL) ("2" (TYPEPRED "E!1") (("2" (DELETE -4 2) (("2" (GRIND) NIL))))) ("3" (REWRITE "member_adherent[T]") (("3" (DELETE -3 2 3) (("3" (TYPEPRED "E!1") (("3" (GRIND) NIL))))))))))) ("2" (DELETE 2) (("2" (GRIND) NIL))))))))))) (|sum_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_sum[T]")) NIL) (|diff_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_diff[T]")) NIL) (|prod_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_prod[T]")) NIL) (|const_set_continuous| "" (GRIND :EXCLUDE ("convergence" "adh") :REWRITES ("convergence_const[T]" "member_adherent[T]")) NIL) (|scal_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_scal[T]")) NIL) (|opp_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_opposite[T]")) NIL) (|div_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_div[T]")) NIL) (|inv_set_continuous| "" (GRIND :EXCLUDE "convergence" :REWRITES ("convergence_inv[T]")) NIL) (|identity_set_continuous| "" (GRIND :EXCLUDE ("convergence" "adh") :REWRITES ("convergence_identity[T]" "member_adherent[T]")) NIL) (|continuous_def2_TCC1| "" (GRIND) NIL) (|continuous_def2| "" (GRIND :EXCLUDE "abs" :IF-MATCH NIL) NIL) (|continuity_subset2| "" (SKOLEM-TYPEPRED) (("" (FLATTEN) (("" (REWRITE "continuous_def2") (("" (FORWARD-CHAIN "continuity_subset") (("" (REWRITE "subset_reflexive") NIL))))))))) (|sum_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("sum_continuous")) NIL))) (|diff_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("diff_continuous")) NIL))) (|prod_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("prod_continuous")) NIL))) (|const_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("const_continuous")) NIL))) (|scal_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("scal_continuous")) NIL))) (|opp_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("opp_continuous")) NIL))) (|div_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("div_continuous")) NIL))) (|inv_fun_continuous| "" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES ("inv_continuous")) NIL))) (|id_fun_continuous| "" (EXPAND "continuous") (("" (SKOLEM!) (("" (REWRITE "identity_continuous") NIL))))) (SUBTYPE_TCC1 "" (SKOSIMP) (("" (ASSERT) NIL))) (|plus_TCC1| "" (SKOSIMP) (("" (REWRITE "sum_fun_continuous") NIL))) (|difference_TCC1| "" (SKOSIMP) (("" (REWRITE "diff_fun_continuous") NIL))) (|times_TCC1| "" (SKOLEM!) (("" (REWRITE "prod_fun_continuous") NIL))) (|times_TCC2| "" (SKOLEM!) (("" (REWRITE "scal_fun_continuous") NIL))) (|difference_TCC2| "" (SKOLEM!) (("" (REWRITE "opp_fun_continuous") NIL))) (|divide_TCC1| "" (SKOLEM!) (("" (REWRITE "div_fun_continuous") NIL))) (|divide_TCC2| "" (SKOLEM!) (("" (REWRITE "scaldiv_function") (("" (REWRITE "div_fun_continuous") (("" (REWRITE "const_fun_continuous") 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 div_simp : LEMMA FORALL (x : nzreal) : x / x = 1 %---------------------------------------- % 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 %--------------------------- % Lower and upper bounds %--------------------------- E : VAR setof[real] ub, lub : VAR real lb, glb : VAR real %--- upper_bound? and least_upper_bound? re-defined as in old PVS ---% upper_bound?(ub, E) : bool = FORALL (x : real) : member(x, E) implies x <= ub least_upper_bound?(lub, E) : bool = upper_bound?(lub, E) and FORALL (x : real) : upper_bound?(x, E) implies lub <= x %--- lower_bound? and greatest_lower_bound? ---% lower_bound?(lb, E) : bool = FORALL (x : real) : member(x, E) implies lb <= x greatest_lower_bound?(glb, E) : bool = lower_bound?(glb, E) and FORALL (x : real) : lower_bound?(x, E) implies x <= glb %--- Relation between lower and upper bounds ---% negset(E) : setof[real] = { x : real | member(-x, E) } neg_neg : LEMMA negset(negset(E)) = E JUDGEMENT negset HAS_TYPE [ (nonempty?[real]) -> (nonempty?[real]) ] lower_to_upper : LEMMA lower_bound?(lb, E) IFF upper_bound?(-lb, negset(E)) glb_to_lub : LEMMA greatest_lower_bound?(glb, E) IFF least_upper_bound?(-glb, negset(E)) %--------------------------- % Completeness properties %--------------------------- S : VAR (nonempty?[real]) %--- Equivalence with definitions in prelude ---% upper_def : LEMMA upper_bound?(ub, S) IFF upper_bound?(<=)(ub, S) least_upper_def : LEMMA least_upper_bound?(lub, S) IFF least_upper_bound?(<=)(lub, S) %--- Reformulation of real_complete for upper bounds ---% real_complete1 : THEOREM (EXISTS (y : real) : upper_bound?(y, S)) implies (EXISTS (x : real) : least_upper_bound?(x, S)) %--- Reformulation of real_complete for lower bounds ---% real_complete2 : THEOREM (EXISTS (y : real) : lower_bound?(y, S)) implies (EXISTS (x : real) : greatest_lower_bound?(x, S)) END real_facts $$$real_facts.prf (|real_facts| (|div_simp| "" (SKOLEM!) (("" (ASSERT) NIL))) (|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))))))) (|upper_def_TCC1| "" (SKOLEM!) (("" (TYPEPRED "S!1") (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[real]") (("" (ASSERT) (("" (SKOLEM!) (("" (INST?) NIL))))))))))))) (|upper_def| "" (SKOLEM!) (("" (EXPAND "upper_bound?") (("" (PROP) (("1" (SKOLEM!) (("1" (INST?) (("1" (EXPAND "member") (("1" (PROPAX) NIL))))))) ("2" (SKOSIMP) (("2" (EXPAND "member") (("2" (INST?) NIL))))))))))) (|least_upper_def| "" (SKOLEM!) (("" (EXPAND "least_upper_bound?") (("" (AUTO-REWRITE "upper_def") (("" (ASSERT) (("" (PROP) (("1" (SKOSIMP) (("1" (INST?) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))) (|neg_neg| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (DELETE 2) (("" (EXPAND "negset") (("" (EXPAND "member") (("" (ASSERT) NIL))))))))))) (|negset_TCC1| "" (GRIND :IF-MATCH NIL) (("" (INST -3 "-x!1") (("" (ASSERT) NIL))))) (|lower_to_upper| "" (SKOLEM!) (("" (EXPAND "lower_bound?") (("" (EXPAND "upper_bound?") (("" (PROP) (("1" (SKOSIMP) (("1" (INST -1 "-x!1") (("1" (EXPAND "negset") (("1" (EXPAND "member" -2 1) (("1" (ASSERT) NIL))))))))) ("2" (SKOSIMP) (("2" (INST -1 "-x!1") (("2" (EXPAND "negset") (("2" (EXPAND "member" -1 1) (("2" (ASSERT) NIL))))))))))))))))) (|glb_to_lub| "" (SKOLEM!) (("" (EXPAND "greatest_lower_bound?") (("" (EXPAND "least_upper_bound?") (("" (AUTO-REWRITE "lower_to_upper") (("" (ASSERT) (("" (PROP) (("1" (SKOSIMP) (("1" (INST -3 "-x!1") (("1" (ASSERT) NIL))))) ("2" (SKOSIMP) (("2" (INST -3 "-x!1") (("2" (ASSERT) NIL))))))))))))))))) (|real_complete1| "" (LEMMA "real_complete") (("" (AUTO-REWRITE "upper_def" "least_upper_def") (("" (SKOSIMP) (("" (INST?) (("" (SPLIT) (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))) (|real_complete2| "" (SKOSIMP) (("" (LEMMA "real_complete1" ("S" "negset(S!1)")) (("" (SPLIT) (("1" (DELETE -2) (("1" (SKOLEM!) (("1" (INST 1 "-x!1") (("1" (REWRITE "glb_to_lub") (("1" (ASSERT) NIL))))))))) ("2" (DELETE 2) (("2" (SKOLEM!) (("2" (INST 1 "-y!1") (("2" (REWRITE "lower_to_upper") 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) ("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))))))))))) ("2" (DELETE -1 2) (("2" (REWRITE "le_times_le_pos" 1) 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))) ("2" (DELETE -1 -2 -3 2) (("2" (SPLIT) (("1" (REWRITE "both_sides_times_pos_le1") (("1" (ASSERT) NIL))) ("2" (REWRITE "le_times_le_pos") 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))) ("2" (PROPAX) NIL) ("3" (PROPAX) NIL))) ("2" (ASSERT) NIL) ("3" (ASSERT) NIL))))))) ("2" (DELETE -1 2) (("2" (SKOLEM!) (("2" (REWRITE "times_div1") (("2" (REWRITE "div_mult_pos_lt1") NIL))))))))))))))))))) (|inv_bound_TCC1| "" (SKOSIMP) NIL) (|inv_bound_TCC2| "" (SKOSIMP) NIL) (|inv_bound_TCC3| "" (SKOSIMP) (("" (REWRITE "zero_times3") (("" (ASSERT) NIL))))) (|inv_bound| "" (SKOSIMP) (("" (LEMMA "null_abs" ("x" "x1!1")) (("" (REPLACE 1) (("" (GROUND) (("" (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 -1 "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) ("2" (PROPAX) NIL) ("3" (DELETE -1 5) (("3" (REWRITE "both_sides_times_pos_le2") (("3" (LEMMA "diff_abs") (("3" (INST -1 "y1!1" "x1!1") (("3" (REWRITE "diff_abs_commute" -2) (("3" (ASSERT) NIL))))))))))))) ("2" (DELETE -1 5) (("2" (CASE "abs(y1!1) * (abs(y1!1) - e1!1) > 0") (("1" (ASSERT) NIL) ("2" (DELETE 2) (("2" (REWRITE "pos_times_gt") 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))))))))) ("3" (DELETE 5) (("3" (REWRITE "pos_times_gt") 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))) ("2" (REWRITE "both_sides_div_pos_lt1") 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))))))))))) ("2" (REWRITE "pos_times_gt") NIL))))) ("2" (DELETE 2 3 4) (("2" (INST 1 "e!1 / (2 + e!1)") (("2" (REWRITE "both_sides_div_pos_lt2") NIL))))))))))))) (|inv_epsilon_TCC1| "" (SKOSIMP*) (("" (REWRITE "zero_times3") (("" (ASSERT) 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) (("1" (ASSERT) NIL))))))))))))))))) ("2" (REWRITE "posreal_mult_closed") 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 %------------------------------------------ const_fun(a) : [T -> real] = LAMBDA x : a CONVERSION const_fun %-------------- % 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_fun(a) * f1 scaldiv_function : PROPOSITION a / f3 = const_fun(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!) (("" (AUTO-REWRITE-THEORY "real_fun_ops") (("" (APPLY-EXTENSIONALITY) NIL))))) (|scaldiv_function| "" (SKOLEM!) (("" (AUTO-REWRITE-THEORY "real_fun_ops") (("" (APPLY-EXTENSIONALITY) 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(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) (|adherence_subset1| "" (GRIND :IF-MATCH NIL :DEFS NIL :REWRITES ("subset?" "member" "adh")) (("" (INST? -5) (("" (SKOSIMP) (("" (INST? -4) (("" (INST? 1) (("" (ASSERT) NIL))))))))))) (|adherence_subset2| "" (EXPAND "subset?" 1 2) (("" (EXPAND "member") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "adherence_subset1") NIL))))))) (|adherence_prop1| "" (SKOLEM-TYPEPRED) (("" (EXPAND "adh") (("" (INST?) NIL))))) (|adherence_prop2| "" (SKOLEM!) (("" (USE "adherence_prop1" ("e" "min(e1!1, e2!1)" "E" "E!1")) (("" (SKOSIMP) (("" (INST?) (("" (GROUND) 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))))))))))))))))))))))))))))))) (|subset_convergence| "" (GRIND :EXCLUDE ("abs" "adh") :IF-MATCH NIL) (("" (INST? -7) (("" (SKOLEM!) (("" (INST 1 "delta!1") (("" (SKOSIMP) (("" (INST? -5) (("" (INST?) (("" (ASSERT) NIL))))))))))))))) (|subset_convergence2| "" (SKOSIMP) (("" (FORWARD-CHAIN "subset_convergence") (("" (INST?) (("" (ASSERT) 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))))))))))))))))))))) (|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))))))))))))))))))))))) (|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))))))))))))))))))) (|convergence_diff| "" (SKOSIMP) (("" (REWRITE "diff_function") (("" (USE "convergence_sum" ("f2" "-f2!1" "l2" "-l2!1")) (("" (ASSERT) (("" (REWRITE "convergence_opposite") 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))))))))))))))))))))))))))))) (|convergence_const| "" (EXPAND "convergence") (("" (SKOSIMP*) (("" (AUTO-REWRITE "null_abs2") (("" (EXPAND "const_fun") (("" (ASSERT) (("" (INST 1 "1") NIL))))))))))) (|convergence_scal| "" (SKOSIMP) (("" (REWRITE "scal_function") (("" (REWRITE "convergence_prod") (("" (REWRITE "convergence_const") (("" (EXPAND "convergence" -) (("" (PROPAX) NIL))))))))))) (|convergence_inv_TCC1| "" (SKOSIMP) 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))))))))))))))))))))))))) (|convergence_div_TCC1| "" (SKOSIMP) NIL) (|convergence_div| "" (SKOSIMP) (("" (REWRITE "div_function") (("" (ASSERT) (("" (USE "convergence_prod" ("l2" "1/l2!1")) (("" (ASSERT) (("" (REWRITE "convergence_inv") NIL))))))))))) (|convergence_identity| "" (GRIND :EXCLUDE ("adh" "abs")) 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))))))))))))))))))))))))) ("2" (ASSERT) NIL))))))) (|convergence_lower_bound| "" (SKOSIMP) (("" (USE "convergence_order" ("f1" "const_fun[T](b!1)")) (("" (GROUND) (("1" (REWRITE "convergence_const") (("1" (EXPAND "convergence" -) (("1" (PROPAX) NIL))))) ("2" (EXPAND "const_fun") (("2" (PROPAX) NIL))))))))) (|convergence_upper_bound| "" (SKOSIMP) (("" (USE "convergence_order" ("f2" "const_fun[T](b!1)")) (("" (GROUND) (("1" (REWRITE "convergence_const") (("1" (EXPAND "convergence" -) (("1" (PROPAX) NIL))))) ("2" (EXPAND "const_fun") (("2" (PROPAX) NIL))))))))) (|convergence_locally_constant| "" (GRIND :IF-MATCH NIL :EXCLUDE ("abs" "adh")) (("" (INST 1 "epsilon!1") (("" (SKOSIMP) (("" (INST?) (("" (ASSERT) (("" (ASSERT) (("" (EXPAND "abs") (("" (ASSERT) 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)))))))))))))))))))))))))) $$$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(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_fun[T](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_fun[T](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))))))) (|adherence_fullset| "" (AUTO-REWRITE "fullset" "member_adherent[T]") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|cv_unique| "" (SKOSIMP) (("" (EXPAND "convergence") (("" (USE "convergence_unicity[T]") (("" (ASSERT) NIL))))))) (|cv_in_domain| "" (SKOSIMP) (("" (EXPAND "convergence") (("" (USE "convergence_in_domain[T]") (("" (EXPAND "fullset") (("" (ASSERT) NIL))))))))) (|cv_sum| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_sum[T]") NIL))) (|cv_diff| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_diff[T]") NIL))) (|cv_prod| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_prod[T]") NIL))) (|cv_const| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_const[T]") NIL))) (|cv_scal| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_scal[T]") NIL))) (|cv_opp| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_opposite[T]") NIL))) (|cv_div_TCC1| "" (SKOSIMP) NIL) (|cv_div| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_div[T]") NIL))) (|cv_inv_TCC1| "" (SKOSIMP) NIL) (|cv_inv| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_inv[T]") NIL))) (|cv_identity| "" (EXPAND "convergence") (("" (GRIND :DEFS NIL :REWRITES "convergence_identity[T]") 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))))))))))))))) (|lim_fun_def| "" (SKOLEM!) (("" (USE "lim_fun_lemma") (("" (GROUND) (("" (USE "cv_unique" ("l2" "lim(f!1, x0!1)")) (("" (ASSERT) NIL))))))))) (|convergence_equiv| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "convergent") (("1" (INST?) NIL))) ("2" (REWRITE "lim_fun_def") (("2" (EXPAND "convergent") (("2" (INST?) NIL))))) ("3" (REWRITE "lim_fun_def") NIL))))) (|convergent_in_domain| "" (GRIND :EXCLUDE "convergence") (("" (FORWARD-CHAIN "cv_in_domain") (("" (ASSERT) NIL))))) (|limit_in_domain| "" (SKOSIMP) (("" (REWRITE "lim_fun_def") (("" (REWRITE "convergent_in_domain") NIL))))) (|sum_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "l!1 + l!2") (("" (REWRITE "cv_sum") NIL))))))) (|opposite_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "cv_opp") (("" (INST?) NIL))))))) (|diff_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "l!1 - l!2") (("" (REWRITE "cv_diff") NIL))))))) (|prod_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "l!1 * l!2") (("" (REWRITE "cv_prod") NIL))))))) (|const_fun_convergent| "" (EXPAND "convergent") (("" (SKOLEM!) (("" (INST?) (("" (REWRITE "cv_const") NIL))))))) (|scal_fun_convergent| "" (EXPAND "convergent") (("" (SKOSIMP*) (("" (INST 1 "b!1 * l!1") (("" (REWRITE "cv_scal") NIL))))))) (|inv_fun_convergent| "" (SKOSIMP) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergent") (("" (SKOSIMP) (("" (ASSERT) (("" (INST 2 "1/l!1") (("" (REWRITE "cv_inv") NIL))))))))))))) (|div_fun_convergent| "" (SKOSIMP) (("" (REWRITE "lim_fun_def") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (ASSERT) (("" (INST 2 "l!1 / l!2") (("" (REWRITE "cv_div") NIL))))))))))))) (|convergent_identity| "" (SKOLEM!) (("" (EXPAND "convergent") (("" (USE "cv_identity") (("" (INST?) NIL))))))) (|limit_sum_fun_TCC1| "" (LEMMA "sum_fun_convergent") (("" (PROPAX) NIL))) (|limit_sum_fun_TCC2| "" (SKOSIMP) NIL) (|limit_sum_fun_TCC3| "" (SKOSIMP) NIL) (|limit_sum_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "sum_fun_convergent" ("cv_sum")) (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|limit_opposite_fun_TCC1| "" (LEMMA "opposite_fun_convergent") (("" (PROPAX) NIL))) (|limit_opposite_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "opposite_fun_convergent" ("cv_opp")) (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|limit_diff_fun_TCC1| "" (LEMMA "diff_fun_convergent") (("" (PROPAX) NIL))) (|limit_diff_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "diff_fun_convergent" ("cv_diff")) (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|limit_prod_fun_TCC1| "" (LEMMA "prod_fun_convergent") (("" (PROPAX) NIL))) (|limit_prod_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "prod_fun_convergent" ("cv_prod")) (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|limit_const_fun_TCC1| "" (LEMMA "const_fun_convergent") (("" (PROPAX) NIL))) (|limit_const_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "const_fun_convergent" ("cv_const")) (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|limit_scal_fun_TCC1| "" (LEMMA "scal_fun_convergent") (("" (PROPAX) NIL))) (|limit_scal_fun| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "scal_fun_convergent" "cv_scal") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|limit_inv_fun_TCC1| "" (LEMMA "inv_fun_convergent") (("" (PROPAX) NIL))) (|limit_inv_fun_TCC2| "" (SKOSIMP) NIL) (|limit_inv_fun_TCC3| "" (SUBTYPE-TCC) NIL) (|limit_inv_fun| "" (SKOSIMP) (("" (ASSERT) (("" (DELETE 1) (("" (AUTO-REWRITE "lim_fun_def" "lim_fun_lemma" "inv_fun_convergent" ("cv_inv")) (("" (ASSERT) NIL))))))))) (|limit_div_fun_TCC1| "" (LEMMA "div_fun_convergent") (("" (PROPAX) NIL))) (|limit_div_fun_TCC2| "" (SKOSIMP) NIL) (|limit_div_fun_TCC3| "" (SKOSIMP) NIL) (|limit_div_fun_TCC4| "" (SUBTYPE-TCC) NIL) (|limit_div_fun| "" (SKOSIMP) (("" (ASSERT) (("" (DELETE 1) (("" (AUTO-REWRITE "lim_fun_def" "lim_fun_lemma" "div_fun_convergent" "cv_div") (("" (ASSERT) NIL))))))))) (|limit_identity_TCC1| "" (LEMMA "convergent_identity") (("" (PROPAX) NIL))) (|limit_identity| "" (AUTO-REWRITE "lim_fun_lemma" "lim_fun_def" "convergent_identity" "cv_identity") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|limit_le1_TCC1| "" (SKOSIMP) 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))))))))))))))))) (|limit_ge1_TCC1| "" (SKOSIMP) 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))))))))))))))))))))) (|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))))))))))))))))))))) (|limit_le2_TCC1| "" (SKOSIMP) 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))))) ("2" (REWRITE "subset_fullset") NIL))))))))))))))) (|limit_ge2_TCC1| "" (SKOSIMP) 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))))))))))))) ("2" (REWRITE "subset_fullset") NIL))))))))))))))) (|limit_order2_TCC1| "" (SKOSIMP) NIL) (|limit_order2_TCC2| "" (SKOSIMP) 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)))))))))))))))))))))))))) $$$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 %--------------------------------------------------------------- % Lemma for type checking. % % BUG in PVS? % derivable_TCC2: OBLIGATION % (FORALL (x): adh[(A(PROJ_2(f, x)))](fullset[real])(0)); %--------------------------------------------------------------- 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_fun[T](b), x) = const_fun(0) identity_NQ : LEMMA NQ(I[T], x) = const_fun(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_fun[T](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_fun[T](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_fun[T](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) } JUDGEMENT nz_deriv_fun SUBTYPE_OF deriv_fun JUDGEMENT deriv_fun SUBTYPE_OF continuous_fun[T] JUDGEMENT nz_deriv_fun SUBTYPE_OF nz_continuous_fun[T] JUDGEMENT +, -, * HAS_TYPE [deriv_fun, deriv_fun -> deriv_fun] JUDGEMENT * HAS_TYPE [real, deriv_fun -> deriv_fun] JUDGEMENT - HAS_TYPE [deriv_fun -> deriv_fun] JUDGEMENT / HAS_TYPE [deriv_fun, nz_deriv_fun -> deriv_fun] JUDGEMENT / HAS_TYPE [real, nz_deriv_fun -> deriv_fun] %-------------------------------------------------- % Redefinition of constant and identity function %-------------------------------------------------- Const : [real -> deriv_fun] = const_fun[T] constant_derivable : LEMMA derivable(Const(b), x) deriv_constant : LEMMA deriv(Const(b), x) = 0 Id : deriv_fun = I[T] id_derivable : LEMMA derivable(Id, x) deriv_id : LEMMA deriv(Id, x) = 1 %------------------------ % Derivative function %------------------------ ff, ff1, ff2 : VAR deriv_fun gg : VAR nz_deriv_fun 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(Id) = Const(1) END derivatives $$$derivatives.prf (|derivatives| (NQ_TCC1 "" (GRIND) 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))) ("2" (INST 3 "if x!1 < y!1 then e!1/2 else -e!1/2 endif") (("1" (GRIND) NIL) ("2" (USE "connected_domain" ("x" "y!1" "y" "x!1")) (("2" (GRIND) NIL))) ("3" (USE "connected_domain" ("x" "x!1" "y" "y!1")) (("3" (GRIND) 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) ("2" (DELETE -5) (("2" (GRIND) NIL))))))))))))) ("2" (INST? -4) (("2" (SKOLEM!) (("2" (INST + "delta!1") (("2" (SKOSIMP :PREDS? T) (("2" (ASSERT) (("2" (INST?) (("2" (ASSERT) NIL))))))))))))))) (|deriv_continuous| "" (SKOSIMP) (("" (REWRITE "continuous_lim" :DIR RL) (("" (CASE-REPLACE "(LAMBDA (h : (A(x!1))) : f!1(h + x!1)) = const_fun[(A(x!1))](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))) ("2" (SKOSIMP) NIL))))) ("2" (DELETE -1 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL) ("2" (GRIND) NIL))))) ("3" (DELETE -1 2) (("3" (GRIND) NIL))))))))) (|derivable_continuous| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (FORWARD-CHAIN "deriv_continuous") NIL))))))) (|derivable_continuous2| "" (EXPAND "derivable") (("" (EXPAND "continuous") (("" (GRIND :DEFS NIL :REWRITES "derivable_continuous") NIL))))) (|sum_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL))))) (|opposite_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL))))) (|diff_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL))))) (|scal_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL))))) (|const_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL))))) (|identity_NQ| "" (SKOLEM!) (("" (APPLY-EXTENSIONALITY) (("" (GRIND) NIL))))) (|prod_NQ| "" (GRIND) 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))))))) ("2" (SKOSIMP) NIL))) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 -3 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL) ("2" (DELETE 2) (("2" (GRIND) NIL))))))))))) ("2" (DELETE -1 -2 2) (("2" (GRIND) NIL))))))))) (|inv_NQ| "" (GRIND) 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))]") (("1" (SKOSIMP) NIL))) ("2" (REWRITE "cv_scal[(A(x!1))]") (("1" (USE "continuous_lim" ("f" "g!1")) (("1" (GROUND) (("1" (FORWARD-CHAIN "deriv_continuous") NIL))))) ("2" (SKOSIMP) NIL))) ("3" (REPLACE -2 1 RL) (("3" (DELETE -1 -2 -3 2) (("3" (GRIND :REWRITES "zero_times3") NIL))))) ("4" (SKOSIMP) NIL))) ("2" (REPLACE -1 + RL) (("2" (DELETE -1 -2 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("1" (GRIND) NIL) ("2" (DELETE 2) (("2" (GRIND :REWRITES "zero_times3") NIL))) ("3" (DELETE 2) (("3" (GRIND) NIL))))))))) ("3" (REPLACE -1 + RL) (("3" (DELETE -1 -2 2) (("3" (GRIND :REWRITES "zero_times3") NIL))))))) ("2" (DELETE -1 2) (("2" (GRIND) NIL))))))))) (|sum_derivable| "" (AUTO-REWRITE "derivable" "sum_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "sum_fun_convergent[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))))))) (|opposite_derivable| "" (AUTO-REWRITE "derivable" "opposite_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "opposite_fun_convergent[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))))))) (|diff_derivable| "" (AUTO-REWRITE "derivable" "diff_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "diff_fun_convergent[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))))))) (|prod_derivable| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (USE "limit_prod_NQ") (("" (ASSERT) (("" (INST?) NIL))))))))))) (|scal_derivable| "" (AUTO-REWRITE "derivable" "scal_NQ" "deriv_TCC") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "scal_fun_convergent[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))))))) (|const_derivable| "" (SKOLEM!) (("" (AUTO-REWRITE "derivable" "const_NQ" "deriv_TCC" ("const_fun_convergent[(A(x!1))]")) (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (|inv_derivable| "" (EXPAND "derivable") (("" (EXPAND "convergent") (("" (SKOSIMP*) (("" (USE "limit_inv_NQ") (("" (ASSERT) (("" (INST?) NIL))))))))))) (|div_derivable| "" (SKOSIMP) (("" (REWRITE "div_function[T]") (("" (REWRITE "prod_derivable") (("" (REWRITE "inv_derivable") NIL))))))) (|identity_derivable| "" (SKOLEM!) (("" (AUTO-REWRITE "derivable" "identity_NQ" "deriv_TCC" ("const_fun_convergent[(A(x!1))]")) (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (|sum_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "sum_derivable") NIL))) (|opposite_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "opposite_derivable") NIL))) (|diff_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "diff_derivable") NIL))) (|prod_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "prod_derivable") NIL))) (|scal_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "scal_derivable") NIL))) (|const_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "const_derivable") NIL))) (|inv_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "inv_derivable") NIL))) (|div_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "div_derivable") NIL))) (|identity_derivable2| "" (EXPAND "derivable") (("" (GRIND :DEFS NIL :REWRITES "identity_derivable") NIL))) (|deriv_TCC1| "" (AUTO-REWRITE "derivable") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) NIL))))) (|deriv_sum_TCC1| "" (LEMMA "sum_derivable") (("" (PROPAX) NIL))) (|deriv_sum_TCC2| "" (SKOSIMP) NIL) (|deriv_sum_TCC3| "" (SKOSIMP) NIL) (|deriv_sum| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "sum_derivable" "derivable" "deriv" "sum_NQ" "limit_sum_fun[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (|deriv_opposite_TCC1| "" (LEMMA "opposite_derivable") (("" (PROPAX) NIL))) (|deriv_opposite| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "opposite_derivable" "derivable" "deriv" "opposite_NQ" "limit_opposite_fun[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (|deriv_diff_TCC1| "" (LEMMA "diff_derivable") (("" (PROPAX) NIL))) (|deriv_diff| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "diff_derivable" "derivable" "deriv" "diff_NQ" "limit_diff_fun[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (|deriv_prod_TCC1| "" (LEMMA "prod_derivable") (("" (PROPAX) 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))]")) (("1" (ASSERT) (("1" (USE "limit_prod_NQ" ("l1" "lim(NQ(f1!1, x!1), 0)" "l2" "lim(NQ(f2!1, x!1), 0)")) (("1" (GROUND) NIL))))) ("2" (SKOSIMP) NIL))))))))) (|deriv_const_TCC1| "" (LEMMA "const_derivable") (("" (PROPAX) NIL))) (|deriv_const| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "const_derivable" "derivable" "deriv" "const_NQ" "limit_const_fun[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (|deriv_scal_TCC1| "" (LEMMA "scal_derivable") (("" (PROPAX) NIL))) (|deriv_scal| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "scal_derivable" "derivable" "deriv" "scal_NQ" "limit_scal_fun[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (|deriv_inv_TCC1| "" (LEMMA "inv_derivable") (("" (PROPAX) 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))]")) (("1" (ASSERT) (("1" (USE "limit_inv_NQ" ("l1" "lim(NQ(g!1, x!1), 0)")) (("1" (ASSERT) NIL))))) ("2" (SKOSIMP) NIL))))))))) (|deriv_div_TCC1| "" (LEMMA "div_derivable") (("" (PROPAX) NIL))) (|deriv_div_TCC2| "" (SKOSIMP) NIL) (|deriv_div_TCC3| "" (SKOSIMP) NIL) (|deriv_div| "" (GRIND :DEFS NIL :REWRITES ("inv_derivable" "deriv_inv" "deriv_prod" "div_function[T]" "/")) NIL) (|deriv_identity_TCC1| "" (LEMMA "identity_derivable") (("" (PROPAX) NIL))) (|deriv_identity| "" (SKOSIMP) (("" (AUTO-REWRITE "deriv_TCC" "identity_derivable" "derivable" "deriv" "identity_NQ" "limit_const_fun[(A(x!1))]") (("1" (ASSERT) NIL) ("2" (SKOSIMP) NIL))))) (SUBTYPE_TCC1 "" (SKOLEM-TYPEPRED) NIL) (SUBTYPE_TCC2 "" (SKOLEM!) (("" (REWRITE "derivable_continuous2") NIL))) (SUBTYPE_TCC3 "" (SKOLEM!) (("" (REWRITE "derivable_continuous2") NIL))) (|plus_TCC1| "" (SKOSIMP) (("" (REWRITE "sum_derivable2") NIL))) (|difference_TCC1| "" (SKOSIMP) (("" (REWRITE "diff_derivable2") NIL))) (|times_TCC1| "" (SKOSIMP) (("" (REWRITE "prod_derivable2") NIL))) (|times_TCC2| "" (SKOSIMP) (("" (REWRITE "scal_derivable2") NIL))) (|difference_TCC2| "" (SKOSIMP) (("" (REWRITE "opposite_derivable2") NIL))) (|divide_TCC1| "" (SKOLEM!) (("" (REWRITE "div_derivable2") NIL))) (|divide_TCC2| "" (SKOLEM!) (("" (REWRITE "scaldiv_function[T]") (("" (REWRITE "div_derivable2") (("" (REWRITE "const_derivable2") NIL))))))) (|Const_TCC1| "" (SKOLEM!) (("" (REWRITE "const_derivable2") NIL))) (|constant_derivable| "" (EXPAND "Const") (("" (LEMMA "const_derivable") (("" (PROPAX) NIL))))) (|deriv_constant_TCC1| "" (LEMMA "constant_derivable") (("" (PROPAX) NIL))) (|deriv_constant| "" (EXPAND "Const") (("" (LEMMA "deriv_const") (("" (PROPAX) NIL))))) (|Id_TCC1| "" (LEMMA "identity_derivable2") (("" (PROPAX) NIL))) (|id_derivable| "" (EXPAND "Id") (("" (LEMMA "identity_derivable") (("" (PROPAX) NIL))))) (|deriv_id_TCC1| "" (LEMMA "id_derivable") (("" (PROPAX) NIL))) (|deriv_id| "" (EXPAND "Id") (("" (LEMMA "deriv_identity") (("" (PROPAX) NIL))))) (|deriv_TCC2| "" (AUTO-REWRITE "derivable" "deriv_TCC") (("" (SKOSIMP :PREDS? T) (("" (ASSERT) (("" (INST?) NIL))))))) (|deriv_sum_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "+" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_sum") (("1" (INST?) NIL) ("2" (INST? -2) NIL))))))))))))) (|deriv_opp_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "-" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_opposite") (("" (INST?) NIL))))))))))))) (|deriv_diff_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "-" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_diff") (("1" (INST?) NIL) ("2" (INST? -2) NIL))))))))))))) (|deriv_prod_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "+" +) (("" (EXPAND "*" 1 2) (("" (EXPAND "*" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_prod") (("1" (INST?) NIL) ("2" (INST? -2) NIL))))))))))))))))) (|deriv_scal_fun| "" (SKOLEM-TYPEPRED) (("" (EXPAND "derivable") (("" (APPLY-EXTENSIONALITY :HIDE? T) (("" (EXPAND "*" 1 2) (("" (EXPAND "deriv") (("" (REWRITE "deriv_scal") (("" (INST?) NIL))))))))))))) (|deriv_inv_fun_TCC1| "" (SKOSIMP) (("" (EXPAND "*") (("" (REWRITE "zero_times3") (("" (GROUND) NIL))))))) (|deriv_inv_fun_TCC2| "" (SUBTYPE-TCC) 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))))))))))) ("2" (DELETE -) (("2" (GRIND :REWRITES "zero_times3") 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))) ("2" (GRIND :REWRITES "zero_times3") NIL))))))))) ("2" (DELETE 2) (("2" (APPLY-EXTENSIONALITY :HIDE? T) (("2" (GRIND) 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))))))))))))) ("2" (DELETE -) (("2" (GRIND :REWRITES "zero_times3") NIL))))))))) (|deriv_const_fun| "" (SKOLEM!) (("" (AUTO-REWRITE "Const" "const_fun" "deriv_const" "const_derivable") (("" (EXPAND "deriv") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL))))))) (|deriv_id_fun| "" (AUTO-REWRITE "Id" "Const" "const_fun" "deriv_identity" "identity_derivable") (("" (EXPAND "deriv") (("" (APPLY-EXTENSIONALITY :HIDE? T) NIL)))))) $$$top_derivative.pvs top_derivative : THEORY BEGIN IMPORTING derivatives, derivative_props, chain_rule END top_derivative