src/HOL/Word/WordGenLib.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 30034 60f64f112174
child 30729 461ee3e49ad3
permissions -rw-r--r--
added lemmas
     1 (* Author: Gerwin Klein, Jeremy Dawson
     2 
     3    Miscellaneous additional library definitions and lemmas for 
     4    the word type. Instantiation to boolean algebras, definition
     5    of recursion and induction patterns for words.
     6 *)
     7 
     8 header {* Miscellaneous Library for Words *}
     9 
    10 theory WordGenLib
    11 imports WordShift Boolean_Algebra
    12 begin
    13 
    14 declare of_nat_2p [simp]
    15 
    16 lemma word_int_cases:
    17   "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len0 word) = word_of_int n; 0 \<le> n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
    18    \<Longrightarrow> P"
    19   by (cases x rule: word_uint.Abs_cases) (simp add: uints_num)
    20 
    21 lemma word_nat_cases [cases type: word]:
    22   "\<lbrakk>\<And>n. \<lbrakk>(x ::'a::len word) = of_nat n; n < 2^len_of TYPE('a)\<rbrakk> \<Longrightarrow> P\<rbrakk>
    23    \<Longrightarrow> P"
    24   by (cases x rule: word_unat.Abs_cases) (simp add: unats_def)
    25 
    26 lemma max_word_eq:
    27   "(max_word::'a::len word) = 2^len_of TYPE('a) - 1"
    28   by (simp add: max_word_def word_of_int_hom_syms word_of_int_2p)
    29 
    30 lemma max_word_max [simp,intro!]:
    31   "n \<le> max_word"
    32   by (cases n rule: word_int_cases)
    33      (simp add: max_word_def word_le_def int_word_uint int_mod_eq')
    34   
    35 lemma word_of_int_2p_len: 
    36   "word_of_int (2 ^ len_of TYPE('a)) = (0::'a::len0 word)"
    37   by (subst word_uint.Abs_norm [symmetric]) 
    38      (simp add: word_of_int_hom_syms)
    39 
    40 lemma word_pow_0:
    41   "(2::'a::len word) ^ len_of TYPE('a) = 0"
    42 proof -
    43   have "word_of_int (2 ^ len_of TYPE('a)) = (0::'a word)"
    44     by (rule word_of_int_2p_len)
    45   thus ?thesis by (simp add: word_of_int_2p)
    46 qed
    47 
    48 lemma max_word_wrap: "x + 1 = 0 \<Longrightarrow> x = max_word"
    49   apply (simp add: max_word_eq)
    50   apply uint_arith
    51   apply auto
    52   apply (simp add: word_pow_0)
    53   done
    54 
    55 lemma max_word_minus: 
    56   "max_word = (-1::'a::len word)"
    57 proof -
    58   have "-1 + 1 = (0::'a word)" by simp
    59   thus ?thesis by (rule max_word_wrap [symmetric])
    60 qed
    61 
    62 lemma max_word_bl [simp]:
    63   "to_bl (max_word::'a::len word) = replicate (len_of TYPE('a)) True"
    64   by (subst max_word_minus to_bl_n1)+ simp
    65 
    66 lemma max_test_bit [simp]:
    67   "(max_word::'a::len word) !! n = (n < len_of TYPE('a))"
    68   by (auto simp add: test_bit_bl word_size)
    69 
    70 lemma word_and_max [simp]:
    71   "x AND max_word = x"
    72   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
    73 
    74 lemma word_or_max [simp]:
    75   "x OR max_word = max_word"
    76   by (rule word_eqI) (simp add: word_ops_nth_size word_size)
    77 
    78 lemma word_ao_dist2:
    79   "x AND (y OR z) = x AND y OR x AND (z::'a::len0 word)"
    80   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
    81 
    82 lemma word_oa_dist2:
    83   "x OR y AND z = (x OR y) AND (x OR (z::'a::len0 word))"
    84   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
    85 
    86 lemma word_and_not [simp]:
    87   "x AND NOT x = (0::'a::len0 word)"
    88   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
    89 
    90 lemma word_or_not [simp]:
    91   "x OR NOT x = max_word"
    92   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
    93 
    94 lemma word_boolean:
    95   "boolean (op AND) (op OR) bitNOT 0 max_word"
    96   apply (rule boolean.intro)
    97            apply (rule word_bw_assocs)
    98           apply (rule word_bw_assocs)
    99          apply (rule word_bw_comms)
   100         apply (rule word_bw_comms)
   101        apply (rule word_ao_dist2)
   102       apply (rule word_oa_dist2)
   103      apply (rule word_and_max)
   104     apply (rule word_log_esimps)
   105    apply (rule word_and_not)
   106   apply (rule word_or_not)
   107   done
   108 
   109 interpretation word_bool_alg!:
   110   boolean "op AND" "op OR" bitNOT 0 max_word
   111   by (rule word_boolean)
   112 
   113 lemma word_xor_and_or:
   114   "x XOR y = x AND NOT y OR NOT x AND (y::'a::len0 word)"
   115   by (rule word_eqI) (auto simp add: word_ops_nth_size word_size)
   116 
   117 interpretation word_bool_alg!:
   118   boolean_xor "op AND" "op OR" bitNOT 0 max_word "op XOR"
   119   apply (rule boolean_xor.intro)
   120    apply (rule word_boolean)
   121   apply (rule boolean_xor_axioms.intro)
   122   apply (rule word_xor_and_or)
   123   done
   124 
   125 lemma shiftr_0 [iff]:
   126   "(x::'a::len0 word) >> 0 = x"
   127   by (simp add: shiftr_bl)
   128 
   129 lemma shiftl_0 [simp]: 
   130   "(x :: 'a :: len word) << 0 = x"
   131   by (simp add: shiftl_t2n)
   132 
   133 lemma shiftl_1 [simp]:
   134   "(1::'a::len word) << n = 2^n"
   135   by (simp add: shiftl_t2n)
   136 
   137 lemma uint_lt_0 [simp]:
   138   "uint x < 0 = False"
   139   by (simp add: linorder_not_less)
   140 
   141 lemma shiftr1_1 [simp]: 
   142   "shiftr1 (1::'a::len word) = 0"
   143   by (simp add: shiftr1_def word_0_alt)
   144 
   145 lemma shiftr_1[simp]: 
   146   "(1::'a::len word) >> n = (if n = 0 then 1 else 0)"
   147   by (induct n) (auto simp: shiftr_def)
   148 
   149 lemma word_less_1 [simp]: 
   150   "((x::'a::len word) < 1) = (x = 0)"
   151   by (simp add: word_less_nat_alt unat_0_iff)
   152 
   153 lemma to_bl_mask:
   154   "to_bl (mask n :: 'a::len word) = 
   155   replicate (len_of TYPE('a) - n) False @ 
   156     replicate (min (len_of TYPE('a)) n) True"
   157   by (simp add: mask_bl word_rep_drop min_def)
   158 
   159 lemma map_replicate_True:
   160   "n = length xs ==>
   161     map (\<lambda>(x,y). x & y) (zip xs (replicate n True)) = xs"
   162   by (induct xs arbitrary: n) auto
   163 
   164 lemma map_replicate_False:
   165   "n = length xs ==> map (\<lambda>(x,y). x & y)
   166     (zip xs (replicate n False)) = replicate n False"
   167   by (induct xs arbitrary: n) auto
   168 
   169 lemma bl_and_mask:
   170   fixes w :: "'a::len word"
   171   fixes n
   172   defines "n' \<equiv> len_of TYPE('a) - n"
   173   shows "to_bl (w AND mask n) =  replicate n' False @ drop n' (to_bl w)"
   174 proof - 
   175   note [simp] = map_replicate_True map_replicate_False
   176   have "to_bl (w AND mask n) = 
   177         map2 op & (to_bl w) (to_bl (mask n::'a::len word))"
   178     by (simp add: bl_word_and)
   179   also
   180   have "to_bl w = take n' (to_bl w) @ drop n' (to_bl w)" by simp
   181   also
   182   have "map2 op & \<dots> (to_bl (mask n::'a::len word)) = 
   183         replicate n' False @ drop n' (to_bl w)"
   184     unfolding to_bl_mask n'_def map2_def
   185     by (subst zip_append) auto
   186   finally
   187   show ?thesis .
   188 qed
   189 
   190 lemma drop_rev_takefill:
   191   "length xs \<le> n ==>
   192     drop (n - length xs) (rev (takefill False n (rev xs))) = xs"
   193   by (simp add: takefill_alt rev_take)
   194 
   195 lemma map_nth_0 [simp]:
   196   "map (op !! (0::'a::len0 word)) xs = replicate (length xs) False"
   197   by (induct xs) auto
   198 
   199 lemma uint_plus_if_size:
   200   "uint (x + y) = 
   201   (if uint x + uint y < 2^size x then 
   202       uint x + uint y 
   203    else 
   204       uint x + uint y - 2^size x)" 
   205   by (simp add: word_arith_alts int_word_uint mod_add_if_z 
   206                 word_size)
   207 
   208 lemma unat_plus_if_size:
   209   "unat (x + (y::'a::len word)) = 
   210   (if unat x + unat y < 2^size x then 
   211       unat x + unat y 
   212    else 
   213       unat x + unat y - 2^size x)" 
   214   apply (subst word_arith_nat_defs)
   215   apply (subst unat_of_nat)
   216   apply (simp add:  mod_nat_add word_size)
   217   done
   218 
   219 lemma word_neq_0_conv [simp]:
   220   fixes w :: "'a :: len word"
   221   shows "(w \<noteq> 0) = (0 < w)"
   222 proof -
   223   have "0 \<le> w" by (rule word_zero_le)
   224   thus ?thesis by (auto simp add: word_less_def)
   225 qed
   226 
   227 lemma max_lt:
   228   "unat (max a b div c) = unat (max a b) div unat (c:: 'a :: len word)"
   229   apply (subst word_arith_nat_defs)
   230   apply (subst word_unat.eq_norm)
   231   apply (subst mod_if)
   232   apply clarsimp
   233   apply (erule notE)
   234   apply (insert div_le_dividend [of "unat (max a b)" "unat c"])
   235   apply (erule order_le_less_trans)
   236   apply (insert unat_lt2p [of "max a b"])
   237   apply simp
   238   done
   239 
   240 lemma uint_sub_if_size:
   241   "uint (x - y) = 
   242   (if uint y \<le> uint x then 
   243       uint x - uint y 
   244    else 
   245       uint x - uint y + 2^size x)"
   246   by (simp add: word_arith_alts int_word_uint mod_sub_if_z 
   247                 word_size)
   248 
   249 lemma unat_sub_simple:
   250   "x \<le> y ==> unat (y - x) = unat y - unat x"
   251   by (simp add: unat_def uint_sub_if_size word_le_def nat_diff_distrib)
   252 
   253 lemmas unat_sub = unat_sub_simple
   254 
   255 lemma word_less_sub1:
   256   fixes x :: "'a :: len word"
   257   shows "x \<noteq> 0 ==> 1 < x = (0 < x - 1)"
   258   by (simp add: unat_sub_if_size word_less_nat_alt)
   259 
   260 lemma word_le_sub1:
   261   fixes x :: "'a :: len word"
   262   shows "x \<noteq> 0 ==> 1 \<le> x = (0 \<le> x - 1)"
   263   by (simp add: unat_sub_if_size order_le_less word_less_nat_alt)
   264 
   265 lemmas word_less_sub1_numberof [simp] =
   266   word_less_sub1 [of "number_of w", standard]
   267 lemmas word_le_sub1_numberof [simp] =
   268   word_le_sub1 [of "number_of w", standard]
   269   
   270 lemma word_of_int_minus: 
   271   "word_of_int (2^len_of TYPE('a) - i) = (word_of_int (-i)::'a::len word)"
   272 proof -
   273   have x: "2^len_of TYPE('a) - i = -i + 2^len_of TYPE('a)" by simp
   274   show ?thesis
   275     apply (subst x)
   276     apply (subst word_uint.Abs_norm [symmetric], subst mod_add_self2)
   277     apply simp
   278     done
   279 qed
   280   
   281 lemmas word_of_int_inj = 
   282   word_uint.Abs_inject [unfolded uints_num, simplified]
   283 
   284 lemma word_le_less_eq:
   285   "(x ::'z::len word) \<le> y = (x = y \<or> x < y)"
   286   by (auto simp add: word_less_def)
   287 
   288 lemma mod_plus_cong:
   289   assumes 1: "(b::int) = b'"
   290       and 2: "x mod b' = x' mod b'"
   291       and 3: "y mod b' = y' mod b'"
   292       and 4: "x' + y' = z'"
   293   shows "(x + y) mod b = z' mod b'"
   294 proof -
   295   from 1 2[symmetric] 3[symmetric] have "(x + y) mod b = (x' mod b' + y' mod b') mod b'"
   296     by (simp add: mod_add_eq[symmetric])
   297   also have "\<dots> = (x' + y') mod b'"
   298     by (simp add: mod_add_eq[symmetric])
   299   finally show ?thesis by (simp add: 4)
   300 qed
   301 
   302 lemma mod_minus_cong:
   303   assumes 1: "(b::int) = b'"
   304       and 2: "x mod b' = x' mod b'"
   305       and 3: "y mod b' = y' mod b'"
   306       and 4: "x' - y' = z'"
   307   shows "(x - y) mod b = z' mod b'"
   308   using assms
   309   apply (subst zmod_zsub_left_eq)
   310   apply (subst zmod_zsub_right_eq)
   311   apply (simp add: zmod_zsub_left_eq [symmetric] zmod_zsub_right_eq [symmetric])
   312   done
   313 
   314 lemma word_induct_less: 
   315   "\<lbrakk>P (0::'a::len word); \<And>n. \<lbrakk>n < m; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
   316   apply (cases m)
   317   apply atomize
   318   apply (erule rev_mp)+
   319   apply (rule_tac x=m in spec)
   320   apply (induct_tac n)
   321    apply simp
   322   apply clarsimp
   323   apply (erule impE)
   324    apply clarsimp
   325    apply (erule_tac x=n in allE)
   326    apply (erule impE)
   327     apply (simp add: unat_arith_simps)
   328     apply (clarsimp simp: unat_of_nat)
   329    apply simp
   330   apply (erule_tac x="of_nat na" in allE)
   331   apply (erule impE)
   332    apply (simp add: unat_arith_simps)
   333    apply (clarsimp simp: unat_of_nat)
   334   apply simp
   335   done
   336   
   337 lemma word_induct: 
   338   "\<lbrakk>P (0::'a::len word); \<And>n. P n \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P m"
   339   by (erule word_induct_less, simp)
   340 
   341 lemma word_induct2 [induct type]: 
   342   "\<lbrakk>P 0; \<And>n. \<lbrakk>1 + n \<noteq> 0; P n\<rbrakk> \<Longrightarrow> P (1 + n)\<rbrakk> \<Longrightarrow> P (n::'b::len word)"
   343   apply (rule word_induct, simp)
   344   apply (case_tac "1+n = 0", auto)
   345   done
   346 
   347 constdefs
   348   word_rec :: "'a \<Rightarrow> ('b::len word \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b word \<Rightarrow> 'a"
   349   "word_rec forZero forSuc n \<equiv> nat_rec forZero (forSuc \<circ> of_nat) (unat n)"
   350 
   351 lemma word_rec_0: "word_rec z s 0 = z"
   352   by (simp add: word_rec_def)
   353 
   354 lemma word_rec_Suc: 
   355   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> word_rec z s (1 + n) = s n (word_rec z s n)"
   356   apply (simp add: word_rec_def unat_word_ariths)
   357   apply (subst nat_mod_eq')
   358    apply (cut_tac x=n in unat_lt2p)
   359    apply (drule Suc_mono)
   360    apply (simp add: less_Suc_eq_le)
   361    apply (simp only: order_less_le, simp)
   362    apply (erule contrapos_pn, simp)
   363    apply (drule arg_cong[where f=of_nat])
   364    apply simp
   365    apply (subst (asm) word_unat.Rep_inverse[of n])
   366    apply simp
   367   apply simp
   368   done
   369 
   370 lemma word_rec_Pred: 
   371   "n \<noteq> 0 \<Longrightarrow> word_rec z s n = s (n - 1) (word_rec z s (n - 1))"
   372   apply (rule subst[where t="n" and s="1 + (n - 1)"])
   373    apply simp
   374   apply (subst word_rec_Suc)
   375    apply simp
   376   apply simp
   377   done
   378 
   379 lemma word_rec_in: 
   380   "f (word_rec z (\<lambda>_. f) n) = word_rec (f z) (\<lambda>_. f) n"
   381   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
   382 
   383 lemma word_rec_in2: 
   384   "f n (word_rec z f n) = word_rec (f 0 z) (f \<circ> op + 1) n"
   385   by (induct n) (simp_all add: word_rec_0 word_rec_Suc)
   386 
   387 lemma word_rec_twice: 
   388   "m \<le> n \<Longrightarrow> word_rec z f n = word_rec (word_rec z f (n - m)) (f \<circ> op + (n - m)) m"
   389 apply (erule rev_mp)
   390 apply (rule_tac x=z in spec)
   391 apply (rule_tac x=f in spec)
   392 apply (induct n)
   393  apply (simp add: word_rec_0)
   394 apply clarsimp
   395 apply (rule_tac t="1 + n - m" and s="1 + (n - m)" in subst)
   396  apply simp
   397 apply (case_tac "1 + (n - m) = 0")
   398  apply (simp add: word_rec_0)
   399  apply (rule_tac f = "word_rec ?a ?b" in arg_cong)
   400  apply (rule_tac t="m" and s="m + (1 + (n - m))" in subst)
   401   apply simp
   402  apply (simp (no_asm_use))
   403 apply (simp add: word_rec_Suc word_rec_in2)
   404 apply (erule impE)
   405  apply uint_arith
   406 apply (drule_tac x="x \<circ> op + 1" in spec)
   407 apply (drule_tac x="x 0 xa" in spec)
   408 apply simp
   409 apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
   410        in subst)
   411  apply (clarsimp simp add: expand_fun_eq)
   412  apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
   413   apply simp
   414  apply (rule refl)
   415 apply (rule refl)
   416 done
   417 
   418 lemma word_rec_id: "word_rec z (\<lambda>_. id) n = z"
   419   by (induct n) (auto simp add: word_rec_0 word_rec_Suc)
   420 
   421 lemma word_rec_id_eq: "\<forall>m < n. f m = id \<Longrightarrow> word_rec z f n = z"
   422 apply (erule rev_mp)
   423 apply (induct n)
   424  apply (auto simp add: word_rec_0 word_rec_Suc)
   425  apply (drule spec, erule mp)
   426  apply uint_arith
   427 apply (drule_tac x=n in spec, erule impE)
   428  apply uint_arith
   429 apply simp
   430 done
   431 
   432 lemma word_rec_max: 
   433   "\<forall>m\<ge>n. m \<noteq> -1 \<longrightarrow> f m = id \<Longrightarrow> word_rec z f -1 = word_rec z f n"
   434 apply (subst word_rec_twice[where n="-1" and m="-1 - n"])
   435  apply simp
   436 apply simp
   437 apply (rule word_rec_id_eq)
   438 apply clarsimp
   439 apply (drule spec, rule mp, erule mp)
   440  apply (rule word_plus_mono_right2[OF _ order_less_imp_le])
   441   prefer 2 
   442   apply assumption
   443  apply simp
   444 apply (erule contrapos_pn)
   445 apply simp
   446 apply (drule arg_cong[where f="\<lambda>x. x - n"])
   447 apply simp
   448 done
   449 
   450 lemma unatSuc: 
   451   "1 + n \<noteq> (0::'a::len word) \<Longrightarrow> unat (1 + n) = Suc (unat n)"
   452   by unat_arith
   453 
   454 
   455 lemmas word_no_1 [simp] = word_1_no [symmetric, unfolded BIT_simps]
   456 lemmas word_no_0 [simp] = word_0_no [symmetric]
   457 
   458 declare word_0_bl [simp]
   459 declare bin_to_bl_def [simp]
   460 declare to_bl_0 [simp]
   461 declare of_bl_True [simp]
   462 
   463 end