# Theory RingLib

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory RingLib = Main:

```(*  Title:      RingLib.thy
Including some theorems by Kevin Donnelly
*)

theory RingLib = Main:;

subsection {* Misc theorems for rings and ordered rings *}

lemma abs_nonneg [simp]: "0 ≤ (x::'a::ordered_ring) ==> abs x = x";

lemma abs_nonpos [simp]: "(x::'a::ordered_field) <= 0 ==> abs x = -x";
apply (simp only: abs_if);
apply (subgoal_tac "x < 0 | x = 0");
apply auto;
done;

lemma nonneg_times_nonneg: "0 <= (x::'a::ordered_ring) ==> 0 <= y ==>
0 <= x * y";
proof -;
assume "0 <= (x::'a)" and "0 <= (y::'a)";
then have "0 * 0 <= x * y";
by (rule mult_mono, auto);
thus ?thesis;
by simp;
qed;

lemma abs_pos [simp]: "0 < (x::'a::ordered_ring) ==> abs x = x";

lemma abs_neg [simp]: "(x::'a::ordered_field) < 0 ==> abs x = -x";
apply (simp only: abs_if);
apply (subgoal_tac "x < 0 | x = 0");
apply auto;
done;

lemma pos_plus_pos: "0 < (x::'a::ordered_semiring) ==> 0 < y ==> 0 < x + y";
apply (subgoal_tac "0 + 0 < x + y");
apply simp;
apply (assumption)+;
done;

lemma nonneg_times_nonneg: "0 ≤ (x::'a::ordered_semiring) ==> 0 ≤ y ==>
0 ≤ x * y";
apply (subgoal_tac "0 * 0 ≤ x * y");
apply simp;
apply (subgoal_tac "0 * 0 ≤ 0 * y");
apply (subgoal_tac "0 * y ≤ x * y");
apply force;
apply (erule mult_right_mono, assumption);
apply (erule mult_left_mono);
apply simp;
done;

lemma nonneg_plus_nonneg: "0 ≤ (x::'a::ordered_semiring) ==> 0 ≤ y ==>
0 ≤ x + y";
apply (subgoal_tac "0 + 0 ≤ x + y");
apply simp;
done;

theorem ring_less_mult_cancel_left: "0 < a ==>
(a * b < a * c) = (b < (c::'a::ordered_ring))";
apply(auto);
apply(case_tac "b < c");
apply(subgoal_tac "a * c <= a * b");
apply(subgoal_tac "~ a * c <= a * b");
apply(simp);
apply(subst linorder_not_le);
apply(simp);

lemma abs_times_pos: "(0::'a::ordered_ring) <= x ==>
(abs y) * x = abs (y * x)";
apply (subst abs_mult);
apply simp;
done;

lemma abs_div: "y ~= 0 ==> abs (x::'a::ordered_field) / abs y = abs(x / y)";
apply (subst nonzero_divide_eq_eq);
apply simp;
apply (subst abs_mult [THEN sym]);
apply (subst times_divide_eq_left);
apply (subst times_divide_eq_right [THEN sym]);
apply simp;
done;

lemma abs_div_pos: "(0::'a::ordered_field) < y ==> abs x / y = abs (x / y)";
apply (subst abs_div [THEN sym]);
apply simp;
apply (subst abs_nonneg);
apply simp_all;
done;

lemma abs_diff: "abs ((a::'a::ordered_ring) - b) = abs(b - a)";
apply (subst abs_minus_cancel [THEN sym]);
apply simp;
done;

lemma add_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
x / y + w / z = (x * z + w * y) / (y * z)";
apply (subgoal_tac "x / y = (x * z) / (y * z)");
apply (erule ssubst);
apply (subgoal_tac "w / z = (w * y) / (y * z)");
apply (erule ssubst);
apply (subst mult_commute);
apply (erule nonzero_mult_divide_cancel_right [THEN sym]);
apply assumption;
apply (erule nonzero_mult_divide_cancel_right [THEN sym]);
apply assumption;
done;

lemma diff_frac_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
x / y - w / z = (x * z - w * y) / (y * z)";
apply (subgoal_tac "x / y = (x * z) / (y * z)");
apply (erule ssubst);
apply (subgoal_tac "w / z = (w * y) / (y * z)");
apply (erule ssubst);
apply (rule diff_divide_distrib [THEN sym]);
apply (subst mult_commute);
apply (erule nonzero_mult_divide_cancel_right [THEN sym]);
apply assumption;
apply (erule nonzero_mult_divide_cancel_right [THEN sym]);
apply assumption;
done;

lemma frac_eq_eq: "(y::'a::field) ~= 0 ==> z ~= 0 ==>
(x / y = w / z) = (x * z = w * y)";
apply (subst nonzero_eq_divide_eq);
apply assumption;
apply (subst times_divide_eq_left);
apply (erule nonzero_divide_eq_eq);
done;

lemma abs_triangle_ineq2: "abs (a::'a::ordered_ring) - abs b <= abs (a - b)";
apply (subgoal_tac "abs a = abs (a - b + b)");
apply (erule ssubst);
apply (rule abs_triangle_ineq);
apply simp;
done;

lemma abs_triangle_ineq3:
"abs(abs (a::'a::ordered_ring) - abs b) <= abs (a - b)";
apply (subst abs_le_iff);
apply auto;
apply (rule abs_triangle_ineq2);
apply (subst abs_minus_cancel [THEN sym]);
apply simp;
apply (rule abs_triangle_ineq2);
done;

lemma abs_triangle_ineq4: "abs ((a::'a::ordered_ring) - b) <= abs a + abs b";
proof -;
have "abs(a - b) = abs(a + - b)";
by (subst diff_minus, rule refl);
also have "... <= abs a + abs (- b)";
by (rule abs_triangle_ineq);
finally show ?thesis;
by simp;
qed;

lemma pos_div_pos: "0 < (x::'a::ordered_field) ==> 0 < y ==> 0 < x / y";
apply (subst pos_less_divide_eq);
apply assumption;
apply simp;
done;

lemma setsum_le_cong2 [rule_format]: "finite B ==> A <= B ==>
ALL x: B - A. 0 <= ((f x)::'a::ordered_semiring) ==>
setsum f A <= setsum f B";
apply (subgoal_tac "setsum f B = setsum f A + setsum f (B - A)");
apply (erule ssubst);
apply (subgoal_tac "setsum f A + 0 <= setsum f A + setsum f (B - A)");
apply simp;
apply (rule setsum_nonneg);
apply (rule finite_subset);
prefer 2;
apply assumption;
apply force;
apply assumption;
apply (subst setsum_Un_disjoint [THEN sym]);
apply (erule finite_subset);
apply assumption;
apply (rule finite_subset);
prefer 2;
apply assumption;
apply force;
apply force;
apply (rule setsum_cong);
apply force;
apply (rule refl);
done;

(* This is useful for as a transitivity rule for Isar calculations
a >= b >= c ... *)

lemma order_trans2: "(b::'a::order) <= c ==> a <= b ==> a <= c";
apply (erule order_trans);
apply assumption;
done;

lemma power3_eq_cube: "(x::'a::ringpower) ^ 3 = x * x * x";
apply (subgoal_tac "3 = Suc (Suc (Suc 0))");
apply (erule ssubst);
apply simp;
done;

end
```

### Misc theorems for rings and ordered rings

lemma abs_nonneg:

`  (0::'a) ≤ x ==> ¦x¦ = x`

lemma abs_nonpos:

`  x ≤ (0::'a) ==> ¦x¦ = - x`

lemma nonneg_times_nonneg:

`  [| (0::'a) ≤ x; (0::'a) ≤ y |] ==> (0::'a) ≤ x * y`

lemma abs_pos:

`  (0::'a) < x ==> ¦x¦ = x`

lemma abs_neg:

`  x < (0::'a) ==> ¦x¦ = - x`

lemma pos_plus_pos:

`  [| (0::'a) < x; (0::'a) < y |] ==> (0::'a) < x + y`

lemma nonneg_times_nonneg:

`  [| (0::'a) ≤ x; (0::'a) ≤ y |] ==> (0::'a) ≤ x * y`

lemma nonneg_plus_nonneg:

`  [| (0::'a) ≤ x; (0::'a) ≤ y |] ==> (0::'a) ≤ x + y`

theorem ring_less_mult_cancel_left:

`  (0::'a) < a ==> (a * b < a * c) = (b < c)`

lemma abs_times_pos:

`  (0::'a) ≤ x ==> ¦y¦ * x = ¦y * x¦`

lemma abs_div:

`  y ≠ (0::'a) ==> ¦x¦ / ¦y¦ = ¦x / y¦`

lemma abs_div_pos:

`  (0::'a) < y ==> ¦x¦ / y = ¦x / y¦`

lemma abs_diff:

`  ¦a - b¦ = ¦b - a¦`

`  [| y ≠ (0::'a); z ≠ (0::'a) |] ==> x / y + w / z = (x * z + w * y) / (y * z)`

lemma diff_frac_eq:

`  [| y ≠ (0::'a); z ≠ (0::'a) |] ==> x / y - w / z = (x * z - w * y) / (y * z)`

lemma frac_eq_eq:

`  [| y ≠ (0::'a); z ≠ (0::'a) |] ==> (x / y = w / z) = (x * z = w * y)`

lemma abs_triangle_ineq2:

`  ¦a¦ - ¦b¦ ≤ ¦a - b¦`

lemma abs_triangle_ineq3:

`  ¦¦a¦ - ¦b¦¦ ≤ ¦a - b¦`

lemma abs_triangle_ineq4:

`  ¦a - b¦ ≤ ¦a¦ + ¦b¦`

lemma pos_div_pos:

`  [| (0::'a) < x; (0::'a) < y |] ==> (0::'a) < x / y`

lemma setsum_le_cong2:

```  [| finite B; A ⊆ B; !!x. x ∈ B - A ==> (0::'a) ≤ f x |]
==> setsum f A ≤ setsum f B```

lemma order_trans2:

`  [| b ≤ c; a ≤ b |] ==> a ≤ c`

lemma power3_eq_cube:

`  x ^ 3 = x * x * x`