# HG changeset patch
# User haftmann
# Date 1571476541 0
# Node ID c550368a4e2987469b3ea450dd485c3e42facc66
# Parent  cb161182ce7f6c30bcaa6ce341e26d0be86bb4eb
added quickcheck setup

diff -r cb161182ce7f -r c550368a4e29 src/HOL/ex/Word_Type.thy
--- a/src/HOL/ex/Word_Type.thy	Sat Oct 19 09:15:37 2019 +0000
+++ b/src/HOL/ex/Word_Type.thy	Sat Oct 19 09:15:41 2019 +0000
@@ -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