author | oheimb |
Thu, 18 Apr 1996 14:11:02 +0200 | |
changeset 1662 | a6b55b9d2f22 |
parent 1661 | 1e2462c3fece |
child 1959 | 58f8379eca73 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: FOL/ex/nat2.ML |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Tobias Nipkow |
0 | 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, |
|
1459 | 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]; |
|
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)); |
|
725 | 23 |
qed "nat_exh"; |
0 | 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); |
|
725 | 43 |
qed "plus_0_right"; |
0 | 44 |
|
45 |
goal Nat2.thy "m+succ(n) = succ(m+n)"; |
|
46 |
by (IND_TAC nat_ind (simp_tac nat_ss) "m" 1); |
|
725 | 47 |
qed "plus_succ_right"; |
0 | 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); |
|
755 | 66 |
val le_imp_le_succ = store_thm("le_imp_le_succ", result() RS mp); |
0 | 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); |
|
755 | 87 |
qed "le_plus"; |
0 | 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); |
|
755 | 92 |
qed "succ_le"; |
0 | 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); |
|
725 | 98 |
qed "not_less"; |
0 | 99 |
|
100 |
goal Nat2.thy "n<=m --> ~m<n"; |
|
101 |
by (simp_tac (nat_ss addsimps [not_less]) 1); |
|
755 | 102 |
qed "le_imp_not_less"; |
0 | 103 |
|
104 |
goal Nat2.thy "m<n --> ~n<=m"; |
|
105 |
by (cut_facts_tac [not_less] 1 THEN fast_tac FOL_cs 1); |
|
755 | 106 |
qed "not_le"; |
0 | 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); |
|
755 | 116 |
qed "plus_le"; |
0 | 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); |
|
755 | 123 |
qed "not0"; |
0 | 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); |
|
755 | 130 |
qed "plus_le_plus"; |
0 | 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); |
|
755 | 139 |
qed "le_trans"; |
0 | 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); |
|
755 | 149 |
qed "less_le_trans"; |
0 | 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); |
|
755 | 155 |
qed "succ_le2"; |
0 | 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); |
|
1662
a6b55b9d2f22
adapted proof of less_succ: problem because of non-confluent SimpSet removed
oheimb
parents:
1661
diff
changeset
|
161 |
by (ALL_IND_TAC nat_exh (simp_tac nat_ss) 1); |
1661 | 162 |
by (asm_simp_tac nat_ss 1); |
755 | 163 |
qed "less_succ"; |
0 | 164 |