*To*: stark at cs.stonybrook.edu*Subject*: Re: [isabelle] "apply auto" transforms provable statement to something false?*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 25 Jan 2016 11:57:59 +0000*Cc*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <56A608E1.1020508@starkeffect.com>*References*: <56A600CE.7040604@starkeffect.com> <56A606D8.3000302@inf.ethz.ch> <56A608E1.1020508@starkeffect.com>

I havenât tried your particular example, but other examples are very easy to generate. Suppose you want to prove âx. x=0 & x=1.Then you can easily give yourself the two subgoals ?x=0 and ?x=1. Then auto will solve one and replace the other by False. Larry Paulson > On 25 Jan 2016, at 11:37, Eugene W. Stark <isabelle-users at starkeffect.com> wrote: > > I wouldn't be surprised if the resulting subgoal was simply unprovable. > What I am surprised about is the fact that it is false. But I suppose > that an incorrect instantiation of a schematic variable could produce > this behavior. In my limited mind's eye view of how theorem provers work, > I was assuming that the instances would be generated by unification > during resolution or something, which would not reduce true goals to > false (not merely unprovable) subgoals.

**References**:**[isabelle] "apply auto" transforms provable statement to something false?***From:*Eugene W. Stark

**Re: [isabelle] "apply auto" transforms provable statement to something false?***From:*Andreas Lochbihler

**Re: [isabelle] "apply auto" transforms provable statement to something false?***From:*Eugene W. Stark

- Previous by Date: Re: [isabelle] "apply auto" transforms provable statement to something false?
- Next by Date: Re: [isabelle] "defines" in a locale
- Previous by Thread: Re: [isabelle] "apply auto" transforms provable statement to something false?
- Next by Thread: [isabelle] simplifying functions on tuples
- Cl-isabelle-users January 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list