moved section "Proof method expressions" to proof chapter;
authorwenzelm
Thu Nov 13 21:37:18 2008 +0100 (2008-11-13)
changeset 287546f2e67a3dfaa
parent 28753 b5926a48c943
child 28755 d5c1b7d67ea9
moved section "Proof method expressions" to proof chapter;
minor rearrangement of proof sections;
doc-src/IsarRef/Thy/Generic.thy
doc-src/IsarRef/Thy/Outer_Syntax.thy
doc-src/IsarRef/Thy/Proof.thy
     1.1 --- a/doc-src/IsarRef/Thy/Generic.thy	Thu Nov 13 21:34:55 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Generic.thy	Thu Nov 13 21:37:18 2008 +0100
     1.3 @@ -100,11 +100,11 @@
     1.4  
     1.5    \item [@{method succeed}] yields a single (unchanged) result; it is
     1.6    the identity of the ``@{text ","}'' method combinator (cf.\
     1.7 -  \secref{sec:syn-meth}).
     1.8 +  \secref{sec:proof-meth}).
     1.9  
    1.10    \item [@{method fail}] yields an empty result sequence; it is the
    1.11    identity of the ``@{text "|"}'' method combinator (cf.\
    1.12 -  \secref{sec:syn-meth}).
    1.13 +  \secref{sec:proof-meth}).
    1.14  
    1.15    \end{descr}
    1.16  
     2.1 --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:34:55 2008 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy	Thu Nov 13 21:37:18 2008 +0100
     2.3 @@ -262,6 +262,51 @@
     2.4  *}
     2.5  
     2.6  
     2.7 +subsection {* Term patterns and declarations \label{sec:term-decls} *}
     2.8 +
     2.9 +text {*
    2.10 +  Wherever explicit propositions (or term fragments) occur in a proof
    2.11 +  text, casual binding of schematic term variables may be given
    2.12 +  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
    2.13 +  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
    2.14 +
    2.15 +  \indexouternonterm{termpat}\indexouternonterm{proppat}
    2.16 +  \begin{rail}
    2.17 +    termpat: '(' ('is' term +) ')'
    2.18 +    ;
    2.19 +    proppat: '(' ('is' prop +) ')'
    2.20 +    ;
    2.21 +  \end{rail}
    2.22 +
    2.23 +  \medskip Declarations of local variables @{text "x :: \<tau>"} and
    2.24 +  logical propositions @{text "a : \<phi>"} represent different views on
    2.25 +  the same principle of introducing a local scope.  In practice, one
    2.26 +  may usually omit the typing of \railnonterm{vars} (due to
    2.27 +  type-inference), and the naming of propositions (due to implicit
    2.28 +  references of current facts).  In any case, Isar proof elements
    2.29 +  usually admit to introduce multiple such items simultaneously.
    2.30 +
    2.31 +  \indexouternonterm{vars}\indexouternonterm{props}
    2.32 +  \begin{rail}
    2.33 +    vars: (name+) ('::' type)?
    2.34 +    ;
    2.35 +    props: thmdecl? (prop proppat? +)
    2.36 +    ;
    2.37 +  \end{rail}
    2.38 +
    2.39 +  The treatment of multiple declarations corresponds to the
    2.40 +  complementary focus of \railnonterm{vars} versus
    2.41 +  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
    2.42 +  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
    2.43 +  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
    2.44 +  Isar language elements that refer to \railnonterm{vars} or
    2.45 +  \railnonterm{props} typically admit separate typings or namings via
    2.46 +  another level of iteration, with explicit @{keyword_ref "and"}
    2.47 +  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
    2.48 +  \secref{sec:proof-context}.
    2.49 +*}
    2.50 +
    2.51 +
    2.52  subsection {* Mixfix annotations *}
    2.53  
    2.54  text {*
    2.55 @@ -314,7 +359,7 @@
    2.56    pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
    2.57    @{text "m > n"} works by attaching concrete notation only to the
    2.58    innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
    2.59 -  instead.  If a term has fewer argument than specified in the mixfix
    2.60 +  instead.  If a term has fewer arguments than specified in the mixfix
    2.61    template, the concrete syntax is ignored.
    2.62  
    2.63    \medskip A mixfix template may also contain additional directives
    2.64 @@ -366,69 +411,22 @@
    2.65    For example, the template @{text "(_ +/ _)"} specifies an infix
    2.66    operator.  There are two argument positions; the delimiter @{text
    2.67    "+"} is preceded by a space and followed by a space or line break;
    2.68 -  the entire phrase is a pretty printing block.  
    2.69 +  the entire phrase is a pretty printing block.
    2.70  
    2.71    The general idea of pretty printing with blocks and breaks is also
    2.72    described in \cite{paulson-ml2}.
    2.73  *}
    2.74  
    2.75  
    2.76 -subsection {* Proof methods \label{sec:syn-meth} *}
    2.77 -
    2.78 -text {*
    2.79 -  Proof methods are either basic ones, or expressions composed of
    2.80 -  methods via ``@{verbatim ","}'' (sequential composition),
    2.81 -  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' 
    2.82 -  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
    2.83 -  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
    2.84 -  sub-goals, with default @{text "n = 1"}).  In practice, proof
    2.85 -  methods are usually just a comma separated list of
    2.86 -  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
    2.87 -  parentheses may be dropped for single method specifications (with no
    2.88 -  arguments).
    2.89 -
    2.90 -  \indexouternonterm{method}
    2.91 -  \begin{rail}
    2.92 -    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
    2.93 -    ;
    2.94 -    methods: (nameref args | method) + (',' | '|')
    2.95 -    ;
    2.96 -  \end{rail}
    2.97 -
    2.98 -  Proper Isar proof methods do \emph{not} admit arbitrary goal
    2.99 -  addressing, but refer either to the first sub-goal or all sub-goals
   2.100 -  uniformly.  The goal restriction operator ``@{text "[n]"}''
   2.101 -  evaluates a method expression within a sandbox consisting of the
   2.102 -  first @{text n} sub-goals (which need to exist).  For example, the
   2.103 -  method ``@{text "simp_all[3]"}'' simplifies the first three
   2.104 -  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
   2.105 -  new goals that emerge from applying rule @{text "foo"} to the
   2.106 -  originally first one.
   2.107 -
   2.108 -  Improper methods, notably tactic emulations, offer a separate
   2.109 -  low-level goal addressing scheme as explicit argument to the
   2.110 -  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
   2.111 -  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
   2.112 -  "n"}.
   2.113 -
   2.114 -  \indexouternonterm{goalspec}
   2.115 -  \begin{rail}
   2.116 -    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
   2.117 -    ;
   2.118 -  \end{rail}
   2.119 -*}
   2.120 -
   2.121 -
   2.122  subsection {* Attributes and theorems \label{sec:syn-att} *}
   2.123  
   2.124 -text {*
   2.125 -  Attributes (and proof methods, see \secref{sec:syn-meth}) have their
   2.126 -  own ``semi-inner'' syntax, in the sense that input conforming to
   2.127 -  \railnonterm{args} below is parsed by the attribute a second time.
   2.128 -  The attribute argument specifications may be any sequence of atomic
   2.129 -  entities (identifiers, strings etc.), or properly bracketed argument
   2.130 -  lists.  Below \railqtok{atom} refers to any atomic entity, including
   2.131 -  any \railtok{keyword} conforming to \railtok{symident}.
   2.132 +text {* Attributes have their own ``semi-inner'' syntax, in the sense
   2.133 +  that input conforming to \railnonterm{args} below is parsed by the
   2.134 +  attribute a second time.  The attribute argument specifications may
   2.135 +  be any sequence of atomic entities (identifiers, strings etc.), or
   2.136 +  properly bracketed argument lists.  Below \railqtok{atom} refers to
   2.137 +  any atomic entity, including any \railtok{keyword} conforming to
   2.138 +  \railtok{symident}.
   2.139  
   2.140    \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
   2.141    \begin{rail}
   2.142 @@ -459,7 +457,7 @@
   2.143  
   2.144    \item literal fact propositions using @{syntax_ref altstring} syntax
   2.145    @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
   2.146 -  @{method_ref fact} in \secref{sec:pure-meth-att}).
   2.147 +  @{method_ref fact}).
   2.148  
   2.149    \end{enumerate}
   2.150  
   2.151 @@ -498,49 +496,4 @@
   2.152    \end{rail}
   2.153  *}
   2.154  
   2.155 -
   2.156 -subsection {* Term patterns and declarations \label{sec:term-decls} *}
   2.157 -
   2.158 -text {*
   2.159 -  Wherever explicit propositions (or term fragments) occur in a proof
   2.160 -  text, casual binding of schematic term variables may be given
   2.161 -  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
   2.162 -  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
   2.163 -
   2.164 -  \indexouternonterm{termpat}\indexouternonterm{proppat}
   2.165 -  \begin{rail}
   2.166 -    termpat: '(' ('is' term +) ')'
   2.167 -    ;
   2.168 -    proppat: '(' ('is' prop +) ')'
   2.169 -    ;
   2.170 -  \end{rail}
   2.171 -
   2.172 -  \medskip Declarations of local variables @{text "x :: \<tau>"} and
   2.173 -  logical propositions @{text "a : \<phi>"} represent different views on
   2.174 -  the same principle of introducing a local scope.  In practice, one
   2.175 -  may usually omit the typing of \railnonterm{vars} (due to
   2.176 -  type-inference), and the naming of propositions (due to implicit
   2.177 -  references of current facts).  In any case, Isar proof elements
   2.178 -  usually admit to introduce multiple such items simultaneously.
   2.179 -
   2.180 -  \indexouternonterm{vars}\indexouternonterm{props}
   2.181 -  \begin{rail}
   2.182 -    vars: (name+) ('::' type)?
   2.183 -    ;
   2.184 -    props: thmdecl? (prop proppat? +)
   2.185 -    ;
   2.186 -  \end{rail}
   2.187 -
   2.188 -  The treatment of multiple declarations corresponds to the
   2.189 -  complementary focus of \railnonterm{vars} versus
   2.190 -  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
   2.191 -  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
   2.192 -  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
   2.193 -  Isar language elements that refer to \railnonterm{vars} or
   2.194 -  \railnonterm{props} typically admit separate typings or namings via
   2.195 -  another level of iteration, with explicit @{keyword_ref "and"}
   2.196 -  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
   2.197 -  \secref{sec:proof-context}.
   2.198 -*}
   2.199 -
   2.200  end
     3.1 --- a/doc-src/IsarRef/Thy/Proof.thy	Thu Nov 13 21:34:55 2008 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/Proof.thy	Thu Nov 13 21:37:18 2008 +0100
     3.3 @@ -42,7 +42,9 @@
     3.4  *}
     3.5  
     3.6  
     3.7 -section {* Context elements \label{sec:proof-context} *}
     3.8 +section {* Statements *}
     3.9 +
    3.10 +subsection {* Context elements \label{sec:proof-context} *}
    3.11  
    3.12  text {*
    3.13    \begin{matharray}{rcl}
    3.14 @@ -127,7 +129,77 @@
    3.15  *}
    3.16  
    3.17  
    3.18 -section {* Facts and forward chaining *}
    3.19 +subsection {* Term abbreviations \label{sec:term-abbrev} *}
    3.20 +
    3.21 +text {*
    3.22 +  \begin{matharray}{rcl}
    3.23 +    @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
    3.24 +    @{keyword_def "is"} & : & syntax \\
    3.25 +  \end{matharray}
    3.26 +
    3.27 +  Abbreviations may be either bound by explicit @{command
    3.28 +  "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
    3.29 +  goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
    3.30 +  p\<^sub>n)"}''.  In both cases, higher-order matching is invoked to
    3.31 +  bind extra-logical term variables, which may be either named
    3.32 +  schematic variables of the form @{text ?x}, or nameless dummies
    3.33 +  ``@{variable _}'' (underscore). Note that in the @{command "let"}
    3.34 +  form the patterns occur on the left-hand side, while the @{keyword
    3.35 +  "is"} patterns are in postfix position.
    3.36 +
    3.37 +  Polymorphism of term bindings is handled in Hindley-Milner style,
    3.38 +  similar to ML.  Type variables referring to local assumptions or
    3.39 +  open goal statements are \emph{fixed}, while those of finished
    3.40 +  results or bound by @{command "let"} may occur in \emph{arbitrary}
    3.41 +  instances later.  Even though actual polymorphism should be rarely
    3.42 +  used in practice, this mechanism is essential to achieve proper
    3.43 +  incremental type-inference, as the user proceeds to build up the
    3.44 +  Isar proof text from left to right.
    3.45 +
    3.46 +  \medskip Term abbreviations are quite different from local
    3.47 +  definitions as introduced via @{command "def"} (see
    3.48 +  \secref{sec:proof-context}).  The latter are visible within the
    3.49 +  logic as actual equations, while abbreviations disappear during the
    3.50 +  input process just after type checking.  Also note that @{command
    3.51 +  "def"} does not support polymorphism.
    3.52 +
    3.53 +  \begin{rail}
    3.54 +    'let' ((term + 'and') '=' term + 'and')
    3.55 +    ;  
    3.56 +  \end{rail}
    3.57 +
    3.58 +  The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
    3.59 +  or \railnonterm{proppat} (see \secref{sec:term-decls}).
    3.60 +
    3.61 +  \begin{descr}
    3.62 +
    3.63 +  \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
    3.64 +  p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
    3.65 +  "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
    3.66 +  against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
    3.67 +
    3.68 +  \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
    3.69 +  "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
    3.70 +  preceding statement.  Also note that @{keyword "is"} is not a
    3.71 +  separate command, but part of others (such as @{command "assume"},
    3.72 +  @{command "have"} etc.).
    3.73 +
    3.74 +  \end{descr}
    3.75 +
    3.76 +  Some \emph{implicit} term abbreviations\index{term abbreviations}
    3.77 +  for goals and facts are available as well.  For any open goal,
    3.78 +  @{variable_ref thesis} refers to its object-level statement,
    3.79 +  abstracted over any meta-level parameters (if present).  Likewise,
    3.80 +  @{variable_ref this} is bound for fact statements resulting from
    3.81 +  assumptions or finished goals.  In case @{variable this} refers to
    3.82 +  an object-logic statement that is an application @{text "f t"}, then
    3.83 +  @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
    3.84 +  (three dots).  The canonical application of this convenience are
    3.85 +  calculational proofs (see \secref{sec:calculation}).
    3.86 +*}
    3.87 +
    3.88 +
    3.89 +subsection {* Facts and forward chaining *}
    3.90  
    3.91  text {*
    3.92    \begin{matharray}{rcl}
    3.93 @@ -215,7 +287,7 @@
    3.94  *}
    3.95  
    3.96  
    3.97 -section {* Goal statements \label{sec:goals} *}
    3.98 +subsection {* Goals \label{sec:goals} *}
    3.99  
   3.100  text {*
   3.101    \begin{matharray}{rcl}
   3.102 @@ -366,7 +438,55 @@
   3.103  *}
   3.104  
   3.105  
   3.106 -section {* Initial and terminal proof steps \label{sec:proof-steps} *}
   3.107 +section {* Refinement steps *}
   3.108 +
   3.109 +subsection {* Proof method expressions \label{sec:proof-meth} *}
   3.110 +
   3.111 +text {*
   3.112 +  Proof methods are either basic ones, or expressions composed of
   3.113 +  methods via ``@{verbatim ","}'' (sequential composition),
   3.114 +  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' 
   3.115 +  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
   3.116 +  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
   3.117 +  sub-goals, with default @{text "n = 1"}).  In practice, proof
   3.118 +  methods are usually just a comma separated list of
   3.119 +  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
   3.120 +  parentheses may be dropped for single method specifications (with no
   3.121 +  arguments).
   3.122 +
   3.123 +  \indexouternonterm{method}
   3.124 +  \begin{rail}
   3.125 +    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
   3.126 +    ;
   3.127 +    methods: (nameref args | method) + (',' | '|')
   3.128 +    ;
   3.129 +  \end{rail}
   3.130 +
   3.131 +  Proper Isar proof methods do \emph{not} admit arbitrary goal
   3.132 +  addressing, but refer either to the first sub-goal or all sub-goals
   3.133 +  uniformly.  The goal restriction operator ``@{text "[n]"}''
   3.134 +  evaluates a method expression within a sandbox consisting of the
   3.135 +  first @{text n} sub-goals (which need to exist).  For example, the
   3.136 +  method ``@{text "simp_all[3]"}'' simplifies the first three
   3.137 +  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
   3.138 +  new goals that emerge from applying rule @{text "foo"} to the
   3.139 +  originally first one.
   3.140 +
   3.141 +  Improper methods, notably tactic emulations, offer a separate
   3.142 +  low-level goal addressing scheme as explicit argument to the
   3.143 +  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
   3.144 +  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
   3.145 +  "n"}.
   3.146 +
   3.147 +  \indexouternonterm{goalspec}
   3.148 +  \begin{rail}
   3.149 +    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
   3.150 +    ;
   3.151 +  \end{rail}
   3.152 +*}
   3.153 +
   3.154 +
   3.155 +subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
   3.156  
   3.157  text {*
   3.158    \begin{matharray}{rcl}
   3.159 @@ -479,7 +599,7 @@
   3.160  *}
   3.161  
   3.162  
   3.163 -section {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
   3.164 +subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
   3.165  
   3.166  text {*
   3.167    The following proof methods and attributes refer to basic logical
   3.168 @@ -626,119 +746,7 @@
   3.169  *}
   3.170  
   3.171  
   3.172 -section {* Term abbreviations \label{sec:term-abbrev} *}
   3.173 -
   3.174 -text {*
   3.175 -  \begin{matharray}{rcl}
   3.176 -    @{command_def "let"} & : & \isartrans{proof(state)}{proof(state)} \\
   3.177 -    @{keyword_def "is"} & : & syntax \\
   3.178 -  \end{matharray}
   3.179 -
   3.180 -  Abbreviations may be either bound by explicit @{command
   3.181 -  "let"}~@{text "p \<equiv> t"} statements, or by annotating assumptions or
   3.182 -  goal statements with a list of patterns ``@{text "(\<IS> p\<^sub>1 \<dots>
   3.183 -  p\<^sub>n)"}''.  In both cases, higher-order matching is invoked to
   3.184 -  bind extra-logical term variables, which may be either named
   3.185 -  schematic variables of the form @{text ?x}, or nameless dummies
   3.186 -  ``@{variable _}'' (underscore). Note that in the @{command "let"}
   3.187 -  form the patterns occur on the left-hand side, while the @{keyword
   3.188 -  "is"} patterns are in postfix position.
   3.189 -
   3.190 -  Polymorphism of term bindings is handled in Hindley-Milner style,
   3.191 -  similar to ML.  Type variables referring to local assumptions or
   3.192 -  open goal statements are \emph{fixed}, while those of finished
   3.193 -  results or bound by @{command "let"} may occur in \emph{arbitrary}
   3.194 -  instances later.  Even though actual polymorphism should be rarely
   3.195 -  used in practice, this mechanism is essential to achieve proper
   3.196 -  incremental type-inference, as the user proceeds to build up the
   3.197 -  Isar proof text from left to right.
   3.198 -
   3.199 -  \medskip Term abbreviations are quite different from local
   3.200 -  definitions as introduced via @{command "def"} (see
   3.201 -  \secref{sec:proof-context}).  The latter are visible within the
   3.202 -  logic as actual equations, while abbreviations disappear during the
   3.203 -  input process just after type checking.  Also note that @{command
   3.204 -  "def"} does not support polymorphism.
   3.205 -
   3.206 -  \begin{rail}
   3.207 -    'let' ((term + 'and') '=' term + 'and')
   3.208 -    ;  
   3.209 -  \end{rail}
   3.210 -
   3.211 -  The syntax of @{keyword "is"} patterns follows \railnonterm{termpat}
   3.212 -  or \railnonterm{proppat} (see \secref{sec:term-decls}).
   3.213 -
   3.214 -  \begin{descr}
   3.215 -
   3.216 -  \item [@{command "let"}~@{text "p\<^sub>1 = t\<^sub>1 \<AND> \<dots>
   3.217 -  p\<^sub>n = t\<^sub>n"}] binds any text variables in patterns @{text
   3.218 -  "p\<^sub>1, \<dots>, p\<^sub>n"} by simultaneous higher-order matching
   3.219 -  against terms @{text "t\<^sub>1, \<dots>, t\<^sub>n"}.
   3.220 -
   3.221 -  \item [@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}] resembles @{command
   3.222 -  "let"}, but matches @{text "p\<^sub>1, \<dots>, p\<^sub>n"} against the
   3.223 -  preceding statement.  Also note that @{keyword "is"} is not a
   3.224 -  separate command, but part of others (such as @{command "assume"},
   3.225 -  @{command "have"} etc.).
   3.226 -
   3.227 -  \end{descr}
   3.228 -
   3.229 -  Some \emph{implicit} term abbreviations\index{term abbreviations}
   3.230 -  for goals and facts are available as well.  For any open goal,
   3.231 -  @{variable_ref thesis} refers to its object-level statement,
   3.232 -  abstracted over any meta-level parameters (if present).  Likewise,
   3.233 -  @{variable_ref this} is bound for fact statements resulting from
   3.234 -  assumptions or finished goals.  In case @{variable this} refers to
   3.235 -  an object-logic statement that is an application @{text "f t"}, then
   3.236 -  @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
   3.237 -  (three dots).  The canonical application of this convenience are
   3.238 -  calculational proofs (see \secref{sec:calculation}).
   3.239 -*}
   3.240 -
   3.241 -
   3.242 -section {* Block structure *}
   3.243 -
   3.244 -text {*
   3.245 -  \begin{matharray}{rcl}
   3.246 -    @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
   3.247 -    @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
   3.248 -    @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
   3.249 -  \end{matharray}
   3.250 -
   3.251 -  While Isar is inherently block-structured, opening and closing
   3.252 -  blocks is mostly handled rather casually, with little explicit
   3.253 -  user-intervention.  Any local goal statement automatically opens
   3.254 -  \emph{two} internal blocks, which are closed again when concluding
   3.255 -  the sub-proof (by @{command "qed"} etc.).  Sections of different
   3.256 -  context within a sub-proof may be switched via @{command "next"},
   3.257 -  which is just a single block-close followed by block-open again.
   3.258 -  The effect of @{command "next"} is to reset the local proof context;
   3.259 -  there is no goal focus involved here!
   3.260 -
   3.261 -  For slightly more advanced applications, there are explicit block
   3.262 -  parentheses as well.  These typically achieve a stronger forward
   3.263 -  style of reasoning.
   3.264 -
   3.265 -  \begin{descr}
   3.266 -
   3.267 -  \item [@{command "next"}] switches to a fresh block within a
   3.268 -  sub-proof, resetting the local context to the initial one.
   3.269 -
   3.270 -  \item [@{command "{"} and @{command "}"}] explicitly open and close
   3.271 -  blocks.  Any current facts pass through ``@{command "{"}''
   3.272 -  unchanged, while ``@{command "}"}'' causes any result to be
   3.273 -  \emph{exported} into the enclosing context.  Thus fixed variables
   3.274 -  are generalized, assumptions discharged, and local definitions
   3.275 -  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
   3.276 -  of @{command "assume"} and @{command "presume"} in this mode of
   3.277 -  forward reasoning --- in contrast to plain backward reasoning with
   3.278 -  the result exported at @{command "show"} time.
   3.279 -
   3.280 -  \end{descr}
   3.281 -*}
   3.282 -
   3.283 -
   3.284 -section {* Emulating tactic scripts \label{sec:tactic-commands} *}
   3.285 +subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
   3.286  
   3.287  text {*
   3.288    The Isar provides separate commands to accommodate tactic-style
   3.289 @@ -814,6 +822,48 @@
   3.290  *}
   3.291  
   3.292  
   3.293 +section {* Block structure *}
   3.294 +
   3.295 +text {*
   3.296 +  \begin{matharray}{rcl}
   3.297 +    @{command_def "next"} & : & \isartrans{proof(state)}{proof(state)} \\
   3.298 +    @{command_def "{"} & : & \isartrans{proof(state)}{proof(state)} \\
   3.299 +    @{command_def "}"} & : & \isartrans{proof(state)}{proof(state)} \\
   3.300 +  \end{matharray}
   3.301 +
   3.302 +  While Isar is inherently block-structured, opening and closing
   3.303 +  blocks is mostly handled rather casually, with little explicit
   3.304 +  user-intervention.  Any local goal statement automatically opens
   3.305 +  \emph{two} internal blocks, which are closed again when concluding
   3.306 +  the sub-proof (by @{command "qed"} etc.).  Sections of different
   3.307 +  context within a sub-proof may be switched via @{command "next"},
   3.308 +  which is just a single block-close followed by block-open again.
   3.309 +  The effect of @{command "next"} is to reset the local proof context;
   3.310 +  there is no goal focus involved here!
   3.311 +
   3.312 +  For slightly more advanced applications, there are explicit block
   3.313 +  parentheses as well.  These typically achieve a stronger forward
   3.314 +  style of reasoning.
   3.315 +
   3.316 +  \begin{descr}
   3.317 +
   3.318 +  \item [@{command "next"}] switches to a fresh block within a
   3.319 +  sub-proof, resetting the local context to the initial one.
   3.320 +
   3.321 +  \item [@{command "{"} and @{command "}"}] explicitly open and close
   3.322 +  blocks.  Any current facts pass through ``@{command "{"}''
   3.323 +  unchanged, while ``@{command "}"}'' causes any result to be
   3.324 +  \emph{exported} into the enclosing context.  Thus fixed variables
   3.325 +  are generalized, assumptions discharged, and local definitions
   3.326 +  unfolded (cf.\ \secref{sec:proof-context}).  There is no difference
   3.327 +  of @{command "assume"} and @{command "presume"} in this mode of
   3.328 +  forward reasoning --- in contrast to plain backward reasoning with
   3.329 +  the result exported at @{command "show"} time.
   3.330 +
   3.331 +  \end{descr}
   3.332 +*}
   3.333 +
   3.334 +
   3.335  section {* Omitting proofs *}
   3.336  
   3.337  text {*
   3.338 @@ -1036,6 +1086,7 @@
   3.339    \end{descr}
   3.340  *}
   3.341  
   3.342 +
   3.343  section {* Proof by cases and induction \label{sec:cases-induct} *}
   3.344  
   3.345  subsection {* Rule contexts *}