[isabelle] How do I do stone age interaction?



Hello all,

(I am a newcomer to Isabelle, so apologies for asking what is probably
an incredibly trivial question.  I have installed Isabelle 2009 from
source, and have already tried looking at bundled documents such as
'intro.dvi', 'main.dvi', 'system.dvi' and 'tutorial.dvi', but to no
avail.)

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.  Starting Isabelle using 'isabelle tty',
followed by entering 'exit' to drop out of Isar sounds promising, but
what do I do then?  Just some examples of basic proofs (e.g. "Socrates
is mortal") would be so helpful.  I'm not convinced that there is even
the concept of term quotations in Isabelle's basic ML top level.  Am I
right?  And what are the ML constructor functions for types and terms?

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?

Thanks,

Mark Adams





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