equal
deleted
inserted
replaced
1014 |
1014 |
1015 lemma drop_bit_of_Suc_0 [simp]: |
1015 lemma drop_bit_of_Suc_0 [simp]: |
1016 "drop_bit n (Suc 0) = of_bool (n = 0)" |
1016 "drop_bit n (Suc 0) = of_bool (n = 0)" |
1017 using drop_bit_of_1 [where ?'a = nat] by simp |
1017 using drop_bit_of_1 [where ?'a = nat] by simp |
1018 |
1018 |
1019 |
|
1020 subsection \<open>Legacy\<close> |
|
1021 |
|
1022 lemma parity_induct [case_names zero even odd]: |
|
1023 assumes zero: "P 0" |
|
1024 assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)" |
|
1025 assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))" |
|
1026 shows "P n" |
|
1027 using assms by (rule nat_parity_induct) |
|
1028 |
|
1029 end |
1019 end |