--- a/src/HOL/Integ/Bin.thy Fri Jun 30 10:58:03 2000 +0200
+++ b/src/HOL/Integ/Bin.thy Fri Jun 30 10:59:50 2000 +0200
@@ -31,7 +31,6 @@
bin_pred :: bin=>bin
bin_minus :: bin=>bin
bin_add,bin_mult :: [bin,bin]=>bin
- adding :: [bin,bool,bin]=>bin
(*NCons inserts a bit, suppressing leading 0s and 1s*)
primrec
@@ -72,14 +71,13 @@
primrec
bin_add_Pls "bin_add Pls w = w"
bin_add_Min "bin_add Min w = bin_pred w"
- bin_add_BIT "bin_add (v BIT x) w = adding v x w"
-
-primrec
- "adding v x Pls = v BIT x"
- "adding v x Min = bin_pred (v BIT x)"
- "adding v x (w BIT y) =
- NCons (bin_add v (if (x & y) then bin_succ w else w))
- (x~=y)"
+ 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 Pls w = Pls"
--- a/src/ZF/Integ/Bin.ML Fri Jun 30 10:58:03 2000 +0200
+++ b/src/ZF/Integ/Bin.ML Fri Jun 30 10:59:50 2000 +0200
@@ -68,7 +68,7 @@
AddTCs [bin_minus_type];
(*This proof is complicated by the mutual recursion*)
-Goal "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
+Goalw [bin_add_def] "v: bin ==> ALL w: bin. bin_add(v,w) : bin";
by (induct_tac "v" 1);
by (rtac ballI 3);
by (rename_tac "w'" 3);
@@ -130,23 +130,23 @@
(*** bin_add: binary addition ***)
-Goal "w: bin ==> bin_add(Pls,w) = w";
+Goalw [bin_add_def] "w: bin ==> bin_add(Pls,w) = w";
by (Asm_simp_tac 1);
qed "bin_add_Pls";
-Goal "w: bin ==> bin_add(Min,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_Min";
-Goal "bin_add(v BIT x,Pls) = v BIT x";
+Goalw [bin_add_def] "bin_add(v BIT x,Pls) = v BIT x";
by (Simp_tac 1);
qed "bin_add_BIT_Pls";
-Goal "bin_add(v BIT x,Min) = bin_pred(v BIT x)";
+Goalw [bin_add_def] "bin_add(v BIT x,Min) = bin_pred(v BIT x)";
by (Simp_tac 1);
qed "bin_add_BIT_Min";
-Goal "[| w: bin; y: bool |] \
+Goalw [bin_add_def] "[| w: bin; y: bool |] \
\ ==> bin_add(v BIT x, w BIT y) = \
\ NCons(bin_add(v, cond(x and y, bin_succ(w), w)), x xor y)";
by (Asm_simp_tac 1);
@@ -167,7 +167,7 @@
qed_spec_mp "integ_of_add";
-(*** bin_add: binary multiplication ***)
+(*** bin_mult: binary multiplication ***)
Goal "[| v: bin; w: bin |] \
\ ==> integ_of(bin_mult(v,w)) = integ_of(v) $* integ_of(w)";
@@ -240,7 +240,7 @@
(*Delete the original rewrites, with their clumsy conditional expressions*)
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT,
- NCons_Pls, NCons_Min, bin_add_BIT, bin_mult_BIT];
+ NCons_Pls, NCons_Min, bin_adder_BIT, bin_mult_BIT];
(*Hide the binary representation of integer constants*)
Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
--- a/src/ZF/Integ/Bin.thy Fri Jun 30 10:58:03 2000 +0200
+++ b/src/ZF/Integ/Bin.thy Fri Jun 30 10:59:50 2000 +0200
@@ -36,7 +36,7 @@
bin_pred :: i=>i
bin_minus :: i=>i
bin_add :: [i,i]=>i
- adding :: [i,i,i]=>i
+ bin_adder :: i=>i
bin_mult :: [i,i]=>i
primrec
@@ -70,20 +70,30 @@
"bin_minus (w BIT b) = cond(b, bin_pred(NCons(bin_minus(w),0)),
bin_minus(w) BIT 0)"
-(*Mutual recursion is not always sound, but it is for primitive recursion.*)
primrec (*sum*)
- bin_add_Pls
- "bin_add (Pls,w) = w"
- bin_add_Min
- "bin_add (Min,w) = bin_pred(w)"
- bin_add_BIT
- "bin_add (v BIT x,w) = adding(v,x,w)"
+ bin_adder_Pls
+ "bin_adder (Pls) = (lam w:bin. w)"
+ bin_adder_Min
+ "bin_adder (Min) = (lam w:bin. bin_pred(w))"
+ bin_adder_BIT
+ "bin_adder (v BIT x) =
+ (lam w:bin.
+ bin_case (v BIT x, bin_pred(v BIT x),
+ %w y. NCons(bin_adder (v) ` cond(x and y, bin_succ(w), w),
+ x xor y),
+ w))"
-primrec (*auxilliary function for sum*)
+(*The bin_case above replaces the following mutually recursive function:
+primrec
"adding (v,x,Pls) = v BIT x"
"adding (v,x,Min) = bin_pred(v BIT x)"
- "adding (v,x,w BIT y) = NCons(bin_add (v, cond(x and y, bin_succ(w), w)),
+ "adding (v,x,w BIT y) = NCons(bin_adder (v, cond(x and y, bin_succ(w), w)),
x xor y)"
+*)
+
+defs
+ bin_add_def "bin_add(v,w) == bin_adder(v)`w"
+
primrec
bin_mult_Pls