diff -r dfda74619509 -r ddd97d9dfbfb src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Thu Oct 29 08:14:39 2009 +0100 +++ b/src/HOL/Presburger.thy Thu Oct 29 11:41:36 2009 +0100 @@ -385,20 +385,6 @@ text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*} -lemma all_nat: "(\x. P x) \ (\x\0. P (nat x))" - by (simp split add: split_nat) - -lemma ex_nat: "(\x. P x) \ (\x. 0 \ x \ P (nat x))" -proof - assume "\x. P x" - then obtain x where "P x" .. - then have "int x \ 0 \ P (nat (int x))" by simp - then show "\x\0. P (nat x)" .. -next - assume "\x\0. P (nat x)" - then show "\x. P x" by auto -qed - lemma zdiff_int_split: "P (int (x - y)) = ((y \ x \ P (int x - int y)) \ (x < y \ P 0))" by (case_tac "y \ x", simp_all add: zdiff_int)