--- a/src/HOL/Parity.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/Parity.thy Fri Jun 14 08:34:27 2019 +0000
@@ -1016,14 +1016,4 @@
"drop_bit n (Suc 0) = of_bool (n = 0)"
using drop_bit_of_1 [where ?'a = nat] by simp
-
-subsection \<open>Legacy\<close>
-
-lemma parity_induct [case_names zero even odd]:
- assumes zero: "P 0"
- assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
- assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
- shows "P n"
- using assms by (rule nat_parity_induct)
-
end
--- a/src/HOL/ex/Bit_Lists.thy Fri Jun 14 08:34:27 2019 +0000
+++ b/src/HOL/ex/Bit_Lists.thy Fri Jun 14 08:34:27 2019 +0000
@@ -61,12 +61,12 @@
lemma not_last_bits_of_nat [simp]:
"\<not> last (bits_of (of_nat n))"
- by (induction n rule: parity_induct)
+ by (induction n rule: nat_parity_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: parity_induct)
+ by (induction n rule: nat_parity_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: parity_induct)
+proof (induction n rule: nat_parity_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: parity_induct)
+ proof (induction n rule: nat_parity_induct)
case zero
then show ?case
by simp