theory church imports lambda begin locale CNUM = CONV + (* Church numerals *) fixes C0 :: "term" fixes C1 :: "term" fixes C2 :: "term" fixes C3 :: "term" fixes C4 :: "term" fixes C5 :: "term" fixes tt :: "term" fixes ff :: "term" (* primitive recursive functions *) fixes zero :: "term" fixes succ :: "term" fixes add :: "term" fixes IF :: "term" (*Jan adds*) fixes mult :: "term" fixes pred :: "term" fixes tuple :: "term" fixes first :: "term" fixes second :: "term" fixes tup_succ :: "term" fixes next_tup :: "term" (*end of Jan adds*) assumes tt_def: "tt == lam x. lam y. x" (* ff_def: "ff == lam x. lam y. x"*) (*Jan Smaus corrects mistake*) assumes ff_def: "ff == lam x. lam y. y" assumes C0_def: "C0 == lam f. lam x. x" assumes C1_def: "C1 == lam f. lam x. f^x" assumes C2_def: "C2 == lam f. lam x. f^(f^x)" assumes C3_def: "C3 == lam f. lam x. f^(f^(f^x))" assumes C4_def: "C4 == lam f. lam x. f^(f^(f^(f^x)))" assumes C5_def: "C5 == lam f. lam x. f^(f^(f^(f^(f^x))))" assumes zero_def: "zero == lam x. x^(lam y. ff)^tt" assumes succ_def: "succ == lam x. lam y. lam z. y^(x^y^z)" assumes add_def: "add == lam u. lam v. lam f. lam x. u^f^(v^f^x)" assumes if_def: "IF == lam b. lam m. lam n. b^m^n" (*Jan adds*) assumes mult_def: "mult == lam u. lam v. lam f. u^(v^f)" assumes tuple_def: "tuple == lam x. lam y. lam f. f^x^y" assumes first_def: "first == lam t. t^tt" assumes second_def: "second == lam t. t^ff" assumes tup_succ_def: "tup_succ == lam t. tuple^(succ^(first^t))^(succ^(second^t))" (*tup_succ_def is correct but useless for defining pred*) assumes next_tup_def: "next_tup == lam t. tuple^(second^t)^(succ^(second^t))" (*(0,0) \\ (0,1). (0,1) \\ (1,2). (1,2) \\ (2,3) etc.*) assumes pred_def: "pred == lam u. first^(u^next_tup^(tuple^C0^C0))" begin end end