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 |] ==> ab ∈ N

theorem mult_typingL:

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

theorem multC0:

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

theorem multC_succ:

  [| a ∈ N; b ∈ N |] ==> succ(a) #× b = b #+ ab ∈ 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 #+ ab ∈ N

theorem mult_commute:

  [| a ∈ N; b ∈ N |] ==> ab = ba ∈ N

theorem add_mult_distrib:

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

theorem mult_assoc:

  [| a ∈ N; b ∈ N; c ∈ N |] ==> (ab) #× c = abc ∈ 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