src/FOL/ex/.nat2.thy.ML

%\urlstyle{rm}
%\isabellestyle{it}

structure Nat2 =
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)
 "Nat2"
 ([],
  [],
  [(["nat"], 0)],
  [(["nat"], ([], "term"))],
  [(["succ", "pred"], "nat => nat")],
  Some (NewSext {
   mixfix =
    [Delimfix("0", "nat", "0"),
     Infixr("+", "[nat,nat] => nat", 90),
     Infixr("<", "[nat,nat] => o", 70),
     Infixr("<=", "[nat,nat] => o", 70)],
   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}))
 [("pred_0", "pred(0) = 0"),
  ("pred_succ", "pred(succ(m)) = m"),
  ("plus_0", "0+n = n"),
  ("plus_succ", "succ(m)+n = succ(m+n)"),
  ("nat_distinct1", "~ 0=succ(n)"),
  ("nat_distinct2", "~ succ(m)=0"),
  ("succ_inject", "succ(m)=succ(n) <-> m=n"),
  ("leq_0", "0 <= n"),
  ("leq_succ_succ", "succ(m)<=succ(n) <-> m<=n"),
  ("leq_succ_0", "~ succ(m) <= 0"),
  ("lt_0_succ", "0 < succ(n)"),
  ("lt_succ_succ", "succ(m)<succ(n) <-> m<n"),
  ("lt_0", "~ m < 0"),
  ("nat_ind", "[| P(0); ALL n. P(n)-->P(succ(n)) |] ==> All(P)")]

val ax = get_axiom thy

val pred_0 = ax "pred_0"
val pred_succ = ax "pred_succ"
val plus_0 = ax "plus_0"
val plus_succ = ax "plus_succ"
val nat_distinct1 = ax "nat_distinct1"
val nat_distinct2 = ax "nat_distinct2"
val succ_inject = ax "succ_inject"
val leq_0 = ax "leq_0"
val leq_succ_succ = ax "leq_succ_succ"
val leq_succ_0 = ax "leq_succ_0"
val lt_0_succ = ax "lt_0_succ"
val lt_succ_succ = ax "lt_succ_succ"
val lt_0 = ax "lt_0"
val nat_ind = ax "nat_ind"


end
end