# HG changeset patch # User huffman # Date 1333635959 -7200 # Node ID 360d7ed4cc0f185c93b50f69638ca6fe153ea1d9 # Parent 776254f89a185954db00f400985116a2fd30e787 use standard quotient lemmas to generate transfer rules diff -r 776254f89a18 -r 360d7ed4cc0f src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Apr 05 15:59:25 2012 +0200 +++ b/src/HOL/Word/Word.thy Thu Apr 05 16:25:59 2012 +0200 @@ -239,33 +239,31 @@ unfolding Quotient_alt_def cr_word_def by (simp add: word_ubin.norm_eq_iff) -lemma equivp_word: - "equivp (\x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)" - by (auto intro!: equivpI reflpI sympI transpI) +lemma reflp_word: + "reflp (\x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)" + by (simp add: reflp_def) local_setup {* - Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm equivp_word} + Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm reflp_word} *} text {* TODO: The next several lemmas could be generated automatically. *} lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word" - unfolding bi_total_def cr_word_def - by (auto intro: word_of_int_uint) + using Quotient_word reflp_word by (rule Quotient_bi_total) lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word" - unfolding right_unique_def cr_word_def by simp + using Quotient_word by (rule Quotient_right_unique) lemma word_eq_transfer [transfer_rule]: "(fun_rel cr_word (fun_rel cr_word op =)) (\x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y) (op = :: 'a::len0 word \ 'a word \ bool)" - unfolding fun_rel_def cr_word_def - by (simp add: word_ubin.norm_eq_iff) + using Quotient_word by (rule Quotient_rel_eq_transfer) lemma word_of_int_transfer [transfer_rule]: "(fun_rel op = cr_word) (\x. x) word_of_int" - unfolding fun_rel_def cr_word_def by simp + using Quotient_word reflp_word by (rule Quotient_id_abs_transfer) lemma uint_transfer [transfer_rule]: "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a)))