# HG changeset patch
# User haftmann
# Date 1555444220 0
# Node ID 85fb1a585f52150a27a81603240e8df4e615d09c
# Parent  40fdd74b75f3153faa942f3a3b8e7518cc1240ed
eliminated type class

diff -r 40fdd74b75f3 -r 85fb1a585f52 NEWS
--- a/NEWS	Tue Apr 16 19:50:19 2019 +0000
+++ b/NEWS	Tue Apr 16 19:50:20 2019 +0000
@@ -287,6 +287,7 @@
 
 * Session HOL-Word:
   * New theory More_Word as comprehensive entrance point.
+  * Merged type class bitss into type class bits.
   INCOMPATIBILITY.
 
 
diff -r 40fdd74b75f3 -r 85fb1a585f52 src/HOL/Word/Bits.thy
--- a/src/HOL/Word/Bits.thy	Tue Apr 16 19:50:19 2019 +0000
+++ b/src/HOL/Word/Bits.thy	Tue Apr 16 19:50:20 2019 +0000
@@ -25,12 +25,10 @@
 class bits = bit +
   fixes test_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool"  (infixl "!!" 100)
     and lsb :: "'a \<Rightarrow> bool"
+    and msb :: "'a \<Rightarrow> bool"
     and set_bit :: "'a \<Rightarrow> nat \<Rightarrow> bool \<Rightarrow> 'a"
     and set_bits :: "(nat \<Rightarrow> bool) \<Rightarrow> 'a"  (binder "BITS " 10)
     and shiftl :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl "<<" 55)
     and shiftr :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixl ">>" 55)
 
-class bitss = bits +
-  fixes msb :: "'a \<Rightarrow> bool"
-
 end
diff -r 40fdd74b75f3 -r 85fb1a585f52 src/HOL/Word/Bits_Int.thy
--- a/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:19 2019 +0000
+++ b/src/HOL/Word/Bits_Int.thy	Tue Apr 16 19:50:20 2019 +0000
@@ -746,7 +746,7 @@
     bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
   by (simp add: numeral_eq_Suc)
 
-instantiation int :: bitss
+instantiation int :: bits
 begin
 
 definition [iff]: "i !! n \<longleftrightarrow> bin_nth i n"
diff -r 40fdd74b75f3 -r 85fb1a585f52 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Tue Apr 16 19:50:19 2019 +0000
+++ b/src/HOL/Word/Word.thy	Tue Apr 16 19:50:20 2019 +0000
@@ -62,7 +62,7 @@
 
 definition sint :: "'a::len word \<Rightarrow> int"
   \<comment> \<open>treats the most-significant-bit as a sign bit\<close>
-  where sint_uint: "sint w = sbintrunc (len_of TYPE('a) - 1) (uint w)"
+  where sint_uint: "sint w = sbintrunc (LENGTH('a) - 1) (uint w)"
 
 definition unat :: "'a::len0 word \<Rightarrow> nat"
   where "unat w = nat (uint w)"
@@ -377,10 +377,12 @@
 
 definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
 
-definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth (len_of TYPE('a)) f)"
+definition word_set_bits_def: "(BITS n. f n) = of_bl (bl_of_nth LENGTH('a) f)"
 
 definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
 
+definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1"
+
 definition shiftl1 :: "'a word \<Rightarrow> 'a word"
   where "shiftl1 w = word_of_int (uint w BIT False)"
 
@@ -396,6 +398,10 @@
 
 end
 
+lemma word_msb_def:
+  "msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
+  by (simp add: msb_word_def sint_uint)
+
 lemma [code]:
   shows word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))"
     and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
@@ -403,15 +409,6 @@
     and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
   by (simp_all add: bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def)
 
-instantiation word :: (len) bitss
-begin
-
-definition word_msb_def: "msb a \<longleftrightarrow> bin_sign (sint a) = -1"
-
-instance ..
-
-end
-
 definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
   where "setBit w n = set_bit w n True"