Re: [isabelle] "by", "blast", etc without importing Main



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:
> 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
> 
> 
> On 7 Apr 2006, at 15:39, Paqui Lucio wrote:
> 
>> 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.





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