reimplementation of HOL records; only one type is created for
each record extension, instead of one type for each field. See NEWS.
(* Title: HOL/Numeral.thy
ID: $Id$
Author: Larry Paulson and Markus Wenzel
Generic numerals represented as twos-complement bit strings.
*)
theory Numeral = Datatype
files "Tools/numeral_syntax.ML":
text{* The file @{text numeral_syntax.ML} hides the constructors Pls and Min.
Only qualified access bin.Pls and bin.Min is allowed.
We do not hide Bit because we need the BIT infix syntax.*}
text{*A number can have multiple representations, namely leading Falses with
sign @{term Pls} and leading Trues with sign @{term Min}.
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"}.
*}
datatype
bin = Pls --{*Plus: Stands for an infinite string of leading Falses*}
| Min --{*Minus: Stands for an infinite string of leading Trues*}
| Bit bin bool (infixl "BIT" 90)
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 bin.Pls"
"Numeral1" == "number_of (bin.Pls BIT True)"
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)
consts
NCons :: "[bin,bool]=>bin"
bin_succ :: "bin=>bin"
bin_pred :: "bin=>bin"
bin_minus :: "bin=>bin"
bin_add :: "[bin,bin]=>bin"
bin_mult :: "[bin,bin]=>bin"
text{*@{term NCons} inserts a bit, suppressing leading 0s and 1s*}
primrec
NCons_Pls: "NCons bin.Pls b = (if b then (bin.Pls BIT b) else bin.Pls)"
NCons_Min: "NCons bin.Min b = (if b then bin.Min else (bin.Min BIT b))"
NCons_BIT: "NCons (w BIT x) b = (w BIT x) BIT b"
primrec
bin_succ_Pls: "bin_succ bin.Pls = bin.Pls BIT True"
bin_succ_Min: "bin_succ bin.Min = bin.Pls"
bin_succ_BIT: "bin_succ(w BIT x) =
(if x then bin_succ w BIT False
else NCons w True)"
primrec
bin_pred_Pls: "bin_pred bin.Pls = bin.Min"
bin_pred_Min: "bin_pred bin.Min = bin.Min BIT False"
bin_pred_BIT: "bin_pred(w BIT x) =
(if x then NCons w False
else (bin_pred w) BIT True)"
primrec
bin_minus_Pls: "bin_minus bin.Pls = bin.Pls"
bin_minus_Min: "bin_minus bin.Min = bin.Pls BIT True"
bin_minus_BIT: "bin_minus(w BIT x) =
(if x then bin_pred (NCons (bin_minus w) False)
else bin_minus w BIT False)"
primrec
bin_add_Pls: "bin_add bin.Pls w = w"
bin_add_Min: "bin_add bin.Min w = bin_pred w"
bin_add_BIT:
"bin_add (v BIT x) w =
(case w of Pls => v BIT x
| Min => bin_pred (v BIT x)
| (w BIT y) =>
NCons (bin_add v (if (x & y) then bin_succ w else w))
(x~=y))"
primrec
bin_mult_Pls: "bin_mult bin.Pls w = bin.Pls"
bin_mult_Min: "bin_mult bin.Min w = bin_minus w"
bin_mult_BIT: "bin_mult (v BIT x) w =
(if x then (bin_add (NCons (bin_mult v w) False) w)
else (NCons (bin_mult v w) False))"
subsection{*Extra rules for @{term bin_succ}, @{term bin_pred},
@{term bin_add} and @{term bin_mult}*}
lemma NCons_Pls_0: "NCons bin.Pls False = bin.Pls"
by simp
lemma NCons_Pls_1: "NCons bin.Pls True = bin.Pls BIT True"
by simp
lemma NCons_Min_0: "NCons bin.Min False = bin.Min BIT False"
by simp
lemma NCons_Min_1: "NCons bin.Min True = bin.Min"
by simp
lemma bin_succ_1: "bin_succ(w BIT True) = (bin_succ w) BIT False"
by simp
lemma bin_succ_0: "bin_succ(w BIT False) = NCons w True"
by simp
lemma bin_pred_1: "bin_pred(w BIT True) = NCons w False"
by simp
lemma bin_pred_0: "bin_pred(w BIT False) = (bin_pred w) BIT True"
by simp
lemma bin_minus_1: "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
by simp
lemma bin_minus_0: "bin_minus(w BIT False) = (bin_minus w) BIT False"
by simp
subsection{*Binary Addition and Multiplication:
@{term bin_add} and @{term bin_mult}*}
lemma bin_add_BIT_11:
"bin_add (v BIT True) (w BIT True) =
NCons (bin_add v (bin_succ w)) False"
by simp
lemma bin_add_BIT_10:
"bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
by simp
lemma bin_add_BIT_0:
"bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
by auto
lemma bin_add_Pls_right: "bin_add w bin.Pls = w"
by (induct_tac "w", auto)
lemma bin_add_Min_right: "bin_add w bin.Min = bin_pred w"
by (induct_tac "w", auto)
lemma bin_add_BIT_BIT:
"bin_add (v BIT x) (w BIT y) =
NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
by simp
lemma bin_mult_1:
"bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
by simp
lemma bin_mult_0: "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
by simp
end