use standard quotient lemmas to generate transfer rules
authorhuffman
Thu Apr 05 16:25:59 2012 +0200 (2012-04-05)
changeset 47377360d7ed4cc0f
parent 47376 776254f89a18
child 47378 96e920e0d09a
use standard quotient lemmas to generate transfer rules
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Word/Word.thy	Thu Apr 05 15:59:25 2012 +0200
     1.2 +++ b/src/HOL/Word/Word.thy	Thu Apr 05 16:25:59 2012 +0200
     1.3 @@ -239,33 +239,31 @@
     1.4    unfolding Quotient_alt_def cr_word_def
     1.5    by (simp add: word_ubin.norm_eq_iff)
     1.6  
     1.7 -lemma equivp_word:
     1.8 -  "equivp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
     1.9 -  by (auto intro!: equivpI reflpI sympI transpI)
    1.10 +lemma reflp_word:
    1.11 +  "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
    1.12 +  by (simp add: reflp_def)
    1.13  
    1.14  local_setup {*
    1.15 -  Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm equivp_word}
    1.16 +  Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm reflp_word}
    1.17  *}
    1.18  
    1.19  text {* TODO: The next several lemmas could be generated automatically. *}
    1.20  
    1.21  lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word"
    1.22 -  unfolding bi_total_def cr_word_def
    1.23 -  by (auto intro: word_of_int_uint)
    1.24 +  using Quotient_word reflp_word by (rule Quotient_bi_total)
    1.25  
    1.26  lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word"
    1.27 -  unfolding right_unique_def cr_word_def by simp
    1.28 +  using Quotient_word by (rule Quotient_right_unique)
    1.29  
    1.30  lemma word_eq_transfer [transfer_rule]:
    1.31    "(fun_rel cr_word (fun_rel cr_word op =))
    1.32      (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y)
    1.33      (op = :: 'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool)"
    1.34 -  unfolding fun_rel_def cr_word_def
    1.35 -  by (simp add: word_ubin.norm_eq_iff)
    1.36 +  using Quotient_word by (rule Quotient_rel_eq_transfer)
    1.37  
    1.38  lemma word_of_int_transfer [transfer_rule]:
    1.39    "(fun_rel op = cr_word) (\<lambda>x. x) word_of_int"
    1.40 -  unfolding fun_rel_def cr_word_def by simp
    1.41 +  using Quotient_word reflp_word by (rule Quotient_id_abs_transfer)
    1.42  
    1.43  lemma uint_transfer [transfer_rule]:
    1.44    "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))