# HG changeset patch
# User paulson
# Date 962355590 -7200
# Node ID 0c294bd701eade8aae4d3176b16220f0001f5b40
# Parent  eaaee6bd74ba9fd7ba73f230bf0457691ccce0b1
removed the mutual recursion from "bin_add"

diff -r eaaee6bd74ba -r 0c294bd701ea src/HOL/Integ/Bin.thy
--- 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"
diff -r eaaee6bd74ba -r 0c294bd701ea src/ZF/Integ/Bin.ML
--- 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];
diff -r eaaee6bd74ba -r 0c294bd701ea src/ZF/Integ/Bin.thy
--- 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