Quelle Nat.thy Sprache: Isabelle

(*  Title:      HOL/Nat.thy
    Author:     Tobias Nipkow
    Author:     Lawrence C Paulson
    Author:     Markus Wenzel
*)

section \<open>Natural numbers\<close>

theory Nat
imports Inductive Typedef Fun Rings
begin

subsection \<open>Type \<open>ind\<close>\<close>

typedecl ind

axiomatization Zero_Rep :: ind and Suc_Rep :: "ind \ ind"
  \<comment> \<open>The axiom of infinity in 2 parts:\<close>
  where Suc_Rep_inject: "Suc_Rep x = Suc_Rep y \ x = y"
    and Suc_Rep_not_Zero_Rep: "Suc_Rep x \ Zero_Rep"

subsection \<open>Type nat\<close>

text \<open>Type definition\<close>

inductive Nat :: "ind \ bool"
  where
    Zero_RepI: "Nat Zero_Rep"
  | Suc_RepI: "Nat i \ Nat (Suc_Rep i)"

typedef nat = "{n. Nat n}"
  morphisms Rep_Nat Abs_Nat
  using Nat.Zero_RepI by auto

lemma Nat_Rep_Nat: "Nat (Rep_Nat n)"
  using Rep_Nat by simp

lemma Nat_Abs_Nat_inverse: "Nat n \ Rep_Nat (Abs_Nat n) = n"
  using Abs_Nat_inverse by simp

lemma Nat_Abs_Nat_inject: "Nat n \ Nat m \ Abs_Nat n = Abs_Nat m \ n = m"
  using Abs_Nat_inject by simp

instantiation nat :: zero
begin

definition Zero_nat_def: "0 = Abs_Nat Zero_Rep"

instance ..

end

definition Suc :: "nat \ nat"
  where "Suc n = Abs_Nat (Suc_Rep (Rep_Nat n))"

lemma Suc_not_Zero: "Suc m \ 0"
  by (simp add: Zero_nat_def Suc_def Suc_RepI Zero_RepI
      Nat_Abs_Nat_inject Suc_Rep_not_Zero_Rep Nat_Rep_Nat)

lemma Zero_not_Suc: "0 \ Suc m"
  by (rule not_sym) (rule Suc_not_Zero)

lemma Suc_Rep_inject': "Suc_Rep x = Suc_Rep y \ x = y"
  by (rule iffI, rule Suc_Rep_inject) simp_all

lemma nat_induct0:
  assumes "P 0" and "\n. P n \ P (Suc n)"
  shows "P n"
proof -
  have "P (Abs_Nat (Rep_Nat n))"
    using assms unfolding Zero_nat_def Suc_def
    by (iprover intro:  Nat_Rep_Nat [THEN Nat.induct] elim: Nat_Abs_Nat_inverse [THEN subst])
  then show ?thesis
    by (simp add: Rep_Nat_inverse)
qed

free_constructors case_nat for "0 :: nat" | Suc pred
  where "pred (0 :: nat) = (0 :: nat)"
proof atomize_elim
  fix n
  show "n = 0 \ (\m. n = Suc m)"
    by (induction n rule: nat_induct0) auto
next
  fix n m
  show "(Suc n = Suc m) = (n = m)"
    by (simp add: Suc_def Nat_Abs_Nat_inject Nat_Rep_Nat Suc_RepI Suc_Rep_inject' Rep_Nat_inject)
next
  fix n
  show "0 \ Suc n"
    by (simp add: Suc_not_Zero)
qed

\<comment> \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
setup \<open>Sign.mandatory_path "old"\<close>

old_rep_datatype "0 :: nat" Suc
  by (erule nat_induct0) auto

setup \<open>Sign.parent_path\<close>

\<comment> \<open>But erase the prefix for properties that are not generated by \<open>free_constructors\<close>.\<close>
setup \<open>Sign.mandatory_path "nat"\<close>

declare old.nat.inject[iff del]
  and old.nat.distinct(1)[simp del, induct_simp del]

lemmas induct = old.nat.induct
lemmas inducts = old.nat.inducts
lemmas rec = old.nat.rec
lemmas simps = nat.inject nat.distinct nat.case nat.rec

setup \<open>Sign.parent_path\<close>

abbreviation rec_nat :: "'a \ (nat \ 'a \ 'a) \ nat \ 'a"
  where "rec_nat \ old.rec_nat"

declare nat.sel[code del]

hide_const (open) Nat.pred \<comment> \<open>hide everything related to the selector\<close>

lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
  "(y = 0 \ P) \ (\nat. y = Suc nat \ P) \ P"
  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
  by (rule old.nat.exhaust)

lemma nat_induct [case_names 0 Suc, induct type: nat]:
  fixes n
  assumes "P 0" and "\n. P n \ P (Suc n)"
  shows "P n"
  \<comment> \<open>for backward compatibility -- names of variables differ\<close>
  using assms by (rule nat.induct)

hide_fact
  nat_exhaust
  nat_induct0

ML \<open>
val nat_basic_lfp_sugar =
  let
    val ctr_sugar = the (Ctr_Sugar.ctr_sugar_of_global \<^theory> \<^type_name>\<open>nat\<close>);
    val recx = Logic.varify_types_global \<^term>\<open>rec_nat\<close>;
    val C = body_type (fastype_of recx);
  in
    {T = HOLogic.natT, fp_res_index = 0, C = C, fun_arg_Tsss = [[], [[HOLogic.natT, C]]],
     ctr_sugar = ctr_sugar, recx = recx, rec_thms = @{thms nat.rec}}
  end;
\<close>

setup \<open>
let
  fun basic_lfp_sugars_of _ [\<^typ>\<open>nat\<close>] _ _ ctxt =
      ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, ctxt)
    | basic_lfp_sugars_of bs arg_Ts callers callssss ctxt =
      BNF_LFP_Rec_Sugar.default_basic_lfp_sugars_of bs arg_Ts callers callssss ctxt;
in
  BNF_LFP_Rec_Sugar.register_lfp_rec_extension
    {nested_simps = [], special_endgame_tac = K (K (K (K no_tac))), is_new_datatype = K (K true),
     basic_lfp_sugars_of = basic_lfp_sugars_of, rewrite_nested_rec_call = NONE}
end
\<close>

text \<open>Injectiveness and distinctness lemmas\<close>

lemma inj_Suc [simp]:
  "inj_on Suc N"
  by (simp add: inj_on_def)

lemma bij_betw_Suc [simp]:
  "bij_betw Suc M N \ Suc ` M = N"
  by (simp add: bij_betw_def)

lemma Suc_neq_Zero: "Suc m = 0 \ R"
  by (rule notE) (rule Suc_not_Zero)

lemma Zero_neq_Suc: "0 = Suc m \ R"
  by (rule Suc_neq_Zero) (erule sym)

lemma Suc_inject: "Suc x = Suc y \ x = y"
  by (rule inj_Suc [THEN injD])

lemma n_not_Suc_n: "n \ Suc n"
  by (induct n) simp_all

lemma Suc_n_not_n: "Suc n \ n"
  by (rule not_sym) (rule n_not_Suc_n)

text \<open>A special form of induction for reasoning about \<^term>\<open>m < n\<close> and \<^term>\<open>m - n\<close>.\<close>
lemma diff_induct:
  assumes "\x. P x 0"
    and "\y. P 0 (Suc y)"
    and "\x y. P x y \ P (Suc x) (Suc y)"
  shows "P m n"
proof (induct n arbitrary: m)
  case 0
  show ?case by (rule assms(1))
next
  case (Suc n)
  show ?case
  proof (induct m)
    case 0
    show ?case by (rule assms(2))
  next
    case (Suc m)
    from \<open>P m n\<close> show ?case by (rule assms(3))
  qed
qed

subsection \<open>Arithmetic operators\<close>

instantiation nat :: comm_monoid_diff
begin

primrec plus_nat
  where
    add_0 [code]: "0 + n = (n::nat)"
  | add_Suc: "Suc m + n = Suc (m + n)"

lemma add_0_right [simp]: "m + 0 = m"
  for m :: nat
  by (induct m) simp_all

lemma add_Suc_right [simp]: "m + Suc n = Suc (m + n)"
  by (induct m) simp_all

lemma add_Suc_shift [code]: "Suc m + n = m + Suc n"
  by simp

primrec minus_nat
  where
    diff_0 [code]: "m - 0 = (m::nat)"
  | diff_Suc: "m - Suc n = (case m - n of 0 \ 0 | Suc k \ k)"

declare diff_Suc [simp del]

lemma diff_0_eq_0 [simp, code]: "0 - n = 0"
  for n :: nat
  by (induct n) (simp_all add: diff_Suc)

lemma diff_Suc_Suc [simp, code]: "Suc m - Suc n = m - n"
  by (induct n) (simp_all add: diff_Suc)

instance
proof
  fix n m q :: nat
  show "(n + m) + q = n + (m + q)" by (induct n) simp_all
  show "n + m = m + n" by (induct n) simp_all
  show "m + n - m = n" by (induct m) simp_all
  show "n - m - q = n - (m + q)" by (induct q) (simp_all add: diff_Suc)
  show "0 + n = n" by simp
  show "0 - n = 0" by simp
qed

end

hide_fact (open) add_0 add_0_right diff_0

instantiation nat :: comm_semiring_1_cancel
begin

definition One_nat_def [simp]: "1 = Suc 0"

primrec times_nat
  where
    mult_0: "0 * n = (0::nat)"
  | mult_Suc: "Suc m * n = n + (m * n)"

lemma mult_0_right [simp]: "m * 0 = 0"
  for m :: nat
  by (induct m) simp_all

lemma mult_Suc_right [simp]: "m * Suc n = m + (m * n)"
  by (induct m) (simp_all add: add.left_commute)

lemma add_mult_distrib: "(m + n) * k = (m * k) + (n * k)"
  for m n k :: nat
  by (induct m) (simp_all add: add.assoc)

instance
proof
  fix k n m q :: nat
  show "0 \ (1::nat)"
    by simp
  show "1 * n = n"
    by simp
  show "n * m = m * n"
    by (induct n) simp_all
  show "(n * m) * q = n * (m * q)"
    by (induct n) (simp_all add: add_mult_distrib)
  show "(n + m) * q = n * q + m * q"
    by (rule add_mult_distrib)
  show "k * (m - n) = (k * m) - (k * n)"
    by (induct m n rule: diff_induct) simp_all
qed

end

subsubsection \<open>Addition\<close>

text \<open>Reasoning about \<open>m + 0 = 0\<close>, etc.\<close>

lemma add_is_0 [iff]: "m + n = 0 \ m = 0 \ n = 0"
  for m n :: nat
  by (cases m) simp_all

lemma add_is_1: "m + n = Suc 0 \ m = Suc 0 \ n = 0 \ m = 0 \ n = Suc 0"
  by (cases m) simp_all

lemma one_is_add: "Suc 0 = m + n \ m = Suc 0 \ n = 0 \ m = 0 \ n = Suc 0"
  by (rule trans, rule eq_commute, rule add_is_1)

lemma add_eq_self_zero: "m + n = m \ n = 0"
  for m n :: nat
  by (induct m) simp_all

lemma plus_1_eq_Suc:
  "plus 1 = Suc"
  by (simp add: fun_eq_iff)

lemma Suc_eq_plus1: "Suc n = n + 1"
  by simp

lemma Suc_eq_plus1_left: "Suc n = 1 + n"
  by simp

subsubsection \<open>Difference\<close>

lemma Suc_diff_diff [simp]: "(Suc m - n) - Suc k = m - n - k"
  by (simp add: diff_diff_add)

lemma diff_Suc_1: "Suc n - 1 = n"
  by simp

lemma diff_Suc_1' [simp]: "Suc n - Suc 0 = n"
  by simp

subsubsection \<open>Multiplication\<close>

lemma mult_is_0 [simp]: "m * n = 0 \ m = 0 \ n = 0" for m n :: nat
  by (induct m) auto

lemma mult_eq_1_iff [simp]: "m * n = Suc 0 \ m = Suc 0 \ n = Suc 0"
proof (induct m)
  case 0
  then show ?case by simp
next
  case (Suc m)
  then show ?case by (induct n) auto
qed

lemma one_eq_mult_iff [simp]: "Suc 0 = m * n \ m = Suc 0 \ n = Suc 0"
  by (simp add: eq_commute flip: mult_eq_1_iff)

lemma nat_mult_eq_1_iff [simp]: "m * n = 1 \ m = 1 \ n = 1"
  and nat_1_eq_mult_iff [simp]: "1 = m * n \ m = 1 \ n = 1" for m n :: nat
  by auto

lemma mult_cancel1 [simp]: "k * m = k * n \ m = n \ k = 0"
  for k m n :: nat
proof -
  have "k \ 0 \ k * m = k * n \ m = n"
  proof (induct n arbitrary: m)
    case 0
    then show "m = 0" by simp
  next
    case (Suc n)
    then show "m = Suc n"
      by (cases m) (simp_all add: eq_commute [of 0])
  qed
  then show ?thesis by auto
qed

lemma mult_cancel2 [simp]: "m * k = n * k \ m = n \ k = 0"
  for k m n :: nat
  by (simp add: mult.commute)

lemma Suc_mult_cancel1: "Suc k * m = Suc k * n \ m = n"
  by (subst mult_cancel1) simp

subsection \<open>Orders on \<^typ>\<open>nat\<close>\<close>

subsubsection \<open>Operation definition\<close>

instantiation nat :: linorder
begin

primrec less_eq_nat
  where
    "(0::nat) \ n \ True"
  | "Suc m \ n \ (case n of 0 \ False | Suc n \ m \ n)"

declare less_eq_nat.simps [simp del]

lemma le0 [iff]: "0 \ n" for
  n :: nat
  by (simp add: less_eq_nat.simps)

lemma [code]: "0 \ n \ True"
  for n :: nat
  by simp

definition less_nat
  where less_eq_Suc_le: "n < m \ Suc n \ m"

lemma Suc_le_mono [iff]: "Suc n \ Suc m \ n \ m"
  by (simp add: less_eq_nat.simps(2))

lemma Suc_le_eq [code]: "Suc m \ n \ m < n"
  unfolding less_eq_Suc_le ..

lemma le_0_eq [iff]: "n \ 0 \ n = 0"
  for n :: nat
  by (induct n) (simp_all add: less_eq_nat.simps(2))

lemma not_less0 [iff]: "\ n < 0"
  for n :: nat
  by (simp add: less_eq_Suc_le)

lemma less_nat_zero_code [code]: "n < 0 \ False"
  for n :: nat
  by simp

lemma Suc_less_eq [iff]: "Suc m < Suc n \ m < n"
  by (simp add: less_eq_Suc_le)

lemma less_Suc_eq_le [code]: "m < Suc n \ m \ n"
  by (simp add: less_eq_Suc_le)

lemma Suc_less_eq2: "Suc n < m \ (\m'. m = Suc m' \ n < m')"
  by (cases m) auto

lemma le_SucI: "m \ n \ m \ Suc n"
  by (induct m arbitrary: n) (simp_all add: less_eq_nat.simps(2) split: nat.splits)

lemma Suc_leD: "Suc m \ n \ m \ n"
  by (cases n) (auto intro: le_SucI)

lemma less_SucI: "m < n \ m < Suc n"
  by (simp add: less_eq_Suc_le) (erule Suc_leD)

lemma Suc_lessD: "Suc m < n \ m < n"
  by (simp add: less_eq_Suc_le) (erule Suc_leD)

instance
proof
  fix n m q :: nat
  show "n < m \ n \ m \ \ m \ n"
  proof (induct n arbitrary: m)
    case 0
    then show ?case
      by (cases m) (simp_all add: less_eq_Suc_le)
  next
    case (Suc n)
    then show ?case
      by (cases m) (simp_all add: less_eq_Suc_le)
  qed
  show "n \ n"
    by (induct n) simp_all
  then show "n = m" if "n \ m" and "m \ n"
    using that by (induct n arbitrary: m)
      (simp_all add: less_eq_nat.simps(2) split: nat.splits)
  show "n \ q" if "n \ m" and "m \ q"
    using that
  proof (induct n arbitrary: m q)
    case 0
    show ?case by simp
  next
    case (Suc n)
    then show ?case
      by (simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
        simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits, clarify,
        simp_all (no_asm_use) add: less_eq_nat.simps(2) split: nat.splits)
  qed
  show "n \ m \ m \ n"
    by (induct n arbitrary: m)
      (simp_all add: less_eq_nat.simps(2) split: nat.splits)
qed

end

instantiation nat :: order_bot
begin

definition bot_nat :: nat
  where "bot_nat = 0"

instance
  by standard (simp add: bot_nat_def)

end

instance nat :: no_top
  by standard (auto intro: less_Suc_eq_le [THEN iffD2])

subsubsection \<open>Introduction properties\<close>

lemma lessI [iff]: "n < Suc n"
  by (simp add: less_Suc_eq_le)

lemma zero_less_Suc [iff]: "0 < Suc n"
  by (simp add: less_Suc_eq_le)

subsubsection \<open>Elimination properties\<close>

lemma less_not_refl: "\ n < n"
  for n :: nat
  by (rule order_less_irrefl)

lemma less_not_refl2: "n < m \ m \ n"
  for m n :: nat
  by (rule not_sym) (rule less_imp_neq)

lemma less_not_refl3: "s < t \ s \ t"
  for s t :: nat
  by (rule less_imp_neq)

lemma less_irrefl_nat: "n < n \ R"
  for n :: nat
  by (rule notE, rule less_not_refl)

lemma less_zeroE: "n < 0 \ R"
  for n :: nat
  by (rule notE) (rule not_less0)

lemma less_Suc_eq: "m < Suc n \ m < n \ m = n"
  unfolding less_Suc_eq_le le_less ..

lemma less_Suc0 [iff]: "(n < Suc 0) = (n = 0)"
  by (simp add: less_Suc_eq)

lemma less_one [iff]: "n < 1 \ n = 0"
  for n :: nat
  unfolding One_nat_def by (rule less_Suc0)

lemma Suc_mono: "m < n \ Suc m < Suc n"
  by simp

text \<open>"Less than" is antisymmetric, sort of.\<close>
lemma less_antisym: "\ n < m \ n < Suc m \ m = n"
  unfolding not_less less_Suc_eq_le by (rule antisym)

lemma nat_neq_iff: "m \ n \ m < n \ n < m"
  for m n :: nat
  by (rule linorder_neq_iff)

subsubsection \<open>Inductive (?) properties\<close>

lemma Suc_lessI: "m < n \ Suc m \ n \ Suc m < n"
  unfolding less_eq_Suc_le [of m] le_less by simp

lemma lessE:
  assumes major: "i < k"
    and 1: "k = Suc i \ P"
    and 2: "\j. i < j \ k = Suc j \ P"
  shows P
proof -
  from major have "\j. i \ j \ k = Suc j"
    unfolding less_eq_Suc_le by (induct k) simp_all
  then have "(\j. i < j \ k = Suc j) \ k = Suc i"
    by (auto simp add: less_le)
  with 1 2 show P by auto
qed

lemma less_SucE:
  assumes major: "m < Suc n"
    and less: "m < n \ P"
    and eq: "m = n \ P"
  shows P
proof (rule major [THEN lessE])
  show "Suc n = Suc m \ P"
    using eq by blast
  show "\j. \m < j; Suc n = Suc j\ \ P"
    by (blast intro: less)
qed

lemma Suc_lessE:
  assumes major: "Suc i < k"
    and minor: "\j. i < j \ k = Suc j \ P"
  shows P
proof (rule major [THEN lessE])
  show "k = Suc (Suc i) \ P"
    using lessI minor by iprover
  show "\j. \Suc i < j; k = Suc j\ \ P"
    using Suc_lessD minor by iprover
qed

lemma Suc_less_SucD: "Suc m < Suc n \ m < n"
  by simp

lemma less_trans_Suc:
  assumes le: "i < j"
  shows "j < k \ Suc i < k"
proof (induct k)
  case 0
  then show ?case by simp
next
  case (Suc k)
  with le show ?case
    by simp (auto simp add: less_Suc_eq dest: Suc_lessD)
qed

text \<open>Can be used with \<open>less_Suc_eq\<close> to get \<^prop>\<open>n = m \<or> n < m\<close>.\<close>
lemma not_less_eq: "\ m < n \ n < Suc m"
  by (simp only: not_less less_Suc_eq_le)

lemma not_less_eq_eq: "\ m \ n \ Suc n \ m"
  by (simp only: not_le Suc_le_eq)

text \<open>Properties of "less than or equal".\<close>

lemma le_imp_less_Suc: "m \ n \ m < Suc n"
  by (simp only: less_Suc_eq_le)

lemma Suc_n_not_le_n: "\ Suc n \ n"
  by (simp add: not_le less_Suc_eq_le)

lemma le_Suc_eq: "m \ Suc n \ m \ n \ m = Suc n"
  by (simp add: less_Suc_eq_le [symmetric] less_Suc_eq)

lemma le_SucE: "m \ Suc n \ (m \ n \ R) \ (m = Suc n \ R) \ R"
  by (drule le_Suc_eq [THEN iffD1], iprover+)

lemma Suc_leI: "m < n \ Suc m \ n"
  by (simp only: Suc_le_eq)

text \<open>Stronger version of \<open>Suc_leD\<close>.\<close>
lemma Suc_le_lessD: "Suc m \ n \ m < n"
  by (simp only: Suc_le_eq)

lemma less_imp_le_nat: "m < n \ m \ n" for m n :: nat
  unfolding less_eq_Suc_le by (rule Suc_leD)

text \<open>For instance, \<open>(Suc m < Suc n) = (Suc m \<le> n) = (m < n)\<close>\<close>
lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq

text \<open>Equivalence of \<open>m \<le> n\<close> and \<open>m < n \<or> m = n\<close>\<close>

lemma less_or_eq_imp_le: "m < n \ m = n \ m \ n"
  for m n :: nat
  unfolding le_less .

lemma le_eq_less_or_eq: "m \ n \ m < n \ m = n"
  for m n :: nat
  by (rule le_less)

text \<open>Useful with \<open>blast\<close>.\<close>
lemma eq_imp_le: "m = n \ m \ n"
  for m n :: nat
  by auto

lemma le_refl: "n \ n"
  for n :: nat
  by simp

lemma le_trans: "i \ j \ j \ k \ i \ k"
  for i j k :: nat
  by (rule order_trans)

lemma le_antisym: "m \ n \ n \ m \ m = n"
  for m n :: nat
  by (rule antisym)

lemma nat_less_le: "m < n \ m \ n \ m \ n"
  for m n :: nat
  by (rule less_le)

lemma le_neq_implies_less: "m \ n \ m \ n \ m < n"
  for m n :: nat
  unfolding less_le ..

lemma nat_le_linear: "m \ n \ n \ m"
  for m n :: nat
  by (rule linear)

lemmas linorder_neqE_nat = linorder_neqE [where 'a = nat]

lemma le_less_Suc_eq: "m \ n \ n < Suc m \ n = m"
  unfolding less_Suc_eq_le by auto

lemma not_less_less_Suc_eq: "\ n < m \ n < Suc m \ n = m"
  unfolding not_less by (rule le_less_Suc_eq)

lemmas not_less_simps = not_less_less_Suc_eq le_less_Suc_eq

lemma not0_implies_Suc: "n \ 0 \ \m. n = Suc m"
  by (cases n) simp_all

lemma gr0_implies_Suc: "n > 0 \ \m. n = Suc m"
  by (cases n) simp_all

lemma gr_implies_not0: "m < n \ n \ 0"
  for m n :: nat
  by (cases n) simp_all

lemma neq0_conv[iff]: "n \ 0 \ 0 < n"
  for n :: nat
  by (cases n) simp_all

text \<open>This theorem is useful with \<open>blast\<close>\<close>
lemma gr0I: "(n = 0 \ False) \ 0 < n"
  for n :: nat
  by (rule neq0_conv[THEN iffD1]) iprover

lemma gr0_conv_Suc: "0 < n \ (\m. n = Suc m)"
  by (fast intro: not0_implies_Suc)

lemma not_gr0 [iff]: "\ 0 < n \ n = 0"
  for n :: nat
  using neq0_conv by blast

lemma Suc_le_D: "Suc n \ m' \ \m. m' = Suc m"
  by (induct m') simp_all

text \<open>Useful in certain inductive arguments\<close>
lemma less_Suc_eq_0_disj: "m < Suc n \ m = 0 \ (\j. m = Suc j \ j < n)"
  by (cases m) simp_all

lemma All_less_Suc: "(\i < Suc n. P i) = (P n \ (\i < n. P i))"
  by (auto simp: less_Suc_eq)

lemma All_less_Suc2: "(\i < Suc n. P i) = (P 0 \ (\i < n. P(Suc i)))"
  by (auto simp: less_Suc_eq_0_disj)

lemma Ex_less_Suc: "(\i < Suc n. P i) = (P n \ (\i < n. P i))"
  by (auto simp: less_Suc_eq)

lemma Ex_less_Suc2: "(\i < Suc n. P i) = (P 0 \ (\i < n. P(Suc i)))"
  by (auto simp: less_Suc_eq_0_disj)

text \<open>@{term mono} (non-strict) doesn't imply increasing, as the function could be constant\<close>
lemma strict_mono_imp_increasing:
  fixes n::nat
  assumes "strict_mono f" shows "f n \ n"
proof (induction n)
  case 0
  then show ?case
    by auto
next
  case (Suc n)
  then show ?case
    unfolding not_less_eq_eq [symmetric]
    using Suc_n_not_le_n assms order_trans strict_mono_less_eq by blast
qed

subsubsection \<open>Monotonicity of Addition\<close>

lemma Suc_pred [simp]: "n > 0 \ Suc (n - Suc 0) = n"
  by (simp add: diff_Suc split: nat.split)

lemma Suc_diff_1 [simp]: "0 < n \ Suc (n - 1) = n"
  unfolding One_nat_def by (rule Suc_pred)

lemma nat_add_left_cancel_le [simp]: "k + m \ k + n \ m \ n"
  for k m n :: nat
  by (induct k) simp_all

lemma nat_add_left_cancel_less [simp]: "k + m < k + n \ m < n"
  for k m n :: nat
  by (induct k) simp_all

lemma add_gr_0 [iff]: "m + n > 0 \ m > 0 \ n > 0"
  for m n :: nat
  by (auto dest: gr0_implies_Suc)

text \<open>strict, in 1st argument\<close>
lemma add_less_mono1: "i < j \ i + k < j + k"
  for i j k :: nat
  by (induct k) simp_all

text \<open>strict, in both arguments\<close>
lemma add_less_mono:
  fixes i j k l :: nat
  assumes "i < j" "k < l" shows "i + k < j + l"
proof -
  have "i + k < j + k"
    by (simp add: add_less_mono1 assms)
  also have "... < j + l"
    using \<open>i < j\<close> by (induction j) (auto simp: assms)
  finally show ?thesis .
qed

lemma less_imp_Suc_add: "m < n \ \k. n = Suc (m + k)"
proof (induct n)
  case 0
  then show ?case by simp
next
  case Suc
  then show ?case
    by (simp add: order_le_less)
      (blast elim!: less_SucE intro!: Nat.add_0_right [symmetric] add_Suc_right [symmetric])
qed

lemma le_Suc_ex: "k \ l \ (\n. l = k + n)"
  for k l :: nat
  by (auto simp: less_Suc_eq_le[symmetric] dest: less_imp_Suc_add)

lemma less_natE:
  assumes \<open>m < n\<close>
  obtains q where \<open>n = Suc (m + q)\<close>
  using assms by (auto dest: less_imp_Suc_add intro: that)

text \<open>strict, in 1st argument; proof is by induction on \<open>k > 0\<close>\<close>
lemma mult_less_mono2:
  fixes i j :: nat
  assumes "i < j" and "0 < k"
  shows "k * i < k * j"
  using \<open>0 < k\<close>
proof (induct k)
  case 0
  then show ?case by simp
next
  case (Suc k)
  with \<open>i < j\<close> show ?case
    by (cases k) (simp_all add: add_less_mono)
qed

text \<open>Addition is the inverse of subtraction:
  if \<^term>\<open>n \<le> m\<close> then \<^term>\<open>n + (m - n) = m\<close>.\<close>
lemma add_diff_inverse_nat: "\ m < n \ n + (m - n) = m"
  for m n :: nat
  by (induct m n rule: diff_induct) simp_all

lemma nat_le_iff_add: "m \ n \ (\k. n = m + k)"
  for m n :: nat
  using nat_add_left_cancel_le[of m 0] by (auto dest: le_Suc_ex)

text \<open>The naturals form an ordered \<open>semidom\<close> and a \<open>dioid\<close>.\<close>

instance nat :: discrete_linordered_semidom
proof
  fix m n q :: nat
  show \<open>0 < (1::nat)\<close>
    by simp
  show \<open>m \<le> n \<Longrightarrow> q + m \<le> q + n\<close>
    by simp
  show \<open>m < n \<Longrightarrow> 0 < q \<Longrightarrow> q * m < q * n\<close>
    by (simp add: mult_less_mono2)
  show \<open>m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> m * n \<noteq> 0\<close>
    by simp
  show \<open>n \<le> m \<Longrightarrow> (m - n) + n = m\<close>
    by (simp add: add_diff_inverse_nat add.commute linorder_not_less)
  show \<open>m < n \<longleftrightarrow> m + 1 \<le> n\<close>
    by (simp add: Suc_le_eq)
qed

instance nat :: dioid
  by standard (rule nat_le_iff_add)

declare le0[simp del] \<comment> \<open>This is now @{thm zero_le}\<close>
declare le_0_eq[simp del] \<comment> \<open>This is now @{thm le_zero_eq}\<close>
declare not_less0[simp del] \<comment> \<open>This is now @{thm not_less_zero}\<close>
declare not_gr0[simp del] \<comment> \<open>This is now @{thm not_gr_zero}\<close>

instance nat :: ordered_cancel_comm_monoid_add ..
instance nat :: ordered_cancel_comm_monoid_diff ..

subsubsection \<open>\<^term>\<open>min\<close> and \<^term>\<open>max\<close>\<close>

global_interpretation bot_nat_0: ordering_top \<open>(\<ge>)\<close> \<open>(>)\<close> \<open>0::nat\<close>
  by standard simp

global_interpretation max_nat: semilattice_neutr_order max \<open>0::nat\<close> \<open>(\<ge>)\<close> \<open>(>)\<close>
  by standard (simp add: max_def)

lemma mono_Suc: "mono Suc"
  by (rule monoI) simp

lemma min_0L [simp]: "min 0 n = 0"
  for n :: nat
  by (rule min_absorb1) simp

lemma min_0R [simp]: "min n 0 = 0"
  for n :: nat
  by (rule min_absorb2) simp

lemma min_Suc_Suc [simp]: "min (Suc m) (Suc n) = Suc (min m n)"
  by (simp add: mono_Suc min_of_mono)

lemma min_Suc1: "min (Suc n) m = (case m of 0 \ 0 | Suc m' \ Suc(min n m'))"
  by (simp split: nat.split)

lemma min_Suc2: "min m (Suc n) = (case m of 0 \ 0 | Suc m' \ Suc(min m' n))"
  by (simp split: nat.split)

lemma max_0L [simp]: "max 0 n = n"
  for n :: nat
  by (fact max_nat.left_neutral)

lemma max_0R [simp]: "max n 0 = n"
  for n :: nat
  by (fact max_nat.right_neutral)

lemma max_Suc_Suc [simp]: "max (Suc m) (Suc n) = Suc (max m n)"
  by (simp add: mono_Suc max_of_mono)

lemma max_Suc1: "max (Suc n) m = (case m of 0 \ Suc n | Suc m' \ Suc (max n m'))"
  by (simp split: nat.split)

lemma max_Suc2: "max m (Suc n) = (case m of 0 \ Suc n | Suc m' \ Suc (max m' n))"
  by (simp split: nat.split)

lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
  for m n q :: nat
  by (simp add: min_def not_le)
    (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)

lemma nat_mult_min_right: "m * min n q = min (m * n) (m * q)"
  for m n q :: nat
  by (simp add: min_def not_le)
    (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)

lemma nat_add_max_left: "max m n + q = max (m + q) (n + q)"
  for m n q :: nat
  by (simp add: max_def)

lemma nat_add_max_right: "m + max n q = max (m + n) (m + q)"
  for m n q :: nat
  by (simp add: max_def)

lemma nat_mult_max_left: "max m n * q = max (m * q) (n * q)"
  for m n q :: nat
  by (simp add: max_def not_le)
    (auto dest: mult_right_le_imp_le mult_right_less_imp_less le_less_trans)

lemma nat_mult_max_right: "m * max n q = max (m * n) (m * q)"
  for m n q :: nat
  by (simp add: max_def not_le)
    (auto dest: mult_left_le_imp_le mult_left_less_imp_less le_less_trans)

subsubsection \<open>Additional theorems about \<^term>\<open>(\<le>)\<close>\<close>

text \<open>Complete induction, aka course-of-values induction\<close>

instance nat :: wellorder
proof
  fix P and n :: nat
  assume step: "(\m. m < n \ P m) \ P n" for n :: nat
  have "\q. q \ n \ P q"
  proof (induct n)
    case (0 n)
    have "P 0" by (rule step) auto
    with 0 show ?case by auto
  next
    case (Suc m n)
    then have "n \ m \ n = Suc m"
      by (simp add: le_Suc_eq)
    then show ?case
    proof
      assume "n \ m"
      then show "P n" by (rule Suc(1))
    next
      assume n: "n = Suc m"
      show "P n" by (rule step) (rule Suc(1), simp add: n le_simps)
    qed
  qed
  then show "P n" by auto
qed

lemma Least_eq_0[simp]: "P 0 \ Least P = 0"
  for P :: "nat \ bool"
  by (rule Least_equality[OF _ le0])

lemma Least_Suc:
  assumes "P n" "\ P 0"
  shows "(LEAST n. P n) = Suc (LEAST m. P (Suc m))"
proof (cases n)
  case (Suc m)
  show ?thesis
  proof (rule antisym)
    show "(LEAST x. P x) \ Suc (LEAST x. P (Suc x))"
      using assms Suc by (force intro: LeastI Least_le)
    have \<section>: "P (LEAST x. P x)"
      by (blast intro: LeastI assms)
    show "Suc (LEAST m. P (Suc m)) \ (LEAST n. P n)"
    proof (cases "(LEAST n. P n)")
      case 0
      then show ?thesis
        using \<section> by (simp add: assms)
    next
      case Suc
      with \<section> show ?thesis
        by (auto simp: Least_le)
    qed
  qed
qed (use assms in auto)

lemma Least_Suc2: "P n \ Q m \ \ P 0 \ \k. P (Suc k) = Q k \ Least P = Suc (Least Q)"
  by (erule (1) Least_Suc [THEN ssubst]) simp

lemma ex_least_nat_le:
  fixes P :: "nat \ bool"
  assumes "P n"
  shows "\k\n. (\i P i) \ P k"
proof (cases n)
  case (Suc m)
  with assms show ?thesis
    by (blast intro: Least_le LeastI_ex dest: not_less_Least)
qed (use assms in auto)

lemma ex_least_nat_less:
  fixes P :: "nat \ bool"
  assumes "P n" "\ P 0"
  shows "\ki\k. \ P i) \ P (Suc k)"
proof (cases n)
  case (Suc m)
  then obtain k where k: "k \ n" "\i P i" "P k"
    using ex_least_nat_le \<open>P n\<close> by blast
  show ?thesis
    by (cases k) (use assms k less_eq_Suc_le in auto)
qed (use assms in auto)

lemma nat_less_induct:
  fixes P :: "nat \ bool"
  assumes "\n. \m. m < n \ P m \ P n"
  shows "P n"
  using assms less_induct by blast

lemma measure_induct_rule [case_names less]:
  fixes f :: "'a \ 'b::wellorder"
  assumes step: "\x. (\y. f y < f x \ P y) \ P x"
  shows "P a"
  by (induct m \<equiv> "f a" arbitrary: a rule: less_induct) (auto intro: step)

text \<open>old style induction rules:\<close>
lemma measure_induct:
  fixes f :: "'a \ 'b::wellorder"
  shows "(\x. \y. f y < f x \ P y \ P x) \ P a"
  by (rule measure_induct_rule [of f P a]) iprover

lemma full_nat_induct:
  assumes step: "\n. (\m. Suc m \ n \ P m) \ P n"
  shows "P n"
  by (rule less_induct) (auto intro: step simp:le_simps)

text\<open>An induction rule for establishing binary relations\<close>
lemma less_Suc_induct [consumes 1]:
  assumes less: "i < j"
    and step: "\i. P i (Suc i)"
    and trans: "\i j k. i < j \ j < k \ P i j \ P j k \ P i k"
  shows "P i j"
proof -
  from less obtain k where j: "j = Suc (i + k)"
    by (auto dest: less_imp_Suc_add)
  have "P i (Suc (i + k))"
  proof (induct k)
    case 0
    show ?case by (simp add: step)
  next
    case (Suc k)
    have "0 + i < Suc k + i" by (rule add_less_mono1) simp
    then have "i < Suc (i + k)" by (simp add: add.commute)
    from trans[OF this lessI Suc step]
    show ?case by simp
  qed
  then show "P i j" by (simp add: j)
qed

text \<open>
  The method of infinite descent, frequently used in number theory.
  Provided by Roelof Oosterhuis.
  \<open>P n\<close> is true for all natural numbers if
  \<^item> case ``0'': given \<open>n = 0\<close> prove \<open>P n\<close>
  \<^item> case ``smaller'': given \<open>n > 0\<close> and \<open>\<not> P n\<close> prove there exists
    a smaller natural number \<open>m\<close> such that \<open>\<not> P m\<close>.
\<close>

lemma infinite_descent: "(\n. \ P n \ \m P m) \ P n" for P :: "nat \ bool"
  \<comment> \<open>compact version without explicit base case\<close>
  by (induct n rule: less_induct) auto

lemma infinite_descent0 [case_names 0 smaller]:
  fixes P :: "nat \ bool"
  assumes "P 0"
    and "\n. n > 0 \ \ P n \ \m. m < n \ \ P m"
  shows "P n"
proof (rule infinite_descent)
  fix n
  show "\ P n \ \m P m"
    using assms by (cases "n > 0") auto
qed

text \<open>
  Infinite descent using a mapping to \<open>nat\<close>:
  \<open>P x\<close> is true for all \<open>x \<in> D\<close> if there exists a \<open>V \<in> D \<Rightarrow> nat\<close> and
  \<^item> case ``0'': given \<open>V x = 0\<close> prove \<open>P x\<close>
  \<^item> ``smaller'': given \<open>V x > 0\<close> and \<open>\<not> P x\<close> prove
  there exists a \<open>y \<in> D\<close> such that \<open>V y < V x\<close> and \<open>\<not> P y\<close>.
\<close>
corollary infinite_descent0_measure [case_names 0 smaller]:
  fixes V :: "'a \ nat"
  assumes 1: "\x. V x = 0 \ P x"
    and 2: "\x. V x > 0 \ \ P x \ \y. V y < V x \ \ P y"
  shows "P x"
proof -
  obtain n where "n = V x" by auto
  moreover have "\x. V x = n \ P x"
  proof (induct n rule: infinite_descent0)
    case 0
    with 1 show "P x" by auto
  next
    case (smaller n)
    then obtain x where *: "V x = n " and "V x > 0 \ \ P x" by auto
    with 2 obtain y where "V y < V x \ \ P y" by auto
    with * obtain m where "m = V y \ m < n \ \ P y" by auto
    then show ?case by auto
  qed
  ultimately show "P x" by auto
qed

text \<open>Again, without explicit base case:\<close>
lemma infinite_descent_measure:
  fixes V :: "'a \ nat"
  assumes "\x. \ P x \ \y. V y < V x \ \ P y"
  shows "P x"
proof -
  from assms obtain n where "n = V x" by auto
  moreover have "\x. V x = n \ P x"
  proof -
    have "\m < V x. \y. V y = m \ \ P y" if "\ P x" for x
      using assms and that by auto
    then show "\x. V x = n \ P x"
      by (induct n rule: infinite_descent, auto)
  qed
  ultimately show "P x" by auto
qed

text \<open>A (clumsy) way of lifting \<open><\<close> monotonicity to \<open>\<le>\<close> monotonicity\<close>
lemma less_mono_imp_le_mono:
  fixes f :: "nat \ nat"
    and i j :: nat
  assumes "\i j::nat. i < j \ f i < f j"
    and "i \ j"
  shows "f i \ f j"
  using assms by (auto simp add: order_le_less)

text \<open>non-strict, in 1st argument\<close>
lemma add_le_mono1: "i \ j \ i + k \ j + k"
  for i j k :: nat
  by (rule add_right_mono)

text \<open>non-strict, in both arguments\<close>
lemma add_le_mono: "i \ j \ k \ l \ i + k \ j + l"
  for i j k l :: nat
  by (rule add_mono)

lemma le_add2: "n \ m + n"
  for m n :: nat
  by simp

lemma le_add1: "n \ n + m"
  for m n :: nat
  by simp

lemma less_add_Suc1: "i < Suc (i + m)"
  by (rule le_less_trans, rule le_add1, rule lessI)

lemma less_add_Suc2: "i < Suc (m + i)"
  by (rule le_less_trans, rule le_add2, rule lessI)

lemma less_iff_Suc_add: "m < n \ (\k. n = Suc (m + k))"
  by (iprover intro!: less_add_Suc1 less_imp_Suc_add)

lemma trans_le_add1: "i \ j \ i \ j + m"
  for i j m :: nat
  by (rule le_trans, assumption, rule le_add1)

lemma trans_le_add2: "i \ j \ i \ m + j"
  for i j m :: nat
  by (rule le_trans, assumption, rule le_add2)

lemma trans_less_add1: "i < j \ i < j + m"
  for i j m :: nat
  by (rule less_le_trans, assumption, rule le_add1)

lemma trans_less_add2: "i < j \ i < m + j"
  for i j m :: nat
  by (rule less_le_trans, assumption, rule le_add2)

lemma add_lessD1: "i + j < k \ i < k"
  for i j k :: nat
  by (rule le_less_trans [of _ "i+j"]) (simp_all add: le_add1)

lemma not_add_less1 [iff]: "\ i + j < i"
  for i j :: nat
  by simp

lemma not_add_less2 [iff]: "\ j + i < i"
  for i j :: nat
  by simp

lemma add_leD1: "m + k \ n \ m \ n"
  for k m n :: nat
  by (rule order_trans [of _ "m + k"]) (simp_all add: le_add1)

lemma add_leD2: "m + k \ n \ k \ n"
  for k m n :: nat
  by (force simp add: add.commute dest: add_leD1)

lemma add_leE: "m + k \ n \ (m \ n \ k \ n \ R) \ R"
  for k m n :: nat
  by (blast dest: add_leD1 add_leD2)

text \<open>needs \<open>\<And>k\<close> for \<open>ac_simps\<close> to work\<close>
lemma less_add_eq_less: "\k. k < l \ m + l = k + n \ m < n"
  for l m n :: nat
  by (force simp del: add_Suc_right simp add: less_iff_Suc_add add_Suc_right [symmetric] ac_simps)

subsubsection \<open>More results about difference\<close>

lemma Suc_diff_le: "n \ m \ Suc m - n = Suc (m - n)"
  by (induct m n rule: diff_induct) simp_all

lemma diff_less_Suc: "m - n < Suc m"
  by (induct m n rule: diff_induct) (auto simp: less_Suc_eq)

lemma diff_le_self [simp]: "m - n \ m"
  for m n :: nat
  by (induct m n rule: diff_induct) (simp_all add: le_SucI)

lemma less_imp_diff_less: "j < k \ j - n < k"
  for j k n :: nat
  by (rule le_less_trans, rule diff_le_self)

lemma diff_Suc_less [simp]: "0 < n \ n - Suc i < n"
  by (cases n) (auto simp add: le_simps)

lemma diff_add_assoc: "k \ j \ (i + j) - k = i + (j - k)"
  for i j k :: nat
  by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc)

lemma add_diff_assoc [simp]: "k \ j \ i + (j - k) = i + j - k"
  for i j k :: nat
  by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc)

lemma diff_add_assoc2: "k \ j \ (j + i) - k = (j - k) + i"
  for i j k :: nat
  by (fact ordered_cancel_comm_monoid_diff_class.diff_add_assoc2)

lemma add_diff_assoc2 [simp]: "k \ j \ j - k + i = j + i - k"
  for i j k :: nat
  by (fact ordered_cancel_comm_monoid_diff_class.add_diff_assoc2)

lemma le_imp_diff_is_add: "i \ j \ (j - i = k) = (j = k + i)"
  for i j k :: nat
  by auto

lemma diff_is_0_eq [simp]: "m - n = 0 \ m \ n"
  for m n :: nat
  by (induct m n rule: diff_induct) simp_all

lemma diff_is_0_eq' [simp]: "m \ n \ m - n = 0"
  for m n :: nat
  by simp

lemma zero_less_diff [simp]: "0 < n - m \ m < n"
  for m n :: nat
  by (induct m n rule: diff_induct) simp_all

lemma less_imp_add_positive:
  assumes "i < j"
  shows "\k::nat. 0 < k \ i + k = j"
proof
  from assms show "0 < j - i \ i + (j - i) = j"
    by (simp add: order_less_imp_le)
qed

text \<open>a nice rewrite for bounded subtraction\<close>
lemma nat_minus_add_max: "n - m + m = max n m"
  for m n :: nat
  by (simp add: max_def not_le order_less_imp_le)

lemma nat_diff_split: "P (a - b) \ (a < b \ P 0) \ (\d. a = b + d \ P d)"
  for a b :: nat
  \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close>\<close>
  by (cases "a < b") (auto simp add: not_less le_less dest!: add_eq_self_zero [OF sym])

lemma nat_diff_split_asm: "P (a - b) \ \ (a < b \ \ P 0 \ (\d. a = b + d \ \ P d))"
  for a b :: nat
  \<comment> \<open>elimination of \<open>-\<close> on \<open>nat\<close> in assumptions\<close>
  by (auto split: nat_diff_split)

lemmas nat_diff_splits = nat_diff_split nat_diff_split_asm

lemma Suc_pred': "0 < n \ n = Suc(n - 1)"
  by simp

lemma add_eq_if: "m + n = (if m = 0 then n else Suc ((m - 1) + n))"
  unfolding One_nat_def by (cases m) simp_all

lemma mult_eq_if: "m * n = (if m = 0 then 0 else n + ((m - 1) * n))"
  for m n :: nat
  by (cases m) simp_all

lemma Suc_diff_eq_diff_pred: "0 < n \ Suc m - n = m - (n - 1)"
  by (cases n) simp_all

lemma diff_Suc_eq_diff_pred: "m - Suc n = (m - 1) - n"
  by (cases m) simp_all

lemma Let_Suc [simp]: "Let (Suc n) f \ f (Suc n)"
  by (fact Let_def)

subsubsection \<open>Monotonicity of multiplication\<close>

lemma mult_le_mono1: "i \ j \ i * k \ j * k"
  for i j k :: nat
  by (simp add: mult_right_mono)

lemma mult_le_mono2: "i \ j \ k * i \ k * j"
  for i j k :: nat
  by (simp add: mult_left_mono)

text \<open>\<open>\<le>\<close> monotonicity, BOTH arguments\<close>
lemma mult_le_mono: "i \ j \ k \ l \ i * k \ j * l"
  for i j k l :: nat
  by (simp add: mult_mono)

lemma mult_less_mono1: "i < j \ 0 < k \ i * k < j * k"
  for i j k :: nat
  by (simp add: mult_strict_right_mono)

text \<open>Differs from the standard \<open>zero_less_mult_iff\<close> in that there are no negative numbers.\<close>
lemma nat_0_less_mult_iff [simp]: "0 < m * n \ 0 < m \ 0 < n"
  for m n :: nat
proof (induct m)
  case 0
  then show ?case by simp
next
  case (Suc m)
  then show ?case by (cases n) simp_all
qed

lemma one_le_mult_iff [simp]: "Suc 0 \ m * n \ Suc 0 \ m \ Suc 0 \ n"
proof (induct m)
  case 0
  then show ?case by simp
next
  case (Suc m)
  then show ?case by (cases n) simp_all
qed

lemma mult_less_cancel2 [simp]: "m * k < n * k \ 0 < k \ m < n"
  for k m n :: nat
proof (intro iffI conjI)
  assume m: "m * k < n * k"
  then show "0 < k"
    by (cases k) auto
  show "m < n"
  proof (cases k)
    case 0
    then show ?thesis
      using m by auto
  next
    case (Suc k')
    then show ?thesis
      using m
      by (simp flip: linorder_not_le) (blast intro: add_mono mult_le_mono1)
  qed
next
  assume "0 < k \ m < n"
  then show "m * k < n * k"
    by (blast intro: mult_less_mono1)
qed

lemma mult_less_cancel1 [simp]: "k * m < k * n \ 0 < k \ m < n"
  for k m n :: nat
  by (simp add: mult.commute [of k])

lemma mult_le_cancel1 [simp]: "k * m \ k * n \ (0 < k \ m \ n)"
  for k m n :: nat
  by (simp add: linorder_not_less [symmetric], auto)

lemma mult_le_cancel2 [simp]: "m * k \ n * k \ (0 < k \ m \ n)"
  for k m n :: nat
  by (simp add: linorder_not_less [symmetric], auto)

lemma Suc_mult_less_cancel1: "Suc k * m < Suc k * n \ m < n"
  by (subst mult_less_cancel1) simp

lemma Suc_mult_le_cancel1: "Suc k * m \ Suc k * n \ m \ n"
  by (subst mult_le_cancel1) simp

lemma le_square: "m \ m * m"
  for m :: nat
  by (cases m) (auto intro: le_add1)

lemma le_cube: "m \ m * (m * m)"
  for m :: nat
  by (cases m) (auto intro: le_add1)

text \<open>Lemma for \<open>gcd\<close>\<close>
lemma mult_eq_self_implies_10:
  fixes m n :: nat
  assumes "m = m * n" shows "n = 1 \ m = 0"
proof (rule disjCI)
  assume "m \ 0"
  show "n = 1"
  proof (cases n "1::nat" rule: linorder_cases)
    case greater
    show ?thesis
      using assms mult_less_mono2 [OF greater, of m] \<open>m \<noteq> 0\<close> by auto
  qed (use assms \<open>m \<noteq> 0\<close> in auto)
qed

lemma mono_times_nat:
  fixes n :: nat
  assumes "n > 0"
  shows "mono (times n)"
proof
  fix m q :: nat
  assume "m \ q"
  with assms show "n * m \ n * q" by simp
qed

text \<open>The lattice order on \<^typ>\<open>nat\<close>.\<close>

instantiation nat :: distrib_lattice
begin

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

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

instance
  by intro_classes
    (auto simp add: inf_nat_def sup_nat_def max_def not_le min_def
      intro: order_less_imp_le antisym elim!: order_trans order_less_trans)

end

subsection \<open>Natural operation of natural numbers on functions\<close>

text \<open>
  We use the same logical constant for the power operations on
  functions and relations, in order to share the same syntax.
\<close>

consts compow :: "nat \ 'a \ 'a"

abbreviation compower :: "'a \ nat \ 'a" (infixr \^^\ 80)
  where "f ^^ n \ compow n f"

notation (latex output)
  compower (\<open>(_\<^bsup>_\<^esup>)\<close> [1000] 1000)

text \<open>\<open>f ^^ n = f \<circ> \<dots> \<circ> f\<close>, the \<open>n\<close>-fold composition of \<open>f\<close>\<close>

overloading
  funpow \<equiv> "compow :: nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)"
begin

primrec funpow :: "nat \ ('a \ 'a) \ 'a \ 'a"
  where
    "funpow 0 f = id"
  | "funpow (Suc n) f = f \ funpow n f"

end

lemma funpow_0 [simp]: "(f ^^ 0) x = x"
  by simp

lemma funpow_Suc_right: "f ^^ Suc n = f ^^ n \ f"
proof (induct n)
  case 0
  then show ?case by simp
next
  fix n
  assume "f ^^ Suc n = f ^^ n \ f"
  then show "f ^^ Suc (Suc n) = f ^^ Suc n \ f"
    by (simp add: o_assoc)
qed

lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right

text \<open>For code generation.\<close>

context
begin

qualified definition funpow :: "nat \ ('a \ 'a) \ 'a \ 'a"
  where funpow_code_def [code_abbrev]: "funpow = compow"

lemma [code]:
  "funpow 0 f = id"
  "funpow (Suc n) f = f \ funpow n f"
  by (simp_all add: funpow_code_def)

end

lemma funpow_add: "f ^^ (m + n) = f ^^ m \ f ^^ n"
  by (induct m) simp_all

lemma funpow_mult: "(f ^^ m) ^^ n = f ^^ (m * n)"
  for f :: "'a \ 'a"
  by (induct n) (simp_all add: funpow_add)

lemma funpow_swap1: "f ((f ^^ n) x) = (f ^^ n) (f x)"
proof -
  have "f ((f ^^ n) x) = (f ^^ (n + 1)) x" by simp
  also have "\ = (f ^^ n \ f ^^ 1) x" by (simp only: funpow_add)
  also have "\ = (f ^^ n) (f x)" by simp
  finally show ?thesis .
qed

lemma comp_funpow: "comp f ^^ n = comp (f ^^ n)"
  for f :: "'a \ 'a"
  by (induct n) simp_all

lemma Suc_funpow[simp]: "Suc ^^ n = ((+) n)"
  by (induct n) simp_all

lemma id_funpow[simp]: "id ^^ n = id"
  by (induct n) simp_all

lemma funpow_mono: "mono f \ A \ B \ (f ^^ n) A \ (f ^^ n) B"
  for f :: "'a \ ('a::order)"
  by (induct n) (auto simp: mono_def)

lemma funpow_mono2:
  assumes "mono f"
    and "i \ j"
    and "x \ y"
    and "x \ f x"
  shows "(f ^^ i) x \ (f ^^ j) y"
  using assms(2,3)
proof (induct j arbitrary: y)
  case 0
  then show ?case by simp
next
  case (Suc j)
  show ?case
  proof(cases "i = Suc j")
    case True
    with assms(1) Suc show ?thesis
      by (simp del: funpow.simps add: funpow_simps_right monoD funpow_mono)
  next
    case False
    with assms(1,4) Suc show ?thesis
      by (simp del: funpow.simps add: funpow_simps_right le_eq_less_or_eq less_Suc_eq_le)
        (simp add: Suc.hyps monoD order_subst1)
  qed
qed

lemma inj_fn[simp]:
  fixes f::"'a \ 'a"
  assumes "inj f"
  shows "inj (f^^n)"
proof (induction n)
  case Suc thus ?case using inj_compose[OF assms Suc.IH] by (simp del: comp_apply)
qed simp

lemma surj_fn[simp]:
  fixes f::"'a \ 'a"
  assumes "surj f"
  shows "surj (f^^n)"
proof (induction n)
  case Suc thus ?case by (simp add: comp_surj[OF Suc.IH assms] del: comp_apply)
qed simp

lemma bij_fn[simp]:
  fixes f::"'a \ 'a"
  assumes "bij f"
  shows "bij (f^^n)"
by (rule bijI[OF inj_fn[OF bij_is_inj[OF assms]] surj_fn[OF bij_is_surj[OF assms]]])

lemma bij_betw_funpow: \<^marker>\<open>contributor \<open>Lars Noschinski\<close>\<close>
  assumes "bij_betw f S S" shows "bij_betw (f ^^ n) S S"
proof (induct n)
  case 0 then show ?case by (auto simp: id_def[symmetric])
next
  case (Suc n)
  then show ?case unfolding funpow.simps using assms by (rule bij_betw_trans)
qed

subsection \<open>Kleene iteration\<close>

lemma Kleene_iter_lpfp:
  fixes f :: "'a::order_bot \ 'a"
  assumes "mono f"
    and "f p \ p"
  shows "(f ^^ k) bot \ p"
proof (induct k)
  case 0
  show ?case by simp
next
  case Suc
  show ?case
    using monoD[OF assms(1) Suc] assms(2) by simp
qed

lemma lfp_Kleene_iter:
  assumes "mono f"
    and "(f ^^ Suc k) bot = (f ^^ k) bot"
  shows "lfp f = (f ^^ k) bot"
proof (rule antisym)
  show "lfp f \ (f ^^ k) bot"
  proof (rule lfp_lowerbound)
    show "f ((f ^^ k) bot) \ (f ^^ k) bot"
      using assms(2) by simp
  qed
  show "(f ^^ k) bot \ lfp f"
    using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
qed

lemma mono_pow: "mono f \ mono (f ^^ n)"
  for f :: "'a \ 'a::order"
  by (induct n) (auto simp: mono_def)

lemma lfp_funpow:
  assumes f: "mono f"
  shows "lfp (f ^^ Suc n) = lfp f"
proof (rule antisym)
  show "lfp f \ lfp (f ^^ Suc n)"
  proof (rule lfp_lowerbound)
    have "f (lfp (f ^^ Suc n)) = lfp (\x. f ((f ^^ n) x))"
      unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def)
    then show "f (lfp (f ^^ Suc n)) \ lfp (f ^^ Suc n)"
      by (simp add: comp_def)
  qed
  have "(f ^^ n) (lfp f) = lfp f" for n
    by (induct n) (auto intro: f lfp_fixpoint)
  then show "lfp (f ^^ Suc n) \ lfp f"
    by (intro lfp_lowerbound) (simp del: funpow.simps)
qed

lemma gfp_funpow:
  assumes f: "mono f"
  shows "gfp (f ^^ Suc n) = gfp f"
proof (rule antisym)
  show "gfp f \ gfp (f ^^ Suc n)"
  proof (rule gfp_upperbound)
    have "f (gfp (f ^^ Suc n)) = gfp (\x. f ((f ^^ n) x))"
      unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def)
    then show "f (gfp (f ^^ Suc n)) \ gfp (f ^^ Suc n)"
      by (simp add: comp_def)
  qed
  have "(f ^^ n) (gfp f) = gfp f" for n
    by (induct n) (auto intro: f gfp_fixpoint)
  then show "gfp (f ^^ Suc n) \ gfp f"
    by (intro gfp_upperbound) (simp del: funpow.simps)
qed

lemma Kleene_iter_gpfp:
  fixes f :: "'a::order_top \ 'a"
  assumes "mono f"
    and "p \ f p"
  shows "p \ (f ^^ k) top"
proof (induct k)
  case 0
  show ?case by simp
next
  case Suc
  show ?case
    using monoD[OF assms(1) Suc] assms(2) by simp
qed

lemma gfp_Kleene_iter:
  assumes "mono f"
    and "(f ^^ Suc k) top = (f ^^ k) top"
  shows "gfp f = (f ^^ k) top"
    (is "?lhs = ?rhs")
proof (rule antisym)
  have "?rhs \ f ?rhs"
    using assms(2) by simp
  then show "?rhs \ ?lhs"
    by (rule gfp_upperbound)
  show "?lhs \ ?rhs"
    using Kleene_iter_gpfp[OF assms(1)] gfp_unfold[OF assms(1)] by simp
qed

subsection \<open>Embedding of the naturals into any \<open>semiring_1\<close>: \<^term>\<open>of_nat\<close>\<close>

context semiring_1
begin

definition of_nat :: "nat \ 'a"
  where "of_nat n = (plus 1 ^^ n) 0"

lemma of_nat_simps [simp]:
  shows of_nat_0: "of_nat 0 = 0"
    and of_nat_Suc: "of_nat (Suc m) = 1 + of_nat m"
  by (simp_all add: of_nat_def)

lemma of_nat_1 [simp]: "of_nat 1 = 1"
  by (simp add: of_nat_def)

lemma of_nat_add [simp]: "of_nat (m + n) = of_nat m + of_nat n"
  by (induct m) (simp_all add: ac_simps)

lemma of_nat_mult [simp]: "of_nat (m * n) = of_nat m * of_nat n"
  by (induct m) (simp_all add: ac_simps distrib_right)

lemma mult_of_nat_commute: "of_nat x * y = y * of_nat x"
  by (induct x) (simp_all add: algebra_simps)

primrec of_nat_aux :: "('a \ 'a) \ nat \ 'a \ 'a"
  where
    "of_nat_aux inc 0 i = i"
  | "of_nat_aux inc (Suc n) i = of_nat_aux inc n (inc i)" \<comment> \<open>tail recursive\<close>

lemma of_nat_code: "of_nat n = of_nat_aux (\i. i + 1) n 0"
proof (induct n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have "\i. of_nat_aux (\i. i + 1) n (i + 1) = of_nat_aux (\i. i + 1) n i + 1"
    by (induct n) simp_all
  from this [of 0] have "of_nat_aux (\i. i + 1) n 1 = of_nat_aux (\i. i + 1) n 0 + 1"
    by simp
  with Suc show ?case
    by (simp add: add.commute)
qed

lemma of_nat_of_bool [simp]:
  "of_nat (of_bool P) = of_bool P"
  by auto

end

declare of_nat_code [code]

context semiring_1_cancel
begin

lemma of_nat_diff [simp]:
  \<open>of_nat (m - n) = of_nat m - of_nat n\<close> if \<open>n \<le> m\<close>
proof -
  from that obtain q where \<open>m = n + q\<close>
    by (blast dest: le_Suc_ex)
  then show ?thesis
    by simp
qed

lemma of_nat_diff_if: \<open>of_nat (m - n) = (if n\<le>m then of_nat m - of_nat n else 0)\<close>
  by (simp add: not_le less_imp_le)

end

text \<open>Class for unital semirings with characteristic zero.
Includes non-ordered rings like the complex numbers.\<close>

class semiring_char_0 = semiring_1 +
  assumes inj_of_nat: "inj of_nat"
begin

lemma of_nat_eq_iff [simp]: "of_nat m = of_nat n \ m = n"
  by (auto intro: inj_of_nat injD)

text \<open>Special cases where either operand is zero\<close>

lemma of_nat_0_eq_iff [simp]: "0 = of_nat n \ 0 = n"
  by (fact of_nat_eq_iff [of 0 n, unfolded of_nat_0])

lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \ m = 0"
  by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])

lemma of_nat_1_eq_iff [simp]: "1 = of_nat n \ n=1"
  using of_nat_eq_iff by fastforce

lemma of_nat_eq_1_iff [simp]: "of_nat n = 1 \ n=1"
  using of_nat_eq_iff by fastforce

lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \ 0"
  unfolding of_nat_eq_0_iff by simp

lemma of_nat_0_neq [simp]: "0 \ of_nat (Suc n)"
  unfolding of_nat_0_eq_iff by simp

end

class ring_char_0 = ring_1 + semiring_char_0

lemma (in ordered_semiring_1) of_nat_0_le_iff [simp]: "0 \ of_nat n"
  by (induct n) simp_all

context linordered_nonzero_semiring
begin

lemma of_nat_less_0_iff [simp]: "\ of_nat m < 0"
  by (simp add: not_less)

lemma of_nat_mono[simp]: "i \ j \ of_nat i \ of_nat j"
  by (auto simp: le_iff_add intro!: add_increasing2)

lemma of_nat_less_iff [simp]: "of_nat m < of_nat n \ m < n"
proof(induct m n rule: diff_induct)
  case (1 m) then show ?case
    by auto
next
  case (2 n) then show ?case
    by (simp add: add_pos_nonneg)
next
  case (3 m n)
  then show ?case
    by (auto simp: add_commute [of 1] add_mono1 not_less add_right_mono leD)
qed

lemma of_nat_le_iff [simp]: "of_nat m \ of_nat n \ m \ n"
  by (simp add: not_less [symmetric] linorder_not_less [symmetric])

lemma less_imp_of_nat_less: "m < n \ of_nat m < of_nat n"
  by simp

lemma of_nat_less_imp_less: "of_nat m < of_nat n \ m < n"
  by simp

text \<open>Every \<open>linordered_nonzero_semiring\<close> has characteristic zero.\<close>

subclass semiring_char_0
  by standard (auto intro!: injI simp add: order.eq_iff)

text \<open>Special cases where either operand is zero\<close>

lemma of_nat_le_0_iff [simp]: "of_nat m \ 0 \ m = 0"
  by (rule of_nat_le_iff [of _ 0, simplified])

lemma of_nat_0_less_iff [simp]: "0 < of_nat n \ 0 < n"
  by (rule of_nat_less_iff [of 0, simplified])

end

context linordered_nonzero_semiring
begin

lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
  by (auto simp: max_def ord_class.max_def)

lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
  by (auto simp: min_def ord_class.min_def)

end

context linordered_semidom
begin

subclass linordered_nonzero_semiring ..

subclass semiring_char_0 ..

end

context linordered_idom
begin

lemma abs_of_nat [simp]:
  "\of_nat n\ = of_nat n"
  by (simp add: abs_if)

lemma sgn_of_nat [simp]:
  "sgn (of_nat n) = of_bool (n > 0)"
  by simp

end

lemma of_nat_id [simp]: "of_nat n = n"
  by (induct n) simp_all

lemma of_nat_eq_id [simp]: "of_nat = id"
  by (auto simp add: fun_eq_iff)

subsection \<open>The set of natural numbers\<close>

context semiring_1
begin

definition Nats :: "'a set"  (\<open>\<nat>\<close>)
  where "\ = range of_nat"

lemma of_nat_in_Nats [simp]: "of_nat n \ \"
  by (simp add: Nats_def)

lemma Nats_0 [simp]: "0 \ \"
  using of_nat_0 [symmetric] unfolding Nats_def
  by (rule range_eqI)

lemma Nats_1 [simp]: "1 \ \"
  using of_nat_1 [symmetric] unfolding Nats_def
  by (rule range_eqI)

lemma Nats_add [simp]: "a \ \ \ b \ \ \ a + b \ \"
  unfolding Nats_def using of_nat_add [symmetric]
  by (blast intro: range_eqI)

lemma Nats_mult [simp]: "a \ \ \ b \ \ \ a * b \ \"
  unfolding Nats_def using of_nat_mult [symmetric]
  by (blast intro: range_eqI)

lemma Nats_cases [cases set: Nats]:
  assumes "x \ \"
  obtains (of_nat) n where "x = of_nat n"
  unfolding Nats_def
proof -
  from \<open>x \<in> \<nat>\<close> have "x \<in> range of_nat" unfolding Nats_def .
  then obtain n where "x = of_nat n" ..
  then show thesis ..
qed

lemma Nats_induct [case_names of_nat, induct set: Nats]: "x \ \ \ (\n. P (of_nat n)) \ P x"
  by (rule Nats_cases) auto

lemma Nats_nonempty [simp]: "\ \ {}"
  unfolding Nats_def by auto

end

lemma Nats_diff [simp]:
  fixes a:: "'a::linordered_idom"
  assumes "a \ \" "b \ \" "b \ a" shows "a - b \ \"
proof -
  obtain i where i: "a = of_nat i"
    using Nats_cases assms by blast
  obtain j where j: "b = of_nat j"
    using Nats_cases assms by blast
  have "j \ i"
    using \<open>b \<le> a\<close> i j of_nat_le_iff by blast
  then have *: "of_nat i - of_nat j = (of_nat (i-j) :: 'a)"
    by (simp add: of_nat_diff)
  then show ?thesis
    by (simp add: * i j)
qed

subsection \<open>Further arithmetic facts concerning the natural numbers\<close>

lemma subst_equals:
  assumes "t = s" and "u = t"
  shows "u = s"
  using assms(2,1) by (rule trans)

locale nat_arith
begin

lemma add1: "(A::'a::comm_monoid_add) \ k + a \ A + b \ k + (a + b)"
  by (simp only: ac_simps)

lemma add2: "(B::'a::comm_monoid_add) \ k + b \ a + B \ k + (a + b)"
  by (simp only: ac_simps)

lemma suc1: "A == k + a \ Suc A \ k + Suc a"
  by (simp only: add_Suc_right)

lemma rule0: "(a::'a::comm_monoid_add) \ a + 0"
  by (simp only: add_0_right)

end

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

simproc_setup nateq_cancel_sums
  ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =
  \<open>K (try o Nat_Arith.cancel_eq_conv)\<close>

simproc_setup natless_cancel_sums
  ("(l::nat) + m < n" | "(l::nat) < m + n" | "Suc m < n" | "m < Suc n") =
  \<open>K (try o Nat_Arith.cancel_less_conv)\<close>

simproc_setup natle_cancel_sums
  ("(l::nat) + m \ n" | "(l::nat) \ m + n" | "Suc m \ n" | "m \ Suc n") =
  \<open>K (try o Nat_Arith.cancel_le_conv)\<close>

simproc_setup natdiff_cancel_sums
  ("(l::nat) + m - n" | "(l::nat) - (m + n)" | "Suc m - n" | "m - Suc n") =
  \<open>K (try o Nat_Arith.cancel_diff_conv)\<close>

context preorder
begin

lemma lift_Suc_mono_le:
  assumes mono: "\n. f n \ f (Suc n)"
    and "n \ n'"
  shows "f n \ f n'"
proof (cases "n < n'")
  case True
  then show ?thesis
    by (induct n n' rule: less_Suc_induct) (auto intro: mono order.trans)
next
  case False
  with \<open>n \<le> n'\<close> show ?thesis by auto
qed

lemma lift_Suc_antimono_le:
  assumes mono: "\n. f n \ f (Suc n)"
    and "n \ n'"
  shows "f n \ f n'"
proof (cases "n < n'")
  case True
  then show ?thesis
    by (induct n n' rule: less_Suc_induct) (auto intro: mono order.trans)
next
  case False
  with \<open>n \<le> n'\<close> show ?thesis by auto
qed

lemma lift_Suc_mono_less:
  assumes mono: "\n. f n < f (Suc n)"
    and "n < n'"
  shows "f n < f n'"
  using \<open>n < n'\<close> by (induct n n' rule: less_Suc_induct) (auto intro: mono order.strict_trans)

lemma lift_Suc_mono_less_iff: "(\n. f n < f (Suc n)) \ f n < f m \ n < m"
  by (blast intro: less_asym' lift_Suc_mono_less [of f]
    dest: linorder_not_less[THEN iffD1] le_eq_less_or_eq [THEN iffD1])

end

lemma mono_iff_le_Suc: "mono f \ (\n. f n \ f (Suc n))"
  unfolding mono_def by (auto intro: lift_Suc_mono_le [of f])

lemma antimono_iff_le_Suc: "antimono f \ (\n. f (Suc n) \ f n)"
  unfolding antimono_def by (auto intro: lift_Suc_antimono_le [of f])

lemma strict_mono_Suc_iff: "strict_mono f \ (\n. f n < f (Suc n))"
proof (intro iffI strict_monoI)
  assume *: "\n. f n < f (Suc n)"
  fix m n :: nat assume "m < n"
  thus "f m < f n"
    by (induction rule: less_Suc_induct) (use * in auto)
qed (auto simp: strict_mono_def)

lemma strict_mono_add: "strict_mono (\n::'a::linordered_semidom. n + k)"
  by (auto simp: strict_mono_def)

lemma mono_nat_linear_lb:
  fixes f :: "nat \ nat"
  assumes "\m n. m < n \ f m < f n"
  shows "f m + k \ f (m + k)"
proof (induct k)
  case 0
  then show ?case by simp
next
  case (Suc k)
  then have "Suc (f m + k) \ Suc (f (m + k))" by simp
  also from assms [of "m + k" "Suc (m + k)"] have "Suc (f (m + k)) \ f (Suc (m + k))"
    by (simp add: Suc_le_eq)
  finally show ?case by simp
qed

lemma bex_const1_if_mono_below_diag: fixes f :: "nat \ nat" assumes "mono f"
shows "f n < n \ \i
proof(induction n)
  case 0
  then show ?case by simp
next
  case (Suc n)
  have *: "f n \ f(Suc n)" using assms[simplified mono_iff_le_Suc] by blast
  from Suc.prems[simplified less_Suc_eq]
  show ?case
  proof
    assume "f(Suc n) < n"
    from order.strict_trans1[OF * this]
    show ?thesis using Suc.IH less_SucI by blast
  next
    assume "f(Suc n) = n"
    from order.strict_trans1[OF * Suc.prems, simplified less_Suc_eq]
    show ?case
    proof
      assume "f n < n"
      thus ?thesis using Suc.IH less_SucI by blast
    next
      assume "f n = n"
      with \<open>f(Suc n) = n\<close> show ?thesis by auto
    qed
  qed
qed

lemma bex_const1_if_mono_below_diag_Suc:
fixes f :: "nat \ nat" assumes "mono f" "f(Suc m) \ m"
shows "\i\m. f (Suc i) = f i"
using bex_const1_if_mono_below_diag[OF assms(1), of "Suc m"] assms(2) less_Suc_eq_le by blast

text \<open>Subtraction laws, mostly by Clemens Ballarin\<close>

lemma diff_less_mono:
  fixes a b c :: nat
  assumes "a < b" and "c \ a"
  shows "a - c < b - c"
proof -
  from assms obtain d e where "b = c + (d + e)" and "a = c + e" and "d > 0"
    by (auto dest!: le_Suc_ex less_imp_Suc_add simp add: ac_simps)
  then show ?thesis by simp
qed

lemma less_diff_conv: "i < j - k \ i + k < j"
  for i j k :: nat
  by (cases "k \ j") (auto simp add: not_le dest: less_imp_Suc_add le_Suc_ex)

lemma less_diff_conv2: "k \ j \ j - k < i \ j < i + k"
  for j k i :: nat
  by (auto dest: le_Suc_ex)

lemma le_diff_conv: "j - k \ i \ j \ i + k"
  for j k i :: nat
  by (cases "k \ j") (auto simp add: not_le dest!: less_imp_Suc_add le_Suc_ex)

lemma diff_diff_cancel [simp]: "i \ n \ n - (n - i) = i"
  for i n :: nat
  by (auto dest: le_Suc_ex)

lemma diff_less [simp]: "0 < n \ 0 < m \ m - n < m"
  for i n :: nat
  by (auto dest: less_imp_Suc_add)

text \<open>Simplification of relational expressions involving subtraction\<close>

lemma diff_diff_eq: "k \ m \ k \ n \ m - k - (n - k) = m - n"
  for m n k :: nat
  by (auto dest!: le_Suc_ex)

hide_fact (open) diff_diff_eq

lemma eq_diff_iff: "k \ m \ k \ n \ m - k = n - k \ m = n"
  for m n k :: nat
  by (auto dest: le_Suc_ex)

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

--> maximum size reached

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

quality99%

¤ Dauer der Verarbeitung: 0.41 Sekunden (vorverarbeitet) ¤

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.

Angebot

Die farbliche Syntaxdarstellung ist noch experimentell.