# Theory Numeral

Up to index of Isabelle/HOL

theory Numeral
imports IntDef Datatype
uses ../Tools/numeral_syntax.ML
begin

    (*  Title:      HOL/Integ/Numeral.thy
        ID:         $Id: Numeral.thy,v 1.5 2005/06/17 14:13:07 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1994  University of Cambridge
    *)

    header{*Arithmetic on Binary Integers*}

    theory Numeral
    imports IntDef Datatype
    uses "../Tools/numeral_syntax.ML"
    begin

    text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
       Only qualified access Numeral.Pls and Numeral.Min is allowed.
       The datatype constructors bit.B0 and bit.B1 are similarly hidden.
       We do not hide Bit because we need the BIT infix syntax.*}

    text{*This formalization defines binary arithmetic in terms of the integers
    rather than using a datatype. This avoids multiple representations (leading
    zeroes, etc.)  See @{text "ZF/Integ/twos-compl.ML"}, function @{text
    int_of_binary}, for the numerical interpretation.

    The representation expects that @{text "(m mod 2)"} is 0 or 1,
    even if m is negative;
    For instance, @{text "-5 div 2 = -3"} and @{text "-5 mod 2 = 1"}; thus
    @{text "-5 = (-3)*2 + 1"}.
    *}

    typedef (Bin)
      bin = "UNIV::int set"
        by (auto)

    text{*This datatype avoids the use of type @{typ bool}, which would make
    all of the rewrite rules higher-order. If the use of datatype causes
    problems, this two-element type can easily be formalized using typedef.*}
    datatype bit = B0 | B1

    constdefs
      Pls :: "bin"
       "Pls == Abs_Bin 0"

      Min :: "bin"
       "Min == Abs_Bin (- 1)"

      Bit :: "[bin,bit] => bin"    (infixl "BIT" 90)
       --{*That is, 2w+b*}
       "w BIT b == Abs_Bin ((case b of B0 => 0 | B1 => 1) + Rep_Bin w + Rep_Bin w)"

    axclass
      number < type  -- {* for numeric types: nat, int, real, \dots *}

    consts
      number_of :: "bin => 'a::number"

    syntax
      "_Numeral" :: "num_const => 'a"    ("_")
      Numeral0 :: 'a
      Numeral1 :: 'a

    translations
      "Numeral0" == "number_of Numeral.Pls"
      "Numeral1" == "number_of (Numeral.Pls BIT bit.B1)"

    setup NumeralSyntax.setup

    syntax (xsymbols)
      "_square" :: "'a => 'a"  ("(_²)" [1000] 999)
    syntax (HTML output)
      "_square" :: "'a => 'a"  ("(_²)" [1000] 999)
    syntax (output)
      "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
    translations
      "x²" == "x^2"
      "x²" <= "x^(2::nat)"

    lemma Let_number_of [simp]: "Let (number_of v) f == f (number_of v)"
      -- {* Unfold all @{text let}s involving constants *}
      by (simp add: Let_def)

    lemma Let_0 [simp]: "Let 0 f == f 0"
      by (simp add: Let_def)

    lemma Let_1 [simp]: "Let 1 f == f 1"
      by (simp add: Let_def)

    constdefs
      bin_succ  :: "bin=>bin"
       "bin_succ w == Abs_Bin(Rep_Bin w + 1)"

      bin_pred  :: "bin=>bin"
       "bin_pred w == Abs_Bin(Rep_Bin w - 1)"

      bin_minus  :: "bin=>bin"
       "bin_minus w == Abs_Bin(- (Rep_Bin w))"

      bin_add  :: "[bin,bin]=>bin"
       "bin_add v w == Abs_Bin(Rep_Bin v + Rep_Bin w)"

      bin_mult  :: "[bin,bin]=>bin"
       "bin_mult v w == Abs_Bin(Rep_Bin v * Rep_Bin w)"

    lemmas Bin_simps =
           bin_succ_def bin_pred_def bin_minus_def bin_add_def bin_mult_def
           Pls_def Min_def Bit_def Abs_Bin_inverse Rep_Bin_inverse Bin_def

    text{*Removal of leading zeroes*}
    lemma Pls_0_eq [simp]: "Numeral.Pls BIT bit.B0 = Numeral.Pls"
    by (simp add: Bin_simps)

    lemma Min_1_eq [simp]: "Numeral.Min BIT bit.B1 = Numeral.Min"
    by (simp add: Bin_simps)

    subsection{*The Functions @{term bin_succ},  @{term bin_pred} and @{term bin_minus}*}

    lemma bin_succ_Pls [simp]: "bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1"
    by (simp add: Bin_simps)

    lemma bin_succ_Min [simp]: "bin_succ Numeral.Min = Numeral.Pls"
    by (simp add: Bin_simps)

    lemma bin_succ_1 [simp]: "bin_succ(w BIT bit.B1) = (bin_succ w) BIT bit.B0"
    by (simp add: Bin_simps add_ac)

    lemma bin_succ_0 [simp]: "bin_succ(w BIT bit.B0) = w BIT bit.B1"
    by (simp add: Bin_simps add_ac)

    lemma bin_pred_Pls [simp]: "bin_pred Numeral.Pls = Numeral.Min"
    by (simp add: Bin_simps)

    lemma bin_pred_Min [simp]: "bin_pred Numeral.Min = Numeral.Min BIT bit.B0"
    by (simp add: Bin_simps diff_minus)

    lemma bin_pred_1 [simp]: "bin_pred(w BIT bit.B1) = w BIT bit.B0"
    by (simp add: Bin_simps)

    lemma bin_pred_0 [simp]: "bin_pred(w BIT bit.B0) = (bin_pred w) BIT bit.B1"
    by (simp add: Bin_simps diff_minus add_ac)

    lemma bin_minus_Pls [simp]: "bin_minus Numeral.Pls = Numeral.Pls"
    by (simp add: Bin_simps)

    lemma bin_minus_Min [simp]: "bin_minus Numeral.Min = Numeral.Pls BIT bit.B1"
    by (simp add: Bin_simps)

    lemma bin_minus_1 [simp]:
         "bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1"
    by (simp add: Bin_simps add_ac diff_minus)

     lemma bin_minus_0 [simp]: "bin_minus(w BIT bit.B0) = (bin_minus w) BIT bit.B0"
    by (simp add: Bin_simps)

    subsection{*Binary Addition and Multiplication:
             @{term bin_add} and @{term bin_mult}*}

    lemma bin_add_Pls [simp]: "bin_add Numeral.Pls w = w"
    by (simp add: Bin_simps)

    lemma bin_add_Min [simp]: "bin_add Numeral.Min w = bin_pred w"
    by (simp add: Bin_simps diff_minus add_ac)

    lemma bin_add_BIT_11 [simp]:
         "bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0"
    by (simp add: Bin_simps add_ac)

    lemma bin_add_BIT_10 [simp]:
         "bin_add (v BIT bit.B1) (w BIT bit.B0) = (bin_add v w) BIT bit.B1"
    by (simp add: Bin_simps add_ac)

    lemma bin_add_BIT_0 [simp]:
         "bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y"
    by (simp add: Bin_simps add_ac)

    lemma bin_add_Pls_right [simp]: "bin_add w Numeral.Pls = w"
    by (simp add: Bin_simps)

    lemma bin_add_Min_right [simp]: "bin_add w Numeral.Min = bin_pred w"
    by (simp add: Bin_simps diff_minus)

    lemma bin_mult_Pls [simp]: "bin_mult Numeral.Pls w = Numeral.Pls"
    by (simp add: Bin_simps)

    lemma bin_mult_Min [simp]: "bin_mult Numeral.Min w = bin_minus w"
    by (simp add: Bin_simps)

    lemma bin_mult_1 [simp]:
         "bin_mult (v BIT bit.B1) w = bin_add ((bin_mult v w) BIT bit.B0) w"
    by (simp add: Bin_simps add_ac left_distrib)

    lemma bin_mult_0 [simp]: "bin_mult (v BIT bit.B0) w = (bin_mult v w) BIT bit.B0"
    by (simp add: Bin_simps left_distrib)

    subsection{*Converting Numerals to Rings: @{term number_of}*}

    axclass number_ring ⊆ number, comm_ring_1
      number_of_eq: "number_of w = of_int (Rep_Bin w)"

    lemma number_of_succ:
         "number_of(bin_succ w) = (1 + number_of w ::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    lemma number_of_pred:
         "number_of(bin_pred w) = (- 1 + number_of w ::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    lemma number_of_minus:
         "number_of(bin_minus w) = (- (number_of w)::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    lemma number_of_add:
         "number_of(bin_add v w) = (number_of v + number_of w::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    lemma number_of_mult:
         "number_of(bin_mult v w) = (number_of v * number_of w::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    text{*The correctness of shifting.  But it doesn't seem to give a measurable
      speed-up.*}
    lemma double_number_of_BIT:
         "(1+1) * number_of w = (number_of (w BIT bit.B0) ::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps left_distrib)

    text{*Converting numerals 0 and 1 to their abstract versions*}
    lemma numeral_0_eq_0 [simp]: "Numeral0 = (0::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    lemma numeral_1_eq_1 [simp]: "Numeral1 = (1::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    text{*Special-case simplification for small constants*}

    text{*Unary minus for the abstract constant 1. Cannot be inserted
      as a simprule until later: it is @{text number_of_Min} re-oriented!*}
    lemma numeral_m1_eq_minus_1: "(-1::'a::number_ring) = - 1"
    by (simp add: number_of_eq Bin_simps)

    lemma mult_minus1 [simp]: "-1 * z = -(z::'a::number_ring)"
    by (simp add: numeral_m1_eq_minus_1)

    lemma mult_minus1_right [simp]: "z * -1 = -(z::'a::number_ring)"
    by (simp add: numeral_m1_eq_minus_1)

    (*Negation of a coefficient*)
    lemma minus_number_of_mult [simp]:
         "- (number_of w) * z = number_of(bin_minus w) * (z::'a::number_ring)"
    by (simp add: number_of_minus)

    text{*Subtraction*}
    lemma diff_number_of_eq:
         "number_of v - number_of w =
          (number_of(bin_add v (bin_minus w))::'a::number_ring)"
    by (simp add: diff_minus number_of_add number_of_minus)

    lemma number_of_Pls: "number_of Numeral.Pls = (0::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    lemma number_of_Min: "number_of Numeral.Min = (- 1::'a::number_ring)"
    by (simp add: number_of_eq Bin_simps)

    lemma number_of_BIT:
         "number_of(w BIT x) = (case x of bit.B0 => 0 | bit.B1 => (1::'a::number_ring)) +
                               (number_of w) + (number_of w)"
    by (simp add: number_of_eq Bin_simps split: bit.split)

    subsection{*Equality of Binary Numbers*}

    text{*First version by Norbert Voelker*}

    lemma eq_number_of_eq:
      "((number_of x::'a::number_ring) = number_of y) =
       iszero (number_of (bin_add x (bin_minus y)) :: 'a)"
    by (simp add: iszero_def compare_rls number_of_add number_of_minus)

    lemma iszero_number_of_Pls: "iszero ((number_of Numeral.Pls)::'a::number_ring)"
    by (simp add: iszero_def numeral_0_eq_0)

    lemma nonzero_number_of_Min: "~ iszero ((number_of Numeral.Min)::'a::number_ring)"
    by (simp add: iszero_def numeral_m1_eq_minus_1 eq_commute)

    subsection{*Comparisons, for Ordered Rings*}

    lemma double_eq_0_iff: "(a + a = 0) = (a = (0::'a::ordered_idom))"
    proof -
      have "a + a = (1+1)*a" by (simp add: left_distrib)
      with zero_less_two [where 'a = 'a]
      show ?thesis by force
    qed

    lemma le_imp_0_less:
      assumes le: "0 ≤ z" shows "(0::int) < 1 + z"
    proof -
      have "0 ≤ z" .
      also have "... < z + 1" by (rule less_add_one)
      also have "... = 1 + z" by (simp add: add_ac)
      finally show "0 < 1 + z" .
    qed

    lemma odd_nonzero: "1 + z + z ≠ (0::int)";
    proof (cases z rule: int_cases)
      case (nonneg n)
      have le: "0 ≤ z+z" by (simp add: nonneg add_increasing)
      thus ?thesis using  le_imp_0_less [OF le]
        by (auto simp add: add_assoc)
    next
      case (neg n)
      show ?thesis
      proof
        assume eq: "1 + z + z = 0"
        have "0 < 1 + (int n + int n)"
          by (simp add: le_imp_0_less add_increasing)
        also have "... = - (1 + z + z)"
          by (simp add: neg add_assoc [symmetric])
        also have "... = 0" by (simp add: eq)
        finally have "0<0" ..
        thus False by blast
      qed
    qed

    text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
    lemma Ints_odd_nonzero: "a ∈ Ints ==> 1 + a + a ≠ (0::'a::ordered_idom)"
    proof (unfold Ints_def)
      assume "a ∈ range of_int"
      then obtain z where a: "a = of_int z" ..
      show ?thesis
      proof
        assume eq: "1 + a + a = 0"
        hence "of_int (1 + z + z) = (of_int 0 :: 'a)" by (simp add: a)
        hence "1 + z + z = 0" by (simp only: of_int_eq_iff)
        with odd_nonzero show False by blast
      qed
    qed

    lemma Ints_number_of: "(number_of w :: 'a::number_ring) ∈ Ints"
    by (simp add: number_of_eq Ints_def)

    lemma iszero_number_of_BIT:
         "iszero (number_of (w BIT x)::'a) =
          (x=bit.B0 & iszero (number_of w::'a::{ordered_idom,number_ring}))"
    by (simp add: iszero_def number_of_eq Bin_simps double_eq_0_iff
                  Ints_odd_nonzero Ints_def split: bit.split)

    lemma iszero_number_of_0:
         "iszero (number_of (w BIT bit.B0) :: 'a::{ordered_idom,number_ring}) =
          iszero (number_of w :: 'a)"
    by (simp only: iszero_number_of_BIT simp_thms)

    lemma iszero_number_of_1:
         "~ iszero (number_of (w BIT bit.B1)::'a::{ordered_idom,number_ring})"
    by (simp add: iszero_number_of_BIT)

    subsection{*The Less-Than Relation*}

    lemma less_number_of_eq_neg:
        "((number_of x::'a::{ordered_idom,number_ring}) < number_of y)
         = neg (number_of (bin_add x (bin_minus y)) :: 'a)"
    apply (subst less_iff_diff_less_0)
    apply (simp add: neg_def diff_minus number_of_add number_of_minus)
    done

    text{*If @{term Numeral0} is rewritten to 0 then this rule can't be applied:
      @{term Numeral0} IS @{term "number_of Numeral.Pls"} *}
    lemma not_neg_number_of_Pls:
         "~ neg (number_of Numeral.Pls ::'a::{ordered_idom,number_ring})"
    by (simp add: neg_def numeral_0_eq_0)

    lemma neg_number_of_Min:
         "neg (number_of Numeral.Min ::'a::{ordered_idom,number_ring})"
    by (simp add: neg_def zero_less_one numeral_m1_eq_minus_1)

    lemma double_less_0_iff: "(a + a < 0) = (a < (0::'a::ordered_idom))"
    proof -
      have "(a + a < 0) = ((1+1)*a < 0)" by (simp add: left_distrib)
      also have "... = (a < 0)"
        by (simp add: mult_less_0_iff zero_less_two
                      order_less_not_sym [OF zero_less_two])
      finally show ?thesis .
    qed

    lemma odd_less_0: "(1 + z + z < 0) = (z < (0::int))";
    proof (cases z rule: int_cases)
      case (nonneg n)
      thus ?thesis by (simp add: linorder_not_less add_assoc add_increasing
                                 le_imp_0_less [THEN order_less_imp_le])
    next
      case (neg n)
      thus ?thesis by (simp del: int_Suc
                            add: int_Suc0_eq_1 [symmetric] zadd_int compare_rls)
    qed

    text{*The premise involving @{term Ints} prevents @{term "a = 1/2"}.*}
    lemma Ints_odd_less_0:
         "a ∈ Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
    proof (unfold Ints_def)
      assume "a ∈ range of_int"
      then obtain z where a: "a = of_int z" ..
      hence "((1::'a) + a + a < 0) = (of_int (1 + z + z) < (of_int 0 :: 'a))"
        by (simp add: a)
      also have "... = (z < 0)" by (simp only: of_int_less_iff odd_less_0)
      also have "... = (a < 0)" by (simp add: a)
      finally show ?thesis .
    qed

    lemma neg_number_of_BIT:
         "neg (number_of (w BIT x)::'a) =
          neg (number_of w :: 'a::{ordered_idom,number_ring})"
    by (simp add: neg_def number_of_eq Bin_simps double_less_0_iff
                  Ints_odd_less_0 Ints_def split: bit.split)

    text{*Less-Than or Equals*}

    text{*Reduces @{term "a≤b"} to @{term "~ (b<a)"} for ALL numerals*}
    lemmas le_number_of_eq_not_less =
           linorder_not_less [of "number_of w" "number_of v", symmetric,
                              standard]

    lemma le_number_of_eq:
        "((number_of x::'a::{ordered_idom,number_ring}) ≤ number_of y)
         = (~ (neg (number_of (bin_add y (bin_minus x)) :: 'a)))"
    by (simp add: le_number_of_eq_not_less less_number_of_eq_neg)

    text{*Absolute value (@{term abs})*}

    lemma abs_number_of:
         "abs(number_of x::'a::{ordered_idom,number_ring}) =
          (if number_of x < (0::'a) then -number_of x else number_of x)"
    by (simp add: abs_if)

    text{*Re-orientation of the equation nnn=x*}
    lemma number_of_reorient: "(number_of w = x) = (x = number_of w)"
    by auto

    subsection{*Simplification of arithmetic operations on integer constants.*}

    lemmas bin_arith_extra_simps =
           number_of_add [symmetric]
           number_of_minus [symmetric] numeral_m1_eq_minus_1 [symmetric]
           number_of_mult [symmetric]
           diff_number_of_eq abs_number_of

    text{*For making a minimal simpset, one must include these default simprules.
      Also include @{text simp_thms} *}
    lemmas bin_arith_simps =
           Numeral.bit.distinct
           Pls_0_eq Min_1_eq
           bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
           bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
           bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10 bin_add_BIT_11
           bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
           bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
           bin_add_Pls_right bin_add_Min_right
           abs_zero abs_one bin_arith_extra_simps

    text{*Simplification of relational operations*}
    lemmas bin_rel_simps =
           eq_number_of_eq iszero_number_of_Pls nonzero_number_of_Min
           iszero_number_of_0 iszero_number_of_1
           less_number_of_eq_neg
           not_neg_number_of_Pls not_neg_0 not_neg_1 not_iszero_1
           neg_number_of_Min neg_number_of_BIT
           le_number_of_eq

    declare bin_arith_extra_simps [simp]
    declare bin_rel_simps [simp]

    subsection{*Simplification of arithmetic when nested to the right*}

    lemma add_number_of_left [simp]:
         "number_of v + (number_of w + z) =
          (number_of(bin_add v w) + z::'a::number_ring)"
    by (simp add: add_assoc [symmetric])

    lemma mult_number_of_left [simp]:
        "number_of v * (number_of w * z) =
         (number_of(bin_mult v w) * z::'a::number_ring)"
    by (simp add: mult_assoc [symmetric])

    lemma add_number_of_diff1:
        "number_of v + (number_of w - c) =
         number_of(bin_add v w) - (c::'a::number_ring)"
    by (simp add: diff_minus add_number_of_left)

    lemma add_number_of_diff2 [simp]: "number_of v + (c - number_of w) =
         number_of (bin_add v (bin_minus w)) + (c::'a::number_ring)"
    apply (subst diff_number_of_eq [symmetric])
    apply (simp only: compare_rls)
    done

    end

lemma Let_number_of:

      Let (number_of v) f == f (number_of v)

lemma Let_0:

      Let (0::'b) f == f (0::'b)

lemma Let_1:

      Let (1::'b) f == f (1::'b)

lemmas Bin_simps:

      bin_succ w == Abs_Bin (Rep_Bin w + 1)

      bin_pred w == Abs_Bin (Rep_Bin w - 1)

      bin_minus w == Abs_Bin (- Rep_Bin w)

      bin_add v w == Abs_Bin (Rep_Bin v + Rep_Bin w)

      bin_mult v w == Abs_Bin (Rep_Bin v * Rep_Bin w)

      Numeral.Pls == Abs_Bin 0

      Numeral.Min == Abs_Bin (- 1)

      w BIT b ==
      Abs_Bin ((case b of bit.B0 => 0 | bit.B1 => 1) + Rep_Bin w + Rep_Bin w)

      y ∈ Bin ==> Rep_Bin (Abs_Bin y) = y

      Abs_Bin (Rep_Bin x) = x

      Bin == UNIV

lemmas Bin_simps:

      bin_succ w == Abs_Bin (Rep_Bin w + 1)

      bin_pred w == Abs_Bin (Rep_Bin w - 1)

      bin_minus w == Abs_Bin (- Rep_Bin w)

      bin_add v w == Abs_Bin (Rep_Bin v + Rep_Bin w)

      bin_mult v w == Abs_Bin (Rep_Bin v * Rep_Bin w)

      Numeral.Pls == Abs_Bin 0

      Numeral.Min == Abs_Bin (- 1)

      w BIT b ==
      Abs_Bin ((case b of bit.B0 => 0 | bit.B1 => 1) + Rep_Bin w + Rep_Bin w)

      y ∈ Bin ==> Rep_Bin (Abs_Bin y) = y

      Abs_Bin (Rep_Bin x) = x

      Bin == UNIV

lemma Pls_0_eq:

      Numeral.Pls BIT bit.B0 = Numeral.Pls

lemma Min_1_eq:

      Numeral.Min BIT bit.B1 = Numeral.Min

### The Functions @{term bin_succ}, @{term bin_pred} and @{term bin_minus}

lemma bin_succ_Pls:

      bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1

lemma bin_succ_Min:

      bin_succ Numeral.Min = Numeral.Pls

lemma bin_succ_1:

      bin_succ (w BIT bit.B1) = bin_succ w BIT bit.B0

lemma bin_succ_0:

      bin_succ (w BIT bit.B0) = w BIT bit.B1

lemma bin_pred_Pls:

      bin_pred Numeral.Pls = Numeral.Min

lemma bin_pred_Min:

      bin_pred Numeral.Min = Numeral.Min BIT bit.B0

lemma bin_pred_1:

      bin_pred (w BIT bit.B1) = w BIT bit.B0

lemma bin_pred_0:

      bin_pred (w BIT bit.B0) = bin_pred w BIT bit.B1

lemma bin_minus_Pls:

      bin_minus Numeral.Pls = Numeral.Pls

lemma bin_minus_Min:

      bin_minus Numeral.Min = Numeral.Pls BIT bit.B1

lemma bin_minus_1:

      bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1

lemma bin_minus_0:

      bin_minus (w BIT bit.B0) = bin_minus w BIT bit.B0

### Binary Addition and Multiplication: @{term bin_add} and @{term bin_mult}

lemma bin_add_Pls:

      bin_add Numeral.Pls w = w

lemma bin_add_Min:

      bin_add Numeral.Min w = bin_pred w

lemma bin_add_BIT_11:

      bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0

lemma bin_add_BIT_10:

      bin_add (v BIT bit.B1) (w BIT bit.B0) = bin_add v w BIT bit.B1

lemma bin_add_BIT_0:

      bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y

lemma bin_add_Pls_right:

      bin_add w Numeral.Pls = w

lemma bin_add_Min_right:

      bin_add w Numeral.Min = bin_pred w

lemma bin_mult_Pls:

      bin_mult Numeral.Pls w = Numeral.Pls

lemma bin_mult_Min:

      bin_mult Numeral.Min w = bin_minus w

lemma bin_mult_1:

      bin_mult (v BIT bit.B1) w = bin_add (bin_mult v w BIT bit.B0) w

lemma bin_mult_0:

      bin_mult (v BIT bit.B0) w = bin_mult v w BIT bit.B0

### Converting Numerals to Rings: @{term number_of}

lemma number_of_succ:

      number_of (bin_succ w) = (1::'a) + number_of w

lemma number_of_pred:

      number_of (bin_pred w) = - (1::'a) + number_of w

lemma number_of_minus:

      number_of (bin_minus w) = - number_of w

lemma number_of_add:

      number_of (bin_add v w) = number_of v + number_of w

lemma number_of_mult:

      number_of (bin_mult v w) = number_of v * number_of w

lemma double_number_of_BIT:

      ((1::'a) + (1::'a)) * number_of w = number_of (w BIT bit.B0)

lemma numeral_0_eq_0:

      Numeral0 = (0::'a)

lemma numeral_1_eq_1:

      Numeral1 = (1::'a)

lemma numeral_m1_eq_minus_1:

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

lemma mult_minus1:

      (-1::'a) * z = - z

lemma mult_minus1_right:

      z * (-1::'a) = - z

lemma minus_number_of_mult:

      - number_of w * z = number_of (bin_minus w) * z

lemma diff_number_of_eq:

      number_of v - number_of w = number_of (bin_add v (bin_minus w))

lemma number_of_Pls:

      Numeral0 = (0::'a)

lemma number_of_Min:

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

lemma number_of_BIT:

      number_of (w BIT x) =
      (case x of bit.B0 => 0::'a | bit.B1 => 1::'a) + number_of w + number_of w

### Equality of Binary Numbers

lemma eq_number_of_eq:

      (number_of x = number_of y) = iszero (number_of (bin_add x (bin_minus y)))

lemma iszero_number_of_Pls:

      iszero Numeral0

lemma nonzero_number_of_Min:

      ¬ iszero (-1::'a)

### Comparisons, for Ordered Rings

lemma double_eq_0_iff:

      (a + a = (0::'a)) = (a = (0::'a))

lemma le_imp_0_less:

      0 ≤ z ==> 0 < 1 + z

lemma odd_nonzero:

      1 + z + z ≠ 0

lemma Ints_odd_nonzero:

      a ∈ Ints ==> (1::'a) + a + a ≠ (0::'a)

lemma Ints_number_of:

      number_of w ∈ Ints

lemma iszero_number_of_BIT:

      iszero (number_of (w BIT x)) = (x = bit.B0 ∧ iszero (number_of w))

lemma iszero_number_of_0:

      iszero (number_of (w BIT bit.B0)) = iszero (number_of w)

lemma iszero_number_of_1:

      ¬ iszero (number_of (w BIT bit.B1))

### The Less-Than Relation

lemma less_number_of_eq_neg:

      (number_of x < number_of y) = neg (number_of (bin_add x (bin_minus y)))

lemma not_neg_number_of_Pls:

      ¬ neg Numeral0

lemma neg_number_of_Min:

      neg (-1::'a)

lemma double_less_0_iff:

      (a + a < (0::'a)) = (a < (0::'a))

lemma odd_less_0:

      (1 + z + z < 0) = (z < 0)

lemma Ints_odd_less_0:

      a ∈ Ints ==> ((1::'a) + a + a < (0::'a)) = (a < (0::'a))

lemma neg_number_of_BIT:

      neg (number_of (w BIT x)) = neg (number_of w)

lemmas le_number_of_eq_not_less:

      (number_of v ≤ number_of w) = (¬ number_of w < number_of v)

lemmas le_number_of_eq_not_less:

      (number_of v ≤ number_of w) = (¬ number_of w < number_of v)

lemma le_number_of_eq:

      (number_of x ≤ number_of y) = (¬ neg (number_of (bin_add y (bin_minus x))))

lemma abs_number_of:

      ¦number_of x¦ = (if number_of x < (0::'a) then - number_of x else number_of x)

lemma number_of_reorient:

      (number_of w = x) = (x = number_of w)

### Simplification of arithmetic operations on integer constants.

lemmas bin_arith_extra_simps:

      number_of v1 + number_of w1 = number_of (bin_add v1 w1)

      - number_of w1 = number_of (bin_minus w1)

      - (1::'a1) = (-1::'a1)

      number_of v1 * number_of w1 = number_of (bin_mult v1 w1)

      number_of v - number_of w = number_of (bin_add v (bin_minus w))

      ¦number_of x¦ = (if number_of x < (0::'a) then - number_of x else number_of x)

lemmas bin_arith_extra_simps:

      number_of v1 + number_of w1 = number_of (bin_add v1 w1)

      - number_of w1 = number_of (bin_minus w1)

      - (1::'a1) = (-1::'a1)

      number_of v1 * number_of w1 = number_of (bin_mult v1 w1)

      number_of v - number_of w = number_of (bin_add v (bin_minus w))

      ¦number_of x¦ = (if number_of x < (0::'a) then - number_of x else number_of x)

lemmas bin_arith_simps:

      bit.B0 ≠ bit.B1

      bit.B1 ≠ bit.B0

      Numeral.Pls BIT bit.B0 = Numeral.Pls

      Numeral.Min BIT bit.B1 = Numeral.Min

      bin_pred Numeral.Pls = Numeral.Min

      bin_pred Numeral.Min = Numeral.Min BIT bit.B0

      bin_pred (w BIT bit.B1) = w BIT bit.B0

      bin_pred (w BIT bit.B0) = bin_pred w BIT bit.B1

      bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1

      bin_succ Numeral.Min = Numeral.Pls

      bin_succ (w BIT bit.B1) = bin_succ w BIT bit.B0

      bin_succ (w BIT bit.B0) = w BIT bit.B1

      bin_add Numeral.Pls w = w

      bin_add Numeral.Min w = bin_pred w

      bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y

      bin_add (v BIT bit.B1) (w BIT bit.B0) = bin_add v w BIT bit.B1

      bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0

      bin_minus Numeral.Pls = Numeral.Pls

      bin_minus Numeral.Min = Numeral.Pls BIT bit.B1

      bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1

      bin_minus (w BIT bit.B0) = bin_minus w BIT bit.B0

      bin_mult Numeral.Pls w = Numeral.Pls

      bin_mult Numeral.Min w = bin_minus w

      bin_mult (v BIT bit.B1) w = bin_add (bin_mult v w BIT bit.B0) w

      bin_mult (v BIT bit.B0) w = bin_mult v w BIT bit.B0

      bin_add w Numeral.Pls = w

      bin_add w Numeral.Min = bin_pred w

      ¦0::'a¦ = (0::'a)

      ¦1::'a¦ = (1::'a)

      number_of v1 + number_of w1 = number_of (bin_add v1 w1)

      - number_of w1 = number_of (bin_minus w1)

      - (1::'a1) = (-1::'a1)

      number_of v1 * number_of w1 = number_of (bin_mult v1 w1)

      number_of v - number_of w = number_of (bin_add v (bin_minus w))

      ¦number_of x¦ = (if number_of x < (0::'a) then - number_of x else number_of x)

lemmas bin_arith_simps:

      bit.B0 ≠ bit.B1

      bit.B1 ≠ bit.B0

      Numeral.Pls BIT bit.B0 = Numeral.Pls

      Numeral.Min BIT bit.B1 = Numeral.Min

      bin_pred Numeral.Pls = Numeral.Min

      bin_pred Numeral.Min = Numeral.Min BIT bit.B0

      bin_pred (w BIT bit.B1) = w BIT bit.B0

      bin_pred (w BIT bit.B0) = bin_pred w BIT bit.B1

      bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1

      bin_succ Numeral.Min = Numeral.Pls

      bin_succ (w BIT bit.B1) = bin_succ w BIT bit.B0

      bin_succ (w BIT bit.B0) = w BIT bit.B1

      bin_add Numeral.Pls w = w

      bin_add Numeral.Min w = bin_pred w

      bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y

      bin_add (v BIT bit.B1) (w BIT bit.B0) = bin_add v w BIT bit.B1

      bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0

      bin_minus Numeral.Pls = Numeral.Pls

      bin_minus Numeral.Min = Numeral.Pls BIT bit.B1

      bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1

      bin_minus (w BIT bit.B0) = bin_minus w BIT bit.B0

      bin_mult Numeral.Pls w = Numeral.Pls

      bin_mult Numeral.Min w = bin_minus w

      bin_mult (v BIT bit.B1) w = bin_add (bin_mult v w BIT bit.B0) w

      bin_mult (v BIT bit.B0) w = bin_mult v w BIT bit.B0

      bin_add w Numeral.Pls = w

      bin_add w Numeral.Min = bin_pred w

      ¦0::'a¦ = (0::'a)

      ¦1::'a¦ = (1::'a)

      number_of v1 + number_of w1 = number_of (bin_add v1 w1)

      - number_of w1 = number_of (bin_minus w1)

      - (1::'a1) = (-1::'a1)

      number_of v1 * number_of w1 = number_of (bin_mult v1 w1)

      number_of v - number_of w = number_of (bin_add v (bin_minus w))

      ¦number_of x¦ = (if number_of x < (0::'a) then - number_of x else number_of x)

lemmas bin_rel_simps:

      (number_of x = number_of y) = iszero (number_of (bin_add x (bin_minus y)))

      iszero Numeral0

      ¬ iszero (-1::'a)

      iszero (number_of (w BIT bit.B0)) = iszero (number_of w)

      ¬ iszero (number_of (w BIT bit.B1))

      (number_of x < number_of y) = neg (number_of (bin_add x (bin_minus y)))

      ¬ neg Numeral0

      ¬ neg (0::'a)

      ¬ neg (1::'a)

      ¬ iszero (1::'a)

      neg (-1::'a)

      neg (number_of (w BIT x)) = neg (number_of w)

      (number_of x ≤ number_of y) = (¬ neg (number_of (bin_add y (bin_minus x))))

lemmas bin_rel_simps:

      (number_of x = number_of y) = iszero (number_of (bin_add x (bin_minus y)))

      iszero Numeral0

      ¬ iszero (-1::'a)

      iszero (number_of (w BIT bit.B0)) = iszero (number_of w)

      ¬ iszero (number_of (w BIT bit.B1))

      (number_of x < number_of y) = neg (number_of (bin_add x (bin_minus y)))

      ¬ neg Numeral0

      ¬ neg (0::'a)

      ¬ neg (1::'a)

      ¬ iszero (1::'a)

      neg (-1::'a)

      neg (number_of (w BIT x)) = neg (number_of w)

      (number_of x ≤ number_of y) = (¬ neg (number_of (bin_add y (bin_minus x))))

### Simplification of arithmetic when nested to the right

lemma add_number_of_left:

      number_of v + (number_of w + z) = number_of (bin_add v w) + z

lemma mult_number_of_left:

      number_of v * (number_of w * z) = number_of (bin_mult v w) * z

lemma add_number_of_diff1:

      number_of v + (number_of w - c) = number_of (bin_add v w) - c

lemma add_number_of_diff2:

      number_of v + (c - number_of w) = number_of (bin_add v (bin_minus w)) + c