# HG changeset patch
# User haftmann
# Date 1592471249 0
# Node ID c9251bc7da4e7c2af22be76504b1017891f48db8
# Parent  5b8b1183c6416c28b57801b104599046546539f1
more transfer rules

diff -r 5b8b1183c641 -r c9251bc7da4e 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
@@ -247,21 +247,45 @@
 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word" is "(*)"
   by (auto simp add: bintrunc_mod2p intro: mod_mult_cong)
 
-definition word_div_def: "a div b = word_of_int (uint a div uint b)"
-
-definition word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
+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
+
+lift_definition modulo_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "\<lambda>a b. take_bit LENGTH('a) a mod take_bit LENGTH('a) b"
+  by simp
 
 instance
   by standard (transfer, simp add: algebra_simps)+
 
 end
 
+lemma word_div_def [code]:
+  "a div b = word_of_int (uint a div uint b)"
+  by transfer rule
+
+lemma word_mod_def [code]:
+  "a mod b = word_of_int (uint a mod uint b)"
+  by transfer rule
+
 quickcheck_generator word
   constructors:
     "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 power_transfer_word [transfer_rule]:
+  \<open>(pcr_word ===> (=) ===> pcr_word) (^) (^)\<close>
+  by transfer_prover
+
+end
+
+
 text \<open>Legacy theorems:\<close>
 
 lemma word_arith_wis [code]:
@@ -297,6 +321,10 @@
 
 lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
 
+instance word :: (len0) comm_monoid_add ..
+
+instance word :: (len0) semiring_numeral ..
+
 instance word :: (len) comm_ring_1
 proof
   have *: "0 < LENGTH('a)" by (rule len_gt_0)
@@ -313,24 +341,98 @@
   apply (simp add: word_of_nat wi_hom_sub)
   done
 
+context
+  includes lifting_syntax
+  notes 
+    transfer_rule_of_bool [transfer_rule]
+    transfer_rule_numeral [transfer_rule]
+    transfer_rule_of_nat [transfer_rule]
+    transfer_rule_of_int [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"
+  by transfer_prover
+
+lemma [transfer_rule]:
+  "((=) ===> pcr_word) int of_nat"
+  by transfer_prover
+
+lemma [transfer_rule]:
+  "((=) ===> pcr_word) (\<lambda>k. k) of_int"
+proof -
+  have "((=) ===> pcr_word) of_int of_int"
+    by transfer_prover
+  then show ?thesis by (simp add: id_def)
+qed
+
+end
+
+lemma word_of_int_eq:
+  "word_of_int = of_int"
+  by (rule ext) (transfer, rule)
+
 definition udvd :: "'a::len word \<Rightarrow> 'a::len word \<Rightarrow> bool" (infixl "udvd" 50)
   where "a udvd b = (\<exists>n\<ge>0. uint b = n * uint a)"
 
+context
+  includes lifting_syntax
+begin
+
+lemma [transfer_rule]:
+  "(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
+proof -
+  have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
+    for k :: int
+  proof
+    assume ?P
+    then show ?Q
+      by auto
+  next
+    assume ?Q
+    then obtain l where "take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l)" ..
+    then have "even (take_bit LENGTH('a) k)"
+      by simp
+    then show ?P
+      by simp
+  qed
+  show ?thesis by (simp only: even_word_unfold [abs_def] dvd_def [where ?'a = "'a word", abs_def])
+    transfer_prover
+qed
+
+end
+
 
 subsection \<open>Ordering\<close>
 
 instantiation word :: (len0) linorder
 begin
 
-definition word_le_def: "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
-
-definition word_less_def: "a < b \<longleftrightarrow> uint a < uint b"
+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
+
+lift_definition less_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> bool"
+  is "\<lambda>a b. take_bit LENGTH('a) a < take_bit LENGTH('a) b"
+  by simp
 
 instance
-  by standard (auto simp: word_less_def word_le_def)
+  by (standard; transfer) auto
 
 end
 
+lemma word_le_def [code]:
+  "a \<le> b \<longleftrightarrow> uint a \<le> uint b"
+  by transfer rule
+
+lemma word_less_def [code]:
+  "a < b \<longleftrightarrow> uint a < uint b"
+  by transfer rule
+
 definition word_sle :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool"  ("(_/ <=s _)" [50, 51] 50)
   where "a <=s b \<longleftrightarrow> sint a \<le> sint b"
 
@@ -549,12 +651,6 @@
 
 declare word_neg_numeral_alt [symmetric, code_abbrev]
 
-lemma word_numeral_transfer [transfer_rule]:
-  "(rel_fun (=) pcr_word) numeral numeral"
-  "(rel_fun (=) pcr_word) (- numeral) (- numeral)"
-  apply (simp_all add: rel_fun_def word.pcr_cr_eq cr_word_def)
-  using word_numeral_alt [symmetric] word_neg_numeral_alt [symmetric] by auto
-
 lemma uint_bintrunc [simp]:
   "uint (numeral bin :: 'a word) =
     bintrunc (LENGTH('a::len0)) (numeral bin)"