14 rec :: [nat, 'a, [nat,'a]=>'a] => 'a |
14 rec :: [nat, 'a, [nat,'a]=>'a] => 'a |
15 "+" :: [nat, nat] => nat (infixl 60) |
15 "+" :: [nat, nat] => nat (infixl 60) |
16 |
16 |
17 rules |
17 rules |
18 induct "[| $H |- $E, P(0), $F; |
18 induct "[| $H |- $E, P(0), $F; |
19 !!x. $H |- $E, P(x) --> P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" |
19 !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" |
20 |
20 |
21 Suc_inject "|- Suc(m)=Suc(n) --> m=n" |
21 Suc_inject "|- Suc(m)=Suc(n) --> m=n" |
22 Suc_neq_0 "|- Suc(m) ~= 0" |
22 Suc_neq_0 "|- Suc(m) ~= 0" |
23 rec_0 "|- rec(0,a,f) = a" |
23 rec_0 "|- rec(0,a,f) = a" |
24 rec_Suc "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))" |
24 rec_Suc "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))" |