more on 'consider' and related concepts;
authorwenzelm
Sat Jun 13 22:42:23 2015 +0200 (2015-06-13)
changeset 604592761a2249c83
parent 60458 0d10ae17e3ee
child 60460 abee0de69a89
more on 'consider' and related concepts;
NEWS
src/Doc/Isar_Ref/Proof.thy
src/Doc/isar.sty
     1.1 --- a/NEWS	Sat Jun 13 20:07:54 2015 +0200
     1.2 +++ b/NEWS	Sat Jun 13 22:42:23 2015 +0200
     1.3 @@ -38,6 +38,11 @@
     1.4  * New command 'supply' supports fact definitions during goal refinement
     1.5  ('apply' scripts).
     1.6  
     1.7 +* New command 'consider' states rules for generalized elimination and
     1.8 +case splitting. This is like a toplevel statement "theorem obtains" used
     1.9 +within a proof body; or like a multi-branch 'obtain' without activation
    1.10 +of the local context elements yet.
    1.11 +
    1.12  * Proof method "cases" allows to specify the rule as first entry of
    1.13  chained facts.  This is particularly useful with 'consider':
    1.14  
     2.1 --- a/src/Doc/Isar_Ref/Proof.thy	Sat Jun 13 20:07:54 2015 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Proof.thy	Sat Jun 13 22:42:23 2015 +0200
     2.3 @@ -445,9 +445,12 @@
     2.4      statement: @{syntax thmdecl}? (@{syntax_ref "includes"}?) (@{syntax context_elem} *) \<newline>
     2.5        conclusion
     2.6      ;
     2.7 -    conclusion: @'shows' stmt | @'obtains' (@{syntax par_name}? obtain_case + '|')
     2.8 +    conclusion: @'shows' stmt | @'obtains' @{syntax obtain_clauses}
     2.9      ;
    2.10 -    obtain_case: (@{syntax vars} + @'and') @'where' (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
    2.11 +    @{syntax_def obtain_clauses}: (@{syntax par_name}? obtain_case + '|')
    2.12 +    ;
    2.13 +    @{syntax_def obtain_case}: (@{syntax vars} + @'and') @'where'
    2.14 +      (@{syntax thmdecl}? (@{syntax prop}+) + @'and')
    2.15    \<close>}
    2.16  
    2.17    \begin{description}
    2.18 @@ -521,11 +524,10 @@
    2.19    @{variable_ref "?thesis"}) to be bound automatically, see also
    2.20    \secref{sec:term-abbrev}.
    2.21  
    2.22 -  The optional case names of @{element_ref "obtains"} have a twofold
    2.23 -  meaning: (1) in the proof of this claim they refer to the local context
    2.24 -  introductions, (2) in the resulting rule they become annotations for
    2.25 -  symbolic case splits, e.g.\ for the @{method_ref cases} method
    2.26 -  (\secref{sec:cases-induct}).
    2.27 +  Structured goal statements involving @{keyword_ref "if"} define the
    2.28 +  special fact ``@{text that}'' to refer to these assumptions in the proof
    2.29 +  body. The user may provide separate names according to the syntax of the
    2.30 +  statement.
    2.31  \<close>
    2.32  
    2.33  
    2.34 @@ -851,15 +853,6 @@
    2.35  subsection \<open>Emulating tactic scripts \label{sec:tactic-commands}\<close>
    2.36  
    2.37  text \<open>
    2.38 -  The Isar provides separate commands to accommodate tactic-style
    2.39 -  proof scripts within the same system.  While being outside the
    2.40 -  orthodox Isar proof language, these might come in handy for
    2.41 -  interactive exploration and debugging, or even actual tactical proof
    2.42 -  within new-style theories (to benefit from document preparation, for
    2.43 -  example).  See also \secref{sec:tactics} for actual tactics, that
    2.44 -  have been encapsulated as proof methods.  Proper proof methods may
    2.45 -  be used in scripts, too.
    2.46 -
    2.47    \begin{matharray}{rcl}
    2.48      @{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    2.49      @{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
    2.50 @@ -870,6 +863,15 @@
    2.51      @{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
    2.52    \end{matharray}
    2.53  
    2.54 +  The Isar language provides separate commands to accommodate tactic-style
    2.55 +  proof scripts within the same system.  While being outside the
    2.56 +  orthodox Isar proof language, these might come in handy for
    2.57 +  interactive exploration and debugging, or even actual tactical proof
    2.58 +  within new-style theories (to benefit from document preparation, for
    2.59 +  example).  See also \secref{sec:tactics} for actual tactics, that
    2.60 +  have been encapsulated as proof methods.  Proper proof methods may
    2.61 +  be used in scripts, too.
    2.62 +
    2.63    @{rail \<open>
    2.64      @@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
    2.65      ;
    2.66 @@ -977,83 +979,125 @@
    2.67  (*<*)end(*>*)
    2.68  
    2.69  
    2.70 -section \<open>Generalized elimination \label{sec:obtain}\<close>
    2.71 +section \<open>Generalized elimination and case splitting \label{sec:obtain}\<close>
    2.72  
    2.73  text \<open>
    2.74    \begin{matharray}{rcl}
    2.75 +    @{command_def "consider"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
    2.76      @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
    2.77      @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
    2.78    \end{matharray}
    2.79  
    2.80 -  Generalized elimination means that additional elements with certain
    2.81 -  properties may be introduced in the current context, by virtue of a
    2.82 -  locally proven ``soundness statement''.  Technically speaking, the
    2.83 -  @{command "obtain"} language element is like a declaration of
    2.84 -  @{command "fix"} and @{command "assume"} (see also see
    2.85 -  \secref{sec:proof-context}), together with a soundness proof of its
    2.86 -  additional claim.  According to the nature of existential reasoning,
    2.87 -  assumptions get eliminated from any result exported from the context
    2.88 -  later, provided that the corresponding parameters do \emph{not}
    2.89 -  occur in the conclusion.
    2.90 +  Generalized elimination means that hypothetical parameters and premises
    2.91 +  may be introduced in the current context, potentially with a split into
    2.92 +  cases. This works by virtue of a locally proven rule that establishes the
    2.93 +  soundness of this temporary context extension. As representative examples,
    2.94 +  one may think of standard rules from Isabelle/HOL like this:
    2.95 +
    2.96 +  \medskip
    2.97 +  \begin{tabular}{ll}
    2.98 +  @{text "\<exists>x. B x \<Longrightarrow> (\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
    2.99 +  @{text "A \<and> B \<Longrightarrow> (A \<Longrightarrow> B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
   2.100 +  @{text "A \<or> B \<Longrightarrow> (A \<Longrightarrow> thesis) \<Longrightarrow> (B \<Longrightarrow> thesis) \<Longrightarrow> thesis"} \\
   2.101 +  \end{tabular}
   2.102 +  \medskip
   2.103 +
   2.104 +  In general, these particular rules and connectives need to get involved at
   2.105 +  all: this concept works directly in Isabelle/Pure via Isar commands
   2.106 +  defined below. In particular, the logic of elimination and case splitting
   2.107 +  is delegated to an Isar proof, which often involves automated tools.
   2.108  
   2.109    @{rail \<open>
   2.110 +    @@{command consider} @{syntax obtain_clauses}
   2.111 +    ;
   2.112      @@{command obtain} @{syntax par_name}? (@{syntax "fixes"} + @'and')
   2.113        @'where' (@{syntax props} + @'and')
   2.114      ;
   2.115 -    @@{command guess} (@{syntax vars} + @'and')
   2.116 +    @@{command guess} (@{syntax "fixes"} + @'and')
   2.117    \<close>}
   2.118  
   2.119 -  The derived Isar command @{command "obtain"} is defined as follows
   2.120 -  (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
   2.121 -  facts indicated for forward chaining).
   2.122 +  \begin{description}
   2.123 +
   2.124 +  \item @{command consider}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x
   2.125 +  | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> "} states a rule for case
   2.126 +  splitting into separate subgoals, such that each case involves new
   2.127 +  parameters and premises. After the proof is finished, the resulting rule
   2.128 +  may be used directly with the @{method cases} proof method
   2.129 +  (\secref{sec:cases-induct}), in order to perform actual case-splitting of
   2.130 +  the proof text via @{command case} and @{command next} as usual.
   2.131 +
   2.132 +  Optional names in round parentheses refer to case names: in the proof of
   2.133 +  the rule this is a fact name, in the resulting rule it is used as
   2.134 +  annotation with the @{attribute_ref case_names} attribute.
   2.135 +
   2.136 +  \medskip Formally, the command @{command consider} is defined as derived
   2.137 +  Isar language element as follows:
   2.138 +
   2.139    \begin{matharray}{l}
   2.140 -    @{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]
   2.141 -    \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"} \\
   2.142 -    \quad @{command "proof"}~@{method succeed} \\
   2.143 -    \qquad @{command "fix"}~@{text thesis} \\
   2.144 -    \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"} \\
   2.145 -    \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
   2.146 -    \quad\qquad @{command "apply"}~@{text -} \\
   2.147 -    \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k  \<langle>proof\<rangle>"} \\
   2.148 -    \quad @{command "qed"} \\
   2.149 -    \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
   2.150 +    @{command "consider"}~@{text "(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b) \<^vec>y \<WHERE> \<^vec>B \<^vec>y | \<dots> \<equiv>"} \\[1ex]
   2.151 +    \quad @{command "have"}~@{text "[case_names a b \<dots>]: thesis"} \\
   2.152 +    \qquad @{text "\<IF> a [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
   2.153 +    \qquad @{text "\<AND> b [Pure.intro?]: \<And>\<^vec>y. \<^vec>B \<^vec>y \<Longrightarrow> thesis"} \\
   2.154 +    \qquad @{text "\<AND> \<dots>"} \\
   2.155 +    \qquad @{text "\<FOR> thesis"} \\
   2.156 +    \qquad @{command "apply"}~@{text "(insert a b \<dots>)"} \\
   2.157    \end{matharray}
   2.158  
   2.159 -  Typically, the soundness proof is relatively straight-forward, often
   2.160 -  just by canonical automated tools such as ``@{command "by"}~@{text
   2.161 -  simp}'' or ``@{command "by"}~@{text blast}''.  Accordingly, the
   2.162 -  ``@{text that}'' reduction above is declared as simplification and
   2.163 -  introduction rule.
   2.164 +  See also \secref{sec:goals} for @{keyword "obtains"} in toplevel goal
   2.165 +  statements, as well as @{command print_statement} to print existing rules
   2.166 +  in a similar format.
   2.167  
   2.168 -  In a sense, @{command "obtain"} represents at the level of Isar
   2.169 -  proofs what would be meta-logical existential quantifiers and
   2.170 -  conjunctions.  This concept has a broad range of useful
   2.171 -  applications, ranging from plain elimination (or introduction) of
   2.172 -  object-level existential and conjunctions, to elimination over
   2.173 -  results of symbolic evaluation of recursive definitions, for
   2.174 -  example.  Also note that @{command "obtain"} without parameters acts
   2.175 -  much like @{command "have"}, where the result is treated as a
   2.176 -  genuine assumption.
   2.177 +  \item @{command obtain}~@{text "\<^vec>x \<WHERE> \<^vec>A \<^vec>x"}
   2.178 +  states a generalized elimination rule with exactly one case. After the
   2.179 +  proof is finished, it is activated for the subsequent proof text: the
   2.180 +  context is augmented via @{command fix}~@{text "\<^vec>x"} @{command
   2.181 +  assume}~@{text "\<^vec>A \<^vec>x"}, with special provisions to export
   2.182 +  later results by discharging these assumptions again.
   2.183 +
   2.184 +  Note that according to the parameter scopes within the elimination rule,
   2.185 +  results \emph{must not} refer to hypothetical parameters; otherwise the
   2.186 +  export will fail! This restriction conforms to the usual manner of
   2.187 +  existential reasoning in Natural Deduction.
   2.188 +
   2.189 +  \medskip Formally, the command @{command obtain} is defined as derived
   2.190 +  Isar language element as follows, using an instrumented variant of
   2.191 +  @{command assume}:
   2.192  
   2.193 -  An alternative name to be used instead of ``@{text that}'' above may
   2.194 -  be given in parentheses.
   2.195 +  \begin{matharray}{l}
   2.196 +    @{command "obtain"}~@{text "\<^vec>x \<WHERE> a: \<^vec>A \<^vec>x  \<langle>proof\<rangle> \<equiv>"} \\[1ex]
   2.197 +    \quad @{command "have"}~@{text "thesis"} \\
   2.198 +    \qquad @{text "\<IF> that [Pure.intro?]: \<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"} \\
   2.199 +    \qquad @{text "\<FOR> thesis"} \\
   2.200 +    \qquad @{command "apply"}~@{text "(insert that)"} \\
   2.201 +    \qquad @{text "\<langle>proof\<rangle>"} \\
   2.202 +    \quad @{command "fix"}~@{text "\<^vec>x"}~@{command "assume"}@{text "\<^sup>* a: \<^vec>A \<^vec>x"} \\
   2.203 +  \end{matharray}
   2.204 +
   2.205 +  \item @{command guess} is similar to @{command obtain}, but it derives the
   2.206 +  obtained context elements from the course of tactical reasoning in the
   2.207 +  proof. Thus it can considerably obscure the proof: it is classified as
   2.208 +  \emph{improper}.
   2.209  
   2.210 -  \medskip The improper variant @{command "guess"} is similar to
   2.211 -  @{command "obtain"}, but derives the obtained statement from the
   2.212 -  course of reasoning!  The proof starts with a fixed goal @{text
   2.213 -  thesis}.  The subsequent proof may refine this to anything of the
   2.214 -  form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
   2.215 -  \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals.  The
   2.216 -  final goal state is then used as reduction rule for the obtain
   2.217 -  scheme described above.  Obtained parameters @{text "x\<^sub>1, \<dots>,
   2.218 -  x\<^sub>m"} are marked as internal by default, which prevents the
   2.219 -  proof context from being polluted by ad-hoc variables.  The variable
   2.220 -  names and type constraints given as arguments for @{command "guess"}
   2.221 -  specify a prefix of obtained parameters explicitly in the text.
   2.222 +  A proof with @{command guess} starts with a fixed goal @{text thesis}. The
   2.223 +  subsequent refinement steps may turn this to anything of the form @{text
   2.224 +  "\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis"}, but without splitting into new
   2.225 +  subgoals. The final goal state is then used as reduction rule for the
   2.226 +  obtain pattern described above. Obtained parameters @{text "\<^vec>x"} are
   2.227 +  marked as internal by default, and thus inaccessible in the proof text.
   2.228 +  The variable names and type constraints given as arguments for @{command
   2.229 +  "guess"} specify a prefix of accessible parameters.
   2.230  
   2.231 -  It is important to note that the facts introduced by @{command
   2.232 -  "obtain"} and @{command "guess"} may not be polymorphic: any
   2.233 -  type-variables occurring here are fixed in the present context!
   2.234 +  \end{description}
   2.235 +
   2.236 +  In the proof of @{command consider} and @{command obtain} the local
   2.237 +  premises are always bound to the fact name ``@{text that}'', according to
   2.238 +  structured Isar statements involving @{keyword_ref "if"}
   2.239 +  (\secref{sec:goals}).
   2.240 +
   2.241 +  Facts that are established by @{command "obtain"} and @{command "guess"}
   2.242 +  may not be polymorphic: any type-variables occurring here are fixed in the
   2.243 +  present context. This is a natural consequence of the role of @{command
   2.244 +  fix} and @{command assume} in these constructs.
   2.245  \<close>
   2.246  
   2.247  
     3.1 --- a/src/Doc/isar.sty	Sat Jun 13 20:07:54 2015 +0200
     3.2 +++ b/src/Doc/isar.sty	Sat Jun 13 22:42:23 2015 +0200
     3.3 @@ -13,6 +13,7 @@
     3.4  \newcommand{\indexouternonterm}[1]{\indexdef{}{syntax}{#1}}
     3.5  \newcommand{\indexisarelem}[1]{\indexdef{}{element}{#1}}
     3.6  
     3.7 +\newcommand{\isasymIF}{\isakeyword{if}}
     3.8  \newcommand{\isasymFOR}{\isakeyword{for}}
     3.9  \newcommand{\isasymAND}{\isakeyword{and}}
    3.10  \newcommand{\isasymIS}{\isakeyword{is}}