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 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" <
> 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 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 use the @ operator to return the upper bound
> m and the coefficient function c, however as the choice of m depends on c
> and visa versa you cannot use 2 separate select statements. (e.g. if m >
> degree(p) then c(n) must be 0 for degree(p)<n<=m )
>
> What is the best way to approach this? Is there a way to return both of
> the values or would they have to be "combined together" inside the select
> statement?
>
>  Thanks
>
> James
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to