26 implies (infix "\<longrightarrow>" 100) and |
26 implies (infix "\<longrightarrow>" 100) and |
27 "==>" (infix "\<Longrightarrow>" 100) and |
27 "==>" (infix "\<Longrightarrow>" 100) and |
28 fun_map ("_ \<singlearr> _" 51) and |
28 fun_map ("_ \<singlearr> _" 51) and |
29 fun_rel ("_ \<doublearr> _" 51) and |
29 fun_rel ("_ \<doublearr> _" 51) and |
30 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
30 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
31 fempty ("\<emptyset>") and |
31 empty_fset ("\<emptyset>") and |
32 funion ("_ \<union> _") and |
32 union_fset ("_ \<union> _") and |
33 finsert ("{_} \<union> _") and |
33 insert_fset ("{_} \<union> _") and |
34 Cons ("_::_") and |
34 Cons ("_::_") and |
35 concat ("flat") and |
35 concat ("flat") and |
36 fconcat ("\<Union>") and |
36 concat_fset ("\<Union>") and |
37 Quotient ("Quot _ _ _") |
37 Quotient ("Quot _ _ _") |
38 |
38 |
39 |
39 |
40 |
40 |
41 ML {* |
41 ML {* |
265 where @{text "@"} is the usual list append. We expect that the corresponding |
265 where @{text "@"} is the usual list append. We expect that the corresponding |
266 operator on finite sets, written @{term "fconcat"}, |
266 operator on finite sets, written @{term "fconcat"}, |
267 builds finite unions of finite sets: |
267 builds finite unions of finite sets: |
268 |
268 |
269 \begin{isabelle}\ \ \ \ \ %%% |
269 \begin{isabelle}\ \ \ \ \ %%% |
270 @{thm fconcat_empty[THEN eq_reflection, no_vars]}\hspace{10mm} |
270 @{thm concat_empty_fset[THEN eq_reflection, no_vars]}\hspace{10mm} |
271 @{thm fconcat_insert[THEN eq_reflection, no_vars]} |
271 @{thm concat_insert_fset[THEN eq_reflection, no_vars]} |
272 \end{isabelle} |
272 \end{isabelle} |
273 |
273 |
274 \noindent |
274 \noindent |
275 The quotient package should automatically provide us with a definition for @{text "\<Union>"} in |
275 The quotient package should automatically provide us with a definition for @{text "\<Union>"} in |
276 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is |
276 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is |
375 |
375 |
376 \noindent |
376 \noindent |
377 Using extensionality and unfolding the definition of @{text "\<singlearr>"}, |
377 Using extensionality and unfolding the definition of @{text "\<singlearr>"}, |
378 we can get back to \eqref{adddef}. |
378 we can get back to \eqref{adddef}. |
379 In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function |
379 In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function |
380 of the type-constructor @{text \<kappa>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the |
380 of the type-constructor @{text \<kappa>}. |
381 type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. |
381 %% a general type for map all types is difficult to give (algebraic types are |
382 For example @{text "map_list"} |
382 %% easy, but for example the function type is not algebraic |
383 has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}. |
383 %For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the |
|
384 %type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. |
|
385 %For example @{text "map_list"} |
|
386 %has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}. |
384 In our implementation we maintain |
387 In our implementation we maintain |
385 a database of these map-functions that can be dynamically extended. |
388 a database of these map-functions that can be dynamically extended. |
386 |
389 |
387 It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"}, |
390 It will also be necessary to have operators, referred to as @{text "rel_\<kappa>"}, |
388 which define equivalence relations in terms of constituent equivalence |
391 which define equivalence relations in terms of constituent equivalence |