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

author | haftmann |

Sun, 16 Jun 2019 16:40:57 +0000 | |

changeset 70353 | 7aa64296b9b0 |

parent 70352 | ce3c1d8791eb |

child 70354 | 9497a6334a26 |

even more appropriate fact name

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

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