59 |
59 |
60 lemma insert_preserve2: |
60 lemma insert_preserve2: |
61 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
61 shows "((rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op #) = |
62 (id ---> rep_fset ---> abs_fset) op #" |
62 (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]) |
63 by (simp add: fun_eq_iff abs_o_rep[OF Quotient_fset] map_id Quotient_abs_rep[OF Quotient_fset]) |
|
64 |
|
65 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)" |
|
67 proof - |
|
68 fix a b ba bb |
|
69 assume a: "list_all2 list_eq a ba" |
|
70 assume b: "list_eq ba bb" |
|
71 assume c: "list_all2 list_eq bb b" |
|
72 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
73 fix x |
|
74 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
|
75 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
|
76 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
|
77 next |
|
78 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
|
79 have a': "list_all2 list_eq ba a" by (rule list_all2_symp[OF list_eq_equivp, OF a]) |
|
80 have b': "list_eq bb ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
|
81 have c': "list_all2 list_eq b bb" by (rule list_all2_symp[OF list_eq_equivp, OF c]) |
|
82 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
|
83 qed |
|
84 qed |
|
85 then show "list_eq (concat a) (concat b)" by auto |
|
86 qed |
64 |
87 |
65 (*>*) |
88 (*>*) |
66 |
89 |
67 |
90 |
68 section {* Introduction *} |
91 section {* Introduction *} |