--- a/NEWS Thu Nov 17 21:58:10 2011 +0100
+++ b/NEWS Fri Nov 18 04:56:35 2011 +0100
@@ -29,6 +29,39 @@
*** HOL ***
+* Session HOL-Word: Discontinued many redundant theorems specific to type
+'a word. INCOMPATIBILITY, use the corresponding generic theorems instead.
+
+ word_sub_alt ~> word_sub_wi
+ word_add_alt ~> word_add_def
+ word_mult_alt ~> word_mult_def
+ word_minus_alt ~> word_minus_def
+ word_0_alt ~> word_0_wi
+ word_1_alt ~> word_1_wi
+ word_add_0 ~> add_0_left
+ word_add_0_right ~> add_0_right
+ word_mult_1 ~> mult_1_left
+ word_mult_1_right ~> mult_1_right
+ word_add_commute ~> add_commute
+ word_add_assoc ~> add_assoc
+ word_add_left_commute ~> add_left_commute
+ word_mult_commute ~> mult_commute
+ word_mult_assoc ~> mult_assoc
+ word_mult_left_commute ~> mult_left_commute
+ word_left_distrib ~> left_distrib
+ word_right_distrib ~> right_distrib
+ word_left_minus ~> left_minus
+ word_diff_0_right ~> diff_0_right
+ word_diff_self ~> diff_self
+ word_add_ac ~> add_ac
+ word_mult_ac ~> mult_ac
+ word_plus_ac0 ~> add_0_left add_0_right add_ac
+ word_times_ac1 ~> mult_1_left mult_1_right mult_ac
+ word_order_trans ~> order_trans
+ word_order_refl ~> order_refl
+ word_order_antisym ~> order_antisym
+ word_order_linear ~> linorder_linear
+
* Clarified attribute "mono_set": pure declararation without modifying
the result of the fact expression.
--- a/src/HOL/Groups.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Groups.thy Fri Nov 18 04:56:35 2011 +0100
@@ -284,7 +284,6 @@
finally show ?thesis .
qed
-
lemmas equals_zero_I = minus_unique (* legacy name *)
lemma minus_zero [simp]: "- 0 = 0"
@@ -413,6 +412,28 @@
unfolding eq_neg_iff_add_eq_0 [symmetric]
by (rule equation_minus_iff)
+lemma minus_diff_eq [simp]: "- (a - b) = b - a"
+ by (simp add: diff_minus minus_add)
+
+lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
+ by (simp add: diff_minus add_assoc)
+
+lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
+ by (auto simp add: diff_minus add_assoc)
+
+lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
+ by (auto simp add: diff_minus add_assoc)
+
+lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
+ by (simp add: diff_minus minus_add add_assoc)
+
+lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
+ by (fact right_minus_eq [symmetric])
+
+lemma diff_eq_diff_eq:
+ "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
+ by (simp add: eq_iff_diff_eq_0 [of a b] eq_iff_diff_eq_0 [of c d])
+
end
class ab_group_add = minus + uminus + comm_monoid_add +
@@ -440,40 +461,17 @@
"- (a + b) = - a + - b"
by (rule minus_unique) (simp add: add_ac)
-lemma minus_diff_eq [simp]:
- "- (a - b) = b - a"
-by (simp add: diff_minus add_commute)
-
-lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c"
-by (simp add: diff_minus add_ac)
-
lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b"
by (simp add: diff_minus add_ac)
-lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b"
-by (auto simp add: diff_minus add_assoc)
-
-lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c"
-by (auto simp add: diff_minus add_assoc)
-
lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)"
by (simp add: diff_minus add_ac)
-lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b"
-by (simp add: diff_minus add_ac)
-
-lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0"
-by (simp add: algebra_simps)
-
(* FIXME: duplicates right_minus_eq from class group_add *)
(* but only this one is declared as a simp rule. *)
lemma diff_eq_0_iff_eq [simp, no_atp]: "a - b = 0 \<longleftrightarrow> a = b"
by (rule right_minus_eq)
-lemma diff_eq_diff_eq:
- "a - b = c - d \<Longrightarrow> a = b \<longleftrightarrow> c = d"
- by (auto simp add: algebra_simps)
-
end
--- a/src/HOL/Import/HOL/real.imp Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Import/HOL/real.imp Fri Nov 18 04:56:35 2011 +0100
@@ -113,7 +113,7 @@
"REAL_NZ_IMP_LT" > "HOL4Real.real.REAL_NZ_IMP_LT"
"REAL_NOT_LT" > "HOL4Compat.real_lte"
"REAL_NOT_LE" > "Orderings.linorder_class.not_le"
- "REAL_NEG_SUB" > "Groups.ab_group_add_class.minus_diff_eq"
+ "REAL_NEG_SUB" > "Groups.group_add_class.minus_diff_eq"
"REAL_NEG_RMUL" > "Int.int_arith_rules_14"
"REAL_NEG_NEG" > "Groups.group_add_class.minus_minus"
"REAL_NEG_MUL2" > "Rings.ring_class.minus_mult_minus"
--- a/src/HOL/Library/Extended_Nat.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Library/Extended_Nat.thy Fri Nov 18 04:56:35 2011 +0100
@@ -174,11 +174,6 @@
end
-lemma plus_enat_0 [simp]:
- "0 + (q\<Colon>enat) = q"
- "(q\<Colon>enat) + 0 = q"
- by (simp_all add: plus_enat_def zero_enat_def split: enat.splits)
-
lemma plus_enat_number [simp]:
"(number_of k \<Colon> enat) + number_of l = (if k < Int.Pls then number_of l
else if l < Int.Pls then number_of k else number_of (k + l))"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 18 04:56:35 2011 +0100
@@ -3861,7 +3861,7 @@
then obtain y e where "e>0" and e:"ball y e \<subseteq> s" and y:"x = a + y" unfolding image_iff Bex_def mem_interior by auto
{ fix z have *:"a + y - z = y + a - z" by auto
assume "z\<in>ball x e"
- hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y ab_group_add_class.diff_diff_eq2 * by auto
+ hence "z - a \<in> s" using e[unfolded subset_eq, THEN bspec[where x="z - a"]] unfolding mem_ball dist_norm y group_add_class.diff_diff_eq2 * by auto
hence "z \<in> op + a ` s" unfolding image_iff by(auto intro!: bexI[where x="z - a"]) }
hence "ball x e \<subseteq> op + a ` s" unfolding subset_eq by auto
thus "x \<in> interior (op + a ` s)" unfolding mem_interior using `e>0` by auto
--- a/src/HOL/NSA/HyperDef.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/NSA/HyperDef.thy Fri Nov 18 04:56:35 2011 +0100
@@ -471,8 +471,8 @@
by transfer (rule power_one_right)
lemma hyperpow_two:
- "\<And>r. (r::'a::monoid_mult star) pow ((1::hypnat) + (1::hypnat)) = r * r"
-by transfer simp
+ "\<And>r. (r::'a::monoid_mult star) pow (2::hypnat) = r * r"
+by transfer (rule power2_eq_square)
lemma hyperpow_gt_zero:
"\<And>r n. (0::'a::{linordered_semidom} star) < r \<Longrightarrow> 0 < r pow n"
@@ -501,16 +501,16 @@
by transfer (rule power_mult_distrib)
lemma hyperpow_two_le [simp]:
- "(0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow (1 + 1)"
+ "\<And>r. (0::'a::{monoid_mult,linordered_ring_strict} star) \<le> r pow 2"
by (auto simp add: hyperpow_two zero_le_mult_iff)
lemma hrabs_hyperpow_two [simp]:
- "abs(x pow (1 + 1)) =
- (x::'a::{monoid_mult,linordered_ring_strict} star) pow (1 + 1)"
+ "abs(x pow 2) =
+ (x::'a::{monoid_mult,linordered_ring_strict} star) pow 2"
by (simp only: abs_of_nonneg hyperpow_two_le)
lemma hyperpow_two_hrabs [simp]:
- "abs(x::'a::{linordered_idom} star) pow (1 + 1) = x pow (1 + 1)"
+ "abs(x::'a::{linordered_idom} star) pow 2 = x pow 2"
by (simp add: hyperpow_hrabs)
text{*The precondition could be weakened to @{term "0\<le>x"}*}
@@ -519,12 +519,12 @@
by (simp add: mult_strict_mono order_less_imp_le)
lemma hyperpow_two_gt_one:
- "\<And>r::'a::{linordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow (1 + 1)"
-by transfer (simp add: power_gt1 del: power_Suc)
+ "\<And>r::'a::{linordered_semidom} star. 1 < r \<Longrightarrow> 1 < r pow 2"
+by transfer simp
lemma hyperpow_two_ge_one:
- "\<And>r::'a::{linordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow (1 + 1)"
-by transfer (simp add: one_le_power del: power_Suc)
+ "\<And>r::'a::{linordered_semidom} star. 1 \<le> r \<Longrightarrow> 1 \<le> r pow 2"
+by transfer (rule one_le_power)
lemma two_hyperpow_ge_one [simp]: "(1::hypreal) \<le> 2 pow n"
apply (rule_tac y = "1 pow n" in order_trans)
@@ -532,8 +532,8 @@
done
lemma hyperpow_minus_one2 [simp]:
- "!!n. -1 pow ((1 + 1)*n) = (1::hypreal)"
-by transfer (subst power_mult, simp)
+ "\<And>n. -1 pow (2*n) = (1::hypreal)"
+by transfer (rule power_m1_even)
lemma hyperpow_less_le:
"!!r n N. [|(0::hypreal) \<le> r; r \<le> 1; n < N|] ==> r pow N \<le> r pow n"
--- a/src/HOL/NSA/NSA.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/NSA/NSA.thy Fri Nov 18 04:56:35 2011 +0100
@@ -646,48 +646,20 @@
lemma approx_trans3: "[| x @= r; x @= s|] ==> r @= s"
by (blast intro: approx_sym approx_trans)
-lemma number_of_approx_reorient: "(number_of w @= x) = (x @= number_of w)"
-by (blast intro: approx_sym)
-
-lemma zero_approx_reorient: "(0 @= x) = (x @= 0)"
-by (blast intro: approx_sym)
-
-lemma one_approx_reorient: "(1 @= x) = (x @= 1)"
+lemma approx_reorient: "(x @= y) = (y @= x)"
by (blast intro: approx_sym)
-
-ML {*
-local
-(*** re-orientation, following HOL/Integ/Bin.ML
- We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
- ***)
-
-(*reorientation simprules using ==, for the following simproc*)
-val meta_zero_approx_reorient = @{thm zero_approx_reorient} RS eq_reflection;
-val meta_one_approx_reorient = @{thm one_approx_reorient} RS eq_reflection;
-val meta_number_of_approx_reorient = @{thm number_of_approx_reorient} RS eq_reflection
-
(*reorientation simplification procedure: reorients (polymorphic)
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
-fun reorient_proc sg _ (_ $ t $ u) =
- case u of
- Const(@{const_name Groups.zero}, _) => NONE
- | Const(@{const_name Groups.one}, _) => NONE
- | Const(@{const_name Int.number_of}, _) $ _ => NONE
- | _ => SOME (case t of
- Const(@{const_name Groups.zero}, _) => meta_zero_approx_reorient
- | Const(@{const_name Groups.one}, _) => meta_one_approx_reorient
- | Const(@{const_name Int.number_of}, _) $ _ =>
- meta_number_of_approx_reorient);
-
-in
-
-val approx_reorient_simproc = Simplifier.simproc_global @{theory}
- "reorient_simproc" ["0@=x", "1@=x", "number_of w @= x"] reorient_proc;
-
-end;
-
-Addsimprocs [approx_reorient_simproc];
+simproc_setup approx_reorient_simproc
+ ("0 @= x" | "1 @= y" | "number_of w @= z") =
+{*
+ let val rule = @{thm approx_reorient} RS eq_reflection
+ fun proc phi ss ct = case term_of ct of
+ _ $ t $ u => if can HOLogic.dest_number u then NONE
+ else if can HOLogic.dest_number t then SOME rule else NONE
+ | _ => NONE
+ in proc end
*}
lemma Infinitesimal_approx_minus: "(x-y \<in> Infinitesimal) = (x @= y)"
@@ -1874,9 +1846,11 @@
lemma st_number_of [simp]: "st (number_of w) = number_of w"
by (rule Reals_number_of [THEN st_SReal_eq])
-(*the theorem above for the special cases of zero and one*)
-lemma [simp]: "st 0 = 0" "st 1 = 1"
-by (simp_all add: st_SReal_eq)
+lemma st_0 [simp]: "st 0 = 0"
+by (simp add: st_SReal_eq)
+
+lemma st_1 [simp]: "st 1 = 1"
+by (simp add: st_SReal_eq)
lemma st_minus: "x \<in> HFinite \<Longrightarrow> st (- x) = - st x"
by (simp add: st_unique st_SReal st_approx_self approx_minus)
@@ -1934,14 +1908,12 @@
done
lemma st_zero_le: "[| 0 \<le> x; x \<in> HFinite |] ==> 0 \<le> st x"
-apply (subst numeral_0_eq_0 [symmetric])
-apply (rule st_number_of [THEN subst])
+apply (subst st_0 [symmetric])
apply (rule st_le, auto)
done
lemma st_zero_ge: "[| x \<le> 0; x \<in> HFinite |] ==> st x \<le> 0"
-apply (subst numeral_0_eq_0 [symmetric])
-apply (rule st_number_of [THEN subst])
+apply (subst st_0 [symmetric])
apply (rule st_le, auto)
done
--- a/src/HOL/NSA/StarDef.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy Fri Nov 18 04:56:35 2011 +0100
@@ -1008,6 +1008,9 @@
instance star :: (ring_char_0) ring_char_0 ..
+instance star :: (number_semiring) number_semiring
+by (intro_classes, simp only: star_number_def star_of_nat_def number_of_int)
+
instance star :: (number_ring) number_ring
by (intro_classes, simp only: star_number_def star_of_int_def number_of_eq)
--- a/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/SPARK/Examples/RIPEMD-160/Round.thy Fri Nov 18 04:56:35 2011 +0100
@@ -194,7 +194,7 @@
have "(?MM::int) = 2 ^ len_of TYPE(32)" by simp
show ?thesis
unfolding
- word_add_alt
+ word_add_def
uint_word_of_int_id[OF `0 <= a` `a <= ?M`]
uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
int_word_uint
@@ -237,7 +237,7 @@
by simp
show ?thesis
unfolding
- word_add_alt
+ word_add_def
uint_word_of_int_id[OF `0 <= a'` `a' <= ?M`]
uint_word_of_int_id[OF `0 <= ?X` `?X <= ?M`]
int_word_uint
--- a/src/HOL/Word/Bit_Int.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Word/Bit_Int.thy Fri Nov 18 04:56:35 2011 +0100
@@ -87,6 +87,8 @@
end
+subsubsection {* Basic simplification rules *}
+
lemma int_not_simps [simp]:
"NOT Int.Pls = Int.Min"
"NOT Int.Min = Int.Pls"
@@ -121,20 +123,6 @@
"(Int.Bit1 x) XOR (Int.Bit1 y) = Int.Bit0 (x XOR y)"
unfolding BIT_simps [symmetric] int_xor_Bits by simp_all
-lemma int_xor_x_simps':
- "w XOR (Int.Pls BIT 0) = w"
- "w XOR (Int.Min BIT 1) = NOT w"
- apply (induct w rule: bin_induct)
- apply simp_all[4]
- apply (unfold int_xor_Bits)
- apply clarsimp+
- done
-
-lemma int_xor_extra_simps [simp]:
- "w XOR Int.Pls = w"
- "w XOR Int.Min = NOT w"
- using int_xor_x_simps' by simp_all
-
lemma int_or_Pls [simp]:
"Int.Pls OR x = x"
by (unfold int_or_def) (simp add: bin_rec_PM)
@@ -154,20 +142,6 @@
"(Int.Bit1 x) OR (Int.Bit1 y) = Int.Bit1 (x OR y)"
unfolding BIT_simps [symmetric] int_or_Bits by simp_all
-lemma int_or_x_simps':
- "w OR (Int.Pls BIT 0) = w"
- "w OR (Int.Min BIT 1) = Int.Min"
- apply (induct w rule: bin_induct)
- apply simp_all[4]
- apply (unfold int_or_Bits)
- apply clarsimp+
- done
-
-lemma int_or_extra_simps [simp]:
- "w OR Int.Pls = w"
- "w OR Int.Min = Int.Min"
- using int_or_x_simps' by simp_all
-
lemma int_and_Pls [simp]:
"Int.Pls AND x = Int.Pls"
unfolding int_and_def by (simp add: bin_rec_PM)
@@ -187,19 +161,61 @@
"(Int.Bit1 x) AND (Int.Bit1 y) = Int.Bit1 (x AND y)"
unfolding BIT_simps [symmetric] int_and_Bits by simp_all
-lemma int_and_x_simps':
- "w AND (Int.Pls BIT 0) = Int.Pls"
- "w AND (Int.Min BIT 1) = w"
- apply (induct w rule: bin_induct)
- apply simp_all[4]
- apply (unfold int_and_Bits)
- apply clarsimp+
- done
+subsubsection {* Binary destructors *}
+
+lemma bin_rest_NOT [simp]: "bin_rest (NOT x) = NOT (bin_rest x)"
+ by (cases x rule: bin_exhaust, simp)
+
+lemma bin_last_NOT [simp]: "bin_last (NOT x) = NOT (bin_last x)"
+ by (cases x rule: bin_exhaust, simp)
+
+lemma bin_rest_AND [simp]: "bin_rest (x AND y) = bin_rest x AND bin_rest y"
+ by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
+
+lemma bin_last_AND [simp]: "bin_last (x AND y) = bin_last x AND bin_last y"
+ by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
+
+lemma bin_rest_OR [simp]: "bin_rest (x OR y) = bin_rest x OR bin_rest y"
+ by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
+
+lemma bin_last_OR [simp]: "bin_last (x OR y) = bin_last x OR bin_last y"
+ by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
+
+lemma bin_rest_XOR [simp]: "bin_rest (x XOR y) = bin_rest x XOR bin_rest y"
+ by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
+
+lemma bin_last_XOR [simp]: "bin_last (x XOR y) = bin_last x XOR bin_last y"
+ by (cases x rule: bin_exhaust, cases y rule: bin_exhaust, simp)
+
+lemma bit_NOT_eq_1_iff [simp]: "NOT (b::bit) = 1 \<longleftrightarrow> b = 0"
+ by (induct b, simp_all)
+
+lemma bit_AND_eq_1_iff [simp]: "(a::bit) AND b = 1 \<longleftrightarrow> a = 1 \<and> b = 1"
+ by (induct a, simp_all)
+
+lemma bin_nth_ops:
+ "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
+ "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
+ "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
+ "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
+ by (induct n) auto
+
+subsubsection {* Derived properties *}
+
+lemma int_xor_extra_simps [simp]:
+ "w XOR Int.Pls = w"
+ "w XOR Int.Min = NOT w"
+ by (auto simp add: bin_eq_iff bin_nth_ops)
+
+lemma int_or_extra_simps [simp]:
+ "w OR Int.Pls = w"
+ "w OR Int.Min = Int.Min"
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma int_and_extra_simps [simp]:
"w AND Int.Pls = Int.Pls"
"w AND Int.Min = w"
- using int_and_x_simps' by simp_all
+ by (auto simp add: bin_eq_iff bin_nth_ops)
(* commutativity of the above *)
lemma bin_ops_comm:
@@ -207,19 +223,16 @@
int_and_comm: "!!y::int. x AND y = y AND x" and
int_or_comm: "!!y::int. x OR y = y OR x" and
int_xor_comm: "!!y::int. x XOR y = y XOR x"
- apply (induct x rule: bin_induct)
- apply simp_all[6]
- apply (case_tac y rule: bin_exhaust, simp add: bit_ops_comm)+
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma bin_ops_same [simp]:
"(x::int) AND x = x"
"(x::int) OR x = x"
"(x::int) XOR x = Int.Pls"
- by (induct x rule: bin_induct) auto
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma int_not_not [simp]: "NOT (NOT (x::int)) = x"
- by (induct x rule: bin_induct) auto
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemmas bin_log_esimps =
int_and_extra_simps int_or_extra_simps int_xor_extra_simps
@@ -229,108 +242,64 @@
lemma bbw_ao_absorb:
"!!y::int. x AND (y OR x) = x & x OR (y AND x) = x"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac [!] y rule: bin_exhaust)
- apply auto
- apply (case_tac [!] bit)
- apply auto
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma bbw_ao_absorbs_other:
"x AND (x OR y) = x \<and> (y AND x) OR x = (x::int)"
"(y OR x) AND x = x \<and> x OR (x AND y) = (x::int)"
"(x OR y) AND x = x \<and> (x AND y) OR x = (x::int)"
- apply (auto simp: bbw_ao_absorb int_or_comm)
- apply (subst int_or_comm)
- apply (simp add: bbw_ao_absorb)
- apply (subst int_and_comm)
- apply (subst int_or_comm)
- apply (simp add: bbw_ao_absorb)
- apply (subst int_and_comm)
- apply (simp add: bbw_ao_absorb)
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemmas bbw_ao_absorbs [simp] = bbw_ao_absorb bbw_ao_absorbs_other
lemma int_xor_not:
"!!y::int. (NOT x) XOR y = NOT (x XOR y) &
x XOR (NOT y) = NOT (x XOR y)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac y rule: bin_exhaust, auto,
- case_tac b, auto)+
- done
-
-lemma bbw_assocs':
- "!!y z::int. (x AND y) AND z = x AND (y AND z) &
- (x OR y) OR z = x OR (y OR z) &
- (x XOR y) XOR z = x XOR (y XOR z)"
- apply (induct x rule: bin_induct)
- apply (auto simp: int_xor_not)
- apply (case_tac [!] y rule: bin_exhaust)
- apply (case_tac [!] z rule: bin_exhaust)
- apply (case_tac [!] bit)
- apply (case_tac [!] b)
- apply (auto simp del: BIT_simps)
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma int_and_assoc:
"(x AND y) AND (z::int) = x AND (y AND z)"
- by (simp add: bbw_assocs')
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma int_or_assoc:
"(x OR y) OR (z::int) = x OR (y OR z)"
- by (simp add: bbw_assocs')
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma int_xor_assoc:
"(x XOR y) XOR (z::int) = x XOR (y XOR z)"
- by (simp add: bbw_assocs')
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemmas bbw_assocs = int_and_assoc int_or_assoc int_xor_assoc
+(* BH: Why are these declared as simp rules??? *)
lemma bbw_lcs [simp]:
"(y::int) AND (x AND z) = x AND (y AND z)"
"(y::int) OR (x OR z) = x OR (y OR z)"
"(y::int) XOR (x XOR z) = x XOR (y XOR z)"
- apply (auto simp: bbw_assocs [symmetric])
- apply (auto simp: bin_ops_comm)
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma bbw_not_dist:
"!!y::int. NOT (x OR y) = (NOT x) AND (NOT y)"
"!!y::int. NOT (x AND y) = (NOT x) OR (NOT y)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac [!] y rule: bin_exhaust)
- apply (case_tac [!] bit, auto simp del: BIT_simps)
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma bbw_oa_dist:
"!!y z::int. (x AND y) OR z =
(x OR z) AND (y OR z)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac y rule: bin_exhaust)
- apply (case_tac z rule: bin_exhaust)
- apply (case_tac ba, auto simp del: BIT_simps)
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
lemma bbw_ao_dist:
"!!y z::int. (x OR y) AND z =
(x AND z) OR (y AND z)"
- apply (induct x rule: bin_induct)
- apply auto
- apply (case_tac y rule: bin_exhaust)
- apply (case_tac z rule: bin_exhaust)
- apply (case_tac ba, auto simp del: BIT_simps)
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops)
(*
Why were these declared simp???
declare bin_ops_comm [simp] bbw_assocs [simp]
*)
+subsubsection {* Interactions with arithmetic *}
+
lemma plus_and_or [rule_format]:
"ALL y::int. (x AND y) + (x OR y) = x + y"
apply (induct x rule: bin_induct)
@@ -359,20 +328,6 @@
lemmas int_and_le =
xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or]
-lemma bin_nth_ops:
- "!!x y. bin_nth (x AND y) n = (bin_nth x n & bin_nth y n)"
- "!!x y. bin_nth (x OR y) n = (bin_nth x n | bin_nth y n)"
- "!!x y. bin_nth (x XOR y) n = (bin_nth x n ~= bin_nth y n)"
- "!!x. bin_nth (NOT x) n = (~ bin_nth x n)"
- apply (induct n)
- apply safe
- apply (case_tac [!] x rule: bin_exhaust)
- apply (simp_all del: BIT_simps)
- apply (case_tac [!] y rule: bin_exhaust)
- apply (simp_all del: BIT_simps)
- apply (auto dest: not_B1_is_B0 intro: B1_ass_B0)
- done
-
(* interaction between bit-wise and arithmetic *)
(* good example of bin_induction *)
lemma bin_add_not: "x + NOT x = Int.Min"
@@ -382,34 +337,21 @@
apply (case_tac bit, auto)
done
-(* truncating results of bit-wise operations *)
+subsubsection {* Truncating results of bit-wise operations *}
+
lemma bin_trunc_ao:
"!!x y. (bintrunc n x) AND (bintrunc n y) = bintrunc n (x AND y)"
"!!x y. (bintrunc n x) OR (bintrunc n y) = bintrunc n (x OR y)"
- apply (induct n)
- apply auto
- apply (case_tac [!] x rule: bin_exhaust)
- apply (case_tac [!] y rule: bin_exhaust)
- apply auto
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
lemma bin_trunc_xor:
"!!x y. bintrunc n (bintrunc n x XOR bintrunc n y) =
bintrunc n (x XOR y)"
- apply (induct n)
- apply auto
- apply (case_tac [!] x rule: bin_exhaust)
- apply (case_tac [!] y rule: bin_exhaust)
- apply auto
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
lemma bin_trunc_not:
"!!x. bintrunc n (NOT (bintrunc n x)) = bintrunc n (NOT x)"
- apply (induct n)
- apply auto
- apply (case_tac [!] x rule: bin_exhaust)
- apply auto
- done
+ by (auto simp add: bin_eq_iff bin_nth_ops nth_bintr)
(* want theorems of the form of bin_trunc_xor *)
lemma bintr_bintr_i:
--- a/src/HOL/Word/Bit_Representation.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Word/Bit_Representation.thy Fri Nov 18 04:56:35 2011 +0100
@@ -270,6 +270,9 @@
lemmas bin_eqI = ext [THEN bin_nth_eq_iff [THEN iffD1], standard]
+lemma bin_eq_iff: "x = y \<longleftrightarrow> (\<forall>n. bin_nth x n = bin_nth y n)"
+ by (auto intro!: bin_nth_lem del: equalityI)
+
lemma bin_nth_Pls [simp]: "~ bin_nth Int.Pls n"
by (induct n) auto
--- a/src/HOL/Word/Bool_List_Representation.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Word/Bool_List_Representation.thy Fri Nov 18 04:56:35 2011 +0100
@@ -481,8 +481,6 @@
apply (case_tac v rule: bin_exhaust)
apply (case_tac w rule: bin_exhaust)
apply clarsimp
- apply (case_tac b)
- apply (case_tac ba, safe, simp_all)+
done
lemma bl_not_aux_bin [rule_format] :
@@ -491,9 +489,6 @@
apply (induct n)
apply clarsimp
apply clarsimp
- apply (case_tac w rule: bin_exhaust)
- apply (case_tac b)
- apply auto
done
lemmas bl_not_bin = bl_not_aux_bin
--- a/src/HOL/Word/Word.thy Thu Nov 17 21:58:10 2011 +0100
+++ b/src/HOL/Word/Word.thy Fri Nov 18 04:56:35 2011 +0100
@@ -30,6 +30,8 @@
code_datatype word_of_int
+subsection {* Random instance *}
+
notation fcomp (infixl "\<circ>>" 60)
notation scomp (infixl "\<circ>\<rightarrow>" 60)
@@ -118,10 +120,86 @@
translations
"case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
+subsection {* Type-definition locale instantiations *}
+
+lemmas word_size_gt_0 [iff] =
+ xtr1 [OF word_size len_gt_0, standard]
+lemmas lens_gt_0 = word_size_gt_0 len_gt_0
+lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
+
+lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
+ by (simp add: uints_def range_bintrunc)
+
+lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
+ by (simp add: sints_def range_sbintrunc)
+
+lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded
+ atLeast_def lessThan_def Collect_conj_eq [symmetric]]
+
+lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
+ unfolding atLeastLessThan_alt by auto
+
+lemma
+ uint_0:"0 <= uint x" and
+ uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
+ by (auto simp: uint [simplified])
+
+lemma uint_mod_same:
+ "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
+ by (simp add: int_mod_eq uint_lt uint_0)
+
+lemma td_ext_uint:
+ "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0)))
+ (%w::int. w mod 2 ^ len_of TYPE('a))"
+ apply (unfold td_ext_def')
+ apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
+ apply (simp add: uint_mod_same uint_0 uint_lt
+ word.uint_inverse word.Abs_word_inverse int_mod_lem)
+ done
+
+lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
+
+interpretation word_uint:
+ td_ext "uint::'a::len0 word \<Rightarrow> int"
+ word_of_int
+ "uints (len_of TYPE('a::len0))"
+ "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
+ by (rule td_ext_uint)
+
+lemmas td_uint = word_uint.td_thm
+
+lemmas td_ext_ubin = td_ext_uint
+ [simplified len_gt_0 no_bintr_alt1 [symmetric]]
+
+interpretation word_ubin:
+ td_ext "uint::'a::len0 word \<Rightarrow> int"
+ word_of_int
+ "uints (len_of TYPE('a::len0))"
+ "bintrunc (len_of TYPE('a::len0))"
+ by (rule td_ext_ubin)
+
+lemma split_word_all:
+ "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
+proof
+ fix x :: "'a word"
+ assume "\<And>x. PROP P (word_of_int x)"
+ hence "PROP P (word_of_int (uint x))" .
+ thus "PROP P x" by simp
+qed
subsection "Arithmetic operations"
-instantiation word :: (len0) "{number, uminus, minus, plus, one, zero, times, Divides.div, ord, bit}"
+definition
+ word_succ :: "'a :: len0 word => 'a word"
+where
+ "word_succ a = word_of_int (Int.succ (uint a))"
+
+definition
+ word_pred :: "'a :: len0 word => 'a word"
+where
+ "word_pred a = word_of_int (Int.pred (uint a))"
+
+instantiation word :: (len0) "{number, Divides.div, comm_monoid_mult, comm_ring}"
begin
definition
@@ -151,12 +229,116 @@
definition
word_number_of_def: "number_of w = word_of_int w"
+lemmas word_arith_wis =
+ word_add_def word_mult_def word_minus_def
+ word_succ_def word_pred_def word_0_wi word_1_wi
+
+lemmas arths =
+ bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
+ folded word_ubin.eq_norm, standard]
+
+lemma wi_homs:
+ shows
+ wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
+ wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
+ wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
+ wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
+ wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
+ by (auto simp: word_arith_wis arths)
+
+lemmas wi_hom_syms = wi_homs [symmetric]
+
+lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
+ unfolding word_sub_wi diff_minus
+ by (simp only : word_uint.Rep_inverse wi_hom_syms)
+
+lemmas word_diff_minus = word_sub_def [standard]
+
+lemma word_of_int_sub_hom:
+ "(word_of_int a) - word_of_int b = word_of_int (a - b)"
+ unfolding word_sub_def diff_minus by (simp only : wi_homs)
+
+lemmas new_word_of_int_homs =
+ word_of_int_sub_hom wi_homs word_0_wi word_1_wi
+
+lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
+
+lemmas word_of_int_hom_syms =
+ new_word_of_int_hom_syms [unfolded succ_def pred_def]
+
+lemmas word_of_int_homs =
+ new_word_of_int_homs [unfolded succ_def pred_def]
+
+lemmas word_of_int_add_hom = word_of_int_homs (2)
+lemmas word_of_int_mult_hom = word_of_int_homs (3)
+lemmas word_of_int_minus_hom = word_of_int_homs (4)
+lemmas word_of_int_succ_hom = word_of_int_homs (5)
+lemmas word_of_int_pred_hom = word_of_int_homs (6)
+lemmas word_of_int_0_hom = word_of_int_homs (7)
+lemmas word_of_int_1_hom = word_of_int_homs (8)
+
+instance
+ by default (auto simp: split_word_all word_of_int_homs algebra_simps)
+
+end
+
+lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
+ unfolding word_arith_wis
+ by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
+
+lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
+
+instance word :: (len) comm_ring_1
+ by (intro_classes) (simp add: lenw1_zero_neq_one)
+
+lemma word_of_nat: "of_nat n = word_of_int (int n)"
+ by (induct n) (auto simp add : word_of_int_hom_syms)
+
+lemma word_of_int: "of_int = word_of_int"
+ apply (rule ext)
+ apply (case_tac x rule: int_diff_cases)
+ apply (simp add: word_of_nat word_of_int_sub_hom)
+ done
+
+lemma word_number_of_eq:
+ "number_of w = (of_int w :: 'a :: len word)"
+ unfolding word_number_of_def word_of_int by auto
+
+instance word :: (len) number_ring
+ by (intro_classes) (simp add : word_number_of_eq)
+
+definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
+ "a udvd b = (EX n>=0. uint b = n * uint a)"
+
+
+subsection "Ordering"
+
+instantiation word :: (len0) linorder
+begin
+
definition
word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
definition
word_less_def: "x < y \<longleftrightarrow> x \<le> y \<and> x \<noteq> (y \<Colon> 'a word)"
+instance
+ by default (auto simp: word_less_def word_le_def)
+
+end
+
+definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
+ "a <=s b = (sint a <= sint b)"
+
+definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
+ "(x <s y) = (x <=s y & x ~= y)"
+
+
+subsection "Bit-wise operations"
+
+instantiation word :: (len0) bits
+begin
+
definition
word_and_def:
"(a::'a word) AND b = word_of_int (uint a AND uint b)"
@@ -173,36 +355,6 @@
word_not_def:
"NOT (a::'a word) = word_of_int (NOT (uint a))"
-instance ..
-
-end
-
-definition
- word_succ :: "'a :: len0 word => 'a word"
-where
- "word_succ a = word_of_int (Int.succ (uint a))"
-
-definition
- word_pred :: "'a :: len0 word => 'a word"
-where
- "word_pred a = word_of_int (Int.pred (uint a))"
-
-definition udvd :: "'a::len word => 'a::len word => bool" (infixl "udvd" 50) where
- "a udvd b = (EX n>=0. uint b = n * uint a)"
-
-definition word_sle :: "'a :: len word => 'a word => bool" ("(_/ <=s _)" [50, 51] 50) where
- "a <=s b = (sint a <= sint b)"
-
-definition word_sless :: "'a :: len word => 'a word => bool" ("(_/ <s _)" [50, 51] 50) where
- "(x <s y) = (x <=s y & x ~= y)"
-
-
-
-subsection "Bit-wise operations"
-
-instantiation word :: (len0) bits
-begin
-
definition
word_test_bit_def: "test_bit a = bin_nth (uint a)"
@@ -327,62 +479,6 @@
lemmas of_nth_def = word_set_bits_def
-lemmas word_size_gt_0 [iff] =
- xtr1 [OF word_size len_gt_0, standard]
-lemmas lens_gt_0 = word_size_gt_0 len_gt_0
-lemmas lens_not_0 [iff] = lens_gt_0 [THEN gr_implies_not0, standard]
-
-lemma uints_num: "uints n = {i. 0 \<le> i \<and> i < 2 ^ n}"
- by (simp add: uints_def range_bintrunc)
-
-lemma sints_num: "sints n = {i. - (2 ^ (n - 1)) \<le> i \<and> i < 2 ^ (n - 1)}"
- by (simp add: sints_def range_sbintrunc)
-
-lemmas atLeastLessThan_alt = atLeastLessThan_def [unfolded
- atLeast_def lessThan_def Collect_conj_eq [symmetric]]
-
-lemma mod_in_reps: "m > 0 \<Longrightarrow> y mod m : {0::int ..< m}"
- unfolding atLeastLessThan_alt by auto
-
-lemma
- uint_0:"0 <= uint x" and
- uint_lt: "uint (x::'a::len0 word) < 2 ^ len_of TYPE('a)"
- by (auto simp: uint [simplified])
-
-lemma uint_mod_same:
- "uint x mod 2 ^ len_of TYPE('a) = uint (x::'a::len0 word)"
- by (simp add: int_mod_eq uint_lt uint_0)
-
-lemma td_ext_uint:
- "td_ext (uint :: 'a word => int) word_of_int (uints (len_of TYPE('a::len0)))
- (%w::int. w mod 2 ^ len_of TYPE('a))"
- apply (unfold td_ext_def')
- apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
- apply (simp add: uint_mod_same uint_0 uint_lt
- word.uint_inverse word.Abs_word_inverse int_mod_lem)
- done
-
-lemmas int_word_uint = td_ext_uint [THEN td_ext.eq_norm, standard]
-
-interpretation word_uint:
- td_ext "uint::'a::len0 word \<Rightarrow> int"
- word_of_int
- "uints (len_of TYPE('a::len0))"
- "\<lambda>w. w mod 2 ^ len_of TYPE('a::len0)"
- by (rule td_ext_uint)
-
-lemmas td_uint = word_uint.td_thm
-
-lemmas td_ext_ubin = td_ext_uint
- [simplified len_gt_0 no_bintr_alt1 [symmetric]]
-
-interpretation word_ubin:
- td_ext "uint::'a::len0 word \<Rightarrow> int"
- word_of_int
- "uints (len_of TYPE('a::len0))"
- "bintrunc (len_of TYPE('a::len0))"
- by (rule td_ext_ubin)
-
lemma sint_sbintrunc':
"sint (word_of_int bin :: 'a word) =
(sbintrunc (len_of TYPE ('a :: len) - 1) bin)"
@@ -986,10 +1082,6 @@
interpretation signed: linorder "word_sle" "word_sless"
by (rule signed_linorder)
-lemmas word_arith_wis =
- word_add_def word_mult_def word_minus_def
- word_succ_def word_pred_def word_0_wi word_1_wi
-
lemma udvdI:
"0 \<le> n \<Longrightarrow> uint b = n * uint a \<Longrightarrow> a udvd b"
by (auto simp: udvd_def)
@@ -1118,67 +1210,14 @@
unfolding ucast_def word_1_wi
by (simp add: word_ubin.eq_norm int_one_bin bintrunc_minus_simps)
-(* abstraction preserves the operations
- (the definitions tell this for bins in range uint) *)
-
-lemmas arths =
- bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1],
- folded word_ubin.eq_norm, standard]
-
-lemma wi_homs:
- shows
- wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)" and
- wi_hom_mult: "word_of_int a * word_of_int b = word_of_int (a * b)" and
- wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
- wi_hom_succ: "word_succ (word_of_int a) = word_of_int (Int.succ a)" and
- wi_hom_pred: "word_pred (word_of_int a) = word_of_int (Int.pred a)"
- by (auto simp: word_arith_wis arths)
-
-lemmas wi_hom_syms = wi_homs [symmetric]
-
-lemma word_sub_def: "a - b = a + - (b :: 'a :: len0 word)"
- unfolding word_sub_wi diff_minus
- by (simp only : word_uint.Rep_inverse wi_hom_syms)
-
-lemmas word_diff_minus = word_sub_def [standard]
-
-lemma word_of_int_sub_hom:
- "(word_of_int a) - word_of_int b = word_of_int (a - b)"
- unfolding word_sub_def diff_minus by (simp only : wi_homs)
-
-lemmas new_word_of_int_homs =
- word_of_int_sub_hom wi_homs word_0_wi word_1_wi
-
-lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric, standard]
-
-lemmas word_of_int_hom_syms =
- new_word_of_int_hom_syms [unfolded succ_def pred_def]
-
-lemmas word_of_int_homs =
- new_word_of_int_homs [unfolded succ_def pred_def]
-
-lemmas word_of_int_add_hom = word_of_int_homs (2)
-lemmas word_of_int_mult_hom = word_of_int_homs (3)
-lemmas word_of_int_minus_hom = word_of_int_homs (4)
-lemmas word_of_int_succ_hom = word_of_int_homs (5)
-lemmas word_of_int_pred_hom = word_of_int_homs (6)
-lemmas word_of_int_0_hom = word_of_int_homs (7)
-lemmas word_of_int_1_hom = word_of_int_homs (8)
-
(* now, to get the weaker results analogous to word_div/mod_def *)
lemmas word_arith_alts =
word_sub_wi [unfolded succ_def pred_def, standard]
word_arith_wis [unfolded succ_def pred_def, standard]
-lemmas word_sub_alt = word_arith_alts (1)
-lemmas word_add_alt = word_arith_alts (2)
-lemmas word_mult_alt = word_arith_alts (3)
-lemmas word_minus_alt = word_arith_alts (4)
lemmas word_succ_alt = word_arith_alts (5)
lemmas word_pred_alt = word_arith_alts (6)
-lemmas word_0_alt = word_arith_alts (7)
-lemmas word_1_alt = word_arith_alts (8)
subsection "Transferring goals from words to ints"
@@ -1236,70 +1275,13 @@
"\<exists>y. x = word_of_int y"
by (rule_tac x="uint x" in exI) simp
-lemma word_arith_eqs:
- fixes a :: "'a::len0 word"
- fixes b :: "'a::len0 word"
- shows
- word_add_0: "0 + a = a" and
- word_add_0_right: "a + 0 = a" and
- word_mult_1: "1 * a = a" and
- word_mult_1_right: "a * 1 = a" and
- word_add_commute: "a + b = b + a" and
- word_add_assoc: "a + b + c = a + (b + c)" and
- word_add_left_commute: "a + (b + c) = b + (a + c)" and
- word_mult_commute: "a * b = b * a" and
- word_mult_assoc: "a * b * c = a * (b * c)" and
- word_mult_left_commute: "a * (b * c) = b * (a * c)" and
- word_left_distrib: "(a + b) * c = a * c + b * c" and
- word_right_distrib: "a * (b + c) = a * b + a * c" and
- word_left_minus: "- a + a = 0" and
- word_diff_0_right: "a - 0 = a" and
- word_diff_self: "a - a = 0"
- using word_of_int_Ex [of a]
- word_of_int_Ex [of b]
- word_of_int_Ex [of c]
- by (auto simp: word_of_int_hom_syms [symmetric]
- add_0_right add_commute add_assoc add_left_commute
- mult_commute mult_assoc mult_left_commute
- left_distrib right_distrib)
-
-lemmas word_add_ac = word_add_commute word_add_assoc word_add_left_commute
-lemmas word_mult_ac = word_mult_commute word_mult_assoc word_mult_left_commute
-
-lemmas word_plus_ac0 = word_add_0 word_add_0_right word_add_ac
-lemmas word_times_ac1 = word_mult_1 word_mult_1_right word_mult_ac
-
subsection "Order on fixed-length words"
-lemma word_order_trans: "x <= y \<Longrightarrow> y <= z \<Longrightarrow> x <= (z :: 'a :: len0 word)"
- unfolding word_le_def by auto
-
-lemma word_order_refl: "z <= (z :: 'a :: len0 word)"
- unfolding word_le_def by auto
-
-lemma word_order_antisym: "x <= y \<Longrightarrow> y <= x \<Longrightarrow> x = (y :: 'a :: len0 word)"
- unfolding word_le_def by (auto intro!: word_uint.Rep_eqD)
-
-lemma word_order_linear:
- "y <= x | x <= (y :: 'a :: len0 word)"
- unfolding word_le_def by auto
-
lemma word_zero_le [simp] :
"0 <= (y :: 'a :: len0 word)"
unfolding word_le_def by auto
-instance word :: (len0) semigroup_add
- by intro_classes (simp add: word_add_assoc)
-
-instance word :: (len0) linorder
- by intro_classes (auto simp: word_less_def word_le_def)
-
-instance word :: (len0) ring
- by intro_classes
- (auto simp: word_arith_eqs word_diff_minus
- word_diff_self [unfolded word_diff_minus])
-
lemma word_m1_ge [simp] : "word_pred 0 >= y"
unfolding word_le_def
by (simp only : word_pred_0_n1 word_uint.eq_norm m1mod2k) auto
@@ -1354,12 +1336,6 @@
lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
-lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
- unfolding word_arith_wis
- by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
-
-lemmas lenw1_zero_neq_one = len_gt_0 [THEN word_zero_neq_one]
-
lemma no_no [simp] : "number_of (number_of b) = number_of b"
by (simp add: number_of_eq)
@@ -1513,7 +1489,7 @@
lemma no_olen_add':
fixes x :: "'a::len0 word"
shows "(x \<le> y + x) = (uint y + uint x < 2 ^ len_of TYPE('a))"
- by (simp add: word_add_ac add_ac no_olen_add)
+ by (simp add: add_ac no_olen_add)
lemmas olen_add_eqv = trans [OF no_olen_add no_olen_add' [symmetric], standard]
@@ -1729,30 +1705,6 @@
subsection "Arithmetic type class instantiations"
-instance word :: (len0) comm_monoid_add ..
-
-instance word :: (len0) comm_monoid_mult
- apply (intro_classes)
- apply (simp add: word_mult_commute)
- apply (simp add: word_mult_1)
- done
-
-instance word :: (len0) comm_semiring
- by (intro_classes) (simp add : word_left_distrib)
-
-instance word :: (len0) ab_group_add ..
-
-instance word :: (len0) comm_ring ..
-
-instance word :: (len) comm_semiring_1
- by (intro_classes) (simp add: lenw1_zero_neq_one)
-
-instance word :: (len) comm_ring_1 ..
-
-instance word :: (len0) comm_semiring_0 ..
-
-instance word :: (len0) order ..
-
(* note that iszero_def is only for class comm_semiring_1_cancel,
which requires word length >= 1, ie 'a :: len word *)
lemma zero_bintrunc:
@@ -1766,26 +1718,10 @@
lemmas word_le_0_iff [simp] =
word_zero_le [THEN leD, THEN linorder_antisym_conv1]
-lemma word_of_nat: "of_nat n = word_of_int (int n)"
- by (induct n) (auto simp add : word_of_int_hom_syms)
-
-lemma word_of_int: "of_int = word_of_int"
- apply (rule ext)
- apply (case_tac x rule: int_diff_cases)
- apply (simp add: word_of_nat word_of_int_sub_hom)
- done
-
lemma word_of_int_nat:
"0 <= x \<Longrightarrow> word_of_int x = of_nat (nat x)"
by (simp add: of_nat_nat word_of_int)
-lemma word_number_of_eq:
- "number_of w = (of_int w :: 'a :: len word)"
- unfolding word_number_of_def word_of_int by auto
-
-instance word :: (len) number_ring
- by (intro_classes) (simp add : word_number_of_eq)
-
lemma iszero_word_no [simp] :
"iszero (number_of bin :: 'a :: len word) =
iszero (number_of (bintrunc (len_of TYPE('a)) bin) :: int)"
@@ -4429,7 +4365,7 @@
lemma shiftr1_1 [simp]:
"shiftr1 (1::'a::len word) = 0"
- by (simp add: shiftr1_def word_0_alt)
+ by (simp add: shiftr1_def word_0_wi)
lemma shiftr_1[simp]:
"(1::'a::len word) >> n = (if n = 0 then 1 else 0)"