src/HOL/ex/Word.thy

 
 subsection \<open>Bit strings as quotient type\<close>
 
 subsubsection \<open>Basic properties\<close>
 
-quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l"
+quotient_type (overloaded) 'a word = int / "\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len) l"
   by (auto intro!: equivpI reflpI sympI transpI)
 
-instantiation word :: (len0) "{semiring_numeral, comm_semiring_0, comm_ring}"
+instantiation word :: (len) "{semiring_numeral, comm_semiring_0, comm_ring}"
 begin
 
 lift_definition zero_word :: "'a word"
   is 0
   .

 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"
+    "zero_class.zero :: ('a::len) word",
+    "numeral :: num \<Rightarrow> ('a::len) word",
+    "uminus :: ('a::len) word \<Rightarrow> ('a::len) word"
 
 context
   includes lifting_syntax
   notes power_transfer [transfer_rule]
 begin

 lemma [transfer_rule]:
   "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool"
   by transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len0 word \<Rightarrow> bool)) numeral numeral"
+  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:
   "((=) ===> pcr_word) int of_nat"
   by transfer_prover

   by (rule ext) (transfer, rule)
 
 context semiring_1
 begin
 
-lift_definition unsigned :: "'b::len0 word \<Rightarrow> 'a"
+lift_definition unsigned :: "'b::len word \<Rightarrow> 'a"
   is "of_nat \<circ> nat \<circ> take_bit LENGTH('b)"
   by simp
 
 lemma unsigned_0 [simp]:
   "unsigned 0 = 0"

   "a = b \<longleftrightarrow> unsigned a = unsigned b"
   by safe (transfer; simp add: eq_nat_nat_iff)
 
 end
 
-instantiation word :: (len0) equal
+instantiation word :: (len) equal
 begin
 
 definition equal_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   where "equal_word a b \<longleftrightarrow> (unsigned a :: int) = unsigned b"
 

 lemma of_int_unsigned [simp]:
   "of_int (unsigned a) = a"
   by transfer simp
 
 lemma unsigned_nat_less:
-  \<open>unsigned a < (2 ^ LENGTH('a) :: nat)\<close> for a :: \<open>'a::len0 word\<close>
+  \<open>unsigned a < (2 ^ LENGTH('a) :: nat)\<close> for a :: \<open>'a::len word\<close>
   by transfer (simp add: take_bit_eq_mod)
 
 lemma unsigned_int_less:
-  \<open>unsigned a < (2 ^ LENGTH('a) :: int)\<close> for a :: \<open>'a::len0 word\<close>
+  \<open>unsigned a < (2 ^ LENGTH('a) :: int)\<close> for a :: \<open>'a::len word\<close>
   by transfer (simp add: take_bit_eq_mod)
 
 context ring_char_0
 begin
 

   by transfer simp
 
 
 subsubsection \<open>Division\<close>
 
-instantiation word :: (len0) modulo
+instantiation word :: (len) modulo
 begin
 
 lift_definition divide_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is "\<lambda>a b. take_bit LENGTH('a) a div take_bit LENGTH('a) b"
   by simp

 instance ..
 
 end
 
 lemma zero_word_div_eq [simp]:
-  \<open>0 div a = 0\<close> for a :: \<open>'a::len0 word\<close>
+  \<open>0 div a = 0\<close> for a :: \<open>'a::len word\<close>
   by transfer simp
 
 lemma div_zero_word_eq [simp]:
-  \<open>a div 0 = 0\<close> for a :: \<open>'a::len0 word\<close>
+  \<open>a div 0 = 0\<close> for a :: \<open>'a::len word\<close>
   by transfer simp
 
 context
   includes lifting_syntax
 begin

 qed
 
 
 subsubsection \<open>Orderings\<close>
 
-instantiation word :: (len0) linorder
+instantiation word :: (len) linorder
 begin
 
 lift_definition less_eq_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
   is "\<lambda>a b. take_bit LENGTH('a) a \<le> take_bit LENGTH('a) b"
   by simp

   by (transfer fixing: less) (auto dest: preorder_class.le_less_trans [OF take_bit_nonnegative])
 
 end
 
 lemma word_greater_zero_iff:
-  \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len0 word\<close>
+  \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len word\<close>
   by transfer (simp add: less_le)
 
 lemma of_nat_word_eq_iff:
   \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close>
   by transfer (simp add: take_bit_of_nat)