# Theory Nat2

Up to index of Isabelle/FOL/ex

theory Nat2
imports FOL
uses [Nat2.ML]
begin

    (*  Title:      FOL/ex/nat2.thy
        ID:         $Id: Nat2.thy,v 1.5 2005/09/03 15:15:52 wenzelm Exp $
        Author:     Tobias Nipkow
        Copyright   1994  University of Cambridge
    *)

    header {* Theory for examples of simplification and induction on the natural numbers *}

    theory Nat2
    imports FOL
    begin

    typedecl nat
    arities nat :: "term"

    consts
      succ :: "nat => nat"
      pred :: "nat => nat"
      0 :: nat    ("0")
      add :: "[nat,nat] => nat"    (infixr "+" 90)
      lt :: "[nat,nat] => o"    (infixr "<" 70)
      leq :: "[nat,nat] => o"    (infixr "<=" 70)

    axioms
     pred_0:         "pred(0) = 0"
     pred_succ:      "pred(succ(m)) = m"

     plus_0:         "0+n = n"
     plus_succ:      "succ(m)+n = succ(m+n)"

     nat_distinct1:  "~ 0=succ(n)"
     nat_distinct2:  "~ succ(m)=0"
     succ_inject:    "succ(m)=succ(n) <-> m=n"

     leq_0:          "0 <= n"
     leq_succ_succ:  "succ(m)<=succ(n) <-> m<=n"
     leq_succ_0:     "~ succ(m) <= 0"

     lt_0_succ:      "0 < succ(n)"
     lt_succ_succ:   "succ(m)<succ(n) <-> m<n"
     lt_0:           "~ m < 0"

     nat_ind:        "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem nat_exh:

      [| P(0); !!x. P(succ(x)) |] ==> All(P)

theorem plus_0_right:

      m + 0 = m

theorem plus_succ_right:

      m + succ(n) = succ(m + n)

theorem le_imp_le_succ:

      m <= n ==> m <= succ(n)

theorem le_plus:

      m <= n --> m <= n + k

theorem succ_le:

      succ(m) <= n --> m <= n

theorem not_less:

      ¬ m < n <-> n <= m

theorem le_imp_not_less:

      n <= m --> ¬ m < n

theorem not_le:

      m < n --> ¬ n <= m

theorem plus_le:

      m + k <= n --> m <= n

theorem not0:

      [| m ≠ 0; m <= n |] ==> n ≠ 0

theorem plus_le_plus:

      a <= a' ∧ b <= b' --> a + b <= a' + b'

theorem le_trans:

      i <= j --> j <= k --> i <= k

theorem less_le_trans:

      i < j --> j <= k --> i < k

theorem succ_le2:

      succ(i) <= j <-> i < j

theorem less_succ:

      i < succ(j) <-> i = j ∨ i < j