|
1 > goal Nat.thy "m+0 = m"; |
|
2 Level 0 |
|
3 m + 0 = m |
|
4 1. m + 0 = m |
|
5 > by (res_inst_tac [("n","m")] induct 1); |
|
6 Level 1 |
|
7 m + 0 = m |
|
8 1. 0 + 0 = 0 |
|
9 2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x) |
|
10 > by (simp_tac add_ss 1); |
|
11 Level 2 |
|
12 m + 0 = m |
|
13 1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x) |
|
14 > by (asm_simp_tac add_ss 1); |
|
15 Level 3 |
|
16 m + 0 = m |
|
17 No subgoals! |
|
18 |
|
19 |
|
20 > goal Nat.thy "m+Suc(n) = Suc(m+n)"; |
|
21 Level 0 |
|
22 m + Suc(n) = Suc(m + n) |
|
23 1. m + Suc(n) = Suc(m + n) |
|
24 val it = [] : thm list |
|
25 > by (res_inst_tac [("n","m")] induct 1); |
|
26 Level 1 |
|
27 m + Suc(n) = Suc(m + n) |
|
28 1. 0 + Suc(n) = Suc(0 + n) |
|
29 2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n) |
|
30 val it = () : unit |
|
31 > by (simp_tac add_ss 1); |
|
32 Level 2 |
|
33 m + Suc(n) = Suc(m + n) |
|
34 1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n) |
|
35 val it = () : unit |
|
36 > trace_simp := true; |
|
37 val it = () : unit |
|
38 > by (asm_simp_tac add_ss 1); |
|
39 Rewriting: |
|
40 Suc(x) + Suc(n) == Suc(x + Suc(n)) |
|
41 Rewriting: |
|
42 x + Suc(n) == Suc(x + n) |
|
43 Rewriting: |
|
44 Suc(x) + n == Suc(x + n) |
|
45 Rewriting: |
|
46 Suc(Suc(x + n)) = Suc(Suc(x + n)) == True |
|
47 Level 3 |
|
48 m + Suc(n) = Suc(m + n) |
|
49 No subgoals! |
|
50 val it = () : unit |
|
51 |
|
52 |
|
53 |
|
54 > val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; |
|
55 Level 0 |
|
56 f(i + j) = i + f(j) |
|
57 1. f(i + j) = i + f(j) |
|
58 > prths prems; |
|
59 f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))] |
|
60 |
|
61 > by (res_inst_tac [("n","i")] induct 1); |
|
62 Level 1 |
|
63 f(i + j) = i + f(j) |
|
64 1. f(0 + j) = 0 + f(j) |
|
65 2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j) |
|
66 > by (simp_tac f_ss 1); |
|
67 Level 2 |
|
68 f(i + j) = i + f(j) |
|
69 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); |
|
71 Level 3 |
|
72 f(i + j) = i + f(j) |
|
73 No subgoals! |