32
|
1 |
theory Ind_Interface
|
346
|
2 |
imports Ind_Intro Simple_Inductive_Package
|
32
|
3 |
begin
|
|
4 |
|
215
|
5 |
section {* Parsing and Typing the Specification\label{sec:interface} *}
|
124
|
6 |
|
219
|
7 |
text_raw {*
|
296
|
8 |
\begin{figure}[t]
|
219
|
9 |
\begin{boxedminipage}{\textwidth}
|
|
10 |
\begin{isabelle}
|
|
11 |
*}
|
|
12 |
simple_inductive
|
|
13 |
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
14 |
where
|
|
15 |
base: "trcl R x x"
|
|
16 |
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
|
|
17 |
|
|
18 |
simple_inductive
|
|
19 |
even and odd
|
|
20 |
where
|
|
21 |
even0: "even 0"
|
|
22 |
| evenS: "odd n \<Longrightarrow> even (Suc n)"
|
|
23 |
| oddS: "even n \<Longrightarrow> odd (Suc n)"
|
|
24 |
|
|
25 |
simple_inductive
|
|
26 |
accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
|
|
27 |
where
|
|
28 |
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
|
|
29 |
|
|
30 |
(*<*)
|
|
31 |
datatype trm =
|
|
32 |
Var "string"
|
|
33 |
| App "trm" "trm"
|
|
34 |
| Lam "string" "trm"
|
|
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
|
244
|
49 |
@{term "fresh"}.\label{fig:specs}}
|
219
|
50 |
\end{figure}
|
|
51 |
*}
|
|
52 |
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
53 |
text {*
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
54 |
To be able to write down the specifications of inductive predicates, we have
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
to introduce a new command (see Section~\ref{sec:newcommand}). As the
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
56 |
keyword for the new command we chose \simpleinductive{}. Examples of
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
57 |
specifications from the previous section are shown in
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
58 |
Figure~\ref{fig:specs}. The syntax used in these examples more or
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
59 |
less translates directly into the parser:
|
219
|
60 |
|
|
61 |
*}
|
|
62 |
|
|
63 |
ML{*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 {*
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
72 |
which we explained in Section~\ref{sec:parsingspecs}. There is no code included
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
for parsing the keyword and what is called a \emph{target}. The latter can be given
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
74 |
optionally after the keyword. The target is an ``advanced'' feature which we will
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
75 |
inherit for ``free'' from the infrastructure on which we shall build the package.
|
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
76 |
The target stands for a locale and allows us to specify
|
127
|
77 |
*}
|
|
78 |
|
|
79 |
locale rel =
|
|
80 |
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
81 |
|
|
82 |
text {*
|
218
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
83 |
and then define the transitive closure and the accessible part of this
|
7ff7325e3b4e
started to adapt the rest of chapter 5 to the simplified version without parameters (they will be described in the extension section)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
84 |
locale as follows:
|
116
|
85 |
*}
|
|
86 |
|
129
|
87 |
simple_inductive (in rel)
|
|
88 |
trcl'
|
116
|
89 |
where
|
127
|
90 |
base: "trcl' x x"
|
|
91 |
| step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"
|
116
|
92 |
|
129
|
93 |
simple_inductive (in rel)
|
|
94 |
accpart'
|
116
|
95 |
where
|
127
|
96 |
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
|
244
|
97 |
(*<*)ML %no{*fun filtered_input str =
|
|
98 |
filter OuterLex.is_proper (OuterSyntax.scan Position.none str)
|
|
99 |
fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*)
|
116
|
100 |
text {*
|
224
|
101 |
Note that in these definitions the parameter @{text R}, standing for the
|
|
102 |
relation, is left implicit. For the moment we will ignore this kind
|
|
103 |
of implicit parameters and rely on the fact that the infrastructure will
|
|
104 |
deal with them. Later, however, we will come back to them.
|
|
105 |
|
|
106 |
If we feed into the parser the string that corresponds to our definition
|
|
107 |
of @{term even} and @{term odd}
|
120
|
108 |
|
|
109 |
@{ML_response [display,gray]
|
|
110 |
"let
|
|
111 |
val input = filtered_input
|
|
112 |
(\"even and odd \" ^
|
|
113 |
\"where \" ^
|
|
114 |
\" even0[intro]: \\\"even 0\\\" \" ^
|
|
115 |
\"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
116 |
\"| oddS[intro]: \\\"even n \<Longrightarrow> odd (Suc n)\\\" \")
|
120
|
117 |
in
|
|
118 |
parse spec_parser input
|
|
119 |
end"
|
186
371e4375c994
made the Ackermann function example safer and included suggestions from MW
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
120 |
"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
|
120
|
121 |
[((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
|
|
122 |
((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
|
|
123 |
((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
|
219
|
124 |
|
224
|
125 |
then we get back the specifications of the predicates (with type and syntax annotations),
|
|
126 |
and specifications of the introduction rules. This is all the information we
|
219
|
127 |
need for calling the package and setting up the keyword. The latter is
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
128 |
done in Lines 5 to 7 in the code below.
|
120
|
129 |
*}
|
245
53112deda119
Jasmin and Christian added examples for the pretty-printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
130 |
(*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy
|
53112deda119
Jasmin and Christian added examples for the pretty-printing section
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
131 |
fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)
|
224
|
132 |
ML_val %linenosgray{*val specification =
|
|
133 |
spec_parser >>
|
|
134 |
(fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
|
|
135 |
|
244
|
136 |
val _ = OuterSyntax.local_theory "simple_inductive2"
|
224
|
137 |
"definition of simple inductive predicates"
|
|
138 |
OuterKeyword.thy_decl specification*}
|
|
139 |
|
|
140 |
text {*
|
316
|
141 |
We call @{ML_ind local_theory in OuterSyntax} with the kind-indicator
|
|
142 |
@{ML_ind thy_decl in OuterKeyword} since the package does not need to open
|
224
|
143 |
up any proof (see Section~\ref{sec:newcommand}).
|
|
144 |
The auxiliary function @{text specification} in Lines 1 to 3
|
|
145 |
gathers the information from the parser to be processed further
|
|
146 |
by the function @{text "add_inductive_cmd"}, which we describe below.
|
|
147 |
|
|
148 |
Note that the predicates when they come out of the parser are just some
|
|
149 |
``naked'' strings: they have no type yet (even if we annotate them with
|
|
150 |
types) and they are also not defined constants yet (which the predicates
|
|
151 |
eventually will be). Also the introduction rules are just strings. What we have
|
|
152 |
to do first is to transform the parser's output into some internal
|
|
153 |
datastructures that can be processed further. For this we can use the
|
316
|
154 |
function @{ML_ind read_spec in Specification}. This function takes some strings
|
224
|
155 |
(with possible typing annotations) and some rule specifications, and attempts
|
|
156 |
to find a typing according to the given type constraints given by the
|
|
157 |
user and the type constraints by the ``ambient'' theory. It returns
|
|
158 |
the type for the predicates and also returns typed terms for the
|
|
159 |
introduction rules. So at the heart of the function
|
|
160 |
@{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.
|
|
161 |
*}
|
219
|
162 |
|
244
|
163 |
ML_val{*fun add_inductive_cmd pred_specs rule_specs lthy =
|
219
|
164 |
let
|
|
165 |
val ((pred_specs', rule_specs'), _) =
|
|
166 |
Specification.read_spec pred_specs rule_specs lthy
|
|
167 |
in
|
|
168 |
add_inductive pred_specs' rule_specs' lthy
|
224
|
169 |
end*}
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
170 |
|
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
text {*
|
224
|
172 |
Once we have the input data as some internal datastructure, we call
|
244
|
173 |
the function @{text add_inductive}. This function does the heavy duty
|
224
|
174 |
lifting in the package: it generates definitions for the
|
|
175 |
predicates and derives from them corresponding induction principles and
|
|
176 |
introduction rules. The description of this function will span over
|
|
177 |
the next two sections.
|
127
|
178 |
*}
|
219
|
179 |
(*<*)end(*>*) |