237 "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y) |
237 "Quotient (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y) |
238 word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)" |
238 word_of_int uint (cr_word :: _ \<Rightarrow> 'a::len0 word \<Rightarrow> bool)" |
239 unfolding Quotient_alt_def cr_word_def |
239 unfolding Quotient_alt_def cr_word_def |
240 by (simp add: word_ubin.norm_eq_iff) |
240 by (simp add: word_ubin.norm_eq_iff) |
241 |
241 |
242 lemma equivp_word: |
242 lemma reflp_word: |
243 "equivp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)" |
243 "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)" |
244 by (auto intro!: equivpI reflpI sympI transpI) |
244 by (simp add: reflp_def) |
245 |
245 |
246 local_setup {* |
246 local_setup {* |
247 Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm equivp_word} |
247 Lifting_Setup.setup_lifting_infr @{thm Quotient_word} @{thm reflp_word} |
248 *} |
248 *} |
249 |
249 |
250 text {* TODO: The next several lemmas could be generated automatically. *} |
250 text {* TODO: The next several lemmas could be generated automatically. *} |
251 |
251 |
252 lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word" |
252 lemma bi_total_cr_word [transfer_rule]: "bi_total cr_word" |
253 unfolding bi_total_def cr_word_def |
253 using Quotient_word reflp_word by (rule Quotient_bi_total) |
254 by (auto intro: word_of_int_uint) |
|
255 |
254 |
256 lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word" |
255 lemma right_unique_cr_word [transfer_rule]: "right_unique cr_word" |
257 unfolding right_unique_def cr_word_def by simp |
256 using Quotient_word by (rule Quotient_right_unique) |
258 |
257 |
259 lemma word_eq_transfer [transfer_rule]: |
258 lemma word_eq_transfer [transfer_rule]: |
260 "(fun_rel cr_word (fun_rel cr_word op =)) |
259 "(fun_rel cr_word (fun_rel cr_word op =)) |
261 (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y) |
260 (\<lambda>x y. bintrunc (len_of TYPE('a)) x = bintrunc (len_of TYPE('a)) y) |
262 (op = :: 'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool)" |
261 (op = :: 'a::len0 word \<Rightarrow> 'a word \<Rightarrow> bool)" |
263 unfolding fun_rel_def cr_word_def |
262 using Quotient_word by (rule Quotient_rel_eq_transfer) |
264 by (simp add: word_ubin.norm_eq_iff) |
|
265 |
263 |
266 lemma word_of_int_transfer [transfer_rule]: |
264 lemma word_of_int_transfer [transfer_rule]: |
267 "(fun_rel op = cr_word) (\<lambda>x. x) word_of_int" |
265 "(fun_rel op = cr_word) (\<lambda>x. x) word_of_int" |
268 unfolding fun_rel_def cr_word_def by simp |
266 using Quotient_word reflp_word by (rule Quotient_id_abs_transfer) |
269 |
267 |
270 lemma uint_transfer [transfer_rule]: |
268 lemma uint_transfer [transfer_rule]: |
271 "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a))) |
269 "(fun_rel cr_word op =) (bintrunc (len_of TYPE('a))) |
272 (uint :: 'a::len0 word \<Rightarrow> int)" |
270 (uint :: 'a::len0 word \<Rightarrow> int)" |
273 unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm) |
271 unfolding fun_rel_def cr_word_def by (simp add: word_ubin.eq_norm) |