equal
deleted
inserted
replaced
46 lemma add_02: "add m 0 = m" |
46 lemma add_02: "add m 0 = m" |
47 apply(induction m) |
47 apply(induction m) |
48 apply(auto) |
48 apply(auto) |
49 done |
49 done |
50 |
50 |
|
51 value "add 2 3" |
|
52 |
|
53 |
51 (**commutative-associative**) |
54 (**commutative-associative**) |
52 lemma add_04: "add m (add n k) = add (add m n) k" |
55 lemma add_04: "add m (add n k) = add (add m n) k" |
53 apply(induct m) |
56 apply(induct m) |
54 apply(simp_all) |
57 apply(simp_all) |
55 done |
58 done |
59 apply(auto) |
62 apply(auto) |
60 done |
63 done |
61 |
64 |
62 lemma add_Suc: "add m (Suc n) = Suc (add m n)" |
65 lemma add_Suc: "add m (Suc n) = Suc (add m n)" |
63 apply(induct m) |
66 apply(induct m) |
|
67 apply(metis add.simps(1)) |
64 apply(auto) |
68 apply(auto) |
65 done |
69 done |
66 |
70 |
67 lemma add_comm: "add m n = add n m" |
71 lemma add_comm: "add m n = add n m" |
68 apply(induct m) |
72 apply(induct m) |