--- a/src/HOL/Word/Bool_List_Representation.thy Sat Dec 28 17:51:54 2013 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Sat Dec 28 21:06:22 2013 +0100
@@ -1062,10 +1062,35 @@
lemma bin_rsplit_aux_len_le [rule_format] :
"\<forall>ws m. n \<noteq> 0 \<longrightarrow> ws = bin_rsplit_aux n nw w bs \<longrightarrow>
length ws \<le> m \<longleftrightarrow> nw + length bs * n \<le> m * n"
- apply (induct n nw w bs rule: bin_rsplit_aux.induct)
- apply (subst bin_rsplit_aux.simps)
- apply (simp add: lrlem Let_def split: prod.split)
- done
+proof -
+ { fix i j j' k k' m :: nat and R
+ assume d: "(i::nat) \<le> j \<or> m < j'"
+ assume R1: "i * k \<le> j * k \<Longrightarrow> R"
+ assume R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
+ have "R" using d
+ apply safe
+ apply (rule R1, erule mult_le_mono1)
+ apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
+ done
+ } note A = this
+ { fix sc m n lb :: nat
+ have "(0::nat) < sc \<Longrightarrow> sc - n + (n + lb * n) \<le> m * n \<longleftrightarrow> sc + lb * n \<le> m * n"
+ apply safe
+ apply arith
+ apply (case_tac "sc >= n")
+ apply arith
+ apply (insert linorder_le_less_linear [of m lb])
+ apply (erule_tac k2=n and k'2=n in A)
+ apply arith
+ apply simp
+ done
+ } note B = this
+ show ?thesis
+ apply (induct n nw w bs rule: bin_rsplit_aux.induct)
+ apply (subst bin_rsplit_aux.simps)
+ apply (simp add: B Let_def split: prod.split)
+ done
+qed
lemma bin_rsplit_len_le:
"n \<noteq> 0 --> ws = bin_rsplit n (nw, w) --> (length ws <= m) = (nw <= m * n)"
--- a/src/HOL/Word/Misc_Numeric.thy Sat Dec 28 17:51:54 2013 +0100
+++ b/src/HOL/Word/Misc_Numeric.thy Sat Dec 28 21:06:22 2013 +0100
@@ -10,17 +10,29 @@
declare iszero_0 [intro]
-lemma min_pm [simp]: "min a b + (a - b) = (a :: nat)" by arith
+lemma min_pm [simp]:
+ "min a b + (a - b) = (a :: nat)"
+ by arith
-lemmas min_pm1 [simp] = trans [OF add_commute min_pm]
+lemma min_pm1 [simp]:
+ "a - b + min a b = (a :: nat)"
+ by arith
-lemma rev_min_pm [simp]: "min b a + (a - b) = (a::nat)" by arith
+lemma rev_min_pm [simp]:
+ "min b a + (a - b) = (a :: nat)"
+ by arith
-lemmas rev_min_pm1 [simp] = trans [OF add_commute rev_min_pm]
+lemma rev_min_pm1 [simp]:
+ "a - b + min b a = (a :: nat)"
+ by arith
-lemma min_minus [simp] : "min m (m - k) = (m - k :: nat)" by arith
+lemma min_minus [simp]:
+ "min m (m - k) = (m - k :: nat)"
+ by arith
-lemmas min_minus' [simp] = trans [OF min.commute min_minus]
+lemma min_minus' [simp]:
+ "min (m - k) m = (m - k :: nat)"
+ by arith
lemma mod_2_neq_1_eq_eq_0:
fixes k :: int
@@ -28,37 +40,30 @@
by (fact not_mod_2_eq_1_eq_0)
lemma z1pmod2:
- "(2 * b + 1) mod 2 = (1::int)"
+ fixes b :: int
+ shows "(2 * b + 1) mod 2 = (1::int)"
+ by arith
+
+lemma diff_le_eq':
+ "a - b \<le> c \<longleftrightarrow> a \<le> b + (c::int)"
by arith
lemma emep1:
- "even n ==> even d ==> 0 <= d ==> (n + 1) mod (d :: int) = (n mod d) + 1"
- apply (simp add: add_commute)
- apply (safe dest!: even_equiv_def [THEN iffD1])
- apply (subst pos_zmod_mult_2)
- apply arith
- apply (simp add: mod_mult_mult1)
- done
+ fixes n d :: int
+ shows "even n \<Longrightarrow> even d \<Longrightarrow> 0 \<le> d \<Longrightarrow> (n + 1) mod d = (n mod d) + 1"
+ by (auto simp add: pos_zmod_mult_2 add_commute even_equiv_def)
+
+lemma int_mod_ge:
+ "a < n \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> a \<le> a mod n"
+ by (metis dual_order.trans le_cases mod_pos_pos_trivial pos_mod_conj)
-lemma int_mod_lem:
- "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
- apply safe
- apply (erule (1) mod_pos_pos_trivial)
- apply (erule_tac [!] subst)
- apply auto
- done
+lemma int_mod_ge':
+ "b < 0 \<Longrightarrow> 0 < (n :: int) \<Longrightarrow> b + n \<le> b mod n"
+ by (metis add_less_same_cancel2 int_mod_ge mod_add_self2)
-lemma int_mod_ge: "a < n ==> 0 < (n :: int) ==> a <= a mod n"
- apply (cases "0 <= a")
- apply (drule (1) mod_pos_pos_trivial)
- apply simp
- apply (rule order_trans [OF _ pos_mod_sign])
- apply simp
- apply assumption
- done
-
-lemma int_mod_ge': "b < 0 ==> 0 < (n :: int) ==> b + n <= b mod n"
- by (rule int_mod_ge [where a = "b + n" and n = n, simplified])
+lemma int_mod_le':
+ "(0::int) \<le> b - n \<Longrightarrow> b mod n \<le> b - n"
+ by (metis minus_mod_self2 zmod_le_nonneg_dividend)
lemma zless2:
"0 < (2 :: int)"
@@ -72,13 +77,8 @@
"0 \<le> (2 ^ n :: int)"
by arith
-lemma int_mod_le': "(0::int) <= b - n ==> b mod n <= b - n"
- using zmod_le_nonneg_dividend [of "b - n" "n"] by simp
-
-lemma diff_le_eq': "(a - b \<le> c) = (a \<le> b + (c::int))" by arith
-
lemma m1mod2k:
- "-1 mod 2 ^ n = (2 ^ n - 1 :: int)"
+ "- 1 mod 2 ^ n = (2 ^ n - 1 :: int)"
using zless2p by (rule zmod_minus1)
lemma p1mod22k':
@@ -91,26 +91,12 @@
shows "(2 * b + 1) mod (2 * 2 ^ n) = 2 * (b mod 2 ^ n) + 1"
by (simp add: p1mod22k' add_commute)
-lemma lrlem':
- assumes d: "(i::nat) \<le> j \<or> m < j'"
- assumes R1: "i * k \<le> j * k \<Longrightarrow> R"
- assumes R2: "Suc m * k' \<le> j' * k' \<Longrightarrow> R"
- shows "R" using d
+lemma int_mod_lem:
+ "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
apply safe
- apply (rule R1, erule mult_le_mono1)
- apply (rule R2, erule Suc_le_eq [THEN iffD2 [THEN mult_le_mono1]])
- done
-
-lemma lrlem: "(0::nat) < sc ==>
- (sc - n + (n + lb * n) <= m * n) = (sc + lb * n <= m * n)"
- apply safe
- apply arith
- apply (case_tac "sc >= n")
- apply arith
- apply (insert linorder_le_less_linear [of m lb])
- apply (erule_tac k=n and k'=n in lrlem')
- apply arith
- apply simp
+ apply (erule (1) mod_pos_pos_trivial)
+ apply (erule_tac [!] subst)
+ apply auto
done
end
--- a/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 28 17:51:54 2013 +0100
+++ b/src/HOL/Word/Word_Miscellaneous.thy Sat Dec 28 21:06:22 2013 +0100
@@ -253,14 +253,6 @@
"(x :: nat) < z ==> (x - y) mod z = x - y"
by (rule nat_mod_eq') arith
-lemma int_mod_lem:
- "(0 :: int) < n ==> (0 <= b & b < n) = (b mod n = b)"
- apply safe
- apply (erule (1) mod_pos_pos_trivial)
- apply (erule_tac [!] subst)
- apply auto
- done
-
lemma int_mod_eq:
"(0 :: int) <= b ==> b < n ==> a mod n = b mod n ==> a mod n = b"
by clarsimp (rule mod_pos_pos_trivial)