equal
deleted
inserted
replaced
84 |
84 |
85 lemma transfer_nat_int_cong: |
85 lemma transfer_nat_int_cong: |
86 "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)" |
86 "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> m \<ge> 0 \<Longrightarrow> [nat x = nat y] (mod (nat m)) \<longleftrightarrow> [x = y] (mod m)" |
87 for x y m :: int |
87 for x y m :: int |
88 unfolding cong_int_def cong_nat_def |
88 unfolding cong_int_def cong_nat_def |
89 by (metis Divides.transfer_int_nat_functions(2) nat_0_le nat_mod_distrib) |
89 by (metis int_nat_eq nat_mod_distrib zmod_int) |
90 |
|
91 |
90 |
92 declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong] |
91 declare transfer_morphism_nat_int [transfer add return: transfer_nat_int_cong] |
93 |
92 |
94 lemma transfer_int_nat_cong: "[int x = int y] (mod (int m)) = [x = y] (mod m)" |
93 lemma transfer_int_nat_cong: "[int x = int y] (mod (int m)) = [x = y] (mod m)" |
95 by (auto simp add: cong_int_def cong_nat_def) (auto simp add: zmod_int [symmetric]) |
94 by (auto simp add: cong_int_def cong_nat_def) (auto simp add: zmod_int [symmetric]) |