Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Extracting assumptions from an Isar proof

Email Gateway (Aug 18 2022 at 15:06):

From: Michael Chan <mchan@inf.ed.ac.uk>
Hi all,

Does anyone know if there's a parser for Isar proofs? In particular,
are there existing ways for extracting the assumptions used in a
particular proof given a .thy file? Thanks.

Michael

Postal Address: School of Informatics, University of Edinburgh,
Room 2.05, Informatics Forum, 10 Crichton Street, Edinburgh
EH8 9AB, UK.
Telephone Number: +44-131-651-3077
Fax Number: +44-131-650-6899,
Email: M.Chan@ed.ac.uk.
Web Page: http://homepages.inf.ed.ac.uk/mchan/

Email Gateway (Aug 18 2022 at 15:06):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Dear Michael,

I'm not sure I totally understand what you want to do. By assumptions,
do you mean the theorems used in the proof?

Jasmin

Email Gateway (Aug 18 2022 at 15:07):

From: Michael Chan <mchan@inf.ed.ac.uk>
On 16/04/10 08:39, Jasmin Blanchette wrote:

Dear Michael,

Does anyone know if there's a parser for Isar proofs? In particular,
are there existing ways for extracting the assumptions used in a
particular proof given a .thy file?

I'm not sure I totally understand what you want to do. By assumptions,
do you mean the theorems used in the proof?

Yes, that's right. Can all theorems used in a proof be extracted?

Michael

Jasmin

Last updated: May 07 2024 at 01:07 UTC