doc-src/IsarRef/Thy/Generic.thy

   \item [@{text "name = value"}] as an attribute expression modifies
   the named option, with the syntax of the value depending on the
   option's type.  For @{ML_type bool} the default value is @{text
   true}.  Any attempt to change a global option in a local context is
   ignored.
-
-  \end{descr}
-*}
-
-
-section {* Derived proof schemes *}
-
-subsection {* Generalized elimination \label{sec:obtain} *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def "obtain"} & : & \isartrans{proof(state)}{proof(prove)} \\
-    @{command_def "guess"}@{text "\<^sup>*"} & : & \isartrans{proof(state)}{proof(prove)} \\
-  \end{matharray}
-
-  Generalized elimination means that additional elements with certain
-  properties may be introduced in the current context, by virtue of a
-  locally proven ``soundness statement''.  Technically speaking, the
-  @{command "obtain"} language element is like a declaration of
-  @{command "fix"} and @{command "assume"} (see also see
-  \secref{sec:proof-context}), together with a soundness proof of its
-  additional claim.  According to the nature of existential reasoning,
-  assumptions get eliminated from any result exported from the context
-  later, provided that the corresponding parameters do \emph{not}
-  occur in the conclusion.
-
-  \begin{rail}
-    'obtain' parname? (vars + 'and') 'where' (props + 'and')
-    ;
-    'guess' (vars + 'and')
-    ;
-  \end{rail}
-
-  The derived Isar command @{command "obtain"} is defined as follows
-  (where @{text "b\<^sub>1, \<dots>, b\<^sub>k"} shall refer to (optional)
-  facts indicated for forward chaining).
-  \begin{matharray}{l}
-    @{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]
-    \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"} \\
-    \quad @{command "proof"}~@{text succeed} \\
-    \qquad @{command "fix"}~@{text thesis} \\
-    \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"} \\
-    \qquad @{command "then"}~@{command "show"}~@{text thesis} \\
-    \quad\qquad @{command "apply"}~@{text -} \\
-    \quad\qquad @{command "using"}~@{text "b\<^sub>1 \<dots> b\<^sub>k  \<langle>proof\<rangle>"} \\
-    \quad @{command "qed"} \\
-    \quad @{command "fix"}~@{text "x\<^sub>1 \<dots> x\<^sub>m"}~@{command "assume"}@{text "\<^sup>* a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} \\
-  \end{matharray}
-
-  Typically, the soundness proof is relatively straight-forward, often
-  just by canonical automated tools such as ``@{command "by"}~@{text
-  simp}'' or ``@{command "by"}~@{text blast}''.  Accordingly, the
-  ``@{text that}'' reduction above is declared as simplification and
-  introduction rule.
-
-  In a sense, @{command "obtain"} represents at the level of Isar
-  proofs what would be meta-logical existential quantifiers and
-  conjunctions.  This concept has a broad range of useful
-  applications, ranging from plain elimination (or introduction) of
-  object-level existential and conjunctions, to elimination over
-  results of symbolic evaluation of recursive definitions, for
-  example.  Also note that @{command "obtain"} without parameters acts
-  much like @{command "have"}, where the result is treated as a
-  genuine assumption.
-
-  An alternative name to be used instead of ``@{text that}'' above may
-  be given in parentheses.
-
-  \medskip The improper variant @{command "guess"} is similar to
-  @{command "obtain"}, but derives the obtained statement from the
-  course of reasoning!  The proof starts with a fixed goal @{text
-  thesis}.  The subsequent proof may refine this to anything of the
-  form like @{text "\<And>x\<^sub>1 \<dots> x\<^sub>m. \<phi>\<^sub>1 \<Longrightarrow> \<dots>
-  \<phi>\<^sub>n \<Longrightarrow> thesis"}, but must not introduce new subgoals.  The
-  final goal state is then used as reduction rule for the obtain
-  scheme described above.  Obtained parameters @{text "x\<^sub>1, \<dots>,
-  x\<^sub>m"} are marked as internal by default, which prevents the
-  proof context from being polluted by ad-hoc variables.  The variable
-  names and type constraints given as arguments for @{command "guess"}
-  specify a prefix of obtained parameters explicitly in the text.
-
-  It is important to note that the facts introduced by @{command
-  "obtain"} and @{command "guess"} may not be polymorphic: any
-  type-variables occurring here are fixed in the present context!
-*}
-
-
-subsection {* Calculational reasoning \label{sec:calculation} *}
-
-text {*
-  \begin{matharray}{rcl}
-    @{command_def "also"} & : & \isartrans{proof(state)}{proof(state)} \\
-    @{command_def "finally"} & : & \isartrans{proof(state)}{proof(chain)} \\
-    @{command_def "moreover"} & : & \isartrans{proof(state)}{proof(state)} \\
-    @{command_def "ultimately"} & : & \isartrans{proof(state)}{proof(chain)} \\
-    @{command_def "print_trans_rules"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
-    @{attribute trans} & : & \isaratt \\
-    @{attribute sym} & : & \isaratt \\
-    @{attribute symmetric} & : & \isaratt \\
-  \end{matharray}
-
-  Calculational proof is forward reasoning with implicit application
-  of transitivity rules (such those of @{text "="}, @{text "\<le>"},
-  @{text "<"}).  Isabelle/Isar maintains an auxiliary fact register
-  @{fact_ref calculation} for accumulating results obtained by
-  transitivity composed with the current result.  Command @{command
-  "also"} updates @{fact calculation} involving @{fact this}, while
-  @{command "finally"} exhibits the final @{fact calculation} by
-  forward chaining towards the next goal statement.  Both commands
-  require valid current facts, i.e.\ may occur only after commands
-  that produce theorems such as @{command "assume"}, @{command
-  "note"}, or some finished proof of @{command "have"}, @{command
-  "show"} etc.  The @{command "moreover"} and @{command "ultimately"}
-  commands are similar to @{command "also"} and @{command "finally"},
-  but only collect further results in @{fact calculation} without
-  applying any rules yet.
-
-  Also note that the implicit term abbreviation ``@{text "\<dots>"}'' has
-  its canonical application with calculational proofs.  It refers to
-  the argument of the preceding statement. (The argument of a curried
-  infix expression happens to be its right-hand side.)
-
-  Isabelle/Isar calculations are implicitly subject to block structure
-  in the sense that new threads of calculational reasoning are
-  commenced for any new block (as opened by a local goal, for
-  example).  This means that, apart from being able to nest
-  calculations, there is no separate \emph{begin-calculation} command
-  required.
-
-  \medskip The Isar calculation proof commands may be defined as
-  follows:\footnote{We suppress internal bookkeeping such as proper
-  handling of block-structure.}
-
-  \begin{matharray}{rcl}
-    @{command "also"}@{text "\<^sub>0"} & \equiv & @{command "note"}~@{text "calculation = this"} \\
-    @{command "also"}@{text "\<^sub>n\<^sub>+\<^sub>1"} & \equiv & @{command "note"}~@{text "calculation = trans [OF calculation this]"} \\[0.5ex]
-    @{command "finally"} & \equiv & @{command "also"}~@{command "from"}~@{text calculation} \\[0.5ex]
-    @{command "moreover"} & \equiv & @{command "note"}~@{text "calculation = calculation this"} \\
-    @{command "ultimately"} & \equiv & @{command "moreover"}~@{command "from"}~@{text calculation} \\
-  \end{matharray}
-
-  \begin{rail}
-    ('also' | 'finally') ('(' thmrefs ')')?
-    ;
-    'trans' (() | 'add' | 'del')
-    ;
-  \end{rail}
-
-  \begin{descr}
-
-  \item [@{command "also"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
-  maintains the auxiliary @{fact calculation} register as follows.
-  The first occurrence of @{command "also"} in some calculational
-  thread initializes @{fact calculation} by @{fact this}. Any
-  subsequent @{command "also"} on the same level of block-structure
-  updates @{fact calculation} by some transitivity rule applied to
-  @{fact calculation} and @{fact this} (in that order).  Transitivity
-  rules are picked from the current context, unless alternative rules
-  are given as explicit arguments.
-
-  \item [@{command "finally"}~@{text "(a\<^sub>1 \<dots> a\<^sub>n)"}]
-  maintaining @{fact calculation} in the same way as @{command
-  "also"}, and concludes the current calculational thread.  The final
-  result is exhibited as fact for forward chaining towards the next
-  goal. Basically, @{command "finally"} just abbreviates @{command
-  "also"}~@{command "from"}~@{fact calculation}.  Typical idioms for
-  concluding calculational proofs are ``@{command "finally"}~@{command
-  "show"}~@{text ?thesis}~@{command "."}'' and ``@{command
-  "finally"}~@{command "have"}~@{text \<phi>}~@{command "."}''.
-
-  \item [@{command "moreover"} and @{command "ultimately"}] are
-  analogous to @{command "also"} and @{command "finally"}, but collect
-  results only, without applying rules.
-
-  \item [@{command "print_trans_rules"}] prints the list of
-  transitivity rules (for calculational commands @{command "also"} and
-  @{command "finally"}) and symmetry rules (for the @{attribute
-  symmetric} operation and single step elimination patters) of the
-  current context.
-
-  \item [@{attribute trans}] declares theorems as transitivity rules.
-
-  \item [@{attribute sym}] declares symmetry rules, as well as
-  @{attribute "Pure.elim?"} rules.
-
-  \item [@{attribute symmetric}] resolves a theorem with some rule
-  declared as @{attribute sym} in the current context.  For example,
-  ``@{command "assume"}~@{text "[symmetric]: x = y"}'' produces a
-  swapped fact derived from that assumption.
-
-  In structured proof texts it is often more appropriate to use an
-  explicit single-step elimination proof, such as ``@{command
-  "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
-  "y = x"}~@{command ".."}''.
 
   \end{descr}
 *}