# Theory NatSimprocs

Up to index of Isabelle/HOL

theory NatSimprocs
imports NatBin
uses int_factor_simprocs.ML nat_simprocs.ML
begin

    (*  Title:      HOL/NatSimprocs.thy
        ID:         $Id: NatSimprocs.thy,v 1.22 2005/09/17 16:25:11 wenzelm Exp $
        Copyright   2003 TU Muenchen
    *)

    header {*Simprocs for the Naturals*}

    theory NatSimprocs
    imports NatBin
    uses "int_factor_simprocs.ML" "nat_simprocs.ML"
    begin

    setup nat_simprocs_setup

    subsection{*For simplifying @{term "Suc m - K"} and  @{term "K - Suc m"}*}

    text{*Where K above is a literal*}

    lemma Suc_diff_eq_diff_pred: "Numeral0 < n ==> Suc m - n = m - (n - Numeral1)"
    by (simp add: numeral_0_eq_0 numeral_1_eq_1 split add: nat_diff_split)

    text {*Now just instantiating @{text n} to @{text "number_of v"} does
      the right simplification, but with some redundant inequality
      tests.*}
    lemma neg_number_of_bin_pred_iff_0:
         "neg (number_of (bin_pred v)::int) = (number_of v = (0::nat))"
    apply (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < Suc 0) ")
    apply (simp only: less_Suc_eq_le le_0_eq)
    apply (subst less_number_of_Suc, simp)
    done

    text{*No longer required as a simprule because of the @{text inverse_fold}
       simproc*}
    lemma Suc_diff_number_of:
         "neg (number_of (bin_minus v)::int) ==>
          Suc m - (number_of v) = m - (number_of (bin_pred v))"
    apply (subst Suc_diff_eq_diff_pred)
    apply (simp add: );
    apply (simp del: nat_numeral_1_eq_1);
    apply (auto simp only: diff_nat_number_of less_0_number_of [symmetric]
                            neg_number_of_bin_pred_iff_0)
    done

    lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
    by (simp add: numerals split add: nat_diff_split)

    subsection{*For @{term nat_case} and @{term nat_rec}*}

    lemma nat_case_number_of [simp]:
         "nat_case a f (number_of v) =
            (let pv = number_of (bin_pred v) in
             if neg pv then a else f (nat pv))"
    by (simp split add: nat.split add: Let_def neg_number_of_bin_pred_iff_0)

    lemma nat_case_add_eq_if [simp]:
         "nat_case a f ((number_of v) + n) =
           (let pv = number_of (bin_pred v) in
             if neg pv then nat_case a f n else f (nat pv + n))"
    apply (subst add_eq_if)
    apply (simp split add: nat.split
                del: nat_numeral_1_eq_1
                add: numeral_1_eq_Suc_0 [symmetric] Let_def
                     neg_imp_number_of_eq_0 neg_number_of_bin_pred_iff_0)
    done

    lemma nat_rec_number_of [simp]:
         "nat_rec a f (number_of v) =
            (let pv = number_of (bin_pred v) in
             if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))"
    apply (case_tac " (number_of v) ::nat")
    apply (simp_all (no_asm_simp) add: Let_def neg_number_of_bin_pred_iff_0)
    apply (simp split add: split_if_asm)
    done

    lemma nat_rec_add_eq_if [simp]:
         "nat_rec a f (number_of v + n) =
            (let pv = number_of (bin_pred v) in
             if neg pv then nat_rec a f n
                       else f (nat pv + n) (nat_rec a f (nat pv + n)))"
    apply (subst add_eq_if)
    apply (simp split add: nat.split
                del: nat_numeral_1_eq_1
                add: numeral_1_eq_Suc_0 [symmetric] Let_def neg_imp_number_of_eq_0
                     neg_number_of_bin_pred_iff_0)
    done

    subsection{*Various Other Lemmas*}

    subsubsection{*Evens and Odds, for Mutilated Chess Board*}

    text{*Lemmas for specialist use, NOT as default simprules*}
    lemma nat_mult_2: "2 * z = (z+z::nat)"
    proof -
      have "2*z = (1 + 1)*z" by simp
      also have "... = z+z" by (simp add: left_distrib)
      finally show ?thesis .
    qed

    lemma nat_mult_2_right: "z * 2 = (z+z::nat)"
    by (subst mult_commute, rule nat_mult_2)

    text{*Case analysis on @{term "n<2"}*}
    lemma less_2_cases: "(n::nat) < 2 ==> n = 0 | n = Suc 0"
    by arith

    lemma div2_Suc_Suc [simp]: "Suc(Suc m) div 2 = Suc (m div 2)"
    by arith

    lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
    by (simp add: nat_mult_2 [symmetric])

    lemma mod2_Suc_Suc [simp]: "Suc(Suc(m)) mod 2 = m mod 2"
    apply (subgoal_tac "m mod 2 < 2")
    apply (erule less_2_cases [THEN disjE])
    apply (simp_all (no_asm_simp) add: Let_def mod_Suc nat_1)
    done

    lemma mod2_gr_0 [simp]: "!!m::nat. (0 < m mod 2) = (m mod 2 = 1)"
    apply (subgoal_tac "m mod 2 < 2")
    apply (force simp del: mod_less_divisor, simp)
    done

    subsubsection{*Removal of Small Numerals: 0, 1 and (in additive positions) 2*}

    lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
    by simp

    lemma add_2_eq_Suc' [simp]: "n + 2 = Suc (Suc n)"
    by simp

    text{*Can be used to eliminate long strings of Sucs, but not by default*}
    lemma Suc3_eq_add_3: "Suc (Suc (Suc n)) = 3 + n"
    by simp

    text{*These lemmas collapse some needless occurrences of Suc:
        at least three Sucs, since two and fewer are rewritten back to Suc again!
        We already have some rules to simplify operands smaller than 3.*}

    lemma div_Suc_eq_div_add3 [simp]: "m div (Suc (Suc (Suc n))) = m div (3+n)"
    by (simp add: Suc3_eq_add_3)

    lemma mod_Suc_eq_mod_add3 [simp]: "m mod (Suc (Suc (Suc n))) = m mod (3+n)"
    by (simp add: Suc3_eq_add_3)

    lemma Suc_div_eq_add3_div: "(Suc (Suc (Suc m))) div n = (3+m) div n"
    by (simp add: Suc3_eq_add_3)

    lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
    by (simp add: Suc3_eq_add_3)

    lemmas Suc_div_eq_add3_div_number_of =
        Suc_div_eq_add3_div [of _ "number_of v", standard]
    declare Suc_div_eq_add3_div_number_of [simp]

    lemmas Suc_mod_eq_add3_mod_number_of =
        Suc_mod_eq_add3_mod [of _ "number_of v", standard]
    declare Suc_mod_eq_add3_mod_number_of [simp]

    subsection{*Special Simplification for Constants*}

    text{*These belong here, late in the development of HOL, to prevent their
    interfering with proofs of abstract properties of instances of the function
    @{term number_of}*}

    text{*These distributive laws move literals inside sums and differences.*}
    lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard]
    declare left_distrib_number_of [simp]

    lemmas right_distrib_number_of = right_distrib [of "number_of v", standard]
    declare right_distrib_number_of [simp]

    lemmas left_diff_distrib_number_of =
        left_diff_distrib [of _ _ "number_of v", standard]
    declare left_diff_distrib_number_of [simp]

    lemmas right_diff_distrib_number_of =
        right_diff_distrib [of "number_of v", standard]
    declare right_diff_distrib_number_of [simp]

    text{*These are actually for fields, like real: but where else to put them?*}
    lemmas zero_less_divide_iff_number_of =
        zero_less_divide_iff [of "number_of w", standard]
    declare zero_less_divide_iff_number_of [simp]

    lemmas divide_less_0_iff_number_of =
        divide_less_0_iff [of "number_of w", standard]
    declare divide_less_0_iff_number_of [simp]

    lemmas zero_le_divide_iff_number_of =
        zero_le_divide_iff [of "number_of w", standard]
    declare zero_le_divide_iff_number_of [simp]

    lemmas divide_le_0_iff_number_of =
        divide_le_0_iff [of "number_of w", standard]
    declare divide_le_0_iff_number_of [simp]

    (****
    IF times_divide_eq_right and times_divide_eq_left are removed as simprules,
    then these special-case declarations may be useful.

    text{*These simprules move numerals into numerators and denominators.*}
    lemma times_recip_eq_right [simp]: "a * (1/c) = a / (c::'a::field)"
    by (simp add: times_divide_eq)

    lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)"
    by (simp add: times_divide_eq)

    lemmas times_divide_eq_right_number_of =
        times_divide_eq_right [of "number_of w", standard]
    declare times_divide_eq_right_number_of [simp]

    lemmas times_divide_eq_right_number_of =
        times_divide_eq_right [of _ _ "number_of w", standard]
    declare times_divide_eq_right_number_of [simp]

    lemmas times_divide_eq_left_number_of =
        times_divide_eq_left [of _ "number_of w", standard]
    declare times_divide_eq_left_number_of [simp]

    lemmas times_divide_eq_left_number_of =
        times_divide_eq_left [of _ _ "number_of w", standard]
    declare times_divide_eq_left_number_of [simp]

    ****)

    text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}.  It looks
      strange, but then other simprocs simplify the quotient.*}

    lemmas inverse_eq_divide_number_of =
        inverse_eq_divide [of "number_of w", standard]
    declare inverse_eq_divide_number_of [simp]

    text{*These laws simplify inequalities, moving unary minus from a term
    into the literal.*}
    lemmas less_minus_iff_number_of =
        less_minus_iff [of "number_of v", standard]
    declare less_minus_iff_number_of [simp]

    lemmas le_minus_iff_number_of =
        le_minus_iff [of "number_of v", standard]
    declare le_minus_iff_number_of [simp]

    lemmas equation_minus_iff_number_of =
        equation_minus_iff [of "number_of v", standard]
    declare equation_minus_iff_number_of [simp]

    lemmas minus_less_iff_number_of =
        minus_less_iff [of _ "number_of v", standard]
    declare minus_less_iff_number_of [simp]

    lemmas minus_le_iff_number_of =
        minus_le_iff [of _ "number_of v", standard]
    declare minus_le_iff_number_of [simp]

    lemmas minus_equation_iff_number_of =
        minus_equation_iff [of _ "number_of v", standard]
    declare minus_equation_iff_number_of [simp]

    text{*These simplify inequalities where one side is the constant 1.*}
    lemmas less_minus_iff_1 = less_minus_iff [of 1, simplified]
    declare less_minus_iff_1 [simp]

    lemmas le_minus_iff_1 = le_minus_iff [of 1, simplified]
    declare le_minus_iff_1 [simp]

    lemmas equation_minus_iff_1 = equation_minus_iff [of 1, simplified]
    declare equation_minus_iff_1 [simp]

    lemmas minus_less_iff_1 = minus_less_iff [of _ 1, simplified]
    declare minus_less_iff_1 [simp]

    lemmas minus_le_iff_1 = minus_le_iff [of _ 1, simplified]
    declare minus_le_iff_1 [simp]

    lemmas minus_equation_iff_1 = minus_equation_iff [of _ 1, simplified]
    declare minus_equation_iff_1 [simp]

    text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "≤"}) *}

    lemmas mult_less_cancel_left_number_of =
        mult_less_cancel_left [of "number_of v", standard]
    declare mult_less_cancel_left_number_of [simp]

    lemmas mult_less_cancel_right_number_of =
        mult_less_cancel_right [of _ "number_of v", standard]
    declare mult_less_cancel_right_number_of [simp]

    lemmas mult_le_cancel_left_number_of =
        mult_le_cancel_left [of "number_of v", standard]
    declare mult_le_cancel_left_number_of [simp]

    lemmas mult_le_cancel_right_number_of =
        mult_le_cancel_right [of _ "number_of v", standard]
    declare mult_le_cancel_right_number_of [simp]

    text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "≤"} and @{text "="}) *}

    lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard]
    declare le_divide_eq_number_of [simp]

    lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard]
    declare divide_le_eq_number_of [simp]

    lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard]
    declare less_divide_eq_number_of [simp]

    lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard]
    declare divide_less_eq_number_of [simp]

    lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard]
    declare eq_divide_eq_number_of [simp]

    lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard]
    declare divide_eq_eq_number_of [simp]

    subsection{*Optional Simplification Rules Involving Constants*}

    text{*Simplify quotients that are compared with a literal constant.*}

    lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
    lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
    lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
    lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
    lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
    lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]

    text{*Not good as automatic simprules because they cause case splits.*}
    lemmas divide_const_simps =
      le_divide_eq_number_of divide_le_eq_number_of less_divide_eq_number_of
      divide_less_eq_number_of eq_divide_eq_number_of divide_eq_eq_number_of
      le_divide_eq_1 divide_le_eq_1 less_divide_eq_1 divide_less_eq_1

    subsubsection{*Division By @{text "-1"}*}

    lemma divide_minus1 [simp]:
         "x/-1 = -(x::'a::{field,division_by_zero,number_ring})"
    by simp

    lemma minus1_divide [simp]:
         "-1 / (x::'a::{field,division_by_zero,number_ring}) = - (1/x)"
    by (simp add: divide_inverse inverse_minus_eq)

    lemma half_gt_zero_iff:
         "(0 < r/2) = (0 < (r::'a::{ordered_field,division_by_zero,number_ring}))"
    by auto

    lemmas half_gt_zero = half_gt_zero_iff [THEN iffD2, simp]

    (* The following lemma should appear in Divides.thy, but there the proof
       doesn't work. *)

    lemma nat_dvd_not_less:
      "[| 0 < m; m < n |] ==> ¬ n dvd (m::nat)"
      by (unfold dvd_def) auto

    ML
    {*
    val divide_minus1 = thm "divide_minus1";
    val minus1_divide = thm "minus1_divide";
    *}

    end

theorem int_mult_div_cancel1:

      k ≠ 0 ==> k * m div (k * n) = m div n

theorem int_mult_div_cancel_disj:

      k * m div (k * n) = (if k = 0 then 0 else m div n)

### For simplifying @{term "Suc m - K"} and @{term "K - Suc m"}

lemma Suc_diff_eq_diff_pred:

      Numeral0 < n ==> Suc m - n = m - (n - Numeral1)

lemma neg_number_of_bin_pred_iff_0:

      neg (number_of (bin_pred v)) = (number_of v = 0)

lemma Suc_diff_number_of:

      neg (number_of (bin_minus v))
      ==> Suc m - number_of v = m - number_of (bin_pred v)

lemma diff_Suc_eq_diff_pred:

      m - Suc n = m - 1 - n

### For @{term nat_case} and @{term nat_rec}

lemma nat_case_number_of:

      nat_case a f (number_of v) =
      (let pv = number_of (bin_pred v) in if neg pv then a else f (nat pv))

lemma nat_case_add_eq_if:

      nat_case a f (number_of v + n) =
      (let pv = number_of (bin_pred v)
       in if neg pv then nat_case a f n else f (nat pv + n))

lemma nat_rec_number_of:

      nat_rec a f (number_of v) =
      (let pv = number_of (bin_pred v)
       in if neg pv then a else f (nat pv) (nat_rec a f (nat pv)))

lemma nat_rec_add_eq_if:

      nat_rec a f (number_of v + n) =
      (let pv = number_of (bin_pred v)
       in if neg pv then nat_rec a f n else f (nat pv + n) (nat_rec a f (nat pv + n)))

### Various Other Lemmas

#### Evens and Odds, for Mutilated Chess Board

lemma nat_mult_2:

      2 * z = z + z

lemma nat_mult_2_right:

      z * 2 = z + z

lemma less_2_cases:

      n < 2 ==> n = 0 ∨ n = Suc 0

lemma div2_Suc_Suc:

      Suc (Suc m) div 2 = Suc (m div 2)

lemma add_self_div_2:

      (m + m) div 2 = m

lemma mod2_Suc_Suc:

      Suc (Suc m) mod 2 = m mod 2

lemma mod2_gr_0:

      (0 < m mod 2) = (m mod 2 = 1)

#### Removal of Small Numerals: 0, 1 and (in additive positions) 2

lemma add_2_eq_Suc:

      2 + n = Suc (Suc n)

lemma add_2_eq_Suc':

      n + 2 = Suc (Suc n)

lemma Suc3_eq_add_3:

      Suc (Suc (Suc n)) = 3 + n

lemma div_Suc_eq_div_add3:

      m div Suc (Suc (Suc n)) = m div (3 + n)

lemma mod_Suc_eq_mod_add3:

      m mod Suc (Suc (Suc n)) = m mod (3 + n)

lemma Suc_div_eq_add3_div:

      Suc (Suc (Suc m)) div n = (3 + m) div n

lemma Suc_mod_eq_add3_mod:

      Suc (Suc (Suc m)) mod n = (3 + m) mod n

lemmas Suc_div_eq_add3_div_number_of:

      Suc (Suc (Suc m)) div number_of v = (3 + m) div number_of v

lemmas Suc_div_eq_add3_div_number_of:

      Suc (Suc (Suc m)) div number_of v = (3 + m) div number_of v

lemmas Suc_mod_eq_add3_mod_number_of:

      Suc (Suc (Suc m)) mod number_of v = (3 + m) mod number_of v

lemmas Suc_mod_eq_add3_mod_number_of:

      Suc (Suc (Suc m)) mod number_of v = (3 + m) mod number_of v

### Special Simplification for Constants

lemmas left_distrib_number_of:

      (a + b) * number_of v = a * number_of v + b * number_of v

lemmas left_distrib_number_of:

      (a + b) * number_of v = a * number_of v + b * number_of v

lemmas right_distrib_number_of:

      number_of v * (b + c) = number_of v * b + number_of v * c

lemmas right_distrib_number_of:

      number_of v * (b + c) = number_of v * b + number_of v * c

lemmas left_diff_distrib_number_of:

      (a - b) * number_of v = a * number_of v - b * number_of v

lemmas left_diff_distrib_number_of:

      (a - b) * number_of v = a * number_of v - b * number_of v

lemmas right_diff_distrib_number_of:

      number_of v * (b - c) = number_of v * b - number_of v * c

lemmas right_diff_distrib_number_of:

      number_of v * (b - c) = number_of v * b - number_of v * c

lemmas zero_less_divide_iff_number_of:

      ((0::'b) < number_of w / b) =
      ((0::'b) < number_of w ∧ (0::'b) < b ∨ number_of w < (0::'b) ∧ b < (0::'b))

lemmas zero_less_divide_iff_number_of:

      ((0::'b) < number_of w / b) =
      ((0::'b) < number_of w ∧ (0::'b) < b ∨ number_of w < (0::'b) ∧ b < (0::'b))

lemmas divide_less_0_iff_number_of:

      (number_of w / b < (0::'b)) =
      ((0::'b) < number_of w ∧ b < (0::'b) ∨ number_of w < (0::'b) ∧ (0::'b) < b)

lemmas divide_less_0_iff_number_of:

      (number_of w / b < (0::'b)) =
      ((0::'b) < number_of w ∧ b < (0::'b) ∨ number_of w < (0::'b) ∧ (0::'b) < b)

lemmas zero_le_divide_iff_number_of:

      ((0::'b) ≤ number_of w / b) =
      ((0::'b) ≤ number_of w ∧ (0::'b) ≤ b ∨ number_of w ≤ (0::'b) ∧ b ≤ (0::'b))

lemmas zero_le_divide_iff_number_of:

      ((0::'b) ≤ number_of w / b) =
      ((0::'b) ≤ number_of w ∧ (0::'b) ≤ b ∨ number_of w ≤ (0::'b) ∧ b ≤ (0::'b))

lemmas divide_le_0_iff_number_of:

      (number_of w / b ≤ (0::'b)) =
      ((0::'b) ≤ number_of w ∧ b ≤ (0::'b) ∨ number_of w ≤ (0::'b) ∧ (0::'b) ≤ b)

lemmas divide_le_0_iff_number_of:

      (number_of w / b ≤ (0::'b)) =
      ((0::'b) ≤ number_of w ∧ b ≤ (0::'b) ∨ number_of w ≤ (0::'b) ∧ (0::'b) ≤ b)

lemmas inverse_eq_divide_number_of:

      inverse (number_of w) = (1::'b) / number_of w

lemmas inverse_eq_divide_number_of:

      inverse (number_of w) = (1::'b) / number_of w

lemmas less_minus_iff_number_of:

      (number_of v < - b) = (b < - number_of v)

lemmas less_minus_iff_number_of:

      (number_of v < - b) = (b < - number_of v)

lemmas le_minus_iff_number_of:

      (number_of v ≤ - b) = (b ≤ - number_of v)

lemmas le_minus_iff_number_of:

      (number_of v ≤ - b) = (b ≤ - number_of v)

lemmas equation_minus_iff_number_of:

      (number_of v = - b) = (b = - number_of v)

lemmas equation_minus_iff_number_of:

      (number_of v = - b) = (b = - number_of v)

lemmas minus_less_iff_number_of:

      (- a < number_of v) = (- number_of v < a)

lemmas minus_less_iff_number_of:

      (- a < number_of v) = (- number_of v < a)

lemmas minus_le_iff_number_of:

      (- a ≤ number_of v) = (- number_of v ≤ a)

lemmas minus_le_iff_number_of:

      (- a ≤ number_of v) = (- number_of v ≤ a)

lemmas minus_equation_iff_number_of:

      (- a = number_of v) = (- number_of v = a)

lemmas minus_equation_iff_number_of:

      (- a = number_of v) = (- number_of v = a)

lemmas less_minus_iff_1:

      ((1::'b) < - b) = (b < - (1::'b))

lemmas less_minus_iff_1:

      ((1::'b) < - b) = (b < - (1::'b))

lemmas le_minus_iff_1:

      ((1::'b) ≤ - b) = (b ≤ - (1::'b))

lemmas le_minus_iff_1:

      ((1::'b) ≤ - b) = (b ≤ - (1::'b))

lemmas equation_minus_iff_1:

      (- b = (1::'b)) = (b = - (1::'b))

lemmas equation_minus_iff_1:

      (- b = (1::'b)) = (b = - (1::'b))

lemmas minus_less_iff_1:

      (- a < (1::'b)) = (- (1::'b) < a)

lemmas minus_less_iff_1:

      (- a < (1::'b)) = (- (1::'b) < a)

lemmas minus_le_iff_1:

      (- a ≤ (1::'b)) = (- (1::'b) ≤ a)

lemmas minus_le_iff_1:

      (- a ≤ (1::'b)) = (- (1::'b) ≤ a)

lemmas minus_equation_iff_1:

      (a = - (1::'b)) = (- (1::'b) = a)

lemmas minus_equation_iff_1:

      (a = - (1::'b)) = (- (1::'b) = a)

lemmas mult_less_cancel_left_number_of:

      (number_of v * a < number_of v * b) =
      (((0::'b) ≤ number_of v --> a < b) ∧ (number_of v ≤ (0::'b) --> b < a))

lemmas mult_less_cancel_left_number_of:

      (number_of v * a < number_of v * b) =
      (((0::'b) ≤ number_of v --> a < b) ∧ (number_of v ≤ (0::'b) --> b < a))

lemmas mult_less_cancel_right_number_of:

      (a * number_of v < b * number_of v) =
      (((0::'b) ≤ number_of v --> a < b) ∧ (number_of v ≤ (0::'b) --> b < a))

lemmas mult_less_cancel_right_number_of:

      (a * number_of v < b * number_of v) =
      (((0::'b) ≤ number_of v --> a < b) ∧ (number_of v ≤ (0::'b) --> b < a))

lemmas mult_le_cancel_left_number_of:

      (number_of v * a ≤ number_of v * b) =
      (((0::'b) < number_of v --> a ≤ b) ∧ (number_of v < (0::'b) --> b ≤ a))

lemmas mult_le_cancel_left_number_of:

      (number_of v * a ≤ number_of v * b) =
      (((0::'b) < number_of v --> a ≤ b) ∧ (number_of v < (0::'b) --> b ≤ a))

lemmas mult_le_cancel_right_number_of:

      (a * number_of v ≤ b * number_of v) =
      (((0::'b) < number_of v --> a ≤ b) ∧ (number_of v < (0::'b) --> b ≤ a))

lemmas mult_le_cancel_right_number_of:

      (a * number_of v ≤ b * number_of v) =
      (((0::'b) < number_of v --> a ≤ b) ∧ (number_of v < (0::'b) --> b ≤ a))

lemmas le_divide_eq_number_of:

      (a ≤ b / number_of w) =
      (if (0::'b) < number_of w then a * number_of w ≤ b
       else if number_of w < (0::'b) then b ≤ a * number_of w else a ≤ (0::'b))

lemmas le_divide_eq_number_of:

      (a ≤ b / number_of w) =
      (if (0::'b) < number_of w then a * number_of w ≤ b
       else if number_of w < (0::'b) then b ≤ a * number_of w else a ≤ (0::'b))

lemmas divide_le_eq_number_of:

      (b / number_of w ≤ a) =
      (if (0::'b) < number_of w then b ≤ a * number_of w
       else if number_of w < (0::'b) then a * number_of w ≤ b else (0::'b) ≤ a)

lemmas divide_le_eq_number_of:

      (b / number_of w ≤ a) =
      (if (0::'b) < number_of w then b ≤ a * number_of w
       else if number_of w < (0::'b) then a * number_of w ≤ b else (0::'b) ≤ a)

lemmas less_divide_eq_number_of:

      (a < b / number_of w) =
      (if (0::'b) < number_of w then a * number_of w < b
       else if number_of w < (0::'b) then b < a * number_of w else a < (0::'b))

lemmas less_divide_eq_number_of:

      (a < b / number_of w) =
      (if (0::'b) < number_of w then a * number_of w < b
       else if number_of w < (0::'b) then b < a * number_of w else a < (0::'b))

lemmas divide_less_eq_number_of:

      (b / number_of w < a) =
      (if (0::'b) < number_of w then b < a * number_of w
       else if number_of w < (0::'b) then a * number_of w < b else (0::'b) < a)

lemmas divide_less_eq_number_of:

      (b / number_of w < a) =
      (if (0::'b) < number_of w then b < a * number_of w
       else if number_of w < (0::'b) then a * number_of w < b else (0::'b) < a)

lemmas eq_divide_eq_number_of:

      (a = b / number_of w) =
      (if number_of w ≠ (0::'b) then a * number_of w = b else a = (0::'b))

lemmas eq_divide_eq_number_of:

      (a = b / number_of w) =
      (if number_of w ≠ (0::'b) then a * number_of w = b else a = (0::'b))

lemmas divide_eq_eq_number_of:

      (b / number_of w = a) =
      (if number_of w ≠ (0::'b) then b = a * number_of w else a = (0::'b))

lemmas divide_eq_eq_number_of:

      (b / number_of w = a) =
      (if number_of w ≠ (0::'b) then b = a * number_of w else a = (0::'b))

### Optional Simplification Rules Involving Constants

lemmas le_divide_eq_number_of:

      (number_of w ≤ b / c) =
      (if (0::'b) < c then number_of w * c ≤ b
       else if c < (0::'b) then b ≤ number_of w * c else number_of w ≤ (0::'b))

lemmas le_divide_eq_number_of:

      (number_of w ≤ b / c) =
      (if (0::'b) < c then number_of w * c ≤ b
       else if c < (0::'b) then b ≤ number_of w * c else number_of w ≤ (0::'b))

lemmas divide_le_eq_number_of:

      (b / c ≤ number_of w) =
      (if (0::'b) < c then b ≤ number_of w * c
       else if c < (0::'b) then number_of w * c ≤ b else (0::'b) ≤ number_of w)

lemmas divide_le_eq_number_of:

      (b / c ≤ number_of w) =
      (if (0::'b) < c then b ≤ number_of w * c
       else if c < (0::'b) then number_of w * c ≤ b else (0::'b) ≤ number_of w)

lemmas less_divide_eq_number_of:

      (number_of w < b / c) =
      (if (0::'b) < c then number_of w * c < b
       else if c < (0::'b) then b < number_of w * c else number_of w < (0::'b))

lemmas less_divide_eq_number_of:

      (number_of w < b / c) =
      (if (0::'b) < c then number_of w * c < b
       else if c < (0::'b) then b < number_of w * c else number_of w < (0::'b))

lemmas divide_less_eq_number_of:

      (b / c < number_of w) =
      (if (0::'b) < c then b < number_of w * c
       else if c < (0::'b) then number_of w * c < b else (0::'b) < number_of w)

lemmas divide_less_eq_number_of:

      (b / c < number_of w) =
      (if (0::'b) < c then b < number_of w * c
       else if c < (0::'b) then number_of w * c < b else (0::'b) < number_of w)

lemmas eq_divide_eq_number_of:

      (number_of w = b / c) =
      (if c ≠ (0::'b) then number_of w * c = b else number_of w = (0::'b))

lemmas eq_divide_eq_number_of:

      (number_of w = b / c) =
      (if c ≠ (0::'b) then number_of w * c = b else number_of w = (0::'b))

lemmas divide_eq_eq_number_of:

      (b / c = number_of w) =
      (if c ≠ (0::'b) then b = number_of w * c else number_of w = (0::'b))

lemmas divide_eq_eq_number_of:

      (b / c = number_of w) =
      (if c ≠ (0::'b) then b = number_of w * c else number_of w = (0::'b))

lemmas divide_const_simps:

      (number_of w ≤ b / c) =
      (if (0::'b) < c then number_of w * c ≤ b
       else if c < (0::'b) then b ≤ number_of w * c else number_of w ≤ (0::'b))

      (b / c ≤ number_of w) =
      (if (0::'b) < c then b ≤ number_of w * c
       else if c < (0::'b) then number_of w * c ≤ b else (0::'b) ≤ number_of w)

      (number_of w < b / c) =
      (if (0::'b) < c then number_of w * c < b
       else if c < (0::'b) then b < number_of w * c else number_of w < (0::'b))

      (b / c < number_of w) =
      (if (0::'b) < c then b < number_of w * c
       else if c < (0::'b) then number_of w * c < b else (0::'b) < number_of w)

      (number_of w = b / c) =
      (if c ≠ (0::'b) then number_of w * c = b else number_of w = (0::'b))

      (b / c = number_of w) =
      (if c ≠ (0::'b) then b = number_of w * c else number_of w = (0::'b))

      ((1::'a) ≤ b / a) = ((0::'a) < a ∧ a ≤ b ∨ a < (0::'a) ∧ b ≤ a)

      (b / a ≤ (1::'a)) = ((0::'a) < a ∧ b ≤ a ∨ a < (0::'a) ∧ a ≤ b ∨ a = (0::'a))

      ((1::'a) < b / a) = ((0::'a) < a ∧ a < b ∨ a < (0::'a) ∧ b < a)

      (b / a < (1::'a)) = ((0::'a) < a ∧ b < a ∨ a < (0::'a) ∧ a < b ∨ a = (0::'a))

lemmas divide_const_simps:

      (number_of w ≤ b / c) =
      (if (0::'b) < c then number_of w * c ≤ b
       else if c < (0::'b) then b ≤ number_of w * c else number_of w ≤ (0::'b))

      (b / c ≤ number_of w) =
      (if (0::'b) < c then b ≤ number_of w * c
       else if c < (0::'b) then number_of w * c ≤ b else (0::'b) ≤ number_of w)

      (number_of w < b / c) =
      (if (0::'b) < c then number_of w * c < b
       else if c < (0::'b) then b < number_of w * c else number_of w < (0::'b))

      (b / c < number_of w) =
      (if (0::'b) < c then b < number_of w * c
       else if c < (0::'b) then number_of w * c < b else (0::'b) < number_of w)

      (number_of w = b / c) =
      (if c ≠ (0::'b) then number_of w * c = b else number_of w = (0::'b))

      (b / c = number_of w) =
      (if c ≠ (0::'b) then b = number_of w * c else number_of w = (0::'b))

      ((1::'a) ≤ b / a) = ((0::'a) < a ∧ a ≤ b ∨ a < (0::'a) ∧ b ≤ a)

      (b / a ≤ (1::'a)) = ((0::'a) < a ∧ b ≤ a ∨ a < (0::'a) ∧ a ≤ b ∨ a = (0::'a))

      ((1::'a) < b / a) = ((0::'a) < a ∧ a < b ∨ a < (0::'a) ∧ b < a)

      (b / a < (1::'a)) = ((0::'a) < a ∧ b < a ∨ a < (0::'a) ∧ a < b ∨ a = (0::'a))

#### Division By @{text "-1"}

lemma divide_minus1:

      x / (-1::'a) = - x

lemma minus1_divide:

      (-1::'a) / x = - ((1::'a) / x)

lemma half_gt_zero_iff:

      ((0::'a) < r / (2::'a)) = ((0::'a) < r)

lemmas half_gt_zero:

      (0::'a1) < r1 ==> (0::'a1) < r1 / (2::'a1)

lemmas half_gt_zero:

      (0::'a1) < r1 ==> (0::'a1) < r1 / (2::'a1)

lemma nat_dvd_not_less:

      [| 0 < m; m < n |] ==> ¬ n dvd m