I have Isabelle/HOL theory, how can I proceed with its application?

Question

I am trying to understand the use of Isabelle/HOL theory. I have written and saved a theory file:

theory MonoidalLogic
  imports sequents
begin
consts
  Test :: "test"
axiomatization where
  identity "φ⊢φ" and
  cut "φ⊢ψ;ψ⊢ρ⟹φ⊢ρ"
  l "φ⊢⊤⨂ψ⟺φ⊢ψ"
  r "φ⊢ψ⨂⊤⟺φ⊢ψ"
end

Now I would like to get some feedback about this theory - is it accepted by Isabelle, somehow compile it - how can I do this? And after this - I would like to use this theory - e.g. write some lemma and invoke interactive proof session for this. How can I do this? I can enter theory in jEdit dialog but I am not receiving any feedback. I don't understand how should I close this theory file and start interactive session from which I can use this theory file?

As far as I understand, then I should:

write initial theory file;
invoke interactive session where I can find proofs of some lemmas for this theory
If I have managed to find proofs of lemmas then I can add those lemmas in my theory file for further immediate use in other proofs (no need for repeated proof of them).

I am reading Concrete Semantics, LNCS tutorials and other tutorials but I don't see the example of this basic workflow - how to do this workflow and whether I understand it correctly.

My intention is to take this logic http://www.sciencedirect.com/science/article/pii/S1570868314000573 and create theorem prover for this logic in Isabelle/HOL, i.e. automate this logic as an object logic in Isabelle.

As I understand - the main jEdit window is for editing thy - theory files. So - I should seek some console (additional window) in which I can run lemmas, lemma proof commands against this theory?

Maybe this question is better posed at the "Mathematics" or the "Computer Science" Stacks? (I didn't even know Category Theory could be used as framework for a Logic). — David Tonhofer
This is technical question and not appropriate for research-level forums of Math and CS. Besides, Stackoverflow has Tag Isabelle and here indeed is some activity around it. — TomR
@DavidTonhofer This question is appropriate for SO. There's no mention of CT even in this post. — larsrh

larsrh larsrh · Accepted Answer · 2017-06-16T08:55:23

I can enter theory in jEdit dialog but I am not receiving any feedback.

This sounds like you may not have a working Isabelle installation. In a working installation, any file with the extension .thy gets checked in Isabelle/jEdit. For example, errors are highlighted in red, you'll see prover output in the "Output" and "State" panels, and you can Ctrl-click on entities to jump to their definition.

So - I should seek some console (additional window) in which I can run lemmas, lemma proof commands against this theory?

You don't have to, but you can. In the system manual, it is described how to run a "batch build" of a set of theories (in Isabelle jargon: "a session"). In the simplest case, that boils down to running isabelle mkroot followed by isabelle build with the appropriate flags. See §3.2 in that manual for a self-contained example.

And after this - I would like to use this theory - e.g. write some lemma and invoke interactive proof session for this.

In the same Isabelle/jEdit window, you can create a new theory file, give it a name, and import your theory as follows:

theory Test
imports MonoidalLogic
begin

I have Isabelle/HOL theory, how can I proceed with its application?

2 Answers