# HG changeset patch # User wenzelm # Date 965379568 -7200 # Node ID fdc3b5bcd79d120d3bc4de7f62415bd6665d595e # Parent 0c8422ed066fdabd8e830a07db22482aafdac8f1 updated; diff -r 0c8422ed066f -r fdc3b5bcd79d doc-src/AxClass/generated/Group.tex --- a/doc-src/AxClass/generated/Group.tex Fri Aug 04 10:59:22 2000 +0200 +++ b/doc-src/AxClass/generated/Group.tex Fri Aug 04 10:59:28 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% % \isamarkupheader{Basic group theory} -\isacommand{theory}~Group~=~Main:% +\isacommand{theory}\ Group\ =\ Main:% \begin{isamarkuptext}% \medskip\noindent The meta-type system of Isabelle supports \emph{intersections} and \emph{inclusions} of type classes. These @@ -19,9 +19,9 @@ signature parts of our structures.% \end{isamarkuptext}% \isacommand{consts}\isanewline -~~times~::~{"}'a~=>~'a~=>~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline -~~inverse~::~{"}'a~=>~'a{"}~~~~~~~~({"}(\_{\isasyminv}){"}~[1000]~999)\isanewline -~~one~::~'a~~~~~~~~~~~~~~~~~~~~({"}{\isasymunit}{"})% +\ \ times\ ::\ {"}'a\ =>\ 'a\ =>\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline +\ \ inverse\ ::\ {"}'a\ =>\ 'a{"}\ \ \ \ \ \ \ \ ({"}(\_{\isasyminv}){"}\ [1000]\ 999)\isanewline +\ \ one\ ::\ 'a\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}{\isasymunit}{"})% \begin{isamarkuptext}% \noindent Next we define class $monoid$ of monoids with operations $\TIMES$ and $1$. Note that multiple class axioms are allowed for @@ -29,15 +29,15 @@ respective universal closures.% \end{isamarkuptext}% \isacommand{axclass}\isanewline -~~monoid~<~{"}term{"}\isanewline -~~assoc:~~~~~~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline -~~left\_unit:~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline -~~right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}% +\ \ monoid\ <\ {"}term{"}\isanewline +\ \ assoc:\ \ \ \ \ \ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline +\ \ left\_unit:\ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline +\ \ right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}% \begin{isamarkuptext}% \noindent So class $monoid$ contains exactly those types $\tau$ where $\TIMES :: \tau \To \tau \To \tau$ and $1 :: \tau$ are specified appropriately, such that $\TIMES$ is associative and $1$ is a left - and right unit element for $\TIMES$.% + and right unit element for the $\TIMES$ operation.% \end{isamarkuptext}% % \begin{isamarkuptext}% @@ -47,17 +47,17 @@ name, so we may re-use common names such as $assoc$.% \end{isamarkuptext}% \isacommand{axclass}\isanewline -~~semigroup~<~{"}term{"}\isanewline -~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline +\ \ semigroup\ <\ {"}term{"}\isanewline +\ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline \isanewline \isacommand{axclass}\isanewline -~~group~<~semigroup\isanewline -~~left\_unit:~~~~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline -~~left\_inverse:~{"}x{\isasyminv}~{\isasymOtimes}~x~=~{\isasymunit}{"}\isanewline +\ \ group\ <\ semigroup\isanewline +\ \ left\_unit:\ \ \ \ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline +\ \ left\_inverse:\ {"}x{\isasyminv}\ {\isasymOtimes}\ x\ =\ {\isasymunit}{"}\isanewline \isanewline \isacommand{axclass}\isanewline -~~agroup~<~group\isanewline -~~commute:~{"}x~{\isasymOtimes}~y~=~y~{\isasymOtimes}~x{"}% +\ \ agroup\ <\ group\isanewline +\ \ commute:\ {"}x\ {\isasymOtimes}\ y\ =\ y\ {\isasymOtimes}\ x{"}% \begin{isamarkuptext}% \noindent Class $group$ inherits associativity of $\TIMES$ from $semigroup$ and adds two further group axioms. Similarly, $agroup$ @@ -85,42 +85,42 @@ ``abstract theorems''. For example, we may now derive the following well-known laws of general groups.% \end{isamarkuptext}% -\isacommand{theorem}~group\_right\_inverse:~{"}x~{\isasymOtimes}~x{\isasyminv}~=~({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline -\isacommand{proof}~-\isanewline -~~\isacommand{have}~{"}x~{\isasymOtimes}~x{\isasyminv}~=~{\isasymunit}~{\isasymOtimes}~(x~{\isasymOtimes}~x{\isasyminv}){"}\isanewline -~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline -~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x~{\isasymOtimes}~x{\isasyminv}{"}\isanewline -~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x)~{\isasymOtimes}~x{\isasyminv}{"}\isanewline -~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~{\isasymunit}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline -~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~({\isasymunit}~{\isasymOtimes}~x{\isasyminv}){"}\isanewline -~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~(x{\isasyminv}){\isasyminv}~{\isasymOtimes}~x{\isasyminv}{"}\isanewline -~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}{"}\isanewline -~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline -~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline +\isacommand{theorem}\ group\_right\_inverse:\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ ({\isasymunit}{\isasymColon}'a{\isasymColon}group){"}\isanewline +\isacommand{proof}\ -\isanewline +\ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ x{\isasyminv}\ =\ {\isasymunit}\ {\isasymOtimes}\ (x\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x)\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ {\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ ({\isasymunit}\ {\isasymOtimes}\ x{\isasyminv}){"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ (x{\isasyminv}){\isasyminv}\ {\isasymOtimes}\ x{\isasyminv}{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline +\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline \isacommand{qed}% \begin{isamarkuptext}% \noindent With $group_right_inverse$ already available, $group_right_unit$\label{thm:group-right-unit} is now established much easier.% \end{isamarkuptext}% -\isacommand{theorem}~group\_right\_unit:~{"}x~{\isasymOtimes}~{\isasymunit}~=~(x{\isasymColon}'a{\isasymColon}group){"}\isanewline -\isacommand{proof}~-\isanewline -~~\isacommand{have}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x~{\isasymOtimes}~(x{\isasyminv}~{\isasymOtimes}~x){"}\isanewline -~~~~\isacommand{by}~(simp~only:~group.left\_inverse)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~x~{\isasymOtimes}~x{\isasyminv}~{\isasymOtimes}~x{"}\isanewline -~~~~\isacommand{by}~(simp~only:~semigroup.assoc)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~{\isasymunit}~{\isasymOtimes}~x{"}\isanewline -~~~~\isacommand{by}~(simp~only:~group\_right\_inverse)\isanewline -~~\isacommand{also}~\isacommand{have}~{"}...~=~x{"}\isanewline -~~~~\isacommand{by}~(simp~only:~group.left\_unit)\isanewline -~~\isacommand{finally}~\isacommand{show}~?thesis~\isacommand{.}\isanewline +\isacommand{theorem}\ group\_right\_unit:\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ (x{\isasymColon}'a{\isasymColon}group){"}\isanewline +\isacommand{proof}\ -\isanewline +\ \ \isacommand{have}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x\ {\isasymOtimes}\ (x{\isasyminv}\ {\isasymOtimes}\ x){"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_inverse)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x\ {\isasymOtimes}\ x{\isasyminv}\ {\isasymOtimes}\ x{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ semigroup.assoc)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ {\isasymunit}\ {\isasymOtimes}\ x{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group\_right\_inverse)\isanewline +\ \ \isacommand{also}\ \isacommand{have}\ {"}...\ =\ x{"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ only:\ group.left\_unit)\isanewline +\ \ \isacommand{finally}\ \isacommand{show}\ ?thesis\ \isacommand{.}\isanewline \isacommand{qed}% \begin{isamarkuptext}% \medskip Abstract theorems may be instantiated to only those types @@ -169,22 +169,22 @@ \end{center} \end{figure}% \end{isamarkuptext}% -\isacommand{instance}~monoid~<~semigroup\isanewline -\isacommand{proof}~intro\_classes\isanewline -~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}monoid{"}\isanewline -~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline -~~~~\isacommand{by}~(rule~monoid.assoc)\isanewline +\isacommand{instance}\ monoid\ <\ semigroup\isanewline +\isacommand{proof}\ intro\_classes\isanewline +\ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}monoid{"}\isanewline +\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline +\ \ \ \ \isacommand{by}\ (rule\ monoid.assoc)\isanewline \isacommand{qed}\isanewline \isanewline -\isacommand{instance}~group~<~monoid\isanewline -\isacommand{proof}~intro\_classes\isanewline -~~\isacommand{fix}~x~y~z~::~{"}'a{\isasymColon}group{"}\isanewline -~~\isacommand{show}~{"}x~{\isasymOtimes}~y~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}\isanewline -~~~~\isacommand{by}~(rule~semigroup.assoc)\isanewline -~~\isacommand{show}~{"}{\isasymunit}~{\isasymOtimes}~x~=~x{"}\isanewline -~~~~\isacommand{by}~(rule~group.left\_unit)\isanewline -~~\isacommand{show}~{"}x~{\isasymOtimes}~{\isasymunit}~=~x{"}\isanewline -~~~~\isacommand{by}~(rule~group\_right\_unit)\isanewline +\isacommand{instance}\ group\ <\ monoid\isanewline +\isacommand{proof}\ intro\_classes\isanewline +\ \ \isacommand{fix}\ x\ y\ z\ ::\ {"}'a{\isasymColon}group{"}\isanewline +\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ y\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}\isanewline +\ \ \ \ \isacommand{by}\ (rule\ semigroup.assoc)\isanewline +\ \ \isacommand{show}\ {"}{\isasymunit}\ {\isasymOtimes}\ x\ =\ x{"}\isanewline +\ \ \ \ \isacommand{by}\ (rule\ group.left\_unit)\isanewline +\ \ \isacommand{show}\ {"}x\ {\isasymOtimes}\ {\isasymunit}\ =\ x{"}\isanewline +\ \ \ \ \isacommand{by}\ (rule\ group\_right\_unit)\isanewline \isacommand{qed}% \begin{isamarkuptext}% \medskip The $\isakeyword{instance}$ command sets up an appropriate @@ -211,13 +211,13 @@ transferred to Isabelle's type signature level. \medskip As a typical example, we show that type $bool$ with - exclusive-or as operation $\TIMES$, identity as $\isasyminv$, and + exclusive-or as $\TIMES$ operation, identity as $\isasyminv$, and $False$ as $1$ forms an Abelian group.% \end{isamarkuptext}% -\isacommand{defs}~(\isakeyword{overloaded})\isanewline -~~times\_bool\_def:~~~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymnoteq}~(y{\isasymColon}bool){"}\isanewline -~~inverse\_bool\_def:~{"}x{\isasyminv}~{\isasymequiv}~x{\isasymColon}bool{"}\isanewline -~~unit\_bool\_def:~~~~{"}{\isasymunit}~{\isasymequiv}~False{"}% +\isacommand{defs}\ (\isakeyword{overloaded})\isanewline +\ \ times\_bool\_def:\ \ \ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymnoteq}\ (y{\isasymColon}bool){"}\isanewline +\ \ inverse\_bool\_def:\ {"}x{\isasyminv}\ {\isasymequiv}\ x{\isasymColon}bool{"}\isanewline +\ \ unit\_bool\_def:\ \ \ \ {"}{\isasymunit}\ {\isasymequiv}\ False{"}% \begin{isamarkuptext}% \medskip It is important to note that above $\DEFS$ are just overloaded meta-level constant definitions, where type classes are @@ -232,14 +232,14 @@ operations on type $bool$ appropriately, the class membership $bool :: agroup$ may be now derived as follows.% \end{isamarkuptext}% -\isacommand{instance}~bool~::~agroup\isanewline -\isacommand{proof}~(intro\_classes,\isanewline -~~~~unfold~times\_bool\_def~inverse\_bool\_def~unit\_bool\_def)\isanewline -~~\isacommand{fix}~x~y~z\isanewline -~~\isacommand{show}~{"}((x~{\isasymnoteq}~y)~{\isasymnoteq}~z)~=~(x~{\isasymnoteq}~(y~{\isasymnoteq}~z)){"}~\isacommand{by}~blast\isanewline -~~\isacommand{show}~{"}(False~{\isasymnoteq}~x)~=~x{"}~\isacommand{by}~blast\isanewline -~~\isacommand{show}~{"}(x~{\isasymnoteq}~x)~=~False{"}~\isacommand{by}~blast\isanewline -~~\isacommand{show}~{"}(x~{\isasymnoteq}~y)~=~(y~{\isasymnoteq}~x){"}~\isacommand{by}~blast\isanewline +\isacommand{instance}\ bool\ ::\ agroup\isanewline +\isacommand{proof}\ (intro\_classes,\isanewline +\ \ \ \ unfold\ times\_bool\_def\ inverse\_bool\_def\ unit\_bool\_def)\isanewline +\ \ \isacommand{fix}\ x\ y\ z\isanewline +\ \ \isacommand{show}\ {"}((x\ {\isasymnoteq}\ y)\ {\isasymnoteq}\ z)\ =\ (x\ {\isasymnoteq}\ (y\ {\isasymnoteq}\ z)){"}\ \isacommand{by}\ blast\isanewline +\ \ \isacommand{show}\ {"}(False\ {\isasymnoteq}\ x)\ =\ x{"}\ \isacommand{by}\ blast\isanewline +\ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ x)\ =\ False{"}\ \isacommand{by}\ blast\isanewline +\ \ \isacommand{show}\ {"}(x\ {\isasymnoteq}\ y)\ =\ (y\ {\isasymnoteq}\ x){"}\ \isacommand{by}\ blast\isanewline \isacommand{qed}% \begin{isamarkuptext}% The result of an $\isakeyword{instance}$ statement is both expressed @@ -269,23 +269,23 @@ products, direct sums or function spaces. Subsequently we lift $\TIMES$ component-wise to binary products $\alpha \times \beta$.% \end{isamarkuptext}% -\isacommand{defs}~(\isakeyword{overloaded})\isanewline -~~times\_prod\_def:~{"}p~{\isasymOtimes}~q~{\isasymequiv}~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q){"}% +\isacommand{defs}\ (\isakeyword{overloaded})\isanewline +\ \ times\_prod\_def:\ {"}p\ {\isasymOtimes}\ q\ {\isasymequiv}\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q){"}% \begin{isamarkuptext}% It is very easy to see that associativity of $\TIMES^\alpha$ and $\TIMES^\beta$ transfers to ${\TIMES}^{\alpha \times \beta}$. Hence the binary type constructor $\times$ maps semigroups to semigroups. This may be established formally as follows.% \end{isamarkuptext}% -\isacommand{instance}~*~::~(semigroup,~semigroup)~semigroup\isanewline -\isacommand{proof}~(intro\_classes,~unfold~times\_prod\_def)\isanewline -~~\isacommand{fix}~p~q~r~::~{"}'a{\isasymColon}semigroup~{\isasymtimes}~'b{\isasymColon}semigroup{"}\isanewline -~~\isacommand{show}\isanewline -~~~~{"}(fst~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~fst~r,\isanewline -~~~~~~snd~(fst~p~{\isasymOtimes}~fst~q,~snd~p~{\isasymOtimes}~snd~q)~{\isasymOtimes}~snd~r)~=\isanewline -~~~~~~~(fst~p~{\isasymOtimes}~fst~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r),\isanewline -~~~~~~~~snd~p~{\isasymOtimes}~snd~(fst~q~{\isasymOtimes}~fst~r,~snd~q~{\isasymOtimes}~snd~r)){"}\isanewline -~~~~\isacommand{by}~(simp~add:~semigroup.assoc)\isanewline +\isacommand{instance}\ *\ ::\ (semigroup,\ semigroup)\ semigroup\isanewline +\isacommand{proof}\ (intro\_classes,\ unfold\ times\_prod\_def)\isanewline +\ \ \isacommand{fix}\ p\ q\ r\ ::\ {"}'a{\isasymColon}semigroup\ {\isasymtimes}\ 'b{\isasymColon}semigroup{"}\isanewline +\ \ \isacommand{show}\isanewline +\ \ \ \ {"}(fst\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ fst\ r,\isanewline +\ \ \ \ \ \ snd\ (fst\ p\ {\isasymOtimes}\ fst\ q,\ snd\ p\ {\isasymOtimes}\ snd\ q)\ {\isasymOtimes}\ snd\ r)\ =\isanewline +\ \ \ \ \ \ \ (fst\ p\ {\isasymOtimes}\ fst\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r),\isanewline +\ \ \ \ \ \ \ \ snd\ p\ {\isasymOtimes}\ snd\ (fst\ q\ {\isasymOtimes}\ fst\ r,\ snd\ q\ {\isasymOtimes}\ snd\ r)){"}\isanewline +\ \ \ \ \isacommand{by}\ (simp\ add:\ semigroup.assoc)\isanewline \isacommand{qed}% \begin{isamarkuptext}% Thus, if we view class instances as ``structures'', then overloaded diff -r 0c8422ed066f -r fdc3b5bcd79d doc-src/AxClass/generated/NatClass.tex --- a/doc-src/AxClass/generated/NatClass.tex Fri Aug 04 10:59:22 2000 +0200 +++ b/doc-src/AxClass/generated/NatClass.tex Fri Aug 04 10:59:28 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% % \isamarkupheader{Defining natural numbers in FOL \label{sec:ex-natclass}} -\isacommand{theory}~NatClass~=~FOL:% +\isacommand{theory}\ NatClass\ =\ FOL:% \begin{isamarkuptext}% \medskip\noindent Axiomatic type classes abstract over exactly one type argument. Thus, any \emph{axiomatic} theory extension where each @@ -13,21 +13,21 @@ \url{http://isabelle.in.tum.de/library/FOL/ex/NatClass.html}}% \end{isamarkuptext}% \isacommand{consts}\isanewline -~~zero~::~'a~~~~({"}0{"})\isanewline -~~Suc~::~{"}'a~{\isasymRightarrow}~'a{"}\isanewline -~~rec~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~('a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a)~{\isasymRightarrow}~'a{"}\isanewline +\ \ zero\ ::\ 'a\ \ \ \ ({"}0{"})\isanewline +\ \ Suc\ ::\ {"}'a\ {\isasymRightarrow}\ 'a{"}\isanewline +\ \ rec\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a)\ {\isasymRightarrow}\ 'a{"}\isanewline \isanewline \isacommand{axclass}\isanewline -~~nat~<~{"}term{"}\isanewline -~~induct:~~~~~{"}P(0)~{\isasymLongrightarrow}~({\isasymAnd}x.~P(x)~{\isasymLongrightarrow}~P(Suc(x)))~{\isasymLongrightarrow}~P(n){"}\isanewline -~~Suc\_inject:~{"}Suc(m)~=~Suc(n)~{\isasymLongrightarrow}~m~=~n{"}\isanewline -~~Suc\_neq\_0:~~{"}Suc(m)~=~0~{\isasymLongrightarrow}~R{"}\isanewline -~~rec\_0:~~~~~~{"}rec(0,~a,~f)~=~a{"}\isanewline -~~rec\_Suc:~~~~{"}rec(Suc(m),~a,~f)~=~f(m,~rec(m,~a,~f)){"}\isanewline +\ \ nat\ <\ {"}term{"}\isanewline +\ \ induct:\ \ \ \ \ {"}P(0)\ {\isasymLongrightarrow}\ ({\isasymAnd}x.\ P(x)\ {\isasymLongrightarrow}\ P(Suc(x)))\ {\isasymLongrightarrow}\ P(n){"}\isanewline +\ \ Suc\_inject:\ {"}Suc(m)\ =\ Suc(n)\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline +\ \ Suc\_neq\_0:\ \ {"}Suc(m)\ =\ 0\ {\isasymLongrightarrow}\ R{"}\isanewline +\ \ rec\_0:\ \ \ \ \ \ {"}rec(0,\ a,\ f)\ =\ a{"}\isanewline +\ \ rec\_Suc:\ \ \ \ {"}rec(Suc(m),\ a,\ f)\ =\ f(m,\ rec(m,\ a,\ f)){"}\isanewline \isanewline \isacommand{constdefs}\isanewline -~~add~::~{"}'a::nat~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}+{"}~60)\isanewline -~~{"}m~+~n~{\isasymequiv}~rec(m,~n,~{\isasymlambda}x~y.~Suc(y)){"}% +\ \ add\ ::\ {"}'a::nat\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}+{"}\ 60)\isanewline +\ \ {"}m\ +\ n\ {\isasymequiv}\ rec(m,\ n,\ {\isasymlambda}x\ y.\ Suc(y)){"}% \begin{isamarkuptext}% This is an abstract version of the plain $Nat$ theory in FOL.\footnote{See diff -r 0c8422ed066f -r fdc3b5bcd79d doc-src/AxClass/generated/Product.tex --- a/doc-src/AxClass/generated/Product.tex Fri Aug 04 10:59:22 2000 +0200 +++ b/doc-src/AxClass/generated/Product.tex Fri Aug 04 10:59:28 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% % \isamarkupheader{Syntactic classes} -\isacommand{theory}~Product~=~Main:% +\isacommand{theory}\ Product\ =\ Main:% \begin{isamarkuptext}% \medskip\noindent There is still a feature of Isabelle's type system left that we have not yet discussed. When declaring polymorphic @@ -17,9 +17,9 @@ syntactic type classes.% \end{isamarkuptext}% \isacommand{axclass}\isanewline -~~product~<~{"}term{"}\isanewline +\ \ product\ <\ {"}term{"}\isanewline \isacommand{consts}\isanewline -~~product~::~{"}'a::product~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)% +\ \ product\ ::\ {"}'a::product\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)% \begin{isamarkuptext}% Here class $product$ is defined as subclass of $term$ without any additional axioms. This effects in logical equivalence of $product$ @@ -48,10 +48,10 @@ This is done for class $product$ and type $bool$ as follows.% \end{isamarkuptext}% -\isacommand{instance}~bool~::~product\isanewline -~~\isacommand{by}~intro\_classes\isanewline -\isacommand{defs}~(\isakeyword{overloaded})\isanewline -~~product\_bool\_def:~{"}x~{\isasymOtimes}~y~{\isasymequiv}~x~{\isasymand}~y{"}% +\isacommand{instance}\ bool\ ::\ product\isanewline +\ \ \isacommand{by}\ intro\_classes\isanewline +\isacommand{defs}\ (\isakeyword{overloaded})\isanewline +\ \ product\_bool\_def:\ {"}x\ {\isasymOtimes}\ y\ {\isasymequiv}\ x\ {\isasymand}\ y{"}% \begin{isamarkuptext}% The definition $prod_bool_def$ becomes syntactically well-formed only after the arity $bool :: product$ is made known to the type checker. diff -r 0c8422ed066f -r fdc3b5bcd79d doc-src/AxClass/generated/Semigroups.tex --- a/doc-src/AxClass/generated/Semigroups.tex Fri Aug 04 10:59:22 2000 +0200 +++ b/doc-src/AxClass/generated/Semigroups.tex Fri Aug 04 10:59:28 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% % \isamarkupheader{Semigroups} -\isacommand{theory}~Semigroups~=~Main:% +\isacommand{theory}\ Semigroups\ =\ Main:% \begin{isamarkuptext}% \medskip\noindent An axiomatic type class is simply a class of types that all meet certain properties, which are also called \emph{class @@ -15,10 +15,10 @@ semigroups.% \end{isamarkuptext}% \isacommand{consts}\isanewline -~~times~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOtimes}{"}~70)\isanewline +\ \ times\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOtimes}{"}\ 70)\isanewline \isacommand{axclass}\isanewline -~~semigroup~<~{"}term{"}\isanewline -~~assoc:~{"}(x~{\isasymOtimes}~y)~{\isasymOtimes}~z~=~x~{\isasymOtimes}~(y~{\isasymOtimes}~z){"}% +\ \ semigroup\ <\ {"}term{"}\isanewline +\ \ assoc:\ {"}(x\ {\isasymOtimes}\ y)\ {\isasymOtimes}\ z\ =\ x\ {\isasymOtimes}\ (y\ {\isasymOtimes}\ z){"}% \begin{isamarkuptext}% \noindent Above we have first declared a polymorphic constant $\TIMES :: \alpha \To \alpha \To \alpha$ and then defined the class @@ -37,10 +37,10 @@ to semigroups $(\tau, \TIMES^\tau)$.% \end{isamarkuptext}% \isacommand{consts}\isanewline -~~plus~::~{"}'a~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a{"}~~~~(\isakeyword{infixl}~{"}{\isasymOplus}{"}~70)\isanewline +\ \ plus\ ::\ {"}'a\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a{"}\ \ \ \ (\isakeyword{infixl}\ {"}{\isasymOplus}{"}\ 70)\isanewline \isacommand{axclass}\isanewline -~~plus\_semigroup~<~{"}term{"}\isanewline -~~assoc:~{"}(x~{\isasymOplus}~y)~{\isasymOplus}~z~=~x~{\isasymOplus}~(y~{\isasymOplus}~z){"}% +\ \ plus\_semigroup\ <\ {"}term{"}\isanewline +\ \ assoc:\ {"}(x\ {\isasymOplus}\ y)\ {\isasymOplus}\ z\ =\ x\ {\isasymOplus}\ (y\ {\isasymOplus}\ z){"}% \begin{isamarkuptext}% \noindent Even if classes $plus_semigroup$ and $semigroup$ both represent semigroups in a sense, they are certainly not quite the