src/HOL/Number_Theory/Cong.thy
changeset 35644 d20cf282342e
parent 33718 06e9aff51d17
child 36350 bc7982c54e37
equal deleted inserted replaced
35643:965c24dd6856 35644:d20cf282342e
   129   apply (subst (asm) eq_nat_nat_iff)
   129   apply (subst (asm) eq_nat_nat_iff)
   130   apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
   130   apply (case_tac "m = 0", force, rule pos_mod_sign, force)+
   131   apply assumption
   131   apply assumption
   132 done
   132 done
   133 
   133 
   134 declare TransferMorphism_nat_int[transfer add return: 
   134 declare transfer_morphism_nat_int[transfer add return: 
   135     transfer_nat_int_cong]
   135     transfer_nat_int_cong]
   136 
   136 
   137 lemma transfer_int_nat_cong:
   137 lemma transfer_int_nat_cong:
   138   "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
   138   "[(int x) = (int y)] (mod (int m)) = [x = y] (mod m)"
   139   apply (auto simp add: cong_int_def cong_nat_def)
   139   apply (auto simp add: cong_int_def cong_nat_def)
   140   apply (auto simp add: zmod_int [symmetric])
   140   apply (auto simp add: zmod_int [symmetric])
   141 done
   141 done
   142 
   142 
   143 declare TransferMorphism_int_nat[transfer add return: 
   143 declare transfer_morphism_int_nat[transfer add return: 
   144     transfer_int_nat_cong]
   144     transfer_int_nat_cong]
   145 
   145 
   146 
   146 
   147 subsection {* Congruence *}
   147 subsection {* Congruence *}
   148 
   148