Re: [isabelle] How do I do stone age interaction?



On Sat, 27 Nov 2010, mark at proof-technologies.com wrote:

Is it possible to do basic ML top level interactive forward proofs in Isabelle HOL, in a style similar to basic forward proof in HOL Light, HOL4 and ProofPower? I don't want to use Isar or Proof General, just the basic ML top level.

You can hardly do anything on the raw ML toplevel, since everything is managed by the Isar infrastructure theses days, notably the theory context and the ML toplevel environment.


Starting Isabelle using 'isabelle tty'

Fine.


followed by entering 'exit' to drop out of Isar sounds promising

Bad move. No ML bindings coming after the Pure bootstrap will be available, because the connection to the formal context is lost.


I'm not convinced that there is even the concept of term quotations in Isabelle's basic ML top level. Am I right?

Isabelle/ML antiquotations are quite advanced, but you need to do things in the proper order: quote ML inside Isar, antiquote logical entities inside ML. See also chapter 0 of http://www4.in.tum.de/~wenzelm/test/implementation.pdf which will be part of the next official release.


So here is my basic HOL4 forward proof:

   (* First some declarations and definitions *)
   new_type ("Person",0);
   new_constant ("Socrates", ``:Person``);
   new_constant ("Man", ``:Person->bool``);
   new_constant ("Mortal", ``:Person->bool``);
   val ax1 = new_axiom ("Socrates Axiom 1", ``Man Socrates``);
   val ax2 = new_axiom ("Socrates Axiom 2", ``! p. Man p ==> Mortal
p``);

   (* Now the proof itself *)
   MP (SPEC ``Socrates`` ax2) ax1;

This gives me:

   val it = |- Mortal Socrates : thm

Can anyone translate this into Isabelle HOL top level commands for me?

Here is my version for Isabelle2009-2:


theory A imports Main begin;

example_proof;
  fix socrates :: 'person;
  fix man :: "'person => bool";
  fix mortal :: "'person => bool";

  assume ax1: "man socrates";
  assume ax2: "!!p. man p ==> mortal p";

  ML_val {*
    val th = @{thm ax2} OF [ at {thm ax1}];
    writeln (Display.string_of_thm @{context} th);
  *};

end;


The old-fashioned semicolons are there for your convenience in the tty. Myself I composed this quickly with Isabelle/jEdit and than pasted it into the terminal.

The th result above is pretty-printed without a proper context, unlike the full version with writeln and Display.string_of_thm.

In order to be productive with Isabelle/ML you should build up your context in Isar source notation and the experiment with it via small ML snippets. What is your application anyway? Serious use of Isabelle outside the Isar system infrastructure is hard to imagine.


	Makarius





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