89 unfolding fun_rel_def ZN_def by (simp add: zmod_int) |
89 unfolding fun_rel_def ZN_def by (simp add: zmod_int) |
90 |
90 |
91 lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" |
91 lemma ZN_gcd [transfer_rule]: "(ZN ===> ZN ===> ZN) gcd gcd" |
92 unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd) |
92 unfolding fun_rel_def ZN_def by (simp add: transfer_int_nat_gcd) |
93 |
93 |
|
94 lemma ZN_atMost [transfer_rule]: |
|
95 "(ZN ===> set_rel ZN) (atLeastAtMost 0) atMost" |
|
96 unfolding fun_rel_def ZN_def set_rel_def |
|
97 by (clarsimp simp add: Bex_def, arith) |
|
98 |
|
99 lemma ZN_atLeastAtMost [transfer_rule]: |
|
100 "(ZN ===> ZN ===> set_rel ZN) atLeastAtMost atLeastAtMost" |
|
101 unfolding fun_rel_def ZN_def set_rel_def |
|
102 by (clarsimp simp add: Bex_def, arith) |
|
103 |
|
104 lemma ZN_setsum [transfer_rule]: |
|
105 "bi_unique A \<Longrightarrow> ((A ===> ZN) ===> set_rel A ===> ZN) setsum setsum" |
|
106 apply (intro fun_relI) |
|
107 apply (erule (1) bi_unique_set_rel_lemma) |
|
108 apply (simp add: setsum.reindex int_setsum ZN_def fun_rel_def) |
|
109 apply (rule setsum_cong2, simp) |
|
110 done |
|
111 |
94 text {* For derived operations, we can use the @{text "transfer_prover"} |
112 text {* For derived operations, we can use the @{text "transfer_prover"} |
95 method to help generate transfer rules. *} |
113 method to help generate transfer rules. *} |
96 |
114 |
97 lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum" |
115 lemma ZN_listsum [transfer_rule]: "(list_all2 ZN ===> ZN) listsum listsum" |
98 unfolding listsum_def [abs_def] by transfer_prover |
116 unfolding listsum_def [abs_def] by transfer_prover |