23 show ?case using Cons by auto |
25 show ?case using Cons by auto |
24 qed |
26 qed |
25 qed |
27 qed |
26 |
28 |
27 lemma concat_rsp_pre: |
29 lemma concat_rsp_pre: |
28 "\<lbrakk>list_rel op \<approx> x x'; x' \<approx> y'; list_rel op \<approx> y' y; \<exists>x\<in>set x. xa \<in> set x\<rbrakk> \<Longrightarrow> |
30 assumes a: "list_rel op \<approx> x x'" |
29 \<exists>x\<in>set y. xa \<in> set x" |
31 and b: "x' \<approx> y'" |
30 apply clarify |
32 and c: "list_rel op \<approx> y' y" |
31 apply (frule list_rel_find_element[of _ "x"]) |
33 and d: "\<exists>x\<in>set x. xa \<in> set x" |
32 apply assumption |
34 shows "\<exists>x\<in>set y. xa \<in> set x" |
33 apply clarify |
35 proof - |
34 apply (subgoal_tac "ya \<in> set y'") |
36 obtain xb where e: "xb \<in> set x" and f: "xa \<in> set xb" using d by auto |
35 prefer 2 |
37 have "\<exists>y. y \<in> set x' \<and> xb \<approx> y" by (rule list_rel_find_element[OF e a]) |
36 apply simp |
38 then obtain ya where h: "ya \<in> set x'" and i: "xb \<approx> ya" by auto |
37 apply (frule list_rel_find_element[of _ "y'"]) |
39 have j: "ya \<in> set y'" using b h by simp |
38 apply assumption |
40 have "\<exists>yb. yb \<in> set y \<and> ya \<approx> yb" by (rule list_rel_find_element[OF j c]) |
39 apply auto |
41 then show ?thesis using f i by auto |
40 done |
42 qed |
|
43 |
|
44 lemma fun_relI [intro]: |
|
45 assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)" |
|
46 shows "(P ===> Q) x y" |
|
47 using assms by (simp add: fun_rel_def) |
41 |
48 |
42 lemma [quot_respect]: |
49 lemma [quot_respect]: |
43 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
50 shows "(list_rel op \<approx> OOO op \<approx> ===> op \<approx>) concat concat" |
44 apply (simp only: fun_rel_def) |
51 proof (rule fun_relI, (erule pred_compE, erule pred_compE)) |
45 apply clarify |
52 fix a b ba bb |
46 apply (simp (no_asm)) |
53 assume a: "list_rel op \<approx> a ba" |
47 apply rule |
54 assume b: "ba \<approx> bb" |
48 apply rule |
55 assume c: "list_rel op \<approx> bb b" |
49 apply (erule concat_rsp_pre) |
56 have "\<forall>x. (\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
50 apply assumption+ |
57 fix x |
51 apply (rule concat_rsp_pre) |
58 show "(\<exists>xa\<in>set a. x \<in> set xa) = (\<exists>xa\<in>set b. x \<in> set xa)" proof |
52 prefer 4 |
59 assume d: "\<exists>xa\<in>set a. x \<in> set xa" |
53 apply assumption |
60 show "\<exists>xa\<in>set b. x \<in> set xa" by (rule concat_rsp_pre[OF a b c d]) |
54 apply (rule list_rel_symp[OF list_eq_equivp]) |
61 next |
55 apply assumption |
62 assume e: "\<exists>xa\<in>set b. x \<in> set xa" |
56 apply (rule equivp_symp[OF list_eq_equivp]) |
63 have a': "list_rel op \<approx> ba a" by (rule list_rel_symp[OF list_eq_equivp, OF a]) |
57 apply assumption |
64 have b': "bb \<approx> ba" by (rule equivp_symp[OF list_eq_equivp, OF b]) |
58 apply (rule list_rel_symp[OF list_eq_equivp]) |
65 have c': "list_rel op \<approx> b bb" by (rule list_rel_symp[OF list_eq_equivp, OF c]) |
59 apply assumption |
66 show "\<exists>xa\<in>set a. x \<in> set xa" by (rule concat_rsp_pre[OF c' b' a' e]) |
60 done |
67 qed |
|
68 qed |
|
69 then show "concat a \<approx> concat b" by simp |
|
70 qed |
61 |
71 |
62 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
72 lemma nil_rsp2[quot_respect]: "(list_rel op \<approx> OOO op \<approx>) [] []" |
63 by (metis nil_rsp list_rel.simps(1) pred_compI) |
73 by (metis nil_rsp list_rel.simps(1) pred_compI) |
64 |
74 |
65 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
75 lemma set_in_eq: "(\<forall>e. ((e \<in> A) \<longleftrightarrow> (e \<in> B))) \<equiv> A = B" |
80 apply (metis equivp_def fset_equivp) |
90 apply (metis equivp_def fset_equivp) |
81 apply rule |
91 apply rule |
82 apply (rule equivp_reflp[OF fset_equivp]) |
92 apply (rule equivp_reflp[OF fset_equivp]) |
83 apply (rule list_rel_refl) |
93 apply (rule list_rel_refl) |
84 apply (metis equivp_def fset_equivp) |
94 apply (metis equivp_def fset_equivp) |
85 apply(rule) |
95 apply (rule) |
86 apply rule |
96 apply rule |
87 apply (rule list_rel_refl) |
97 apply (rule list_rel_refl) |
88 apply (metis equivp_def fset_equivp) |
98 apply (metis equivp_def fset_equivp) |
89 apply rule |
99 apply rule |
90 apply (rule equivp_reflp[OF fset_equivp]) |
100 apply (rule equivp_reflp[OF fset_equivp]) |
92 apply (metis equivp_def fset_equivp) |
102 apply (metis equivp_def fset_equivp) |
93 apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") |
103 apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") |
94 apply (metis Quotient_rel[OF Quotient_fset]) |
104 apply (metis Quotient_rel[OF Quotient_fset]) |
95 apply (auto simp only:)[1] |
105 apply (auto simp only:)[1] |
96 apply (subgoal_tac "map abs_fset r = map abs_fset b") |
106 apply (subgoal_tac "map abs_fset r = map abs_fset b") |
97 prefer 2 |
107 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
|
108 apply (simp only: map_rel_cong) |
98 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
109 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
99 apply (subgoal_tac "map abs_fset s = map abs_fset ba") |
|
100 prefer 2 |
|
101 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
110 apply (metis Quotient_rel[OF list_quotient[OF Quotient_fset]]) |
102 apply (simp only: map_rel_cong) |
|
103 apply rule |
111 apply rule |
104 apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"]) |
112 apply (rule rep_abs_rsp[of "list_rel op \<approx>" "map abs_fset"]) |
105 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
113 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
106 apply (rule list_rel_refl) |
114 apply (rule list_rel_refl) |
107 apply (metis equivp_def fset_equivp) |
115 apply (metis equivp_def fset_equivp) |
108 apply rule |
116 apply rule |
|
117 apply (erule conjE)+ |
109 prefer 2 |
118 prefer 2 |
110 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"]) |
119 apply (rule rep_abs_rsp_left[of "list_rel op \<approx>" "map abs_fset"]) |
111 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
120 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
112 apply (rule list_rel_refl) |
121 apply (rule list_rel_refl) |
113 apply (metis equivp_def fset_equivp) |
122 apply (metis equivp_def fset_equivp) |
114 apply (erule conjE)+ |
|
115 apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") |
123 apply (subgoal_tac "map abs_fset r \<approx> map abs_fset s") |
116 prefer 2 |
|
117 apply (metis Quotient_def Quotient_fset equivp_reflp fset_equivp) |
|
118 apply (rule map_rel_cong) |
124 apply (rule map_rel_cong) |
119 apply (assumption) |
125 apply (assumption) |
|
126 apply (subst Quotient_rel[OF Quotient_fset]) |
|
127 apply simp |
120 done |
128 done |
121 |
129 |
122 lemma quotient_compose_list[quot_thm]: |
130 lemma quotient_compose_list[quot_thm]: |
123 shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>)) |
131 shows "Quotient ((list_rel op \<approx>) OOO (op \<approx>)) |
124 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
132 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
137 apply rule |
145 apply rule |
138 apply rule |
146 apply rule |
139 apply (rule quotient_compose_list_pre) |
147 apply (rule quotient_compose_list_pre) |
140 done |
148 done |
141 |
149 |
|
150 lemma nil_prs2[quot_preserve]: "(abs_fset \<circ> map f) [] = abs_fset []" |
|
151 by simp |
|
152 |
142 lemma fconcat_empty: |
153 lemma fconcat_empty: |
143 shows "fconcat {||} = {||}" |
154 shows "fconcat {||} = {||}" |
144 apply(lifting concat.simps(1)) |
155 by (lifting concat.simps(1)) |
145 apply(cleaning) |
|
146 apply(simp add: comp_def bot_fset_def) |
|
147 done |
|
148 |
156 |
149 lemma insert_rsp2[quot_respect]: |
157 lemma insert_rsp2[quot_respect]: |
150 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
158 "(op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op # op #" |
151 apply auto |
159 apply auto |
152 apply (simp add: set_in_eq) |
160 apply (simp add: set_in_eq) |
158 |
166 |
159 lemma append_rsp[quot_respect]: |
167 lemma append_rsp[quot_respect]: |
160 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
168 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
161 by (auto) |
169 by (auto) |
162 |
170 |
|
171 lemma insert_prs2[quot_preserve]: |
|
172 "(rep_fset ---> (map rep_fset \<circ> rep_fset) ---> (abs_fset \<circ> map abs_fset)) op # = finsert" |
|
173 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
|
174 abs_o_rep[OF Quotient_fset] map_id finsert_def) |
|
175 |
163 lemma fconcat_insert: |
176 lemma fconcat_insert: |
164 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
177 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
165 apply (lifting concat.simps(2)) |
178 by (lifting concat.simps(2)) |
166 apply (cleaning) |
179 |
167 apply (simp add: finsert_def fconcat_def comp_def) |
180 lemma append_prs2[quot_preserve]: |
168 apply (cleaning) |
181 "((map rep_fset \<circ> rep_fset) ---> (map rep_fset \<circ> rep_fset) ---> abs_fset \<circ> map abs_fset) op @ = funion" |
169 done |
182 by (simp add: expand_fun_eq Quotient_abs_rep[OF Quotient_fset] |
|
183 abs_o_rep[OF Quotient_fset] map_id sup_fset_def) |
|
184 |
|
185 lemma append_rsp2[quot_respect]: |
|
186 "(list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx> ===> list_rel op \<approx> OOO op \<approx>) op @ op @" |
|
187 sorry |
|
188 |
|
189 lemma "fconcat (xs |\<union>| ys) = fconcat xs |\<union>| fconcat ys" |
|
190 by (lifting concat_append) |
170 |
191 |
171 (* TBD *) |
192 (* TBD *) |
|
193 |
|
194 |
|
195 find_theorems concat |
172 |
196 |
173 text {* syntax for fset comprehensions (adapted from lists) *} |
197 text {* syntax for fset comprehensions (adapted from lists) *} |
174 |
198 |
175 nonterminals fsc_qual fsc_quals |
199 nonterminals fsc_qual fsc_quals |
176 |
200 |