6 |
6 |
7 text {* |
7 text {* |
8 The purpose of the package we show next is that the user just specifies the |
8 The purpose of the package we show next is that the user just specifies the |
9 inductive predicate by stating some introduction rules and then the packages |
9 inductive predicate by stating some introduction rules and then the packages |
10 makes the equivalent definition and derives from it the needed properties. |
10 makes the equivalent definition and derives from it the needed properties. |
|
11 *} |
|
12 |
|
13 text {* |
|
14 From a high-level perspective the package consists of 6 subtasks: |
|
15 |
|
16 \begin{itemize} |
|
17 \item reading the various parts of specification (i.e.~parser), |
|
18 \item transforming the parser outut into an internal |
|
19 (typed) datastructure, |
|
20 \item making the definitions, |
|
21 \item deriving the induction principles, |
|
22 \item deriving the introduction rules, and |
|
23 \item storing the results in the given theory. |
|
24 to the user. |
|
25 \end{itemize} |
|
26 |
|
27 *} |
|
28 |
|
29 text {* |
11 To be able to write down the specification in Isabelle, we have to introduce |
30 To be able to write down the specification in Isabelle, we have to introduce |
12 a new command (see Section~\ref{sec:newcommand}). As the keyword for the new |
31 a new command (see Section~\ref{sec:newcommand}). As the keyword for the new |
13 command we chose \simpleinductive{}. The specifications corresponding to our |
32 command we chose \simpleinductive{}. The specifications corresponding to our |
14 examples described earlier are: |
33 examples described earlier are: |
15 *} |
34 *} |
78 relation @{text R} is explicitly fixed. Simiraly the second definition |
97 relation @{text R} is explicitly fixed. Simiraly the second definition |
79 of the accessible part of the relation @{text R}. The last two definitions |
98 of the accessible part of the relation @{text R}. The last two definitions |
80 specify the same inductive predicates, but this time defined inside |
99 specify the same inductive predicates, but this time defined inside |
81 a locale.\label{fig:inddefsfixed}} |
100 a locale.\label{fig:inddefsfixed}} |
82 \end{figure} |
101 \end{figure} |
83 *} |
|
84 |
|
85 text {* |
|
86 From a high-level perspective the package consists of 6 subtasks: |
|
87 |
|
88 \begin{itemize} |
|
89 \item reading the various parts of specification (i.e.~parser), |
|
90 \item transforming the parser outut into an internal |
|
91 (typed) datastructure, |
|
92 \item making the definitions, |
|
93 \item deriving the induction principles, |
|
94 \item deriving the introduction rules, and |
|
95 \item storing the results in the given theory to be visible |
|
96 to the user. |
|
97 \end{itemize} |
|
98 |
|
99 *} |
102 *} |
100 |
103 |
101 text {* |
104 text {* |
102 \begin{figure}[p] |
105 \begin{figure}[p] |
103 \begin{isabelle} |
106 \begin{isabelle} |
230 |
233 |
231 @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE} |
234 @{ML_chunk [display,gray] SIMPLE_INDUCTIVE_PACKAGE} |
232 *} |
235 *} |
233 |
236 |
234 text {* |
237 text {* |
235 (FIXME: explain Binding.binding; mixfix; Attrib.src; Attrib.src somewhere else) |
238 (FIXME: explain Binding.binding; Attrib.binding somewhere else) |
236 |
239 |
237 |
240 |
238 The function for external invocation of the package is called @{ML |
241 The function for external invocation of the package is called @{ML |
239 add_inductive in SimpleInductivePackage}, whereas the one for internal |
242 add_inductive in SimpleInductivePackage}, whereas the one for internal |
240 invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both |
243 invocation is called @{ML add_inductive_i in SimpleInductivePackage}. Both |