src/Doc/Isar_Ref/Spec.thy

 theory Spec
 imports Base Main
 begin
 
-chapter {* Specifications *}
-
-text {*
+chapter \<open>Specifications\<close>
+
+text \<open>
   The Isabelle/Isar theory format integrates specifications and
   proofs, supporting interactive development with unlimited undo
   operation.  There is an integrated document preparation system (see
   \chref{ch:document-prep}), for typesetting formal developments
   together with informal text.  The resulting hyper-linked PDF

   stating some @{command theorem} or @{command lemma} at the theory
   level, and left again with the final conclusion (e.g.\ via @{command
   qed}).  Some theory specification mechanisms also require a proof,
   such as @{command typedef} in HOL, which demands non-emptiness of
   the representing sets.
-*}
-
-
-section {* Defining theories \label{sec:begin-thy} *}
-
-text {*
+\<close>
+
+
+section \<open>Defining theories \label{sec:begin-thy}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "theory"} & : & @{text "toplevel \<rightarrow> theory"} \\
     @{command_def (global) "end"} & : & @{text "theory \<rightarrow> toplevel"} \\
   \end{matharray}
 

   targets @{command locale} or @{command class} may involve a
   @{keyword "begin"} that needs to be matched by @{command (local)
   "end"}, according to the usual rules for nested blocks.
 
   \end{description}
-*}
-
-
-section {* Local theory targets \label{sec:target} *}
-
-text {*
+\<close>
+
+
+section \<open>Local theory targets \label{sec:target}\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def (local) "end"} & : & @{text "local_theory \<rightarrow> theory"} \\
   \end{matharray}
 

   @{text "?x"}.
 
   \medskip The Isabelle/HOL library contains numerous applications of
   locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}.  An
   example for an unnamed auxiliary contexts is given in @{file
-  "~~/src/HOL/Isar_Examples/Group_Context.thy"}.  *}
-
-
-section {* Bundled declarations \label{sec:bundle} *}
-
-text {*
+  "~~/src/HOL/Isar_Examples/Group_Context.thy"}.\<close>
+
+
+section \<open>Bundled declarations \label{sec:bundle}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "bundle"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "print_bundles"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
     @{command_def "include"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
     @{command_def "including"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\

   statements of @{command theorem} etc.
 
   \end{description}
 
   Here is an artificial example of bundling various configuration
-  options: *}
+  options:\<close>
 
 bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
 
 lemma "x = x"
   including trace by metis
 
 
-section {* Term definitions \label{sec:term-definitions} *}
-
-text {*
+section \<open>Term definitions \label{sec:term-definitions}\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "definition"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{attribute_def "defn"} & : & @{text attribute} \\
     @{command_def "print_defn_rules"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow> "} \\
     @{command_def "abbreviation"} & : & @{text "local_theory \<rightarrow> local_theory"} \\

   
   \item @{command "print_abbrevs"} prints all constant abbreviations
   of the current context.
   
   \end{description}
-*}
-
-
-section {* Axiomatizations \label{sec:axiomatizations} *}
-
-text {*
+\<close>
+
+
+section \<open>Axiomatizations \label{sec:axiomatizations}\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "axiomatization"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   \end{matharray}
 
   @{rail \<open>

   within Isabelle/Pure, but in an application environment like Isabelle/HOL
   the user normally stays within definitional mechanisms provided by the
   logic and its libraries.
 
   \end{description}
-*}
-
-
-section {* Generic declarations *}
-
-text {*
+\<close>
+
+
+section \<open>Generic declarations\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "syntax_declaration"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "declare"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}

   unlike @{command "theorems"} or @{command "lemmas"} (cf.\
   \secref{sec:theorems}), so @{command "declare"} only has the effect
   of applying attributes as included in the theorem specification.
 
   \end{description}
-*}
-
-
-section {* Locales \label{sec:locale} *}
-
-text {*
+\<close>
+
+
+section \<open>Locales \label{sec:locale}\<close>
+
+text \<open>
   A locale is a functor that maps parameters (including implicit type
   parameters) and a specification to a list of declarations.  The
   syntax of locales is modeled after the Isar proof context commands
   (cf.\ \secref{sec:proof-context}).
 

   as a local theory.  In this process, which is called \emph{roundup},
   redundant locale instances are omitted.  A locale instance is
   redundant if it is subsumed by an instance encountered earlier.  A
   more detailed description of this process is available elsewhere
   @{cite Ballarin2014}.
-*}
-
-
-subsection {* Locale expressions \label{sec:locale-expr} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Locale expressions \label{sec:locale-expr}\<close>
+
+text \<open>
   A \emph{locale expression} denotes a context composed of instances
   of existing locales.  The context consists of the declaration
   elements from the locale instances.  Redundant locale instances are
   omitted according to roundup.
 

   ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
   is used.  For @{command "interpretation"} and @{command "interpret"}
   the default is ``mandatory'', for @{command "locale"} and @{command
   "sublocale"} the default is ``optional''.  Qualifiers play no role
   in determining whether one locale instance subsumes another.
-*}
-
-
-subsection {* Locale declarations *}
-
-text {*
+\<close>
+
+
+subsection \<open>Locale declarations\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "locale"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "print_locale"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_locales"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "locale_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

   specifications entailed by the context, both from target statements,
   and from interpretations (see below).  New goals that are entailed
   by the current context are discharged automatically.
 
   \end{description}
-*}
-
-
-subsection {* Locale interpretation *}
-
-text {*
+\<close>
+
+
+subsection \<open>Locale interpretation\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "interpretation"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\
     @{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
     @{command_def "sublocale"} & : & @{text "theory | local_theory \<rightarrow> proof(prove)"} \\
     @{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\

     is interpreted twice and the instantiation of the second
     interpretation is more general than the interpretation of the
     first.  The locale package does not attempt to remove subsumed
     interpretations.
   \end{warn}
-*}
-
-
-section {* Classes \label{sec:class} *}
-
-text {*
+\<close>
+
+
+section \<open>Classes \label{sec:class}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "class"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "instantiation"} & : & @{text "theory \<rightarrow> local_theory"} \\
     @{command_def "instance"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command "instance"} & : & @{text "theory \<rightarrow> proof(prove)"} \\

   default proof step (e.g.\ of @{command "proof"}).  In particular,
   instantiation of trivial (syntactic) classes may be performed by a
   single ``@{command ".."}'' proof step.
 
   \end{description}
-*}
-
-
-subsection {* The class target *}
-
-text {*
+\<close>
+
+
+subsection \<open>The class target\<close>
+
+text \<open>
   %FIXME check
 
   A named context may refer to a locale (cf.\ \secref{sec:target}).
   If this locale is also a class @{text c}, apart from the common
   locale target behaviour the following happens.

   global operations @{text "g[?\<alpha> :: c]"} uniformly.  Type inference
   resolves ambiguities.  In rare cases, manual type annotations are
   needed.
   
   \end{itemize}
-*}
-
-
-subsection {* Co-regularity of type classes and arities *}
-
-text {* The class relation together with the collection of
+\<close>
+
+
+subsection \<open>Co-regularity of type classes and arities\<close>
+
+text \<open>The class relation together with the collection of
   type-constructor arities must obey the principle of
   \emph{co-regularity} as defined below.
 
   \medskip For the subsequent formulation of co-regularity we assume
   that the class relation is closed by transitivity and reflexivity.

   argument sorts need to be related in the same way.
 
   \medskip Co-regularity is a very fundamental property of the
   order-sorted algebra of types.  For example, it entails principle
   types and most general unifiers, e.g.\ see @{cite "nipkow-prehofer"}.
-*}
-
-
-section {* Unrestricted overloading *}
-
-text {*
+\<close>
+
+
+section \<open>Unrestricted overloading\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "overloading"} & : & @{text "theory \<rightarrow> local_theory"} \\
   \end{matharray}
 
   Isabelle/Pure's definitional schemes support certain forms of

   exotic overloading (see \secref{sec:consts} for a precise description).
   It is at the discretion of the user to avoid
   malformed theory specifications!
 
   \end{description}
-*}
-
-
-section {* Incorporating ML code \label{sec:ML} *}
-
-text {*
+\<close>
+
+
+section \<open>Incorporating ML code \label{sec:ML}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "SML_file"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "ML_file"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "ML"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "ML_prf"} & : & @{text "proof \<rightarrow> proof"} \\

   In principle, attributes can operate both on a given theorem and the
   implicit context, although in practice only one is modified and the
   other serves as parameter.  Here are examples for these two cases:
 
   \end{description}
-*}
-
-  attribute_setup my_rule = {*
+\<close>
+
+  attribute_setup my_rule = \<open>
     Attrib.thms >> (fn ths =>
       Thm.rule_attribute
         (fn context: Context.generic => fn th: thm =>
           let val th' = th OF ths
-          in th' end)) *}
-
-  attribute_setup my_declaration = {*
+          in th' end))\<close>
+
+  attribute_setup my_declaration = \<open>
     Attrib.thms >> (fn ths =>
       Thm.declaration_attribute
         (fn th: thm => fn context: Context.generic =>
           let val context' = context
-          in context' end)) *}
-
-text {*
+          in context' end))\<close>
+
+text \<open>
   \begin{description}
 
   \item @{attribute ML_print_depth} controls the printing depth of the ML
   toplevel pretty printer; the precise effect depends on the ML compiler and
   run-time system. Typically the limit should be less than 10. Bigger values

   Runtime.exn_trace} into ML code for debugging @{cite
   "isabelle-implementation"}, closer to the point where it actually
   happens.
 
   \end{description}
-*}
-
-
-section {* Primitive specification elements *}
-
-subsection {* Sorts *}
-
-text {*
+\<close>
+
+
+section \<open>Primitive specification elements\<close>
+
+subsection \<open>Sorts\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
   \end{matharray}
 
   @{rail \<open>

   When merging theories, the default sorts of the parents are
   logically intersected, i.e.\ the representations as lists of classes
   are joined.
 
   \end{description}
-*}
-
-
-subsection {* Types \label{sec:types-pure} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Types \label{sec:types-pure}\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}
 

   free-form axiomatizations can coexist with other axiomatization schemes
   for types, notably @{command_def typedef} in Isabelle/HOL
   (\secref{sec:hol-typedef}), or any other extension that people might have
   introduced elsewhere.
   \end{warn}
-*}
-
-
-subsection {* Constants and definitions \label{sec:consts} *}
-
-text {*
+\<close>
+
+
+subsection \<open>Constants and definitions \label{sec:consts}\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "consts"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "defs"} & : & @{text "theory \<rightarrow> theory"} \\
   \end{matharray}
 

   potentially overloaded.  Unless this option is given, a warning
   message would be issued for any definitional equation with a more
   special type than that of the corresponding constant declaration.
   
   \end{description}
-*}
-
-
-section {* Naming existing theorems \label{sec:theorems} *}
-
-text {*
+\<close>
+
+
+section \<open>Naming existing theorems \label{sec:theorems}\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "lemmas"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "named_theorems"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
   \end{matharray}

   an attribute with the usual @{text add}/@{text del} syntax (e.g.\ see
   \secref{sec:simp-rules}) to maintain the content incrementally, in
   canonical declaration order of the text structure.
 
   \end{description}
-*}
-
-
-section {* Oracles *}
-
-text {*
+\<close>
+
+
+section \<open>Oracles\<close>
+
+text \<open>
   \begin{matharray}{rcll}
     @{command_def "oracle"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
   \end{matharray}
 
   Oracles allow Isabelle to take advantage of external reasoners such

   \end{description}
 
   See @{file "~~/src/HOL/ex/Iff_Oracle.thy"} for a worked example of
   defining a new primitive rule as oracle, and turning it into a proof
   method.
-*}
-
-
-section {* Name spaces *}
-
-text {*
+\<close>
+
+
+section \<open>Name spaces\<close>
+
+text \<open>
   \begin{matharray}{rcl}
     @{command_def "hide_class"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "hide_type"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "hide_const"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "hide_fact"} & : & @{text "theory \<rightarrow> theory"} \\

   \item @{command "hide_type"}, @{command "hide_const"}, and @{command
   "hide_fact"} are similar to @{command "hide_class"}, but hide types,
   constants, and facts, respectively.
   
   \end{description}
-*}
+\<close>
 
 end