equal
deleted
inserted
replaced
26 |
26 |
27 instance .. |
27 instance .. |
28 |
28 |
29 end |
29 end |
30 |
30 |
|
31 lemma transfer_int_nat_relations: |
|
32 "even (int x) \<longleftrightarrow> even x" |
|
33 by (simp add: even_nat_def) |
|
34 |
|
35 declare TransferMorphism_int_nat[transfer add return: |
|
36 transfer_int_nat_relations |
|
37 ] |
31 |
38 |
32 lemma even_zero_int[simp]: "even (0::int)" by presburger |
39 lemma even_zero_int[simp]: "even (0::int)" by presburger |
33 |
40 |
34 lemma odd_one_int[simp]: "odd (1::int)" by presburger |
41 lemma odd_one_int[simp]: "odd (1::int)" by presburger |
35 |
42 |
308 qed |
315 qed |
309 qed |
316 qed |
310 |
317 |
311 subsection {* General Lemmas About Division *} |
318 subsection {* General Lemmas About Division *} |
312 |
319 |
|
320 (*FIXME move to Divides.thy*) |
|
321 |
313 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" |
322 lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1" |
314 apply (induct "m") |
323 apply (induct "m") |
315 apply (simp_all add: mod_Suc) |
324 apply (simp_all add: mod_Suc) |
316 done |
325 done |
317 |
326 |