# HG changeset patch
# User paulson
# Date 901875047 -7200
# Node ID 8d132a14e722ff94804cf2c61e97690afe8a66aa
# Parent  4cb05273f7641880b44a52454e80734a250acbb5
tidied

diff -r 4cb05273f764 -r 8d132a14e722 src/HOL/Integ/Bin.ML
--- a/src/HOL/Integ/Bin.ML	Fri Jul 31 10:48:42 1998 +0200
+++ b/src/HOL/Integ/Bin.ML	Fri Jul 31 10:50:47 1998 +0200
@@ -138,8 +138,7 @@
                      integ_of_bin_norm_Bcons];
 val bin_simps = [iob_Plus,iob_Minus,iob_Bcons];
 
-Goal
-    "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
+Goal "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
 by (induct_tac "v" 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
 by (simp_tac (simpset() addsimps bin_add_simps) 1);
@@ -151,12 +150,7 @@
 by (etac disjE 1);
 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
 by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1);
-val integ_of_bin_add_lemma = result();
-
-Goal "integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w";
-by (cut_facts_tac [integ_of_bin_add_lemma] 1);
-by (Fast_tac 1);
-qed "integ_of_bin_add";
+qed_spec_mp "integ_of_bin_add";
 
 val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add,
                       integ_of_bin_norm_Bcons];
@@ -195,8 +189,7 @@
 
 Addsimps [zadd_assoc];
 
-Goal  
-    "(integ_of_bin x = integ_of_bin y) \ 
+Goal "(integ_of_bin x = integ_of_bin y) \ 
 \   = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)"; 
   by (simp_tac (HOL_ss addsimps
                 [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1); 
@@ -218,8 +211,7 @@
   by (Simp_tac 1);
 val iob_Minus_not_eq_0 = result(); 
 
-Goal 
-    "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; 
+Goal "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)"; 
   by (stac iob_Bcons 1);
   by (case_tac "x" 1); 
   by (ALLGOALS Asm_simp_tac); 
@@ -229,6 +221,7 @@
                (simpset() addsimps[zminus_zadd_distrib RS sym, 
                                 znat_add RS sym]))); 
   by (rtac notI 1); 
+  (*Add  Suc(Suc(n + n))  to both sides*)
   by (dres_inst_tac [("f","(% z. z +  $# Suc (Suc (n + n)))")] arg_cong 1); 
   by (Asm_full_simp_tac 1); 
 val iob_Bcons_eq_0 = result(); 
@@ -247,8 +240,7 @@
   by (stac iob_Minus 1); by (Simp_tac 1);
 val iob_Minus_lt_0 = result(); 
 
-Goal 
-    "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; 
+Goal "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)"; 
   by (stac iob_Bcons 1);
   by (case_tac "x" 1); 
   by (ALLGOALS Asm_simp_tac); 
@@ -262,8 +254,7 @@
   by (Simp_tac 1); 
 val iob_Bcons_lt_0 = result(); 
 
-Goal
-  "integ_of_bin x <= integ_of_bin y \
+Goal "integ_of_bin x <= integ_of_bin y \
 \  = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \
 \    | integ_of_bin (bin_add x (bin_minus y)) = $# 0)";
 by (simp_tac (HOL_ss addsimps