1459
|
1 |
(* Title: FOL/ex/NatClass.ML
|
1246
|
2 |
ID: $Id$
|
2469
|
3 |
Author: Markus Wenzel, TU Muenchen
|
1246
|
4 |
|
|
5 |
This is Nat.ML trivially modified to make it work with NatClass.thy.
|
|
6 |
*)
|
|
7 |
|
|
8 |
open NatClass;
|
|
9 |
|
5050
|
10 |
Goal "Suc(k) ~= (k::'a::nat)";
|
1246
|
11 |
by (res_inst_tac [("n","k")] induct 1);
|
1459
|
12 |
by (rtac notI 1);
|
|
13 |
by (etac Suc_neq_0 1);
|
|
14 |
by (rtac notI 1);
|
|
15 |
by (etac notE 1);
|
|
16 |
by (etac Suc_inject 1);
|
1246
|
17 |
qed "Suc_n_not_n";
|
|
18 |
|
|
19 |
|
5050
|
20 |
Goal "(k+m)+n = k+(m+n)";
|
1246
|
21 |
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
|
1459
|
22 |
by (rtac induct 1);
|
1246
|
23 |
back();
|
|
24 |
back();
|
|
25 |
back();
|
|
26 |
back();
|
|
27 |
back();
|
|
28 |
back();
|
|
29 |
|
5050
|
30 |
Goalw [add_def] "0+n = n";
|
1459
|
31 |
by (rtac rec_0 1);
|
1246
|
32 |
qed "add_0";
|
|
33 |
|
5050
|
34 |
Goalw [add_def] "Suc(m)+n = Suc(m+n)";
|
1459
|
35 |
by (rtac rec_Suc 1);
|
1246
|
36 |
qed "add_Suc";
|
|
37 |
|
2469
|
38 |
Addsimps [add_0, add_Suc];
|
1246
|
39 |
|
5050
|
40 |
Goal "(k+m)+n = k+(m+n)";
|
1246
|
41 |
by (res_inst_tac [("n","k")] induct 1);
|
2469
|
42 |
by (Simp_tac 1);
|
|
43 |
by (Asm_simp_tac 1);
|
1246
|
44 |
qed "add_assoc";
|
|
45 |
|
5050
|
46 |
Goal "m+0 = m";
|
1246
|
47 |
by (res_inst_tac [("n","m")] induct 1);
|
2469
|
48 |
by (Simp_tac 1);
|
|
49 |
by (Asm_simp_tac 1);
|
1246
|
50 |
qed "add_0_right";
|
|
51 |
|
5050
|
52 |
Goal "m+Suc(n) = Suc(m+n)";
|
1246
|
53 |
by (res_inst_tac [("n","m")] induct 1);
|
2469
|
54 |
by (ALLGOALS (Asm_simp_tac));
|
1246
|
55 |
qed "add_Suc_right";
|
|
56 |
|
|
57 |
val [prem] = goal NatClass.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
|
|
58 |
by (res_inst_tac [("n","i")] induct 1);
|
2469
|
59 |
by (Simp_tac 1);
|
4091
|
60 |
by (asm_simp_tac (simpset() addsimps [prem]) 1);
|
1246
|
61 |
result();
|