src/HOL/Parity.thy
changeset 33318 ddd97d9dfbfb
parent 31718 7715d4d3586f
child 33358 3495dbba0da2
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 29 08:14:39 2009 +0100
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 29 11:41:36 2009 +0100
     1.3 @@ -28,6 +28,13 @@
     1.4  
     1.5  end
     1.6  
     1.7 +lemma transfer_int_nat_relations:
     1.8 +  "even (int x) \<longleftrightarrow> even x"
     1.9 +  by (simp add: even_nat_def)
    1.10 +
    1.11 +declare TransferMorphism_int_nat[transfer add return:
    1.12 +  transfer_int_nat_relations
    1.13 +]
    1.14  
    1.15  lemma even_zero_int[simp]: "even (0::int)" by presburger
    1.16  
    1.17 @@ -310,6 +317,8 @@
    1.18  
    1.19  subsection {* General Lemmas About Division *}
    1.20  
    1.21 +(*FIXME move to Divides.thy*)
    1.22 +
    1.23  lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" 
    1.24  apply (induct "m")
    1.25  apply (simp_all add: mod_Suc)