# HG changeset patch
# User haftmann
# Date 1413783958 -7200
# Node ID 7216a10d69ba807cfcb972cbf230b093072e581a
# Parent  efdc6c533bd3c67e19fa814a283dd68e18bcfb07
augmented and tuned facts on even/odd and division

diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Decision_Procs/Commutative_Ring.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -140,19 +140,17 @@
     mkPX (sqr A) (x + x) (sqr B) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
 
 text {* Fast Exponentation *}
+
 fun pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
 where
-  "pow 0 P = Pc 1"
-| "pow n P =
-    (if even n then pow (n div 2) (sqr P)
-     else P \<otimes> pow (n div 2) (sqr P))"
-
-lemma pow_if:
-  "pow n P =
+  pow_if [simp del]: "pow n P =
    (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P)
     else P \<otimes> pow (n div 2) (sqr P))"
-  by (cases n) simp_all
 
+lemma pow_simps [simp]:    
+  "pow 0 P = Pc 1"
+  "pow (Suc n) P = (if odd n then pow (Suc n div 2) (sqr P) else P \<otimes> pow (Suc n div 2) (sqr P))"
+  by (simp_all add: pow_if)
 
 text {* Normalization of polynomial expressions *}
 
@@ -244,7 +242,8 @@
     (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add)
 
 text {* Power *}
-lemma even_pow:"even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
+lemma even_pow:
+  "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
   by (induct n) simp_all
 
 lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
@@ -260,12 +259,12 @@
     proof cases
       assume "even l"
       then have "Suc l div 2 = l div 2"
-        by (simp add: eval_nat_numeral even_nat_plus_one_div_two)
+        by simp
       moreover
       from Suc have "l < k" by simp
       with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp
       moreover
-      note Suc `even l` even_nat_plus_one_div_two
+      note Suc `even l`
       ultimately show ?thesis by (auto simp add: mul_ci even_pow)
     next
       assume "odd l"
@@ -278,8 +277,8 @@
         next
           case (Suc w)
           with `odd l` have "even w" by simp
-          have two_times: "2 * (w div 2) = w"
-            by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
+          then have two_times: "2 * (w div 2) = w"
+            by (simp add: even_two_times_div_two)
           have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
             by simp
           then have "Ipol ls P * Ipol ls P = (Ipol ls P)\<^sup>2"
@@ -288,7 +287,9 @@
             by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
                      simp del: power_Suc)
         qed
-      } with 1 Suc `odd l` show ?thesis by simp
+      }
+      with 1 `odd l` Suc show ?thesis
+        by (simp del: odd_Suc_div_two)
     qed
   qed
 qed
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
--- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -551,7 +551,7 @@
     then have K2: "k div 2 < k" by (cases k) auto
     from less have "isnorm (sqr P)" by (simp add: sqr_cn)
     with less False K2 show ?thesis
-      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
+      by (cases k) (auto simp del: odd_Suc_div_two simp add: mul_cn)
   qed
 qed
 
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -789,20 +789,18 @@
       by (simp only: power_add power_one_right) simp
     also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
       by (simp only: th)
-    finally have ?case
-    using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp
+    finally have ?case unfolding numeral_2_eq_2 [symmetric]
+    using odd_two_times_div_two_Suc [OF odd] by simp
   }
   moreover
   {
     assume even: "even (Suc n)"
-    have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2"
-      by arith
     from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"
       by (simp add: Let_def)
-    also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
-      using "2.hyps" by (simp only: power_add) simp
-    finally have ?case using even_nat_div_two_times_two[OF even]
-      by (simp only: th)
+    also have "\<dots> = (Ipoly bs p) ^ (2 * (Suc n div 2))"
+      using "2.hyps" by (simp only: mult_2 power_add) simp
+    finally have ?case using even_two_times_div_two [OF even]
+      by simp
   }
   ultimately show ?case by blast
 qed
@@ -823,8 +821,8 @@
     by simp
   from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n"
     by simp
-  from dn on show ?case
-    by (simp add: Let_def)
+  from dn on show ?case by (simp, unfold Let_def) auto
+    
 qed
 
 lemma polypow_norm:
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Divides.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -507,6 +507,7 @@
 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"
+  assumes zero_not_eq_two: "0 \<noteq> 2"
 begin
 
 lemma parity_cases [case_names even odd]:
@@ -573,6 +574,9 @@
 next
   show "1 mod 2 = 1"
     by (rule mod_less) simp_all
+next
+  show "0 \<noteq> 2"
+    by simp
 qed
 
 lemma divmod_digit_1:
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Enum.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -705,10 +705,6 @@
   "2 = a\<^sub>1"
   by (simp add: numeral.simps plus_finite_2_def)
   
-instance finite_2 :: semiring_div_parity
-by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits)
-
-
 hide_const (open) a\<^sub>1 a\<^sub>2
 
 datatype (plugins only: code "quickcheck" extraction) finite_3 =
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -122,9 +122,7 @@
 by (induct x) simp_all
 
 lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
-unfolding sum_decode_def sum_encode_def numeral_2_eq_2
-by (simp add: even_nat_div_two_times_two odd_nat_div_two_times_two_plus_one
-         del: mult_Suc)
+  by (simp add: even_two_times_div_two odd_two_times_div_two_Suc sum_decode_def sum_encode_def)
 
 lemma inj_sum_encode: "inj_on sum_encode A"
 by (rule inj_on_inverseI, rule sum_encode_inverse)
@@ -270,18 +268,15 @@
   "Suc -` insert (Suc n) A = insert n (Suc -` A)"
 by auto
 
-lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
-by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
-
 lemma div2_even_ext_nat:
-  "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
+  "x div 2 = y div 2 \<Longrightarrow> even x \<longleftrightarrow> even y \<Longrightarrow> (x::nat) = y"
 apply (rule mod_div_equality [of x 2, THEN subst])
 apply (rule mod_div_equality [of y 2, THEN subst])
-apply (case_tac "even x")
-apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
-apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
+apply (cases "even x")
+apply (simp_all add: even_iff_mod_2_eq_zero)
 done
 
+
 subsubsection {* From sets to naturals *}
 
 definition
@@ -303,7 +298,7 @@
 apply (cases "finite A")
 apply (erule finite_induct, simp)
 apply (case_tac x)
-apply (simp add: even_nat_Suc_div_2 even_set_encode_iff vimage_Suc_insert_0)
+apply (simp add: even_set_encode_iff vimage_Suc_insert_0)
 apply (simp add: finite_vimageI add.commute vimage_Suc_insert_Suc)
 apply (simp add: set_encode_def finite_vimage_Suc_iff)
 done
@@ -333,7 +328,7 @@
 lemma set_decode_plus_power_2:
   "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
  apply (induct n arbitrary: z, simp_all)
-  apply (rule set_eqI, induct_tac x, simp, simp add: even_nat_Suc_div_2)
+  apply (rule set_eqI, induct_tac x, simp, simp)
  apply (rule set_eqI, induct_tac x, simp, simp add: add.commute)
 done
 
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Library/Stream.thy
--- a/src/HOL/Library/Stream.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Library/Stream.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -491,9 +491,8 @@
 
 lemma sinterleave_snth[simp]:
   "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
-   "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
-  by (induct n arbitrary: s1 s2)
-    (auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2])
+  "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
+  by (induct n arbitrary: s1 s2) simp_all
 
 lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2"
 proof (intro equalityI subsetI)
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Parity.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -279,13 +279,45 @@
 
 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 [presburger]:
   "even a \<longleftrightarrow> a mod 2 = 0"
   by (simp add: even_def 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"
+  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
+
+lemma even_two_times_div_two:
+  "even a \<Longrightarrow> 2 * (a div 2) = a"
+  by (rule dvd_mult_div_cancel) (simp add: even_def)
+
+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
 
 
@@ -312,8 +344,37 @@
   "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
   by (simp add: even_int_iff [symmetric])
 
+lemma even_num_iff:
+  "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
+  by simp
 
-subsubsection {* Parity and powers *}
+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
+  
+text {* Nice facts about division by @{term 4} *}  
+
+lemma even_even_mod_4_iff:
+  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
+  by presburger
+
+lemma odd_mod_4_div_2:
+  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
+  by presburger
+
+lemma even_mod_4_div_2:
+  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
+  by presburger
+  
+text {* Parity and powers *}
 
 context comm_ring_1
 begin
@@ -370,7 +431,7 @@
   "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
   by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
 
-lemma zero_le_power_iff [presburger]:
+lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. zero_le_power_eq\<close>
   "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
 proof (cases "even n")
   case True
@@ -385,7 +446,7 @@
     by (auto simp add: zero_le_mult_iff zero_le_even_power)
 qed
 
-lemma zero_le_power_eq [presburger]: -- \<open>FIXME weaker version of @{text zero_le_power_iff}\<close>
+lemma zero_le_power_eq [presburger]:
   "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   using zero_le_power_iff [of a n] by auto
 
@@ -395,7 +456,7 @@
   have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
     unfolding power_eq_0_iff' [of a n, symmetric] by blast
   show ?thesis
-  unfolding less_le zero_le_power_iff by auto
+  unfolding less_le zero_le_power_eq by auto
 qed
 
 lemma power_less_zero_eq [presburger]:
@@ -511,64 +572,5 @@
   "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
   by presburger
 
-
-subsubsection {* Miscellaneous *}
-
-lemma even_nat_plus_one_div_two:
-  "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
-  by presburger
-
-lemma odd_nat_plus_one_div_two:
-  "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
-  by presburger
-
-lemma even_nat_mod_two_eq_zero:
-  "even (x::nat) ==> x mod Suc (Suc 0) = 0"
-  by presburger
-
-lemma odd_nat_mod_two_eq_one:
-  "odd (x::nat) ==> x mod Suc (Suc 0) = Suc 0"
-  by presburger
-
-lemma even_nat_equiv_def:
-  "even (x::nat) = (x mod Suc (Suc 0) = 0)"
-  by presburger
-
-lemma odd_nat_equiv_def:
-  "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
-  by presburger
-
-lemma even_nat_div_two_times_two:
-  "even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x"
-  by presburger
-
-lemma odd_nat_div_two_times_two_plus_one:
-  "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x"
-  by presburger
-
-lemma lemma_even_div2 [simp]:
-  "even (n::nat) ==> (n + 1) div 2 = n div 2"
-  by presburger
-
-lemma lemma_odd_div2 [simp]:
-  "odd n ==> (n + 1) div 2 = Suc (n div 2)"
-  by presburger
-
-lemma even_num_iff:
-  "0 < n ==> even n = (odd (n - 1 :: nat))"
-  by presburger
-
-lemma even_even_mod_4_iff:
-  "even (n::nat) = even (n mod 4)"
-  by presburger
-
-lemma lemma_odd_mod_4_div_2:
-  "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
-  by presburger
-
-lemma lemma_even_mod_4_div_2:
-  "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
-  by presburger
-
 end
 
diff -r efdc6c533bd3 -r 7216a10d69ba src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Oct 19 18:05:26 2014 +0200
+++ b/src/HOL/Transcendental.thy	Mon Oct 20 07:45:58 2014 +0200
@@ -200,14 +200,10 @@
     have "?SUM (2 * (m div 2)) = ?SUM m"
     proof (cases "even m")
       case True
-      show ?thesis
-        unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
+      then show ?thesis by (auto simp add: even_two_times_div_two)
     next
       case False
-      hence "even (Suc m)" by auto
-      from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]]
-        odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
-      have eq: "Suc (2 * (m div 2)) = m" by auto
+      then have eq: "Suc (2 * (m div 2)) = m" by (simp add: odd_two_times_div_two_Suc)
       hence "even (2 * (m div 2))" using `odd m` by auto
       have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
       also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
@@ -321,9 +317,7 @@
       have "norm (?Sa n - l) < r"
       proof (cases "even n")
         case True
-        from even_nat_div_two_times_two[OF this]
-        have n_eq: "2 * (n div 2) = n"
-          unfolding numeral_2_eq_2[symmetric] by auto
+        then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two)
         with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
           by auto
         from f[OF this] show ?thesis
@@ -331,9 +325,8 @@
       next
         case False
         hence "even (n - 1)" by simp
-        from even_nat_div_two_times_two[OF this]
-        have n_eq: "2 * ((n - 1) div 2) = n - 1"
-          unfolding numeral_2_eq_2[symmetric] by auto
+        then have n_eq: "2 * ((n - 1) div 2) = n - 1"
+          by (simp add: even_two_times_div_two)
         hence range_eq: "n - 1 + 1 = n"
           using odd_pos[OF False] by auto