# HG changeset patch
# User haftmann
# Date 1560703257 0
# Node ID 7aa64296b9b06e381da9123f1223d615838ea56a
# Parent  ce3c1d8791eb79ec65f5f45b9748b95885ce9063
even more appropriate fact name

diff -r ce3c1d8791eb -r 7aa64296b9b0 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Jun 16 16:40:57 2019 +0000
+++ b/src/HOL/Parity.thy	Sun Jun 16 16:40:57 2019 +0000
@@ -541,7 +541,7 @@
   "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
   using not_mod_2_eq_1_eq_0 [of n] by simp
 
-lemma nat_parity_induct [case_names zero even odd]:
+lemma nat_bit_induct [case_names zero even odd]:
   "P n" if zero: "P 0"
     and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
     and odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
@@ -720,7 +720,7 @@
 lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   by (simp add: even_of_nat [of "nat k", where ?'a = int, symmetric])
 
-lemma int_parity_induct [case_names zero minus even odd]:
+lemma int_bit_induct [case_names zero minus even odd]:
   "P k" if zero_int: "P 0"
     and minus_int: "P (- 1)"
     and even_int: "\<And>k. P k \<Longrightarrow> k \<noteq> 0 \<Longrightarrow> P (k * 2)"
@@ -731,7 +731,7 @@
   with True have "k = int n"
     by simp
   then show "P k"
-  proof (induction n arbitrary: k rule: nat_parity_induct)
+  proof (induction n arbitrary: k rule: nat_bit_induct)
     case zero
     then show ?case
       by (simp add: zero_int)
@@ -754,7 +754,7 @@
   with False have "k = - int n - 1"
     by simp
   then show "P k"
-  proof (induction n arbitrary: k rule: nat_parity_induct)
+  proof (induction n arbitrary: k rule: nat_bit_induct)
     case zero
     then show ?case
       by (simp add: minus_int)
diff -r ce3c1d8791eb -r 7aa64296b9b0 src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Sun Jun 16 16:40:57 2019 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Sun Jun 16 16:40:57 2019 +0000
@@ -61,12 +61,12 @@
 
 lemma not_last_bits_of_nat [simp]:
   "\<not> last (bits_of (of_nat n))"
-  by (induction n rule: nat_parity_induct)
+  by (induction n rule: nat_bit_induct)
     (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
 
 lemma of_unsigned_bits_of_nat:
   "of_unsigned (bits_of (of_nat n)) = of_nat n"
-  by (induction n rule: nat_parity_induct)
+  by (induction n rule: nat_bit_induct)
     (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
 
 end
@@ -106,7 +106,7 @@
 
 lemma last_bits_of_neg_of_nat [simp]:
   "last (bits_of (- 1 - of_nat n))"
-proof (induction n rule: nat_parity_induct)
+proof (induction n rule: nat_bit_induct)
   case zero
   then show ?case
     by simp
@@ -132,7 +132,7 @@
   "of_signed (bits_of (- 1 - of_nat n)) = - 1 - of_nat n"
 proof -
   have "of_unsigned (map Not (bits_of (- 1 - of_nat n))) = of_nat n"
-  proof (induction n rule: nat_parity_induct)
+  proof (induction n rule: nat_bit_induct)
     case zero
     then show ?case
       by simp