src/HOL/Parity.thy
changeset 66816 212a3334e7da
parent 66815 93c6632ddf44
child 66839 909ba5ed93dd
     1.1 --- a/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
     1.2 +++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
     1.3 @@ -483,4 +483,40 @@
     1.4  
     1.5  end
     1.6  
     1.7 +
     1.8 +subsection \<open>Instance for @{typ int}\<close>
     1.9 +
    1.10 +instance int :: ring_parity
    1.11 +proof
    1.12 +  fix k l :: int
    1.13 +  show "k mod 2 = 1" if "\<not> 2 dvd k"
    1.14 +  proof (rule order_antisym)
    1.15 +    have "0 \<le> k mod 2" and "k mod 2 < 2"
    1.16 +      by auto
    1.17 +    moreover have "k mod 2 \<noteq> 0"
    1.18 +      using that by (simp add: dvd_eq_mod_eq_0)
    1.19 +    ultimately have "0 < k mod 2"
    1.20 +      by (simp only: less_le) simp
    1.21 +    then show "1 \<le> k mod 2"
    1.22 +      by simp
    1.23 +    from \<open>k mod 2 < 2\<close> show "k mod 2 \<le> 1"
    1.24 +      by (simp only: less_le) simp
    1.25 +  qed
    1.26 +qed (simp_all add: dvd_eq_mod_eq_0 divide_int_def)
    1.27 +
    1.28 +lemma even_diff_iff [simp]:
    1.29 +  "even (k - l) \<longleftrightarrow> even (k + l)" for k l :: int
    1.30 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
    1.31 +
    1.32 +lemma even_abs_add_iff [simp]:
    1.33 +  "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)" for k l :: int
    1.34 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
    1.35 +
    1.36 +lemma even_add_abs_iff [simp]:
    1.37 +  "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)" for k l :: int
    1.38 +  using even_abs_add_iff [of l k] by (simp add: ac_simps)
    1.39 +
    1.40 +lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
    1.41 +  by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
    1.42 +
    1.43  end