# HG changeset patch
# User wenzelm
# Date 1571494584 -7200
# Node ID 3ed399935d7c602dba239e258b23b1ddc5d3dda5
# Parent  c550368a4e2987469b3ea450dd485c3e42facc66# Parent  9e05f382e749f60cf48547a06b6a408b47bd6bf1
merged

diff -r 9e05f382e749 -r 3ed399935d7c src/HOL/Library/Type_Length.thy
--- 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
diff -r 9e05f382e749 -r 3ed399935d7c src/HOL/Rings.thy
--- 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)
diff -r 9e05f382e749 -r 3ed399935d7c src/HOL/Word/Word.thy
--- 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"
diff -r 9e05f382e749 -r 3ed399935d7c src/HOL/ex/Word_Type.thy
--- 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