--- 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 =
- @{thms mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]};
+ @{thms mkPX_def mkPinj_def sub_def power_add even_iff_mod_2_eq_zero pow_if power_add [symmetric]};
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"
by (simp add: even_def dvd_eq_mod_eq_0)
lemma even_zero [simp]:
"even 0"
- by (simp add: even_def)
+ by (simp add: even_iff_mod_2_eq_zero)
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 @@
fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
+fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
+
+fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
+
(** code antiquotation **)