theory IntEx2
imports "Quotient_Int"
begin

subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}

(*
context ring_1
begin

 
definition 
  of_int :: "int \<Rightarrow> 'a" 
where
  "of_int 
*)


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.
*}

subsubsection {* The constructors @{term Bit0}, @{term Bit1}, @{term Pls} and @{term Min} *}

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

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

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

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

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

(*use "~~/src/HOL/Tools/numeral.ML"

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

use "~~/src/HOL/Tools/numeral_syntax.ML"

setup NumeralSyntax.setup

abbreviation
  "Numeral0 \<equiv> number_of Pls"

abbreviation
  "Numeral1 \<equiv> number_of (Bit1 Pls)"

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 del]: "succ k = k + 1"

definition
  pred :: "int \<Rightarrow> int" where
  [code 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 Bit0_def Bit1_def

text {* Removal of leading zeroes *}

lemma Bit0_Pls [simp, code_post]:
  "Bit0 Pls = Pls"
  unfolding numeral_simps by simp

lemma Bit1_Min [simp, code_post]:
  "Bit1 Min = Min"
  unfolding numeral_simps by simp

lemmas normalize_bin_simps =
  Bit0_Pls Bit1_Min
*)

end