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
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
Hi
This is a question about using the select operator @ to return multiple values
which depend on each other in HOL Light.
For example when working with polynomial_function defined as
polynomial_function p <=> ?m c. !x. p x = sum(0..m) (\i. c i * x pow i) it
might be useful to be able to
CALL FOR WORKSHOPS AND TUTORIALS
LPAR-23: 23rd International Conference on Logic for Programming,
Artificial Intelligence and Reasoning
22-27 May, 2020, Alicante, Spain
https://easychair.org/smart-program/LPAR23/
Workshop and tutorial proposals for LPAR-23 are solicited.
These events will take
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
