(*  Title:      NUMC.thy
    Author:     Ayari/Vigano`  WS00/WS01

Church Numerals (based on Conversion and Booleans)
*)

(*Jan Smaus modified by replacing "CNUMC" with "CNUM*)
CNUM = CONV +

consts
  
  (* Church numerals *)
  C0     :: "term"
  C1     :: "term"
  C2     :: "term"
  C3     :: "term"
  C4     :: "term"
  C5     :: "term"
  tt     :: "term"
  ff     :: "term"
  (* primitive recursive functions *)
  zero :: "term"
  succ :: "term"
  add  :: "term"
  IF   :: "term"
  (*Jan adds*)
  mult :: "term"
  pred :: "term"
  tuple :: "term"
  first :: "term"
  second :: "term"
  tup_succ :: "term"
  next_tup :: "term"
  
  (*end of Jan adds*)
rules
  tt_def    "tt == lam x. lam y. x"
(*  ff_def    "ff == lam x. lam y. x"*)
(*Jan Smaus corrects mistake*)
  ff_def    "ff == lam x. lam y. y"

  C0_def    "C0 == lam f. lam x. x"
  C1_def    "C1 == lam f. lam x. f^x"
  C2_def    "C2 == lam f. lam x. f^(f^x)"
  C3_def    "C3 == lam f. lam x. f^(f^(f^x))"
  C4_def    "C4 == lam f. lam x. f^(f^(f^(f^x)))"  
  C5_def    "C5 == lam f. lam x. f^(f^(f^(f^(f^x))))"

  zero_def "zero == lam x. x^(lam y. ff)^tt"
  succ_def "succ == lam x. lam y. lam z. y^(x^y^z)"
  add_def  "add  == lam u. lam v. lam f. lam x.  u^f^(v^f^x)"
  if_def   "IF   == lam b. lam m. lam n. b^m^n"

(*Jan adds*)
  mult_def "mult == lam u. lam v. lam f. u^(v^f)"
  tuple_def "tuple == lam x. lam y. lam f. f^x^y"
  first_def "first == lam t. t^tt"
  second_def "second == lam t. t^ff"
  tup_succ_def "tup_succ == lam
		t. tuple^(succ^(first^t))^(succ^(second^t))"
(*tup_succ_def is correct but useless for defining pred*)
  next_tup_def "next_tup == lam
		t. tuple^(second^t)^(succ^(second^t))"
(*(0,0) \\<rightarrow> (0,1). (0,1) \\<rightarrow> (1,2). (1,2) \\<rightarrow> (2,3) etc.*)
  pred_def "pred == lam u. first^(u^next_tup^(tuple^C0^C0))"
  
(*end of Jan adds*)
end