%Patch files loaded: patch2 version 1.2.2.11 \$\$\$square_root.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Defines square root % % Specializes the lemmas on roots % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% square_root : THEORY BEGIN IMPORTING roots x, y : VAR nonneg_real px, py : VAR posreal %-------------- % Definition %-------------- sqrt(x) : nonneg_real = root(x, 2) sqrt_def : LEMMA sqrt(x) = y IFF y * y = x square_sqrt : LEMMA sqrt(x) * sqrt(x) = x sqrt_square : LEMMA sqrt(x * x) = x square_sqrt2 : LEMMA expt(sqrt(x), 2) = x sqrt_square2 : LEMMA sqrt(expt(x, 2)) = x posreal_sqrt_is_positive: JUDGEMENT sqrt(px) HAS_TYPE posreal %-------------- % Properties %-------------- sqrt_zero : LEMMA sqrt(0) = 0 sqrt_one : LEMMA sqrt(1) = 1 null_sqrt : LEMMA sqrt(x) = 0 IFF x = 0 sqrt_mult : LEMMA sqrt(x * y) = sqrt(x) * sqrt(y) sqrt_inv : LEMMA sqrt(1/px) = 1 / sqrt(px) sqrt_div : LEMMA sqrt(x/py) = sqrt(x) / sqrt(py) %---------------- % Monotonicity %---------------- both_sides_sqrt : LEMMA sqrt(x) = sqrt(y) IFF x = y both_sides_sqrt_lt : LEMMA sqrt(x) < sqrt(y) IFF x < y both_sides_sqrt_le : LEMMA sqrt(x) <= sqrt(y) IFF x <= y both_sides_sqrt_gt : LEMMA sqrt(x) > sqrt(y) IFF x > y both_sides_sqrt_ge : LEMMA sqrt(x) >= sqrt(y) IFF x >= y %---------- % Bounds %---------- sqrt_lt1_bound : LEMMA sqrt(x) < 1 IFF x < 1 sqrt_gt1_bound : LEMMA sqrt(x) > 1 IFF x > 1 sqrt_le1_bound : LEMMA sqrt(x) <= 1 IFF x <= 1 sqrt_ge1_bound : LEMMA sqrt(x) >= 1 IFF x >= 1 END square_root \$\$\$square_root.prf (|square_root| (|sqrt_def| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "expt_x2" "root_def" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|square_sqrt| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (REWRITE "sqrt_def" :DIR RL) NIL NIL)) NIL) (|sqrt_square| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (REWRITE "sqrt_def") NIL NIL)) NIL) (|square_sqrt2| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "expt_root" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_square2| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "root_expt" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|posreal_sqrt_is_positive| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|sqrt_zero| (:NEW-GROUND? NIL) "" (REWRITE "sqrt_def") NIL NIL) (|sqrt_one| (:NEW-GROUND? NIL) "" (REWRITE "sqrt_def") NIL NIL) (|null_sqrt| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "sqrt" "null_root") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_mult| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "sqrt" "root_mult") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_inv_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|sqrt_inv| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "sqrt" "root_inv") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_div| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "sqrt" "root_div") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|both_sides_sqrt| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "both_sides_root" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|both_sides_sqrt_lt| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "both_sides_root_lt" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|both_sides_sqrt_le| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "both_sides_root_le" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|both_sides_sqrt_gt| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "both_sides_root_gt" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|both_sides_sqrt_ge| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "both_sides_root_ge" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_lt1_bound| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "root_lt1_bound2" "sqrt") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_gt1_bound| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "root_gt1_bound2" "sqrt") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_le1_bound| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "root_le1_bound" "sqrt") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|sqrt_ge1_bound| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "root_ge1_bound" "sqrt") (("" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL)) NIL)) \$\$\$extra_props.pvs extra_props : THEORY BEGIN IMPORTING absolute_value x1, x2, y1, y2 : VAR real e, e1, e2, d: VAR posreal n : VAR nat 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 expt_continuous : LEMMA FORALL x1, e, n : EXISTS d : FORALL y1 : abs(y1 - x1) < d IMPLIES abs(expt(y1, n) - expt(x1, n)) < e END extra_props \$\$\$extra_props.prf (|extra_props| (|prod_bound| (:NEW-GROUND? NIL) "" (SKOSIMP) (("" (LEMMA "sum_abs" ("x" "(x1!1 - y1!1) * x2!1" "y" "(x2!1 - y2!1) * y1!1")) (("" (REWRITE "prod_abs") (("" (REWRITE "prod_abs") (("" (ASSERT) (("" (CASE "abs(x2!1 - y2!1) * abs(y1!1) <= e2!1 * abs(y1!1)") (("1" (CASE "abs(x1!1 - y1!1) * abs(x2!1) < e1!1 * (abs(y2!1) + e2!1)") (("1" (ASSERT) NIL NIL) ("2" (DELETE -1 -2 2) (("2" (REWRITE "lt_times_lt_pos1") (("2" (LEMMA "diff_abs" ("x" "x2!1" "y" "y2!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -1 2) (("2" (REWRITE "le_times_le_pos") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|prod_epsilon| (:NEW-GROUND? NIL) "" (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 + "min(u!1, w!1)" "v!1") (("1" (ASSERT) (("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" (GROUND) NIL NIL) ("2" (AUTO-REWRITE "both_sides_times_pos_le1" "le_times_le_pos") (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (NAME-REPLACE "f" "e!1/3") (("2" (CASE "FORALL (x : nonneg_real) : x * (f / (x+1)) < f") (("1" (INST-CP - "abs(y1!1)") (("1" (INST - "abs(y2!1)") (("1" (ASSERT) (("1" (INST + "abs(y1!1) + 1" "f / (abs(y1!1) + 1)" "f / (abs(y2!1) + 1)") (("1" (REWRITE "div_cancel1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (REWRITE "times_div1") (("2" (REWRITE "div_mult_pos_lt1") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|expt_continuous| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "expt" "null_abs2") (("" (INDUCT "n") (("1" (SKOLEM!) (("1" (INST + "1") (("1" (SKOSIMP) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (SKOSIMP*) (("2" (ASSERT) (("2" (USE "prod_epsilon" ("e" "e!1" "y1" "x1!1" "y2" "expt(x1!1, j!1)")) (("2" (SKOSIMP) (("2" (INST - "x1!1" "e2!1") (("2" (SKOLEM!) (("2" (INST + "min(d!1, e1!1)") (("2" (SKOSIMP) (("2" (INST - "y1!1") (("2" (ASSERT) (("2" (USE "prod_bound") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$parity.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % A few lemmas about odd or even numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% parity : THEORY BEGIN i : VAR int incr_odd : LEMMA odd?(i + 1) IFF even?(i) incr_even : LEMMA even?(i + 1) IFF odd?(i) opposite_odd : LEMMA odd?(- i) IFF odd?(i) opposite_even : LEMMA even?(- i) IFF even?(i) parity1 : LEMMA odd?(i) OR odd?(i + 1) parity2 : LEMMA even?(i) OR even?(i + 1) odd_not_even : LEMMA odd?(i) IFF not even?(i) even_not_odd : LEMMA even?(i) IFF not odd?(i) even_2i : LEMMA even?(2 * i) odd_2i_plus1 : LEMMA odd?(2 * i + 1) odd_2i_minus1 : LEMMA odd?(2 * i - 1) %------------------------------------- % Rewrite rules for small constants %------------------------------------- parity_zero: LEMMA even?(0) parity_one: LEMMA odd?(1) parity_two: LEMMA even?(2) parity_three: LEMMA odd?(3) parity_minus_one: LEMMA odd?(-1) parity_minus_two: LEMMA even?(-2) parity_minus_three: LEMMA odd?(-3) END parity \$\$\$parity.prf (|parity| (|incr_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) NIL NIL) (|incr_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "j!1 - 1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "j!1 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_odd| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1-1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "- j!1 -1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|opposite_even| (:NEW-GROUND? NIL) "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST + "-j!1") (("2" (ASSERT) NIL NIL)) NIL)) NIL) (|parity1| (:NEW-GROUND? NIL) "" (CASE "FORALL (n : nat) : odd?(n) OR odd?(n + 1)") (("1" (SKOSIMP) (("1" (CASE "i!1 >= 0") (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) (("2" (INST - "- (1 + i!1)") (("2" (REWRITE "opposite_odd" 2 :DIR RL) (("2" (REWRITE "opposite_odd" 3 :DIR RL) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GRIND) NIL NIL) ("2" (SKOLEM!) (("2" (GROUND) (("2" (DELETE 1) (("2" (EXPAND "odd?") (("2" (SKOLEM!) (("2" (INST + "j!2 + 1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|parity2| (:NEW-GROUND? NIL) "" (AUTO-REWRITE "incr_even") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "parity1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|odd_not_even| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_not_odd| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_2i| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|odd_2i_plus1| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|odd_2i_minus1| (:NEW-GROUND? NIL) "" (SKOLEM!) (("" (REWRITE "incr_even" :DIR RL) (("" (REWRITE "even_2i") NIL NIL)) NIL)) NIL) (|parity_zero| (:NEW-GROUND? NIL) "" (GRIND) NIL NIL) (|parity_one| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd") (("" (REWRITE "parity_zero") NIL NIL)) NIL) (|parity_two| (:NEW-GROUND? NIL) "" (REWRITE "incr_even") (("" (REWRITE "parity_one") NIL NIL)) NIL) (|parity_three| (:NEW-GROUND? NIL) "" (REWRITE "incr_odd") (("" (REWRITE "parity_two") NIL NIL)) NIL) (|parity_minus_one_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_one| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd") (("" (REWRITE "parity_one") NIL NIL)) NIL) (|parity_minus_two_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_two| (:NEW-GROUND? NIL) "" (REWRITE "opposite_even") (("" (REWRITE "parity_two") NIL NIL)) NIL) (|parity_minus_three_TCC1| (:NEW-GROUND? NIL) "" (SUBTYPE-TCC) NIL NIL) (|parity_minus_three| (:NEW-GROUND? NIL) "" (REWRITE "opposite_odd") (("" (REWRITE "parity_three") NIL NIL)) NIL)) \$\$\$absolute_value.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properites of absolute value %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% absolute_value : THEORY BEGIN x, y : VAR real z : VAR nzreal null_abs : PROPOSITION abs(x) = 0 IFF x = 0 null_abs2 : PROPOSITION abs(0) = 0 positive_abs : PROPOSITION abs(z) > 0 diff_abs : PROPOSITION abs(x) - abs(y) <= abs(x - y) % sum_abs is triangle in prelude % sum_abs : PROPOSITION abs(x + y) <= abs(x) + abs(y) neg_abs : PROPOSITION abs(- x) = abs(x) % prod_abs is abs_mult in prelude % prod_abs : PROPOSITION abs(x * y) = abs(x) * abs(y) inverse_abs : PROPOSITION abs(1/z) = 1/abs(z) divide_abs : PROPOSITION abs(x/z) = abs(x)/abs(z) abs_abs : PROPOSITION abs(abs(x)) = abs(x) abs_square : PROPOSITION abs(x * x) = x * x %--- abs(x - y) as distance between x and y ---% t, a, b : VAR real diff_abs_commute : PROPOSITION abs(x - y) = abs(y - x) null_distance : PROPOSITION x = y IFF abs(x - y) = 0 triangle2 : PROPOSITION abs(x - t) < a AND abs(x - y) < b IMPLIES abs(t - y) < a + b END absolute_value \$\$\$absolute_value.prf (|absolute_value| (|null_abs| "" (SKOLEM!) (("" (PROP) (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (ASSERT) NIL))))) ("2" (REPLACE -1) (("2" (EXPAND "abs") (("2" (PROPAX) NIL))))))))) (|null_abs2| "" (EXPAND "abs") (("" (PROPAX) NIL))) (|positive_abs| "" (SKOLEM!) (("" (ASSERT) NIL))) (|diff_abs| "" (SKOLEM!) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (LIFT-IF) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))))) (|sum_abs| "" (LEMMA "triangle") (("" (PROPAX) NIL))) (|neg_abs| "" (SKOLEM!) (("" (EXPAND "abs") (("" (LIFT-IF) (("" (ASSERT) (("" (LIFT-IF) (("" (ASSERT) NIL))))))))))) (|prod_abs| "" (LEMMA "abs_mult") (("" (PROPAX) NIL))) (|inverse_abs| "" (SKOLEM!) (("" (EXPAND "abs") (("" (CASE "1 / z!1 < 0") (("1" (ASSERT) (("1" (REWRITE "quotient_neg_lt") (("1" (ASSERT) NIL))))) ("2" (ASSERT) (("2" (REWRITE "quotient_neg_lt") (("2" (ASSERT) NIL))))))))))) (|divide_abs| "" (SKOLEM!) (("" (LEMMA "times_div1" ("x" "x!1" "y" "1" "n0z" "z!1")) (("" (ASSERT) (("" (REPLACE -1 + RL) (("" (REWRITE "prod_abs") (("" (REWRITE "inverse_abs") (("" (ASSERT) NIL))))))))))))) (|abs_abs| "" (SKOLEM!) (("" (EXPAND "abs" 1 1) (("" (LIFT-IF) (("" (GROUND) NIL))))))) (|abs_square| "" (SKOLEM!) (("" (REWRITE "prod_abs") (("" (GRIND) NIL))))) (|diff_abs_commute| "" (SKOLEM!) (("" (LEMMA "neg_abs" ("x" "x!1 - y!1")) (("" (ASSERT) NIL))))) (|null_distance| "" (SKOLEM!) (("" (REWRITE "null_abs") (("" (GROUND) NIL))))) (|triangle2| "" (SKOSIMP) (("" (REWRITE "diff_abs_commute") (("" (LEMMA "sum_abs" ("x" "t!1 - x!1" "y" "x!1 - y!1")) (("" (ASSERT) NIL)))))))) \$\$\$exponent_props.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%% % More properties of expt % %%%%%%%%%%%%%%%%%%%%%%%%%%%%% exponent_props : THEORY BEGIN IMPORTING absolute_value, parity n, m : VAR nat p : VAR posnat x, y : VAR real z : VAR nzreal nnx, nny : VAR nonneg_real npx, npy : VAR nonpos_real a, b : VAR posreal lt1x : VAR { a | a < 1} gt1x : VAR { a | 1 < a } evn : VAR { n | even?(n) } evp : VAR { p | even?(p) } odn : VAR { n | odd?(n) } oddnat_positive : LEMMA odn > 0 expt_nonzero_is_nonzero: JUDGEMENT expt(z, n) HAS_TYPE nzreal %------------------------------------ % Powers of product, inverse, etc. %------------------------------------ expt_x0 : LEMMA expt(x, 0) = 1 expt_x1 : LEMMA expt(x, 1) = x expt_x2 : LEMMA expt(x, 2) = x * x expt_1n : LEMMA expt(1, n) = 1 expt_mult : LEMMA expt(x * y, n) = expt(x, n) * expt(y, n) expt_div : LEMMA expt(x / z, n) = expt(x, n) / expt(z, n) expt_inv : LEMMA expt(1 / z, n) = 1 / expt(z, n) abs_expt : LEMMA abs(expt(x, n)) = expt(abs(x), n) %------------------------------------------------------- % Same properties as in the prelude % (not restricted to non-zero reals unless necessary) %------------------------------------------------------- expt_plus : LEMMA expt(x, n + m) = expt(x, n) * expt(x, m) expt_minus : LEMMA n <= m IMPLIES expt(z, m - n) = expt(z, m) / expt(z, n) expt_times : LEMMA expt(x, n * m) = expt(expt(x, n), m) expt_divide : LEMMA 1 / expt(z, m * n) = expt(1/expt(z, m), n) expt_zero : LEMMA expt(0, p) = 0 null_expt : LEMMA expt(x, n) = 0 IFF x = 0 AND n > 0 %---------------- % Powers of -1 %---------------- expt_minus_one : LEMMA expt(-1, n) = IF even?(n) THEN 1 ELSE -1 ENDIF odd_expt_m1 : LEMMA expt(-1, odn) = -1 even_expt_m1 : LEMMA expt(-1, evn) = 1 expt_m1_2n : LEMMA expt(-1, 2 * n) = 1 expt_m1_2n1 : LEMMA expt(-1, 2 * n + 1) = -1 %---------------- % Powers of -x %---------------- expt_opp_aux : LEMMA expt(- x, n) = expt(-1, n) * expt(x, n) expt_opposite : LEMMA expt(- x, n) = IF even?(n) THEN expt(x, n) ELSE - expt(x, n) ENDIF odd_expt_opposite : LEMMA expt(- x, odn) = - expt(x, odn) even_expt_opposite : LEMMA expt(-x, evn) = expt(x, evn) expt_opp_2n : LEMMA expt(-x, 2 * n) = expt(x, 2 * n) expt_opp_2n1 : LEMMA expt(-x, 2 * n + 1) = - expt(x, 2 * n + 1) %--------------------------------- % Sign of x^n for n odd or even %--------------------------------- odd_expt_negative : LEMMA expt(x, odn) < 0 IFF x < 0 odd_expt_positive : LEMMA expt(x, odn) > 0 IFF x > 0 even_expt_positive : LEMMA expt(x, evn) > 0 IFF x /= 0 OR evn = 0 even_expt_negative : LEMMA NOT expt(x, evn) < 0 %-------------------------------------------------------------- % Monotonicity for non-negative arguments, positive exponent %-------------------------------------------------------------- both_sides_expt_nonneg_lt : LEMMA expt(nnx, p) < expt(nny, p) IFF nnx < nny both_sides_expt_nonneg_le : LEMMA expt(nnx, p) <= expt(nny, p) IFF nnx <= nny both_sides_expt_nonneg_gt : LEMMA expt(nnx, p) > expt(nny, p) IFF nnx > nny both_sides_expt_nonneg_ge : LEMMA expt(nnx, p) >= expt(nny, p) IFF nnx >= nny both_sides_expt_nonneg : LEMMA expt(nnx, p) = expt(nny, p) IFF nnx = nny %--------------------------------- % Monotonicity for odd exponent %--------------------------------- both_sides_expt_odd_lt : LEMMA expt(x, odn) < expt(y, odn) IFF x < y both_sides_expt_odd_le : LEMMA expt(x, odn) <= expt(y, odn) IFF x <= y both_sides_expt_odd_gt : LEMMA expt(x, odn) > expt(y, odn) IFF x > y both_sides_expt_odd_ge : LEMMA expt(x, odn) >= expt(y, odn) IFF x >= y both_sides_expt_odd : LEMMA expt(x, odn) = expt(y, odn) IFF x = y %------------------------------------------------- % Monotonicity for positive, even exponent % and non-positive arguments %------------------------------------------------- both_sides_expt_nonpos_even_lt : LEMMA expt(npx, evp) < expt(npy, evp) IFF npy < npx both_sides_expt_nonpos_even_le : LEMMA expt(npx, evp) <= expt(npy, evp) IFF npy <= npx both_sides_expt_nonpos_even_gt : LEMMA expt(npx, evp) > expt(npy, evp) IFF npy > npx both_sides_expt_nonpos_even_ge : LEMMA expt(npx, evp) >= expt(npy, evp) IFF npy >= npx both_sides_expt_nonpos_even : LEMMA expt(npx, evp) = expt(npy, evp) IFF npx = npy %---------------------------------------------- % Bounds of powers x for 0 < x < 1 OR x > 1 %---------------------------------------------- expt_lt1_bound1 : LEMMA expt(lt1x, n) <= 1 expt_lt1_bound2 : LEMMA expt(lt1x, p) < 1 expt_gt1_bound1 : LEMMA 1 <= expt(gt1x, n) expt_gt1_bound2 : LEMMA 1 < expt(gt1x, p) expt_lt_one : LEMMA expt(nnx, p) < 1 IFF nnx < 1 expt_le_one : LEMMA expt(nnx, p) <= 1 IFF nnx <= 1 expt_gt_one : LEMMA expt(nnx, p) > 1 IFF nnx > 1 expt_ge_one : LEMMA expt(nnx, p) >= 1 IFF nnx >= 1 expt_eq_one : LEMMA expt(nnx, p) = 1 IFF nnx = 1 %---------------------------------- % Order relations for 0 < x < 1 %---------------------------------- both_sides_expt_lt1_lt : LEMMA expt(lt1x, n) < expt(lt1x, m) IFF m < n both_sides_expt_lt1_le : LEMMA expt(lt1x, n) <= expt(lt1x, m) IFF m <= n both_sides_expt_lt1_gt : LEMMA expt(lt1x, n) > expt(lt1x, m) IFF m > n both_sides_expt_lt1_ge : LEMMA expt(lt1x, n) >= expt(lt1x, m) IFF m >= n %----------------------------- % Order relations for x > 1 %----------------------------- both_sides_expt_gt1_lt : LEMMA expt(gt1x, n) < expt(gt1x, m) IFF n < m both_sides_expt_gt1_le : LEMMA expt(gt1x, n) <= expt(gt1x, m) IFF n <= m both_sides_expt_gt1_gt : LEMMA expt(gt1x, n) > expt(gt1x, m) IFF n > m both_sides_expt_gt1_ge : LEMMA expt(gt1x, n) >= expt(gt1x, m) IFF n >= m %--------------------------------------- % Equal powers for a /= 1 %--------------------------------------- both_sides_expt_pos : LEMMA FORALL (a | a /= 1) : expt(a, n) = expt(a, m) IFF n = m %---------------------------------- % No upper bound on a^n if 1 < a % Lower bound = 0 if 0 < a < 1 %---------------------------------- large_expt : LEMMA 1 < a IMPLIES (FORALL b : EXISTS n : b < expt(a, n)) small_expt : LEMMA a < 1 IMPLIES (FORALL b : EXISTS n : expt(a, n) < b) END exponent_props \$\$\$exponent_props.prf (|exponent_props| (|oddnat_positive| "" (GRIND) NIL NIL) (|expt_nonzero_is_nonzero| "" (INDUCT-AND-SIMPLIFY "n" :REWRITES ("zero_times3")) NIL NIL) (|expt_x0| "" (GRIND) NIL NIL) (|expt_x1| "" (GRIND) NIL NIL) (|expt_x2| "" (GRIND) NIL NIL) (|expt_1n| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL) (|expt_mult| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL) (|expt_div| "" (INDUCT-AND-SIMPLIFY "n") NIL NIL) (|expt_inv| "" (SKOLEM!) (("" (REWRITE "expt_div") (("" (REWRITE "expt_1n") NIL NIL)) NIL)) NIL) (|abs_expt| "" (INDUCT-AND-SIMPLIFY "n" :REWRITES "prod_abs") NIL NIL) (|expt_plus| "" (SKOLEM 1 ("m!1" _ "x!1")) (("" (INDUCT-AND-SIMPLIFY "n") NIL NIL)) NIL) (|expt_minus_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL NIL)) NIL) (|expt_minus| "" (SKOSIMP) (("" (ASSERT) (("" (USE "expt_plus" ("n" "m!1 - n!1" "m" "n!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|expt_times| "" (SKOLEM 1 (_ "n!1" "x!1")) (("" (INDUCT-AND-SIMPLIFY "m" :REWRITES ("expt_plus")) NIL NIL)) NIL) (|expt_divide| "" (SKOLEM!) (("" (REWRITE "expt_inv") (("" (REWRITE "expt_times") NIL NIL)) NIL)) NIL) (|expt_zero| "" (GRIND) NIL NIL) (|null_expt| "" (CASE "FORALL n, x : expt(x, n) = 0 IMPLIES x=0 AND n>0") (("1" (SKOLEM!) (("1" (INST?) (("1" (CASE "expt(x!1, n!1) = 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOLEM 1 (_ "x!1")) (("2" (INDUCT-AND-REWRITE "n" 1 "expt" "zero_times3") NIL NIL)) NIL)) NIL)) NIL) (|expt_minus_one| "" (INDUCT "n") (("1" (GRIND) NIL NIL) ("2" (SKOSIMP) (("2" (AUTO-REWRITE "expt") (("2" (ASSERT) (("2" (REWRITE "incr_even" +) (("2" (REWRITE "odd_not_even") (("2" (SMASH) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|odd_expt_m1| "" (SKOLEM-TYPEPRED) (("" (AUTO-REWRITE "expt_minus_one" "even_not_odd") (("" (ASSERT) NIL NIL)) NIL)) NIL) (|even_expt_m1| "" (SKOLEM!) (("" (REWRITE "expt_minus_one") NIL NIL)) NIL) (|expt_m1_2n| "" (AUTO-REWRITE "expt_minus_one" "even_2i") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_m1_2n1| "" (AUTO-REWRITE "expt_minus_one" "even_not_odd" "odd_2i_plus1") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_opp_aux| "" (SKOLEM!) (("" (REWRITE "expt_mult" :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_opposite| "" (AUTO-REWRITE "expt_minus_one") (("" (SKOLEM!) (("" (REWRITE "expt_opp_aux") (("" (SMASH) NIL NIL)) NIL)) NIL)) NIL) (|odd_expt_opposite| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "expt_opp_aux") (("" (REWRITE "odd_expt_m1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_expt_opposite| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "expt_opp_aux") (("" (REWRITE "even_expt_m1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_opp_2n| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_m1_2n") (("" (REWRITE "expt_opp_aux") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|expt_opp_2n1| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_m1_2n1") (("" (REWRITE "expt_opp_aux") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|odd_expt_negative| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_pos_aux") (("1" (ASSERT) NIL NIL) ("2" (EXPAND "expt") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "expt_pos_aux" ("px" "- x!1" "n" "odn!1")) (("2" (REWRITE "odd_expt_opposite") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|odd_expt_positive| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_pos_aux" ("px" "- x!1")) (("1" (REWRITE "odd_expt_opposite") (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "expt") (("2" (USE "oddnat_positive") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "expt_pos_aux") NIL NIL)) NIL)) NIL) (|even_expt_positive| "" (SKOLEM!) (("" (AUTO-REWRITE "expt" "even_expt_opposite") (("" (GROUND) (("1" (EXPAND "expt") (("1" (ASSERT) NIL NIL)) NIL) ("2" (CASE "x!1 < 0") (("1" (ASSERT) (("1" (USE "expt_pos_aux" ("px" "-x!1" "n" "evn!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (REWRITE "expt_pos_aux") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|even_expt_negative| "" (SKOLEM!) (("" (USE "even_expt_positive") (("" (AUTO-REWRITE "expt") (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_expt_nonneg_lt| "" (AUTO-REWRITE "expt_x1" "expt_zero") (("" (SKOLEM 1 ("x!1" "y!1" _)) (("" (CASE "FORALL n : expt(x!1, n+1) < expt(y!1, n+1) IFF x!1 < y!1") (("1" (SKOLEM!) (("1" (INST?) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GROUND) NIL NIL) ("2" (GROUND) NIL NIL) ("3" (SKOSIMP) (("3" (EXPAND "expt" +) (("3" (GROUND) (("1" (CASE-REPLACE "x!1 = 0") (("1" (ASSERT) (("1" (REWRITE "pos_times_lt") NIL NIL)) NIL) ("2" (ASSERT) (("2" (REWRITE "lt_times_lt_pos1") NIL NIL)) NIL)) NIL) ("2" (USE "le_times_le_pos" ("nnx" "y!1" "y" "x!1" "nnz" "expt(y!1, 1 + j!1)" "w" "expt(x!1, 1 + j!1)")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_nonneg_le| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonneg_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonneg_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_gt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonneg| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nny" "nny!1")) (("" (USE "both_sides_expt_nonneg_gt" ("nny" "nny!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_expt_odd_lt| "" (SKOLEM!) (("" (AUTO-REWRITE "odd_expt_opposite" "oddnat_positive") (("" (USE "odd_expt_negative") (("" (USE "odd_expt_negative" ("x" "y!1")) (("" (CASE "x!1 < 0") (("1" (CASE "y!1 < 0") (("1" (ASSERT) (("1" (USE "both_sides_expt_nonneg_lt" ("nnx" "-y!1" "nny" "-x!1" "p" "odn!1")) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL) ("2" (CASE "y!1 < 0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (REWRITE "both_sides_expt_nonneg_lt") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_odd_le| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_odd_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_odd_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_gt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_odd| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("y" "y!1")) (("" (USE "both_sides_expt_odd_gt" ("y" "y!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_lt| "" (SKOLEM!) (("" (USE "even_expt_opposite" ("x" "npx!1")) (("" (USE "even_expt_opposite" ("x" "npy!1")) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "-npx!1" "nny" "-npy!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_le| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_lt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_lt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_gt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_nonpos_even| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_gt" ("npy" "npy!1")) (("" (USE "both_sides_expt_nonpos_even_lt" ("npy" "npy!1")) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|expt_lt1_bound1| "" (INDUCT-AND-SIMPLIFY "n") (("" (USE "both_sides_times_pos_le2" ("pz" "lt1x!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|expt_lt1_bound2| "" (SKOLEM!) (("" (USE "expt_lt1_bound1" ("n" "p!1 - 1")) (("" (AUTO-REWRITE "expt") (("" (EXPAND "expt" +) (("" (USE "both_sides_times_pos_le1" ("pz" "lt1x!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|expt_gt1_bound1| "" (SKOLEM 1 ("a!1" _)) (("" (INDUCT-AND-SIMPLIFY "n") (("" (LEMMA "both_sides_times_pos_le2") (("" (INST -1 "expt(a!1, j!1)" "1" "a!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_gt1_bound2| "" (SKOLEM!) (("" (USE "expt_gt1_bound1" ("n" "p!1 - 1")) (("" (EXPAND "expt" +) (("" (USE "both_sides_times_pos_le1" ("pz" "gt1x!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_lt_one| "" (SKOLEM!) (("" (AUTO-REWRITE "expt_1n" "expt_zero" "expt_lt1_bound2") (("" (GROUND) (("1" (CASE-REPLACE "nnx!1 = 1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) (("2" (USE "expt_gt1_bound1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (CASE-REPLACE "nnx!1=0") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_le_one| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_gt1_bound2") (("1" (ASSERT) NIL NIL)) NIL) ("2" (AUTO-REWRITE "expt_zero" "expt_1n" "expt_lt1_bound1") (("2" (CASE-REPLACE "nnx!1=0") (("1" (ASSERT) NIL NIL) ("2" (CASE-REPLACE "nnx!1=1") (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|expt_gt_one| "" (SKOLEM!) (("" (USE "expt_le_one") (("" (GROUND) NIL NIL)) NIL)) NIL) (|expt_ge_one| "" (SKOLEM!) (("" (USE "expt_lt_one") (("" (GROUND) NIL NIL)) NIL)) NIL) (|expt_eq_one| "" (SKOLEM!) (("" (USE* "expt_lt_one" "expt_gt_one") (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_lt1_lt| "" (SKOLEM!) (("" (CASE "FORALL (n, m : nat) : m < n IMPLIES expt(lt1x!1, n) < expt(lt1x!1, m)") (("1" (PROP) (("1" (INST -2 "m!1" "n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (USE "expt_plus" ("n" "m!2" "m" "n!2 - m!2")) (("2" (ASSERT) (("2" (LEMMA "both_sides_times_pos_lt1") (("2" (INST - "expt(lt1x!1, m!2)" "expt(lt1x!1, n!2 - m!2)" "1") (("2" (AUTO-REWRITE "expt_lt1_bound2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_lt1_le| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_lt1_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_lt1_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_le" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_gt1_lt| "" (SKOLEM!) (("" (CASE "FORALL (n, m : nat) : n < m IMPLIES expt(gt1x!1, n) < expt(gt1x!1, m)") (("1" (PROP) (("1" (INST -2 "m!1" "n!1") (("1" (ASSERT) NIL NIL)) NIL) ("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (SKOSIMP) (("2" (ASSERT) (("2" (USE "expt_plus" ("n" "n!2" "m" "m!2 - n!2")) (("2" (ASSERT) (("2" (LEMMA "both_sides_times_pos_lt2") (("2" (INST - "expt(gt1x!1, n!2)" "1" "expt(gt1x!1, m!2 - n!2)") (("2" (AUTO-REWRITE "expt_gt1_bound2") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_expt_gt1_le| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_gt1_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_gt1_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_le" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_expt_pos| "" (SKOLEM!) (("" (CASE "a!1 < 1") (("1" (USE "both_sides_expt_lt1_lt" ("m" "m!1")) (("1" (USE "both_sides_expt_lt1_gt" ("m" "m!1")) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (USE "both_sides_expt_gt1_lt" ("m" "m!1")) (("2" (USE "both_sides_expt_gt1_gt" ("m" "m!1")) (("2" (GROUND) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|large_expt| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[real]") (("" (LEMMA "real_complete" ("S" "{x:real | EXISTS (n : nat) : x = expt(a!1, n)}")) (("1" (GROUND) (("1" (DELETE 1) (("1" (GRIND :IF-MATCH NIL) (("1" (INST -3 "y!1 / a!1") (("1" (CASE "y!1 > 0") (("1" (GROUND) (("1" (LEMMA "both_sides_div_pos_le2" ("px" "1" "py" "a!1" "pz" "y!1")) (("1" (ASSERT) NIL NIL)) NIL) ("2" (SKOSIMP* :PREDS? T) (("2" (INST - "s!1 * a!1") (("1" (REWRITE "div_mult_pos_le2") NIL NIL) ("2" (INST + "n!1+1") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE -3) (("2" (INST - "1") (("1" (ASSERT) NIL NIL) ("2" (INST + "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (SKOLEM!) (("2" (INST + "b!1") (("2" (GRIND :IF-MATCH NIL) (("2" (INST?) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (INST - "1") (("2" (INST + "0") (("2" (EXPAND "expt") (("2" (PROPAX) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|small_expt| "" (SKOSIMP*) (("" (LEMMA "large_expt" ("a" "1/a!1")) (("" (REWRITE "div_mult_pos_lt2") (("" (ASSERT) (("" (INST - "1/b!1") (("" (SKOLEM!) (("" (INST + "n!1") (("" (REWRITE "expt_inv") (("" (REWRITE "both_sides_div_pos_lt2") NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) \$\$\$roots.pvs roots : THEORY BEGIN IMPORTING exponent_props, extra_props x, y, z : VAR nonneg_real px, py : VAR posreal m, p : VAR posnat lt1x : VAR { px | px < 1 } gt1x : VAR { x | 1 < x } %--------------------- % Existence of root %--------------------- root_aux1 : LEMMA expt(x, m) < y IMPLIES EXISTS z : x < z AND expt(z, m) < y root_aux2 : LEMMA y < expt(x, m) IMPLIES EXISTS z : z < x AND y < expt(z, m) root_exists : LEMMA FORALL x, m : EXISTS y : expt(y, m) = x %-------------- % Definition %-------------- root(x, m) : { y | expt(y, m) = x } expt_root : LEMMA expt(root(x, m), m) = x root_def : LEMMA root(x, m) = y IFF expt(y, m) = x root_expt : LEMMA root(expt(x, m), m) = x posreal_root_is_positive: JUDGEMENT root(px, m) HAS_TYPE posreal %-------------- % Properties %-------------- root_zero : LEMMA root(0, m) = 0 root_one : LEMMA root(1, m) = 1 root_x1 : LEMMA root(x, 1) = x null_root : LEMMA root(x, m) = 0 IFF x = 0 root_mult : LEMMA root(x * y, m) = root(x, m) * root(y, m) root_inv : LEMMA root(1/px, m) = 1 / root(px, m) root_div : LEMMA root(x/py, m) = root(x, m) / root(py, m) root_times : LEMMA root(x, m * p) = root(root(x, m), p) %--------------------- % Monotonicity, etc. %--------------------- both_sides_root : LEMMA root(x, m) = root(y, m) IFF x = y both_sides_root_lt : LEMMA root(x, m) < root(y, m) IFF x < y both_sides_root_le : LEMMA root(x, m) <= root(y, m) IFF x <= y both_sides_root_gt : LEMMA root(x, m) > root(y, m) IFF x > y both_sides_root_ge : LEMMA root(x, m) >= root(y, m) IFF x >= y %---------- % Bounds %---------- root_lt1_bound : LEMMA root(lt1x, m) < 1 root_gt1_bound : LEMMA root(gt1x, m) > 1 root_lt1_bound2 : LEMMA root(x, m) < 1 IFF x < 1 root_gt1_bound2 : LEMMA root(x, m) > 1 IFF x > 1 root_le1_bound : LEMMA root(x, m) <= 1 IFF x <= 1 root_ge1_bound : LEMMA root(x, m) >= 1 IFF x >= 1 %-------------------- % Order properties %-------------------- both_sides_root_lt1_lt : LEMMA root(lt1x, m) < root(lt1x, p) IFF m < p both_sides_root_lt1_le : LEMMA root(lt1x, m) <= root(lt1x, p) IFF m <= p both_sides_root_lt1_gt : LEMMA root(lt1x, m) > root(lt1x, p) IFF m > p both_sides_root_lt1_ge : LEMMA root(lt1x, m) >= root(lt1x, p) IFF m >= p both_sides_root_gt1_lt : LEMMA root(gt1x, m) < root(gt1x, p) IFF p < m both_sides_root_gt1_le : LEMMA root(gt1x, m) <= root(gt1x, p) IFF p <= m both_sides_root_gt1_gt : LEMMA root(gt1x, m) > root(gt1x, p) IFF p > m both_sides_root_gt1_ge : LEMMA root(gt1x, m) >= root(gt1x, p) IFF p >= m equal_roots : LEMMA x /= 0 AND x /= 1 AND root(x, m) = root(x, p) IMPLIES m = p END roots \$\$\$roots.prf (|roots| (|root_aux1| (:NEW-GROUND? T) "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE "abs") (("" (USE "expt_continuous" ("e" "y!1 - expt(x!1, m!1)" "x1" "x!1")) (("" (SKOSIMP) (("" (INST + "x!1 + d!1/2") (("" (ASSERT) (("" (INST - "d!1 / 2 + x!1") (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|root_aux2| (:NEW-GROUND? T) "" (SKOSIMP) (("" (ASSERT) (("" (USE "expt_continuous" ("e" "expt(x!1, m!1) - y!1" "x1" "x!1")) (("" (SKOSIMP) (("" (INST + "x!1 - d!1/2") (("1" (ASSERT) (("1" (INST - "x!1 - d!1/2") (("1" (AUTO-REWRITE "abs") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST - "0") (("2" (CASE-REPLACE "expt(0, m!1) = 0") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL NIL)) NIL)) NIL) ("2" (EXPAND "expt" +) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|root_exists| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "least_upper_bound?" "upper_bound?" "expt_zero" "expt_x1_aux") (("" (LEMMA "real_complete" ("S" "{ u:real | u >= 0 AND expt(u, m!1) <= x!1 }")) (("1" (GROUND) (("1" (SKOSIMP) (("1" (INST-CP - "0") (("1" (ASSERT) (("1" (INST? +) (("1" (USE "root_aux1" ("y" "x!1")) (("1" (GROUND) (("1" (SKOSIMP) (("1" (ASSERT) (("1" (INST - "z!1") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (USE "root_aux2" ("y" "x!1")) (("2" (GROUND) (("2" (SKOSIMP) (("2" (DELETE -3) (("2" (INST - "z!1") (("2" (ASSERT) (("2" (SKOLEM-TYPEPRED) (("2" (USE "both_sides_expt_nonneg_lt" ("nnx" "s!1" "nny" "z!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (CASE "x!1 <= 1") (("1" (INST + "1") (("1" (SKOLEM-TYPEPRED) (("1" (ASSERT) (("1" (USE "expt_gt1_bound2") (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (INST + "x!1") (("2" (SKOLEM-TYPEPRED) (("2" (USE "both_sides_expt_nonneg_le" ("nny" "x!1")) (("2" (USE "both_sides_expt_gt1_le" ("gt1x" "x!1" "n" "1" "m" "m!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) ("2" (DELETE 2) (("2" (AUTO-REWRITE-THEORY "sets[real]") (("2" (DO-REWRITE) (("2" (INST - "0") (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|root_TCC1| (:NEW-GROUND? T) "" (INST + "lambda x, m: epsilon! y: expt(y, m) = x") (("" (SKOLEM!) (("" (USE "epsilon_ax[nonneg_real]") (("" (GROUND) (("" (USE "root_exists") NIL NIL)) NIL)) NIL)) NIL)) NIL) (|expt_root| (:NEW-GROUND? T) "" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL) (|root_def| (:NEW-GROUND? T) "" (SKOLEM!) (("" (GROUND) (("" (USE "both_sides_expt_nonneg" ("nny" "root(x!1, m!1)")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|root_expt| (:NEW-GROUND? T) "" (SKOLEM!) (("" (REWRITE "root_def") NIL NIL)) NIL) (|posreal_root_is_positive| (:NEW-GROUND? T) "" (SKOLEM!) (("" (NAME-REPLACE "xxx" "root(px!1, m!1)" :HIDE? NIL) (("" (REWRITE "root_def") (("" (GRIND) NIL NIL)) NIL)) NIL)) NIL) (|root_zero| (:NEW-GROUND? T) "" (SKOLEM!) (("" (REWRITE "root_def") (("" (REWRITE "expt_zero") NIL NIL)) NIL)) NIL) (|root_one| (:NEW-GROUND? T) "" (AUTO-REWRITE "root_def" "expt_1n") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|root_x1| (:NEW-GROUND? T) "" (AUTO-REWRITE "root_def" "expt_x1") (("" (SKOLEM!) (("" (ASSERT) NIL NIL)) NIL)) NIL) (|null_root| (:NEW-GROUND? T) "" (GRIND :DEFS NIL :REWRITES ("root_zero" "root_def" "expt")) NIL NIL) (|root_mult| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "expt_mult") (("" (NAME-REPLACE "xx1" "root(x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(y!1, m!1)" :HIDE? NIL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|root_inv| (:NEW-GROUND? T) "" (SKOLEM!) (("" (NAME-REPLACE "xxx" "root(px!1, m!1)" :HIDE? NIL) (("" (CASE "xxx > 0") (("1" (AUTO-REWRITE "root_def" "expt_inv") (("1" (ASSERT) NIL NIL)) NIL) ("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) (|root_div| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "expt_div") (("" (NAME-REPLACE "xx1" "root(x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(py!1, m!1)" :HIDE? NIL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL) (|root_times| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def") (("" (NAME-REPLACE "xx1" "root(x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "xx2" "root(xx1, p!1)" :HIDE? NIL) (("" (ASSERT) (("" (USE "expt_times" ("n" "p!1" "m" "m!1")) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_root| (:NEW-GROUND? T) "" (AUTO-REWRITE "root_def" "expt_root") (("" (SKOLEM!) (("" (ASSERT) (("" (GROUND) NIL NIL)) NIL)) NIL)) NIL) (|both_sides_root_lt| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "both_sides_expt_nonneg_lt") (("" (NAME-REPLACE "xx1" "root(x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(y!1, m!1)" :HIDE? NIL) (("" (ASSERT) (("" (REPLACE -1 :DIR RL) (("" (REPLACE -2 :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_root_le| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "both_sides_expt_nonneg_le") (("" (NAME-REPLACE "xx1" "root(x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(y!1, m!1)" :HIDE? NIL) (("" (ASSERT) (("" (REPLACE -1 :DIR RL) (("" (REPLACE -2 :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_root_gt| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "both_sides_expt_nonneg_gt") (("" (NAME-REPLACE "xx1" "root(x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(y!1, m!1)" :HIDE? NIL) (("" (ASSERT) (("" (REPLACE -1 :DIR RL) (("" (REPLACE -2 :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_root_ge| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "both_sides_expt_nonneg_ge") (("" (NAME-REPLACE "xx1" "root(x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(y!1, m!1)" :HIDE? NIL) (("" (ASSERT) (("" (REPLACE -1 :DIR RL) (("" (REPLACE -2 :DIR RL) (("" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|root_lt1_bound| (:NEW-GROUND? T) "" (SKOLEM!) (("" (CASE-REPLACE "1 = root(1, m!1)") (("1" (REWRITE "both_sides_root_lt") NIL NIL) ("2" (REWRITE "root_one") NIL NIL)) NIL)) NIL) (|root_gt1_bound| (:NEW-GROUND? T) "" (SKOLEM!) (("" (CASE-REPLACE "1 = root(1, m!1)") (("1" (REWRITE "both_sides_root_gt") NIL NIL) ("2" (REWRITE "root_one") NIL NIL)) NIL)) NIL) (|root_lt1_bound2| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_lt" ("y" "1")) (("" (REWRITE "root_one") NIL NIL)) NIL)) NIL) (|root_gt1_bound2| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_gt" ("y" "1")) (("" (REWRITE "root_one") NIL NIL)) NIL)) NIL) (|root_le1_bound| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_le" ("y" "1")) (("" (REWRITE "root_one") NIL NIL)) NIL)) NIL) (|root_ge1_bound| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_ge" ("y" "1")) (("" (REWRITE "root_one") NIL NIL)) NIL)) NIL) (|both_sides_root_lt1_lt| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def") (("" (NAME-REPLACE "xx1" "root(lt1x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(lt1x!1, p!1)" :HIDE? NIL) (("" (ASSERT) (("" (USE "expt_lt_one" ("nnx" "yy1")) (("" (ASSERT) (("" (GROUND) (("1" (USE "both_sides_expt_lt1_ge" ("lt1x" "yy1" "m" "m!1" "n" "p!1")) (("1" (USE "both_sides_expt_nonneg_lt" ("nnx" "xx1" "nny" "yy1" "p" "m!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "both_sides_expt_nonneg_ge" ("p" "m!1" "nnx" "xx1" "nny" "yy1")) (("2" (USE "both_sides_expt_lt1_lt" ("lt1x" "yy1" "m" "m!1" "n" "p!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_root_lt1_le| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_lt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_root_lt1_gt| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_lt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_root_lt1_ge| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_lt1_gt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_root_gt1_lt| (:NEW-GROUND? T) "" (SKOLEM!) (("" (AUTO-REWRITE "root_def") (("" (NAME-REPLACE "xx1" "root(gt1x!1, m!1)" :HIDE? NIL) (("" (NAME-REPLACE "yy1" "root(gt1x!1, p!1)" :HIDE? NIL) (("" (ASSERT) (("" (USE "expt_gt_one" ("nnx" "xx1")) (("" (ASSERT) (("" (GROUND) (("1" (USE "both_sides_expt_gt1_ge" ("gt1x" "yy1" "m" "m!1" "n" "p!1")) (("1" (USE "both_sides_expt_nonneg_lt" ("nnx" "xx1" "nny" "yy1" "p" "m!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL) ("2" (USE "both_sides_expt_nonneg_ge" ("p" "p!1" "nnx" "xx1" "nny" "yy1")) (("2" (USE "both_sides_expt_gt1_lt" ("gt1x" "xx1" "m" "m!1" "n" "p!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL)) NIL) (|both_sides_root_gt1_le| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_gt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_root_gt1_gt| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_gt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|both_sides_root_gt1_ge| (:NEW-GROUND? T) "" (SKOLEM!) (("" (USE "both_sides_root_gt1_gt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL NIL)) NIL)) NIL) (|equal_roots| (:NEW-GROUND? T) "" (SKOSIMP) (("" (CASE "x!1 < 1") (("1" (ASSERT) (("1" (USE "both_sides_root_lt1_lt" ("p" "p!1")) (("1" (USE "both_sides_root_lt1_gt" ("p" "p!1")) (("1" (ASSERT) NIL NIL)) NIL)) NIL)) NIL) ("2" (ASSERT) (("2" (USE "both_sides_root_gt1_lt" ("p" "p!1")) (("2" (USE "both_sides_root_gt1_gt" ("p" "p!1")) (("2" (ASSERT) NIL NIL)) NIL)) NIL)) NIL)) NIL)) NIL))