2114
|
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
|
2273
|
14 |
1. either derive a contradiction,
|
2114
|
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)) 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
|
2273
|
228 |
val lesss = flat(ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
|
2114
|
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 |
***)
|