# HG changeset patch
# User haftmann
# Date 1412887428 -7200
# Node ID 94bef115c08f2764bdcebb51d399a499b1fbdd49
# Parent  8171ef2936347963bb5fdf1fa835997ab94aa1e1
more foundational definition for predicate even

diff -r 8171ef293634 -r 94bef115c08f NEWS
--- 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.
 
diff -r 8171ef293634 -r 94bef115c08f src/HOL/Decision_Procs/commutative_ring_tac.ML
--- 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
diff -r 8171ef293634 -r 94bef115c08f src/HOL/Number_Theory/Gauss.thy
--- 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 *}
diff -r 8171ef293634 -r 94bef115c08f src/HOL/Number_Theory/Primes.thy
--- 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? *)
diff -r 8171ef293634 -r 94bef115c08f src/HOL/Parity.thy
--- 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
diff -r 8171ef293634 -r 94bef115c08f src/HOL/Word/Bit_Representation.thy
--- 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"
diff -r 8171ef293634 -r 94bef115c08f src/Tools/Code/code_runtime.ML
--- 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 **)