new lemmas about binary division
authorpaulson
Fri May 05 17:49:34 2000 +0200 (2000-05-05)
changeset 8798d289a68e74ea
parent 8797 b55e2354d71e
child 8799 89e9deef4bcb
new lemmas about binary division
src/HOL/Integ/NatBin.ML
     1.1 --- a/src/HOL/Integ/NatBin.ML	Fri May 05 12:51:33 2000 +0200
     1.2 +++ b/src/HOL/Integ/NatBin.ML	Fri May 05 17:49:34 2000 +0200
     1.3 @@ -481,3 +481,44 @@
     1.4  
     1.5  (* Push int(.) inwards: *)
     1.6  Addsimps [int_Suc,zadd_int RS sym];
     1.7 +
     1.8 +Goal "(m+m = n+n) = (m = (n::int))";
     1.9 +by Auto_tac;
    1.10 +val lemma1 = result();
    1.11 +
    1.12 +Goal "m+m ~= int 1 + n + n";
    1.13 +by Auto_tac;
    1.14 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
    1.15 +by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
    1.16 +val lemma2 = result();
    1.17 +
    1.18 +Goal "((number_of (v BIT x) ::int) = number_of (w BIT y)) = \
    1.19 +\     (x=y & (((number_of v) ::int) = number_of w))"; 
    1.20 +by (simp_tac (simpset_of Int.thy addsimps
    1.21 +	       [number_of_BIT, lemma1, lemma2, eq_commute]) 1); 
    1.22 +qed "eq_number_of_BIT_BIT"; 
    1.23 +
    1.24 +Goal "((number_of (v BIT x) ::int) = number_of Pls) = \
    1.25 +\     (x=False & (((number_of v) ::int) = number_of Pls))"; 
    1.26 +by (simp_tac (simpset_of Int.thy addsimps
    1.27 +	       [number_of_BIT, number_of_Pls, eq_commute]) 1); 
    1.28 +by (res_inst_tac [("x", "number_of v")] spec 1);
    1.29 +by Safe_tac;
    1.30 +by (ALLGOALS Full_simp_tac);
    1.31 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
    1.32 +by (full_simp_tac (simpset() addsimps [zmod_zadd1_eq]) 1); 
    1.33 +qed "eq_number_of_BIT_Pls"; 
    1.34 +
    1.35 +Goal "((number_of (v BIT x) ::int) = number_of Min) = \
    1.36 +\     (x=True & (((number_of v) ::int) = number_of Min))"; 
    1.37 +by (simp_tac (simpset_of Int.thy addsimps
    1.38 +	       [number_of_BIT, number_of_Min, eq_commute]) 1); 
    1.39 +by (res_inst_tac [("x", "number_of v")] spec 1);
    1.40 +by Auto_tac;
    1.41 +by (dres_inst_tac [("f", "%x. x mod #2")] arg_cong 1);
    1.42 +by Auto_tac;
    1.43 +qed "eq_number_of_BIT_Min"; 
    1.44 +
    1.45 +Goal "(number_of Pls ::int) ~= number_of Min"; 
    1.46 +by Auto_tac;
    1.47 +qed "eq_number_of_Pls_Min";