# HG changeset patch
# User haftmann
# Date 1592471249 0
# Node ID 6ede899d26d329324b9b41afec244dd55aebef34
# Parent  476b9e6904d97b580c658805b736e503360d9627
fundamental construction of word type following existing transfer rules

diff -r 476b9e6904d9 -r 6ede899d26d3 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Jun 18 09:07:29 2020 +0000
+++ b/src/HOL/Word/Word.thy	Thu Jun 18 09:07:29 2020 +0000
@@ -19,36 +19,34 @@
 
 subsection \<open>Type definition\<close>
 
-typedef (overloaded) 'a word = "{(0::int) ..< 2 ^ LENGTH('a::len0)}"
-  morphisms uint Abs_word by auto
+quotient_type (overloaded) 'a word = int / \<open>\<lambda>k l. take_bit LENGTH('a) k = take_bit LENGTH('a::len0) l\<close>
+  morphisms rep_word word_of_int by (auto intro!: equivpI reflpI sympI transpI)
+
+lift_definition uint :: \<open>'a::len0 word \<Rightarrow> int\<close>
+  is \<open>take_bit LENGTH('a)\<close> .
 
 lemma uint_nonnegative: "0 \<le> uint w"
-  using word.uint [of w] by simp
+  by transfer simp
 
 lemma uint_bounded: "uint w < 2 ^ LENGTH('a)"
   for w :: "'a::len0 word"
-  using word.uint [of w] by simp
+  by transfer (simp add: take_bit_eq_mod)
 
 lemma uint_idem: "uint w mod 2 ^ LENGTH('a) = uint w"
   for w :: "'a::len0 word"
   using uint_nonnegative uint_bounded by (rule mod_pos_pos_trivial)
 
+lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b"
+  by transfer simp
+
 lemma word_uint_eq_iff: "a = b \<longleftrightarrow> uint a = uint b"
-  by (simp add: uint_inject)
-
-lemma word_uint_eqI: "uint a = uint b \<Longrightarrow> a = b"
-  by (simp add: word_uint_eq_iff)
-
-definition word_of_int :: "int \<Rightarrow> 'a::len0 word"
-  \<comment> \<open>representation of words using unsigned or signed bins,
-    only difference in these is the type class\<close>
-  where "word_of_int k = Abs_word (k mod 2 ^ LENGTH('a))"
+  using word_uint_eqI by auto
 
 lemma uint_word_of_int: "uint (word_of_int k :: 'a::len0 word) = k mod 2 ^ LENGTH('a)"
-  by (auto simp add: word_of_int_def intro: Abs_word_inverse)
-
+  by transfer (simp add: take_bit_eq_mod)
+  
 lemma word_of_int_uint: "word_of_int (uint w) = w"
-  by (simp add: word_of_int_def uint_idem uint_inverse)
+  by transfer simp
 
 lemma split_word_all: "(\<And>x::'a::len0 word. PROP P x) \<equiv> (\<And>x. PROP P (word_of_int x))"
 proof
@@ -143,31 +141,6 @@
   "case x of (XCONST of_int :: 'a) y \<Rightarrow> b" \<rightharpoonup> "CONST word_int_case (\<lambda>y. b) x"
 
 
-subsection \<open>Correspondence relation for theorem transfer\<close>
-
-definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
-  where "cr_word = (\<lambda>x y. word_of_int x = y)"
-
-lemma Quotient_word:
-  "Quotient (\<lambda>x y. bintrunc (LENGTH('a)) x = bintrunc (LENGTH('a)) y)
-    word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
-  unfolding Quotient_alt_def cr_word_def
-  by (simp add: no_bintr_alt1 word_of_int_uint) (simp add: word_of_int_def Abs_word_inject)
-
-lemma reflp_word:
-  "reflp (\<lambda>x y. bintrunc (LENGTH('a::len0)) x = bintrunc (LENGTH('a)) y)"
-  by (simp add: reflp_def)
-
-setup_lifting Quotient_word reflp_word
-
-text \<open>TODO: The next lemma could be generated automatically.\<close>
-
-lemma uint_transfer [transfer_rule]:
-  "(rel_fun pcr_word (=)) (bintrunc (LENGTH('a))) (uint :: 'a::len0 word \<Rightarrow> int)"
-  unfolding rel_fun_def word.pcr_cr_eq cr_word_def
-  by (simp add: no_bintr_alt1 uint_word_of_int)
-
-
 subsection \<open>Basic code generation setup\<close>
 
 definition Word :: "int \<Rightarrow> 'a::len0 word"
@@ -218,9 +191,8 @@
   "td_ext (uint :: 'a word \<Rightarrow> int) word_of_int (uints (LENGTH('a::len0)))
     (\<lambda>w::int. w mod 2 ^ LENGTH('a))"
   apply (unfold td_ext_def')
-  apply (simp add: uints_num word_of_int_def bintrunc_mod2p)
-  apply (simp add: uint_mod_same uint_0 uint_lt
-                   word.uint_inverse word.Abs_word_inverse int_mod_lem)
+  apply transfer
+  apply (simp add: uints_num take_bit_eq_mod)
   done
 
 interpretation word_uint:
@@ -301,9 +273,14 @@
     and word_pred_alt: "word_pred a = word_of_int (uint a - 1)"
     and word_0_wi: "0 = word_of_int 0"
     and word_1_wi: "1 = word_of_int 1"
-  unfolding plus_word_def minus_word_def times_word_def uminus_word_def
-  unfolding word_succ_def word_pred_def zero_word_def one_word_def
-  by simp_all
+         apply (simp_all flip: plus_word.abs_eq minus_word.abs_eq
+           times_word.abs_eq uminus_word.abs_eq
+           zero_word.abs_eq one_word.abs_eq)
+   apply transfer
+   apply simp
+  apply transfer
+  apply simp
+  done
 
 lemma wi_homs:
   shows wi_hom_add: "word_of_int a + word_of_int b = word_of_int (a + b)"
@@ -410,7 +387,8 @@
     and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
     and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)"
     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)
+  by (simp_all flip: bitNOT_word.abs_eq bitAND_word.abs_eq
+     bitOR_word.abs_eq bitXOR_word.abs_eq)
 
 definition setBit :: "'a::len0 word \<Rightarrow> nat \<Rightarrow> 'a word"
   where "setBit w n = set_bit w n True"
@@ -736,10 +714,35 @@
   apply fast
   done
 
-lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)"
+lemma word_eq_iff: "x = y \<longleftrightarrow> (\<forall>n<LENGTH('a). x !! n = y !! n)" (is \<open>?P \<longleftrightarrow> ?Q\<close>)
   for x y :: "'a::len0 word"
-  unfolding uint_inject [symmetric] bin_eq_iff word_test_bit_def [symmetric]
-  by (metis test_bit_size [unfolded word_size])
+proof
+  assume ?P
+  then show ?Q
+    by simp
+next
+  assume ?Q
+  then have *: \<open>bit (uint x) n \<longleftrightarrow> bit (uint y) n\<close> if \<open>n < LENGTH('a)\<close> for n
+    using that by (simp add: word_test_bit_def bin_nth_iff)
+  show ?P
+  proof (rule word_uint_eqI, rule bit_eqI, rule iffI)
+    fix n
+    assume \<open>bit (uint x) n\<close>
+    then have \<open>n < LENGTH('a)\<close>
+      by (simp add: bit_take_bit_iff uint.rep_eq)
+    with * \<open>bit (uint x) n\<close>
+    show \<open>bit (uint y) n\<close>
+      by simp
+  next
+    fix n
+    assume \<open>bit (uint y) n\<close>
+    then have \<open>n < LENGTH('a)\<close>
+      by (simp add: bit_take_bit_iff uint.rep_eq)
+    with * \<open>bit (uint y) n\<close>
+    show \<open>bit (uint x) n\<close>
+      by simp
+  qed
+qed  
 
 lemma word_eqI: "(\<And>n. n < size u \<longrightarrow> u !! n = v !! n) \<Longrightarrow> u = v"
   for u :: "'a::len0 word"
@@ -1661,14 +1664,14 @@
 
 \<comment> \<open>links with \<open>rbl\<close> operations\<close>
 lemma word_succ_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_succ w) = rev (rbl_succ (rev bl))"
-  apply (unfold word_succ_def)
+  apply (unfold word_succ_alt)
   apply clarify
   apply (simp add: to_bl_of_bin)
   apply (simp add: to_bl_def rbl_succ)
   done
 
 lemma word_pred_rbl: "to_bl w = bl \<Longrightarrow> to_bl (word_pred w) = rev (rbl_pred (rev bl))"
-  apply (unfold word_pred_def)
+  apply (unfold word_pred_alt)
   apply clarify
   apply (simp add: to_bl_of_bin)
   apply (simp add: to_bl_def rbl_pred)
@@ -2089,16 +2092,34 @@
 
 subsection \<open>Cardinality, finiteness of set of words\<close>
 
-instance word :: (len0) finite
-  by standard (simp add: type_definition.univ [OF type_definition_word])
+lemma inj_on_word_of_int: \<open>inj_on (word_of_int :: int \<Rightarrow> 'a word) {0..<2 ^ LENGTH('a::len0)}\<close>
+  by (rule inj_onI) (simp add: word.abs_eq_iff take_bit_eq_mod)
+
+lemma inj_uint: \<open>inj uint\<close>
+  by (rule injI) simp
+
+lemma range_uint: \<open>range (uint :: 'a word \<Rightarrow> int) = {0..<2 ^ LENGTH('a::len0)}\<close>
+  by transfer (auto simp add: bintr_lt2p range_bintrunc)
+
+lemma UNIV_eq: \<open>(UNIV :: 'a word set) = word_of_int ` {0..<2 ^ LENGTH('a::len0)}\<close>
+proof -
+  have \<open>uint ` (UNIV :: 'a word set) = uint ` (word_of_int :: int \<Rightarrow> 'a word) ` {0..<2 ^ LENGTH('a::len0)}\<close>
+    by (simp add: range_uint image_image uint.abs_eq take_bit_eq_mod)
+  then show ?thesis
+    using inj_image_eq_iff [of \<open>uint :: 'a word \<Rightarrow> int\<close> \<open>UNIV :: 'a word set\<close> \<open>word_of_int ` {0..<2 ^ LENGTH('a)} :: 'a word set\<close>, OF inj_uint]
+    by simp
+qed
 
 lemma card_word: "CARD('a word) = 2 ^ LENGTH('a::len0)"
-  by (simp add: type_definition.card [OF type_definition_word] nat_power_eq)
+  by (simp add: UNIV_eq card_image inj_on_word_of_int)
 
 lemma card_word_size: "CARD('a word) = 2 ^ size x"
   for x :: "'a::len0 word"
   unfolding word_size by (rule card_word)
 
+instance word :: (len0) finite
+  by standard (simp add: UNIV_eq)
+
 
 subsection \<open>Bitwise Operations on Words\<close>
 
@@ -3182,7 +3203,7 @@
       simp del: word_of_int_numeral)
   apply (drule xtr8 [rotated])
    apply (rule int_mod_le)
-   apply (auto simp add : mod_pos_pos_trivial)
+   apply simp_all
   done
 
 lemmas mask_eq_iff_w2p = trans [OF mask_eq_iff word_2p_lem [symmetric]]