configure transfer method for 'a word -> int
authorhuffman
Thu Apr 05 10:48:46 2012 +0200 (2012-04-05)
changeset 473729ab4e22dac7b
parent 47371 4193098c4ec1
child 47373 3c31e6f1b3bd
configure transfer method for 'a word -> int
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Word.thy	Thu Apr 05 08:43:31 2012 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Apr 05 10:48:46 2012 +0200
     1.3 @@ -228,6 +228,34 @@
     1.4    thus "PROP P x" by simp
     1.5  qed
     1.6  
     1.7 +subsection {* Correspondence relation for theorem transfer *}
     1.8 +
     1.9 +definition cr_word :: "int \<Rightarrow> 'a::len0 word \<Rightarrow> bool"
    1.10 +  where "cr_word \<equiv> (\<lambda>x y. word_of_int x = y)"
    1.11 +
    1.12 +lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word"
    1.13 +  unfolding bi_total_def cr_word_def
    1.14 +  by (auto intro: word_of_int_uint)
    1.15 +
    1.16 +lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word"
    1.17 +  unfolding right_unique_def cr_word_def by simp
    1.18 +
    1.19 +lemma word_eq_transfer [transfer_rule]:
    1.20 +  "(fun_rel cr_word (fun_rel cr_word op =))
    1.21 +    (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
    1.22 +    (op = :: 'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool)"
    1.23 +  unfolding fun_rel_def cr_word_def
    1.24 +  by (simp add: word_ubin.norm_eq_iff)
    1.25 +
    1.26 +lemma word_of_int_transfer [transfer_rule]:
    1.27 +  "(fun_rel op = cr_word) (\<lambda>x. x) word_of_int"
    1.28 +  unfolding fun_rel_def cr_word_def by simp
    1.29 +
    1.30 +lemma uint_transfer [transfer_rule]:
    1.31 +  "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))
    1.32 +    (uint :: 'a::len0 word \<Rightarrow> int)"
    1.33 +  unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm)
    1.34 +
    1.35  subsection  "Arithmetic operations"
    1.36  
    1.37  definition
    1.38 @@ -290,8 +318,19 @@
    1.39  
    1.40  lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
    1.41  
    1.42 +lemma word_arith_transfer [transfer_rule]:
    1.43 +  "cr_word 0 0"
    1.44 +  "cr_word 1 1"
    1.45 +  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op +) (op +)"
    1.46 +  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op -) (op -)"
    1.47 +  "(fun_rel cr_word (fun_rel cr_word cr_word)) (op *) (op *)"
    1.48 +  "(fun_rel cr_word cr_word) uminus uminus"
    1.49 +  "(fun_rel cr_word cr_word) (\<lambda>x. x + 1) word_succ"
    1.50 +  "(fun_rel cr_word cr_word) (\<lambda>x. x - 1) word_pred"
    1.51 +  unfolding cr_word_def fun_rel_def by (simp_all add: word_of_int_homs)
    1.52 +
    1.53  instance
    1.54 -  by default (auto simp: split_word_all word_of_int_homs algebra_simps)
    1.55 +  by default (transfer, simp add: algebra_simps)+
    1.56  
    1.57  end
    1.58  
    1.59 @@ -299,8 +338,7 @@
    1.60  proof
    1.61    have "0 < len_of TYPE('a)" by (rule len_gt_0)
    1.62    then show "(0::'a word) \<noteq> 1"
    1.63 -    unfolding word_0_wi word_1_wi
    1.64 -    by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
    1.65 +    by - (transfer, auto simp add: gr0_conv_Suc)
    1.66  qed
    1.67  
    1.68  lemma word_of_nat: "of_nat n = word_of_int (int n)"
    1.69 @@ -567,6 +605,12 @@
    1.70  
    1.71  declare word_neg_numeral_alt [symmetric, code_abbrev]
    1.72  
    1.73 +lemma word_numeral_transfer [transfer_rule]:
    1.74 +  "(fun_rel op = cr_word) numeral numeral"
    1.75 +  "(fun_rel op = cr_word) neg_numeral neg_numeral"
    1.76 +  unfolding fun_rel_def cr_word_def word_numeral_alt word_neg_numeral_alt
    1.77 +  by simp_all
    1.78 +
    1.79  lemma uint_bintrunc [simp]:
    1.80    "uint (numeral bin :: 'a word) = 
    1.81      bintrunc (len_of TYPE ('a :: len0)) (numeral bin)"
    1.82 @@ -2120,6 +2164,14 @@
    1.83    "word_of_int a XOR word_of_int b = word_of_int (a XOR b)"
    1.84    unfolding word_log_defs wils1 by simp_all
    1.85  
    1.86 +lemma word_bitwise_transfer [transfer_rule]:
    1.87 +  "(fun_rel cr_word cr_word) bitNOT bitNOT"
    1.88 +  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitAND bitAND"
    1.89 +  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitOR bitOR"
    1.90 +  "(fun_rel cr_word (fun_rel cr_word cr_word)) bitXOR bitXOR"
    1.91 +  unfolding fun_rel_def cr_word_def
    1.92 +  by (simp_all add: word_wi_log_defs)
    1.93 +
    1.94  lemma word_no_log_defs [simp]:
    1.95    "NOT (numeral a) = word_of_int (NOT (numeral a))"
    1.96    "NOT (neg_numeral a) = word_of_int (NOT (neg_numeral a))"
    1.97 @@ -2135,7 +2187,7 @@
    1.98    "numeral a XOR neg_numeral b = word_of_int (numeral a XOR neg_numeral b)"
    1.99    "neg_numeral a XOR numeral b = word_of_int (neg_numeral a XOR numeral b)"
   1.100    "neg_numeral a XOR neg_numeral b = word_of_int (neg_numeral a XOR neg_numeral b)"
   1.101 -  unfolding word_numeral_alt word_neg_numeral_alt word_wi_log_defs by simp_all
   1.102 +  by (transfer, rule refl)+
   1.103  
   1.104  text {* Special cases for when one of the arguments equals 1. *}
   1.105  
   1.106 @@ -2153,15 +2205,23 @@
   1.107    "1 XOR neg_numeral b = word_of_int (1 XOR neg_numeral b)"
   1.108    "numeral a XOR 1 = word_of_int (numeral a XOR 1)"
   1.109    "neg_numeral a XOR 1 = word_of_int (neg_numeral a XOR 1)"
   1.110 -  unfolding word_1_no word_no_log_defs by simp_all
   1.111 +  by (transfer, simp)+
   1.112  
   1.113  lemma uint_or: "uint (x OR y) = (uint x) OR (uint y)"
   1.114 -  by (simp add: word_or_def word_wi_log_defs word_ubin.eq_norm
   1.115 -                bin_trunc_ao(2) [symmetric])
   1.116 +  by (transfer, simp add: bin_trunc_ao)
   1.117  
   1.118  lemma uint_and: "uint (x AND y) = (uint x) AND (uint y)"
   1.119 -  by (simp add: word_and_def word_wi_log_defs word_ubin.eq_norm
   1.120 -                bin_trunc_ao(1) [symmetric]) 
   1.121 +  by (transfer, simp add: bin_trunc_ao)
   1.122 +
   1.123 +lemma test_bit_wi [simp]:
   1.124 +  "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
   1.125 +  unfolding word_test_bit_def
   1.126 +  by (simp add: word_ubin.eq_norm nth_bintr)
   1.127 +
   1.128 +lemma word_test_bit_transfer [transfer_rule]:
   1.129 +  "(fun_rel cr_word (fun_rel op = op =))
   1.130 +    (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
   1.131 +  unfolding fun_rel_def cr_word_def by simp
   1.132  
   1.133  lemma word_ops_nth_size:
   1.134    "n < size (x::'a::len0 word) \<Longrightarrow> 
   1.135 @@ -2169,42 +2229,32 @@
   1.136      (x AND y) !! n = (x !! n & y !! n) & 
   1.137      (x XOR y) !! n = (x !! n ~= y !! n) & 
   1.138      (NOT x) !! n = (~ x !! n)"
   1.139 -  unfolding word_size word_test_bit_def word_log_defs
   1.140 -  by (clarsimp simp add : word_ubin.eq_norm nth_bintr bin_nth_ops)
   1.141 +  unfolding word_size by transfer (simp add: bin_nth_ops)
   1.142  
   1.143  lemma word_ao_nth:
   1.144    fixes x :: "'a::len0 word"
   1.145    shows "(x OR y) !! n = (x !! n | y !! n) & 
   1.146           (x AND y) !! n = (x !! n & y !! n)"
   1.147 -  apply (cases "n < size x")
   1.148 -   apply (drule_tac y = "y" in word_ops_nth_size)
   1.149 -   apply simp
   1.150 -  apply (simp add : test_bit_bin word_size)
   1.151 -  done
   1.152 -
   1.153 -lemma test_bit_wi [simp]:
   1.154 -  "(word_of_int x::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a) \<and> bin_nth x n"
   1.155 -  unfolding word_test_bit_def
   1.156 -  by (simp add: nth_bintr [symmetric] word_ubin.eq_norm)
   1.157 +  by transfer (auto simp add: bin_nth_ops)
   1.158  
   1.159  lemma test_bit_numeral [simp]:
   1.160    "(numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
   1.161      n < len_of TYPE('a) \<and> bin_nth (numeral w) n"
   1.162 -  unfolding word_numeral_alt test_bit_wi ..
   1.163 +  by transfer (rule refl)
   1.164  
   1.165  lemma test_bit_neg_numeral [simp]:
   1.166    "(neg_numeral w :: 'a::len0 word) !! n \<longleftrightarrow>
   1.167      n < len_of TYPE('a) \<and> bin_nth (neg_numeral w) n"
   1.168 -  unfolding word_neg_numeral_alt test_bit_wi ..
   1.169 +  by transfer (rule refl)
   1.170  
   1.171  lemma test_bit_1 [simp]: "(1::'a::len word) !! n \<longleftrightarrow> n = 0"
   1.172 -  unfolding word_1_wi test_bit_wi by auto
   1.173 +  by transfer auto
   1.174    
   1.175  lemma nth_0 [simp]: "~ (0::'a::len0 word) !! n"
   1.176 -  unfolding word_test_bit_def by simp
   1.177 +  by transfer simp
   1.178  
   1.179  lemma nth_minus1 [simp]: "(-1::'a::len0 word) !! n \<longleftrightarrow> n < len_of TYPE('a)"
   1.180 -  unfolding word_test_bit_def by (simp add: nth_bintr)
   1.181 +  by transfer simp
   1.182  
   1.183  (* get from commutativity, associativity etc of int_and etc
   1.184    to same for word_and etc *)
   1.185 @@ -2299,15 +2349,12 @@
   1.186  lemma word_add_not [simp]: 
   1.187    fixes x :: "'a::len0 word"
   1.188    shows "x + NOT x = -1"
   1.189 -  using word_of_int_Ex [where x=x] 
   1.190 -  by (auto simp: bwsimps bin_add_not [unfolded Min_def])
   1.191 +  by transfer (simp add: bin_add_not)
   1.192  
   1.193  lemma word_plus_and_or [simp]:
   1.194    fixes x :: "'a::len0 word"
   1.195    shows "(x AND y) + (x OR y) = x + y"
   1.196 -  using word_of_int_Ex [where x=x] 
   1.197 -        word_of_int_Ex [where x=y] 
   1.198 -  by (auto simp: bwsimps plus_and_or)
   1.199 +  by transfer (simp add: plus_and_or)
   1.200  
   1.201  lemma leoa:   
   1.202    fixes x :: "'a::len0 word"