author  wenzelm 
Sat, 16 Apr 2011 16:15:37 +0200  
changeset 42361  23f352990944 
parent 40721  e5089e903e39 
child 42793  88bee9f6eec7 
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) 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

29 
 @{term "op * :: real => _"}$_$n => 
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 

39032  42 
val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg) 
36938  43 
fun int_lincomb_cmul c t = 
39032  44 
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

45 
fun int_lincomb_add l r = FuncUtil.Intfunc.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

46 
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

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

48 

36938  49 
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

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

51 
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

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

53 
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

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

55 
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

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

57 
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

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

61 
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

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

63 
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

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

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

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

67 
 _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one) 
29841
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 = 
36938  70 
fold_rev 
29841
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 
36938  72 
NONE => 
73 
let val f = vector_lincomb t 

29841
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 
36938  76 
 NONE => (t,f) :: fns 
29841
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 

36938  80 
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

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

36938  85 
fun flip v eq = 
86 
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

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

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 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

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

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

100 
[] => NONE 
36938  101 
 v::_ => 
102 
if FuncUtil.Intfunc.defined eq v 

103 
then 

104 
let 

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

105 
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

106 
val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq 
36938  107 
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

108 
else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn 
33040  109 
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

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

111 
 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

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 
36938  116 
case l of 
29841
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 
fun vertices vs eqs = 
36938  121 
let 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

122 
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

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

124 
 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

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

129 

40718  130 
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

131 

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

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

133 
[] => dun 
36938  134 
v::ovs => 
40718  135 
let val dun' = if exists (fn w => subsumes (w, v)) dun then dun 
136 
else v:: filter (fn w => not (subsumes (v, w))) dun 

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

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

139 

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

140 
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

141 

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

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

145 
if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a 
36938  146 
else Thm.capply (Thm.capply @{cterm "op / :: real => _"} 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

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

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

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

150 

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

151 
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

152 

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

153 
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

154 

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

155 
(* I think here the static context should be sufficient!! *) 
36938  156 
fun inequality_canon_rule ctxt = 
157 
let 

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

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

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

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

162 
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

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

164 

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

165 
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

166 
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

167 
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

168 
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

169 
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

170 
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

171 
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

172 
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

173 
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

174 
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

175 
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

176 
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

177 
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

178 

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

180 
Const(@{const_name plus}, _)$ 
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

181 
(Const(@{const_name scaleR}, _)$l$v)$r => v 
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

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

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

184 

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

185 
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

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

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

188 

36938  189 
fun vector_add_conv ct = apply_pth7 ct 
190 
handle CTERM _ => 

191 
(apply_pth8 ct 

192 
handle CTERM _ => 

193 
(case term_of ct of 

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

194 
Const(@{const_name plus},_)$lt$rt => 
36938  195 
let 
196 
val l = headvector lt 

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

197 
val r = headvector rt 
35408  198 
in (case Term_Ord.fast_term_ord (l,r) of 
36938  199 
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

200 
then_conv apply_pthd) ct 
36938  201 
 GREATER => (apply_pthc then_conv arg_conv vector_add_conv 
202 
then_conv apply_pthd) ct 

203 
 EQUAL => (apply_pth9 then_conv 

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

205 
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

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

208 

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

209 
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

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

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

214 
val rth = vector_canon_conv r 
36938  215 
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

216 
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

217 

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

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

220 
val (p,r) = Thm.dest_comb ct 
36938  221 
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

222 
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

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

224 

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

225 
 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

226 

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

227 
 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

228 

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

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

231 
let val n = Thm.dest_arg ct 
36938  232 
in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) 
36945  233 
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

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

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

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

237 

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

238 
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

239 
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

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

241 

36938  242 
fun int_flip v eq = 
243 
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

244 
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

245 

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

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

247 
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

248 
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

249 
pth_zero 
36938  250 
val concl = Thm.dest_arg o cprop_of 
251 
fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = 

252 
let 

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

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

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

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

257 
val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs 
36938  258 
val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] 
259 
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

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

261 
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

262 
val srcfuns = map vector_lincomb sources 
36938  263 
val destfuns = map vector_lincomb dests 
33042  264 
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

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

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

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

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

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

272 
val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x)) 
36938  273 
else FuncUtil.Intfunc.empty 
274 
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

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

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

277 
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

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

280 
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

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

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

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

285 
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

286 
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

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

288 
val goodverts = filter check_solution rawverts 
36938  289 
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

290 
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

291 
end 
36938  292 
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

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

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

295 
fun compute_ineq v = 
36938  296 
let 
297 
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

298 
else SOME(norm_cmul_rule v t)) 
36938  299 
(v ~~ nubs) 
32402  300 
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

301 
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

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

303 
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

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

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

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

307 

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

308 
in fst (RealArith.real_linear_prover translator 
31445
c8a474a919a7
generalize norm method to work over class real_normed_vector
huffman
parents:
31344
diff
changeset

309 
(map (fn t => instantiate ([(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

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

311 
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

312 
arg_conv (arg_conv real_poly_conv))) ges', 
36938  313 
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

314 
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

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

316 
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

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

318 

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

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

320 
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

321 
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

322 
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

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

324 
fun conjunct2 th = th RS @{thm conjunct2} 
36938  325 
fun real_vector_ineq_prover ctxt translator (ges,gts) = 
326 
let 

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

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

328 
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

329 
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

330 
val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt 
32402  331 
fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) 
32832
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

332 
fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t 
4602cb6ae0b5
additional fixes in normarith.ML due to FuncFun and FuncUtil changes
Philipp Meyer
parents:
32645
diff
changeset

333 
fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r 
42361  334 
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

335 
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

336 
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

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

338 
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

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

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

341 
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

342 
val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts') 
36938  343 
val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1)) 
36945  344 
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

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

346 
val th12 = instantiate ([], cps) th11 
36945  347 
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

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

350 
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

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

352 

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

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

354 
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

355 
fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2}) 
35408  356 
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

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

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

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

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

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

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

364 
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

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

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

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

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

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

370 

36938  371 
fun init_conv ctxt = 
372 
Simplifier.rewrite (Simplifier.context ctxt 

36587  373 
(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  374 
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

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

376 

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

377 
fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt); 
36938  378 
fun norm_arith ctxt ct = 
379 
let 

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

380 
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

381 
val th = init_conv ctxt' ct 
36945  382 
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

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

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

385 

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

387 
clarify_tac HOL_cs THEN' 
35625  388 
Object_Logic.full_atomize_tac THEN' 
29841
86d94bb79226
A generic decision procedure for linear rea arithmetic and normed vector spaces
chaieb
parents:
diff
changeset

389 
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

390 

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

391 
end; 