tuned

--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu Oct 09 09:18:32 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Thu Oct 09 18:16:07 2008 +0200
@@ -3,10 +3,11 @@
 (*<*)
 theory Classes
 imports Main Code_Integer
+uses "../../../more_antiquote"
 begin
 
 ML {*
-CodeTarget.code_width := 74;
+Code_Target.code_width := 74;
 *}
 
 syntax
@@ -75,8 +76,8 @@
   but form a generic calculus, an instance of order-sorted
   algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
 
-  From a software engineering point of view, type classes
-  correspond to interfaces in object-oriented languages like Java;
+  From a software engeneering point of view, type classes
+  roughly correspond to interfaces in object-oriented languages like Java;
   so, it is naturally desirable that type classes do not only
   provide functions (class parameters) but also state specifications
   implementations must obey.  For example, the @{text "class eq"}
@@ -100,7 +101,7 @@
   \begin{enumerate}
     \item specifying abstract parameters together with
        corresponding specifications,
-    \item instantating those abstract parameters by a particular
+    \item instantiating those abstract parameters by a particular
        type
     \item in connection with a ``less ad-hoc'' approach to overloading,
     \item with a direct link to the Isabelle module system
@@ -445,8 +446,7 @@
   in locales:
 *}
 
-    primrec (in monoid)
-      pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
+    primrec (in monoid) pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
       "pow_nat 0 x = \<one>"
       | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"
 
@@ -493,19 +493,21 @@
   be appropriate to map derived definitions accordingly:
 *}
 
-    fun
-      replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list"
-    where
+    fun replicate :: "nat \<Rightarrow> \<alpha> list \<Rightarrow> \<alpha> list" where
       "replicate 0 _ = []"
       | "replicate (Suc n) xs = xs @ replicate n xs"
 
     interpretation list_monoid: monoid ["op @" "[]"] where
       "monoid.pow_nat (op @) [] = replicate"
-    proof
-      fix n :: nat
-      show "monoid.pow_nat (op @) [] n = replicate n"
-	by (induct n) auto
-    qed
+    proof -
+      interpret monoid ["op @" "[]"] ..
+      show "monoid.pow_nat (op @) [] = replicate"
+      proof
+        fix n
+        show "monoid.pow_nat (op @) [] n = replicate n"
+          by (induct n) auto
+      qed
+    qed intro_locales
 
 
 subsection {* Additional subclass relations *}
@@ -619,7 +621,7 @@
   takes this into account.  Concerning target languages
   lacking type classes (e.g.~SML), type classes
   are implemented by explicit dictionary construction.
-  For example, lets go back to the power function:
+  As example, let's go back to the power function:
 *}
 
     definition
@@ -630,29 +632,12 @@
   \noindent This maps to Haskell as:
 *}
 
-export_code example in Haskell module_name Classes file "code_examples/"
-  (* NOTE: you may use Haskell only once in this document, otherwise
-  you have to work in distinct subdirectories *)
+text %quoteme {*@{code_stmts example (Haskell)}*}
 
 text {*
-  \lsthaskell{Thy/code_examples/Classes.hs}
-
   \noindent The whole code in SML with explicit dictionary passing:
 *}
 
-export_code example (*<*)in SML module_name Classes(*>*)in SML module_name Classes file "code_examples/classes.ML"
-
-text {*
-  \lstsml{Thy/code_examples/classes.ML}
-*}
-
-
-(* subsection {* Different syntax for same specifications *}
-
-text {*
-
-subsection {* Syntactic classes *}
-
-*} *)
+text %quoteme {*@{code_stmts example (SML)}*}
 
 end

--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/Classes.hs	Thu Oct 09 09:18:32 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-module Classes where {
-
-
-data Nat = Suc Nat | Zero_nat;
-
-nat_aux :: Integer -> Nat -> Nat;
-nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));
-
-nat :: Integer -> Nat;
-nat i = nat_aux i Zero_nat;
-
-class Semigroup a where {
-  mult :: a -> a -> a;
-};
-
-class (Semigroup a) => Monoidl a where {
-  neutral :: a;
-};
-
-class (Monoidl a) => Monoid a where {
-};
-
-class (Monoid a) => Group a where {
-  inverse :: a -> a;
-};
-
-inverse_int :: Integer -> Integer;
-inverse_int i = negate i;
-
-neutral_int :: Integer;
-neutral_int = 0;
-
-mult_int :: Integer -> Integer -> Integer;
-mult_int i j = i + j;
-
-instance Semigroup Integer where {
-  mult = mult_int;
-};
-
-instance Monoidl Integer where {
-  neutral = neutral_int;
-};
-
-instance Monoid Integer where {
-};
-
-instance Group Integer where {
-  inverse = inverse_int;
-};
-
-pow_nat :: forall a. (Monoid a) => Nat -> a -> a;
-pow_nat (Suc n) x = mult x (pow_nat n x);
-pow_nat Zero_nat x = neutral;
-
-pow_int :: forall a. (Group a) => Integer -> a -> a;
-pow_int k x =
-  (if 0 <= k then pow_nat (nat k) x
-    else inverse (pow_nat (nat (negate k)) x));
-
-example :: Integer;
-example = pow_int 10 (-2);
-
-}

--- a/doc-src/IsarAdvanced/Classes/Thy/code_examples/classes.ML	Thu Oct 09 09:18:32 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,58 +0,0 @@
-structure Classes = 
-struct
-
-datatype nat = Suc of nat | Zero_nat;
-
-fun nat_aux i n =
-  (if IntInf.<= (i, (0 : IntInf.int)) then n
-    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));
-
-fun nat i = nat_aux i Zero_nat;
-
-type 'a semigroup = {mult : 'a -> 'a -> 'a};
-fun mult (A_:'a semigroup) = #mult A_;
-
-type 'a monoidl =
-  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};
-fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;
-fun neutral (A_:'a monoidl) = #neutral A_;
-
-type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};
-fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;
-
-type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};
-fun monoid_group (A_:'a group) = #Classes__monoid_group A_;
-fun inverse (A_:'a group) = #inverse A_;
-
-fun inverse_int i = IntInf.~ i;
-
-val neutral_int : IntInf.int = (0 : IntInf.int);
-
-fun mult_int i j = IntInf.+ (i, j);
-
-val semigroup_int = {mult = mult_int} : IntInf.int semigroup;
-
-val monoidl_int =
-  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :
-  IntInf.int monoidl;
-
-val monoid_int = {Classes__monoidl_monoid = monoidl_int} :
-  IntInf.int monoid;
-
-val group_int =
-  {Classes__monoid_group = monoid_int, inverse = inverse_int} :
-  IntInf.int group;
-
-fun pow_nat A_ (Suc n) x =
-  mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x)
-  | pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_);
-
-fun pow_int A_ k x =
-  (if IntInf.<= ((0 : IntInf.int), k)
-    then pow_nat (monoid_group A_) (nat k) x
-    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));
-
-val example : IntInf.int =
-  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);
-
-end; (*struct Classes*)

--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Oct 09 09:18:32 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Thu Oct 09 18:16:07 2008 +0200
@@ -86,8 +86,8 @@
   but form a generic calculus, an instance of order-sorted
   algebra \cite{Nipkow-Prehofer:1993,nipkow-sorts93,Wenzel:1997:TPHOL}.
 
-  From a software engineering point of view, type classes
-  correspond to interfaces in object-oriented languages like Java;
+  From a software engeneering point of view, type classes
+  roughly correspond to interfaces in object-oriented languages like Java;
   so, it is naturally desirable that type classes do not only
   provide functions (class parameters) but also state specifications
   implementations must obey.  For example, the \isa{class\ eq}
@@ -111,7 +111,7 @@
   \begin{enumerate}
     \item specifying abstract parameters together with
        corresponding specifications,
-    \item instantating those abstract parameters by a particular
+    \item instantiating those abstract parameters by a particular
        type
     \item in connection with a ``less ad-hoc'' approach to overloading,
     \item with a direct link to the Isabelle module system
@@ -741,8 +741,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{primrec}\isamarkupfalse%
-\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
-\ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
+\ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
@@ -806,9 +805,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 \ \ \ \ \isacommand{fun}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\isanewline
-\ \ \ \ \isakeyword{where}\isanewline
+\ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
 \ \ \ \ \ \ {\isachardoublequoteopen}replicate\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
 \isanewline
@@ -822,15 +819,24 @@
 %
 \isatagproof
 \isacommand{proof}\isamarkupfalse%
+\ {\isacharminus}\isanewline
+\ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
+\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
 \isanewline
-\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
-\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline
 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ n\isanewline
+\ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
 \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
+\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
+\isanewline
 \ \ \ \ \isacommand{qed}\isamarkupfalse%
-%
+\ intro{\isacharunderscore}locales%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -1006,21 +1012,171 @@
 \noindent This maps to Haskell as:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
-\ example\ \isakeyword{in}\ Haskell\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}{\isachardoublequoteclose}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
 \begin{isamarkuptext}%
-\lsthaskell{Thy/code_examples/Classes.hs}
-
-  \noindent The whole code in SML with explicit dictionary passing:%
+\isaverbatim%
+\noindent%
+\verb|module Example where {|\newline%
+\newline%
+\newline%
+\verb|data Nat = Suc Nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|nat_aux :: Integer -> Nat -> Nat;|\newline%
+\verb|nat_aux i n = (if i <= 0 then n else nat_aux (i - 1) (Suc n));|\newline%
+\newline%
+\verb|nat :: Integer -> Nat;|\newline%
+\verb|nat i = nat_aux i Zero_nat;|\newline%
+\newline%
+\verb|class Semigroup a where {|\newline%
+\verb|  mult :: a -> a -> a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|class (Semigroup a) => Monoidl a where {|\newline%
+\verb|  neutral :: a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|class (Monoidl a) => Monoid a where {|\newline%
+\verb|};|\newline%
+\newline%
+\verb|class (Monoid a) => Group a where {|\newline%
+\verb|  inverse :: a -> a;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|inverse_int :: Integer -> Integer;|\newline%
+\verb|inverse_int i = negate i;|\newline%
+\newline%
+\verb|neutral_int :: Integer;|\newline%
+\verb|neutral_int = 0;|\newline%
+\newline%
+\verb|mult_int :: Integer -> Integer -> Integer;|\newline%
+\verb|mult_int i j = i + j;|\newline%
+\newline%
+\verb|instance Semigroup Integer where {|\newline%
+\verb|  mult = mult_int;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|instance Monoidl Integer where {|\newline%
+\verb|  neutral = neutral_int;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|instance Monoid Integer where {|\newline%
+\verb|};|\newline%
+\newline%
+\verb|instance Group Integer where {|\newline%
+\verb|  inverse = inverse_int;|\newline%
+\verb|};|\newline%
+\newline%
+\verb|pow_nat :: forall a. (Monoid a) => Nat -> a -> a;|\newline%
+\verb|pow_nat Zero_nat x = neutral;|\newline%
+\verb|pow_nat (Suc n) x = mult x (pow_nat n x);|\newline%
+\newline%
+\verb|pow_int :: forall a. (Group a) => Integer -> a -> a;|\newline%
+\verb|pow_int k x =|\newline%
+\verb|  (if 0 <= k then pow_nat (nat k) x|\newline%
+\verb|    else inverse (pow_nat (nat (negate k)) x));|\newline%
+\newline%
+\verb|example :: Integer;|\newline%
+\verb|example = pow_int 10 (-2);|\newline%
+\newline%
+\verb|}|%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{export{\isacharunderscore}code}\isamarkupfalse%
-\ example\ \isakeyword{in}\ SML\ \isakeyword{module{\isacharunderscore}name}\ Classes\ \isakeyword{file}\ {\isachardoublequoteopen}code{\isacharunderscore}examples{\isacharslash}classes{\isachardot}ML{\isachardoublequoteclose}%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
 \begin{isamarkuptext}%
-\lstsml{Thy/code_examples/classes.ML}%
+\noindent The whole code in SML with explicit dictionary passing:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
+\isatagquoteme
+%
+\begin{isamarkuptext}%
+\isaverbatim%
+\noindent%
+\verb|structure Example = |\newline%
+\verb|struct|\newline%
+\newline%
+\verb|datatype nat = Suc of nat |\verb,|,\verb| Zero_nat;|\newline%
+\newline%
+\verb|fun nat_aux i n =|\newline%
+\verb|  (if IntInf.<= (i, (0 : IntInf.int)) then n|\newline%
+\verb|    else nat_aux (IntInf.- (i, (1 : IntInf.int))) (Suc n));|\newline%
+\newline%
+\verb|fun nat i = nat_aux i Zero_nat;|\newline%
+\newline%
+\verb|type 'a semigroup = {mult : 'a -> 'a -> 'a};|\newline%
+\verb|fun mult (A_:'a semigroup) = #mult A_;|\newline%
+\newline%
+\verb|type 'a monoidl =|\newline%
+\verb|  {Classes__semigroup_monoidl : 'a semigroup, neutral : 'a};|\newline%
+\verb|fun semigroup_monoidl (A_:'a monoidl) = #Classes__semigroup_monoidl A_;|\newline%
+\verb|fun neutral (A_:'a monoidl) = #neutral A_;|\newline%
+\newline%
+\verb|type 'a monoid = {Classes__monoidl_monoid : 'a monoidl};|\newline%
+\verb|fun monoidl_monoid (A_:'a monoid) = #Classes__monoidl_monoid A_;|\newline%
+\newline%
+\verb|type 'a group = {Classes__monoid_group : 'a monoid, inverse : 'a -> 'a};|\newline%
+\verb|fun monoid_group (A_:'a group) = #Classes__monoid_group A_;|\newline%
+\verb|fun inverse (A_:'a group) = #inverse A_;|\newline%
+\newline%
+\verb|fun inverse_int i = IntInf.~ i;|\newline%
+\newline%
+\verb|val neutral_int : IntInf.int = (0 : IntInf.int);|\newline%
+\newline%
+\verb|fun mult_int i j = IntInf.+ (i, j);|\newline%
+\newline%
+\verb|val semigroup_int = {mult = mult_int} : IntInf.int semigroup;|\newline%
+\newline%
+\verb|val monoidl_int =|\newline%
+\verb|  {Classes__semigroup_monoidl = semigroup_int, neutral = neutral_int} :|\newline%
+\verb|  IntInf.int monoidl;|\newline%
+\newline%
+\verb|val monoid_int = {Classes__monoidl_monoid = monoidl_int} :|\newline%
+\verb|  IntInf.int monoid;|\newline%
+\newline%
+\verb|val group_int =|\newline%
+\verb|  {Classes__monoid_group = monoid_int, inverse = inverse_int} :|\newline%
+\verb|  IntInf.int group;|\newline%
+\newline%
+\verb|fun pow_nat A_ Zero_nat x = neutral (monoidl_monoid A_)|\newline%
+\verb|  |\verb,|,\verb| pow_nat A_ (Suc n) x =|\newline%
+\verb|    mult ((semigroup_monoidl o monoidl_monoid) A_) x (pow_nat A_ n x);|\newline%
+\newline%
+\verb|fun pow_int A_ k x =|\newline%
+\verb|  (if IntInf.<= ((0 : IntInf.int), k)|\newline%
+\verb|    then pow_nat (monoid_group A_) (nat k) x|\newline%
+\verb|    else inverse A_ (pow_nat (monoid_group A_) (nat (IntInf.~ k)) x));|\newline%
+\newline%
+\verb|val example : IntInf.int =|\newline%
+\verb|  pow_int group_int (10 : IntInf.int) (~2 : IntInf.int);|\newline%
+\newline%
+\verb|end; (*struct Example*)|%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\endisatagquoteme
+{\isafoldquoteme}%
+%
+\isadelimquoteme
+%
+\endisadelimquoteme
+%
 \isadelimtheory
 %
 \endisadelimtheory

--- a/doc-src/IsarAdvanced/Classes/classes.tex	Thu Oct 09 09:18:32 2008 +0200
+++ b/doc-src/IsarAdvanced/Classes/classes.tex	Thu Oct 09 18:16:07 2008 +0200
@@ -10,6 +10,17 @@
 \usepackage{style}
 \usepackage{../../pdfsetup}
 
+\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
+
+\makeatletter
+
+\isakeeptag{quoteme}
+\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
+\renewcommand{\isatagquoteme}{\begin{quoteme}}
+\renewcommand{\endisatagquoteme}{\end{quoteme}}
+
+\makeatother
+
 \renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
 \renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
 \renewcommand{\isasymotimes}{\isamath{\circ}}