equal
deleted
inserted
replaced
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{prime{\isaliteral{5F}{\isacharunderscore}}def}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \begin{warn} |
|
20 A common mistake when writing definitions is to introduce extra free |
|
21 variables on the right-hand side. Consider the following, flawed definition |
|
22 (where \isa{dvd} means ``divides''): |
|
23 \begin{isabelle}% |
|
24 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}prime\ p\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ p\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}m\ dvd\ p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ m\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}% |
|
25 \end{isabelle} |
|
26 \par\noindent\hangindent=0pt |
|
27 Isabelle rejects this ``definition'' because of the extra \isa{m} on the |
|
28 right-hand side, which would introduce an inconsistency (why?). |
|
29 The correct version is |
|
30 \begin{isabelle}% |
|
31 \ \ \ \ \ {\isaliteral{22}{\isachardoublequote}}prime\ p\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isadigit{1}}\ {\isaliteral{3C}{\isacharless}}\ p\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}m{\isaliteral{2E}{\isachardot}}\ m\ dvd\ p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ m\ {\isaliteral{3D}{\isacharequal}}\ p{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}% |
|
32 \end{isabelle} |
|
33 \end{warn}% |
|
34 \end{isamarkuptext}% |
|
35 \isamarkuptrue% |
|
36 % |
|
37 \isadelimtheory |
|
38 % |
|
39 \endisadelimtheory |
|
40 % |
|
41 \isatagtheory |
|
42 % |
|
43 \endisatagtheory |
|
44 {\isafoldtheory}% |
|
45 % |
|
46 \isadelimtheory |
|
47 % |
|
48 \endisadelimtheory |
|
49 \end{isabellebody}% |
|
50 %%% Local Variables: |
|
51 %%% mode: latex |
|
52 %%% TeX-master: "root" |
|
53 %%% End: |
|