*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Removing trivial premises*From*: Makarius <makarius at sketis.net>*Date*: Fri, 20 May 2016 11:45:52 +0200*In-reply-to*: <573E11F1.7030101@uibk.ac.at>*References*: <573E11F1.7030101@uibk.ac.at>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.7.2

On 19/05/16 21:20, Michael FÃrber wrote: > when I resolve theorems, I sometimes obtain trivial premises such as in > this case: > > ~~~ > val th1 = Thm.assume @{cprop "P ==> Q"} > val th2 = Thm.assume @{cprop "(P ==> Q) ==> R"} > val th3 = th2 OF [th1] > ~~~ > > This produces a th3 with proposition "(P ==> P) ==> R". > However, I would like to obtain only "R". Larry Paulson introduced the concept of "elim-resolution" for that around 1989. Apart from the original papers from that time, it is also briefly explained in the "implementation" manual in section 4.2.1 â for tactical backwards proof. In principle, it is possible to make elim versions of the forward proof combinators (RS, OF), but it is not done, because backwards proof scales better to real applications. > So what is the canonical way to deal with trivial premises? The canonical way is to avoid getting them in the first place, i.e. via elim-resolution. > P.S.: I know that in Isar, trivial premises can be eliminated when > closing a proof with ".", but I do not know how to do that in ML. > Reading the source for hours unfortunately did not bring me > enlightenment yet. :) Reading sources is important, but one needs to have an idea about the general concepts behind them. Apart from the original published literature (which is naturally a bit outdated), the canonical entry points are the "implementation" manual and the "isar-ref" manual. The Prover IDE also helps a lot to navigate around, e.g. to find the Isabelle/ML definitions of Isabelle/Isar commands. The implicit finishing of the left-over proof state in structured Isar proofs is defined in src/Pure/Isar/method.ML as "finish". This is very specific for how Isar works. It is unlikely to make much sense in a different context. Makarius

**References**:**[isabelle] Removing trivial premises***From:*Michael FÃrber

- Previous by Date: Re: [isabelle] Shortest way to prove an object-level implication via ML
- Next by Date: [isabelle] A single way to reference AFP entries
- Previous by Thread: [isabelle] Removing trivial premises
- Next by Thread: Re: [isabelle] Removing trivial premises
- Cl-isabelle-users May 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