9 | "[] \<approx> []" |
9 | "[] \<approx> []" |
10 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
10 | "xs \<approx> ys \<Longrightarrow> ys \<approx> xs" |
11 | "a#a#xs \<approx> a#xs" |
11 | "a#a#xs \<approx> a#xs" |
12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
12 | "xs \<approx> ys \<Longrightarrow> a#xs \<approx> a#ys" |
13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
13 | "\<lbrakk>xs1 \<approx> xs2; xs2 \<approx> xs3\<rbrakk> \<Longrightarrow> xs1 \<approx> xs3" |
14 |
|
15 lemma |
|
16 "(list_eq ===> (list_eq ===> (op =))) (list_eq) (list_eq)" |
|
17 apply(simp add: FUN_REL.simps) |
|
18 apply(rule allI | rule impI)+ |
|
19 sorry |
|
20 |
14 |
21 lemma list_eq_refl: |
15 lemma list_eq_refl: |
22 shows "xs \<approx> xs" |
16 shows "xs \<approx> xs" |
23 by (induct xs) (auto intro: list_eq.intros) |
17 by (induct xs) (auto intro: list_eq.intros) |
24 |
18 |
295 apply (erule_tac list_eq.induct) |
289 apply (erule_tac list_eq.induct) |
296 apply (simp_all) |
290 apply (simp_all) |
297 apply (auto simp add: memb_rsp rsp_fold_def) |
291 apply (auto simp add: memb_rsp rsp_fold_def) |
298 done |
292 done |
299 |
293 |
|
294 lemma list_eq_rsp[quot_rsp]: |
|
295 "(op \<approx> ===> op \<approx> ===> op =) (op \<approx>) (op \<approx>)" |
|
296 apply(simp add: FUN_REL.simps) |
|
297 apply(auto) |
|
298 apply(blast intro: list_eq.intros) |
|
299 apply(blast intro: list_eq.intros) |
|
300 done |
|
301 |
|
302 lemma list_eq_rsp2[quot_rsp]: |
|
303 "(op \<approx> ===> op =) (op \<approx>) (op \<approx>)" |
|
304 apply(simp add: FUN_REL.simps) |
|
305 apply(rule allI)+ |
|
306 apply(rule impI) |
|
307 apply(simp add: expand_fun_eq) |
|
308 apply(rule allI) |
|
309 apply(blast intro: list_eq.intros) |
|
310 done |
|
311 |
300 print_quotients |
312 print_quotients |
301 |
313 |
302 ML {* val qty = @{typ "'a fset"} *} |
314 ML {* val qty = @{typ "'a fset"} *} |
303 ML {* val rsp_thms = |
315 ML {* val rsp_thms = |
304 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
316 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
307 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
319 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *} |
308 ML {* val consts = lookup_quot_consts defs *} |
320 ML {* val consts = lookup_quot_consts defs *} |
309 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
321 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
310 |
322 |
311 thm m1 |
323 thm m1 |
|
324 |
312 |
325 |
313 lemma "IN x EMPTY = False" |
326 lemma "IN x EMPTY = False" |
314 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
327 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *}) |
315 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
328 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
316 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
329 apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *}) |
342 (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)" |
355 (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)" |
343 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
356 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
344 done |
357 done |
345 |
358 |
346 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
359 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
|
360 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
|
361 ML_prf {* val qtm = #concl (fst (Subgoal.focus @{context} 1 (#goal (Isar.goal ())))) *} |
|
362 apply(tactic {* procedure_tac @{context} @{thm map_append} 1 *}) |
|
363 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
|
364 prefer 2 |
|
365 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
|
366 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
367 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
368 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
369 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
370 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
371 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
372 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
373 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
374 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
375 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
376 |
|
377 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
378 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
379 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
380 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
381 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
382 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
383 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
384 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
385 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
386 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
387 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
388 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
389 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
390 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
391 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
394 back |
|
395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
396 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
397 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
398 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
399 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
400 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
401 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
402 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
403 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) |
|
404 |
347 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
405 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
348 done |
406 done |
349 |
407 |
350 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
408 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
351 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
409 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |