doc-src/IsarImplementation/Thy/Isar.thy
author wenzelm
Tue Oct 12 20:03:31 2010 +0100 (2010-10-12)
changeset 39842 7205191afde4
parent 30272 2d612824e642
child 39843 21d189bfdfd1
permissions -rw-r--r--
more on "Isar language elements";
wenzelm@29755
     1
theory Isar
wenzelm@29755
     2
imports Base
wenzelm@29755
     3
begin
wenzelm@20472
     4
wenzelm@29759
     5
chapter {* Isar language elements *}
wenzelm@29759
     6
wenzelm@39842
     7
text {* The Isar proof language (see also
wenzelm@39842
     8
  \cite[\S2]{isabelle-isar-ref}) consists of three main categories of
wenzelm@29759
     9
  language elements:
wenzelm@29759
    10
wenzelm@29759
    11
  \begin{enumerate}
wenzelm@29759
    12
wenzelm@39842
    13
  \item Proof \emph{commands} define the primary language of
wenzelm@39842
    14
  transactions of the underlying Isar/VM interpreter.  Typical
wenzelm@39842
    15
  examples are @{command "fix"}, @{command "assume"}, @{command
wenzelm@39842
    16
  "show"}, and @{command "by"}.
wenzelm@39842
    17
wenzelm@39842
    18
  Composing proof commands according to the rules of the Isar/VM
wenzelm@39842
    19
  essentially leads to expressions of structured proof text, such that
wenzelm@39842
    20
  both the machine and the human reader can give it a meaning as
wenzelm@39842
    21
  formal reasoning.
wenzelm@20472
    22
wenzelm@39842
    23
  \item Proof \emph{methods} define a secondary language of mixed
wenzelm@39842
    24
  forward-backward refinement steps involving facts and goals.
wenzelm@39842
    25
  Typical example methods are @{method rule}, @{method unfold}, or
wenzelm@39842
    26
  @{text simp}.  %FIXME proper formal markup!?
wenzelm@29759
    27
wenzelm@39842
    28
  Methods can occur in certain well-defined parts of the Isar proof
wenzelm@39842
    29
  language, say as arguments to @{command "proof"}, @{command "qed"},
wenzelm@39842
    30
  or @{command "by"}.
wenzelm@39842
    31
wenzelm@39842
    32
  \item \emph{Attributes} define a tertiary language of small
wenzelm@39842
    33
  annotations to facts: facts being defined or referenced may always
wenzelm@39842
    34
  be decorated with attribute expressions.  Attributes can modify both
wenzelm@39842
    35
  the fact and the context.
wenzelm@39842
    36
wenzelm@39842
    37
  Typical example attributes are @{attribute intro} (which affects the
wenzelm@39842
    38
  context), or @{attribute symmetric} (which affects the fact).
wenzelm@29759
    39
wenzelm@29759
    40
  \end{enumerate}
wenzelm@29759
    41
*}
wenzelm@29759
    42
wenzelm@29759
    43
wenzelm@29759
    44
section {* Proof commands *}
wenzelm@20520
    45
wenzelm@39842
    46
text {* In principle, Isar proof commands could be defined in
wenzelm@39842
    47
  user-space as well.  The system is built like that in the first
wenzelm@39842
    48
  place: part of the commands are primitive, the other part is defined
wenzelm@39842
    49
  as derived elements.  Adding to the genuine structured proof
wenzelm@39842
    50
  language requires profound understanding of the Isar/VM machinery,
wenzelm@39842
    51
  though, so this is far beyond the scope of this manual.
wenzelm@39842
    52
wenzelm@39842
    53
  What can be done realistically is to define some diagnostic commands
wenzelm@39842
    54
  that merely inspect the general state of the Isar/VM, and report
wenzelm@39842
    55
  some feedback to the user.  Typically this involves checking of the
wenzelm@39842
    56
  linguistic \emph{mode} of a proof state, or peeking at the pending
wenzelm@39842
    57
  goals (if available).
wenzelm@39842
    58
*}
wenzelm@39842
    59
wenzelm@39842
    60
text %mlref {*
wenzelm@39842
    61
  \begin{mldecls}
wenzelm@39842
    62
  @{index_ML_type Proof.state} \\
wenzelm@39842
    63
  @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
wenzelm@39842
    64
  @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
wenzelm@39842
    65
  @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
wenzelm@39842
    66
  @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
wenzelm@39842
    67
  @{index_ML Proof.goal: "Proof.state ->
wenzelm@39842
    68
  {context: Proof.context, facts: thm list, goal: thm}"} \\
wenzelm@39842
    69
  @{index_ML Proof.raw_goal: "Proof.state ->
wenzelm@39842
    70
  {context: Proof.context, facts: thm list, goal: thm}"} \\
wenzelm@39842
    71
  \end{mldecls}
wenzelm@39842
    72
wenzelm@39842
    73
  \begin{description}
wenzelm@39842
    74
wenzelm@39842
    75
  \item @{ML_type Proof.state} represents Isar proof states.  This is
wenzelm@39842
    76
  a block-structured configuration with proof context, linguistic
wenzelm@39842
    77
  mode, and optional goal state.  An Isar goal consists of goal
wenzelm@39842
    78
  context, goal facts (``@{text "using"}''), and tactical goal state
wenzelm@39842
    79
  (see \secref{sec:tactical-goals}).
wenzelm@39842
    80
wenzelm@39842
    81
  The general idea is that the facts shall contribute to the
wenzelm@39842
    82
  refinement of the goal state --- how exactly is defined by the proof
wenzelm@39842
    83
  method that is applied in that situation.
wenzelm@39842
    84
wenzelm@39842
    85
  \item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML
wenzelm@39842
    86
  Proof.assert_backward} are partial identity functions that fail
wenzelm@39842
    87
  unless a certain linguistic mode is active, namely ``@{text
wenzelm@39842
    88
  "proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text
wenzelm@39842
    89
  "proof(prove)"}'', respectively (using the terminology of
wenzelm@39842
    90
  \cite{isabelle-isar-ref}).
wenzelm@39842
    91
wenzelm@39842
    92
  It is advisable study the implementations of existing proof commands
wenzelm@39842
    93
  for suitable modes to be asserted.
wenzelm@39842
    94
wenzelm@39842
    95
  \item @{ML Proof.simple_goal}~@{text "state"} returns the structured
wenzelm@39842
    96
  Isar goal (if available) in the form seen by ``simple'' methods
wenzelm@39842
    97
  (like @{text simp} or @{text blast}).  The Isar goal facts are
wenzelm@39842
    98
  already inserted as premises into the subgoals, which are presented
wenzelm@39842
    99
  separately as in @{ML Proof.goal}.
wenzelm@39842
   100
wenzelm@39842
   101
  \item @{ML Proof.goal}~@{text "state"} returns the structured Isar
wenzelm@39842
   102
  goal (if available) in the form seen by regular methods (like
wenzelm@39842
   103
  @{method rule}).  The auxiliary internal encoding of Pure
wenzelm@39842
   104
  conjunctions is split into individual subgoals as usual.
wenzelm@39842
   105
wenzelm@39842
   106
  \item @{ML Proof.raw_goal}~@{text "state"} returns the structured
wenzelm@39842
   107
  Isar goal (if available) in the raw internal form seen by ``raw''
wenzelm@39842
   108
  methods (like @{text induct}).  This form is very rarely appropriate
wenzelm@39842
   109
  for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal}
wenzelm@39842
   110
  should be used in most situations.
wenzelm@39842
   111
wenzelm@39842
   112
  \end{description}
wenzelm@39842
   113
*}
wenzelm@39842
   114
wenzelm@20520
   115
wenzelm@20520
   116
wenzelm@20472
   117
section {* Proof methods *}
wenzelm@20472
   118
wenzelm@20472
   119
text FIXME
wenzelm@20472
   120
wenzelm@29759
   121
wenzelm@20472
   122
section {* Attributes *}
wenzelm@20472
   123
wenzelm@29759
   124
text FIXME
wenzelm@30272
   125
wenzelm@20472
   126
end