# HG changeset patch # User huffman # Date 1333716000 -7200 # Node ID a0f257197741840418f0de5b54195de9ad69692d # Parent 09c5160ba550a15d07ff80f86ccdc388ceacbbc5 remove now-unnecessary type annotations from lift_definition commands diff -r 09c5160ba550 -r a0f257197741 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Fri Apr 06 14:39:27 2012 +0200 +++ b/src/HOL/Word/Word.thy Fri Apr 06 14:40:00 2012 +0200 @@ -272,33 +272,29 @@ subsection "Arithmetic operations" -lift_definition word_succ :: "'a::len0 word \ 'a word" is "\x::int. x + 1" +lift_definition word_succ :: "'a::len0 word \ 'a word" is "\x. x + 1" by (metis bintr_ariths(6)) -lift_definition word_pred :: "'a::len0 word \ 'a word" is "\x::int. x - 1" +lift_definition word_pred :: "'a::len0 word \ 'a word" is "\x. x - 1" by (metis bintr_ariths(7)) instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}" begin -lift_definition zero_word :: "'a word" is "0::int" . - -lift_definition one_word :: "'a word" is "1::int" . - -lift_definition plus_word :: "'a word \ 'a word \ 'a word" - is "op + :: int \ int \ int" +lift_definition zero_word :: "'a word" is "0" . + +lift_definition one_word :: "'a word" is "1" . + +lift_definition plus_word :: "'a word \ 'a word \ 'a word" is "op +" by (metis bintr_ariths(2)) -lift_definition minus_word :: "'a word \ 'a word \ 'a word" - is "op - :: int \ int \ int" +lift_definition minus_word :: "'a word \ 'a word \ 'a word" is "op -" by (metis bintr_ariths(3)) -lift_definition uminus_word :: "'a word \ 'a word" - is "uminus :: int \ int" +lift_definition uminus_word :: "'a word \ 'a word" is uminus by (metis bintr_ariths(5)) -lift_definition times_word :: "'a word \ 'a word \ 'a word" - is "op * :: int \ int \ int" +lift_definition times_word :: "'a word \ 'a word \ 'a word" is "op *" by (metis bintr_ariths(4)) definition @@ -394,20 +390,16 @@ instantiation word :: (len0) bits begin -lift_definition bitNOT_word :: "'a word \ 'a word" - is "bitNOT :: int \ int" +lift_definition bitNOT_word :: "'a word \ 'a word" is bitNOT by (metis bin_trunc_not) -lift_definition bitAND_word :: "'a word \ 'a word \ 'a word" - is "bitAND :: int \ int \ int" +lift_definition bitAND_word :: "'a word \ 'a word \ 'a word" is bitAND by (metis bin_trunc_and) -lift_definition bitOR_word :: "'a word \ 'a word \ 'a word" - is "bitOR :: int \ int \ int" +lift_definition bitOR_word :: "'a word \ 'a word \ 'a word" is bitOR by (metis bin_trunc_or) -lift_definition bitXOR_word :: "'a word \ 'a word \ 'a word" - is "bitXOR :: int \ int \ int" +lift_definition bitXOR_word :: "'a word \ 'a word \ 'a word" is bitXOR by (metis bin_trunc_xor) definition