(* 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) \\ (0,1). (0,1) \\ (1,2). (1,2) \\ (2,3) etc.*) pred_def "pred == lam u. first^(u^next_tup^(tuple^C0^C0))" (*end of Jan adds*) end