src/Doc/Isar_Ref/Proof.thy

 theory Proof
 imports Base Main
 begin
 
-chapter {* Proofs \label{ch:proofs} *}
-
-text {*
+chapter \<open>Proofs \label{ch:proofs}\<close>
+
+text \<open>
   Proof commands perform transitions of Isar/VM machine
   configurations, which are block-structured, consisting of a stack of
   nodes with three main components: logical proof context, current
   facts, and open goals.  Isar/VM transitions are typed according to
   the following three different modes of operation:

 
   \Appref{ap:refcard} gives a simplified grammar of the (extensible)
   language emerging that way from the different types of proof
   commands.  The main ideas of the overall Isar framework are
   explained in \chref{ch:isar-framework}.
-*}
-
-
-section {* Proof structure *}
-
-subsection {* Formal notepad *}
-
-text {*
+\<close>
+
+
+section \<open>Proof structure\<close>
+
+subsection \<open>Formal notepad\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "notepad"} & : & @{text "local_theory \<rightarrow> proof(state)"} \\
   \end{matharray}
 
   @{rail \<open>

 
   The notepad can be closed by @{command "end"} or discontinued by
   @{command "oops"}.
 
   \end{description}
-*}
-
-
-subsection {* Blocks *}
-
-text {*
+\<close>
+
+
+subsection \<open>Blocks\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "next"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "{"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "}"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
   \end{matharray}

   of @{command "assume"} and @{command "presume"} in this mode of
   forward reasoning --- in contrast to plain backward reasoning with
   the result exported at @{command "show"} time.
 
   \end{description}
-*}
-
-
-subsection {* Omitting proofs *}
-
-text {*
+\<close>
+
+
+subsection \<open>Omitting proofs\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "oops"} & : & @{text "proof \<rightarrow> local_theory | theory"} \\
   \end{matharray}
 
   The @{command "oops"} command discontinues the current proof

   preparation tools of Isabelle described in \chref{ch:document-prep}.
   Thus partial or even wrong proof attempts can be discussed in a
   logically sound manner.  Note that the Isabelle {\LaTeX} macros can
   be easily adapted to print something like ``@{text "\<dots>"}'' instead of
   the keyword ``@{command "oops"}''.
-*}
-
-
-section {* Statements *}
-
-subsection {* Context elements \label{sec:proof-context} *}
-
-text {*
+\<close>
+
+
+section \<open>Statements\<close>
+
+subsection \<open>Context elements \label{sec:proof-context}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "fix"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "assume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "presume"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "def"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\

   \end{description}
 
   The special name @{fact_ref prems} refers to all assumptions of the
   current context as a list of theorems.  This feature should be used
   with great care!  It is better avoided in final proof texts.
-*}
-
-
-subsection {* Term abbreviations \label{sec:term-abbrev} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Term abbreviations \label{sec:term-abbrev}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "let"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{keyword_def "is"} & : & syntax \\
   \end{matharray}
 

   assumptions or finished goals.  In case @{variable this} refers to
   an object-logic statement that is an application @{text "f t"}, then
   @{text t} is bound to the special text variable ``@{variable "\<dots>"}''
   (three dots).  The canonical application of this convenience are
   calculational proofs (see \secref{sec:calculation}).
-*}
-
-
-subsection {* Facts and forward chaining \label{sec:proof-facts} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Facts and forward chaining \label{sec:proof-facts}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "note"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "then"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
     @{command_def "from"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
     @{command_def "with"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

 
   Automated methods (such as @{method simp} or @{method auto}) just
   insert any given facts before their usual operation.  Depending on
   the kind of procedure involved, the order of facts is less
   significant here.
-*}
-
-
-subsection {* Goals \label{sec:goals} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Goals \label{sec:goals}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
     @{command_def "theorem"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
     @{command_def "corollary"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
     @{command_def "schematic_lemma"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\

   The optional case names of @{element_ref "obtains"} have a twofold
   meaning: (1) in the proof of this claim they refer to the local context
   introductions, (2) in the resulting rule they become annotations for
   symbolic case splits, e.g.\ for the @{method_ref cases} method
   (\secref{sec:cases-induct}).
-*}
-
-
-section {* Refinement steps *}
-
-subsection {* Proof method expressions \label{sec:proof-meth} *}
-
-text {* Proof methods are either basic ones, or expressions composed
+\<close>
+
+
+section \<open>Refinement steps\<close>
+
+subsection \<open>Proof method expressions \label{sec:proof-meth}\<close>
+
+text \<open>Proof methods are either basic ones, or expressions composed
   of methods via ``@{verbatim ","}'' (sequential composition),
   ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}''
   (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
   "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
   sub-goals, with default @{text "n = 1"}).  In practice, proof

 
   @{rail \<open>
     @{syntax_def goal_spec}:
       '[' (@{syntax nat} '-' @{syntax nat} | @{syntax nat} '-' | @{syntax nat} | '!' ) ']'
   \<close>}
-*}
-
-
-subsection {* Initial and terminal proof steps \label{sec:proof-steps} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Initial and terminal proof steps \label{sec:proof-steps}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "proof"} & : & @{text "proof(prove) \<rightarrow> proof(state)"} \\
     @{command_def "qed"} & : & @{text "proof(state) \<rightarrow> proof(state) | local_theory | theory"} \\
     @{command_def "by"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
     @{command_def ".."} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\

   
   The most important application of @{command "sorry"} is to support
   experimentation and top-down proof development.
 
   \end{description}
-*}
-
-
-subsection {* Fundamental methods and attributes \label{sec:pure-meth-att} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Fundamental methods and attributes \label{sec:pure-meth-att}\<close>
+
+text \<open>
   The following proof methods and attributes refer to basic logical
   operations of Isar.  Further methods and attributes are provided by
   several generic and object-logic specific tools and packages (see
   \chref{ch:gen-tools} and \partref{part:hol}).
 

 
   An optional context of local variables @{text "\<FOR> x\<^sub>1 \<dots> x\<^sub>m"} may
   be specified as for @{attribute "of"} above.
 
   \end{description}
-*}
-
-
-subsection {* Emulating tactic scripts \label{sec:tactic-commands} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Emulating tactic scripts \label{sec:tactic-commands}\<close>
+
+text \<open>
   The Isar provides separate commands to accommodate tactic-style
   proof scripts within the same system.  While being outside the
   orthodox Isar proof language, these might come in handy for
   interactive exploration and debugging, or even actual tactical proof
   within new-style theories (to benefit from document preparation, for

 
   Any proper Isar proof method may be used with tactic script commands
   such as @{command "apply"}.  A few additional emulations of actual
   tactics are provided as well; these would be never used in actual
   structured proofs, of course.
-*}
-
-
-subsection {* Defining proof methods *}
-
-text {*
+\<close>
+
+
+subsection \<open>Defining proof methods\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "method_setup"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   @{rail \<open>

   addressing.
 
   Here are some example method definitions:
 
   \end{description}
-*}
-
-  method_setup my_method1 = {*
+\<close>
+
+  method_setup my_method1 = \<open>
     Scan.succeed (K (SIMPLE_METHOD' (fn i: int => no_tac)))
-  *}  "my first method (without any arguments)"
-
-  method_setup my_method2 = {*
+\<close>  "my first method (without any arguments)"
+
+  method_setup my_method2 = \<open>
     Scan.succeed (fn ctxt: Proof.context =>
       SIMPLE_METHOD' (fn i: int => no_tac))
-  *}  "my second method (with context)"
-
-  method_setup my_method3 = {*
+\<close>  "my second method (with context)"
+
+  method_setup my_method3 = \<open>
     Attrib.thms >> (fn thms: thm list => fn ctxt: Proof.context =>
       SIMPLE_METHOD' (fn i: int => no_tac))
-  *}  "my third method (with theorem arguments and context)"
-
-
-section {* Generalized elimination \label{sec:obtain} *}
-
-text {*
+\<close>  "my third method (with theorem arguments and context)"
+
+
+section \<open>Generalized elimination \label{sec:obtain}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "obtain"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
     @{command_def "guess"}@{text "\<^sup>*"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
   \end{matharray}
 

   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!
-*}
-
-
-section {* Calculational reasoning \label{sec:calculation} *}
-
-text {*
+\<close>
+
+
+section \<open>Calculational reasoning \label{sec:calculation}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "also"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "finally"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\
     @{command_def "moreover"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "ultimately"} & : & @{text "proof(state) \<rightarrow> proof(chain)"} \\

   explicit single-step elimination proof, such as ``@{command
   "assume"}~@{text "x = y"}~@{command "then"}~@{command "have"}~@{text
   "y = x"}~@{command ".."}''.
 
   \end{description}
-*}
-
-
-section {* Proof by cases and induction \label{sec:cases-induct} *}
-
-subsection {* Rule contexts *}
-
-text {*
+\<close>
+
+
+section \<open>Proof by cases and induction \label{sec:cases-induct}\<close>
+
+subsection \<open>Rule contexts\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "case"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "print_cases"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def case_names} & : & @{text attribute} \\
     @{attribute_def case_conclusion} & : & @{text attribute} \\

   rarely needed; this is already taken care of automatically by the
   higher-level @{attribute cases}, @{attribute induct}, and
   @{attribute coinduct} declarations.
 
   \end{description}
-*}
-
-
-subsection {* Proof methods *}
-
-text {*
+\<close>
+
+
+subsection \<open>Proof methods\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{method_def cases} & : & @{text method} \\
     @{method_def induct} & : & @{text method} \\
     @{method_def induction} & : & @{text method} \\
     @{method_def coinduct} & : & @{text method} \\

   usually 0 for plain cases and induction rules of datatypes etc.\ and
   1 for rules of inductive predicates or sets and the like.  The
   remaining facts are inserted into the goal verbatim before the
   actual @{text cases}, @{text induct}, or @{text coinduct} rule is
   applied.
-*}
-
-
-subsection {* Declaring rules *}
-
-text {*
+\<close>
+
+
+subsection \<open>Declaring rules\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "print_induct_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def cases} & : & @{text attribute} \\
     @{attribute_def induct} & : & @{text attribute} \\
     @{attribute_def coinduct} & : & @{text attribute} \\

   declaration is taken care of automatically: @{attribute
   consumes}~@{text 0} is specified for ``type'' rules and @{attribute
   consumes}~@{text 1} for ``predicate'' / ``set'' rules.
 
   \end{description}
-*}
+\<close>
 
 end