Quelle Int.thy Sprache: Isabelle

(*  Title:      HOL/Int.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
*)

section \<open>The Integers as Equivalence Classes over Pairs of Natural Numbers\<close>

theory Int
  imports Quotient Groups_Big Fun_Def
begin

subsection \<open>Definition of integers as a quotient type\<close>

definition intrel :: "(nat \ nat) \ (nat \ nat) \ bool"
  where "intrel = (\(x, y) (u, v). x + v = u + y)"

lemma intrel_iff [simp]: "intrel (x, y) (u, v) \ x + v = u + y"
  by (simp add: intrel_def)

quotient_type int = "nat \ nat" / "intrel"
  morphisms Rep_Integ Abs_Integ
proof (rule equivpI)
  show "reflp intrel" by (auto simp: reflp_def)
  show "symp intrel" by (auto simp: symp_def)
  show "transp intrel" by (auto simp: transp_def)
qed

subsection \<open>Integers form a commutative ring\<close>

instantiation int :: comm_ring_1
begin

lift_definition zero_int :: "int" is "(0, 0)" .

lift_definition one_int :: "int" is "(1, 0)" .

lift_definition plus_int :: "int \ int \ int"
  is "\(x, y) (u, v). (x + u, y + v)"
  by clarsimp

lift_definition uminus_int :: "int \ int"
  is "\(x, y). (y, x)"
  by clarsimp

lift_definition minus_int :: "int \ int \ int"
  is "\(x, y) (u, v). (x + v, y + u)"
  by clarsimp

lift_definition times_int :: "int \ int \ int"
  is "\(x, y) (u, v). (x*u + y*v, x*v + y*u)"
proof (unfold intrel_def, clarify)
  fix s t u v w x y z :: nat
  assume "s + v = u + t" and "w + z = y + x"
  then have "(s + v) * w + (u + t) * x + u * (w + z) + v * (y + x) =
    (u + t) * w + (s + v) * x + u * (y + x) + v * (w + z)"
    by simp
  then show "(s * w + t * x) + (u * z + v * y) = (u * y + v * z) + (s * x + t * w)"
    by (simp add: algebra_simps)
qed

instance
  by standard (transfer; clarsimp simp: algebra_simps)+

end

abbreviation int :: "nat \ int"
  where "int \ of_nat"

lemma int_def: "int n = Abs_Integ (n, 0)"
  by (induct n) (simp add: zero_int.abs_eq, simp add: one_int.abs_eq plus_int.abs_eq)

lemma int_transfer [transfer_rule]:
  includes lifting_syntax
  shows "rel_fun (=) pcr_int (\n. (n, 0)) int"
  by (simp add: rel_fun_def int.pcr_cr_eq cr_int_def int_def)

lemma int_diff_cases: obtains (diff) m n where "z = int m - int n"
  by transfer clarsimp

subsection \<open>Integers are totally ordered\<close>

instantiation int :: linorder
begin

lift_definition less_eq_int :: "int \ int \ bool"
  is "\(x, y) (u, v). x + v \ u + y"
  by auto

lift_definition less_int :: "int \ int \ bool"
  is "\(x, y) (u, v). x + v < u + y"
  by auto

instance
  by standard (transfer, force)+

end

instantiation int :: distrib_lattice
begin

definition "(inf :: int \ int \ int) = min"

definition "(sup :: int \ int \ int) = max"

instance
  by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2)

end

subsection \<open>Ordering properties of arithmetic operations\<close>

instance int :: ordered_cancel_ab_semigroup_add
proof
  fix i j k :: int
  show "i \ j \ k + i \ k + j"
    by transfer clarsimp
qed

text \<open>Strict Monotonicity of Multiplication.\<close>

text \<open>Strict, in 1st argument; proof is by induction on \<open>k > 0\<close>.\<close>
lemma zmult_zless_mono2_lemma: "i < j \ 0 < k \ int k * i < int k * j"
  for i j :: int
proof (induct k)
  case 0
  then show ?case by simp
next
  case (Suc k)
  then show ?case
    by (cases "k = 0") (simp_all add: distrib_right add_strict_mono)
qed

lemma zero_le_imp_eq_int:
  assumes "k \ (0::int)" shows "\n. k = int n"
proof -
  have "b \ a \ \n::nat. a = n + b" for a b
    using exI[of _ "a - b"] by simp
  with assms show ?thesis
    by transfer auto
qed

lemma zero_less_imp_eq_int:
  assumes "k > (0::int)" shows "\n>0. k = int n"
proof -
  have "b < a \ \n::nat. n>0 \ a = n + b" for a b
    using exI[of _ "a - b"] by simp
  with assms show ?thesis
    by transfer auto
qed

lemma zmult_zless_mono2: "i < j \ 0 < k \ k * i < k * j"
  for i j k :: int
  by (drule zero_less_imp_eq_int) (auto simp add: zmult_zless_mono2_lemma)

text \<open>The integers form an ordered integral domain.\<close>

instantiation int :: linordered_idom
begin

definition zabs_def: "\i::int\ = (if i < 0 then - i else i)"

definition zsgn_def: "sgn (i::int) = (if i = 0 then 0 else if 0 < i then 1 else - 1)"

instance
proof
  fix i j k :: int
  show "i < j \ 0 < k \ k * i < k * j"
    by (rule zmult_zless_mono2)
  show "\i\ = (if i < 0 then -i else i)"
    by (simp only: zabs_def)
  show "sgn (i::int) = (if i=0 then 0 else if 0
    by (simp only: zsgn_def)
qed

end

instance int :: discrete_linordered_semidom
proof
  fix k l :: int
  show \<open>k < l \<longleftrightarrow> k + 1 \<le> l\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
  proof
    assume ?Q
    then show ?P
      by simp
  next
    assume ?P
    then have \<open>l - k > 0\<close>
      by simp
    with zero_less_imp_eq_int obtain n where \<open>l - k = int n\<close>
      by blast
    then have \<open>n > 0\<close>
      using \<open>l - k > 0\<close> by simp
    then have \<open>n \<ge> 1\<close>
      by simp
    then have \<open>int n \<ge> int 1\<close>
      by (rule of_nat_mono)
    with \<open>l - k = int n\<close> show ?Q
      by (simp add: algebra_simps)
  qed
qed

lemma zless_imp_add1_zle: "w < z \ w + 1 \ z"
  for w z :: int
  by transfer clarsimp

lemma zless_iff_Suc_zadd: "w < z \ (\n. z = w + int (Suc n))"
  for w z :: int
proof -
  have "\a b c d. a + d < c + b \ \n. c + b = Suc (a + n + d)"
  proof -
    fix a b c d :: nat
    assume "a + d < c + b"
    then have "c + b = Suc (a + (c + b - Suc (a + d)) + d) "
      by arith
    then show "\n. c + b = Suc (a + n + d)"
      by (rule exI)
  qed
  then show ?thesis
    by transfer auto
qed

lemma zabs_less_one_iff [simp]: "\z\ < 1 \ z = 0" (is "?lhs \ ?rhs")
  for z :: int
proof
  assume ?rhs
  then show ?lhs by simp
next
  assume ?lhs
  with zless_imp_add1_zle [of "\z\" 1] have "\z\ + 1 \ 1" by simp
  then have "\z\ \ 0" by simp
  then show ?rhs by simp
qed

subsection \<open>Embedding of the Integers into any \<open>ring_1\<close>: \<open>of_int\<close>\<close>

context ring_1
begin

lift_definition of_int :: "int \ 'a"
  is "\(i, j). of_nat i - of_nat j"
  by (clarsimp simp add: diff_eq_eq eq_diff_eq diff_add_eq
      of_nat_add [symmetric] simp del: of_nat_add)

lemma of_int_0 [simp]: "of_int 0 = 0"
  by transfer simp

lemma of_int_1 [simp]: "of_int 1 = 1"
  by transfer simp

lemma of_int_add [simp]: "of_int (w + z) = of_int w + of_int z"
  by transfer (clarsimp simp add: algebra_simps)

lemma of_int_minus [simp]: "of_int (- z) = - (of_int z)"
  by (transfer fixing: uminus) clarsimp

lemma of_int_diff [simp]: "of_int (w - z) = of_int w - of_int z"
  using of_int_add [of w "- z"] by simp

lemma of_int_mult [simp]: "of_int (w*z) = of_int w * of_int z"
  by (transfer fixing: times) (clarsimp simp add: algebra_simps)

lemma mult_of_int_commute: "of_int x * y = y * of_int x"
  by (transfer fixing: times) (auto simp: algebra_simps mult_of_nat_commute)

text \<open>Collapse nested embeddings.\<close>
lemma of_int_of_nat_eq [simp]: "of_int (int n) = of_nat n"
  by (induct n) auto

lemma of_int_numeral [simp, code_post]: "of_int (numeral k) = numeral k"
  by (simp add: of_nat_numeral [symmetric] of_int_of_nat_eq [symmetric])

lemma of_int_neg_numeral [code_post]: "of_int (- numeral k) = - numeral k"
  by simp

lemma of_int_power [simp]: "of_int (z ^ n) = of_int z ^ n"
  by (induct n) simp_all

lemma of_int_of_bool [simp]:
  "of_int (of_bool P) = of_bool P"
  by auto

end

context ring_char_0
begin

lemma of_int_eq_iff [simp]: "of_int w = of_int z \ w = z"
  by transfer (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)

text \<open>Special cases where either operand is zero.\<close>
lemma of_int_eq_0_iff [simp]: "of_int z = 0 \ z = 0"
  using of_int_eq_iff [of z 0] by simp

lemma of_int_0_eq_iff [simp]: "0 = of_int z \ z = 0"
  using of_int_eq_iff [of 0 z] by simp

lemma of_int_eq_1_iff [iff]: "of_int z = 1 \ z = 1"
  using of_int_eq_iff [of z 1] by simp

lemma of_nat_of_int_iff: "of_int i = of_nat n \ i = of_nat n" "of_nat n = of_int i \ i = of_nat n"
  by (metis of_int_eq_iff of_int_of_nat_eq)+

lemma numeral_power_eq_of_int_cancel_iff [simp]:
  "numeral x ^ n = of_int y \ numeral x ^ n = y"
  using of_int_eq_iff[of "numeral x ^ n" y, unfolded of_int_numeral of_int_power] .

lemma of_int_eq_numeral_power_cancel_iff [simp]:
  "of_int y = numeral x ^ n \ y = numeral x ^ n"
  using numeral_power_eq_of_int_cancel_iff [of x n y] by (metis (mono_tags))

lemma neg_numeral_power_eq_of_int_cancel_iff [simp]:
  "(- numeral x) ^ n = of_int y \ (- numeral x) ^ n = y"
  using of_int_eq_iff[of "(- numeral x) ^ n" y]
  by simp

lemma of_int_eq_neg_numeral_power_cancel_iff [simp]:
  "of_int y = (- numeral x) ^ n \ y = (- numeral x) ^ n"
  using neg_numeral_power_eq_of_int_cancel_iff[of x n y] by (metis (mono_tags))

lemma of_int_eq_of_int_power_cancel_iff[simp]: "(of_int b) ^ w = of_int x \ b ^ w = x"
  by (metis of_int_power of_int_eq_iff)

lemma of_int_power_eq_of_int_cancel_iff[simp]: "of_int x = (of_int b) ^ w \ x = b ^ w"
  by (metis of_int_eq_of_int_power_cancel_iff)

end

context linordered_idom
begin

text \<open>Every \<open>linordered_idom\<close> has characteristic zero.\<close>
subclass ring_char_0 ..

lemma of_int_le_iff [simp]: "of_int w \ of_int z \ w \ z"
  by (transfer fixing: less_eq)
    (clarsimp simp add: algebra_simps of_nat_add [symmetric] simp del: of_nat_add)

lemma of_int_less_iff [simp]: "of_int w < of_int z \ w < z"
  by (simp add: less_le order_less_le)

lemma of_int_0_le_iff [simp]: "0 \ of_int z \ 0 \ z"
  using of_int_le_iff [of 0 z] by simp

lemma of_int_le_0_iff [simp]: "of_int z \ 0 \ z \ 0"
  using of_int_le_iff [of z 0] by simp

lemma of_int_0_less_iff [simp]: "0 < of_int z \ 0 < z"
  using of_int_less_iff [of 0 z] by simp

lemma of_int_less_0_iff [simp]: "of_int z < 0 \ z < 0"
  using of_int_less_iff [of z 0] by simp

lemma of_int_1_le_iff [simp]: "1 \ of_int z \ 1 \ z"
  using of_int_le_iff [of 1 z] by simp

lemma of_int_le_1_iff [simp]: "of_int z \ 1 \ z \ 1"
  using of_int_le_iff [of z 1] by simp

lemma of_int_1_less_iff [simp]: "1 < of_int z \ 1 < z"
  using of_int_less_iff [of 1 z] by simp

lemma of_int_less_1_iff [simp]: "of_int z < 1 \ z < 1"
  using of_int_less_iff [of z 1] by simp

lemma of_int_pos: "z > 0 \ of_int z > 0"
  by simp

lemma of_int_nonneg: "z \ 0 \ of_int z \ 0"
  by simp

lemma of_int_abs [simp]: "of_int \x\ = \of_int x\"
  by (auto simp add: abs_if)

lemma of_int_lessD:
  assumes "\of_int n\ < x"
  shows "n = 0 \ x > 1"
proof (cases "n = 0")
  case True
  then show ?thesis by simp
next
  case False
  then have "\n\ \ 0" by simp
  then have "\n\ > 0" by simp
  then have "\n\ \ 1"
    using zless_imp_add1_zle [of 0 "\n\"] by simp
  then have "\of_int n\ \ 1"
    unfolding of_int_1_le_iff [of "\n\", symmetric] by simp
  then have "1 < x" using assms by (rule le_less_trans)
  then show ?thesis ..
qed

lemma of_int_leD:
  assumes "\of_int n\ \ x"
  shows "n = 0 \ 1 \ x"
proof (cases "n = 0")
  case True
  then show ?thesis by simp
next
  case False
  then have "\n\ \ 0" by simp
  then have "\n\ > 0" by simp
  then have "\n\ \ 1"
    using zless_imp_add1_zle [of 0 "\n\"] by simp
  then have "\of_int n\ \ 1"
    unfolding of_int_1_le_iff [of "\n\", symmetric] by simp
  then have "1 \ x" using assms by (rule order_trans)
  then show ?thesis ..
qed

lemma numeral_power_le_of_int_cancel_iff [simp]:
  "numeral x ^ n \ of_int a \ numeral x ^ n \ a"
  by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_le_iff)

lemma of_int_le_numeral_power_cancel_iff [simp]:
  "of_int a \ numeral x ^ n \ a \ numeral x ^ n"
  by (metis (mono_tags) local.numeral_power_eq_of_int_cancel_iff of_int_le_iff)

lemma numeral_power_less_of_int_cancel_iff [simp]:
  "numeral x ^ n < of_int a \ numeral x ^ n < a"
  by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff)

lemma of_int_less_numeral_power_cancel_iff [simp]:
  "of_int a < numeral x ^ n \ a < numeral x ^ n"
  by (metis (mono_tags) local.of_int_eq_numeral_power_cancel_iff of_int_less_iff)

lemma neg_numeral_power_le_of_int_cancel_iff [simp]:
  "(- numeral x) ^ n \ of_int a \ (- numeral x) ^ n \ a"
  by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power)

lemma of_int_le_neg_numeral_power_cancel_iff [simp]:
  "of_int a \ (- numeral x) ^ n \ a \ (- numeral x) ^ n"
  by (metis (mono_tags) of_int_le_iff of_int_neg_numeral of_int_power)

lemma neg_numeral_power_less_of_int_cancel_iff [simp]:
  "(- numeral x) ^ n < of_int a \ (- numeral x) ^ n < a"
  using of_int_less_iff[of "(- numeral x) ^ n" a]
  by simp

lemma of_int_less_neg_numeral_power_cancel_iff [simp]:
  "of_int a < (- numeral x) ^ n \ a < (- numeral x::int) ^ n"
  using of_int_less_iff[of a "(- numeral x) ^ n"]
  by simp

lemma of_int_le_of_int_power_cancel_iff[simp]: "(of_int b) ^ w \ of_int x \ b ^ w \ x"
  by (metis (mono_tags) of_int_le_iff of_int_power)

lemma of_int_power_le_of_int_cancel_iff[simp]: "of_int x \ (of_int b) ^ w\ x \ b ^ w"
  by (metis (mono_tags) of_int_le_iff of_int_power)

lemma of_int_less_of_int_power_cancel_iff[simp]: "(of_int b) ^ w < of_int x \ b ^ w < x"
  by (metis (mono_tags) of_int_less_iff of_int_power)

lemma of_int_power_less_of_int_cancel_iff[simp]: "of_int x < (of_int b) ^ w\ x < b ^ w"
  by (metis (mono_tags) of_int_less_iff of_int_power)

lemma of_int_max: "of_int (max x y) = max (of_int x) (of_int y)"
  by (auto simp: max_def)

lemma of_int_min: "of_int (min x y) = min (of_int x) (of_int y)"
  by (auto simp: min_def)

end

context division_ring
begin

lemmas mult_inverse_of_int_commute =
  mult_commute_imp_mult_inverse_commute[OF mult_of_int_commute]

end

text \<open>Comparisons involving \<^term>\<open>of_int\<close>.\<close>

lemma of_int_eq_numeral_iff [iff]: "of_int z = (numeral n :: 'a::ring_char_0) \ z = numeral n"
  using of_int_eq_iff by fastforce

lemma of_int_le_numeral_iff [simp]:
  "of_int z \ (numeral n :: 'a::linordered_idom) \ z \ numeral n"
  using of_int_le_iff [of z "numeral n"] by simp

lemma of_int_numeral_le_iff [simp]:
  "(numeral n :: 'a::linordered_idom) \ of_int z \ numeral n \ z"
  using of_int_le_iff [of "numeral n"] by simp

lemma of_int_less_numeral_iff [simp]:
  "of_int z < (numeral n :: 'a::linordered_idom) \ z < numeral n"
  using of_int_less_iff [of z "numeral n"] by simp

lemma of_int_numeral_less_iff [simp]:
  "(numeral n :: 'a::linordered_idom) < of_int z \ numeral n < z"
  using of_int_less_iff [of "numeral n" z] by simp

lemma of_nat_less_of_int_iff: "(of_nat n::'a::linordered_idom) < of_int x \ int n < x"
  by (metis of_int_of_nat_eq of_int_less_iff)

lemma of_int_eq_id [simp]: "of_int = id"
proof
  show "of_int z = id z" for z
    by (cases z rule: int_diff_cases) simp
qed

instance int :: no_top
proof
  fix x::int
  have "x < x + 1"
    by simp
  then show "\y. x < y"
    by (rule exI)
qed

instance int :: no_bot
proof
  fix x::int
  have "x - 1< x"
    by simp
  then show "\y. y < x"
    by (rule exI)
qed

subsection \<open>Magnitude of an Integer, as a Natural Number: \<open>nat\<close>\<close>

lift_definition nat :: "int \ nat" is "\(x, y). x - y"
  by auto

lemma nat_int [simp]: "nat (int n) = n"
  by transfer simp

lemma int_nat_eq [simp]: "int (nat z) = (if 0 \ z then z else 0)"
  by transfer clarsimp

lemma nat_0_le: "0 \ z \ int (nat z) = z"
  by simp

lemma nat_le_0 [simp]: "z \ 0 \ nat z = 0"
  by transfer clarsimp

lemma nat_le_eq_zle: "0 < w \ 0 \ z \ nat w \ nat z \ w \ z"
  by transfer (clarsimp, arith)

text \<open>An alternative condition is \<^term>\<open>0 \<le> w\<close>.\<close>
lemma nat_mono_iff: "0 < z \ nat w < nat z \ w < z"
  by (simp add: nat_le_eq_zle linorder_not_le [symmetric])

lemma nat_less_eq_zless: "0 \ w \ nat w < nat z \ w < z"
  by (simp add: nat_le_eq_zle linorder_not_le [symmetric])

lemma zless_nat_conj [simp]: "nat w < nat z \ 0 < z \ w < z"
  by transfer (clarsimp, arith)

lemma nonneg_int_cases:
  assumes "0 \ k"
  obtains n where "k = int n"
proof -
  from assms have "k = int (nat k)"
    by simp
  then show thesis
    by (rule that)
qed

lemma pos_int_cases:
  assumes "0 < k"
  obtains n where "k = int n" and "n > 0"
proof -
  from assms have "0 \ k"
    by simp
  then obtain n where "k = int n"
    by (rule nonneg_int_cases)
  moreover have "n > 0"
    using \<open>k = int n\<close> assms by simp
  ultimately show thesis
    by (rule that)
qed

lemma nonpos_int_cases:
  assumes "k \ 0"
  obtains n where "k = - int n"
proof -
  from assms have "- k \ 0"
    by simp
  then obtain n where "- k = int n"
    by (rule nonneg_int_cases)
  then have "k = - int n"
    by simp
  then show thesis
    by (rule that)
qed

lemma neg_int_cases:
  assumes "k < 0"
  obtains n where "k = - int n" and "n > 0"
proof -
  from assms have "- k > 0"
    by simp
  then obtain n where "- k = int n" and "- k > 0"
    by (blast elim: pos_int_cases)
  then have "k = - int n" and "n > 0"
    by simp_all
  then show thesis
    by (rule that)
qed

lemma nat_eq_iff: "nat w = m \ (if 0 \ w then w = int m else m = 0)"
  by transfer (clarsimp simp add: le_imp_diff_is_add)

lemma nat_eq_iff2: "m = nat w \ (if 0 \ w then w = int m else m = 0)"
  using nat_eq_iff [of w m] by auto

lemma nat_0 [simp]: "nat 0 = 0"
  by (simp add: nat_eq_iff)

lemma nat_1 [simp]: "nat 1 = Suc 0"
  by (simp add: nat_eq_iff)

lemma nat_numeral [simp]: "nat (numeral k) = numeral k"
  by (simp add: nat_eq_iff)

lemma nat_neg_numeral [simp]: "nat (- numeral k) = 0"
  by simp

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

lemma nat_less_iff: "0 \ w \ nat w < m \ w < of_nat m"
  by transfer (clarsimp, arith)

lemma nat_le_iff: "nat x \ n \ x \ int n"
  by transfer (clarsimp simp add: le_diff_conv)

lemma nat_mono: "x \ y \ nat x \ nat y"
  by transfer auto

lemma nat_0_iff[simp]: "nat i = 0 \ i \ 0"
  for i :: int
  by transfer clarsimp

lemma int_eq_iff: "of_nat m = z \ m = nat z \ 0 \ z"
  by (auto simp add: nat_eq_iff2)

lemma zero_less_nat_eq [simp]: "0 < nat z \ 0 < z"
  using zless_nat_conj [of 0] by auto

lemma nat_add_distrib: "0 \ z \ 0 \ z' \ nat (z + z') = nat z + nat z'"
  by transfer clarsimp

lemma nat_diff_distrib': "0 \ x \ 0 \ y \ nat (x - y) = nat x - nat y"
  by transfer clarsimp

lemma nat_diff_distrib: "0 \ z' \ z' \ z \ nat (z - z') = nat z - nat z'"
  by (rule nat_diff_distrib') auto

lemma nat_zminus_int [simp]: "nat (- int n) = 0"
  by transfer simp

lemma le_nat_iff: "k \ 0 \ n \ nat k \ int n \ k"
  by transfer auto

lemma zless_nat_eq_int_zless: "m < nat z \ int m < z"
  by transfer (clarsimp simp add: less_diff_conv)

lemma (in ring_1) of_nat_nat [simp]: "0 \ z \ of_nat (nat z) = of_int z"
  by transfer (clarsimp simp add: of_nat_diff)

lemma diff_nat_numeral [simp]: "(numeral v :: nat) - numeral v' = nat (numeral v - numeral v')"
  by (simp only: nat_diff_distrib' zero_le_numeral nat_numeral)

lemma nat_abs_triangle_ineq:
  "nat \k + l\ \ nat \k\ + nat \l\"
  by (simp add: nat_add_distrib [symmetric] nat_le_eq_zle abs_triangle_ineq)

lemma nat_of_bool [simp]:
  "nat (of_bool P) = of_bool P"
  by auto

lemma split_nat [linarith_split]: "P (nat i) \ ((\n. i = int n \ P n) \ (i < 0 \ P 0))"
  (is "?P = (?L \ ?R)")
  for i :: int
proof (cases "i < 0")
  case True
  then show ?thesis
    by auto
next
  case False
  have "?P = ?L"
  proof
    assume ?P
    then show ?L using False by auto
  next
    assume ?L
    moreover from False have "int (nat i) = i"
      by (simp add: not_less)
    ultimately show ?P
      by simp
  qed
  with False show ?thesis by simp
qed

lemma all_nat: "(\x. P x) \ (\x\0. P (nat x))"
  by (auto split: split_nat)

lemma ex_nat: "(\x. P x) \ (\x. 0 \ x \ P (nat x))"
proof
  assume "\x. P x"
  then obtain x where "P x" ..
  then have "int x \ 0 \ P (nat (int x))" by simp
  then show "\x\0. P (nat x)" ..
next
  assume "\x\0. P (nat x)"
  then show "\x. P x" by auto
qed

text \<open>For termination proofs:\<close>
lemma measure_function_int[measure_function]: "is_measure (nat \ abs)" ..

subsection \<open>Lemmas about the Function \<^term>\<open>of_nat\<close> and Orderings\<close>

lemma negative_zless_0: "- (int (Suc n)) < (0 :: int)"
  by (simp add: order_less_le del: of_nat_Suc)

lemma negative_zless [iff]: "- (int (Suc n)) < int m"
  by (rule negative_zless_0 [THEN order_less_le_trans], simp)

lemma negative_zle_0: "- int n \ 0"
  by (simp add: minus_le_iff)

lemma negative_zle [iff]: "- int n \ int m"
  by (rule order_trans [OF negative_zle_0 of_nat_0_le_iff])

lemma not_zle_0_negative [simp]: "\ 0 \ - int (Suc n)"
  by (subst le_minus_iff) (simp del: of_nat_Suc)

lemma int_zle_neg: "int n \ - int m \ n = 0 \ m = 0"
  by transfer simp

lemma not_int_zless_negative [simp]: "\ int n < - int m"
  by (simp add: linorder_not_less)

lemma negative_eq_positive [simp]: "- int n = of_nat m \ n = 0 \ m = 0"
  by (force simp add: order_eq_iff [of "- of_nat n"] int_zle_neg)

lemma zle_iff_zadd: "w \ z \ (\n. z = w + int n)"
  (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs by auto
next
  assume ?lhs
  then have "0 \ z - w" by simp
  then obtain n where "z - w = int n"
    using zero_le_imp_eq_int [of "z - w"] by blast
  then have "z = w + int n" by simp
  then show ?rhs ..
qed

lemma zadd_int_left: "int m + (int n + z) = int (m + n) + z"
  by simp

lemma negD:
  assumes "x < 0" shows "\n. x = - (int (Suc n))"
proof -
  have "\a b. a < b \ \n. Suc (a + n) = b"
  proof -
    fix a b:: nat
    assume "a < b"
    then have "Suc (a + (b - Suc a)) = b"
      by arith
    then show "\n. Suc (a + n) = b"
      by (rule exI)
  qed
  with assms show ?thesis
    by transfer auto
qed

subsection \<open>Cases and induction\<close>

text \<open>
  Now we replace the case analysis rule by a more conventional one:
  whether an integer is negative or not.
\<close>

text \<open>This version is symmetric in the two subgoals.\<close>
lemma int_cases2 [case_names nonneg nonpos, cases type: int]:
  "(\n. z = int n \ P) \ (\n. z = - (int n) \ P) \ P"
  by (cases "z < 0") (auto simp add: linorder_not_less dest!: negD nat_0_le [THEN sym])

text \<open>This is the default, with a negative case.\<close>
lemma int_cases [case_names nonneg neg, cases type: int]:
  assumes pos: "\n. z = int n \ P" and neg: "\n. z = - (int (Suc n)) \ P"
  shows P
proof (cases "z < 0")
  case True
  with neg show ?thesis
    by (blast dest!: negD)
next
  case False
  with pos show ?thesis
    by (force simp add: linorder_not_less dest: nat_0_le [THEN sym])
qed

lemma int_cases3 [case_names zero pos neg]:
  fixes k :: int
  assumes "k = 0 \ P" and "\n. k = int n \ n > 0 \ P"
    and "\n. k = - int n \ n > 0 \ P"
  shows "P"
proof (cases k "0::int" rule: linorder_cases)
  case equal
  with assms(1) show P by simp
next
  case greater
  then have *: "nat k > 0" by simp
  moreover from * have "k = int (nat k)" by auto
  ultimately show P using assms(2) by blast
next
  case less
  then have *: "nat (- k) > 0" by simp
  moreover from * have "k = - int (nat (- k))" by auto
  ultimately show P using assms(3) by blast
qed

lemma int_of_nat_induct [case_names nonneg neg, induct type: int]:
  "(\n. P (int n)) \ (\n. P (- (int (Suc n)))) \ P z"
  by (cases z) auto

lemma sgn_mult_dvd_iff [simp]:
  "sgn r * l dvd k \ l dvd k \ (r = 0 \ k = 0)" for k l r :: int
  by (cases r rule: int_cases3) auto

lemma mult_sgn_dvd_iff [simp]:
  "l * sgn r dvd k \ l dvd k \ (r = 0 \ k = 0)" for k l r :: int
  using sgn_mult_dvd_iff [of r l k] by (simp add: ac_simps)

lemma dvd_sgn_mult_iff [simp]:
  "l dvd sgn r * k \ l dvd k \ r = 0" for k l r :: int
  by (cases r rule: int_cases3) simp_all

lemma dvd_mult_sgn_iff [simp]:
  "l dvd k * sgn r \ l dvd k \ r = 0" for k l r :: int
  using dvd_sgn_mult_iff [of l r k] by (simp add: ac_simps)

lemma int_sgnE:
  fixes k :: int
  obtains n and l where "k = sgn l * int n"
proof -
  have "k = sgn k * int (nat \k\)"
    by (simp add: sgn_mult_abs)
  then show ?thesis ..
qed

subsubsection \<open>Binary comparisons\<close>

text \<open>Preliminaries\<close>

lemma le_imp_0_less:
  fixes z :: int
  assumes le: "0 \ z"
  shows "0 < 1 + z"
proof -
  have "0 \ z" by fact
  also have "\ < z + 1" by (rule less_add_one)
  also have "\ = 1 + z" by (simp add: ac_simps)
  finally show "0 < 1 + z" .
qed

lemma odd_less_0_iff: "1 + z + z < 0 \ z < 0"
  for z :: int
proof (cases z)
  case (nonneg n)
  then show ?thesis
    by (simp add: linorder_not_less add.assoc add_increasing le_imp_0_less [THEN order_less_imp_le])
next
  case (neg n)
  then show ?thesis
    by (simp del: of_nat_Suc of_nat_add of_nat_1
        add: algebra_simps of_nat_1 [where 'a=int, symmetric] of_nat_add [symmetric])
qed

subsubsection \<open>Comparisons, for Ordered Rings\<close>

lemma odd_nonzero: "1 + z + z \ 0"
  for z :: int
proof (cases z)
  case (nonneg n)
  have le: "0 \ z + z"
    by (simp add: nonneg add_increasing)
  then show ?thesis
    using le_imp_0_less [OF le] by (auto simp: ac_simps)
next
  case (neg n)
  show ?thesis
  proof
    assume eq: "1 + z + z = 0"
    have "0 < 1 + (int n + int n)"
      by (simp add: le_imp_0_less add_increasing)
    also have "\ = - (1 + z + z)"
      by (simp add: neg add.assoc [symmetric])
    also have "\ = 0" by (simp add: eq)
    finally have "0<0" ..
    then show False by blast
  qed
qed

subsection \<open>The Set of Integers\<close>

context ring_1
begin

definition Ints :: "'a set"  (\<open>\<int>\<close>)
  where "\ = range of_int"

lemma Ints_of_int [simp]: "of_int z \ \"
  by (simp add: Ints_def)

lemma Ints_of_nat [simp]: "of_nat n \ \"
  using Ints_of_int [of "of_nat n"] by simp

lemma Ints_0 [simp]: "0 \ \"
  using Ints_of_int [of "0"] by simp

lemma Ints_1 [simp]: "1 \ \"
  using Ints_of_int [of "1"] by simp

lemma Ints_numeral [simp]: "numeral n \ \"
  by (subst of_nat_numeral [symmetric], rule Ints_of_nat)

lemma Ints_add [simp]: "a \ \ \ b \ \ \ a + b \ \"
  by (force simp add: Ints_def simp flip: of_int_add intro: range_eqI)

lemma Ints_minus [simp]: "a \ \ \ -a \ \"
  by (force simp add: Ints_def simp flip: of_int_minus intro: range_eqI)

lemma minus_in_Ints_iff [simp]: "-x \ \ \ x \ \"
  using Ints_minus[of x] Ints_minus[of "-x"] by auto

lemma Ints_diff [simp]: "a \ \ \ b \ \ \ a - b \ \"
  by (force simp add: Ints_def simp flip: of_int_diff intro: range_eqI)

lemma Ints_mult [simp]: "a \ \ \ b \ \ \ a * b \ \"
  by (force simp add: Ints_def simp flip: of_int_mult intro: range_eqI)

lemma Ints_power [simp]: "a \ \ \ a ^ n \ \"
  by (induct n) simp_all

lemma Ints_cases [cases set: Ints]:
  assumes "q \ \"
  obtains (of_int) z where "q = of_int z"
  unfolding Ints_def
proof -
  from \<open>q \<in> \<int>\<close> have "q \<in> range of_int" unfolding Ints_def .
  then obtain z where "q = of_int z" ..
  then show thesis ..
qed

lemma Ints_induct [case_names of_int, induct set: Ints]:
  "q \ \ \ (\z. P (of_int z)) \ P q"
  by (rule Ints_cases) auto

lemma Nats_subset_Ints: "\ \ \"
  unfolding Nats_def Ints_def
  by (rule subsetI, elim imageE, hypsubst, subst of_int_of_nat_eq[symmetric], rule imageI) simp_all

lemma Nats_altdef1: "\ = {of_int n |n. n \ 0}"
proof (intro subsetI equalityI)
  fix x :: 'a
  assume "x \ {of_int n |n. n \ 0}"
  then obtain n where "x = of_int n" "n \ 0"
    by (auto elim!: Ints_cases)
  then have "x = of_nat (nat n)"
    by (subst of_nat_nat) simp_all
  then show "x \ \"
    by simp
next
  fix x :: 'a
  assume "x \ \"
  then obtain n where "x = of_nat n"
    by (auto elim!: Nats_cases)
  then have "x = of_int (int n)" by simp
  also have "int n \ 0" by simp
  then have "of_int (int n) \ {of_int n |n. n \ 0}" by blast
  finally show "x \ {of_int n |n. n \ 0}" .
qed

end

lemma Ints_sum [intro]: "(\x. x \ A \ f x \ \) \ sum f A \ \"
  by (induction A rule: infinite_finite_induct) auto

lemma Ints_prod [intro]: "(\x. x \ A \ f x \ \) \ prod f A \ \"
  by (induction A rule: infinite_finite_induct) auto

lemma (in linordered_idom) Ints_abs [simp]:
  shows "a \ \ \ abs a \ \"
  by (auto simp: abs_if)

lemma (in linordered_idom) Nats_altdef2: "\ = {n \ \. n \ 0}"
proof (intro subsetI equalityI)
  fix x :: 'a
  assume "x \ {n \ \. n \ 0}"
  then obtain n where "x = of_int n" "n \ 0"
    by (auto elim!: Ints_cases)
  then have "x = of_nat (nat n)"
    by (subst of_nat_nat) simp_all
  then show "x \ \"
    by simp
qed (auto elim!: Nats_cases)

lemma (in idom_divide) of_int_divide_in_Ints:
  "of_int a div of_int b \ \" if "b dvd a"
proof -
  from that obtain c where "a = b * c" ..
  then show ?thesis
    by (cases "of_int b = 0") simp_all
qed

text \<open>The premise involving \<^term>\<open>Ints\<close> prevents \<^term>\<open>a = 1/2\<close>.\<close>

lemma Ints_double_eq_0_iff:
  fixes a :: "'a::ring_char_0"
  assumes in_Ints: "a \ \"
  shows "a + a = 0 \ a = 0"
    (is "?lhs \ ?rhs")
proof -
  from in_Ints have "a \ range of_int"
    unfolding Ints_def [symmetric] .
  then obtain z where a: "a = of_int z" ..
  show ?thesis
  proof
    assume ?rhs
    then show ?lhs by simp
  next
    assume ?lhs
    with a have "of_int (z + z) = (of_int 0 :: 'a)" by simp
    then have "z + z = 0" by (simp only: of_int_eq_iff)
    then have "z = 0" by (simp only: double_zero)
    with a show ?rhs by simp
  qed
qed

lemma Ints_odd_nonzero:
  fixes a :: "'a::ring_char_0"
  assumes in_Ints: "a \ \"
  shows "1 + a + a \ 0"
proof -
  from in_Ints have "a \ range of_int"
    unfolding Ints_def [symmetric] .
  then obtain z where a: "a = of_int z" ..
  show ?thesis
  proof
    assume "1 + a + a = 0"
    with a have "of_int (1 + z + z) = (of_int 0 :: 'a)" by simp
    then have "1 + z + z = 0" by (simp only: of_int_eq_iff)
    with odd_nonzero show False by blast
  qed
qed

lemma Nats_numeral [simp]: "numeral w \ \"
  using of_nat_in_Nats [of "numeral w"] by simp

lemma Ints_odd_less_0:
  fixes a :: "'a::linordered_idom"
  assumes in_Ints: "a \ \"
  shows "1 + a + a < 0 \ a < 0"
proof -
  from in_Ints have "a \ range of_int"
    unfolding Ints_def [symmetric] .
  then obtain z where a: "a = of_int z" ..
  with a have "1 + a + a < 0 \ of_int (1 + z + z) < (of_int 0 :: 'a)"
    by simp
  also have "\ \ z < 0"
    by (simp only: of_int_less_iff odd_less_0_iff)
  also have "\ \ a < 0"
    by (simp add: a)
  finally show ?thesis .
qed

lemma add_in_Ints_iff_left [simp]: "x \ \ \ x + y \ \ \ y \ \"
  by (metis Ints_add Ints_diff add_diff_cancel_left')

lemma add_in_Ints_iff_right [simp]: "y \ \ \ x + y \ \ \ x \ \"
  by (subst add.commute) auto

lemma diff_in_Ints_iff_left [simp]: "x \ \ \ x - y \ \ \ y \ \"
  by (metis Ints_diff add_in_Ints_iff_left diff_add_cancel)

lemma diff_in_Ints_iff_right [simp]: "y \ \ \ x - y \ \ \ x \ \"
  by (metis Ints_minus diff_in_Ints_iff_left minus_diff_eq)

lemmas [simp] = minus_in_Ints_iff

lemma fraction_not_in_Ints:
  assumes "\(n dvd m)" "n \ 0"
  shows   "of_int m / of_int n \ (\ :: 'a :: {division_ring,ring_char_0} set)"
proof
  assume "of_int m / (of_int n :: 'a) \ \"
  then obtain k where "of_int m / of_int n = (of_int k :: 'a)" by (elim Ints_cases)
  with assms have "of_int m = (of_int (k * n) :: 'a)" by (auto simp add: field_split_simps)
  hence "m = k * n" by (subst (asm) of_int_eq_iff)
  hence "n dvd m" by simp
  with assms(1) show False by contradiction
qed

lemma of_int_div_of_int_in_Ints_iff:
  "(of_int n / of_int m :: 'a :: {division_ring,ring_char_0}) \ \ \ m = 0 \ m dvd n"
proof
  assume *: "m = 0 \ m dvd n"
  have "of_int n / of_int m \ (\ :: 'a set)" if "m \ 0" "m dvd n"
  proof -
    from \<open>m dvd n\<close> obtain k where "n = m * k"
      by (elim dvdE)
    hence "n = k * m"
      by (simp add: mult.commute)
    hence "of_int n / (of_int m :: 'a) = of_int k"
      using \<open>m \<noteq> 0\<close> by (simp add: field_simps)
    also have "\ \ \"
      by auto
    finally show ?thesis .
  qed
  with * show "of_int n / of_int m \ (\ :: 'a set)"
    by (cases "m = 0") auto
next
  assume *: "(of_int n / of_int m :: 'a) \ \"
  thus "m = 0 \ m dvd n"
    using fraction_not_in_Ints[of m n, where ?'a = 'a] by auto
qed

lemma fraction_numeral_not_in_Ints [simp]:
  assumes "\(numeral b :: int) dvd numeral a"
  shows   "numeral a / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)"
  using fraction_not_in_Ints[of "numeral b" "numeral a", where ?'a = 'a] assms by simp

subsection \<open>\<^term>\<open>sum\<close> and \<^term>\<open>prod\<close>\<close>

context semiring_1
begin

lemma of_nat_sum [simp]:
  "of_nat (sum f A) = (\x\A. of_nat (f x))"
  by (induction A rule: infinite_finite_induct) auto

end

context ring_1
begin

lemma of_int_sum [simp]:
  "of_int (sum f A) = (\x\A. of_int (f x))"
  by (induction A rule: infinite_finite_induct) auto

end

context comm_semiring_1
begin

lemma of_nat_prod [simp]:
  "of_nat (prod f A) = (\x\A. of_nat (f x))"
  by (induction A rule: infinite_finite_induct) auto

end

context comm_ring_1
begin

lemma of_int_prod [simp]:
  "of_int (prod f A) = (\x\A. of_int (f x))"
  by (induction A rule: infinite_finite_induct) auto

end

subsection \<open>Setting up simplification procedures\<close>

ML_file \<open>Tools/int_arith.ML\<close>

declaration \<open>K (
  Lin_Arith.add_discrete_type \<^type_name>\<open>Int.int\<close>
  #> Lin_Arith.add_lessD @{thm zless_imp_add1_zle}
  #> Lin_Arith.add_inj_thms @{thms of_nat_le_iff [THEN iffD2] of_nat_eq_iff [THEN iffD2]}
  #> Lin_Arith.add_inj_const (\<^const_name>\<open>of_nat\<close>, \<^typ>\<open>nat \<Rightarrow> int\<close>)
  #> Lin_Arith.add_simps
      @{thms of_int_0 of_int_1 of_int_add of_int_mult of_int_numeral of_int_neg_numeral nat_0 nat_1 diff_nat_numeral nat_numeral
      neg_less_iff_less
      True_implies_equals
      distrib_left [where a = "numeral v" for v]
      distrib_left [where a = "- numeral v" for v]
      div_by_1 div_0
      times_divide_eq_right times_divide_eq_left
      minus_divide_left [THEN sym] minus_divide_right [THEN sym]
      add_divide_distrib diff_divide_distrib
      of_int_minus of_int_diff
      of_int_of_nat_eq}
  #> Lin_Arith.add_simprocs [Int_Arith.zero_one_idom_simproc]
)\<close>

simproc_setup fast_arith
  ("(m::'a::linordered_idom) < n" |
    "(m::'a::linordered_idom) \ n" |
    "(m::'a::linordered_idom) = n") =
  \<open>K Lin_Arith.simproc\<close>

subsection\<open>More Inequality Reasoning\<close>

lemma zless_add1_eq: "w < z + 1 \ w < z \ w = z"
  for w z :: int
  by arith

lemma add1_zle_eq: "w + 1 \ z \ w < z"
  for w z :: int
  by arith

lemma zle_diff1_eq [simp]: "w \ z - 1 \ w < z"
  for w z :: int
  by arith

lemma zle_add1_eq_le [simp]: "w < z + 1 \ w \ z"
  for w z :: int
  by arith

lemma int_one_le_iff_zero_less: "1 \ z \ 0 < z"
  for z :: int
  by arith

lemma Ints_nonzero_abs_ge1:
  fixes x:: "'a :: linordered_idom"
    assumes "x \ Ints" "x \ 0"
    shows "1 \ abs x"
proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>])
  fix z::int
  assume "x = of_int z"
  with \<open>x \<noteq> 0\<close>
  show "1 \ \x\"
    apply (auto simp: abs_if)
    by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq)
qed

lemma Ints_nonzero_abs_less1:
  fixes x:: "'a :: linordered_idom"
  shows "\x \ Ints; abs x < 1\ \ x = 0"
    using Ints_nonzero_abs_ge1 [of x] by auto

lemma Ints_eq_abs_less1:
  fixes x:: "'a :: linordered_idom"
  shows "\x \ Ints; y \ Ints\ \ x = y \ abs (x-y) < 1"
  using eq_iff_diff_eq_0 by (fastforce intro: Ints_nonzero_abs_less1)

subsection \<open>The functions \<^term>\<open>nat\<close> and \<^term>\<open>int\<close>\<close>

text \<open>Simplify the term \<^term>\<open>w + - z\<close>.\<close>

lemma one_less_nat_eq [simp]: "Suc 0 < nat z \ 1 < z"
  using zless_nat_conj [of 1 z] by auto

lemma int_eq_iff_numeral [simp]:
  "int m = numeral v \ m = numeral v"
  by (simp add: int_eq_iff)

lemma nat_abs_int_diff:
  "nat \int a - int b\ = (if a \ b then b - a else a - b)"
  by auto

lemma nat_int_add: "nat (int a + int b) = a + b"
  by auto

context ring_1
begin

lemma of_int_of_nat [nitpick_simp]:
  "of_int k = (if k < 0 then - of_nat (nat (- k)) else of_nat (nat k))"
proof (cases "k < 0")
  case True
  then have "0 \ - k" by simp
  then have "of_nat (nat (- k)) = of_int (- k)" by (rule of_nat_nat)
  with True show ?thesis by simp
next
  case False
  then show ?thesis by (simp add: not_less)
qed

end

lemma transfer_rule_of_int:
  includes lifting_syntax
  fixes R :: "'a::ring_1 \ 'b::ring_1 \ bool"
  assumes [transfer_rule]: "R 0 0" "R 1 1"
    "(R ===> R ===> R) (+) (+)"
    "(R ===> R) uminus uminus"
  shows "((=) ===> R) of_int of_int"
proof -
  note assms
  note transfer_rule_of_nat [transfer_rule]
  have [transfer_rule]: "((=) ===> R) of_nat of_nat"
    by transfer_prover
  show ?thesis
    by (unfold of_int_of_nat [abs_def]) transfer_prover
qed

lemma nat_mult_distrib:
  fixes z z' :: int
  assumes "0 \ z"
  shows "nat (z * z') = nat z * nat z'"
proof (cases "0 \ z'")
  case False
  with assms have "z * z' \ 0"
    by (simp add: not_le mult_le_0_iff)
  then have "nat (z * z') = 0" by simp
  moreover from False have "nat z' = 0" by simp
  ultimately show ?thesis by simp
next
  case True
  with assms have ge_0: "z * z' \ 0" by (simp add: zero_le_mult_iff)
  show ?thesis
    by (rule injD [of "of_nat :: nat \ int", OF inj_of_nat])
      (simp only: of_nat_mult of_nat_nat [OF True]
         of_nat_nat [OF assms] of_nat_nat [OF ge_0], simp)
qed

lemma nat_mult_distrib_neg:
  assumes "z \ (0::int)" shows "nat (z * z') = nat (- z) * nat (- z')" (is "?L = ?R")
proof -
  have "?L = nat (- z * - z')"
    using assms by auto
  also have "... = ?R"
    by (rule nat_mult_distrib) (use assms in auto)
  finally show ?thesis .
qed

lemma nat_abs_mult_distrib: "nat \w * z\ = nat \w\ * nat \z\"
  by (cases "z = 0 \ w = 0")
    (auto simp add: abs_if nat_mult_distrib [symmetric]
      nat_mult_distrib_neg [symmetric] mult_less_0_iff)

lemma int_in_range_abs [simp]: "int n \ range abs"
proof (rule range_eqI)
  show "int n = \int n\" by simp
qed

lemma range_abs_Nats [simp]: "range abs = (\ :: int set)"
proof -
  have "\k\ \ \" for k :: int
    by (cases k) simp_all
  moreover have "k \ range abs" if "k \ \" for k :: int
    using that by induct simp
  ultimately show ?thesis by blast
qed

lemma Suc_nat_eq_nat_zadd1: "0 \ z \ Suc (nat z) = nat (1 + z)"
  for z :: int
  by (rule sym) (simp add: nat_eq_iff)

lemma diff_nat_eq_if:
  "nat z - nat z' =
    (if z' < 0 then nat z
     else
      let d = z - z'
      in if d < 0 then 0 else nat d)"
  by (simp add: Let_def nat_diff_distrib [symmetric])

lemma nat_numeral_diff_1 [simp]: "numeral v - (1::nat) = nat (numeral v - 1)"
  using diff_nat_numeral [of v Num.One] by simp

subsection \<open>Induction principles for int\<close>

text \<open>Well-founded segments of the integers.\<close>

definition int_ge_less_than :: "int \ (int \ int) set"
  where "int_ge_less_than d = {(z', z). d \ z' \ z' < z}"

lemma wf_int_ge_less_than: "wf (int_ge_less_than d)"
proof -
  have "int_ge_less_than d \ measure (\z. nat (z - d))"
    by (auto simp add: int_ge_less_than_def)
  then show ?thesis
    by (rule wf_subset [OF wf_measure])
qed

text \<open>
  This variant looks odd, but is typical of the relations suggested
  by RankFinder.\<close>

definition int_ge_less_than2 :: "int \ (int \ int) set"
  where "int_ge_less_than2 d = {(z',z). d \ z \ z' < z}"

lemma wf_int_ge_less_than2: "wf (int_ge_less_than2 d)"
proof -
  have "int_ge_less_than2 d \ measure (\z. nat (1 + z - d))"
    by (auto simp add: int_ge_less_than2_def)
  then show ?thesis
    by (rule wf_subset [OF wf_measure])
qed

(* `set:int': dummy construction *)
theorem int_ge_induct [case_names base step, induct set: int]:
  fixes i :: int
  assumes ge: "k \ i"
    and base: "P k"
    and step: "\i. k \ i \ P i \ P (i + 1)"
  shows "P i"
proof -
  have "\i::int. n = nat (i - k) \ k \ i \ P i" for n
  proof (induct n)
    case 0
    then have "i = k" by arith
    with base show "P i" by simp
  next
    case (Suc n)
    then have "n = nat ((i - 1) - k)" by arith
    moreover have k: "k \ i - 1" using Suc.prems by arith
    ultimately have "P (i - 1)" by (rule Suc.hyps)
    from step [OF k this] show ?case by simp
  qed
  with ge show ?thesis by fast
qed

(* `set:int': dummy construction *)
theorem int_gr_induct [case_names base step, induct set: int]:
  fixes i k :: int
  assumes "k < i" "P (k + 1)" "\i. k < i \ P i \ P (i + 1)"
  shows "P i"
proof -
  have "k+1 \ i"
    using assms by auto
  then show ?thesis
    by (induction i rule: int_ge_induct) (auto simp: assms)
qed

theorem int_le_induct [consumes 1, case_names base step]:
  fixes i k :: int
  assumes le: "i \ k"
    and base: "P k"
    and step: "\i. i \ k \ P i \ P (i - 1)"
  shows "P i"
proof -
  have "\i::int. n = nat(k-i) \ i \ k \ P i" for n
  proof (induct n)
    case 0
    then have "i = k" by arith
    with base show "P i" by simp
  next
    case (Suc n)
    then have "n = nat (k - (i + 1))" by arith
    moreover have k: "i + 1 \ k" using Suc.prems by arith
    ultimately have "P (i + 1)" by (rule Suc.hyps)
    from step[OF k this] show ?case by simp
  qed
  with le show ?thesis by fast
qed

theorem int_less_induct [consumes 1, case_names base step]:
  fixes i k :: int
  assumes "i < k" "P (k - 1)" "\i. i < k \ P i \ P (i - 1)"
  shows "P i"
proof -
  have "i \ k-1"
    using assms by auto
  then show ?thesis
    by (induction i rule: int_le_induct) (auto simp: assms)
qed

theorem int_induct [case_names base step1 step2]:
  fixes k :: int
  assumes base: "P k"
    and step1: "\i. k \ i \ P i \ P (i + 1)"
    and step2: "\i. k \ i \ P i \ P (i - 1)"
  shows "P i"
proof -
  have "i \ k \ i \ k" by arith
  then show ?thesis
  proof
    assume "i \ k"
    then show ?thesis
      using base by (rule int_ge_induct) (fact step1)
  next
    assume "i \ k"
    then show ?thesis
      using base by (rule int_le_induct) (fact step2)
  qed
qed

subsection \<open>Intermediate value theorems\<close>

lemma nat_ivt_aux:
  "\\if (Suc i) - f i\ \ 1; f 0 \ k; k \ f n\ \ \i \ n. f i = k"
  for m n :: nat and k :: int
proof (induct n)
  case (Suc n)
  show ?case
  proof (cases "k = f (Suc n)")
    case False
    with Suc have "k \ f n"
      by auto
    with Suc show ?thesis
      by (auto simp add: abs_if split: if_split_asm intro: le_SucI)
  qed (use Suc in auto)
qed auto

lemma nat_intermed_int_val:
  fixes m n :: nat and k :: int
  assumes "\i. m \ i \ i < n \ \f (Suc i) - f i\ \ 1" "m \ n" "f m \ k" "k \ f n"
  shows "\i. m \ i \ i \ n \ f i = k"
proof -
  obtain i where "i \ n - m" "k = f (m + i)"
    using nat_ivt_aux [of "n - m" "f \ plus m" k] assms by auto
  with assms show ?thesis
    using exI[of _ "m + i"] by auto
qed

lemma nat0_intermed_int_val:
  "\i\n. f i = k"
  if "\if (i + 1) - f i\ \ 1" "f 0 \ k" "k \ f n"
  for n :: nat and k :: int
  using nat_intermed_int_val [of 0 n f k] that by auto

subsection \<open>Products and 1, by T. M. Rasmussen\<close>

lemma abs_zmult_eq_1:
  fixes m n :: int
  assumes mn: "\m * n\ = 1"
  shows "\m\ = 1"
proof -
  from mn have 0: "m \ 0" "n \ 0" by auto
  have "\ 2 \ \m\"
  proof
    assume "2 \ \m\"
    then have "2 * \n\ \ \m\ * \n\" by (simp add: mult_mono 0)
    also have "\ = \m * n\" by (simp add: abs_mult)
    also from mn have "\ = 1" by simp
    finally have "2 * \n\ \ 1" .
    with 0 show "False" by arith
  qed
  with 0 show ?thesis by auto
qed

lemma pos_zmult_eq_1_iff_lemma: "m * n = 1 \ m = 1 \ m = - 1"
  for m n :: int
  using abs_zmult_eq_1 [of m n] by arith

lemma pos_zmult_eq_1_iff:
  fixes m n :: int
  assumes "0 < m"
  shows "m * n = 1 \ m = 1 \ n = 1"
proof -
  from assms have "m * n = 1 \ m = 1"
    by (auto dest: pos_zmult_eq_1_iff_lemma)
  then show ?thesis
    by (auto dest: pos_zmult_eq_1_iff_lemma)
qed

lemma zmult_eq_1_iff: "m * n = 1 \ (m = 1 \ n = 1) \ (m = - 1 \ n = - 1)" (is "?L = ?R")
  for m n :: int
proof
  assume L: ?L show ?R
    using pos_zmult_eq_1_iff_lemma [OF L] L by force
qed auto

lemma zmult_eq_neg1_iff: "a * b = (-1 :: int) \ a = 1 \ b = -1 \ a = -1 \ b = 1"
  using zmult_eq_1_iff[of a "-b"] by auto

lemma infinite_UNIV_int [simp]: "\ finite (UNIV::int set)"
proof
  assume "finite (UNIV::int set)"
  moreover have "inj (\i::int. 2 * i)"
    by (rule injI) simp
  ultimately have "surj (\i::int. 2 * i)"
    by (rule finite_UNIV_inj_surj)
  then obtain i :: int where "1 = 2 * i" by (rule surjE)
  then show False by (simp add: pos_zmult_eq_1_iff)
qed

subsection \<open>The divides relation\<close>

lemma zdvd_antisym_nonneg: "0 \ m \ 0 \ n \ m dvd n \ n dvd m \ m = n"
  for m n :: int
  by (auto simp add: dvd_def mult.assoc zero_le_mult_iff zmult_eq_1_iff)

lemma zdvd_antisym_abs:
  fixes a b :: int
  assumes "a dvd b" and "b dvd a"
  shows "\a\ = \b\"
proof (cases "a = 0")
  case True
  with assms show ?thesis by simp
next
  case False
  from \<open>a dvd b\<close> obtain k where k: "b = a * k"
    unfolding dvd_def by blast
  from \<open>b dvd a\<close> obtain k' where k': "a = b * k'"
    unfolding dvd_def by blast
  from k k' have "a = a * k * k'" by simp
  with mult_cancel_left1[where c="a" and b="k*k'"] have kk': "k * k' = 1"
    using \<open>a \<noteq> 0\<close> by (simp add: mult.assoc)
  then have "k = 1 \ k' = 1 \ k = -1 \ k' = -1"
    by (simp add: zmult_eq_1_iff)
  with k k' show ?thesis by auto
qed

lemma zdvd_zdiffD: "k dvd m - n \ k dvd n \ k dvd m"
  for k m n :: int
  using dvd_add_right_iff [of k "- n" m] by simp

lemma zdvd_reduce: "k dvd n + k * m \ k dvd n"
  for k m n :: int
  using dvd_add_times_triv_right_iff [of k n m] by (simp add: ac_simps)

lemma dvd_imp_le_int:
  fixes d i :: int
  assumes "i \ 0" and "d dvd i"
  shows "\d\ \ \i\"
proof -
  from \<open>d dvd i\<close> obtain k where "i = d * k" ..
  with \<open>i \<noteq> 0\<close> have "k \<noteq> 0" by auto
  then have "1 \ \k\" and "0 \ \d\" by auto
  then have "\d\ * 1 \ \d\ * \k\" by (rule mult_left_mono)
  with \<open>i = d * k\<close> show ?thesis by (simp add: abs_mult)
qed

lemma zdvd_not_zless:
  fixes m n :: int
  assumes "0 < m" and "m < n"
  shows "\ n dvd m"
proof
  from assms have "0 < n" by auto
  assume "n dvd m" then obtain k where k: "m = n * k" ..
  with \<open>0 < m\<close> have "0 < n * k" by auto
  with \<open>0 < n\<close> have "0 < k" by (simp add: zero_less_mult_iff)
  with k \<open>0 < n\<close> \<open>m < n\<close> have "n * k < n * 1" by simp
  with \<open>0 < n\<close> \<open>0 < k\<close> show False unfolding mult_less_cancel_left by auto
qed

lemma zdvd_mult_cancel:
  fixes k m n :: int
  assumes d: "k * m dvd k * n"
    and "k \ 0"
  shows "m dvd n"
proof -
  from d obtain h where h: "k * n = k * m * h"
    unfolding dvd_def by blast
  have "n = m * h"
  proof (rule ccontr)
    assume "\ ?thesis"
    with \<open>k \<noteq> 0\<close> have "k * n \<noteq> k * (m * h)" by simp
    with h show False
      by (simp add: mult.assoc)
  qed
  then show ?thesis by simp
qed

lemma int_dvd_int_iff [simp]:
  "int m dvd int n \ m dvd n"
proof -
  have "m dvd n" if "int n = int m * k" for k
  proof (cases k)
    case (nonneg q)
    with that have "n = m * q"
      by (simp del: of_nat_mult add: of_nat_mult [symmetric])
    then show ?thesis ..
  next
    case (neg q)
    with that have "int n = int m * (- int (Suc q))"
      by simp
    also have "\ = - (int m * int (Suc q))"
      by (simp only: mult_minus_right)
    also have "\ = - int (m * Suc q)"
      by (simp only: of_nat_mult [symmetric])
    finally have "- int (m * Suc q) = int n" ..
    then show ?thesis
      by (simp only: negative_eq_positive) auto
  qed
  then show ?thesis by (auto simp add: dvd_def)
qed

lemma dvd_nat_abs_iff [simp]:
  "n dvd nat \k\ \ int n dvd k"
proof -
  have "n dvd nat \k\ \ int n dvd int (nat \k\)"
    by (simp only: int_dvd_int_iff)
  then show ?thesis
    by simp
qed

lemma nat_abs_dvd_iff [simp]:
  "nat \k\ dvd n \ k dvd int n"
proof -
  have "nat \k\ dvd n \ int (nat \k\) dvd int n"
    by (simp only: int_dvd_int_iff)
  then show ?thesis
    by simp
qed

lemma zdvd1_eq [simp]: "x dvd 1 \ \x\ = 1" (is "?lhs \ ?rhs")
  for x :: int
proof
  assume ?lhs
  then have "nat \x\ dvd nat \1\"
    by (simp only: nat_abs_dvd_iff) simp
  then have "nat \x\ = 1"
    by simp
  then show ?rhs
    by (cases "x < 0") simp_all
next
  assume ?rhs
  then have "x = 1 \ x = - 1"
    by auto
  then show ?lhs
    by (auto intro: dvdI)
qed

lemma zdvd_mult_cancel1:
  fixes m :: int
  assumes mp: "m \ 0"
  shows "m * n dvd m \ \n\ = 1"
    (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs
    by (cases "n > 0") (auto simp add: minus_equation_iff)
next
  assume ?lhs
  then have "m * n dvd m * 1" by simp
  from zdvd_mult_cancel[OF this mp] show ?rhs
    by (simp only: zdvd1_eq)
qed

lemma nat_dvd_iff: "nat z dvd m \ (if 0 \ z then z dvd int m else m = 0)"
  using nat_abs_dvd_iff [of z m] by (cases "z \ 0") auto

lemma eq_nat_nat_iff: "0 \ z \ 0 \ z' \ nat z = nat z' \ z = z'"
  by (auto elim: nonneg_int_cases)

lemma nat_power_eq: "0 \ z \ nat (z ^ n) = nat z ^ n"
  by (induct n) (simp_all add: nat_mult_distrib)

lemma numeral_power_eq_nat_cancel_iff [simp]:
  "numeral x ^ n = nat y \ numeral x ^ n = y"
  using nat_eq_iff2 by auto

lemma nat_eq_numeral_power_cancel_iff [simp]:
  "nat y = numeral x ^ n \ y = numeral x ^ n"
  using numeral_power_eq_nat_cancel_iff[of x n y]
  by (metis (mono_tags))

lemma numeral_power_le_nat_cancel_iff [simp]:
  "numeral x ^ n \ nat a \ numeral x ^ n \ a"
  using nat_le_eq_zle[of "numeral x ^ n" a]
  by (auto simp: nat_power_eq)

lemma nat_le_numeral_power_cancel_iff [simp]:
  "nat a \ numeral x ^ n \ a \ numeral x ^ n"
  by (simp add: nat_le_iff)

lemma numeral_power_less_nat_cancel_iff [simp]:
  "numeral x ^ n < nat a \ numeral x ^ n < a"
  using nat_less_eq_zless[of "numeral x ^ n" a]
  by (auto simp: nat_power_eq)

lemma nat_less_numeral_power_cancel_iff [simp]:
  "nat a < numeral x ^ n \ a < numeral x ^ n"
  using nat_less_eq_zless[of a "numeral x ^ n"]
  by (cases "a < 0") (auto simp: nat_power_eq less_le_trans[where y=0])

lemma zdvd_imp_le: "z \ n" if "z dvd n" "0 < n" for n z :: int
proof (cases n)
  case (nonneg n)
  show ?thesis
    by (cases z) (use nonneg dvd_imp_le that in auto)
qed (use that in auto)

lemma zdvd_period:
  fixes a d :: int
  assumes "a dvd d"
  shows "a dvd (x + t) \ a dvd ((x + c * d) + t)"
    (is "?lhs \ ?rhs")
proof -
  from assms have "a dvd (x + t) \ a dvd ((x + t) + c * d)"
    by (simp add: dvd_add_left_iff)
  then show ?thesis
    by (simp add: ac_simps)
qed

lemma fraction_numeral_not_in_Ints' [simp]:
  assumes "b \ Num.One"
  shows   "1 / numeral b \ (\ :: 'a :: {division_ring, ring_char_0} set)"
proof -
  have *: "\numeral b dvd (1 :: int)"
    using assms by simp
  have "of_int 1 / of_int (numeral b) \ (\ :: 'a set)"
    by (rule fraction_not_in_Ints) (use * in auto)
  thus ?thesis
    by simp
qed

subsection \<open>Powers with integer exponents\<close>

text \<open>
  The following allows writing powers with an integer exponent. While the type signature
  is very generic, most theorems will assume that the underlying type is a division ring or
  a field.

  The notation `powi' is inspired by the `powr' notation for real/complex exponentiation.
\<close>
definition power_int :: "'a :: {inverse, power} \ int \ 'a" (infixr \powi\ 80) where
  "power_int x n = (if n \ 0 then x ^ nat n else inverse x ^ (nat (-n)))"

lemma power_int_0_right [simp]: "power_int x 0 = 1"
  and power_int_1_right [simp]:
        "power_int (y :: 'a :: {power, inverse, monoid_mult}) 1 = y"
  and power_int_minus1_right [simp]:
        "power_int (y :: 'a :: {power, inverse, monoid_mult}) (-1) = inverse y"
  by (simp_all add: power_int_def)

lemma power_int_of_nat [simp]: "power_int x (int n) = x ^ n"
  by (simp add: power_int_def)

lemma power_int_numeral [simp]: "power_int x (numeral n) = x ^ numeral n"
  by (simp add: power_int_def)

lemma powi_numeral_reduce: "x powi numeral n = x * x powi int (pred_numeral n)"
  by (simp add: numeral_eq_Suc)

lemma powi_minus_numeral_reduce: "x powi - (numeral n) = inverse x * x powi - int(pred_numeral n)"
  by (simp add: numeral_eq_Suc power_int_def)

lemma int_cases4 [case_names nonneg neg]:
  fixes m :: int
  obtains n where "m = int n" | n where "n > 0" "m = -int n"
proof (cases "m \ 0")
  case True
  thus ?thesis using that(1)[of "nat m"] by auto
next
  case False
  thus ?thesis using that(2)[of "nat (-m)"] by auto
qed

context
  assumes "SORT_CONSTRAINT('a::division_ring)"
begin

lemma power_int_minus: "power_int (x::'a) (-n) = inverse (power_int x n)"
  by (auto simp: power_int_def power_inverse)

lemma power_int_minus_divide: "power_int (x::'a) (-n) = 1 / (power_int x n)"
  by (simp add: divide_inverse power_int_minus)

lemma power_int_eq_0_iff [simp]: "power_int (x::'a) n = 0 \ x = 0 \ n \ 0"
  by (auto simp: power_int_def)

lemma power_int_0_left_if: "power_int (0 :: 'a) m = (if m = 0 then 1 else 0)"
  by (auto simp: power_int_def)

lemma power_int_0_left [simp]: "m \ 0 \ power_int (0 :: 'a) m = 0"
  by (simp add: power_int_0_left_if)

lemma power_int_1_left [simp]: "power_int 1 n = (1 :: 'a :: division_ring)"
  by (auto simp: power_int_def)

lemma power_diff_conv_inverse: "x \ 0 \ m \ n \ (x :: 'a) ^ (n - m) = x ^ n * inverse x ^ m"
  by (simp add: field_simps flip: power_add)

lemma power_mult_inverse_distrib: "x ^ m * inverse (x :: 'a) = inverse x * x ^ m"
proof (cases "x = 0")
  case [simp]: False
  show ?thesis
  proof (cases m)
    case (Suc m')
    have "x ^ Suc m' * inverse x = x ^ m'"
      by (subst power_Suc2) (auto simp: mult.assoc)
    also have "\ = inverse x * x ^ Suc m'"
      by (subst power_Suc) (auto simp: mult.assoc [symmetric])
    finally show ?thesis using Suc by simp
  qed auto
qed auto

lemma power_mult_power_inverse_commute:
  "x ^ m * inverse (x :: 'a) ^ n = inverse x ^ n * x ^ m"
proof (induction n)
  case (Suc n)
  have "x ^ m * inverse x ^ Suc n = (x ^ m * inverse x ^ n) * inverse x"
    by (simp only: power_Suc2 mult.assoc)
  also have "x ^ m * inverse x ^ n = inverse x ^ n * x ^ m"
    by (rule Suc)
  also have "\ * inverse x = (inverse x ^ n * inverse x) * x ^ m"
    by (simp add: mult.assoc power_mult_inverse_distrib)
  also have "\ = inverse x ^ (Suc n) * x ^ m"
    by (simp only: power_Suc2)
  finally show ?case .
qed auto

lemma power_int_add:
  assumes "x \ 0 \ m + n \ 0"
  shows   "power_int (x::'a) (m + n) = power_int x m * power_int x n"
proof (cases "x = 0")
  case True
  thus ?thesis using assms by (auto simp: power_int_0_left_if)
next
  case [simp]: False
  show ?thesis
  proof (cases m n rule: int_cases4[case_product int_cases4])
    case (nonneg_nonneg a b)
    thus ?thesis
      by (auto simp: power_int_def nat_add_distrib power_add)
  next
    case (nonneg_neg a b)
    thus ?thesis
      by (auto simp: power_int_def nat_diff_distrib not_le power_diff_conv_inverse
                     power_mult_power_inverse_commute)
  next
    case (neg_nonneg a b)
    thus ?thesis
      by (auto simp: power_int_def nat_diff_distrib not_le power_diff_conv_inverse
                     power_mult_power_inverse_commute)
  next
    case (neg_neg a b)
    thus ?thesis
      by (auto simp: power_int_def nat_add_distrib add.commute simp flip: power_add)
  qed
qed

lemma power_int_add_1:
  assumes "x \ 0 \ m \ -1"
  shows   "power_int (x::'a) (m + 1) = power_int x m * x"
  using assms by (subst power_int_add) auto

lemma power_int_add_1':
  assumes "x \ 0 \ m \ -1"
  shows   "power_int (x::'a) (m + 1) = x * power_int x m"
  using assms by (subst add.commute, subst power_int_add) auto

lemma power_int_commutes: "power_int (x :: 'a) n * x = x * power_int x n"
  by (cases "x = 0") (auto simp flip: power_int_add_1 power_int_add_1')

lemma power_int_inverse [field_simps, field_split_simps, divide_simps]:
  "power_int (inverse (x :: 'a)) n = inverse (power_int x n)"
  by (auto simp: power_int_def power_inverse)

lemma power_int_mult: "power_int (x :: 'a) (m * n) = power_int (power_int x m) n"
  by (auto simp: power_int_def zero_le_mult_iff simp flip: power_mult power_inverse nat_mult_distrib)

lemma power_int_power: "(a ^ b :: 'a :: division_ring) powi c = a powi (int b * c)"
  by (subst power_int_mult) simp

lemma power_int_power': "(a powi b :: 'a :: division_ring) ^ c = a powi (b * int c)"
  by (simp add: power_int_mult)

lemma power_int_nonneg_exp: "n \ 0 \ x powi n = x ^ nat n"
  by (simp add: power_int_def)

end

context
  assumes "SORT_CONSTRAINT('a::field)"
begin

lemma power_int_diff:
  assumes "x \ 0 \ m \ n"
  shows   "power_int (x::'a) (m - n) = power_int x m / power_int x n"
  using power_int_add[of x m "-n"] assms by (auto simp: field_simps power_int_minus)

lemma power_int_minus_mult: "x \ 0 \ n \ 0 \ power_int (x :: 'a) (n - 1) * x = power_int x n"
  by (auto simp flip: power_int_add_1)

lemma power_int_mult_distrib: "power_int (x * y :: 'a) m = power_int x m * power_int y m"
  by (auto simp: power_int_def power_mult_distrib)

lemmas power_int_mult_distrib_numeral1 = power_int_mult_distrib [where x = "numeral w" for w, simp]
lemmas power_int_mult_distrib_numeral2 = power_int_mult_distrib [where y = "numeral w" for w, simp]

lemma power_int_divide_distrib: "power_int (x / y :: 'a) m = power_int x m / power_int y m"
  using power_int_mult_distrib[of x "inverse y" m] unfolding power_int_inverse
  by (simp add: field_simps)

end

lemma power_int_add_numeral [simp]:
  "power_int x (numeral m) * power_int x (numeral n) = power_int x (numeral (m + n))"
  for x :: "'a :: division_ring"
  by (simp add: power_int_add [symmetric])

lemma power_int_add_numeral2 [simp]:
  "power_int x (numeral m) * (power_int x (numeral n) * b) = power_int x (numeral (m + n)) * b"
  for x :: "'a :: division_ring"
  by (simp add: mult.assoc [symmetric])

lemma power_int_mult_numeral [simp]:
  "power_int (power_int x (numeral m)) (numeral n) = power_int x (numeral (m * n))"
  for x :: "'a :: division_ring"
  by (simp only: numeral_mult power_int_mult)

--> --------------------

--> maximum size reached

--> --------------------

quality99%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.24Bemerkung: (vorverarbeitet) ¤

*© Formatika GbR, Deutschland

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.