69 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j) |
71 1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j) |
70 > by (asm_simp_tac (f_ss addrews prems) 1); |
72 > by (asm_simp_tac (f_ss addrews prems) 1); |
71 Level 3 |
73 Level 3 |
72 f(i + j) = i + f(j) |
74 f(i + j) = i + f(j) |
73 No subgoals! |
75 No subgoals! |
|
76 |
|
77 |
|
78 |
|
79 > goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)"; |
|
80 Level 0 |
|
81 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) |
|
82 1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) |
|
83 |
|
84 > by (simp_tac natsum_ss 1); |
|
85 Level 1 |
|
86 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) |
|
87 1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n |
|
88 |
|
89 > by (nat_ind_tac "n" 1); |
|
90 Level 2 |
|
91 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) |
|
92 1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0 |
|
93 2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) = |
|
94 n1 + n1 * n1 ==> |
|
95 Suc(n1) + |
|
96 (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) = |
|
97 Suc(n1) + Suc(n1) * Suc(n1) |
|
98 |
|
99 > by (simp_tac natsum_ss 1); |
|
100 Level 3 |
|
101 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) |
|
102 1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) = |
|
103 n1 + n1 * n1 ==> |
|
104 Suc(n1) + |
|
105 (Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) = |
|
106 Suc(n1) + Suc(n1) * Suc(n1) |
|
107 |
|
108 > by (asm_simp_tac natsum_ss 1); |
|
109 Level 4 |
|
110 Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n) |
|
111 No subgoals! |