1.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML Sat May 15 18:11:00 2010 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat May 15 18:12:58 2010 +0200
1.3 @@ -1,18 +1,16 @@
1.4 -(* Title: Library/normarith.ML
1.5 - Author: Amine Chaieb, University of Cambridge
1.6 - Description: A simple decision procedure for linear problems in euclidean space
1.7 +(* Title: Library/normarith.ML
1.8 + Author: Amine Chaieb, University of Cambridge
1.9 +
1.10 +Simple decision procedure for linear problems in Euclidean space.
1.11 *)
1.12
1.13 - (* Now the norm procedure for euclidean spaces *)
1.14 -
1.15 -
1.16 -signature NORM_ARITH =
1.17 +signature NORM_ARITH =
1.18 sig
1.19 val norm_arith : Proof.context -> conv
1.20 val norm_arith_tac : Proof.context -> int -> tactic
1.21 end
1.22
1.23 -structure NormArith : NORM_ARITH =
1.24 +structure NormArith : NORM_ARITH =
1.25 struct
1.26
1.27 open Conv;
1.28 @@ -22,7 +20,7 @@
1.29 | Const(@{const_name inverse}, _)$a => Rat.rat_of_quotient(1, HOLogic.dest_number a |> snd)
1.30 | _ => Rat.rat_of_int (HOLogic.dest_number (term_of t) |> snd)
1.31 fun is_ratconst t = can dest_ratconst t
1.32 - fun augment_norm b t acc = case term_of t of
1.33 + fun augment_norm b t acc = case term_of t of
1.34 Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc
1.35 | _ => acc
1.36 fun find_normedterms t acc = case term_of t of
1.37 @@ -30,25 +28,25 @@
1.38 find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
1.39 | @{term "op * :: real => _"}$_$n =>
1.40 if not (is_ratconst (Thm.dest_arg1 t)) then acc else
1.41 - augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
1.42 + augment_norm (dest_ratconst (Thm.dest_arg1 t) >=/ Rat.zero)
1.43 (Thm.dest_arg t) acc
1.44 - | _ => augment_norm true t acc
1.45 + | _ => augment_norm true t acc
1.46
1.47 val cterm_lincomb_neg = FuncUtil.Ctermfunc.map Rat.neg
1.48 - fun cterm_lincomb_cmul c t =
1.49 + fun cterm_lincomb_cmul c t =
1.50 if c =/ Rat.zero then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn x => x */ c) t
1.51 fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
1.52 fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
1.53 fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
1.54
1.55 val int_lincomb_neg = FuncUtil.Intfunc.map Rat.neg
1.56 - fun int_lincomb_cmul c t =
1.57 + fun int_lincomb_cmul c t =
1.58 if c =/ Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn x => x */ c) t
1.59 fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ Rat.zero) l r
1.60 fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
1.61 fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
1.62
1.63 -fun vector_lincomb t = case term_of t of
1.64 +fun vector_lincomb t = case term_of t of
1.65 Const(@{const_name plus}, _) $ _ $ _ =>
1.66 cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
1.67 | Const(@{const_name minus}, _) $ _ $ _ =>
1.68 @@ -58,9 +56,9 @@
1.69 | Const(@{const_name uminus}, _)$_ =>
1.70 cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t))
1.71 (* FIXME: how should we handle numerals?
1.72 - | Const(@ {const_name vec},_)$_ =>
1.73 - let
1.74 - val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
1.75 + | Const(@ {const_name vec},_)$_ =>
1.76 + let
1.77 + val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
1.78 handle TERM _=> false)
1.79 in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one)
1.80 else FuncUtil.Ctermfunc.empty
1.81 @@ -69,44 +67,44 @@
1.82 | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one)
1.83
1.84 fun vector_lincombs ts =
1.85 - fold_rev
1.86 + fold_rev
1.87 (fn t => fn fns => case AList.lookup (op aconvc) fns t of
1.88 - NONE =>
1.89 - let val f = vector_lincomb t
1.90 + NONE =>
1.91 + let val f = vector_lincomb t
1.92 in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of
1.93 SOME (_,f') => (t,f') :: fns
1.94 - | NONE => (t,f) :: fns
1.95 + | NONE => (t,f) :: fns
1.96 end
1.97 | SOME _ => fns) ts []
1.98
1.99 -fun replacenegnorms cv t = case term_of t of
1.100 +fun replacenegnorms cv t = case term_of t of
1.101 @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
1.102 -| @{term "op * :: real => _"}$_$_ =>
1.103 +| @{term "op * :: real => _"}$_$_ =>
1.104 if dest_ratconst (Thm.dest_arg1 t) </ Rat.zero then arg_conv cv t else reflexive t
1.105 | _ => reflexive t
1.106 -fun flip v eq =
1.107 - if FuncUtil.Ctermfunc.defined eq v
1.108 +fun flip v eq =
1.109 + if FuncUtil.Ctermfunc.defined eq v
1.110 then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
1.111 -fun allsubsets s = case s of
1.112 +fun allsubsets s = case s of
1.113 [] => [[]]
1.114 |(a::t) => let val res = allsubsets t in
1.115 map (cons a) res @ res end
1.116 fun evaluate env lin =
1.117 - FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x))
1.118 + FuncUtil.Intfunc.fold (fn (x,c) => fn s => s +/ c */ (FuncUtil.Intfunc.apply env x))
1.119 lin Rat.zero
1.120
1.121 fun solve (vs,eqs) = case (vs,eqs) of
1.122 ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one))
1.123 - |(_,eq::oeqs) =>
1.124 + |(_,eq::oeqs) =>
1.125 (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
1.126 [] => NONE
1.127 - | v::_ =>
1.128 - if FuncUtil.Intfunc.defined eq v
1.129 - then
1.130 - let
1.131 + | v::_ =>
1.132 + if FuncUtil.Intfunc.defined eq v
1.133 + then
1.134 + let
1.135 val c = FuncUtil.Intfunc.apply eq v
1.136 val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
1.137 - fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
1.138 + fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
1.139 else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
1.140 in (case solve (remove (op =) v vs, map eliminate oeqs) of
1.141 NONE => NONE
1.142 @@ -115,44 +113,44 @@
1.143 else NONE)
1.144
1.145 fun combinations k l = if k = 0 then [[]] else
1.146 - case l of
1.147 + case l of
1.148 [] => []
1.149 | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
1.150
1.151
1.152 -fun forall2 p l1 l2 = case (l1,l2) of
1.153 +fun forall2 p l1 l2 = case (l1,l2) of
1.154 ([],[]) => true
1.155 | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
1.156 | _ => false;
1.157
1.158
1.159 fun vertices vs eqs =
1.160 - let
1.161 + let
1.162 fun vertex cmb = case solve(vs,cmb) of
1.163 NONE => NONE
1.164 | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
1.165 val rawvs = map_filter vertex (combinations (length vs) eqs)
1.166 - val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
1.167 - in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset []
1.168 - end
1.169 + val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
1.170 + in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset []
1.171 + end
1.172
1.173 -fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m
1.174 +fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m
1.175
1.176 fun subsume todo dun = case todo of
1.177 [] => dun
1.178 -|v::ovs =>
1.179 +|v::ovs =>
1.180 let val dun' = if exists (fn w => subsumes w v) dun then dun
1.181 - else v::(filter (fn w => not(subsumes v w)) dun)
1.182 - in subsume ovs dun'
1.183 + else v::(filter (fn w => not(subsumes v w)) dun)
1.184 + in subsume ovs dun'
1.185 end;
1.186
1.187 fun match_mp PQ P = P RS PQ;
1.188
1.189 -fun cterm_of_rat x =
1.190 +fun cterm_of_rat x =
1.191 let val (a, b) = Rat.quotient_of_rat x
1.192 -in
1.193 +in
1.194 if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
1.195 - else Thm.capply (Thm.capply @{cterm "op / :: real => _"}
1.196 + else Thm.capply (Thm.capply @{cterm "op / :: real => _"}
1.197 (Numeral.mk_cnumber @{ctyp "real"} a))
1.198 (Numeral.mk_cnumber @{ctyp "real"} b)
1.199 end;
1.200 @@ -162,24 +160,24 @@
1.201 fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
1.202
1.203 (* I think here the static context should be sufficient!! *)
1.204 -fun inequality_canon_rule ctxt =
1.205 - let
1.206 +fun inequality_canon_rule ctxt =
1.207 + let
1.208 (* FIXME : Should be computed statically!! *)
1.209 - val real_poly_conv =
1.210 + val real_poly_conv =
1.211 Semiring_Normalizer.semiring_normalize_wrapper ctxt
1.212 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
1.213 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)))
1.214 end;
1.215
1.216 - fun absc cv ct = case term_of ct of
1.217 - Abs (v,_, _) =>
1.218 + fun absc cv ct = case term_of ct of
1.219 + Abs (v,_, _) =>
1.220 let val (x,t) = Thm.dest_abs (SOME v) ct
1.221 in Thm.abstract_rule ((fst o dest_Free o term_of) x) x (cv t)
1.222 end
1.223 | _ => all_conv ct;
1.224
1.225 fun sub_conv cv ct = (comb_conv cv else_conv absc cv) ct;
1.226 -fun botc1 conv ct =
1.227 +fun botc1 conv ct =
1.228 ((sub_conv (botc1 conv)) then_conv (conv else_conv all_conv)) ct;
1.229
1.230 val apply_pth1 = rewr_conv @{thm pth_1};
1.231 @@ -196,7 +194,7 @@
1.232 val apply_pthc = rewrs_conv @{thms pth_c};
1.233 val apply_pthd = try_conv (rewr_conv @{thm pth_d});
1.234
1.235 -fun headvector t = case t of
1.236 +fun headvector t = case t of
1.237 Const(@{const_name plus}, _)$
1.238 (Const(@{const_name scaleR}, _)$l$v)$r => v
1.239 | Const(@{const_name scaleR}, _)$l$v => v
1.240 @@ -206,39 +204,39 @@
1.241 ((apply_pth5 then_conv arg1_conv Numeral_Simprocs.field_comp_conv) else_conv
1.242 (apply_pth6 then_conv binop_conv vector_cmul_conv)) ct
1.243
1.244 -fun vector_add_conv ct = apply_pth7 ct
1.245 - handle CTERM _ =>
1.246 - (apply_pth8 ct
1.247 - handle CTERM _ =>
1.248 - (case term_of ct of
1.249 +fun vector_add_conv ct = apply_pth7 ct
1.250 + handle CTERM _ =>
1.251 + (apply_pth8 ct
1.252 + handle CTERM _ =>
1.253 + (case term_of ct of
1.254 Const(@{const_name plus},_)$lt$rt =>
1.255 - let
1.256 - val l = headvector lt
1.257 + let
1.258 + val l = headvector lt
1.259 val r = headvector rt
1.260 in (case Term_Ord.fast_term_ord (l,r) of
1.261 - LESS => (apply_pthb then_conv arg_conv vector_add_conv
1.262 + LESS => (apply_pthb then_conv arg_conv vector_add_conv
1.263 then_conv apply_pthd) ct
1.264 - | GREATER => (apply_pthc then_conv arg_conv vector_add_conv
1.265 - then_conv apply_pthd) ct
1.266 - | EQUAL => (apply_pth9 then_conv
1.267 - ((apply_ptha then_conv vector_add_conv) else_conv
1.268 + | GREATER => (apply_pthc then_conv arg_conv vector_add_conv
1.269 + then_conv apply_pthd) ct
1.270 + | EQUAL => (apply_pth9 then_conv
1.271 + ((apply_ptha then_conv vector_add_conv) else_conv
1.272 arg_conv vector_add_conv then_conv apply_pthd)) ct)
1.273 end
1.274 | _ => reflexive ct))
1.275
1.276 fun vector_canon_conv ct = case term_of ct of
1.277 Const(@{const_name plus},_)$_$_ =>
1.278 - let
1.279 + let
1.280 val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb
1.281 - val lth = vector_canon_conv l
1.282 + val lth = vector_canon_conv l
1.283 val rth = vector_canon_conv r
1.284 - val th = Drule.binop_cong_rule p lth rth
1.285 + val th = Drule.binop_cong_rule p lth rth
1.286 in fconv_rule (arg_conv vector_add_conv) th end
1.287
1.288 | Const(@{const_name scaleR}, _)$_$_ =>
1.289 - let
1.290 + let
1.291 val (p,r) = Thm.dest_comb ct
1.292 - val rth = Drule.arg_cong_rule p (vector_canon_conv r)
1.293 + val rth = Drule.arg_cong_rule p (vector_canon_conv r)
1.294 in fconv_rule (arg_conv (apply_pth4 else_conv vector_cmul_conv)) rth
1.295 end
1.296
1.297 @@ -247,9 +245,9 @@
1.298 | Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv vector_canon_conv) ct
1.299
1.300 (* FIXME
1.301 -| Const(@{const_name vec},_)$n =>
1.302 +| Const(@{const_name vec},_)$n =>
1.303 let val n = Thm.dest_arg ct
1.304 - in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
1.305 + in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
1.306 then reflexive ct else apply_pth1 ct
1.307 end
1.308 *)
1.309 @@ -263,64 +261,64 @@
1.310 | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z)
1.311 | fold_rev2 f _ _ _ = raise UnequalLengths;
1.312
1.313 -fun int_flip v eq =
1.314 - if FuncUtil.Intfunc.defined eq v
1.315 +fun int_flip v eq =
1.316 + if FuncUtil.Intfunc.defined eq v
1.317 then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
1.318
1.319 local
1.320 val pth_zero = @{thm norm_zero}
1.321 val tv_n = (ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o cprop_of)
1.322 pth_zero
1.323 - val concl = Thm.dest_arg o cprop_of
1.324 - fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
1.325 - let
1.326 + val concl = Thm.dest_arg o cprop_of
1.327 + fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
1.328 + let
1.329 (* FIXME: Should be computed statically!!*)
1.330 - val real_poly_conv =
1.331 + val real_poly_conv =
1.332 Semiring_Normalizer.semiring_normalize_wrapper ctxt
1.333 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
1.334 val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
1.335 - val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
1.336 - val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
1.337 + val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
1.338 + val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
1.339 else ()
1.340 val dests = distinct (op aconvc) (map snd rawdests)
1.341 val srcfuns = map vector_lincomb sources
1.342 - val destfuns = map vector_lincomb dests
1.343 + val destfuns = map vector_lincomb dests
1.344 val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
1.345 val n = length srcfuns
1.346 val nvs = 1 upto n
1.347 val srccombs = srcfuns ~~ nvs
1.348 fun consider d =
1.349 - let
1.350 + let
1.351 fun coefficients x =
1.352 - let
1.353 + let
1.354 val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x))
1.355 - else FuncUtil.Intfunc.empty
1.356 - 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
1.357 + else FuncUtil.Intfunc.empty
1.358 + 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
1.359 end
1.360 val equations = map coefficients vvs
1.361 val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs
1.362 fun plausiblevertices f =
1.363 - let
1.364 + let
1.365 val flippedequations = map (fold_rev int_flip f) equations
1.366 val constraints = flippedequations @ inequalities
1.367 val rawverts = vertices nvs constraints
1.368 fun check_solution v =
1.369 - let
1.370 + let
1.371 val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one))
1.372 in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
1.373 end
1.374 val goodverts = filter check_solution rawverts
1.375 - val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
1.376 + val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
1.377 in map (map2 (fn s => fn c => Rat.rat_of_int s */ c) signfixups) goodverts
1.378 end
1.379 - val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
1.380 + val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
1.381 in subsume allverts []
1.382 end
1.383 fun compute_ineq v =
1.384 - let
1.385 - val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
1.386 + let
1.387 + val ths = map_filter (fn (v,t) => if v =/ Rat.zero then NONE
1.388 else SOME(norm_cmul_rule v t))
1.389 - (v ~~ nubs)
1.390 + (v ~~ nubs)
1.391 fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
1.392 in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
1.393 end
1.394 @@ -334,7 +332,7 @@
1.395 zerodests,
1.396 map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
1.397 arg_conv (arg_conv real_poly_conv))) ges',
1.398 - map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
1.399 + map (fconv_rule (try_conv (Conv.top_sweep_conv (K norm_canon_conv) ctxt) then_conv
1.400 arg_conv (arg_conv real_poly_conv))) gts))
1.401 end
1.402 in val real_vector_combo_prover = real_vector_combo_prover
1.403 @@ -346,8 +344,8 @@
1.404 val concl = Thm.dest_arg o cprop_of
1.405 fun conjunct1 th = th RS @{thm conjunct1}
1.406 fun conjunct2 th = th RS @{thm conjunct2}
1.407 -fun real_vector_ineq_prover ctxt translator (ges,gts) =
1.408 - let
1.409 +fun real_vector_ineq_prover ctxt translator (ges,gts) =
1.410 + let
1.411 (* val _ = error "real_vector_ineq_prover: pause" *)
1.412 val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
1.413 val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
1.414 @@ -364,13 +362,13 @@
1.415 val gts' = map replace_rule gts
1.416 val nubs = map (conjunct2 o norm_mp) asl
1.417 val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
1.418 - val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
1.419 + val shs = filter (member (fn (t,th) => t aconvc cprop_of th) asl) (#hyps (crep_thm th1))
1.420 val th11 = hd (Variable.export ctxt' ctxt [fold implies_intr shs th1])
1.421 val cps = map (swap o Thm.dest_equals) (cprems_of th11)
1.422 val th12 = instantiate ([], cps) th11
1.423 val th13 = fold Thm.elim_implies (map (reflexive o snd) cps) th12;
1.424 in hd (Variable.export ctxt' ctxt [th13])
1.425 - end
1.426 + end
1.427 in val real_vector_ineq_prover = real_vector_ineq_prover
1.428 end;
1.429
1.430 @@ -380,7 +378,7 @@
1.431 fun simple_cterm_ord t u = Term_Ord.term_ord (term_of t, term_of u) = LESS;
1.432 (* FIXME: Lookup in the context every time!!! Fix this !!!*)
1.433 fun splitequation ctxt th acc =
1.434 - let
1.435 + let
1.436 val real_poly_neg_conv = #neg
1.437 (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
1.438 (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
1.439 @@ -392,22 +390,22 @@
1.440 (fold_rev (splitequation ctxt) eqs ges,gts), RealArith.Trivial)
1.441 end;
1.442
1.443 - fun init_conv ctxt =
1.444 - Simplifier.rewrite (Simplifier.context ctxt
1.445 + fun init_conv ctxt =
1.446 + Simplifier.rewrite (Simplifier.context ctxt
1.447 (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})))
1.448 - then_conv Numeral_Simprocs.field_comp_conv
1.449 + then_conv Numeral_Simprocs.field_comp_conv
1.450 then_conv nnf_conv
1.451
1.452 fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
1.453 - fun norm_arith ctxt ct =
1.454 - let
1.455 + fun norm_arith ctxt ct =
1.456 + let
1.457 val ctxt' = Variable.declare_term (term_of ct) ctxt
1.458 val th = init_conv ctxt' ct
1.459 - in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th))
1.460 + in equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (symmetric th))
1.461 (pure ctxt' (Thm.rhs_of th))
1.462 end
1.463
1.464 - fun norm_arith_tac ctxt =
1.465 + fun norm_arith_tac ctxt =
1.466 clarify_tac HOL_cs THEN'
1.467 Object_Logic.full_atomize_tac THEN'
1.468 CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);