--- a/NEWS Fri Oct 24 11:30:39 2014 +0200
+++ b/NEWS Fri Oct 24 20:49:23 2014 +0200
@@ -49,6 +49,8 @@
*** HOL ***
+* Add NO_MATCH-simproc, allows to check for syntactic non-equality
+
* Generalized and consolidated some theorems concerning divsibility:
dvd_reduce ~> dvd_add_triv_right_iff
dvd_plus_eq_right ~> dvd_add_right_iff
@@ -63,6 +65,12 @@
* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
Minor INCOMPATIBILITY.
+* field_simps: Use NO_MATCH-simproc for distribution rules, to avoid
+ non-termination in case of distributing a division. With this change
+ field_simps is in some cases slightly less powerful, if it fails try
+ to add algebra_simps, or use divide_simps.
+Minor INCOMPATIBILITY.
+
* Bootstrap of listsum as special case of abstract product over lists.
Fact rename:
listsum_def ~> listsum.eq_foldr
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Fri Oct 24 20:49:23 2014 +0200
@@ -375,7 +375,7 @@
lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q"
by (induct p q rule: polyadd.induct)
- (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left)
+ (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH)
lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)"
using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
--- a/src/HOL/Divides.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Divides.thy Fri Oct 24 20:49:23 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"
+ 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 (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
+ by (simp add: dvd_mult_div_cancel)
+ next
+ case False
+ with hyp odd [of "n div 2"] show ?thesis
+ by (simp add: odd_two_times_div_two_Suc)
+ qed
+ qed
+qed
+
subsection {* Division on @{typ int} *}
--- a/src/HOL/Fields.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Fields.thy Fri Oct 24 20:49:23 2014 +0200
@@ -23,11 +23,37 @@
fixes inverse :: "'a \<Rightarrow> 'a"
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
+setup {* Sign.add_const_constraint
+ (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
+
+context semiring
+begin
+
+lemma [field_simps]:
+ shows distrib_left_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b + c) = a * b + a * c"
+ and distrib_right_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a + b) * c = a * c + b * c"
+ by (rule distrib_left distrib_right)+
+
+end
+
+context ring
+begin
+
+lemma [field_simps]:
+ shows left_diff_distrib_NO_MATCH: "NO_MATCH c (x / y) \<Longrightarrow> (a - b) * c = a * c - b * c"
+ and right_diff_distrib_NO_MATCH: "NO_MATCH a (x / y) \<Longrightarrow> a * (b - c) = a * b - a * c"
+ by (rule left_diff_distrib right_diff_distrib)+
+
+end
+
+setup {* Sign.add_const_constraint
+ (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
+
text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
named_theorems divide_simps "rewrite rules to eliminate divisions"
-
class division_ring = ring_1 + inverse +
assumes left_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1"
assumes right_inverse [simp]: "a \<noteq> 0 \<Longrightarrow> a * inverse a = 1"
--- a/src/HOL/GCD.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/GCD.thy Fri Oct 24 20:49:23 2014 +0200
@@ -1049,7 +1049,7 @@
apply (subst mod_div_equality [of m n, symmetric])
(* applying simp here undoes the last substitution!
what is procedure cancel_div_mod? *)
- apply (simp only: field_simps of_nat_add of_nat_mult)
+ apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
done
qed
--- a/src/HOL/Groebner_Basis.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy Fri Oct 24 20:49:23 2014 +0200
@@ -5,7 +5,7 @@
header {* Groebner bases *}
theory Groebner_Basis
-imports Semiring_Normalization
+imports Semiring_Normalization Parity
keywords "try0" :: diag
begin
@@ -77,4 +77,22 @@
declare zmod_eq_dvd_iff[algebra]
declare nat_mod_eq_iff[algebra]
+context semiring_parity
+begin
+
+declare even_times_iff [algebra]
+declare even_power [algebra]
+
end
+
+context ring_parity
+begin
+
+declare even_minus [algebra]
+
+end
+
+declare even_Suc [algebra]
+declare even_diff_nat [algebra]
+
+end
--- a/src/HOL/HOL.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/HOL.thy Fri Oct 24 20:49:23 2014 +0200
@@ -1701,6 +1701,29 @@
ML_file "Tools/cnf.ML"
+section {* @{text NO_MATCH} simproc *}
+
+text {*
+ The simplification procedure can be used to avoid simplification of terms of a certain form
+*}
+
+definition NO_MATCH :: "'a \<Rightarrow> 'b \<Rightarrow> bool" where "NO_MATCH val pat \<equiv> True"
+lemma NO_MATCH_cong[cong]: "NO_MATCH val pat = NO_MATCH val pat" by (rule refl)
+
+simproc_setup NO_MATCH ("NO_MATCH val pat") = {* fn _ => fn ctxt => fn ct =>
+ let
+ val thy = Proof_Context.theory_of ctxt
+ val dest_binop = Term.dest_comb #> apfst (Term.dest_comb #> snd)
+ val m = Pattern.matches thy (dest_binop (Thm.term_of ct))
+ in if m then NONE else SOME @{thm NO_MATCH_def} end
+*}
+
+text {*
+ This setup ensures that a rewrite rule of the form @{term "NO_MATCH val pat \<Longrightarrow> t"}
+ is only applied, if the pattern @{term pat} does not match the value @{term val}.
+*}
+
+
subsection {* Code generator setup *}
subsubsection {* Generic code generator preprocessor setup *}
--- a/src/HOL/Main.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Main.thy Fri Oct 24 20:49:23 2014 +0200
@@ -2,7 +2,7 @@
theory Main
imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
- BNF_Greatest_Fixpoint Parity
+ BNF_Greatest_Fixpoint
begin
text {*
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Fri Oct 24 20:49:23 2014 +0200
@@ -5915,29 +5915,10 @@
proof -
fix y
assume as: "y\<in>cbox (x - ?d) (x + ?d)"
- {
- fix i :: 'a
- assume i: "i \<in> Basis"
- have "x \<bullet> i \<le> d + y \<bullet> i" "y \<bullet> i \<le> d + x \<bullet> i"
- using as[unfolded mem_box, THEN bspec[where x=i]] i
- by (auto simp: inner_simps)
- then have "1 \<ge> inverse d * (x \<bullet> i - y \<bullet> i)" "1 \<ge> inverse d * (y \<bullet> i - x \<bullet> i)"
- apply (rule_tac[!] mult_left_le_imp_le[OF _ assms])
- unfolding mult.assoc[symmetric]
- using assms
- by (auto simp add: field_simps)
- then have "inverse d * (x \<bullet> i * 2) \<le> 2 + inverse d * (y \<bullet> i * 2)"
- "inverse d * (y \<bullet> i * 2) \<le> 2 + inverse d * (x \<bullet> i * 2)"
- using `0<d` by (auto simp add: field_simps) }
then have "inverse (2 * d) *\<^sub>R (y - (x - ?d)) \<in> cbox 0 (\<Sum>Basis)"
- unfolding mem_box using assms
- by (auto simp add: field_simps inner_simps simp del: inverse_eq_divide)
- then show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
- apply -
- apply (rule_tac x="inverse (2 * d) *\<^sub>R (y - (x - ?d))" in bexI)
- using assms
- apply auto
- done
+ using assms by (simp add: mem_box field_simps inner_simps)
+ with `0 < d` show "\<exists>z\<in>cbox 0 (\<Sum>Basis). y = x - ?d + (2 * d) *\<^sub>R z"
+ by (intro bexI[of _ "inverse (2 * d) *\<^sub>R (y - (x - ?d))"]) auto
next
fix y z
assume as: "z\<in>cbox 0 (\<Sum>Basis)" "y = x - ?d + (2*d) *\<^sub>R z"
@@ -6076,7 +6057,7 @@
using `0 < t` `2 < t` and `y \<in> s` `w \<in> s`
by (auto simp add:field_simps)
also have "\<dots> = (f w + t * f y) / (1 + t)"
- using `t > 0` unfolding divide_inverse by (auto simp add: field_simps)
+ using `t > 0` by (auto simp add: divide_simps)
also have "\<dots> < e + f y"
using `t > 0` * `e > 0` by (auto simp add: field_simps)
finally have "f x - f y < e" by auto
--- a/src/HOL/Parity.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Parity.thy Fri Oct 24 20:49:23 2014 +0200
@@ -6,7 +6,7 @@
header {* Even and Odd for int and nat *}
theory Parity
-imports Presburger
+imports Nat_Transfer
begin
subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
@@ -36,7 +36,7 @@
lemma two_dvd_diff_iff:
fixes k l :: int
shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
- using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps)
+ using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
lemma two_dvd_abs_add_iff:
fixes k l :: 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"
- 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 (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
- by (simp add: dvd_mult_div_cancel)
- next
- case False
- with hyp odd [of "n div 2"] show ?thesis
- by (simp add: odd_two_times_div_two_Suc)
- qed
- qed
-qed
-
text {* Parity and powers *}
context comm_ring_1
@@ -546,77 +425,5 @@
even_int_iff
]
-context semiring_parity
-begin
-
-declare even_times_iff [presburger, algebra]
-
-declare even_power [presburger, algebra]
-
-lemma [presburger]:
- "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
- by auto
-
-end
-
-context ring_parity
-begin
-
-declare even_minus [presburger, algebra]
-
-end
-
-context linordered_idom
-begin
-
-declare zero_le_power_iff [presburger]
-
-declare zero_le_power_eq [presburger]
-
-declare zero_less_power_eq [presburger]
-
-declare power_less_zero_eq [presburger]
-
-declare power_le_zero_eq [presburger]
-
end
-declare even_Suc [presburger, algebra]
-
-lemma [presburger]:
- "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
- by presburger
-
-declare even_diff_nat [presburger, algebra]
-
-lemma [presburger]:
- fixes k :: int
- shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
- by presburger
-
-lemma [presburger]:
- fixes k :: int
- shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
- by presburger
-
-lemma [presburger]:
- "even n \<longleftrightarrow> even (int n)"
- using even_int_iff [of n] by simp
-
-
-subsubsection {* 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
-
-end
-
--- a/src/HOL/Presburger.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Presburger.thy Fri Oct 24 20:49:23 2014 +0200
@@ -434,6 +434,78 @@
lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
+context semiring_parity
+begin
+
+declare even_times_iff [presburger]
+
+declare even_power [presburger]
+
+lemma [presburger]:
+ "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
+ by auto
+
+end
+
+context ring_parity
+begin
+
+declare even_minus [presburger]
+
+end
+
+context linordered_idom
+begin
+
+declare zero_le_power_iff [presburger]
+
+declare zero_le_power_eq [presburger]
+
+declare zero_less_power_eq [presburger]
+
+declare power_less_zero_eq [presburger]
+
+declare power_le_zero_eq [presburger]
+
+end
+
+declare even_Suc [presburger]
+
+lemma [presburger]:
+ "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
+ by presburger
+
+declare even_diff_nat [presburger]
+
+lemma [presburger]:
+ fixes k :: int
+ shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
+ by presburger
+
+lemma [presburger]:
+ fixes k :: int
+ shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
+ by presburger
+
+lemma [presburger]:
+ "even n \<longleftrightarrow> even (int n)"
+ using even_int_iff [of n] by simp
+
+
+subsection {* 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
+
subsection {* Try0 *}
--- a/src/HOL/Rings.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Rings.thy Fri Oct 24 20:49:23 2014 +0200
@@ -14,8 +14,8 @@
begin
class semiring = ab_semigroup_add + semigroup_mult +
- assumes distrib_right[algebra_simps, field_simps]: "(a + b) * c = a * c + b * c"
- assumes distrib_left[algebra_simps, field_simps]: "a * (b + c) = a * b + a * c"
+ assumes distrib_right[algebra_simps]: "(a + b) * c = a * c + b * c"
+ assumes distrib_left[algebra_simps]: "a * (b + c) = a * b + a * c"
begin
text{*For the @{text combine_numerals} simproc*}
@@ -299,11 +299,11 @@
lemma minus_mult_commute: "- a * b = a * - b"
by simp
-lemma right_diff_distrib [algebra_simps, field_simps]:
+lemma right_diff_distrib [algebra_simps]:
"a * (b - c) = a * b - a * c"
using distrib_left [of a b "-c "] by simp
-lemma left_diff_distrib [algebra_simps, field_simps]:
+lemma left_diff_distrib [algebra_simps]:
"(a - b) * c = a * c - b * c"
using distrib_right [of a "- b" c] by simp
--- a/src/HOL/SMT.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/SMT.thy Fri Oct 24 20:49:23 2014 +0200
@@ -322,6 +322,7 @@
refl eq_commute conj_commute disj_commute simp_thms nnf_simps
ring_distribs field_simps times_divide_eq_right times_divide_eq_left
if_True if_False not_not
+ NO_MATCH_def
lemma [z3_rule]:
"(P \<and> Q) = (\<not> (\<not> P \<or> \<not> Q))"
--- a/src/HOL/Tools/SMT/z3_replay_util.ML Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_util.ML Fri Oct 24 20:49:23 2014 +0200
@@ -121,7 +121,7 @@
val basic_simpset =
simpset_of (put_simpset HOL_ss @{context}
addsimps @{thms field_simps times_divide_eq_right times_divide_eq_left arith_special
- arith_simps rel_simps array_rules z3div_def z3mod_def}
+ arith_simps rel_simps array_rules z3div_def z3mod_def NO_MATCH_def}
addsimprocs [@{simproc binary_int_div}, @{simproc binary_int_mod},
Simplifier.simproc_global @{theory} "fast_int_arith" [
"(m::int) < n", "(m::int) <= n", "(m::int) = n"] Lin_Arith.simproc,
--- a/src/HOL/ex/Lagrange.thy Fri Oct 24 11:30:39 2014 +0200
+++ b/src/HOL/ex/Lagrange.thy Fri Oct 24 20:49:23 2014 +0200
@@ -28,7 +28,7 @@
sq (x1*y2 + x2*y1 + x3*y4 - x4*y3) +
sq (x1*y3 - x2*y4 + x3*y1 + x4*y2) +
sq (x1*y4 + x2*y3 - x3*y2 + x4*y1)"
-by (simp only: sq_def field_simps)
+by (simp only: sq_def algebra_simps)
text {* A challenge by John Harrison. Takes about 12s on a 1.6GHz machine. *}
@@ -44,6 +44,6 @@
sq (p1*u2 + q1*t2 - r1*w2 + s1*v2 - t1*q2 + u1*p2 - v1*s2 + w1*r2) +
sq (p1*v2 + q1*w2 + r1*t2 - s1*u2 - t1*r2 + u1*s2 + v1*p2 - w1*q2) +
sq (p1*w2 - q1*v2 + r1*u2 + s1*t2 - t1*s2 - u1*r2 + v1*q2 + w1*p2)"
-by (simp only: sq_def field_simps)
+by (simp only: sq_def algebra_simps)
end