# HG changeset patch # User paulson # Date 906367389 -7200 # Node ID 4327eec06849107c408a36c1d224a819a3bc6695 # Parent 7f52fb755581c904667fd51abb6e9ae9d5f33fdd much renaming and tidying diff -r 7f52fb755581 -r 4327eec06849 src/HOL/Integ/Bin.ML --- 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] diff -r 7f52fb755581 -r 4327eec06849 src/HOL/Integ/Bin.thy --- 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 diff -r 7f52fb755581 -r 4327eec06849 src/ZF/ex/Bin.ML --- 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(); diff -r 7f52fb755581 -r 4327eec06849 src/ZF/ex/Bin.thy --- 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; diff -r 7f52fb755581 -r 4327eec06849 src/ZF/ex/twos_compl.ML --- 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);