Quantification over Define's result

[mn200]

The following seems to be a mild regression:

val _ = Datatype`inum = inum num | infty`;
val ilt_def = Define`
  (ilt (inum x) (inum y) <=> x < y) ∧
  (ilt (inum _) infty    <=> T) ∧
  (ilt infty _           <=> F)
`;

giving as return value

Equations stored under "ilt_def".
Induction stored under "ilt_ind".
val ilt_def =
   |- ∀y x v1 v0.
     (ilt (inum x) (inum y) ⇔ x < y) ∧ (ilt (inum v0) infty ⇔ T) ∧
     (ilt infty v1 ⇔ F):
   thm

Notice how the universal quantifiers have been lifted to the top-level. Once upon a time, they used to stick with the relevant clauses. This breaks some old code (easily fixed), but is also a tad on the ugly side.

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[konrad-slind]

To the best of my recall, Define wouldn't return equations with a particular quantification format. If a definition happened to be prim. rec. then each clause would be quantified. But if a wf. rec. definition was needed then I don't think any effort was made to quantify every resulting clause.

.... having done some experiments, it seems that this has changed in the interim (or that my recall is faulty).

Konrad.

On Sun, Aug 10, 2014 at 7:47 PM, Michael Norrish notifications@github.com wrote:

The following seems to be a mild regression:

val _ = Datatypeinum = inum num | infty; val iltdef = Define` (ilt (inum x) (inum y) <=> x < y) ∧ (ilt (inum ) infty <=> T) ∧ (ilt infty _ <=> F) `;

giving as return value

Equations stored under "ilt_def". Induction stored under "ilt_ind". val ilt_def = |- ∀y x v1 v0. (ilt (inum x) (inum y) ⇔ x < y) ∧ (ilt (inum v0) infty ⇔ T) ∧ (ilt infty v1 ⇔ F): thm

Notice how the universal quantifiers have been lifted to the top-level. Once upon a time, they used to stick with the relevant clauses. This breaks some old code (easily fixed), but is also a tad on the ugly side.

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/186.

[xrchz]

Ideally I think the specification of Define should be to return a theorem that is exactly the same as the input quotation, after a substitution of new constants for variables. Any post-processing to introduce/remove quantifiers, do alpha-renaming, or eta-conversion should be the responsibility of Define. I'm happy for this issue to be reused for this goal, or to open a new one...

[xrchz]

58 and #59 and possibly #114 are related.