104
|
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!
|