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 |
|
54 (**commutative-associative**) |
51 (**commutative-associative**) |
55 lemma add_04: "add m (add n k) = add (add m n) k" |
52 lemma add_04: "add m (add n k) = add (add m n) k" |
56 apply(induct m) |
53 apply(induct m) |
57 apply(simp_all) |
54 apply(simp_all) |
58 done |
55 done |
59 |
56 |
60 lemma add_zero: "add n 0 = n" |
57 lemma add_zero: "add n 0 = n" |
61 sorry |
58 apply(induct n) |
|
59 apply(auto) |
|
60 done |
62 |
61 |
63 lemma add_Suc: "add m (Suc n) = Suc (add m n)" |
62 lemma add_Suc: "add m (Suc n) = Suc (add m n)" |
64 sorry |
63 apply(induct m) |
|
64 apply(auto) |
|
65 done |
65 |
66 |
66 lemma add_comm: "add m n = add n m" |
67 lemma add_comm: "add m n = add n m" |
67 apply(induct m) |
68 apply(induct m) |
68 apply(simp add: add_zero) |
69 apply(simp add: add_zero) |
69 apply(simp add: add_Suc) |
70 apply(simp add: add_Suc) |