1 (* Title: Library/normarith.ML |
1 (* Title: Library/normarith.ML |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 Description: A simple decision procedure for linear problems in euclidean space |
3 |
|
4 Simple decision procedure for linear problems in Euclidean space. |
4 *) |
5 *) |
5 |
6 |
6 (* Now the norm procedure for euclidean spaces *) |
7 signature NORM_ARITH = |
7 |
|
8 |
|
9 signature NORM_ARITH = |
|
10 sig |
8 sig |
11 val norm_arith : Proof.context -> conv |
9 val norm_arith : Proof.context -> conv |
12 val norm_arith_tac : Proof.context -> int -> tactic |
10 val norm_arith_tac : Proof.context -> int -> tactic |
13 end |
11 end |
14 |
12 |
15 structure NormArith : NORM_ARITH = |
13 structure NormArith : NORM_ARITH = |
16 struct |
14 struct |
17 |
15 |
18 open Conv; |
16 open Conv; |
19 val bool_eq = op = : bool *bool -> bool |
17 val bool_eq = op = : bool *bool -> bool |
20 fun dest_ratconst t = case term_of t of |
18 fun dest_ratconst t = case term_of t of |
21 Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) |
19 Const(@{const_name divide}, _)$a$b => Rat.rat_of_quotient(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) |
22 | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd) |
20 | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd) |
23 | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd) |
21 | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd) |
24 fun is_ratconst t = can dest_ratconst t |
22 fun is_ratconst t = can dest_ratconst t |
25 fun augment_norm b t acc = case term_of t of |
23 fun augment_norm b t acc = case term_of t of |
26 Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc |
24 Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc |
27 | _ => acc |
25 | _ => acc |
28 fun find_normedterms t acc = case term_of t of |
26 fun find_normedterms t acc = case term_of t of |
29 @{term "op + :: real => _"}$_$_ => |
27 @{term "op + :: real => _"}$_$_ => |
30 find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc) |
28 find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc) |
31 | @{term "op * :: real => _"}$_$n => |
29 | @{term "op * :: real => _"}$_$n => |
32 if not (is_ratconst (Thm.dest_arg1 t)) then acc else |
30 if not (is_ratconst (Thm.dest_arg1 t)) then acc else |
33 augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero) |
31 augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero) |
34 (Thm.dest_arg t) acc |
32 (Thm.dest_arg t) acc |
35 | _ => augment_norm true t acc |
33 | _ => augment_norm true t acc |
36 |
34 |
37 val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg |
35 val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg |
38 fun cterm_lincomb_cmul c t = |
36 fun cterm_lincomb_cmul c t = |
39 if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t |
37 if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t |
40 fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r |
38 fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r |
41 fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r) |
39 fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r) |
42 fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r) |
40 fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r) |
43 |
41 |
44 val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg |
42 val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg |
45 fun int_lincomb_cmul c t = |
43 fun int_lincomb_cmul c t = |
46 if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t |
44 if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t |
47 fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r |
45 fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r |
48 fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r) |
46 fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r) |
49 fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r) |
47 fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r) |
50 |
48 |
51 fun vector_lincomb t = case term_of t of |
49 fun vector_lincomb t = case term_of t of |
52 Const(@{const_name plus}, _) $ _ $ _ => |
50 Const(@{const_name plus}, _) $ _ $ _ => |
53 cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) |
51 cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) |
54 | Const(@{const_name minus}, _) $ _ $ _ => |
52 | Const(@{const_name minus}, _) $ _ $ _ => |
55 cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) |
53 cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) |
56 | Const(@{const_name scaleR}, _)$_$_ => |
54 | Const(@{const_name scaleR}, _)$_$_ => |
57 cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) |
55 cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t)) |
58 | Const(@{const_name uminus}, _)$_ => |
56 | Const(@{const_name uminus}, _)$_ => |
59 cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t)) |
57 cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t)) |
60 (* FIXME: how should we handle numerals? |
58 (* FIXME: how should we handle numerals? |
61 | Const(@ {const_name vec},_)$_ => |
59 | Const(@ {const_name vec},_)$_ => |
62 let |
60 let |
63 val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0 |
61 val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0 |
64 handle TERM _=> false) |
62 handle TERM _=> false) |
65 in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one) |
63 in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one) |
66 else FuncUtil.Ctermfunc.empty |
64 else FuncUtil.Ctermfunc.empty |
67 end |
65 end |
68 *) |
66 *) |
69 | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one) |
67 | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one) |
70 |
68 |
71 fun vector_lincombs ts = |
69 fun vector_lincombs ts = |
72 fold_rev |
70 fold_rev |
73 (fn t => fn fns => case AList.lookup (op aconvc) fns t of |
71 (fn t => fn fns => case AList.lookup (op aconvc) fns t of |
74 NONE => |
72 NONE => |
75 let val f = vector_lincomb t |
73 let val f = vector_lincomb t |
76 in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of |
74 in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of |
77 SOME (_,f') => (t,f') :: fns |
75 SOME (_,f') => (t,f') :: fns |
78 | NONE => (t,f) :: fns |
76 | NONE => (t,f) :: fns |
79 end |
77 end |
80 | SOME _ => fns) ts [] |
78 | SOME _ => fns) ts [] |
81 |
79 |
82 fun replacenegnorms cv t = case term_of t of |
80 fun replacenegnorms cv t = case term_of t of |
83 @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t |
81 @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t |
84 | @{term "op * :: real => _"}$_$_ => |
82 | @{term "op * :: real => _"}$_$_ => |
85 if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t |
83 if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t |
86 | _ => reflexive t |
84 | _ => reflexive t |
87 fun flip v eq = |
85 fun flip v eq = |
88 if FuncUtil.Ctermfunc.defined eq v |
86 if FuncUtil.Ctermfunc.defined eq v |
89 then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq |
87 then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq |
90 fun allsubsets s = case s of |
88 fun allsubsets s = case s of |
91 [] => [[]] |
89 [] => [[]] |
92 |(a::t) => let val res = allsubsets t in |
90 |(a::t) => let val res = allsubsets t in |
93 map (cons a) res @ res end |
91 map (cons a) res @ res end |
94 fun evaluate env lin = |
92 fun evaluate env lin = |
95 FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x)) |
93 FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x)) |
96 lin Rat.zero |
94 lin Rat.zero |
97 |
95 |
98 fun solve (vs,eqs) = case (vs,eqs) of |
96 fun solve (vs,eqs) = case (vs,eqs) of |
99 ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one)) |
97 ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one)) |
100 |(_,eq::oeqs) => |
98 |(_,eq::oeqs) => |
101 (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*) |
99 (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*) |
102 [] => NONE |
100 [] => NONE |
103 | v::_ => |
101 | v::_ => |
104 if FuncUtil.Intfunc.defined eq v |
102 if FuncUtil.Intfunc.defined eq v |
105 then |
103 then |
106 let |
104 let |
107 val c = FuncUtil.Intfunc.apply eq v |
105 val c = FuncUtil.Intfunc.apply eq v |
108 val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq |
106 val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq |
109 fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn |
107 fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn |
110 else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn |
108 else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn |
111 in (case solve (remove (op =) v vs, map eliminate oeqs) of |
109 in (case solve (remove (op =) v vs, map eliminate oeqs) of |
112 NONE => NONE |
110 NONE => NONE |
113 | SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln)) |
111 | SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln)) |
114 end |
112 end |
115 else NONE) |
113 else NONE) |
116 |
114 |
117 fun combinations k l = if k = 0 then [[]] else |
115 fun combinations k l = if k = 0 then [[]] else |
118 case l of |
116 case l of |
119 [] => [] |
117 [] => [] |
120 | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t |
118 | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t |
121 |
119 |
122 |
120 |
123 fun forall2 p l1 l2 = case (l1,l2) of |
121 fun forall2 p l1 l2 = case (l1,l2) of |
124 ([],[]) => true |
122 ([],[]) => true |
125 | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 |
123 | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2 |
126 | _ => false; |
124 | _ => false; |
127 |
125 |
128 |
126 |
129 fun vertices vs eqs = |
127 fun vertices vs eqs = |
130 let |
128 let |
131 fun vertex cmb = case solve(vs,cmb) of |
129 fun vertex cmb = case solve(vs,cmb) of |
132 NONE => NONE |
130 NONE => NONE |
133 | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs) |
131 | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs) |
134 val rawvs = map_filter vertex (combinations (length vs) eqs) |
132 val rawvs = map_filter vertex (combinations (length vs) eqs) |
135 val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs |
133 val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs |
136 in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset [] |
134 in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset [] |
137 end |
135 end |
138 |
136 |
139 fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m |
137 fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m |
140 |
138 |
141 fun subsume todo dun = case todo of |
139 fun subsume todo dun = case todo of |
142 [] => dun |
140 [] => dun |
143 |v::ovs => |
141 |v::ovs => |
144 let val dun' = if exists (fn w => subsumes w v) dun then dun |
142 let val dun' = if exists (fn w => subsumes w v) dun then dun |
145 else v::(filter (fn w => not(subsumes v w)) dun) |
143 else v::(filter (fn w => not(subsumes v w)) dun) |
146 in subsume ovs dun' |
144 in subsume ovs dun' |
147 end; |
145 end; |
148 |
146 |
149 fun match_mp PQ P = P RS PQ; |
147 fun match_mp PQ P = P RS PQ; |
150 |
148 |
151 fun cterm_of_rat x = |
149 fun cterm_of_rat x = |
152 let val (a, b) = Rat.quotient_of_rat x |
150 let val (a, b) = Rat.quotient_of_rat x |
153 in |
151 in |
154 if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a |
152 if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a |
155 else Thm.capply (Thm.capply @{cterm "op / :: real => _"} |
153 else Thm.capply (Thm.capply @{cterm "op / :: real => _"} |
156 (Numeral.mk_cnumber @{ctyp "real"} a)) |
154 (Numeral.mk_cnumber @{ctyp "real"} a)) |
157 (Numeral.mk_cnumber @{ctyp "real"} b) |
155 (Numeral.mk_cnumber @{ctyp "real"} b) |
158 end; |
156 end; |
159 |
157 |
160 fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); |
158 fun norm_cmul_rule c th = instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm}); |
161 |
159 |
162 fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm}; |
160 fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm}; |
163 |
161 |
164 (* I think here the static context should be sufficient!! *) |
162 (* I think here the static context should be sufficient!! *) |
165 fun inequality_canon_rule ctxt = |
163 fun inequality_canon_rule ctxt = |
166 let |
164 let |
167 (* FIXME : Should be computed statically!! *) |
165 (* FIXME : Should be computed statically!! *) |
168 val real_poly_conv = |
166 val real_poly_conv = |
169 Semiring_Normalizer.semiring_normalize_wrapper ctxt |
167 Semiring_Normalizer.semiring_normalize_wrapper ctxt |
170 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
168 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
171 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))) |
169 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))) |
172 end; |
170 end; |
173 |
171 |
174 fun absc cv ct = case term_of ct of |
172 fun absc cv ct = case term_of ct of |
175 Abs (v,_, _) => |
173 Abs (v,_, _) => |
176 let val (x,t) = Thm.dest_abs (SOME v) ct |
174 let val (x,t) = Thm.dest_abs (SOME v) ct |
177 in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) |
175 in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t) |
178 end |
176 end |
179 | _ => all_conv ct; |
177 | _ => all_conv ct; |
180 |
178 |
181 fun sub_conv cv ct = (comb_conv cv else_conv absc cv) ct; |
179 fun sub_conv cv ct = (comb_conv cv else_conv absc cv) ct; |
182 fun botc1 conv ct = |
180 fun botc1 conv ct = |
183 ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct; |
181 ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct; |
184 |
182 |
185 val apply_pth1 = rewr_conv @{thm pth_1}; |
183 val apply_pth1 = rewr_conv @{thm pth_1}; |
186 val apply_pth2 = rewr_conv @{thm pth_2}; |
184 val apply_pth2 = rewr_conv @{thm pth_2}; |
187 val apply_pth3 = rewr_conv @{thm pth_3}; |
185 val apply_pth3 = rewr_conv @{thm pth_3}; |
194 val apply_ptha = rewr_conv @{thm pth_a}; |
192 val apply_ptha = rewr_conv @{thm pth_a}; |
195 val apply_pthb = rewrs_conv @{thms pth_b}; |
193 val apply_pthb = rewrs_conv @{thms pth_b}; |
196 val apply_pthc = rewrs_conv @{thms pth_c}; |
194 val apply_pthc = rewrs_conv @{thms pth_c}; |
197 val apply_pthd = try_conv (rewr_conv @{thm pth_d}); |
195 val apply_pthd = try_conv (rewr_conv @{thm pth_d}); |
198 |
196 |
199 fun headvector t = case t of |
197 fun headvector t = case t of |
200 Const(@{const_name plus}, _)$ |
198 Const(@{const_name plus}, _)$ |
201 (Const(@{const_name scaleR}, _)$l$v)$r => v |
199 (Const(@{const_name scaleR}, _)$l$v)$r => v |
202 | Const(@{const_name scaleR}, _)$l$v => v |
200 | Const(@{const_name scaleR}, _)$l$v => v |
203 | _ => error "headvector: non-canonical term" |
201 | _ => error "headvector: non-canonical term" |
204 |
202 |
205 fun vector_cmul_conv ct = |
203 fun vector_cmul_conv ct = |
206 ((apply_pth5 then_conv arg1_conv Numeral_Simprocs.field_comp_conv) else_conv |
204 ((apply_pth5 then_conv arg1_conv Numeral_Simprocs.field_comp_conv) else_conv |
207 (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct |
205 (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct |
208 |
206 |
209 fun vector_add_conv ct = apply_pth7 ct |
207 fun vector_add_conv ct = apply_pth7 ct |
210 handle CTERM _ => |
208 handle CTERM _ => |
211 (apply_pth8 ct |
209 (apply_pth8 ct |
212 handle CTERM _ => |
210 handle CTERM _ => |
213 (case term_of ct of |
211 (case term_of ct of |
214 Const(@{const_name plus},_)$lt$rt => |
212 Const(@{const_name plus},_)$lt$rt => |
215 let |
213 let |
216 val l = headvector lt |
214 val l = headvector lt |
217 val r = headvector rt |
215 val r = headvector rt |
218 in (case Term_Ord.fast_term_ord (l,r) of |
216 in (case Term_Ord.fast_term_ord (l,r) of |
219 LESS => (apply_pthb then_conv arg_conv vector_add_conv |
217 LESS => (apply_pthb then_conv arg_conv vector_add_conv |
220 then_conv apply_pthd) ct |
218 then_conv apply_pthd) ct |
221 | GREATER => (apply_pthc then_conv arg_conv vector_add_conv |
219 | GREATER => (apply_pthc then_conv arg_conv vector_add_conv |
222 then_conv apply_pthd) ct |
220 then_conv apply_pthd) ct |
223 | EQUAL => (apply_pth9 then_conv |
221 | EQUAL => (apply_pth9 then_conv |
224 ((apply_ptha then_conv vector_add_conv) else_conv |
222 ((apply_ptha then_conv vector_add_conv) else_conv |
225 arg_conv vector_add_conv then_conv apply_pthd)) ct) |
223 arg_conv vector_add_conv then_conv apply_pthd)) ct) |
226 end |
224 end |
227 | _ => reflexive ct)) |
225 | _ => reflexive ct)) |
228 |
226 |
229 fun vector_canon_conv ct = case term_of ct of |
227 fun vector_canon_conv ct = case term_of ct of |
230 Const(@{const_name plus},_)$_$_ => |
228 Const(@{const_name plus},_)$_$_ => |
231 let |
229 let |
232 val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb |
230 val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb |
233 val lth = vector_canon_conv l |
231 val lth = vector_canon_conv l |
234 val rth = vector_canon_conv r |
232 val rth = vector_canon_conv r |
235 val th = Drule.binop_cong_rule p lth rth |
233 val th = Drule.binop_cong_rule p lth rth |
236 in fconv_rule (arg_conv vector_add_conv) th end |
234 in fconv_rule (arg_conv vector_add_conv) th end |
237 |
235 |
238 | Const(@{const_name scaleR}, _)$_$_ => |
236 | Const(@{const_name scaleR}, _)$_$_ => |
239 let |
237 let |
240 val (p,r) = Thm.dest_comb ct |
238 val (p,r) = Thm.dest_comb ct |
241 val rth = Drule.arg_cong_rule p (vector_canon_conv r) |
239 val rth = Drule.arg_cong_rule p (vector_canon_conv r) |
242 in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth |
240 in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth |
243 end |
241 end |
244 |
242 |
245 | Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv vector_canon_conv) ct |
243 | Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv vector_canon_conv) ct |
246 |
244 |
247 | Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct |
245 | Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct |
248 |
246 |
249 (* FIXME |
247 (* FIXME |
250 | Const(@{const_name vec},_)$n => |
248 | Const(@{const_name vec},_)$n => |
251 let val n = Thm.dest_arg ct |
249 let val n = Thm.dest_arg ct |
252 in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) |
250 in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero) |
253 then reflexive ct else apply_pth1 ct |
251 then reflexive ct else apply_pth1 ct |
254 end |
252 end |
255 *) |
253 *) |
256 | _ => apply_pth1 ct |
254 | _ => apply_pth1 ct |
257 |
255 |
261 |
259 |
262 fun fold_rev2 f [] [] z = z |
260 fun fold_rev2 f [] [] z = z |
263 | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z) |
261 | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z) |
264 | fold_rev2 f _ _ _ = raise UnequalLengths; |
262 | fold_rev2 f _ _ _ = raise UnequalLengths; |
265 |
263 |
266 fun int_flip v eq = |
264 fun int_flip v eq = |
267 if FuncUtil.Intfunc.defined eq v |
265 if FuncUtil.Intfunc.defined eq v |
268 then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq; |
266 then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq; |
269 |
267 |
270 local |
268 local |
271 val pth_zero = @{thm norm_zero} |
269 val pth_zero = @{thm norm_zero} |
272 val tv_n = (ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o cprop_of) |
270 val tv_n = (ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o cprop_of) |
273 pth_zero |
271 pth_zero |
274 val concl = Thm.dest_arg o cprop_of |
272 val concl = Thm.dest_arg o cprop_of |
275 fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = |
273 fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = |
276 let |
274 let |
277 (* FIXME: Should be computed statically!!*) |
275 (* FIXME: Should be computed statically!!*) |
278 val real_poly_conv = |
276 val real_poly_conv = |
279 Semiring_Normalizer.semiring_normalize_wrapper ctxt |
277 Semiring_Normalizer.semiring_normalize_wrapper ctxt |
280 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
278 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) |
281 val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs |
279 val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs |
282 val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] |
280 val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] |
283 val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" |
281 val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" |
284 else () |
282 else () |
285 val dests = distinct (op aconvc) (map snd rawdests) |
283 val dests = distinct (op aconvc) (map snd rawdests) |
286 val srcfuns = map vector_lincomb sources |
284 val srcfuns = map vector_lincomb sources |
287 val destfuns = map vector_lincomb dests |
285 val destfuns = map vector_lincomb dests |
288 val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] |
286 val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) [] |
289 val n = length srcfuns |
287 val n = length srcfuns |
290 val nvs = 1 upto n |
288 val nvs = 1 upto n |
291 val srccombs = srcfuns ~~ nvs |
289 val srccombs = srcfuns ~~ nvs |
292 fun consider d = |
290 fun consider d = |
293 let |
291 let |
294 fun coefficients x = |
292 fun coefficients x = |
295 let |
293 let |
296 val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x)) |
294 val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x)) |
297 else FuncUtil.Intfunc.empty |
295 else FuncUtil.Intfunc.empty |
298 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 |
296 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 |
299 end |
297 end |
300 val equations = map coefficients vvs |
298 val equations = map coefficients vvs |
301 val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs |
299 val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs |
302 fun plausiblevertices f = |
300 fun plausiblevertices f = |
303 let |
301 let |
304 val flippedequations = map (fold_rev int_flip f) equations |
302 val flippedequations = map (fold_rev int_flip f) equations |
305 val constraints = flippedequations @ inequalities |
303 val constraints = flippedequations @ inequalities |
306 val rawverts = vertices nvs constraints |
304 val rawverts = vertices nvs constraints |
307 fun check_solution v = |
305 fun check_solution v = |
308 let |
306 let |
309 val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one)) |
307 val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one)) |
310 in forall (fn e => evaluate f e =/ Rat.zero) flippedequations |
308 in forall (fn e => evaluate f e =/ Rat.zero) flippedequations |
311 end |
309 end |
312 val goodverts = filter check_solution rawverts |
310 val goodverts = filter check_solution rawverts |
313 val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs |
311 val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs |
314 in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts |
312 in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts |
315 end |
313 end |
316 val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] |
314 val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) [] |
317 in subsume allverts [] |
315 in subsume allverts [] |
318 end |
316 end |
319 fun compute_ineq v = |
317 fun compute_ineq v = |
320 let |
318 let |
321 val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE |
319 val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE |
322 else SOME(norm_cmul_rule v t)) |
320 else SOME(norm_cmul_rule v t)) |
323 (v ~~ nubs) |
321 (v ~~ nubs) |
324 fun end_itlist f xs = split_last xs |> uncurry (fold_rev f) |
322 fun end_itlist f xs = split_last xs |> uncurry (fold_rev f) |
325 in inequality_canon_rule ctxt (end_itlist norm_add_rule ths) |
323 in inequality_canon_rule ctxt (end_itlist norm_add_rule ths) |
326 end |
324 end |
327 val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @ |
325 val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @ |
328 map (inequality_canon_rule ctxt) nubs @ ges |
326 map (inequality_canon_rule ctxt) nubs @ ges |