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