src/HOL/Integ/Numeral.thy

tuned;

(*  Title:	HOL/Integ/Numeral.thy
    ID:         $Id$
    Author:	Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright	1994  University of Cambridge
*)

header{*Arithmetic on Binary Integers*}

theory Numeral
imports IntDef Datatype
files "../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"  ("(_\<twosuperior>)" [1000] 999)
syntax (HTML output)
  "_square" :: "'a => 'a"  ("(_\<twosuperior>)" [1000] 999)
syntax (output)
  "_square" :: "'a => 'a"  ("(_ ^/ 2)" [81] 80)
translations
  "x\<twosuperior>" == "x^2"
  "x\<twosuperior>" <= "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 \<subseteq> 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 \<le> z" shows "(0::int) < 1 + z"
proof -
  have "0 \<le> 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 \<noteq> (0::int)";
proof (cases z rule: int_cases)
  case (nonneg n)
  have le: "0 \<le> 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 \<in> Ints ==> 1 + a + a \<noteq> (0::'a::ordered_idom)"
proof (unfold Ints_def) 
  assume "a \<in> 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) \<in> 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 \<in> Ints ==> (1 + a + a < 0) = (a < (0::'a::ordered_idom))";
proof (unfold Ints_def) 
  assume "a \<in> 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\<le>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}) \<le> 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