equal
deleted
inserted
replaced
351 let |
351 let |
352 (* val _ = error "real_vector_ineq_prover: pause" *) |
352 (* val _ = error "real_vector_ineq_prover: pause" *) |
353 val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) [] |
353 val ntms = fold_rev find_normedterms (map (dest_arg o concl) (ges @ gts)) [] |
354 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
354 val lctab = vector_lincombs (map snd (filter (not o fst) ntms)) |
355 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
355 val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt |
356 fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: norm) => real"}) t |
356 fun mk_norm t = capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t |
357 fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
357 fun mk_equals l r = capply (capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r |
358 val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns |
358 val asl = map2 (fn (t,_) => fn n => assume (mk_equals (mk_norm t) (cterm_of (ProofContext.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns |
359 val replace_conv = try_conv (rewrs_conv asl) |
359 val replace_conv = try_conv (rewrs_conv asl) |
360 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
360 val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv)) |
361 val ges' = |
361 val ges' = |