1 theory Ind_Interface |
1 theory Ind_Interface |
2 imports "../Base" "../Parsing" Ind_Prelims Simple_Inductive_Package |
2 imports "../Base" "../Parsing" Simple_Inductive_Package |
3 begin |
3 begin |
4 |
4 |
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_raw {* |
8 To be able to write down the specification in Isabelle, we have to introduce |
8 \begin{figure}[p] |
9 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
9 \begin{boxedminipage}{\textwidth} |
10 new command we chose \simpleinductive{}. The ``infrastructure'' already |
10 \begin{isabelle} |
11 provides an ``advanced'' feature for this command. For example we will |
11 *} |
12 be able to declare the locale |
12 simple_inductive |
13 *} |
13 trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" |
14 |
14 where |
15 locale rel = |
15 base: "trcl R x x" |
16 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
16 | step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z" |
17 |
17 |
18 text {* |
18 simple_inductive |
19 and then define the transitive closure and the accessible part of this |
19 even and odd |
20 locale as follows: |
20 where |
21 *} |
21 even0: "even 0" |
22 |
22 | evenS: "odd n \<Longrightarrow> even (Suc n)" |
23 simple_inductive (in rel) |
23 | oddS: "even n \<Longrightarrow> odd (Suc n)" |
24 trcl' |
24 |
25 where |
25 simple_inductive |
26 base: "trcl' x x" |
26 accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool" |
27 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z" |
27 where |
28 |
28 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x" |
29 simple_inductive (in rel) |
29 |
30 accpart' |
30 (*<*) |
31 where |
31 datatype trm = |
32 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
32 Var "string" |
33 |
33 | App "trm" "trm" |
34 text {* |
34 | Lam "string" "trm" |
35 \begin{figure}[t] |
35 (*>*) |
|
36 |
|
37 simple_inductive |
|
38 fresh :: "string \<Rightarrow> trm \<Rightarrow> bool" |
|
39 where |
|
40 fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)" |
|
41 | fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)" |
|
42 | fresh_lam1: "fresh a (Lam a t)" |
|
43 | fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)" |
|
44 text_raw {* |
|
45 \end{isabelle} |
|
46 \end{boxedminipage} |
|
47 \caption{Specification given by the user for the inductive predicates |
|
48 @{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and |
|
49 @{text "fresh"}.\label{fig:specs}} |
|
50 \end{figure} |
|
51 *} |
|
52 |
|
53 text {* |
|
54 \begin{figure}[p] |
|
55 \begin{boxedminipage}{\textwidth} |
36 \begin{isabelle} |
56 \begin{isabelle} |
37 \railnontermfont{\rmfamily\itshape} |
57 \railnontermfont{\rmfamily\itshape} |
38 \railterm{simpleinductive,where,for} |
58 \railterm{simpleinductive,where,for} |
39 \railalias{simpleinductive}{\simpleinductive{}} |
59 \railalias{simpleinductive}{\simpleinductive{}} |
40 \railalias{where}{\isacommand{where}} |
60 \railalias{where}{\isacommand{where}} |
43 simpleinductive target?\\ fixes |
63 simpleinductive target?\\ fixes |
44 (where (thmdecl? prop + '|'))? |
64 (where (thmdecl? prop + '|'))? |
45 ; |
65 ; |
46 \end{rail} |
66 \end{rail} |
47 \end{isabelle} |
67 \end{isabelle} |
|
68 \end{boxedminipage} |
48 \caption{A railroad diagram describing the syntax of \simpleinductive{}. |
69 \caption{A railroad diagram describing the syntax of \simpleinductive{}. |
49 The \emph{target} indicates an optional locale; the \emph{fixes} are an |
70 The \emph{target} indicates an optional locale; the \emph{fixes} are an |
50 \isacommand{and}-separated list of names for the inductive predicates (they |
71 \isacommand{and}-separated list of names for the inductive predicates (they |
51 can also contain typing- and syntax anotations); \emph{prop} stands for a |
72 can also contain typing- and syntax anotations); \emph{prop} stands for a |
52 introduction rule with an optional theorem declaration (\emph{thmdecl}). |
73 introduction rule with an optional theorem declaration (\emph{thmdecl}). |
53 \label{fig:railroad}} |
74 \label{fig:railroad}} |
54 \end{figure} |
75 \end{figure} |
55 *} |
76 *} |
56 |
77 |
57 text {* |
78 text {* |
58 This leads directly to the railroad diagram shown in |
79 To be able to write down the specification in Isabelle, we have to introduce |
59 Figure~\ref{fig:railroad} for the syntax of \simpleinductive{}. This diagram |
80 a new command (see Section~\ref{sec:newcommand}). As the keyword for the |
60 more or less translates directly into the parser: |
81 new command we chose \simpleinductive{}. Examples of specifications we expect |
61 *} |
82 the user gives for the inductive predicates from the previous section are |
62 |
83 shown in Figure~ref{fig:specs}. The general syntax we will parse is specified |
63 ML %linenosgray{*val spec_parser = |
84 in the railroad diagram shown in Figure~\ref{fig:railroad} for the syntax of |
64 OuterParse.fixes -- |
85 \simpleinductive{}. This diagram more or less translates directly into |
65 Scan.optional |
86 the parser: |
66 (OuterParse.$$$ "where" |-- |
87 *} |
67 OuterParse.!!! |
88 |
68 (OuterParse.enum1 "|" |
89 ML{*val spec_parser = |
69 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
90 OuterParse.fixes -- |
70 |
91 Scan.optional |
71 text {* |
92 (OuterParse.$$$ "where" |-- |
72 which we described in Section~\ref{sec:parsingspecs}. If we feed into the |
93 OuterParse.!!! |
|
94 (OuterParse.enum1 "|" |
|
95 (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*} |
|
96 |
|
97 text {* |
|
98 which we explaind in Section~\ref{sec:parsingspecs}. |
|
99 If you look closely, there is no code for parsing the optional |
|
100 target in Figure~\ref{fig:railroad}. This is an ``advanced'' feature |
|
101 which we will inherit for ``free'' from the infrastructure on which |
|
102 we build the package. The target stands for a locale and allows us |
|
103 to specify |
|
104 *} |
|
105 |
|
106 locale rel = |
|
107 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
|
108 |
|
109 text {* |
|
110 and then define the transitive closure and the accessible part of this |
|
111 locale as follows: |
|
112 *} |
|
113 |
|
114 simple_inductive (in rel) |
|
115 trcl' |
|
116 where |
|
117 base: "trcl' x x" |
|
118 | step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z" |
|
119 |
|
120 simple_inductive (in rel) |
|
121 accpart' |
|
122 where |
|
123 accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x" |
|
124 |
|
125 text {* |
|
126 Note that in these definitions the parameter @{text R} for the |
|
127 relation is left implicit. If we feed into the |
73 parser the string (which corresponds to our definition of @{term even} and |
128 parser the string (which corresponds to our definition of @{term even} and |
74 @{term odd}): |
129 @{term odd}): |
75 |
130 |
76 @{ML_response [display,gray] |
131 @{ML_response [display,gray] |
77 "let |
132 "let |
86 end" |
141 end" |
87 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
142 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], |
88 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
143 [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), |
89 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
144 ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"), |
90 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
145 ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"} |
91 *} |
146 |
92 |
147 then we get back the predicates (with type |
93 |
148 and syntax annotations), and the specifications of the introduction |
94 text {* |
149 rules. This is all the information we |
95 then we get back a locale (in this case @{ML NONE}), the predicates (with type |
|
96 and syntax annotations), the parameters (similar as the predicates) and |
|
97 the specifications of the introduction rules. |
|
98 |
|
99 |
|
100 |
|
101 This is all the information we |
|
102 need for calling the package and setting up the keyword. The latter is |
150 need for calling the package and setting up the keyword. The latter is |
103 done in Lines 6 and 7 in the code below. |
151 done in Lines 6 and 7 in the code below. |
104 |
152 *} |
105 @{ML_chunk [display,gray,linenos] syntax} |
153 |
106 |
154 (*<*) |
|
155 ML{* fun add_inductive pred_specs rule_specs lthy = lthy *} |
|
156 (*>*) |
|
157 |
|
158 ML{*fun add_inductive_cmd pred_specs rule_specs lthy = |
|
159 let |
|
160 val ((pred_specs', rule_specs'), _) = |
|
161 Specification.read_spec pred_specs rule_specs lthy |
|
162 in |
|
163 add_inductive pred_specs' rule_specs' lthy |
|
164 end*} |
|
165 |
|
166 |
|
167 ML{*val specification = |
|
168 spec_parser >> |
|
169 (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)*} |
|
170 |
|
171 ML{*val _ = OuterSyntax.local_theory "simple_inductive" |
|
172 "definition of simple inductive predicates" |
|
173 OuterKeyword.thy_decl specification*} |
|
174 |
|
175 |
|
176 text {* |
107 We call @{ML OuterSyntax.command} with the kind-indicator @{ML |
177 We call @{ML OuterSyntax.command} with the kind-indicator @{ML |
108 OuterKeyword.thy_decl} since the package does not need to open up any goal |
178 OuterKeyword.thy_decl} since the package does not need to open up any goal |
109 state (see Section~\ref{sec:newcommand}). Note that the predicates and |
179 state (see Section~\ref{sec:newcommand}). Note that the predicates and |
110 parameters are at the moment only some ``naked'' variables: they have no |
180 parameters are at the moment only some ``naked'' variables: they have no |
111 type yet (even if we annotate them with types) and they are also no defined |
181 type yet (even if we annotate them with types) and they are also no defined |