src/HOL/Word/Word.thy
changeset 51375 d9e62d9c98de
parent 51286 44a521ff87cf
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Word/Word.thy	Fri Mar 08 13:14:23 2013 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Fri Mar 08 13:21:06 2013 +0100
     1.3 @@ -247,9 +247,9 @@
     1.4  text {* TODO: The next lemma could be generated automatically. *}
     1.5  
     1.6  lemma uint_transfer [transfer_rule]:
     1.7 -  "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))
     1.8 +  "(fun_rel pcr_word op =) (bintrunc (len_of TYPE('a)))
     1.9      (uint :: 'a::len0 word \<Rightarrow> int)"
    1.10 -  unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm)
    1.11 +  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by (simp add: word_ubin.eq_norm)
    1.12  
    1.13  subsection  "Arithmetic operations"
    1.14  
    1.15 @@ -599,9 +599,9 @@
    1.16  declare word_neg_numeral_alt [symmetric, code_abbrev]
    1.17  
    1.18  lemma word_numeral_transfer [transfer_rule]:
    1.19 -  "(fun_rel op = cr_word) numeral numeral"
    1.20 -  "(fun_rel op = cr_word) neg_numeral neg_numeral"
    1.21 -  unfolding fun_rel_def cr_word_def word_numeral_alt word_neg_numeral_alt
    1.22 +  "(fun_rel op = pcr_word) numeral numeral"
    1.23 +  "(fun_rel op = pcr_word) neg_numeral neg_numeral"
    1.24 +  unfolding fun_rel_def word.pcr_cr_eq cr_word_def word_numeral_alt word_neg_numeral_alt
    1.25    by simp_all
    1.26  
    1.27  lemma uint_bintrunc [simp]:
    1.28 @@ -2194,9 +2194,9 @@
    1.29    by (simp add: word_ubin.eq_norm nth_bintr)
    1.30  
    1.31  lemma word_test_bit_transfer [transfer_rule]:
    1.32 -  "(fun_rel cr_word (fun_rel op = op =))
    1.33 +  "(fun_rel pcr_word (fun_rel op = op =))
    1.34      (\<lambda>x n. n < len_of TYPE('a) \<and> bin_nth x n) (test_bit :: 'a::len0 word \<Rightarrow> _)"
    1.35 -  unfolding fun_rel_def cr_word_def by simp
    1.36 +  unfolding fun_rel_def word.pcr_cr_eq cr_word_def by simp
    1.37  
    1.38  lemma word_ops_nth_size:
    1.39    "n < size (x::'a::len0 word) \<Longrightarrow>