# HG changeset patch # User haftmann # Date 1383216260 -3600 # Node ID 63b441f4964586de1442ab07eb59e6af78321aa8 # Parent e3df2a4e02fc4dc6894fab06ce22e9daebd4a4fd moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas; tuned presburger diff -r e3df2a4e02fc -r 63b441f49645 NEWS --- a/NEWS Thu Oct 31 11:44:20 2013 +0100 +++ b/NEWS Thu Oct 31 11:44:20 2013 +0100 @@ -4,6 +4,11 @@ New in this Isabelle version ---------------------------- +*** HOL *** + +* Fact name generalization and consolidation: + neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1 + New in Isabelle2013-1 (November 2013) diff -r e3df2a4e02fc -r 63b441f49645 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Divides.thy Thu Oct 31 11:44:20 2013 +0100 @@ -2620,11 +2620,6 @@ "Suc 0 mod numeral v' = nat (1 mod numeral v')" by (subst nat_mod_distrib) simp_all -lemma mod_2_not_eq_zero_eq_one_int: - fixes k :: int - shows "k mod 2 \ 0 \ k mod 2 = 1" - by auto - instance int :: semiring_numeral_div by intro_classes (auto intro: zmod_le_nonneg_dividend simp add: zmult_div_cancel diff -r e3df2a4e02fc -r 63b441f49645 src/HOL/Library/Code_Target_Int.thy --- a/src/HOL/Library/Code_Target_Int.thy Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Library/Code_Target_Int.thy Thu Oct 31 11:44:20 2013 +0100 @@ -99,7 +99,7 @@ proof - from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp show ?thesis - by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int + by (simp add: Let_def divmod_int_mod_div not_mod_2_eq_0_eq_1 of_int_add [symmetric]) (simp add: * mult_commute) qed diff -r e3df2a4e02fc -r 63b441f49645 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Parity.thy Thu Oct 31 11:44:20 2013 +0100 @@ -11,11 +11,14 @@ class even_odd = fixes even :: "'a \ bool" +begin -abbreviation - odd :: "'a\even_odd \ bool" where +abbreviation odd :: "'a \ bool" +where "odd x \ \ even x" +end + instantiation nat and int :: even_odd begin @@ -52,7 +55,7 @@ unfolding even_def by simp (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *) -declare even_def[of "neg_numeral v", simp] for v +declare even_def [of "neg_numeral v", simp] for v lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)" unfolding even_nat_def by simp @@ -62,13 +65,6 @@ subsection {* Even and odd are mutually exclusive *} -lemma int_pos_lt_two_imp_zero_or_one: - "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1" - by presburger - -lemma neq_one_mod_two [simp, presburger]: - "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger - subsection {* Behavior under integer arithmetic operations *} declare dvd_def[algebra] @@ -158,10 +154,6 @@ subsection {* Equivalent definitions *} -lemma nat_lt_two_imp_zero_or_one: - "(x::nat) < Suc (Suc 0) ==> x = 0 | x = Suc 0" -by presburger - lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0" by presburger @@ -244,7 +236,7 @@ apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square) done -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = +lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = (even n | (odd n & 0 <= x))" apply auto apply (subst zero_le_odd_power [symmetric]) @@ -277,9 +269,6 @@ apply (simp add: zero_le_even_power) done -lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" - by (induct n) auto - lemma power_minus_even [simp]: "even n ==> (- x)^n = (x^n::'a::{comm_ring_1})" apply (subst power_minus) @@ -336,13 +325,6 @@ lemma odd_add [simp]: "odd(m + n::nat) = (odd m \ odd n)" by presburger -lemma div_Suc: "Suc a div c = a div c + Suc 0 div c + - (a mod c + Suc 0 mod c) div c" - apply (subgoal_tac "Suc a = a + Suc 0") - apply (erule ssubst) - apply (rule div_add1_eq, simp) - done - lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)" @@ -359,31 +341,29 @@ text {* Simplify, when the exponent is a numeral *} lemmas zero_le_power_eq_numeral [simp] = - zero_le_power_eq [of _ "numeral w"] for w + zero_le_power_eq [of _ "numeral w"] for w lemmas zero_less_power_eq_numeral [simp] = - zero_less_power_eq [of _ "numeral w"] for w + zero_less_power_eq [of _ "numeral w"] for w lemmas power_le_zero_eq_numeral [simp] = - power_le_zero_eq [of _ "numeral w"] for w + power_le_zero_eq [of _ "numeral w"] for w lemmas power_less_zero_eq_numeral [simp] = - power_less_zero_eq [of _ "numeral w"] for w + power_less_zero_eq [of _ "numeral w"] for w lemmas zero_less_power_nat_eq_numeral [simp] = - zero_less_power_nat_eq [of _ "numeral w"] for w + nat_zero_less_power_iff [of _ "numeral w"] for w -lemmas power_eq_0_iff_numeral [simp] = power_eq_0_iff [of _ "numeral w"] for w +lemmas power_eq_0_iff_numeral [simp] = + power_eq_0_iff [of _ "numeral w"] for w -lemmas power_even_abs_numeral [simp] = power_even_abs [of "numeral w" _] for w +lemmas power_even_abs_numeral [simp] = + power_even_abs [of "numeral w" _] for w subsection {* An Equivalence for @{term [source] "0 \ a^n"} *} -lemma even_power_le_0_imp_0: - "a ^ (2*k) \ (0::'a::{linordered_idom}) ==> a=0" - by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) - lemma zero_le_power_iff[presburger]: "(0 \ a^n) = (0 \ (a::'a::{linordered_idom}) | even n)" proof cases @@ -395,9 +375,10 @@ assume odd: "odd n" then obtain k where "n = Suc(2*k)" by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) - thus ?thesis - by (auto simp add: zero_le_mult_iff zero_le_even_power - dest!: even_power_le_0_imp_0) + moreover have "a ^ (2 * k) \ 0 \ a = 0" + by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) + ultimately show ?thesis + by (auto simp add: zero_le_mult_iff zero_le_even_power) qed @@ -409,7 +390,6 @@ lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \ even x" by presburger -lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \ even x" by presburger lemma even_nat_plus_one_div_two: "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger @@ -417,3 +397,4 @@ (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger end + diff -r e3df2a4e02fc -r 63b441f49645 src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Presburger.thy Thu Oct 31 11:44:20 2013 +0100 @@ -360,11 +360,15 @@ apply simp done -lemma zdvd_mono: assumes not0: "(k::int) \ 0" -shows "((m::int) dvd t) \ (k*m dvd k*t)" - using not0 by (simp add: dvd_def) +lemma zdvd_mono: + fixes k m t :: int + assumes "k \ 0" + shows "m dvd t \ k * m dvd k * t" + using assms by simp -lemma uminus_dvd_conv: "(d dvd (t::int)) \ (-d dvd t)" "(d dvd (t::int)) \ (d dvd -t)" +lemma uminus_dvd_conv: + fixes d t :: int + shows "d dvd t \ - d dvd t" and "d dvd t \ d dvd - t" by simp_all text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} @@ -406,24 +410,23 @@ end *} "Cooper's algorithm for Presburger arithmetic" -declare dvd_eq_mod_eq_0[symmetric, presburger] -declare mod_1[presburger] -declare mod_0[presburger] -declare mod_by_1[presburger] -declare mod_self[presburger] -declare mod_by_0[presburger] -declare mod_div_trivial[presburger] -declare div_mod_equality2[presburger] -declare div_mod_equality[presburger] -declare mod_div_equality2[presburger] -declare mod_div_equality[presburger] -declare mod_mult_self1[presburger] -declare mod_mult_self2[presburger] -declare div_mod_equality[presburger] -declare div_mod_equality2[presburger] +declare dvd_eq_mod_eq_0 [symmetric, presburger] +declare mod_1 [presburger] +declare mod_0 [presburger] +declare mod_by_1 [presburger] +declare mod_self [presburger] +declare div_by_0 [presburger] +declare mod_by_0 [presburger] +declare mod_div_trivial [presburger] +declare div_mod_equality2 [presburger] +declare div_mod_equality [presburger] +declare mod_div_equality2 [presburger] +declare mod_div_equality [presburger] +declare mod_mult_self1 [presburger] +declare mod_mult_self2 [presburger] declare mod2_Suc_Suc[presburger] -lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a" -by simp_all +declare not_mod_2_eq_0_eq_1 [presburger] +declare nat_zero_less_power_iff [presburger] lemma [presburger, algebra]: "m mod 2 = (1::nat) \ \ 2 dvd m " by presburger lemma [presburger, algebra]: "m mod 2 = Suc 0 \ \ 2 dvd m " by presburger @@ -432,3 +435,4 @@ lemma [presburger, algebra]: "m mod 2 = (1::int) \ \ 2 dvd m " by presburger end + diff -r e3df2a4e02fc -r 63b441f49645 src/HOL/Tools/Qelim/qelim.ML --- a/src/HOL/Tools/Qelim/qelim.ML Thu Oct 31 11:44:20 2013 +0100 +++ b/src/HOL/Tools/Qelim/qelim.ML Thu Oct 31 11:44:20 2013 +0100 @@ -37,7 +37,7 @@ val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p') |> Drule.arg_cong_rule e val th' = simpex_conv (Thm.rhs_of th) - val (l,r) = Thm.dest_equals (cprop_of th') + val (_, r) = Thm.dest_equals (cprop_of th') in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th)) else Thm.transitive (Thm.transitive th th') (conv env r) end | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p