author haftmann Thu, 23 Oct 2014 19:40:41 +0200 changeset 58778 e29cae8eab1f parent 58777 6ba2f1fa243b child 58781 c385da5c665e
even further downshift of theory Parity in the hierarchy
 src/HOL/Divides.thy file | annotate | diff | comparison | revisions src/HOL/Parity.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Divides.thy	Thu Oct 23 19:40:39 2014 +0200
+++ b/src/HOL/Divides.thy	Thu Oct 23 19:40:41 2014 +0200
@@ -6,7 +6,7 @@
header {* The division operators div and mod *}

theory Divides
-imports Nat_Transfer
+imports Parity
begin

subsection {* Syntactic division operations *}
@@ -504,6 +504,9 @@

end

+
+subsubsection {* Parity and division *}
+
class semiring_div_parity = semiring_div + semiring_numeral +
assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
assumes one_mod_two_eq_one: "1 mod 2 = 1"
@@ -524,6 +527,76 @@
"a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
by (cases a rule: parity_cases) simp_all

+lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
+  "1 div 2 = 0"
+proof (cases "2 = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
+  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
+  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
+  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
+  with False show ?thesis by auto
+qed
+
+subclass semiring_parity
+proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
+  fix a b c
+  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
+    by simp
+next
+  fix a b c
+  assume "(b + c) mod a = 0"
+  with mod_add_eq [of b c a]
+  have "(b mod a + c mod a) mod a = 0"
+    by simp
+  moreover assume "b mod a = 0"
+  ultimately show "c mod a = 0"
+    by simp
+next
+  show "1 mod 2 = 1"
+    by (fact one_mod_two_eq_one)
+next
+  fix a b
+  assume "a mod 2 = 1"
+  moreover assume "b mod 2 = 1"
+  ultimately show "(a + b) mod 2 = 0"
+    using mod_add_eq [of a b 2] by simp
+next
+  fix a b
+  assume "(a * b) mod 2 = 0"
+  then have "(a mod 2) * (b mod 2) = 0"
+    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
+  then show "a mod 2 = 0 \<or> b mod 2 = 0"
+    by (rule divisors_zero)
+next
+  fix a
+  assume "a mod 2 = 1"
+  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
+  then show "\<exists>b. a = b + 1" ..
+qed
+
+lemma even_iff_mod_2_eq_zero:
+  "even a \<longleftrightarrow> a mod 2 = 0"
+  by (fact dvd_eq_mod_eq_0)
+
+lemma even_succ_div_two [simp]:
+  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
+  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
+
+lemma odd_succ_div_two [simp]:
+  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
+
+lemma even_two_times_div_two:
+  "even a \<Longrightarrow> 2 * (a div 2) = a"
+  by (fact dvd_mult_div_cancel)
+
+lemma odd_two_times_div_two_succ:
+  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
+  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
+
end

@@ -1451,6 +1524,44 @@
instance nat :: semiring_numeral_div
by intro_classes (auto intro: div_positive simp add: mult_div_cancel mod_mult2_eq div_mult2_eq)

+lemma even_Suc_div_two [simp]:
+  "even n \<Longrightarrow> Suc n div 2 = n div 2"
+  using even_succ_div_two [of n] by simp
+
+lemma odd_Suc_div_two [simp]:
+  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
+  using odd_succ_div_two [of n] by simp
+
+lemma odd_two_times_div_two_Suc:
+  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
+  using odd_two_times_div_two_succ [of n] by simp
+
+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"
+proof (induct n rule: less_induct)
+  case (less n)
+  show "P n"
+  proof (cases "n = 0")
+    case True with zero show ?thesis by simp
+  next
+    case False
+    with less have hyp: "P (n div 2)" by simp
+    show ?thesis
+    proof (cases "even n")
+      case True
+      with hyp even [of "n div 2"] show ?thesis
+    next
+      case False
+      with hyp odd [of "n div 2"] show ?thesis
+    qed
+  qed
+qed
+

subsection {* Division on @{typ int} *}

--- a/src/HOL/Parity.thy	Thu Oct 23 19:40:39 2014 +0200
+++ b/src/HOL/Parity.thy	Thu Oct 23 19:40:41 2014 +0200
@@ -6,7 +6,7 @@
header {* Even and Odd for int and nat *}

theory Parity
-imports Divides
+imports Nat_Transfer
begin

subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
@@ -139,48 +139,6 @@
then show "\<exists>l. k = l + 1" ..
qed

-context semiring_div_parity
-begin
-
-subclass semiring_parity
-proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
-  fix a b c
-  show "(c * a + b) mod a = 0 \<longleftrightarrow> b mod a = 0"
-    by simp
-next
-  fix a b c
-  assume "(b + c) mod a = 0"
-  with mod_add_eq [of b c a]
-  have "(b mod a + c mod a) mod a = 0"
-    by simp
-  moreover assume "b mod a = 0"
-  ultimately show "c mod a = 0"
-    by simp
-next
-  show "1 mod 2 = 1"
-    by (fact one_mod_two_eq_one)
-next
-  fix a b
-  assume "a mod 2 = 1"
-  moreover assume "b mod 2 = 1"
-  ultimately show "(a + b) mod 2 = 0"
-    using mod_add_eq [of a b 2] by simp
-next
-  fix a b
-  assume "(a * b) mod 2 = 0"
-  then have "(a mod 2) * (b mod 2) = 0"
-    by (cases "a mod 2 = 0") (simp_all add: mod_mult_eq [of a b 2])
-  then show "a mod 2 = 0 \<or> b mod 2 = 0"
-    by (rule divisors_zero)
-next
-  fix a
-  assume "a mod 2 = 1"
-  then have "a = a div 2 * 2 + 1" using mod_div_equality [of a 2] by simp
-  then show "\<exists>b. a = b + 1" ..
-qed
-
-end
-

subsection {* Dedicated @{text even}/@{text odd} predicate *}

@@ -274,47 +232,6 @@
end

-subsubsection {* Parity and division *}
-
-context semiring_div_parity
-begin
-
-lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
-  "1 div 2 = 0"
-proof (cases "2 = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
-  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
-  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
-  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
-  with False show ?thesis by auto
-qed
-
-lemma even_iff_mod_2_eq_zero:
-  "even a \<longleftrightarrow> a mod 2 = 0"
-  by (fact dvd_eq_mod_eq_0)
-
-lemma even_succ_div_two [simp]:
-  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
-  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
-
-lemma odd_succ_div_two [simp]:
-  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
-
-lemma even_two_times_div_two:
-  "even a \<Longrightarrow> 2 * (a div 2) = a"
-  by (fact dvd_mult_div_cancel)
-
-lemma odd_two_times_div_two_succ:
-  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
-  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
-
-end
-
-
subsubsection {* Particularities for @{typ nat} and @{typ int} *}

lemma even_Suc [simp]:
@@ -342,44 +259,6 @@
"0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
by simp

-lemma even_Suc_div_two [simp]:
-  "even n \<Longrightarrow> Suc n div 2 = n div 2"
-  using even_succ_div_two [of n] by simp
-
-lemma odd_Suc_div_two [simp]:
-  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
-  using odd_succ_div_two [of n] by simp
-
-lemma odd_two_times_div_two_Suc:
-  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
-  using odd_two_times_div_two_succ [of n] by simp
-
-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"
-proof (induct n rule: less_induct)
-  case (less n)
-  show "P n"
-  proof (cases "n = 0")
-    case True with zero show ?thesis by simp
-  next
-    case False
-    with less have hyp: "P (n div 2)" by simp
-    show ?thesis
-    proof (cases "even n")
-      case True
-      with hyp even [of "n div 2"] show ?thesis