5 section {* Parsing and Typing the Specification\label{sec:interface} *} |
5 section {* Parsing and Typing the Specification\label{sec:interface} *} |
6 |
6 |
7 text {* |
7 text {* |
8 To be able to write down the specification in Isabelle, we have to introduce |
8 To be able to write down the specification in Isabelle, we have to introduce |
9 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
9 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
10 new command we chose \simpleinductive{}. In the package we want to support |
10 new command we chose \simpleinductive{}. The ``infrastructure'' already |
11 some ``advanced'' features: First, we want that the package can cope with |
11 provides an ``advanced'' feature for this command. For example we will |
12 specifications inside locales. For example it should be possible to declare |
12 be able to declare the locale |
13 *} |
13 *} |
14 |
14 |
15 locale rel = |
15 locale rel = |
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
17 |
17 |
18 text {* |
18 text {* |
19 and then define the transitive closure and the accessible part as follows: |
19 and then define the transitive closure and the accessible part of this |
20 *} |
20 locale as follows: |
21 |
21 *} |
22 |
22 |
23 simple_inductive (in rel) |
23 simple_inductive (in rel) |
24 trcl' |
24 trcl' |
25 where |
25 where |
26 base: "trcl' x x" |
26 base: "trcl' x x" |
28 |
28 |
29 simple_inductive (in rel) |
29 simple_inductive (in rel) |
30 accpart' |
30 accpart' |
31 where |
31 where |
32 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
32 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
33 |
|
34 text {* |
|
35 Second, we want that the user can specify fixed parameters. |
|
36 Remember in the previous section we stated that the user can give the |
|
37 specification for the transitive closure of a relation @{text R} as |
|
38 *} |
|
39 |
|
40 simple_inductive |
|
41 trcl\<iota>\<iota> :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
42 where |
|
43 base: "trcl\<iota>\<iota> R x x" |
|
44 | step: "trcl\<iota>\<iota> R x y \<Longrightarrow> R y z \<Longrightarrow> trcl\<iota>\<iota> R x z" |
|
45 |
|
46 text {* |
|
47 Note that there is no locale given in this specification---the parameter |
|
48 @{text "R"} therefore needs to be included explicitly in @{term trcl\<iota>\<iota>}, but |
|
49 stays fixed throughout the specification. The problem with this way of |
|
50 stating the specification for the transitive closure is that it derives the |
|
51 following induction principle. |
|
52 |
|
53 \begin{center}\small |
|
54 \mprset{flushleft} |
|
55 \mbox{\inferrule{ |
|
56 @{thm_style prem1 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
|
57 @{thm_style prem2 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}\\\\ |
|
58 @{thm_style prem3 trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}} |
|
59 {@{thm_style concl trcl\<iota>\<iota>.induct[where P=P, where z=R, where za=x, where zb=y]}}} |
|
60 \end{center} |
|
61 |
|
62 But this does not correspond to the induction principle we derived by hand, which |
|
63 was |
|
64 |
|
65 \begin{center}\small |
|
66 \mprset{flushleft} |
|
67 \mbox{\inferrule{ |
|
68 @{thm_style prem1 trcl_induct[no_vars]}\\\\ |
|
69 @{thm_style prem2 trcl_induct[no_vars]}\\\\ |
|
70 @{thm_style prem3 trcl_induct[no_vars]}} |
|
71 {@{thm_style concl trcl_induct[no_vars]}}} |
|
72 \end{center} |
|
73 |
|
74 The difference is that in the one derived by hand the relation @{term R} is not |
|
75 a parameter of the proposition @{term P} to be proved and it is also not universally |
|
76 qunatified in the second and third premise. The point is that the parameter @{term R} |
|
77 stays fixed thoughout the definition and we do not want to regard it as an ``ordinary'' |
|
78 argument of the transitive closure, but one that can be freely instantiated. |
|
79 In order to recognise such parameters, we have to extend the specification |
|
80 to include a mechanism to state fixed parameters. The user should be able |
|
81 to write |
|
82 |
|
83 *} |
|
84 |
|
85 simple_inductive |
|
86 trcl'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
87 where |
|
88 base: "trcl'' R x x" |
|
89 | step: "trcl'' R x y \<Longrightarrow> R y z \<Longrightarrow> trcl'' R x z" |
|
90 |
|
91 simple_inductive |
|
92 accpart'' for R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
93 where |
|
94 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart'' R y) \<Longrightarrow> accpart'' R x" |
|
95 |
33 |
96 text {* |
34 text {* |
97 \begin{figure}[t] |
35 \begin{figure}[t] |
98 \begin{isabelle} |
36 \begin{isabelle} |
99 \railnontermfont{\rmfamily\itshape} |
37 \railnontermfont{\rmfamily\itshape} |
100 \railterm{simpleinductive,where,for} |
38 \railterm{simpleinductive,where,for} |
101 \railalias{simpleinductive}{\simpleinductive{}} |
39 \railalias{simpleinductive}{\simpleinductive{}} |
102 \railalias{where}{\isacommand{where}} |
40 \railalias{where}{\isacommand{where}} |
103 \railalias{for}{\isacommand{for}} |
41 \railalias{for}{\isacommand{for}} |
104 \begin{rail} |
42 \begin{rail} |
105 simpleinductive target? fixes (for fixes)? \\ |
43 simpleinductive target?\\ fixes |
106 (where (thmdecl? prop + '|'))? |
44 (where (thmdecl? prop + '|'))? |
107 ; |
45 ; |
108 \end{rail} |
46 \end{rail} |
109 \end{isabelle} |
47 \end{isabelle} |
110 \caption{A railroad diagram describing the syntax of \simpleinductive{}. |
48 \caption{A railroad diagram describing the syntax of \simpleinductive{}. |
111 The \emph{target} indicates an optional locale; the \emph{fixes} are an |
49 The \emph{target} indicates an optional locale; the \emph{fixes} are an |
112 \isacommand{and}-separated list of names for the inductive predicates (they |
50 \isacommand{and}-separated list of names for the inductive predicates (they |
113 can also contain typing- and syntax anotations); similarly the \emph{fixes} |
51 can also contain typing- and syntax anotations); \emph{prop} stands for a |
114 after \isacommand{for} to indicate fixed parameters; \emph{prop} stands for a |
|
115 introduction rule with an optional theorem declaration (\emph{thmdecl}). |
52 introduction rule with an optional theorem declaration (\emph{thmdecl}). |
116 \label{fig:railroad}} |
53 \label{fig:railroad}} |
117 \end{figure} |
54 \end{figure} |
118 *} |
55 *} |
119 |
56 |
120 text {* |
57 text {* |
121 This leads directly to the railroad diagram shown in |
58 This leads directly to the railroad diagram shown in |
122 Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram |
59 Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram |
123 more or less translates directly into the parser: |
60 more or less translates directly into the parser: |
124 |
61 *} |
125 @{ML_chunk [display,gray] parser} |
62 |
126 |
63 ML %linenosgray{*val spec_parser = |
|
64 OuterParse.fixes -- |
|
65 Scan.optional |
|
66 (OuterParse.$$$ "where" |-- |
|
67 OuterParse.!!! |
|
68 (OuterParse.enum1 "|" |
|
69 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
|
70 |
|
71 text {* |
127 which we described in Section~\ref{sec:parsingspecs}. If we feed into the |
72 which we described in Section~\ref{sec:parsingspecs}. If we feed into the |
128 parser the string (which corresponds to our definition of @{term even} and |
73 parser the string (which corresponds to our definition of @{term even} and |
129 @{term odd}): |
74 @{term odd}): |
130 |
75 |
131 @{ML_response [display,gray] |
76 @{ML_response [display,gray] |