115 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
115 few predefined control symbols, such as \verb,\,\verb,<^sub>, and |
116 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
116 \verb,\,\verb,<^sup>, for sub- and superscript of the subsequent |
117 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
117 printable symbol, respectively. For example, \verb,A\<^sup>\<star>, is |
118 output as @{text "A\<^sup>\<star>"}. |
118 output as @{text "A\<^sup>\<star>"}. |
119 |
119 |
120 A number of symbols are considered letters by the Isabelle lexer |
120 A number of symbols are considered letters by the Isabelle lexer and |
121 and can be used as part of identifiers. These are the greek letters |
121 can be used as part of identifiers. These are the greek letters |
122 @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"}, etc apart from |
122 @{text "\<alpha>"} (\verb+\+\verb+<alpha>+), @{text "\<beta>"} |
123 @{text "\<lambda>"}, caligraphic letters like @{text "\<A>"} |
123 (\verb+\+\verb+<beta>+), etc. (excluding @{text "\<lambda>"}), |
124 (\verb+\+\verb+<A>+) and @{text "\<AA>"} (\verb+\+\verb+<AA>+), |
124 special letters like @{text "\<A>"} (\verb+\+\verb+<A>+) and @{text |
125 and the special control symbols \verb+\+\verb+<^isub>+ and |
125 "\<AA>"} (\verb+\+\verb+<AA>+), and the control symbols |
126 \verb+\+\verb+<^isup>+ for single letter sub and super scripts. This |
126 \verb+\+\verb+<^isub>+ and \verb+\+\verb+<^isup>+ for single letter |
127 means that the input |
127 sub and super scripts. This means that the input |
128 |
128 |
129 \medskip |
129 \medskip |
130 {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.\,\verb,<alpha>\<^isub>1=\,\verb,<Pi>\<^isup>\<A>,} |
130 {\small\noindent \verb,\,\verb,<forall>\,\verb,<alpha>\<^isub>1.,~\verb,\,\verb,<alpha>\<^isub>1 = \,\verb,<Pi>\<^isup>\<A>,} |
131 |
131 |
132 \medskip |
132 \medskip |
133 \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"} |
133 \noindent is recognized as the term @{term "\<forall>\<alpha>\<^isub>1. \<alpha>\<^isub>1 = \<Pi>\<^isup>\<A>"} |
134 by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single entity like |
134 by Isabelle. Note that @{text "\<Pi>\<^isup>\<A>"} is a single |
135 @{text "PA"}, not an exponentiation. |
135 syntactic entity, not an exponentiation. |
136 |
136 |
137 |
137 \medskip Replacing our previous definition of @{text xor} by the |
138 \medskip Replacing our definition of @{text xor} by the following |
138 following specifies an Isabelle symbol for the new operator: |
139 specifies an Isabelle symbol for the new operator: |
|
140 *} |
139 *} |
141 |
140 |
142 (*<*) |
141 (*<*) |
143 hide const xor |
142 hide const xor |
144 ML_setup {* Context.>> (Theory.add_path "version1") *} |
143 ML_setup {* Context.>> (Theory.add_path "version1") *} |
749 |
745 |
750 \begin{verbatim} |
746 \begin{verbatim} |
751 no_document use_thy "T"; |
747 no_document use_thy "T"; |
752 \end{verbatim} |
748 \end{verbatim} |
753 |
749 |
754 \medskip Theory output may be suppressed more selectively. Research |
750 \medskip Theory output may be suppressed more selectively, either |
755 articles and slides usually do not include the formal content in |
751 via \bfindex{tagged command regions} or \bfindex{ignored material}. |
756 full. Delimiting \bfindex{ignored material} by the special source |
752 |
757 comments \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and |
753 Tagged command regions works by annotating commands with named tags, |
758 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), tells the document |
754 which correspond to certain {\LaTeX} markup that tells how to treat |
759 preparation system to suppress these parts; the formal checking of |
755 particular parts of a document when doing the actual type-setting. |
760 the theory is unchanged, of course. |
756 By default, certain Isabelle/Isar commands are implicitly marked up |
761 |
757 using the predefined tags ``\emph{theory}'' (for theory begin and |
762 In this example, we hide a theory's \isakeyword{theory} and |
758 end), ``\emph{proof}'' (for proof commands), and ``\emph{ML}'' (for |
763 \isakeyword{end} brackets: |
759 commands involving ML code). Users may add their own tags using the |
764 |
760 \verb,%,\emph{tag} notation right after a command name. In the |
765 \medskip |
761 subsequent example we hide a particularly irrelevant proof: |
766 |
762 *} |
767 \begin{tabular}{l} |
763 |
768 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
764 lemma "x = x" by %invisible (simp) |
769 \texttt{theory T} \\ |
765 |
770 \texttt{imports Main} \\ |
766 text {* |
771 \texttt{begin} \\ |
767 The original source has been ``\verb,lemma "x = x" by %invisible (simp),''. |
772 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ |
768 Tags observe the structure of proofs; adjacent commands with the |
773 ~~$\vdots$ \\ |
769 same tag are joined into a single region. The Isabelle document |
774 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), \\ |
770 preparation system allows the user to specify how to interpret a |
775 \texttt{end} \\ |
771 tagged region, in order to keep, drop, or fold the corresponding |
776 \verb,(,\verb,*,\verb,>,\verb,*,\verb,), \\ |
772 parts of the document. See the \emph{Isabelle System Manual} |
777 \end{tabular} |
773 \cite{isabelle-sys} for further details, especially on |
778 |
774 \texttt{isatool usedir} and \texttt{isatool document}. |
779 \medskip |
775 |
780 |
776 Ignored material is specified by delimiting the original formal |
781 Text may be suppressed in a fine-grained manner. We may even hide |
777 source with special source comments |
782 vital parts of a proof, pretending that things have been simpler |
778 \verb,(,\verb,*,\verb,<,\verb,*,\verb,), and |
783 than they really were. For example, this ``fully automatic'' proof |
779 \verb,(,\verb,*,\verb,>,\verb,*,\verb,),. These parts are stripped |
784 is actually a fake: |
780 before the type-setting phase, without affecting the formal checking |
|
781 of the theory, of course. For example, we may hide parts of a proof |
|
782 that seem unfit for general public inspection. The following |
|
783 ``fully automatic'' proof is actually a fake: |
785 *} |
784 *} |
786 |
785 |
787 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x" |
786 lemma "x \<noteq> (0::int) \<Longrightarrow> 0 < x * x" |
788 by (auto(*<*)simp add: zero_less_mult_iff(*>*)) |
787 by (auto(*<*)simp add: zero_less_mult_iff(*>*)) |
789 |
788 |
790 text {* |
789 text {* |
791 \noindent Here the real source of the proof has been as follows: |
790 \noindent The real source of the proof has been as follows: |
792 |
791 |
793 \begin{verbatim} |
792 \begin{verbatim} |
794 by (auto(*<*)simp add: zero_less_mult_iff(*>*)) |
793 by (auto(*<*)simp add: zero_less_mult_iff(*>*)) |
795 \end{verbatim} |
794 \end{verbatim} |
796 %(* |
795 %(* |
797 |
796 |
798 \medskip Suppressing portions of printed text demands care. You |
797 \medskip Suppressing portions of printed text demands care. You |
799 should not misrepresent the underlying theory development. It is |
798 should not misrepresent the underlying theory development. It is |
800 easy to invalidate the visible text by hiding references to |
799 easy to invalidate the visible text by hiding references to |
801 questionable axioms. |
800 questionable axioms, for example. |
802 |
|
803 % I removed this because the page overflowed and I disagree a little. TN |
|
804 % |
|
805 % Authentic reports of Isabelle/Isar theories, say as part of a |
|
806 % library, should suppress nothing. Other users may need the full |
|
807 % information for their own derivative work. If a particular |
|
808 % formalization appears inadequate for general public coverage, it is |
|
809 % often more appropriate to think of a better way in the first place. |
|
810 |
|
811 \medskip Some technical subtleties of the |
|
812 \verb,(,\verb,*,\verb,<,\verb,*,\verb,),~\verb,(,\verb,*,\verb,>,\verb,*,\verb,), |
|
813 elements need to be kept in mind, too --- the system performs few |
|
814 sanity checks here. Arguments of markup commands and formal |
|
815 comments must not be hidden, otherwise presentation fails. Open and |
|
816 close parentheses need to be inserted carefully; it is easy to hide |
|
817 the wrong parts, especially after rearranging the theory text. |
|
818 *} |
801 *} |
819 |
802 |
820 (*<*) |
803 (*<*) |
821 end |
804 end |
822 (*>*) |
805 (*>*) |