Theory RingLib

(*  Title:      RingLib.thy
    Authors:    Jeremy Avigad
                Including some theorems by Kevin Donnelly
*)

header {* Facts about rings and fields*}

theory RingLib = Main:;

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

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

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";
  by (auto simp add: abs_if);

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 (rule add_strict_mono);
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;
  apply (rule add_mono, assumption+);
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(auto simp add: linorder_not_less);
apply(subgoal_tac "a * c <= a * b");
apply(subgoal_tac "~ a * c <= a * b");
apply(simp);
apply(subst linorder_not_le);
apply(simp);
apply(simp add: mult_left_mono order_less_le);
by(auto simp add: mult_strict_left_mono);

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 (rule add_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 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 (simp add: compare_rls);
  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 add_left_mono);
  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 add: power_Suc mult_ac);
  apply simp;
done;


end