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