331 lemma "FOLD f g (z::'b) (INSERT a x) = |
331 lemma "FOLD f g (z::'b) (INSERT a x) = |
332 (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)" |
332 (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 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
333 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *}) |
334 done |
334 done |
335 |
335 |
|
336 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
|
337 |
336 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
338 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)" |
337 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
339 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *}) |
338 done |
340 done |
339 |
341 |
340 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
342 lemma "FUNION (FUNION x xa) xb = FUNION x (FUNION xa xb)" |
341 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
343 apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) |
342 done |
344 done |
343 |
345 |
344 lemma cheat: "P" sorry |
346 lemma cheat: "P" sorry |
345 |
347 |
346 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
|
347 |
348 |
348 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
349 lemma "\<lbrakk>P EMPTY; \<And>a x. P x \<Longrightarrow> P (INSERT a x)\<rbrakk> \<Longrightarrow> P l" |
349 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
350 apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) |
350 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
351 apply(tactic {* procedure_tac @{context} @{thm list.induct} 1 *}) |
351 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
352 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
392 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
393 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 8 *) (* = reflexivity arising from cong *) |
393 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 *) |
394 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* E *) (* R x y assumptions *) |
395 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
396 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* A *) (* application if type needs lifting *) |
396 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
397 apply(tactic {* inj_repabs_tac_fset @{context} 1*}) (* 9 *) (* Rep-Abs-elim - can be complex Rep-Abs *) |
397 done |
|
398 |
|
399 quotient_def |
|
400 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
|
401 where |
|
402 "fset_rec \<equiv> list_rec" |
|
403 |
|
404 quotient_def |
|
405 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
|
406 where |
|
407 "fset_case \<equiv> list_case" |
|
408 |
|
409 (* Probably not true without additional assumptions about the function *) |
|
410 lemma list_rec_rsp[quot_rsp]: |
|
411 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
|
412 apply (auto simp add: FUN_REL_EQ) |
|
413 apply (erule_tac list_eq.induct) |
|
414 apply (simp_all) |
|
415 sorry |
|
416 |
|
417 lemma list_case_rsp[quot_rsp]: |
|
418 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
|
419 apply (auto simp add: FUN_REL_EQ) |
|
420 sorry |
|
421 |
|
422 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
|
423 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
|
424 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
|
425 |
|
426 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
|
427 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
|
428 done |
|
429 |
|
430 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
|
431 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) |
|
432 done |
398 done |
433 |
399 |
434 lemma list_induct_part: |
400 lemma list_induct_part: |
435 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
401 assumes a: "P (x :: 'a list) ([] :: 'c list)" |
436 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
402 assumes b: "\<And>e t. P x t \<Longrightarrow> P x (e # t)" |
439 apply (rule a) |
405 apply (rule a) |
440 apply (rule b) |
406 apply (rule b) |
441 apply (assumption) |
407 apply (assumption) |
442 done |
408 done |
443 |
409 |
444 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *} |
|
445 |
|
446 (* Construction site starts here *) |
|
447 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" |
410 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" |
448 apply (tactic {* procedure_tac @{context} @{thm list_induct_part} 1 *}) |
411 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
449 apply (tactic {* regularize_tac @{context} [rel_eqv] 1 *}) |
412 done |
450 prefer 2 |
413 |
451 apply (tactic {* clean_tac @{context} [quot] defs 1 *}) |
414 lemma "P (x :: 'a fset) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l" |
452 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
415 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
453 apply (rule FUN_QUOTIENT) |
416 done |
454 apply (rule FUN_QUOTIENT) |
417 |
455 apply (rule IDENTITY_QUOTIENT) |
418 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
456 apply (rule FUN_QUOTIENT) |
419 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *}) |
457 apply (rule QUOTIENT_fset) |
420 done |
458 apply (rule IDENTITY_QUOTIENT) |
421 |
459 apply (rule IDENTITY_QUOTIENT) |
422 quotient_def |
460 apply (rule IDENTITY_QUOTIENT) |
423 fset_rec::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
461 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
424 where |
462 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
425 "fset_rec \<equiv> list_rec" |
463 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
426 |
464 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
427 quotient_def |
465 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
428 fset_case::"'a \<Rightarrow> ('b \<Rightarrow> 'b fset \<Rightarrow> 'a) \<Rightarrow> 'b fset \<Rightarrow> 'a" |
466 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
429 where |
467 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
430 "fset_case \<equiv> list_case" |
468 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
431 |
469 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
432 (* Probably not true without additional assumptions about the function *) |
470 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
433 lemma list_rec_rsp[quot_rsp]: |
471 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
434 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec" |
472 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
435 apply (auto simp add: FUN_REL_EQ) |
473 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
436 apply (erule_tac list_eq.induct) |
474 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
437 apply (simp_all) |
475 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
438 sorry |
476 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
439 |
477 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
440 lemma list_case_rsp[quot_rsp]: |
478 apply (tactic {* (APPLY_RSP_TAC rty @{context}) 1 *}) |
441 "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case" |
479 apply (rule IDENTITY_QUOTIENT) |
442 apply (auto simp add: FUN_REL_EQ) |
480 apply (rule FUN_QUOTIENT) |
443 sorry |
481 apply (rule QUOTIENT_fset) |
444 |
482 apply (rule IDENTITY_QUOTIENT) |
445 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *} |
483 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
446 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *} |
484 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
447 ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *} |
485 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
448 |
486 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
449 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)" |
487 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
450 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *}) |
488 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
451 done |
489 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
452 |
490 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
453 lemma "fset_case (f1::'t) f2 (INSERT a xa) = f2 a xa" |
491 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
454 apply (tactic {* lift_tac_fset @{context} @{thm list.cases(2)} 1 *}) |
492 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
455 done |
493 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
456 |
494 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
457 thm all_prs |
495 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
458 |
496 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
497 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
498 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
499 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
500 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
501 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
502 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
503 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
504 apply (rule IDENTITY_QUOTIENT) |
|
505 apply (rule FUN_QUOTIENT) |
|
506 apply (rule QUOTIENT_fset) |
|
507 apply (rule IDENTITY_QUOTIENT) |
|
508 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
|
509 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
|
510 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
511 apply assumption |
|
512 apply (rule refl) |
|
513 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
514 apply assumption |
|
515 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
516 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
517 apply (rule IDENTITY_QUOTIENT) |
|
518 apply (rule FUN_QUOTIENT) |
|
519 apply (rule QUOTIENT_fset) |
|
520 apply (rule IDENTITY_QUOTIENT) |
|
521 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
|
522 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
|
523 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
524 apply assumption |
|
525 apply (rule refl) |
|
526 apply (tactic {* REPEAT_ALL_NEW (inj_repabs_tac_fset @{context}) 1 *}) |
|
527 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
528 apply (tactic {* instantiate_tac @{thm APPLY_RSP} @{context} 1 *}) |
|
529 apply (rule IDENTITY_QUOTIENT) |
|
530 apply (rule FUN_QUOTIENT) |
|
531 apply (rule QUOTIENT_fset) |
|
532 apply (rule IDENTITY_QUOTIENT) |
|
533 prefer 2 apply(tactic{* quot_true_tac @{context} (snd o dest_comb) 1*}) |
|
534 prefer 2 apply(tactic{* quot_true_tac @{context} (fst o dest_comb) 1*}) |
|
535 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
536 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
537 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
538 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
539 apply (tactic {* (inj_repabs_tac_fset @{context}) 1 *}) |
|
540 done |
|
541 |
|
542 ML {* #quot_thm (hd (quotdata_dest @{theory})) *} |
|
543 print_quotients |
|
544 thm QUOTIENT_fset |
|
545 end |
459 end |