--- a/src/HOL/Library/Type_Length.thy Sat Oct 19 16:09:39 2019 +0200
+++ b/src/HOL/Library/Type_Length.thy Sat Oct 19 16:16:24 2019 +0200
@@ -70,4 +70,37 @@
instance bit1 :: (len0) len
by standard simp
+instantiation Enum.finite_1 :: len
+begin
+
+definition
+ "len_of_finite_1 (x :: Enum.finite_1 itself) \<equiv> (1 :: nat)"
+
+instance
+ by standard (auto simp: len_of_finite_1_def)
+
end
+
+instantiation Enum.finite_2 :: len
+begin
+
+definition
+ "len_of_finite_2 (x :: Enum.finite_2 itself) \<equiv> (2 :: nat)"
+
+instance
+ by standard (auto simp: len_of_finite_2_def)
+
+end
+
+instantiation Enum.finite_3 :: len
+begin
+
+definition
+ "len_of_finite_3 (x :: Enum.finite_3 itself) \<equiv> (4 :: nat)"
+
+instance
+ by standard (auto simp: len_of_finite_3_def)
+
+end
+
+end
--- a/src/HOL/Rings.thy Sat Oct 19 16:09:39 2019 +0200
+++ b/src/HOL/Rings.thy Sat Oct 19 16:16:24 2019 +0200
@@ -1684,6 +1684,15 @@
lemma minus_mod_eq_mult_div: "a - a mod b = b * (a div b)"
by (rule add_implies_diff [symmetric]) (fact mult_div_mod_eq)
+lemma mod_0_imp_dvd [dest!]:
+ "b dvd a" if "a mod b = 0"
+proof -
+ have "b dvd (a div b) * b" by simp
+ also have "(a div b) * b = a"
+ using div_mult_mod_eq [of a b] by (simp add: that)
+ finally show ?thesis .
+qed
+
lemma [nitpick_unfold]:
"a mod b = a - a div b * b"
by (fact minus_div_mult_eq_mod [symmetric])
@@ -1718,15 +1727,6 @@
"b mod a = 0" if "a dvd b"
using that minus_div_mult_eq_mod [of b a] by simp
-lemma mod_0_imp_dvd [dest!]:
- "b dvd a" if "a mod b = 0"
-proof -
- have "b dvd (a div b) * b" by simp
- also have "(a div b) * b = a"
- using div_mult_mod_eq [of a b] by (simp add: that)
- finally show ?thesis .
-qed
-
lemma mod_eq_0_iff_dvd:
"a mod b = 0 \<longleftrightarrow> b dvd a"
by (auto intro: mod_0_imp_dvd)
--- a/src/HOL/Word/Word.thy Sat Oct 19 16:09:39 2019 +0200
+++ b/src/HOL/Word/Word.thy Sat Oct 19 16:16:24 2019 +0200
@@ -286,6 +286,12 @@
end
+quickcheck_generator word
+ constructors:
+ "zero_class.zero :: ('a::len) word",
+ "numeral :: num \<Rightarrow> ('a::len) word",
+ "uminus :: ('a::len) word \<Rightarrow> ('a::len) word"
+
text \<open>Legacy theorems:\<close>
lemma word_arith_wis [code]:
@@ -1279,6 +1285,21 @@
unfolding unat_def word_less_alt
by (rule nat_less_eq_zless [symmetric]) simp
+lemmas unat_mono = word_less_nat_alt [THEN iffD1]
+
+instance word :: (len) wellorder
+proof
+ fix P :: "'a word \<Rightarrow> bool" and a
+ assume *: "(\<And>b. (\<And>a. a < b \<Longrightarrow> P a) \<Longrightarrow> P b)"
+ have "wf (measure unat)" ..
+ moreover have "{(a, b :: ('a::len) word). a < b} \<subseteq> measure unat"
+ by (auto simp add: word_less_nat_alt)
+ ultimately have "wf {(a, b :: ('a::len) word). a < b}"
+ by (rule wf_subset)
+ then show "P a" using *
+ by induction blast
+qed
+
lemma wi_less:
"(word_of_int n < (word_of_int m :: 'a::len0 word)) =
(n mod 2 ^ LENGTH('a) < m mod 2 ^ LENGTH('a))"
@@ -1305,8 +1326,6 @@
lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y"
unfolding dvd_def udvd_nat_alt by force
-lemmas unat_mono = word_less_nat_alt [THEN iffD1]
-
lemma unat_minus_one:
assumes "w \<noteq> 0"
shows "unat (w - 1) = unat w - 1"
--- a/src/HOL/ex/Word_Type.thy Sat Oct 19 16:09:39 2019 +0200
+++ b/src/HOL/ex/Word_Type.thy Sat Oct 19 16:16:24 2019 +0200
@@ -132,6 +132,12 @@
instance word :: (len) comm_ring_1
by standard (transfer; simp)+
+quickcheck_generator word
+ constructors:
+ "zero_class.zero :: ('a::len0) word",
+ "numeral :: num \<Rightarrow> ('a::len0) word",
+ "uminus :: ('a::len0) word \<Rightarrow> ('a::len0) word"
+
subsubsection \<open>Conversions\<close>
@@ -180,6 +186,20 @@
end
+instantiation word :: (len0) equal
+begin
+
+definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+ where "equal_word a b \<longleftrightarrow> (unsigned a :: int) = unsigned b"
+
+instance proof
+ fix a b :: "'a word"
+ show "HOL.equal a b \<longleftrightarrow> a = b"
+ using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def)
+qed
+
+end
+
context ring_1
begin