src/HOL/Parity.thy
changeset 70353 7aa64296b9b0
parent 70341 972c0c744e7c
child 70365 4df0628e8545
     1.1 --- a/src/HOL/Parity.thy	Sun Jun 16 16:40:57 2019 +0000
     1.2 +++ b/src/HOL/Parity.thy	Sun Jun 16 16:40:57 2019 +0000
     1.3 @@ -541,7 +541,7 @@
     1.4    "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
     1.5    using not_mod_2_eq_1_eq_0 [of n] by simp
     1.6  
     1.7 -lemma nat_parity_induct [case_names zero even odd]:
     1.8 +lemma nat_bit_induct [case_names zero even odd]:
     1.9    "P n" if zero: "P 0"
    1.10      and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
    1.11      and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
    1.12 @@ -720,7 +720,7 @@
    1.13  lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
    1.14    by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
    1.15  
    1.16 -lemma int_parity_induct [case_names zero minus even odd]:
    1.17 +lemma int_bit_induct [case_names zero minus even odd]:
    1.18    "P k" if zero_int: "P 0"
    1.19      and minus_int: "P (- 1)"
    1.20      and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
    1.21 @@ -731,7 +731,7 @@
    1.22    with True have "k = int n"
    1.23      by simp
    1.24    then show "P k"
    1.25 -  proof (induction n arbitrary: k rule: nat_parity_induct)
    1.26 +  proof (induction n arbitrary: k rule: nat_bit_induct)
    1.27      case zero
    1.28      then show ?case
    1.29        by (simp add: zero_int)
    1.30 @@ -754,7 +754,7 @@
    1.31    with False have "k = - int n - 1"
    1.32      by simp
    1.33    then show "P k"
    1.34 -  proof (induction n arbitrary: k rule: nat_parity_induct)
    1.35 +  proof (induction n arbitrary: k rule: nat_bit_induct)
    1.36      case zero
    1.37      then show ?case
    1.38        by (simp add: minus_int)