moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
authorhaftmann
Thu Oct 31 11:44:20 2013 +0100 (2013-10-31)
changeset 5422763b441f49645
parent 54226 e3df2a4e02fc
child 54228 229282d53781
moving generic lemmas out of theory parity, disregarding some unused auxiliary lemmas;
tuned presburger
NEWS
src/HOL/Decision_Procs/Rat_Pair.thy
src/HOL/Divides.thy
src/HOL/Library/Code_Target_Int.thy
src/HOL/Parity.thy
src/HOL/Presburger.thy
src/HOL/Tools/Qelim/qelim.ML
     1.1 --- a/NEWS	Thu Oct 31 11:44:20 2013 +0100
     1.2 +++ b/NEWS	Thu Oct 31 11:44:20 2013 +0100
     1.3 @@ -4,6 +4,11 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Fact name generalization and consolidation:
    1.10 +  neq_one_mod_two, mod_2_not_eq_zero_eq_one_int ~> not_mod_2_eq_0_eq_1
    1.11 +
    1.12  
    1.13  
    1.14  New in Isabelle2013-1 (November 2013)
     2.1 --- a/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
     2.2 +++ b/src/HOL/Divides.thy	Thu Oct 31 11:44:20 2013 +0100
     2.3 @@ -2620,11 +2620,6 @@
     2.4    "Suc 0 mod numeral v' = nat (1 mod numeral v')"
     2.5    by (subst nat_mod_distrib) simp_all
     2.6  
     2.7 -lemma mod_2_not_eq_zero_eq_one_int:
     2.8 -  fixes k :: int
     2.9 -  shows "k mod 2 \<noteq> 0 \<longleftrightarrow> k mod 2 = 1"
    2.10 -  by auto
    2.11 -
    2.12  instance int :: semiring_numeral_div
    2.13    by intro_classes (auto intro: zmod_le_nonneg_dividend
    2.14      simp add: zmult_div_cancel
     3.1 --- a/src/HOL/Library/Code_Target_Int.thy	Thu Oct 31 11:44:20 2013 +0100
     3.2 +++ b/src/HOL/Library/Code_Target_Int.thy	Thu Oct 31 11:44:20 2013 +0100
     3.3 @@ -99,7 +99,7 @@
     3.4  proof -
     3.5    from mod_div_equality have *: "of_int k = of_int (k div 2 * 2 + k mod 2)" by simp
     3.6    show ?thesis
     3.7 -    by (simp add: Let_def divmod_int_mod_div mod_2_not_eq_zero_eq_one_int
     3.8 +    by (simp add: Let_def divmod_int_mod_div not_mod_2_eq_0_eq_1
     3.9        of_int_add [symmetric]) (simp add: * mult_commute)
    3.10  qed
    3.11  
     4.1 --- a/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
     4.2 +++ b/src/HOL/Parity.thy	Thu Oct 31 11:44:20 2013 +0100
     4.3 @@ -11,11 +11,14 @@
     4.4  
     4.5  class even_odd = 
     4.6    fixes even :: "'a \<Rightarrow> bool"
     4.7 +begin
     4.8  
     4.9 -abbreviation
    4.10 -  odd :: "'a\<Colon>even_odd \<Rightarrow> bool" where
    4.11 +abbreviation odd :: "'a \<Rightarrow> bool"
    4.12 +where
    4.13    "odd x \<equiv> \<not> even x"
    4.14  
    4.15 +end
    4.16 +
    4.17  instantiation nat and int  :: even_odd
    4.18  begin
    4.19  
    4.20 @@ -52,7 +55,7 @@
    4.21    unfolding even_def by simp
    4.22  
    4.23  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
    4.24 -declare even_def[of "neg_numeral v", simp] for v
    4.25 +declare even_def [of "neg_numeral v", simp] for v
    4.26  
    4.27  lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
    4.28    unfolding even_nat_def by simp
    4.29 @@ -62,13 +65,6 @@
    4.30  
    4.31  subsection {* Even and odd are mutually exclusive *}
    4.32  
    4.33 -lemma int_pos_lt_two_imp_zero_or_one:
    4.34 -    "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1"
    4.35 -  by presburger
    4.36 -
    4.37 -lemma neq_one_mod_two [simp, presburger]: 
    4.38 -  "((x::int) mod 2 ~= 0) = (x mod 2 = 1)" by presburger
    4.39 -
    4.40  
    4.41  subsection {* Behavior under integer arithmetic operations *}
    4.42  declare dvd_def[algebra]
    4.43 @@ -158,10 +154,6 @@
    4.44  
    4.45  subsection {* Equivalent definitions *}
    4.46  
    4.47 -lemma nat_lt_two_imp_zero_or_one:
    4.48 -  "(x::nat) < Suc (Suc 0) ==> x = 0 | x = Suc 0"
    4.49 -by presburger
    4.50 -
    4.51  lemma even_nat_mod_two_eq_zero: "even (x::nat) ==> x mod (Suc (Suc 0)) = 0"
    4.52  by presburger
    4.53  
    4.54 @@ -244,7 +236,7 @@
    4.55  apply (metis field_power_not_zero divisors_zero order_antisym_conv zero_le_square)
    4.56  done
    4.57  
    4.58 -lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
    4.59 +lemma zero_le_power_eq [presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) =
    4.60      (even n | (odd n & 0 <= x))"
    4.61    apply auto
    4.62    apply (subst zero_le_odd_power [symmetric])
    4.63 @@ -277,9 +269,6 @@
    4.64    apply (simp add: zero_le_even_power)
    4.65    done
    4.66  
    4.67 -lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)"
    4.68 -  by (induct n) auto
    4.69 -
    4.70  lemma power_minus_even [simp]: "even n ==>
    4.71      (- x)^n = (x^n::'a::{comm_ring_1})"
    4.72    apply (subst power_minus)
    4.73 @@ -336,13 +325,6 @@
    4.74  
    4.75  lemma odd_add [simp]: "odd(m + n::nat) = (odd m \<noteq> odd n)" by presburger
    4.76  
    4.77 -lemma div_Suc: "Suc a div c = a div c + Suc 0 div c +
    4.78 -    (a mod c + Suc 0 mod c) div c" 
    4.79 -  apply (subgoal_tac "Suc a = a + Suc 0")
    4.80 -  apply (erule ssubst)
    4.81 -  apply (rule div_add1_eq, simp)
    4.82 -  done
    4.83 -
    4.84  lemma lemma_even_div2 [simp]: "even (n::nat) ==> (n + 1) div 2 = n div 2" by presburger
    4.85  
    4.86  lemma lemma_not_even_div2 [simp]: "~even n ==> (n + 1) div 2 = Suc (n div 2)"
    4.87 @@ -359,31 +341,29 @@
    4.88  text {* Simplify, when the exponent is a numeral *}
    4.89  
    4.90  lemmas zero_le_power_eq_numeral [simp] =
    4.91 -    zero_le_power_eq [of _ "numeral w"] for w
    4.92 +  zero_le_power_eq [of _ "numeral w"] for w
    4.93  
    4.94  lemmas zero_less_power_eq_numeral [simp] =
    4.95 -    zero_less_power_eq [of _ "numeral w"] for w
    4.96 +  zero_less_power_eq [of _ "numeral w"] for w
    4.97  
    4.98  lemmas power_le_zero_eq_numeral [simp] =
    4.99 -    power_le_zero_eq [of _ "numeral w"] for w
   4.100 +  power_le_zero_eq [of _ "numeral w"] for w
   4.101  
   4.102  lemmas power_less_zero_eq_numeral [simp] =
   4.103 -    power_less_zero_eq [of _ "numeral w"] for w
   4.104 +  power_less_zero_eq [of _ "numeral w"] for w
   4.105  
   4.106  lemmas zero_less_power_nat_eq_numeral [simp] =
   4.107 -    zero_less_power_nat_eq [of _ "numeral w"] for w
   4.108 +  nat_zero_less_power_iff [of _ "numeral w"] for w
   4.109  
   4.110 -lemmas power_eq_0_iff_numeral [simp] = power_eq_0_iff [of _ "numeral w"] for w
   4.111 +lemmas power_eq_0_iff_numeral [simp] =
   4.112 +  power_eq_0_iff [of _ "numeral w"] for w
   4.113  
   4.114 -lemmas power_even_abs_numeral [simp] = power_even_abs [of "numeral w" _] for w
   4.115 +lemmas power_even_abs_numeral [simp] =
   4.116 +  power_even_abs [of "numeral w" _] for w
   4.117  
   4.118  
   4.119  subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
   4.120  
   4.121 -lemma even_power_le_0_imp_0:
   4.122 -    "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
   4.123 -  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   4.124 -
   4.125  lemma zero_le_power_iff[presburger]:
   4.126    "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
   4.127  proof cases
   4.128 @@ -395,9 +375,10 @@
   4.129    assume odd: "odd n"
   4.130    then obtain k where "n = Suc(2*k)"
   4.131      by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
   4.132 -  thus ?thesis
   4.133 -    by (auto simp add: zero_le_mult_iff zero_le_even_power
   4.134 -             dest!: even_power_le_0_imp_0)
   4.135 +  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
   4.136 +    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
   4.137 +  ultimately show ?thesis
   4.138 +    by (auto simp add: zero_le_mult_iff zero_le_even_power)
   4.139  qed
   4.140  
   4.141  
   4.142 @@ -409,7 +390,6 @@
   4.143  lemma odd_plus_one_div_two: "odd (x::int) ==> (x + 1) div 2 = x div 2 + 1" by presburger
   4.144  
   4.145  lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
   4.146 -lemma [presburger]: "(Suc x) div Suc (Suc 0) = x div Suc (Suc 0) \<longleftrightarrow> even x" by presburger
   4.147  lemma even_nat_plus_one_div_two: "even (x::nat) ==>
   4.148      (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)" by presburger
   4.149  
   4.150 @@ -417,3 +397,4 @@
   4.151      (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))" by presburger
   4.152  
   4.153  end
   4.154 +
     5.1 --- a/src/HOL/Presburger.thy	Thu Oct 31 11:44:20 2013 +0100
     5.2 +++ b/src/HOL/Presburger.thy	Thu Oct 31 11:44:20 2013 +0100
     5.3 @@ -360,11 +360,15 @@
     5.4    apply simp
     5.5    done
     5.6  
     5.7 -lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"
     5.8 -shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 
     5.9 -  using not0 by (simp add: dvd_def)
    5.10 +lemma zdvd_mono:
    5.11 +  fixes k m t :: int
    5.12 +  assumes "k \<noteq> 0"
    5.13 +  shows "m dvd t \<equiv> k * m dvd k * t" 
    5.14 +  using assms by simp
    5.15  
    5.16 -lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
    5.17 +lemma uminus_dvd_conv:
    5.18 +  fixes d t :: int
    5.19 +  shows "d dvd t \<equiv> - d dvd t" and "d dvd t \<equiv> d dvd - t"
    5.20    by simp_all
    5.21  
    5.22  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
    5.23 @@ -406,24 +410,23 @@
    5.24    end
    5.25  *} "Cooper's algorithm for Presburger arithmetic"
    5.26  
    5.27 -declare dvd_eq_mod_eq_0[symmetric, presburger]
    5.28 -declare mod_1[presburger] 
    5.29 -declare mod_0[presburger]
    5.30 -declare mod_by_1[presburger]
    5.31 -declare mod_self[presburger]
    5.32 -declare mod_by_0[presburger]
    5.33 -declare mod_div_trivial[presburger]
    5.34 -declare div_mod_equality2[presburger]
    5.35 -declare div_mod_equality[presburger]
    5.36 -declare mod_div_equality2[presburger]
    5.37 -declare mod_div_equality[presburger]
    5.38 -declare mod_mult_self1[presburger]
    5.39 -declare mod_mult_self2[presburger]
    5.40 -declare div_mod_equality[presburger]
    5.41 -declare div_mod_equality2[presburger]
    5.42 +declare dvd_eq_mod_eq_0 [symmetric, presburger]
    5.43 +declare mod_1 [presburger] 
    5.44 +declare mod_0 [presburger]
    5.45 +declare mod_by_1 [presburger]
    5.46 +declare mod_self [presburger]
    5.47 +declare div_by_0 [presburger]
    5.48 +declare mod_by_0 [presburger]
    5.49 +declare mod_div_trivial [presburger]
    5.50 +declare div_mod_equality2 [presburger]
    5.51 +declare div_mod_equality [presburger]
    5.52 +declare mod_div_equality2 [presburger]
    5.53 +declare mod_div_equality [presburger]
    5.54 +declare mod_mult_self1 [presburger]
    5.55 +declare mod_mult_self2 [presburger]
    5.56  declare mod2_Suc_Suc[presburger]
    5.57 -lemma [presburger]: "(a::int) div 0 = 0" and [presburger]: "a mod 0 = a"
    5.58 -by simp_all
    5.59 +declare not_mod_2_eq_0_eq_1 [presburger] 
    5.60 +declare nat_zero_less_power_iff [presburger]
    5.61  
    5.62  lemma [presburger, algebra]: "m mod 2 = (1::nat) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    5.63  lemma [presburger, algebra]: "m mod 2 = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
    5.64 @@ -432,3 +435,4 @@
    5.65  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
    5.66  
    5.67  end
    5.68 +
     6.1 --- a/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 31 11:44:20 2013 +0100
     6.2 +++ b/src/HOL/Tools/Qelim/qelim.ML	Thu Oct 31 11:44:20 2013 +0100
     6.3 @@ -37,7 +37,7 @@
     6.4       val th = Thm.abstract_rule s x ((conv env' then_conv ncv env') p')
     6.5                     |> Drule.arg_cong_rule e
     6.6       val th' = simpex_conv (Thm.rhs_of th)
     6.7 -     val (l,r) = Thm.dest_equals (cprop_of th')
     6.8 +     val (_, r) = Thm.dest_equals (cprop_of th')
     6.9      in if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
    6.10         else Thm.transitive (Thm.transitive th th') (conv env r) end
    6.11    | Const(@{const_name Ex},_)$ _ => (Thm.eta_long_conversion then_conv conv env) p