176 term fmap |
176 term fmap |
177 thm fmap_def |
177 thm fmap_def |
178 |
178 |
179 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} |
179 ML {* val defs = @{thms EMPTY_def IN_def FUNION_def CARD_def INSERT_def fmap_def FOLD_def} *} |
180 |
180 |
181 lemma memb_rsp: |
181 lemma memb_rsp[quot_rsp]: |
182 fixes z |
182 fixes z |
183 assumes a: "list_eq x y" |
183 assumes a: "x \<approx> y" |
184 shows "(z memb x) = (z memb y)" |
184 shows "(z memb x) = (z memb y)" |
185 using a by induct auto |
185 using a by induct auto |
186 |
186 |
187 lemma ho_memb_rsp: |
187 lemma ho_memb_rsp[quot_rsp]: |
188 "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)" |
188 "(op = ===> (op \<approx> ===> op =)) (op memb) (op memb)" |
189 by (simp add: memb_rsp) |
189 by (simp add: memb_rsp) |
190 |
190 |
191 lemma card1_rsp: |
191 lemma card1_rsp[quot_rsp]: |
192 fixes a b :: "'a list" |
192 fixes a b :: "'a list" |
193 assumes e: "a \<approx> b" |
193 assumes e: "a \<approx> b" |
194 shows "card1 a = card1 b" |
194 shows "card1 a = card1 b" |
195 using e by induct (simp_all add:memb_rsp) |
195 using e by induct (simp_all add:memb_rsp) |
196 |
196 |
197 lemma ho_card1_rsp: "(op \<approx> ===> op =) card1 card1" |
197 lemma ho_card1_rsp[quot_rsp]: |
|
198 "(op \<approx> ===> op =) card1 card1" |
198 by (simp add: card1_rsp) |
199 by (simp add: card1_rsp) |
199 |
200 |
200 lemma cons_rsp: |
201 lemma cons_rsp[quot_rsp]: |
201 fixes z |
202 fixes z |
202 assumes a: "xs \<approx> ys" |
203 assumes a: "xs \<approx> ys" |
203 shows "(z # xs) \<approx> (z # ys)" |
204 shows "(z # xs) \<approx> (z # ys)" |
204 using a by (rule list_eq.intros(5)) |
205 using a by (rule list_eq.intros(5)) |
205 |
206 |
206 lemma ho_cons_rsp: |
207 lemma ho_cons_rsp[quot_rsp]: |
207 "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
208 "(op = ===> op \<approx> ===> op \<approx>) op # op #" |
208 by (simp add: cons_rsp) |
209 by (simp add: cons_rsp) |
209 |
210 |
210 lemma append_rsp_fst: |
211 lemma append_rsp_fst: |
211 assumes a : "list_eq l1 l2" |
212 assumes a : "l1 \<approx> l2" |
212 shows "(l1 @ s) \<approx> (l2 @ s)" |
213 shows "(l1 @ s) \<approx> (l2 @ s)" |
213 using a |
214 using a |
214 by (induct) (auto intro: list_eq.intros list_eq_refl) |
215 by (induct) (auto intro: list_eq.intros list_eq_refl) |
215 |
216 |
216 lemma append_end: |
217 lemma append_end: |
243 apply (rule append_rsp_fst) |
244 apply (rule append_rsp_fst) |
244 apply (rule list_eq.intros(3)) |
245 apply (rule list_eq.intros(3)) |
245 apply (rule rev_rsp) |
246 apply (rule rev_rsp) |
246 done |
247 done |
247 |
248 |
248 lemma append_rsp: |
249 lemma append_rsp[quot_rsp]: |
249 assumes a : "list_eq l1 r1" |
250 assumes a : "l1 \<approx> r1" |
250 assumes b : "list_eq l2 r2 " |
251 assumes b : "l2 \<approx> r2 " |
251 shows "(l1 @ l2) \<approx> (r1 @ r2)" |
252 shows "(l1 @ l2) \<approx> (r1 @ r2)" |
252 apply (rule list_eq.intros(6)) |
253 apply (rule list_eq.intros(6)) |
253 apply (rule append_rsp_fst) |
254 apply (rule append_rsp_fst) |
254 using a apply (assumption) |
255 using a apply (assumption) |
255 apply (rule list_eq.intros(6)) |
256 apply (rule list_eq.intros(6)) |
258 apply (rule append_rsp_fst) |
259 apply (rule append_rsp_fst) |
259 using b apply (assumption) |
260 using b apply (assumption) |
260 apply (rule append_sym_rsp) |
261 apply (rule append_sym_rsp) |
261 done |
262 done |
262 |
263 |
263 lemma ho_append_rsp: |
264 lemma ho_append_rsp[quot_rsp]: |
264 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
265 "(op \<approx> ===> op \<approx> ===> op \<approx>) op @ op @" |
265 by (simp add: append_rsp) |
266 by (simp add: append_rsp) |
266 |
267 |
267 lemma map_rsp: |
268 lemma map_rsp[quot_rsp]: |
268 assumes a: "a \<approx> b" |
269 assumes a: "a \<approx> b" |
269 shows "map f a \<approx> map f b" |
270 shows "map f a \<approx> map f b" |
270 using a |
271 using a |
271 apply (induct) |
272 apply (induct) |
272 apply(auto intro: list_eq.intros) |
273 apply(auto intro: list_eq.intros) |
273 done |
274 done |
274 |
275 |
275 lemma ho_map_rsp: |
276 lemma ho_map_rsp[quot_rsp]: |
276 "(op = ===> op \<approx> ===> op \<approx>) map map" |
277 "(op = ===> op \<approx> ===> op \<approx>) map map" |
277 by (simp add: map_rsp) |
278 by (simp add: map_rsp) |
278 |
279 |
279 lemma map_append: |
280 lemma map_append: |
280 "(map f (a @ b)) \<approx> |
281 "(map f (a @ b)) \<approx> (map f a) @ (map f b)" |
281 (map f a) @ (map f b)" |
|
282 by simp (rule list_eq_refl) |
282 by simp (rule list_eq_refl) |
283 |
283 |
284 lemma ho_fold_rsp: |
284 lemma ho_fold_rsp[quot_rsp]: |
285 "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
285 "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1" |
286 apply (auto simp add: FUN_REL_EQ) |
286 apply (auto simp add: FUN_REL_EQ) |
287 apply (case_tac "rsp_fold x") |
287 apply (case_tac "rsp_fold x") |
288 prefer 2 |
288 prefer 2 |
289 apply (erule_tac list_eq.induct) |
289 apply (erule_tac list_eq.induct) |
293 apply (auto simp add: memb_rsp rsp_fold_def) |
293 apply (auto simp add: memb_rsp rsp_fold_def) |
294 done |
294 done |
295 |
295 |
296 print_quotients |
296 print_quotients |
297 |
297 |
298 |
|
299 ML {* val qty = @{typ "'a fset"} *} |
298 ML {* val qty = @{typ "'a fset"} *} |
300 ML {* val rsp_thms = |
299 ML {* val rsp_thms = |
301 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
300 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} |
302 @ @{thms ho_all_prs ho_ex_prs} *} |
301 @ @{thms ho_all_prs ho_ex_prs} *} |
303 |
302 |
304 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
303 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *} |
305 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
304 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
306 ML {* val consts = lookup_quot_consts defs *} |
305 ML {* val consts = lookup_quot_consts defs *} |
307 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} |
306 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
308 |
307 |
309 lemma "IN x EMPTY = False" |
308 lemma "IN x EMPTY = False" |
310 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
309 by (tactic {* lift_tac_fset @{context} @{thm m1} 1 *}) |
311 |
310 |
312 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
311 lemma "IN x (INSERT y xa) = (x = y \<or> IN x xa)" |
326 |
325 |
327 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
326 lemma "(\<not> IN x xa) = (CARD (INSERT x xa) = Suc (CARD xa))" |
328 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) |
327 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *}) |
329 done |
328 done |
330 |
329 |
331 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
330 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
332 |
331 |
333 lemma "FOLD f g (z::'b) (INSERT a x) = |
332 lemma "FOLD f g (z::'b) (INSERT a x) = |
334 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
333 (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)" |
335 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
334 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
336 done |
335 done |
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
394 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
394 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
396 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
397 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
398 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
|
399 done |
395 done |
400 |
396 |
401 quotient_def |
397 quotient_def |
402 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
398 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
403 where |
399 where |
407 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
403 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
408 where |
404 where |
409 "fset_case \<equiv> list_case" |
405 "fset_case \<equiv> list_case" |
410 |
406 |
411 (* Probably not true without additional assumptions about the function *) |
407 (* Probably not true without additional assumptions about the function *) |
412 lemma list_rec_rsp: |
408 lemma list_rec_rsp[quot_rsp]: |
413 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
409 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
414 apply (auto simp add: FUN_REL_EQ) |
410 apply (auto simp add: FUN_REL_EQ) |
415 apply (erule_tac list_eq.induct) |
411 apply (erule_tac list_eq.induct) |
416 apply (simp_all) |
412 apply (simp_all) |
417 sorry |
413 sorry |
418 |
414 |
419 lemma list_case_rsp: |
415 lemma list_case_rsp[quot_rsp]: |
420 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
416 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
421 apply (auto simp add: FUN_REL_EQ) |
417 apply (auto simp add: FUN_REL_EQ) |
422 sorry |
418 sorry |
423 |
419 |
424 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
420 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
425 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
421 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
426 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *} |
422 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
427 |
423 |
428 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
424 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
429 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
425 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
430 done |
426 done |
431 |
427 |
441 apply (rule a) |
437 apply (rule a) |
442 apply (rule b) |
438 apply (rule b) |
443 apply (assumption) |
439 apply (assumption) |
444 done |
440 done |
445 |
441 |
446 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *} |
442 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
447 |
443 |
448 (* Construction site starts here *) |
444 (* Construction site starts here *) |
449 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
445 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
450 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) |
446 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) |
451 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
447 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |