doc-src/IsarImplementation/Thy/Isar.thy

more examples;
more on "Proof methods";

theory Isar
imports Base
begin

chapter {* Isar language elements *}

text {* The Isar proof language (see also
  \cite[\S2]{isabelle-isar-ref}) consists of three main categories of
  language elements:

  \begin{enumerate}

  \item Proof \emph{commands} define the primary language of
  transactions of the underlying Isar/VM interpreter.  Typical
  examples are @{command "fix"}, @{command "assume"}, @{command
  "show"}, and @{command "by"}.

  Composing proof commands according to the rules of the Isar/VM
  essentially leads to expressions of structured proof text, such that
  both the machine and the human reader can give it a meaning as
  formal reasoning.

  \item Proof \emph{methods} define a secondary language of mixed
  forward-backward refinement steps involving facts and goals.
  Typical example methods are @{method rule}, @{method unfold}, or
  @{text simp}.  %FIXME proper formal markup!?

  Methods can occur in certain well-defined parts of the Isar proof
  language, say as arguments to @{command "proof"}, @{command "qed"},
  or @{command "by"}.

  \item \emph{Attributes} define a tertiary language of small
  annotations to facts: facts being defined or referenced may always
  be decorated with attribute expressions.  Attributes can modify both
  the fact and the context.

  Typical example attributes are @{attribute intro} (which affects the
  context), or @{attribute symmetric} (which affects the fact).

  \end{enumerate}
*}


section {* Proof commands *}

text {* In principle, Isar proof commands could be defined in
  user-space as well.  The system is built like that in the first
  place: part of the commands are primitive, the other part is defined
  as derived elements.  Adding to the genuine structured proof
  language requires profound understanding of the Isar/VM machinery,
  though, so this is far beyond the scope of this manual.

  What can be done realistically is to define some diagnostic commands
  that merely inspect the general state of the Isar/VM, and report
  some feedback to the user.  Typically this involves checking of the
  linguistic \emph{mode} of a proof state, or peeking at the pending
  goals (if available).
*}

text %mlref {*
  \begin{mldecls}
  @{index_ML_type Proof.state} \\
  @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
  @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
  @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
  @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
  @{index_ML Proof.goal: "Proof.state ->
  {context: Proof.context, facts: thm list, goal: thm}"} \\
  @{index_ML Proof.raw_goal: "Proof.state ->
  {context: Proof.context, facts: thm list, goal: thm}"} \\
  \end{mldecls}

  \begin{description}

  \item @{ML_type Proof.state} represents Isar proof states.  This is
  a block-structured configuration with proof context, linguistic
  mode, and optional goal state.  An Isar goal consists of goal
  context, goal facts (``@{text "using"}''), and tactical goal state
  (see \secref{sec:tactical-goals}).

  The general idea is that the facts shall contribute to the
  refinement of the goal state --- how exactly is defined by the proof
  method that is applied in that situation.

  \item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML
  Proof.assert_backward} are partial identity functions that fail
  unless a certain linguistic mode is active, namely ``@{text
  "proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text
  "proof(prove)"}'', respectively (using the terminology of
  \cite{isabelle-isar-ref}).

  It is advisable study the implementations of existing proof commands
  for suitable modes to be asserted.

  \item @{ML Proof.simple_goal}~@{text "state"} returns the structured
  Isar goal (if available) in the form seen by ``simple'' methods
  (like @{text simp} or @{text blast}).  The Isar goal facts are
  already inserted as premises into the subgoals, which are presented
  separately as in @{ML Proof.goal}.

  \item @{ML Proof.goal}~@{text "state"} returns the structured Isar
  goal (if available) in the form seen by regular methods (like
  @{method rule}).  The auxiliary internal encoding of Pure
  conjunctions is split into individual subgoals as usual.

  \item @{ML Proof.raw_goal}~@{text "state"} returns the structured
  Isar goal (if available) in the raw internal form seen by ``raw''
  methods (like @{text induct}).  This form is very rarely appropriate
  for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal}
  should be used in most situations.

  \end{description}
*}


text %mlantiq {*
  \begin{matharray}{rcl}
  @{ML_antiquotation_def "Isar.goal"} & : & @{text ML_antiquotation} \\
  \end{matharray}

  \begin{description}

  \item @{text "@{Isar.goal}"} refers to the regular goal state (if
  available) of the current proof state managed by the Isar toplevel
  --- as abstract value.

  This only works for diagnostic ML commands, such as @{command
  ML_val} or @{command ML_command}.

  \end{description}
*}

text %mlex {* The following example peeks at a certain goal configuration. *}

example_proof
  have "PROP A" and "PROP B" and "PROP C"
    ML_val {* Thm.nprems_of (#goal @{Isar.goal}) *}
    oops

text {* \noindent Here we see 3 individual subgoals in the same way as
  regular proof methods would do.
*}


section {* Proof methods *}

text {* Proof methods are syntactically embedded into the Isar proof
  language as arguments to certain commands, e.g.\ @{command "by"} or
  @{command apply}.  User-space additions are relatively easy by
  plugging a suitable method-valued parser function into the
  framework.

  Operationally, a proof method is like a structurally enhanced
  tactic: it operates on the full Isar goal configuration with
  context, goal facts, and primitive goal state.  Like a tactic, it
  enumerates possible follow-up goal states, with the potential
  addition of named extensions of the proof context (called
  \emph{cases}).

  To get a better idea about the range of possibilities, consider
  first the following structured proof scheme:

  \medskip
  \begin{tabular}{l}
  @{command from}~@{text "facts\<^sub>1"}~@{command have}~@{text "props"}~@{command using}~@{text "facts\<^sub>2"} \\
  @{command proof}~@{text "(initial_method)"} \\
  \quad@{text "body"} \\
  @{command qed}~@{text "(terminal_method)"} \\
  \end{tabular}
  \medskip

  \noindent The goal configuration consists of @{text "facts\<^sub>1"} and
  @{text "facts\<^sub>2"} appended in that order, and various @{text "props"}
  that are claimed here.  The @{text "initial_method"} is invoked with
  that information and refines the problem to something that is
  accommodated recursively in the proof @{text "body"}.  The @{text
  "terminal_method"} has another chance to finish-off any remaining
  subgoals, but it does not see the facts of the initial step.

  \medskip Here is another pattern for unstructured proof scripts:

  \begin{tabular}{l}
  @{command have}~@{text "props"} \\
  \quad@{command using}~@{text "facts\<^sub>1"} \\
  \quad@{command apply}~@{text "method\<^sub>1"} \\
  \quad@{command apply}~@{text "method\<^sub>2"} \\
  \quad@{command using}~@{text "facts\<^sub>3"} \\
  \quad@{command apply}~@{text "method\<^sub>3"} \\
  \quad@{command done} \\
  \end{tabular}
  \medskip

  \noindent The @{text "method\<^sub>1"} operates on the original claim
  together while using @{text "facts\<^bsub>1\<^esub>"}.  Since the @{command apply}
  command structurally resets the facts, the @{text "method\<^sub>2"} will
  operate on the remaining goal state without facts.  The @{text
  "method\<^sub>3"} will see a collection of @{text "facts\<^sub>3"} that has been
  inserted into the script explicitly.

  \medskip Empirically, Isar proof methods can be categorized as follows:

  \begin{enumerate}

  \item structured method with cases, e.g.\ @{text "induct"}

  \item regular method: strong emphasis on facts, e.g.\ @{text "rule"}

  \item simple method: weak emphasis on facts, merely inserted into subgoals, e.g.\ @{text "simp"}

  \item old-style tactic emulation, e.g. @{text "rule_tac"}

  \begin{itemize}

  \item naming convention @{text "foo_tac"}

  \item numeric goal addressing

  \item explicit references to internal goal state (invisible from text!)

  \end{itemize}

  \end{enumerate}

  FIXME
*}


section {* Attributes *}

text FIXME

end