author haftmann Thu, 09 Oct 2014 22:43:48 +0200 changeset 58645 94bef115c08f parent 58644 8171ef293634 child 58646 cd63a4b12a33
more foundational definition for predicate even
 NEWS file | annotate | diff | comparison | revisions src/HOL/Decision_Procs/commutative_ring_tac.ML file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Gauss.thy file | annotate | diff | comparison | revisions src/HOL/Number_Theory/Primes.thy file | annotate | diff | comparison | revisions src/HOL/Parity.thy file | annotate | diff | comparison | revisions src/HOL/Word/Bit_Representation.thy file | annotate | diff | comparison | revisions src/Tools/Code/code_runtime.ML file | annotate | diff | comparison | revisions
```--- a/NEWS	Fri Oct 10 18:23:59 2014 +0200
+++ b/NEWS	Thu Oct 09 22:43:48 2014 +0200
@@ -42,6 +42,10 @@

*** HOL ***

+* More foundational definition for predicate "even":
+  even_def ~> even_iff_mod_2_eq_zero
+Minor INCOMPATIBILITY.
+
* Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
Minor INCOMPATIBILITY.
```
```--- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Fri Oct 10 18:23:59 2014 +0200
+++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Oct 09 22:43:48 2014 +0200
@@ -90,7 +90,7 @@
(* Attention: You have to make sure that no t^0 is in the goal!! *)
(* Use simply rewriting t^0 = 1 *)
val cring_simps =

fun tac ctxt = SUBGOAL (fn (g, i) =>
let```
```--- a/src/HOL/Number_Theory/Gauss.thy	Fri Oct 10 18:23:59 2014 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 09 22:43:48 2014 +0200
@@ -57,7 +57,7 @@

lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
using odd_p p_ge_2
-  by (auto simp add: even_def) (metis p_eq2)
+  by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)

subsection {* Basic Properties of the Gauss Sets *}```
```--- a/src/HOL/Number_Theory/Primes.thy	Fri Oct 10 18:23:59 2014 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Thu Oct 09 22:43:48 2014 +0200
@@ -43,8 +43,8 @@
subsection {* Primes *}

lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
-  apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
-  apply (metis dvd_eq_mod_eq_0 even_Suc even_def mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
+  apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
+  apply (metis dvd_eq_mod_eq_0 even_Suc even_iff_mod_2_eq_zero mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
done

(* FIXME Is there a better way to handle these, rather than making them elim rules? *)```
```--- a/src/HOL/Parity.thy	Fri Oct 10 18:23:59 2014 +0200
+++ b/src/HOL/Parity.thy	Thu Oct 09 22:43:48 2014 +0200
@@ -14,15 +14,17 @@

definition even :: "'a \<Rightarrow> bool"
where
-  even_def [presburger]: "even a \<longleftrightarrow> a mod 2 = 0"
+  [algebra]: "even a \<longleftrightarrow> 2 dvd a"

-lemma even_iff_2_dvd [algebra]:
-  "even a \<longleftrightarrow> 2 dvd a"
+lemmas even_iff_2_dvd = even_def
+
+lemma even_iff_mod_2_eq_zero [presburger]:
+  "even a \<longleftrightarrow> a mod 2 = 0"

lemma even_zero [simp]:
"even 0"

lemma even_times_anything:
"even a \<Longrightarrow> even (a * b)"
@@ -38,7 +40,7 @@

lemma odd_times_odd:
"odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)"
-  by (auto simp add: even_def mod_mult_left_eq)
+  by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq)

lemma even_product [simp, presburger]:
"even (a * b) \<longleftrightarrow> even a \<or> even b"
@@ -53,7 +55,7 @@

lemma even_nat_def [presburger]:
"even x \<longleftrightarrow> even (int x)"
-  by (auto simp add: even_def int_eq_iff int_mult nat_mult_distrib)
+  by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib)

lemma transfer_int_nat_relations:
"even (int x) \<longleftrightarrow> even x"
@@ -72,13 +74,13 @@
by presburger

lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
-  unfolding even_def by simp
+  unfolding even_iff_mod_2_eq_zero by simp

lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
-  unfolding even_def by simp
+  unfolding even_iff_mod_2_eq_zero by simp

(* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
-declare even_def [of "- numeral v", simp] for v
+declare even_iff_mod_2_eq_zero [of "- numeral v", simp] for v

lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
unfolding even_nat_def by simp```
```--- a/src/HOL/Word/Bit_Representation.thy	Fri Oct 10 18:23:59 2014 +0200
+++ b/src/HOL/Word/Bit_Representation.thy	Thu Oct 09 22:43:48 2014 +0200
@@ -34,7 +34,7 @@

lemma bin_last_odd:
"bin_last = odd"
-  by (rule ext) (simp add: bin_last_def even_def)
+  by (rule ext) (simp add: bin_last_def even_iff_mod_2_eq_zero)

definition bin_rest :: "int \<Rightarrow> int"
where
@@ -317,7 +317,7 @@
zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
apply (rule trans [symmetric, OF _ emep1])
apply auto
-  apply (auto simp: even_def)
+  apply (auto simp: even_iff_mod_2_eq_zero)
done

subsection "Simplifications for (s)bintrunc"```
```--- a/src/Tools/Code/code_runtime.ML	Fri Oct 10 18:23:59 2014 +0200
+++ b/src/Tools/Code/code_runtime.ML	Thu Oct 09 22:43:48 2014 +0200
@@ -323,6 +323,10 @@