# HG changeset patch
# User haftmann
# Date 1252584478 -7200
# Node ID bf781ef40c8193b3ecc4318ccb776325607e475c
# Parent  b4119bbb2b79ae63d2c83d8085b93c2100a48c92
cleanedup theorems all_nat ex_nat

diff -r b4119bbb2b79 -r bf781ef40c81 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Sep 09 12:29:06 2009 +0200
+++ b/src/HOL/IntDiv.thy	Thu Sep 10 14:07:58 2009 +0200
@@ -1102,20 +1102,6 @@
   thus ?thesis by simp
 qed
 
-
-theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-apply (simp split add: split_nat)
-apply (rule iffI)
-apply (erule exE)
-apply (rule_tac x = "int x" in exI)
-apply simp
-apply (erule exE)
-apply (rule_tac x = "nat x" in exI)
-apply (erule conjE)
-apply (erule_tac x = "nat x" in allE)
-apply simp
-done
-
 theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
 proof -
   have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
diff -r b4119bbb2b79 -r bf781ef40c81 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Wed Sep 09 12:29:06 2009 +0200
+++ b/src/HOL/Presburger.thy	Thu Sep 10 14:07:58 2009 +0200
@@ -382,15 +382,22 @@
 
 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))"
+
+lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
   by (simp split add: split_nat)
 
-lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
-  apply (auto split add: split_nat)
-  apply (rule_tac x="int x" in exI, simp)
-  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
-  done
+lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
+proof
+  assume "\<exists>x. P x"
+  then obtain x where "P x" ..
+  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
+  then show "\<exists>x\<ge>0. P (nat x)" ..
+next
+  assume "\<exists>x\<ge>0. P (nat x)"
+  then show "\<exists>x. P x" by auto
+qed
 
 lemma zdiff_int_split: "P (int (x - y)) =
   ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"