Up to index of Isabelle/HOL/HOL-Complex/transnumber
theory TransNumberDerivationsheader {* Transarithmetic Theorems *} theory TransNumberDerivations imports TransNumberAxclass begin declare A3[simp] A4[simp] A7[simp] A9[simp] A11[simp] A14[simp] A15[simp] A16[simp] A20[simp] A21[simp] A22[simp] A25[simp]; constdefs reals :: "('a::trans_reals) set" "reals == {x. x ≠ Φ ∧ x ≠ ∞ ∧ x ≠ -∞}"; text{*Note : following subclassing allows reuse of standard add\_ac, etc. *} instance trans_reals ⊆ comm_monoid_add .. ; subsection{* Very elementary equations *} lemma additive_identity_right[simp]:" (x ::'a::trans_reals) + 0 = x"; by (subst A2, simp); lemma multiplicative_identity_right[simp]:" (x ::'a::trans_reals) * 1 = x"; by (subst A13, simp); lemma additive_nullity_right[simp]:" (x ::'a::trans_reals) + Φ = Φ"; by (subst A2, simp); lemma additive_infinity_right:"[| x ≠ -∞; x ≠ Φ |] ==> (x ::'a::trans_reals) + ∞ = ∞ "; by (subst A2, subst A5, auto); lemma minus_minus[simp]: "(x ::'a::trans_reals) - - y = x + y"; by (simp add: A6); lemma zero_mult_infinity[simp]: "0 * (∞ ::'a::trans_reals) = Φ"; by (subst A13, rule A16); lemma nullity_minus_left[simp]: "Φ - (x::'a::trans_reals) = Φ"; by (simp add: A6); lemma nullity_minus_right[simp]: " (x::'a::trans_reals) - Φ = Φ"; by (simp add: A6); lemma zero_minus_eq_uminus[simp]: "(0::'a::trans_reals) - x = -x"; by (simp add: A6); lemma uminus_eq_uminus[simp]: "(-(x::'a::trans_reals) = -y) = (x = y)"; by (safe, drule_tac f="λ x. - x" in arg_cong, simp); lemma uminus_add_eq_minus: "-x + y = y - (x::'a::trans_reals)"; by (subst A2, simp add: A6); lemma uminus_minus_commute: "-x - y = - y - (x::'a::trans_reals)"; by (simp add: A6 A2); lemma x_add_y_minus_y: "[| y ≠ Φ; y ≠ ∞; y ≠ -∞ |] ==> x + y - y = (x::'a::trans_reals)"; apply (subst A6, subst A1[THEN sym]); by (simp add: A6[THEN sym] A8); lemma uminus_x_add_x: "[| x≠ ∞; x≠ -∞; x≠ Φ |] ==> -x + x = (0::'a::trans_reals)"; by (subst A2, simp add: A6[THEN sym] A8); lemma x_minus_y_add_y: "[| y ≠ Φ; y ≠ ∞; y ≠ -∞ |] ==> x - y + y = (x::'a::trans_reals)"; apply (subst A6, subst A1[THEN sym]); by (simp add: uminus_x_add_x); lemma uminus_eq_nullity_iff[simp]: "!! x::'a::trans_reals. (-x = Φ) = (x = Φ)"; by (auto, drule_tac f="λ x. -x" in arg_cong, simp); lemma uminus_eq_infinity_iff[simp]: "!! x::'a::trans_reals. (-x = ∞) = (x = -∞)"; by (auto, drule_tac f="λ x. -x" in arg_cong, simp); lemma infinity_minus: "[| x ≠ Φ; x ≠ ∞ |] ==> ∞ - x = (∞::'a::trans_reals)"; by (subst A6, subst A5, simp_all); subsection{*Distinctness of six basic constants: 0, nullity, +1,-1, plus/minus infinity *} lemma not_zero_less_zero[simp]: "¬ 0 < (0::'a::trans_reals)"; by (cut_tac a="0::'a" in A28, auto); lemma zero_noteq_nullity[simp]: "(0 ::'a::trans_reals) ≠ Φ"; by (cut_tac a="Φ::'a" in A28, auto); lemmas nullity_noteq_zero[simp] = zero_noteq_nullity[THEN not_sym]; lemma zero_noteq_infinity[simp]: "(0 ::'a::trans_reals) ≠ ∞"; by (cut_tac a="(∞::'a)" in A28, simp); lemmas infinity_noteq_zero[simp] = zero_noteq_infinity[THEN not_sym]; lemma nullity_not_less_zero[simp]: "¬ Φ < (0 ::'a::trans_reals)"; by (cut_tac a="(Φ::'a)" in A28, simp); lemma zero_not_less_nullity[simp]: "¬ 0 < (Φ ::'a::trans_reals)"; by (cut_tac a="(Φ::'a)" in A28, simp); lemma infinity_noteq_nullity[simp]: "(∞::'a::trans_reals) ≠ Φ"; by (rule notI, drule_tac f="λ x. 0 < x" in arg_cong, simp); lemmas nullity_noteq_infinity[simp] = infinity_noteq_nullity[THEN not_sym]; lemma zero_less_one[simp]: "(0 ::'a::trans_reals) < 1"; by (simp add: A23[THEN sym]); lemma not_one_less_zero[simp]: "¬ (1 < (0::'a::trans_reals))"; by (cut_tac a="(1::'a)" in A28, auto); lemma zero_noteq_one[simp]: "(0 ::'a::trans_reals) ≠ 1"; by (cut_tac a="(1::'a)" in A28, auto); lemmas one_noteq_zero[simp] = zero_noteq_one[THEN not_sym]; lemma one_noteq_infinity[simp]: "(1 ::'a::trans_reals) ≠ ∞"; apply (rule classical, simp); by (drule_tac f="λ y. y * 0" in arg_cong, simp); lemmas infinity_noteq_one[simp] = one_noteq_infinity [THEN not_sym]; lemma nullity_noteq_one[simp]: "Φ ≠ (1 ::'a::trans_reals)"; by (rule notI, drule_tac f="λ x. 0 < x" in arg_cong, simp); lemmas one_not_nullity [simp] = nullity_noteq_one [THEN not_sym]; lemma minus_one_less_zero[simp]: "(- 1 ::'a::trans_reals) < 0"; by (subst A26[THEN sym], simp); lemma minus_one_mult_infinity[simp]: "(- 1 ::'a::trans_reals) * ∞ = - ∞"; by (subst A13, rule A24[THEN iffD2], rule minus_one_less_zero); lemma zero_noteq_minus_one[simp]: "(0::'a::trans_reals) ≠ - 1"; by (cut_tac a="- (1::'a)" in A28, auto); lemmas minus_one_noteq_zero[simp] = zero_noteq_minus_one [THEN not_sym]; lemma not_one_less_minus_one[simp]: "¬ ((0::'a::trans_reals) < - 1)"; by (cut_tac a="- (1::'a)" in A28, auto); lemma one_noteq_minus_one[simp]: "(1::'a::trans_reals) ≠ - 1"; by (rule notI, drule_tac f="λ x. x < 0" in arg_cong, simp); lemmas minus_one_noteq_one[simp] = one_noteq_minus_one [THEN not_sym]; lemma infinity_noteq_minus_one[simp]: "∞ ≠ (- 1 ::'a::trans_reals)"; by (rule notI, drule_tac f="λ x. 0 < x" in arg_cong, simp); lemmas minus_one_not_infinity [simp] = infinity_noteq_minus_one [THEN not_sym]; lemma nullity_noteq_minus_one[simp]: "Φ ≠ (- 1 ::'a::trans_reals)"; by (rule notI, drule_tac f="λ x. x < 0" in arg_cong, simp); lemmas minus_one_not_nullity [simp] = nullity_noteq_minus_one [THEN not_sym]; lemma zero_noteq_minus_infinity[simp]: "0 ≠ (- ∞ ::'a::trans_reals)"; apply (cut_tac a="- (∞ ::'a)" in A28, simp,safe); apply (erule notE); apply (rule A26[THEN iffD1]); by (subst A6, subst A7, simp); lemmas minus_infinity_noteq_zero[simp] = zero_noteq_minus_infinity[THEN not_sym]; lemma uminus_zero[simp]: "-(0 ::'a::trans_reals) = 0"; by (cut_tac a="0::'a" in A8, simp_all add: A6); lemma uminus_eq_zero_iff[simp]: "!! x::'a::trans_reals. (-x = 0) = (x = 0)"; by (auto, drule_tac f="λ x. -x" in arg_cong, simp); lemma minus_infinity_less_zero[simp]: "(-∞ ::'a::trans_reals) < 0"; by (rule A26 [THEN iffD1], simp); lemma minus_infinity_mult_infinity[simp]: "(-∞ ::'a::trans_reals) * ∞ = - ∞"; by (subst A13, rule A24[THEN iffD2], rule minus_infinity_less_zero); lemma not_zero_less_minus_infinity[simp]: "¬ 0 < (-∞ ::'a::trans_reals)"; by (cut_tac a="- (∞ ::'a)" in A28, auto); lemma one_noteq_minus_infinity[simp]: "1 ≠ (-∞ ::'a::trans_reals)"; apply (rule notI, drule_tac f="λ x. - x" in arg_cong); by (simp only: A7 minus_one_not_infinity); lemmas minus_infinity_noteq_one[simp] = one_noteq_minus_infinity [THEN not_sym]; lemma infinity_noteq_minus_infinity[simp]: "∞ ≠ (-∞ ::'a::trans_reals)"; by (rule notI, drule_tac f="λ x. 0 < x" in arg_cong, simp); lemmas minus_infinity_noteq_infinity[simp] = infinity_noteq_minus_infinity[THEN not_sym]; lemma nullity_noteq_minus_infinity[simp]: "Φ ≠ (-∞ ::'a::trans_reals)"; by (rule notI, drule_tac f="λ x. - x" in arg_cong, simp); lemmas minus_infinity_noteq_nullity[simp] = nullity_noteq_minus_infinity[THEN not_sym]; lemma one_minus_one_eq_zero[simp]: "(1::'a::trans_reals) - 1 = 0"; by (subst A8, auto); lemma less_irreflexive[simp]: "¬ x < (x::'a::trans_reals)"; apply (subst A26[THEN sym]); apply (case_tac "x = ∞", simp); apply (case_tac "x = -∞", simp add: A2 A6[THEN sym]); apply (case_tac "x=Φ", simp add: A6); by (subst A8, auto); text {* TODO: less\_transitive *} lemma not_less_zero_and_zero_less: "[| x < (0 ::'a::trans_reals); 0 < x |] ==> P"; by (cut_tac a="(x::'a)" in A28, auto); lemma less_zero_imp_not_zero: "x < (0 ::'a::trans_reals) ==> x ≠ 0"; by auto; lemma zero_less_imp_not_zero: "(0 ::'a::trans_reals) < x ==> x ≠ 0"; by auto; subsection{* sign equivalences *} lemma sgn_negative_iff: "!! a ::'a::trans_reals. (sgn a = - 1) = (a < 0)"; apply (unfold trans_sgn, auto); by (erule not_less_zero_and_zero_less, auto); lemma sgn_positive_iff: "!! a ::'a::trans_reals. (sgn a = 1) = (0 < a)"; by (unfold trans_sgn, auto); lemma sgn_zero[simp]: "sgn (0 ::'a::trans_reals) = 0"; by (unfold trans_sgn, simp); lemma sgn_zero_iff: "(sgn (x ::'a::trans_reals) = 0) = (x = 0)"; by (unfold trans_sgn, simp); lemma sgn_nullity[simp]: "sgn (Φ ::'a::trans_reals) = Φ"; by (unfold trans_sgn, simp); lemma sgn_nullity_iff: "(sgn (x ::'a::trans_reals) = Φ) = (x = Φ)"; apply (unfold trans_sgn, simp); by (cut_tac a="(x::'a)" in A28, auto); subsection{* Algebraic stuff and inequalities... *} lemma infinity_add_infinity[simp]: "(∞ ::'a::trans_reals) + ∞ = ∞"; by (simp add: A5); lemma minus_infinity_minus_infinity[simp]: "-(∞ ::'a::trans_reals) - ∞ = -∞"; by (simp add: A10); lemma minus_infinity_add_infinity[simp]: "-(∞ ::'a::trans_reals) + ∞ = Φ"; by (subst A2, simp add: A6[THEN sym]); lemma not_nullity_less[simp]: "¬ Φ < (x::'a::trans_reals)"; apply (subst A26[THEN sym]); apply (simp add: A23[THEN sym] A6); by (subst A13, simp); lemma not_less_nullity[simp]: "¬ x < (Φ::'a::trans_reals)"; apply (subst A26[THEN sym]); apply (simp add: A23[THEN sym] A6); by (subst A13, simp); lemma not_nullity_le_infinity: "x ≠ Φ ==> x < ∞ | x = (∞::'a::trans_reals)"; by (subst A26[THEN sym], clarsimp simp: infinity_minus); lemma less_infinity_iff: "(x < ∞) = (x ≠ (∞::'a::trans_reals) ∧ x ≠ Φ)"; by (auto dest: not_nullity_le_infinity); lemma not_nullity_minus_infinity_le: "x ≠ Φ ==> -∞ < x | x = (-∞::'a::trans_reals)"; by (subst A26[THEN sym], clarsimp simp: infinity_minus additive_infinity_right); lemma minus_infinity_less_iff: "(-∞ < x) = (x ≠ (-∞::'a::trans_reals) ∧ x ≠ Φ)"; by (auto dest: not_nullity_minus_infinity_le); lemma infinity_add_eq_nullity: "(∞ + x = Φ) = (x = - (∞ ::'a::trans_reals) ∨ x = Φ)"; apply (safe, simp_all add: A6[THEN sym]); apply (case_tac "x=∞", simp); apply (drule_tac f="λ a. a - x" in arg_cong); apply (erule_tac Q="?x = ?y" in contrapos_pp); apply (simp add: A1[THEN sym] A6); by(simp add: A6[THEN sym] A8); lemma infinity_minus_eq_nullity: "(x - ∞ = Φ) = (x = (∞ ::'a::trans_reals) ∨ x = Φ)"; apply (safe, simp_all add: A6[THEN sym]); apply (case_tac "x=-∞", simp); apply (drule_tac f="λ a. -x + a" in arg_cong); apply (erule_tac Q="?x = ?y" in contrapos_pp); by (simp add: A1 A6 uminus_x_add_x); lemma add_eq_nullity_iff: "(x + y = (Φ::'a::trans_reals)) = (x = Φ ∨ y = Φ ∨ (x=∞ ∧ y = - ∞) ∨ (x= - ∞ ∧ y = ∞))"; apply auto; apply (simp_all add: A6[THEN sym]); apply (drule_tac f="λ a. - x + a" in arg_cong); apply (erule_tac Q="?x = ?y" in contrapos_pp); apply (simp add: A1 uminus_x_add_x); apply (case_tac "x=∞", simp add: infinity_add_eq_nullity); apply (drule_tac f="λ a. - x + a" in arg_cong); apply (erule_tac Q="?x = ?y" in contrapos_pp); apply (simp add: A1 uminus_x_add_x); apply (case_tac "y=-∞", simp add: A6[THEN sym] infinity_minus_eq_nullity); apply (drule_tac f="λ a. a - y" in arg_cong); apply (erule_tac Q="?x = ?y" in contrapos_pp); apply (simp add: x_add_y_minus_y); apply (drule_tac f="λ a. a - y" in arg_cong); apply (erule_tac Q="?x = ?y" in contrapos_pp); by (simp add: x_add_y_minus_y); lemma minus_nullity_eq_iff: "(x - y = (Φ ::'a::trans_reals)) = (x = Φ ∨ y = Φ ∨ (x=∞ ∧ y = ∞) ∨ (x= - ∞ ∧ y = -∞))"; by (simp add: A6 add_eq_nullity_iff); lemma add_infinity: "x + (∞ ::'a::trans_reals) = (if x = Φ | x = -∞ then Φ else ∞)"; apply (case_tac "x=Φ", simp); apply (case_tac "x=-∞", subst A2, simp add: A6[THEN sym]); by (subst A2, simp add: A5); lemma add_infinity_not_eq[simp]: "(x ::'a::trans_reals) + ∞ ≠ 0 ∧ (x ::'a::trans_reals) + ∞ ≠ -∞"; by (simp add: add_infinity); lemma subtract_infinity: "x - (∞ ::'a::trans_reals) = (if x = Φ | x = ∞ then Φ else -∞)"; apply (case_tac "x=Φ", simp); apply (case_tac "x=∞", simp); by (simp add: A10); lemma subtract_infinity_not_eq[simp]: "(x ::'a::trans_reals) - ∞ ≠ 0 ∧ (x ::'a::trans_reals) - ∞ ≠ ∞"; by (simp add: subtract_infinity); lemma minus_nullD: "x - y = (0 ::'a::trans_reals) ==> x = y"; apply (case_tac "y = Φ", simp); apply (case_tac "y=∞", simp); apply (case_tac "y = -∞", simp); apply (drule_tac f="λ a. a + y" in arg_cong); apply (erule_tac Q="?x = ?y" in contrapos_pp); by (simp add: A6 A1[THEN sym] uminus_x_add_x); lemma add_cancel_right: "[| x + a = y + a; a ≠ Φ; a ≠ ∞; a ≠ -∞ |] ==> x = (y ::'a::trans_reals)"; apply (drule_tac f = "λ x. x - a" in arg_cong); by (simp add: x_add_y_minus_y); lemma add_cancel_left: "[| a + x = a + y; a ≠ Φ; a ≠ ∞; a ≠ -∞ |] ==> x = (y ::'a::trans_reals)"; apply (drule_tac f = "λ x. x - a" in arg_cong); apply (simp add: A6); apply (erule_tac Q="?a = ?b" in contrapos_pp); apply (subst add_commute); apply (subst add_commute [where a=a]); apply (simp add: add_assoc); by (simp add: A6[THEN sym] A8); lemma add_eq_infinity_iff: "(x + y = (∞::'a::trans_reals)) = ((x = ∞ ∧ y ≠ Φ ∧ y ≠ -∞) ∨ (y = ∞ ∧ x ≠ Φ ∧ x ≠ -∞))"; apply safe; apply (simp_all add: A6[THEN sym] A5 uminus_add_eq_minus); defer; apply (subst A2, simp add: A5); apply (case_tac "y=Φ", simp); apply (case_tac "y=-∞", simp add: A6[THEN sym]); apply (rule_tac a="y" in add_cancel_right); by (simp add: A5, assumption+); lemma add_eq_minus_infinity_iff: "(x + y = (-∞::'a::trans_reals)) = ((x = -∞ ∧ y ≠ Φ ∧ y ≠ ∞) ∨ (y = -∞ ∧ x ≠ Φ ∧ x ≠ ∞))"; apply safe; apply (simp_all add: A6[THEN sym] A10 uminus_add_eq_minus); defer; apply (erule contrapos_pp, subst A2, simp); apply (case_tac "y=Φ", simp); apply (case_tac "y=∞", simp add: A6[THEN sym]); apply (rule_tac a="y" in add_cancel_right); by (simp add: uminus_add_eq_minus A10, assumption+); lemma reals_add: "!! x::'a::trans_reals. [| x ≠ Φ; x ≠ ∞; x ≠ -∞; y ≠ Φ; y ≠ ∞; y ≠ -∞ |] ==> (x + y) ≠ Φ ∧ (x + y) ≠ ∞ ∧ (x + y) ≠ -∞ "; apply safe; apply (simp add: add_eq_nullity_iff); apply (simp add: add_eq_infinity_iff); by (simp add: add_eq_minus_infinity_iff); subsection {* Closure of reals under addition *} lemma reals_add_closed: "[| x ∈ reals; y ∈ reals |] ==> x + y ∈ reals"; by (unfold reals_def, simp add: reals_add); text {* Distributivity of uminus over addition *} lemma uminus_distrib_add: "-(x + y) = - x - (y ::'a::trans_reals)"; apply (case_tac "x=Φ", simp); apply (tactic "ALLGOALS(case_tac \"y=Φ\")", simp_all); apply (case_tac "x=∞", simp); apply (tactic "ALLGOALS(case_tac \"y=∞\")", simp_all); apply (tactic "ALLGOALS(case_tac \"x=-∞\")", simp_all); apply (tactic "ALLGOALS(case_tac \"y=-∞\")"); apply (simp_all add: A6[THEN sym] uminus_add_eq_minus infinity_minus A10); apply (simp add: A5, subst uminus_minus_commute); apply (simp add: A10); apply (subst A2, simp add: A5); apply (rule_tac a = "x" in add_cancel_left); apply (simp add: A6 A1); apply (simp add: A6[THEN sym] A8); apply (rule_tac a = "y" in add_cancel_left); apply (simp add: A6[THEN sym] A8); apply (simp add: A6); apply (subst A1[where a = y]); apply (simp add: A6[THEN sym]); apply (subst A2 [where a=y]); apply (rule A8); by (simp_all add: reals_add); lemma uminus_distrib_minus: "-(x - y) = - x + (y ::'a::trans_reals)"; by (simp add: A6 uminus_distrib_add); lemma ordering_opp: "(x - y < 0) = (x < (y::'a::trans_reals))"; apply (subst A26 [THEN sym]); apply (simp add: A6 uminus_distrib_add uminus_add_eq_minus); by (simp add: A26 A6[THEN sym]); text {* Trichotomy *} lemma trichotomy: "[| x ≠ Φ; y ≠ (Φ::'a::trans_reals) |] ==> (x < y) | (x = y) | (y < x)"; apply (cut_tac a="((x-y)::'a)" in A28, auto); apply (simp_all add: A26); apply (simp add: minus_nullity_eq_iff, safe); apply (erule minus_nullD); by (simp add: ordering_opp); lemma reals_uminus: "!! x::'a::trans_reals. [| x ≠ Φ; x ≠ ∞; x ≠ -∞ |] ==> -x ≠ Φ ∧ -x ≠ ∞ ∧ -x ≠ -∞ "; by (safe, simp_all); subsection{* Closure of reals under uminus *} lemma reals_uminus_closed: " x ∈ reals ==> -x ∈ reals"; by (unfold reals_def, simp add: reals_add); text{* Closure of positives transreals under addition *} lemma zero_less_add: "!! a ::'a::trans_reals. [| 0 < a; 0 < b |] ==> 0 < a + b"; apply (subst A23[THEN sym]); apply (subst A29, auto); apply (simp add: sgn_positive_iff[THEN iffD2]); by (simp add: A23[THEN iffD2]); lemma reals_interval: "reals = {x. -∞ < x ∧ x < ∞}"; by (auto simp: reals_def less_infinity_iff minus_infinity_less_iff); lemma reals_cases: "x ∈ reals ==> (x < 0) | x = 0 | (0 < x)"; apply (unfold reals_def, clarsimp); by (cut_tac A28 [where a="x"], simp); lemma not_infinity_less[simp]: "¬ (∞ < (x::'a::trans_reals))"; by (subst A26[THEN sym], simp add: subtract_infinity); lemma not_less_minus_infinity[simp]: "¬ ((x::'a::trans_reals) < -∞)"; apply (subst A26[THEN sym]); apply (subst uminus_minus_commute); by (simp add: subtract_infinity); text {* Left distributivy of multiplication over addition *} lemma distrib_left: "¬ ((c = ∞ ∨ c = - ∞) ∧ sgn a ≠ sgn b ∧ (a + b ∉ {0,Φ})) ==> (a+b) * c = (a * c)+(b * (c::'a::trans_reals))"; apply (subst A13[where a="a+b"]); apply (subst A13[where a="a"]); apply (subst A13[where a="b"]); by (simp add: A29); lemma zero_mult_not_less_zero:"¬ ((0::'a::trans_reals) * x < 0)"; by (simp add: A24[THEN sym] A12); lemma not_zero_less_zero_mult:"¬ (0 < (0::'a::trans_reals) * x)"; by (simp add: A23[THEN sym] A12); lemma zero_mult_eq_zero_or_nullity: "(0::'a::trans_reals) * x = 0 ∨ 0 * x = Φ"; apply (cut_tac A28 [where a="0 * x"]); by (auto simp: zero_mult_not_less_zero not_zero_less_zero_mult); lemma zero_mult_minus_one: "(0::'a::trans_reals) * - 1 = 0"; apply (cut_tac zero_mult_eq_zero_or_nullity [where x="- 1::'a"], clarsimp); apply (drule_tac f ="λ x. x + 0 * (1 + 1)" in arg_cong); by (simp add: A29[THEN sym] A1 uminus_add_eq_minus A8); lemma zero_mult_zero: "(0::'a::trans_reals) * 0 = 0"; apply (subgoal_tac "(0::'a::trans_reals) * (1 + - 1) = 0"); apply (simp add: A6 [THEN sym]); by (simp add: A29 zero_mult_minus_one); text {* Multiplicative inverse *} lemma mult_inverse: "[| a ≠ 0; a: reals |] ==> a * inverse a = (1::'a::trans_reals)"; by (unfold reals_def, clarsimp, drule A18, assumption+, simp add: A17); lemma zero_mult_real_not_zero: "[| (x::'a::trans_reals): reals; x ≠ 0 |] ==> 0 * x = 0"; apply (cut_tac zero_mult_eq_zero_or_nullity [where x="x"], safe); apply (drule_tac f="λ y. y * inverse x" in arg_cong); by (simp add: A12 [THEN sym] mult_inverse); text {* Multiplication with zero *} lemma zero_mult_reals: "x : reals ==> 0 * x = (0::'a::trans_reals) ∧ x * 0 = 0"; apply (rule context_conjI); apply (case_tac "x=0"); apply (simp add: zero_mult_zero); apply (erule zero_mult_real_not_zero, assumption); by (subst A13, assumption); lemmas zero_mult = zero_mult_reals [unfolded reals_def, simplified]; lemma mult_zero: "x ≠ Φ ∧ x ≠ ∞ ∧ x ≠ - ∞ ==> x * (0::'a::trans_reals) = 0"; apply (rule trans); defer; apply (rule zero_mult [THEN conjunct1], assumption); by (rule A13); text {* Multiplication with -1 *} lemma minus_one_mult_uminus_reals: "x : reals ==> (- 1 ::'a::trans_reals) * x = -x"; apply (rule_tac a="x" in add_cancel_right, unfold reals_def, safe); apply (simp add: uminus_add_eq_minus A8); apply (subst A14[where a="x", THEN sym]); back; apply (subst A13); apply (subst A13); back; apply (subst A29[THEN sym]); apply simp; by (simp add: uminus_add_eq_minus A8 mult_zero); lemma minus_one_mult_minus_one[simp]: "(- 1 ::'a::trans_reals) * - 1 = 1"; by (simp add: minus_one_mult_uminus_reals reals_def); lemma minus_one_mult_uminus: "(- 1 ::'a::trans_reals) * x = -x"; apply (case_tac "x=Φ", simp add: A13); apply (case_tac "x=∞", simp); apply (case_tac "x=-∞", clarsimp); apply (subst minus_one_mult_infinity[THEN sym]); apply (subst A12); apply (subst minus_one_mult_minus_one, simp); apply (rule minus_one_mult_uminus_reals); by (simp add: reals_def); lemma minus_one_mult_minus_infinity[simp]: "(- 1 ::'a::trans_reals) * - ∞ = ∞"; by (simp add: minus_one_mult_uminus); lemma mult_nullity_right[simp]: "(x::'a::trans_reals) * Φ = Φ"; by (subst A13, rule A15); lemma zero_mult_minus_infinity[simp]: "(0::'a::trans_reals) * - ∞ = Φ"; apply (subst minus_one_mult_infinity[THEN sym]); apply (subst A12); by (simp add: zero_mult); lemma minus_infinity_mult_zero[simp]: "- ∞ * (0::'a::trans_reals) = Φ"; by (subst A13, rule zero_mult_minus_infinity); lemma uminus_mult_left: "-((x::'a::trans_reals) * y) = (- x) * y"; apply (subst minus_one_mult_uminus[THEN sym]); apply (subst A12); by (simp add: minus_one_mult_uminus); lemma uminus_mult_right: "-((x::'a::trans_reals) * y) = x * (- y)"; apply (subst minus_one_mult_uminus[THEN sym]); apply (subst A13); apply (subst A12 [THEN sym]); apply (subst A13 [where a="y"]); by (simp add: minus_one_mult_uminus); lemma uminus_mult_uminus [simp]: "-(x::'a::trans_reals) * (- y) = x * y"; apply (subst uminus_mult_left[THEN sym]); by (simp add: uminus_mult_right); lemma zero_less_uminus_iff_less_zero: "(0 < - x) = ((x::'a::trans_reals) < 0)"; apply (simp add: A23[THEN sym] A24[THEN sym], auto); apply (drule_tac f ="λ x. -x" in arg_cong); apply (simp add: uminus_mult_right); apply (drule_tac f ="λ x. -x" in arg_cong); by (simp add: uminus_mult_right); lemma uminus_less_zero_iff_zero_less: "(-x < 0) = (0 < (x::'a::trans_reals))"; apply (simp add: A23[THEN sym] A24[THEN sym], auto); apply (drule_tac f ="λ x. -x" in arg_cong); apply (simp add: uminus_mult_right); apply (drule_tac f ="λ x. -x" in arg_cong); by (simp add: uminus_mult_right); lemma less_not_sym: "(x::'a::trans_reals) < y ==> ¬ (y < x)"; apply (rule notI, drule A26[THEN iffD2], drule A26[THEN iffD2]); apply (drule uminus_less_zero_iff_zero_less[THEN iffD2]); apply (simp add: uminus_distrib_minus uminus_add_eq_minus); by (erule not_less_zero_and_zero_less, assumption); text{* Closure of positive transreals under multiplication *} lemma mult_gt_zero_gt_zero: "!! a ::'a::trans_reals. [| 0 < a; 0 < b |] ==> 0 < a * b"; apply (subst A23[THEN sym]); apply (subst A12); apply (subst A23[THEN iffD2], assumption); by (erule A23[THEN iffD2]); text{* Mixed-sign multiplication *} lemma mult_gt_zero_less_zero: "!! a::'a::trans_reals. [| 0 < a; b < 0 |] ==> a * b < 0"; apply (subst A24[THEN sym]); apply (subst A12); apply (subst A23[THEN iffD2], assumption); by (erule A24[THEN iffD2]); lemma mult_less_zero_gt_zero: "!! a::'a::trans_reals. [| a < 0; 0 < b |] ==> a * b < 0"; by (subst A13, erule mult_gt_zero_less_zero, assumption); text{* Multiplication of two negative transreals *} lemma mult_less_zero_less_zero: "!! a::'a::trans_reals. [| a < 0; b < 0 |] ==> 0 < a * b"; apply (subst A23[THEN sym]); apply (subst A12); apply (subst A24[THEN iffD2], assumption); apply (subst minus_one_mult_infinity [THEN sym]); apply (subst A12[THEN sym]); by (subst A24 [THEN iffD2], auto); lemma infinity_mult: "∞ * (x::'a::trans_reals) = (if x < 0 then -∞ else if 0 < x then ∞ else Φ)"; apply (auto simp add: A23 A24); by (cut_tac A28 [where a="x"], auto); lemma mult_infinity: "(x::'a::trans_reals) * ∞ = (if x < 0 then -∞ else if 0 < x then ∞ else Φ)"; by (subst A13, rule infinity_mult); lemma minus_infinity_mult: "-∞ * (x::'a::trans_reals) = (if x < 0 then ∞ else if 0 < x then -∞ else Φ)"; apply (subst minus_one_mult_infinity[THEN sym]); apply (subst A12 [THEN sym]); apply (subst infinity_mult); by (auto simp: minus_one_mult_uminus); lemma mult_minus_infinity: "(x::'a::trans_reals) * -∞= (if x < 0 then ∞ else if 0 < x then -∞ else Φ)"; by (subst A13, rule minus_infinity_mult); text{* Some inverse rules *} lemma inverse_infinity[simp]: "inverse (∞) = (0 ::'a::trans_reals)"; apply (subst A20[THEN sym]); apply (rule A19); by (cut_tac a="(∞::'a)" in A28, auto); lemma inverse_nullity_iff: "!! x::'a::trans_reals. (inverse x = Φ) = (x = Φ)"; apply (safe, simp_all); apply (frule_tac f="inverse" in arg_cong); apply (case_tac "x=-∞", simp); by (thin_tac "inverse x = Φ", simp add: A19); lemma inverse_noteq_zero: "!! x::'a::trans_reals. [| x ≠ ∞; x ≠ -∞ |] ==> inverse x ≠ 0"; apply (case_tac "x=Φ", simp); apply (subst inverse_infinity[THEN sym]); apply (rule notI); by (drule_tac f="inverse" in arg_cong, simp add: A19); lemma inverse_zero_iff[simp]: "!! x::'a::trans_reals. (inverse x = 0) = (x = ∞ | x = -∞)"; by (auto, rule classical, cut_tac x="x" in inverse_noteq_zero, auto); lemma inverse_infinity_iff[simp]: "!! x::'a::trans_reals. (inverse x = ∞) = (x = 0)"; apply (case_tac "x=Φ", simp); apply (case_tac "x=∞", simp); apply (case_tac "x=-∞", simp); apply (case_tac "x=0", auto); apply (drule_tac f= "λ a. x * a" in arg_cong); apply (simp add: mult_inverse reals_def mult_infinity); apply (case_tac "x < 0", simp); by (case_tac "0 < x", simp_all); lemma inverse_minus_infinity_iff[simp]: "!! x::'a::trans_reals. (inverse x ≠ -∞)"; apply (case_tac "x=Φ", simp); apply (case_tac "x=∞", simp); apply (case_tac "x=-∞", simp); apply (case_tac "x=0", auto); apply (drule_tac f= "λ a. x * a" in arg_cong); apply (simp add: mult_inverse reals_def mult_minus_infinity); apply (case_tac "x < 0", simp); by (case_tac "0 < x", simp_all); subsection{* Closure of positive reals under inverse *} lemma zero_less_inverse: "!! x ::'a::trans_reals. [| 0 < x; x ≠ ∞ |] ==> 0 < inverse x" apply (case_tac "x=Φ", simp); apply (case_tac "x=0", simp); apply (case_tac "x=-∞", simp); apply (cut_tac a="x" in A18, assumption+); apply (simp add: A17); apply (subgoal_tac "inverse x ≠ Φ"); defer; apply (simp add: inverse_nullity_iff); apply (drule_tac trichotomy[where y = "0"]); back; apply (auto); by (drule_tac mult_gt_zero_less_zero, assumption, simp); lemma inverse_less_zero: "[| (x::'a::trans_reals) < 0; x ≠ -∞ |] ==> inverse x < 0" apply (case_tac "x=Φ", simp); apply (case_tac "x=0", simp); apply (case_tac "x=∞", simp); apply (cut_tac a="x" in A18, assumption+); apply (simp add: A17); apply (subgoal_tac "inverse x ≠ Φ"); defer; apply (simp add: inverse_nullity_iff); apply (cut_tac reals_cases [where x = "inverse x"],auto); apply (drule_tac mult_less_zero_gt_zero, assumption, simp); by (auto simp: reals_def); lemma inverse_less_zero_iff[simp]: "(x::'a::trans_reals) ≠ -∞ ==> (inverse x < 0) = (x < 0)" apply (rule iffI); apply (drule_tac inverse_less_zero, simp); apply (simp add: A19); by (erule inverse_less_zero, assumption); lemma zero_less_inverse_iff[simp]: "[| (x::'a::trans_reals) ≠ ∞; x ≠ 0 |] ==> (0 < inverse x) = (0 < x)"; apply (case_tac "x=-∞", simp); apply (rule iffI); apply (drule_tac zero_less_inverse, simp); apply (simp add: A19); by (erule zero_less_inverse, assumption); lemma less_not_nullity: "(x::'a::trans_reals) < y ==> x ≠ Φ ∧ y ≠ Φ ∧ x ≠ ∞ ∧ y ≠ -∞"; by (auto); subsection{* Closure of reals under multiplication *} lemma reals_mult_closed: "[| x : reals; y : reals |] ==> x * y : reals"; apply (frule_tac x="x" in reals_cases, frule_tac x="y" in reals_cases, safe); apply (simp_all add: zero_mult_reals); (* case <,< *) apply (frule mult_less_zero_less_zero, assumption); back; apply (subst reals_def, clarsimp simp: less_not_nullity); apply (drule_tac f = "λ a. a * inverse y" in arg_cong); apply (simp add: A12 [THEN sym] mult_inverse less_zero_imp_not_zero infinity_mult reals_def); (* case <,> *) apply (frule mult_less_zero_gt_zero, assumption); apply (subst reals_def, clarsimp simp: less_not_nullity); apply (drule_tac f = "λ a. a * inverse y" in arg_cong); apply (frule_tac y="y" in less_not_sym); apply (simp add: A12 [THEN sym] mult_inverse zero_less_imp_not_zero minus_infinity_mult reals_def); (* case >,< *) apply (frule mult_gt_zero_less_zero, assumption); apply (subst reals_def, clarsimp simp: less_not_nullity); apply (drule_tac f = "λ a. a * inverse y" in arg_cong); apply (simp add: A12 [THEN sym] mult_inverse less_zero_imp_not_zero minus_infinity_mult reals_def); (* case >,> *) apply (frule mult_gt_zero_gt_zero, assumption); back; apply (subst reals_def, clarsimp simp: less_not_nullity); apply (drule_tac f = "λ a. a * inverse y" in arg_cong); apply (frule_tac y="y" in less_not_sym); by (simp add: A12 [THEN sym] mult_inverse zero_less_imp_not_zero infinity_mult reals_def); end
lemma additive_identity_right:
x + (0::'a) = x
lemma multiplicative_identity_right:
x * (1::'a) = x
lemma additive_nullity_right:
x + Φ = Φ
lemma additive_infinity_right:
[| x ≠ - ∞; x ≠ Φ |] ==> x + ∞ = ∞
lemma minus_minus:
x - - y = x + y
lemma zero_mult_infinity:
(0::'a) * ∞ = Φ
lemma nullity_minus_left:
Φ - x = Φ
lemma nullity_minus_right:
x - Φ = Φ
lemma zero_minus_eq_uminus:
(0::'a) - x = - x
lemma uminus_eq_uminus:
(- x = - y) = (x = y)
lemma uminus_add_eq_minus:
- x + y = y - x
lemma uminus_minus_commute:
- x - y = - y - x
lemma x_add_y_minus_y:
[| y ≠ Φ; y ≠ ∞; y ≠ - ∞ |] ==> x + y - y = x
lemma uminus_x_add_x:
[| x ≠ ∞; x ≠ - ∞; x ≠ Φ |] ==> - x + x = (0::'a)
lemma x_minus_y_add_y:
[| y ≠ Φ; y ≠ ∞; y ≠ - ∞ |] ==> x - y + y = x
lemma uminus_eq_nullity_iff:
(- x = Φ) = (x = Φ)
lemma uminus_eq_infinity_iff:
(- x = ∞) = (x = - ∞)
lemma infinity_minus:
[| x ≠ Φ; x ≠ ∞ |] ==> ∞ - x = ∞
lemma not_zero_less_zero:
¬ (0::'a) < (0::'a)
lemma zero_noteq_nullity:
(0::'a) ≠ Φ
lemmas nullity_noteq_zero:
Φ ≠ (0::'a1)
lemmas nullity_noteq_zero:
Φ ≠ (0::'a1)
lemma zero_noteq_infinity:
(0::'a) ≠ ∞
lemmas infinity_noteq_zero:
∞ ≠ (0::'a1)
lemmas infinity_noteq_zero:
∞ ≠ (0::'a1)
lemma nullity_not_less_zero:
¬ Φ < (0::'a)
lemma zero_not_less_nullity:
¬ (0::'a) < Φ
lemma infinity_noteq_nullity:
∞ ≠ Φ
lemmas nullity_noteq_infinity:
Φ ≠ ∞
lemmas nullity_noteq_infinity:
Φ ≠ ∞
lemma zero_less_one:
(0::'a) < (1::'a)
lemma not_one_less_zero:
¬ (1::'a) < (0::'a)
lemma zero_noteq_one:
(0::'a) ≠ (1::'a)
lemmas one_noteq_zero:
(1::'a1) ≠ (0::'a1)
lemmas one_noteq_zero:
(1::'a1) ≠ (0::'a1)
lemma one_noteq_infinity:
(1::'a) ≠ ∞
lemmas infinity_noteq_one:
∞ ≠ (1::'a1)
lemmas infinity_noteq_one:
∞ ≠ (1::'a1)
lemma nullity_noteq_one:
Φ ≠ (1::'a)
lemmas one_not_nullity:
(1::'a1) ≠ Φ
lemmas one_not_nullity:
(1::'a1) ≠ Φ
lemma minus_one_less_zero:
- (1::'a) < (0::'a)
lemma minus_one_mult_infinity:
- (1::'a) * ∞ = - ∞
lemma zero_noteq_minus_one:
(0::'a) ≠ - (1::'a)
lemmas minus_one_noteq_zero:
- (1::'a1) ≠ (0::'a1)
lemmas minus_one_noteq_zero:
- (1::'a1) ≠ (0::'a1)
lemma not_one_less_minus_one:
¬ (0::'a) < - (1::'a)
lemma one_noteq_minus_one:
(1::'a) ≠ - (1::'a)
lemmas minus_one_noteq_one:
- (1::'a1) ≠ (1::'a1)
lemmas minus_one_noteq_one:
- (1::'a1) ≠ (1::'a1)
lemma infinity_noteq_minus_one:
∞ ≠ - (1::'a)
lemmas minus_one_not_infinity:
- (1::'a1) ≠ ∞
lemmas minus_one_not_infinity:
- (1::'a1) ≠ ∞
lemma nullity_noteq_minus_one:
Φ ≠ - (1::'a)
lemmas minus_one_not_nullity:
- (1::'a1) ≠ Φ
lemmas minus_one_not_nullity:
- (1::'a1) ≠ Φ
lemma zero_noteq_minus_infinity:
(0::'a) ≠ - ∞
lemmas minus_infinity_noteq_zero:
- ∞ ≠ (0::'a1)
lemmas minus_infinity_noteq_zero:
- ∞ ≠ (0::'a1)
lemma uminus_zero:
- (0::'a) = (0::'a)
lemma uminus_eq_zero_iff:
(- x = (0::'a)) = (x = (0::'a))
lemma minus_infinity_less_zero:
- ∞ < (0::'a)
lemma minus_infinity_mult_infinity:
- ∞ * ∞ = - ∞
lemma not_zero_less_minus_infinity:
¬ (0::'a) < - ∞
lemma one_noteq_minus_infinity:
(1::'a) ≠ - ∞
lemmas minus_infinity_noteq_one:
- ∞ ≠ (1::'a1)
lemmas minus_infinity_noteq_one:
- ∞ ≠ (1::'a1)
lemma infinity_noteq_minus_infinity:
∞ ≠ - ∞
lemmas minus_infinity_noteq_infinity:
- ∞ ≠ ∞
lemmas minus_infinity_noteq_infinity:
- ∞ ≠ ∞
lemma nullity_noteq_minus_infinity:
Φ ≠ - ∞
lemmas minus_infinity_noteq_nullity:
- ∞ ≠ Φ
lemmas minus_infinity_noteq_nullity:
- ∞ ≠ Φ
lemma one_minus_one_eq_zero:
(1::'a) - (1::'a) = (0::'a)
lemma less_irreflexive:
¬ x < x
lemma not_less_zero_and_zero_less:
[| x < (0::'a); (0::'a) < x |] ==> P
lemma less_zero_imp_not_zero:
x < (0::'a) ==> x ≠ (0::'a)
lemma zero_less_imp_not_zero:
(0::'a) < x ==> x ≠ (0::'a)
lemma sgn_negative_iff:
(sgn a = - (1::'a)) = (a < (0::'a))
lemma sgn_positive_iff:
(sgn a = (1::'a)) = ((0::'a) < a)
lemma sgn_zero:
sgn (0::'a) = (0::'a)
lemma sgn_zero_iff:
(sgn x = (0::'a)) = (x = (0::'a))
lemma sgn_nullity:
sgn Φ = Φ
lemma sgn_nullity_iff:
(sgn x = Φ) = (x = Φ)
lemma infinity_add_infinity:
∞ + ∞ = ∞
lemma minus_infinity_minus_infinity:
- ∞ - ∞ = - ∞
lemma minus_infinity_add_infinity:
- ∞ + ∞ = Φ
lemma not_nullity_less:
¬ Φ < x
lemma not_less_nullity:
¬ x < Φ
lemma not_nullity_le_infinity:
x ≠ Φ ==> x < ∞ ∨ x = ∞
lemma less_infinity_iff:
(x < ∞) = (x ≠ ∞ ∧ x ≠ Φ)
lemma not_nullity_minus_infinity_le:
x ≠ Φ ==> - ∞ < x ∨ x = - ∞
lemma minus_infinity_less_iff:
(- ∞ < x) = (x ≠ - ∞ ∧ x ≠ Φ)
lemma infinity_add_eq_nullity:
(∞ + x = Φ) = (x = - ∞ ∨ x = Φ)
lemma infinity_minus_eq_nullity:
(x - ∞ = Φ) = (x = ∞ ∨ x = Φ)
lemma add_eq_nullity_iff:
(x + y = Φ) = (x = Φ ∨ y = Φ ∨ x = ∞ ∧ y = - ∞ ∨ x = - ∞ ∧ y = ∞)
lemma minus_nullity_eq_iff:
(x - y = Φ) = (x = Φ ∨ y = Φ ∨ x = ∞ ∧ y = ∞ ∨ x = - ∞ ∧ y = - ∞)
lemma add_infinity:
x + ∞ = (if x = Φ ∨ x = - ∞ then Φ else ∞)
lemma add_infinity_not_eq:
x + ∞ ≠ (0::'a) ∧ x + ∞ ≠ - ∞
lemma subtract_infinity:
x - ∞ = (if x = Φ ∨ x = ∞ then Φ else - ∞)
lemma subtract_infinity_not_eq:
x - ∞ ≠ (0::'a) ∧ x - ∞ ≠ ∞
lemma minus_nullD:
x - y = (0::'a) ==> x = y
lemma add_cancel_right:
[| x + a = y + a; a ≠ Φ; a ≠ ∞; a ≠ - ∞ |] ==> x = y
lemma add_cancel_left:
[| a + x = a + y; a ≠ Φ; a ≠ ∞; a ≠ - ∞ |] ==> x = y
lemma add_eq_infinity_iff:
(x + y = ∞) = (x = ∞ ∧ y ≠ Φ ∧ y ≠ - ∞ ∨ y = ∞ ∧ x ≠ Φ ∧ x ≠ - ∞)
lemma add_eq_minus_infinity_iff:
(x + y = - ∞) = (x = - ∞ ∧ y ≠ Φ ∧ y ≠ ∞ ∨ y = - ∞ ∧ x ≠ Φ ∧ x ≠ ∞)
lemma reals_add:
[| x ≠ Φ; x ≠ ∞; x ≠ - ∞; y ≠ Φ; y ≠ ∞; y ≠ - ∞ |] ==> x + y ≠ Φ ∧ x + y ≠ ∞ ∧ x + y ≠ - ∞
lemma reals_add_closed:
[| x ∈ reals; y ∈ reals |] ==> x + y ∈ reals
lemma uminus_distrib_add:
- (x + y) = - x - y
lemma uminus_distrib_minus:
- (x - y) = - x + y
lemma ordering_opp:
(x - y < (0::'a)) = (x < y)
lemma trichotomy:
[| x ≠ Φ; y ≠ Φ |] ==> x < y ∨ x = y ∨ y < x
lemma reals_uminus:
[| x ≠ Φ; x ≠ ∞; x ≠ - ∞ |] ==> - x ≠ Φ ∧ - x ≠ ∞ ∧ - x ≠ - ∞
lemma reals_uminus_closed:
x ∈ reals ==> - x ∈ reals
lemma zero_less_add:
[| (0::'a) < a; (0::'a) < b |] ==> (0::'a) < a + b
lemma reals_interval:
reals = {x. - ∞ < x ∧ x < ∞}
lemma reals_cases:
x ∈ reals ==> x < (0::'a) ∨ x = (0::'a) ∨ (0::'a) < x
lemma not_infinity_less:
¬ ∞ < x
lemma not_less_minus_infinity:
¬ x < - ∞
lemma distrib_left:
¬ ((c = ∞ ∨ c = - ∞) ∧ sgn a ≠ sgn b ∧ a + b ∉ {0::'a, Φ}) ==> (a + b) * c = a * c + b * c
lemma zero_mult_not_less_zero:
¬ (0::'a) * x < (0::'a)
lemma not_zero_less_zero_mult:
¬ (0::'a) < (0::'a) * x
lemma zero_mult_eq_zero_or_nullity:
(0::'a) * x = (0::'a) ∨ (0::'a) * x = Φ
lemma zero_mult_minus_one:
(0::'a) * - (1::'a) = (0::'a)
lemma zero_mult_zero:
(0::'a) * (0::'a) = (0::'a)
lemma mult_inverse:
[| a ≠ (0::'a); a ∈ reals |] ==> a * inverse a = (1::'a)
lemma zero_mult_real_not_zero:
[| x ∈ reals; x ≠ (0::'a) |] ==> (0::'a) * x = (0::'a)
lemma zero_mult_reals:
x ∈ reals ==> (0::'a) * x = (0::'a) ∧ x * (0::'a) = (0::'a)
lemmas zero_mult:
x ≠ Φ ∧ x ≠ ∞ ∧ x ≠ - ∞ ==> (0::'a) * x = (0::'a) ∧ x * (0::'a) = (0::'a)
lemmas zero_mult:
x ≠ Φ ∧ x ≠ ∞ ∧ x ≠ - ∞ ==> (0::'a) * x = (0::'a) ∧ x * (0::'a) = (0::'a)
lemma mult_zero:
x ≠ Φ ∧ x ≠ ∞ ∧ x ≠ - ∞ ==> x * (0::'a) = (0::'a)
lemma minus_one_mult_uminus_reals:
x ∈ reals ==> - (1::'a) * x = - x
lemma minus_one_mult_minus_one:
- (1::'a) * - (1::'a) = (1::'a)
lemma minus_one_mult_uminus:
- (1::'a) * x = - x
lemma minus_one_mult_minus_infinity:
- (1::'a) * - ∞ = ∞
lemma mult_nullity_right:
x * Φ = Φ
lemma zero_mult_minus_infinity:
(0::'a) * - ∞ = Φ
lemma minus_infinity_mult_zero:
- ∞ * (0::'a) = Φ
lemma uminus_mult_left:
- (x * y) = - x * y
lemma uminus_mult_right:
- (x * y) = x * - y
lemma uminus_mult_uminus:
- x * - y = x * y
lemma zero_less_uminus_iff_less_zero:
((0::'a) < - x) = (x < (0::'a))
lemma uminus_less_zero_iff_zero_less:
(- x < (0::'a)) = ((0::'a) < x)
lemma less_not_sym:
x < y ==> ¬ y < x
lemma mult_gt_zero_gt_zero:
[| (0::'a) < a; (0::'a) < b |] ==> (0::'a) < a * b
lemma mult_gt_zero_less_zero:
[| (0::'a) < a; b < (0::'a) |] ==> a * b < (0::'a)
lemma mult_less_zero_gt_zero:
[| a < (0::'a); (0::'a) < b |] ==> a * b < (0::'a)
lemma mult_less_zero_less_zero:
[| a < (0::'a); b < (0::'a) |] ==> (0::'a) < a * b
lemma infinity_mult:
∞ * x = (if x < (0::'a) then - ∞ else if (0::'a) < x then ∞ else Φ)
lemma mult_infinity:
x * ∞ = (if x < (0::'a) then - ∞ else if (0::'a) < x then ∞ else Φ)
lemma minus_infinity_mult:
- ∞ * x = (if x < (0::'a) then ∞ else if (0::'a) < x then - ∞ else Φ)
lemma mult_minus_infinity:
x * - ∞ = (if x < (0::'a) then ∞ else if (0::'a) < x then - ∞ else Φ)
lemma inverse_infinity:
inverse (∞) = (0::'a)
lemma inverse_nullity_iff:
(inverse x = Φ) = (x = Φ)
lemma inverse_noteq_zero:
[| x ≠ ∞; x ≠ - ∞ |] ==> inverse x ≠ (0::'a)
lemma inverse_zero_iff:
(inverse x = (0::'a)) = (x = ∞ ∨ x = - ∞)
lemma inverse_infinity_iff:
(inverse x = ∞) = (x = (0::'a))
lemma inverse_minus_infinity_iff:
inverse x ≠ - ∞
lemma zero_less_inverse:
[| (0::'a) < x; x ≠ ∞ |] ==> (0::'a) < inverse x
lemma inverse_less_zero:
[| x < (0::'a); x ≠ - ∞ |] ==> inverse x < (0::'a)
lemma inverse_less_zero_iff:
x ≠ - ∞ ==> (inverse x < (0::'a)) = (x < (0::'a))
lemma zero_less_inverse_iff:
[| x ≠ ∞; x ≠ (0::'a) |] ==> ((0::'a) < inverse x) = ((0::'a) < x)
lemma less_not_nullity:
x < y ==> x ≠ Φ ∧ y ≠ Φ ∧ x ≠ ∞ ∧ y ≠ - ∞
lemma reals_mult_closed:
[| x ∈ reals; y ∈ reals |] ==> x * y ∈ reals