256 if FuncUtil.Intfunc.defined eq v |
256 if FuncUtil.Intfunc.defined eq v |
257 then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq; |
257 then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq; |
258 |
258 |
259 local |
259 local |
260 val pth_zero = @{thm norm_zero} |
260 val pth_zero = @{thm norm_zero} |
261 val tv_n = (Thm.ctyp_of_term o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) |
261 val tv_n = (Thm.ctyp_of_cterm o Thm.dest_arg o Thm.dest_arg1 o Thm.dest_arg o Thm.cprop_of) |
262 pth_zero |
262 pth_zero |
263 val concl = Thm.dest_arg o Thm.cprop_of |
263 val concl = Thm.dest_arg o Thm.cprop_of |
264 fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = |
264 fun real_vector_combo_prover ctxt translator (nubs,ges,gts) = |
265 let |
265 let |
266 (* FIXME: Should be computed statically!!*) |
266 (* FIXME: Should be computed statically!!*) |
317 map (inequality_canon_rule ctxt) nubs @ ges |
317 map (inequality_canon_rule ctxt) nubs @ ges |
318 val zerodests = filter |
318 val zerodests = filter |
319 (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests) |
319 (fn t => null (FuncUtil.Ctermfunc.dom (vector_lincomb t))) (map snd rawdests) |
320 |
320 |
321 in fst (RealArith.real_linear_prover translator |
321 in fst (RealArith.real_linear_prover translator |
322 (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_term t)],[]) pth_zero) |
322 (map (fn t => Drule.instantiate_normalize ([(tv_n, Thm.ctyp_of_cterm t)],[]) pth_zero) |
323 zerodests, |
323 zerodests, |
324 map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv |
324 map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv |
325 arg_conv (arg_conv real_poly_conv))) ges', |
325 arg_conv (arg_conv real_poly_conv))) ges', |
326 map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv |
326 map (fconv_rule (try_conv (Conv.top_sweep_conv (K (norm_canon_conv ctxt)) ctxt) then_conv |
327 arg_conv (arg_conv real_poly_conv))) gts)) |
327 arg_conv (arg_conv real_poly_conv))) gts)) |
340 (* val _ = error "real_vector_ineq_prover: pause" *) |
340 (* val _ = error "real_vector_ineq_prover: pause" *) |
341 val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) [] |
341 val ntms = fold_rev find_normedterms (map (Thm.dest_arg o concl) (ges @ gts)) [] |
342 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
342 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
343 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
343 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
344 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) |
344 fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms) |
345 fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t |
345 fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t |
346 fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
346 fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (Thm.ctyp_of_cterm l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
347 val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Proof_Context.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns |
347 val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (Proof_Context.cterm_of ctxt' (Free(n,@{typ real}))))) lctab fxns |
348 val replace_conv = try_conv (rewrs_conv asl) |
348 val replace_conv = try_conv (rewrs_conv asl) |
349 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
349 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
350 val ges' = |
350 val ges' = |
351 fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) |
351 fold_rev (fn th => fn ths => conjunct1(norm_mp th)::ths) |