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