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



You might consider downloading an older version from here: http://www.cl.cam.ac.uk/~lp15/archive/

Until around 2005, ML level interaction was still supported.

Larry Paulson


On 27 Nov 2010, at 07:54, <mark at proof-technologies.com> wrote:

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