Search code examples
isabelle

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

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:

  1. write initial theory file;

  2. invoke interactive session where I can find proofs of some lemmas for this theory

  3. 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?

Solution

  • 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