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 i)`, REWRITE_TAC[GSYM SKOLEM_THM] THEN MESON_TAC[polynomial_function]) in REWRITE_RULE[RIGHT_IMP_FORALL_THM] (new_specification ["polynomial_degree"; "polynomial_coeffs"] th);; This gives you the following theorem val POLYNOMIAL_DEGREE_COEFFS : thm = |- !p x. polynomial_function p ==> p x = sum (0..polynomial_degree p) (\i. polynomial_coeffs p i * x pow i) Instead of this direct Skolemization you could instead choose to define these concepts in a more refined way with minimal degree and coefficients having a zero tail, something like this: let polynomial_deg = new_definition `polynomial_deg p = minimal m. ?c. !x. p x = sum(0..m) (\i. c i * x pow i)`;; let polynomial_cfs = new_definition `polynomial_cfs p = \i. if i <= polynomial_deg p then (@c. !x. p x = sum(0..polynomial_deg p) (\i. c i * x pow i)) i else &0`;; let POLYNOMIAL_DEG_CFS = prove (`!p x. polynomial_function p ==> p x = sum (0..polynomial_deg p) (\i. polynomial_cfs p i * x pow i)`, REPEAT GEN_TAC THEN REWRITE_TAC[polynomial_function] THEN GEN_REWRITE_TAC LAND_CONV [MINIMAL] THEN REWRITE_TAC[GSYM polynomial_deg] THEN DISCH_THEN(MP_TAC o SELECT_RULE o CONJUNCT1) THEN DISCH_THEN(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN MATCH_MP_TAC SUM_EQ_NUMSEG THEN SIMP_TAC[polynomial_cfs]);; But the main point is again that once you've got this and maybe a few other lemmas, you probably don't need much if any manual handling of select-terms at all. John. On Tue, Feb 18, 2020 at 5:09 PM Konrad Slind <konrad.sl...@gmail.com<mailto:konrad.sl...@gmail.com>> wrote: 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<mailto: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<mailto:jpe...@student.bham.ac.uk>" <jpe...@student.bham.ac.uk<mailto: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<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto: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