# HG changeset patch # User haftmann # Date 1196860539 -3600 # Node ID 0140cc7b26ad7a6e525d05e121be91b45944e443 # Parent 27f6771ae8fb28aca48cabf2a5ea3430cbe5bb43 added something about instantiation target diff -r 27f6771ae8fb -r 0140cc7b26ad doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Dec 05 04:34:15 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Dec 05 14:15:39 2007 +0100 @@ -12,6 +12,8 @@ syntax "_alpha" :: "type" ("\") "_alpha_ofsort" :: "sort \ type" ("\()\_" [0] 1000) + "_beta" :: "type" ("\") + "_beta_ofsort" :: "sort \ type" ("\()\_" [0] 1000) parse_ast_translation {* let @@ -20,8 +22,14 @@ fun alpha_ofsort_ast_tr [ast] = Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast] | alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts); + fun beta_ast_tr [] = Syntax.Variable "'b" + | beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); + fun beta_ofsort_ast_tr [ast] = + Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast] + | beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts); in [ - ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr) + ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr), + ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr) ] end *} (*>*) @@ -145,38 +153,54 @@ The concrete type @{text "int"} is made a @{text "semigroup"} instance by providing a suitable definition for the class parameter @{text "mult"} and a proof for the specification of @{text "assoc"}. + This is accomplished by the @{text "\"} target: *} - instance int :: semigroup - mult_int_def: "i \ j \ i + j" - proof + instantiation int :: semigroup + begin + + definition + mult_int_def: "i \ j = i + (j\int)" + + instance proof fix i j k :: int have "(i + j) + k = i + (j + k)" by simp then show "(i \ j) \ k = i \ (j \ k)" unfolding mult_int_def . qed + end + text {* - \noindent From now on, the type-checker will consider @{text "int"} - as a @{text "semigroup"} automatically, i.e.\ any general results - are immediately available on concrete instances. - - Note that the first proof step is the @{text default} method, - which for instantiation proofs maps to the @{text intro_classes} method. - This boils down an instantiation judgement to the relevant primitive + \noindent @{text "\"} allows to define class parameters + at a particular instance using common specification tools (here, + @{text "\"}). The concluding @{text "\"} + opens a proof that the given parameters actually conform + to the class specification. Note that the first proof step + is the @{text default} method, + which for such instance proofs maps to the @{text intro_classes} method. + This boils down an instance judgement to the relevant primitive proof goals and should conveniently always be the first method applied in an instantiation proof. + From now on, the type-checker will consider @{text "int"} + as a @{text "semigroup"} automatically, i.e.\ any general results + are immediately available on concrete instances. \medskip Another instance of @{text "semigroup"} are the natural numbers: *} - instance nat :: semigroup - mult_nat_def: "m \ n \ m + n" - proof + instantiation nat :: semigroup + begin + + definition + mult_nat_def: "m \ n = m + (n\nat)" + + instance proof fix m n q :: nat show "m \ n \ q = m \ (n \ q)" unfolding mult_nat_def by simp qed + end subsection {* Lifting and parametric types *} @@ -187,14 +211,20 @@ using our simple algebra: *} - instance * :: (semigroup, semigroup) semigroup - mult_prod_def: "p\<^isub>1 \ p\<^isub>2 \ (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" - proof - fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "'a\semigroup \ 'b\semigroup" + instantiation * :: (semigroup, semigroup) semigroup + begin + + definition + mult_prod_def: "p\<^isub>1 \ p\<^isub>2 = (fst p\<^isub>1 \ fst p\<^isub>2, snd p\<^isub>1 \ snd p\<^isub>2)" + + instance proof + fix p\<^isub>1 p\<^isub>2 p\<^isub>3 :: "\\semigroup \ \\semigroup" show "p\<^isub>1 \ p\<^isub>2 \ p\<^isub>3 = p\<^isub>1 \ (p\<^isub>2 \ p\<^isub>3)" unfolding mult_prod_def by (simp add: assoc) qed + end + text {* \noindent Associativity from product semigroups is established using @@ -223,33 +253,45 @@ text {* \noindent Again, we prove some instances, by providing suitable parameter definitions and proofs for the - additional specifications: + additional specifications. Obverve that instantiations + for types with the same arity may be simultaneous: *} - instance nat :: monoidl - neutral_nat_def: "\ \ 0" - proof + instantiation nat and int :: monoidl + begin + + definition + neutral_nat_def: "\ = (0\nat)" + + definition + neutral_int_def: "\ = (0\int)" + + instance proof fix n :: nat show "\ \ n = n" unfolding neutral_nat_def mult_nat_def by simp - qed - - instance int :: monoidl - neutral_int_def: "\ \ 0" - proof + next fix k :: int show "\ \ k = k" unfolding neutral_int_def mult_int_def by simp qed - instance * :: (monoidl, monoidl) monoidl - neutral_prod_def: "\ \ (\, \)" - proof - fix p :: "'a\monoidl \ 'b\monoidl" + end + + instantiation * :: (monoidl, monoidl) monoidl + begin + + definition + neutral_prod_def: "\ = (\, \)" + + instance proof + fix p :: "\\monoidl \ \\monoidl" show "\ \ p = p" unfolding neutral_prod_def mult_prod_def by (simp add: neutl) qed + end + text {* \noindent Fully-fledged monoids are modelled by another subclass which does not add new parameters but tightens the specification: @@ -258,27 +300,32 @@ class monoid = monoidl + assumes neutr: "x \ \ = x" - instance nat :: monoid - proof + instantiation nat and int :: monoid + begin + + instance proof fix n :: nat show "n \ \ = n" unfolding neutral_nat_def mult_nat_def by simp - qed - - instance int :: monoid - proof + next fix k :: int show "k \ \ = k" unfolding neutral_int_def mult_int_def by simp qed - instance * :: (monoid, monoid) monoid - proof - fix p :: "'a\monoid \ 'b\monoid" + end + + instantiation * :: (monoid, monoid) monoid + begin + + instance proof + fix p :: "\\monoid \ \\monoid" show "p \ \ = p" unfolding neutral_prod_def mult_prod_def by (simp add: neutr) qed + end + text {* \noindent To finish our small algebra example, we add a @{text "group"} class with a corresponding instance: @@ -288,15 +335,21 @@ fixes inverse :: "\ \ \" ("(_\
)" [1000] 999) assumes invl: "x\
\ x = \" - instance int :: group - inverse_int_def: "i\
\ - i" - proof + instantiation int :: group + begin + + definition + inverse_int_def: "i\
= - (i\int)" + + instance proof fix i :: int have "-i + i = 0" by simp then show "i\
\ i = \" unfolding mult_int_def neutral_int_def inverse_int_def . qed + end + section {* Type classes as locales *} subsection {* A look behind the scene *} @@ -335,7 +388,7 @@ text {* \noindent together with a corresponding interpretation: *} interpretation idem_class: - idem ["f \ ('a\idem) \ \"] + idem ["f \ (\\idem) \ \"] by unfold_locales (rule idem) (*<*) setup {* Sign.parent_path *} (*>*) text {* @@ -431,7 +484,7 @@ *} fun - replicate :: "nat \ 'a list \ 'a list" + replicate :: "nat \ \ list \ \ list" where "replicate 0 _ = []" | "replicate (Suc n) xs = xs @ replicate n xs" @@ -524,8 +577,9 @@ text {* Turning back to the first motivation for type classes, namely overloading, it is obvious that overloading - stemming from @{text "\"} and @{text "\"} - statements naturally maps to Haskell type classes. + stemming from @{text "\"} statements and + @{text "\"} + targets naturally maps to Haskell type classes. The code generator framework \cite{isabelle-codegen} takes this into account. Concerning target languages lacking type classes (e.g.~SML), type classes @@ -533,17 +587,6 @@ For example, lets go back to the power function: *} -(* fun - pow_nat :: "nat \ \\group \ \\group" where - "pow_nat 0 x = \" - | "pow_nat (Suc n) x = x \ pow_nat n x" - - definition - pow_int :: "int \ \\group \ \\group" where - "pow_int k x = (if k >= 0 - then pow_nat (nat k) x - else (pow_nat (nat (- k)) x)\
)"*) - definition example :: int where "example = pow_int 10 (-2)" diff -r 27f6771ae8fb -r 0140cc7b26ad doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 05 04:34:15 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Dec 05 14:15:39 2007 +0100 @@ -166,15 +166,22 @@ \begin{isamarkuptext}% The concrete type \isa{int} is made a \isa{semigroup} instance by providing a suitable definition for the class parameter - \isa{mult} and a proof for the specification of \isa{assoc}.% + \isa{mult} and a proof for the specification of \isa{assoc}. + This is accomplished by the \isa{{\isasymINSTANTIATION}} target:% \end{isamarkuptext}% \isamarkuptrue% -\ \ \ \ \isacommand{instance}\isamarkupfalse% +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% \ int\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline -\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isasymequiv}\ i\ {\isacharplus}\ j{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{begin}\isanewline +\isanewline +\ \ \ \ \isacommand{definition}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ mult{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i\ {\isasymotimes}\ j\ {\isacharequal}\ i\ {\isacharplus}\ {\isacharparenleft}j{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\ \ \ \ \isacommand{instance}\isamarkupfalse% % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof @@ -198,27 +205,40 @@ \isadelimproof % \endisadelimproof +\isanewline +\isanewline +\ \ \ \ \isacommand{end}\isamarkupfalse% % \begin{isamarkuptext}% -\noindent From now on, the type-checker will consider \isa{int} - as a \isa{semigroup} automatically, i.e.\ any general results - are immediately available on concrete instances. - - Note that the first proof step is the \isa{default} method, - which for instantiation proofs maps to the \isa{intro{\isacharunderscore}classes} method. - This boils down an instantiation judgement to the relevant primitive +\noindent \isa{{\isasymINSTANTIATION}} allows to define class parameters + at a particular instance using common specification tools (here, + \isa{{\isasymDEFINITION}}). The concluding \isa{{\isasymINSTANCE}} + opens a proof that the given parameters actually conform + to the class specification. Note that the first proof step + is the \isa{default} method, + which for such instance proofs maps to the \isa{intro{\isacharunderscore}classes} method. + This boils down an instance judgement to the relevant primitive proof goals and should conveniently always be the first method applied in an instantiation proof. + From now on, the type-checker will consider \isa{int} + as a \isa{semigroup} automatically, i.e.\ any general results + are immediately available on concrete instances. \medskip Another instance of \isa{semigroup} are the natural numbers:% \end{isamarkuptext}% \isamarkuptrue% -\ \ \ \ \isacommand{instance}\isamarkupfalse% +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% \ nat\ {\isacharcolon}{\isacharcolon}\ semigroup\isanewline -\ \ \ \ \ \ mult{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}m\ {\isasymotimes}\ n\ {\isasymequiv}\ m\ {\isacharplus}\ n{\isachardoublequoteclose}\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 +\isanewline +\ \ \ \ \isacommand{instance}\isamarkupfalse% % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof @@ -239,6 +259,9 @@ \isadelimproof % \endisadelimproof +\isanewline +\isanewline +\ \ \ \ \isacommand{end}\isamarkupfalse% % \isamarkupsubsection{Lifting and parametric types% } @@ -251,19 +274,25 @@ using our simple algebra:% \end{isamarkuptext}% \isamarkuptrue% -\ \ \ \ \isacommand{instance}\isamarkupfalse% +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}semigroup{\isacharcomma}\ semigroup{\isacharparenright}\ semigroup\isanewline -\ \ \ \ \ \ mult{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}p\isactrlisub {\isadigit{1}}\ {\isasymotimes}\ p\isactrlisub {\isadigit{2}}\ {\isasymequiv}\ {\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 +\ \ \ \ \isakeyword{begin}\isanewline +\isanewline +\ \ \ \ \isacommand{definition}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ 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 +\isanewline +\ \ \ \ \isacommand{instance}\isamarkupfalse% % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof \isacommand{proof}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% -\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}semigroup\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline +\ p\isactrlisub {\isadigit{1}}\ p\isactrlisub {\isadigit{2}}\ p\isactrlisub {\isadigit{3}}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}semigroup\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}semigroup{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% \ {\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 \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% @@ -277,6 +306,9 @@ \isadelimproof % \endisadelimproof +\ \ \ \ \ \ \isanewline +\isanewline +\ \ \ \ \isacommand{end}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Associativity from product semigroups is @@ -308,15 +340,26 @@ \begin{isamarkuptext}% \noindent Again, we prove some instances, by providing suitable parameter definitions and proofs for the - additional specifications:% + additional specifications. Obverve that instantiations + for types with the same arity may be simultaneous:% \end{isamarkuptext}% \isamarkuptrue% +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% +\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline +\ \ \ \ \isakeyword{begin}\isanewline +\isanewline +\ \ \ \ \isacommand{definition}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\ \ \ \ \isacommand{definition}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% -\ nat\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline -\ \ \ \ \ \ neutral{\isacharunderscore}nat{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof @@ -329,26 +372,7 @@ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\ \ \ \ \isacommand{instance}\isamarkupfalse% -\ int\ {\isacharcolon}{\isacharcolon}\ monoidl\isanewline -\ \ \ \ \ \ neutral{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isadigit{0}}{\isachardoublequoteclose}\isanewline -% -\isadelimproof -\ \ \ \ % -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% +\ \ \ \ \isacommand{next}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline @@ -363,23 +387,32 @@ {\isafoldproof}% % \isadelimproof -\isanewline % \endisadelimproof \isanewline -\ \ \ \ \isacommand{instance}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{end}\isamarkupfalse% +\isanewline +\isanewline +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% \ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoidl{\isacharcomma}\ monoidl{\isacharparenright}\ monoidl\isanewline -\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{begin}\isanewline +\isanewline +\ \ \ \ \isacommand{definition}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ neutral{\isacharunderscore}prod{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isacharequal}\ {\isacharparenleft}{\isasymone}{\isacharcomma}\ {\isasymone}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\ \ \ \ \isacommand{instance}\isamarkupfalse% % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof \isacommand{proof}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% -\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline +\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoidl\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% @@ -393,6 +426,9 @@ \isadelimproof % \endisadelimproof +\isanewline +\isanewline +\ \ \ \isacommand{end}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Fully-fledged monoids are modelled by another subclass @@ -403,11 +439,14 @@ \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline \ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline \isanewline +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% +\ nat\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline +\ \ \ \ \isakeyword{begin}\isanewline +\isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof @@ -420,25 +459,7 @@ \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \isacommand{qed}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -\isanewline -% -\endisadelimproof -\isanewline -\ \ \ \ \isacommand{instance}\isamarkupfalse% -\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline -% -\isadelimproof -\ \ \ \ % -\endisadelimproof -% -\isatagproof -\isacommand{proof}\isamarkupfalse% +\ \ \ \ \isacommand{next}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline @@ -453,22 +474,28 @@ {\isafoldproof}% % \isadelimproof -\isanewline % \endisadelimproof \isanewline +\isanewline +\ \ \ \ \isacommand{end}\isamarkupfalse% +\isanewline +\isanewline +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% +\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline +\ \ \ \ \isakeyword{begin}\isanewline +\isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% -\ {\isacharasterisk}\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}monoid{\isacharcomma}\ monoid{\isacharparenright}\ monoid\isanewline % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof \isacommand{proof}\isamarkupfalse% \ \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% -\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoid\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoid{\isachardoublequoteclose}\isanewline +\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isasymColon}monoid\ {\isasymtimes}\ {\isasymbeta}{\isasymColon}monoid{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% @@ -482,6 +509,9 @@ \isadelimproof % \endisadelimproof +\isanewline +\isanewline +\ \ \ \ \isacommand{end}\isamarkupfalse% % \begin{isamarkuptext}% \noindent To finish our small algebra example, we add a \isa{group} class @@ -493,12 +523,18 @@ \ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline \ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline \isanewline -\ \ \ \ \isacommand{instance}\isamarkupfalse% +\ \ \ \ \isacommand{instantiation}\isamarkupfalse% \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline -\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline +\ \ \ \ \isakeyword{begin}\isanewline +\isanewline +\ \ \ \ \isacommand{definition}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isacharequal}\ {\isacharminus}\ {\isacharparenleft}i{\isasymColon}int{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\ \ \ \ \isacommand{instance}\isamarkupfalse% % \isadelimproof -\ \ \ \ % +\ % \endisadelimproof % \isatagproof @@ -523,6 +559,9 @@ \isadelimproof % \endisadelimproof +\isanewline +\isanewline +\ \ \ \ \isacommand{end}\isamarkupfalse% % \isamarkupsection{Type classes as locales% } @@ -584,7 +623,7 @@ \isamarkuptrue% \isacommand{interpretation}\isamarkupfalse% \ idem{\isacharunderscore}class{\isacharcolon}\isanewline -\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isacharprime}a{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline +\ \ idem\ {\isacharbrackleft}{\isachardoublequoteopen}f\ {\isasymColon}\ {\isacharparenleft}{\isasymalpha}{\isasymColon}idem{\isacharparenright}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}{\isacharbrackright}\isanewline % \isadelimproof % @@ -758,7 +797,7 @@ \isamarkuptrue% \ \ \ \ \isacommand{fun}\isamarkupfalse% \isanewline -\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ list\ {\isasymRightarrow}\ {\isasymalpha}\ list{\isachardoublequoteclose}\isanewline \ \ \ \ \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 @@ -897,8 +936,9 @@ \begin{isamarkuptext}% Turning back to the first motivation for type classes, namely overloading, it is obvious that overloading - stemming from \isa{{\isasymCLASS}} and \isa{{\isasymINSTANCE}} - statements naturally maps to Haskell type classes. + stemming from \isa{{\isasymCLASS}} statements and + \isa{{\isasymINSTANTIATION}} + targets naturally maps to Haskell type classes. The code generator framework \cite{isabelle-codegen} takes this into account. Concerning target languages lacking type classes (e.g.~SML), type classes diff -r 27f6771ae8fb -r 0140cc7b26ad doc-src/IsarAdvanced/Classes/classes.tex --- a/doc-src/IsarAdvanced/Classes/classes.tex Wed Dec 05 04:34:15 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/classes.tex Wed Dec 05 14:15:39 2007 +0100 @@ -28,6 +28,7 @@ \newcommand{\isasymSHOWS}{\cmd{shows}} \newcommand{\isasymCLASS}{\cmd{class}} \newcommand{\isasymINSTANCE}{\cmd{instance}} +\newcommand{\isasymINSTANTIATION}{\cmd{instantiation}} \newcommand{\isasymLEMMA}{\cmd{lemma}} \newcommand{\isasymPROOF}{\cmd{proof}} \newcommand{\isasymQED}{\cmd{qed}} diff -r 27f6771ae8fb -r 0140cc7b26ad doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Dec 05 04:34:15 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Wed Dec 05 14:15:39 2007 +0100 @@ -372,17 +372,24 @@ | "head (x#xs) = x" text {* - We provide some instances for our @{text null}: + \noindent We provide some instances for our @{text null}: *} -instance option :: (type) null - "null \ None" .. +instantiation option and list :: (type) null +begin + +definition + "null = None" -instance list :: (type) null - "null \ []" .. +definition + "null = []" + +instance .. + +end text {* - Constructing a dummy example: + \noindent Constructing a dummy example: *} definition diff -r 27f6771ae8fb -r 0140cc7b26ad doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex --- a/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Dec 05 04:34:15 2007 +0100 +++ b/doc-src/IsarAdvanced/Codegen/Thy/document/Codegen.tex Wed Dec 05 14:15:39 2007 +0100 @@ -464,9 +464,20 @@ We provide some instances for our \isa{null}:% \end{isamarkuptext}% \isamarkuptrue% +\isacommand{instantiation}\isamarkupfalse% +\ option\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline +\isakeyword{begin}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\isanewline +\ \ {\isachardoublequoteopen}null\ {\isacharequal}\ None{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\isanewline +\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\isanewline \isacommand{instance}\isamarkupfalse% -\ option\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline -\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ None{\isachardoublequoteclose}% +% \isadelimproof \ % \endisadelimproof @@ -482,22 +493,7 @@ \endisadelimproof \isanewline \isanewline -\isacommand{instance}\isamarkupfalse% -\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ null\isanewline -\ \ {\isachardoublequoteopen}null\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}% -\isadelimproof -\ % -\endisadelimproof -% -\isatagproof -\isacommand{{\isachardot}{\isachardot}}\isamarkupfalse% -% -\endisatagproof -{\isafoldproof}% -% -\isadelimproof -% -\endisadelimproof +\isacommand{end}\isamarkupfalse% % \begin{isamarkuptext}% Constructing a dummy example:% diff -r 27f6771ae8fb -r 0140cc7b26ad doc-src/isar.sty --- a/doc-src/isar.sty Wed Dec 05 04:34:15 2007 +0100 +++ b/doc-src/isar.sty Wed Dec 05 14:15:39 2007 +0100 @@ -78,6 +78,7 @@ \newcommand{\DEFS}{\isarkeyword{defs}} \newcommand{\AXCLASS}{\isarkeyword{axclass}} \newcommand{\INSTANCE}{\isarkeyword{instance}} +\newcommand{\INSTANTIATION}{\isarkeyword{instantiation}} \newcommand{\DECLARE}{\isarkeyword{declare}} \newcommand{\LEMMAS}{\isarkeyword{lemmas}} \newcommand{\THEOREMS}{\isarkeyword{theorems}}