tuned proofs and declarations
authorhaftmann
Fri Dec 27 20:35:32 2013 +0100 (2013-12-27)
changeset 548690046711700c8
parent 54868 bab6cade3cc5
child 54870 1b5f2485757b
tuned proofs and declarations
src/HOL/Word/Bool_List_Representation.thy
src/HOL/Word/Misc_Numeric.thy
     1.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 14:35:14 2013 +0100
     1.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 20:35:32 2013 +0100
     1.3 @@ -245,7 +245,7 @@
     1.4  
     1.5  lemma len_bin_to_bl_aux: 
     1.6    "length (bin_to_bl_aux n w bs) = n + length bs"
     1.7 -  by (induct n arbitrary: w bs) auto
     1.8 +  by (fact size_bin_to_bl_aux)
     1.9  
    1.10  lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
    1.11    by (fact size_bin_to_bl) (* FIXME: duplicate *)
     2.1 --- a/src/HOL/Word/Misc_Numeric.thy	Fri Dec 27 14:35:14 2013 +0100
     2.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Fri Dec 27 20:35:32 2013 +0100
     2.3 @@ -8,7 +8,7 @@
     2.4  imports Main Parity
     2.5  begin
     2.6  
     2.7 -declare iszero_0 [iff]
     2.8 +declare iszero_0 [intro]
     2.9  
    2.10  lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith
    2.11    
    2.12 @@ -25,10 +25,11 @@
    2.13  lemma mod_2_neq_1_eq_eq_0:
    2.14    fixes k :: int
    2.15    shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
    2.16 -  by arith
    2.17 +  by (fact not_mod_2_eq_1_eq_0)
    2.18  
    2.19  lemma z1pmod2:
    2.20 -  "(2 * b + 1) mod 2 = (1::int)" by arith
    2.21 +  "(2 * b + 1) mod 2 = (1::int)"
    2.22 +  by arith
    2.23  
    2.24  lemma emep1:
    2.25    "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
    2.26 @@ -61,7 +62,7 @@
    2.27  
    2.28  lemma zless2:
    2.29    "0 < (2 :: int)"
    2.30 -  by arith
    2.31 +  by (fact zero_less_numeral)
    2.32  
    2.33  lemma zless2p:
    2.34    "0 < (2 ^ n :: int)"