author | paulson |
Fri, 16 Jun 2000 13:13:55 +0200 | |
changeset 9073 | 40d8dfac96b8 |
parent 8263 | 699d4ad2ced3 |
child 9420 | d4e9f60fe25a |
permissions | -rw-r--r-- |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
1 |
(* Title: Provers/Arith/fast_lin_arith.ML |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
2 |
ID: $Id$ |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
4 |
Copyright 1998 TU Munich |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
5 |
|
6062 | 6 |
A generic linear arithmetic package. |
6102 | 7 |
It provides two tactics |
8 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
9 |
lin_arith_tac: int -> tactic |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
10 |
cut_lin_arith_tac: thms -> int -> tactic |
6102 | 11 |
|
12 |
and a simplification procedure |
|
13 |
||
14 |
lin_arith_prover: Sign.sg -> thm list -> term -> thm option |
|
15 |
||
16 |
Only take premises and conclusions into account that are already (negated) |
|
17 |
(in)equations. lin_arith_prover tries to prove or disprove the term. |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
18 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
19 |
|
9073 | 20 |
(* Debugging: set Fast_Arith.trace *) |
7582 | 21 |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
22 |
(*** Data needed for setting up the linear arithmetic package ***) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
23 |
|
6102 | 24 |
signature LIN_ARITH_LOGIC = |
25 |
sig |
|
26 |
val conjI: thm |
|
27 |
val ccontr: thm (* (~ P ==> False) ==> P *) |
|
28 |
val neqE: thm (* [| m ~= n; m < n ==> P; n < m ==> P |] ==> P *) |
|
29 |
val notI: thm (* (P ==> False) ==> ~ P *) |
|
6110 | 30 |
val not_lessD: thm (* ~(m < n) ==> n <= m *) |
6128 | 31 |
val not_leD: thm (* ~(m <= n) ==> n < m *) |
6102 | 32 |
val sym: thm (* x = y ==> y = x *) |
33 |
val mk_Eq: thm -> thm |
|
34 |
val mk_Trueprop: term -> term |
|
35 |
val neg_prop: term -> term |
|
36 |
val is_False: thm -> bool |
|
6128 | 37 |
val is_nat: typ list * term -> bool |
38 |
val mk_nat_thm: Sign.sg -> term -> thm |
|
6102 | 39 |
end; |
40 |
(* |
|
41 |
mk_Eq(~in) = `in == False' |
|
42 |
mk_Eq(in) = `in == True' |
|
43 |
where `in' is an (in)equality. |
|
44 |
||
45 |
neg_prop(t) = neg if t is wrapped up in Trueprop and |
|
46 |
nt is the (logically) negated version of t, where the negation |
|
47 |
of a negative term is the term itself (no double negation!); |
|
6128 | 48 |
|
49 |
is_nat(parameter-types,t) = t:nat |
|
50 |
mk_nat_thm(t) = "0 <= t" |
|
6102 | 51 |
*) |
52 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
53 |
signature LIN_ARITH_DATA = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
54 |
sig |
6128 | 55 |
val add_mono_thms: thm list ref |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
56 |
(* [| i rel1 j; m rel2 n |] ==> i + m rel3 j + n *) |
6128 | 57 |
val lessD: thm list ref (* m < n ==> m+1 <= n *) |
58 |
val decomp: |
|
7582 | 59 |
term -> ((term*int)list * int * string * (term*int)list * int * bool)option |
60 |
val ss_ref: simpset ref |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
61 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
62 |
(* |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
63 |
decomp(`x Rel y') should yield (p,i,Rel,q,j,d) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
64 |
where Rel is one of "<", "~<", "<=", "~<=" and "=" and |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
65 |
p/q is the decomposition of the sum terms x/y into a list |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
66 |
of summand * multiplicity pairs and a constant summand and |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
67 |
d indicates if the domain is discrete. |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
68 |
|
7582 | 69 |
ss_ref must reduce contradictory <= to False. |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
70 |
It should also cancel common summands to keep <= reduced; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
71 |
otherwise <= can grow to massive proportions. |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
72 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
73 |
|
6062 | 74 |
signature FAST_LIN_ARITH = |
75 |
sig |
|
9073 | 76 |
val trace : bool ref |
6074 | 77 |
val lin_arith_prover: Sign.sg -> thm list -> term -> thm option |
6062 | 78 |
val lin_arith_tac: int -> tactic |
79 |
val cut_lin_arith_tac: thm list -> int -> tactic |
|
80 |
end; |
|
81 |
||
6102 | 82 |
functor Fast_Lin_Arith(structure LA_Logic:LIN_ARITH_LOGIC |
83 |
and LA_Data:LIN_ARITH_DATA) : FAST_LIN_ARITH = |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
84 |
struct |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
85 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
86 |
(*** A fast decision procedure ***) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
87 |
(*** Code ported from HOL Light ***) |
6056 | 88 |
(* possible optimizations: |
89 |
use (var,coeff) rep or vector rep tp save space; |
|
90 |
treat non-negative atoms separately rather than adding 0 <= atom |
|
91 |
*) |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
92 |
|
9073 | 93 |
val trace = ref false; |
94 |
||
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
95 |
datatype lineq_type = Eq | Le | Lt; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
96 |
|
6056 | 97 |
datatype injust = Asm of int |
98 |
| Nat of int (* index of atom *) |
|
6128 | 99 |
| LessD of injust |
100 |
| NotLessD of injust |
|
101 |
| NotLeD of injust |
|
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
102 |
| NotLeDD of injust |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
103 |
| Multiplied of int * injust |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
104 |
| Added of injust * injust; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
105 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
106 |
datatype lineq = Lineq of int * lineq_type * int list * injust; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
107 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
108 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
109 |
(* Calculate new (in)equality type after addition. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
110 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
111 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
112 |
fun find_add_type(Eq,x) = x |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
113 |
| find_add_type(x,Eq) = x |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
114 |
| find_add_type(_,Lt) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
115 |
| find_add_type(Lt,_) = Lt |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
116 |
| find_add_type(Le,Le) = Le; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
117 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
118 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
119 |
(* Multiply out an (in)equation. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
120 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
121 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
122 |
fun multiply_ineq n (i as Lineq(k,ty,l,just)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
123 |
if n = 1 then i |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
124 |
else if n = 0 andalso ty = Lt then sys_error "multiply_ineq" |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
125 |
else if n < 0 andalso (ty=Le orelse ty=Lt) then sys_error "multiply_ineq" |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
126 |
else Lineq(n * k,ty,map (apl(n,op * )) l,Multiplied(n,just)); |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
127 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
128 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
129 |
(* Add together (in)equations. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
130 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
131 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
132 |
fun add_ineq (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
133 |
let val l = map2 (op +) (l1,l2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
134 |
in Lineq(k1+k2,find_add_type(ty1,ty2),l,Added(just1,just2)) end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
135 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
136 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
137 |
(* Elimination of variable between a single pair of (in)equations. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
138 |
(* If they're both inequalities, 1st coefficient must be +ve, 2nd -ve. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
139 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
140 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
141 |
fun gcd x y = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
142 |
let fun gxd x y = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
143 |
if y = 0 then x else gxd y (x mod y) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
144 |
in if x < y then gxd y x else gxd x y end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
145 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
146 |
fun lcm x y = (x * y) div gcd x y; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
147 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
148 |
fun el 0 (h::_) = h |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
149 |
| el n (_::t) = el (n - 1) t |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
150 |
| el _ _ = sys_error "el"; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
151 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
152 |
fun elim_var v (i1 as Lineq(k1,ty1,l1,just1)) (i2 as Lineq(k2,ty2,l2,just2)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
153 |
let val c1 = el v l1 and c2 = el v l2 |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
154 |
val m = lcm (abs c1) (abs c2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
155 |
val m1 = m div (abs c1) and m2 = m div (abs c2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
156 |
val (n1,n2) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
157 |
if (c1 >= 0) = (c2 >= 0) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
158 |
then if ty1 = Eq then (~m1,m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
159 |
else if ty2 = Eq then (m1,~m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
160 |
else sys_error "elim_var" |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
161 |
else (m1,m2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
162 |
val (p1,p2) = if ty1=Eq andalso ty2=Eq andalso (n1 = ~1 orelse n2 = ~1) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
163 |
then (~n1,~n2) else (n1,n2) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
164 |
in add_ineq (multiply_ineq n1 i1) (multiply_ineq n2 i2) end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
165 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
166 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
167 |
(* The main refutation-finding code. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
168 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
169 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
170 |
fun is_trivial (Lineq(_,_,l,_)) = forall (fn i => i=0) l; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
171 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
172 |
fun is_answer (ans as Lineq(k,ty,l,_)) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
173 |
case ty of Eq => k <> 0 | Le => k > 0 | Lt => k >= 0; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
174 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
175 |
fun calc_blowup l = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
176 |
let val (p,n) = partition (apl(0,op<)) (filter (apl(0,op<>)) l) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
177 |
in (length p) * (length n) end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
178 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
179 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
180 |
(* Main elimination code: *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
181 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
182 |
(* (1) Looks for immediate solutions (false assertions with no variables). *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
183 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
184 |
(* (2) If there are any equations, picks a variable with the lowest absolute *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
185 |
(* coefficient in any of them, and uses it to eliminate. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
186 |
(* *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
187 |
(* (3) Otherwise, chooses a variable in the inequality to minimize the *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
188 |
(* blowup (number of consequences generated) and eliminates it. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
189 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
190 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
191 |
fun allpairs f xs ys = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
192 |
flat(map (fn x => map (fn y => f x y) ys) xs); |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
193 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
194 |
fun extract_first p = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
195 |
let fun extract xs (y::ys) = if p y then (Some y,xs@ys) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
196 |
else extract (y::xs) ys |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
197 |
| extract xs [] = (None,xs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
198 |
in extract [] end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
199 |
|
6056 | 200 |
fun print_ineqs ineqs = |
9073 | 201 |
if !trace then |
202 |
writeln(cat_lines(""::map (fn Lineq(c,t,l,_) => |
|
203 |
string_of_int c ^ |
|
204 |
(case t of Eq => " = " | Lt=> " < " | Le => " <= ") ^ |
|
205 |
commas(map string_of_int l)) ineqs)) |
|
206 |
else (); |
|
6056 | 207 |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
208 |
fun elim ineqs = |
9073 | 209 |
let val dummy = print_ineqs ineqs; |
6056 | 210 |
val (triv,nontriv) = partition is_trivial ineqs in |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
211 |
if not(null triv) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
212 |
then case find_first is_answer triv of |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
213 |
None => elim nontriv | some => some |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
214 |
else |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
215 |
if null nontriv then None else |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
216 |
let val (eqs,noneqs) = partition (fn (Lineq(_,ty,_,_)) => ty=Eq) nontriv in |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
217 |
if not(null eqs) then |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
218 |
let val clist = foldl (fn (cs,Lineq(_,_,l,_)) => l union cs) ([],eqs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
219 |
val sclist = sort (fn (x,y) => int_ord(abs(x),abs(y))) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
220 |
(filter (fn i => i<>0) clist) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
221 |
val c = hd sclist |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
222 |
val (Some(eq as Lineq(_,_,ceq,_)),othereqs) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
223 |
extract_first (fn Lineq(_,_,l,_) => c mem l) eqs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
224 |
val v = find_index (fn k => k=c) ceq |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
225 |
val (ioth,roth) = partition (fn (Lineq(_,_,l,_)) => el v l = 0) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
226 |
(othereqs @ noneqs) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
227 |
val others = map (elim_var v eq) roth @ ioth |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
228 |
in elim others end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
229 |
else |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
230 |
let val lists = map (fn (Lineq(_,_,l,_)) => l) noneqs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
231 |
val numlist = 0 upto (length(hd lists) - 1) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
232 |
val coeffs = map (fn i => map (el i) lists) numlist |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
233 |
val blows = map calc_blowup coeffs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
234 |
val iblows = blows ~~ numlist |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
235 |
val nziblows = filter (fn (i,_) => i<>0) iblows |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
236 |
in if null nziblows then None else |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
237 |
let val (c,v) = hd(sort (fn (x,y) => int_ord(fst(x),fst(y))) nziblows) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
238 |
val (no,yes) = partition (fn (Lineq(_,_,l,_)) => el v l = 0) ineqs |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
239 |
val (pos,neg) = partition(fn (Lineq(_,_,l,_)) => el v l > 0) yes |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
240 |
in elim (no @ allpairs (elim_var v) pos neg) end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
241 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
242 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
243 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
244 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
245 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
246 |
(* Translate back a proof. *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
247 |
(* ------------------------------------------------------------------------- *) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
248 |
|
9073 | 249 |
fun trace_thm msg th = |
250 |
if !trace then (writeln msg; prth th) else th; |
|
251 |
||
252 |
fun trace_msg msg = |
|
253 |
if !trace then writeln msg else (); |
|
254 |
||
6056 | 255 |
(* FIXME OPTIMIZE!!!! |
256 |
Addition/Multiplication need i*t representation rather than t+t+... |
|
257 |
||
258 |
Simplification may detect a contradiction 'prematurely' due to type |
|
259 |
information: n+1 <= 0 is simplified to False and does not need to be crossed |
|
260 |
with 0 <= n. |
|
261 |
*) |
|
262 |
local |
|
263 |
exception FalseE of thm |
|
264 |
in |
|
6074 | 265 |
fun mkthm sg asms just = |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
266 |
let val atoms = foldl (fn (ats,(lhs,_,_,rhs,_,_)) => |
6056 | 267 |
map fst lhs union (map fst rhs union ats)) |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
268 |
([], mapfilter (LA_Data.decomp o concl_of) asms) |
6056 | 269 |
|
270 |
fun addthms thm1 thm2 = |
|
6102 | 271 |
let val conj = thm1 RS (thm2 RS LA_Logic.conjI) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
272 |
in the(get_first (fn th => Some(conj RS th) handle _ => None) |
6128 | 273 |
(!LA_Data.add_mono_thms)) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
274 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
275 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
276 |
fun multn(n,thm) = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
277 |
let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th) |
6102 | 278 |
in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
279 |
|
6056 | 280 |
fun simp thm = |
7582 | 281 |
let val thm' = simplify (!LA_Data.ss_ref) thm |
6102 | 282 |
in if LA_Logic.is_False thm' then raise FalseE thm' else thm' end |
6056 | 283 |
|
9073 | 284 |
fun mk(Asm i) = trace_thm "Asm" (nth_elem(i,asms)) |
285 |
| mk(Nat(i)) = (trace_msg "Nat"; |
|
286 |
LA_Logic.mk_nat_thm sg (nth_elem(i,atoms))) |
|
287 |
| mk(LessD(j)) = trace_thm "L" (hd([mk j] RL !LA_Data.lessD)) |
|
288 |
| mk(NotLeD(j)) = trace_thm "NLe" (mk j RS LA_Logic.not_leD) |
|
289 |
| mk(NotLeDD(j)) = trace_thm "NLeD" (hd([mk j RS LA_Logic.not_leD] RL |
|
290 |
!LA_Data.lessD)) |
|
291 |
| mk(NotLessD(j)) = trace_thm "NL" (mk j RS LA_Logic.not_lessD) |
|
292 |
| mk(Added(j1,j2)) = simp (trace_thm "+" (addthms (mk j1) (mk j2))) |
|
293 |
| mk(Multiplied(n,j)) = (trace_msg "*"; multn(n,mk j)) |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
294 |
|
9073 | 295 |
in trace_msg "mkthm"; |
7582 | 296 |
simplify (!LA_Data.ss_ref) (mk just) handle FalseE thm => thm end |
6056 | 297 |
end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
298 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
299 |
fun coeff poly atom = case assoc(poly,atom) of None => 0 | Some i => i; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
300 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
301 |
fun mklineq atoms = |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
302 |
let val n = length atoms in |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
303 |
fn ((lhs,i,rel,rhs,j,discrete),k) => |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
304 |
let val lhsa = map (coeff lhs) atoms |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
305 |
and rhsa = map (coeff rhs) atoms |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
306 |
val diff = map2 (op -) (rhsa,lhsa) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
307 |
val c = i-j |
6056 | 308 |
val just = Asm k |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
309 |
in case rel of |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
310 |
"<=" => Some(Lineq(c,Le,diff,just)) |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
311 |
| "~<=" => if discrete |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
312 |
then Some(Lineq(1-c,Le,map (op ~) diff,NotLeDD(just))) |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
313 |
else Some(Lineq(~c,Lt,map (op ~) diff,NotLeD(just))) |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
314 |
| "<" => if discrete |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
315 |
then Some(Lineq(c+1,Le,diff,LessD(just))) |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
316 |
else Some(Lineq(c,Lt,diff,just)) |
6128 | 317 |
| "~<" => Some(Lineq(~c,Le,map (op~) diff,NotLessD(just))) |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
318 |
| "=" => Some(Lineq(c,Eq,diff,just)) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
319 |
| "~=" => None |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
320 |
| _ => sys_error("mklineq" ^ rel) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
321 |
end |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
322 |
end; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
323 |
|
6056 | 324 |
fun mknat pTs ixs (atom,i) = |
6128 | 325 |
if LA_Logic.is_nat(pTs,atom) |
6056 | 326 |
then let val l = map (fn j => if j=i then 1 else 0) ixs |
327 |
in Some(Lineq(0,Le,l,Nat(i))) end |
|
328 |
else None |
|
329 |
||
330 |
fun abstract pTs items = |
|
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
331 |
let val atoms = foldl (fn (ats,((lhs,_,_,rhs,_,_),_)) => |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
332 |
(map fst lhs) union ((map fst rhs) union ats)) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
333 |
([],items) |
6056 | 334 |
val ixs = 0 upto (length(atoms)-1) |
335 |
val iatoms = atoms ~~ ixs |
|
336 |
in mapfilter (mklineq atoms) items @ mapfilter (mknat pTs ixs) iatoms end; |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
337 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
338 |
(* Ordinary refutation *) |
6074 | 339 |
fun refute1(pTs,items) = |
340 |
(case elim (abstract pTs items) of |
|
341 |
None => [] |
|
342 |
| Some(Lineq(_,_,_,j)) => [j]); |
|
343 |
||
344 |
fun refute1_tac(i,just) = |
|
345 |
fn state => |
|
346 |
let val sg = #sign(rep_thm state) |
|
6102 | 347 |
in resolve_tac [LA_Logic.notI,LA_Logic.ccontr] i THEN |
6074 | 348 |
METAHYPS (fn asms => rtac (mkthm sg asms just) 1) i |
349 |
end |
|
350 |
state; |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
351 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
352 |
(* Double refutation caused by equality in conclusion *) |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
353 |
fun refute2(pTs,items, (rhs,i,_,lhs,j,d), nHs) = |
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
354 |
(case elim (abstract pTs (items@[((rhs,i,"<",lhs,j,d),nHs)])) of |
6074 | 355 |
None => [] |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
356 |
| Some(Lineq(_,_,_,j1)) => |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
357 |
(case elim (abstract pTs (items@[((lhs,j,"<",rhs,i,d),nHs)])) of |
6074 | 358 |
None => [] |
359 |
| Some(Lineq(_,_,_,j2)) => [j1,j2])); |
|
360 |
||
361 |
fun refute2_tac(i,just1,just2) = |
|
362 |
fn state => |
|
363 |
let val sg = #sign(rep_thm state) |
|
6102 | 364 |
in rtac LA_Logic.ccontr i THEN rotate_tac ~1 i THEN etac LA_Logic.neqE i THEN |
6074 | 365 |
METAHYPS (fn asms => rtac (mkthm sg asms just1) 1) i THEN |
366 |
METAHYPS (fn asms => rtac (mkthm sg asms just2) 1) i |
|
367 |
end |
|
368 |
state; |
|
369 |
||
370 |
fun prove(pTs,Hs,concl) = |
|
371 |
let val nHs = length Hs |
|
372 |
val ixHs = Hs ~~ (0 upto (nHs-1)) |
|
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
373 |
val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of |
6074 | 374 |
None => None | Some(it) => Some(it,i)) ixHs |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
375 |
in case LA_Data.decomp concl of |
6074 | 376 |
None => if null Hitems then [] else refute1(pTs,Hitems) |
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
377 |
| Some(citem as (r,i,rel,l,j,d)) => |
6074 | 378 |
if rel = "=" |
379 |
then refute2(pTs,Hitems,citem,nHs) |
|
380 |
else let val neg::rel0 = explode rel |
|
381 |
val nrel = if neg = "~" then implode rel0 else "~"^rel |
|
7551
8e934d1a9ac6
Now distinguishes discrete from non-distrete types.
nipkow
parents:
6128
diff
changeset
|
382 |
in refute1(pTs, Hitems@[((r,i,nrel,l,j,d),nHs)]) end |
6074 | 383 |
end; |
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
384 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
385 |
(* |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
386 |
Fast but very incomplete decider. Only premises and conclusions |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
387 |
that are already (negated) (in)equations are taken into account. |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
388 |
*) |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
389 |
val lin_arith_tac = SUBGOAL (fn (A,n) => |
6056 | 390 |
let val pTs = rev(map snd (Logic.strip_params A)) |
391 |
val Hs = Logic.strip_assums_hyp A |
|
6074 | 392 |
val concl = Logic.strip_assums_concl A |
393 |
in case prove(pTs,Hs,concl) of |
|
394 |
[j] => refute1_tac(n,j) |
|
395 |
| [j1,j2] => refute2_tac(n,j1,j2) |
|
396 |
| _ => no_tac |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
397 |
end); |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
398 |
|
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
399 |
fun cut_lin_arith_tac thms i = cut_facts_tac thms i THEN lin_arith_tac i; |
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
400 |
|
6079 | 401 |
fun prover1(just,sg,thms,concl,pos) = |
6102 | 402 |
let val nconcl = LA_Logic.neg_prop concl |
6074 | 403 |
val cnconcl = cterm_of sg nconcl |
404 |
val Fthm = mkthm sg (thms @ [assume cnconcl]) just |
|
6102 | 405 |
val contr = if pos then LA_Logic.ccontr else LA_Logic.notI |
406 |
in Some(LA_Logic.mk_Eq ((implies_intr cnconcl Fthm) COMP contr)) end |
|
6074 | 407 |
handle _ => None; |
408 |
||
409 |
(* handle thm with equality conclusion *) |
|
410 |
fun prover2(just1,just2,sg,thms,concl) = |
|
6102 | 411 |
let val nconcl = LA_Logic.neg_prop concl (* m ~= n *) |
6074 | 412 |
val cnconcl = cterm_of sg nconcl |
413 |
val neqthm = assume cnconcl |
|
6102 | 414 |
val casethm = neqthm COMP LA_Logic.neqE (* [|m<n ==> R; n<m ==> R|] ==> R *) |
6074 | 415 |
val [lessimp1,lessimp2] = prems_of casethm |
416 |
val less1 = fst(Logic.dest_implies lessimp1) (* m<n *) |
|
417 |
and less2 = fst(Logic.dest_implies lessimp2) (* n<m *) |
|
418 |
val cless1 = cterm_of sg less1 and cless2 = cterm_of sg less2 |
|
419 |
val thm1 = mkthm sg (thms @ [assume cless1]) just1 |
|
420 |
and thm2 = mkthm sg (thms @ [assume cless2]) just2 |
|
421 |
val dthm1 = implies_intr cless1 thm1 and dthm2 = implies_intr cless2 thm2 |
|
422 |
val thm = dthm2 COMP (dthm1 COMP casethm) |
|
6102 | 423 |
in Some(LA_Logic.mk_Eq ((implies_intr cnconcl thm) COMP LA_Logic.ccontr)) end |
6074 | 424 |
handle _ => None; |
425 |
||
6079 | 426 |
(* PRE: concl is not negated! *) |
6074 | 427 |
fun lin_arith_prover sg thms concl = |
428 |
let val Hs = map (#prop o rep_thm) thms |
|
6102 | 429 |
val Tconcl = LA_Logic.mk_Trueprop concl |
6074 | 430 |
in case prove([],Hs,Tconcl) of |
6079 | 431 |
[j] => prover1(j,sg,thms,Tconcl,true) |
6074 | 432 |
| [j1,j2] => prover2(j1,j2,sg,thms,Tconcl) |
6102 | 433 |
| _ => let val nTconcl = LA_Logic.neg_prop Tconcl |
6079 | 434 |
in case prove([],Hs,nTconcl) of |
435 |
[j] => prover1(j,sg,thms,nTconcl,false) |
|
436 |
(* [_,_] impossible because of negation *) |
|
437 |
| _ => None |
|
438 |
end |
|
5982
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset
|
439 |
end; |
6074 | 440 |
|
441 |
end; |