Handle paired-abstractions better

[mn200]

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]

When? By the simplifier?

[mn200]

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

When? By the simplifier?

Yeah; in srw_ss() with an appropriate conversion.

[thtuerk]

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]

The pairarg_tac tactic does this for unbound arguments.