# Theory Arith

Up to index of Isabelle/CTT

theory Arith
imports Bool
uses [Arith.ML]
begin

    (*  Title:      CTT/Arith.thy
        ID:         $Id: Arith.thy,v 1.6 2005/09/16 21:01:29 wenzelm Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
        Copyright   1991  University of Cambridge
    *)

    header {* Arithmetic operators and their definitions *}

    theory Arith
    imports Bool
    begin

    text {*
      Proves about elementary arithmetic: addition, multiplication, etc.
      Tests definitions and simplifier.
    *}

    consts
      "#+"  :: "[i,i]=>i"   (infixr 65)
      "-"   :: "[i,i]=>i"   (infixr 65)
      "|-|" :: "[i,i]=>i"   (infixr 65)
      "#*"  :: "[i,i]=>i"   (infixr 70)
      div   :: "[i,i]=>i"   (infixr 70)
      mod   :: "[i,i]=>i"   (infixr 70)

    syntax (xsymbols)
      "op #*"      :: "[i, i] => i"   (infixr "#×" 70)

    syntax (HTML output)
      "op #*"      :: "[i, i] => i"   (infixr "#×" 70)

    defs
      add_def:     "a#+b == rec(a, b, %u v. succ(v))"
      diff_def:    "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
      absdiff_def: "a|-|b == (a-b) #+ (b-a)"
      mult_def:    "a#*b == rec(a, 0, %u v. b #+ v)"
      mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
      div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"

    ML {* use_legacy_bindings (the_context ()) *}

    end

theorem add_typing:

      [| a ∈ N; b ∈ N |] ==> a #+ b ∈ N

theorem add_typingL:

      [| a = c ∈ N; b = d ∈ N |] ==> a #+ b = c #+ d ∈ N

theorem addC0:

      b ∈ N ==> 0 #+ b = b ∈ N

theorem addC_succ:

      [| a ∈ N; b ∈ N |] ==> succ(a) #+ b = succ(a #+ b) ∈ N

theorem mult_typing:

      [| a ∈ N; b ∈ N |] ==> a #× b ∈ N

theorem mult_typingL:

      [| a = c ∈ N; b = d ∈ N |] ==> a #× b = c #× d ∈ N

theorem multC0:

      b ∈ N ==> 0 #× b = 0 ∈ N

theorem multC_succ:

      [| a ∈ N; b ∈ N |] ==> succ(a) #× b = b #+ a #× b ∈ N

theorem diff_typing:

      [| a ∈ N; b ∈ N |] ==> a - b ∈ N

theorem diff_typingL:

      [| a = c ∈ N; b = d ∈ N |] ==> a - b = c - d ∈ N

theorem diffC0:

      a ∈ N ==> a - 0 = a ∈ N

theorem diff_0_eq_0:

      b ∈ N ==> 0 - b = 0 ∈ N

theorem diff_succ_succ:

      [| a ∈ N; b ∈ N |] ==> succ(a) - succ(b) = a - b ∈ N

theorem add_assoc:

      [| a ∈ N; b ∈ N; c ∈ N |] ==> (a #+ b) #+ c = a #+ b #+ c ∈ N

theorem add_commute:

      [| a ∈ N; b ∈ N |] ==> a #+ b = b #+ a ∈ N

theorem mult_0_right:

      a ∈ N ==> a #× 0 = 0 ∈ N

theorem mult_succ_right:

      [| a ∈ N; b ∈ N |] ==> a #× succ(b) = a #+ a #× b ∈ N

theorem mult_commute:

      [| a ∈ N; b ∈ N |] ==> a #× b = b #× a ∈ N

theorem add_mult_distrib:

      [| a ∈ N; b ∈ N; c ∈ N |] ==> (a #+ b) #× c = a #× c #+ b #× c ∈ N

theorem mult_assoc:

      [| a ∈ N; b ∈ N; c ∈ N |] ==> (a #× b) #× c = a #× b #× c ∈ N

theorem diff_self_eq_0:

      a ∈ N ==> a - a = 0 ∈ N

theorem add_diff_inverse_lemma:

      b ∈ N
      ==> rec(b, λλx xa. eq, %u v. λλx. rec(x, λλx. eq, %u v. λλx. eq))
          ∈ Π x∈N. Eq(N, b - x, 0) --> Eq(N, b #+ x - b, x)

theorem add_diff_inverse:

      [| a ∈ N; b ∈ N; b - a = 0 ∈ N |] ==> b #+ a - b = a ∈ N

theorem absdiff_typing:

      [| a ∈ N; b ∈ N |] ==> a |-| b ∈ N

theorem absdiff_typingL:

      [| a = c ∈ N; b = d ∈ N |] ==> a |-| b = c |-| d ∈ N

theorem absdiff_self_eq_0:

      a ∈ N ==> a |-| a = 0 ∈ N

theorem absdiffC0:

      a ∈ N ==> 0 |-| a = a ∈ N

theorem absdiff_succ_succ:

      [| a ∈ N; b ∈ N |] ==> succ(a) |-| succ(b) = a |-| b ∈ N

theorem absdiff_commute:

      [| a ∈ N; b ∈ N |] ==> a |-| b = b |-| a ∈ N

theorem add_eq0_lemma:

      [| a ∈ N; b ∈ N |]
      ==> rec(a, λλx. eq, %u v. λλx. contr(0)) ∈ Eq(N, a #+ b, 0) --> Eq(N, a, 0)

theorem add_eq0:

      [| a ∈ N; b ∈ N; a #+ b = 0 ∈ N |] ==> a = 0 ∈ N

theorem absdiff_eq0_lem:

      [| a ∈ N; b ∈ N; a |-| b = 0 ∈ N |]
      ==> <eq,eq> ∈ Eq(N, a - b, 0) × Eq(N, b - a, 0)

theorem absdiff_eq0:

      [| a |-| b = 0 ∈ N; a ∈ N; b ∈ N |] ==> a = b ∈ N

theorem mod_typing:

      [| a ∈ N; b ∈ N |] ==> a mod b ∈ N

theorem mod_typingL:

      [| a = c ∈ N; b = d ∈ N |] ==> a mod b = c mod d ∈ N

theorem modC0:

      b ∈ N ==> 0 mod b = 0 ∈ N

theorem modC_succ:

      [| a ∈ N; b ∈ N |]
      ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) ∈ N

theorem div_typing:

      [| a ∈ N; b ∈ N |] ==> a div b ∈ N

theorem div_typingL:

      [| a = c ∈ N; b = d ∈ N |] ==> a div b = c div d ∈ N

theorem divC0:

      b ∈ N ==> 0 div b = 0 ∈ N

theorem divC_succ:

      [| a ∈ N; b ∈ N |]
      ==> succ(a) div b = rec(succ(a) mod b, succ(a div b), %x y. a div b) ∈ N

theorem divC_succ2:

      [| a ∈ N; b ∈ N |]
      ==> succ(a) div b = rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) ∈ N

theorem iszero_decidable:

      a ∈ N
      ==> rec(a, inl(eq), %ka kb. inr(<ka,eq>))
          ∈ Eq(N, a, 0) + (Σ x∈N. Eq(N, a, succ(x)))

theorem mod_div_equality:

      [| a ∈ N; b ∈ N |] ==> a mod b #+ (a div b) #× b = a ∈ N