author  huffman 
Fri, 29 May 2009 15:32:33 0700  
changeset 31344  fc09ec06b89b 
parent 31293  198eae6f5a35 
child 31445  c8a474a919a7 
permissions  rwrr 
31118
541d43bee678
Isolated decision procedure for noms and the general arithmetic solver
chaieb
parents:
30868
diff
changeset

1 
(* Title: Library/normarith.ML 
541d43bee678
Isolated decision procedure for noms and the general arithmetic solver
chaieb
parents:
30868
diff
changeset

2 
Author: Amine Chaieb, University of Cambridge 
541d43bee678
Isolated decision procedure for noms and the general arithmetic solver
chaieb
parents:
30868
diff
changeset

3 
Description: A simple decision procedure for linear problems in euclidean space 
541d43bee678
Isolated decision procedure for noms and the general arithmetic solver
chaieb
parents:
30868
diff
changeset

4 
*) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

5 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

6 
(* Now the norm procedure for euclidean spaces *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

7 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

8 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

9 
signature NORM_ARITH = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

10 
sig 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

11 
val norm_arith : Proof.context > conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

12 
val norm_arith_tac : Proof.context > int > tactic 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

13 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

14 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

15 
structure NormArith : NORM_ARITH = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

16 
struct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

17 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

18 
open Conv Thm Conv2; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

19 
val bool_eq = op = : bool *bool > bool 
30868  20 
fun dest_ratconst t = case term_of t of 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

21 
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a > snd, HOLogic.dest_number b > snd) 
30868  22 
 Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a > snd) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

23 
 _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) > snd) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

24 
fun is_ratconst t = can dest_ratconst t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

25 
fun augment_norm b t acc = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

26 
Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,dest_arg t) acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

27 
 _ => acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

28 
fun find_normedterms t acc = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

29 
@{term "op + :: real => _"}$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

30 
find_normedterms (dest_arg1 t) (find_normedterms (dest_arg t) acc) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

31 
 @{term "op * :: real => _"}$_$n => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

32 
if not (is_ratconst (dest_arg1 t)) then acc else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

33 
augment_norm (dest_ratconst (dest_arg1 t) >=/ Rat.zero) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

34 
(dest_arg t) acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

35 
 _ => augment_norm true t acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

36 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

37 
val cterm_lincomb_neg = Ctermfunc.mapf Rat.neg 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

38 
fun cterm_lincomb_cmul c t = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

39 
if c =/ Rat.zero then Ctermfunc.undefined else Ctermfunc.mapf (fn x => x */ c) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

40 
fun cterm_lincomb_add l r = Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

41 
fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

42 
fun cterm_lincomb_eq l r = Ctermfunc.is_undefined (cterm_lincomb_sub l r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

43 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

44 
val int_lincomb_neg = Intfunc.mapf Rat.neg 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

45 
fun int_lincomb_cmul c t = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

46 
if c =/ Rat.zero then Intfunc.undefined else Intfunc.mapf (fn x => x */ c) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

47 
fun int_lincomb_add l r = Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

48 
fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

49 
fun int_lincomb_eq l r = Intfunc.is_undefined (int_lincomb_sub l r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

50 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

51 
fun vector_lincomb t = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

52 
Const(@{const_name plus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) $ _ $ _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

53 
cterm_lincomb_add (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

54 
 Const(@{const_name minus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_])) $ _ $ _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

55 
cterm_lincomb_sub (vector_lincomb (dest_arg1 t)) (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

56 
 Const(@{const_name vector_scalar_mult},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

57 
cterm_lincomb_cmul (dest_ratconst (dest_arg1 t)) (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

58 
 Const(@{const_name uminus},Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

59 
cterm_lincomb_neg (vector_lincomb (dest_arg t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

60 
 Const(@{const_name vec},_)$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

61 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

62 
val b = ((snd o HOLogic.dest_number o term_of o dest_arg) t = 0 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

63 
handle TERM _=> false) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

64 
in if b then Ctermfunc.onefunc (t,Rat.one) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

65 
else Ctermfunc.undefined 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

66 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

67 
 _ => Ctermfunc.onefunc (t,Rat.one) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

68 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

69 
fun vector_lincombs ts = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

70 
fold_rev 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

71 
(fn t => fn fns => case AList.lookup (op aconvc) fns t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

72 
NONE => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

73 
let val f = vector_lincomb t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

74 
in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

75 
SOME (_,f') => (t,f') :: fns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

76 
 NONE => (t,f) :: fns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

77 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

78 
 SOME _ => fns) ts [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

79 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

80 
fun replacenegnorms cv t = case term_of t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

81 
@{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

82 
 @{term "op * :: real => _"}$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

83 
if dest_ratconst (dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

84 
 _ => reflexive t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

85 
fun flip v eq = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

86 
if Ctermfunc.defined eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

87 
then Ctermfunc.update (v, Rat.neg (Ctermfunc.apply eq v)) eq else eq 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

88 
fun allsubsets s = case s of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

89 
[] => [[]] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

90 
(a::t) => let val res = allsubsets t in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

91 
map (cons a) res @ res end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

92 
fun evaluate env lin = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

93 
Intfunc.fold (fn (x,c) => fn s => s +/ c */ (Intfunc.apply env x)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

94 
lin Rat.zero 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

95 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

96 
fun solve (vs,eqs) = case (vs,eqs) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

97 
([],[]) => SOME (Intfunc.onefunc (0,Rat.one)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

98 
(_,eq::oeqs) => 
30373
ffdd7a1f1ff0
attempt to bypass spurious infix syntax problem on polyml/sun
haftmann
parents:
29843
diff
changeset

99 
(case filter (member (op =) vs) (Intfunc.dom eq) of (*FIXME use find_first here*) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

100 
[] => NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

101 
 v::_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

102 
if Intfunc.defined eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

103 
then 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

104 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

105 
val c = Intfunc.apply eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

106 
val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

107 
fun eliminate eqn = if not (Intfunc.defined eqn v) then eqn 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

108 
else int_lincomb_add (int_lincomb_cmul (Intfunc.apply eqn v) vdef) eqn 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

109 
in (case solve (vs \ v,map eliminate oeqs) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

110 
NONE => NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

111 
 SOME soln => SOME (Intfunc.update (v, evaluate soln (Intfunc.undefine v vdef)) soln)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

112 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

113 
else NONE) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

114 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

115 
fun combinations k l = if k = 0 then [[]] else 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

116 
case l of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

117 
[] => [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

118 
 h::t => map (cons h) (combinations (k  1) t) @ combinations k t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

119 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

120 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

121 
fun forall2 p l1 l2 = case (l1,l2) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

122 
([],[]) => true 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

123 
 (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

124 
 _ => false; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

125 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

126 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

127 
fun vertices vs eqs = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

128 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

129 
fun vertex cmb = case solve(vs,cmb) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

130 
NONE => NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

131 
 SOME soln => SOME (map (fn v => Intfunc.tryapplyd soln v Rat.zero) vs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

132 
val rawvs = map_filter vertex (combinations (length vs) eqs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

133 
val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

134 
in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

135 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

136 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

137 
fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

138 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

139 
fun subsume todo dun = case todo of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

140 
[] => dun 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

141 
v::ovs => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

142 
let val dun' = if exists (fn w => subsumes w v) dun then dun 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

143 
else v::(filter (fn w => not(subsumes v w)) dun) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

144 
in subsume ovs dun' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

145 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

146 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

147 
fun match_mp PQ P = P RS PQ; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

148 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

149 
fun cterm_of_rat x = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

150 
let val (a, b) = Rat.quotient_of_rat x 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

151 
in 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

152 
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

153 
else Thm.capply (Thm.capply @{cterm "op / :: real => _"} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

154 
(Numeral.mk_cnumber @{ctyp "real"} a)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

155 
(Numeral.mk_cnumber @{ctyp "real"} b) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

156 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

157 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

158 
fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

159 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

160 
fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

161 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

162 
(* I think here the static context should be sufficient!! *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

163 
fun inequality_canon_rule ctxt = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

164 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

165 
(* FIXME : Should be computed statically!! *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

166 
val real_poly_conv = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

167 
Normalizer.semiring_normalize_wrapper ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

168 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

169 
in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv))) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

170 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

171 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

172 
fun absc cv ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

173 
Abs (v,_, _) => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

174 
let val (x,t) = Thm.dest_abs (SOME v) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

175 
in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

176 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

177 
 _ => all_conv ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

178 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

179 
fun sub_conv cv ct = (comb_conv cv else_conv absc cv) ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

180 
fun botc1 conv ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

181 
((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

182 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

183 
fun rewrs_conv eqs ct = first_conv (map rewr_conv eqs) ct; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

184 
val apply_pth1 = rewr_conv @{thm pth_1}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

185 
val apply_pth2 = rewr_conv @{thm pth_2}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

186 
val apply_pth3 = rewr_conv @{thm pth_3}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

187 
val apply_pth4 = rewrs_conv @{thms pth_4}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

188 
val apply_pth5 = rewr_conv @{thm pth_5}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

189 
val apply_pth6 = rewr_conv @{thm pth_6}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

190 
val apply_pth7 = rewrs_conv @{thms pth_7}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

191 
val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm vector_smult_lzero}))); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

192 
val apply_pth9 = rewrs_conv @{thms pth_9} then_conv arg1_conv (arg1_conv field_comp_conv); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

193 
val apply_ptha = rewr_conv @{thm pth_a}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

194 
val apply_pthb = rewrs_conv @{thms pth_b}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

195 
val apply_pthc = rewrs_conv @{thms pth_c}; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

196 
val apply_pthd = try_conv (rewr_conv @{thm pth_d}); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

197 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

198 
fun headvector t = case t of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

199 
Const(@{const_name plus}, Type("fun",[Type("Finite_Cartesian_Product.^",_),_]))$ 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

200 
(Const(@{const_name vector_scalar_mult}, _)$l$v)$r => v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

201 
 Const(@{const_name vector_scalar_mult}, _)$l$v => v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

202 
 _ => error "headvector: noncanonical term" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

203 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

204 
fun vector_cmul_conv ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

205 
((apply_pth5 then_conv arg1_conv field_comp_conv) else_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

206 
(apply_pth6 then_conv binop_conv vector_cmul_conv)) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

207 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

208 
fun vector_add_conv ct = apply_pth7 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

209 
handle CTERM _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

210 
(apply_pth8 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

211 
handle CTERM _ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

212 
(case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

213 
Const(@{const_name plus},_)$lt$rt => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

214 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

215 
val l = headvector lt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

216 
val r = headvector rt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

217 
in (case TermOrd.fast_term_ord (l,r) of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

218 
LESS => (apply_pthb then_conv arg_conv vector_add_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

219 
then_conv apply_pthd) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

220 
 GREATER => (apply_pthc then_conv arg_conv vector_add_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

221 
then_conv apply_pthd) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

222 
 EQUAL => (apply_pth9 then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

223 
((apply_ptha then_conv vector_add_conv) else_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

224 
arg_conv vector_add_conv then_conv apply_pthd)) ct) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

225 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

226 
 _ => reflexive ct)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

227 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

228 
fun vector_canon_conv ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

229 
Const(@{const_name plus},_)$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

230 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

231 
val ((p,l),r) = Thm.dest_comb ct >> Thm.dest_comb 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

232 
val lth = vector_canon_conv l 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

233 
val rth = vector_canon_conv r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

234 
val th = Drule.binop_cong_rule p lth rth 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

235 
in fconv_rule (arg_conv vector_add_conv) th end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

236 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

237 
 Const(@{const_name vector_scalar_mult}, _)$_$_ => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

238 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

239 
val (p,r) = Thm.dest_comb ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

240 
val rth = Drule.arg_cong_rule p (vector_canon_conv r) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

241 
in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

242 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

243 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

244 
 Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv vector_canon_conv) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

245 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

246 
 Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

247 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

248 
 Const(@{const_name vec},_)$n => 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

249 
let val n = Thm.dest_arg ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

250 
in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

251 
then reflexive ct else apply_pth1 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

252 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

253 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

254 
 _ => apply_pth1 ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

255 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

256 
fun norm_canon_conv ct = case term_of ct of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

257 
Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

258 
 _ => raise CTERM ("norm_canon_conv", [ct]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

259 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

260 
fun fold_rev2 f [] [] z = z 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

261 
 fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

262 
 fold_rev2 f _ _ _ = raise UnequalLengths; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

263 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

264 
fun int_flip v eq = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

265 
if Intfunc.defined eq v 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

266 
then Intfunc.update (v, Rat.neg (Intfunc.apply eq v)) eq else eq; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

267 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

268 
local 
29843  269 
val pth_zero = @{thm "norm_0"} 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

270 
val tv_n = (hd o tl o dest_ctyp o ctyp_of_term o dest_arg o dest_arg1 o dest_arg o cprop_of) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

271 
pth_zero 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

272 
val concl = dest_arg o cprop_of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

273 
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

274 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

275 
(* FIXME: Should be computed statically!!*) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

276 
val real_poly_conv = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

277 
Normalizer.semiring_normalize_wrapper ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

278 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

279 
val sources = map (dest_arg o dest_arg1 o concl) nubs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

280 
val rawdests = fold_rev (find_normedterms o dest_arg o concl) (ges @ gts) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

281 
val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

282 
else () 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

283 
val dests = distinct (op aconvc) (map snd rawdests) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

284 
val srcfuns = map vector_lincomb sources 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

285 
val destfuns = map vector_lincomb dests 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

286 
val vvs = fold_rev (curry (gen_union op aconvc) o Ctermfunc.dom) (srcfuns @ destfuns) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

287 
val n = length srcfuns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

288 
val nvs = 1 upto n 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

289 
val srccombs = srcfuns ~~ nvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

290 
fun consider d = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

291 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

292 
fun coefficients x = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

293 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

294 
val inp = if Ctermfunc.defined d x then Intfunc.onefunc (0, Rat.neg(Ctermfunc.apply d x)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

295 
else Intfunc.undefined 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

296 
in fold_rev (fn (f,v) => fn g => if Ctermfunc.defined f x then Intfunc.update (v, Ctermfunc.apply f x) g else g) srccombs inp 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

297 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

298 
val equations = map coefficients vvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

299 
val inequalities = map (fn n => Intfunc.onefunc (n,Rat.one)) nvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

300 
fun plausiblevertices f = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

301 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

302 
val flippedequations = map (fold_rev int_flip f) equations 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

303 
val constraints = flippedequations @ inequalities 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

304 
val rawverts = vertices nvs constraints 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

305 
fun check_solution v = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

306 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

307 
val f = fold_rev2 (curry Intfunc.update) nvs v (Intfunc.onefunc (0, Rat.one)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

308 
in forall (fn e => evaluate f e =/ Rat.zero) flippedequations 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

309 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

310 
val goodverts = filter check_solution rawverts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

311 
val signfixups = map (fn n => if n mem_int f then ~1 else 1) nvs 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

312 
in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

313 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

314 
val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

315 
in subsume allverts [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

316 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

317 
fun compute_ineq v = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

318 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

319 
val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

320 
else SOME(norm_cmul_rule v t)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

321 
(v ~~ nubs) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

322 
in inequality_canon_rule ctxt (end_itlist norm_add_rule ths) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

323 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

324 
val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @ 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

325 
map (inequality_canon_rule ctxt) nubs @ ges 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

326 
val zerodests = filter 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

327 
(fn t => null (Ctermfunc.dom (vector_lincomb t))) (map snd rawdests) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

328 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

329 
in RealArith.real_linear_prover translator 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

330 
(map (fn t => instantiate ([(tv_n,(hd o tl o dest_ctyp o ctyp_of_term) t)],[]) pth_zero) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

331 
zerodests, 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

332 
map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

333 
arg_conv (arg_conv real_poly_conv))) ges', 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

334 
map (fconv_rule (once_depth_conv (norm_canon_conv) then_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

335 
arg_conv (arg_conv real_poly_conv))) gts) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

336 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

337 
in val real_vector_combo_prover = real_vector_combo_prover 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

338 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

339 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

340 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

341 
val pth = @{thm norm_imp_pos_and_ge} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

342 
val norm_mp = match_mp pth 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

343 
val concl = dest_arg o cprop_of 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

344 
fun conjunct1 th = th RS @{thm conjunct1} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

345 
fun conjunct2 th = th RS @{thm conjunct2} 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

346 
fun C f x y = f y x 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

347 
fun real_vector_ineq_prover ctxt translator (ges,gts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

348 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

349 
(* val _ = error "real_vector_ineq_prover: pause" *) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

350 
val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) [] 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

351 
val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

352 
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

353 
fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: norm) => real"}) t 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

354 
fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

355 
val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

356 
val replace_conv = try_conv (rewrs_conv asl) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

357 
val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

358 
val ges' = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

359 
fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

360 
asl (map replace_rule ges) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

361 
val gts' = map replace_rule gts 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

362 
val nubs = map (conjunct2 o norm_mp) asl 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

363 
val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts') 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

364 
val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

365 
val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

366 
val cps = map (swap o dest_equals) (cprems_of th11) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

367 
val th12 = instantiate ([], cps) th11 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

368 
val th13 = fold (C implies_elim) (map (reflexive o snd) cps) th12; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

369 
in hd (Variable.export ctxt' ctxt [th13]) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

370 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

371 
in val real_vector_ineq_prover = real_vector_ineq_prover 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

372 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

373 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

374 
local 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

375 
val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0})) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

376 
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

377 
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

378 
(* FIXME: Lookup in the context every time!!! Fix this !!!*) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

379 
fun splitequation ctxt th acc = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

380 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

381 
val real_poly_neg_conv = #neg 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

382 
(Normalizer.semiring_normalizers_ord_wrapper ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

383 
(valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

384 
val (th1,th2) = conj_pair(rawrule th) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

385 
in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

386 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

387 
in fun real_vector_prover ctxt translator (eqs,ges,gts) = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

388 
real_vector_ineq_prover ctxt translator 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

389 
(fold_rev (splitequation ctxt) eqs ges,gts) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

390 
end; 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

391 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

392 
fun init_conv ctxt = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

393 
Simplifier.rewrite (Simplifier.context ctxt 
31344
fc09ec06b89b
instance ^ :: (metric_space, finite) metric_space
huffman
parents:
31293
diff
changeset

394 
(HOL_basic_ss addsimps ([@{thm vec_0}, @{thm vec_1}, @{thm vector_dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_0}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

395 
then_conv field_comp_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

396 
then_conv nnf_conv 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

397 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

398 
fun pure ctxt = RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

399 
fun norm_arith ctxt ct = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

400 
let 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

401 
val ctxt' = Variable.declare_term (term_of ct) ctxt 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

402 
val th = init_conv ctxt' ct 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

403 
in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

404 
(pure ctxt' (rhs_of th)) 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

405 
end 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

406 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

407 
fun norm_arith_tac ctxt = 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

408 
clarify_tac HOL_cs THEN' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

409 
ObjectLogic.full_atomize_tac THEN' 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

410 
CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i); 
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

411 

86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

412 
end; 