author haftmann Fri, 27 Dec 2013 20:35:32 +0100 changeset 54869 0046711700c8 parent 54868 bab6cade3cc5 child 54870 1b5f2485757b
tuned proofs and declarations
--- a/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 14:35:14 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Dec 27 20:35:32 2013 +0100
@@ -245,7 +245,7 @@

lemma len_bin_to_bl_aux:
"length (bin_to_bl_aux n w bs) = n + length bs"
-  by (induct n arbitrary: w bs) auto
+  by (fact size_bin_to_bl_aux)

lemma len_bin_to_bl [simp]: "length (bin_to_bl n w) = n"
by (fact size_bin_to_bl) (* FIXME: duplicate *)
--- a/src/HOL/Word/Misc_Numeric.thy	Fri Dec 27 14:35:14 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy	Fri Dec 27 20:35:32 2013 +0100
@@ -8,7 +8,7 @@
imports Main Parity
begin

-declare iszero_0 [iff]
+declare iszero_0 [intro]

lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith

@@ -25,10 +25,11 @@
lemma mod_2_neq_1_eq_eq_0:
fixes k :: int
shows "k mod 2 \<noteq> 1 \<longleftrightarrow> k mod 2 = 0"
-  by arith
+  by (fact not_mod_2_eq_1_eq_0)

lemma z1pmod2:
-  "(2 * b + 1) mod 2 = (1::int)" by arith
+  "(2 * b + 1) mod 2 = (1::int)"
+  by arith

lemma emep1:
"even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
@@ -61,7 +62,7 @@

lemma zless2:
"0 < (2 :: int)"
-  by arith
+  by (fact zero_less_numeral)

lemma zless2p:
"0 < (2 ^ n :: int)"