more foundational definition for predicate even
authorhaftmann
Thu Oct 09 22:43:48 2014 +0200 (2014-10-09)
changeset 5864594bef115c08f
parent 58644 8171ef293634
child 58646 cd63a4b12a33
more foundational definition for predicate even
NEWS
src/HOL/Decision_Procs/commutative_ring_tac.ML
src/HOL/Number_Theory/Gauss.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Parity.thy
src/HOL/Word/Bit_Representation.thy
src/Tools/Code/code_runtime.ML
     1.1 --- a/NEWS	Fri Oct 10 18:23:59 2014 +0200
     1.2 +++ b/NEWS	Thu Oct 09 22:43:48 2014 +0200
     1.3 @@ -42,6 +42,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* More foundational definition for predicate "even":
     1.8 +  even_def ~> even_iff_mod_2_eq_zero
     1.9 +Minor INCOMPATIBILITY.
    1.10 +
    1.11  * Lemma name consolidation: divide_Numeral1 ~> divide_numeral_1
    1.12  Minor INCOMPATIBILITY.
    1.13  
     2.1 --- a/src/HOL/Decision_Procs/commutative_ring_tac.ML	Fri Oct 10 18:23:59 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/commutative_ring_tac.ML	Thu Oct 09 22:43:48 2014 +0200
     2.3 @@ -90,7 +90,7 @@
     2.4  (* Attention: You have to make sure that no t^0 is in the goal!! *)
     2.5  (* Use simply rewriting t^0 = 1 *)
     2.6  val cring_simps =
     2.7 -  @{thms mkPX_def mkPinj_def sub_def power_add even_def pow_if power_add [symmetric]};
     2.8 +  @{thms mkPX_def mkPinj_def sub_def power_add even_iff_mod_2_eq_zero pow_if power_add [symmetric]};
     2.9  
    2.10  fun tac ctxt = SUBGOAL (fn (g, i) =>
    2.11    let
     3.1 --- a/src/HOL/Number_Theory/Gauss.thy	Fri Oct 10 18:23:59 2014 +0200
     3.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Thu Oct 09 22:43:48 2014 +0200
     3.3 @@ -57,7 +57,7 @@
     3.4  
     3.5  lemma p_odd_int: obtains z::int where "int p = 2*z+1" "0<z"
     3.6    using odd_p p_ge_2
     3.7 -  by (auto simp add: even_def) (metis p_eq2)
     3.8 +  by (auto simp add: even_iff_mod_2_eq_zero) (metis p_eq2)
     3.9  
    3.10  
    3.11  subsection {* Basic Properties of the Gauss Sets *}
     4.1 --- a/src/HOL/Number_Theory/Primes.thy	Fri Oct 10 18:23:59 2014 +0200
     4.2 +++ b/src/HOL/Number_Theory/Primes.thy	Thu Oct 09 22:43:48 2014 +0200
     4.3 @@ -43,8 +43,8 @@
     4.4  subsection {* Primes *}
     4.5  
     4.6  lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
     4.7 -  apply (auto simp add: prime_nat_def even_def dvd_eq_mod_eq_0)
     4.8 -  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)
     4.9 +  apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
    4.10 +  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)
    4.11    done
    4.12  
    4.13  (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
     5.1 --- a/src/HOL/Parity.thy	Fri Oct 10 18:23:59 2014 +0200
     5.2 +++ b/src/HOL/Parity.thy	Thu Oct 09 22:43:48 2014 +0200
     5.3 @@ -14,15 +14,17 @@
     5.4  
     5.5  definition even :: "'a \<Rightarrow> bool"
     5.6  where
     5.7 -  even_def [presburger]: "even a \<longleftrightarrow> a mod 2 = 0"
     5.8 +  [algebra]: "even a \<longleftrightarrow> 2 dvd a"
     5.9  
    5.10 -lemma even_iff_2_dvd [algebra]:
    5.11 -  "even a \<longleftrightarrow> 2 dvd a"
    5.12 +lemmas even_iff_2_dvd = even_def
    5.13 +
    5.14 +lemma even_iff_mod_2_eq_zero [presburger]:
    5.15 +  "even a \<longleftrightarrow> a mod 2 = 0"
    5.16    by (simp add: even_def dvd_eq_mod_eq_0)
    5.17  
    5.18  lemma even_zero [simp]:
    5.19    "even 0"
    5.20 -  by (simp add: even_def)
    5.21 +  by (simp add: even_iff_mod_2_eq_zero)
    5.22  
    5.23  lemma even_times_anything:
    5.24    "even a \<Longrightarrow> even (a * b)"
    5.25 @@ -38,7 +40,7 @@
    5.26  
    5.27  lemma odd_times_odd:
    5.28    "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)" 
    5.29 -  by (auto simp add: even_def mod_mult_left_eq)
    5.30 +  by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq)
    5.31  
    5.32  lemma even_product [simp, presburger]:
    5.33    "even (a * b) \<longleftrightarrow> even a \<or> even b"
    5.34 @@ -53,7 +55,7 @@
    5.35  
    5.36  lemma even_nat_def [presburger]:
    5.37    "even x \<longleftrightarrow> even (int x)"
    5.38 -  by (auto simp add: even_def int_eq_iff int_mult nat_mult_distrib)
    5.39 +  by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib)
    5.40    
    5.41  lemma transfer_int_nat_relations:
    5.42    "even (int x) \<longleftrightarrow> even x"
    5.43 @@ -72,13 +74,13 @@
    5.44    by presburger
    5.45  
    5.46  lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
    5.47 -  unfolding even_def by simp
    5.48 +  unfolding even_iff_mod_2_eq_zero by simp
    5.49  
    5.50  lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
    5.51 -  unfolding even_def by simp
    5.52 +  unfolding even_iff_mod_2_eq_zero by simp
    5.53  
    5.54  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
    5.55 -declare even_def [of "- numeral v", simp] for v
    5.56 +declare even_iff_mod_2_eq_zero [of "- numeral v", simp] for v
    5.57  
    5.58  lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
    5.59    unfolding even_nat_def by simp
     6.1 --- a/src/HOL/Word/Bit_Representation.thy	Fri Oct 10 18:23:59 2014 +0200
     6.2 +++ b/src/HOL/Word/Bit_Representation.thy	Thu Oct 09 22:43:48 2014 +0200
     6.3 @@ -34,7 +34,7 @@
     6.4  
     6.5  lemma bin_last_odd:
     6.6    "bin_last = odd"
     6.7 -  by (rule ext) (simp add: bin_last_def even_def)
     6.8 +  by (rule ext) (simp add: bin_last_def even_iff_mod_2_eq_zero)
     6.9  
    6.10  definition bin_rest :: "int \<Rightarrow> int"
    6.11  where
    6.12 @@ -317,7 +317,7 @@
    6.13           zmod_zdiv_equality [THEN diff_eq_eq [THEN iffD2 [THEN sym]]])
    6.14    apply (rule trans [symmetric, OF _ emep1])
    6.15       apply auto
    6.16 -  apply (auto simp: even_def)
    6.17 +  apply (auto simp: even_iff_mod_2_eq_zero)
    6.18    done
    6.19  
    6.20  subsection "Simplifications for (s)bintrunc"
     7.1 --- a/src/Tools/Code/code_runtime.ML	Fri Oct 10 18:23:59 2014 +0200
     7.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Oct 09 22:43:48 2014 +0200
     7.3 @@ -323,6 +323,10 @@
     7.4  
     7.5  fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
     7.6  
     7.7 +fun static_value_strict' cookie = Exn.release ooo static_value_exn' cookie;
     7.8 +
     7.9 +fun static_value' cookie = partiality_as_none ooo static_value_exn' cookie;
    7.10 +
    7.11  
    7.12  (** code antiquotation **)
    7.13