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