|
wenzelm@4396
|
1 |
|
|
lcp@359
|
2 |
Pretty.setmargin 70;
|
|
lcp@359
|
3 |
|
|
wenzelm@4396
|
4 |
|
|
wenzelm@4396
|
5 |
context Arith.thy;
|
|
wenzelm@4396
|
6 |
goal Arith.thy "0 + (x + 0) = x + 0 + 0";
|
|
wenzelm@4396
|
7 |
by (Simp_tac 1);
|
|
wenzelm@4396
|
8 |
|
|
wenzelm@4396
|
9 |
|
|
wenzelm@4396
|
10 |
|
|
wenzelm@4396
|
11 |
|
|
lcp@104
|
12 |
> goal Nat.thy "m+0 = m";
|
|
lcp@104
|
13 |
Level 0
|
|
lcp@104
|
14 |
m + 0 = m
|
|
lcp@104
|
15 |
1. m + 0 = m
|
|
lcp@104
|
16 |
> by (res_inst_tac [("n","m")] induct 1);
|
|
lcp@104
|
17 |
Level 1
|
|
lcp@104
|
18 |
m + 0 = m
|
|
lcp@104
|
19 |
1. 0 + 0 = 0
|
|
lcp@104
|
20 |
2. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)
|
|
lcp@104
|
21 |
> by (simp_tac add_ss 1);
|
|
lcp@104
|
22 |
Level 2
|
|
lcp@104
|
23 |
m + 0 = m
|
|
lcp@104
|
24 |
1. !!x. x + 0 = x ==> Suc(x) + 0 = Suc(x)
|
|
lcp@104
|
25 |
> by (asm_simp_tac add_ss 1);
|
|
lcp@104
|
26 |
Level 3
|
|
lcp@104
|
27 |
m + 0 = m
|
|
lcp@104
|
28 |
No subgoals!
|
|
lcp@104
|
29 |
|
|
lcp@104
|
30 |
|
|
lcp@104
|
31 |
> goal Nat.thy "m+Suc(n) = Suc(m+n)";
|
|
lcp@104
|
32 |
Level 0
|
|
lcp@104
|
33 |
m + Suc(n) = Suc(m + n)
|
|
lcp@104
|
34 |
1. m + Suc(n) = Suc(m + n)
|
|
lcp@104
|
35 |
val it = [] : thm list
|
|
lcp@104
|
36 |
> by (res_inst_tac [("n","m")] induct 1);
|
|
lcp@104
|
37 |
Level 1
|
|
lcp@104
|
38 |
m + Suc(n) = Suc(m + n)
|
|
lcp@104
|
39 |
1. 0 + Suc(n) = Suc(0 + n)
|
|
lcp@104
|
40 |
2. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)
|
|
lcp@104
|
41 |
val it = () : unit
|
|
lcp@104
|
42 |
> by (simp_tac add_ss 1);
|
|
lcp@104
|
43 |
Level 2
|
|
lcp@104
|
44 |
m + Suc(n) = Suc(m + n)
|
|
lcp@104
|
45 |
1. !!x. x + Suc(n) = Suc(x + n) ==> Suc(x) + Suc(n) = Suc(Suc(x) + n)
|
|
lcp@104
|
46 |
val it = () : unit
|
|
lcp@104
|
47 |
> trace_simp := true;
|
|
lcp@104
|
48 |
val it = () : unit
|
|
lcp@104
|
49 |
> by (asm_simp_tac add_ss 1);
|
|
lcp@104
|
50 |
Rewriting:
|
|
lcp@104
|
51 |
Suc(x) + Suc(n) == Suc(x + Suc(n))
|
|
lcp@104
|
52 |
Rewriting:
|
|
lcp@104
|
53 |
x + Suc(n) == Suc(x + n)
|
|
lcp@104
|
54 |
Rewriting:
|
|
lcp@104
|
55 |
Suc(x) + n == Suc(x + n)
|
|
lcp@104
|
56 |
Rewriting:
|
|
lcp@104
|
57 |
Suc(Suc(x + n)) = Suc(Suc(x + n)) == True
|
|
lcp@104
|
58 |
Level 3
|
|
lcp@104
|
59 |
m + Suc(n) = Suc(m + n)
|
|
lcp@104
|
60 |
No subgoals!
|
|
lcp@104
|
61 |
val it = () : unit
|
|
lcp@104
|
62 |
|
|
lcp@104
|
63 |
|
|
lcp@104
|
64 |
|
|
lcp@104
|
65 |
> val prems = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
|
|
lcp@104
|
66 |
Level 0
|
|
lcp@104
|
67 |
f(i + j) = i + f(j)
|
|
lcp@104
|
68 |
1. f(i + j) = i + f(j)
|
|
lcp@104
|
69 |
> prths prems;
|
|
lcp@104
|
70 |
f(Suc(?n)) = Suc(f(?n)) [!!n. f(Suc(n)) = Suc(f(n))]
|
|
lcp@104
|
71 |
|
|
lcp@104
|
72 |
> by (res_inst_tac [("n","i")] induct 1);
|
|
lcp@104
|
73 |
Level 1
|
|
lcp@104
|
74 |
f(i + j) = i + f(j)
|
|
lcp@104
|
75 |
1. f(0 + j) = 0 + f(j)
|
|
lcp@104
|
76 |
2. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)
|
|
lcp@104
|
77 |
> by (simp_tac f_ss 1);
|
|
lcp@104
|
78 |
Level 2
|
|
lcp@104
|
79 |
f(i + j) = i + f(j)
|
|
lcp@104
|
80 |
1. !!x. f(x + j) = x + f(j) ==> f(Suc(x) + j) = Suc(x) + f(j)
|
|
lcp@104
|
81 |
> by (asm_simp_tac (f_ss addrews prems) 1);
|
|
lcp@104
|
82 |
Level 3
|
|
lcp@104
|
83 |
f(i + j) = i + f(j)
|
|
lcp@104
|
84 |
No subgoals!
|
|
lcp@359
|
85 |
|
|
lcp@359
|
86 |
|
|
lcp@359
|
87 |
|
|
lcp@359
|
88 |
> goal NatSum.thy "Suc(Suc(0))*sum(%i.i,Suc(n)) = n*Suc(n)";
|
|
lcp@359
|
89 |
Level 0
|
|
lcp@359
|
90 |
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
|
|
lcp@359
|
91 |
1. Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
|
|
lcp@359
|
92 |
|
|
lcp@359
|
93 |
> by (simp_tac natsum_ss 1);
|
|
lcp@359
|
94 |
Level 1
|
|
lcp@359
|
95 |
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
|
|
lcp@359
|
96 |
1. n + (n + (sum(%i. i, n) + sum(%i. i, n))) = n + n * n
|
|
lcp@359
|
97 |
|
|
lcp@359
|
98 |
> by (nat_ind_tac "n" 1);
|
|
lcp@359
|
99 |
Level 2
|
|
lcp@359
|
100 |
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
|
|
lcp@359
|
101 |
1. 0 + (0 + (sum(%i. i, 0) + sum(%i. i, 0))) = 0 + 0 * 0
|
|
lcp@359
|
102 |
2. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
|
|
lcp@359
|
103 |
n1 + n1 * n1 ==>
|
|
lcp@359
|
104 |
Suc(n1) +
|
|
lcp@359
|
105 |
(Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
|
|
lcp@359
|
106 |
Suc(n1) + Suc(n1) * Suc(n1)
|
|
lcp@359
|
107 |
|
|
lcp@359
|
108 |
> by (simp_tac natsum_ss 1);
|
|
lcp@359
|
109 |
Level 3
|
|
lcp@359
|
110 |
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
|
|
lcp@359
|
111 |
1. !!n1. n1 + (n1 + (sum(%i. i, n1) + sum(%i. i, n1))) =
|
|
lcp@359
|
112 |
n1 + n1 * n1 ==>
|
|
lcp@359
|
113 |
Suc(n1) +
|
|
lcp@359
|
114 |
(Suc(n1) + (sum(%i. i, Suc(n1)) + sum(%i. i, Suc(n1)))) =
|
|
lcp@359
|
115 |
Suc(n1) + Suc(n1) * Suc(n1)
|
|
lcp@359
|
116 |
|
|
lcp@359
|
117 |
> by (asm_simp_tac natsum_ss 1);
|
|
lcp@359
|
118 |
Level 4
|
|
lcp@359
|
119 |
Suc(Suc(0)) * sum(%i. i, Suc(n)) = n * Suc(n)
|
|
lcp@359
|
120 |
No subgoals!
|