doc-src/IsarImplementation/Thy/Isar.thy
author wenzelm
Sun Oct 17 20:25:36 2010 +0100 (2010-10-17)
changeset 39861 b8d89db3e238
parent 39851 7219a771ab63
child 39864 f3b4fde34cd1
permissions -rw-r--r--
use continental paragraph style, which works better with mixture of (in)formal text;
tuned skips and indents;
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
  The Isar proof language (see also \cite[\S2]{isabelle-isar-ref})
wenzelm@39844
     9
  consists of three main categories of 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@39844
    16
  "show"}, @{command "proof"}, and @{command "qed"}.
wenzelm@39842
    17
wenzelm@39844
    18
  Composing proof commands according to the rules of the Isar/VM leads
wenzelm@39844
    19
  to expressions of structured proof text, such that both the machine
wenzelm@39844
    20
  and the human reader can give it a meaning as formal reasoning.
wenzelm@20472
    21
wenzelm@39842
    22
  \item Proof \emph{methods} define a secondary language of mixed
wenzelm@39842
    23
  forward-backward refinement steps involving facts and goals.
wenzelm@39846
    24
  Typical examples are @{method rule}, @{method unfold}, and @{method
wenzelm@39844
    25
  simp}.
wenzelm@29759
    26
wenzelm@39842
    27
  Methods can occur in certain well-defined parts of the Isar proof
wenzelm@39842
    28
  language, say as arguments to @{command "proof"}, @{command "qed"},
wenzelm@39842
    29
  or @{command "by"}.
wenzelm@39842
    30
wenzelm@39842
    31
  \item \emph{Attributes} define a tertiary language of small
wenzelm@39849
    32
  annotations to theorems being defined or referenced.  Attributes can
wenzelm@39849
    33
  modify both the context and the theorem.
wenzelm@39842
    34
wenzelm@39849
    35
  Typical examples are @{attribute intro} (which affects the context),
wenzelm@39849
    36
  and @{attribute symmetric} (which affects the theorem).
wenzelm@29759
    37
wenzelm@29759
    38
  \end{enumerate}
wenzelm@29759
    39
*}
wenzelm@29759
    40
wenzelm@29759
    41
wenzelm@29759
    42
section {* Proof commands *}
wenzelm@20520
    43
wenzelm@39849
    44
text {* A \emph{proof command} is state transition of the Isar/VM
wenzelm@39849
    45
  proof interpreter.
wenzelm@39849
    46
wenzelm@39849
    47
  In principle, Isar proof commands could be defined in
wenzelm@39842
    48
  user-space as well.  The system is built like that in the first
wenzelm@39842
    49
  place: part of the commands are primitive, the other part is defined
wenzelm@39842
    50
  as derived elements.  Adding to the genuine structured proof
wenzelm@39842
    51
  language requires profound understanding of the Isar/VM machinery,
wenzelm@39844
    52
  though, so this is beyond the scope of this manual.
wenzelm@39842
    53
wenzelm@39842
    54
  What can be done realistically is to define some diagnostic commands
wenzelm@39844
    55
  that inspect the general state of the Isar/VM, and report some
wenzelm@39844
    56
  feedback to the user.  Typically this involves checking of the
wenzelm@39842
    57
  linguistic \emph{mode} of a proof state, or peeking at the pending
wenzelm@39842
    58
  goals (if available).
wenzelm@39845
    59
wenzelm@39845
    60
  Another common application is to define a toplevel command that
wenzelm@39845
    61
  poses a problem to the user as Isar proof state and stores the final
wenzelm@39845
    62
  result in a suitable context data slot.  Thus a proof can be
wenzelm@39845
    63
  incorporated into the context of some user-space tool, without
wenzelm@39845
    64
  modifying the Isar proof language itself.
wenzelm@39842
    65
*}
wenzelm@39842
    66
wenzelm@39842
    67
text %mlref {*
wenzelm@39842
    68
  \begin{mldecls}
wenzelm@39842
    69
  @{index_ML_type Proof.state} \\
wenzelm@39842
    70
  @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\
wenzelm@39842
    71
  @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\
wenzelm@39842
    72
  @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\
wenzelm@39842
    73
  @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\
wenzelm@39842
    74
  @{index_ML Proof.goal: "Proof.state ->
wenzelm@39842
    75
  {context: Proof.context, facts: thm list, goal: thm}"} \\
wenzelm@39842
    76
  @{index_ML Proof.raw_goal: "Proof.state ->
wenzelm@39842
    77
  {context: Proof.context, facts: thm list, goal: thm}"} \\
wenzelm@39845
    78
  @{index_ML Proof.theorem: "Method.text option ->
wenzelm@39845
    79
  (thm list list -> Proof.context -> Proof.context) ->
wenzelm@39845
    80
  (term * term list) list list -> Proof.context -> Proof.state"} \\
wenzelm@39842
    81
  \end{mldecls}
wenzelm@39842
    82
wenzelm@39842
    83
  \begin{description}
wenzelm@39842
    84
wenzelm@39842
    85
  \item @{ML_type Proof.state} represents Isar proof states.  This is
wenzelm@39842
    86
  a block-structured configuration with proof context, linguistic
wenzelm@39844
    87
  mode, and optional goal.  The latter consists of goal context, goal
wenzelm@39844
    88
  facts (``@{text "using"}''), and tactical goal state (see
wenzelm@39844
    89
  \secref{sec:tactical-goals}).
wenzelm@39842
    90
wenzelm@39842
    91
  The general idea is that the facts shall contribute to the
wenzelm@39844
    92
  refinement of some parts of the tactical goal --- how exactly is
wenzelm@39844
    93
  defined by the proof method that is applied in that situation.
wenzelm@39842
    94
wenzelm@39842
    95
  \item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML
wenzelm@39842
    96
  Proof.assert_backward} are partial identity functions that fail
wenzelm@39842
    97
  unless a certain linguistic mode is active, namely ``@{text
wenzelm@39842
    98
  "proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text
wenzelm@39842
    99
  "proof(prove)"}'', respectively (using the terminology of
wenzelm@39842
   100
  \cite{isabelle-isar-ref}).
wenzelm@39842
   101
wenzelm@39842
   102
  It is advisable study the implementations of existing proof commands
wenzelm@39842
   103
  for suitable modes to be asserted.
wenzelm@39842
   104
wenzelm@39842
   105
  \item @{ML Proof.simple_goal}~@{text "state"} returns the structured
wenzelm@39842
   106
  Isar goal (if available) in the form seen by ``simple'' methods
wenzelm@39846
   107
  (like @{method simp} or @{method blast}).  The Isar goal facts are
wenzelm@39842
   108
  already inserted as premises into the subgoals, which are presented
wenzelm@39844
   109
  individually as in @{ML Proof.goal}.
wenzelm@39842
   110
wenzelm@39842
   111
  \item @{ML Proof.goal}~@{text "state"} returns the structured Isar
wenzelm@39842
   112
  goal (if available) in the form seen by regular methods (like
wenzelm@39842
   113
  @{method rule}).  The auxiliary internal encoding of Pure
wenzelm@39842
   114
  conjunctions is split into individual subgoals as usual.
wenzelm@39842
   115
wenzelm@39842
   116
  \item @{ML Proof.raw_goal}~@{text "state"} returns the structured
wenzelm@39842
   117
  Isar goal (if available) in the raw internal form seen by ``raw''
wenzelm@39846
   118
  methods (like @{method induct}).  This form is rarely appropriate
wenzelm@39846
   119
  for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal}
wenzelm@39846
   120
  should be used in most situations.
wenzelm@39842
   121
wenzelm@39845
   122
  \item @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"}
wenzelm@39845
   123
  initializes a toplevel Isar proof state within a given context.
wenzelm@39845
   124
wenzelm@39845
   125
  The optional @{text "before_qed"} method is applied at the end of
wenzelm@39845
   126
  the proof, just before extracting the result (this feature is rarely
wenzelm@39845
   127
  used).
wenzelm@39845
   128
wenzelm@39845
   129
  The @{text "after_qed"} continuation receives the extracted result
wenzelm@39845
   130
  in order to apply it to the final context in a suitable way (e.g.\
wenzelm@39845
   131
  storing named facts).  Note that at this generic level the target
wenzelm@39845
   132
  context is specified as @{ML_type Proof.context}, but the usual
wenzelm@39845
   133
  wrapping of toplevel proofs into command transactions will provide a
wenzelm@39845
   134
  @{ML_type local_theory} here (see also \chref{ch:local-theory}).
wenzelm@39845
   135
  This usually affects the way how results are stored.
wenzelm@39845
   136
wenzelm@39845
   137
  The @{text "statement"} is given as a nested list of terms, each
wenzelm@39845
   138
  associated with optional @{keyword "is"} patterns as usual in the
wenzelm@39845
   139
  Isar source language.  The original list structure over terms is
wenzelm@39845
   140
  turned into one over theorems when @{text "after_qed"} is invoked.
wenzelm@39845
   141
wenzelm@39842
   142
  \end{description}
wenzelm@39842
   143
*}
wenzelm@39842
   144
wenzelm@20520
   145
wenzelm@39843
   146
text %mlantiq {*
wenzelm@39843
   147
  \begin{matharray}{rcl}
wenzelm@39843
   148
  @{ML_antiquotation_def "Isar.goal"} & : & @{text ML_antiquotation} \\
wenzelm@39843
   149
  \end{matharray}
wenzelm@39843
   150
wenzelm@39843
   151
  \begin{description}
wenzelm@39843
   152
wenzelm@39843
   153
  \item @{text "@{Isar.goal}"} refers to the regular goal state (if
wenzelm@39843
   154
  available) of the current proof state managed by the Isar toplevel
wenzelm@39843
   155
  --- as abstract value.
wenzelm@39843
   156
wenzelm@39843
   157
  This only works for diagnostic ML commands, such as @{command
wenzelm@39843
   158
  ML_val} or @{command ML_command}.
wenzelm@39843
   159
wenzelm@39843
   160
  \end{description}
wenzelm@39843
   161
*}
wenzelm@39843
   162
wenzelm@39843
   163
text %mlex {* The following example peeks at a certain goal configuration. *}
wenzelm@39843
   164
wenzelm@39843
   165
example_proof
wenzelm@39846
   166
  have A and B and C
wenzelm@39843
   167
    ML_val {* Thm.nprems_of (#goal @{Isar.goal}) *}
wenzelm@39843
   168
    oops
wenzelm@39843
   169
wenzelm@39861
   170
text {* Here we see 3 individual subgoals in the same way as regular
wenzelm@39861
   171
  proof methods would do.  *}
wenzelm@39843
   172
wenzelm@20520
   173
wenzelm@20472
   174
section {* Proof methods *}
wenzelm@20472
   175
wenzelm@39847
   176
text {* A @{text "method"} is a function @{text "context \<rightarrow> thm\<^sup>* \<rightarrow> goal
wenzelm@39847
   177
  \<rightarrow> (cases \<times> goal)\<^sup>*\<^sup>*"} that operates on the full Isar goal
wenzelm@39847
   178
  configuration with context, goal facts, and tactical goal state and
wenzelm@39843
   179
  enumerates possible follow-up goal states, with the potential
wenzelm@39844
   180
  addition of named extensions of the proof context (\emph{cases}).
wenzelm@39847
   181
  The latter feature is rarely used.
wenzelm@39847
   182
wenzelm@39847
   183
  This means a proof method is like a structurally enhanced tactic
wenzelm@39847
   184
  (cf.\ \secref{sec:tactics}).  The well-formedness conditions for
wenzelm@39847
   185
  tactics need to hold for methods accordingly, with the following
wenzelm@39847
   186
  additions.
wenzelm@39847
   187
wenzelm@39847
   188
  \begin{itemize}
wenzelm@39847
   189
wenzelm@39847
   190
  \item Goal addressing is further limited either to operate either
wenzelm@39847
   191
  uniformly on \emph{all} subgoals, or specifically on the
wenzelm@39847
   192
  \emph{first} subgoal.
wenzelm@39847
   193
wenzelm@39847
   194
  Exception: old-style tactic emulations that are embedded into the
wenzelm@39847
   195
  method space, e.g.\ @{method rule_tac}.
wenzelm@39847
   196
wenzelm@39847
   197
  \item A non-trivial method always needs to make progress: an
wenzelm@39847
   198
  identical follow-up goal state has to be avoided.\footnote{This
wenzelm@39847
   199
  enables the user to write method expressions like @{text "meth\<^sup>+"}
wenzelm@39847
   200
  without looping, while the trivial do-nothing case can be recovered
wenzelm@39847
   201
  via @{text "meth\<^sup>?"}.}
wenzelm@39847
   202
wenzelm@39847
   203
  Exception: trivial stuttering steps, such as ``@{method -}'' or
wenzelm@39847
   204
  @{method succeed}.
wenzelm@39847
   205
wenzelm@39847
   206
  \item Goal facts passed to the method must not be ignored.  If there
wenzelm@39847
   207
  is no sensible use of facts outside the goal state, facts should be
wenzelm@39847
   208
  inserted into the subgoals that are addressed by the method.
wenzelm@39847
   209
wenzelm@39847
   210
  \end{itemize}
wenzelm@39847
   211
wenzelm@39847
   212
  \medskip Syntactically, the language of proof methods is embedded
wenzelm@39847
   213
  into Isar as arguments to certain commands, e.g.\ @{command "by"} or
wenzelm@39847
   214
  @{command apply}.  User-space additions are reasonably easy by
wenzelm@39847
   215
  plugging suitable method-valued parser functions into the framework,
wenzelm@39847
   216
  using the @{command method_setup} command, for example.
wenzelm@39843
   217
wenzelm@39844
   218
  To get a better idea about the range of possibilities, consider the
wenzelm@39844
   219
  following Isar proof schemes.  First some general form of structured
wenzelm@39844
   220
  proof text:
wenzelm@39843
   221
wenzelm@39843
   222
  \medskip
wenzelm@39843
   223
  \begin{tabular}{l}
wenzelm@39843
   224
  @{command from}~@{text "facts\<^sub>1"}~@{command have}~@{text "props"}~@{command using}~@{text "facts\<^sub>2"} \\
wenzelm@39843
   225
  @{command proof}~@{text "(initial_method)"} \\
wenzelm@39843
   226
  \quad@{text "body"} \\
wenzelm@39843
   227
  @{command qed}~@{text "(terminal_method)"} \\
wenzelm@39843
   228
  \end{tabular}
wenzelm@39843
   229
  \medskip
wenzelm@39843
   230
wenzelm@39861
   231
  The goal configuration consists of @{text "facts\<^sub>1"} and @{text
wenzelm@39861
   232
  "facts\<^sub>2"} appended in that order, and various @{text "props"} being
wenzelm@39861
   233
  claimed here.  The @{text "initial_method"} is invoked with facts
wenzelm@39861
   234
  and goals together and refines the problem to something that is
wenzelm@39861
   235
  handled recursively in the proof @{text "body"}.  The @{text
wenzelm@39843
   236
  "terminal_method"} has another chance to finish-off any remaining
wenzelm@39843
   237
  subgoals, but it does not see the facts of the initial step.
wenzelm@39843
   238
wenzelm@39844
   239
  \medskip The second pattern illustrates unstructured proof scripts:
wenzelm@39843
   240
wenzelm@39844
   241
  \medskip
wenzelm@39843
   242
  \begin{tabular}{l}
wenzelm@39843
   243
  @{command have}~@{text "props"} \\
wenzelm@39844
   244
  \quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\
wenzelm@39843
   245
  \quad@{command apply}~@{text "method\<^sub>2"} \\
wenzelm@39844
   246
  \quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\
wenzelm@39843
   247
  \quad@{command done} \\
wenzelm@39843
   248
  \end{tabular}
wenzelm@39843
   249
  \medskip
wenzelm@39843
   250
wenzelm@39861
   251
  The @{text "method\<^sub>1"} operates on the original claim together while
wenzelm@39861
   252
  using @{text "facts\<^sub>1"}.  Since the @{command apply} command
wenzelm@39861
   253
  structurally resets the facts, the @{text "method\<^sub>2"} will operate on
wenzelm@39861
   254
  the remaining goal state without facts.  The @{text "method\<^sub>3"} will
wenzelm@39861
   255
  see again a collection of @{text "facts\<^sub>3"} that has been inserted
wenzelm@39861
   256
  into the script explicitly.
wenzelm@39843
   257
wenzelm@39847
   258
  \medskip Empirically, Isar proof methods can be categorized as
wenzelm@39847
   259
  follows.
wenzelm@39843
   260
wenzelm@39843
   261
  \begin{enumerate}
wenzelm@39843
   262
wenzelm@39847
   263
  \item \emph{Special method with cases} with named context additions
wenzelm@39847
   264
  associated with the follow-up goal state.
wenzelm@39843
   265
wenzelm@39847
   266
  Example: @{method "induct"}, which is also a ``raw'' method since it
wenzelm@39847
   267
  operates on the internal representation of simultaneous claims as
wenzelm@39847
   268
  Pure conjunction, instead of separate subgoals.
wenzelm@39843
   269
wenzelm@39847
   270
  \item \emph{Structured method} with strong emphasis on facts outside
wenzelm@39847
   271
  the goal state.
wenzelm@39847
   272
wenzelm@39847
   273
  Example: @{method "rule"}, which captures the key ideas behind
wenzelm@39847
   274
  structured reasoning in Isar in purest form.
wenzelm@39843
   275
wenzelm@39847
   276
  \item \emph{Simple method} with weaker emphasis on facts, which are
wenzelm@39847
   277
  inserted into subgoals to emulate old-style tactical as
wenzelm@39847
   278
  ``premises''.
wenzelm@39843
   279
wenzelm@39847
   280
  Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}.
wenzelm@39843
   281
wenzelm@39847
   282
  \item \emph{Old-style tactic emulation} with detailed numeric goal
wenzelm@39847
   283
  addressing and explicit references to entities of the internal goal
wenzelm@39847
   284
  state (which are otherwise invisible from proper Isar proof text).
wenzelm@39847
   285
  To make the special non-standard status clear, the naming convention
wenzelm@39847
   286
  @{text "foo_tac"} needs to be observed.
wenzelm@39843
   287
wenzelm@39847
   288
  Example: @{method "rule_tac"}.
wenzelm@39843
   289
wenzelm@39843
   290
  \end{enumerate}
wenzelm@39843
   291
wenzelm@39847
   292
  When implementing proof methods, it is advisable to study existing
wenzelm@39847
   293
  implementations carefully and imitate the typical ``boiler plate''
wenzelm@39847
   294
  for context-sensitive parsing and further combinators to wrap-up
wenzelm@39848
   295
  tactic expressions as methods.\footnote{Aliases or abbreviations of
wenzelm@39848
   296
  the standard method combinators should be avoided.  Note that from
wenzelm@39848
   297
  Isabelle99 until Isabelle2009 the system did provide various odd
wenzelm@39848
   298
  combinations of method wrappers that made user applications more
wenzelm@39848
   299
  complicated than necessary.}
wenzelm@39847
   300
*}
wenzelm@39847
   301
wenzelm@39847
   302
text %mlref {*
wenzelm@39847
   303
  \begin{mldecls}
wenzelm@39847
   304
  @{index_ML_type Proof.method} \\
wenzelm@39847
   305
  @{index_ML METHOD_CASES: "(thm list -> cases_tactic) -> Proof.method"} \\
wenzelm@39847
   306
  @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
wenzelm@39847
   307
  @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
wenzelm@39847
   308
  @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
wenzelm@39847
   309
  @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
wenzelm@39847
   310
  @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\
wenzelm@39847
   311
  @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
wenzelm@39847
   312
  string -> theory -> theory"} \\
wenzelm@39847
   313
  \end{mldecls}
wenzelm@39847
   314
wenzelm@39847
   315
  \begin{description}
wenzelm@39847
   316
wenzelm@39847
   317
  \item @{ML_type Proof.method} represents proof methods as abstract type.
wenzelm@39847
   318
wenzelm@39847
   319
  \item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps
wenzelm@39847
   320
  @{text cases_tactic} depending on goal facts as proof method with
wenzelm@39847
   321
  cases; the goal context is passed via method syntax.
wenzelm@39847
   322
wenzelm@39847
   323
  \item @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text
wenzelm@39847
   324
  tactic} depending on goal facts as regular proof method; the goal
wenzelm@39847
   325
  context is passed via method syntax.
wenzelm@39847
   326
wenzelm@39847
   327
  \item @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that
wenzelm@39847
   328
  addresses all subgoals uniformly as simple proof method.  Goal facts
wenzelm@39847
   329
  are already inserted into all subgoals before @{text "tactic"} is
wenzelm@39847
   330
  applied.
wenzelm@39847
   331
wenzelm@39847
   332
  \item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that
wenzelm@39847
   333
  addresses a specific subgoal as simple proof method.  Goal facts are
wenzelm@39847
   334
  already inserted into the first subgoal before @{text "tactic"} is
wenzelm@39847
   335
  applied to the same.
wenzelm@39847
   336
wenzelm@39847
   337
  \item @{ML HEADGOAL}~@{text "tactic"} applies @{text "tactic"} to
wenzelm@39847
   338
  the first subgoal.  This is convenient to reproduce part the @{ML
wenzelm@39847
   339
  SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example.
wenzelm@39847
   340
wenzelm@39847
   341
  \item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text
wenzelm@39847
   342
  "facts"} into subgoal @{text "i"}.  This is convenient to reproduce
wenzelm@39847
   343
  part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping
wenzelm@39847
   344
  within regular @{ML METHOD}, for example.
wenzelm@39847
   345
wenzelm@39847
   346
  \item @{ML Method.setup}~@{text "name parser description"} provides
wenzelm@39848
   347
  the functionality of the Isar command @{command method_setup} as ML
wenzelm@39848
   348
  function.
wenzelm@39847
   349
wenzelm@39847
   350
  \end{description}
wenzelm@39847
   351
*}
wenzelm@39847
   352
wenzelm@39851
   353
text %mlex {* See also @{command method_setup} in
wenzelm@39851
   354
  \cite{isabelle-isar-ref} which includes some abstract examples.
wenzelm@39851
   355
wenzelm@39851
   356
  \medskip The following toy examples illustrate how the goal facts
wenzelm@39848
   357
  and state are passed to proof methods.  The pre-defined proof method
wenzelm@39848
   358
  called ``@{method tactic}'' wraps ML source of type @{ML_type
wenzelm@39847
   359
  tactic} (abstracted over @{verbatim facts}).  This allows immediate
wenzelm@39848
   360
  experimentation without parsing of concrete syntax. *}
wenzelm@20472
   361
wenzelm@39847
   362
example_proof
wenzelm@39847
   363
  assume a: A and b: B
wenzelm@39847
   364
wenzelm@39847
   365
  have "A \<and> B"
wenzelm@39847
   366
    apply (tactic {* rtac @{thm conjI} 1 *})
wenzelm@39847
   367
    using a apply (tactic {* resolve_tac facts 1 *})
wenzelm@39847
   368
    using b apply (tactic {* resolve_tac facts 1 *})
wenzelm@39847
   369
    done
wenzelm@39847
   370
wenzelm@39847
   371
  have "A \<and> B"
wenzelm@39847
   372
    using a and b
wenzelm@39847
   373
    ML_val "@{Isar.goal}"
wenzelm@39847
   374
    apply (tactic {* Method.insert_tac facts 1 *})
wenzelm@39847
   375
    apply (tactic {* (rtac @{thm conjI} THEN_ALL_NEW atac) 1 *})
wenzelm@39847
   376
    done
wenzelm@39847
   377
qed
wenzelm@39847
   378
wenzelm@39848
   379
text {* \medskip The next example implements a method that simplifies
wenzelm@39848
   380
  the first subgoal by rewrite rules given as arguments.  *}
wenzelm@39848
   381
wenzelm@39848
   382
method_setup my_simp = {*
wenzelm@39848
   383
  Attrib.thms >> (fn thms => fn ctxt =>
wenzelm@39848
   384
    SIMPLE_METHOD' (fn i =>
wenzelm@39848
   385
      CHANGED (asm_full_simp_tac
wenzelm@39848
   386
        (HOL_basic_ss addsimps thms) i)))
wenzelm@39848
   387
*} "rewrite subgoal by given rules"
wenzelm@39848
   388
wenzelm@39848
   389
text {* The concrete syntax wrapping of @{command method_setup} always
wenzelm@39848
   390
  passes-through the proof context at the end of parsing, but it is
wenzelm@39848
   391
  not used in this example.
wenzelm@39848
   392
wenzelm@39848
   393
  The @{ML Attrib.thms} parser produces a list of theorems from the
wenzelm@39848
   394
  usual Isar syntax involving attribute expressions etc.\ (syntax
wenzelm@39848
   395
  category @{syntax thmrefs}).  The resulting @{verbatim thms} are
wenzelm@39848
   396
  added to @{ML HOL_basic_ss} which already contains the basic
wenzelm@39848
   397
  Simplifier setup for HOL.
wenzelm@39848
   398
wenzelm@39848
   399
  The tactic @{ML asm_full_simp_tac} is the one that is also used in
wenzelm@39848
   400
  method @{method simp} by default.  The extra wrapping by the @{ML
wenzelm@39848
   401
  CHANGED} tactical ensures progress of simplification: identical goal
wenzelm@39848
   402
  states are filtered out explicitly to make the raw tactic conform to
wenzelm@39848
   403
  standard Isar method behaviour.
wenzelm@39848
   404
wenzelm@39848
   405
  \medskip Method @{method my_simp} can be used in Isar proofs like
wenzelm@39848
   406
  this:
wenzelm@39847
   407
*}
wenzelm@39847
   408
wenzelm@39848
   409
example_proof
wenzelm@39848
   410
  fix a b c
wenzelm@39851
   411
  assume a: "a = b"
wenzelm@39851
   412
  assume b: "b = c"
wenzelm@39851
   413
  have "a = c" by (my_simp a b)
wenzelm@39851
   414
qed
wenzelm@39851
   415
wenzelm@39851
   416
text {* Here is a similar method that operates on all subgoals,
wenzelm@39851
   417
  instead of just the first one. *}
wenzelm@39851
   418
wenzelm@39851
   419
method_setup my_simp_all = {*
wenzelm@39851
   420
  Attrib.thms >> (fn thms => fn ctxt =>
wenzelm@39851
   421
    SIMPLE_METHOD
wenzelm@39851
   422
      (CHANGED
wenzelm@39851
   423
        (ALLGOALS (asm_full_simp_tac
wenzelm@39851
   424
          (HOL_basic_ss addsimps thms)))))
wenzelm@39851
   425
*} "rewrite all subgoals by given rules"
wenzelm@39851
   426
wenzelm@39851
   427
example_proof
wenzelm@39851
   428
  fix a b c
wenzelm@39851
   429
  assume a: "a = b"
wenzelm@39851
   430
  assume b: "b = c"
wenzelm@39851
   431
  have "a = c" and "c = b" by (my_simp_all a b)
wenzelm@39851
   432
wenzelm@39848
   433
qed
wenzelm@39848
   434
wenzelm@39848
   435
text {* \medskip Apart from explicit arguments, common proof methods
wenzelm@39848
   436
  typically work with a default configuration provided by the context.
wenzelm@39848
   437
  As a shortcut to rule management we use a cheap solution via functor
wenzelm@39848
   438
  @{ML_functor Named_Thms} (see also @{"file"
wenzelm@39848
   439
  "~~/src/Pure/Tools/named_thms.ML"}).  *}
wenzelm@39848
   440
wenzelm@39847
   441
ML {*
wenzelm@39847
   442
  structure My_Simps =
wenzelm@39847
   443
    Named_Thms
wenzelm@39847
   444
      (val name = "my_simp" val description = "my_simp rule")
wenzelm@39847
   445
*}
wenzelm@39847
   446
setup My_Simps.setup
wenzelm@39847
   447
wenzelm@39861
   448
text {* This provides ML access to a list of theorems in canonical
wenzelm@39861
   449
  declaration order via @{ML My_Simps.get}.  The user can add or
wenzelm@39861
   450
  delete rules via the attribute @{attribute my_simp}.  The actual
wenzelm@39861
   451
  proof method is now defined as before, but we append the explicit
wenzelm@39861
   452
  arguments and the rules from the context.  *}
wenzelm@39847
   453
wenzelm@39848
   454
method_setup my_simp' = {*
wenzelm@39848
   455
  Attrib.thms >> (fn thms => fn ctxt =>
wenzelm@39847
   456
    SIMPLE_METHOD' (fn i =>
wenzelm@39847
   457
      CHANGED (asm_full_simp_tac
wenzelm@39848
   458
        (HOL_basic_ss addsimps (thms @ My_Simps.get ctxt)) i)))
wenzelm@39848
   459
*} "rewrite subgoal by given rules and my_simp rules from the context"
wenzelm@39847
   460
wenzelm@39848
   461
text {*
wenzelm@39848
   462
  \medskip Method @{method my_simp'} can be used in Isar proofs
wenzelm@39848
   463
  like this:
wenzelm@39848
   464
*}
wenzelm@39847
   465
wenzelm@39847
   466
example_proof
wenzelm@39847
   467
  fix a b c
wenzelm@39847
   468
  assume [my_simp]: "a \<equiv> b"
wenzelm@39847
   469
  assume [my_simp]: "b \<equiv> c"
wenzelm@39848
   470
  have "a \<equiv> c" by my_simp'
wenzelm@39847
   471
qed
wenzelm@39847
   472
wenzelm@39851
   473
text {* \medskip The @{method my_simp} variants defined above are
wenzelm@39851
   474
  ``simple'' methods, i.e.\ the goal facts are merely inserted as goal
wenzelm@39851
   475
  premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper.
wenzelm@39851
   476
  For proof methods that are similar to the standard collection of
wenzelm@39851
   477
  @{method simp}, @{method blast}, @{method auto} little more can be
wenzelm@39851
   478
  done here.
wenzelm@39847
   479
wenzelm@39847
   480
  Note that using the primary goal facts in the same manner as the
wenzelm@39848
   481
  method arguments obtained via concrete syntax or the context does
wenzelm@39848
   482
  not meet the requirement of ``strong emphasis on facts'' of regular
wenzelm@39848
   483
  proof methods, because rewrite rules as used above can be easily
wenzelm@39848
   484
  ignored.  A proof text ``@{command using}~@{text "foo"}~@{command
wenzelm@39848
   485
  "by"}~@{text "my_simp"}'' where @{text "foo"} is not used would
wenzelm@39848
   486
  deceive the reader.
wenzelm@39847
   487
wenzelm@39847
   488
  \medskip The technical treatment of rules from the context requires
wenzelm@39847
   489
  further attention.  Above we rebuild a fresh @{ML_type simpset} from
wenzelm@39848
   490
  the arguments and \emph{all} rules retrieved from the context on
wenzelm@39848
   491
  every invocation of the method.  This does not scale to really large
wenzelm@39848
   492
  collections of rules, which easily emerges in the context of a big
wenzelm@39848
   493
  theory library, for example.
wenzelm@39847
   494
wenzelm@39848
   495
  This is an inherent limitation of the simplistic rule management via
wenzelm@39848
   496
  functor @{ML_functor Named_Thms}, because it lacks tool-specific
wenzelm@39847
   497
  storage and retrieval.  More realistic applications require
wenzelm@39847
   498
  efficient index-structures that organize theorems in a customized
wenzelm@39847
   499
  manner, such as a discrimination net that is indexed by the
wenzelm@39848
   500
  left-hand sides of rewrite rules.  For variations on the Simplifier,
wenzelm@39848
   501
  re-use of the existing type @{ML_type simpset} is adequate, but
wenzelm@39847
   502
  scalability requires it be maintained statically within the context
wenzelm@39847
   503
  data, not dynamically on each tool invocation.  *}
wenzelm@39847
   504
wenzelm@29759
   505
wenzelm@20472
   506
section {* Attributes *}
wenzelm@20472
   507
wenzelm@39849
   508
text {* An \emph{attribute} is a function @{text "context \<times> thm \<rightarrow>
wenzelm@39849
   509
  context \<times> thm"}, which means both a (generic) context and a theorem
wenzelm@39849
   510
  can be modified simultaneously.  In practice this fully general form
wenzelm@39849
   511
  is very rare, instead attributes are presented either as
wenzelm@39849
   512
  \emph{declaration attribute:} @{text "thm \<rightarrow> context \<rightarrow> context"} or
wenzelm@39849
   513
  \emph{rule attribute:} @{text "context \<rightarrow> thm \<rightarrow> thm"}.
wenzelm@39849
   514
wenzelm@39849
   515
  Attributes can have additional arguments via concrete syntax.  There
wenzelm@39849
   516
  is a collection of context-sensitive parsers for various logical
wenzelm@39849
   517
  entities (types, terms, theorems).  These already take care of
wenzelm@39849
   518
  applying morphisms to the arguments when attribute expressions are
wenzelm@39849
   519
  moved into a different context (see also \secref{sec:morphisms}).
wenzelm@39849
   520
wenzelm@39849
   521
  When implementing declaration attributes, it is important to operate
wenzelm@39849
   522
  exactly on the variant of the generic context that is provided by
wenzelm@39849
   523
  the system, which is either global theory context or local proof
wenzelm@39849
   524
  context.  In particular, the background theory of a local context
wenzelm@39849
   525
  must not be modified in this situation! *}
wenzelm@39849
   526
wenzelm@39849
   527
text %mlref {*
wenzelm@39849
   528
  \begin{mldecls}
wenzelm@39849
   529
  @{index_ML_type attribute: "Context.generic * thm -> Context.generic * thm"} \\
wenzelm@39849
   530
  @{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\
wenzelm@39849
   531
  @{index_ML Thm.declaration_attribute: "
wenzelm@39849
   532
  (thm -> Context.generic -> Context.generic) -> attribute"} \\
wenzelm@39849
   533
  @{index_ML Attrib.setup: "binding -> attribute context_parser ->
wenzelm@39849
   534
  string -> theory -> theory"} \\
wenzelm@39849
   535
  \end{mldecls}
wenzelm@39849
   536
wenzelm@39849
   537
  \begin{description}
wenzelm@39849
   538
wenzelm@39849
   539
  \item @{ML_type attribute} represents attributes as concrete type alias.
wenzelm@39849
   540
wenzelm@39849
   541
  \item @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps
wenzelm@39849
   542
  a context-dependent rule (mapping on @{ML_type thm}) as attribute.
wenzelm@39849
   543
wenzelm@39849
   544
  \item @{ML Thm.declaration_attribute}~@{text "(fn thm => decl)"}
wenzelm@39849
   545
  wraps a theorem-dependent declaration (mapping on @{ML_type
wenzelm@39849
   546
  Context.generic}) as attribute.
wenzelm@39849
   547
wenzelm@39849
   548
  \item @{ML Attrib.setup}~@{text "name parser description"} provides
wenzelm@39849
   549
  the functionality of the Isar command @{command attribute_setup} as
wenzelm@39849
   550
  ML function.
wenzelm@39849
   551
wenzelm@39849
   552
  \end{description}
wenzelm@39849
   553
*}
wenzelm@39849
   554
wenzelm@39849
   555
text %mlex {* See also @{command attribute_setup} in
wenzelm@39849
   556
  \cite{isabelle-isar-ref} which includes some abstract examples. *}
wenzelm@30272
   557
wenzelm@20472
   558
end