Re: [isabelle] axiom of choice in Isabelle/HOL, and sledgehammer



> On 02.02.2016, at 23:41, Thomas Sewell <Thomas.Sewell at nicta.com.au> wrote:
> 
> I played around with this about a year ago, and discovered that this
> doesn't buy you much in modern Isabelle. The lifting and transfer
> packages seem to make extensive use of Eps, and pretty much everything
> that isn't a natural seems to now use lifting/transfer in the definition
> of some primitive functions. Even proofs about naturals seem to depend
> on the axiom about Eps because the simprocs about naturals sometimes
> coerce to integers, and int/of_nat is defined by lifting/transfer.

In addition, the BNF (co)datatype package uses "Eps" in a few places. Granted, some of it could be avoided, e.g.

    HOLogic.choice_const T $ absdummy T @{term True}

could (and perhaps should) be replaced by

    Const (@{const_name undefined}, T)

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.