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

author | haftmann |

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

changeset 70338 | c832d431636b |

parent 70337 | 48609a6af1a0 |

child 70339 | e939ea997f5f |

slightly more stringent ordering of theorems

--- 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 @@ -548,63 +548,6 @@ qed qed -lemma int_parity_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)" - and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int -proof (cases "k \<ge> 0") - case True - define n where "n = nat k" - with True have "k = int n" - by simp - then show "P k" - proof (induction n arbitrary: k rule: nat_parity_induct) - case zero - then show ?case - by (simp add: zero_int) - next - case (even n) - have "P (int n * 2)" - by (rule even_int) (use even in simp_all) - with even show ?case - by (simp add: ac_simps) - next - case (odd n) - have "P (1 + (int n * 2))" - by (rule odd_int) (use odd in simp_all) - with odd show ?case - by (simp add: ac_simps) - qed -next - case False - define n where "n = nat (- k - 1)" - with False have "k = - int n - 1" - by simp - then show "P k" - proof (induction n arbitrary: k rule: nat_parity_induct) - case zero - then show ?case - by (simp add: minus_int) - next - case (even n) - have "P (1 + (- int (Suc n) * 2))" - by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>) - also have "\<dots> = - int (2 * n) - 1" - by (simp add: algebra_simps) - finally show ?case - using even by simp - next - case (odd n) - have "P (- int (Suc n) * 2)" - by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>) - also have "\<dots> = - int (Suc (2 * n)) - 1" - by (simp add: algebra_simps) - finally show ?case - using odd by simp - qed -qed - lemma not_mod2_eq_Suc_0_eq_0 [simp]: "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0" using not_mod_2_eq_1_eq_0 [of n] by simp @@ -759,6 +702,63 @@ 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]: + "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)" + and odd_int: "\<And>k. P k \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> P (1 + (k * 2))" for k :: int +proof (cases "k \<ge> 0") + case True + define n where "n = nat k" + with True have "k = int n" + by simp + then show "P k" + proof (induction n arbitrary: k rule: nat_parity_induct) + case zero + then show ?case + by (simp add: zero_int) + next + case (even n) + have "P (int n * 2)" + by (rule even_int) (use even in simp_all) + with even show ?case + by (simp add: ac_simps) + next + case (odd n) + have "P (1 + (int n * 2))" + by (rule odd_int) (use odd in simp_all) + with odd show ?case + by (simp add: ac_simps) + qed +next + case False + define n where "n = nat (- k - 1)" + with False have "k = - int n - 1" + by simp + then show "P k" + proof (induction n arbitrary: k rule: nat_parity_induct) + case zero + then show ?case + by (simp add: minus_int) + next + case (even n) + have "P (1 + (- int (Suc n) * 2))" + by (rule odd_int) (use even in \<open>simp_all add: algebra_simps\<close>) + also have "\<dots> = - int (2 * n) - 1" + by (simp add: algebra_simps) + finally show ?case + using even by simp + next + case (odd n) + have "P (- int (Suc n) * 2)" + by (rule even_int) (use odd in \<open>simp_all add: algebra_simps\<close>) + also have "\<dots> = - int (Suc (2 * n)) - 1" + by (simp add: algebra_simps) + finally show ?case + using odd by simp + qed +qed + subsection \<open>Abstract bit operations\<close>