dropped weaker legacy alias
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (4 weeks ago)
changeset 70339e939ea997f5f
parent 70338 c832d431636b
child 70340 7383930fc946
dropped weaker legacy alias
src/HOL/Parity.thy
src/HOL/ex/Bit_Lists.thy
     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 @@ -1016,14 +1016,4 @@
     1.4    "drop_bit n (Suc 0) = of_bool (n = 0)"
     1.5    using drop_bit_of_1 [where ?'a = nat] by simp
     1.6  
     1.7 -
     1.8 -subsection \<open>Legacy\<close>
     1.9 -
    1.10 -lemma parity_induct [case_names zero even odd]:
    1.11 -  assumes zero: "P 0"
    1.12 -  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
    1.13 -  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
    1.14 -  shows "P n"
    1.15 -  using assms by (rule nat_parity_induct)
    1.16 -
    1.17  end
     2.1 --- a/src/HOL/ex/Bit_Lists.thy	Fri Jun 14 08:34:27 2019 +0000
     2.2 +++ b/src/HOL/ex/Bit_Lists.thy	Fri Jun 14 08:34:27 2019 +0000
     2.3 @@ -61,12 +61,12 @@
     2.4  
     2.5  lemma not_last_bits_of_nat [simp]:
     2.6    "\<not> last (bits_of (of_nat n))"
     2.7 -  by (induction n rule: parity_induct)
     2.8 +  by (induction n rule: nat_parity_induct)
     2.9      (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
    2.10  
    2.11  lemma of_unsigned_bits_of_nat:
    2.12    "of_unsigned (bits_of (of_nat n)) = of_nat n"
    2.13 -  by (induction n rule: parity_induct)
    2.14 +  by (induction n rule: nat_parity_induct)
    2.15      (use of_nat_neq_0 in \<open>simp_all add: algebra_simps\<close>)
    2.16  
    2.17  end
    2.18 @@ -106,7 +106,7 @@
    2.19  
    2.20  lemma last_bits_of_neg_of_nat [simp]:
    2.21    "last (bits_of (- 1 - of_nat n))"
    2.22 -proof (induction n rule: parity_induct)
    2.23 +proof (induction n rule: nat_parity_induct)
    2.24    case zero
    2.25    then show ?case
    2.26      by simp
    2.27 @@ -132,7 +132,7 @@
    2.28    "of_signed (bits_of (- 1 - of_nat n)) = - 1 - of_nat n"
    2.29  proof -
    2.30    have "of_unsigned (map Not (bits_of (- 1 - of_nat n))) = of_nat n"
    2.31 -  proof (induction n rule: parity_induct)
    2.32 +  proof (induction n rule: nat_parity_induct)
    2.33      case zero
    2.34      then show ?case
    2.35        by simp