moved lemma all_not_ex to HOL.thy ; tuned proofs
authorchaieb
Sun Jun 17 13:39:27 2007 +0200 (2007-06-17)
changeset 234058993b3144358
parent 23404 8659acd81f9d
child 23406 167b53019d6f
moved lemma all_not_ex to HOL.thy ; tuned proofs
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Presburger.thy	Sun Jun 17 13:39:25 2007 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Sun Jun 17 13:39:27 2007 +0200
     1.3 @@ -373,9 +373,6 @@
     1.4  shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 
     1.5    using not0 by (simp add: dvd_def)
     1.6  
     1.7 -lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))"
     1.8 -by blast
     1.9 -
    1.10  lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
    1.11    by simp_all
    1.12  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
    1.13 @@ -599,7 +596,7 @@
    1.14  
    1.15  
    1.16  lemma less_Pls_Pls:
    1.17 -  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by presburger 
    1.18 +  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp 
    1.19  
    1.20  lemma less_Pls_Min:
    1.21    "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
    1.22 @@ -618,7 +615,7 @@
    1.23    unfolding Pls_def Min_def by presburger 
    1.24  
    1.25  lemma less_Min_Min:
    1.26 -  "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by presburger 
    1.27 +  "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp
    1.28  
    1.29  lemma less_Min_Bit:
    1.30    "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"