Thanks for the help.
James
On Feb 19, 2020 02:56, jrh...@gmail.com wrote:
Yes, here's one explicit HOL Light realization of Konrad's solution:
let POLYNOMIAL_DEGREE_COEFFS =
let th = prove
(`?m c. !p. polynomial_function p
==> !x. p x = sum(0..m p) (\i. c p i * x pow
Yes, here's one explicit HOL Light realization of Konrad's solution:
let POLYNOMIAL_DEGREE_COEFFS =
let th = prove
(`?m c. !p. polynomial_function p
==> !x. p x = sum(0..m p) (\i. c p i * x pow i)`,
REWRITE_TAC[GSYM SKOLEM_THM] THEN
If you have |- !p. ?m c. ... as a theorem, then you are set up to use
constant specification. Just have to apply SKOLEM_THM to move the
existentials out to the top level .
Konrad.
On Tue, Feb 18, 2020 at 4:33 PM Norrish, Michael (Data61, Acton) <
michael.norr...@data61.csiro.au> wrote:
> Maybe
Maybe use the choice function to select a pair. I.e., write
@(m,c). .
?
Michael
On 19 Feb 2020, at 09:30, "jpe...@student.bham.ac.uk"
wrote:
Hi
This is a question about using the select operator @ to return multiple values
which depend on each other in HOL Light.
For example
