set up and use lift_definition for word operations
authorhuffman
Thu Apr 05 14:14:16 2012 +0200 (2012-04-05)
changeset 473749475d524bafb
parent 47373 3c31e6f1b3bd
child 47375 8e6a45f1bf8f
set up and use lift_definition for word operations
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Word.thy	Thu Apr 05 12:18:06 2012 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Apr 05 14:14:16 2012 +0200
     1.3 @@ -233,6 +233,22 @@
     1.4  definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
     1.5    where "cr_word \<equiv> (\<lambda>x y. word_of_int x = y)"
     1.6  
     1.7 +lemma Quotient_word:
     1.8 +  "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
     1.9 +    word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)"
    1.10 +  unfolding Quotient_alt_def cr_word_def
    1.11 +  by (simp add: word_ubin.norm_eq_iff)
    1.12 +
    1.13 +lemma equivp_word:
    1.14 +  "equivp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
    1.15 +  by (auto intro!: equivpI reflpI sympI transpI)
    1.16 +
    1.17 +local_setup {*
    1.18 +  Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm equivp_word}
    1.19 +*}
    1.20 +
    1.21 +text {* TODO: The next several lemmas could be generated automatically. *}
    1.22 +
    1.23  lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word"
    1.24    unfolding bi_total_def cr_word_def
    1.25    by (auto intro: word_of_int_uint)
    1.26 @@ -258,36 +274,34 @@
    1.27  
    1.28  subsection  "Arithmetic operations"
    1.29  
    1.30 -definition
    1.31 -  word_succ :: "'a :: len0 word => 'a word"
    1.32 -where
    1.33 -  "word_succ a = word_of_int (uint a + 1)"
    1.34 -
    1.35 -definition
    1.36 -  word_pred :: "'a :: len0 word => 'a word"
    1.37 -where
    1.38 -  "word_pred a = word_of_int (uint a - 1)"
    1.39 +lift_definition word_succ :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x + 1"
    1.40 +  by (metis bintr_ariths(6))
    1.41 +
    1.42 +lift_definition word_pred :: "'a::len0 word \<Rightarrow> 'a word" is "\<lambda>x::int. x - 1"
    1.43 +  by (metis bintr_ariths(7))
    1.44  
    1.45  instantiation word :: (len0) "{neg_numeral, Divides.div, comm_monoid_mult, comm_ring}"
    1.46  begin
    1.47  
    1.48 -definition
    1.49 -  word_0_wi: "0 = word_of_int 0"
    1.50 -
    1.51 -definition
    1.52 -  word_1_wi: "1 = word_of_int 1"
    1.53 -
    1.54 -definition
    1.55 -  word_add_def: "a + b = word_of_int (uint a + uint b)"
    1.56 -
    1.57 -definition
    1.58 -  word_sub_wi: "a - b = word_of_int (uint a - uint b)"
    1.59 -
    1.60 -definition
    1.61 -  word_minus_def: "- a = word_of_int (- uint a)"
    1.62 -
    1.63 -definition
    1.64 -  word_mult_def: "a * b = word_of_int (uint a * uint b)"
    1.65 +lift_definition zero_word :: "'a word" is "0::int" .
    1.66 +
    1.67 +lift_definition one_word :: "'a word" is "1::int" .
    1.68 +
    1.69 +lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
    1.70 +  is "op + :: int \<Rightarrow> int \<Rightarrow> int"
    1.71 +  by (metis bintr_ariths(2))
    1.72 +
    1.73 +lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
    1.74 +  is "op - :: int \<Rightarrow> int \<Rightarrow> int"
    1.75 +  by (metis bintr_ariths(3))
    1.76 +
    1.77 +lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
    1.78 +  is "uminus :: int \<Rightarrow> int"
    1.79 +  by (metis bintr_ariths(5))
    1.80 +
    1.81 +lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
    1.82 +  is "op * :: int \<Rightarrow> int \<Rightarrow> int"
    1.83 +  by (metis bintr_ariths(4))
    1.84  
    1.85  definition
    1.86    word_div_def: "a div b = word_of_int (uint a div uint b)"
    1.87 @@ -295,9 +309,25 @@
    1.88  definition
    1.89    word_mod_def: "a mod b = word_of_int (uint a mod uint b)"
    1.90  
    1.91 -lemmas word_arith_wis =
    1.92 -  word_add_def word_sub_wi word_mult_def word_minus_def 
    1.93 -  word_succ_def word_pred_def word_0_wi word_1_wi
    1.94 +instance
    1.95 +  by default (transfer, simp add: algebra_simps)+
    1.96 +
    1.97 +end
    1.98 +
    1.99 +text {* Legacy theorems: *}
   1.100 +
   1.101 +lemma word_arith_wis: shows
   1.102 +  word_add_def: "a + b = word_of_int (uint a + uint b)" and
   1.103 +  word_sub_wi: "a - b = word_of_int (uint a - uint b)" and
   1.104 +  word_mult_def: "a * b = word_of_int (uint a * uint b)" and
   1.105 +  word_minus_def: "- a = word_of_int (- uint a)" and
   1.106 +  word_succ_alt: "word_succ a = word_of_int (uint a + 1)" and
   1.107 +  word_pred_alt: "word_pred a = word_of_int (uint a - 1)" and
   1.108 +  word_0_wi: "0 = word_of_int 0" and
   1.109 +  word_1_wi: "1 = word_of_int 1"
   1.110 +  unfolding plus_word_def minus_word_def times_word_def uminus_word_def
   1.111 +  unfolding word_succ_def word_pred_def zero_word_def one_word_def
   1.112 +  by simp_all
   1.113  
   1.114  lemmas arths = 
   1.115    bintr_ariths [THEN word_ubin.norm_eq_iff [THEN iffD1], folded word_ubin.eq_norm]
   1.116 @@ -310,7 +340,7 @@
   1.117    wi_hom_neg: "- word_of_int a = word_of_int (- a)" and
   1.118    wi_hom_succ: "word_succ (word_of_int a) = word_of_int (a + 1)" and
   1.119    wi_hom_pred: "word_pred (word_of_int a) = word_of_int (a - 1)"
   1.120 -  by (auto simp: word_arith_wis arths)
   1.121 +  by (transfer, simp)+
   1.122  
   1.123  lemmas wi_hom_syms = wi_homs [symmetric]
   1.124  
   1.125 @@ -318,22 +348,6 @@
   1.126  
   1.127  lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
   1.128  
   1.129 -lemma word_arith_transfer [transfer_rule]:
   1.130 -  "cr_word 0 0"
   1.131 -  "cr_word 1 1"
   1.132 -  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op +) (op +)"
   1.133 -  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op -) (op -)"
   1.134 -  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op *) (op *)"
   1.135 -  "(fun_rel cr_word cr_word) uminus uminus"
   1.136 -  "(fun_rel cr_word cr_word) (\<lambda>x. x + 1) word_succ"
   1.137 -  "(fun_rel cr_word cr_word) (\<lambda>x. x - 1) word_pred"
   1.138 -  unfolding cr_word_def fun_rel_def by (simp_all add: word_of_int_homs)
   1.139 -
   1.140 -instance
   1.141 -  by default (transfer, simp add: algebra_simps)+
   1.142 -
   1.143 -end
   1.144 -
   1.145  instance word :: (len) comm_ring_1
   1.146  proof
   1.147    have "0 < len_of TYPE('a)" by (rule len_gt_0)
   1.148 @@ -382,21 +396,21 @@
   1.149  instantiation word :: (len0) bits
   1.150  begin
   1.151  
   1.152 -definition
   1.153 -  word_and_def: 
   1.154 -  "(a::'a word) AND b = word_of_int (uint a AND uint b)"
   1.155 -
   1.156 -definition
   1.157 -  word_or_def:  
   1.158 -  "(a::'a word) OR b = word_of_int (uint a OR uint b)"
   1.159 -
   1.160 -definition
   1.161 -  word_xor_def: 
   1.162 -  "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
   1.163 -
   1.164 -definition
   1.165 -  word_not_def: 
   1.166 -  "NOT (a::'a word) = word_of_int (NOT (uint a))"
   1.167 +lift_definition bitNOT_word :: "'a word \<Rightarrow> 'a word"
   1.168 +  is "bitNOT :: int \<Rightarrow> int"
   1.169 +  by (metis bin_trunc_not)
   1.170 +
   1.171 +lift_definition bitAND_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.172 +  is "bitAND :: int \<Rightarrow> int \<Rightarrow> int"
   1.173 +  by (metis bin_trunc_and)
   1.174 +
   1.175 +lift_definition bitOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.176 +  is "bitOR :: int \<Rightarrow> int \<Rightarrow> int"
   1.177 +  by (metis bin_trunc_or)
   1.178 +
   1.179 +lift_definition bitXOR_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   1.180 +  is "bitXOR :: int \<Rightarrow> int \<Rightarrow> int"
   1.181 +  by (metis bin_trunc_xor)
   1.182  
   1.183  definition
   1.184    word_test_bit_def: "test_bit a = bin_nth (uint a)"
   1.185 @@ -428,6 +442,14 @@
   1.186  
   1.187  end
   1.188  
   1.189 +lemma shows
   1.190 +  word_not_def: "NOT (a::'a::len0 word) = word_of_int (NOT (uint a))" and
   1.191 +  word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" and
   1.192 +  word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" and
   1.193 +  word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)"
   1.194 +  unfolding bitNOT_word_def bitAND_word_def bitOR_word_def bitXOR_word_def
   1.195 +  by simp_all
   1.196 +
   1.197  instantiation word :: (len) bitss
   1.198  begin
   1.199  
   1.200 @@ -1245,9 +1267,6 @@
   1.201    word_sub_wi
   1.202    word_arith_wis (* FIXME: duplicate *)
   1.203  
   1.204 -lemmas word_succ_alt = word_succ_def (* FIXME: duplicate *)
   1.205 -lemmas word_pred_alt = word_pred_def (* FIXME: duplicate *)
   1.206 -
   1.207  subsection  "Transferring goals from words to ints"
   1.208  
   1.209  lemma word_ths:  
   1.210 @@ -1257,11 +1276,7 @@
   1.211    word_pred_succ: "word_pred (word_succ a) = a" and
   1.212    word_succ_pred: "word_succ (word_pred a) = a" and
   1.213    word_mult_succ: "word_succ a * b = b + a * b"
   1.214 -  by (rule word_uint.Abs_cases [of b],
   1.215 -      rule word_uint.Abs_cases [of a],
   1.216 -      simp add: add_commute mult_commute 
   1.217 -                ring_distribs word_of_int_homs
   1.218 -           del: word_of_int_0 word_of_int_1)+
   1.219 +  by (transfer, simp add: algebra_simps)+
   1.220  
   1.221  lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
   1.222    by simp
   1.223 @@ -1281,7 +1296,7 @@
   1.224  lemmas uint_mod_alt = word_mod_def [THEN trans [OF uint_cong int_word_uint]]
   1.225  
   1.226  lemma word_pred_0_n1: "word_pred 0 = word_of_int -1"
   1.227 -  unfolding word_pred_def uint_eq_0 by simp
   1.228 +  unfolding word_pred_m1 by simp
   1.229  
   1.230  lemma succ_pred_no [simp]:
   1.231    "word_succ (numeral w) = numeral w + 1"
   1.232 @@ -2162,15 +2177,7 @@
   1.233    "word_of_int a AND word_of_int b = word_of_int (a AND b)"
   1.234    "word_of_int a OR word_of_int b = word_of_int (a OR b)"
   1.235    "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
   1.236 -  unfolding word_log_defs wils1 by simp_all
   1.237 -
   1.238 -lemma word_bitwise_transfer [transfer_rule]:
   1.239 -  "(fun_rel cr_word cr_word) bitNOT bitNOT"
   1.240 -  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitAND bitAND"
   1.241 -  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitOR bitOR"
   1.242 -  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitXOR bitXOR"
   1.243 -  unfolding fun_rel_def cr_word_def
   1.244 -  by (simp_all add: word_wi_log_defs)
   1.245 +  by (transfer, rule refl)+
   1.246  
   1.247  lemma word_no_log_defs [simp]:
   1.248    "NOT (numeral a) = word_of_int (NOT (numeral a))"