13735
|
1 |
(*
|
|
2 |
Title: Transitivity reasoner for linear orders
|
|
3 |
Id: $Id$
|
|
4 |
Author: Clemens Ballarin, started 8 November 2002
|
|
5 |
Copyright: TU Muenchen
|
|
6 |
*)
|
|
7 |
|
|
8 |
(***
|
|
9 |
This is a very simple package for transitivity reasoning over linear orders.
|
|
10 |
Simple means exponential time (and space) in the number of premises.
|
|
11 |
Should be replaced by a graph-theoretic algorithm.
|
|
12 |
|
|
13 |
The package provides a tactic trans_tac that uses all premises of the form
|
|
14 |
|
|
15 |
t = u, t < u, t <= u, ~(t < u) and ~(t <= u)
|
|
16 |
|
|
17 |
to
|
|
18 |
1. either derive a contradiction,
|
|
19 |
in which case the conclusion can be any term,
|
|
20 |
2. or prove the conclusion, which must be of the same form as the premises.
|
|
21 |
|
|
22 |
To get rid of ~= in the premises, it is advisable to use an elimination
|
|
23 |
rule of the form
|
|
24 |
|
|
25 |
[| t ~= u; t < u ==> P; u < t ==> P |] ==> P.
|
|
26 |
|
|
27 |
The package is implemented as an ML functor and thus not limited to the
|
|
28 |
relation <= and friends. It can be instantiated to any total order ---
|
|
29 |
for example, the divisibility relation "dvd".
|
|
30 |
***)
|
|
31 |
|
|
32 |
(*** Credits ***
|
|
33 |
|
|
34 |
This package is closely based on a (no longer used) transitivity reasoner for
|
|
35 |
the natural numbers, which was written by Tobias Nipkow.
|
|
36 |
|
|
37 |
****************)
|
|
38 |
|
|
39 |
signature LESS_ARITH =
|
|
40 |
sig
|
|
41 |
val less_reflE: thm (* x < x ==> P *)
|
|
42 |
val le_refl: thm (* x <= x *)
|
|
43 |
val less_imp_le: thm (* x <= y ==> x < y *)
|
|
44 |
val not_lessI: thm (* y <= x ==> ~(x < y) *)
|
|
45 |
val not_leI: thm (* y < x ==> ~(x <= y) *)
|
|
46 |
val not_lessD: thm (* ~(x < y) ==> y <= x *)
|
|
47 |
val not_leD: thm (* ~(x <= y) ==> y < x *)
|
|
48 |
val eqI: thm (* [| x <= y; y <= x |] ==> x = y *)
|
|
49 |
val eqD1: thm (* x = y ==> x <= y *)
|
|
50 |
val eqD2: thm (* x = y ==> y <= x *)
|
|
51 |
val less_trans: thm (* [| x <= y; y <= z |] ==> x <= z *)
|
|
52 |
val less_le_trans: thm (* [| x <= y; y < z |] ==> x < z *)
|
|
53 |
val le_less_trans: thm (* [| x < y; y <= z |] ==> x < z *)
|
|
54 |
val le_trans: thm (* [| x < y; y < z |] ==> x < z *)
|
|
55 |
val decomp: term -> (term * string * term) option
|
|
56 |
(* decomp (`x Rel y') should yield (x, Rel, y)
|
|
57 |
where Rel is one of "<", "<=", "~<", "~<=", "=" and "~="
|
|
58 |
other relation symbols are ignored *)
|
|
59 |
end;
|
|
60 |
|
|
61 |
signature TRANS_TAC =
|
|
62 |
sig
|
|
63 |
val trans_tac: int -> tactic
|
|
64 |
end;
|
|
65 |
|
|
66 |
functor Trans_Tac_Fun (Less: LESS_ARITH): TRANS_TAC =
|
|
67 |
struct
|
|
68 |
|
|
69 |
(*** Proof objects ***)
|
|
70 |
|
|
71 |
datatype proof
|
|
72 |
= Asm of int
|
|
73 |
| Thm of proof list * thm;
|
|
74 |
|
|
75 |
(* Turn proof objects into theorems *)
|
|
76 |
|
|
77 |
fun prove asms =
|
|
78 |
let fun pr (Asm i) = nth_elem (i, asms)
|
|
79 |
| pr (Thm (prfs, thm)) = (map pr prfs) MRS thm
|
|
80 |
in pr end;
|
|
81 |
|
|
82 |
(*** Exceptions ***)
|
|
83 |
|
|
84 |
exception Contr of proof; (* Raised when contradiction is found *)
|
|
85 |
|
|
86 |
exception Cannot; (* Raised when goal cannot be proved *)
|
|
87 |
|
|
88 |
(*** Internal representation of inequalities ***)
|
|
89 |
|
|
90 |
datatype less
|
|
91 |
= Less of term * term * proof
|
|
92 |
| Le of term * term * proof;
|
|
93 |
|
|
94 |
fun lower (Less (x, _, _)) = x
|
|
95 |
| lower (Le (x, _, _)) = x;
|
|
96 |
|
|
97 |
fun upper (Less (_, y, _)) = y
|
|
98 |
| upper (Le (_, y, _)) = y;
|
|
99 |
|
|
100 |
infix subsumes;
|
|
101 |
|
|
102 |
fun (Less (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
|
|
103 |
| (Less (x, y, _)) subsumes (Less (x', y', _)) = (x = x' andalso y = y')
|
|
104 |
| (Le (x, y, _)) subsumes (Le (x', y', _)) = (x = x' andalso y = y')
|
|
105 |
| _ subsumes _ = false;
|
|
106 |
|
|
107 |
fun trivial (Le (x, x', _)) = (x = x')
|
|
108 |
| trivial _ = false;
|
|
109 |
|
|
110 |
(*** Transitive closure ***)
|
|
111 |
|
|
112 |
fun add new =
|
|
113 |
let fun adds([], news) = new::news
|
|
114 |
| adds(old::olds, news) = if new subsumes old then adds(olds, news)
|
|
115 |
else adds(olds, old::news)
|
|
116 |
in adds end;
|
|
117 |
|
|
118 |
fun ctest (less as Less (x, x', p)) =
|
|
119 |
if x = x' then raise Contr (Thm ([p], Less.less_reflE))
|
|
120 |
else less
|
|
121 |
| ctest less = less;
|
|
122 |
|
|
123 |
fun mktrans (Less (x, _, p), Less (_, z, q)) =
|
|
124 |
Less (x, z, Thm([p, q], Less.less_trans))
|
|
125 |
| mktrans (Less (x, _, p), Le (_, z, q)) =
|
|
126 |
Less (x, z, Thm([p, q], Less.less_le_trans))
|
|
127 |
| mktrans (Le (x, _, p), Less (_, z, q)) =
|
|
128 |
Less (x, z, Thm([p, q], Less.le_less_trans))
|
|
129 |
| mktrans (Le (x, _, p), Le (_, z, q)) =
|
|
130 |
Le (x, z, Thm([p, q], Less.le_trans));
|
|
131 |
|
|
132 |
fun trans new olds =
|
|
133 |
let fun tr (news, old) =
|
|
134 |
if upper old = lower new then mktrans (old, new)::news
|
|
135 |
else if upper new = lower old then mktrans (new, old)::news
|
|
136 |
else news
|
|
137 |
in foldl tr ([], olds) end;
|
|
138 |
|
|
139 |
fun close1 olds new =
|
|
140 |
if trivial new orelse exists (fn old => old subsumes new) olds then olds
|
|
141 |
else let val news = trans new olds
|
|
142 |
in close (add new (olds, [])) news end
|
|
143 |
and close olds [] = olds
|
|
144 |
| close olds (new::news) = close (close1 olds (ctest new)) news;
|
|
145 |
|
|
146 |
(*** Solving and proving goals ***)
|
|
147 |
|
|
148 |
(* Recognise and solve trivial goal *)
|
|
149 |
|
|
150 |
fun triv_sol (Le (x, x', _)) =
|
|
151 |
if x = x' then Some (Thm ([], Less.le_refl))
|
|
152 |
else None
|
|
153 |
| triv_sol _ = None;
|
|
154 |
|
|
155 |
(* Solve less starting from facts *)
|
|
156 |
|
|
157 |
fun solve facts less =
|
|
158 |
case triv_sol less of
|
|
159 |
None => (case (Library.find_first (fn fact => fact subsumes less) facts, less) of
|
|
160 |
(None, _) => raise Cannot
|
|
161 |
| (Some (Less (_, _, p)), Less _) => p
|
|
162 |
| (Some (Le (_, _, p)), Less _) =>
|
|
163 |
error "trans_tac/solve: internal error: le cannot subsume less"
|
|
164 |
| (Some (Less (_, _, p)), Le _) => Thm ([p], Less.less_imp_le)
|
|
165 |
| (Some (Le (_, _, p)), Le _) => p)
|
|
166 |
| Some prf => prf;
|
|
167 |
|
|
168 |
(* Turn term t into Less or Le; n is position of t in list of assumptions *)
|
|
169 |
|
|
170 |
fun mkasm (t, n) =
|
|
171 |
case Less.decomp t of
|
|
172 |
Some (x, rel, y) => (case rel of
|
|
173 |
"<" => [Less (x, y, Asm n)]
|
|
174 |
| "~<" => [Le (y, x, Thm ([Asm n], Less.not_lessD))]
|
|
175 |
| "<=" => [Le (x, y, Asm n)]
|
|
176 |
| "~<=" => [Less (y, x, Thm ([Asm n], Less.not_leD))]
|
|
177 |
| "=" => [Le (x, y, Thm ([Asm n], Less.eqD1)),
|
|
178 |
Le (x, y, Thm ([Asm n], Less.eqD1))]
|
|
179 |
| "~=" => []
|
|
180 |
| _ => error ("trans_tac/mkasm: unknown relation " ^ rel))
|
|
181 |
| None => [];
|
|
182 |
|
|
183 |
(* Turn goal t into a pair (goals, proof) where goals is a list of
|
|
184 |
Le/Less-subgoals to solve, and proof the validation that proves the concl t
|
|
185 |
Asm ~1 is dummy (denotes a goal)
|
|
186 |
*)
|
|
187 |
|
|
188 |
fun mkconcl t =
|
|
189 |
case Less.decomp t of
|
|
190 |
Some (x, rel, y) => (case rel of
|
|
191 |
"<" => ([Less (x, y, Asm ~1)], Asm 0)
|
|
192 |
| "~<" => ([Le (y, x, Asm ~1)], Thm ([Asm 0], Less.not_lessI))
|
|
193 |
| "<=" => ([Le (x, y, Asm ~1)], Asm 0)
|
|
194 |
| "~<=" => ([Less (y, x, Asm ~1)], Thm ([Asm 0], Less.not_leI))
|
|
195 |
| "=" => ([Le (x, y, Asm ~1), Le (y, x, Asm ~1)],
|
|
196 |
Thm ([Asm 0, Asm 1], Less.eqI))
|
|
197 |
| _ => raise Cannot)
|
|
198 |
| None => raise Cannot;
|
|
199 |
|
|
200 |
val trans_tac = SUBGOAL (fn (A, n) =>
|
|
201 |
let val Hs = Logic.strip_assums_hyp A
|
|
202 |
val C = Logic.strip_assums_concl A
|
|
203 |
val lesss = flat (ListPair.map mkasm (Hs, 0 upto (length Hs - 1)))
|
|
204 |
val clesss = close [] lesss
|
|
205 |
val (subgoals, prf) = mkconcl C
|
|
206 |
val prfs = map (solve clesss) subgoals
|
|
207 |
in METAHYPS (fn asms =>
|
|
208 |
let val thms = map (prove asms) prfs
|
|
209 |
in rtac (prove thms prf) 1 end) n
|
|
210 |
end
|
|
211 |
handle Contr p => METAHYPS (fn asms => rtac (prove asms p) 1) n
|
|
212 |
| Cannot => no_tac);
|
|
213 |
|
|
214 |
end;
|