search

HOL-Theorem-Prover / HOL

Canonical sources for HOL4 theorem-proving system. Branch develop is where “mainline development” occurs; when develop passes our regression tests, master is merged forward to catch up.
https://hol-theorem-prover.org
Other
610 stars 133 forks source link

Handle paired-abstractions better #7

Open mn200 opened 12 years ago

mn200 commented 12 years ago

In particular, if there is a quantifier over a variable of pair type, and that same variable is an argument to a paired abstraction, then the quantifier should be rewritten to pick up the abstraction's names, and the abstraction should be β-reduced.

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

xrchz commented 12 years ago

When? By the simplifier?

mn200 commented 12 years ago

On 6/09/11 5:08 PM, xrchz wrote:

When? By the simplifier?

Yeah; in srw_ss() with an appropriate conversion.

thtuerk commented 7 years ago

Something like this is implemented in the quantifier heuristics lib. There is no fast, special purpose conversion, though.

> SIMP_CONV (std_ss++QI_ss) [] ``!xyz. P ((\(aa, cc, bb). f aa bb cc) xyz)``

val it =
   |- (!xyz. P ((\(aa,cc,bb). f aa bb cc) xyz)) <=>
   !aa cc bb. P (f aa bb cc):
   thm
mn200 commented 9 months ago

The pairarg_tac tactic does this for unbound arguments.