35 Cons ("_::_") and |
35 Cons ("_::_") and |
36 concat ("flat") and |
36 concat ("flat") and |
37 concat_fset ("\<Union>") and |
37 concat_fset ("\<Union>") and |
38 Quotient ("Quot _ _ _") |
38 Quotient ("Quot _ _ _") |
39 |
39 |
40 |
40 declare [[show_question_marks = false]] |
41 |
41 |
42 ML {* |
42 ML {* |
43 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
43 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
44 |
44 |
45 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
45 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
55 setup {* |
55 setup {* |
56 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #> |
56 Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #> |
57 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #> |
57 Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #> |
58 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) |
58 Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2)) |
59 *} |
59 *} |
60 |
|
61 lemma insert_preserve2: |
|
62 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
|
63 (id ---> rep_fset ---> abs_fset) op #" |
|
64 by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
|
65 |
|
66 lemma list_all2_symp: |
|
67 assumes a: "equivp R" |
|
68 and b: "list_all2 R xs ys" |
|
69 shows "list_all2 R ys xs" |
|
70 using list_all2_lengthD[OF b] b |
|
71 apply(induct xs ys rule: list_induct2) |
|
72 apply(auto intro: equivp_symp[OF a]) |
|
73 done |
|
74 |
|
75 lemma concat_rsp_unfolded: |
|
76 "\<lbrakk>list_all2 list_eq a ba; list_eq ba bb; list_all2 list_eq bb b\<rbrakk> \<Longrightarrow> list_eq (concat a) (concat b)" |
|
77 proof - |
|
78 fix a b ba bb |
|
79 assume a: "list_all2 list_eq a ba" |
|
80 assume b: "list_eq ba bb" |
|
81 assume c: "list_all2 list_eq bb b" |
|
82 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
83 fix x |
|
84 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
85 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
|
86 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
87 next |
|
88 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
89 have a': "list_all2 list_eq ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a]) |
|
90 have b': "list_eq bb ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
|
91 have c': "list_all2 list_eq b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c]) |
|
92 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
93 qed |
|
94 qed |
|
95 then show "list_eq (concat a) (concat b)" by auto |
|
96 qed |
|
97 |
60 |
98 (*>*) |
61 (*>*) |
99 |
62 |
100 |
63 |
101 section {* Introduction *} |
64 section {* Introduction *} |
273 in case of quotienting lists to yield finite sets and the operator that |
236 in case of quotienting lists to yield finite sets and the operator that |
274 flattens lists of lists, defined as follows |
237 flattens lists of lists, defined as follows |
275 |
238 |
276 \begin{isabelle}\ \ \ \ \ %%% |
239 \begin{isabelle}\ \ \ \ \ %%% |
277 @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm} |
240 @{thm concat.simps(1)[THEN eq_reflection]}\hspace{10mm} |
278 @{thm concat.simps(2)[THEN eq_reflection, no_vars]} |
241 @{thm concat.simps(2)[THEN eq_reflection]} |
279 \end{isabelle} |
242 \end{isabelle} |
280 |
243 |
281 \noindent |
244 \noindent |
282 where @{text "@"} is the usual |
245 where @{text "@"} is the usual |
283 list append. We expect that the corresponding |
246 list append. We expect that the corresponding |
284 operator on finite sets, written @{term "fconcat"}, |
247 operator on finite sets, written @{term "fconcat"}, |
285 builds finite unions of finite sets: |
248 builds finite unions of finite sets: |
286 |
249 |
287 \begin{isabelle}\ \ \ \ \ %%% |
250 \begin{isabelle}\ \ \ \ \ %%% |
288 @{thm concat_empty_fset[THEN eq_reflection, no_vars]}\hspace{10mm} |
251 @{thm concat_empty_fset[THEN eq_reflection]}\hspace{10mm} |
289 @{thm concat_insert_fset[THEN eq_reflection, no_vars]} |
252 @{thm concat_insert_fset[THEN eq_reflection]} |
290 \end{isabelle} |
253 \end{isabelle} |
291 |
254 |
292 \noindent |
255 \noindent |
293 The quotient package should automatically provide us with a definition for @{text "\<Union>"} in |
256 The quotient package should automatically provide us with a definition for @{text "\<Union>"} in |
294 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is |
257 terms of @{text flat}, @{text Rep_fset} and @{text Abs_fset}. The problem is |
323 according to the type of the raw constant and the type |
286 according to the type of the raw constant and the type |
324 of the quotient constant. This means we also have to extend the notions |
287 of the quotient constant. This means we also have to extend the notions |
325 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
288 of \emph{aggregate equivalence relation}, \emph{respectfulness} and \emph{preservation} |
326 from Homeier \cite{Homeier05}. |
289 from Homeier \cite{Homeier05}. |
327 |
290 |
328 {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset[no_vars]}} |
291 {\bf EXAMPLE BY HUFFMAN @{thm map_concat_fset}} |
329 |
292 |
330 In addition we are able to clearly specify what is involved |
293 In addition we are able to clearly specify what is involved |
331 in the lifting process (this was only hinted at in \cite{Homeier05} and |
294 in the lifting process (this was only hinted at in \cite{Homeier05} and |
332 implemented as a ``rough recipe'' in ML-code). A pleasing side-result |
295 implemented as a ``rough recipe'' in ML-code). A pleasing side-result |
333 is that our procedure for lifting theorems is completely deterministic |
296 is that our procedure for lifting theorems is completely deterministic |
381 constructor taking some arguments, for example @{text map_list} for lists. Homeier |
344 constructor taking some arguments, for example @{text map_list} for lists. Homeier |
382 describes in \cite{Homeier05} map-functions for products, sums, options and |
345 describes in \cite{Homeier05} map-functions for products, sums, options and |
383 also the following map for function types |
346 also the following map for function types |
384 |
347 |
385 \begin{isabelle}\ \ \ \ \ %%% |
348 \begin{isabelle}\ \ \ \ \ %%% |
386 @{thm map_fun_def[no_vars, THEN eq_reflection]} |
349 @{thm map_fun_def[THEN eq_reflection]} |
387 \end{isabelle} |
350 \end{isabelle} |
388 |
351 |
389 \noindent |
352 \noindent |
390 Using this map-function, we can give the following, equivalent, but more |
353 Using this map-function, we can give the following, equivalent, but more |
391 uniform definition for @{text add} shown in \eqref{adddef}: |
354 uniform definition for @{text add} shown in \eqref{adddef}: |
421 \noindent |
384 \noindent |
422 Homeier gives also the following operator for defining equivalence |
385 Homeier gives also the following operator for defining equivalence |
423 relations over function types |
386 relations over function types |
424 % |
387 % |
425 \begin{isabelle}\ \ \ \ \ %%% |
388 \begin{isabelle}\ \ \ \ \ %%% |
426 @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", no_vars, THEN eq_reflection]} |
389 @{thm fun_rel_def[of "R\<^isub>1" "R\<^isub>2", THEN eq_reflection]} |
427 \hfill\numbered{relfun} |
390 \hfill\numbered{relfun} |
428 \end{isabelle} |
391 \end{isabelle} |
429 |
392 |
430 \noindent |
393 \noindent |
431 In the context of quotients, the following two notions from \cite{Homeier05} |
394 In the context of quotients, the following two notions from \cite{Homeier05} |
447 Given a relation $R$, an abstraction function $Abs$ |
410 Given a relation $R$, an abstraction function $Abs$ |
448 and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"} |
411 and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"} |
449 holds if and only if |
412 holds if and only if |
450 \begin{isabelle}\ \ \ \ \ %%%% |
413 \begin{isabelle}\ \ \ \ \ %%%% |
451 \begin{tabular}{rl} |
414 \begin{tabular}{rl} |
452 (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R", no_vars]}\end{isa}\\ |
415 (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R"]}\end{isa}\\ |
453 (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R", no_vars]}\end{isa}\\ |
416 (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R"]}\end{isa}\\ |
454 (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R", no_vars]}\end{isa}\\ |
417 (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R"]}\end{isa}\\ |
455 \end{tabular} |
418 \end{tabular} |
456 \end{isabelle} |
419 \end{isabelle} |
457 \end{definition} |
420 \end{definition} |
458 |
421 |
459 \noindent |
422 \noindent |
916 under the assumption @{term "Quotient R Abs Rep"}. The point is that if we have |
879 under the assumption @{term "Quotient R Abs Rep"}. The point is that if we have |
917 an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated |
880 an instance of @{text cons} where the type variable @{text \<alpha>} is instantiated |
918 with @{text "nat \<times> nat"} and we also quotient this type to yield integers, |
881 with @{text "nat \<times> nat"} and we also quotient this type to yield integers, |
919 then we need to show this preservation property. |
882 then we need to show this preservation property. |
920 |
883 |
921 %%%@ {thm [display, indent=10] insert_preserve2[no_vars]} |
884 %%%@ {thm [display, indent=10] Cons_prs2} |
922 |
885 |
923 %Given two quotients, one of which quotients a container, and the |
886 %Given two quotients, one of which quotients a container, and the |
924 %other quotients the type in the container, we can write the |
887 %other quotients the type in the container, we can write the |
925 %composition of those quotients. To compose two quotient theorems |
888 %composition of those quotients. To compose two quotient theorems |
926 %we compose the relations with relation composition as defined above |
889 %we compose the relations with relation composition as defined above |
1130 |
1093 |
1131 %%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we |
1094 %%% FIXME Reviewer 1 claims the theorem is obviously false so maybe we |
1132 %%% should include a proof sketch? |
1095 %%% should include a proof sketch? |
1133 |
1096 |
1134 %\begin{isabelle}\ \ \ \ \ %%% |
1097 %\begin{isabelle}\ \ \ \ \ %%% |
1135 %@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2, no_vars]} |
1098 %@{thm (concl) ball_reg_eqv_range[of R\<^isub>1 R\<^isub>2]} |
1136 %\end{isabelle} |
1099 %\end{isabelle} |
1137 |
1100 |
1138 %\noindent |
1101 %\noindent |
1139 %The last theorem is new in comparison with Homeier's package. There the |
1102 %The last theorem is new in comparison with Homeier's package. There the |
1140 %injection procedure would be used to prove such goals and |
1103 %injection procedure would be used to prove such goals and |
1181 %over variables that include quotient types. We show here only |
1144 %over variables that include quotient types. We show here only |
1182 %the lambda preservation theorem. Given |
1145 %the lambda preservation theorem. Given |
1183 %@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have: |
1146 %@{term "Quotient R\<^isub>1 Abs\<^isub>1 Rep\<^isub>1"} and @{term "Quotient R\<^isub>2 Abs\<^isub>2 Rep\<^isub>2"}, we have: |
1184 |
1147 |
1185 %\begin{isabelle}\ \ \ \ \ %%% |
1148 %\begin{isabelle}\ \ \ \ \ %%% |
1186 %@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2", no_vars]} |
1149 %@{thm (concl) lambda_prs[of _ "Abs\<^isub>1" "Rep\<^isub>1" _ "Abs\<^isub>2" "Rep\<^isub>2"]} |
1187 %\end{isabelle} |
1150 %\end{isabelle} |
1188 |
1151 |
1189 %\noindent |
1152 %\noindent |
1190 %Next, relations over lifted types can be rewritten to equalities |
1153 %Next, relations over lifted types can be rewritten to equalities |
1191 %over lifted type. Rewriting is performed with the following theorem, |
1154 %over lifted type. Rewriting is performed with the following theorem, |
1192 %which has been shown by Homeier~\cite{Homeier05}: |
1155 %which has been shown by Homeier~\cite{Homeier05}: |
1193 |
1156 |
1194 %\begin{isabelle}\ \ \ \ \ %%% |
1157 %\begin{isabelle}\ \ \ \ \ %%% |
1195 %@{thm (concl) Quotient_rel_rep[no_vars]} |
1158 %@{thm (concl) Quotient_rel_rep} |
1196 %\end{isabelle} |
1159 %\end{isabelle} |
1197 |
1160 |
1198 |
1161 |
1199 %Finally, we rewrite with the preservation theorems. This will result |
1162 %Finally, we rewrite with the preservation theorems. This will result |
1200 %in two equal terms that can be solved by reflexivity. |
1163 %in two equal terms that can be solved by reflexivity. |