# HG changeset patch # User haftmann # Date 1193821850 -3600 # Node ID 7bacd1798fc44b886131dd06d1b3962f1c76d51d # Parent 584d8f2e1fc9cbc4eaa508d1969862d1944c08a7 tuned diff -r 584d8f2e1fc9 -r 7bacd1798fc4 doc-src/IsarAdvanced/Classes/Thy/Classes.thy --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Tue Oct 30 17:58:03 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy Wed Oct 31 10:10:50 2007 +0100 @@ -151,7 +151,8 @@ mult_int_def: "i \ j \ i + j" 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 . + then show "(i \ j) \ k = i \ (j \ k)" + unfolding mult_int_def . qed text {* @@ -172,27 +173,41 @@ mult_nat_def: "m \ n \ m + n" proof fix m n q :: nat - show "m \ n \ q = m \ (n \ q)" unfolding mult_nat_def by simp - qed - -text {* - \noindent Also @{text "list"}s form a semigroup with @{const "op @"} as - parameter: -*} - - instance list :: (type) semigroup - mult_list_def: "xs \ ys \ xs @ ys" - proof - fix xs ys zs :: "\ list" - show "xs \ ys \ zs = xs \ (ys \ zs)" - proof - - from mult_list_def have "\xs ys\\ list. xs \ ys \ xs @ ys" . - thus ?thesis by simp - qed + show "m \ n \ q = m \ (n \ q)" + unfolding mult_nat_def by simp qed -subsection {* Subclasses *} +subsection {* Lifting and parametric types *} + +text {* + Overloaded definitions giving on class instantiation + may include recursion over the syntactic structure of types. + As a canonical example, we model product semigroups + 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" + 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 + +text {* + \noindent Associativity from product semigroups is + established using + the definition of @{text \} on products and the hypothetical + associativety of the type components; these hypothesis + are facts due to the @{text semigroup} constraints imposed + on the type components by the @{text instance} proposition. + Indeed, this pattern often occurs with parametric types + and type classes. +*} + + +subsection {* Subclassing *} text {* We define a subclass @{text "monoidl"} (a semigroup with a left-hand neutral) @@ -206,36 +221,34 @@ assumes neutl: "\ \ x = x" text {* - \noindent Again, we make some instances, by + \noindent Again, we prove some instances, by providing suitable parameter definitions and proofs for the - additional specifications. + additional specifications: *} instance nat :: monoidl neutral_nat_def: "\ \ 0" proof fix n :: nat - show "\ \ n = n" unfolding neutral_nat_def mult_nat_def by simp + show "\ \ n = n" + unfolding neutral_nat_def mult_nat_def by simp qed instance int :: monoidl neutral_int_def: "\ \ 0" proof fix k :: int - show "\ \ k = k" unfolding neutral_int_def mult_int_def by simp + show "\ \ k = k" + unfolding neutral_int_def mult_int_def by simp qed - instance list :: (type) monoidl - neutral_list_def: "\ \ []" + instance * :: (monoidl, monoidl) monoidl + neutral_prod_def: "\ \ (\, \)" proof - fix xs :: "\ list" - show "\ \ xs = xs" - proof - - from mult_list_def have "\xs ys\\ list. xs \ ys \ xs @ ys" . - moreover from mult_list_def neutral_list_def have "\ \ []\\ list" by simp - ultimately show ?thesis by simp - qed - qed + fix p :: "'a\monoidl \ 'b\monoidl" + show "\ \ p = p" + unfolding neutral_prod_def mult_prod_def by (simp add: neutl) + qed text {* \noindent Fully-fledged monoids are modelled by another subclass @@ -245,26 +258,25 @@ class monoid = monoidl + assumes neutr: "x \ \ = x" -text {* - \noindent Instantiations may also be given simultaneously for different - type constructors: -*} - - instance nat :: monoid and int :: monoid and list :: (type) monoid + instance nat :: monoid proof fix n :: nat - show "n \ \ = n" unfolding neutral_nat_def mult_nat_def by simp - next + show "n \ \ = n" + unfolding neutral_nat_def mult_nat_def by simp + qed + + instance int :: monoid + proof fix k :: int - show "k \ \ = k" unfolding neutral_int_def mult_int_def by simp - next - fix xs :: "\ list" - show "xs \ \ = xs" - proof - - from mult_list_def have "\xs ys\\ list. xs \ ys \ xs @ ys" . - moreover from mult_list_def neutral_list_def have "\ \ []\\ list" by simp - ultimately show ?thesis by simp - qed + show "k \ \ = k" + unfolding neutral_int_def mult_int_def by simp + qed + + instance * :: (monoid, monoid) monoid + proof + fix p :: "'a\monoid \ 'b\monoid" + show "p \ \ = p" + unfolding neutral_prod_def mult_prod_def by (simp add: neutr) qed text {* @@ -282,7 +294,7 @@ fix i :: int have "-i + i = 0" by simp then show "i\
\ i = \" - unfolding mult_int_def and neutral_int_def and inverse_int_def . + unfolding mult_int_def neutral_int_def inverse_int_def . qed section {* Type classes as locales *} @@ -338,17 +350,17 @@ Isabelle locales enable reasoning at a general level, while results are implicitly transferred to all instances. For example, we can now establish the @{text "left_cancel"} lemma for groups, which - states that the function @{text "(x \)"} is injective: + states that the function @{text "(x \)"} is injective: *} lemma (in group) left_cancel: "x \ y = x \ z \ y = z" proof - assume "x \ y = x \ z" + assume "x \ y = x \ z" then have "x\
\ (x \ y) = x\
\ (x \ z)" by simp then have "(x\
\ x) \ y = (x\
\ x) \ z" using assoc by simp then show "y = z" using neutl and invl by simp next - assume "y = z" + assume "y = z" then show "x \ y = x \ z" by simp qed @@ -389,11 +401,56 @@ *} +subsection {* A functor analogy *} + +text {* + We introduced Isar classes by analogy to type classes + functional programming; if we reconsider this in the + context of what has been said about type classes and locales, + we can drive this analogy further by stating that type + classes essentially correspond to functors which have + a canonical interpretation as type classes. + Anyway, there is also the possibility of other interpretations. + For example, also @{text "list"}s form a monoid with + @{const "op @"} and @{const "[]"} as operations, but it + seems inappropriate to apply to lists + the same operations as for genuinly algebraic types. + In such a case, we simply can do a particular interpretation + of monoids for lists: +*} + + interpretation list_monoid: monoid ["op @" "[]"] + by unfold_locales auto + +text {* + \noindent This enables us to apply facts on monoids + to lists, e.g. @{thm list_monoid.neutl [no_vars]}. + + When using this interpretation pattern, it may also + be appropriate to map derived definitions accordingly: +*} + + fun + replicate :: "nat \ 'a list \ 'a list" + where + "replicate 0 _ = []" + | "replicate (Suc n) xs = xs @ replicate n xs" + + interpretation list_monoid: monoid ["op @" "[]"] where + "monoid.pow_nat (op @) [] = replicate" + proof + fix n :: nat + show "monoid.pow_nat (op @) [] n = replicate n" + by (induct n) auto + qed + + subsection {* Additional subclass relations *} text {* Any @{text "group"} is also a @{text "monoid"}; this - can be made explicit by claiming an additional subclass relation, + can be made explicit by claiming an additional + subclass relation, together with a proof of the logical difference: *} @@ -411,7 +468,41 @@ method which only leaves the logical differences still open to proof to the user. Afterwards it is propagated to the type system, making @{text group} an instance of - @{text monoid}. For illustration, a derived definition + @{text monoid} by adding an additional edge + to the graph of subclass relations + (cf.\ \figref{fig:subclass}). + + \begin{figure}[htbp] + \begin{center} + \small + \unitlength 0.6mm + \begin{picture}(40,60)(0,0) + \put(20,60){\makebox(0,0){@{text semigroup}}} + \put(20,40){\makebox(0,0){@{text monoidl}}} + \put(00,20){\makebox(0,0){@{text monoid}}} + \put(40,00){\makebox(0,0){@{text group}}} + \put(20,55){\vector(0,-1){10}} + \put(15,35){\vector(-1,-1){10}} + \put(25,35){\vector(1,-3){10}} + \end{picture} + \hspace{8em} + \begin{picture}(40,60)(0,0) + \put(20,60){\makebox(0,0){@{text semigroup}}} + \put(20,40){\makebox(0,0){@{text monoidl}}} + \put(00,20){\makebox(0,0){@{text monoid}}} + \put(40,00){\makebox(0,0){@{text group}}} + \put(20,55){\vector(0,-1){10}} + \put(15,35){\vector(-1,-1){10}} + \put(05,15){\vector(3,-1){30}} + \end{picture} + \caption{Subclass relationship of monoids and groups: + before and after establishing the relationship + @{text "group \ monoid"}; transitive edges left out.} + \label{fig:subclass} + \end{center} + \end{figure} + + For illustration, a derived definition in @{text group} which uses @{text pow_nat}: *} @@ -422,15 +513,13 @@ else (pow_nat (nat (- k)) x)\
)" text {* - \noindent yields the global definition of + \noindent yields the global definition of @{term [source] "pow_int \ int \ \\group \ \\group"} with the corresponding theorem @{thm pow_int_def [no_vars]}. *} -section {* Further issues *} - -subsection {* Code generation *} +section {* Type classes and code generation *} text {* Turning back to the first motivation for type classes, diff -r 584d8f2e1fc9 -r 7bacd1798fc4 doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex --- a/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Tue Oct 30 17:58:03 2007 +0100 +++ b/doc-src/IsarAdvanced/Classes/Thy/document/Classes.tex Wed Oct 31 10:10:50 2007 +0100 @@ -186,7 +186,8 @@ \ simp\isanewline \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isacharparenleft}i\ {\isasymotimes}\ j{\isacharparenright}\ {\isasymotimes}\ k\ {\isacharequal}\ i\ {\isasymotimes}\ {\isacharparenleft}j\ {\isasymotimes}\ k{\isacharparenright}{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% @@ -226,7 +227,8 @@ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ 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}\ \isacommand{unfolding}\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{qed}\isamarkupfalse% @@ -238,14 +240,20 @@ % \endisadelimproof % +\isamarkupsubsection{Lifting and parametric types% +} +\isamarkuptrue% +% \begin{isamarkuptext}% -\noindent Also \isa{list}s form a semigroup with \isa{op\ {\isacharat}} as - parameter:% +Overloaded definitions giving on class instantiation + may include recursion over the syntactic structure of types. + As a canonical example, we model product semigroups + using our simple algebra:% \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% -\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ semigroup\isanewline -\ \ \ \ \ \ mult{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\isanewline +\ {\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 % \isadelimproof \ \ \ \ % @@ -255,20 +263,12 @@ \isacommand{proof}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% -\ xs\ ys\ zs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline +\ 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 \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ ys\ {\isasymotimes}\ zs\ {\isacharequal}\ xs\ {\isasymotimes}\ {\isacharparenleft}ys\ {\isasymotimes}\ zs{\isacharparenright}{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% -\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse% -\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% -\isanewline +\ {\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% +\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ assoc{\isacharparenright}\isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% % \endisatagproof @@ -278,7 +278,19 @@ % \endisadelimproof % -\isamarkupsubsection{Subclasses% +\begin{isamarkuptext}% +\noindent Associativity from product semigroups is + established using + the definition of \isa{{\isasymotimes}} on products and the hypothetical + associativety of the type components; these hypothesis + are facts due to the \isa{semigroup} constraints imposed + on the type components by the \isa{instance} proposition. + Indeed, this pattern often occurs with parametric types + and type classes.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Subclassing% } \isamarkuptrue% % @@ -294,9 +306,9 @@ \ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline \ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}% \begin{isamarkuptext}% -\noindent Again, we make some instances, by +\noindent Again, we prove some instances, by providing suitable parameter definitions and proofs for the - additional specifications.% + additional specifications:% \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{instance}\isamarkupfalse% @@ -313,7 +325,8 @@ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ n\ {\isacharequal}\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ neutral{\isacharunderscore}nat{\isacharunderscore}def\ mult{\isacharunderscore}nat{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% @@ -340,7 +353,8 @@ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ k\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% @@ -354,8 +368,8 @@ \endisadelimproof \isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% -\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoidl\isanewline -\ \ \ \ \ \ neutral{\isacharunderscore}list{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}\isanewline +\ {\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 % \isadelimproof \ \ \ \ % @@ -365,26 +379,12 @@ \isacommand{proof}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% -\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline +\ p\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a{\isasymColon}monoidl\ {\isasymtimes}\ {\isacharprime}b{\isasymColon}monoidl{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ xs\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% -\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% -\isanewline -\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse% -\ \isacommand{from}\isamarkupfalse% -\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse% -\ \isacommand{show}\isamarkupfalse% -\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% -\isanewline +\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ p\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% +\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutl{\isacharparenright}\isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% % \endisatagproof @@ -401,14 +401,10 @@ \isamarkuptrue% \ \ \ \ \isacommand{class}\isamarkupfalse% \ monoid\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline -\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}% -\begin{isamarkuptext}% -\noindent Instantiations may also be given simultaneously for different - type constructors:% -\end{isamarkuptext}% -\isamarkuptrue% +\ \ \ \ \ \ \isakeyword{assumes}\ neutr{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\isanewline +\isanewline \ \ \ \ \isacommand{instance}\isamarkupfalse% -\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ int\ {\isacharcolon}{\isacharcolon}\ monoid\ \isakeyword{and}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}\ monoid\isanewline +\ nat\ {\isacharcolon}{\isacharcolon}\ monoid\ \isanewline % \isadelimproof \ \ \ \ % @@ -420,40 +416,64 @@ \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}n\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ n{\isachardoublequoteclose}\ \isacommand{unfolding}\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 -\ \ \ \ \isacommand{next}\isamarkupfalse% +\ \ \ \ \isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\ \ \ \ \isacommand{instance}\isamarkupfalse% +\ int\ {\isacharcolon}{\isacharcolon}\ monoid\isanewline +% +\isadelimproof +\ \ \ \ % +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% \isanewline \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% \ k\ {\isacharcolon}{\isacharcolon}\ int\isanewline \ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\ \isacommand{unfolding}\isamarkupfalse% +\ {\isachardoublequoteopen}k\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ k{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% \ neutral{\isacharunderscore}int{\isacharunderscore}def\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% \ simp\isanewline -\ \ \ \ \isacommand{next}\isamarkupfalse% +\ \ \ \ \isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof \isanewline -\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% -\ xs\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ list{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \isacommand{show}\isamarkupfalse% -\ {\isachardoublequoteopen}xs\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ xs{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse% -\ {\isacharminus}\isanewline -\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% -\ mult{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymAnd}xs\ ys{\isasymColon}{\isasymalpha}\ list{\isachardot}\ xs\ {\isasymotimes}\ ys\ {\isasymequiv}\ xs\ {\isacharat}\ ys{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% +% +\endisadelimproof \isanewline -\ \ \ \ \ \ \ \ \isacommand{moreover}\isamarkupfalse% -\ \isacommand{from}\isamarkupfalse% -\ mult{\isacharunderscore}list{\isacharunderscore}def\ neutral{\isacharunderscore}list{\isacharunderscore}def\ \isacommand{have}\isamarkupfalse% -\ {\isachardoublequoteopen}{\isasymone}\ {\isasymequiv}\ {\isacharbrackleft}{\isacharbrackright}{\isasymColon}{\isasymalpha}\ list{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \ \ \isacommand{ultimately}\isamarkupfalse% -\ \isacommand{show}\isamarkupfalse% -\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse% -\ simp\isanewline -\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse% -\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 +\ \ \ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}p\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ p{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% +\ neutral{\isacharunderscore}prod{\isacharunderscore}def\ mult{\isacharunderscore}prod{\isacharunderscore}def\ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}simp\ add{\isacharcolon}\ neutr{\isacharparenright}\isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% % \endisatagproof @@ -492,8 +512,8 @@ \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% \ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymotimes}\ i\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline -\ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% -\ mult{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ neutral{\isacharunderscore}int{\isacharunderscore}def\ \isakeyword{and}\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% +\ \ \ \ \ \ \ \ \isacommand{unfolding}\isamarkupfalse% +\ mult{\isacharunderscore}int{\isacharunderscore}def\ neutral{\isacharunderscore}int{\isacharunderscore}def\ inverse{\isacharunderscore}int{\isacharunderscore}def\ \isacommand{{\isachardot}}\isamarkupfalse% \isanewline \ \ \ \ \isacommand{qed}\isamarkupfalse% % @@ -608,7 +628,7 @@ Isabelle locales enable reasoning at a general level, while results are implicitly transferred to all instances. For example, we can now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which - states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:% + states that the function \isa{{\isacharparenleft}x\ {\isasymotimes}{\isacharparenright}} is injective:% \end{isamarkuptext}% \isamarkuptrue% \ \ \ \ \isacommand{lemma}\isamarkupfalse% @@ -621,7 +641,7 @@ \isatagproof \isacommand{proof}\isamarkupfalse% \isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{have}\isamarkupfalse% @@ -639,7 +659,7 @@ \ simp\isanewline \ \ \ \ \isacommand{next}\isamarkupfalse% \isanewline -\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% \ \isacommand{show}\isamarkupfalse% @@ -691,13 +711,92 @@ \end{isamarkuptext}% \isamarkuptrue% % +\isamarkupsubsection{A functor analogy% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +We introduced Isar classes by analogy to type classes + functional programming; if we reconsider this in the + context of what has been said about type classes and locales, + we can drive this analogy further by stating that type + classes essentially correspond to functors which have + a canonical interpretation as type classes. + Anyway, there is also the possibility of other interpretations. + For example, also \isa{list}s form a monoid with + \isa{op\ {\isacharat}} and \isa{{\isacharbrackleft}{\isacharbrackright}} as operations, but it + seems inappropriate to apply to lists + the same operations as for genuinly algebraic types. + In such a case, we simply can do a particular interpretation + of monoids for lists:% +\end{isamarkuptext}% +\isamarkuptrue% +\ \ \ \ \isacommand{interpretation}\isamarkupfalse% +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\isanewline +% +\isadelimproof +\ \ \ \ \ \ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ unfold{\isacharunderscore}locales\ auto% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\begin{isamarkuptext}% +\noindent This enables us to apply facts on monoids + to lists, e.g. \isa{{\isacharbrackleft}{\isacharbrackright}\ {\isacharat}\ x\ {\isacharequal}\ x}. + + When using this interpretation pattern, it may also + be appropriate to map derived definitions accordingly:% +\end{isamarkuptext}% +\isamarkuptrue% +\ \ \ \ \isacommand{fun}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ replicate\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isacharprime}a\ list\ {\isasymRightarrow}\ {\isacharprime}a\ 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 +\isanewline +\ \ \ \ \isacommand{interpretation}\isamarkupfalse% +\ list{\isacharunderscore}monoid{\isacharcolon}\ monoid\ {\isacharbrackleft}{\isachardoublequoteopen}op\ {\isacharat}{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharbrackleft}{\isacharbrackright}{\isachardoublequoteclose}{\isacharbrackright}\ \isakeyword{where}\isanewline +\ \ \ \ \ \ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ replicate{\isachardoublequoteclose}\isanewline +% +\isadelimproof +\ \ \ \ % +\endisadelimproof +% +\isatagproof +\isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% +\ n\ {\isacharcolon}{\isacharcolon}\ nat\isanewline +\ \ \ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isachardoublequoteopen}monoid{\isachardot}pow{\isacharunderscore}nat\ {\isacharparenleft}op\ {\isacharat}{\isacharparenright}\ {\isacharbrackleft}{\isacharbrackright}\ n\ {\isacharequal}\ replicate\ n{\isachardoublequoteclose}\isanewline +\ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse% +\ {\isacharparenleft}induct\ n{\isacharparenright}\ auto\isanewline +\ \ \ \ \isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% \isamarkupsubsection{Additional subclass relations% } \isamarkuptrue% % \begin{isamarkuptext}% Any \isa{group} is also a \isa{monoid}; this - can be made explicit by claiming an additional subclass relation, + can be made explicit by claiming an additional + subclass relation, together with a proof of the logical difference:% \end{isamarkuptext}% \isamarkuptrue% @@ -740,7 +839,41 @@ method which only leaves the logical differences still open to proof to the user. Afterwards it is propagated to the type system, making \isa{group} an instance of - \isa{monoid}. For illustration, a derived definition + \isa{monoid} by adding an additional edge + to the graph of subclass relations + (cf.\ \figref{fig:subclass}). + + \begin{figure}[htbp] + \begin{center} + \small + \unitlength 0.6mm + \begin{picture}(40,60)(0,0) + \put(20,60){\makebox(0,0){\isa{semigroup}}} + \put(20,40){\makebox(0,0){\isa{monoidl}}} + \put(00,20){\makebox(0,0){\isa{monoid}}} + \put(40,00){\makebox(0,0){\isa{group}}} + \put(20,55){\vector(0,-1){10}} + \put(15,35){\vector(-1,-1){10}} + \put(25,35){\vector(1,-3){10}} + \end{picture} + \hspace{8em} + \begin{picture}(40,60)(0,0) + \put(20,60){\makebox(0,0){\isa{semigroup}}} + \put(20,40){\makebox(0,0){\isa{monoidl}}} + \put(00,20){\makebox(0,0){\isa{monoid}}} + \put(40,00){\makebox(0,0){\isa{group}}} + \put(20,55){\vector(0,-1){10}} + \put(15,35){\vector(-1,-1){10}} + \put(05,15){\vector(3,-1){30}} + \end{picture} + \caption{Subclass relationship of monoids and groups: + before and after establishing the relationship + \isa{group\ {\isasymsubseteq}\ monoid}; transitive edges left out.} + \label{fig:subclass} + \end{center} + \end{figure} + + For illustration, a derived definition in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:% \end{isamarkuptext}% \isamarkuptrue% @@ -751,17 +884,13 @@ \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}% \begin{isamarkuptext}% -\noindent yields the global definition of +\noindent yields the global definition of \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}} with the corresponding theorem \isa{pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ {\isadigit{0}}\ {\isasymle}\ k\ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}}.% \end{isamarkuptext}% \isamarkuptrue% % -\isamarkupsection{Further issues% -} -\isamarkuptrue% -% -\isamarkupsubsection{Code generation% +\isamarkupsection{Type classes and code generation% } \isamarkuptrue% %