src/HOL/Numeral.thy

more instantiation

(*  Title:      HOL/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 Datatype IntDef
uses
  ("Tools/numeral.ML")
  ("Tools/numeral_syntax.ML")
begin

subsection {* Binary representation *}

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/Tools/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"}.
  
  This two's complement binary representation derives from the paper 
  "An Efficient Representation of Arithmetic for Term Rewriting" by
  Dave Cohen and Phil Watson, Rewriting Techniques and Applications,
  Springer LNCS 488 (240-251), 1991.
*}

datatype bit = B0 | B1

text{*
  Type @{typ bit} avoids the use of type @{typ bool}, which would make
  all of the rewrite rules higher-order.
*}

definition
  Pls :: int where
  [code func del]: "Pls = 0"

definition
  Min :: int where
  [code func del]: "Min = - 1"

definition
  Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
  [code func del]: "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"

class number = type + -- {* for numeric types: nat, int, real, \dots *}
  fixes number_of :: "int \<Rightarrow> 'a"

use "Tools/numeral.ML"

syntax
  "_Numeral" :: "num_const \<Rightarrow> 'a"    ("_")

use "Tools/numeral_syntax.ML"
setup NumeralSyntax.setup

abbreviation
  "Numeral0 \<equiv> number_of Pls"

abbreviation
  "Numeral1 \<equiv> number_of (Pls BIT B1)"

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

definition
  succ :: "int \<Rightarrow> int" where
  [code func del]: "succ k = k + 1"

definition
  pred :: "int \<Rightarrow> int" where
  [code func del]: "pred k = k - 1"

lemmas
  max_number_of [simp] = max_def
    [of "number_of u" "number_of v", standard, simp]
and
  min_number_of [simp] = min_def 
    [of "number_of u" "number_of v", standard, simp]
  -- {* unfolding @{text minx} and @{text max} on numerals *}

lemmas numeral_simps = 
  succ_def pred_def Pls_def Min_def Bit_def

text {* Removal of leading zeroes *}

lemma Pls_0_eq [simp, code post]:
  "Pls BIT B0 = Pls"
  unfolding numeral_simps by simp

lemma Min_1_eq [simp, code post]:
  "Min BIT B1 = Min"
  unfolding numeral_simps by simp


subsection {* The Functions @{term succ}, @{term pred} and @{term uminus} *}

lemma succ_Pls [simp]:
  "succ Pls = Pls BIT B1"
  unfolding numeral_simps by simp

lemma succ_Min [simp]:
  "succ Min = Pls"
  unfolding numeral_simps by simp

lemma succ_1 [simp]:
  "succ (k BIT B1) = succ k BIT B0"
  unfolding numeral_simps by simp

lemma succ_0 [simp]:
  "succ (k BIT B0) = k BIT B1"
  unfolding numeral_simps by simp

lemma pred_Pls [simp]:
  "pred Pls = Min"
  unfolding numeral_simps by simp

lemma pred_Min [simp]:
  "pred Min = Min BIT B0"
  unfolding numeral_simps by simp

lemma pred_1 [simp]:
  "pred (k BIT B1) = k BIT B0"
  unfolding numeral_simps by simp

lemma pred_0 [simp]:
  "pred (k BIT B0) = pred k BIT B1"
  unfolding numeral_simps by simp 

lemma minus_Pls [simp]:
  "- Pls = Pls"
  unfolding numeral_simps by simp 

lemma minus_Min [simp]:
  "- Min = Pls BIT B1"
  unfolding numeral_simps by simp 

lemma minus_1 [simp]:
  "- (k BIT B1) = pred (- k) BIT B1"
  unfolding numeral_simps by simp 

lemma minus_0 [simp]:
  "- (k BIT B0) = (- k) BIT B0"
  unfolding numeral_simps by simp 


subsection {*
  Binary Addition and Multiplication: @{term "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
    and @{term "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"}
*}

lemma add_Pls [simp]:
  "Pls + k = k"
  unfolding numeral_simps by simp 

lemma add_Min [simp]:
  "Min + k = pred k"
  unfolding numeral_simps by simp

lemma add_BIT_11 [simp]:
  "(k BIT B1) + (l BIT B1) = (k + succ l) BIT B0"
  unfolding numeral_simps by simp

lemma add_BIT_10 [simp]:
  "(k BIT B1) + (l BIT B0) = (k + l) BIT B1"
  unfolding numeral_simps by simp

lemma add_BIT_0 [simp]:
  "(k BIT B0) + (l BIT b) = (k + l) BIT b"
  unfolding numeral_simps by simp 

lemma add_Pls_right [simp]:
  "k + Pls = k"
  unfolding numeral_simps by simp 

lemma add_Min_right [simp]:
  "k + Min = pred k"
  unfolding numeral_simps by simp 

lemma mult_Pls [simp]:
  "Pls * w = Pls"
  unfolding numeral_simps by simp 

lemma mult_Min [simp]:
  "Min * k = - k"
  unfolding numeral_simps by simp 

lemma mult_num1 [simp]:
  "(k BIT B1) * l = ((k * l) BIT B0) + l"
  unfolding numeral_simps int_distrib by simp 

lemma mult_num0 [simp]:
  "(k BIT B0) * l = (k * l) BIT B0"
  unfolding numeral_simps int_distrib by simp 


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

class number_ring = number + comm_ring_1 +
  assumes number_of_eq: "number_of k = of_int k"

text {* self-embedding of the integers *}

instantiation int :: number_ring
begin

definition
  int_number_of_def [code func del]: "number_of w = (of_int w \<Colon> int)"

instance
  by intro_classes (simp only: int_number_of_def)

end

lemma number_of_is_id:
  "number_of (k::int) = k"
  unfolding int_number_of_def by simp

lemma number_of_succ:
  "number_of (succ k) = (1 + number_of k ::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

lemma number_of_pred:
  "number_of (pred w) = (- 1 + number_of w ::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

lemma number_of_minus:
  "number_of (uminus w) = (- (number_of w)::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

lemma number_of_add:
  "number_of (v + w) = (number_of v + number_of w::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

lemma number_of_mult:
  "number_of (v * w) = (number_of v * number_of w::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

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 B0) ::'a::number_ring)"
  unfolding number_of_eq numeral_simps left_distrib by simp

text {*
  Converting numerals 0 and 1 to their abstract versions.
*}

lemma numeral_0_eq_0 [simp]:
  "Numeral0 = (0::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

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

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"
  unfolding number_of_eq numeral_simps by simp

lemma mult_minus1 [simp]:
  "-1 * z = -(z::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

lemma mult_minus1_right [simp]:
  "z * -1 = -(z::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

(*Negation of a coefficient*)
lemma minus_number_of_mult [simp]:
   "- (number_of w) * z = number_of (uminus w) * (z::'a::number_ring)"
   unfolding number_of_eq by simp

text {* Subtraction *}

lemma diff_number_of_eq:
  "number_of v - number_of w =
    (number_of (v + uminus w)::'a::number_ring)"
  unfolding number_of_eq by simp

lemma number_of_Pls:
  "number_of Pls = (0::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

lemma number_of_Min:
  "number_of Min = (- 1::'a::number_ring)"
  unfolding number_of_eq numeral_simps by simp

lemma number_of_BIT:
  "number_of(w BIT x) = (case x of B0 => 0 | B1 => (1::'a::number_ring))
    + (number_of w) + (number_of w)"
  unfolding number_of_eq numeral_simps by (simp 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 (x + uminus y) :: 'a)"
  unfolding iszero_def number_of_add number_of_minus
  by (simp add: compare_rls)

lemma iszero_number_of_Pls:
  "iszero ((number_of Pls)::'a::number_ring)"
  unfolding iszero_def numeral_0_eq_0 ..

lemma nonzero_number_of_Min:
  "~ iszero ((number_of Min)::'a::number_ring)"
  unfolding iszero_def numeral_m1_eq_minus_1 by simp


subsection {* Comparisons, for Ordered Rings *}

lemmas double_eq_0_iff = double_zero

lemma le_imp_0_less: 
  assumes le: "0 \<le> z"
  shows "(0::int) < 1 + z"
proof -
  have "0 \<le> z" by fact
  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_double_eq_0_iff:
  assumes in_Ints: "a \<in> Ints"
  shows "(a + a = 0) = (a = (0::'a::ring_char_0))"
proof -
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  then obtain z where a: "a = of_int z" ..
  show ?thesis
  proof
    assume "a = 0"
    thus "a + a = 0" by simp
  next
    assume eq: "a + a = 0"
    hence "of_int (z + z) = (of_int 0 :: 'a)" by (simp add: a)
    hence "z + z = 0" by (simp only: of_int_eq_iff)
    hence "z = 0" by (simp only: double_eq_0_iff)
    thus "a = 0" by (simp add: a)
  qed
qed

lemma Ints_odd_nonzero:
  assumes in_Ints: "a \<in> Ints"
  shows "1 + a + a \<noteq> (0::'a::ring_char_0)"
proof -
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  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"
  unfolding number_of_eq Ints_def by simp

lemma iszero_number_of_BIT:
  "iszero (number_of (w BIT x)::'a) = 
   (x = B0 \<and> iszero (number_of w::'a::{ring_char_0,number_ring}))"
  by (simp add: iszero_def number_of_eq numeral_simps Ints_double_eq_0_iff 
    Ints_odd_nonzero Ints_def split: bit.split)

lemma iszero_number_of_0:
  "iszero (number_of (w BIT B0) :: 'a::{ring_char_0,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 B1)::'a::{ring_char_0,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 (x + uminus 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 Pls"}
*}

lemma not_neg_number_of_Pls:
  "~ neg (number_of Pls ::'a::{ordered_idom,number_ring})"
  by (simp add: neg_def numeral_0_eq_0)

lemma neg_number_of_Min:
  "neg (number_of 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: of_nat_Suc of_nat_add
    add: compare_rls of_nat_1 [symmetric] of_nat_add [symmetric])
qed

text {* The premise involving @{term Ints} prevents @{term "a = 1/2"}. *}

lemma Ints_odd_less_0: 
  assumes in_Ints: "a \<in> Ints"
  shows "(1 + a + a < 0) = (a < (0::'a::ordered_idom))";
proof -
  from in_Ints have "a \<in> range of_int" unfolding Ints_def [symmetric] .
  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 numeral_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 (y + uminus 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 arith_extra_simps [standard, simp] =
  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 arith_simps = 
  bit.distinct
  Pls_0_eq Min_1_eq
  pred_Pls pred_Min pred_1 pred_0
  succ_Pls succ_Min succ_1 succ_0
  add_Pls add_Min add_BIT_0 add_BIT_10 add_BIT_11
  minus_Pls minus_Min minus_1 minus_0
  mult_Pls mult_Min mult_num1 mult_num0 
  add_Pls_right add_Min_right
  abs_zero abs_one arith_extra_simps

text {* Simplification of relational operations *}

lemmas rel_simps [simp] = 
  eq_number_of_eq iszero_0 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
(* iszero_number_of_Pls would never be used
   because its lhs simplifies to "iszero 0" *)


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

lemma add_number_of_left [simp]:
  "number_of v + (number_of w + z) =
   (number_of(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(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(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 (v + uminus w) + (c::'a::number_ring)"
apply (subst diff_number_of_eq [symmetric])
apply (simp only: compare_rls)
done


subsection {* Configuration of the code generator *}

instance int :: eq ..

code_datatype Pls Min Bit "number_of \<Colon> int \<Rightarrow> int"

definition
  int_aux :: "nat \<Rightarrow> int \<Rightarrow> int" where
  "int_aux n i = int n + i"

lemma [code]:
  "int_aux 0 i  = i"
  "int_aux (Suc n) i = int_aux n (i + 1)" -- {* tail recursive *}
  by (simp add: int_aux_def)+

lemma [code, code unfold, code inline del]:
  "int n = int_aux n 0"
  by (simp add: int_aux_def)

definition
  nat_aux :: "int \<Rightarrow> nat \<Rightarrow> nat" where
  "nat_aux i n = nat i + n"

lemma [code]:
  "nat_aux i n = (if i \<le> 0 then n else nat_aux (i - 1) (Suc n))"  -- {* tail recursive *}
  by (auto simp add: nat_aux_def nat_eq_iff linorder_not_le order_less_imp_le
    dest: zless_imp_add1_zle)

lemma [code]: "nat i = nat_aux i 0"
  by (simp add: nat_aux_def)

lemma zero_is_num_zero [code func, code inline, symmetric, code post]:
  "(0\<Colon>int) = Numeral0" 
  by simp

lemma one_is_num_one [code func, code inline, symmetric, code post]:
  "(1\<Colon>int) = Numeral1" 
  by simp 

code_modulename SML
  IntDef Integer

code_modulename OCaml
  IntDef Integer

code_modulename Haskell
  IntDef Integer

code_modulename SML
  Numeral Integer

code_modulename OCaml
  Numeral Integer

code_modulename Haskell
  Numeral Integer

types_code
  "int" ("int")
attach (term_of) {*
val term_of_int = HOLogic.mk_number HOLogic.intT;
*}
attach (test) {*
fun gen_int i = one_of [~1, 1] * random_range 0 i;
*}

setup {*
let

fun strip_number_of (@{term "Numeral.number_of :: int => int"} $ t) = t
  | strip_number_of t = t;

fun numeral_codegen thy defs gr dep module b t =
  let val i = HOLogic.dest_numeral (strip_number_of t)
  in
    SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
      Pretty.str (string_of_int i))
  end handle TERM _ => NONE;

in

Codegen.add_codegen "numeral_codegen" numeral_codegen

end
*}

consts_code
  "number_of :: int \<Rightarrow> int"    ("(_)")
  "0 :: int"                   ("0")
  "1 :: int"                   ("1")
  "uminus :: int => int"       ("~")
  "op + :: int => int => int"  ("(_ +/ _)")
  "op * :: int => int => int"  ("(_ */ _)")
  "op \<le> :: int => int => bool" ("(_ <=/ _)")
  "op < :: int => int => bool" ("(_ </ _)")

quickcheck_params [default_type = int]

(*setup continues in theory Presburger*)

hide (open) const Pls Min B0 B1 succ pred

end