equal
deleted
inserted
replaced
32 primrec |
32 primrec |
33 "add2 Z n = n" |
33 "add2 Z n = n" |
34 "add2 (S m) n = S(add2 m n)" |
34 "add2 (S m) n = S(add2 m n)" |
35 |
35 |
36 declare add2.simps [code] |
36 declare add2.simps [code] |
37 lemma [code]: "add2 (add2 n m) k = add2 n (add2 m k)" |
37 lemma [code nbe]: "add2 (add2 n m) k = add2 n (add2 m k)" |
38 by (induct n) auto |
38 by (induct n) auto |
39 lemma [code]: "add2 n (S m) = S (add2 n m)" |
39 lemma [code]: "add2 n (S m) = S (add2 n m)" |
40 by(induct n) auto |
40 by(induct n) auto |
41 lemma [code]: "add2 n Z = n" |
41 lemma [code]: "add2 n Z = n" |
42 by(induct n) auto |
42 by(induct n) auto |