author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46497  89ccf66aa73d 
child 48112  b1240319ef15 
permissions  rwrr 
37744  1 
(* Title: HOL/Multivariate_Analysis/normarith.ML 
36938  2 
Author: Amine Chaieb, University of Cambridge 
3 

4 
Simple decision procedure for linear problems in Euclidean space. 

31118
541d43bee678
Isolated decision procedure for noms and the general arithmetic solver
chaieb
parents:
30868
diff
changeset

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

6 

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

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

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

10 
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

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

12 

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

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

15 

32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

17 
val bool_eq = op = : bool *bool > bool 
30868  18 
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

19 
Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a > snd, HOLogic.dest_number b > snd) 
30868  20 
 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

21 
 _ => 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

22 
fun is_ratconst t = can dest_ratconst t 
36938  23 
fun augment_norm b t acc = case term_of t of 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

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

26 
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

27 
@{term "op + :: real => _"}$_$_ => 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

28 
find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc) 
44454  29 
 @{term "op * :: real => _"}$_$_ => 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

30 
if not (is_ratconst (Thm.dest_arg1 t)) then acc else 
36938  31 
augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

32 
(Thm.dest_arg t) acc 
36938  33 
 _ => augment_norm true t acc 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

34 

39032  35 
val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg) 
36938  36 
fun cterm_lincomb_cmul c t = 
39032  37 
if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x */ c) t 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

39 
fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

41 

44454  42 
(* 
39032  43 
val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg) 
44454  44 
*) 
36938  45 
fun int_lincomb_cmul c t = 
39032  46 
if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x */ c) t 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

49 
fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

50 
fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r) 
44454  51 
*) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

52 

36938  53 
fun vector_lincomb t = case term_of t of 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

54 
Const(@{const_name plus}, _) $ _ $ _ => 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

55 
cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

56 
 Const(@{const_name minus}, _) $ _ $ _ => 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

57 
cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

58 
 Const(@{const_name scaleR}, _)$_$_ => 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

59 
cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

60 
 Const(@{const_name uminus}, _)$_ => 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

61 
cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t)) 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

62 
(* FIXME: how should we handle numerals? 
36938  63 
 Const(@ {const_name vec},_)$_ => 
64 
let 

65 
val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0 

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

66 
handle TERM _=> false) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

67 
in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one) 
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

68 
else FuncUtil.Ctermfunc.empty 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

69 
end 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

70 
*) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

72 

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

73 
fun vector_lincombs ts = 
36938  74 
fold_rev 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

75 
(fn t => fn fns => case AList.lookup (op aconvc) fns t of 
36938  76 
NONE => 
77 
let val f = vector_lincomb t 

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

78 
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

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

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

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

83 

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

85 
@{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t 
36938  86 
 @{term "op * :: real => _"}$_$_ => 
36945  87 
if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else Thm.reflexive t 
88 
 _ => Thm.reflexive t 

44454  89 
(* 
36938  90 
fun flip v eq = 
91 
if FuncUtil.Ctermfunc.defined eq v 

32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

92 
then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq 
44454  93 
*) 
36938  94 
fun allsubsets s = case s of 
29841
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 
(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

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

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

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

101 

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

102 
fun solve (vs,eqs) = case (vs,eqs) of 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

103 
([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one)) 
36938  104 
(_,eq::oeqs) => 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

105 
(case filter (member (op =) vs) (FuncUtil.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

106 
[] => NONE 
36938  107 
 v::_ => 
108 
if FuncUtil.Intfunc.defined eq v 

109 
then 

110 
let 

32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

112 
val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq 
36938  113 
fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

114 
else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn 
33040  115 
in (case solve (remove (op =) v vs, map eliminate oeqs) of 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

116 
NONE => NONE 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

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

119 
else NONE) 
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 combinations k l = if k = 0 then [[]] else 
36938  122 
case l of 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

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

124 
 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

125 

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

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

128 
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

129 
NONE => NONE 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

131 
val rawvs = map_filter vertex (combinations (length vs) eqs) 
36938  132 
val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs 
40718  133 
in fold_rev (insert (eq_list op =/)) unset [] 
36938  134 
end 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

135 

40718  136 
val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

137 

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

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

139 
[] => dun 
36938  140 
v::ovs => 
40718  141 
let val dun' = if exists (fn w => subsumes (w, v)) dun then dun 
142 
else v:: filter (fn w => not (subsumes (v, w))) dun 

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

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

145 

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

146 
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

147 

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

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

151 
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
44454
diff
changeset

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

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

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

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

156 

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

157 
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

158 

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

159 
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

160 

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

161 
(* I think here the static context should be sufficient!! *) 
36938  162 
fun inequality_canon_rule ctxt = 
163 
let 

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

164 
(* FIXME : Should be computed statically!! *) 
36938  165 
val real_poly_conv = 
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

166 
Semiring_Normalizer.semiring_normalize_wrapper ctxt 
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

167 
(the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36721
diff
changeset

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

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

170 

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

171 
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

172 
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

173 
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

174 
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

175 
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

176 
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

177 
val apply_pth7 = rewrs_conv @{thms pth_7}; 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36721
diff
changeset

178 
val apply_pth8 = rewr_conv @{thm pth_8} then_conv arg1_conv Numeral_Simprocs.field_comp_conv then_conv (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left}))); 
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36721
diff
changeset

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

180 
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

181 
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

182 
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

183 
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

184 

36938  185 
fun headvector t = case t of 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

186 
Const(@{const_name plus}, _)$ 
44454  187 
(Const(@{const_name scaleR}, _)$_$v)$_ => v 
188 
 Const(@{const_name scaleR}, _)$_$v => v 

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

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

190 

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

191 
fun vector_cmul_conv ct = 
36751
7f1da69cacb3
split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
haftmann
parents:
36721
diff
changeset

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

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

194 

36938  195 
fun vector_add_conv ct = apply_pth7 ct 
196 
handle CTERM _ => 

197 
(apply_pth8 ct 

198 
handle CTERM _ => 

199 
(case term_of ct of 

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

200 
Const(@{const_name plus},_)$lt$rt => 
36938  201 
let 
202 
val l = headvector lt 

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

203 
val r = headvector rt 
35408  204 
in (case Term_Ord.fast_term_ord (l,r) of 
36938  205 
LESS => (apply_pthb then_conv arg_conv vector_add_conv 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

206 
then_conv apply_pthd) ct 
36938  207 
 GREATER => (apply_pthc then_conv arg_conv vector_add_conv 
208 
then_conv apply_pthd) ct 

209 
 EQUAL => (apply_pth9 then_conv 

210 
((apply_ptha then_conv vector_add_conv) else_conv 

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

211 
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

212 
end 
36945  213 
 _ => Thm.reflexive ct)) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

214 

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

215 
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

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

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

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

222 
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

223 

31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

224 
 Const(@{const_name scaleR}, _)$_$_ => 
36938  225 
let 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

226 
val (p,r) = Thm.dest_comb ct 
36938  227 
val rth = Drule.arg_cong_rule p (vector_canon_conv r) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

228 
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

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

230 

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

231 
 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

232 

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

233 
 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

234 

31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

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

237 
let val n = Thm.dest_arg ct 
36938  238 
in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) 
36945  239 
then Thm.reflexive ct else apply_pth1 ct 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

240 
end 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

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

242 
 _ => apply_pth1 ct 
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 
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

245 
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

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

247 

36938  248 
fun int_flip v eq = 
249 
if FuncUtil.Intfunc.defined eq v 

32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

251 

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

252 
local 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

253 
val pth_zero = @{thm norm_zero} 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

254 
val tv_n = (ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o cprop_of) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

255 
pth_zero 
36938  256 
val concl = Thm.dest_arg o cprop_of 
257 
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = 

258 
let 

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

259 
(* FIXME: Should be computed statically!!*) 
36938  260 
val real_poly_conv = 
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

261 
Semiring_Normalizer.semiring_normalize_wrapper ctxt 
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

262 
(the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

263 
val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs 
36938  264 
val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] 
265 
val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 

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

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

267 
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

268 
val srcfuns = map vector_lincomb sources 
36938  269 
val destfuns = map vector_lincomb dests 
33042  270 
val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

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

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

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

274 
fun consider d = 
36938  275 
let 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

276 
fun coefficients x = 
36938  277 
let 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

278 
val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x)) 
36938  279 
else FuncUtil.Intfunc.empty 
280 
in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp 

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

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

282 
val equations = map coefficients vvs 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

284 
fun plausiblevertices f = 
36938  285 
let 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

286 
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

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

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

289 
fun check_solution v = 
36938  290 
let 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

292 
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

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

294 
val goodverts = filter check_solution rawverts 
36938  295 
val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

296 
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

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

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

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

301 
fun compute_ineq v = 
36938  302 
let 
303 
val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE 

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

304 
else SOME(norm_cmul_rule v t)) 
36938  305 
(v ~~ nubs) 
32402  306 
fun end_itlist f xs = split_last xs > uncurry (fold_rev f) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

307 
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

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

309 
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

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

311 
val zerodests = filter 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

313 

32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32402
diff
changeset

314 
in fst (RealArith.real_linear_prover translator 
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42793
diff
changeset

315 
(map (fn t => Drule.instantiate_normalize ([(tv_n, ctyp_of_term t)],[]) pth_zero) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

316 
zerodests, 
36936
c52d1c130898
incorporated further conversions and conversionals, after some minor tuning;
wenzelm
parents:
36753
diff
changeset

317 
map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

318 
arg_conv (arg_conv real_poly_conv))) ges', 
36938  319 
map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv 
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32402
diff
changeset

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

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

322 
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

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

324 

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

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

326 
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

327 
val norm_mp = match_mp pth 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

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

330 
fun conjunct2 th = th RS @{thm conjunct2} 
36938  331 
fun real_vector_ineq_prover ctxt translator (ges,gts) = 
332 
let 

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

333 
(* val _ = error "real_vector_ineq_prover: pause" *) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

335 
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

336 
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt 
32402  337 
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) 
46497
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
44454
diff
changeset

338 
fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t 
89ccf66aa73d
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
wenzelm
parents:
44454
diff
changeset

339 
fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r 
42361  340 
val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (Proof_Context.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

341 
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

342 
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

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

344 
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

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

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

347 
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

348 
val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts') 
36938  349 
val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1)) 
36945  350 
val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1]) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

351 
val cps = map (swap o Thm.dest_equals) (cprems_of th11) 
43333
2bdec7f430d3
renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
wenzelm
parents:
42793
diff
changeset

352 
val th12 = Drule.instantiate_normalize ([], cps) th11 
36945  353 
val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12; 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

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

356 
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

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

358 

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

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

360 
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

361 
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) 
35408  362 
fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS; 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

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

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

366 
val real_poly_neg_conv = #neg 
36753
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

367 
(Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt 
5cf4e9128f22
renamed Normalizer to the more specific Semiring_Normalizer
haftmann
parents:
36751
diff
changeset

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

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

370 
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

371 
end 
32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32402
diff
changeset

372 
in fun real_vector_prover ctxt _ translator (eqs,ges,gts) = 
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32402
diff
changeset

373 
(real_vector_ineq_prover ctxt translator 
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32402
diff
changeset

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

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

376 

36938  377 
fun init_conv ctxt = 
378 
Simplifier.rewrite (Simplifier.context ctxt 

36587  379 
(HOL_basic_ss addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm diff_0_right}, @{thm right_minus}, @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))) 
36938  380 
then_conv Numeral_Simprocs.field_comp_conv 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

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

382 

32645
1cc5b24f5a01
sos method generates and uses proof certificates
Philipp Meyer
parents:
32402
diff
changeset

383 
fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); 
36938  384 
fun norm_arith ctxt ct = 
385 
let 

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

386 
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

387 
val th = init_conv ctxt' ct 
36945  388 
in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th)) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

389 
(pure ctxt' (Thm.rhs_of th)) 
29841
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 

36938  392 
fun norm_arith_tac ctxt = 
42793  393 
clarify_tac (put_claset HOL_cs ctxt) THEN' 
35625  394 
Object_Logic.full_atomize_tac THEN' 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

395 
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

396 

31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

397 
end; 