src/HOL/Parity.thy
 changeset 70338 c832d431636b parent 70226 accbd801fefa child 70339 e939ea997f5f
```     1.1 --- a/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
1.2 +++ b/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
1.3 @@ -548,63 +548,6 @@
1.4    qed
1.5  qed
1.6
1.7 -lemma int_parity_induct [case_names zero minus even odd]:
1.8 -  "P k" if zero_int: "P 0"
1.9 -    and minus_int: "P (- 1)"
1.10 -    and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
1.11 -    and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int
1.12 -proof (cases "k \<ge> 0")
1.13 -  case True
1.14 -  define n where "n = nat k"
1.15 -  with True have "k = int n"
1.16 -    by simp
1.17 -  then show "P k"
1.18 -  proof (induction n arbitrary: k rule: nat_parity_induct)
1.19 -    case zero
1.20 -    then show ?case
1.21 -      by (simp add: zero_int)
1.22 -  next
1.23 -    case (even n)
1.24 -    have "P (int n * 2)"
1.25 -      by (rule even_int) (use even in simp_all)
1.26 -    with even show ?case
1.27 -      by (simp add: ac_simps)
1.28 -  next
1.29 -    case (odd n)
1.30 -    have "P (1 + (int n * 2))"
1.31 -      by (rule odd_int) (use odd in simp_all)
1.32 -    with odd show ?case
1.33 -      by (simp add: ac_simps)
1.34 -  qed
1.35 -next
1.36 -  case False
1.37 -  define n where "n = nat (- k - 1)"
1.38 -  with False have "k = - int n - 1"
1.39 -    by simp
1.40 -  then show "P k"
1.41 -  proof (induction n arbitrary: k rule: nat_parity_induct)
1.42 -    case zero
1.43 -    then show ?case
1.44 -      by (simp add: minus_int)
1.45 -  next
1.46 -    case (even n)
1.47 -    have "P (1 + (- int (Suc n) * 2))"
1.48 -      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
1.49 -    also have "\<dots> = - int (2 * n) - 1"
1.50 -      by (simp add: algebra_simps)
1.51 -    finally show ?case
1.52 -      using even by simp
1.53 -  next
1.54 -    case (odd n)
1.55 -    have "P (- int (Suc n) * 2)"
1.56 -      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
1.57 -    also have "\<dots> = - int (Suc (2 * n)) - 1"
1.58 -      by (simp add: algebra_simps)
1.59 -    finally show ?case
1.60 -      using odd by simp
1.61 -  qed
1.62 -qed
1.63 -
1.64  lemma not_mod2_eq_Suc_0_eq_0 [simp]:
1.65    "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
1.66    using not_mod_2_eq_1_eq_0 [of n] by simp
1.67 @@ -759,6 +702,63 @@
1.68  lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
1.69    by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
1.70
1.71 +lemma int_parity_induct [case_names zero minus even odd]:
1.72 +  "P k" if zero_int: "P 0"
1.73 +    and minus_int: "P (- 1)"
1.74 +    and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
1.75 +    and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int
1.76 +proof (cases "k \<ge> 0")
1.77 +  case True
1.78 +  define n where "n = nat k"
1.79 +  with True have "k = int n"
1.80 +    by simp
1.81 +  then show "P k"
1.82 +  proof (induction n arbitrary: k rule: nat_parity_induct)
1.83 +    case zero
1.84 +    then show ?case
1.85 +      by (simp add: zero_int)
1.86 +  next
1.87 +    case (even n)
1.88 +    have "P (int n * 2)"
1.89 +      by (rule even_int) (use even in simp_all)
1.90 +    with even show ?case
1.91 +      by (simp add: ac_simps)
1.92 +  next
1.93 +    case (odd n)
1.94 +    have "P (1 + (int n * 2))"
1.95 +      by (rule odd_int) (use odd in simp_all)
1.96 +    with odd show ?case
1.97 +      by (simp add: ac_simps)
1.98 +  qed
1.99 +next
1.100 +  case False
1.101 +  define n where "n = nat (- k - 1)"
1.102 +  with False have "k = - int n - 1"
1.103 +    by simp
1.104 +  then show "P k"
1.105 +  proof (induction n arbitrary: k rule: nat_parity_induct)
1.106 +    case zero
1.107 +    then show ?case
1.108 +      by (simp add: minus_int)
1.109 +  next
1.110 +    case (even n)
1.111 +    have "P (1 + (- int (Suc n) * 2))"
1.112 +      by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>)
1.113 +    also have "\<dots> = - int (2 * n) - 1"
1.114 +      by (simp add: algebra_simps)
1.115 +    finally show ?case
1.116 +      using even by simp
1.117 +  next
1.118 +    case (odd n)
1.119 +    have "P (- int (Suc n) * 2)"
1.120 +      by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>)
1.121 +    also have "\<dots> = - int (Suc (2 * n)) - 1"
1.122 +      by (simp add: algebra_simps)
1.123 +    finally show ?case
1.124 +      using odd by simp
1.125 +  qed
1.126 +qed
1.127 +
1.128
1.129  subsection \<open>Abstract bit operations\<close>
1.130
```