Re: [isabelle] Syntax issue: lost between HOL and Isar



On Thu, 2 Aug 2012, Gottfried Barrow wrote:

I'll check out on this thread, and store away any other comments that come in for future reference.

You have already managed quite well on this thread to ask the right questions, and get into the right direction to understand things more deeply.

Just a few more side-remarks on these earlier messages below.


On Wed, 1 Aug 2012, Gottfried Barrow wrote:

As far as I'm concerned, everything between "theory" and "end" is the
Isar programming language. There is the ML in the "ML{ ... }", but other
than that, it's all Isar to me now.

On Thu, 2 Aug 2012, Gottfried Barrow wrote:

I was wanting to start using the phrase "the Pure programming language",
but "Outer_syntax.command" is an Isar command, so the HOL outer syntax
"datatype" is defined as HOL syntax using an Isar command.

On Thu, 2 Aug 2012, Gottfried Barrow wrote:

I understand that between "theory MyTheory" and "end" in "MyTheory.thy"
there are things like Latex and ML. But I can consider any of that as
part of an argument to an Isar command like "ML{ .... }" or "text{ ...
}".  I'm trying to figure out if there's anything between "theory" and
"end" that someone would have to say, "Most of what's between 'theory'
and 'end' is Isar, but there are exceptions."

On Thu, 2 Aug 2012, Gottfried Barrow wrote:

This brings up "Outer_syntax.command", which I mentioned in the email I
sent out before this one.

I'm going to call "Outer_syntax.command" an Isar command, and it's used
in Datatype.thy to define "datatype" as outer syntax. If I don't call it
an Isar command, then what am I going to call it? If I call it an ML
command or a Pure command, then I can't say that Isar is the programming
language that's being used to define "datatype". If that's the case,
then there's a lower level programming language that I'm using. If there
is, I want to know what to call it.


* The content of a theory file between 'theory' and the final 'end' is by
  definition the Isar source language.

* Isar is a general framework to define "domain-specific formal
  languages".  It allows to nest various sub-languages easily, most
  notably the Isar proof language.  Other more exotic language embeddings
  are here:

notepad
begin
  (* Isar proof language here *)
  fix a b :: nat
  fix n :: nat
  assume a: "⋀m. n + m > 0"
    ML_val {*
      (* ML inside Isar proof context here *)

      (* antiquotation of logical entities here:*)
      fun foo th = th RS @{thm a}

      (* further nesting: term language inside fact language: *)
      fun bar th = th RS @{thm a [of "a + b"]}
    *}
end

end

  * Note that above the Prover IDE markup will tell you about the formal
    entities occurring in the nested sublanguages.  E.g. CTRL-hover over
    "a + b" parts will do the same as if they would occur directly as
    terms within the main Isar source language (statements, proofs).

  * ML has a special role in the game: it is the platform for first
    bootstrapping the Isar language framework, and later gets re-embedded
    into the Isar source language, with the above antiquotation
    mechanisms to get some parts of Isar back into ML.  E.g. like this:

    ML {*
      val my_thm = @{lemma "⋀x. x = x" by (rule refl)}
    *}

  * Formal latex is another special sub-language.  For example, it allows
    to embed ML with embedded formal entities like this:

     text {*
       blah blah; this is mainly {\LaTeX}, but with some antiquotations
       @{ML "
         (* this is again ML inside the Isar context *)
         let val my_thm = @{lemma \"⋀x. x = x\" by (rule refl)}
         in Thm.prop_of my_thm end"}
     *}

    Here the incremental parser of Isabelle/jEdit sometimes gets problems
    with the nested quotes, but in the end you should get proper formal
    markup of everything to hover over, and understand this formal
    gibberish.

  * Outer_syntax.command that was left somewhat myterious above is not
    very special.  It is just an Isabelle/ML function that defines new
    Isar commands.  Similar to the ML function Method.setup to define
    proof methods, but the latter also has an Isar source language
    counterpart called method_setup; both Method.setup and
    method_setup take an ML expression for the method implementation as
    argument: ML that is embedded into Isar in the usual way.

    It is just a historical accident, that Outer_syntax.command is still
    not fully-integrated into the self-defining self-embedding game of
    formal languages.  (Just today I've made further stepts towards that,
    and found out that only 'theory' needs to be given from outside; all
    other Isar commands can be defined inside the Isar framework.)


On now to make sophisticated specifications and serious proofs in Isabelle/HOL ...


	Makarius


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