(*  Title:      HOL/Integ/IntArith.thy

    ID:         $Id$

    Authors:    Larry Paulson and Tobias Nipkow

*)

header {* Integer arithmetic *}

theory IntArith = Bin

files ("int_arith1.ML"):

subsection{*Inequality Reasoning for the Arithmetic Simproc*}

lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"

apply (rule eq_Abs_Integ [of z])

apply (rule eq_Abs_Integ [of w])

apply (simp add: linorder_not_le [symmetric] zle int_def zadd One_int_def)

done

use "int_arith1.ML"

setup int_arith_setup

subsection{*More inequality reasoning*}

lemma zless_add1_eq: "(w < z + (1::int)) = (w<z | w=z)"

by arith

lemma add1_zle_eq: "(w + (1::int) \<le> z) = (w<z)"

by arith

lemma zle_diff1_eq [simp]: "(w \<le> z - (1::int)) = (w<(z::int))"

by arith

lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w\<le>(z::int))"

by arith

lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"

by arith

lemma int_one_le_iff_zero_less: "((1::int) \<le> z) = (0 < z)"

by arith

subsection{*The Functions @{term nat} and @{term int}*}

lemma nonneg_eq_int: "[| 0 \<le> z;  !!m. z = int m ==> P |] ==> P"

by (blast dest: nat_0_le sym)

lemma nat_eq_iff: "(nat w = m) = (if 0 \<le> w then w = int m else m=0)"

by auto

lemma nat_eq_iff2: "(m = nat w) = (if 0 \<le> w then w = int m else m=0)"

by auto

lemma nat_less_iff: "0 \<le> w ==> (nat w < m) = (w < int m)"

apply (rule iffI)

apply (erule nat_0_le [THEN subst])

apply (simp_all del: zless_int add: zless_int [symmetric]) 

done

lemma int_eq_iff: "(int m = z) = (m = nat z & 0 \<le> z)"

by (auto simp add: nat_eq_iff2)

text{*Simplify the terms @{term "int 0"}, @{term "int(Suc 0)"} and

  @{term "w + - z"}*}

declare Zero_int_def [symmetric, simp]

declare One_int_def [symmetric, simp]

text{*cooper.ML refers to this theorem*}

lemmas zdiff_def_symmetric = zdiff_def [symmetric, simp]

lemma nat_0: "nat 0 = 0"

by (simp add: nat_eq_iff)

lemma nat_1: "nat 1 = Suc 0"

by (subst nat_eq_iff, simp)

lemma nat_2: "nat 2 = Suc (Suc 0)"

by (subst nat_eq_iff, simp)

lemma nat_less_eq_zless: "0 \<le> w ==> (nat w < nat z) = (w<z)"

apply (case_tac "z < 0")

apply (auto simp add: nat_less_iff)

done

lemma nat_le_eq_zle: "0 < w | 0 \<le> z ==> (nat w \<le> nat z) = (w\<le>z)"

by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)

text{*This simplifies expressions of the form @{term "int n = z"} where

      z is an integer literal.*}

declare int_eq_iff [of _ "number_of v", standard, simp]

lemma int_nat_eq [simp]: "int (nat z) = (if 0 \<le> z then z else 0)"

  by simp

lemma split_nat [arith_split]:

  "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"

  (is "?P = (?L & ?R)")

proof (cases "i < 0")

  case True thus ?thesis by simp

next

  case False

  have "?P = ?L"

  proof

    assume ?P thus ?L using False by clarsimp

  next

    assume ?L thus ?P using False by simp

  qed

  with False show ?thesis by simp

qed

subsubsection "Induction principles for int"

                     (* `set:int': dummy construction *)

theorem int_ge_induct[case_names base step,induct set:int]:

  assumes ge: "k \<le> (i::int)" and

        base: "P(k)" and

        step: "\<And>i. \<lbrakk>k \<le> i; P i\<rbrakk> \<Longrightarrow> P(i+1)"

  shows "P i"

proof -

  { fix n have "\<And>i::int. n = nat(i-k) \<Longrightarrow> k \<le> i \<Longrightarrow> P i"

    proof (induct n)

      case 0

      hence "i = k" by arith

      thus "P i" using base by simp

    next

      case (Suc n)

      hence "n = nat((i - 1) - k)" by arith

      moreover

      have ki1: "k \<le> i - 1" using Suc.prems by arith

      ultimately

      have "P(i - 1)" by(rule Suc.hyps)

      from step[OF ki1 this] show ?case by simp

    qed

  }

  from this ge show ?thesis by fast

qed

                     (* `set:int': dummy construction *)

theorem int_gr_induct[case_names base step,induct set:int]:

  assumes gr: "k < (i::int)" and

        base: "P(k+1)" and

        step: "\<And>i. \<lbrakk>k < i; P i\<rbrakk> \<Longrightarrow> P(i+1)"

  shows "P i"

apply(rule int_ge_induct[of "k + 1"])

  using gr apply arith

 apply(rule base)

apply (rule step, simp+)

done

theorem int_le_induct[consumes 1,case_names base step]:

  assumes le: "i \<le> (k::int)" and

        base: "P(k)" and

        step: "\<And>i. \<lbrakk>i \<le> k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"

  shows "P i"

proof -

  { fix n have "\<And>i::int. n = nat(k-i) \<Longrightarrow> i \<le> k \<Longrightarrow> P i"

    proof (induct n)

      case 0

      hence "i = k" by arith

      thus "P i" using base by simp

    next

      case (Suc n)

      hence "n = nat(k - (i+1))" by arith

      moreover

      have ki1: "i + 1 \<le> k" using Suc.prems by arith

      ultimately

      have "P(i+1)" by(rule Suc.hyps)

      from step[OF ki1 this] show ?case by simp

    qed

  }

  from this le show ?thesis by fast

qed

theorem int_less_induct[consumes 1,case_names base step]:

  assumes less: "(i::int) < k" and

        base: "P(k - 1)" and

        step: "\<And>i. \<lbrakk>i < k; P i\<rbrakk> \<Longrightarrow> P(i - 1)"

  shows "P i"

apply(rule int_le_induct[of _ "k - 1"])

  using less apply arith

 apply(rule base)

apply (rule step, simp+)

done

subsection{*Intermediate value theorems*}

lemma int_val_lemma:

     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->  

      f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"

apply (induct_tac "n", simp)

apply (intro strip)

apply (erule impE, simp)

apply (erule_tac x = n in allE, simp)

apply (case_tac "k = f (n+1) ")

 apply force

apply (erule impE)

 apply (simp add: zabs_def split add: split_if_asm)

apply (blast intro: le_SucI)

done

lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]

lemma nat_intermed_int_val:

     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;  

         f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"

apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k 

       in int_val_lemma)

apply simp

apply (erule impE)

 apply (intro strip)

 apply (erule_tac x = "i+m" in allE, arith)

apply (erule exE)

apply (rule_tac x = "i+m" in exI, arith)

done

subsection{*Products and 1, by T. M. Rasmussen*}

lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"

apply auto

apply (subgoal_tac "m*1 = m*n")

apply (drule mult_cancel_left [THEN iffD1], auto)

done

lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"

apply (rule_tac y = "1*n" in order_less_trans)

apply (rule_tac [2] mult_strict_right_mono)

apply (simp_all (no_asm_simp))

done

lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"

apply auto

apply (case_tac "m=1")

apply (case_tac [2] "n=1")

apply (case_tac [4] "m=1")

apply (case_tac [5] "n=1", auto)

apply (tactic"distinct_subgoals_tac")

apply (subgoal_tac "1<m*n", simp)

apply (rule zless_1_zmult, arith)

apply (subgoal_tac "0<n", arith)

apply (subgoal_tac "0<m*n")

apply (drule zero_less_mult_iff [THEN iffD1], auto)

done

lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"

apply (case_tac "0<m")

apply (simp add: pos_zmult_eq_1_iff)

apply (case_tac "m=0")

apply (simp del: number_of_reorient)

apply (subgoal_tac "0 < -m")

apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)

done

subsection{*More about nat*}

(*Analogous to zadd_int*)

lemma zdiff_int: "n \<le> m ==> int m - int n = int (m-n)"

by (induct m n rule: diff_induct, simp_all)

lemma nat_add_distrib:

     "[| (0::int) \<le> z;  0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"

apply (rule inj_int [THEN injD])

apply (simp add: zadd_int [symmetric])

done

lemma nat_diff_distrib:

     "[| (0::int) \<le> z';  z' \<le> z |] ==> nat (z-z') = nat z - nat z'"

apply (rule inj_int [THEN injD])

apply (simp add: zdiff_int [symmetric] nat_le_eq_zle)

done

lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"

apply (case_tac "0 \<le> z'")

apply (rule inj_int [THEN injD])

apply (simp add: zmult_int [symmetric] zero_le_mult_iff)

apply (simp add: mult_le_0_iff)

done

lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"

apply (rule trans)

apply (rule_tac [2] nat_mult_distrib, auto)

done

lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"

apply (case_tac "z=0 | w=0")

apply (auto simp add: zabs_def nat_mult_distrib [symmetric] 

                      nat_mult_distrib_neg [symmetric] mult_less_0_iff)

done

ML

{*

val zle_diff1_eq = thm "zle_diff1_eq";

val zle_add1_eq_le = thm "zle_add1_eq_le";

val nonneg_eq_int = thm "nonneg_eq_int";

val nat_eq_iff = thm "nat_eq_iff";

val nat_eq_iff2 = thm "nat_eq_iff2";

val nat_less_iff = thm "nat_less_iff";

val int_eq_iff = thm "int_eq_iff";

val nat_0 = thm "nat_0";

val nat_1 = thm "nat_1";

val nat_2 = thm "nat_2";

val nat_less_eq_zless = thm "nat_less_eq_zless";

val nat_le_eq_zle = thm "nat_le_eq_zle";

val nat_intermed_int_val = thm "nat_intermed_int_val";

val zmult_eq_self_iff = thm "zmult_eq_self_iff";

val zless_1_zmult = thm "zless_1_zmult";

val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";

val zmult_eq_1_iff = thm "zmult_eq_1_iff";

val nat_add_distrib = thm "nat_add_distrib";

val nat_diff_distrib = thm "nat_diff_distrib";

val nat_mult_distrib = thm "nat_mult_distrib";

val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";

val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";

*}

end