Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] About using frule with impI


view this post on Zulip Email Gateway (Mar 02 2022 at 10:55):

From: FRANCISCO JESUS MARTIN MATEOS <fjesus@us.es>
Hello

I teach Mathematical Logic at University of Seville and I use Isabelle to explain natural deduction rules.
I have found a situation difficult to explain to my students. It happens when we use 'frule' with 'impI', for example, in order to prove
"(P ⟹ Q) ⟹ P ⟶ Q" (this is a simplified situation):

A typical proof could be:

lemma
"(P ⟹ Q) ⟹ P ⟶ Q"
apply (drule impI)
apply assumption
done

But if I use 'frule' instead of 'drule' the new goal generated is:
(P ⟹ Q) ⟹ ?P ⟶ ?P ⟹ P ⟶ Q

I consider that 'drule' is the same as 'frule' but dropping the assumption used to unify the premise, as is indicated in https://svhol.pbmichel.com/reference/frule, so I don't understand why the new hypotesis included by 'frule' is '?P ⟶ ?P'.
Moreover, (frule_tac P="P" and Q="Q" in impI) does not work.
Could you explain me this?

Thanks in advance.
Regards

Francisco J. Martín Mateos
Computational Logic Group
University of Seville

view this post on Zulip Email Gateway (Mar 02 2022 at 11:35):

From: Lawrence Paulson <lp15@cam.ac.uk>
Dear Francisco,

These low-level natural deduction proof methods need to be used with the correct sort of natural deduction inference rule. These are classified as

To me the mystery is not that frule exhibits the behaviour you show, but that either drule or frule succeed at all. They are intended to operate on a formula of the object logic (i.e., first-order or higher-order logic) and not on anything of the form P ==> Q, which is a formula of the logical framework itself.

Try your examples using the appropriate proof method and see how that goes.

Larry Paulson


Last updated: Mar 29 2024 at 12:28 UTC