equal
deleted
inserted
replaced
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "Quotient" "Quotient_Syntax" |
3 imports "Quotient" |
|
4 "~~/src/HOL/Library/Quotient_Syntax" |
4 "~~/src/HOL/Library/LaTeXsugar" |
5 "~~/src/HOL/Library/LaTeXsugar" |
5 "~~/src/HOL/Quotient_Examples/FSet" |
6 "~~/src/HOL/Quotient_Examples/FSet" |
6 begin |
7 begin |
7 |
8 |
8 (**** |
9 (**** |
23 notation (latex output) |
24 notation (latex output) |
24 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
25 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
25 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
26 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
26 implies (infix "\<longrightarrow>" 100) and |
27 implies (infix "\<longrightarrow>" 100) and |
27 "==>" (infix "\<Longrightarrow>" 100) and |
28 "==>" (infix "\<Longrightarrow>" 100) and |
28 fun_map ("_ \<singlearr> _" 51) and |
29 map_fun ("_ \<singlearr> _" 51) and |
29 fun_rel ("_ \<doublearr> _" 51) and |
30 fun_rel ("_ \<doublearr> _" 51) and |
30 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
31 list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *) |
31 empty_fset ("\<emptyset>") and |
32 empty_fset ("\<emptyset>") and |
32 union_fset ("_ \<union> _") and |
33 union_fset ("_ \<union> _") and |
33 insert_fset ("{_} \<union> _") and |
34 insert_fset ("{_} \<union> _") and |
59 |
60 |
60 lemma insert_preserve2: |
61 lemma insert_preserve2: |
61 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
62 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
62 (id ---> rep_fset ---> abs_fset) op #" |
63 (id ---> rep_fset ---> abs_fset) op #" |
63 by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
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 |
64 |
74 |
65 lemma concat_rsp_unfolded: |
75 lemma concat_rsp_unfolded: |
66 "\<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)" |
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)" |
67 proof - |
77 proof - |
68 fix a b ba bb |
78 fix a b ba bb |
362 constructor taking some arguments, for example @{text map_list} for lists. Homeier |
372 constructor taking some arguments, for example @{text map_list} for lists. Homeier |
363 describes in \cite{Homeier05} map-functions for products, sums, options and |
373 describes in \cite{Homeier05} map-functions for products, sums, options and |
364 also the following map for function types |
374 also the following map for function types |
365 |
375 |
366 \begin{isabelle}\ \ \ \ \ %%% |
376 \begin{isabelle}\ \ \ \ \ %%% |
367 @{thm fun_map_def[no_vars, THEN eq_reflection]} |
377 @{thm map_fun_def[no_vars, THEN eq_reflection]} |
368 \end{isabelle} |
378 \end{isabelle} |
369 |
379 |
370 \noindent |
380 \noindent |
371 Using this map-function, we can give the following, equivalent, but more |
381 Using this map-function, we can give the following, equivalent, but more |
372 uniform definition for @{text add} shown in \eqref{adddef}: |
382 uniform definition for @{text add} shown in \eqref{adddef}: |