146 assumed to be associative:% |
146 assumed to be associative:% |
147 \end{isamarkuptext}% |
147 \end{isamarkuptext}% |
148 \isamarkuptrue% |
148 \isamarkuptrue% |
149 \ \ \ \ \isacommand{class}\isamarkupfalse% |
149 \ \ \ \ \isacommand{class}\isamarkupfalse% |
150 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline |
150 \ semigroup\ {\isacharequal}\ type\ {\isacharplus}\isanewline |
151 \ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}\isactrlloc {\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
151 \ \ \ \ \ \ \isakeyword{fixes}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymotimes}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline |
152 \ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}y\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}% |
152 \ \ \ \ \ \ \isakeyword{assumes}\ assoc{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isasymotimes}\ z\ {\isacharequal}\ x\ {\isasymotimes}\ {\isacharparenleft}y\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}% |
153 \begin{isamarkuptext}% |
153 \begin{isamarkuptext}% |
154 \noindent This \isa{{\isasymCLASS}} specification consists of two |
154 \noindent This \isa{{\isasymCLASS}} specification consists of two |
155 parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them |
155 parts: the \qn{operational} part names the class parameter (\isa{{\isasymFIXES}}), the \qn{logical} part specifies properties on them |
156 (\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global |
156 (\isa{{\isasymASSUMES}}). The local \isa{{\isasymFIXES}} and \isa{{\isasymASSUMES}} are lifted to the theory toplevel, yielding the global |
157 parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the |
157 parameter \isa{{\isachardoublequote}mult\ {\isasymColon}\ {\isasymalpha}{\isasymColon}semigroup\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequote}} and the |
289 with its property:% |
289 with its property:% |
290 \end{isamarkuptext}% |
290 \end{isamarkuptext}% |
291 \isamarkuptrue% |
291 \isamarkuptrue% |
292 \ \ \ \ \isacommand{class}\isamarkupfalse% |
292 \ \ \ \ \isacommand{class}\isamarkupfalse% |
293 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline |
293 \ monoidl\ {\isacharequal}\ semigroup\ {\isacharplus}\isanewline |
294 \ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}\isactrlloc {\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
294 \ \ \ \ \ \ \isakeyword{fixes}\ neutral\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}{\isachardoublequoteclose}\ {\isacharparenleft}{\isachardoublequoteopen}{\isasymone}{\isachardoublequoteclose}{\isacharparenright}\isanewline |
295 \ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}\isactrlloc {\isasymone}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}% |
295 \ \ \ \ \ \ \isakeyword{assumes}\ neutl{\isacharcolon}\ {\isachardoublequoteopen}{\isasymone}\ {\isasymotimes}\ x\ {\isacharequal}\ x{\isachardoublequoteclose}% |
296 \begin{isamarkuptext}% |
296 \begin{isamarkuptext}% |
297 \noindent Again, we make some instances, by |
297 \noindent Again, we make some instances, by |
298 providing suitable parameter definitions and proofs for the |
298 providing suitable parameter definitions and proofs for the |
299 additional specifications.% |
299 additional specifications.% |
300 \end{isamarkuptext}% |
300 \end{isamarkuptext}% |
468 with a corresponding instance:% |
468 with a corresponding instance:% |
469 \end{isamarkuptext}% |
469 \end{isamarkuptext}% |
470 \isamarkuptrue% |
470 \isamarkuptrue% |
471 \ \ \ \ \isacommand{class}\isamarkupfalse% |
471 \ \ \ \ \isacommand{class}\isamarkupfalse% |
472 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline |
472 \ group\ {\isacharequal}\ monoidl\ {\isacharplus}\isanewline |
473 \ \ \ \ \ \ \isakeyword{fixes}\ inverse\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \ \ \ {\isacharparenleft}{\isachardoublequoteopen}{\isacharparenleft}{\isacharunderscore}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}\ {\isacharbrackleft}{\isadigit{1}}{\isadigit{0}}{\isadigit{0}}{\isadigit{0}}{\isacharbrackright}\ {\isadigit{9}}{\isadigit{9}}{\isadigit{9}}{\isacharparenright}\isanewline |
473 \ \ \ \ \ \ \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 |
474 \ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline |
474 \ \ \ \ \ \ \isakeyword{assumes}\ invl{\isacharcolon}\ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
475 \isanewline |
475 \isanewline |
476 \ \ \ \ \isacommand{instance}\isamarkupfalse% |
476 \ \ \ \ \isacommand{instance}\isamarkupfalse% |
477 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline |
477 \ int\ {\isacharcolon}{\isacharcolon}\ group\isanewline |
478 \ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline |
478 \ \ \ \ \ \ inverse{\isacharunderscore}int{\isacharunderscore}def{\isacharcolon}\ {\isachardoublequoteopen}i{\isasymdiv}\ {\isasymequiv}\ {\isacharminus}\ i{\isachardoublequoteclose}\isanewline |
479 % |
479 % |
610 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which |
610 now establish the \isa{left{\isacharunderscore}cancel} lemma for groups, which |
611 states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:% |
611 states that the function \isa{{\isacharparenleft}x\ {\isasymcirc}{\isacharparenright}} is injective:% |
612 \end{isamarkuptext}% |
612 \end{isamarkuptext}% |
613 \isamarkuptrue% |
613 \isamarkuptrue% |
614 \ \ \ \ \isacommand{lemma}\isamarkupfalse% |
614 \ \ \ \ \isacommand{lemma}\isamarkupfalse% |
615 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
615 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\ left{\isacharunderscore}cancel{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z\ {\isasymlongleftrightarrow}\ y\ {\isacharequal}\ z{\isachardoublequoteclose}\isanewline |
616 % |
616 % |
617 \isadelimproof |
617 \isadelimproof |
618 \ \ \ \ % |
618 \ \ \ \ % |
619 \endisadelimproof |
619 \endisadelimproof |
620 % |
620 % |
621 \isatagproof |
621 \isatagproof |
622 \isacommand{proof}\isamarkupfalse% |
622 \isacommand{proof}\isamarkupfalse% |
623 \isanewline |
623 \isanewline |
624 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
624 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
625 \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline |
625 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ y\ {\isacharequal}\ x\ {\isasymotimes}\ z{\isachardoublequoteclose}\isanewline |
626 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
626 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
627 \ \isacommand{have}\isamarkupfalse% |
627 \ \isacommand{have}\isamarkupfalse% |
628 \ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
628 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ y{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ z{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
629 \ simp\isanewline |
629 \ simp\isanewline |
630 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
630 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
631 \ \isacommand{have}\isamarkupfalse% |
631 \ \isacommand{have}\isamarkupfalse% |
632 \ {\isachardoublequoteopen}{\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isacharparenright}\ \isactrlloc {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
632 \ {\isachardoublequoteopen}{\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ y\ {\isacharequal}\ {\isacharparenleft}x{\isasymdiv}\ {\isasymotimes}\ x{\isacharparenright}\ {\isasymotimes}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
633 \ assoc\ \isacommand{by}\isamarkupfalse% |
633 \ assoc\ \isacommand{by}\isamarkupfalse% |
634 \ simp\isanewline |
634 \ simp\isanewline |
635 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
635 \ \ \ \ \ \ \isacommand{then}\isamarkupfalse% |
636 \ \isacommand{show}\isamarkupfalse% |
636 \ \isacommand{show}\isamarkupfalse% |
637 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
637 \ {\isachardoublequoteopen}y\ {\isacharequal}\ z{\isachardoublequoteclose}\ \isacommand{using}\isamarkupfalse% |
672 \end{isamarkuptext}% |
672 \end{isamarkuptext}% |
673 \isamarkuptrue% |
673 \isamarkuptrue% |
674 \ \ \ \ \isacommand{fun}\isamarkupfalse% |
674 \ \ \ \ \isacommand{fun}\isamarkupfalse% |
675 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline |
675 \ {\isacharparenleft}\isakeyword{in}\ monoid{\isacharparenright}\isanewline |
676 \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
676 \ \ \ \ \ \ pow{\isacharunderscore}nat\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
677 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\isanewline |
677 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isadigit{0}}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\isanewline |
678 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ \isactrlloc {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}% |
678 \ \ \ \ \ \ {\isacharbar}\ {\isachardoublequoteopen}pow{\isacharunderscore}nat\ {\isacharparenleft}Suc\ n{\isacharparenright}\ x\ {\isacharequal}\ x\ {\isasymotimes}\ pow{\isacharunderscore}nat\ n\ x{\isachardoublequoteclose}% |
679 \begin{isamarkuptext}% |
679 \begin{isamarkuptext}% |
680 \noindent If the locale \isa{group} is also a class, this local |
680 \noindent If the locale \isa{group} is also a class, this local |
681 definition is propagated onto a global definition of |
681 definition is propagated onto a global definition of |
682 \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}} |
682 \isa{{\isachardoublequote}pow{\isacharunderscore}nat\ {\isasymColon}\ nat\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}monoid{\isachardoublequote}} |
683 with corresponding theorems |
683 with corresponding theorems |
713 \ unfold{\isacharunderscore}locales\isanewline |
713 \ unfold{\isacharunderscore}locales\isanewline |
714 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
714 \ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% |
715 \ x\isanewline |
715 \ x\isanewline |
716 \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% |
716 \ \ \ \ \ \ \isacommand{from}\isamarkupfalse% |
717 \ invl\ \isacommand{have}\isamarkupfalse% |
717 \ invl\ \isacommand{have}\isamarkupfalse% |
718 \ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x\ {\isacharequal}\ \isactrlloc {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
718 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ x\ {\isacharequal}\ {\isasymone}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
719 \ simp\isanewline |
719 \ simp\isanewline |
720 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
720 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
721 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse% |
721 \ assoc\ {\isacharbrackleft}symmetric{\isacharbrackright}\ neutl\ invl\ \isacommand{have}\isamarkupfalse% |
722 \ {\isachardoublequoteopen}x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ {\isacharparenleft}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}{\isacharparenright}\ {\isacharequal}\ x\isactrlloc {\isasymdiv}\ \isactrlloc {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
722 \ {\isachardoublequoteopen}x{\isasymdiv}\ {\isasymotimes}\ {\isacharparenleft}x\ {\isasymotimes}\ {\isasymone}{\isacharparenright}\ {\isacharequal}\ x{\isasymdiv}\ {\isasymotimes}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
723 \ simp\isanewline |
723 \ simp\isanewline |
724 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
724 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse% |
725 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse% |
725 \ left{\isacharunderscore}cancel\ \isacommand{show}\isamarkupfalse% |
726 \ {\isachardoublequoteopen}x\ \isactrlloc {\isasymotimes}\ \isactrlloc {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
726 \ {\isachardoublequoteopen}x\ {\isasymotimes}\ {\isasymone}\ {\isacharequal}\ x{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
727 \ simp\isanewline |
727 \ simp\isanewline |
728 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
728 \ \ \ \ \isacommand{qed}\isamarkupfalse% |
729 % |
729 % |
730 \endisatagproof |
730 \endisatagproof |
731 {\isafoldproof}% |
731 {\isafoldproof}% |
732 % |
732 % |
733 \isadelimproof |
733 \isadelimproof |
734 % |
734 % |
735 \endisadelimproof |
735 \endisadelimproof |
736 % |
736 % |
737 \begin{isamarkuptext}% |
737 \begin{isamarkuptext}% |
738 The logical proof is carried out on the locale level |
738 \noindent The logical proof is carried out on the locale level |
739 and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales} |
739 and thus conveniently is opened using the \isa{unfold{\isacharunderscore}locales} |
740 method which only leaves the logical differences still |
740 method which only leaves the logical differences still |
741 open to proof to the user. After the proof it is propagated |
741 open to proof to the user. Afterwards it is propagated |
742 to the type system, making \isa{group} an instance of |
742 to the type system, making \isa{group} an instance of |
743 \isa{monoid}. For illustration, a derived definition |
743 \isa{monoid}. For illustration, a derived definition |
744 in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:% |
744 in \isa{group} which uses \isa{pow{\isacharunderscore}nat}:% |
745 \end{isamarkuptext}% |
745 \end{isamarkuptext}% |
746 \isamarkuptrue% |
746 \isamarkuptrue% |
747 \ \ \ \ \isacommand{definition}\isamarkupfalse% |
747 \ \ \ \ \isacommand{definition}\isamarkupfalse% |
748 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline |
748 \ {\isacharparenleft}\isakeyword{in}\ group{\isacharparenright}\isanewline |
749 \ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
749 \ \ \ \ \ \ pow{\isacharunderscore}int\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}int\ {\isasymRightarrow}\ {\isasymalpha}\ {\isasymRightarrow}\ {\isasymalpha}{\isachardoublequoteclose}\ \isakeyword{where}\isanewline |
750 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline |
750 \ \ \ \ \ \ {\isachardoublequoteopen}pow{\isacharunderscore}int\ k\ x\ {\isacharequal}\ {\isacharparenleft}if\ k\ {\isachargreater}{\isacharequal}\ {\isadigit{0}}\isanewline |
751 \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline |
751 \ \ \ \ \ \ \ \ then\ pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ k{\isacharparenright}\ x\isanewline |
752 \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}\isactrlloc {\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}% |
752 \ \ \ \ \ \ \ \ else\ {\isacharparenleft}pow{\isacharunderscore}nat\ {\isacharparenleft}nat\ {\isacharparenleft}{\isacharminus}\ k{\isacharparenright}{\isacharparenright}\ x{\isacharparenright}{\isasymdiv}{\isacharparenright}{\isachardoublequoteclose}% |
753 \begin{isamarkuptext}% |
753 \begin{isamarkuptext}% |
754 yields the global definition of |
754 \noindent yields the global definition of |
755 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}} |
755 \isa{{\isachardoublequote}pow{\isacharunderscore}int\ {\isasymColon}\ int\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group\ {\isasymRightarrow}\ {\isasymalpha}{\isasymColon}group{\isachardoublequote}} |
756 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}}.% |
756 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}}.% |
757 \end{isamarkuptext}% |
757 \end{isamarkuptext}% |
758 \isamarkuptrue% |
758 \isamarkuptrue% |
759 % |
759 % |