Re: [Hol-info] Using @ for multiple selections in HOL Light

2020-02-20 Thread jpe...@student.bham.ac.uk 
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 
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) 
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>> 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)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
___
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

Re: [Hol-info] Using @ for multiple selections in HOL Light

2020-02-18 Thread John R Harrison 
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  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> 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)>
>> 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
>
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info

Re: [Hol-info] Using @ for multiple selections in HOL Light

2020-02-18 Thread Konrad Slind 
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)
> 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

Re: [Hol-info] Using @ for multiple selections in HOL Light

2020-02-18 Thread Norrish, Michael (Data61, Acton) 
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 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)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