src/Doc/Isar_Ref/Proof_Script.thy
author wenzelm
Thu, 02 Jul 2015 14:09:43 +0200
changeset 60631 441fdbfbb2d3
parent 60484 98ee86354354
child 61439 2bf52eec4e8a
permissions -rw-r--r--
documentation for 'subgoal' command;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60484
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     1
theory Proof_Script
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     2
imports Base Main
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     3
begin
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     4
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     5
chapter \<open>Proof scripts\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     6
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     7
text \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     8
  Interactive theorem proving is traditionally associated with ``proof
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
     9
  scripts'', but Isabelle/Isar is centered around structured \emph{proof
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    10
  documents} instead (see also \chref{ch:proofs}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    11
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    12
  Nonetheless, it is possible to emulate proof scripts by sequential
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    13
  refinements of a proof state in backwards mode, notably with the @{command
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    14
  apply} command (see \secref{sec:tactic-commands}). There are also various
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    15
  proof methods that allow to refer to implicit goal state information that
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    16
  is normally not accessible to structured Isar proofs (see
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    17
  \secref{sec:tactics}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    18
\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    19
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    20
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    21
section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    22
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    23
text \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    24
  \begin{matharray}{rcl}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    25
    @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    26
    @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    27
    @{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    28
    @{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    29
    @{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    30
    @{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    31
    @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    32
  \end{matharray}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    33
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    34
  @{rail \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    35
    @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    36
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    37
    ( @@{command apply} | @@{command apply_end} ) @{syntax method}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    38
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    39
    @@{command defer} @{syntax nat}?
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    40
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    41
    @@{command prefer} @{syntax nat}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    42
  \<close>}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    43
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    44
  \begin{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    45
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    46
  \item @{command "supply"} supports fact definitions during goal
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    47
  refinement: it is similar to @{command "note"}, but it operates in
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    48
  backwards mode and does not have any impact on chained facts.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    49
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    50
  \item @{command "apply"}~@{text m} applies proof method @{text m} in
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    51
  initial position, but unlike @{command "proof"} it retains ``@{text
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    52
  "proof(prove)"}'' mode.  Thus consecutive method applications may be
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    53
  given just as in tactic scripts.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    54
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    55
  Facts are passed to @{text m} as indicated by the goal's
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    56
  forward-chain mode, and are \emph{consumed} afterwards.  Thus any
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    57
  further @{command "apply"} command would always work in a purely
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    58
  backward manner.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    59
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    60
  \item @{command "apply_end"}~@{text "m"} applies proof method @{text
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    61
  m} as if in terminal position.  Basically, this simulates a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    62
  multi-step tactic script for @{command "qed"}, but may be given
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    63
  anywhere within the proof body.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    64
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    65
  No facts are passed to @{text m} here.  Furthermore, the static
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    66
  context is that of the enclosing goal (as for actual @{command
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    67
  "qed"}).  Thus the proof method may not refer to any assumptions
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    68
  introduced in the current body, for example.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    69
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    70
  \item @{command "done"} completes a proof script, provided that the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    71
  current goal state is solved completely.  Note that actual
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    72
  structured proof commands (e.g.\ ``@{command "."}'' or @{command
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    73
  "sorry"}) may be used to conclude proof scripts as well.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    74
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    75
  \item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    76
  shuffle the list of pending goals: @{command "defer"} puts off
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    77
  sub-goal @{text n} to the end of the list (@{text "n = 1"} by
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    78
  default), while @{command "prefer"} brings sub-goal @{text n} to the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    79
  front.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    80
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    81
  \item @{command "back"} does back-tracking over the result sequence
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    82
  of the latest proof command.  Any proof command may return multiple
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    83
  results, and this command explores the possibilities step-by-step.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    84
  It is mainly useful for experimentation and interactive exploration,
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    85
  and should be avoided in finished proofs.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    86
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    87
  \end{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    88
\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    89
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
    90
60631
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    91
section \<open>Explicit subgoal structure\<close>
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    92
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    93
text \<open>
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    94
  \begin{matharray}{rcl}
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    95
    @{command_def "subgoal"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    96
  \end{matharray}
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    97
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    98
  @{rail \<open>
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
    99
    @@{command subgoal} @{syntax thmbind}? prems? params?
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   100
    ;
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   101
    prems: @'premises' @{syntax thmbind}?
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   102
    ;
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   103
    params: @'for' '\<dots>'? (('_' | @{syntax name})+)
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   104
  \<close>}
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   105
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   106
  \begin{description}
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   107
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   108
  \item @{command "subgoal"} allows to impose some structure on backward
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   109
  refinements, to avoid proof scripts degenerating into long of @{command
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   110
  apply} sequences.
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   111
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   112
  The current goal state, which is essentially a hidden part of the Isar/VM
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   113
  configurtation, is turned into a proof context and remaining conclusion.
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   114
  This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   115
  structured proofs, but the text of the parameters, premises and conclusion
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   116
  is not given explicitly.
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   117
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   118
  Goal parameters may be specified separately, in order to allow referring
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   119
  to them in the proof body: ``@{command subgoal}~@{keyword "for"}~@{text "x
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   120
  y z"}'' names a \emph{prefix}, and ``@{command subgoal}~@{keyword
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   121
  "for"}~@{text "\<dots> x y z"}'' names a \emph{suffix} of goal parameters. The
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   122
  latter uses a literal @{verbatim "\<dots>"} symbol as notation. Parameter
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   123
  positions may be skipped via dummies (underscore). Unspecified names
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   124
  remain internal, and thus inaccessible in the proof text.
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   125
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   126
  ``@{command subgoal}~@{keyword "premises"}~@{text prems}'' indicates that
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   127
  goal premises should be turned into assumptions of the context (otherwise
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   128
  the remaining conclusion is a Pure implication). The fact name and
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   129
  attributes are optional; the particular name ``@{text prems}'' is a common
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   130
  convention for the premises of an arbitrary goal context in proof scripts.
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   131
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   132
  ``@{command subgoal}~@{text result}'' indicates a fact name for the result
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   133
  of a proven subgoal. Thus it may be re-used in further reasoning, similar
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   134
  to the result of @{command show} in structured Isar proofs.
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   135
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   136
  \end{description}
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   137
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   138
  Here are some abstract examples:
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   139
\<close>
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   140
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   141
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   142
  and "\<And>u v. X u \<Longrightarrow> Y v"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   143
  subgoal sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   144
  subgoal sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   145
  done
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   146
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   147
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   148
  and "\<And>u v. X u \<Longrightarrow> Y v"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   149
  subgoal for x y z sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   150
  subgoal for u v sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   151
  done
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   152
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   153
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   154
  and "\<And>u v. X u \<Longrightarrow> Y v"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   155
  subgoal premises for x y z
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   156
    using \<open>A x\<close> \<open>B y\<close>
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   157
    sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   158
  subgoal premises for u v
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   159
    using \<open>X u\<close>
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   160
    sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   161
  done
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   162
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   163
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   164
  and "\<And>u v. X u \<Longrightarrow> Y v"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   165
  subgoal r premises prems for x y z
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   166
  proof -
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   167
    have "A x" by (fact prems)
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   168
    moreover have "B y" by (fact prems)
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   169
    ultimately show ?thesis sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   170
  qed
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   171
  subgoal premises prems for u v
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   172
  proof -
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   173
    have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   174
    moreover
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   175
    have "X u" by (fact prems)
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   176
    ultimately show ?thesis sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   177
  qed
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   178
  done
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   179
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   180
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   181
  subgoal premises prems for \<dots> z
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   182
  proof -
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   183
    from prems show "C z" sorry
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   184
  qed
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   185
  done
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   186
441fdbfbb2d3 documentation for 'subgoal' command;
wenzelm
parents: 60484
diff changeset
   187
60484
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   188
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   189
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   190
text \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   191
  The following improper proof methods emulate traditional tactics.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   192
  These admit direct access to the goal state, which is normally
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   193
  considered harmful!  In particular, this may involve both numbered
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   194
  goal addressing (default 1), and dynamic instantiation within the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   195
  scope of some subgoal.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   196
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   197
  \begin{warn}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   198
    Dynamic instantiations refer to universally quantified parameters
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   199
    of a subgoal (the dynamic context) rather than fixed variables and
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   200
    term abbreviations of a (static) Isar context.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   201
  \end{warn}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   202
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   203
  Tactic emulation methods, unlike their ML counterparts, admit
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   204
  simultaneous instantiation from both dynamic and static contexts.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   205
  If names occur in both contexts goal parameters hide locally fixed
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   206
  variables.  Likewise, schematic variables refer to term
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   207
  abbreviations, if present in the static context.  Otherwise the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   208
  schematic variable is interpreted as a schematic variable and left
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   209
  to be solved by unification with certain parts of the subgoal.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   210
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   211
  Note that the tactic emulation proof methods in Isabelle/Isar are
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   212
  consistently named @{text foo_tac}.  Note also that variable names
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   213
  occurring on left hand sides of instantiations must be preceded by a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   214
  question mark if they coincide with a keyword or contain dots.  This
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   215
  is consistent with the attribute @{attribute "where"} (see
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   216
  \secref{sec:pure-meth-att}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   217
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   218
  \begin{matharray}{rcl}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   219
    @{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   220
    @{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   221
    @{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   222
    @{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   223
    @{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   224
    @{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   225
    @{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   226
    @{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   227
    @{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   228
    @{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   229
    @{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   230
  \end{matharray}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   231
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   232
  @{rail \<open>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   233
    (@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   234
      @@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   235
    (@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   236
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   237
    @@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   238
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   239
    @@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   240
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   241
    @@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   242
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   243
    @@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   244
    ;
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   245
    (@@{method tactic} | @@{method raw_tactic}) @{syntax text}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   246
  \<close>}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   247
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   248
\begin{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   249
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   250
  \item @{method rule_tac} etc. do resolution of rules with explicit
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   251
  instantiation.  This works the same way as the ML tactics @{ML
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   252
  Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   253
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   254
  Multiple rules may be only given if there is no instantiation; then
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   255
  @{method rule_tac} is the same as @{ML resolve_tac} in ML (see
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   256
  @{cite "isabelle-implementation"}).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   257
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   258
  \item @{method cut_tac} inserts facts into the proof state as
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   259
  assumption of a subgoal; instantiations may be given as well.  Note
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   260
  that the scope of schematic variables is spread over the main goal
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   261
  statement and rule premises are turned into new subgoals.  This is
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   262
  in contrast to the regular method @{method insert} which inserts
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   263
  closed rule statements.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   264
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   265
  \item @{method thin_tac}~@{text \<phi>} deletes the specified premise
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   266
  from a subgoal.  Note that @{text \<phi>} may contain schematic
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   267
  variables, to abbreviate the intended proposition; the first
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   268
  matching subgoal premise will be deleted.  Removing useless premises
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   269
  from a subgoal increases its readability and can make search tactics
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   270
  run faster.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   271
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   272
  \item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   273
  @{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   274
  as new subgoals (in the original context).
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   275
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   276
  \item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   277
  goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   278
  \emph{suffix} of variables.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   279
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   280
  \item @{method rotate_tac}~@{text n} rotates the premises of a
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   281
  subgoal by @{text n} positions: from right to left if @{text n} is
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   282
  positive, and from left to right if @{text n} is negative; the
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   283
  default value is 1.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   284
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   285
  \item @{method tactic}~@{text "text"} produces a proof method from
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   286
  any ML text of type @{ML_type tactic}.  Apart from the usual ML
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   287
  environment and the current proof context, the ML code may refer to
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   288
  the locally bound values @{ML_text facts}, which indicates any
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   289
  current facts used for forward-chaining.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   290
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   291
  \item @{method raw_tactic} is similar to @{method tactic}, but
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   292
  presents the goal state in its raw internal form, where simultaneous
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   293
  subgoals appear as conjunction of the logical framework instead of
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   294
  the usual split into several subgoals.  While feature this is useful
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   295
  for debugging of complex method definitions, it should not never
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   296
  appear in production theories.
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   297
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   298
  \end{description}
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   299
\<close>
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   300
98ee86354354 moved sections;
wenzelm
parents:
diff changeset
   301
end