eliminated type class
authorhaftmann
Tue Apr 16 19:50:20 2019 +0000 (7 days ago)
changeset 7017585fb1a585f52
parent 70174 40fdd74b75f3
child 70176 330382e284a4
eliminated type class
NEWS
src/HOL/Word/Bits.thy
src/HOL/Word/Bits_Int.thy
src/HOL/Word/Word.thy
     1.1 --- a/NEWS	Tue Apr 16 19:50:19 2019 +0000
     1.2 +++ b/NEWS	Tue Apr 16 19:50:20 2019 +0000
     1.3 @@ -287,6 +287,7 @@
     1.4  
     1.5  * Session HOL-Word:
     1.6    * New theory More_Word as comprehensive entrance point.
     1.7 +  * Merged type class bitss into type class bits.
     1.8    INCOMPATIBILITY.
     1.9  
    1.10  
     2.1 --- a/src/HOL/Word/Bits.thy	Tue Apr 16 19:50:19 2019 +0000
     2.2 +++ b/src/HOL/Word/Bits.thy	Tue Apr 16 19:50:20 2019 +0000
     2.3 @@ -25,12 +25,10 @@
     2.4  class bits = bit +
     2.5    fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"  (infixl "!!" 100)
     2.6      and lsb :: "'a \<Rightarrow> bool"
     2.7 +    and msb :: "'a \<Rightarrow> bool"
     2.8      and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
     2.9      and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
    2.10      and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
    2.11      and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
    2.12  
    2.13 -class bitss = bits +
    2.14 -  fixes msb :: "'a \<Rightarrow> bool"
    2.15 -
    2.16  end
     3.1 --- a/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:19 2019 +0000
     3.2 +++ b/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:20 2019 +0000
     3.3 @@ -746,7 +746,7 @@
     3.4      bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
     3.5    by (simp add: numeral_eq_Suc)
     3.6  
     3.7 -instantiation int :: bitss
     3.8 +instantiation int :: bits
     3.9  begin
    3.10  
    3.11  definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
     4.1 --- a/src/HOL/Word/Word.thy	Tue Apr 16 19:50:19 2019 +0000
     4.2 +++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:20 2019 +0000
     4.3 @@ -62,7 +62,7 @@
     4.4  
     4.5  definition sint :: "'a::len word \<Rightarrow> int"
     4.6    \<comment> \<open>treats the most-significant-bit as a sign bit\<close>
     4.7 -  where sint_uint: "sint w = sbintrunc (len_of TYPE('a) - 1) (uint w)"
     4.8 +  where sint_uint: "sint w = sbintrunc (LENGTH('a) - 1) (uint w)"
     4.9  
    4.10  definition unat :: "'a::len0 word \<Rightarrow> nat"
    4.11    where "unat w = nat (uint w)"
    4.12 @@ -377,10 +377,12 @@
    4.13  
    4.14  definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
    4.15  
    4.16 -definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE('a)) f)"
    4.17 +definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)"
    4.18  
    4.19  definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
    4.20  
    4.21 +definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1"
    4.22 +
    4.23  definition shiftl1 :: "'a word \<Rightarrow> 'a word"
    4.24    where "shiftl1 w = word_of_int (uint w BIT False)"
    4.25  
    4.26 @@ -396,6 +398,10 @@
    4.27  
    4.28  end
    4.29  
    4.30 +lemma word_msb_def:
    4.31 +  "msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
    4.32 +  by (simp add: msb_word_def sint_uint)
    4.33 +
    4.34  lemma [code]:
    4.35    shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))"
    4.36      and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
    4.37 @@ -403,15 +409,6 @@
    4.38      and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
    4.39    by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def)
    4.40  
    4.41 -instantiation word :: (len) bitss
    4.42 -begin
    4.43 -
    4.44 -definition word_msb_def: "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
    4.45 -
    4.46 -instance ..
    4.47 -
    4.48 -end
    4.49 -
    4.50  definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
    4.51    where "setBit w n = set_bit w n True"
    4.52