Re: [isabelle] Removing trivial premises



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








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