--- a/src/HOL/Numeral.thy Sat Feb 14 02:06:12 2004 +0100
+++ b/src/HOL/Numeral.thy Sun Feb 15 10:46:37 2004 +0100
@@ -8,14 +8,24 @@
theory Numeral = Datatype
files "Tools/numeral_syntax.ML":
-(* The constructors Pls/Min are hidden in numeral_syntax.ML.
- Only qualified access bin.Pls/Min is allowed.
- Should also hide Bit, but that means one cannot use BIT anymore.
-*)
+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
- | Min
+ 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
@@ -58,4 +68,136 @@
by (simp add: Let_def)
+consts
+ ring_of :: "bin => 'a::ring"
+
+ 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
+ ring_of_Pls: "ring_of bin.Pls = 0"
+ ring_of_Min: "ring_of bin.Min = - (1::'a::ring)"
+ ring_of_BIT: "ring_of(w BIT x) = (if x then 1 else 0) +
+ (ring_of w) + (ring_of w)"
+
+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