# HG changeset patch
# User huffman
# Date 1333628056 -7200
# Node ID 9475d524bafb039006242e5485c28c2368b315b6
# Parent  3c31e6f1b3bdfdca240ed02da114281214f5a154
set up and use lift_definition for word operations

diff -r 3c31e6f1b3bd -r 9475d524bafb src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Apr 05 12:18:06 2012 +0200
+++ b/src/HOL/Word/Word.thy	Thu Apr 05 14:14:16 2012 +0200
@@ -233,6 +233,22 @@
 definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
   where "cr_word \<equiv> (\<lambda>x y. word_of_int x = y)"
 
+lemma Quotient_word:
+  "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
+    word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
+  unfolding Quotient_alt_def cr_word_def
+  by (simp add: word_ubin.norm_eq_iff)
+
+lemma equivp_word:
+  "equivp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
+  by (auto intro!: equivpI reflpI sympI transpI)
+
+local_setup {*
+  Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm equivp_word}
+*}
+
+text {* TODO: The next several lemmas could be generated automatically. *}
+
 lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word"
   unfolding bi_total_def cr_word_def
   by (auto intro: word_of_int_uint)
@@ -258,36 +274,34 @@
 
 subsection  "Arithmetic operations"
 
-definition
-  word_succ :: "'a :: len0 word => 'a word"
-where
-  "word_succ a = word_of_int (uint a + 1)"
-
-definition
-  word_pred :: "'a :: len0 word => 'a word"
-where
-  "word_pred a = word_of_int (uint a - 1)"
+lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x + 1"
+  by (metis bintr_ariths(6))
+
+lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x - 1"
+  by (metis bintr_ariths(7))
 
 instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}"
 begin
 
-definition
-  word_0_wi: "0 = word_of_int 0"
-
-definition
-  word_1_wi: "1 = word_of_int 1"
-
-definition
-  word_add_def: "a + b = word_of_int (uint a + uint b)"
-
-definition
-  word_sub_wi: "a - b = word_of_int (uint a - uint b)"
-
-definition
-  word_minus_def: "- a = word_of_int (- uint a)"
-
-definition
-  word_mult_def: "a * b = word_of_int (uint a * uint b)"
+lift_definition zero_word :: "'a word" is "0::int" .
+
+lift_definition one_word :: "'a word" is "1::int" .
+
+lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "op + :: int \<Rightarrow> int \<Rightarrow> int"
+  by (metis bintr_ariths(2))
+
+lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "op - :: int \<Rightarrow> int \<Rightarrow> int"
+  by (metis bintr_ariths(3))
+
+lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
+  is "uminus :: int \<Rightarrow> int"
+  by (metis bintr_ariths(5))
+
+lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "op * :: int \<Rightarrow> int \<Rightarrow> int"
+  by (metis bintr_ariths(4))
 
 definition
   word_div_def: "a div b = word_of_int (uint a div uint b)"
@@ -295,9 +309,25 @@
 definition
   word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
 
-lemmas word_arith_wis =
-  word_add_def word_sub_wi word_mult_def word_minus_def 
-  word_succ_def word_pred_def word_0_wi word_1_wi
+instance
+  by default (transfer, simp add: algebra_simps)+
+
+end
+
+text {* Legacy theorems: *}
+
+lemma word_arith_wis: shows
+  word_add_def: "a + b = word_of_int (uint a + uint b)" and
+  word_sub_wi: "a - b = word_of_int (uint a - uint b)" and
+  word_mult_def: "a * b = word_of_int (uint a * uint b)" and
+  word_minus_def: "- a = word_of_int (- uint a)" and
+  word_succ_alt: "word_succ a = word_of_int (uint a + 1)" 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
 
 lemmas arths = 
   bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm]
@@ -310,7 +340,7 @@
   wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
   wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and
   wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
-  by (auto simp: word_arith_wis arths)
+  by (transfer, simp)+
 
 lemmas wi_hom_syms = wi_homs [symmetric]
 
@@ -318,22 +348,6 @@
 
 lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
 
-lemma word_arith_transfer [transfer_rule]:
-  "cr_word 0 0"
-  "cr_word 1 1"
-  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op +) (op +)"
-  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op -) (op -)"
-  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op *) (op *)"
-  "(fun_rel cr_word cr_word) uminus uminus"
-  "(fun_rel cr_word cr_word) (\<lambda>x. x + 1) word_succ"
-  "(fun_rel cr_word cr_word) (\<lambda>x. x - 1) word_pred"
-  unfolding cr_word_def fun_rel_def by (simp_all add: word_of_int_homs)
-
-instance
-  by default (transfer, simp add: algebra_simps)+
-
-end
-
 instance word :: (len) comm_ring_1
 proof
   have "0 < len_of TYPE('a)" by (rule len_gt_0)
@@ -382,21 +396,21 @@
 instantiation word :: (len0) bits
 begin
 
-definition
-  word_and_def: 
-  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
-
-definition
-  word_or_def:  
-  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
-
-definition
-  word_xor_def: 
-  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
-
-definition
-  word_not_def: 
-  "NOT (a::'a word) = word_of_int (NOT (uint a))"
+lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word"
+  is "bitNOT :: int \<Rightarrow> int"
+  by (metis bin_trunc_not)
+
+lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "bitAND :: int \<Rightarrow> int \<Rightarrow> int"
+  by (metis bin_trunc_and)
+
+lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "bitOR :: int \<Rightarrow> int \<Rightarrow> int"
+  by (metis bin_trunc_or)
+
+lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
+  is "bitXOR :: int \<Rightarrow> int \<Rightarrow> int"
+  by (metis bin_trunc_xor)
 
 definition
   word_test_bit_def: "test_bit a = bin_nth (uint a)"
@@ -428,6 +442,14 @@
 
 end
 
+lemma 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)" 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)"
+  unfolding bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def
+  by simp_all
+
 instantiation word :: (len) bitss
 begin
 
@@ -1245,9 +1267,6 @@
   word_sub_wi
   word_arith_wis (* FIXME: duplicate *)
 
-lemmas word_succ_alt = word_succ_def (* FIXME: duplicate *)
-lemmas word_pred_alt = word_pred_def (* FIXME: duplicate *)
-
 subsection  "Transferring goals from words to ints"
 
 lemma word_ths:  
@@ -1257,11 +1276,7 @@
   word_pred_succ: "word_pred (word_succ a) = a" and
   word_succ_pred: "word_succ (word_pred a) = a" and
   word_mult_succ: "word_succ a * b = b + a * b"
-  by (rule word_uint.Abs_cases [of b],
-      rule word_uint.Abs_cases [of a],
-      simp add: add_commute mult_commute 
-                ring_distribs word_of_int_homs
-           del: word_of_int_0 word_of_int_1)+
+  by (transfer, simp add: algebra_simps)+
 
 lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
   by simp
@@ -1281,7 +1296,7 @@
 lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
 
 lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
-  unfolding word_pred_def uint_eq_0 by simp
+  unfolding word_pred_m1 by simp
 
 lemma succ_pred_no [simp]:
   "word_succ (numeral w) = numeral w + 1"
@@ -2162,15 +2177,7 @@
   "word_of_int a AND word_of_int b = word_of_int (a AND b)"
   "word_of_int a OR word_of_int b = word_of_int (a OR b)"
   "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
-  unfolding word_log_defs wils1 by simp_all
-
-lemma word_bitwise_transfer [transfer_rule]:
-  "(fun_rel cr_word cr_word) bitNOT bitNOT"
-  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitAND bitAND"
-  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitOR bitOR"
-  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitXOR bitXOR"
-  unfolding fun_rel_def cr_word_def
-  by (simp_all add: word_wi_log_defs)
+  by (transfer, rule refl)+
 
 lemma word_no_log_defs [simp]:
   "NOT (numeral a) = word_of_int (NOT (numeral a))"