some more primrec

--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Jan 09 08:32:09 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Wed Jan 09 08:33:01 2008 +0100
@@ -191,17 +191,27 @@
     instantiation nat :: semigroup
     begin
 
-    definition
-      mult_nat_def: "m \<otimes> n = m + (n\<Colon>nat)"
+    primrec mult_nat where
+      "(0\<Colon>nat) \<otimes> n = n"
+      | "Suc m \<otimes> n = Suc (m \<otimes> n)"
 
     instance proof
       fix m n q :: nat 
       show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)"
-	unfolding mult_nat_def by simp
+        by (induct m) auto
     qed
 
     end
 
+text {*
+  \noindent Note the occurence of the name @{text mult_nat}
+  in the primrec declaration;  by default, the local name of
+  a class operation @{text f} to instantiate on type constructor
+  @{text \<kappa>} are mangled as @{text f_\<kappa>}.  In case of uncertainty,
+  these names may be inspected using the @{text "\<PRINTCONTEXT>"} command
+  or the corresponding ProofGeneral button.
+*}
+
 subsection {* Lifting and parametric types *}
 
 text {*
@@ -306,7 +316,7 @@
     instance proof
       fix n :: nat
       show "n \<otimes> \<one> = n"
-	unfolding neutral_nat_def mult_nat_def by simp
+	unfolding neutral_nat_def by (induct n) simp_all
     next
       fix k :: int
       show "k \<otimes> \<one> = k"
@@ -435,7 +445,7 @@
   in locales:
 *}
 
-    fun (in monoid)
+    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"

--- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Wed Jan 09 08:32:09 2008 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex	Wed Jan 09 08:33:01 2008 +0100
@@ -231,9 +231,10 @@
 \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline
 \ \ \ \ \isakeyword{begin}\isanewline
 \isanewline
-\ \ \ \ \isacommand{definition}\isamarkupfalse%
-\isanewline
-\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isacharequal}\ m\ {\isacharplus}\ {\isacharparenleft}n{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{primrec}\isamarkupfalse%
+\ mult{\isacharunderscore}nat\ \isakeyword{where}\isanewline
+\ \ \ \ \ \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}Suc\ m\ {\isasymotimes}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}m\ {\isasymotimes}\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
 \isanewline
 \ \ \ \ \isacommand{instance}\isamarkupfalse%
 %
@@ -248,9 +249,8 @@
 \ m\ n\ q\ {\isacharcolon}{\isacharcolon}\ nat\ \isanewline
 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymotimes}\ q\ {\isacharequal}\ m\ {\isasymotimes}\ {\isacharparenleft}n\ {\isasymotimes}\ q{\isacharparenright}{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
+\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ m{\isacharparenright}\ auto\isanewline
 \ \ \ \ \isacommand{qed}\isamarkupfalse%
 %
 \endisatagproof
@@ -263,6 +263,16 @@
 \isanewline
 \ \ \ \ \isacommand{end}\isamarkupfalse%
 %
+\begin{isamarkuptext}%
+\noindent Note the occurence of the name \isa{mult{\isacharunderscore}nat}
+  in the primrec declaration;  by default, the local name of
+  a class operation \isa{f} to instantiate on type constructor
+  \isa{{\isasymkappa}} are mangled as \isa{f{\isacharunderscore}{\isasymkappa}}.  In case of uncertainty,
+  these names may be inspected using the \isa{{\isasymPRINTCONTEXT}} command
+  or the corresponding ProofGeneral button.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
 \isamarkupsubsection{Lifting and parametric types%
 }
 \isamarkuptrue%
@@ -457,8 +467,8 @@
 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
 \ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline
 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse%
-\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
-\ simp\isanewline
+\ neutral{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
 \ \ \ \ \isacommand{next}\isamarkupfalse%
 \isanewline
 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
@@ -730,7 +740,7 @@
   in locales:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\ \ \ \ \isacommand{fun}\isamarkupfalse%
+\ \ \ \ \isacommand{primrec}\isamarkupfalse%
 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline
 \ \ \ \ \ \ 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

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