1 (* Title: FOL/ex/nat2.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 For ex/nat.thy. |
|
7 Examples of simplification and induction on the natural numbers |
|
8 *) |
|
9 |
|
10 open Nat2; |
|
11 |
|
12 val nat_rews = [pred_0, pred_succ, plus_0, plus_succ, |
|
13 nat_distinct1, nat_distinct2, succ_inject, |
|
14 leq_0,leq_succ_succ,leq_succ_0, |
|
15 lt_0_succ,lt_succ_succ,lt_0]; |
|
16 |
|
17 val nat_ss = FOL_ss addsimps nat_rews; |
|
18 |
|
19 val prems = goal Nat2.thy |
|
20 "[| P(0); !!x. P(succ(x)) |] ==> All(P)"; |
|
21 by (rtac nat_ind 1); |
|
22 by (REPEAT (resolve_tac (prems@[allI,impI]) 1)); |
|
23 val nat_exh = result(); |
|
24 |
|
25 goal Nat2.thy "~ n=succ(n)"; |
|
26 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
27 result(); |
|
28 |
|
29 goal Nat2.thy "~ succ(n)=n"; |
|
30 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
31 result(); |
|
32 |
|
33 goal Nat2.thy "~ succ(succ(n))=n"; |
|
34 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
35 result(); |
|
36 |
|
37 goal Nat2.thy "~ n=succ(succ(n))"; |
|
38 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
39 result(); |
|
40 |
|
41 goal Nat2.thy "m+0 = m"; |
|
42 by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1); |
|
43 val plus_0_right = result(); |
|
44 |
|
45 goal Nat2.thy "m+succ(n) = succ(m+n)"; |
|
46 by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1); |
|
47 val plus_succ_right = result(); |
|
48 |
|
49 goal Nat2.thy "~n=0 --> m+pred(n) = pred(m+n)"; |
|
50 by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_succ_right])) "n" 1); |
|
51 result(); |
|
52 |
|
53 goal Nat2.thy "~n=0 --> succ(pred(n))=n"; |
|
54 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
55 result(); |
|
56 |
|
57 goal Nat2.thy "m+n=0 <-> m=0 & n=0"; |
|
58 by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1); |
|
59 result(); |
|
60 |
|
61 goal Nat2.thy "m <= n --> m <= succ(n)"; |
|
62 by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1); |
|
63 by (rtac (impI RS allI) 1); |
|
64 by (ALL_IND_TAC nat_ind (simp_tac nat_ss) 1); |
|
65 by (fast_tac FOL_cs 1); |
|
66 val le_imp_le_succ = result() RS mp; |
|
67 |
|
68 goal Nat2.thy "n<succ(n)"; |
|
69 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
70 result(); |
|
71 |
|
72 goal Nat2.thy "~ n<n"; |
|
73 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
74 result(); |
|
75 |
|
76 goal Nat2.thy "m < n --> m < succ(n)"; |
|
77 by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1); |
|
78 by (rtac (impI RS allI) 1); |
|
79 by (ALL_IND_TAC nat_ind (simp_tac nat_ss) 1); |
|
80 by (fast_tac FOL_cs 1); |
|
81 result(); |
|
82 |
|
83 goal Nat2.thy "m <= n --> m <= n+k"; |
|
84 by (IND_TAC nat_ind |
|
85 (simp_tac (nat_ss addsimps [plus_0_right, plus_succ_right, le_imp_le_succ])) |
|
86 "k" 1); |
|
87 val le_plus = result(); |
|
88 |
|
89 goal Nat2.thy "succ(m) <= n --> m <= n"; |
|
90 by (res_inst_tac [("x","n")]spec 1); |
|
91 by (ALL_IND_TAC nat_exh (simp_tac (nat_ss addsimps [le_imp_le_succ])) 1); |
|
92 val succ_le = result(); |
|
93 |
|
94 goal Nat2.thy "~m<n <-> n<=m"; |
|
95 by (IND_TAC nat_ind (simp_tac nat_ss) "n" 1); |
|
96 by (rtac (impI RS allI) 1); |
|
97 by (ALL_IND_TAC nat_ind (asm_simp_tac nat_ss) 1); |
|
98 val not_less = result(); |
|
99 |
|
100 goal Nat2.thy "n<=m --> ~m<n"; |
|
101 by (simp_tac (nat_ss addsimps [not_less]) 1); |
|
102 val le_imp_not_less = result(); |
|
103 |
|
104 goal Nat2.thy "m<n --> ~n<=m"; |
|
105 by (cut_facts_tac [not_less] 1 THEN fast_tac FOL_cs 1); |
|
106 val not_le = result(); |
|
107 |
|
108 goal Nat2.thy "m+k<=n --> m<=n"; |
|
109 by (IND_TAC nat_ind (K all_tac) "k" 1); |
|
110 by (simp_tac (nat_ss addsimps [plus_0_right]) 1); |
|
111 by (rtac (impI RS allI) 1); |
|
112 by (simp_tac (nat_ss addsimps [plus_succ_right]) 1); |
|
113 by (REPEAT (resolve_tac [allI,impI] 1)); |
|
114 by (cut_facts_tac [succ_le] 1); |
|
115 by (fast_tac FOL_cs 1); |
|
116 val plus_le = result(); |
|
117 |
|
118 val prems = goal Nat2.thy "[| ~m=0; m <= n |] ==> ~n=0"; |
|
119 by (cut_facts_tac prems 1); |
|
120 by (REPEAT (etac rev_mp 1)); |
|
121 by (IND_TAC nat_exh (simp_tac nat_ss) "m" 1); |
|
122 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
|
123 val not0 = result(); |
|
124 |
|
125 goal Nat2.thy "a<=a' & b<=b' --> a+b<=a'+b'"; |
|
126 by (IND_TAC nat_ind (simp_tac (nat_ss addsimps [plus_0_right,le_plus])) "b" 1); |
|
127 by (resolve_tac [impI RS allI] 1); |
|
128 by (resolve_tac [allI RS allI] 1); |
|
129 by (ALL_IND_TAC nat_exh (asm_simp_tac (nat_ss addsimps [plus_succ_right])) 1); |
|
130 val plus_le_plus = result(); |
|
131 |
|
132 goal Nat2.thy "i<=j --> j<=k --> i<=k"; |
|
133 by (IND_TAC nat_ind (K all_tac) "i" 1); |
|
134 by (simp_tac nat_ss 1); |
|
135 by (resolve_tac [impI RS allI] 1); |
|
136 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
|
137 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
|
138 by (fast_tac FOL_cs 1); |
|
139 val le_trans = result(); |
|
140 |
|
141 goal Nat2.thy "i < j --> j <=k --> i < k"; |
|
142 by (IND_TAC nat_ind (K all_tac) "j" 1); |
|
143 by (simp_tac nat_ss 1); |
|
144 by (resolve_tac [impI RS allI] 1); |
|
145 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
|
146 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
|
147 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
|
148 by (fast_tac FOL_cs 1); |
|
149 val less_le_trans = result(); |
|
150 |
|
151 goal Nat2.thy "succ(i) <= j <-> i < j"; |
|
152 by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1); |
|
153 by (resolve_tac [impI RS allI] 1); |
|
154 by (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1); |
|
155 val succ_le = result(); |
|
156 |
|
157 goal Nat2.thy "i<succ(j) <-> i=j | i<j"; |
|
158 by (IND_TAC nat_ind (simp_tac nat_ss) "j" 1); |
|
159 by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
|
160 by (resolve_tac [impI RS allI] 1); |
|
161 by (ALL_IND_TAC nat_exh (asm_simp_tac nat_ss) 1); |
|
162 val less_succ = result(); |
|
163 |
|