Up to index of Isabelle/HOL
theory Numeral(* 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
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
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
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
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)
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))
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)
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))))
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