cleanedup theorems all_nat ex_nat
authorhaftmann
Thu Sep 10 14:07:58 2009 +0200 (2009-09-10)
changeset 32553bf781ef40c81
parent 32548 b4119bbb2b79
child 32554 4ccd84fb19d3
cleanedup theorems all_nat ex_nat
src/HOL/IntDiv.thy
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/IntDiv.thy	Wed Sep 09 12:29:06 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Thu Sep 10 14:07:58 2009 +0200
     1.3 @@ -1102,20 +1102,6 @@
     1.4    thus ?thesis by simp
     1.5  qed
     1.6  
     1.7 -
     1.8 -theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
     1.9 -apply (simp split add: split_nat)
    1.10 -apply (rule iffI)
    1.11 -apply (erule exE)
    1.12 -apply (rule_tac x = "int x" in exI)
    1.13 -apply simp
    1.14 -apply (erule exE)
    1.15 -apply (rule_tac x = "nat x" in exI)
    1.16 -apply (erule conjE)
    1.17 -apply (erule_tac x = "nat x" in allE)
    1.18 -apply simp
    1.19 -done
    1.20 -
    1.21  theorem zdvd_int: "(x dvd y) = (int x dvd int y)"
    1.22  proof -
    1.23    have "\<And>k. int y = int x * k \<Longrightarrow> x dvd y"
     2.1 --- a/src/HOL/Presburger.thy	Wed Sep 09 12:29:06 2009 +0200
     2.2 +++ b/src/HOL/Presburger.thy	Thu Sep 10 14:07:58 2009 +0200
     2.3 @@ -382,15 +382,22 @@
     2.4  
     2.5  lemma uminus_dvd_conv: "(d dvd (t::int)) \<equiv> (-d dvd t)" "(d dvd (t::int)) \<equiv> (d dvd -t)"
     2.6    by simp_all
     2.7 +
     2.8  text {* \bigskip Theorems for transforming predicates on nat to predicates on @{text int}*}
     2.9 -lemma all_nat: "(\<forall>x::nat. P x) = (\<forall>x::int. 0 <= x \<longrightarrow> P (nat x))"
    2.10 +
    2.11 +lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
    2.12    by (simp split add: split_nat)
    2.13  
    2.14 -lemma ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
    2.15 -  apply (auto split add: split_nat)
    2.16 -  apply (rule_tac x="int x" in exI, simp)
    2.17 -  apply (rule_tac x = "nat x" in exI,erule_tac x = "nat x" in allE, simp)
    2.18 -  done
    2.19 +lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
    2.20 +proof
    2.21 +  assume "\<exists>x. P x"
    2.22 +  then obtain x where "P x" ..
    2.23 +  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
    2.24 +  then show "\<exists>x\<ge>0. P (nat x)" ..
    2.25 +next
    2.26 +  assume "\<exists>x\<ge>0. P (nat x)"
    2.27 +  then show "\<exists>x. P x" by auto
    2.28 +qed
    2.29  
    2.30  lemma zdiff_int_split: "P (int (x - y)) =
    2.31    ((y \<le> x \<longrightarrow> P (int x - int y)) \<and> (x < y \<longrightarrow> P 0))"