equal
deleted
inserted
replaced
1 % |
1 % |
2 \begin{isabellebody}% |
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{prime_def}% |
3 % |
4 % |
4 \begin{isamarkuptext}% |
5 \begin{isamarkuptext}% |
5 \begin{warn} |
6 \begin{warn} |
6 A common mistake when writing definitions is to introduce extra free |
7 A common mistake when writing definitions is to introduce extra free |
7 variables on the right-hand side as in the following fictitious definition: |
8 variables on the right-hand side as in the following fictitious definition: |
8 % |
|
9 \begin{isabelle}% |
9 \begin{isabelle}% |
10 \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}% |
10 \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}% |
11 \end{isabelle}% |
11 \end{isabelle} |
12 |
|
13 where \isa{dvd} means ``divides''. |
12 where \isa{dvd} means ``divides''. |
14 Isabelle rejects this ``definition'' because of the extra \isa{m} on the |
13 Isabelle rejects this ``definition'' because of the extra \isa{m} on the |
15 right-hand side, which would introduce an inconsistency (why?). What you |
14 right-hand side, which would introduce an inconsistency (why?). What you |
16 should have written is |
15 should have written is |
17 % |
|
18 \begin{isabelle}% |
16 \begin{isabelle}% |
19 \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}% |
17 \ \ \ \ \ {\isachardoublequote}prime\ p\ {\isasymequiv}\ \isadigit{1}\ {\isacharless}\ p\ {\isasymand}\ {\isacharparenleft}{\isasymforall}m{\isachardot}\ m\ dvd\ p\ {\isasymlongrightarrow}\ m\ {\isacharequal}\ \isadigit{1}\ {\isasymor}\ m\ {\isacharequal}\ p{\isacharparenright}{\isachardoublequote}% |
20 \end{isabelle}% |
18 \end{isabelle} |
21 |
|
22 \end{warn}% |
19 \end{warn}% |
23 \end{isamarkuptext}% |
20 \end{isamarkuptext}% |
24 \end{isabellebody}% |
21 \end{isabellebody}% |
25 %%% Local Variables: |
22 %%% Local Variables: |
26 %%% mode: latex |
23 %%% mode: latex |