src/FOL/ex/.nat.thy.ML

Initial revision

structure Nat =
struct

local
 val parse_ast_translation = []
 val parse_preproc = None
 val parse_postproc = None
 val parse_translation = []
 val print_translation = []
 val print_preproc = None
 val print_postproc = None
 val print_ast_translation = []
in

(**** begin of user section ****)

(**** end of user section ****)

val thy = extend_theory (FOL.thy)
 "Nat"
 ([],
  [],
  [(["nat"], 0)],
  [(["nat"], ([], "term"))],
  [(["Suc"], "nat=>nat"),
   (["rec"], "[nat, 'a, [nat,'a]=>'a] => 'a")],
  Some (NewSext {
   mixfix =
    [Delimfix("0", "nat", "0"),
     Infixl("+", "[nat, nat] => nat", 60)],
   xrules =
    [],
   parse_ast_translation = parse_ast_translation,
   parse_preproc = parse_preproc,
   parse_postproc = parse_postproc,
   parse_translation = parse_translation,
   print_translation = print_translation,
   print_preproc = print_preproc,
   print_postproc = print_postproc,
   print_ast_translation = print_ast_translation}))
 [("induct", "[| P(0);  !!x. P(x) ==> P(Suc(x)) |]  ==> P(n)"),
  ("Suc_inject", "Suc(m)=Suc(n) ==> m=n"),
  ("Suc_neq_0", "Suc(m)=0      ==> R"),
  ("rec_0", "rec(0,a,f) = a"),
  ("rec_Suc", "rec(Suc(m), a, f) = f(m, rec(m,a,f))"),
  ("add_def", "m+n == rec(m, n, %x y. Suc(y))")]

val ax = get_axiom thy

val induct = ax "induct"
val Suc_inject = ax "Suc_inject"
val Suc_neq_0 = ax "Suc_neq_0"
val rec_0 = ax "rec_0"
val rec_Suc = ax "rec_Suc"
val add_def = ax "add_def"


end
end