--- 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}}