doc-src/IsarRef/Thy/Proof.thy
author wenzelm
Fri, 11 Jul 2008 23:17:23 +0200
changeset 27554 2deaa546ba0d
parent 27141 9bfcdb1905e1
child 28754 6f2e67a3dfaa
permissions -rw-r--r--
Sorts.weaken: abstract argument;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26869
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     1
(* $Id$ *)
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     2
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     3
theory Proof
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     4
imports Main
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     5
begin
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     6
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     7
chapter {* Proofs *}
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
     8
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
     9
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    10
  Proof commands perform transitions of Isar/VM machine
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    11
  configurations, which are block-structured, consisting of a stack of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    12
  nodes with three main components: logical proof context, current
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    13
  facts, and open goals.  Isar/VM transitions are \emph{typed}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    14
  according to the following three different modes of operation:
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    15
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    16
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    17
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    18
  \item [@{text "proof(prove)"}] means that a new goal has just been
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    19
  stated that is now to be \emph{proven}; the next command may refine
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    20
  it by some proof method, and enter a sub-proof to establish the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    21
  actual result.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    22
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    23
  \item [@{text "proof(state)"}] is like a nested theory mode: the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    24
  context may be augmented by \emph{stating} additional assumptions,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    25
  intermediate results etc.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    26
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    27
  \item [@{text "proof(chain)"}] is intermediate between @{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    28
  "proof(state)"} and @{text "proof(prove)"}: existing facts (i.e.\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    29
  the contents of the special ``@{fact_ref this}'' register) have been
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    30
  just picked up in order to be used when refining the goal claimed
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    31
  next.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    32
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    33
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    34
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    35
  The proof mode indicator may be read as a verb telling the writer
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    36
  what kind of operation may be performed next.  The corresponding
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    37
  typings of proof commands restricts the shape of well-formed proof
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    38
  texts to particular command sequences.  So dynamic arrangements of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    39
  commands eventually turn out as static texts of a certain structure.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    40
  \Appref{ap:refcard} gives a simplified grammar of the overall
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    41
  (extensible) language emerging that way.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    42
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    43
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    44
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    45
section {* Context elements \label{sec:proof-context} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    46
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    47
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    48
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    49
    @{command_def "fix"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    50
    @{command_def "assume"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    51
    @{command_def "presume"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    52
    @{command_def "def"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    53
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    54
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    55
  The logical proof context consists of fixed variables and
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    56
  assumptions.  The former closely correspond to Skolem constants, or
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    57
  meta-level universal quantification as provided by the Isabelle/Pure
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    58
  logical framework.  Introducing some \emph{arbitrary, but fixed}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    59
  variable via ``@{command "fix"}~@{text x}'' results in a local value
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    60
  that may be used in the subsequent proof as any other variable or
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    61
  constant.  Furthermore, any result @{text "\<turnstile> \<phi>[x]"} exported from
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    62
  the context will be universally closed wrt.\ @{text x} at the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    63
  outermost level: @{text "\<turnstile> \<And>x. \<phi>[x]"} (this is expressed in normal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    64
  form using Isabelle's meta-variables).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    65
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    66
  Similarly, introducing some assumption @{text \<chi>} has two effects.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    67
  On the one hand, a local theorem is created that may be used as a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    68
  fact in subsequent proof steps.  On the other hand, any result
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    69
  @{text "\<chi> \<turnstile> \<phi>"} exported from the context becomes conditional wrt.\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    70
  the assumption: @{text "\<turnstile> \<chi> \<Longrightarrow> \<phi>"}.  Thus, solving an enclosing goal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    71
  using such a result would basically introduce a new subgoal stemming
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    72
  from the assumption.  How this situation is handled depends on the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    73
  version of assumption command used: while @{command "assume"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    74
  insists on solving the subgoal by unification with some premise of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    75
  the goal, @{command "presume"} leaves the subgoal unchanged in order
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    76
  to be proved later by the user.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    77
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    78
  Local definitions, introduced by ``@{command "def"}~@{text "x \<equiv>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    79
  t"}'', are achieved by combining ``@{command "fix"}~@{text x}'' with
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    80
  another version of assumption that causes any hypothetical equation
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    81
  @{text "x \<equiv> t"} to be eliminated by the reflexivity rule.  Thus,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    82
  exporting some result @{text "x \<equiv> t \<turnstile> \<phi>[x]"} yields @{text "\<turnstile>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    83
  \<phi>[t]"}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    84
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    85
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    86
    'fix' (vars + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    87
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    88
    ('assume' | 'presume') (props + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    89
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    90
    'def' (def + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    91
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    92
    def: thmdecl? \\ name ('==' | equiv) term termpat?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    93
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    94
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    95
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    96
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    97
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    98
  \item [@{command "fix"}~@{text x}] introduces a local variable
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
    99
  @{text x} that is \emph{arbitrary, but fixed.}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   100
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   101
  \item [@{command "assume"}~@{text "a: \<phi>"} and @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   102
  "presume"}~@{text "a: \<phi>"}] introduce a local fact @{text "\<phi> \<turnstile> \<phi>"} by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   103
  assumption.  Subsequent results applied to an enclosing goal (e.g.\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   104
  by @{command_ref "show"}) are handled as follows: @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   105
  "assume"} expects to be able to unify with existing premises in the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   106
  goal, while @{command "presume"} leaves @{text \<phi>} as new subgoals.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   107
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   108
  Several lists of assumptions may be given (separated by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   109
  @{keyword_ref "and"}; the resulting list of current facts consists
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   110
  of all of these concatenated.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   111
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   112
  \item [@{command "def"}~@{text "x \<equiv> t"}] introduces a local
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   113
  (non-polymorphic) definition.  In results exported from the context,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   114
  @{text x} is replaced by @{text t}.  Basically, ``@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   115
  "def"}~@{text "x \<equiv> t"}'' abbreviates ``@{command "fix"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   116
  x}~@{command "assume"}~@{text "x \<equiv> t"}'', with the resulting
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   117
  hypothetical equation solved by reflexivity.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   118
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   119
  The default name for the definitional equation is @{text x_def}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   120
  Several simultaneous definitions may be given at the same time.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   121
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   122
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   123
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   124
  The special name @{fact_ref prems} refers to all assumptions of the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   125
  current context as a list of theorems.  This feature should be used
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   126
  with great care!  It is better avoided in final proof texts.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   127
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   128
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   129
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   130
section {* Facts and forward chaining *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   131
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   132
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   133
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   134
    @{command_def "note"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   135
    @{command_def "then"} & : & \isartrans{proof(state)}{proof(chain)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   136
    @{command_def "from"} & : & \isartrans{proof(state)}{proof(chain)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   137
    @{command_def "with"} & : & \isartrans{proof(state)}{proof(chain)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   138
    @{command_def "using"} & : & \isartrans{proof(prove)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   139
    @{command_def "unfolding"} & : & \isartrans{proof(prove)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   140
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   141
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   142
  New facts are established either by assumption or proof of local
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   143
  statements.  Any fact will usually be involved in further proofs,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   144
  either as explicit arguments of proof methods, or when forward
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   145
  chaining towards the next goal via @{command "then"} (and variants);
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   146
  @{command "from"} and @{command "with"} are composite forms
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   147
  involving @{command "note"}.  The @{command "using"} elements
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   148
  augments the collection of used facts \emph{after} a goal has been
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   149
  stated.  Note that the special theorem name @{fact_ref this} refers
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   150
  to the most recently established facts, but only \emph{before}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   151
  issuing a follow-up claim.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   152
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   153
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   154
    'note' (thmdef? thmrefs + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   155
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   156
    ('from' | 'with' | 'using' | 'unfolding') (thmrefs + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   157
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   158
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   159
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   160
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   161
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   162
  \item [@{command "note"}~@{text "a = b\<^sub>1 \<dots> b\<^sub>n"}]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   163
  recalls existing facts @{text "b\<^sub>1, \<dots>, b\<^sub>n"}, binding
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   164
  the result as @{text a}.  Note that attributes may be involved as
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   165
  well, both on the left and right hand sides.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   166
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   167
  \item [@{command "then"}] indicates forward chaining by the current
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   168
  facts in order to establish the goal to be claimed next.  The
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   169
  initial proof method invoked to refine that will be offered the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   170
  facts to do ``anything appropriate'' (see also
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   171
  \secref{sec:proof-steps}).  For example, method @{method_ref rule}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   172
  (see \secref{sec:pure-meth-att}) would typically do an elimination
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   173
  rather than an introduction.  Automatic methods usually insert the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   174
  facts into the goal state before operation.  This provides a simple
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   175
  scheme to control relevance of facts in automated proof search.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   176
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   177
  \item [@{command "from"}~@{text b}] abbreviates ``@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   178
  "note"}~@{text b}~@{command "then"}''; thus @{command "then"} is
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   179
  equivalent to ``@{command "from"}~@{text this}''.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   180
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   181
  \item [@{command "with"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   182
  abbreviates ``@{command "from"}~@{text "b\<^sub>1 \<dots> b\<^sub>n \<AND>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   183
  this"}''; thus the forward chaining is from earlier facts together
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   184
  with the current ones.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   185
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   186
  \item [@{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] augments
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   187
  the facts being currently indicated for use by a subsequent
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   188
  refinement step (such as @{command_ref "apply"} or @{command_ref
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   189
  "proof"}).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   190
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   191
  \item [@{command "unfolding"}~@{text "b\<^sub>1 \<dots> b\<^sub>n"}] is
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   192
  structurally similar to @{command "using"}, but unfolds definitional
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   193
  equations @{text "b\<^sub>1, \<dots> b\<^sub>n"} throughout the goal state
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   194
  and facts.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   195
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   196
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   197
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   198
  Forward chaining with an empty list of theorems is the same as not
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   199
  chaining at all.  Thus ``@{command "from"}~@{text nothing}'' has no
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   200
  effect apart from entering @{text "prove(chain)"} mode, since
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   201
  @{fact_ref nothing} is bound to the empty list of theorems.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   202
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   203
  Basic proof methods (such as @{method_ref rule}) expect multiple
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   204
  facts to be given in their proper order, corresponding to a prefix
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   205
  of the premises of the rule involved.  Note that positions may be
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   206
  easily skipped using something like @{command "from"}~@{text "_
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   207
  \<AND> a \<AND> b"}, for example.  This involves the trivial rule
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   208
  @{text "PROP \<psi> \<Longrightarrow> PROP \<psi>"}, which is bound in Isabelle/Pure as
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   209
  ``@{fact_ref "_"}'' (underscore).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   210
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   211
  Automated methods (such as @{method simp} or @{method auto}) just
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   212
  insert any given facts before their usual operation.  Depending on
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   213
  the kind of procedure involved, the order of facts is less
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   214
  significant here.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   215
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   216
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   217
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   218
section {* Goal statements \label{sec:goals} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   219
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   220
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   221
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   222
    @{command_def "lemma"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   223
    @{command_def "theorem"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   224
    @{command_def "corollary"} & : & \isartrans{local{\dsh}theory}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   225
    @{command_def "have"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   226
    @{command_def "show"} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   227
    @{command_def "hence"} & : & \isartrans{proof(state)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   228
    @{command_def "thus"} & : & \isartrans{proof(state)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   229
    @{command_def "print_statement"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   230
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   231
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   232
  From a theory context, proof mode is entered by an initial goal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   233
  command such as @{command "lemma"}, @{command "theorem"}, or
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   234
  @{command "corollary"}.  Within a proof, new claims may be
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   235
  introduced locally as well; four variants are available here to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   236
  indicate whether forward chaining of facts should be performed
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   237
  initially (via @{command_ref "then"}), and whether the final result
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   238
  is meant to solve some pending goal.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   239
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   240
  Goals may consist of multiple statements, resulting in a list of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   241
  facts eventually.  A pending multi-goal is internally represented as
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   242
  a meta-level conjunction (printed as @{text "&&"}), which is usually
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   243
  split into the corresponding number of sub-goals prior to an initial
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   244
  method application, via @{command_ref "proof"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   245
  (\secref{sec:proof-steps}) or @{command_ref "apply"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   246
  (\secref{sec:tactic-commands}).  The @{method_ref induct} method
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   247
  covered in \secref{sec:cases-induct} acts on multiple claims
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   248
  simultaneously.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   249
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   250
  Claims at the theory level may be either in short or long form.  A
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   251
  short goal merely consists of several simultaneous propositions
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   252
  (often just one).  A long goal includes an explicit context
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   253
  specification for the subsequent conclusion, involving local
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   254
  parameters and assumptions.  Here the role of each part of the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   255
  statement is explicitly marked by separate keywords (see also
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   256
  \secref{sec:locale}); the local assumptions being introduced here
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   257
  are available as @{fact_ref assms} in the proof.  Moreover, there
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   258
  are two kinds of conclusions: @{element_def "shows"} states several
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   259
  simultaneous propositions (essentially a big conjunction), while
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   260
  @{element_def "obtains"} claims several simultaneous simultaneous
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   261
  contexts of (essentially a big disjunction of eliminated parameters
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   262
  and assumptions, cf.\ \secref{sec:obtain}).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   263
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   264
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   265
    ('lemma' | 'theorem' | 'corollary') target? (goal | longgoal)
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   266
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   267
    ('have' | 'show' | 'hence' | 'thus') goal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   268
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   269
    'print\_statement' modes? thmrefs
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   270
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   271
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   272
    goal: (props + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   273
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   274
    longgoal: thmdecl? (contextelem *) conclusion
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   275
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   276
    conclusion: 'shows' goal | 'obtains' (parname? case + '|')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   277
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   278
    case: (vars + 'and') 'where' (props + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   279
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   280
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   281
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   282
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   283
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   284
  \item [@{command "lemma"}~@{text "a: \<phi>"}] enters proof mode with
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   285
  @{text \<phi>} as main goal, eventually resulting in some fact @{text "\<turnstile>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   286
  \<phi>"} to be put back into the target context.  An additional
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   287
  \railnonterm{context} specification may build up an initial proof
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   288
  context for the subsequent claim; this includes local definitions
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   289
  and syntax as well, see the definition of @{syntax contextelem} in
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   290
  \secref{sec:locale}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   291
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   292
  \item [@{command "theorem"}~@{text "a: \<phi>"} and @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   293
  "corollary"}~@{text "a: \<phi>"}] are essentially the same as @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   294
  "lemma"}~@{text "a: \<phi>"}, but the facts are internally marked as
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   295
  being of a different kind.  This discrimination acts like a formal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   296
  comment.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   297
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   298
  \item [@{command "have"}~@{text "a: \<phi>"}] claims a local goal,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   299
  eventually resulting in a fact within the current logical context.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   300
  This operation is completely independent of any pending sub-goals of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   301
  an enclosing goal statements, so @{command "have"} may be freely
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   302
  used for experimental exploration of potential results within a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   303
  proof body.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   304
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   305
  \item [@{command "show"}~@{text "a: \<phi>"}] is like @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   306
  "have"}~@{text "a: \<phi>"} plus a second stage to refine some pending
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   307
  sub-goal for each one of the finished result, after having been
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   308
  exported into the corresponding context (at the head of the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   309
  sub-proof of this @{command "show"} command).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   310
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   311
  To accommodate interactive debugging, resulting rules are printed
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   312
  before being applied internally.  Even more, interactive execution
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   313
  of @{command "show"} predicts potential failure and displays the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   314
  resulting error as a warning beforehand.  Watch out for the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   315
  following message:
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   316
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   317
  %FIXME proper antiquitation
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   318
  \begin{ttbox}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   319
  Problem! Local statement will fail to solve any pending goal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   320
  \end{ttbox}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   321
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   322
  \item [@{command "hence"}] abbreviates ``@{command "then"}~@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   323
  "have"}'', i.e.\ claims a local goal to be proven by forward
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   324
  chaining the current facts.  Note that @{command "hence"} is also
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   325
  equivalent to ``@{command "from"}~@{text this}~@{command "have"}''.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   326
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   327
  \item [@{command "thus"}] abbreviates ``@{command "then"}~@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   328
  "show"}''.  Note that @{command "thus"} is also equivalent to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   329
  ``@{command "from"}~@{text this}~@{command "show"}''.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   330
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   331
  \item [@{command "print_statement"}~@{text a}] prints facts from the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   332
  current theory or proof context in long statement form, according to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   333
  the syntax for @{command "lemma"} given above.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   334
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   335
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   336
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   337
  Any goal statement causes some term abbreviations (such as
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   338
  @{variable_ref "?thesis"}) to be bound automatically, see also
26922
c795d4b706b1 removed obsolete case rule_context;
wenzelm
parents: 26901
diff changeset
   339
  \secref{sec:term-abbrev}.
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   340
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   341
  The optional case names of @{element_ref "obtains"} have a twofold
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   342
  meaning: (1) during the of this claim they refer to the the local
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   343
  context introductions, (2) the resulting rule is annotated
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   344
  accordingly to support symbolic case splits when used with the
27116
wenzelm
parents: 27040
diff changeset
   345
  @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   346
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   347
  \medskip
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   348
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   349
  \begin{warn}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   350
    Isabelle/Isar suffers theory-level goal statements to contain
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   351
    \emph{unbound schematic variables}, although this does not conform
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   352
    to the aim of human-readable proof documents!  The main problem
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   353
    with schematic goals is that the actual outcome is usually hard to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   354
    predict, depending on the behavior of the proof methods applied
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   355
    during the course of reasoning.  Note that most semi-automated
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   356
    methods heavily depend on several kinds of implicit rule
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   357
    declarations within the current theory context.  As this would
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   358
    also result in non-compositional checking of sub-proofs,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   359
    \emph{local goals} are not allowed to be schematic at all.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   360
    Nevertheless, schematic goals do have their use in Prolog-style
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   361
    interactive synthesis of proven results, usually by stepwise
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   362
    refinement via emulation of traditional Isabelle tactic scripts
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   363
    (see also \secref{sec:tactic-commands}).  In any case, users
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   364
    should know what they are doing.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   365
  \end{warn}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   366
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   367
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   368
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   369
section {* Initial and terminal proof steps \label{sec:proof-steps} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   370
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   371
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   372
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   373
    @{command_def "proof"} & : & \isartrans{proof(prove)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   374
    @{command_def "qed"} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   375
    @{command_def "by"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   376
    @{command_def ".."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   377
    @{command_def "."} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   378
    @{command_def "sorry"} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   379
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   380
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   381
  Arbitrary goal refinement via tactics is considered harmful.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   382
  Structured proof composition in Isar admits proof methods to be
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   383
  invoked in two places only.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   384
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   385
  \begin{enumerate}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   386
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   387
  \item An \emph{initial} refinement step @{command_ref
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   388
  "proof"}~@{text "m\<^sub>1"} reduces a newly stated goal to a number
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   389
  of sub-goals that are to be solved later.  Facts are passed to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   390
  @{text "m\<^sub>1"} for forward chaining, if so indicated by @{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   391
  "proof(chain)"} mode.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   392
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   393
  \item A \emph{terminal} conclusion step @{command_ref "qed"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   394
  "m\<^sub>2"} is intended to solve remaining goals.  No facts are
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   395
  passed to @{text "m\<^sub>2"}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   396
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   397
  \end{enumerate}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   398
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   399
  The only other (proper) way to affect pending goals in a proof body
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   400
  is by @{command_ref "show"}, which involves an explicit statement of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   401
  what is to be solved eventually.  Thus we avoid the fundamental
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   402
  problem of unstructured tactic scripts that consist of numerous
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   403
  consecutive goal transformations, with invisible effects.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   404
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   405
  \medskip As a general rule of thumb for good proof style, initial
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   406
  proof methods should either solve the goal completely, or constitute
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   407
  some well-understood reduction to new sub-goals.  Arbitrary
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   408
  automatic proof tools that are prone leave a large number of badly
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   409
  structured sub-goals are no help in continuing the proof document in
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   410
  an intelligible manner.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   411
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   412
  Unless given explicitly by the user, the default initial method is
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   413
  ``@{method_ref rule}'', which applies a single standard elimination
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   414
  or introduction rule according to the topmost symbol involved.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   415
  There is no separate default terminal method.  Any remaining goals
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   416
  are always solved by assumption in the very last step.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   417
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   418
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   419
    'proof' method?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   420
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   421
    'qed' method?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   422
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   423
    'by' method method?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   424
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   425
    ('.' | '..' | 'sorry')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   426
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   427
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   428
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   429
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   430
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   431
  \item [@{command "proof"}~@{text "m\<^sub>1"}] refines the goal by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   432
  proof method @{text "m\<^sub>1"}; facts for forward chaining are
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   433
  passed if so indicated by @{text "proof(chain)"} mode.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   434
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   435
  \item [@{command "qed"}~@{text "m\<^sub>2"}] refines any remaining
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   436
  goals by proof method @{text "m\<^sub>2"} and concludes the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   437
  sub-proof by assumption.  If the goal had been @{text "show"} (or
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   438
  @{text "thus"}), some pending sub-goal is solved as well by the rule
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   439
  resulting from the result \emph{exported} into the enclosing goal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   440
  context.  Thus @{text "qed"} may fail for two reasons: either @{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   441
  "m\<^sub>2"} fails, or the resulting rule does not fit to any
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   442
  pending goal\footnote{This includes any additional ``strong''
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   443
  assumptions as introduced by @{command "assume"}.} of the enclosing
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   444
  context.  Debugging such a situation might involve temporarily
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   445
  changing @{command "show"} into @{command "have"}, or weakening the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   446
  local context by replacing occurrences of @{command "assume"} by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   447
  @{command "presume"}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   448
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   449
  \item [@{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}] is a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   450
  \emph{terminal proof}\index{proof!terminal}; it abbreviates
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   451
  @{command "proof"}~@{text "m\<^sub>1"}~@{text "qed"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   452
  "m\<^sub>2"}, but with backtracking across both methods.  Debugging
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   453
  an unsuccessful @{command "by"}~@{text "m\<^sub>1 m\<^sub>2"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   454
  command can be done by expanding its definition; in many cases
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   455
  @{command "proof"}~@{text "m\<^sub>1"} (or even @{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   456
  "apply"}~@{text "m\<^sub>1"}) is already sufficient to see the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   457
  problem.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   458
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   459
  \item [``@{command ".."}''] is a \emph{default
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   460
  proof}\index{proof!default}; it abbreviates @{command "by"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   461
  "rule"}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   462
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   463
  \item [``@{command "."}''] is a \emph{trivial
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   464
  proof}\index{proof!trivial}; it abbreviates @{command "by"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   465
  "this"}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   466
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   467
  \item [@{command "sorry"}] is a \emph{fake proof}\index{proof!fake}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   468
  pretending to solve the pending claim without further ado.  This
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   469
  only works in interactive development, or if the @{ML
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   470
  quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   471
  proofs are not the real thing.  Internally, each theorem container
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   472
  is tainted by an oracle invocation, which is indicated as ``@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   473
  "[!]"}'' in the printed result.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   474
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   475
  The most important application of @{command "sorry"} is to support
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   476
  experimentation and top-down proof development.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   477
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   478
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   479
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   480
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   481
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   482
section {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   483
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   484
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   485
  The following proof methods and attributes refer to basic logical
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   486
  operations of Isar.  Further methods and attributes are provided by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   487
  several generic and object-logic specific tools and packages (see
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   488
  \chref{ch:gen-tools} and \chref{ch:hol}).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   489
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   490
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   491
    @{method_def "-"} & : & \isarmeth \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   492
    @{method_def "fact"} & : & \isarmeth \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   493
    @{method_def "assumption"} & : & \isarmeth \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   494
    @{method_def "this"} & : & \isarmeth \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   495
    @{method_def "rule"} & : & \isarmeth \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   496
    @{method_def "iprover"} & : & \isarmeth \\[0.5ex]
26901
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   497
    @{attribute_def (Pure) "intro"} & : & \isaratt \\
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   498
    @{attribute_def (Pure) "elim"} & : & \isaratt \\
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   499
    @{attribute_def (Pure) "dest"} & : & \isaratt \\
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   500
    @{attribute_def "rule"} & : & \isaratt \\[0.5ex]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   501
    @{attribute_def "OF"} & : & \isaratt \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   502
    @{attribute_def "of"} & : & \isaratt \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   503
    @{attribute_def "where"} & : & \isaratt \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   504
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   505
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   506
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   507
    'fact' thmrefs?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   508
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   509
    'rule' thmrefs?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   510
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   511
    'iprover' ('!' ?) (rulemod *)
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   512
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   513
    rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   514
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   515
    ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   516
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   517
    'rule' 'del'
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   518
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   519
    'OF' thmrefs
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   520
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   521
    'of' insts ('concl' ':' insts)?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   522
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   523
    'where' ((name | var | typefree | typevar) '=' (type | term) * 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   524
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   525
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   526
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   527
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   528
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   529
  \item [``@{method "-"}'' (minus)] does nothing but insert the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   530
  forward chaining facts as premises into the goal.  Note that command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   531
  @{command_ref "proof"} without any method actually performs a single
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   532
  reduction step using the @{method_ref rule} method; thus a plain
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   533
  \emph{do-nothing} proof step would be ``@{command "proof"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   534
  "-"}'' rather than @{command "proof"} alone.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   535
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   536
  \item [@{method "fact"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] composes
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   537
  some fact from @{text "a\<^sub>1, \<dots>, a\<^sub>n"} (or implicitly from
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   538
  the current proof context) modulo unification of schematic type and
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   539
  term variables.  The rule structure is not taken into account, i.e.\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   540
  meta-level implication is considered atomic.  This is the same
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   541
  principle underlying literal facts (cf.\ \secref{sec:syn-att}):
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   542
  ``@{command "have"}~@{text "\<phi>"}~@{command "by"}~@{text fact}'' is
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   543
  equivalent to ``@{command "note"}~@{verbatim "`"}@{text \<phi>}@{verbatim
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   544
  "`"}'' provided that @{text "\<turnstile> \<phi>"} is an instance of some known
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   545
  @{text "\<turnstile> \<phi>"} in the proof context.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   546
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   547
  \item [@{method assumption}] solves some goal by a single assumption
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   548
  step.  All given facts are guaranteed to participate in the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   549
  refinement; this means there may be only 0 or 1 in the first place.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   550
  Recall that @{command "qed"} (\secref{sec:proof-steps}) already
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   551
  concludes any remaining sub-goals by assumption, so structured
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   552
  proofs usually need not quote the @{method assumption} method at
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   553
  all.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   554
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   555
  \item [@{method this}] applies all of the current facts directly as
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   556
  rules.  Recall that ``@{command "."}'' (dot) abbreviates ``@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   557
  "by"}~@{text this}''.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   558
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   559
  \item [@{method rule}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   560
  rule given as argument in backward manner; facts are used to reduce
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   561
  the rule before applying it to the goal.  Thus @{method rule}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   562
  without facts is plain introduction, while with facts it becomes
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   563
  elimination.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   564
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   565
  When no arguments are given, the @{method rule} method tries to pick
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   566
  appropriate rules automatically, as declared in the current context
26901
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   567
  using the @{attribute (Pure) intro}, @{attribute (Pure) elim},
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   568
  @{attribute (Pure) dest} attributes (see below).  This is the
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   569
  default behavior of @{command "proof"} and ``@{command ".."}'' 
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   570
  (double-dot) steps (see \secref{sec:proof-steps}).
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   571
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   572
  \item [@{method iprover}] performs intuitionistic proof search,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   573
  depending on specifically declared rules from the context, or given
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   574
  as explicit arguments.  Chained facts are inserted into the goal
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   575
  before commencing proof search; ``@{method iprover}@{text "!"}'' 
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   576
  means to include the current @{fact prems} as well.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   577
  
26901
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   578
  Rules need to be classified as @{attribute (Pure) intro},
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   579
  @{attribute (Pure) elim}, or @{attribute (Pure) dest}; here the
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   580
  ``@{text "!"}'' indicator refers to ``safe'' rules, which may be
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   581
  applied aggressively (without considering back-tracking later).
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   582
  Rules declared with ``@{text "?"}'' are ignored in proof search (the
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   583
  single-step @{method rule} method still observes these).  An
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   584
  explicit weight annotation may be given as well; otherwise the
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   585
  number of rule premises will be taken into account here.
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   586
  
26901
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   587
  \item [@{attribute (Pure) intro}, @{attribute (Pure) elim}, and
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   588
  @{attribute (Pure) dest}] declare introduction, elimination, and
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   589
  destruct rules, to be used with the @{method rule} and @{method
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   590
  iprover} methods.  Note that the latter will ignore rules declared
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   591
  with ``@{text "?"}'', while ``@{text "!"}''  are used most
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   592
  aggressively.
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   593
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   594
  The classical reasoner (see \secref{sec:classical}) introduces its
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   595
  own variants of these attributes; use qualified names to access the
26901
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   596
  present versions of Isabelle/Pure, i.e.\ @{attribute (Pure)
d1694ef6e7a7 fixed some Isar element markups;
wenzelm
parents: 26894
diff changeset
   597
  "Pure.intro"}.
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   598
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   599
  \item [@{attribute rule}~@{text del}] undeclares introduction,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   600
  elimination, or destruct rules.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   601
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   602
  \item [@{attribute OF}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] applies some
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   603
  theorem to all of the given rules @{text "a\<^sub>1, \<dots>, a\<^sub>n"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   604
  (in parallel).  This corresponds to the @{ML "op MRS"} operation in
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   605
  ML, but note the reversed order.  Positions may be effectively
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   606
  skipped by including ``@{text _}'' (underscore) as argument.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   607
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   608
  \item [@{attribute of}~@{text "t\<^sub>1 \<dots> t\<^sub>n"}] performs
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   609
  positional instantiation of term variables.  The terms @{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   610
  "t\<^sub>1, \<dots>, t\<^sub>n"} are substituted for any schematic
26888
9942cd184c48 remobed obsolete keyword concl;
wenzelm
parents: 26870
diff changeset
   611
  variables occurring in a theorem from left to right; ``@{text _}''
9942cd184c48 remobed obsolete keyword concl;
wenzelm
parents: 26870
diff changeset
   612
  (underscore) indicates to skip a position.  Arguments following a
9942cd184c48 remobed obsolete keyword concl;
wenzelm
parents: 26870
diff changeset
   613
  ``@{text "concl:"}'' specification refer to positions of the
9942cd184c48 remobed obsolete keyword concl;
wenzelm
parents: 26870
diff changeset
   614
  conclusion of a rule.
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   615
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   616
  \item [@{attribute "where"}~@{text "x\<^sub>1 = t\<^sub>1 \<AND> \<dots>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   617
  x\<^sub>n = t\<^sub>n"}] performs named instantiation of schematic
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   618
  type and term variables occurring in a theorem.  Schematic variables
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   619
  have to be specified on the left-hand side (e.g.\ @{text "?x1.3"}).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   620
  The question mark may be omitted if the variable name is a plain
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   621
  identifier without index.  As type instantiations are inferred from
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   622
  term instantiations, explicit type instantiations are seldom
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   623
  necessary.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   624
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   625
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   626
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   627
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   628
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   629
section {* Term abbreviations \label{sec:term-abbrev} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   630
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   631
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   632
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   633
    @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   634
    @{keyword_def "is"} & : & syntax \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   635
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   636
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   637
  Abbreviations may be either bound by explicit @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   638
  "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   639
  goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   640
  p\<^sub>n)"}''.  In both cases, higher-order matching is invoked to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   641
  bind extra-logical term variables, which may be either named
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   642
  schematic variables of the form @{text ?x}, or nameless dummies
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   643
  ``@{variable _}'' (underscore). Note that in the @{command "let"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   644
  form the patterns occur on the left-hand side, while the @{keyword
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   645
  "is"} patterns are in postfix position.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   646
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   647
  Polymorphism of term bindings is handled in Hindley-Milner style,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   648
  similar to ML.  Type variables referring to local assumptions or
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   649
  open goal statements are \emph{fixed}, while those of finished
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   650
  results or bound by @{command "let"} may occur in \emph{arbitrary}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   651
  instances later.  Even though actual polymorphism should be rarely
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   652
  used in practice, this mechanism is essential to achieve proper
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   653
  incremental type-inference, as the user proceeds to build up the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   654
  Isar proof text from left to right.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   655
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   656
  \medskip Term abbreviations are quite different from local
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   657
  definitions as introduced via @{command "def"} (see
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   658
  \secref{sec:proof-context}).  The latter are visible within the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   659
  logic as actual equations, while abbreviations disappear during the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   660
  input process just after type checking.  Also note that @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   661
  "def"} does not support polymorphism.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   662
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   663
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   664
    'let' ((term + 'and') '=' term + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   665
    ;  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   666
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   667
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   668
  The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   669
  or \railnonterm{proppat} (see \secref{sec:term-decls}).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   670
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   671
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   672
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   673
  \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   674
  p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   675
  "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   676
  against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   677
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   678
  \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   679
  "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   680
  preceding statement.  Also note that @{keyword "is"} is not a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   681
  separate command, but part of others (such as @{command "assume"},
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   682
  @{command "have"} etc.).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   683
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   684
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   685
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   686
  Some \emph{implicit} term abbreviations\index{term abbreviations}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   687
  for goals and facts are available as well.  For any open goal,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   688
  @{variable_ref thesis} refers to its object-level statement,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   689
  abstracted over any meta-level parameters (if present).  Likewise,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   690
  @{variable_ref this} is bound for fact statements resulting from
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   691
  assumptions or finished goals.  In case @{variable this} refers to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   692
  an object-logic statement that is an application @{text "f t"}, then
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   693
  @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   694
  (three dots).  The canonical application of this convenience are
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   695
  calculational proofs (see \secref{sec:calculation}).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   696
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   697
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   698
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   699
section {* Block structure *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   700
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   701
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   702
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   703
    @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   704
    @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   705
    @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   706
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   707
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   708
  While Isar is inherently block-structured, opening and closing
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   709
  blocks is mostly handled rather casually, with little explicit
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   710
  user-intervention.  Any local goal statement automatically opens
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   711
  \emph{two} internal blocks, which are closed again when concluding
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   712
  the sub-proof (by @{command "qed"} etc.).  Sections of different
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   713
  context within a sub-proof may be switched via @{command "next"},
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   714
  which is just a single block-close followed by block-open again.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   715
  The effect of @{command "next"} is to reset the local proof context;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   716
  there is no goal focus involved here!
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   717
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   718
  For slightly more advanced applications, there are explicit block
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   719
  parentheses as well.  These typically achieve a stronger forward
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   720
  style of reasoning.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   721
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   722
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   723
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   724
  \item [@{command "next"}] switches to a fresh block within a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   725
  sub-proof, resetting the local context to the initial one.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   726
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   727
  \item [@{command "{"} and @{command "}"}] explicitly open and close
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   728
  blocks.  Any current facts pass through ``@{command "{"}''
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   729
  unchanged, while ``@{command "}"}'' causes any result to be
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   730
  \emph{exported} into the enclosing context.  Thus fixed variables
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   731
  are generalized, assumptions discharged, and local definitions
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   732
  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   733
  of @{command "assume"} and @{command "presume"} in this mode of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   734
  forward reasoning --- in contrast to plain backward reasoning with
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   735
  the result exported at @{command "show"} time.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   736
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   737
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   738
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   739
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   740
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   741
section {* Emulating tactic scripts \label{sec:tactic-commands} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   742
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   743
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   744
  The Isar provides separate commands to accommodate tactic-style
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   745
  proof scripts within the same system.  While being outside the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   746
  orthodox Isar proof language, these might come in handy for
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   747
  interactive exploration and debugging, or even actual tactical proof
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   748
  within new-style theories (to benefit from document preparation, for
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   749
  example).  See also \secref{sec:tactics} for actual tactics, that
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   750
  have been encapsulated as proof methods.  Proper proof methods may
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   751
  be used in scripts, too.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   752
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   753
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   754
    @{command_def "apply"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   755
    @{command_def "apply_end"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   756
    @{command_def "done"}@{text "\<^sup>*"} & : & \isartrans{proof(prove)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   757
    @{command_def "defer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   758
    @{command_def "prefer"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   759
    @{command_def "back"}@{text "\<^sup>*"} & : & \isartrans{proof}{proof} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   760
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   761
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   762
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   763
    ( 'apply' | 'apply\_end' ) method
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   764
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   765
    'defer' nat?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   766
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   767
    'prefer' nat
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   768
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   769
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   770
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   771
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   772
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   773
  \item [@{command "apply"}~@{text m}] applies proof method @{text m}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   774
  in initial position, but unlike @{command "proof"} it retains
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   775
  ``@{text "proof(prove)"}'' mode.  Thus consecutive method
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   776
  applications may be given just as in tactic scripts.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   777
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   778
  Facts are passed to @{text m} as indicated by the goal's
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   779
  forward-chain mode, and are \emph{consumed} afterwards.  Thus any
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   780
  further @{command "apply"} command would always work in a purely
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   781
  backward manner.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   782
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   783
  \item [@{command "apply_end"}~@{text "m"}] applies proof method
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   784
  @{text m} as if in terminal position.  Basically, this simulates a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   785
  multi-step tactic script for @{command "qed"}, but may be given
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   786
  anywhere within the proof body.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   787
  
26894
1120f6cc10b0 proper checking of various Isar elements;
wenzelm
parents: 26888
diff changeset
   788
  No facts are passed to @{text m} here.  Furthermore, the static
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   789
  context is that of the enclosing goal (as for actual @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   790
  "qed"}).  Thus the proof method may not refer to any assumptions
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   791
  introduced in the current body, for example.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   792
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   793
  \item [@{command "done"}] completes a proof script, provided that
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   794
  the current goal state is solved completely.  Note that actual
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   795
  structured proof commands (e.g.\ ``@{command "."}'' or @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   796
  "sorry"}) may be used to conclude proof scripts as well.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   797
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   798
  \item [@{command "defer"}~@{text n} and @{command "prefer"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   799
  n}] shuffle the list of pending goals: @{command "defer"} puts off
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   800
  sub-goal @{text n} to the end of the list (@{text "n = 1"} by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   801
  default), while @{command "prefer"} brings sub-goal @{text n} to the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   802
  front.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   803
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   804
  \item [@{command "back"}] does back-tracking over the result
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   805
  sequence of the latest proof command.  Basically, any proof command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   806
  may return multiple results.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   807
  
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   808
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   809
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   810
  Any proper Isar proof method may be used with tactic script commands
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   811
  such as @{command "apply"}.  A few additional emulations of actual
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   812
  tactics are provided as well; these would be never used in actual
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   813
  structured proofs, of course.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   814
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   815
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   816
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   817
section {* Omitting proofs *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   818
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   819
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   820
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   821
    @{command_def "oops"} & : & \isartrans{proof}{theory} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   822
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   823
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   824
  The @{command "oops"} command discontinues the current proof
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   825
  attempt, while considering the partial proof text as properly
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   826
  processed.  This is conceptually quite different from ``faking''
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   827
  actual proofs via @{command_ref "sorry"} (see
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   828
  \secref{sec:proof-steps}): @{command "oops"} does not observe the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   829
  proof structure at all, but goes back right to the theory level.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   830
  Furthermore, @{command "oops"} does not produce any result theorem
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   831
  --- there is no intended claim to be able to complete the proof
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   832
  anyhow.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   833
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   834
  A typical application of @{command "oops"} is to explain Isar proofs
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   835
  \emph{within} the system itself, in conjunction with the document
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   836
  preparation tools of Isabelle described in \cite{isabelle-sys}.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   837
  Thus partial or even wrong proof attempts can be discussed in a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   838
  logically sound manner.  Note that the Isabelle {\LaTeX} macros can
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   839
  be easily adapted to print something like ``@{text "\<dots>"}'' instead of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   840
  the keyword ``@{command "oops"}''.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   841
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   842
  \medskip The @{command "oops"} command is undo-able, unlike
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   843
  @{command_ref "kill"} (see \secref{sec:history}).  The effect is to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   844
  get back to the theory just before the opening of the proof.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   845
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   846
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   847
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   848
section {* Generalized elimination \label{sec:obtain} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   849
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   850
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   851
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   852
    @{command_def "obtain"} & : & \isartrans{proof(state)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   853
    @{command_def "guess"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(prove)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   854
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   855
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   856
  Generalized elimination means that additional elements with certain
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   857
  properties may be introduced in the current context, by virtue of a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   858
  locally proven ``soundness statement''.  Technically speaking, the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   859
  @{command "obtain"} language element is like a declaration of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   860
  @{command "fix"} and @{command "assume"} (see also see
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   861
  \secref{sec:proof-context}), together with a soundness proof of its
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   862
  additional claim.  According to the nature of existential reasoning,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   863
  assumptions get eliminated from any result exported from the context
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   864
  later, provided that the corresponding parameters do \emph{not}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   865
  occur in the conclusion.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   866
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   867
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   868
    'obtain' parname? (vars + 'and') 'where' (props + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   869
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   870
    'guess' (vars + 'and')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   871
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   872
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   873
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   874
  The derived Isar command @{command "obtain"} is defined as follows
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   875
  (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   876
  facts indicated for forward chaining).
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   877
  \begin{matharray}{l}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   878
    @{text "\<langle>using b\<^sub>1 \<dots> b\<^sub>k\<rangle>"}~~@{command "obtain"}~@{text "x\<^sub>1 \<dots> x\<^sub>m \<WHERE> a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n  \<langle>proof\<rangle> \<equiv>"} \\[1ex]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   879
    \quad @{command "have"}~@{text "\<And>thesis. (\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   880
    \quad @{command "proof"}~@{text succeed} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   881
    \qquad @{command "fix"}~@{text thesis} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   882
    \qquad @{command "assume"}~@{text "that [Pure.intro?]: \<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> thesis"} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   883
    \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   884
    \quad\qquad @{command "apply"}~@{text -} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   885
    \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k  \<langle>proof\<rangle>"} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   886
    \quad @{command "qed"} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   887
    \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   888
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   889
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   890
  Typically, the soundness proof is relatively straight-forward, often
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   891
  just by canonical automated tools such as ``@{command "by"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   892
  simp}'' or ``@{command "by"}~@{text blast}''.  Accordingly, the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   893
  ``@{text that}'' reduction above is declared as simplification and
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   894
  introduction rule.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   895
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   896
  In a sense, @{command "obtain"} represents at the level of Isar
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   897
  proofs what would be meta-logical existential quantifiers and
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   898
  conjunctions.  This concept has a broad range of useful
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   899
  applications, ranging from plain elimination (or introduction) of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   900
  object-level existential and conjunctions, to elimination over
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   901
  results of symbolic evaluation of recursive definitions, for
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   902
  example.  Also note that @{command "obtain"} without parameters acts
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   903
  much like @{command "have"}, where the result is treated as a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   904
  genuine assumption.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   905
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   906
  An alternative name to be used instead of ``@{text that}'' above may
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   907
  be given in parentheses.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   908
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   909
  \medskip The improper variant @{command "guess"} is similar to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   910
  @{command "obtain"}, but derives the obtained statement from the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   911
  course of reasoning!  The proof starts with a fixed goal @{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   912
  thesis}.  The subsequent proof may refine this to anything of the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   913
  form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   914
  \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals.  The
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   915
  final goal state is then used as reduction rule for the obtain
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   916
  scheme described above.  Obtained parameters @{text "x\<^sub>1, \<dots>,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   917
  x\<^sub>m"} are marked as internal by default, which prevents the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   918
  proof context from being polluted by ad-hoc variables.  The variable
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   919
  names and type constraints given as arguments for @{command "guess"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   920
  specify a prefix of obtained parameters explicitly in the text.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   921
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   922
  It is important to note that the facts introduced by @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   923
  "obtain"} and @{command "guess"} may not be polymorphic: any
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   924
  type-variables occurring here are fixed in the present context!
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   925
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   926
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   927
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   928
section {* Calculational reasoning \label{sec:calculation} *}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   929
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   930
text {*
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   931
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   932
    @{command_def "also"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   933
    @{command_def "finally"} & : & \isartrans{proof(state)}{proof(chain)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   934
    @{command_def "moreover"} & : & \isartrans{proof(state)}{proof(state)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   935
    @{command_def "ultimately"} & : & \isartrans{proof(state)}{proof(chain)} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   936
    @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   937
    @{attribute trans} & : & \isaratt \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   938
    @{attribute sym} & : & \isaratt \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   939
    @{attribute symmetric} & : & \isaratt \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   940
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   941
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   942
  Calculational proof is forward reasoning with implicit application
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   943
  of transitivity rules (such those of @{text "="}, @{text "\<le>"},
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   944
  @{text "<"}).  Isabelle/Isar maintains an auxiliary fact register
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   945
  @{fact_ref calculation} for accumulating results obtained by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   946
  transitivity composed with the current result.  Command @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   947
  "also"} updates @{fact calculation} involving @{fact this}, while
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   948
  @{command "finally"} exhibits the final @{fact calculation} by
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   949
  forward chaining towards the next goal statement.  Both commands
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   950
  require valid current facts, i.e.\ may occur only after commands
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   951
  that produce theorems such as @{command "assume"}, @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   952
  "note"}, or some finished proof of @{command "have"}, @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   953
  "show"} etc.  The @{command "moreover"} and @{command "ultimately"}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   954
  commands are similar to @{command "also"} and @{command "finally"},
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   955
  but only collect further results in @{fact calculation} without
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   956
  applying any rules yet.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   957
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   958
  Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   959
  its canonical application with calculational proofs.  It refers to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   960
  the argument of the preceding statement. (The argument of a curried
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   961
  infix expression happens to be its right-hand side.)
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   962
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   963
  Isabelle/Isar calculations are implicitly subject to block structure
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   964
  in the sense that new threads of calculational reasoning are
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   965
  commenced for any new block (as opened by a local goal, for
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   966
  example).  This means that, apart from being able to nest
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   967
  calculations, there is no separate \emph{begin-calculation} command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   968
  required.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   969
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   970
  \medskip The Isar calculation proof commands may be defined as
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   971
  follows:\footnote{We suppress internal bookkeeping such as proper
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   972
  handling of block-structure.}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   973
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   974
  \begin{matharray}{rcl}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   975
    @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   976
    @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   977
    @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   978
    @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   979
    @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   980
  \end{matharray}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   981
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   982
  \begin{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   983
    ('also' | 'finally') ('(' thmrefs ')')?
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   984
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   985
    'trans' (() | 'add' | 'del')
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   986
    ;
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   987
  \end{rail}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   988
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   989
  \begin{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   990
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   991
  \item [@{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   992
  maintains the auxiliary @{fact calculation} register as follows.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   993
  The first occurrence of @{command "also"} in some calculational
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   994
  thread initializes @{fact calculation} by @{fact this}. Any
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   995
  subsequent @{command "also"} on the same level of block-structure
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   996
  updates @{fact calculation} by some transitivity rule applied to
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   997
  @{fact calculation} and @{fact this} (in that order).  Transitivity
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   998
  rules are picked from the current context, unless alternative rules
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
   999
  are given as explicit arguments.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1000
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1001
  \item [@{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1002
  maintaining @{fact calculation} in the same way as @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1003
  "also"}, and concludes the current calculational thread.  The final
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1004
  result is exhibited as fact for forward chaining towards the next
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1005
  goal. Basically, @{command "finally"} just abbreviates @{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1006
  "also"}~@{command "from"}~@{fact calculation}.  Typical idioms for
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1007
  concluding calculational proofs are ``@{command "finally"}~@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1008
  "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1009
  "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1010
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1011
  \item [@{command "moreover"} and @{command "ultimately"}] are
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1012
  analogous to @{command "also"} and @{command "finally"}, but collect
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1013
  results only, without applying rules.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1014
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1015
  \item [@{command "print_trans_rules"}] prints the list of
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1016
  transitivity rules (for calculational commands @{command "also"} and
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1017
  @{command "finally"}) and symmetry rules (for the @{attribute
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1018
  symmetric} operation and single step elimination patters) of the
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1019
  current context.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1020
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1021
  \item [@{attribute trans}] declares theorems as transitivity rules.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1022
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1023
  \item [@{attribute sym}] declares symmetry rules, as well as
26894
1120f6cc10b0 proper checking of various Isar elements;
wenzelm
parents: 26888
diff changeset
  1024
  @{attribute "Pure.elim"}@{text "?"} rules.
26870
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1025
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1026
  \item [@{attribute symmetric}] resolves a theorem with some rule
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1027
  declared as @{attribute sym} in the current context.  For example,
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1028
  ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1029
  swapped fact derived from that assumption.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1030
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1031
  In structured proof texts it is often more appropriate to use an
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1032
  explicit single-step elimination proof, such as ``@{command
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1033
  "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1034
  "y = x"}~@{command ".."}''.
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1035
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1036
  \end{descr}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1037
*}
94bedbb34b92 misc reorganization;
wenzelm
parents: 26869
diff changeset
  1038
27040
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1039
section {* Proof by cases and induction \label{sec:cases-induct} *}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1040
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1041
subsection {* Rule contexts *}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1042
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1043
text {*
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1044
  \begin{matharray}{rcl}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1045
    @{command_def "case"} & : & \isartrans{proof(state)}{proof(state)} \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1046
    @{command_def "print_cases"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1047
    @{attribute_def case_names} & : & \isaratt \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1048
    @{attribute_def case_conclusion} & : & \isaratt \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1049
    @{attribute_def params} & : & \isaratt \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1050
    @{attribute_def consumes} & : & \isaratt \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1051
  \end{matharray}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1052
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1053
  The puristic way to build up Isar proof contexts is by explicit
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1054
  language elements like @{command "fix"}, @{command "assume"},
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1055
  @{command "let"} (see \secref{sec:proof-context}).  This is adequate
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1056
  for plain natural deduction, but easily becomes unwieldy in concrete
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1057
  verification tasks, which typically involve big induction rules with
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1058
  several cases.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1059
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1060
  The @{command "case"} command provides a shorthand to refer to a
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1061
  local context symbolically: certain proof methods provide an
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1062
  environment of named ``cases'' of the form @{text "c: x\<^sub>1, \<dots>,
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1063
  x\<^sub>m, \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>n"}; the effect of ``@{command
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1064
  "case"}~@{text c}'' is then equivalent to ``@{command "fix"}~@{text
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1065
  "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1066
  \<phi>\<^sub>n"}''.  Term bindings may be covered as well, notably
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1067
  @{variable ?case} for the main conclusion.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1068
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1069
  By default, the ``terminology'' @{text "x\<^sub>1, \<dots>, x\<^sub>m"} of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1070
  a case value is marked as hidden, i.e.\ there is no way to refer to
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1071
  such parameters in the subsequent proof text.  After all, original
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1072
  rule parameters stem from somewhere outside of the current proof
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1073
  text.  By using the explicit form ``@{command "case"}~@{text "(c
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1074
  y\<^sub>1 \<dots> y\<^sub>m)"}'' instead, the proof author is able to
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1075
  chose local names that fit nicely into the current context.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1076
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1077
  \medskip It is important to note that proper use of @{command
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1078
  "case"} does not provide means to peek at the current goal state,
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1079
  which is not directly observable in Isar!  Nonetheless, goal
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1080
  refinement commands do provide named cases @{text "goal\<^sub>i"}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1081
  for each subgoal @{text "i = 1, \<dots>, n"} of the resulting goal state.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1082
  Using this extra feature requires great care, because some bits of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1083
  the internal tactical machinery intrude the proof text.  In
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1084
  particular, parameter names stemming from the left-over of automated
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1085
  reasoning tools are usually quite unpredictable.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1086
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1087
  Under normal circumstances, the text of cases emerge from standard
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1088
  elimination or induction rules, which in turn are derived from
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1089
  previous theory specifications in a canonical way (say from
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1090
  @{command "inductive"} definitions).
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1091
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1092
  \medskip Proper cases are only available if both the proof method
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1093
  and the rules involved support this.  By using appropriate
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1094
  attributes, case names, conclusions, and parameters may be also
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1095
  declared by hand.  Thus variant versions of rules that have been
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1096
  derived manually become ready to use in advanced case analysis
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1097
  later.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1098
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1099
  \begin{rail}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1100
    'case' (caseref | '(' caseref ((name | underscore) +) ')')
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1101
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1102
    caseref: nameref attributes?
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1103
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1104
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1105
    'case\_names' (name +)
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1106
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1107
    'case\_conclusion' name (name *)
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1108
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1109
    'params' ((name *) + 'and')
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1110
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1111
    'consumes' nat?
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1112
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1113
  \end{rail}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1114
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1115
  \begin{descr}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1116
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1117
  \item [@{command "case"}~@{text "(c x\<^sub>1 \<dots> x\<^sub>m)"}]
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1118
  invokes a named local context @{text "c: x\<^sub>1, \<dots>, x\<^sub>m,
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1119
  \<phi>\<^sub>1, \<dots>, \<phi>\<^sub>m"}, as provided by an appropriate
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1120
  proof method (such as @{method_ref cases} and @{method_ref induct}).
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1121
  The command ``@{command "case"}~@{text "(c x\<^sub>1 \<dots>
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1122
  x\<^sub>m)"}'' abbreviates ``@{command "fix"}~@{text "x\<^sub>1 \<dots>
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1123
  x\<^sub>m"}~@{command "assume"}~@{text "c: \<phi>\<^sub>1 \<dots>
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1124
  \<phi>\<^sub>n"}''.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1125
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1126
  \item [@{command "print_cases"}] prints all local contexts of the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1127
  current state, using Isar proof language notation.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1128
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1129
  \item [@{attribute case_names}~@{text "c\<^sub>1 \<dots> c\<^sub>k"}]
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1130
  declares names for the local contexts of premises of a theorem;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1131
  @{text "c\<^sub>1, \<dots>, c\<^sub>k"} refers to the \emph{suffix} of the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1132
  list of premises.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1133
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1134
  \item [@{attribute case_conclusion}~@{text "c d\<^sub>1 \<dots>
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1135
  d\<^sub>k"}] declares names for the conclusions of a named premise
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1136
  @{text c}; here @{text "d\<^sub>1, \<dots>, d\<^sub>k"} refers to the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1137
  prefix of arguments of a logical formula built by nesting a binary
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1138
  connective (e.g.\ @{text "\<or>"}).
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1139
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1140
  Note that proof methods such as @{method induct} and @{method
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1141
  coinduct} already provide a default name for the conclusion as a
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1142
  whole.  The need to name subformulas only arises with cases that
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1143
  split into several sub-cases, as in common co-induction rules.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1144
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1145
  \item [@{attribute params}~@{text "p\<^sub>1 \<dots> p\<^sub>m \<AND> \<dots>
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1146
  q\<^sub>1 \<dots> q\<^sub>n"}] renames the innermost parameters of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1147
  premises @{text "1, \<dots>, n"} of some theorem.  An empty list of names
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1148
  may be given to skip positions, leaving the present parameters
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1149
  unchanged.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1150
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1151
  Note that the default usage of case rules does \emph{not} directly
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1152
  expose parameters to the proof context.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1153
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1154
  \item [@{attribute consumes}~@{text n}] declares the number of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1155
  ``major premises'' of a rule, i.e.\ the number of facts to be
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1156
  consumed when it is applied by an appropriate proof method.  The
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1157
  default value of @{attribute consumes} is @{text "n = 1"}, which is
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1158
  appropriate for the usual kind of cases and induction rules for
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1159
  inductive sets (cf.\ \secref{sec:hol-inductive}).  Rules without any
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1160
  @{attribute consumes} declaration given are treated as if
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1161
  @{attribute consumes}~@{text 0} had been specified.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1162
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1163
  Note that explicit @{attribute consumes} declarations are only
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1164
  rarely needed; this is already taken care of automatically by the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1165
  higher-level @{attribute cases}, @{attribute induct}, and
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1166
  @{attribute coinduct} declarations.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1167
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1168
  \end{descr}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1169
*}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1170
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1171
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1172
subsection {* Proof methods *}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1173
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1174
text {*
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1175
  \begin{matharray}{rcl}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1176
    @{method_def cases} & : & \isarmeth \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1177
    @{method_def induct} & : & \isarmeth \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1178
    @{method_def coinduct} & : & \isarmeth \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1179
  \end{matharray}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1180
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1181
  The @{method cases}, @{method induct}, and @{method coinduct}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1182
  methods provide a uniform interface to common proof techniques over
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1183
  datatypes, inductive predicates (or sets), recursive functions etc.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1184
  The corresponding rules may be specified and instantiated in a
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1185
  casual manner.  Furthermore, these methods provide named local
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1186
  contexts that may be invoked via the @{command "case"} proof command
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1187
  within the subsequent proof text.  This accommodates compact proof
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1188
  texts even when reasoning about large specifications.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1189
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1190
  The @{method induct} method also provides some additional
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1191
  infrastructure in order to be applicable to structure statements
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1192
  (either using explicit meta-level connectives, or including facts
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1193
  and parameters separately).  This avoids cumbersome encoding of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1194
  ``strengthened'' inductive statements within the object-logic.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1195
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1196
  \begin{rail}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1197
    'cases' (insts * 'and') rule?
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1198
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1199
    'induct' (definsts * 'and') \\ arbitrary? taking? rule?
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1200
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1201
    'coinduct' insts taking rule?
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1202
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1203
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1204
    rule: ('type' | 'pred' | 'set') ':' (nameref +) | 'rule' ':' (thmref +)
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1205
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1206
    definst: name ('==' | equiv) term | inst
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1207
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1208
    definsts: ( definst *)
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1209
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1210
    arbitrary: 'arbitrary' ':' ((term *) 'and' +)
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1211
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1212
    taking: 'taking' ':' insts
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1213
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1214
  \end{rail}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1215
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1216
  \begin{descr}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1217
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1218
  \item [@{method cases}~@{text "insts R"}] applies method @{method
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1219
  rule} with an appropriate case distinction theorem, instantiated to
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1220
  the subjects @{text insts}.  Symbolic case names are bound according
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1221
  to the rule's local contexts.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1222
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1223
  The rule is determined as follows, according to the facts and
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1224
  arguments passed to the @{method cases} method:
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1225
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1226
  \medskip
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1227
  \begin{tabular}{llll}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1228
    facts           &                 & arguments   & rule \\\hline
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1229
                    & @{method cases} &             & classical case split \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1230
                    & @{method cases} & @{text t}   & datatype exhaustion (type of @{text t}) \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1231
    @{text "\<turnstile> A t"} & @{method cases} & @{text "\<dots>"} & inductive predicate/set elimination (of @{text A}) \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1232
    @{text "\<dots>"}     & @{method cases} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1233
  \end{tabular}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1234
  \medskip
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1235
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1236
  Several instantiations may be given, referring to the \emph{suffix}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1237
  of premises of the case rule; within each premise, the \emph{prefix}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1238
  of variables is instantiated.  In most situations, only a single
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1239
  term needs to be specified; this refers to the first variable of the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1240
  last premise (it is usually the same for all cases).
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1241
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1242
  \item [@{method induct}~@{text "insts R"}] is analogous to the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1243
  @{method cases} method, but refers to induction rules, which are
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1244
  determined as follows:
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1245
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1246
  \medskip
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1247
  \begin{tabular}{llll}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1248
    facts           &                  & arguments            & rule \\\hline
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1249
                    & @{method induct} & @{text "P x"}        & datatype induction (type of @{text x}) \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1250
    @{text "\<turnstile> A x"} & @{method induct} & @{text "\<dots>"}          & predicate/set induction (of @{text A}) \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1251
    @{text "\<dots>"}     & @{method induct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1252
  \end{tabular}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1253
  \medskip
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1254
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1255
  Several instantiations may be given, each referring to some part of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1256
  a mutual inductive definition or datatype --- only related partial
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1257
  induction rules may be used together, though.  Any of the lists of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1258
  terms @{text "P, x, \<dots>"} refers to the \emph{suffix} of variables
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1259
  present in the induction rule.  This enables the writer to specify
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1260
  only induction variables, or both predicates and variables, for
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1261
  example.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1262
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1263
  Instantiations may be definitional: equations @{text "x \<equiv> t"}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1264
  introduce local definitions, which are inserted into the claim and
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1265
  discharged after applying the induction rule.  Equalities reappear
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1266
  in the inductive cases, but have been transformed according to the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1267
  induction principle being involved here.  In order to achieve
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1268
  practically useful induction hypotheses, some variables occurring in
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1269
  @{text t} need to be fixed (see below).
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1270
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1271
  The optional ``@{text "arbitrary: x\<^sub>1 \<dots> x\<^sub>m"}''
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1272
  specification generalizes variables @{text "x\<^sub>1, \<dots>,
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1273
  x\<^sub>m"} of the original goal before applying induction.  Thus
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1274
  induction hypotheses may become sufficiently general to get the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1275
  proof through.  Together with definitional instantiations, one may
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1276
  effectively perform induction over expressions of a certain
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1277
  structure.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1278
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1279
  The optional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1280
  specification provides additional instantiations of a prefix of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1281
  pending variables in the rule.  Such schematic induction rules
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1282
  rarely occur in practice, though.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1283
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1284
  \item [@{method coinduct}~@{text "inst R"}] is analogous to the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1285
  @{method induct} method, but refers to coinduction rules, which are
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1286
  determined as follows:
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1287
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1288
  \medskip
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1289
  \begin{tabular}{llll}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1290
    goal          &                    & arguments & rule \\\hline
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1291
                  & @{method coinduct} & @{text x} & type coinduction (type of @{text x}) \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1292
    @{text "A x"} & @{method coinduct} & @{text "\<dots>"} & predicate/set coinduction (of @{text A}) \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1293
    @{text "\<dots>"}   & @{method coinduct} & @{text "\<dots> rule: R"} & explicit rule @{text R} \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1294
  \end{tabular}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1295
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1296
  Coinduction is the dual of induction.  Induction essentially
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1297
  eliminates @{text "A x"} towards a generic result @{text "P x"},
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1298
  while coinduction introduces @{text "A x"} starting with @{text "B
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1299
  x"}, for a suitable ``bisimulation'' @{text B}.  The cases of a
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1300
  coinduct rule are typically named after the predicates or sets being
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1301
  covered, while the conclusions consist of several alternatives being
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1302
  named after the individual destructor patterns.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1303
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1304
  The given instantiation refers to the \emph{suffix} of variables
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1305
  occurring in the rule's major premise, or conclusion if unavailable.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1306
  An additional ``@{text "taking: t\<^sub>1 \<dots> t\<^sub>n"}''
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1307
  specification may be required in order to specify the bisimulation
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1308
  to be used in the coinduction step.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1309
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1310
  \end{descr}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1311
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1312
  Above methods produce named local contexts, as determined by the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1313
  instantiated rule as given in the text.  Beyond that, the @{method
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1314
  induct} and @{method coinduct} methods guess further instantiations
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1315
  from the goal specification itself.  Any persisting unresolved
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1316
  schematic variables of the resulting rule will render the the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1317
  corresponding case invalid.  The term binding @{variable ?case} for
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1318
  the conclusion will be provided with each case, provided that term
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1319
  is fully specified.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1320
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1321
  The @{command "print_cases"} command prints all named cases present
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1322
  in the current proof state.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1323
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1324
  \medskip Despite the additional infrastructure, both @{method cases}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1325
  and @{method coinduct} merely apply a certain rule, after
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1326
  instantiation, while conforming due to the usual way of monotonic
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1327
  natural deduction: the context of a structured statement @{text
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1328
  "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<dots>"}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1329
  reappears unchanged after the case split.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1330
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1331
  The @{method induct} method is fundamentally different in this
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1332
  respect: the meta-level structure is passed through the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1333
  ``recursive'' course involved in the induction.  Thus the original
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1334
  statement is basically replaced by separate copies, corresponding to
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1335
  the induction hypotheses and conclusion; the original goal context
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1336
  is no longer available.  Thus local assumptions, fixed parameters
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1337
  and definitions effectively participate in the inductive rephrasing
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1338
  of the original statement.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1339
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1340
  In induction proofs, local assumptions introduced by cases are split
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1341
  into two different kinds: @{text hyps} stemming from the rule and
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1342
  @{text prems} from the goal statement.  This is reflected in the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1343
  extracted cases accordingly, so invoking ``@{command "case"}~@{text
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1344
  c}'' will provide separate facts @{text c.hyps} and @{text c.prems},
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1345
  as well as fact @{text c} to hold the all-inclusive list.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1346
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1347
  \medskip Facts presented to either method are consumed according to
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1348
  the number of ``major premises'' of the rule involved, which is
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1349
  usually 0 for plain cases and induction rules of datatypes etc.\ and
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1350
  1 for rules of inductive predicates or sets and the like.  The
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1351
  remaining facts are inserted into the goal verbatim before the
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1352
  actual @{text cases}, @{text induct}, or @{text coinduct} rule is
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1353
  applied.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1354
*}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1355
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1356
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1357
subsection {* Declaring rules *}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1358
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1359
text {*
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1360
  \begin{matharray}{rcl}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1361
    @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1362
    @{attribute_def cases} & : & \isaratt \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1363
    @{attribute_def induct} & : & \isaratt \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1364
    @{attribute_def coinduct} & : & \isaratt \\
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1365
  \end{matharray}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1366
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1367
  \begin{rail}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1368
    'cases' spec
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1369
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1370
    'induct' spec
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1371
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1372
    'coinduct' spec
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1373
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1374
27141
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1375
    spec: (('type' | 'pred' | 'set') ':' nameref) | 'del'
27040
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1376
    ;
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1377
  \end{rail}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1378
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1379
  \begin{descr}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1380
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1381
  \item [@{command "print_induct_rules"}] prints cases and induct
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1382
  rules for predicates (or sets) and types of the current context.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1383
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1384
  \item [@{attribute cases}, @{attribute induct}, and @{attribute
27141
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1385
  coinduct}] (as attributes) declare rules for reasoning about
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1386
  (co)inductive predicates (or sets) and types, using the
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1387
  corresponding methods of the same name.  Certain definitional
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1388
  packages of object-logics usually declare emerging cases and
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1389
  induction rules as expected, so users rarely need to intervene.
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1390
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1391
  Rules may be deleted via the @{text "del"} specification, which
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1392
  covers all of the @{text "type"}/@{text "pred"}/@{text "set"}
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1393
  sub-categories simultaneously.  For example, @{attribute
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1394
  cases}~@{text del} removes any @{attribute cases} rules declared for
9bfcdb1905e1 * Attributes cases, induct, coinduct support del option.
wenzelm
parents: 27116
diff changeset
  1395
  some type, predicate, or set.
27040
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1396
  
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1397
  Manual rule declarations usually refer to the @{attribute
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1398
  case_names} and @{attribute params} attributes to adjust names of
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1399
  cases and parameters of a rule; the @{attribute consumes}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1400
  declaration is taken care of automatically: @{attribute
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1401
  consumes}~@{text 0} is specified for ``type'' rules and @{attribute
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1402
  consumes}~@{text 1} for ``predicate'' / ``set'' rules.
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1403
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1404
  \end{descr}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1405
*}
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 26922
diff changeset
  1406
26869
3bc332135aa7 added chapters for "Specifications" and "Proofs";
wenzelm
parents:
diff changeset
  1407
end