Email Gateway (Aug 17 2022 at 14:15): Email Gateway (Aug 17 2022 at 14:15):From: Paqui Lucio <paqui.lucio@ehu.es>
Hi,
I am defining a new logic over Pure (indeed, I have almost achieve it).
Now, I am trying to prove theorems using the rules (axioms) of my logic.
However, I cannot use elemental commands like "by", or tactics like
"blast". It seems like I need Main (instead of Pure) to use them. Is
that true? In the positive case, what can I do to use this features
without using Main. The problem is that I use Sequents.thy which is
problematics to mix with Main.
Email Gateway (Aug 17 2022 at 14:15):From: Lawrence Paulson <lp15@cam.ac.uk>
Commands like "by" and tactics like "blast" are very different
things. If you have set up your logic correctly--and I admit that we
don't provide much documentation for people who set up new logics--
then the entire Isar proof language should be available to you.
However, tactics like "blast", "simp" and "auto" rely upon specific
inference rules being present in your logic. They need to be set up
separately for each logic. I'd be surprised if "blast" or "auto" can
be got working at all on top of a sequent-based logic, although a
very crude blast-like tactic is available.
Larry Paulson
Email Gateway (Aug 17 2022 at 14:16):From: Lucas Dixon <ldixon@inf.ed.ac.uk>
I recall seeing blast_tac being used in the theory of ILL, also based on
Sequents, by Sara Kalvala and Valeria de Paiva. They have a paper
(ftp://ftp.dcs.warwick.ac.uk/people/Sara.Kalvala/lli.dvi) which talks
about this. This was done before Isar, so they don't have an Isar
bindings for blast but I guess you could make one for your logic so that
it can be used in the Isar scripts for your logic.
See:
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/library/Sequents/ILL.html
http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/library/Sequents/ILL.ML.html
best,
lucas
Lawrence Paulson wrote:
Last updated: May 03 2024 at 04:19 UTC