author chaieb Sun Jun 17 13:39:27 2007 +0200 (2007-06-17) changeset 23405 8993b3144358 parent 23404 8659acd81f9d child 23406 167b53019d6f
moved lemma all_not_ex to HOL.thy ; tuned proofs
 src/HOL/Presburger.thy file | annotate | diff | revisions
```     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"
```