# HG changeset patch
# User paulson
# Date 957541774 -7200
# Node ID d289a68e74ea3eafc1752c22887472f3b30980d2
# Parent  b55e2354d71e873fd70730edc7e1dbf5c074652c
new lemmas about binary division

diff -r b55e2354d71e -r d289a68e74ea src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Fri May 05 12:51:33 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Fri May 05 17:49:34 2000 +0200
@@ -481,3 +481,44 @@
 
 (* Push int(.) inwards: *)
 Addsimps [int_Suc,zadd_int RS sym];
+
+Goal "(m+m = n+n) = (m = (n::int))";
+by Auto_tac;
+val lemma1 = result();
+
+Goal "m+m ~= int 1 + n + n";
+by Auto_tac;
+by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
+val lemma2 = result();
+
+Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
+\     (x=y & (((number_of v) ::int) = number_of w))"; 
+by (simp_tac (simpset_of Int.thy addsimps
+	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
+qed "eq_number_of_BIT_BIT"; 
+
+Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
+\     (x=False & (((number_of v) ::int) = number_of Pls))"; 
+by (simp_tac (simpset_of Int.thy addsimps
+	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
+by (res_inst_tac [("x", "number_of v")] spec 1);
+by Safe_tac;
+by (ALLGOALS Full_simp_tac);
+by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
+by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
+qed "eq_number_of_BIT_Pls"; 
+
+Goal "((number_of (v BIT x) ::int) = number_of Min) = \
+\     (x=True & (((number_of v) ::int) = number_of Min))"; 
+by (simp_tac (simpset_of Int.thy addsimps
+	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
+by (res_inst_tac [("x", "number_of v")] spec 1);
+by Auto_tac;
+by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
+by Auto_tac;
+qed "eq_number_of_BIT_Min"; 
+
+Goal "(number_of Pls ::int) ~= number_of Min"; 
+by Auto_tac;
+qed "eq_number_of_Pls_Min";