289 apply (erule_tac list_eq.induct) |
289 apply (erule_tac list_eq.induct) |
290 apply (simp_all) |
290 apply (simp_all) |
291 apply (auto simp add: memb_rsp rsp_fold_def) |
291 apply (auto simp add: memb_rsp rsp_fold_def) |
292 done |
292 done |
293 |
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 |
|
312 print_quotients |
294 print_quotients |
313 |
295 |
314 ML {* val qty = @{typ "'a fset"} *} |
296 ML {* val qty = @{typ "'a fset"} *} |
315 ML {* val rsp_thms = |
297 ML {* val rsp_thms = |
316 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
298 @{thms ho_memb_rsp ho_cons_rsp ho_card1_rsp ho_map_rsp ho_append_rsp ho_fold_rsp} *} |
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)" |
337 (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)" |
356 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
338 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
357 done |
339 done |
358 |
340 |
359 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
341 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 |
|
405 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
342 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
406 done |
343 done |
407 |
344 |
408 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
345 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
409 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
346 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
418 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
355 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
419 prefer 2 |
356 prefer 2 |
420 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
357 apply(tactic {* clean_tac @{context} [quot] defs 1 *}) |
421 apply(rule_tac a="\<forall>(P\<Colon>'a fset \<Rightarrow> bool) l\<Colon>'a fset. P EMPTY \<longrightarrow> (\<forall>(a\<Colon>'a) x\<Colon>'a fset. P x \<longrightarrow> P (INSERT a x)) \<longrightarrow> P l" in QUOT_TRUE_i) |
358 apply(rule_tac a="\<forall>(P\<Colon>'a fset \<Rightarrow> bool) l\<Colon>'a fset. P EMPTY \<longrightarrow> (\<forall>(a\<Colon>'a) x\<Colon>'a fset. P x \<longrightarrow> P (INSERT a x)) \<longrightarrow> P l" in QUOT_TRUE_i) |
422 |
359 |
|
360 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
423 apply (drule QT_all) |
361 apply (drule QT_all) |
424 apply (drule_tac x = "x" in QT_lam) |
362 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
363 apply(tactic {* lambda_res_tac @{context} 1 *}) |
|
364 apply(tactic {* rule FUN_REL_I) |
|
365 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
|
366 apply(clarify) |
|
367 apply (drule_tac x="x" in QT_lam) |
|
368 |
|
369 |
|
370 |
|
371 thm QT_lam |
425 apply (drule QT_all) |
372 apply (drule QT_all) |
426 apply (drule_tac x = "y" in QT_lam) |
373 apply (drule_tac x = "yyy" in QT_lam) |
427 apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *}) |
374 apply (tactic {* quot_true_tac @{context} (fst o strip_comb) 1 *}) |
428 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
375 |
429 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
|
430 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
|
431 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
376 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 3 *) (* Ball-Ball *) |
432 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
377 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
433 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
378 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 2 *) (* lam-lam-elim for R = (===>) *) |
434 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
379 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
435 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |
380 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* B *) (* Cong *) |