1 (* Title: Provers/nat_transitive.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 1996 TU Munich |
|
5 *) |
|
6 |
|
7 (*** |
|
8 A very simple package for inequalities over nat. |
|
9 It uses all premises of the form |
|
10 |
|
11 t = u, t < u, t <= u, ~(t < u), ~(t <= u) |
|
12 |
|
13 where t and u must be of type nat, to |
|
14 1. either derive a contradiction, |
|
15 in which case the conclusion can be any term, |
|
16 2. or prove the conclusion, which must be of the same form as the premises. |
|
17 |
|
18 The package |
|
19 - does not deal with the relation ~= |
|
20 - treats `pred', +, *, ... as atomic terms. Hence it can prove |
|
21 [| x < y+z; y+z < u |] ==> Suc x < u |
|
22 but not |
|
23 [| x < y+z; z < u |] ==> Suc x < y+u |
|
24 - takes only (in)equalities which are atomic premises into account. It does |
|
25 not deal with logical operators like -->, & etc. Hence it cannot prove |
|
26 [| x < y+z & y+z < u |] ==> Suc x < u |
|
27 |
|
28 In order not to fall foul of the above limitations, the following hints are |
|
29 useful: |
|
30 |
|
31 1. You may need to run `by(safe_tac HOL_cs)' in order to bring out the atomic |
|
32 premises. |
|
33 |
|
34 2. To get rid of ~= in the premises, it is advisable to use a rule like |
|
35 nat_neqE = "[| (m::nat) ~= n; m < n ==> P; n < m ==> P |] ==> P" : thm |
|
36 (the name nat_eqE is chosen in HOL), for example as follows: |
|
37 by(safe_tac (HOL_cs addSEs [nat_neqE]) |
|
38 |
|
39 3. To get rid of `pred', you may be able to do the following: |
|
40 expand `pred(m)' into `case m of 0 => 0 | Suc n => n' and use split_tac |
|
41 to turn the case-expressions into logical case distinctions. In HOL: |
|
42 simp_tac (... addsimps [pred_def] setloop (split_tac [expand_nat_case])) |
|
43 |
|
44 The basic tactic is `trans_tac'. In order to use `trans_tac' as a solver in |
|
45 the simplifier, `cut_trans_tac' is also provided, which cuts the given thms |
|
46 in as facts. |
|
47 |
|
48 Notes: |
|
49 - It should easily be possible to adapt this package to other numeric types |
|
50 like int. |
|
51 - There is ample scope for optimizations, which so far have not proved |
|
52 necessary. |
|
53 - The code can be simplified by adding the negated conclusion to the |
|
54 premises to derive a contradiction. However, this would restrict the |
|
55 package to classical logics. |
|
56 ***) |
|
57 |
|
58 (* The package works for arbitrary logics. |
|
59 You just need to instantiate the following parameter structure. |
|
60 *) |
|
61 signature LESS_ARITH = |
|
62 sig |
|
63 val lessI: thm (* n < Suc n *) |
|
64 val zero_less_Suc: thm (* 0 < Suc n *) |
|
65 val less_reflE: thm (* n < n ==> P *) |
|
66 val less_zeroE: thm (* n < 0 ==> P *) |
|
67 val less_incr: thm (* m < n ==> Suc m < Suc n *) |
|
68 val less_decr: thm (* Suc m < Suc n ==> m < n *) |
|
69 val less_incr_rhs: thm (* m < n ==> m < Suc n *) |
|
70 val less_decr_lhs: thm (* Suc m < n ==> m < n *) |
|
71 val less_trans_Suc: thm (* [| i < j; j < k |] ==> Suc i < k *) |
|
72 val leD: thm (* m <= n ==> m < Suc n *) |
|
73 val not_lessD: thm (* ~(m < n) ==> n < Suc m *) |
|
74 val not_leD: thm (* ~(m <= n) ==> n < m *) |
|
75 val eqD1: thm (* m = n ==> m < Suc n *) |
|
76 val eqD2: thm (* m = n ==> m < Suc n *) |
|
77 val not_lessI: thm (* n < Suc m ==> ~(m < n) *) |
|
78 val leI: thm (* m < Suc n ==> m <= n *) |
|
79 val not_leI: thm (* n < m ==> ~(m <= n) *) |
|
80 val eqI: thm (* [| m < Suc n; n < Suc m |] ==> n = m *) |
|
81 val is_zero: term -> bool |
|
82 val decomp: term -> (term * int * string * term * int)option |
|
83 (* decomp(`Suc^i(x) Rel Suc^j(y)') should yield (x,i,Rel,y,j) |
|
84 where Rel is one of "<", "~<", "<=", "~<=" and "=" *) |
|
85 end; |
|
86 |
|
87 |
|
88 signature TRANS_TAC = |
|
89 sig |
|
90 val trans_tac: int -> tactic |
|
91 val cut_trans_tac: thm list -> int -> tactic |
|
92 end; |
|
93 |
|
94 functor Trans_Tac_Fun(Less:LESS_ARITH):TRANS_TAC = |
|
95 struct |
|
96 |
|
97 datatype proof = Asm of int |
|
98 | Thm of proof list * thm |
|
99 | Incr1 of proof * int (* Increment 1 side *) |
|
100 | Incr2 of proof * int (* Increment 2 sides *); |
|
101 |
|
102 |
|
103 (*** Turn proof objects into thms ***) |
|
104 |
|
105 fun incr2(th,i) = if i=0 then th else |
|
106 if i>0 then incr2(th RS Less.less_incr,i-1) |
|
107 else incr2(th RS Less.less_decr,i+1); |
|
108 |
|
109 fun incr1(th,i) = if i=0 then th else |
|
110 if i>0 then incr1(th RS Less.less_incr_rhs,i-1) |
|
111 else incr1(th RS Less.less_decr_lhs,i+1); |
|
112 |
|
113 fun prove asms = |
|
114 let fun pr(Asm i) = nth_elem(i,asms) |
|
115 | pr(Thm(prfs,thm)) = (map pr prfs) MRS thm |
|
116 | pr(Incr1(p,i)) = incr1(pr p,i) |
|
117 | pr(Incr2(p,i)) = incr2(pr p,i) |
|
118 in pr end; |
|
119 |
|
120 (*** Internal representation of inequalities |
|
121 (x,i,y,j) means x+i < y+j. |
|
122 Leads to simpler case distinctions than the normalized x < y+k |
|
123 ***) |
|
124 type less = term * int * term * int * proof; |
|
125 |
|
126 (*** raised when contradiction is found ***) |
|
127 exception Contr of proof; |
|
128 |
|
129 (*** raised when goal can't be proved ***) |
|
130 exception Cant; |
|
131 |
|
132 infix subsumes; |
|
133 |
|
134 fun (x,i,y,j:int,_) subsumes (x',i',y',j',_) = |
|
135 x=x' andalso y=y' andalso j-i<=j'-i'; |
|
136 |
|
137 fun trivial(x,i:int,y,j,_) = (x=y orelse Less.is_zero(x)) andalso i<j; |
|
138 |
|
139 (*** transitive closure ***) |
|
140 |
|
141 (* Very naive: computes all consequences of a set of less-statements. *) |
|
142 (* In the worst case very expensive not just in time but also space *) |
|
143 (* Could easily be optimized but there are ususally only a few < asms *) |
|
144 |
|
145 fun add new = |
|
146 let fun adds([],news) = new::news |
|
147 | adds(old::olds,news) = if new subsumes old then adds(olds,news) |
|
148 else adds(olds,old::news) |
|
149 in adds end; |
|
150 |
|
151 fun ctest(less as (x,i,y,j,p)) = |
|
152 if x=y andalso i>=j |
|
153 then raise Contr(Thm([Incr1(Incr2(p,~j),j-i)],Less.less_reflE)) else |
|
154 if Less.is_zero(y) andalso i>=j |
|
155 then raise Contr(Thm([Incr2(p,~j)],Less.less_zeroE)) |
|
156 else less; |
|
157 |
|
158 fun mktrans((x,i,_,j,p):less,(_,k,z,l,q)) = |
|
159 ctest(if j >= k |
|
160 then (x,i+1,z,l+(j-k),Thm([p,Incr2(q,j-k)],Less.less_trans_Suc)) |
|
161 else (x,i+(k-j)+1,z,l,Thm([Incr2(p,k-j),q],Less.less_trans_Suc))); |
|
162 |
|
163 fun trans (new as (x,i,y,j,p)) olds = |
|
164 let fun tr(news, old as (x1,i1,y1,j1,p1):less) = |
|
165 if y1=x then mktrans(old,new)::news else |
|
166 if x1=y then mktrans(new,old)::news else news |
|
167 in foldl tr ([],olds) end; |
|
168 |
|
169 fun close1(olds: less list)(new:less):less list = |
|
170 if trivial new orelse exists (fn old => old subsumes new) olds then olds |
|
171 else let val news = trans new olds |
|
172 in close (add new (olds,[])) news end |
|
173 and close (olds: less list) ([]:less list) = olds |
|
174 | close olds ((new:less)::news) = close (close1 olds (ctest new)) news; |
|
175 |
|
176 (*** end of transitive closure ***) |
|
177 |
|
178 (* recognize and solve trivial goal *) |
|
179 fun triv_sol(x,i,y,j,_) = |
|
180 if x=y andalso i<j |
|
181 then Some(Incr1(Incr2(Thm([],Less.lessI),i),j-i-1)) else |
|
182 if Less.is_zero(x) andalso i<j |
|
183 then Some(Incr1(Incr2(Thm([],Less.zero_less_Suc),i),j-i-1)) |
|
184 else None; |
|
185 |
|
186 (* solve less starting from facts *) |
|
187 fun solve facts (less as (x,i,y,j,_)) = |
|
188 case triv_sol less of |
|
189 None => (case find_first (fn fact => fact subsumes less) facts of |
|
190 None => raise Cant |
|
191 | Some(a,m,b,n,p) => Incr1(Incr2(p,j-n),n+i-m-j)) |
|
192 | Some prf => prf; |
|
193 |
|
194 (* turn term into a less-tuple *) |
|
195 fun mkasm(t,n) = |
|
196 case Less.decomp(t) of |
|
197 Some(x,i,rel,y,j) => (case rel of |
|
198 "<" => [(x,i,y,j,Asm n)] |
|
199 | "~<" => [(y,j,x,i+1,Thm([Asm n],Less.not_lessD))] |
|
200 | "<=" => [(x,i,y,j+1,Thm([Asm n],Less.leD))] |
|
201 | "~<=" => [(y,j,x,i,Thm([Asm n],Less.not_leD))] |
|
202 | "=" => [(x,i,y,j+1,Thm([Asm n],Less.eqD1)), |
|
203 (y,j,x,i+1,Thm([Asm n],Less.eqD2))] |
|
204 | "~=" => [] |
|
205 | _ => error("trans_tac/decomp: unknown relation " ^ rel)) |
|
206 | None => []; |
|
207 |
|
208 (* mkconcl t returns a pair (goals,proof) where goals is a list of *) |
|
209 (* less-subgoals to solve, and proof the validation which proves the concl t *) |
|
210 (* from the subgoals. Asm ~1 is dummy *) |
|
211 fun mkconcl t = |
|
212 case Less.decomp(t) of |
|
213 Some(x,i,rel,y,j) => (case rel of |
|
214 "<" => ([(x,i,y,j,Asm ~1)],Asm 0) |
|
215 | "~<" => ([(y,j,x,i+1,Asm ~1)],Thm([Asm 0],Less.not_lessI)) |
|
216 | "<=" => ([(x,i,y,j+1,Asm ~1)],Thm([Asm 0],Less.leI)) |
|
217 | "~<=" => ([(y,j,x,i,Asm ~1)],Thm([Asm 0],Less.not_leI)) |
|
218 | "=" => ([(x,i,y,j+1,Asm ~1),(y,j,x,i+1,Asm ~1)], |
|
219 Thm([Asm 0,Asm 1],Less.eqI)) |
|
220 | "~=" => raise Cant |
|
221 | _ => error("trans_tac/decomp: unknown relation " ^ rel)) |
|
222 | None => raise Cant; |
|
223 |
|
224 |
|
225 val trans_tac = SUBGOAL (fn (A,n) => |
|
226 let val Hs = Logic.strip_assums_hyp A |
|
227 val C = Logic.strip_assums_concl A |
|
228 val lesss = flat(ListPair.map mkasm (Hs, 0 upto (length Hs - 1))) |
|
229 val clesss = close [] lesss |
|
230 val (subgoals,prf) = mkconcl C |
|
231 val prfs = map (solve clesss) subgoals |
|
232 in METAHYPS (fn asms => let val thms = map (prove asms) prfs |
|
233 in rtac (prove thms prf) 1 end) n |
|
234 end |
|
235 handle Contr(p) => METAHYPS (fn asms => rtac (prove asms p) 1) n |
|
236 | Cant => no_tac); |
|
237 |
|
238 fun cut_trans_tac thms = cut_facts_tac thms THEN' trans_tac; |
|
239 |
|
240 end; |
|
241 |
|
242 (*** Tests |
|
243 fun test s = prove_goal Nat.thy ("!!m::nat." ^ s) (fn _ => [trans_tac 1]); |
|
244 |
|
245 test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> Suc(Suc i) < m"; |
|
246 test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> Suc(Suc(Suc i)) <= m"; |
|
247 test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> ~ m <= Suc(Suc i)"; |
|
248 test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l) |] ==> ~ m < Suc(Suc(Suc i))"; |
|
249 test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l); m <= Suc(Suc(Suc i)) |] \ |
|
250 \ ==> m = Suc(Suc(Suc i))"; |
|
251 test "[| i<j; j<=k; ~(l < Suc k); ~(m <= l); m=n; n <= Suc(Suc(Suc i)) |] \ |
|
252 \ ==> m = Suc(Suc(Suc i))"; |
|
253 ***) |
|