# 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 \ ('a::len0) word", + "uminus :: ('a::len0) word \ ('a::len0) word" + subsubsection \Conversions\ @@ -180,6 +186,20 @@ end +instantiation word :: (len0) equal +begin + +definition equal_word :: "'a word \ 'a word \ bool" + where "equal_word a b \ (unsigned a :: int) = unsigned b" + +instance proof + fix a b :: "'a word" + show "HOL.equal a b \ a = b" + using word_eq_iff_unsigned [of a b] by (auto simp add: equal_word_def) +qed + +end + context ring_1 begin