tuned
authorhaftmann
Fri Oct 10 15:52:45 2008 +0200 (2008-10-10)
changeset 28565519b17118926
parent 28564 1358b1ddd915
child 28566 be2a72b421ae
tuned
doc-src/IsarAdvanced/Classes/Thy/Classes.thy
doc-src/IsarAdvanced/Classes/Thy/ROOT.ML
doc-src/IsarAdvanced/Classes/Thy/Setup.thy
doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex
doc-src/IsarAdvanced/Classes/classes.tex
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 10 15:23:33 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Fri Oct 10 15:52:45 2008 +0200
     1.3 @@ -1,41 +1,7 @@
     1.4 -(* $Id$ *)
     1.5 -
     1.6 -(*<*)
     1.7  theory Classes
     1.8 -imports Main Code_Integer
     1.9 -uses "../../../more_antiquote"
    1.10 +imports Main Setup
    1.11  begin
    1.12  
    1.13 -ML {*
    1.14 -Code_Target.code_width := 74;
    1.15 -*}
    1.16 -
    1.17 -syntax
    1.18 -  "_alpha" :: "type"  ("\<alpha>")
    1.19 -  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
    1.20 -  "_beta" :: "type"  ("\<beta>")
    1.21 -  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
    1.22 -
    1.23 -parse_ast_translation {*
    1.24 -  let
    1.25 -    fun alpha_ast_tr [] = Syntax.Variable "'a"
    1.26 -      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    1.27 -    fun alpha_ofsort_ast_tr [ast] =
    1.28 -      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
    1.29 -      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    1.30 -    fun beta_ast_tr [] = Syntax.Variable "'b"
    1.31 -      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    1.32 -    fun beta_ofsort_ast_tr [ast] =
    1.33 -      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
    1.34 -      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    1.35 -  in [
    1.36 -    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
    1.37 -    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
    1.38 -  ] end
    1.39 -*}
    1.40 -(*>*)
    1.41 -
    1.42 -
    1.43  chapter {* Haskell-style classes with Isabelle/Isar *}
    1.44  
    1.45  section {* Introduction *}
    1.46 @@ -52,23 +18,27 @@
    1.47    of the @{text eq} function from its overloaded definitions by means
    1.48    of @{text class} and @{text instance} declarations:
    1.49  
    1.50 -  \medskip\noindent\hspace*{2ex}@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
    1.51 -  \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
    1.52 +  \begin{quote}
    1.53 +
    1.54 +  \noindent@{text "class eq where"}\footnote{syntax here is a kind of isabellized Haskell} \\
    1.55 +  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
    1.56  
    1.57 -  \medskip\noindent\hspace*{2ex}@{text "instance nat \<Colon> eq where"} \\
    1.58 -  \hspace*{4ex}@{text "eq 0 0 = True"} \\
    1.59 -  \hspace*{4ex}@{text "eq 0 _ = False"} \\
    1.60 -  \hspace*{4ex}@{text "eq _ 0 = False"} \\
    1.61 -  \hspace*{4ex}@{text "eq (Suc n) (Suc m) = eq n m"}
    1.62 +  \medskip\noindent@{text "instance nat \<Colon> eq where"} \\
    1.63 +  \hspace*{2ex}@{text "eq 0 0 = True"} \\
    1.64 +  \hspace*{2ex}@{text "eq 0 _ = False"} \\
    1.65 +  \hspace*{2ex}@{text "eq _ 0 = False"} \\
    1.66 +  \hspace*{2ex}@{text "eq (Suc n) (Suc m) = eq n m"}
    1.67  
    1.68 -  \medskip\noindent\hspace*{2ex}@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
    1.69 -  \hspace*{4ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
    1.70 +  \medskip\noindent\@{text "instance (\<alpha>\<Colon>eq, \<beta>\<Colon>eq) pair \<Colon> eq where"} \\
    1.71 +  \hspace*{2ex}@{text "eq (x1, y1) (x2, y2) = eq x1 x2 \<and> eq y1 y2"}
    1.72  
    1.73 -  \medskip\noindent\hspace*{2ex}@{text "class ord extends eq where"} \\
    1.74 -  \hspace*{4ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
    1.75 -  \hspace*{4ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
    1.76 +  \medskip\noindent@{text "class ord extends eq where"} \\
    1.77 +  \hspace*{2ex}@{text "less_eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
    1.78 +  \hspace*{2ex}@{text "less \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"}
    1.79  
    1.80 -  \medskip\noindent Type variables are annotated with (finitely many) classes;
    1.81 +  \end{quote}
    1.82 +
    1.83 +  \noindent Type variables are annotated with (finitely many) classes;
    1.84    these annotations are assertions that a particular polymorphic type
    1.85    provides definitions for overloaded functions.
    1.86  
    1.87 @@ -85,14 +55,18 @@
    1.88    @{text "class eq"} is an equivalence relation obeying reflexivity,
    1.89    symmetry and transitivity:
    1.90  
    1.91 -  \medskip\noindent\hspace*{2ex}@{text "class eq where"} \\
    1.92 -  \hspace*{4ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
    1.93 -  \hspace*{2ex}@{text "satisfying"} \\
    1.94 -  \hspace*{4ex}@{text "refl: eq x x"} \\
    1.95 -  \hspace*{4ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
    1.96 -  \hspace*{4ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
    1.97 +  \begin{quote}
    1.98  
    1.99 -  \medskip\noindent From a theoretic point of view, type classes are lightweight
   1.100 +  \noindent@{text "class eq where"} \\
   1.101 +  \hspace*{2ex}@{text "eq \<Colon> \<alpha> \<Rightarrow> \<alpha> \<Rightarrow> bool"} \\
   1.102 +  @{text "satisfying"} \\
   1.103 +  \hspace*{2ex}@{text "refl: eq x x"} \\
   1.104 +  \hspace*{2ex}@{text "sym: eq x y \<longleftrightarrow> eq x y"} \\
   1.105 +  \hspace*{2ex}@{text "trans: eq x y \<and> eq y z \<longrightarrow> eq x z"}
   1.106 +
   1.107 +  \end{quote}
   1.108 +
   1.109 +  \noindent From a theoretic point of view, type classes are lightweight
   1.110    modules; Haskell type classes may be emulated by
   1.111    SML functors \cite{classes_modules}. 
   1.112    Isabelle/Isar offers a discipline of type classes which brings
   1.113 @@ -128,22 +102,23 @@
   1.114  
   1.115  text {*
   1.116    Depending on an arbitrary type @{text "\<alpha>"}, class @{text
   1.117 -  "semigroup"} introduces a binary operator @{text "\<otimes>"} that is
   1.118 +  "semigroup"} introduces a binary operator @{text "(\<otimes>)"} that is
   1.119    assumed to be associative:
   1.120  *}
   1.121  
   1.122 -    class semigroup = type +
   1.123 -      fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
   1.124 -      assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   1.125 +class %quote semigroup = type +
   1.126 +  fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<otimes>" 70)
   1.127 +  assumes assoc: "(x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"
   1.128  
   1.129  text {*
   1.130 -  \noindent This @{text "\<CLASS>"} specification consists of two
   1.131 -  parts: the \qn{operational} part names the class parameter (@{text
   1.132 -  "\<FIXES>"}), the \qn{logical} part specifies properties on them
   1.133 -  (@{text "\<ASSUMES>"}).  The local @{text "\<FIXES>"} and @{text
   1.134 -  "\<ASSUMES>"} are lifted to the theory toplevel, yielding the global
   1.135 +  \noindent This @{command class} specification consists of two
   1.136 +  parts: the \qn{operational} part names the class parameter
   1.137 +  (@{element "fixes"}), the \qn{logical} part specifies properties on them
   1.138 +  (@{element "assumes"}).  The local @{element "fixes"} and
   1.139 +  @{element "assumes"} are lifted to the theory toplevel,
   1.140 +  yielding the global
   1.141    parameter @{term [source] "mult \<Colon> \<alpha>\<Colon>semigroup \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"} and the
   1.142 -  global theorem @{text "semigroup.assoc:"}~@{prop [source] "\<And>x y
   1.143 +  global theorem @{fact "semigroup.assoc:"}~@{prop [source] "\<And>x y
   1.144    z \<Colon> \<alpha>\<Colon>semigroup. (x \<otimes> y) \<otimes> z = x \<otimes> (y \<otimes> z)"}.
   1.145  *}
   1.146  
   1.147 @@ -151,65 +126,66 @@
   1.148  subsection {* Class instantiation \label{sec:class_inst} *}
   1.149  
   1.150  text {*
   1.151 -  The concrete type @{text "int"} is made a @{text "semigroup"}
   1.152 +  The concrete type @{typ int} is made a @{class semigroup}
   1.153    instance by providing a suitable definition for the class parameter
   1.154 -  @{text "mult"} and a proof for the specification of @{text "assoc"}.
   1.155 -  This is accomplished by the @{text "\<INSTANTIATION>"} target:
   1.156 +  @{text "(\<otimes>)"} and a proof for the specification of @{fact assoc}.
   1.157 +  This is accomplished by the @{command instantiation} target:
   1.158  *}
   1.159  
   1.160 -    instantiation int :: semigroup
   1.161 -    begin
   1.162 +instantiation %quote int :: semigroup
   1.163 +begin
   1.164  
   1.165 -    definition
   1.166 -      mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
   1.167 +definition %quote
   1.168 +  mult_int_def: "i \<otimes> j = i + (j\<Colon>int)"
   1.169  
   1.170 -    instance proof
   1.171 -      fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
   1.172 -      then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
   1.173 -	unfolding mult_int_def .
   1.174 -    qed
   1.175 +instance %quote proof
   1.176 +  fix i j k :: int have "(i + j) + k = i + (j + k)" by simp
   1.177 +  then show "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"
   1.178 +  unfolding mult_int_def .
   1.179 +qed
   1.180  
   1.181 -    end
   1.182 +end %quote
   1.183  
   1.184  text {*
   1.185 -  \noindent @{text "\<INSTANTIATION>"} allows to define class parameters
   1.186 +  \noindent @{command instantiation} allows to define class parameters
   1.187    at a particular instance using common specification tools (here,
   1.188 -  @{text "\<DEFINITION>"}).  The concluding @{text "\<INSTANCE>"}
   1.189 +  @{command definition}).  The concluding @{command instance}
   1.190    opens a proof that the given parameters actually conform
   1.191    to the class specification.  Note that the first proof step
   1.192 -  is the @{text default} method,
   1.193 -  which for such instance proofs maps to the @{text intro_classes} method.
   1.194 +  is the @{method default} method,
   1.195 +  which for such instance proofs maps to the @{method intro_classes} method.
   1.196    This boils down an instance judgement to the relevant primitive
   1.197    proof goals and should conveniently always be the first method applied
   1.198    in an instantiation proof.
   1.199  
   1.200 -  From now on, the type-checker will consider @{text "int"}
   1.201 -  as a @{text "semigroup"} automatically, i.e.\ any general results
   1.202 +  From now on, the type-checker will consider @{typ int}
   1.203 +  as a @{class semigroup} automatically, i.e.\ any general results
   1.204    are immediately available on concrete instances.
   1.205 -  \medskip Another instance of @{text "semigroup"} are the natural numbers:
   1.206 +
   1.207 +  \medskip Another instance of @{class semigroup} are the natural numbers:
   1.208  *}
   1.209  
   1.210 -    instantiation nat :: semigroup
   1.211 -    begin
   1.212 +instantiation %quote nat :: semigroup
   1.213 +begin
   1.214  
   1.215 -    primrec mult_nat where
   1.216 -      "(0\<Colon>nat) \<otimes> n = n"
   1.217 -      | "Suc m \<otimes> n = Suc (m \<otimes> n)"
   1.218 +primrec %quote mult_nat where
   1.219 +  "(0\<Colon>nat) \<otimes> n = n"
   1.220 +  | "Suc m \<otimes> n = Suc (m \<otimes> n)"
   1.221  
   1.222 -    instance proof
   1.223 -      fix m n q :: nat 
   1.224 -      show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
   1.225 -        by (induct m) auto
   1.226 -    qed
   1.227 +instance %quote proof
   1.228 +  fix m n q :: nat 
   1.229 +  show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
   1.230 +    by (induct m) auto
   1.231 +qed
   1.232  
   1.233 -    end
   1.234 +end %quote
   1.235  
   1.236  text {*
   1.237    \noindent Note the occurence of the name @{text mult_nat}
   1.238    in the primrec declaration;  by default, the local name of
   1.239    a class operation @{text f} to instantiate on type constructor
   1.240    @{text \<kappa>} are mangled as @{text f_\<kappa>}.  In case of uncertainty,
   1.241 -  these names may be inspected using the @{text "\<PRINTCONTEXT>"} command
   1.242 +  these names may be inspected using the @{command "print_context"} command
   1.243    or the corresponding ProofGeneral button.
   1.244  *}
   1.245  
   1.246 @@ -222,27 +198,27 @@
   1.247    using our simple algebra:
   1.248  *}
   1.249  
   1.250 -    instantiation * :: (semigroup, semigroup) semigroup
   1.251 -    begin
   1.252 +instantiation %quote * :: (semigroup, semigroup) semigroup
   1.253 +begin
   1.254  
   1.255 -    definition
   1.256 -      mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
   1.257 +definition %quote
   1.258 +  mult_prod_def: "p\<^isub>1 \<otimes> p\<^isub>2 = (fst p\<^isub>1 \<otimes> fst p\<^isub>2, snd p\<^isub>1 \<otimes> snd p\<^isub>2)"
   1.259  
   1.260 -    instance proof
   1.261 -      fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
   1.262 -      show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
   1.263 -	unfolding mult_prod_def by (simp add: assoc)
   1.264 -    qed      
   1.265 +instance %quote proof
   1.266 +  fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\<alpha>\<Colon>semigroup \<times> \<beta>\<Colon>semigroup"
   1.267 +  show "p\<^isub>1 \<otimes> p\<^isub>2 \<otimes> p\<^isub>3 = p\<^isub>1 \<otimes> (p\<^isub>2 \<otimes> p\<^isub>3)"
   1.268 +  unfolding mult_prod_def by (simp add: assoc)
   1.269 +qed      
   1.270  
   1.271 -    end
   1.272 +end %quote
   1.273  
   1.274  text {*
   1.275    \noindent Associativity from product semigroups is
   1.276    established using
   1.277 -  the definition of @{text \<otimes>} on products and the hypothetical
   1.278 +  the definition of @{text "(\<otimes>)"} on products and the hypothetical
   1.279    associativity of the type components;  these hypotheses
   1.280 -  are facts due to the @{text semigroup} constraints imposed
   1.281 -  on the type components by the @{text instance} proposition.
   1.282 +  are facts due to the @{class semigroup} constraints imposed
   1.283 +  on the type components by the @{command instance} proposition.
   1.284    Indeed, this pattern often occurs with parametric types
   1.285    and type classes.
   1.286  *}
   1.287 @@ -251,15 +227,15 @@
   1.288  subsection {* Subclassing *}
   1.289  
   1.290  text {*
   1.291 -  We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral)
   1.292 -  by extending @{text "semigroup"}
   1.293 -  with one additional parameter @{text "neutral"} together
   1.294 +  We define a subclass @{text monoidl} (a semigroup with a left-hand neutral)
   1.295 +  by extending @{class semigroup}
   1.296 +  with one additional parameter @{text neutral} together
   1.297    with its property:
   1.298  *}
   1.299  
   1.300 -    class monoidl = semigroup +
   1.301 -      fixes neutral :: "\<alpha>" ("\<one>")
   1.302 -      assumes neutl: "\<one> \<otimes> x = x"
   1.303 +class %quote monoidl = semigroup +
   1.304 +  fixes neutral :: "\<alpha>" ("\<one>")
   1.305 +  assumes neutl: "\<one> \<otimes> x = x"
   1.306  
   1.307  text {*
   1.308    \noindent Again, we prove some instances, by
   1.309 @@ -338,7 +314,7 @@
   1.310      end
   1.311  
   1.312  text {*
   1.313 -  \noindent To finish our small algebra example, we add a @{text "group"} class
   1.314 +  \noindent To finish our small algebra example, we add a @{text group} class
   1.315    with a corresponding instance:
   1.316  *}
   1.317  
   1.318 @@ -379,7 +355,9 @@
   1.319  text {*
   1.320    \noindent essentially introduces the locale
   1.321  *}
   1.322 -(*<*) setup {* Sign.add_path "foo" *} (*>*)
   1.323 +
   1.324 +setup %invisible {* Sign.add_path "foo" *}
   1.325 +
   1.326  locale idem =
   1.327    fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   1.328    assumes idem: "f (f x) = f x"
   1.329 @@ -401,7 +379,9 @@
   1.330  interpretation idem_class:
   1.331    idem ["f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"]
   1.332  by unfold_locales (rule idem)
   1.333 -(*<*) setup {* Sign.parent_path *} (*>*)
   1.334 +
   1.335 +setup %invisible {* Sign.parent_path *}
   1.336 +
   1.337  text {*
   1.338    This give you at hand the full power of the Isabelle module system;
   1.339    conclusions in locale @{text idem} are implicitly propagated
   1.340 @@ -429,9 +409,9 @@
   1.341      qed
   1.342  
   1.343  text {*
   1.344 -  \noindent Here the \qt{@{text "\<IN> group"}} target specification
   1.345 +  \noindent Here the \qt{@{keyword "in"} @{class group}} target specification
   1.346    indicates that the result is recorded within that context for later
   1.347 -  use.  This local theorem is also lifted to the global one @{text
   1.348 +  use.  This local theorem is also lifted to the global one @{fact
   1.349    "group.left_cancel:"} @{prop [source] "\<And>x y z \<Colon> \<alpha>\<Colon>group. x \<otimes> y = x \<otimes>
   1.350    z \<longleftrightarrow> y = z"}.  Since type @{text "int"} has been made an instance of
   1.351    @{text "group"} before, we may refer to that fact as well: @{prop
   1.352 @@ -474,15 +454,15 @@
   1.353    classes essentially correspond to functors which have
   1.354    a canonical interpretation as type classes.
   1.355    Anyway, there is also the possibility of other interpretations.
   1.356 -  For example, also @{text "list"}s form a monoid with
   1.357 -  @{term "op @"} and @{term "[]"} as operations, but it
   1.358 +  For example, also @{text list}s form a monoid with
   1.359 +  @{text append} and @{term "[]"} as operations, but it
   1.360    seems inappropriate to apply to lists
   1.361    the same operations as for genuinely algebraic types.
   1.362    In such a case, we simply can do a particular interpretation
   1.363    of monoids for lists:
   1.364  *}
   1.365  
   1.366 -    interpretation list_monoid: monoid ["op @" "[]"]
   1.367 +    interpretation list_monoid: monoid [append "[]"]
   1.368        by unfold_locales auto
   1.369  
   1.370  text {*
   1.371 @@ -497,14 +477,14 @@
   1.372        "replicate 0 _ = []"
   1.373        | "replicate (Suc n) xs = xs @ replicate n xs"
   1.374  
   1.375 -    interpretation list_monoid: monoid ["op @" "[]"] where
   1.376 -      "monoid.pow_nat (op @) [] = replicate"
   1.377 +    interpretation list_monoid: monoid [append "[]"] where
   1.378 +      "monoid.pow_nat append [] = replicate"
   1.379      proof -
   1.380 -      interpret monoid ["op @" "[]"] ..
   1.381 -      show "monoid.pow_nat (op @) [] = replicate"
   1.382 +      interpret monoid [append "[]"] ..
   1.383 +      show "monoid.pow_nat append [] = replicate"
   1.384        proof
   1.385          fix n
   1.386 -        show "monoid.pow_nat (op @) [] n = replicate n"
   1.387 +        show "monoid.pow_nat append [] n = replicate n"
   1.388            by (induct n) auto
   1.389        qed
   1.390      qed intro_locales
   1.391 @@ -571,11 +551,10 @@
   1.392    in @{text group} which uses @{text pow_nat}:
   1.393  *}
   1.394  
   1.395 -    definition (in group)
   1.396 -      pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
   1.397 -      "pow_int k x = (if k >= 0
   1.398 -        then pow_nat (nat k) x
   1.399 -        else (pow_nat (nat (- k)) x)\<div>)"
   1.400 +definition %quote (in group) pow_int :: "int \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
   1.401 +  "pow_int k x = (if k >= 0
   1.402 +    then pow_nat (nat k) x
   1.403 +    else (pow_nat (nat (- k)) x)\<div>)"
   1.404  
   1.405  text {*
   1.406    \noindent yields the global definition of
   1.407 @@ -591,15 +570,15 @@
   1.408    uniformly;  type inference resolves ambiguities.  For example:
   1.409  *}
   1.410  
   1.411 -context semigroup
   1.412 +context %quote semigroup
   1.413  begin
   1.414  
   1.415 -term "x \<otimes> y" -- {* example 1 *}
   1.416 -term "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
   1.417 +term %quote "x \<otimes> y" -- {* example 1 *}
   1.418 +term %quote "(x\<Colon>nat) \<otimes> y" -- {* example 2 *}
   1.419  
   1.420  end
   1.421  
   1.422 -term "x \<otimes> y" -- {* example 3 *}
   1.423 +term %quote "x \<otimes> y" -- {* example 3 *}
   1.424  
   1.425  text {*
   1.426    \noindent Here in example 1, the term refers to the local class operation
   1.427 @@ -614,8 +593,8 @@
   1.428  text {*
   1.429    Turning back to the first motivation for type classes,
   1.430    namely overloading, it is obvious that overloading
   1.431 -  stemming from @{text "\<CLASS>"} statements and
   1.432 -  @{text "\<INSTANTIATION>"}
   1.433 +  stemming from @{command class} statements and
   1.434 +  @{command instantiation}
   1.435    targets naturally maps to Haskell type classes.
   1.436    The code generator framework \cite{isabelle-codegen} 
   1.437    takes this into account.  Concerning target languages
   1.438 @@ -624,20 +603,19 @@
   1.439    As example, let's go back to the power function:
   1.440  *}
   1.441  
   1.442 -    definition
   1.443 -      example :: int where
   1.444 -      "example = pow_int 10 (-2)"
   1.445 +definition %quote example :: int where
   1.446 +  "example = pow_int 10 (-2)"
   1.447  
   1.448  text {*
   1.449    \noindent This maps to Haskell as:
   1.450  *}
   1.451  
   1.452 -text %quoteme {*@{code_stmts example (Haskell)}*}
   1.453 +text %quote {*@{code_stmts example (Haskell)}*}
   1.454  
   1.455  text {*
   1.456    \noindent The whole code in SML with explicit dictionary passing:
   1.457  *}
   1.458  
   1.459 -text %quoteme {*@{code_stmts example (SML)}*}
   1.460 +text %quote {*@{code_stmts example (SML)}*}
   1.461  
   1.462  end
     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/ROOT.ML	Fri Oct 10 15:23:33 2008 +0200
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/ROOT.ML	Fri Oct 10 15:52:45 2008 +0200
     2.3 @@ -1,4 +1,6 @@
     2.4  
     2.5  (* $Id$ *)
     2.6  
     2.7 +no_document use_thy "Setup";
     2.8 +
     2.9  use_thy "Classes";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Setup.thy	Fri Oct 10 15:52:45 2008 +0200
     3.3 @@ -0,0 +1,34 @@
     3.4 +theory Setup
     3.5 +imports Main Code_Integer
     3.6 +uses
     3.7 +  "../../../antiquote_setup"
     3.8 +  "../../../more_antiquote"
     3.9 +begin
    3.10 +
    3.11 +ML {* Code_Target.code_width := 74 *}
    3.12 +
    3.13 +syntax
    3.14 +  "_alpha" :: "type"  ("\<alpha>")
    3.15 +  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
    3.16 +  "_beta" :: "type"  ("\<beta>")
    3.17 +  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
    3.18 +
    3.19 +parse_ast_translation {*
    3.20 +  let
    3.21 +    fun alpha_ast_tr [] = Syntax.Variable "'a"
    3.22 +      | alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    3.23 +    fun alpha_ofsort_ast_tr [ast] =
    3.24 +      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
    3.25 +      | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
    3.26 +    fun beta_ast_tr [] = Syntax.Variable "'b"
    3.27 +      | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    3.28 +    fun beta_ofsort_ast_tr [ast] =
    3.29 +      Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
    3.30 +      | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
    3.31 +  in [
    3.32 +    ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
    3.33 +    ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
    3.34 +  ] end
    3.35 +*}
    3.36 +
    3.37 +end
    3.38 \ No newline at end of file
     4.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 15:23:33 2008 +0200
     4.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Fri Oct 10 15:52:45 2008 +0200
     4.3 @@ -3,12 +3,14 @@
     4.4  \def\isabellecontext{Classes}%
     4.5  %
     4.6  \isadelimtheory
     4.7 -\isanewline
     4.8  %
     4.9  \endisadelimtheory
    4.10  %
    4.11  \isatagtheory
    4.12 -%
    4.13 +\isacommand{theory}\isamarkupfalse%
    4.14 +\ Classes\isanewline
    4.15 +\isakeyword{imports}\ Main\ Setup\isanewline
    4.16 +\isakeyword{begin}%
    4.17  \endisatagtheory
    4.18  {\isafoldtheory}%
    4.19  %
    4.20 @@ -16,32 +18,6 @@
    4.21  %
    4.22  \endisadelimtheory
    4.23  %
    4.24 -\isadelimML
    4.25 -%
    4.26 -\endisadelimML
    4.27 -%
    4.28 -\isatagML
    4.29 -%
    4.30 -\endisatagML
    4.31 -{\isafoldML}%
    4.32 -%
    4.33 -\isadelimML
    4.34 -%
    4.35 -\endisadelimML
    4.36 -%
    4.37 -\isadelimML
    4.38 -%
    4.39 -\endisadelimML
    4.40 -%
    4.41 -\isatagML
    4.42 -%
    4.43 -\endisatagML
    4.44 -{\isafoldML}%
    4.45 -%
    4.46 -\isadelimML
    4.47 -%
    4.48 -\endisadelimML
    4.49 -%
    4.50  \isamarkupchapter{Haskell-style classes with Isabelle/Isar%
    4.51  }
    4.52  \isamarkuptrue%
    4.53 @@ -62,23 +38,27 @@
    4.54    of the \isa{eq} function from its overloaded definitions by means
    4.55    of \isa{class} and \isa{instance} declarations:
    4.56  
    4.57 -  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
    4.58 -  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    4.59 +  \begin{quote}
    4.60 +
    4.61 +  \noindent\isa{class\ eq\ where}\footnote{syntax here is a kind of isabellized Haskell} \\
    4.62 +  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    4.63  
    4.64 -  \medskip\noindent\hspace*{2ex}\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
    4.65 -  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
    4.66 -  \hspace*{4ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
    4.67 -  \hspace*{4ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
    4.68 -  \hspace*{4ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
    4.69 +  \medskip\noindent\isa{instance\ nat\ {\isasymColon}\ eq\ where} \\
    4.70 +  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isadigit{0}}\ {\isacharequal}\ True} \\
    4.71 +  \hspace*{2ex}\isa{eq\ {\isadigit{0}}\ {\isacharunderscore}\ {\isacharequal}\ False} \\
    4.72 +  \hspace*{2ex}\isa{eq\ {\isacharunderscore}\ {\isadigit{0}}\ {\isacharequal}\ False} \\
    4.73 +  \hspace*{2ex}\isa{eq\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharparenleft}Suc\ m{\isacharparenright}\ {\isacharequal}\ eq\ n\ m}
    4.74  
    4.75 -  \medskip\noindent\hspace*{2ex}\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
    4.76 -  \hspace*{4ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
    4.77 +  \medskip\noindent\\isa{instance\ {\isacharparenleft}{\isasymalpha}{\isasymColon}eq{\isacharcomma}\ {\isasymbeta}{\isasymColon}eq{\isacharparenright}\ pair\ {\isasymColon}\ eq\ where} \\
    4.78 +  \hspace*{2ex}\isa{eq\ {\isacharparenleft}x{\isadigit{1}}{\isacharcomma}\ y{\isadigit{1}}{\isacharparenright}\ {\isacharparenleft}x{\isadigit{2}}{\isacharcomma}\ y{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ eq\ x{\isadigit{1}}\ x{\isadigit{2}}\ {\isasymand}\ eq\ y{\isadigit{1}}\ y{\isadigit{2}}}
    4.79  
    4.80 -  \medskip\noindent\hspace*{2ex}\isa{class\ ord\ extends\ eq\ where} \\
    4.81 -  \hspace*{4ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
    4.82 -  \hspace*{4ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    4.83 +  \medskip\noindent\isa{class\ ord\ extends\ eq\ where} \\
    4.84 +  \hspace*{2ex}\isa{less{\isacharunderscore}eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
    4.85 +  \hspace*{2ex}\isa{less\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool}
    4.86  
    4.87 -  \medskip\noindent Type variables are annotated with (finitely many) classes;
    4.88 +  \end{quote}
    4.89 +
    4.90 +  \noindent Type variables are annotated with (finitely many) classes;
    4.91    these annotations are assertions that a particular polymorphic type
    4.92    provides definitions for overloaded functions.
    4.93  
    4.94 @@ -95,14 +75,18 @@
    4.95    \isa{class\ eq} is an equivalence relation obeying reflexivity,
    4.96    symmetry and transitivity:
    4.97  
    4.98 -  \medskip\noindent\hspace*{2ex}\isa{class\ eq\ where} \\
    4.99 -  \hspace*{4ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
   4.100 -  \hspace*{2ex}\isa{satisfying} \\
   4.101 -  \hspace*{4ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
   4.102 -  \hspace*{4ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
   4.103 -  \hspace*{4ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
   4.104 +  \begin{quote}
   4.105  
   4.106 -  \medskip\noindent From a theoretic point of view, type classes are lightweight
   4.107 +  \noindent\isa{class\ eq\ where} \\
   4.108 +  \hspace*{2ex}\isa{eq\ {\isasymColon}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ bool} \\
   4.109 +  \isa{satisfying} \\
   4.110 +  \hspace*{2ex}\isa{refl{\isacharcolon}\ eq\ x\ x} \\
   4.111 +  \hspace*{2ex}\isa{sym{\isacharcolon}\ eq\ x\ y\ {\isasymlongleftrightarrow}\ eq\ x\ y} \\
   4.112 +  \hspace*{2ex}\isa{trans{\isacharcolon}\ eq\ x\ y\ {\isasymand}\ eq\ y\ z\ {\isasymlongrightarrow}\ eq\ x\ z}
   4.113 +
   4.114 +  \end{quote}
   4.115 +
   4.116 +  \noindent From a theoretic point of view, type classes are lightweight
   4.117    modules; Haskell type classes may be emulated by
   4.118    SML functors \cite{classes_modules}. 
   4.119    Isabelle/Isar offers a discipline of type classes which brings
   4.120 @@ -142,20 +126,36 @@
   4.121  \isamarkuptrue%
   4.122  %
   4.123  \begin{isamarkuptext}%
   4.124 -Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isasymotimes}} that is
   4.125 +Depending on an arbitrary type \isa{{\isasymalpha}}, class \isa{semigroup} introduces a binary operator \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} that is
   4.126    assumed to be associative:%
   4.127  \end{isamarkuptext}%
   4.128  \isamarkuptrue%
   4.129 -\ \ \ \ \isacommand{class}\isamarkupfalse%
   4.130 +%
   4.131 +\isadelimquote
   4.132 +%
   4.133 +\endisadelimquote
   4.134 +%
   4.135 +\isatagquote
   4.136 +\isacommand{class}\isamarkupfalse%
   4.137  \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline
   4.138 -\ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
   4.139 -\ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
   4.140 +\ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
   4.141 +\ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}%
   4.142 +\endisatagquote
   4.143 +{\isafoldquote}%
   4.144 +%
   4.145 +\isadelimquote
   4.146 +%
   4.147 +\endisadelimquote
   4.148 +%
   4.149  \begin{isamarkuptext}%
   4.150 -\noindent This \isa{{\isasymCLASS}} specification consists of two
   4.151 -  parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them
   4.152 -  (\isa{{\isasymASSUMES}}).  The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global
   4.153 +\noindent This \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} specification consists of two
   4.154 +  parts: the \qn{operational} part names the class parameter
   4.155 +  (\hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}}), the \qn{logical} part specifies properties on them
   4.156 +  (\hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}).  The local \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} and
   4.157 +  \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}} are lifted to the theory toplevel,
   4.158 +  yielding the global
   4.159    parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the
   4.160 -  global theorem \isa{semigroup{\isachardot}assoc{\isacharcolon}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
   4.161 +  global theorem \hyperlink{fact.semigroup.assoc:}{\mbox{\isa{semigroup{\isachardot}assoc{\isacharcolon}}}}~\isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup{\isachardot}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequote}}.%
   4.162  \end{isamarkuptext}%
   4.163  \isamarkuptrue%
   4.164  %
   4.165 @@ -166,57 +166,57 @@
   4.166  \begin{isamarkuptext}%
   4.167  The concrete type \isa{int} is made a \isa{semigroup}
   4.168    instance by providing a suitable definition for the class parameter
   4.169 -  \isa{mult} and a proof for the specification of \isa{assoc}.
   4.170 -  This is accomplished by the \isa{{\isasymINSTANTIATION}} target:%
   4.171 +  \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} and a proof for the specification of \hyperlink{fact.assoc}{\mbox{\isa{assoc}}}.
   4.172 +  This is accomplished by the \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} target:%
   4.173  \end{isamarkuptext}%
   4.174  \isamarkuptrue%
   4.175 -\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   4.176 +%
   4.177 +\isadelimquote
   4.178 +%
   4.179 +\endisadelimquote
   4.180 +%
   4.181 +\isatagquote
   4.182 +\isacommand{instantiation}\isamarkupfalse%
   4.183  \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
   4.184 -\ \ \ \ \isakeyword{begin}\isanewline
   4.185 -\isanewline
   4.186 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   4.187 -\isanewline
   4.188 -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.189 +\isakeyword{begin}\isanewline
   4.190  \isanewline
   4.191 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
   4.192 -%
   4.193 -\isadelimproof
   4.194 -\ %
   4.195 -\endisadelimproof
   4.196 -%
   4.197 -\isatagproof
   4.198 -\isacommand{proof}\isamarkupfalse%
   4.199 +\isacommand{definition}\isamarkupfalse%
   4.200 +\isanewline
   4.201 +\ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.202  \isanewline
   4.203 -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   4.204 +\isacommand{instance}\isamarkupfalse%
   4.205 +\ \isacommand{proof}\isamarkupfalse%
   4.206 +\isanewline
   4.207 +\ \ \isacommand{fix}\isamarkupfalse%
   4.208  \ i\ j\ k\ {\isacharcolon}{\isacharcolon}\ int\ \isacommand{have}\isamarkupfalse%
   4.209  \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isacharplus}\ j{\isacharparenright}\ {\isacharplus}\ k\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j\ {\isacharplus}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
   4.210  \ simp\isanewline
   4.211 -\ \ \ \ \ \ \isacommand{then}\isamarkupfalse%
   4.212 +\ \ \isacommand{then}\isamarkupfalse%
   4.213  \ \isacommand{show}\isamarkupfalse%
   4.214  \ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.215 -\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   4.216 +\ \ \isacommand{unfolding}\isamarkupfalse%
   4.217  \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse%
   4.218  \isanewline
   4.219 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
   4.220 -%
   4.221 -\endisatagproof
   4.222 -{\isafoldproof}%
   4.223 -%
   4.224 -\isadelimproof
   4.225 -%
   4.226 -\endisadelimproof
   4.227 +\isacommand{qed}\isamarkupfalse%
   4.228  \isanewline
   4.229  \isanewline
   4.230 -\ \ \ \ \isacommand{end}\isamarkupfalse%
   4.231 +\isacommand{end}\isamarkupfalse%
   4.232 +%
   4.233 +\endisatagquote
   4.234 +{\isafoldquote}%
   4.235 +%
   4.236 +\isadelimquote
   4.237 +%
   4.238 +\endisadelimquote
   4.239  %
   4.240  \begin{isamarkuptext}%
   4.241 -\noindent \isa{{\isasymINSTANTIATION}} allows to define class parameters
   4.242 +\noindent \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}} allows to define class parameters
   4.243    at a particular instance using common specification tools (here,
   4.244 -  \isa{{\isasymDEFINITION}}).  The concluding \isa{{\isasymINSTANCE}}
   4.245 +  \hyperlink{command.definition}{\mbox{\isa{\isacommand{definition}}}}).  The concluding \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}}
   4.246    opens a proof that the given parameters actually conform
   4.247    to the class specification.  Note that the first proof step
   4.248 -  is the \isa{default} method,
   4.249 -  which for such instance proofs maps to the \isa{intro{\isacharunderscore}classes} method.
   4.250 +  is the \hyperlink{method.default}{\mbox{\isa{default}}} method,
   4.251 +  which for such instance proofs maps to the \hyperlink{method.intro-classes}{\mbox{\isa{intro{\isacharunderscore}classes}}} method.
   4.252    This boils down an instance judgement to the relevant primitive
   4.253    proof goals and should conveniently always be the first method applied
   4.254    in an instantiation proof.
   4.255 @@ -224,51 +224,52 @@
   4.256    From now on, the type-checker will consider \isa{int}
   4.257    as a \isa{semigroup} automatically, i.e.\ any general results
   4.258    are immediately available on concrete instances.
   4.259 +
   4.260    \medskip Another instance of \isa{semigroup} are the natural numbers:%
   4.261  \end{isamarkuptext}%
   4.262  \isamarkuptrue%
   4.263 -\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   4.264 -\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
   4.265 -\ \ \ \ \isakeyword{begin}\isanewline
   4.266 -\isanewline
   4.267 -\ \ \ \ \isacommand{primrec}\isamarkupfalse%
   4.268 -\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
   4.269 -\ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
   4.270 -\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.271 -\isanewline
   4.272 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
   4.273  %
   4.274 -\isadelimproof
   4.275 -\ %
   4.276 -\endisadelimproof
   4.277 +\isadelimquote
   4.278 +%
   4.279 +\endisadelimquote
   4.280  %
   4.281 -\isatagproof
   4.282 -\isacommand{proof}\isamarkupfalse%
   4.283 +\isatagquote
   4.284 +\isacommand{instantiation}\isamarkupfalse%
   4.285 +\ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
   4.286 +\isakeyword{begin}\isanewline
   4.287  \isanewline
   4.288 -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   4.289 +\isacommand{primrec}\isamarkupfalse%
   4.290 +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
   4.291 +\ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
   4.292 +\ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.293 +\isanewline
   4.294 +\isacommand{instance}\isamarkupfalse%
   4.295 +\ \isacommand{proof}\isamarkupfalse%
   4.296 +\isanewline
   4.297 +\ \ \isacommand{fix}\isamarkupfalse%
   4.298  \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
   4.299 -\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   4.300 +\ \ \isacommand{show}\isamarkupfalse%
   4.301  \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.302 -\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
   4.303 +\ \ \ \ \isacommand{by}\isamarkupfalse%
   4.304  \ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
   4.305 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
   4.306 -%
   4.307 -\endisatagproof
   4.308 -{\isafoldproof}%
   4.309 -%
   4.310 -\isadelimproof
   4.311 -%
   4.312 -\endisadelimproof
   4.313 +\isacommand{qed}\isamarkupfalse%
   4.314  \isanewline
   4.315  \isanewline
   4.316 -\ \ \ \ \isacommand{end}\isamarkupfalse%
   4.317 +\isacommand{end}\isamarkupfalse%
   4.318 +%
   4.319 +\endisatagquote
   4.320 +{\isafoldquote}%
   4.321 +%
   4.322 +\isadelimquote
   4.323 +%
   4.324 +\endisadelimquote
   4.325  %
   4.326  \begin{isamarkuptext}%
   4.327  \noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
   4.328    in the primrec declaration;  by default, the local name of
   4.329    a class operation \isa{f} to instantiate on type constructor
   4.330    \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
   4.331 -  these names may be inspected using the \isa{{\isasymPRINTCONTEXT}} command
   4.332 +  these names may be inspected using the \hyperlink{command.print-context}{\mbox{\isa{\isacommand{print{\isacharunderscore}context}}}} command
   4.333    or the corresponding ProofGeneral button.%
   4.334  \end{isamarkuptext}%
   4.335  \isamarkuptrue%
   4.336 @@ -284,49 +285,49 @@
   4.337    using our simple algebra:%
   4.338  \end{isamarkuptext}%
   4.339  \isamarkuptrue%
   4.340 -\ \ \ \ \isacommand{instantiation}\isamarkupfalse%
   4.341 -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
   4.342 -\ \ \ \ \isakeyword{begin}\isanewline
   4.343 -\isanewline
   4.344 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   4.345 -\isanewline
   4.346 -\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.347 -\isanewline
   4.348 -\ \ \ \ \isacommand{instance}\isamarkupfalse%
   4.349 +%
   4.350 +\isadelimquote
   4.351 +%
   4.352 +\endisadelimquote
   4.353  %
   4.354 -\isadelimproof
   4.355 -\ %
   4.356 -\endisadelimproof
   4.357 -%
   4.358 -\isatagproof
   4.359 -\isacommand{proof}\isamarkupfalse%
   4.360 +\isatagquote
   4.361 +\isacommand{instantiation}\isamarkupfalse%
   4.362 +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline
   4.363 +\isakeyword{begin}\isanewline
   4.364 +\isanewline
   4.365 +\isacommand{definition}\isamarkupfalse%
   4.366 +\isanewline
   4.367 +\ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isacharequal}\ {\isacharparenleft}fst\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ fst\ p\isactrlisub {\isadigit{2}}{\isacharcomma}\ snd\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ snd\ p\isactrlisub {\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.368  \isanewline
   4.369 -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   4.370 +\isacommand{instance}\isamarkupfalse%
   4.371 +\ \isacommand{proof}\isamarkupfalse%
   4.372 +\isanewline
   4.373 +\ \ \isacommand{fix}\isamarkupfalse%
   4.374  \ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline
   4.375 -\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   4.376 +\ \ \isacommand{show}\isamarkupfalse%
   4.377  \ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}\ {\isacharequal}\ p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ {\isacharparenleft}p\isactrlisub {\isadigit{2}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{3}}{\isacharparenright}{\isachardoublequoteclose}\isanewline
   4.378 -\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
   4.379 +\ \ \isacommand{unfolding}\isamarkupfalse%
   4.380  \ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
   4.381  \ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline
   4.382 -\ \ \ \ \isacommand{qed}\isamarkupfalse%
   4.383 -%
   4.384 -\endisatagproof
   4.385 -{\isafoldproof}%
   4.386 -%
   4.387 -\isadelimproof
   4.388 -%
   4.389 -\endisadelimproof
   4.390 +\isacommand{qed}\isamarkupfalse%
   4.391  \ \ \ \ \ \ \isanewline
   4.392  \isanewline
   4.393 -\ \ \ \ \isacommand{end}\isamarkupfalse%
   4.394 +\isacommand{end}\isamarkupfalse%
   4.395 +%
   4.396 +\endisatagquote
   4.397 +{\isafoldquote}%
   4.398 +%
   4.399 +\isadelimquote
   4.400 +%
   4.401 +\endisadelimquote
   4.402  %
   4.403  \begin{isamarkuptext}%
   4.404  \noindent Associativity from product semigroups is
   4.405    established using
   4.406 -  the definition of \isa{{\isasymotimes}} on products and the hypothetical
   4.407 +  the definition of \isa{{\isacharparenleft}{\isasymotimes}{\isacharparenright}} on products and the hypothetical
   4.408    associativity of the type components;  these hypotheses
   4.409    are facts due to the \isa{semigroup} constraints imposed
   4.410 -  on the type components by the \isa{instance} proposition.
   4.411 +  on the type components by the \hyperlink{command.instance}{\mbox{\isa{\isacommand{instance}}}} proposition.
   4.412    Indeed, this pattern often occurs with parametric types
   4.413    and type classes.%
   4.414  \end{isamarkuptext}%
   4.415 @@ -343,10 +344,23 @@
   4.416    with its property:%
   4.417  \end{isamarkuptext}%
   4.418  \isamarkuptrue%
   4.419 -\ \ \ \ \isacommand{class}\isamarkupfalse%
   4.420 +%
   4.421 +\isadelimquote
   4.422 +%
   4.423 +\endisadelimquote
   4.424 +%
   4.425 +\isatagquote
   4.426 +\isacommand{class}\isamarkupfalse%
   4.427  \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline
   4.428 -\ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   4.429 -\ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
   4.430 +\ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline
   4.431 +\ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}%
   4.432 +\endisatagquote
   4.433 +{\isafoldquote}%
   4.434 +%
   4.435 +\isadelimquote
   4.436 +%
   4.437 +\endisadelimquote
   4.438 +%
   4.439  \begin{isamarkuptext}%
   4.440  \noindent Again, we prove some instances, by
   4.441    providing suitable parameter definitions and proofs for the
   4.442 @@ -597,18 +611,21 @@
   4.443  \end{isamarkuptext}%
   4.444  \isamarkuptrue%
   4.445  %
   4.446 -\isadelimML
   4.447 +\isadeliminvisible
   4.448  %
   4.449 -\endisadelimML
   4.450 -%
   4.451 -\isatagML
   4.452 +\endisadeliminvisible
   4.453  %
   4.454 -\endisatagML
   4.455 -{\isafoldML}%
   4.456 +\isataginvisible
   4.457 +\isacommand{setup}\isamarkupfalse%
   4.458 +\ {\isacharverbatimopen}\ Sign{\isachardot}add{\isacharunderscore}path\ {\isachardoublequote}foo{\isachardoublequote}\ {\isacharverbatimclose}%
   4.459 +\endisataginvisible
   4.460 +{\isafoldinvisible}%
   4.461  %
   4.462 -\isadelimML
   4.463 +\isadeliminvisible
   4.464  %
   4.465 -\endisadelimML
   4.466 +\endisadeliminvisible
   4.467 +\isanewline
   4.468 +\isanewline
   4.469  \isacommand{locale}\isamarkupfalse%
   4.470  \ idem\ {\isacharequal}\isanewline
   4.471  \ \ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\isanewline
   4.472 @@ -646,21 +663,24 @@
   4.473  {\isafoldproof}%
   4.474  %
   4.475  \isadelimproof
   4.476 +\isanewline
   4.477  %
   4.478  \endisadelimproof
   4.479  %
   4.480 -\isadelimML
   4.481 +\isadeliminvisible
   4.482 +\isanewline
   4.483  %
   4.484 -\endisadelimML
   4.485 -%
   4.486 -\isatagML
   4.487 +\endisadeliminvisible
   4.488  %
   4.489 -\endisatagML
   4.490 -{\isafoldML}%
   4.491 +\isataginvisible
   4.492 +\isacommand{setup}\isamarkupfalse%
   4.493 +\ {\isacharverbatimopen}\ Sign{\isachardot}parent{\isacharunderscore}path\ {\isacharverbatimclose}%
   4.494 +\endisataginvisible
   4.495 +{\isafoldinvisible}%
   4.496  %
   4.497 -\isadelimML
   4.498 +\isadeliminvisible
   4.499  %
   4.500 -\endisadelimML
   4.501 +\endisadeliminvisible
   4.502  %
   4.503  \begin{isamarkuptext}%
   4.504  This give you at hand the full power of the Isabelle module system;
   4.505 @@ -724,9 +744,9 @@
   4.506  \endisadelimproof
   4.507  %
   4.508  \begin{isamarkuptext}%
   4.509 -\noindent Here the \qt{\isa{{\isasymIN}\ group}} target specification
   4.510 +\noindent Here the \qt{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}} \isa{group}} target specification
   4.511    indicates that the result is recorded within that context for later
   4.512 -  use.  This local theorem is also lifted to the global one \isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
   4.513 +  use.  This local theorem is also lifted to the global one \hyperlink{fact.group.left-cancel:}{\mbox{\isa{group{\isachardot}left{\isacharunderscore}cancel{\isacharcolon}}}} \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ {\isasymalpha}{\isasymColon}group{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.  Since type \isa{int} has been made an instance of
   4.514    \isa{group} before, we may refer to that fact as well: \isa{{\isachardoublequote}{\isasymAnd}x\ y\ z\ {\isasymColon}\ int{\isachardot}\ x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequote}}.%
   4.515  \end{isamarkuptext}%
   4.516  \isamarkuptrue%
   4.517 @@ -772,7 +792,7 @@
   4.518    a canonical interpretation as type classes.
   4.519    Anyway, there is also the possibility of other interpretations.
   4.520    For example, also \isa{list}s form a monoid with
   4.521 -  \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   4.522 +  \isa{append} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it
   4.523    seems inappropriate to apply to lists
   4.524    the same operations as for genuinely algebraic types.
   4.525    In such a case, we simply can do a particular interpretation
   4.526 @@ -780,7 +800,7 @@
   4.527  \end{isamarkuptext}%
   4.528  \isamarkuptrue%
   4.529  \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
   4.530 -\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
   4.531 +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline
   4.532  %
   4.533  \isadelimproof
   4.534  \ \ \ \ \ \ %
   4.535 @@ -810,8 +830,8 @@
   4.536  \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}replicate\ {\isacharparenleft}Suc\ n{\isacharparenright}\ xs\ {\isacharequal}\ xs\ {\isacharat}\ replicate\ n\ xs{\isachardoublequoteclose}\isanewline
   4.537  \isanewline
   4.538  \ \ \ \ \isacommand{interpretation}\isamarkupfalse%
   4.539 -\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
   4.540 -\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   4.541 +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline
   4.542 +\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   4.543  %
   4.544  \isadelimproof
   4.545  \ \ \ \ %
   4.546 @@ -821,16 +841,16 @@
   4.547  \isacommand{proof}\isamarkupfalse%
   4.548  \ {\isacharminus}\isanewline
   4.549  \ \ \ \ \ \ \isacommand{interpret}\isamarkupfalse%
   4.550 -\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   4.551 +\ monoid\ {\isacharbrackleft}append\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
   4.552  \isanewline
   4.553  \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   4.554 -\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   4.555 +\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline
   4.556  \ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
   4.557  \isanewline
   4.558  \ \ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
   4.559  \ n\isanewline
   4.560  \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
   4.561 -\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
   4.562 +\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ append\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline
   4.563  \ \ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
   4.564  \ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline
   4.565  \ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
   4.566 @@ -932,12 +952,24 @@
   4.567    in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:%
   4.568  \end{isamarkuptext}%
   4.569  \isamarkuptrue%
   4.570 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   4.571 -\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline
   4.572 -\ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   4.573 -\ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
   4.574 -\ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   4.575 -\ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
   4.576 +%
   4.577 +\isadelimquote
   4.578 +%
   4.579 +\endisadelimquote
   4.580 +%
   4.581 +\isatagquote
   4.582 +\isacommand{definition}\isamarkupfalse%
   4.583 +\ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
   4.584 +\ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline
   4.585 +\ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline
   4.586 +\ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}%
   4.587 +\endisatagquote
   4.588 +{\isafoldquote}%
   4.589 +%
   4.590 +\isadelimquote
   4.591 +%
   4.592 +\endisadelimquote
   4.593 +%
   4.594  \begin{isamarkuptext}%
   4.595  \noindent yields the global definition of
   4.596    \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}}
   4.597 @@ -955,6 +987,12 @@
   4.598    uniformly;  type inference resolves ambiguities.  For example:%
   4.599  \end{isamarkuptext}%
   4.600  \isamarkuptrue%
   4.601 +%
   4.602 +\isadelimquote
   4.603 +%
   4.604 +\endisadelimquote
   4.605 +%
   4.606 +\isatagquote
   4.607  \isacommand{context}\isamarkupfalse%
   4.608  \ semigroup\isanewline
   4.609  \isakeyword{begin}\isanewline
   4.610 @@ -968,16 +1006,36 @@
   4.611  \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
   4.612  \isamarkupcmt{example 2%
   4.613  }
   4.614 +%
   4.615 +\endisatagquote
   4.616 +{\isafoldquote}%
   4.617 +%
   4.618 +\isadelimquote
   4.619 +%
   4.620 +\endisadelimquote
   4.621  \isanewline
   4.622  \isanewline
   4.623  \isacommand{end}\isamarkupfalse%
   4.624  \isanewline
   4.625 +%
   4.626 +\isadelimquote
   4.627  \isanewline
   4.628 +%
   4.629 +\endisadelimquote
   4.630 +%
   4.631 +\isatagquote
   4.632  \isacommand{term}\isamarkupfalse%
   4.633  \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y{\isachardoublequoteclose}\ %
   4.634  \isamarkupcmt{example 3%
   4.635  }
   4.636  %
   4.637 +\endisatagquote
   4.638 +{\isafoldquote}%
   4.639 +%
   4.640 +\isadelimquote
   4.641 +%
   4.642 +\endisadelimquote
   4.643 +%
   4.644  \begin{isamarkuptext}%
   4.645  \noindent Here in example 1, the term refers to the local class operation
   4.646    \isa{mult\ {\isacharbrackleft}{\isasymalpha}{\isacharbrackright}}, whereas in example 2 the type constraint
   4.647 @@ -994,30 +1052,42 @@
   4.648  \begin{isamarkuptext}%
   4.649  Turning back to the first motivation for type classes,
   4.650    namely overloading, it is obvious that overloading
   4.651 -  stemming from \isa{{\isasymCLASS}} statements and
   4.652 -  \isa{{\isasymINSTANTIATION}}
   4.653 +  stemming from \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} statements and
   4.654 +  \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}
   4.655    targets naturally maps to Haskell type classes.
   4.656    The code generator framework \cite{isabelle-codegen} 
   4.657    takes this into account.  Concerning target languages
   4.658    lacking type classes (e.g.~SML), type classes
   4.659    are implemented by explicit dictionary construction.
   4.660 -  For example, lets go back to the power function:%
   4.661 +  As example, let's go back to the power function:%
   4.662  \end{isamarkuptext}%
   4.663  \isamarkuptrue%
   4.664 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
   4.665 -\isanewline
   4.666 -\ \ \ \ \ \ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
   4.667 -\ \ \ \ \ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
   4.668 +%
   4.669 +\isadelimquote
   4.670 +%
   4.671 +\endisadelimquote
   4.672 +%
   4.673 +\isatagquote
   4.674 +\isacommand{definition}\isamarkupfalse%
   4.675 +\ example\ {\isacharcolon}{\isacharcolon}\ int\ \isakeyword{where}\isanewline
   4.676 +\ \ {\isachardoublequoteopen}example\ {\isacharequal}\ pow{\isacharunderscore}int\ {\isadigit{1}}{\isadigit{0}}\ {\isacharparenleft}{\isacharminus}{\isadigit{2}}{\isacharparenright}{\isachardoublequoteclose}%
   4.677 +\endisatagquote
   4.678 +{\isafoldquote}%
   4.679 +%
   4.680 +\isadelimquote
   4.681 +%
   4.682 +\endisadelimquote
   4.683 +%
   4.684  \begin{isamarkuptext}%
   4.685  \noindent This maps to Haskell as:%
   4.686  \end{isamarkuptext}%
   4.687  \isamarkuptrue%
   4.688  %
   4.689 -\isadelimquoteme
   4.690 +\isadelimquote
   4.691  %
   4.692 -\endisadelimquoteme
   4.693 +\endisadelimquote
   4.694  %
   4.695 -\isatagquoteme
   4.696 +\isatagquote
   4.697  %
   4.698  \begin{isamarkuptext}%
   4.699  \isaverbatim%
   4.700 @@ -1088,23 +1158,23 @@
   4.701  \end{isamarkuptext}%
   4.702  \isamarkuptrue%
   4.703  %
   4.704 -\endisatagquoteme
   4.705 -{\isafoldquoteme}%
   4.706 +\endisatagquote
   4.707 +{\isafoldquote}%
   4.708  %
   4.709 -\isadelimquoteme
   4.710 +\isadelimquote
   4.711  %
   4.712 -\endisadelimquoteme
   4.713 +\endisadelimquote
   4.714  %
   4.715  \begin{isamarkuptext}%
   4.716  \noindent The whole code in SML with explicit dictionary passing:%
   4.717  \end{isamarkuptext}%
   4.718  \isamarkuptrue%
   4.719  %
   4.720 -\isadelimquoteme
   4.721 +\isadelimquote
   4.722  %
   4.723 -\endisadelimquoteme
   4.724 +\endisadelimquote
   4.725  %
   4.726 -\isatagquoteme
   4.727 +\isatagquote
   4.728  %
   4.729  \begin{isamarkuptext}%
   4.730  \isaverbatim%
   4.731 @@ -1170,12 +1240,12 @@
   4.732  \end{isamarkuptext}%
   4.733  \isamarkuptrue%
   4.734  %
   4.735 -\endisatagquoteme
   4.736 -{\isafoldquoteme}%
   4.737 +\endisatagquote
   4.738 +{\isafoldquote}%
   4.739  %
   4.740 -\isadelimquoteme
   4.741 +\isadelimquote
   4.742  %
   4.743 -\endisadelimquoteme
   4.744 +\endisadelimquote
   4.745  %
   4.746  \isadelimtheory
   4.747  %
     5.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:23:33 2008 +0200
     5.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex	Fri Oct 10 15:52:45 2008 +0200
     5.3 @@ -3,71 +3,51 @@
     5.4  
     5.5  \documentclass[12pt,a4paper,fleqn]{report}
     5.6  \usepackage{latexsym,graphicx}
     5.7 -\usepackage{listings}
     5.8  \usepackage[refpage]{nomencl}
     5.9  \usepackage{../../iman,../../extra,../../isar,../../proof}
    5.10  \usepackage{../../isabelle,../../isabellesym}
    5.11  \usepackage{style}
    5.12  \usepackage{../../pdfsetup}
    5.13  
    5.14 -\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
    5.15 -
    5.16 -\makeatletter
    5.17 -
    5.18 -\isakeeptag{quoteme}
    5.19 -\newenvironment{quoteme}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    5.20 -\renewcommand{\isatagquoteme}{\begin{quoteme}}
    5.21 -\renewcommand{\endisatagquoteme}{\end{quoteme}}
    5.22 -
    5.23 -\makeatother
    5.24 -
    5.25 -\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
    5.26 -\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
    5.27 -\renewcommand{\isasymotimes}{\isamath{\circ}}
    5.28 -
    5.29 -\newcommand{\cmd}[1]{\isacommand{#1}}
    5.30  
    5.31 -\newcommand{\isasymINFIX}{\cmd{infix}}
    5.32 -\newcommand{\isasymLOCALE}{\cmd{locale}}
    5.33 -\newcommand{\isasymINCLUDES}{\cmd{includes}}
    5.34 -\newcommand{\isasymDATATYPE}{\cmd{datatype}}
    5.35 -\newcommand{\isasymAXCLASS}{\cmd{axclass}}
    5.36 -\newcommand{\isasymFIXES}{\cmd{fixes}}
    5.37 -\newcommand{\isasymASSUMES}{\cmd{assumes}}
    5.38 -\newcommand{\isasymDEFINES}{\cmd{defines}}
    5.39 -\newcommand{\isasymNOTES}{\cmd{notes}}
    5.40 -\newcommand{\isasymSHOWS}{\cmd{shows}}
    5.41 -\newcommand{\isasymCLASS}{\cmd{class}}
    5.42 -\newcommand{\isasymINSTANCE}{\cmd{instance}}
    5.43 -\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
    5.44 -\newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}
    5.45 -\newcommand{\isasymLEMMA}{\cmd{lemma}}
    5.46 -\newcommand{\isasymPROOF}{\cmd{proof}}
    5.47 -\newcommand{\isasymQED}{\cmd{qed}}
    5.48 -\newcommand{\isasymFIX}{\cmd{fix}}
    5.49 -\newcommand{\isasymASSUME}{\cmd{assume}}
    5.50 -\newcommand{\isasymSHOW}{\cmd{show}}
    5.51 -\newcommand{\isasymNOTE}{\cmd{note}}
    5.52 +%% setup
    5.53  
    5.54 -\newcommand{\qt}[1]{``#1''}
    5.55 -\newcommand{\qtt}[1]{"{}{#1}"{}}
    5.56 -\newcommand{\qn}[1]{\emph{#1}}
    5.57 -\newcommand{\strong}[1]{{\bfseries #1}}
    5.58 -\newcommand{\fixme}[1][!]{\strong{FIXME: #1}}
    5.59 -
    5.60 -\lstset{basicstyle=\scriptsize\ttfamily,keywordstyle=\itshape,commentstyle=\itshape\sffamily,frame=single}
    5.61 -\newcommand{\lstsml}[1]{\lstset{language=ML}\lstinputlisting{#1}}
    5.62 -\newcommand{\lsthaskell}[1]{\lstset{language=Haskell}\lstinputlisting{#1}}
    5.63 -
    5.64 +% hyphenation
    5.65  \hyphenation{Isabelle}
    5.66  \hyphenation{Isar}
    5.67  
    5.68 +% logical markup
    5.69 +\newcommand{\strong}[1]{{\bfseries {#1}}}
    5.70 +\newcommand{\qn}[1]{\emph{#1}}
    5.71 +
    5.72 +% typographic conventions
    5.73 +\newcommand{\qt}[1]{``{#1}''}
    5.74 +
    5.75 +% verbatim text
    5.76 +\newcommand{\isaverbatim}{\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{8pt}\fontsize{8pt}{0pt}}
    5.77 +
    5.78 +% invisibility
    5.79  \isadroptag{theory}
    5.80 +
    5.81 +% quoted segments
    5.82 +\makeatletter
    5.83 +\isakeeptag{quote}
    5.84 +\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
    5.85 +\renewcommand{\isatagquote}{\begin{quotesegment}}
    5.86 +\renewcommand{\endisatagquote}{\end{quotesegment}}
    5.87 +\makeatother
    5.88 +
    5.89 +%\renewcommand{\isasymlongleftrightarrow}{\isamath{\leftrightarrow}}
    5.90 +%\renewcommand{\isasymdiv}{\isamath{{}^{-1}}}
    5.91 +%\renewcommand{\isasymotimes}{\isamath{\circ}}
    5.92 +
    5.93 +
    5.94 +%% content
    5.95 +
    5.96  \title{\includegraphics[scale=0.5]{isabelle_isar}
    5.97    \\[4ex] Haskell-style type classes with Isabelle/Isar}
    5.98  \author{\emph{Florian Haftmann}}
    5.99  
   5.100 -
   5.101  \begin{document}
   5.102  
   5.103  \maketitle