|
1 structure Nat = |
|
2 struct |
|
3 |
|
4 local |
|
5 val parse_ast_translation = [] |
|
6 val parse_preproc = None |
|
7 val parse_postproc = None |
|
8 val parse_translation = [] |
|
9 val print_translation = [] |
|
10 val print_preproc = None |
|
11 val print_postproc = None |
|
12 val print_ast_translation = [] |
|
13 in |
|
14 |
|
15 (**** begin of user section ****) |
|
16 |
|
17 (**** end of user section ****) |
|
18 |
|
19 val thy = extend_theory (FOL.thy) |
|
20 "Nat" |
|
21 ([], |
|
22 [], |
|
23 [(["nat"], 0)], |
|
24 [(["nat"], ([], "term"))], |
|
25 [(["Suc"], "nat=>nat"), |
|
26 (["rec"], "[nat, 'a, [nat,'a]=>'a] => 'a")], |
|
27 Some (NewSext { |
|
28 mixfix = |
|
29 [Delimfix("0", "nat", "0"), |
|
30 Infixl("+", "[nat, nat] => nat", 60)], |
|
31 xrules = |
|
32 [], |
|
33 parse_ast_translation = parse_ast_translation, |
|
34 parse_preproc = parse_preproc, |
|
35 parse_postproc = parse_postproc, |
|
36 parse_translation = parse_translation, |
|
37 print_translation = print_translation, |
|
38 print_preproc = print_preproc, |
|
39 print_postproc = print_postproc, |
|
40 print_ast_translation = print_ast_translation})) |
|
41 [("induct", "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"), |
|
42 ("Suc_inject", "Suc(m)=Suc(n) ==> m=n"), |
|
43 ("Suc_neq_0", "Suc(m)=0 ==> R"), |
|
44 ("rec_0", "rec(0,a,f) = a"), |
|
45 ("rec_Suc", "rec(Suc(m), a, f) = f(m, rec(m,a,f))"), |
|
46 ("add_def", "m+n == rec(m, n, %x y. Suc(y))")] |
|
47 |
|
48 val ax = get_axiom thy |
|
49 |
|
50 val induct = ax "induct" |
|
51 val Suc_inject = ax "Suc_inject" |
|
52 val Suc_neq_0 = ax "Suc_neq_0" |
|
53 val rec_0 = ax "rec_0" |
|
54 val rec_Suc = ax "rec_Suc" |
|
55 val add_def = ax "add_def" |
|
56 |
|
57 |
|
58 end |
|
59 end |