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