author  nipkow 
Fri, 27 Nov 1998 16:54:59 +0100  
changeset 5982  aeb97860d352 
child 6056  b21813d1b701 
permissions  rwrr 
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 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

6 
A generic linear arithmetic package. At the moment only used for nat. 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

7 
The two tactics provided: 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

8 
lin_arith_tac: int > tactic 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

9 
cut_lin_arith_tac: thms > int > tactic 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

10 
Only take premises and conclusions into account 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

11 
that are already (negated) (in)equations. 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

12 
*) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

13 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

14 
(*** 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

15 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

16 
signature LIN_ARITH_DATA = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

17 
sig 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

18 
val add_mono_thms: thm list 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

19 
(* [ i rel1 j; m rel2 n ] ==> i + m rel3 j + n *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

20 
val conjI: thm 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

21 
val ccontr: thm (* (~ P ==> False) ==> P *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

22 
val lessD: thm (* m < n ==> Suc m <= n *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

23 
val nat_neqE: thm (* [ m ~= n; m < n ==> P; n < m ==> P ] ==> P *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

24 
val notI: thm (* (P ==> False) ==> ~ P *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

25 
val not_leD: thm (* ~(m <= n) ==> Suc n <= m *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

26 
val not_lessD: thm (* ~(m < n) ==> n < m *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

27 
val sym: thm (* x = y ==> y = x *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

28 
val decomp: term > 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

29 
((term * int)list * int * string * (term * int)list * int)option 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

30 
val simp: thm > thm 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

31 
end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

32 
(* 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

33 
decomp(`x Rel y') should yield (p,i,Rel,q,j) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

34 
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

35 
p/q is the decomposition of the sum terms x/y into a list 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

36 
of summand * multiplicity pairs and a constant summand. 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

37 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

38 
simp must reduce contradictory <= to False. 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

39 
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

40 
otherwise <= can grow to massive proportions. 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

41 
*) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

42 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

43 
functor Fast_Lin_Arith(LA_Data:LIN_ARITH_DATA) = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

44 
struct 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

45 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

46 
(*** A fast decision procedure ***) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

47 
(*** Code ported from HOL Light ***) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

48 
(* possible optimizations: eliminate eqns first; use (var,coeff) rep *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

49 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

50 
datatype lineq_type = Eq  Le  Lt; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

51 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

52 
datatype injust = Given of int 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

53 
 Fwd of injust * thm 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

54 
 Multiplied of int * injust 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

55 
 Added of injust * injust; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

56 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

57 
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

58 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

59 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

60 
(* 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

61 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

62 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

63 
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

64 
 find_add_type(x,Eq) = x 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

65 
 find_add_type(_,Lt) = Lt 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

66 
 find_add_type(Lt,_) = Lt 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

67 
 find_add_type(Le,Le) = Le; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

68 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

69 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

70 
(* Multiply out an (in)equation. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

71 
(*  *) 
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 
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

74 
if n = 1 then i 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

75 
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

76 
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

77 
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

78 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

79 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

80 
(* Add together (in)equations. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

81 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

82 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

83 
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

84 
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

85 
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

86 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

87 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

88 
(* 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

89 
(* 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

90 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

91 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

92 
fun gcd x y = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

93 
let fun gxd x y = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

94 
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

95 
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

96 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

97 
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

98 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

99 
fun el 0 (h::_) = h 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

100 
 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

101 
 el _ _ = sys_error "el"; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

102 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

103 
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

104 
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

105 
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

106 
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

107 
val (n1,n2) = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

108 
if (c1 >= 0) = (c2 >= 0) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

109 
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

110 
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

111 
else sys_error "elim_var" 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

112 
else (m1,m2) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

113 
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

114 
then (~n1,~n2) else (n1,n2) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

115 
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

116 

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 
(* The main refutationfinding code. *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

119 
(*  *) 
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 
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

122 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

123 
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

124 
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

125 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

126 
fun calc_blowup l = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

127 
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

128 
in (length p) * (length n) end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

129 

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 
(* Main elimination code: *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

132 
(* *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

133 
(* (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

134 
(* *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

135 
(* (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

136 
(* 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

137 
(* *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

138 
(* (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

139 
(* 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

140 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

141 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

142 
fun allpairs f xs ys = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

143 
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

144 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

145 
fun extract_first p = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

146 
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

147 
else extract (y::xs) ys 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

148 
 extract xs [] = (None,xs) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

149 
in extract [] end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

150 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

151 
fun elim ineqs = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

152 
let val (triv,nontriv) = partition is_trivial ineqs in 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

153 
if not(null triv) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

154 
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

155 
None => elim nontriv  some => some 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

156 
else 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

157 
if null nontriv then None else 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

158 
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

159 
if not(null eqs) then 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

160 
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

161 
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

162 
(filter (fn i => i<>0) clist) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

163 
val c = hd sclist 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

164 
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

165 
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

166 
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

167 
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

168 
(othereqs @ noneqs) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

169 
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

170 
in elim others end 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

171 
else 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

172 
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

173 
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

174 
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

175 
val blows = map calc_blowup coeffs 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

176 
val iblows = blows ~~ numlist 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

177 
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

178 
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

179 
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

180 
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

181 
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

182 
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

183 
end 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

184 
end 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

185 
end; 
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 
(*  *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

188 
(* Translate back a proof. *) 
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 
(* FIXME OPTIMIZE!!!! *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

192 
fun mkproof asms just = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

193 
let fun addthms thm1 thm2 = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

194 
let val conj = thm1 RS (thm2 RS LA_Data.conjI) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

195 
in the(get_first (fn th => Some(conj RS th) handle _ => None) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

196 
LA_Data.add_mono_thms) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

197 
end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

198 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

199 
fun multn(n,thm) = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

200 
let fun mul(i,th) = if i=1 then th else mul(i1, addthms thm th) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

201 
in if n < 0 then mul(~n,thm) RS LA_Data.sym else mul(n,thm) end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

202 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

203 
fun mk(Given i) = nth_elem(i,asms) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

204 
 mk(Fwd(j,thm)) = mk j RS thm 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

205 
 mk(Added(j1,j2)) = LA_Data.simp(addthms (mk j1) (mk j2)) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

206 
 mk(Multiplied(n,j)) = multn(n,mk j) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

207 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

208 
in LA_Data.simp(mk just) end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

209 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

210 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

211 
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

212 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

213 
fun mklineq atoms = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

214 
let val n = length atoms in 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

215 
fn ((lhs,i,rel,rhs,j),k) => 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

216 
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

217 
and rhsa = map (coeff rhs) atoms 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

218 
val diff = map2 (op ) (rhsa,lhsa) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

219 
val c = ij 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

220 
val just = Given k 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

221 
in case rel of 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

222 
"<=" => Some(Lineq(c,Le,diff,just)) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

223 
 "~<=" => Some(Lineq(1c,Le,map (op ~) diff,Fwd(just,LA_Data.not_leD))) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

224 
 "<" => Some(Lineq(c+1,Le,diff,Fwd(just,LA_Data.lessD))) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

225 
 "~<" => Some(Lineq(~c,Le,map (op~) diff,Fwd(just,LA_Data.not_lessD))) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

226 
 "=" => Some(Lineq(c,Eq,diff,just)) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

227 
 "~=" => None 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

228 
 _ => sys_error("mklineq" ^ rel) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

229 
end 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

230 
end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

231 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

232 
fun abstract items = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

233 
let val atoms = foldl (fn (ats,((lhs,_,_,rhs,_),_)) => 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

234 
(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

235 
([],items) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

236 
in mapfilter (mklineq atoms) items end; 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

237 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

238 
(* Ordinary refutation *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

239 
fun refute1_tac items = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

240 
let val lineqs = abstract items 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

241 
in case elim lineqs of 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

242 
None => K no_tac 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

243 
 Some(Lineq(_,_,_,j)) => 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

244 
resolve_tac [LA_Data.notI,LA_Data.ccontr] THEN' 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

245 
METAHYPS (fn asms => rtac (mkproof asms j) 1) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

246 
end; 
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 
(* Double refutation caused by equality in conclusion *) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

249 
fun refute2_tac items (rhs,i,_,lhs,j) nHs = 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

250 
(case elim (abstract(items@[((rhs,i,"<",lhs,j),nHs)])) of 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

251 
None => K no_tac 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

252 
 Some(Lineq(_,_,_,j1)) => 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

253 
(case elim (abstract(items@[((lhs,j,"<",rhs,i),nHs)])) of 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

254 
None => K no_tac 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

255 
 Some(Lineq(_,_,_,j2)) => 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

256 
rtac LA_Data.ccontr THEN' etac LA_Data.nat_neqE THEN' 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

257 
METAHYPS (fn asms => rtac (mkproof asms j1) 1) THEN' 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

258 
METAHYPS (fn asms => rtac (mkproof asms j2) 1) )); 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

259 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

260 
(* 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

261 
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

262 
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

263 
*) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

264 
val lin_arith_tac = SUBGOAL (fn (A,n) => 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

265 
let val Hs = Logic.strip_assums_hyp A 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

266 
val nHs = length Hs 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

267 
val His = Hs ~~ (0 upto (nHs1)) 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

268 
val Hitems = mapfilter (fn (h,i) => case LA_Data.decomp h of 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

269 
None => None  Some(it) => Some(it,i)) His 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

270 
in case LA_Data.decomp(Logic.strip_assums_concl A) of 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

271 
None => if null Hitems then no_tac else refute1_tac Hitems n 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

272 
 Some(citem as (r,i,rel,l,j)) => 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

273 
if rel = "=" 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

274 
then refute2_tac Hitems citem nHs n 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

275 
else let val neg::rel0 = explode rel 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

276 
val nrel = if neg = "~" then implode rel0 else "~"^rel 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

277 
in refute1_tac (Hitems@[((r,i,nrel,l,j),nHs)]) n end 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

278 
end); 
aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

279 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

280 
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

281 

aeb97860d352
Replaced the puny nat_transitive.ML by the general fast_lin_arith.ML.
nipkow
parents:
diff
changeset

282 
end; 