src/HOL/Int.thy
 changeset 66836 4eb431c3f974 parent 66816 212a3334e7da child 66886 960509bfd47e
```     1.1 --- a/src/HOL/Int.thy	Tue Oct 10 22:18:58 2017 +0100
1.2 +++ b/src/HOL/Int.thy	Mon Oct 09 19:10:47 2017 +0200
1.3 @@ -556,6 +556,43 @@
1.4    "nat (of_bool P) = of_bool P"
1.5    by auto
1.6
1.7 +lemma split_nat [arith_split]: "P (nat i) \<longleftrightarrow> ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
1.8 +  (is "?P = (?L \<and> ?R)")
1.9 +  for i :: int
1.10 +proof (cases "i < 0")
1.11 +  case True
1.12 +  then show ?thesis
1.13 +    by auto
1.14 +next
1.15 +  case False
1.16 +  have "?P = ?L"
1.17 +  proof
1.18 +    assume ?P
1.19 +    then show ?L using False by auto
1.20 +  next
1.21 +    assume ?L
1.22 +    moreover from False have "int (nat i) = i"
1.23 +      by (simp add: not_less)
1.24 +    ultimately show ?P
1.25 +      by simp
1.26 +  qed
1.27 +  with False show ?thesis by simp
1.28 +qed
1.29 +
1.30 +lemma all_nat: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x\<ge>0. P (nat x))"
1.31 +  by (auto split: split_nat)
1.32 +
1.33 +lemma ex_nat: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> P (nat x))"
1.34 +proof
1.35 +  assume "\<exists>x. P x"
1.36 +  then obtain x where "P x" ..
1.37 +  then have "int x \<ge> 0 \<and> P (nat (int x))" by simp
1.38 +  then show "\<exists>x\<ge>0. P (nat x)" ..
1.39 +next
1.40 +  assume "\<exists>x\<ge>0. P (nat x)"
1.41 +  then show "\<exists>x. P x" by auto
1.42 +qed
1.43 +
1.44
1.45  text \<open>For termination proofs:\<close>
1.46  lemma measure_function_int[measure_function]: "is_measure (nat \<circ> abs)" ..
1.47 @@ -1043,25 +1080,6 @@
1.48  \<close>
1.49  lemmas int_eq_iff_numeral [simp] = int_eq_iff [of _ "numeral v"] for v
1.50
1.51 -lemma split_nat [arith_split]: "P (nat i) = ((\<forall>n. i = int n \<longrightarrow> P n) \<and> (i < 0 \<longrightarrow> P 0))"
1.52 -  (is "?P = (?L \<and> ?R)")
1.53 -  for i :: int
1.54 -proof (cases "i < 0")
1.55 -  case True
1.56 -  then show ?thesis by auto
1.57 -next
1.58 -  case False
1.59 -  have "?P = ?L"
1.60 -  proof
1.61 -    assume ?P
1.62 -    then show ?L using False by auto
1.63 -  next
1.64 -    assume ?L
1.65 -    then show ?P using False by simp
1.66 -  qed
1.67 -  with False show ?thesis by simp
1.68 -qed
1.69 -
1.70  lemma nat_abs_int_diff: "nat \<bar>int a - int b\<bar> = (if a \<le> b then b - a else a - b)"
1.71    by auto
1.72
```