src/Doc/Locales/Examples3.thy

 theory Examples3
 imports Examples
 begin
 
-subsection {* Third Version: Local Interpretation
-  \label{sec:local-interpretation} *}
-
-text {* In the above example, the fact that @{term "op \<le>"} is a partial
+subsection \<open>Third Version: Local Interpretation
+  \label{sec:local-interpretation}\<close>
+
+text \<open>In the above example, the fact that @{term "op \<le>"} is a partial
   order for the integers was used in the second goal to
   discharge the premise in the definition of @{text "op \<sqsubset>"}.  In
   general, proofs of the equations not only may involve definitions
   from the interpreted locale but arbitrarily complex arguments in the
   context of the locale.  Therefore it would be convenient to have the
   interpreted locale conclusions temporarily available in the proof.
   This can be achieved by a locale interpretation in the proof body.
   The command for local interpretations is \isakeyword{interpret}.  We
-  repeat the example from the previous section to illustrate this. *}
+  repeat the example from the previous section to illustrate this.\<close>
 
   interpretation %visible int: partial_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
     where "int.less x y = (x < y)"
   proof -
     show "partial_order (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"

     then interpret int: partial_order "op \<le> :: [int, int] \<Rightarrow> bool" .
     show "int.less x y = (x < y)"
       unfolding int.less_def by auto
   qed
 
-text {* The inner interpretation is immediate from the preceding fact
+text \<open>The inner interpretation is immediate from the preceding fact
   and proved by assumption (Isar short hand ``.'').  It enriches the
   local proof context by the theorems
   also obtained in the interpretation from Section~\ref{sec:po-first},
   and @{text int.less_def} may directly be used to unfold the
   definition.  Theorems from the local interpretation disappear after
   leaving the proof context --- that is, after the succeeding
-  \isakeyword{next} or \isakeyword{qed} statement. *}
-
-
-subsection {* Further Interpretations *}
-
-text {* Further interpretations are necessary for
+  \isakeyword{next} or \isakeyword{qed} statement.\<close>
+
+
+subsection \<open>Further Interpretations\<close>
+
+text \<open>Further interpretations are necessary for
   the other locales.  In @{text lattice} the operations~@{text \<sqinter>}
   and~@{text \<squnion>} are substituted by @{term "min :: int \<Rightarrow> int \<Rightarrow> int"}
   and @{term "max :: int \<Rightarrow> int \<Rightarrow> int"}.  The entire proof for the
   interpretation is reproduced to give an example of a more
   elaborate interpretation proof.  Note that the equations are named
-  so they can be used in a later example.  *}
+  so they can be used in a later example.\<close>
 
   interpretation %visible int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
     where int_min_eq: "int.meet x y = min x y"
       and int_max_eq: "int.join x y = max x y"
   proof -
     show "lattice (op \<le> :: int \<Rightarrow> int \<Rightarrow> bool)"
-      txt {* \normalsize We have already shown that this is a partial
-        order, *}
+      txt \<open>\normalsize We have already shown that this is a partial
+        order,\<close>
       apply unfold_locales
-      txt {* \normalsize hence only the lattice axioms remain to be
+      txt \<open>\normalsize hence only the lattice axioms remain to be
         shown.
         @{subgoals [display]}
-        By @{text is_inf} and @{text is_sup}, *}
+        By @{text is_inf} and @{text is_sup},\<close>
       apply (unfold int.is_inf_def int.is_sup_def)
-      txt {* \normalsize the goals are transformed to these
+      txt \<open>\normalsize the goals are transformed to these
         statements:
         @{subgoals [display]}
         This is Presburger arithmetic, which can be solved by the
-        method @{text arith}. *}
+        method @{text arith}.\<close>
       by arith+
-    txt {* \normalsize In order to show the equations, we put ourselves
+    txt \<open>\normalsize In order to show the equations, we put ourselves
       in a situation where the lattice theorems can be used in a
-      convenient way. *}
+      convenient way.\<close>
     then interpret int: lattice "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool" .
     show "int.meet x y = min x y"
       by (bestsimp simp: int.meet_def int.is_inf_def)
     show "int.join x y = max x y"
       by (bestsimp simp: int.join_def int.is_sup_def)
   qed
 
-text {* Next follows that @{text "op \<le>"} is a total order, again for
-  the integers. *}
+text \<open>Next follows that @{text "op \<le>"} is a total order, again for
+  the integers.\<close>
 
   interpretation %visible int: total_order "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"
     by unfold_locales arith
 
-text {* Theorems that are available in the theory at this point are shown in
+text \<open>Theorems that are available in the theory at this point are shown in
   Table~\ref{tab:int-lattice}.  Two points are worth noting:
 
 \begin{table}
 \hrule
 \vspace{2ex}

   given in the interpretation of @{text partial_order}.  The
   interpretation equations are pushed downwards the hierarchy for
   related interpretations --- that is, for interpretations that share
   the instances of parameters they have in common.
 \end{itemize}
-  *}
-
-text {* The interpretations for a locale $n$ within the current
+\<close>
+
+text \<open>The interpretations for a locale $n$ within the current
   theory may be inspected with \isakeyword{print\_interps}~$n$.  This
   prints the list of instances of $n$, for which interpretations exist.
   For example, \isakeyword{print\_interps} @{term partial_order}
   outputs the following:
 \begin{small}

   ``!'' or ``?'' respectively.  Mandatory qualifiers must occur in a
   name reference while optional ones need not.  Mandatory qualifiers
   prevent accidental hiding of names, while optional qualifiers can be
   more convenient to use.  For \isakeyword{interpretation}, the
   default is ``!''.
-*}
-
-
-section {* Locale Expressions \label{sec:expressions} *}
-
-text {*
+\<close>
+
+
+section \<open>Locale Expressions \label{sec:expressions}\<close>
+
+text \<open>
   A map~@{term \<phi>} between partial orders~@{text \<sqsubseteq>} and~@{text \<preceq>}
   is called order preserving if @{text "x \<sqsubseteq> y"} implies @{text "\<phi> x \<preceq>
   \<phi> y"}.  This situation is more complex than those encountered so
   far: it involves two partial orders, and it is desirable to use the
   existing locale for both.

   clause.  The \isakeyword{for} clause is also where the syntax of these
   parameters is declared.
 
   Two context elements for the map parameter~@{text \<phi>} and the
   assumptions that it is order preserving complete the locale
-  declaration. *}
+  declaration.\<close>
 
   locale order_preserving =
     le: partial_order le + le': partial_order le'
       for le (infixl "\<sqsubseteq>" 50) and le' (infixl "\<preceq>" 50) +
     fixes \<phi>
     assumes hom_le: "x \<sqsubseteq> y \<Longrightarrow> \<phi> x \<preceq> \<phi> y"
 
-text (in order_preserving) {* Here are examples of theorems that are
+text (in order_preserving) \<open>Here are examples of theorems that are
   available in the locale:
 
   \hspace*{1em}@{thm [source] hom_le}: @{thm hom_le}
 
   \hspace*{1em}@{thm [source] le.less_le_trans}: @{thm le.less_le_trans}

   While there is infix syntax for the strict operation associated to
   @{term "op \<sqsubseteq>"}, there is none for the strict version of @{term
   "op \<preceq>"}.  The abbreviation @{text less} with its infix syntax is only
   available for the original instance it was declared for.  We may
   introduce the abbreviation @{text less'} with infix syntax~@{text \<prec>}
-  with the following declaration: *}
+  with the following declaration:\<close>
 
   abbreviation (in order_preserving)
     less' (infixl "\<prec>" 50) where "less' \<equiv> partial_order.less le'"
 
-text (in order_preserving) {* Now the theorem is displayed nicely as
+text (in order_preserving) \<open>Now the theorem is displayed nicely as
   @{thm [source]  le'.less_le_trans}:
-  @{thm [display, indent=2] le'.less_le_trans} *}
-
-text {* There are short notations for locale expressions.  These are
-  discussed in the following. *}
-
-
-subsection {* Default Instantiations *}
-
-text {* 
+  @{thm [display, indent=2] le'.less_le_trans}\<close>
+
+text \<open>There are short notations for locale expressions.  These are
+  discussed in the following.\<close>
+
+
+subsection \<open>Default Instantiations\<close>
+
+text \<open>
   It is possible to omit parameter instantiations.  The
   instantiation then defaults to the name of
   the parameter itself.  For example, the locale expression @{text
   partial_order} is short for @{text "partial_order le"}, since the
   locale's single parameter is~@{text le}.  We took advantage of this
   in the \isakeyword{sublocale} declarations of
-  Section~\ref{sec:changing-the-hierarchy}. *}
-
-
-subsection {* Implicit Parameters \label{sec:implicit-parameters} *}
-
-text {* In a locale expression that occurs within a locale
+  Section~\ref{sec:changing-the-hierarchy}.\<close>
+
+
+subsection \<open>Implicit Parameters \label{sec:implicit-parameters}\<close>
+
+text \<open>In a locale expression that occurs within a locale
   declaration, omitted parameters additionally extend the (possibly
   empty) \isakeyword{for} clause.
 
   The \isakeyword{for} clause is a general construct of Isabelle/Isar
   to mark names occurring in the preceding declaration as ``arbitrary

   partial_order le \isakeyword{for} le (\isakeyword{infixl} "\(\sqsubseteq\)" 50)\textrm{.}
 \end{alltt}
 \end{small}
   This short hand was used in the locale declarations throughout
   Section~\ref{sec:import}.
- *}
-
-text{*
+\<close>
+
+text\<open>
   The following locale declarations provide more examples.  A
   map~@{text \<phi>} is a lattice homomorphism if it preserves meet and
-  join. *}
+  join.\<close>
 
   locale lattice_hom =
     le: lattice + le': lattice le' for le' (infixl "\<preceq>" 50) +
     fixes \<phi>
     assumes hom_meet: "\<phi> (x \<sqinter> y) = le'.meet (\<phi> x) (\<phi> y)"
       and hom_join: "\<phi> (x \<squnion> y) = le'.join (\<phi> x) (\<phi> y)"
 
-text {* The parameter instantiation in the first instance of @{term
+text \<open>The parameter instantiation in the first instance of @{term
   lattice} is omitted.  This causes the parameter~@{text le} to be
   added to the \isakeyword{for} clause, and the locale has
   parameters~@{text le},~@{text le'} and, of course,~@{text \<phi>}.
 
   Before turning to the second example, we complete the locale by
   providing infix syntax for the meet and join operations of the
   second lattice.
-*}
+\<close>
 
   context lattice_hom
   begin
   abbreviation meet' (infixl "\<sqinter>''" 50) where "meet' \<equiv> le'.meet"
   abbreviation join' (infixl "\<squnion>''" 50) where "join' \<equiv> le'.join"
   end
 
-text {* The next example makes radical use of the short hand
+text \<open>The next example makes radical use of the short hand
   facilities.  A homomorphism is an endomorphism if both orders
-  coincide. *}
+  coincide.\<close>
 
   locale lattice_end = lattice_hom _ le
 
-text {* The notation~@{text _} enables to omit a parameter in a
+text \<open>The notation~@{text _} enables to omit a parameter in a
   positional instantiation.  The omitted parameter,~@{text le} becomes
   the parameter of the declared locale and is, in the following
   position, used to instantiate the second parameter of @{text
   lattice_hom}.  The effect is that of identifying the first in second
-  parameter of the homomorphism locale. *}
-
-text {* The inheritance diagram of the situation we have now is shown
+  parameter of the homomorphism locale.\<close>
+
+text \<open>The inheritance diagram of the situation we have now is shown
   in Figure~\ref{fig:hom}, where the dashed line depicts an
   interpretation which is introduced below.  Parameter instantiations
   are indicated by $\sqsubseteq \mapsto \preceq$ etc.  By looking at
   the inheritance diagram it would seem
   that two identical copies of each of the locales @{text

 \end{center}
 \hrule
 \caption{Hierarchy of Homomorphism Locales.}
 \label{fig:hom}
 \end{figure}
-  *}
-
-text {* It can be shown easily that a lattice homomorphism is order
+\<close>
+
+text \<open>It can be shown easily that a lattice homomorphism is order
   preserving.  As the final example of this section, a locale
-  interpretation is used to assert this: *}
+  interpretation is used to assert this:\<close>
 
   sublocale lattice_hom \<subseteq> order_preserving
   proof unfold_locales
     fix x y
     assume "x \<sqsubseteq> y"
     then have "y = (x \<squnion> y)" by (simp add: le.join_connection)
     then have "\<phi> y = (\<phi> x \<squnion>' \<phi> y)" by (simp add: hom_join [symmetric])
     then show "\<phi> x \<preceq> \<phi> y" by (simp add: le'.join_connection)
   qed
 
-text (in lattice_hom) {*
+text (in lattice_hom) \<open>
   Theorems and other declarations --- syntax, in particular --- from
   the locale @{text order_preserving} are now active in @{text
   lattice_hom}, for example
   @{thm [source] hom_le}:
   @{thm [display, indent=2] hom_le}
   This theorem will be useful in the following section.
-  *}
-
-
-section {* Conditional Interpretation *}
-
-text {* There are situations where an interpretation is not possible
+\<close>
+
+
+section \<open>Conditional Interpretation\<close>
+
+text \<open>There are situations where an interpretation is not possible
   in the general case since the desired property is only valid if
   certain conditions are fulfilled.  Take, for example, the function
   @{text "\<lambda>i. n * i"} that scales its argument by a constant factor.
   This function is order preserving (and even a lattice endomorphism)
   with respect to @{term "op \<le>"} provided @{text "n \<ge> 0"}.

   This is not fully satisfactory either, since potentially
   interpretations may be required to make interpretations in many
   contexts.  What is
   required is an interpretation that depends on the condition --- and
   this can be done with the \isakeyword{sublocale} command.  For this
-  purpose, we introduce a locale for the condition. *}
+  purpose, we introduce a locale for the condition.\<close>
 
   locale non_negative =
     fixes n :: int
     assumes non_neg: "0 \<le> n"
 
-text {* It is again convenient to make the interpretation in an
+text \<open>It is again convenient to make the interpretation in an
   incremental fashion, first for order preserving maps, the for
-  lattice endomorphisms. *}
+  lattice endomorphisms.\<close>
 
   sublocale non_negative \<subseteq>
       order_preserving "op \<le>" "op \<le>" "\<lambda>i. n * i"
     using non_neg by unfold_locales (rule mult_left_mono)
 
-text {* While the proof of the previous interpretation
+text \<open>While the proof of the previous interpretation
   is straightforward from monotonicity lemmas for~@{term "op *"}, the
-  second proof follows a useful pattern. *}
+  second proof follows a useful pattern.\<close>
 
   sublocale %visible non_negative \<subseteq> lattice_end "op \<le>" "\<lambda>i. n * i"
   proof (unfold_locales, unfold int_min_eq int_max_eq)
-    txt {* \normalsize Unfolding the locale predicates \emph{and} the
+    txt \<open>\normalsize Unfolding the locale predicates \emph{and} the
       interpretation equations immediately yields two subgoals that
       reflect the core conjecture.
       @{subgoals [display]}
       It is now necessary to show, in the context of @{term
       non_negative}, that multiplication by~@{term n} commutes with
-      @{term min} and @{term max}. *}
+      @{term min} and @{term max}.\<close>
   qed (auto simp: hom_le)
 
-text (in order_preserving) {* The lemma @{thm [source] hom_le}
+text (in order_preserving) \<open>The lemma @{thm [source] hom_le}
   simplifies a proof that would have otherwise been lengthy and we may
-  consider making it a default rule for the simplifier: *}
+  consider making it a default rule for the simplifier:\<close>
 
   lemmas (in order_preserving) hom_le [simp]
 
 
-subsection {* Avoiding Infinite Chains of Interpretations
-  \label{sec:infinite-chains} *}
-
-text {* Similar situations arise frequently in formalisations of
+subsection \<open>Avoiding Infinite Chains of Interpretations
+  \label{sec:infinite-chains}\<close>
+
+text \<open>Similar situations arise frequently in formalisations of
   abstract algebra where it is desirable to express that certain
   constructions preserve certain properties.  For example, polynomials
   over rings are rings, or --- an example from the domain where the
   illustrations of this tutorial are taken from --- a partial order
   may be obtained for a function space by point-wise lifting of the
   partial order of the co-domain.  This corresponds to the following
-  interpretation: *}
+  interpretation:\<close>
 
   sublocale %visible partial_order \<subseteq> f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
     oops
 
-text {* Unfortunately this is a cyclic interpretation that leads to an
+text \<open>Unfortunately this is a cyclic interpretation that leads to an
   infinite chain, namely
   @{text [display, indent=2] "partial_order \<subseteq> partial_order (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) \<subseteq>
   partial_order (\<lambda>f g. \<forall>x y. f x y \<sqsubseteq> g x y) \<subseteq>  \<dots>"}
   and the interpretation is rejected.
 
   Instead it is necessary to declare a locale that is logically
   equivalent to @{term partial_order} but serves to collect facts
   about functions spaces where the co-domain is a partial order, and
-  to make the interpretation in its context: *}
+  to make the interpretation in its context:\<close>
 
   locale fun_partial_order = partial_order
 
   sublocale fun_partial_order \<subseteq>
       f: partial_order "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
     by unfold_locales (fast,rule,fast,blast intro: trans)
 
-text {* It is quite common in abstract algebra that such a construction
+text \<open>It is quite common in abstract algebra that such a construction
   maps a hierarchy of algebraic structures (or specifications) to a
   related hierarchy.  By means of the same lifting, a function space
-  is a lattice if its co-domain is a lattice: *}
+  is a lattice if its co-domain is a lattice:\<close>
 
   locale fun_lattice = fun_partial_order + lattice
 
   sublocale fun_lattice \<subseteq> f: lattice "\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x"
   proof unfold_locales

     then show "\<exists>sup. partial_order.is_sup (\<lambda>f g. \<forall>x. f x \<sqsubseteq> g x) f g sup"
       by fast
   qed
 
 
-section {* Further Reading *}
-
-text {* More information on locales and their interpretation is
+section \<open>Further Reading\<close>
+
+text \<open>More information on locales and their interpretation is
   available.  For the locale hierarchy of import and interpretation
   dependencies see~@{cite Ballarin2006a}; interpretations in theories
   and proofs are covered in~@{cite Ballarin2006b}.  In the latter, I
   show how interpretation in proofs enables to reason about families
   of algebraic structures, which cannot be expressed with locales

   taken from Jacobson's textbook on algebra~@{cite \<open>Chapter~8\<close> Jacobson1985}.
 
   The sources of this tutorial, which include all proofs, are
   available with the Isabelle distribution at
   @{url "http://isabelle.in.tum.de"}.
-  *}
-
-text {*
+\<close>
+
+text \<open>
 \begin{table}
 \hrule
 \vspace{2ex}
 \begin{center}
 \begin{tabular}{l>$c<$l}

 \end{center}
 \hrule
 \caption{Syntax of Locale Commands.}
 \label{tab:commands}
 \end{table}
-  *}
-
-text {* \textbf{Revision History.}  For the present third revision of
+\<close>
+
+text \<open>\textbf{Revision History.}  For the present third revision of
   the tutorial, much of the explanatory text
   was rewritten.  Inheritance of interpretation equations is
   available with the forthcoming release of Isabelle, which at the
   time of editing these notes is expected for the end of 2009.
   The second revision accommodates changes introduced by the locales
   reimplementation for Isabelle 2009.  Most notably locale expressions
-  have been generalised from renaming to instantiation.  *}
-
-text {* \textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
+  have been generalised from renaming to instantiation.\<close>
+
+text \<open>\textbf{Acknowledgements.}  Alexander Krauss, Tobias Nipkow,
   Randy Pollack, Andreas Schropp, Christian Sternagel and Makarius Wenzel
   have made
   useful comments on earlier versions of this document.  The section
   on conditional interpretation was inspired by a number of e-mail
   enquiries the author received from locale users, and which suggested
   that this use case is important enough to deserve explicit
   explanation.  The term \emph{conditional interpretation} is due to
-  Larry Paulson. *}
+  Larry Paulson.\<close>
 
 end