76 In the context of HOL, there have been several quotient packages (...). The |
76 In the context of HOL, there have been several quotient packages (...). The |
77 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
77 most notable is the one by Homeier (...) implemented in HOL4. However, what is |
78 surprising, none of them can deal compositions of quotients, for example with |
78 surprising, none of them can deal compositions of quotients, for example with |
79 lifting theorems about @{text "concat"}: |
79 lifting theorems about @{text "concat"}: |
80 |
80 |
81 @{thm concat.simps(1)}\\ |
81 @{thm [display] concat.simps(1)} |
82 @{thm concat.simps(2)[no_vars]} |
82 @{thm [display] concat.simps(2)[no_vars]} |
83 |
83 |
84 \noindent |
84 \noindent |
85 One would like to lift this definition to the operation: |
85 One would like to lift this definition to the operation: |
86 |
86 |
87 @{thm fconcat_empty[no_vars]}\\ |
87 @{thm [display] fconcat_empty[no_vars]} |
88 @{thm fconcat_insert[no_vars]} |
88 @{thm [display] fconcat_insert[no_vars]} |
89 |
89 |
90 \noindent |
90 \noindent |
91 What is special about this operation is that we have as input |
91 What is special about this operation is that we have as input |
92 lists of lists which after lifting turn into finite sets of finite |
92 lists of lists which after lifting turn into finite sets of finite |
93 sets. |
93 sets. |
94 *} |
94 *} |
95 |
95 |
96 subsection {* Contributions *} |
96 subsection {* Contributions *} |
97 |
97 |
98 text {* |
98 text {* |
143 \end{enumerate} |
143 \end{enumerate} |
144 |
144 |
145 \end{definition} |
145 \end{definition} |
146 |
146 |
147 \begin{definition}[Relation map and function map]\\ |
147 \begin{definition}[Relation map and function map]\\ |
148 @{thm fun_rel_def[no_vars]}\\ |
148 @{thm fun_rel_def[of "R1" "R2", no_vars]}\\ |
149 @{thm fun_map_def[no_vars]} |
149 @{thm fun_map_def[no_vars]} |
150 \end{definition} |
150 \end{definition} |
151 |
151 |
152 The main theorems for building higher order quotients is: |
152 The main theorems for building higher order quotients is: |
153 \begin{lemma}[Function Quotient] |
153 \begin{lemma}[Function Quotient] |
217 classes of the arguments applied to the constant. This can be |
217 classes of the arguments applied to the constant. This can be |
218 expressed in terms of an aggregate relation between the constant |
218 expressed in terms of an aggregate relation between the constant |
219 and itself, for example the respectfullness for @{term "append"} |
219 and itself, for example the respectfullness for @{term "append"} |
220 can be stated as: |
220 can be stated as: |
221 |
221 |
222 @{thm append_rsp[no_vars]} |
222 @{thm [display] append_rsp[no_vars]} |
223 |
223 |
|
224 \noindent |
224 Which is equivalent to: |
225 Which is equivalent to: |
225 |
226 |
226 @{thm append_rsp[no_vars,simplified fun_rel_def]} |
227 @{thm [display] append_rsp_unfolded[no_vars]} |
227 |
228 |
228 Below we show the algorithm for finding the aggregate relation. |
229 Below we show the algorithm for finding the aggregate relation. |
229 This algorithm uses |
230 This algorithm uses |
230 the relation composition which we define as: |
231 the relation composition which we define as: |
231 |
232 |
232 \begin{definition}[Composition of Relations] |
233 \begin{definition}[Composition of Relations] |
233 @{abbrev "rel_conj R1 R2"} |
234 @{abbrev "rel_conj R1 R2"} where @{text OO} is the predicate |
|
235 composition @{thm pred_compI[no_vars]} |
234 \end{definition} |
236 \end{definition} |
235 |
237 |
236 Given an aggregate raw type and quotient type: |
238 Given an aggregate raw type and quotient type: |
237 |
239 |
238 \begin{itemize} |
240 \begin{itemize} |
248 the aggregate relation function. |
250 the aggregate relation function. |
249 |
251 |
250 \end{itemize} |
252 \end{itemize} |
251 |
253 |
252 Again, the the behaviour of our algorithm in the last situation is |
254 Again, the the behaviour of our algorithm in the last situation is |
253 novel, so lets look at the example of respectfullness for @{term concat}: |
255 novel, so lets look at the example of respectfullness for @{term concat}. |
254 |
256 The statement as computed by the algorithm above is: |
255 @{thm concat_rsp} |
257 |
256 |
258 @{thm [display] concat_rsp[no_vars]} |
257 This means... |
259 |
|
260 \noindent |
|
261 By unfolding the definition of relation composition and relation map |
|
262 we can see the equivalent statement just using the primitive list |
|
263 equivalence relation: |
|
264 |
|
265 @{thm [display] concat_rsp_unfolded[of "a" "a'" "b'" "b", no_vars]} |
|
266 |
|
267 The statement reads that, for any lists of lists @{term a} and @{term b} |
|
268 if there exist intermediate lists of lists @{term "a'"} and @{term "b'"} |
|
269 such that each element of @{term a} is in the relation with an appropriate |
|
270 element of @{term a'}, @{term a'} is in relation with @{term b'} and each |
|
271 element of @{term b'} is in relation with the appropriate element of |
|
272 @{term b}. |
258 |
273 |
259 *} |
274 *} |
260 |
275 |
261 subsection {* Preservation *} |
276 subsection {* Preservation *} |
|
277 |
|
278 text {* |
|
279 To be able to lift theorems that talk about constants that are not |
|
280 lifted but whose type changes when lifting is performed additionally |
|
281 preservation theorems are needed. |
|
282 *} |
262 |
283 |
263 section {* Lifting Theorems *} |
284 section {* Lifting Theorems *} |
264 |
285 |
265 text{* |
286 text{* |
266 Aggregate @{term "Rep"} and @{term "Abs"} functions are also |
287 Aggregate @{term "Rep"} and @{term "Abs"} functions are also |
267 present in composition quotients. An example composition quotient |
288 present in composition quotients. An example composition quotient |
268 theorem that needs to be proved is the one needed to lift theorems |
289 theorem that needs to be proved is the one needed to lift theorems |
269 about concat: |
290 about concat: |
270 |
291 |
271 @{thm quotient_compose_list[no_vars]} |
292 @{thm [display] quotient_compose_list[no_vars]} |
272 *} |
293 *} |
273 |
294 |
274 text {* TBD *} |
295 text {* TBD *} |
275 |
296 |
276 text {* Why providing a statement to prove is necessary is some cases *} |
297 text {* Why providing a statement to prove is necessary is some cases *} |