equal
deleted
inserted
replaced
101 |
101 |
102 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
102 lemma map_rel_cong: "b \<approx> ba \<Longrightarrow> map f b \<approx> map f ba" |
103 unfolding list_eq.simps |
103 unfolding list_eq.simps |
104 by (simp only: set_map set_in_eq) |
104 by (simp only: set_map set_in_eq) |
105 |
105 |
|
106 text {* Peter *} |
|
107 ML {* Quotient_Info.quotient_rules_get @{context} *} |
|
108 |
|
109 lemma |
|
110 assumes "Quotient R1 abs1 rep1" |
|
111 and "Quotient R2 abs2 rep2" |
|
112 shows "Quotient (R1 OOO R2) (abs1 o ab2) (rep1 o rep2)" |
|
113 using assms |
|
114 sorry |
|
115 |
|
116 lemma |
|
117 assumes "Quotient R1 abs1 rep1" |
|
118 and "Quotient R2 abs2 rep2" |
|
119 shows "Quotient (R3) (abs1 o ab2) (rep1 o rep2)" |
|
120 using assms |
|
121 sorry |
106 |
122 |
107 lemma quotient_compose_list[quot_thm]: |
123 lemma quotient_compose_list[quot_thm]: |
108 shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
124 shows "Quotient ((list_all2 op \<approx>) OOO (op \<approx>)) |
109 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
125 (abs_fset \<circ> (map abs_fset)) ((map rep_fset) \<circ> rep_fset)" |
110 unfolding Quotient_def comp_def |
126 unfolding Quotient_def comp_def |
162 text {* Respectfullness *} |
178 text {* Respectfullness *} |
163 |
179 |
164 lemma append_rsp[quot_respect]: |
180 lemma append_rsp[quot_respect]: |
165 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
181 shows "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
166 apply(simp del: list_eq.simps) |
182 apply(simp del: list_eq.simps) |
167 by auto |
183 by auto |
168 |
184 |
169 lemma append_rsp_unfolded: |
185 lemma append_rsp_unfolded: |
170 "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w" |
186 "\<lbrakk>x \<approx> y; v \<approx> w\<rbrakk> \<Longrightarrow> x @ v \<approx> y @ w" |
171 by auto |
187 by auto |
172 |
188 |
603 quotient_definition |
619 quotient_definition |
604 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
620 "fconcat :: ('a fset) fset \<Rightarrow> 'a fset" |
605 is |
621 is |
606 "concat" |
622 "concat" |
607 |
623 |
608 thm fconcat_def |
|
609 |
|
610 quotient_definition |
624 quotient_definition |
611 "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
625 "ffilter :: ('a \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'a fset" |
612 is |
626 is |
613 "filter" |
627 "filter" |
614 |
628 |
1302 text {* concat *} |
1316 text {* concat *} |
1303 |
1317 |
1304 lemma fconcat_empty: |
1318 lemma fconcat_empty: |
1305 shows "fconcat {||} = {||}" |
1319 shows "fconcat {||} = {||}" |
1306 by (lifting concat.simps(1)) |
1320 by (lifting concat.simps(1)) |
|
1321 |
|
1322 text {* Peter *} |
|
1323 lemma test: "equivp R ==> a = b --> R a b" |
|
1324 by (simp add: equivp_def) |
|
1325 |
|
1326 lemma |
|
1327 shows "fconcat {||} = {||}" |
|
1328 apply(lifting_setup concat.simps(1)) |
|
1329 apply(rule test) |
|
1330 apply(tactic {* resolve_tac (Quotient_Info.equiv_rules_get @{context}) 1 *}) |
|
1331 sorry |
1307 |
1332 |
1308 lemma fconcat_insert: |
1333 lemma fconcat_insert: |
1309 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
1334 shows "fconcat (finsert x S) = x |\<union>| fconcat S" |
1310 by (lifting concat.simps(2)) |
1335 by (lifting concat.simps(2)) |
1311 |
1336 |