equal
deleted
inserted
replaced
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 [induct type: nat]: |
21 "P(0) \<Longrightarrow> (!!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))" |
26 |
26 |