src/FOL/ex/Natural_Numbers.thy
changeset 11696 233362cfecc7
parent 11679 afdbee613f58
child 11726 2b2a45abe876
equal deleted inserted replaced
11695:8c66866fb0ff 11696:233362cfecc7
    15   Zero :: nat    ("0")
    15   Zero :: nat    ("0")
    16   Suc :: "nat => nat"
    16   Suc :: "nat => nat"
    17   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
    17   rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
    18 
    18 
    19 axioms
    19 axioms
    20   induct [induct type: nat]:
    20   induct [case_names Zero Suc, induct type: nat]:
    21     "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)"
    21     "P(0) ==> (!!x. P(x) ==> P(Suc(x))) ==> P(n)"
    22   Suc_inject: "Suc(m) = Suc(n) ==> m = n"
    22   Suc_inject: "Suc(m) = Suc(n) ==> m = n"
    23   Suc_neq_0: "Suc(m) = 0 ==> R"
    23   Suc_neq_0: "Suc(m) = 0 ==> R"
    24   rec_0: "rec(0, a, f) = a"
    24   rec_0: "rec(0, a, f) = a"
    25   rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"
    25   rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m, a, f))"