doc-src/IsarImplementation/Thy/Isar.thy
author wenzelm
Wed Oct 13 10:52:15 2010 +0100 (2010-10-13)
changeset 39844 57c7498f11a8
parent 39843 21d189bfdfd1
child 39845 50f42116ebdb
permissions -rw-r--r--
tuned;
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@39844
     7
text {*
wenzelm@39844
     8
  %FIXME proper formal markup of methods!?
wenzelm@39844
     9
wenzelm@39844
    10
  The Isar proof language (see also \cite[\S2]{isabelle-isar-ref})
wenzelm@39844
    11
  consists of three main categories of language elements:
wenzelm@29759
    12
wenzelm@29759
    13
  \begin{enumerate}
wenzelm@29759
    14
wenzelm@39842
    15
  \item Proof \emph{commands} define the primary language of
wenzelm@39842
    16
  transactions of the underlying Isar/VM interpreter.  Typical
wenzelm@39842
    17
  examples are @{command "fix"}, @{command "assume"}, @{command
wenzelm@39844
    18
  "show"}, @{command "proof"}, and @{command "qed"}.
wenzelm@39842
    19
wenzelm@39844
    20
  Composing proof commands according to the rules of the Isar/VM leads
wenzelm@39844
    21
  to expressions of structured proof text, such that both the machine
wenzelm@39844
    22
  and the human reader can give it a meaning as formal reasoning.
wenzelm@20472
    23
wenzelm@39842
    24
  \item Proof \emph{methods} define a secondary language of mixed
wenzelm@39842
    25
  forward-backward refinement steps involving facts and goals.
wenzelm@39844
    26
  Typical examples are @{method rule}, @{method unfold}, and @{text
wenzelm@39844
    27
  simp}.
wenzelm@29759
    28
wenzelm@39842
    29
  Methods can occur in certain well-defined parts of the Isar proof
wenzelm@39842
    30
  language, say as arguments to @{command "proof"}, @{command "qed"},
wenzelm@39842
    31
  or @{command "by"}.
wenzelm@39842
    32
wenzelm@39842
    33
  \item \emph{Attributes} define a tertiary language of small
wenzelm@39844
    34
  annotations to facts being defined or referenced.  Attributes can
wenzelm@39844
    35
  modify both the fact and the context.
wenzelm@39842
    36
wenzelm@39844
    37
  Typical examples are @{attribute symmetric} (which affects the
wenzelm@39844
    38
  fact), and @{attribute intro} (which affects the context).
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@39844
    51
  though, so this is beyond the scope of this manual.
wenzelm@39842
    52
wenzelm@39842
    53
  What can be done realistically is to define some diagnostic commands
wenzelm@39844
    54
  that inspect the general state of the Isar/VM, and report some
wenzelm@39844
    55
  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@39844
    77
  mode, and optional goal.  The latter consists of goal context, goal
wenzelm@39844
    78
  facts (``@{text "using"}''), and tactical goal state (see
wenzelm@39844
    79
  \secref{sec:tactical-goals}).
wenzelm@39842
    80
wenzelm@39842
    81
  The general idea is that the facts shall contribute to the
wenzelm@39844
    82
  refinement of some parts of the tactical goal --- how exactly is
wenzelm@39844
    83
  defined by the proof 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@39844
    99
  individually 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@39844
   108
  methods (like @{text induct}).  This form is rarely appropriate for
wenzelm@39844
   109
  dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} should
wenzelm@39844
   110
  be used in most situations.
wenzelm@39842
   111
wenzelm@39842
   112
  \end{description}
wenzelm@39842
   113
*}
wenzelm@39842
   114
wenzelm@20520
   115
wenzelm@39843
   116
text %mlantiq {*
wenzelm@39843
   117
  \begin{matharray}{rcl}
wenzelm@39843
   118
  @{ML_antiquotation_def "Isar.goal"} & : & @{text ML_antiquotation} \\
wenzelm@39843
   119
  \end{matharray}
wenzelm@39843
   120
wenzelm@39843
   121
  \begin{description}
wenzelm@39843
   122
wenzelm@39843
   123
  \item @{text "@{Isar.goal}"} refers to the regular goal state (if
wenzelm@39843
   124
  available) of the current proof state managed by the Isar toplevel
wenzelm@39843
   125
  --- as abstract value.
wenzelm@39843
   126
wenzelm@39843
   127
  This only works for diagnostic ML commands, such as @{command
wenzelm@39843
   128
  ML_val} or @{command ML_command}.
wenzelm@39843
   129
wenzelm@39843
   130
  \end{description}
wenzelm@39843
   131
*}
wenzelm@39843
   132
wenzelm@39843
   133
text %mlex {* The following example peeks at a certain goal configuration. *}
wenzelm@39843
   134
wenzelm@39843
   135
example_proof
wenzelm@39843
   136
  have "PROP A" and "PROP B" and "PROP C"
wenzelm@39843
   137
    ML_val {* Thm.nprems_of (#goal @{Isar.goal}) *}
wenzelm@39843
   138
    oops
wenzelm@39843
   139
wenzelm@39843
   140
text {* \noindent Here we see 3 individual subgoals in the same way as
wenzelm@39843
   141
  regular proof methods would do.
wenzelm@39843
   142
*}
wenzelm@39843
   143
wenzelm@20520
   144
wenzelm@20472
   145
section {* Proof methods *}
wenzelm@20472
   146
wenzelm@39843
   147
text {* Proof methods are syntactically embedded into the Isar proof
wenzelm@39843
   148
  language as arguments to certain commands, e.g.\ @{command "by"} or
wenzelm@39844
   149
  @{command apply}.  User-space additions are reasonably easy by
wenzelm@39844
   150
  plugging suitable method-valued parser functions into the framework.
wenzelm@39843
   151
wenzelm@39843
   152
  Operationally, a proof method is like a structurally enhanced
wenzelm@39843
   153
  tactic: it operates on the full Isar goal configuration with
wenzelm@39844
   154
  context, goal facts, and tactical goal state.  Like a tactic, it
wenzelm@39843
   155
  enumerates possible follow-up goal states, with the potential
wenzelm@39844
   156
  addition of named extensions of the proof context (\emph{cases}).
wenzelm@39843
   157
wenzelm@39844
   158
  To get a better idea about the range of possibilities, consider the
wenzelm@39844
   159
  following Isar proof schemes.  First some general form of structured
wenzelm@39844
   160
  proof text:
wenzelm@39843
   161
wenzelm@39843
   162
  \medskip
wenzelm@39843
   163
  \begin{tabular}{l}
wenzelm@39843
   164
  @{command from}~@{text "facts\<^sub>1"}~@{command have}~@{text "props"}~@{command using}~@{text "facts\<^sub>2"} \\
wenzelm@39843
   165
  @{command proof}~@{text "(initial_method)"} \\
wenzelm@39843
   166
  \quad@{text "body"} \\
wenzelm@39843
   167
  @{command qed}~@{text "(terminal_method)"} \\
wenzelm@39843
   168
  \end{tabular}
wenzelm@39843
   169
  \medskip
wenzelm@39843
   170
wenzelm@39843
   171
  \noindent The goal configuration consists of @{text "facts\<^sub>1"} and
wenzelm@39843
   172
  @{text "facts\<^sub>2"} appended in that order, and various @{text "props"}
wenzelm@39844
   173
  being claimed here.  The @{text "initial_method"} is invoked with
wenzelm@39844
   174
  facts and goals together and refines the problem to something that
wenzelm@39844
   175
  is handled recursively in the proof @{text "body"}.  The @{text
wenzelm@39843
   176
  "terminal_method"} has another chance to finish-off any remaining
wenzelm@39843
   177
  subgoals, but it does not see the facts of the initial step.
wenzelm@39843
   178
wenzelm@39844
   179
  \medskip The second pattern illustrates unstructured proof scripts:
wenzelm@39843
   180
wenzelm@39844
   181
  \medskip
wenzelm@39843
   182
  \begin{tabular}{l}
wenzelm@39843
   183
  @{command have}~@{text "props"} \\
wenzelm@39844
   184
  \quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\
wenzelm@39843
   185
  \quad@{command apply}~@{text "method\<^sub>2"} \\
wenzelm@39844
   186
  \quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\
wenzelm@39843
   187
  \quad@{command done} \\
wenzelm@39843
   188
  \end{tabular}
wenzelm@39843
   189
  \medskip
wenzelm@39843
   190
wenzelm@39843
   191
  \noindent The @{text "method\<^sub>1"} operates on the original claim
wenzelm@39843
   192
  together while using @{text "facts\<^bsub>1\<^esub>"}.  Since the @{command apply}
wenzelm@39843
   193
  command structurally resets the facts, the @{text "method\<^sub>2"} will
wenzelm@39843
   194
  operate on the remaining goal state without facts.  The @{text
wenzelm@39844
   195
  "method\<^sub>3"} will see again a collection of @{text "facts\<^sub>3"} that has
wenzelm@39844
   196
  been inserted into the script explicitly.
wenzelm@39843
   197
wenzelm@39843
   198
  \medskip Empirically, Isar proof methods can be categorized as follows:
wenzelm@39843
   199
wenzelm@39843
   200
  \begin{enumerate}
wenzelm@39843
   201
wenzelm@39843
   202
  \item structured method with cases, e.g.\ @{text "induct"}
wenzelm@39843
   203
wenzelm@39843
   204
  \item regular method: strong emphasis on facts, e.g.\ @{text "rule"}
wenzelm@39843
   205
wenzelm@39843
   206
  \item simple method: weak emphasis on facts, merely inserted into subgoals, e.g.\ @{text "simp"}
wenzelm@39843
   207
wenzelm@39843
   208
  \item old-style tactic emulation, e.g. @{text "rule_tac"}
wenzelm@39843
   209
wenzelm@39843
   210
  \begin{itemize}
wenzelm@39843
   211
wenzelm@39843
   212
  \item naming convention @{text "foo_tac"}
wenzelm@39843
   213
wenzelm@39843
   214
  \item numeric goal addressing
wenzelm@39843
   215
wenzelm@39843
   216
  \item explicit references to internal goal state (invisible from text!)
wenzelm@39843
   217
wenzelm@39843
   218
  \end{itemize}
wenzelm@39843
   219
wenzelm@39843
   220
  \end{enumerate}
wenzelm@39843
   221
wenzelm@39843
   222
  FIXME
wenzelm@39843
   223
*}
wenzelm@20472
   224
wenzelm@29759
   225
wenzelm@20472
   226
section {* Attributes *}
wenzelm@20472
   227
wenzelm@29759
   228
text FIXME
wenzelm@30272
   229
wenzelm@20472
   230
end