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