$$$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 JUDGEMENT sqrt HAS_TYPE [posreal -> 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 x < 1 IMPLIES sqrt(x) < 1 sqrt_gt1_bound : LEMMA x > 1 IMPLIES sqrt(x) > 1 sqrt_le1_bound : LEMMA x <= 1 IMPLIES sqrt(x) <= 1 sqrt_ge1_bound : LEMMA x >= 1 IMPLIES sqrt(x) >= 1 END square_root $$$square_root.prf (|square_root| (|sqrt_def| "" (AUTO-REWRITE "expt_x2" "root_def" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|square_sqrt| "" (SKOLEM!) (("" (REWRITE "sqrt_def" :DIR RL) NIL))) (|sqrt_square| "" (SKOLEM!) (("" (REWRITE "sqrt_def") NIL))) (|square_sqrt2| "" (AUTO-REWRITE "expt_root" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|sqrt_square2| "" (AUTO-REWRITE "root_expt" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|sqrt_TCC1| "" (SKOLEM!) (("" (EXPAND "sqrt") (("" (REWRITE "root_TCC2") NIL))))) (|sqrt_zero| "" (REWRITE "sqrt_def") NIL) (|sqrt_one| "" (REWRITE "sqrt_def") NIL) (|null_sqrt| "" (AUTO-REWRITE "sqrt" "null_root") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|sqrt_mult| "" (AUTO-REWRITE "sqrt" "root_mult") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|sqrt_inv| "" (AUTO-REWRITE "sqrt" "root_inv") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|sqrt_div| "" (AUTO-REWRITE "sqrt" "root_div") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|both_sides_sqrt| "" (AUTO-REWRITE "both_sides_root" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|both_sides_sqrt_lt| "" (AUTO-REWRITE "both_sides_root_lt" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|both_sides_sqrt_le| "" (AUTO-REWRITE "both_sides_root_le" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|both_sides_sqrt_gt| "" (AUTO-REWRITE "both_sides_root_gt" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|both_sides_sqrt_ge| "" (AUTO-REWRITE "both_sides_root_ge" "sqrt") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|sqrt_lt1_bound| "" (AUTO-REWRITE "root_lt1_bound2" "sqrt") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|sqrt_gt1_bound| "" (AUTO-REWRITE "root_gt1_bound" "sqrt") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|sqrt_le1_bound| "" (AUTO-REWRITE "root_le1_bound" "sqrt") (("" (SKOSIMP) (("" (ASSERT) NIL))))) (|sqrt_ge1_bound| "" (AUTO-REWRITE "root_ge1_bound" "sqrt") (("" (SKOSIMP) (("" (ASSERT) 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| "" (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) ("2" (DELETE -1 -2 2) (("2" (REWRITE "lt_times_lt_pos1") (("2" (LEMMA "diff_abs" ("x" "x2!1" "y" "y2!1")) (("2" (ASSERT) NIL))))))))) ("2" (DELETE -1 2) (("2" (REWRITE "le_times_le_pos") 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 + "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) ("2" (AUTO-REWRITE "both_sides_times_pos_le1" "le_times_le_pos") (("2" (GROUND) 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))))))))))) ("2" (SKOLEM!) (("2" (REWRITE "times_div1") (("2" (REWRITE "div_mult_pos_lt1") NIL))))))))))))))) (|expt_continuous| "" (AUTO-REWRITE "expt" "null_abs2") (("" (INDUCT "n") (("1" (SKOLEM!) (("1" (INST + "1") (("1" (SKOSIMP) (("1" (ASSERT) 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)))))))))))))))))))))))))))) $$$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| "" (GRIND :IF-MATCH NIL) NIL) (|incr_even| "" (GRIND :IF-MATCH NIL) (("1" (INST + "j!1 - 1") (("1" (ASSERT) NIL))) ("2" (INST + "j!1 + 1") (("2" (ASSERT) NIL))))) (|opposite_odd| "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1-1") (("1" (ASSERT) NIL))) ("2" (INST + "- j!1 -1") (("2" (ASSERT) NIL))))) (|opposite_even| "" (GRIND :IF-MATCH NIL) (("1" (INST + "-j!1") (("1" (ASSERT) NIL))) ("2" (INST + "-j!1") (("2" (ASSERT) NIL))))) (|parity1| "" (CASE "FORALL (n : nat) : odd?(n) OR odd?(n + 1)") (("1" (SKOSIMP) (("1" (CASE "i!1 >= 0") (("1" (INST?) (("1" (ASSERT) 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))))))))))))) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOLEM!) (("2" (GROUND) (("2" (DELETE 1) (("2" (EXPAND "odd?") (("2" (SKOLEM!) (("2" (INST + "j!2 + 1") (("2" (ASSERT) NIL))))))))))))))))))) (|parity2| "" (AUTO-REWRITE "incr_even") (("" (SKOSIMP) (("" (ASSERT) (("" (USE "parity1") (("" (ASSERT) NIL))))))))) (|odd_not_even| "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL))))))))) (|even_not_odd| "" (SKOLEM!) (("" (GROUND) (("1" (GRIND) NIL) ("2" (USE "parity1") (("2" (ASSERT) (("2" (REWRITE "incr_odd" -1) NIL))))))))) (|even_2i| "" (GRIND) NIL) (|odd_2i_plus1| "" (GRIND) NIL) (|odd_2i_minus1| "" (SKOLEM!) (("" (REWRITE "incr_even" :DIR RL) (("" (REWRITE "even_2i") NIL))))) (|parity_zero| "" (GRIND) NIL) (|parity_one| "" (REWRITE "incr_odd") (("" (REWRITE "parity_zero") NIL))) (|parity_two| "" (REWRITE "incr_even") (("" (REWRITE "parity_one") NIL))) (|parity_three| "" (REWRITE "incr_odd") (("" (REWRITE "parity_two") NIL))) (|parity_minus_one| "" (REWRITE "opposite_odd") (("" (REWRITE "parity_one") NIL))) (|parity_minus_two| "" (REWRITE "opposite_even") (("" (REWRITE "parity_two") NIL))) (|parity_minus_three| "" (REWRITE "opposite_odd") (("" (REWRITE "parity_three") NIL)))) $$$real_facts.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Properties of real numbers % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% real_facts : THEORY BEGIN %---------------------------------------- % More properties of archimedean field %---------------------------------------- archimedean2 : THEOREM FORALL (x : posreal) : EXISTS (a : posnat) : 1/a < x archimedean3 : THEOREM FORALL (x : nonneg_real) : (FORALL (a : posnat) : x <= 1/a) implies x = 0 %------------------------------------------------- % Every real is between two successive integers %------------------------------------------------- nat_interval : LEMMA FORALL (x : nonneg_real) : EXISTS (a : nat) : a <= x and x < a + 1 int_interval : PROPOSITION FORALL (x : real) : EXISTS (a : integer) : a <= x and x < a +1 %--------------------------- % 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)))))))))))))) $$$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, real_facts, 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 JUDGEMENT expt HAS_TYPE [nzreal, nat -> 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 %------------------------------------------------- % Anti-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) (|expt_TCC1| "" (INDUCT-AND-SIMPLIFY "x2" :REWRITES ("zero_times3")) NIL) (|expt_x0| "" (GRIND) NIL) (|expt_x1| "" (GRIND) NIL) (|expt_x2| "" (GRIND) NIL) (|expt_1n| "" (INDUCT-AND-SIMPLIFY "n") NIL) (|expt_mult| "" (INDUCT-AND-SIMPLIFY "n") NIL) (|expt_div| "" (INDUCT-AND-SIMPLIFY "n") NIL) (|expt_inv| "" (SKOLEM!) (("" (REWRITE "expt_div") (("" (REWRITE "expt_1n") NIL))))) (|abs_expt| "" (INDUCT-AND-SIMPLIFY "n" :REWRITES "prod_abs") NIL) (|expt_plus| "" (SKOLEM 1 ("m!1" _ "x!1")) (("" (INDUCT-AND-SIMPLIFY "n") NIL))) (|expt_minus_TCC1| "" (SKOSIMP) (("" (ASSERT) NIL))) (|expt_minus| "" (SKOSIMP) (("" (ASSERT) (("" (USE "expt_plus" ("n" "m!1 - n!1" "m" "n!1")) (("" (ASSERT) NIL))))))) (|expt_times| "" (SKOLEM 1 (_ "n!1" "x!1")) (("" (INDUCT-AND-SIMPLIFY "m" :REWRITES ("expt_plus")) NIL))) (|expt_divide| "" (SKOLEM!) (("" (REWRITE "expt_inv") (("" (REWRITE "expt_times") NIL))))) (|expt_zero| "" (GRIND) 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) ("2" (ASSERT) (("2" (GRIND) NIL))))))))) ("2" (DELETE 2) (("2" (SKOLEM 1 (_ "x!1")) (("2" (INDUCT-AND-REWRITE "n" 1 "expt" "zero_times3") NIL))))))) (|expt_minus_one| "" (INDUCT "n") (("1" (GRIND) NIL) ("2" (SKOSIMP) (("2" (AUTO-REWRITE "expt") (("2" (ASSERT) (("2" (REWRITE "incr_even" +) (("2" (REWRITE "odd_not_even") (("2" (SMASH) NIL))))))))))))) (|odd_expt_m1| "" (SKOLEM-TYPEPRED) (("" (AUTO-REWRITE "expt_minus_one" "even_not_odd") (("" (ASSERT) NIL))))) (|even_expt_m1| "" (SKOLEM!) (("" (REWRITE "expt_minus_one") NIL))) (|expt_m1_2n| "" (AUTO-REWRITE "expt_minus_one" "even_2i") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|expt_m1_2n1| "" (AUTO-REWRITE "expt_minus_one" "even_not_odd" "odd_2i_plus1") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|expt_opp_aux| "" (SKOLEM!) (("" (REWRITE "expt_mult" :DIR RL) (("" (ASSERT) NIL))))) (|expt_opposite| "" (AUTO-REWRITE "expt_minus_one") (("" (SKOLEM!) (("" (REWRITE "expt_opp_aux") (("" (SMASH) NIL))))))) (|odd_expt_opposite| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "expt_opp_aux") (("" (REWRITE "odd_expt_m1") (("" (ASSERT) NIL))))))))) (|even_expt_opposite| "" (SKOSIMP) (("" (ASSERT) (("" (REWRITE "expt_opp_aux") (("" (REWRITE "even_expt_m1") (("" (ASSERT) NIL))))))))) (|expt_opp_2n| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_m1_2n") (("" (REWRITE "expt_opp_aux") (("" (ASSERT) NIL))))))) (|expt_opp_2n1| "" (SKOSIMP) (("" (AUTO-REWRITE "expt_m1_2n1") (("" (REWRITE "expt_opp_aux") (("" (ASSERT) NIL))))))) (|odd_expt_negative| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_pos_aux") (("1" (ASSERT) NIL) ("2" (EXPAND "expt") (("2" (LIFT-IF) (("2" (GROUND) NIL))))))) ("2" (USE "expt_pos_aux" ("px" "- x!1" "n" "odn!1")) (("2" (REWRITE "odd_expt_opposite") (("2" (ASSERT) NIL))))))))) (|odd_expt_positive| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_pos_aux" ("px" "- x!1")) (("1" (REWRITE "odd_expt_opposite") (("1" (ASSERT) NIL))) ("2" (AUTO-REWRITE "expt") (("2" (USE "oddnat_positive") (("2" (ASSERT) NIL))))))) ("2" (USE "expt_pos_aux") NIL))))) (|even_expt_positive| "" (SKOLEM!) (("" (AUTO-REWRITE "expt" "even_expt_opposite") (("" (GROUND) (("1" (EXPAND "expt") (("1" (ASSERT) NIL))) ("2" (CASE "x!1 < 0") (("1" (ASSERT) (("1" (USE "expt_pos_aux" ("px" "-x!1" "n" "evn!1")) (("1" (ASSERT) NIL))))) ("2" (REWRITE "expt_pos_aux") NIL))))))))) (|even_expt_negative| "" (SKOLEM!) (("" (USE "even_expt_positive") (("" (AUTO-REWRITE "expt") (("" (GROUND) 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))))) ("2" (DELETE 2) (("2" (INDUCT "n") (("1" (GROUND) NIL) ("2" (GROUND) NIL) ("3" (SKOSIMP) (("3" (EXPAND "expt" +) (("3" (GROUND) (("1" (CASE-REPLACE "x!1 = 0") (("1" (ASSERT) (("1" (REWRITE "pos_times_lt") NIL))) ("2" (ASSERT) (("2" (REWRITE "lt_times_lt_pos1") 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))))))))))))))))))) (|both_sides_expt_nonneg_le| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL))))) (|both_sides_expt_nonneg_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_lt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) NIL))))) (|both_sides_expt_nonneg_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_nonneg_gt" ("nnx" "nny!1" "nny" "nnx!1")) (("" (GROUND) 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))))))) (|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))))) ("2" (ASSERT) NIL))) ("2" (CASE "y!1 < 0") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (REWRITE "both_sides_expt_nonneg_lt") NIL))))))))))))))) (|both_sides_expt_odd_le| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL))))) (|both_sides_expt_odd_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_lt" ("x" "y!1" "y" "x!1")) (("" (GROUND) NIL))))) (|both_sides_expt_odd_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_odd_gt" ("x" "y!1" "y" "x!1")) (("" (GROUND) 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))))))) (|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))))))))) (|both_sides_expt_nonpos_even_le| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_lt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL))))) (|both_sides_expt_nonpos_even_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_lt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) NIL))))) (|both_sides_expt_nonpos_even_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_nonpos_even_gt" ("npx" "npy!1" "npy" "npx!1")) (("" (GROUND) 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))))))) (|expt_lt1_bound1| "" (INDUCT-AND-SIMPLIFY "n") (("" (USE "both_sides_times_pos_le2" ("pz" "lt1x!1")) (("" (ASSERT) 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))))))))))) (|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))))))))) (|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))))))))) (|expt_lt_one| "" (SKOLEM!) (("" (AUTO-REWRITE "expt_1n" "expt_zero" "expt_lt1_bound2") (("" (GROUND) (("1" (CASE-REPLACE "nnx!1 = 1") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (USE "expt_gt1_bound1") (("2" (ASSERT) NIL))))))) ("2" (CASE-REPLACE "nnx!1=0") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))) (|expt_le_one| "" (SKOLEM!) (("" (GROUND) (("1" (USE "expt_gt1_bound2") (("1" (ASSERT) NIL))) ("2" (AUTO-REWRITE "expt_zero" "expt_1n" "expt_lt1_bound1") (("2" (CASE-REPLACE "nnx!1=0") (("1" (ASSERT) NIL) ("2" (CASE-REPLACE "nnx!1=1") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))))))) (|expt_gt_one| "" (SKOLEM!) (("" (USE "expt_le_one") (("" (GROUND) NIL))))) (|expt_ge_one| "" (SKOLEM!) (("" (USE "expt_lt_one") (("" (GROUND) NIL))))) (|expt_eq_one| "" (SKOLEM!) (("" (USE* "expt_lt_one" "expt_gt_one") (("" (GROUND) 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))) ("2" (INST?) (("2" (ASSERT) 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))))))))))))))))))))) (|both_sides_expt_lt1_le| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL))))) (|both_sides_expt_lt1_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL))))) (|both_sides_expt_lt1_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_lt1_le" ("n" "m!1" "m" "n!1")) (("" (GROUND) 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))) ("2" (INST?) (("2" (ASSERT) 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))))))))))))))))))))) (|both_sides_expt_gt1_le| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL))))) (|both_sides_expt_gt1_gt| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_lt" ("n" "m!1" "m" "n!1")) (("" (GROUND) NIL))))) (|both_sides_expt_gt1_ge| "" (SKOLEM!) (("" (USE "both_sides_expt_gt1_le" ("n" "m!1" "m" "n!1")) (("" (GROUND) 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))))) ("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))))))))))) (|large_expt| "" (SKOSIMP) (("" (ASSERT) (("" (AUTO-REWRITE-THEORY "sets[real]") (("" (LEMMA "real_complete1" ("S" "{x:real | EXISTS (n : nat) : x = expt(a!1, n)}")) (("1" (SPLIT) (("1" (DELETE 1) (("1" (GRIND :EXCLUDE "expt" :IF-MATCH NIL) (("1" (INST -3 "x!1 / a!1") (("1" (CASE "x!1 > 0") (("1" (GROUND) (("1" (LEMMA "both_sides_div_pos_le2" ("px" "1" "py" "a!1" "pz" "x!1")) (("1" (ASSERT) NIL))) ("2" (SKOSIMP*) (("2" (INST -4 "x!2 * a!1") (("2" (REWRITE "div_mult_pos_le2") (("2" (ASSERT) (("2" (INST 2 "n!1+1") (("2" (EXPAND "expt" +) (("2" (ASSERT) NIL))))))))))))))) ("2" (DELETE -3) (("2" (INST -2 "1") (("2" (ASSERT) (("2" (INST 2 "0") (("2" (EXPAND "expt") (("2" (PROPAX) NIL))))))))))))))))))) ("2" (SKOLEM!) (("2" (INST 1 "b!1") (("2" (GRIND :EXCLUDE "expt" :IF-MATCH NIL) (("2" (INST? 2) (("2" (ASSERT) NIL))))))))))) ("2" (INST -1 "1") (("2" (INST 1 "0") (("2" (EXPAND "expt") (("2" (PROPAX) NIL))))))))))))))) (|small_expt| "" (SKOSIMP*) (("" (LEMMA "large_expt" ("a" "1/a!1")) (("" (REWRITE "div_mult_pos_lt2") (("" (ASSERT) (("" (INST -1 "1/b!1") (("" (SKOLEM!) (("" (INST 1 "n!1") (("" (REWRITE "expt_inv") (("" (REWRITE "both_sides_div_pos_lt2") 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 JUDGEMENT root HAS_TYPE [posreal, posnat -> 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 x < 1 IMPLIES root(x, m) < 1 root_le1_bound : LEMMA x <= 1 IMPLIES root(x, m) <= 1 root_ge1_bound : LEMMA x >= 1 IMPLIES root(x, m) >= 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| "" (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))))))))))))))))) (|root_aux2| "" (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))))))) ("2" (ASSERT) (("2" (INST - "0") (("2" (CASE-REPLACE "expt(0, m!1) = 0") (("1" (EXPAND "abs") (("1" (LIFT-IF) (("1" (GROUND) NIL))))) ("2" (EXPAND "expt" +) (("2" (ASSERT) NIL))))))))))))))))))) (|root_exists| "" (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))))))) ("2" (USE "root_aux2" ("y" "x!1")) (("2" (ASSERT) (("2" (SKOSIMP) (("2" (DELETE -3) (("2" (INST - "z!1") (("2" (ASSERT) (("2" (SKOLEM-TYPEPRED) (("2" (USE "both_sides_expt_nonneg_lt" ("nnx" "y!2" "nny" "z!1")) (("2" (ASSERT) 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))))))))) ("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))))))))))))))))) ("2" (DELETE 2) (("2" (AUTO-REWRITE-THEORY "sets[real]") (("2" (ASSERT) (("2" (INST - "0") (("2" (ASSERT) NIL))))))))))))))) (|root_TCC1| "" (INST + "lambda x, m: epsilon! y: expt(y, m) = x") (("" (SKOLEM!) (("" (USE "epsilon_ax[nonneg_real]") (("" (GROUND) (("" (USE "root_exists") NIL))))))))) (|expt_root| "" (SKOLEM!) (("" (ASSERT) NIL))) (|root_def| "" (SKOLEM!) (("" (GROUND) (("" (USE "both_sides_expt_nonneg" ("nny" "root(x!1, m!1)")) (("" (ASSERT) NIL))))))) (|root_expt| "" (SKOLEM!) (("" (REWRITE "root_def") NIL))) (|root_TCC2| "" (SKOLEM!) (("" (NAME-REPLACE "xxx" "root(x1!1, x2!1)" :HIDE? NIL) (("" (REWRITE "root_def") (("" (GRIND) NIL))))))) (|root_zero| "" (SKOLEM!) (("" (REWRITE "root_def") (("" (REWRITE "expt_zero") NIL))))) (|root_one| "" (AUTO-REWRITE "root_def" "expt_1n") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|root_x1| "" (AUTO-REWRITE "root_def" "expt_x1") (("" (SKOLEM!) (("" (ASSERT) NIL))))) (|null_root| "" (GRIND :DEFS NIL :REWRITES ("root_zero" "root_def" "expt")) NIL) (|root_mult| "" (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))))))))) (|root_inv| "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "expt_inv") (("" (NAME-REPLACE "xxx" "root(px!1, m!1)" :HIDE? NIL) (("" (ASSERT) NIL))))))) (|root_div| "" (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))))))))) (|root_times| "" (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))))))))))))) (|both_sides_root| "" (AUTO-REWRITE "root_def" "expt_root") (("" (SKOLEM!) (("" (ASSERT) (("" (GROUND) NIL))))))) (|both_sides_root_lt| "" (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))))))))))))))) (|both_sides_root_le| "" (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))))))))))))))) (|both_sides_root_gt| "" (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))))))))))))))) (|both_sides_root_ge| "" (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))))))))))))))) (|root_lt1_bound| "" (SKOLEM!) (("" (NAME-REPLACE "xx1" "root(lt1x!1, m!1)" :HIDE? NIL) (("" (REWRITE "root_def") (("" (USE "expt_gt1_bound1") (("1" (ASSERT) NIL) ("2" (USE "expt_1n" ("n" "m!1")) (("2" (ASSERT) NIL))))))))))) (|root_gt1_bound| "" (SKOLEM!) (("" (AUTO-REWRITE "root_def" "expt_1n" "expt_zero") (("" (NAME-REPLACE "xx1" "root(gt1x!1, m!1)" :HIDE? NIL) (("" (ASSERT) (("" (CASE-REPLACE "xx1=0") (("1" (ASSERT) NIL) ("2" (CASE-REPLACE "xx1=1") (("1" (ASSERT) NIL) ("2" (ASSERT) (("2" (USE "expt_lt1_bound1") (("2" (ASSERT) NIL))))))))))))))))) (|root_lt1_bound2| "" (SKOSIMP) (("" (AUTO-REWRITE "root_zero" "root_lt1_bound") (("" (CASE-REPLACE "x!1 = 0") (("1" (ASSERT) NIL) ("2" (ASSERT) NIL))))))) (|root_le1_bound| "" (SKOSIMP) (("" (CASE-REPLACE "x!1 = 1") (("1" (REWRITE "root_one") NIL) ("2" (ASSERT) (("2" (USE "root_lt1_bound2") (("2" (ASSERT) NIL))))))))) (|root_ge1_bound| "" (SKOSIMP) (("" (CASE-REPLACE "x!1 = 1") (("1" (REWRITE "root_one") NIL) ("2" (ASSERT) (("2" (USE "root_gt1_bound") (("2" (ASSERT) NIL))))))))) (|both_sides_root_lt1_lt| "" (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))))) ("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))))))))))))))))))))) (|both_sides_root_lt1_le| "" (SKOLEM!) (("" (USE "both_sides_root_lt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL))))) (|both_sides_root_lt1_gt| "" (SKOLEM!) (("" (USE "both_sides_root_lt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL))))) (|both_sides_root_lt1_ge| "" (SKOLEM!) (("" (USE "both_sides_root_lt1_gt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL))))) (|both_sides_root_gt1_lt| "" (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))))) ("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))))))))))))))))))))) (|both_sides_root_gt1_le| "" (SKOLEM!) (("" (USE "both_sides_root_gt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL))))) (|both_sides_root_gt1_gt| "" (SKOLEM!) (("" (USE "both_sides_root_gt1_lt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL))))) (|both_sides_root_gt1_ge| "" (SKOLEM!) (("" (USE "both_sides_root_gt1_gt" ("m" "p!1" "p" "m!1")) (("" (GROUND) NIL))))) (|equal_roots| "" (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))))))) ("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))))))))))))