474 preserving maps can be declared in the following way.% |
474 preserving maps can be declared in the following way.% |
475 \end{isamarkuptext}% |
475 \end{isamarkuptext}% |
476 \isamarkuptrue% |
476 \isamarkuptrue% |
477 \ \ \isacommand{locale}\isamarkupfalse% |
477 \ \ \isacommand{locale}\isamarkupfalse% |
478 \ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline |
478 \ order{\isacharunderscore}preserving\ {\isacharequal}\isanewline |
479 \ \ \ \ partial{\isacharunderscore}order\ {\isacharplus}\ po{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline |
479 \ \ \ \ le{\isacharcolon}\ partial{\isacharunderscore}order\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ partial{\isacharunderscore}order\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline |
480 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline |
480 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b{\isachardoublequoteclose}\isanewline |
481 \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}% |
481 \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}le{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y\ {\isasymLongrightarrow}\ {\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}% |
482 \begin{isamarkuptext}% |
482 \begin{isamarkuptext}% |
483 The second line contains the expression, which is the |
483 The second line contains the expression, which is the |
484 merge of two partial order locales. The parameter of the second one |
484 merge of two partial order locales. The parameter of the second one |
503 right locale.% |
503 right locale.% |
504 \end{isamarkuptext}% |
504 \end{isamarkuptext}% |
505 \isamarkuptrue% |
505 \isamarkuptrue% |
506 % |
506 % |
507 \begin{isamarkuptext}% |
507 \begin{isamarkuptext}% |
508 % FIXME needs update |
508 The locale \isa{order{\isacharunderscore}preserving} contains theorems for both |
509 The locale \isa{order{\isacharunderscore}preserving} contains theorems for both |
|
510 orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}. How can one refer to a theorem for |
509 orders \isa{{\isasymsqsubseteq}} and \isa{{\isasympreceq}}. How can one refer to a theorem for |
511 a particular order, \isa{{\isasymsqsubseteq}} or \isa{{\isasympreceq}}? Names in locales are |
510 a particular order, \isa{{\isasymsqsubseteq}} or \isa{{\isasympreceq}}? Names in locales are |
512 qualified by the locale parameters. More precisely, a name is |
511 qualified by the locale parameters. More precisely, a name is |
513 qualified by the parameters of the locale in which its declaration |
512 qualified by the parameters of the locale in which its declaration |
514 occurs. Here are examples:% |
513 occurs. Here are examples:% |
528 \isadeliminvisible |
527 \isadeliminvisible |
529 % |
528 % |
530 \endisadeliminvisible |
529 \endisadeliminvisible |
531 % |
530 % |
532 \begin{isamarkuptext}% |
531 \begin{isamarkuptext}% |
533 % FIXME needs update? |
532 \isa{le{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasymsqsubseteq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymsqsubset}\ {\isacharquery}z} |
534 \isa{less{\isacharunderscore}le{\isacharunderscore}trans}: \isa{{\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z} |
|
535 |
533 |
536 \isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}% |
534 \isa{hom{\isacharunderscore}le}: \isa{{\isacharquery}x\ {\isasymsqsubseteq}\ {\isacharquery}y\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isacharquery}x\ {\isasympreceq}\ {\isasymphi}\ {\isacharquery}y}% |
537 \end{isamarkuptext}% |
535 \end{isamarkuptext}% |
538 \isamarkuptrue% |
536 \isamarkuptrue% |
539 % |
537 % |
540 \begin{isamarkuptext}% |
538 \begin{isamarkuptext}% |
541 When renaming a locale, the morphism is also applied |
539 When renaming a locale, the morphism is also applied |
542 to the qualifiers. Hence theorems for the partial order \isa{{\isasympreceq}} |
540 to the qualifiers. Hence theorems for the partial order \isa{{\isasympreceq}} |
543 are qualified by \isa{le{\isacharprime}}. For example, \isa{po{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}% |
541 are qualified by \isa{le{\isacharprime}}. For example, \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: \begin{isabelle}% |
544 \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline |
542 \ \ {\isasymlbrakk}partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\isanewline |
545 \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z% |
543 \isaindent{\ \ }{\isasymLongrightarrow}\ partial{\isacharunderscore}order{\isachardot}less\ op\ {\isasympreceq}\ {\isacharquery}x\ {\isacharquery}z% |
546 \end{isabelle}% |
544 \end{isabelle}% |
547 \end{isamarkuptext}% |
545 \end{isamarkuptext}% |
548 \isamarkuptrue% |
546 \isamarkuptrue% |
560 \isadeliminvisible |
558 \isadeliminvisible |
561 % |
559 % |
562 \endisadeliminvisible |
560 \endisadeliminvisible |
563 % |
561 % |
564 \begin{isamarkuptext}% |
562 \begin{isamarkuptext}% |
565 % FIXME needs update? |
563 This example reveals that there is no infix syntax for the strict |
566 This example reveals that there is no infix syntax for the strict |
|
567 version of \isa{{\isasympreceq}}! This can, of course, not be introduced |
564 version of \isa{{\isasympreceq}}! This can, of course, not be introduced |
568 automatically, but it can be declared manually through an abbreviation.% |
565 automatically, but it can be declared manually through an abbreviation.% |
569 \end{isamarkuptext}% |
566 \end{isamarkuptext}% |
570 \isamarkuptrue% |
567 \isamarkuptrue% |
571 \ \ \isacommand{abbreviation}\isamarkupfalse% |
568 \ \ \isacommand{abbreviation}\isamarkupfalse% |
590 Two more locales illustrate working with locale expressions. |
587 Two more locales illustrate working with locale expressions. |
591 A map \isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and join.% |
588 A map \isa{{\isasymphi}} is a lattice homomorphism if it preserves meet and join.% |
592 \end{isamarkuptext}% |
589 \end{isamarkuptext}% |
593 \isamarkuptrue% |
590 \isamarkuptrue% |
594 \ \ \isacommand{locale}\isamarkupfalse% |
591 \ \ \isacommand{locale}\isamarkupfalse% |
595 \ lattice{\isacharunderscore}hom\ {\isacharequal}\ lattice\ {\isacharplus}\ lat{\isacharprime}{\isacharbang}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline |
592 \ lattice{\isacharunderscore}hom\ {\isacharequal}\ le{\isacharcolon}\ lattice\ {\isacharplus}\ le{\isacharprime}{\isacharcolon}\ lattice\ le{\isacharprime}\ \isakeyword{for}\ le{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasympreceq}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ {\isacharplus}\isanewline |
596 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline |
593 \ \ \ \ \isakeyword{fixes}\ {\isasymphi}\isanewline |
597 \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\isanewline |
594 \ \ \ \ \isakeyword{assumes}\ hom{\isacharunderscore}meet{\isacharcolon}\isanewline |
598 \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
595 \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}meet\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}meet\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
599 \ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\isanewline |
596 \ \ \ \ \ \ \isakeyword{and}\ hom{\isacharunderscore}join{\isacharcolon}\isanewline |
600 \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}join\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}join\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
597 \ \ \ \ \ \ \ \ {\isachardoublequoteopen}{\isasymphi}\ {\isacharparenleft}lattice{\isachardot}join\ le\ x\ y{\isacharparenright}\ {\isacharequal}\ lattice{\isachardot}join\ le{\isacharprime}\ {\isacharparenleft}{\isasymphi}\ x{\isacharparenright}\ {\isacharparenleft}{\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
601 \isanewline |
598 \isanewline |
602 \ \ \isacommand{abbreviation}\isamarkupfalse% |
599 \ \ \isacommand{abbreviation}\isamarkupfalse% |
603 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline |
600 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline |
604 \ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline |
601 \ \ \ \ meet{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqinter}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}meet{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}meet{\isachardoublequoteclose}\isanewline |
605 \ \ \isacommand{abbreviation}\isamarkupfalse% |
602 \ \ \isacommand{abbreviation}\isamarkupfalse% |
606 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline |
603 \ {\isacharparenleft}\isakeyword{in}\ lattice{\isacharunderscore}hom{\isacharparenright}\isanewline |
607 \ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ lat{\isacharprime}{\isachardot}join{\isachardoublequoteclose}% |
604 \ \ \ \ join{\isacharprime}\ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isasymsqunion}{\isacharprime}{\isacharprime}{\isachardoublequoteclose}\ {\isadigit{5}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\ {\isachardoublequoteopen}join{\isacharprime}\ {\isasymequiv}\ le{\isacharprime}{\isachardot}join{\isachardoublequoteclose}% |
608 \begin{isamarkuptext}% |
605 \begin{isamarkuptext}% |
609 A homomorphism is an endomorphism if both orders coincide.% |
606 A homomorphism is an endomorphism if both orders coincide.% |
610 \end{isamarkuptext}% |
607 \end{isamarkuptext}% |
611 \isamarkuptrue% |
608 \isamarkuptrue% |
612 \ \ \isacommand{locale}\isamarkupfalse% |
609 \ \ \isacommand{locale}\isamarkupfalse% |
676 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
673 \ \ \ \ \isacommand{assume}\isamarkupfalse% |
677 \ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y{\isachardoublequoteclose}\isanewline |
674 \ {\isachardoublequoteopen}x\ {\isasymsqsubseteq}\ y{\isachardoublequoteclose}\isanewline |
678 \ \ \ \ \isacommand{then}\isamarkupfalse% |
675 \ \ \ \ \isacommand{then}\isamarkupfalse% |
679 \ \isacommand{have}\isamarkupfalse% |
676 \ \isacommand{have}\isamarkupfalse% |
680 \ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
677 \ {\isachardoublequoteopen}y\ {\isacharequal}\ {\isacharparenleft}x\ {\isasymsqunion}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
681 \ {\isacharparenleft}simp\ add{\isacharcolon}\ join{\isacharunderscore}connection{\isacharparenright}\isanewline |
678 \ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline |
682 \ \ \ \ \isacommand{then}\isamarkupfalse% |
679 \ \ \ \ \isacommand{then}\isamarkupfalse% |
683 \ \isacommand{have}\isamarkupfalse% |
680 \ \isacommand{have}\isamarkupfalse% |
684 \ {\isachardoublequoteopen}{\isasymphi}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymphi}\ x\ {\isasymsqunion}{\isacharprime}\ {\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
681 \ {\isachardoublequoteopen}{\isasymphi}\ y\ {\isacharequal}\ {\isacharparenleft}{\isasymphi}\ x\ {\isasymsqunion}{\isacharprime}\ {\isasymphi}\ y{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
685 \ {\isacharparenleft}simp\ add{\isacharcolon}\ hom{\isacharunderscore}join\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
682 \ {\isacharparenleft}simp\ add{\isacharcolon}\ hom{\isacharunderscore}join\ {\isacharbrackleft}symmetric{\isacharbrackright}{\isacharparenright}\isanewline |
686 \ \ \ \ \isacommand{then}\isamarkupfalse% |
683 \ \ \ \ \isacommand{then}\isamarkupfalse% |
687 \ \isacommand{show}\isamarkupfalse% |
684 \ \isacommand{show}\isamarkupfalse% |
688 \ {\isachardoublequoteopen}{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
685 \ {\isachardoublequoteopen}{\isasymphi}\ x\ {\isasympreceq}\ {\isasymphi}\ y{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse% |
689 \ {\isacharparenleft}simp\ add{\isacharcolon}\ lat{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline |
686 \ {\isacharparenleft}simp\ add{\isacharcolon}\ le{\isacharprime}{\isachardot}join{\isacharunderscore}connection{\isacharparenright}\isanewline |
690 \ \ \isacommand{qed}\isamarkupfalse% |
687 \ \ \isacommand{qed}\isamarkupfalse% |
691 % |
688 % |
692 \endisatagproof |
689 \endisatagproof |
693 {\isafoldproof}% |
690 {\isafoldproof}% |
694 % |
691 % |
698 % |
695 % |
699 \begin{isamarkuptext}% |
696 \begin{isamarkuptext}% |
700 Theorems and other declarations --- syntax, in particular --- |
697 Theorems and other declarations --- syntax, in particular --- |
701 from the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example |
698 from the locale \isa{order{\isacharunderscore}preserving} are now active in \isa{lattice{\isacharunderscore}hom}, for example |
702 |
699 |
703 \isa{lat{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: |
700 \isa{le{\isacharprime}{\isachardot}less{\isacharunderscore}le{\isacharunderscore}trans}: |
704 \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}% |
701 \isa{{\isasymlbrakk}{\isacharquery}x\ {\isasymprec}\ {\isacharquery}y{\isacharsemicolon}\ {\isacharquery}y\ {\isasympreceq}\ {\isacharquery}z{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}x\ {\isasymprec}\ {\isacharquery}z}% |
705 \end{isamarkuptext}% |
702 \end{isamarkuptext}% |
706 \isamarkuptrue% |
703 \isamarkuptrue% |
707 % |
704 % |
708 \isamarkupsection{Further Reading% |
705 \isamarkupsection{Further Reading% |
742 \begin{tabular}{l>$c<$l} |
739 \begin{tabular}{l>$c<$l} |
743 \multicolumn{3}{l}{Miscellaneous} \\ |
740 \multicolumn{3}{l}{Miscellaneous} \\ |
744 |
741 |
745 \textit{attr-name} & ::= |
742 \textit{attr-name} & ::= |
746 & \textit{name} $|$ \textit{attribute} $|$ |
743 & \textit{name} $|$ \textit{attribute} $|$ |
747 \textit{name} \textit{attribute} \\[2ex] |
744 \textit{name} \textit{attribute} \\ |
|
745 \textit{qualifier} & ::= |
|
746 & \textit{name} [``\textbf{!}''] \\[2ex] |
748 |
747 |
749 \multicolumn{3}{l}{Context Elements} \\ |
748 \multicolumn{3}{l}{Context Elements} \\ |
750 |
749 |
751 \textit{fixes} & ::= |
750 \textit{fixes} & ::= |
752 & \textit{name} [ ``\textbf{::}'' \textit{type} ] |
751 & \textit{name} [ ``\textbf{::}'' \textit{type} ] |
782 % & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\ |
781 % & \textbf{notes} \textit{notes} ( \textbf{and} \textit{notes} )$^*$ \\ |
783 %\end{comment} |
782 %\end{comment} |
784 |
783 |
785 \multicolumn{3}{l}{Locale Expressions} \\ |
784 \multicolumn{3}{l}{Locale Expressions} \\ |
786 |
785 |
787 \textit{rename} & ::= |
786 \textit{pos-insts} & ::= |
788 & \textit{name} [ \textit{mixfix} ] $|$ ``\textbf{\_}'' \\ |
787 & ( \textit{term} $|$ ``\textbf{\_}'' )$^*$ \\ |
789 \textit{expr} & ::= |
788 \textit{named-insts} & ::= |
790 & \textit{renamed-expr} ( ``\textbf{+}'' \textit{renamed-expr} )$^*$ \\ |
789 & \textbf{where} \textit{name} ``\textbf{=}'' \textit{term} |
791 \textit{renamed-expr} & ::= |
790 ( \textbf{and} \textit{name} ``\textbf{=}'' \textit{term} )$^*$ \\ |
792 & ( \textit{qualified-name} $|$ |
791 \textit{instance} & ::= |
793 ``\textbf{(}'' \textit{expr} ``\textbf{)}'' ) \textit{rename}$^*$ \\[2ex] |
792 & [ \textit{qualifier} \textbf{:} ] |
|
793 \textit{qualified-name} ( \textit{pos-insts} $|$ \textit{named-inst} ) \\ |
|
794 \textit{expression} & ::= |
|
795 & \textit{instance} ( ``\textbf{+}'' \textit{instance} )$^*$ |
|
796 [ \textbf{for} \textit{fixes} ( \textbf{and} \textit{fixes} )$^*$ ] \\[2ex] |
794 |
797 |
795 \multicolumn{3}{l}{Declaration of Locales} \\ |
798 \multicolumn{3}{l}{Declaration of Locales} \\ |
796 |
799 |
797 \textit{locale} & ::= |
800 \textit{locale} & ::= |
798 & \textit{element}$^+$ \\ |
801 & \textit{element}$^+$ \\ |
799 & | & \textit{locale-expr} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ |
802 & | & \textit{expression} [ ``\textbf{+}'' \textit{element}$^+$ ] \\ |
800 \textit{toplevel} & ::= |
803 \textit{toplevel} & ::= |
801 & \textbf{locale} \textit{name} [ ``\textbf{=}'' |
804 & \textbf{locale} \textit{name} [ ``\textbf{=}'' |
802 \textit{locale} ] \\[2ex] |
805 \textit{locale} ] \\[2ex] |
803 |
806 |
804 \multicolumn{3}{l}{Interpretation} \\ |
807 \multicolumn{3}{l}{Interpretation} \\ |
805 |
808 |
806 \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ] |
809 \textit{equation} & ::= & [ \textit{attr-name} ``\textbf{:}'' ] |
807 \textit{prop} \\ |
810 \textit{prop} \\ |
808 \textit{insts} & ::= & [ ``\textbf{[}'' \textit{term}$^+$ |
811 \textit{equations} & ::= & \textbf{where} \textit{equation} ( \textbf{and} |
809 ``\textbf{]}'' ] \\ |
812 \textit{equation} )$^*$ \\ |
810 & & [ \textbf{where} \textit{equation} ( \textbf{and} |
|
811 \textit{equation} )$^*$ ] \\ |
|
812 \textit{toplevel} & ::= |
813 \textit{toplevel} & ::= |
813 & \textbf{interpretation} \textit{name} ( ``$<$'' $|$ |
814 & \textbf{sublocale} \textit{name} ( ``$<$'' $|$ |
814 ``$\subseteq$'' ) \textit{expr} \textit{proof} \\ |
815 ``$\subseteq$'' ) \textit{expression} \textit{proof} \\ |
815 & | |
816 & | |
816 & \textbf{interpretation} [ \textit{attr-name} ``\textbf{:}'' ] |
817 & \textbf{interpretation} |
817 \textit{expr} \textit{insts} \textit{proof} \\ |
818 \textit{expression} [ \textit{equations} ] \textit{proof} \\ |
818 & | |
819 & | |
819 & \textbf{interpret} [ \textit{attr-name} ``\textbf{:}'' ] |
820 & \textbf{interpret} |
820 \textit{expr} \textit{insts} \textit{proof} \\[2ex] |
821 \textit{expression} \textit{proof} \\[2ex] |
821 |
822 |
822 \multicolumn{3}{l}{Diagnostics} \\ |
823 \multicolumn{3}{l}{Diagnostics} \\ |
823 |
824 |
824 \textit{toplevel} & ::= |
825 \textit{toplevel} & ::= |
825 & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ |
826 & \textbf{print\_locale} [ ``\textbf{!}'' ] \textit{locale} \\ |
826 & | & \textbf{print\_locales} |
827 & | & \textbf{print\_locales} |
827 \end{tabular} |
828 \end{tabular} |
828 \end{center} |
829 \end{center} |
829 \hrule |
830 \hrule |
830 \caption{Syntax of Locale Commands.} |
831 \caption{Syntax of Locale Commands (abridged).} |
831 \label{tab:commands} |
832 \label{tab:commands} |
832 \end{table}% |
833 \end{table}% |
833 \end{isamarkuptext}% |
834 \end{isamarkuptext}% |
834 \isamarkuptrue% |
835 \isamarkuptrue% |
835 % |
836 % |