1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Jan 09 08:32:09 2008 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Jan 09 08:33:01 2008 +0100
     1.3 @@ -191,17 +191,27 @@
     1.4      instantiation nat :: semigroup
     1.5      begin
     1.6  
     1.7 -    definition
     1.8 -      mult_nat_def: "m \<otimes> n = m + (n\<Colon>nat)"
     1.9 +    primrec mult_nat where
    1.10 +      "(0\<Colon>nat) \<otimes> n = n"
    1.11 +      | "Suc m \<otimes> n = Suc (m \<otimes> n)"
    1.12  
    1.13      instance proof
    1.14        fix m n q :: nat 
    1.15        show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
    1.16 -	unfolding mult_nat_def by simp
    1.17 +        by (induct m) auto
    1.18      qed
    1.19  
    1.20      end
    1.21  
    1.22 +text {*
    1.23 +  \noindent Note the occurence of the name @{text mult_nat}
    1.24 +  in the primrec declaration;  by default, the local name of
    1.25 +  a class operation @{text f} to instantiate on type constructor
    1.26 +  @{text \<kappa>} are mangled as @{text f_\<kappa>}.  In case of uncertainty,
    1.27 +  these names may be inspected using the @{text "\<PRINTCONTEXT>"} command
    1.28 +  or the corresponding ProofGeneral button.
    1.29 +*}
    1.30 +
    1.31  subsection {* Lifting and parametric types *}
    1.32  
    1.33  text {*
    1.34 @@ -306,7 +316,7 @@
    1.35      instance proof
    1.36        fix n :: nat
    1.37        show "n \<otimes> \<one> = n"
    1.38 -	unfolding neutral_nat_def mult_nat_def by simp
    1.39 +	unfolding neutral_nat_def by (induct n) simp_all
    1.40      next
    1.41        fix k :: int
    1.42        show "k \<otimes> \<one> = k"
    1.43 @@ -435,7 +445,7 @@
    1.44    in locales:
    1.45  *}
    1.46  
    1.47 -    fun (in monoid)
    1.48 +    primrec (in monoid)
    1.49        pow_nat :: "nat \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>" where
    1.50        "pow_nat 0 x = \<one>"
    1.51        | "pow_nat (Suc n) x = x \<otimes> pow_nat n x"

     2.1 --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Wed Jan 09 08:32:09 2008 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Wed Jan 09 08:33:01 2008 +0100
     2.3 @@ -231,9 +231,10 @@
     2.4  \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
     2.5  \ \ \ \ \isakeyword{begin}\isanewline
     2.6  \isanewline
     2.7 -\ \ \ \ \isacommand{definition}\isamarkupfalse%
     2.8 -\isanewline
     2.9 -\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.10 +\ \ \ \ \isacommand{primrec}\isamarkupfalse%
    2.11 +\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
    2.12 +\ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
    2.13 +\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.14  \isanewline
    2.15  \ \ \ \ \isacommand{instance}\isamarkupfalse%
    2.16  %
    2.17 @@ -248,9 +249,8 @@
    2.18  \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
    2.19  \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
    2.20  \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
    2.21 -\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
    2.22 -\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
    2.23 -\ simp\isanewline
    2.24 +\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
    2.25 +\ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
    2.26  \ \ \ \ \isacommand{qed}\isamarkupfalse%
    2.27  %
    2.28  \endisatagproof
    2.29 @@ -263,6 +263,16 @@
    2.30  \isanewline
    2.31  \ \ \ \ \isacommand{end}\isamarkupfalse%
    2.32  %
    2.33 +\begin{isamarkuptext}%
    2.34 +\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
    2.35 +  in the primrec declaration;  by default, the local name of
    2.36 +  a class operation \isa{f} to instantiate on type constructor
    2.37 +  \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
    2.38 +  these names may be inspected using the \isa{{\isasymPRINTCONTEXT}} command
    2.39 +  or the corresponding ProofGeneral button.%
    2.40 +\end{isamarkuptext}%
    2.41 +\isamarkuptrue%
    2.42 +%
    2.43  \isamarkupsubsection{Lifting and parametric types%
    2.44  }
    2.45  \isamarkuptrue%
    2.46 @@ -457,8 +467,8 @@
    2.47  \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
    2.48  \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
    2.49  \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
    2.50 -\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
    2.51 -\ simp\isanewline
    2.52 +\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
    2.53 +\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
    2.54  \ \ \ \ \isacommand{next}\isamarkupfalse%
    2.55  \isanewline
    2.56  \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
    2.57 @@ -730,7 +740,7 @@
    2.58    in locales:%
    2.59  \end{isamarkuptext}%
    2.60  \isamarkuptrue%
    2.61 -\ \ \ \ \isacommand{fun}\isamarkupfalse%
    2.62 +\ \ \ \ \isacommand{primrec}\isamarkupfalse%
    2.63  \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
    2.64  \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
    2.65  \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline

     3.1 --- a/doc-src/IsarAdvanced/Classes/classes.tex	Wed Jan 09 08:32:09 2008 +0100
     3.2 +++ b/doc-src/IsarAdvanced/Classes/classes.tex	Wed Jan 09 08:33:01 2008 +0100
     3.3 @@ -29,6 +29,7 @@
     3.4  \newcommand{\isasymCLASS}{\cmd{class}}
     3.5  \newcommand{\isasymINSTANCE}{\cmd{instance}}
     3.6  \newcommand{\isasymINSTANTIATION}{\cmd{instantiation}}
     3.7 +\newcommand{\isasymPRINTCONTEXT}{\cmd{print-context}}
     3.8  \newcommand{\isasymLEMMA}{\cmd{lemma}}
     3.9  \newcommand{\isasymPROOF}{\cmd{proof}}
    3.10  \newcommand{\isasymQED}{\cmd{qed}}