summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Fri, 14 Jun 2019 08:34:27 +0000 | |

changeset 70339 | e939ea997f5f |

parent 70338 | c832d431636b |

child 70340 | 7383930fc946 |

dropped weaker legacy alias

src/HOL/Parity.thy | file | annotate | diff | comparison | revisions | |

src/HOL/ex/Bit_Lists.thy | file | annotate | diff | comparison | revisions |

--- 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