0
|
1 |
(* Title: FOL/ex/nat.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1992 University of Cambridge
|
|
5 |
|
|
6 |
Examples for the manual "Introduction to Isabelle"
|
|
7 |
|
|
8 |
Proofs about the natural numbers
|
|
9 |
|
|
10 |
INCOMPATIBLE with nat2.ML, Nipkow's examples
|
|
11 |
|
|
12 |
To generate similar output to manual, execute these commands:
|
|
13 |
Pretty.setmargin 72; print_depth 0;
|
|
14 |
*)
|
|
15 |
|
|
16 |
open Nat;
|
|
17 |
|
36
|
18 |
goal Nat.thy "Suc(k) ~= k";
|
0
|
19 |
by (res_inst_tac [("n","k")] induct 1);
|
|
20 |
by (resolve_tac [notI] 1);
|
|
21 |
by (eresolve_tac [Suc_neq_0] 1);
|
|
22 |
by (resolve_tac [notI] 1);
|
|
23 |
by (eresolve_tac [notE] 1);
|
|
24 |
by (eresolve_tac [Suc_inject] 1);
|
|
25 |
val Suc_n_not_n = result();
|
|
26 |
|
|
27 |
|
|
28 |
goal Nat.thy "(k+m)+n = k+(m+n)";
|
|
29 |
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
|
|
30 |
by (resolve_tac [induct] 1);
|
|
31 |
back();
|
|
32 |
back();
|
|
33 |
back();
|
|
34 |
back();
|
|
35 |
back();
|
|
36 |
back();
|
|
37 |
|
|
38 |
goalw Nat.thy [add_def] "0+n = n";
|
|
39 |
by (resolve_tac [rec_0] 1);
|
|
40 |
val add_0 = result();
|
|
41 |
|
|
42 |
goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
|
|
43 |
by (resolve_tac [rec_Suc] 1);
|
|
44 |
val add_Suc = result();
|
|
45 |
|
132
|
46 |
val add_ss = FOL_ss addsimps [add_0, add_Suc];
|
0
|
47 |
|
|
48 |
goal Nat.thy "(k+m)+n = k+(m+n)";
|
|
49 |
by (res_inst_tac [("n","k")] induct 1);
|
|
50 |
by (simp_tac add_ss 1);
|
|
51 |
by (asm_simp_tac add_ss 1);
|
|
52 |
val add_assoc = result();
|
|
53 |
|
|
54 |
goal Nat.thy "m+0 = m";
|
|
55 |
by (res_inst_tac [("n","m")] induct 1);
|
|
56 |
by (simp_tac add_ss 1);
|
|
57 |
by (asm_simp_tac add_ss 1);
|
|
58 |
val add_0_right = result();
|
|
59 |
|
|
60 |
goal Nat.thy "m+Suc(n) = Suc(m+n)";
|
|
61 |
by (res_inst_tac [("n","m")] induct 1);
|
|
62 |
by (ALLGOALS (asm_simp_tac add_ss));
|
|
63 |
val add_Suc_right = result();
|
|
64 |
|
|
65 |
val [prem] = goal Nat.thy "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)";
|
|
66 |
by (res_inst_tac [("n","i")] induct 1);
|
|
67 |
by (simp_tac add_ss 1);
|
|
68 |
by (asm_simp_tac (add_ss addsimps [prem]) 1);
|
|
69 |
result();
|