--- a/src/HOL/Integ/Bin.ML Fri Sep 18 16:07:55 1998 +0200
+++ b/src/HOL/Integ/Bin.ML Mon Sep 21 10:43:09 1998 +0200
@@ -9,88 +9,88 @@
(** extra rules for bin_succ, bin_pred, bin_add, bin_mult **)
-qed_goal "norm_Bcons_Plus_0" Bin.thy
- "norm_Bcons PlusSign False = PlusSign"
+qed_goal "NCons_Pls_0" Bin.thy
+ "NCons Pls False = Pls"
(fn _ => [(Simp_tac 1)]);
-qed_goal "norm_Bcons_Plus_1" Bin.thy
- "norm_Bcons PlusSign True = Bcons PlusSign True"
+qed_goal "NCons_Pls_1" Bin.thy
+ "NCons Pls True = Pls BIT True"
(fn _ => [(Simp_tac 1)]);
-qed_goal "norm_Bcons_Minus_0" Bin.thy
- "norm_Bcons MinusSign False = Bcons MinusSign False"
+qed_goal "NCons_Min_0" Bin.thy
+ "NCons Min False = Min BIT False"
(fn _ => [(Simp_tac 1)]);
-qed_goal "norm_Bcons_Minus_1" Bin.thy
- "norm_Bcons MinusSign True = MinusSign"
+qed_goal "NCons_Min_1" Bin.thy
+ "NCons Min True = Min"
(fn _ => [(Simp_tac 1)]);
-qed_goal "norm_Bcons_Bcons" Bin.thy
- "norm_Bcons (Bcons w x) b = Bcons (Bcons w x) b"
+qed_goal "NCons_BIT" Bin.thy
+ "NCons (w BIT x) b = (w BIT x) BIT b"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_succ_Bcons1" Bin.thy
- "bin_succ(Bcons w True) = Bcons (bin_succ w) False"
+qed_goal "bin_succ_1" Bin.thy
+ "bin_succ(w BIT True) = (bin_succ w) BIT False"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_succ_Bcons0" Bin.thy
- "bin_succ(Bcons w False) = norm_Bcons w True"
+qed_goal "bin_succ_0" Bin.thy
+ "bin_succ(w BIT False) = NCons w True"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_pred_Bcons1" Bin.thy
- "bin_pred(Bcons w True) = norm_Bcons w False"
+qed_goal "bin_pred_1" Bin.thy
+ "bin_pred(w BIT True) = NCons w False"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_pred_Bcons0" Bin.thy
- "bin_pred(Bcons w False) = Bcons (bin_pred w) True"
+qed_goal "bin_pred_0" Bin.thy
+ "bin_pred(w BIT False) = (bin_pred w) BIT True"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_minus_Bcons1" Bin.thy
- "bin_minus(Bcons w True) = bin_pred (Bcons(bin_minus w) False)"
+qed_goal "bin_minus_1" Bin.thy
+ "bin_minus(w BIT True) = bin_pred (NCons (bin_minus w) False)"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_minus_Bcons0" Bin.thy
- "bin_minus(Bcons w False) = Bcons (bin_minus w) False"
+qed_goal "bin_minus_0" Bin.thy
+ "bin_minus(w BIT False) = (bin_minus w) BIT False"
(fn _ => [(Simp_tac 1)]);
(*** bin_add: binary addition ***)
-qed_goal "bin_add_Bcons_Bcons11" Bin.thy
- "bin_add (Bcons v True) (Bcons w True) = \
-\ norm_Bcons (bin_add v (bin_succ w)) False"
+qed_goal "bin_add_BIT_11" Bin.thy
+ "bin_add (v BIT True) (w BIT True) = \
+\ NCons (bin_add v (bin_succ w)) False"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_add_Bcons_Bcons10" Bin.thy
- "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True"
+qed_goal "bin_add_BIT_10" Bin.thy
+ "bin_add (v BIT True) (w BIT False) = NCons (bin_add v w) True"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_add_Bcons_Bcons0" Bin.thy
- "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y"
+qed_goal "bin_add_BIT_0" Bin.thy
+ "bin_add (v BIT False) (w BIT y) = NCons (bin_add v w) y"
(fn _ => [Auto_tac]);
-qed_goal "bin_add_Bcons_Plus" Bin.thy
- "bin_add (Bcons v x) PlusSign = Bcons v x"
+qed_goal "bin_add_BIT_Pls" Bin.thy
+ "bin_add (v BIT x) Pls = v BIT x"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_add_Bcons_Minus" Bin.thy
- "bin_add (Bcons v x) MinusSign = bin_pred (Bcons v x)"
+qed_goal "bin_add_BIT_Min" Bin.thy
+ "bin_add (v BIT x) Min = bin_pred (v BIT x)"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_add_Bcons_Bcons" Bin.thy
- "bin_add (Bcons v x) (Bcons w y) = \
-\ norm_Bcons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
+qed_goal "bin_add_BIT_BIT" Bin.thy
+ "bin_add (v BIT x) (w BIT y) = \
+\ NCons(bin_add v (if x & y then (bin_succ w) else w)) (x~= y)"
(fn _ => [(Simp_tac 1)]);
(*** bin_add: binary multiplication ***)
-qed_goal "bin_mult_Bcons1" Bin.thy
- "bin_mult (Bcons v True) w = bin_add (norm_Bcons (bin_mult v w) False) w"
+qed_goal "bin_mult_1" Bin.thy
+ "bin_mult (v BIT True) w = bin_add (NCons (bin_mult v w) False) w"
(fn _ => [(Simp_tac 1)]);
-qed_goal "bin_mult_Bcons0" Bin.thy
- "bin_mult (Bcons v False) w = norm_Bcons (bin_mult v w) False"
+qed_goal "bin_mult_0" Bin.thy
+ "bin_mult (v BIT False) w = NCons (bin_mult v w) False"
(fn _ => [(Simp_tac 1)]);
@@ -99,12 +99,12 @@
(**** integ_of ****)
-qed_goal "integ_of_norm_Bcons" Bin.thy
- "integ_of(norm_Bcons w b) = integ_of(Bcons w b)"
+qed_goal "integ_of_NCons" Bin.thy
+ "integ_of(NCons w b) = integ_of(w BIT b)"
(fn _ =>[(induct_tac "w" 1),
(ALLGOALS Asm_simp_tac) ]);
-Addsimps [integ_of_norm_Bcons];
+Addsimps [integ_of_NCons];
qed_goal "integ_of_succ" Bin.thy
"integ_of(bin_succ w) = $#1 + integ_of w"
@@ -121,13 +121,13 @@
by (Simp_tac 1);
by (Simp_tac 1);
by (asm_simp_tac (simpset()
- delsimps [pred_Plus,pred_Minus,pred_Bcons]
+ delsimps [pred_Pls,pred_Min,pred_BIT]
addsimps [integ_of_succ,integ_of_pred,
zadd_assoc]) 1);
qed "integ_of_minus";
-val bin_add_simps = [bin_add_Bcons_Bcons,
+val bin_add_simps = [bin_add_BIT_BIT,
integ_of_succ, integ_of_pred];
Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w";
@@ -139,8 +139,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac))));
qed_spec_mp "integ_of_add";
-val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add,
- integ_of_norm_Bcons];
+val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add];
Goal "integ_of(bin_mult v w) = integ_of v * integ_of w";
@@ -240,23 +239,23 @@
(zcompare_rls @ [integ_of_add, integ_of_minus])) 1);
qed "eq_integ_of_eq";
-Goalw [iszero_def] "iszero (integ_of PlusSign)";
+Goalw [iszero_def] "iszero (integ_of Pls)";
by (Simp_tac 1);
-qed "iszero_integ_of_Plus";
+qed "iszero_integ_of_Pls";
-Goalw [iszero_def] "~ iszero(integ_of MinusSign)";
+Goalw [iszero_def] "~ iszero(integ_of Min)";
by (Simp_tac 1);
-qed "nonzero_integ_of_Minus";
+qed "nonzero_integ_of_Min";
Goalw [iszero_def]
- "iszero (integ_of (Bcons w x)) = (~x & iszero (integ_of w))";
+ "iszero (integ_of (w BIT x)) = (~x & iszero (integ_of w))";
by (Simp_tac 1);
by (int_case_tac "integ_of w" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps (zcompare_rls @
[zminus_zadd_distrib RS sym,
add_znat]))));
-qed "iszero_integ_of_Bcons";
+qed "iszero_integ_of_BIT";
(** Less-than (<) **)
@@ -267,22 +266,22 @@
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
qed "less_integ_of_eq_zneg";
-Goal "~ znegative (integ_of PlusSign)";
+Goal "~ znegative (integ_of Pls)";
by (Simp_tac 1);
-qed "not_neg_integ_of_Plus";
+qed "not_neg_integ_of_Pls";
-Goal "znegative (integ_of MinusSign)";
+Goal "znegative (integ_of Min)";
by (Simp_tac 1);
-qed "neg_integ_of_Minus";
+qed "neg_integ_of_Min";
-Goal "znegative (integ_of (Bcons w x)) = znegative (integ_of w)";
+Goal "znegative (integ_of (w BIT x)) = znegative (integ_of w)";
by (Asm_simp_tac 1);
by (int_case_tac "integ_of w" 1);
by (ALLGOALS (asm_simp_tac
(simpset() addsimps ([add_znat, znegative_eq_less_nat0,
symmetric zdiff_def] @
zcompare_rls))));
-qed "neg_integ_of_Bcons";
+qed "neg_integ_of_BIT";
(** Less-than-or-equals (<=) **)
@@ -293,29 +292,29 @@
(*Hide the binary representation of integer constants*)
-Delsimps [succ_Bcons, pred_Bcons, min_Bcons, add_Bcons, mult_Bcons,
- integ_of_Plus, integ_of_Minus, integ_of_Bcons,
- norm_Plus, norm_Minus, norm_Bcons];
+Delsimps [succ_BIT, pred_BIT, minus_BIT, add_BIT, mult_BIT,
+ integ_of_Pls, integ_of_Min, integ_of_BIT,
+ norm_Pls, norm_Min, NCons];
(*Add simplification of arithmetic operations on integer constants*)
Addsimps [integ_of_add RS sym,
integ_of_minus RS sym,
integ_of_mult RS sym,
- bin_succ_Bcons1, bin_succ_Bcons0,
- bin_pred_Bcons1, bin_pred_Bcons0,
- bin_minus_Bcons1, bin_minus_Bcons0,
- bin_add_Bcons_Plus, bin_add_Bcons_Minus,
- bin_add_Bcons_Bcons0, bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
- bin_mult_Bcons1, bin_mult_Bcons0,
- norm_Bcons_Plus_0, norm_Bcons_Plus_1,
- norm_Bcons_Minus_0, norm_Bcons_Minus_1,
- norm_Bcons_Bcons];
+ bin_succ_1, bin_succ_0,
+ bin_pred_1, bin_pred_0,
+ bin_minus_1, bin_minus_0,
+ bin_add_BIT_Pls, bin_add_BIT_Min,
+ bin_add_BIT_0, bin_add_BIT_10, bin_add_BIT_11,
+ bin_mult_1, bin_mult_0,
+ NCons_Pls_0, NCons_Pls_1,
+ NCons_Min_0, NCons_Min_1,
+ NCons_BIT];
(*... and simplification of relational operations*)
-Addsimps [eq_integ_of_eq, iszero_integ_of_Plus, nonzero_integ_of_Minus,
- iszero_integ_of_Bcons,
+Addsimps [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
+ iszero_integ_of_BIT,
less_integ_of_eq_zneg,
- not_neg_integ_of_Plus, neg_integ_of_Minus, neg_integ_of_Bcons,
+ not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
le_integ_of_eq_not_less];
Goalw [zdiff_def]
--- a/src/HOL/Integ/Bin.thy Fri Sep 18 16:07:55 1998 +0200
+++ b/src/HOL/Integ/Bin.thy Mon Sep 21 10:43:09 1998 +0200
@@ -6,11 +6,11 @@
Arithmetic on binary integers.
- The sign PlusSign stands for an infinite string of leading F's.
- The sign MinusSign stands for an infinite string of leading T's.
+ The sign Pls stands for an infinite string of leading F's.
+ The sign Min stands for an infinite string of leading T's.
A number can have multiple representations, namely leading F's with sign
-PlusSign and leading T's with sign MinusSign. See twos-compl.ML/int_of_binary
+Pls and leading T's with sign Min. See ZF/ex/twos-compl.ML/int_of_binary
for the numerical interpretation.
The representation expects that (m mod 2) is 0 or 1, even if m is negative;
@@ -28,62 +28,70 @@
"_Int" :: xnum => int ("_")
datatype
- bin = PlusSign
- | MinusSign
- | Bcons bin bool
+ bin = Pls
+ | Min
+ | BIT bin bool (infixl 90)
consts
- integ_of :: bin=>int
- norm_Bcons :: [bin,bool]=>bin
+ integ_of :: bin=>int
+ NCons :: [bin,bool]=>bin
bin_succ :: bin=>bin
bin_pred :: bin=>bin
bin_minus :: bin=>bin
bin_add,bin_mult :: [bin,bin]=>bin
- h_bin :: [bin,bool,bin]=>bin
-
-(*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
+ h_bin :: [bin,bool,bin]=>bin
+(*NCons inserts a bit, suppressing leading 0s and 1s*)
primrec
- norm_Plus "norm_Bcons PlusSign b = (if b then (Bcons PlusSign b) else PlusSign)"
- norm_Minus "norm_Bcons MinusSign b = (if b then MinusSign else (Bcons MinusSign b))"
- norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b"
+ norm_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
+ norm_Min "NCons Min b = (if b then Min else (Min BIT b))"
+ NCons "NCons (w' BIT x') b = (w' BIT x') BIT b"
primrec
- integ_of_Plus "integ_of PlusSign = $# 0"
- integ_of_Minus "integ_of MinusSign = - ($# 1)"
- integ_of_Bcons "integ_of(Bcons w x) = (if x then $# 1 else $# 0) +
- (integ_of w) + (integ_of w)"
+ integ_of_Pls "integ_of Pls = $# 0"
+ integ_of_Min "integ_of Min = - ($# 1)"
+ integ_of_BIT "integ_of(w BIT x) = (if x then $# 1 else $# 0) +
+ (integ_of w) + (integ_of w)"
primrec
- succ_Plus "bin_succ PlusSign = Bcons PlusSign True"
- succ_Minus "bin_succ MinusSign = PlusSign"
- succ_Bcons "bin_succ(Bcons w x) = (if x then (Bcons (bin_succ w) False) else (norm_Bcons w True))"
+ succ_Pls "bin_succ Pls = Pls BIT True"
+ succ_Min "bin_succ Min = Pls"
+ succ_BIT "bin_succ(w BIT x) =
+ (if x then bin_succ w BIT False
+ else NCons w True)"
primrec
- pred_Plus "bin_pred(PlusSign) = MinusSign"
- pred_Minus "bin_pred(MinusSign) = Bcons MinusSign False"
- pred_Bcons "bin_pred(Bcons w x) = (if x then (norm_Bcons w False) else (Bcons (bin_pred w) True))"
+ pred_Pls "bin_pred Pls = Min"
+ pred_Min "bin_pred Min = Min BIT False"
+ pred_BIT "bin_pred(w BIT x) =
+ (if x then NCons w False
+ else (bin_pred w) BIT True)"
primrec
- min_Plus "bin_minus PlusSign = PlusSign"
- min_Minus "bin_minus MinusSign = Bcons PlusSign True"
- min_Bcons "bin_minus(Bcons w x) = (if x then (bin_pred (Bcons (bin_minus w) False)) else (Bcons (bin_minus w) False))"
+ minus_Pls "bin_minus Pls = Pls"
+ minus_Min "bin_minus Min = Pls BIT True"
+ minus_BIT "bin_minus(w BIT x) =
+ (if x then bin_pred (NCons (bin_minus w) False)
+ else bin_minus w BIT False)"
primrec
- add_Plus "bin_add PlusSign w = w"
- add_Minus "bin_add MinusSign w = bin_pred w"
- add_Bcons "bin_add (Bcons v x) w = h_bin v x w"
+ add_Pls "bin_add Pls w = w"
+ add_Min "bin_add Min w = bin_pred w"
+ add_BIT "bin_add (v BIT x) w = h_bin v x w"
primrec
- mult_Plus "bin_mult PlusSign w = PlusSign"
- mult_Minus "bin_mult MinusSign w = bin_minus w"
- mult_Bcons "bin_mult (Bcons v x) w = (if x then (bin_add (norm_Bcons (bin_mult v w) False) w) else (norm_Bcons (bin_mult v w) False))"
+ "h_bin v x Pls = v BIT x"
+ "h_bin v x Min = bin_pred (v BIT x)"
+ "h_bin v x (w BIT y) =
+ NCons (bin_add v (if (x & y) then bin_succ w else w))
+ (x~=y)"
primrec
- h_Plus "h_bin v x PlusSign = Bcons v x"
- h_Minus "h_bin v x MinusSign = bin_pred (Bcons v x)"
- h_BCons "h_bin v x (Bcons w y) = norm_Bcons
- (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)"
+ mult_Pls "bin_mult Pls w = Pls"
+ mult_Min "bin_mult Min w = bin_minus w"
+ 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))"
end
@@ -116,28 +124,26 @@
let
val (sign, digs) =
(case Symbol.explode str of
- "#" :: "~" :: cs => (~1, cs)
+ "#" :: "-" :: cs => (~1, cs)
| "#" :: cs => (1, cs)
| _ => raise ERROR);
- val zs = prefix_len (equal "0") digs;
+ fun bin_of 0 = []
+ | bin_of ~1 = [~1]
+ | bin_of n = (n mod 2) :: bin_of (n div 2);
- fun bin_of 0 = replicate zs 0
- | bin_of ~1 = replicate zs 1 @ [~1]
- | bin_of n = (n mod 2) :: bin_of (n div 2);
-
- fun term_of [] = const "PlusSign"
- | term_of [~1] = const "MinusSign"
- | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
+ fun term_of [] = const "Bin.bin.Pls"
+ | term_of [~1] = const "Bin.bin.Min"
+ | term_of (b :: bs) = const "Bin.bin.op BIT" $ term_of bs $ mk_bit b;
in
term_of (bin_of (sign * (#1 (read_int digs))))
end;
fun dest_bin tm =
let
- fun bin_of (Const ("PlusSign", _)) = []
- | bin_of (Const ("MinusSign", _)) = [~1]
- | bin_of (Const ("Bcons", _) $ bs $ b) = dest_bit b :: bin_of bs
+ fun bin_of (Const ("Pls", _)) = []
+ | bin_of (Const ("Min", _)) = [~1]
+ | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
fun int_of [] = 0
@@ -146,7 +152,7 @@
val rev_digs = bin_of tm;
val (sign, zs) =
(case rev rev_digs of
- ~1 :: bs => ("~", prefix_len (equal 1) bs)
+ ~1 :: bs => ("-", prefix_len (equal 1) bs)
| bs => ("", prefix_len (equal 0) bs));
val num = string_of_int (abs (int_of rev_digs));
in
--- a/src/ZF/ex/Bin.ML Fri Sep 18 16:07:55 1998 +0200
+++ b/src/ZF/ex/Bin.ML Mon Sep 21 10:43:09 1998 +0200
@@ -3,11 +3,9 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
-For Bin.thy. Arithmetic on binary integers.
+Arithmetic on binary integers.
*)
-open Bin;
-
Addsimps bin.case_eqns;
(*Perform induction on l, then prove the major premise using prems. *)
@@ -19,135 +17,131 @@
(** bin_rec -- by Vset recursion **)
-Goal "bin_rec(Plus,a,b,h) = a";
+Goal "bin_rec(Pls,a,b,h) = a";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac bin.con_defs);
by (simp_tac rank_ss 1);
-qed "bin_rec_Plus";
+qed "bin_rec_Pls";
-Goal "bin_rec(Minus,a,b,h) = b";
+Goal "bin_rec(Min,a,b,h) = b";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac bin.con_defs);
by (simp_tac rank_ss 1);
-qed "bin_rec_Minus";
+qed "bin_rec_Min";
-Goal "bin_rec(Bcons(w,x),a,b,h) = h(w, x, bin_rec(w,a,b,h))";
+Goal "bin_rec(Cons(w,x),a,b,h) = h(w, x, bin_rec(w,a,b,h))";
by (rtac (bin_rec_def RS def_Vrec RS trans) 1);
by (rewrite_goals_tac bin.con_defs);
by (simp_tac rank_ss 1);
-qed "bin_rec_Bcons";
+qed "bin_rec_Cons";
(*Type checking*)
val prems = goal Bin.thy
"[| w: bin; \
-\ a: C(Plus); b: C(Minus); \
-\ !!w x r. [| w: bin; x: bool; r: C(w) |] ==> h(w,x,r): C(Bcons(w,x)) \
+\ a: C(Pls); b: C(Min); \
+\ !!w x r. [| w: bin; x: bool; r: C(w) |] ==> h(w,x,r): C(Cons(w,x)) \
\ |] ==> bin_rec(w,a,b,h) : C(w)";
by (bin_ind_tac "w" prems 1);
by (ALLGOALS
- (asm_simp_tac (simpset() addsimps (prems@[bin_rec_Plus, bin_rec_Minus,
- bin_rec_Bcons]))));
+ (asm_simp_tac (simpset() addsimps (prems@[bin_rec_Pls, bin_rec_Min,
+ bin_rec_Cons]))));
qed "bin_rec_type";
(** Versions for use with definitions **)
val [rew] = goal Bin.thy
- "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Plus) = a";
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Pls) = a";
by (rewtac rew);
-by (rtac bin_rec_Plus 1);
-qed "def_bin_rec_Plus";
+by (rtac bin_rec_Pls 1);
+qed "def_bin_rec_Pls";
val [rew] = goal Bin.thy
- "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Minus) = b";
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Min) = b";
by (rewtac rew);
-by (rtac bin_rec_Minus 1);
-qed "def_bin_rec_Minus";
+by (rtac bin_rec_Min 1);
+qed "def_bin_rec_Min";
val [rew] = goal Bin.thy
- "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Bcons(w,x)) = h(w,x,j(w))";
+ "[| !!w. j(w)==bin_rec(w,a,b,h) |] ==> j(Cons(w,x)) = h(w,x,j(w))";
by (rewtac rew);
-by (rtac bin_rec_Bcons 1);
-qed "def_bin_rec_Bcons";
+by (rtac bin_rec_Cons 1);
+qed "def_bin_rec_Cons";
fun bin_recs def = map standard
- ([def] RL [def_bin_rec_Plus, def_bin_rec_Minus, def_bin_rec_Bcons]);
+ ([def] RL [def_bin_rec_Pls, def_bin_rec_Min, def_bin_rec_Cons]);
-Goalw [norm_Bcons_def] "norm_Bcons(Plus,0) = Plus";
+Goalw [NCons_def] "NCons(Pls,0) = Pls";
by (Asm_simp_tac 1);
-qed "norm_Bcons_Plus_0";
+qed "NCons_Pls_0";
-Goalw [norm_Bcons_def] "norm_Bcons(Plus,1) = Bcons(Plus,1)";
+Goalw [NCons_def] "NCons(Pls,1) = Cons(Pls,1)";
by (Asm_simp_tac 1);
-qed "norm_Bcons_Plus_1";
+qed "NCons_Pls_1";
-Goalw [norm_Bcons_def] "norm_Bcons(Minus,0) = Bcons(Minus,0)";
+Goalw [NCons_def] "NCons(Min,0) = Cons(Min,0)";
by (Asm_simp_tac 1);
-qed "norm_Bcons_Minus_0";
+qed "NCons_Min_0";
-Goalw [norm_Bcons_def] "norm_Bcons(Minus,1) = Minus";
+Goalw [NCons_def] "NCons(Min,1) = Min";
by (Asm_simp_tac 1);
-qed "norm_Bcons_Minus_1";
+qed "NCons_Min_1";
-Goalw [norm_Bcons_def]
- "norm_Bcons(Bcons(w,x),b) = Bcons(Bcons(w,x),b)";
+Goalw [NCons_def]
+ "NCons(Cons(w,x),b) = Cons(Cons(w,x),b)";
by (asm_simp_tac (simpset() addsimps bin.case_eqns) 1);
-qed "norm_Bcons_Bcons";
+qed "NCons_Cons";
-val norm_Bcons_simps = [norm_Bcons_Plus_0, norm_Bcons_Plus_1,
- norm_Bcons_Minus_0, norm_Bcons_Minus_1,
- norm_Bcons_Bcons];
+val NCons_simps = [NCons_Pls_0, NCons_Pls_1,
+ NCons_Min_0, NCons_Min_1,
+ NCons_Cons];
(** Type checking **)
val bin_typechecks0 = bin_rec_type :: bin.intrs;
-Goalw [integ_of_bin_def]
- "w: bin ==> integ_of_bin(w) : integ";
+Goalw [integ_of_def] "w: bin ==> integ_of(w) : integ";
by (typechk_tac (bin_typechecks0@integ_typechecks@
nat_typechecks@[bool_into_nat]));
-qed "integ_of_bin_type";
+qed "integ_of_type";
-Goalw [norm_Bcons_def]
- "[| w: bin; b: bool |] ==> norm_Bcons(w,b) : bin";
+Goalw [NCons_def] "[| w: bin; b: bool |] ==> NCons(w,b) : bin";
by (etac bin.elim 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps bin.case_eqns)));
by (typechk_tac (bin_typechecks0@bool_typechecks));
-qed "norm_Bcons_type";
+qed "NCons_type";
-Goalw [bin_succ_def]
- "w: bin ==> bin_succ(w) : bin";
-by (typechk_tac ([norm_Bcons_type]@bin_typechecks0@bool_typechecks));
+Goalw [bin_succ_def] "w: bin ==> bin_succ(w) : bin";
+by (typechk_tac ([NCons_type]@bin_typechecks0@bool_typechecks));
qed "bin_succ_type";
-Goalw [bin_pred_def]
- "w: bin ==> bin_pred(w) : bin";
-by (typechk_tac ([norm_Bcons_type]@bin_typechecks0@bool_typechecks));
+Goalw [bin_pred_def] "w: bin ==> bin_pred(w) : bin";
+by (typechk_tac ([NCons_type]@bin_typechecks0@bool_typechecks));
qed "bin_pred_type";
-Goalw [bin_minus_def]
- "w: bin ==> bin_minus(w) : bin";
-by (typechk_tac ([bin_pred_type]@bin_typechecks0@bool_typechecks));
+Goalw [bin_minus_def] "w: bin ==> bin_minus(w) : bin";
+by (typechk_tac ([NCons_type,bin_pred_type]@
+ bin_typechecks0@bool_typechecks));
qed "bin_minus_type";
Goalw [bin_add_def]
"[| v: bin; w: bin |] ==> bin_add(v,w) : bin";
-by (typechk_tac ([norm_Bcons_type, bin_succ_type, bin_pred_type]@
+by (typechk_tac ([NCons_type, bin_succ_type, bin_pred_type]@
bin_typechecks0@ bool_typechecks@ZF_typechecks));
qed "bin_add_type";
Goalw [bin_mult_def]
"[| v: bin; w: bin |] ==> bin_mult(v,w) : bin";
-by (typechk_tac ([norm_Bcons_type, bin_minus_type, bin_add_type]@
+by (typechk_tac ([NCons_type, bin_minus_type, bin_add_type]@
bin_typechecks0@ bool_typechecks));
qed "bin_mult_type";
val bin_typechecks = bin_typechecks0 @
- [integ_of_bin_type, norm_Bcons_type, bin_succ_type, bin_pred_type,
+ [integ_of_type, NCons_type, bin_succ_type, bin_pred_type,
bin_minus_type, bin_add_type, bin_mult_type];
Addsimps ([bool_1I, bool_0I,
- bin_rec_Plus, bin_rec_Minus, bin_rec_Bcons] @
- bin_recs integ_of_bin_def @ bin_typechecks);
+ bin_rec_Pls, bin_rec_Min, bin_rec_Cons] @
+ bin_recs integ_of_def @ bin_typechecks);
val typechecks = bin_typechecks @ integ_typechecks @ nat_typechecks @
[bool_subset_nat RS subsetD];
@@ -176,107 +170,104 @@
Addsimps (bin_recs bin_succ_def @ bin_recs bin_pred_def);
-(*norm_Bcons preserves the integer value of its argument*)
+(*NCons preserves the integer value of its argument*)
Goal "[| w: bin; b: bool |] ==> \
-\ integ_of_bin(norm_Bcons(w,b)) = integ_of_bin(Bcons(w,b))";
+\ integ_of(NCons(w,b)) = integ_of(Cons(w,b))";
by (etac bin.elim 1);
-by (asm_simp_tac (simpset() addsimps norm_Bcons_simps) 3);
+by (asm_simp_tac (simpset() addsimps NCons_simps) 3);
by (ALLGOALS (etac boolE));
-by (ALLGOALS (asm_simp_tac (simpset() addsimps (norm_Bcons_simps))));
-qed "integ_of_bin_norm_Bcons";
+by (ALLGOALS (asm_simp_tac (simpset() addsimps (NCons_simps))));
+qed "integ_of_NCons";
-Goal "w: bin ==> integ_of_bin(bin_succ(w)) = $#1 $+ integ_of_bin(w)";
+Addsimps [integ_of_NCons];
+
+Goal "w: bin ==> integ_of(bin_succ(w)) = $#1 $+ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (etac boolE 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps integ_of_bin_norm_Bcons::zadd_ac)));
-qed "integ_of_bin_succ";
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
+qed "integ_of_succ";
-Goal "w: bin ==> integ_of_bin(bin_pred(w)) = $~ ($#1) $+ integ_of_bin(w)";
+Goal "w: bin ==> integ_of(bin_pred(w)) = $~ ($#1) $+ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (etac boolE 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps integ_of_bin_norm_Bcons::zadd_ac)));
-qed "integ_of_bin_pred";
+by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
+qed "integ_of_pred";
(*These two results replace the definitions of bin_succ and bin_pred*)
(*** bin_minus: (unary!) negation of binary integers ***)
-Addsimps (bin_recs bin_minus_def @
- [integ_of_bin_succ, integ_of_bin_pred]);
+Addsimps (bin_recs bin_minus_def @ [integ_of_succ, integ_of_pred]);
-Goal "w: bin ==> integ_of_bin(bin_minus(w)) = $~ integ_of_bin(w)";
+Goal "w: bin ==> integ_of(bin_minus(w)) = $~ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (etac boolE 1);
by (ALLGOALS
(asm_simp_tac (simpset() addsimps (zadd_ac@[zminus_zadd_distrib]))));
-qed "integ_of_bin_minus";
+qed "integ_of_minus";
(*** bin_add: binary addition ***)
-Goalw [bin_add_def] "w: bin ==> bin_add(Plus,w) = w";
+Goalw [bin_add_def] "w: bin ==> bin_add(Pls,w) = w";
by (Asm_simp_tac 1);
-qed "bin_add_Plus";
+qed "bin_add_Pls";
-Goalw [bin_add_def] "w: bin ==> bin_add(Minus,w) = bin_pred(w)";
+Goalw [bin_add_def] "w: bin ==> bin_add(Min,w) = bin_pred(w)";
by (Asm_simp_tac 1);
-qed "bin_add_Minus";
+qed "bin_add_Min";
-Goalw [bin_add_def] "bin_add(Bcons(v,x),Plus) = Bcons(v,x)";
+Goalw [bin_add_def] "bin_add(Cons(v,x),Pls) = Cons(v,x)";
by (Simp_tac 1);
-qed "bin_add_Bcons_Plus";
+qed "bin_add_Cons_Pls";
-Goalw [bin_add_def] "bin_add(Bcons(v,x),Minus) = bin_pred(Bcons(v,x))";
+Goalw [bin_add_def] "bin_add(Cons(v,x),Min) = bin_pred(Cons(v,x))";
by (Simp_tac 1);
-qed "bin_add_Bcons_Minus";
+qed "bin_add_Cons_Min";
Goalw [bin_add_def]
"[| w: bin; y: bool |] ==> \
-\ bin_add(Bcons(v,x), Bcons(w,y)) = \
-\ norm_Bcons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
+\ bin_add(Cons(v,x), Cons(w,y)) = \
+\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
by (Asm_simp_tac 1);
-qed "bin_add_Bcons_Bcons";
+qed "bin_add_Cons_Cons";
-Addsimps [bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
- bin_add_Bcons_Minus, bin_add_Bcons_Bcons,
- integ_of_bin_succ, integ_of_bin_pred,
- integ_of_bin_norm_Bcons];
+Addsimps [bin_add_Pls, bin_add_Min, bin_add_Cons_Pls,
+ bin_add_Cons_Min, bin_add_Cons_Cons,
+ integ_of_succ, integ_of_pred];
Addsimps [bool_subset_nat RS subsetD];
Goal "v: bin ==> \
-\ ALL w: bin. integ_of_bin(bin_add(v,w)) = \
-\ integ_of_bin(v) $+ integ_of_bin(w)";
+\ ALL w: bin. integ_of(bin_add(v,w)) = \
+\ integ_of(v) $+ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
by (rtac ballI 1);
by (bin_ind_tac "wa" [] 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac setloop (etac boolE))));
-val integ_of_bin_add_lemma = result();
+val integ_of_add_lemma = result();
-bind_thm("integ_of_bin_add", integ_of_bin_add_lemma RS bspec);
+bind_thm("integ_of_add", integ_of_add_lemma RS bspec);
(*** bin_add: binary multiplication ***)
Addsimps (bin_recs bin_mult_def @
- [integ_of_bin_minus, integ_of_bin_add,
- integ_of_bin_norm_Bcons]);
+ [integ_of_minus, integ_of_add]);
val major::prems = goal Bin.thy
"[| v: bin; w: bin |] ==> \
-\ integ_of_bin(bin_mult(v,w)) = \
-\ integ_of_bin(v) $* integ_of_bin(w)";
+\ integ_of(bin_mult(v,w)) = \
+\ integ_of(v) $* integ_of(w)";
by (cut_facts_tac prems 1);
by (bin_ind_tac "v" [major] 1);
by (Asm_simp_tac 1);
@@ -285,91 +276,91 @@
by (asm_simp_tac (simpset() addsimps [zadd_zmult_distrib]) 2);
by (asm_simp_tac
(simpset() addsimps ([zadd_zmult_distrib, zmult_1] @ zadd_ac)) 1);
-qed "integ_of_bin_mult";
+qed "integ_of_mult";
(**** Computations ****)
(** extra rules for bin_succ, bin_pred **)
-val [bin_succ_Plus, bin_succ_Minus, _] = bin_recs bin_succ_def;
-val [bin_pred_Plus, bin_pred_Minus, _] = bin_recs bin_pred_def;
+val [bin_succ_Pls, bin_succ_Min, _] = bin_recs bin_succ_def;
+val [bin_pred_Pls, bin_pred_Min, _] = bin_recs bin_pred_def;
-Goal "bin_succ(Bcons(w,1)) = Bcons(bin_succ(w), 0)";
+Goal "bin_succ(Cons(w,1)) = Cons(bin_succ(w), 0)";
by (Simp_tac 1);
-qed "bin_succ_Bcons1";
+qed "bin_succ_Cons1";
-Goal "bin_succ(Bcons(w,0)) = norm_Bcons(w,1)";
+Goal "bin_succ(Cons(w,0)) = NCons(w,1)";
by (Simp_tac 1);
-qed "bin_succ_Bcons0";
+qed "bin_succ_Cons0";
-Goal "bin_pred(Bcons(w,1)) = norm_Bcons(w,0)";
+Goal "bin_pred(Cons(w,1)) = NCons(w,0)";
by (Simp_tac 1);
-qed "bin_pred_Bcons1";
+qed "bin_pred_Cons1";
-Goal "bin_pred(Bcons(w,0)) = Bcons(bin_pred(w), 1)";
+Goal "bin_pred(Cons(w,0)) = Cons(bin_pred(w), 1)";
by (Simp_tac 1);
-qed "bin_pred_Bcons0";
+qed "bin_pred_Cons0";
(** extra rules for bin_minus **)
-val [bin_minus_Plus, bin_minus_Minus, _] = bin_recs bin_minus_def;
+val [bin_minus_Pls, bin_minus_Min, _] = bin_recs bin_minus_def;
-Goal "bin_minus(Bcons(w,1)) = bin_pred(Bcons(bin_minus(w), 0))";
+Goal "bin_minus(Cons(w,1)) = bin_pred(NCons(bin_minus(w), 0))";
by (Simp_tac 1);
-qed "bin_minus_Bcons1";
+qed "bin_minus_Cons1";
-Goal "bin_minus(Bcons(w,0)) = Bcons(bin_minus(w), 0)";
+Goal "bin_minus(Cons(w,0)) = Cons(bin_minus(w), 0)";
by (Simp_tac 1);
-qed "bin_minus_Bcons0";
+qed "bin_minus_Cons0";
(** extra rules for bin_add **)
-Goal "w: bin ==> bin_add(Bcons(v,1), Bcons(w,1)) = \
-\ norm_Bcons(bin_add(v, bin_succ(w)), 0)";
+Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,1)) = \
+\ NCons(bin_add(v, bin_succ(w)), 0)";
by (Asm_simp_tac 1);
-qed "bin_add_Bcons_Bcons11";
+qed "bin_add_Cons_Cons11";
-Goal "w: bin ==> bin_add(Bcons(v,1), Bcons(w,0)) = \
-\ norm_Bcons(bin_add(v,w), 1)";
+Goal "w: bin ==> bin_add(Cons(v,1), Cons(w,0)) = \
+\ NCons(bin_add(v,w), 1)";
by (Asm_simp_tac 1);
-qed "bin_add_Bcons_Bcons10";
+qed "bin_add_Cons_Cons10";
Goal "[| w: bin; y: bool |] ==> \
-\ bin_add(Bcons(v,0), Bcons(w,y)) = norm_Bcons(bin_add(v,w), y)";
+\ bin_add(Cons(v,0), Cons(w,y)) = NCons(bin_add(v,w), y)";
by (Asm_simp_tac 1);
-qed "bin_add_Bcons_Bcons0";
+qed "bin_add_Cons_Cons0";
(** extra rules for bin_mult **)
-val [bin_mult_Plus, bin_mult_Minus, _] = bin_recs bin_mult_def;
+val [bin_mult_Pls, bin_mult_Min, _] = bin_recs bin_mult_def;
-Goal "bin_mult(Bcons(v,1), w) = bin_add(norm_Bcons(bin_mult(v,w),0), w)";
+Goal "bin_mult(Cons(v,1), w) = bin_add(NCons(bin_mult(v,w),0), w)";
by (Simp_tac 1);
-qed "bin_mult_Bcons1";
+qed "bin_mult_Cons1";
-Goal "bin_mult(Bcons(v,0), w) = norm_Bcons(bin_mult(v,w),0)";
+Goal "bin_mult(Cons(v,0), w) = NCons(bin_mult(v,w),0)";
by (Simp_tac 1);
-qed "bin_mult_Bcons0";
+qed "bin_mult_Cons0";
(*** The computation simpset ***)
val bin_comp_ss = simpset_of Integ.thy
- addsimps [integ_of_bin_add RS sym, (*invoke bin_add*)
- integ_of_bin_minus RS sym, (*invoke bin_minus*)
- integ_of_bin_mult RS sym, (*invoke bin_mult*)
- bin_succ_Plus, bin_succ_Minus,
- bin_succ_Bcons1, bin_succ_Bcons0,
- bin_pred_Plus, bin_pred_Minus,
- bin_pred_Bcons1, bin_pred_Bcons0,
- bin_minus_Plus, bin_minus_Minus,
- bin_minus_Bcons1, bin_minus_Bcons0,
- bin_add_Plus, bin_add_Minus, bin_add_Bcons_Plus,
- bin_add_Bcons_Minus, bin_add_Bcons_Bcons0,
- bin_add_Bcons_Bcons10, bin_add_Bcons_Bcons11,
- bin_mult_Plus, bin_mult_Minus,
- bin_mult_Bcons1, bin_mult_Bcons0] @
- norm_Bcons_simps
+ addsimps [integ_of_add RS sym, (*invoke bin_add*)
+ integ_of_minus RS sym, (*invoke bin_minus*)
+ integ_of_mult RS sym, (*invoke bin_mult*)
+ bin_succ_Pls, bin_succ_Min,
+ bin_succ_Cons1, bin_succ_Cons0,
+ bin_pred_Pls, bin_pred_Min,
+ bin_pred_Cons1, bin_pred_Cons0,
+ bin_minus_Pls, bin_minus_Min,
+ bin_minus_Cons1, bin_minus_Cons0,
+ bin_add_Pls, bin_add_Min, bin_add_Cons_Pls,
+ bin_add_Cons_Min, bin_add_Cons_Cons0,
+ bin_add_Cons_Cons10, bin_add_Cons_Cons11,
+ bin_mult_Pls, bin_mult_Min,
+ bin_mult_Cons1, bin_mult_Cons0] @
+ NCons_simps
setSolver (type_auto_tac ([bool_1I, bool_0I] @ bin_typechecks0));
@@ -390,26 +381,26 @@
bin_add(binary_of_int 1234, binary_of_int 5678);
-Goal "#1359 $+ #~2468 = #~1109";
+Goal "#1359 $+ #-2468 = #-1109";
by (simp_tac bin_comp_ss 1); (*1.2 secs*)
result();
bin_add(binary_of_int 1359, binary_of_int ~2468);
-Goal "#93746 $+ #~46375 = #47371";
+Goal "#93746 $+ #-46375 = #47371";
by (simp_tac bin_comp_ss 1); (*1.9 secs*)
result();
bin_add(binary_of_int 93746, binary_of_int ~46375);
-Goal "$~ #65745 = #~65745";
+Goal "$~ #65745 = #-65745";
by (simp_tac bin_comp_ss 1); (*0.4 secs*)
result();
bin_minus(binary_of_int 65745);
(* negation of ~54321 *)
-Goal "$~ #~54321 = #54321";
+Goal "$~ #-54321 = #54321";
by (simp_tac bin_comp_ss 1); (*0.5 secs*)
result();
@@ -421,7 +412,7 @@
bin_mult(binary_of_int 13, binary_of_int 19);
-Goal "#~84 $* #51 = #~4284";
+Goal "#-84 $* #51 = #-4284";
by (simp_tac bin_comp_ss 1); (*1.3 secs*)
result();
@@ -434,7 +425,7 @@
bin_mult(binary_of_int 255, binary_of_int 255);
-Goal "#1359 $* #~2468 = #~3354012";
+Goal "#1359 $* #-2468 = #-3354012";
by (simp_tac bin_comp_ss 1); (*6.1 secs*)
result();
--- a/src/ZF/ex/Bin.thy Fri Sep 18 16:07:55 1998 +0200
+++ b/src/ZF/ex/Bin.thy Mon Sep 21 10:43:09 1998 +0200
@@ -5,11 +5,11 @@
Arithmetic on binary integers.
- The sign Plus stands for an infinite string of leading 0's.
- The sign Minus stands for an infinite string of leading 1's.
+ The sign Pls stands for an infinite string of leading 0's.
+ The sign Min stands for an infinite string of leading 1's.
A number can have multiple representations, namely leading 0's with sign
-Plus and leading 1's with sign Minus. See twos-compl.ML/int_of_binary for
+Pls and leading 1's with sign Min. See twos-compl.ML/int_of_binary for
the numerical interpretation.
The representation expects that (m mod 2) is 0 or 1, even if m is negative;
@@ -22,8 +22,8 @@
consts
bin_rec :: [i, i, i, [i,i,i]=>i] => i
- integ_of_bin :: i=>i
- norm_Bcons :: [i,i]=>i
+ integ_of :: i=>i
+ NCons :: [i,i]=>i
bin_succ :: i=>i
bin_pred :: i=>i
bin_minus :: i=>i
@@ -35,9 +35,9 @@
"_Int" :: xnum => i ("_")
datatype
- "bin" = Plus
- | Minus
- | Bcons ("w: bin", "b: bool")
+ "bin" = Pls
+ | Min
+ | Cons ("w: bin", "b: bool")
type_intrs "[bool_into_univ]"
@@ -47,31 +47,31 @@
"bin_rec(z,a,b,h) ==
Vrec(z, %z g. bin_case(a, b, %w x. h(w, x, g`w), z))"
- integ_of_bin_def
- "integ_of_bin(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
+ integ_of_def
+ "integ_of(w) == bin_rec(w, $#0, $~($#1), %w x r. $#x $+ r $+ r)"
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
- (*norm_Bcons adds a bit, suppressing leading 0s and 1s*)
- norm_Bcons_def
- "norm_Bcons(w,b) ==
- bin_case(cond(b,Bcons(w,b),w), cond(b,w,Bcons(w,b)),
- %w' x'. Bcons(w,b), w)"
+ (*NCons adds a bit, suppressing leading 0s and 1s*)
+ NCons_def
+ "NCons(w,b) ==
+ bin_case(cond(b,Cons(w,b),w), cond(b,w,Cons(w,b)),
+ %w' x'. Cons(w,b), w)"
bin_succ_def
"bin_succ(w0) ==
- bin_rec(w0, Bcons(Plus,1), Plus,
- %w x r. cond(x, Bcons(r,0), norm_Bcons(w,1)))"
+ bin_rec(w0, Cons(Pls,1), Pls,
+ %w x r. cond(x, Cons(r,0), NCons(w,1)))"
bin_pred_def
"bin_pred(w0) ==
- bin_rec(w0, Minus, Bcons(Minus,0),
- %w x r. cond(x, norm_Bcons(w,0), Bcons(r,1)))"
+ bin_rec(w0, Min, Cons(Min,0),
+ %w x r. cond(x, NCons(w,0), Cons(r,1)))"
bin_minus_def
"bin_minus(w0) ==
- bin_rec(w0, Plus, Bcons(Plus,1),
- %w x r. cond(x, bin_pred(Bcons(r,0)), Bcons(r,0)))"
+ bin_rec(w0, Pls, Cons(Pls,1),
+ %w x r. cond(x, bin_pred(NCons(r,0)), Cons(r,0)))"
bin_add_def
"bin_add(v0,w0) ==
@@ -79,14 +79,14 @@
lam w:bin. w,
lam w:bin. bin_pred(w),
%v x r. lam w1:bin.
- bin_rec(w1, Bcons(v,x), bin_pred(Bcons(v,x)),
- %w y s. norm_Bcons(r`cond(x and y, bin_succ(w), w),
+ bin_rec(w1, Cons(v,x), bin_pred(Cons(v,x)),
+ %w y s. NCons(r`cond(x and y, bin_succ(w), w),
x xor y))) ` w0"
bin_mult_def
"bin_mult(v0,w) ==
- bin_rec(v0, Plus, bin_minus(w),
- %v x r. cond(x, bin_add(norm_Bcons(r,0),w), norm_Bcons(r,0)))"
+ bin_rec(v0, Pls, bin_minus(w),
+ %v x r. cond(x, bin_add(NCons(r,0),w), NCons(r,0)))"
end
@@ -118,28 +118,28 @@
let
val (sign, digs) =
(case Symbol.explode str of
- "#" :: "~" :: cs => (~1, cs)
+ "#" :: "-" :: cs => (~1, cs)
| "#" :: cs => (1, cs)
| _ => raise ERROR);
val zs = prefix_len (equal "0") digs;
- fun bin_of 0 = replicate zs 0
- | bin_of ~1 = replicate zs 1 @ [~1]
- | bin_of n = (n mod 2) :: bin_of (n div 2);
+ fun bin_of 0 = []
+ | bin_of ~1 = [~1]
+ | bin_of n = (n mod 2) :: bin_of (n div 2);
- fun term_of [] = const "Plus"
- | term_of [~1] = const "Minus"
- | term_of (b :: bs) = const "Bcons" $ term_of bs $ mk_bit b;
+ fun term_of [] = const "Pls"
+ | term_of [~1] = const "Min"
+ | term_of (b :: bs) = const "Cons" $ term_of bs $ mk_bit b;
in
term_of (bin_of (sign * (#1 (read_int digs))))
end;
fun dest_bin tm =
let
- fun bin_of (Const ("Plus", _)) = []
- | bin_of (Const ("Minus", _)) = [~1]
- | bin_of (Const ("Bcons", _) $ bs $ b) = dest_bit b :: bin_of bs
+ fun bin_of (Const ("Pls", _)) = []
+ | bin_of (Const ("Min", _)) = [~1]
+ | bin_of (Const ("Cons", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
fun int_of [] = 0
@@ -148,7 +148,7 @@
val rev_digs = bin_of tm;
val (sign, zs) =
(case rev rev_digs of
- ~1 :: bs => ("~", prefix_len (equal 1) bs)
+ ~1 :: bs => ("-", prefix_len (equal 1) bs)
| bs => ("", prefix_len (equal 0) bs));
val num = string_of_int (abs (int_of rev_digs));
in
@@ -159,7 +159,7 @@
(* translation of integer constant tokens to and from binary *)
fun int_tr (*"_Int"*) [t as Free (str, _)] =
- (const "integ_of_bin" $
+ (const "integ_of" $
(mk_bin str handle ERROR => raise TERM ("int_tr", [t])))
| int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts);
@@ -167,5 +167,5 @@
| int_tr' (*"integ_of"*) _ = raise Match;
in
val parse_translation = [("_Int", int_tr)];
- val print_translation = [("integ_of_bin", int_tr')];
+ val print_translation = [("integ_of", int_tr')];
end;
--- a/src/ZF/ex/twos_compl.ML Fri Sep 18 16:07:55 1998 +0200
+++ b/src/ZF/ex/twos_compl.ML Mon Sep 21 10:43:09 1998 +0200
@@ -5,12 +5,12 @@
ML code for Arithmetic on binary integers; the model for theory Bin
- The sign Plus stands for an infinite string of leading 0s.
- The sign Minus stands for an infinite string of leading 1s.
+ The sign Pls stands for an infinite string of leading 0s.
+ The sign Min stands for an infinite string of leading 1s.
See int_of_binary for the numerical interpretation. A number can have
-multiple representations, namely leading 0s with sign Plus and leading 1s with
-sign Minus. A number is in NORMAL FORM if it has no such extra bits.
+multiple representations, namely leading 0s with sign Pls and leading 1s with
+sign Min. A number is in NORMAL FORM if it has no such extra bits.
The representation expects that (m mod 2) is 0 or 1, even if m is negative;
For instance, ~5 div 2 = ~3 and ~5 mod 2 = 1; thus ~5 = (~3)*2 + 1
@@ -24,64 +24,64 @@
infix 5 $$ $$$
(*Recursive datatype of binary integers*)
-datatype bin = Plus | Minus | op $$ of bin * int;
+datatype bin = Pls | Min | $$ of bin * int;
(** Conversions between bin and int **)
-fun int_of_binary Plus = 0
- | int_of_binary Minus = ~1
+fun int_of_binary Pls = 0
+ | int_of_binary Min = ~1
| int_of_binary (w$$b) = 2 * int_of_binary w + b;
-fun binary_of_int 0 = Plus
- | binary_of_int ~1 = Minus
+fun binary_of_int 0 = Pls
+ | binary_of_int ~1 = Min
| binary_of_int n = binary_of_int (n div 2) $$ (n mod 2);
(*** Addition ***)
(*Attach a bit while preserving the normal form. Cases left as default
- are Plus$$$1 and Minus$$$0. *)
-fun Plus $$$ 0 = Plus
- | Minus $$$ 1 = Minus
+ are Pls$$$1 and Min$$$0. *)
+fun Pls $$$ 0 = Pls
+ | Min $$$ 1 = Min
| v $$$ x = v$$x;
(*Successor of an integer, assumed to be in normal form.
- If w$$1 is normal then w is not Minus, so bin_succ(w) $$ 0 is normal.
- But Minus$$0 is normal while Minus$$1 is not.*)
-fun bin_succ Plus = Plus$$1
- | bin_succ Minus = Plus
+ If w$$1 is normal then w is not Min, so bin_succ(w) $$ 0 is normal.
+ But Min$$0 is normal while Min$$1 is not.*)
+fun bin_succ Pls = Pls$$1
+ | bin_succ Min = Pls
| bin_succ (w$$1) = bin_succ(w) $$ 0
| bin_succ (w$$0) = w $$$ 1;
(*Predecessor of an integer, assumed to be in normal form.
- If w$$0 is normal then w is not Plus, so bin_pred(w) $$ 1 is normal.
- But Plus$$1 is normal while Plus$$0 is not.*)
-fun bin_pred Plus = Minus
- | bin_pred Minus = Minus$$0
+ If w$$0 is normal then w is not Pls, so bin_pred(w) $$ 1 is normal.
+ But Pls$$1 is normal while Pls$$0 is not.*)
+fun bin_pred Pls = Min
+ | bin_pred Min = Min$$0
| bin_pred (w$$1) = w $$$ 0
| bin_pred (w$$0) = bin_pred(w) $$ 1;
(*Sum of two binary integers in normal form.
Ensure last $$ preserves normal form! *)
-fun bin_add (Plus, w) = w
- | bin_add (Minus, w) = bin_pred w
- | bin_add (v$$x, Plus) = v$$x
- | bin_add (v$$x, Minus) = bin_pred (v$$x)
+fun bin_add (Pls, w) = w
+ | bin_add (Min, w) = bin_pred w
+ | bin_add (v$$x, Pls) = v$$x
+ | bin_add (v$$x, Min) = bin_pred (v$$x)
| bin_add (v$$x, w$$y) =
bin_add(v, if x+y=2 then bin_succ w else w) $$$ ((x+y) mod 2);
(*** Subtraction ***)
(*Unary minus*)
-fun bin_minus Plus = Plus
- | bin_minus Minus = Plus$$1
- | bin_minus (w$$1) = bin_pred (bin_minus(w) $$ 0)
+fun bin_minus Pls = Pls
+ | bin_minus Min = Pls$$1
+ | bin_minus (w$$1) = bin_pred (bin_minus(w) $$$ 0)
| bin_minus (w$$0) = bin_minus(w) $$ 0;
(*** Multiplication ***)
(*product of two bins; a factor of 0 might cause leading 0s in result*)
-fun bin_mult (Plus, _) = Plus
- | bin_mult (Minus, v) = bin_minus v
+fun bin_mult (Pls, _) = Pls
+ | bin_mult (Min, v) = bin_minus v
| bin_mult (w$$1, v) = bin_add(bin_mult(w,v) $$$ 0, v)
| bin_mult (w$$0, v) = bin_mult(w,v) $$$ 0;
@@ -96,7 +96,7 @@
else raise Match
end;
-fun bfact n = if n=0 then Plus$$1
+fun bfact n = if n=0 then Pls$$1
else bin_mult(binary_of_int n, bfact(n-1));
(*Examples...
@@ -107,7 +107,7 @@
(*leading zeros??*)
bin_add(binary_of_int 1234, binary_of_int ~1234);
-bin_mult(binary_of_int 1234, Plus);
+bin_mult(binary_of_int 1234, Pls);
(*leading ones??*)
bin_add(binary_of_int 1, binary_of_int ~2);