src/HOL/Presburger.thy

 
 lemma zdvd_mono: assumes not0: "(k::int) \<noteq> 0"
 shows "((m::int) dvd t) \<equiv> (k*m dvd k*t)" 
   using not0 by (simp add: dvd_def)
 
-lemma all_not_ex: "(ALL x. P x) = (~ (EX x. ~ P x ))"
-by blast
-
 lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
   by simp_all
 text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
 lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
   by (simp split add: split_nat)

   "(number_of k \<Colon> int) \<le> number_of l \<longleftrightarrow> k \<le> l"
   unfolding number_of_is_id ..
 
 
 lemma less_Pls_Pls:
-  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by presburger 
+  "Numeral.Pls < Numeral.Pls \<longleftrightarrow> False" by simp 
 
 lemma less_Pls_Min:
   "Numeral.Pls < Numeral.Min \<longleftrightarrow> False"
   unfolding Pls_def Min_def  by presburger 
 

 lemma less_Min_Pls:
   "Numeral.Min < Numeral.Pls \<longleftrightarrow> True"
   unfolding Pls_def Min_def by presburger 
 
 lemma less_Min_Min:
-  "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by presburger 
+  "Numeral.Min < Numeral.Min \<longleftrightarrow> False"  by simp
 
 lemma less_Min_Bit:
   "Numeral.Min < Numeral.Bit k v \<longleftrightarrow> Numeral.Min < k"
   unfolding Min_def Bit_def by (auto split: bit.split)