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+ −