32
|
1 |
theory Ind_Interface
|
346
|
2 |
imports Ind_Intro Simple_Inductive_Package
|
514
|
3 |
keywords "simple_inductive2" :: thy_decl
|
32
|
4 |
begin
|
|
5 |
|
565
|
6 |
section \<open>Parsing and Typing the Specification\label{sec:interface}\<close>
|
124
|
7 |
|
565
|
8 |
text_raw \<open>
|
296
|
9 |
\begin{figure}[t]
|
219
|
10 |
\begin{boxedminipage}{\textwidth}
|
|
11 |
\begin{isabelle}
|
565
|
12 |
\<close>
|
219
|
13 |
simple_inductive
|
|
14 |
trcl :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
15 |
where
|
|
16 |
base: "trcl R x x"
|
|
17 |
| step: "trcl R x y \<Longrightarrow> R y z \<Longrightarrow> trcl R x z"
|
|
18 |
|
|
19 |
simple_inductive
|
|
20 |
even and odd
|
|
21 |
where
|
|
22 |
even0: "even 0"
|
|
23 |
| evenS: "odd n \<Longrightarrow> even (Suc n)"
|
|
24 |
| oddS: "even n \<Longrightarrow> odd (Suc n)"
|
|
25 |
|
|
26 |
simple_inductive
|
|
27 |
accpart :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
|
|
28 |
where
|
|
29 |
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart R y) \<Longrightarrow> accpart R x"
|
|
30 |
|
|
31 |
(*<*)
|
|
32 |
datatype trm =
|
|
33 |
Var "string"
|
|
34 |
| App "trm" "trm"
|
|
35 |
| Lam "string" "trm"
|
|
36 |
(*>*)
|
|
37 |
|
|
38 |
simple_inductive
|
|
39 |
fresh :: "string \<Rightarrow> trm \<Rightarrow> bool"
|
|
40 |
where
|
|
41 |
fresh_var: "a\<noteq>b \<Longrightarrow> fresh a (Var b)"
|
|
42 |
| fresh_app: "\<lbrakk>fresh a t; fresh a s\<rbrakk> \<Longrightarrow> fresh a (App t s)"
|
|
43 |
| fresh_lam1: "fresh a (Lam a t)"
|
|
44 |
| fresh_lam2: "\<lbrakk>a\<noteq>b; fresh a t\<rbrakk> \<Longrightarrow> fresh a (Lam b t)"
|
565
|
45 |
text_raw \<open>
|
219
|
46 |
\end{isabelle}
|
|
47 |
\end{boxedminipage}
|
|
48 |
\caption{Specification given by the user for the inductive predicates
|
|
49 |
@{term "trcl"}, @{term "even"} and @{term "odd"}, @{term "accpart"} and
|
244
|
50 |
@{term "fresh"}.\label{fig:specs}}
|
219
|
51 |
\end{figure}
|
565
|
52 |
\<close>
|
219
|
53 |
|
565
|
54 |
text \<open>
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
55 |
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
|
56 |
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
|
57 |
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
|
58 |
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
|
59 |
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
|
60 |
less translates directly into the parser:
|
219
|
61 |
|
565
|
62 |
\<close>
|
219
|
63 |
|
565
|
64 |
ML %grayML\<open>val spec_parser =
|
562
|
65 |
Parse.vars --
|
219
|
66 |
Scan.optional
|
426
|
67 |
(Parse.$$$ "where" |--
|
|
68 |
Parse.!!!
|
|
69 |
(Parse.enum1 "|"
|
565
|
70 |
(Parse_Spec.opt_thm_name ":" -- Parse.prop))) []\<close>
|
219
|
71 |
|
565
|
72 |
text \<open>
|
295
24c68350d059
polished the package chapter used FOCUS to explain the subproofs
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
73 |
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
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
The target stands for a locale and allows us to specify
|
565
|
78 |
\<close>
|
127
|
79 |
|
|
80 |
locale rel =
|
|
81 |
fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
|
|
82 |
|
565
|
83 |
text \<open>
|
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
|
84 |
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
|
85 |
locale as follows:
|
565
|
86 |
\<close>
|
116
|
87 |
|
129
|
88 |
simple_inductive (in rel)
|
|
89 |
trcl'
|
116
|
90 |
where
|
127
|
91 |
base: "trcl' x x"
|
|
92 |
| step: "trcl' x y \<Longrightarrow> R y z \<Longrightarrow> trcl' x z"
|
116
|
93 |
|
129
|
94 |
simple_inductive (in rel)
|
|
95 |
accpart'
|
116
|
96 |
where
|
127
|
97 |
accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
|
565
|
98 |
(*<*)ML %no\<open>fun filtered_input str =
|
562
|
99 |
filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
|
565
|
100 |
fun parse p input = Scan.finite Token.stopper (Scan.error p) input\<close>(*>*)
|
|
101 |
text \<open>
|
|
102 |
Note that in these definitions the parameter \<open>R\<close>, standing for the
|
224
|
103 |
relation, is left implicit. For the moment we will ignore this kind
|
|
104 |
of implicit parameters and rely on the fact that the infrastructure will
|
|
105 |
deal with them. Later, however, we will come back to them.
|
|
106 |
|
|
107 |
If we feed into the parser the string that corresponds to our definition
|
|
108 |
of @{term even} and @{term odd}
|
120
|
109 |
|
567
|
110 |
@{ML_matchresult [display,gray]
|
569
|
111 |
\<open>let
|
120
|
112 |
val input = filtered_input
|
569
|
113 |
("even and odd " ^
|
|
114 |
"where " ^
|
|
115 |
" even0[intro]: \"even 0\" " ^
|
|
116 |
"| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^
|
|
117 |
"| oddS[intro]: \"even n \<Longrightarrow> odd (Suc n)\" ")
|
120
|
118 |
in
|
|
119 |
parse spec_parser input
|
569
|
120 |
end\<close>
|
|
121 |
\<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
|
566
6103b0eadbf2
tuned parser for patterns in ML_response... antiquotations
Norbert Schirmer <norbert.schirmer@web.de>
diff
changeset
|
122 |
[((even0,_), _),
|
6103b0eadbf2
tuned parser for patterns in ML_response... antiquotations
Norbert Schirmer <norbert.schirmer@web.de>
diff
changeset
|
123 |
((evenS,_), _),
|
569
|
124 |
((oddS,_), _)]), [])\<close>}
|
219
|
125 |
|
224
|
126 |
then we get back the specifications of the predicates (with type and syntax annotations),
|
|
127 |
and specifications of the introduction rules. This is all the information we
|
219
|
128 |
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
|
129 |
done in Lines 5 to 7 in the code below.
|
565
|
130 |
\<close>
|
|
131 |
(*<*)ML %no\<open>fun add_inductive_cmd pred_specs rule_specs lthy = lthy
|
|
132 |
fun add_inductive pred_specs rule_specs lthy = lthy\<close>(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*)
|
|
133 |
ML %linenosgray\<open>val specification : (local_theory -> local_theory) parser =
|
224
|
134 |
spec_parser >>
|
|
135 |
(fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
|
|
136 |
|
562
|
137 |
val _ = Outer_Syntax.local_theory @{command_keyword "simple_inductive2"}
|
224
|
138 |
"definition of simple inductive predicates"
|
565
|
139 |
specification\<close>
|
224
|
140 |
|
565
|
141 |
text \<open>
|
426
|
142 |
We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator
|
|
143 |
@{ML_ind thy_decl in Keyword} since the package does not need to open
|
224
|
144 |
up any proof (see Section~\ref{sec:newcommand}).
|
565
|
145 |
The auxiliary function \<open>specification\<close> in Lines 1 to 3
|
224
|
146 |
gathers the information from the parser to be processed further
|
565
|
147 |
by the function \<open>add_inductive_cmd\<close>, which we describe below.
|
224
|
148 |
|
|
149 |
Note that the predicates when they come out of the parser are just some
|
|
150 |
``naked'' strings: they have no type yet (even if we annotate them with
|
|
151 |
types) and they are also not defined constants yet (which the predicates
|
|
152 |
eventually will be). Also the introduction rules are just strings. What we have
|
|
153 |
to do first is to transform the parser's output into some internal
|
|
154 |
datastructures that can be processed further. For this we can use the
|
562
|
155 |
function @{ML_ind read_multi_specs in Specification}. This function takes some strings
|
224
|
156 |
(with possible typing annotations) and some rule specifications, and attempts
|
|
157 |
to find a typing according to the given type constraints given by the
|
|
158 |
user and the type constraints by the ``ambient'' theory. It returns
|
|
159 |
the type for the predicates and also returns typed terms for the
|
|
160 |
introduction rules. So at the heart of the function
|
565
|
161 |
\<open>add_inductive_cmd\<close> is a call to @{ML read_multi_specs in Specification}.
|
|
162 |
\<close>
|
219
|
163 |
|
565
|
164 |
ML_val%grayML\<open>fun add_inductive_cmd pred_specs rule_specs lthy =
|
219
|
165 |
let
|
|
166 |
val ((pred_specs', rule_specs'), _) =
|
562
|
167 |
Specification.read_multi_specs pred_specs rule_specs lthy
|
219
|
168 |
in
|
|
169 |
add_inductive pred_specs' rule_specs' lthy
|
565
|
170 |
end\<close>
|
53
0c3580c831a4
removed the @{ML ...} antiquotation in favour of @{ML_open ...x}
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
171 |
|
565
|
172 |
text \<open>
|
224
|
173 |
Once we have the input data as some internal datastructure, we call
|
565
|
174 |
the function \<open>add_inductive\<close>. This function does the heavy duty
|
224
|
175 |
lifting in the package: it generates definitions for the
|
|
176 |
predicates and derives from them corresponding induction principles and
|
|
177 |
introduction rules. The description of this function will span over
|
|
178 |
the next two sections.
|
565
|
179 |
\<close>
|
517
d8c376662bb4
removed special ML-setup and replaced it by explicit markups (i.e., %grayML)
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
180 |
(*<*)end(*>*)
|