src/HOL/Multivariate_Analysis/normarith.ML
changeset 63627 6ddb43c6b711
parent 63626 44ce6b524ff3
child 63631 2edc8da89edc
child 63633 2accfb71e33b
     1.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri Aug 05 18:34:57 2016 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,414 +0,0 @@
     1.4 -(*  Title:      HOL/Multivariate_Analysis/normarith.ML
     1.5 -    Author:     Amine Chaieb, University of Cambridge
     1.6 -
     1.7 -Simple decision procedure for linear problems in Euclidean space.
     1.8 -*)
     1.9 -
    1.10 -signature NORM_ARITH =
    1.11 -sig
    1.12 - val norm_arith : Proof.context -> conv
    1.13 - val norm_arith_tac : Proof.context -> int -> tactic
    1.14 -end
    1.15 -
    1.16 -structure NormArith : NORM_ARITH =
    1.17 -struct
    1.18 -
    1.19 - open Conv;
    1.20 - val bool_eq = op = : bool *bool -> bool
    1.21 -  fun dest_ratconst t = case Thm.term_of t of
    1.22 -   Const(@{const_name divide}, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
    1.23 - | Const(@{const_name inverse}, _)$a => Rat.make(1, HOLogic.dest_number a |> snd)
    1.24 - | _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
    1.25 - fun is_ratconst t = can dest_ratconst t
    1.26 - fun augment_norm b t acc = case Thm.term_of t of
    1.27 -     Const(@{const_name norm}, _) $ _ => insert (eq_pair bool_eq (op aconvc)) (b,Thm.dest_arg t) acc
    1.28 -   | _ => acc
    1.29 - fun find_normedterms t acc = case Thm.term_of t of
    1.30 -    @{term "op + :: real => _"}$_$_ =>
    1.31 -            find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
    1.32 -      | @{term "op * :: real => _"}$_$_ =>
    1.33 -            if not (is_ratconst (Thm.dest_arg1 t)) then acc else
    1.34 -            augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0)
    1.35 -                      (Thm.dest_arg t) acc
    1.36 -      | _ => augment_norm true t acc
    1.37 -
    1.38 - val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K ~)
    1.39 - fun cterm_lincomb_cmul c t =
    1.40 -    if c = @0 then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
    1.41 - fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = @0) l r
    1.42 - fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
    1.43 - fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
    1.44 -
    1.45 -(*
    1.46 - val int_lincomb_neg = FuncUtil.Intfunc.map (K ~)
    1.47 -*)
    1.48 - fun int_lincomb_cmul c t =
    1.49 -    if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
    1.50 - fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = @0) l r
    1.51 -(*
    1.52 - fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
    1.53 - fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
    1.54 -*)
    1.55 -
    1.56 -fun vector_lincomb t = case Thm.term_of t of
    1.57 -   Const(@{const_name plus}, _) $ _ $ _ =>
    1.58 -    cterm_lincomb_add (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
    1.59 - | Const(@{const_name minus}, _) $ _ $ _ =>
    1.60 -    cterm_lincomb_sub (vector_lincomb (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
    1.61 - | Const(@{const_name scaleR}, _)$_$_ =>
    1.62 -    cterm_lincomb_cmul (dest_ratconst (Thm.dest_arg1 t)) (vector_lincomb (Thm.dest_arg t))
    1.63 - | Const(@{const_name uminus}, _)$_ =>
    1.64 -     cterm_lincomb_neg (vector_lincomb (Thm.dest_arg t))
    1.65 -(* FIXME: how should we handle numerals?
    1.66 - | Const(@ {const_name vec},_)$_ =>
    1.67 -   let
    1.68 -     val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
    1.69 -               handle TERM _=> false)
    1.70 -   in if b then FuncUtil.Ctermfunc.onefunc (t,@1)
    1.71 -      else FuncUtil.Ctermfunc.empty
    1.72 -   end
    1.73 -*)
    1.74 - | _ => FuncUtil.Ctermfunc.onefunc (t,@1)
    1.75 -
    1.76 - fun vector_lincombs ts =
    1.77 -  fold_rev
    1.78 -   (fn t => fn fns => case AList.lookup (op aconvc) fns t of
    1.79 -     NONE =>
    1.80 -       let val f = vector_lincomb t
    1.81 -       in case find_first (fn (_,f') => cterm_lincomb_eq f f') fns of
    1.82 -           SOME (_,f') => (t,f') :: fns
    1.83 -         | NONE => (t,f) :: fns
    1.84 -       end
    1.85 -   | SOME _ => fns) ts []
    1.86 -
    1.87 -fun replacenegnorms cv t = case Thm.term_of t of
    1.88 -  @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
    1.89 -| @{term "op * :: real => _"}$_$_ =>
    1.90 -    if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
    1.91 -| _ => Thm.reflexive t
    1.92 -(*
    1.93 -fun flip v eq =
    1.94 -  if FuncUtil.Ctermfunc.defined eq v
    1.95 -  then FuncUtil.Ctermfunc.update (v, ~ (FuncUtil.Ctermfunc.apply eq v)) eq else eq
    1.96 -*)
    1.97 -fun allsubsets s = case s of
    1.98 -  [] => [[]]
    1.99 -|(a::t) => let val res = allsubsets t in
   1.100 -               map (cons a) res @ res end
   1.101 -fun evaluate env lin =
   1.102 - FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
   1.103 -   lin @0
   1.104 -
   1.105 -fun solve (vs,eqs) = case (vs,eqs) of
   1.106 -  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,@1))
   1.107 - |(_,eq::oeqs) =>
   1.108 -   (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
   1.109 -     [] => NONE
   1.110 -    | v::_ =>
   1.111 -       if FuncUtil.Intfunc.defined eq v
   1.112 -       then
   1.113 -        let
   1.114 -         val c = FuncUtil.Intfunc.apply eq v
   1.115 -         val vdef = int_lincomb_cmul (~ (Rat.inv c)) eq
   1.116 -         fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
   1.117 -                             else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
   1.118 -        in (case solve (remove (op =) v vs, map eliminate oeqs) of
   1.119 -            NONE => NONE
   1.120 -          | SOME soln => SOME (FuncUtil.Intfunc.update (v, evaluate soln (FuncUtil.Intfunc.delete_safe v vdef)) soln))
   1.121 -        end
   1.122 -       else NONE)
   1.123 -
   1.124 -fun combinations k l = if k = 0 then [[]] else
   1.125 - case l of
   1.126 -  [] => []
   1.127 -| h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
   1.128 -
   1.129 -fun vertices vs eqs =
   1.130 - let
   1.131 -  fun vertex cmb = case solve(vs,cmb) of
   1.132 -    NONE => NONE
   1.133 -   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v @0) vs)
   1.134 -  val rawvs = map_filter vertex (combinations (length vs) eqs)
   1.135 -  val unset = filter (forall (fn c => c >= @0)) rawvs
   1.136 - in fold_rev (insert (eq_list op =)) unset []
   1.137 - end
   1.138 -
   1.139 -val subsumes = eq_list (fn (x, y) => Rat.abs x <= Rat.abs y)
   1.140 -
   1.141 -fun subsume todo dun = case todo of
   1.142 - [] => dun
   1.143 -|v::ovs =>
   1.144 -   let val dun' = if exists (fn w => subsumes (w, v)) dun then dun
   1.145 -                  else v:: filter (fn w => not (subsumes (v, w))) dun
   1.146 -   in subsume ovs dun'
   1.147 -   end;
   1.148 -
   1.149 -fun match_mp PQ P = P RS PQ;
   1.150 -
   1.151 -fun cterm_of_rat x =
   1.152 -let val (a, b) = Rat.dest x
   1.153 -in
   1.154 - if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
   1.155 -  else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
   1.156 -                   (Numeral.mk_cnumber @{ctyp "real"} a))
   1.157 -        (Numeral.mk_cnumber @{ctyp "real"} b)
   1.158 -end;
   1.159 -
   1.160 -fun norm_cmul_rule c th = Thm.instantiate' [] [SOME (cterm_of_rat c)] (th RS @{thm norm_cmul_rule_thm});
   1.161 -
   1.162 -fun norm_add_rule th1 th2 = [th1, th2] MRS @{thm norm_add_rule_thm};
   1.163 -
   1.164 -  (* I think here the static context should be sufficient!! *)
   1.165 -fun inequality_canon_rule ctxt =
   1.166 - let
   1.167 -  (* FIXME : Should be computed statically!! *)
   1.168 -  val real_poly_conv =
   1.169 -    Semiring_Normalizer.semiring_normalize_wrapper ctxt
   1.170 -     (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
   1.171 - in
   1.172 -  fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv
   1.173 -    arg_conv (Numeral_Simprocs.field_comp_conv ctxt then_conv real_poly_conv)))
   1.174 -end;
   1.175 -
   1.176 - val apply_pth1 = rewr_conv @{thm pth_1};
   1.177 - val apply_pth2 = rewr_conv @{thm pth_2};
   1.178 - val apply_pth3 = rewr_conv @{thm pth_3};
   1.179 - val apply_pth4 = rewrs_conv @{thms pth_4};
   1.180 - val apply_pth5 = rewr_conv @{thm pth_5};
   1.181 - val apply_pth6 = rewr_conv @{thm pth_6};
   1.182 - val apply_pth7 = rewrs_conv @{thms pth_7};
   1.183 - fun apply_pth8 ctxt =
   1.184 -  rewr_conv @{thm pth_8} then_conv
   1.185 -  arg1_conv (Numeral_Simprocs.field_comp_conv ctxt) then_conv
   1.186 -  (try_conv (rewr_conv (mk_meta_eq @{thm scaleR_zero_left})));
   1.187 - fun apply_pth9 ctxt =
   1.188 -  rewrs_conv @{thms pth_9} then_conv
   1.189 -  arg1_conv (arg1_conv (Numeral_Simprocs.field_comp_conv ctxt));
   1.190 - val apply_ptha = rewr_conv @{thm pth_a};
   1.191 - val apply_pthb = rewrs_conv @{thms pth_b};
   1.192 - val apply_pthc = rewrs_conv @{thms pth_c};
   1.193 - val apply_pthd = try_conv (rewr_conv @{thm pth_d});
   1.194 -
   1.195 -fun headvector t = case t of
   1.196 -  Const(@{const_name plus}, _)$
   1.197 -   (Const(@{const_name scaleR}, _)$_$v)$_ => v
   1.198 - | Const(@{const_name scaleR}, _)$_$v => v
   1.199 - | _ => error "headvector: non-canonical term"
   1.200 -
   1.201 -fun vector_cmul_conv ctxt ct =
   1.202 -   ((apply_pth5 then_conv arg1_conv (Numeral_Simprocs.field_comp_conv ctxt)) else_conv
   1.203 -    (apply_pth6 then_conv binop_conv (vector_cmul_conv ctxt))) ct
   1.204 -
   1.205 -fun vector_add_conv ctxt ct = apply_pth7 ct
   1.206 - handle CTERM _ =>
   1.207 -  (apply_pth8 ctxt ct
   1.208 -   handle CTERM _ =>
   1.209 -    (case Thm.term_of ct of
   1.210 -     Const(@{const_name plus},_)$lt$rt =>
   1.211 -      let
   1.212 -       val l = headvector lt
   1.213 -       val r = headvector rt
   1.214 -      in (case Term_Ord.fast_term_ord (l,r) of
   1.215 -         LESS => (apply_pthb then_conv arg_conv (vector_add_conv ctxt)
   1.216 -                  then_conv apply_pthd) ct
   1.217 -        | GREATER => (apply_pthc then_conv arg_conv (vector_add_conv ctxt)
   1.218 -                     then_conv apply_pthd) ct
   1.219 -        | EQUAL => (apply_pth9 ctxt then_conv
   1.220 -                ((apply_ptha then_conv (vector_add_conv ctxt)) else_conv
   1.221 -              arg_conv (vector_add_conv ctxt) then_conv apply_pthd)) ct)
   1.222 -      end
   1.223 -     | _ => Thm.reflexive ct))
   1.224 -
   1.225 -fun vector_canon_conv ctxt ct = case Thm.term_of ct of
   1.226 - Const(@{const_name plus},_)$_$_ =>
   1.227 -  let
   1.228 -   val ((p,l),r) = Thm.dest_comb ct |>> Thm.dest_comb
   1.229 -   val lth = vector_canon_conv ctxt l
   1.230 -   val rth = vector_canon_conv ctxt r
   1.231 -   val th = Drule.binop_cong_rule p lth rth
   1.232 -  in fconv_rule (arg_conv (vector_add_conv ctxt)) th end
   1.233 -
   1.234 -| Const(@{const_name scaleR}, _)$_$_ =>
   1.235 -  let
   1.236 -   val (p,r) = Thm.dest_comb ct
   1.237 -   val rth = Drule.arg_cong_rule p (vector_canon_conv ctxt r)
   1.238 -  in fconv_rule (arg_conv (apply_pth4 else_conv (vector_cmul_conv ctxt))) rth
   1.239 -  end
   1.240 -
   1.241 -| Const(@{const_name minus},_)$_$_ => (apply_pth2 then_conv (vector_canon_conv ctxt)) ct
   1.242 -
   1.243 -| Const(@{const_name uminus},_)$_ => (apply_pth3 then_conv (vector_canon_conv ctxt)) ct
   1.244 -
   1.245 -(* FIXME
   1.246 -| Const(@{const_name vec},_)$n =>
   1.247 -  let val n = Thm.dest_arg ct
   1.248 -  in if is_ratconst n andalso not (dest_ratconst n =/ @0)
   1.249 -     then Thm.reflexive ct else apply_pth1 ct
   1.250 -  end
   1.251 -*)
   1.252 -| _ => apply_pth1 ct
   1.253 -
   1.254 -fun norm_canon_conv ctxt ct = case Thm.term_of ct of
   1.255 -  Const(@{const_name norm},_)$_ => arg_conv (vector_canon_conv ctxt) ct
   1.256 - | _ => raise CTERM ("norm_canon_conv", [ct])
   1.257 -
   1.258 -fun int_flip v eq =
   1.259 -  if FuncUtil.Intfunc.defined eq v
   1.260 -  then FuncUtil.Intfunc.update (v, ~ (FuncUtil.Intfunc.apply eq v)) eq else eq;
   1.261 -
   1.262 -local
   1.263 - val pth_zero = @{thm norm_zero}
   1.264 - val tv_n =
   1.265 -  (dest_TVar o Thm.typ_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of)
   1.266 -    pth_zero
   1.267 - val concl = Thm.dest_arg o Thm.cprop_of
   1.268 - fun real_vector_combo_prover ctxt translator (nubs,ges,gts) =
   1.269 -  let
   1.270 -   (* FIXME: Should be computed statically!!*)
   1.271 -   val real_poly_conv =
   1.272 -      Semiring_Normalizer.semiring_normalize_wrapper ctxt
   1.273 -       (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"}))
   1.274 -   val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
   1.275 -   val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
   1.276 -   val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
   1.277 -           else ()
   1.278 -   val dests = distinct (op aconvc) (map snd rawdests)
   1.279 -   val srcfuns = map vector_lincomb sources
   1.280 -   val destfuns = map vector_lincomb dests
   1.281 -   val vvs = fold_rev (union (op aconvc) o FuncUtil.Ctermfunc.dom) (srcfuns @ destfuns) []
   1.282 -   val n = length srcfuns
   1.283 -   val nvs = 1 upto n
   1.284 -   val srccombs = srcfuns ~~ nvs
   1.285 -   fun consider d =
   1.286 -    let
   1.287 -     fun coefficients x =
   1.288 -      let
   1.289 -       val inp =
   1.290 -        if FuncUtil.Ctermfunc.defined d x
   1.291 -        then FuncUtil.Intfunc.onefunc (0, ~ (FuncUtil.Ctermfunc.apply d x))
   1.292 -        else FuncUtil.Intfunc.empty
   1.293 -      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.294 -      end
   1.295 -     val equations = map coefficients vvs
   1.296 -     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,@1)) nvs
   1.297 -     fun plausiblevertices f =
   1.298 -      let
   1.299 -       val flippedequations = map (fold_rev int_flip f) equations
   1.300 -       val constraints = flippedequations @ inequalities
   1.301 -       val rawverts = vertices nvs constraints
   1.302 -       fun check_solution v =
   1.303 -        let
   1.304 -          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, @1))
   1.305 -        in forall (fn e => evaluate f e = @0) flippedequations
   1.306 -        end
   1.307 -       val goodverts = filter check_solution rawverts
   1.308 -       val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
   1.309 -      in map (map2 (fn s => fn c => Rat.of_int s * c) signfixups) goodverts
   1.310 -      end
   1.311 -     val allverts = fold_rev append (map plausiblevertices (allsubsets nvs)) []
   1.312 -    in subsume allverts []
   1.313 -    end
   1.314 -   fun compute_ineq v =
   1.315 -    let
   1.316 -     val ths = map_filter (fn (v,t) => if v = @0 then NONE
   1.317 -                                     else SOME(norm_cmul_rule v t))
   1.318 -                            (v ~~ nubs)
   1.319 -     fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)
   1.320 -    in inequality_canon_rule ctxt (end_itlist norm_add_rule ths)
   1.321 -    end
   1.322 -   val ges' = map_filter (try compute_ineq) (fold_rev (append o consider) destfuns []) @
   1.323 -                 map (inequality_canon_rule ctxt) nubs @ ges
   1.324 -   val zerodests = filter
   1.325 -        (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests)
   1.326 -
   1.327 -  in fst (RealArith.real_linear_prover translator
   1.328 -        (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_cterm t)],[]) pth_zero)
   1.329 -            zerodests,
   1.330 -        map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
   1.331 -                       arg_conv (arg_conv real_poly_conv))) ges',
   1.332 -        map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv
   1.333 -                       arg_conv (arg_conv real_poly_conv))) gts))
   1.334 -  end
   1.335 -in val real_vector_combo_prover = real_vector_combo_prover
   1.336 -end;
   1.337 -
   1.338 -local
   1.339 - val pth = @{thm norm_imp_pos_and_ge}
   1.340 - val norm_mp = match_mp pth
   1.341 - val concl = Thm.dest_arg o Thm.cprop_of
   1.342 - fun conjunct1 th = th RS @{thm conjunct1}
   1.343 - fun conjunct2 th = th RS @{thm conjunct2}
   1.344 -fun real_vector_ineq_prover ctxt translator (ges,gts) =
   1.345 - let
   1.346 -(*   val _ = error "real_vector_ineq_prover: pause" *)
   1.347 -  val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) []
   1.348 -  val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   1.349 -  val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
   1.350 -  fun instantiate_cterm' ty tms = Drule.cterm_rule (Thm.instantiate' ty tms)
   1.351 -  fun mk_norm t =
   1.352 -    let val T = Thm.typ_of_cterm t
   1.353 -    in Thm.apply (Thm.cterm_of ctxt' (Const (@{const_name norm}, T --> @{typ real}))) t end
   1.354 -  fun mk_equals l r =
   1.355 -    let
   1.356 -      val T = Thm.typ_of_cterm l
   1.357 -      val eq = Thm.cterm_of ctxt (Const (@{const_name Pure.eq}, T --> T --> propT))
   1.358 -    in Thm.apply (Thm.apply eq l) r end
   1.359 -  val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Thm.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns
   1.360 -  val replace_conv = try_conv (rewrs_conv asl)
   1.361 -  val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
   1.362 -  val ges' =
   1.363 -       fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths)
   1.364 -              asl (map replace_rule ges)
   1.365 -  val gts' = map replace_rule gts
   1.366 -  val nubs = map (conjunct2 o norm_mp) asl
   1.367 -  val th1 = real_vector_combo_prover ctxt' translator (nubs,ges',gts')
   1.368 -  val shs = filter (member (fn (t,th) => t aconvc Thm.cprop_of th) asl) (Thm.chyps_of th1)
   1.369 -  val th11 = hd (Variable.export ctxt' ctxt [fold Thm.implies_intr shs th1])
   1.370 -  val cps = map (swap o Thm.dest_equals) (cprems_of th11)
   1.371 -  val th12 = Drule.instantiate_normalize ([], map (apfst (dest_Var o Thm.term_of)) cps) th11
   1.372 -  val th13 = fold Thm.elim_implies (map (Thm.reflexive o snd) cps) th12;
   1.373 - in hd (Variable.export ctxt' ctxt [th13])
   1.374 - end
   1.375 -in val real_vector_ineq_prover = real_vector_ineq_prover
   1.376 -end;
   1.377 -
   1.378 -local
   1.379 - val rawrule = fconv_rule (arg_conv (rewr_conv @{thm real_eq_0_iff_le_ge_0}))
   1.380 - fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   1.381 - fun simple_cterm_ord t u = Term_Ord.term_ord (Thm.term_of t, Thm.term_of u) = LESS;
   1.382 -  (* FIXME: Lookup in the context every time!!! Fix this !!!*)
   1.383 - fun splitequation ctxt th acc =
   1.384 -  let
   1.385 -   val real_poly_neg_conv = #neg
   1.386 -       (Semiring_Normalizer.semiring_normalizers_ord_wrapper ctxt
   1.387 -        (the (Semiring_Normalizer.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
   1.388 -   val (th1,th2) = conj_pair(rawrule th)
   1.389 -  in th1::fconv_rule (arg_conv (arg_conv (real_poly_neg_conv ctxt))) th2::acc
   1.390 -  end
   1.391 -in fun real_vector_prover ctxt _ translator (eqs,ges,gts) =
   1.392 -     (real_vector_ineq_prover ctxt translator
   1.393 -         (fold_rev (splitequation ctxt) eqs ges,gts), RealArith.Trivial)
   1.394 -end;
   1.395 -
   1.396 -  fun init_conv ctxt =
   1.397 -   Simplifier.rewrite (put_simpset HOL_basic_ss ctxt
   1.398 -    addsimps ([(*@{thm vec_0}, @{thm vec_1},*) @{thm dist_norm}, @{thm right_minus},
   1.399 -      @{thm diff_self}, @{thm norm_zero}] @ @{thms arithmetic_simps} @ @{thms norm_pths}))
   1.400 -   then_conv Numeral_Simprocs.field_comp_conv ctxt
   1.401 -   then_conv nnf_conv ctxt
   1.402 -
   1.403 - fun pure ctxt = fst o RealArith.gen_prover_real_arith ctxt (real_vector_prover ctxt);
   1.404 - fun norm_arith ctxt ct =
   1.405 -  let
   1.406 -   val ctxt' = Variable.declare_term (Thm.term_of ct) ctxt
   1.407 -   val th = init_conv ctxt' ct
   1.408 -  in Thm.equal_elim (Drule.arg_cong_rule @{cterm Trueprop} (Thm.symmetric th))
   1.409 -                (pure ctxt' (Thm.rhs_of th))
   1.410 - end
   1.411 -
   1.412 - fun norm_arith_tac ctxt =
   1.413 -   clarify_tac (put_claset HOL_cs ctxt) THEN'
   1.414 -   Object_Logic.full_atomize_tac ctxt THEN'
   1.415 -   CSUBGOAL ( fn (p,i) => resolve_tac ctxt [norm_arith ctxt (Thm.dest_arg p )] i);
   1.416 -
   1.417 -end;