468 quotient_definition |
468 quotient_definition |
469 Abs_set ("[_]set. _" [60, 60] 60) |
469 Abs_set ("[_]set. _" [60, 60] 60) |
470 where |
470 where |
471 "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set" |
471 "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set" |
472 is |
472 is |
473 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
473 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" . |
474 |
474 |
475 quotient_definition |
475 quotient_definition |
476 Abs_res ("[_]res. _" [60, 60] 60) |
476 Abs_res ("[_]res. _" [60, 60] 60) |
477 where |
477 where |
478 "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res" |
478 "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res" |
479 is |
479 is |
480 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
480 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" . |
481 |
481 |
482 quotient_definition |
482 quotient_definition |
483 Abs_lst ("[_]lst. _" [60, 60] 60) |
483 Abs_lst ("[_]lst. _" [60, 60] 60) |
484 where |
484 where |
485 "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst" |
485 "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst" |
486 is |
486 is |
487 "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)" |
487 "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)" . |
488 |
488 |
489 lemma [quot_respect]: |
489 lemma [quot_respect]: |
490 shows "(op= ===> op= ===> alpha_abs_set) Pair Pair" |
490 shows "(op= ===> op= ===> alpha_abs_set) Pair Pair" |
491 and "(op= ===> op= ===> alpha_abs_res) Pair Pair" |
491 and "(op= ===> op= ===> alpha_abs_res) Pair Pair" |
492 and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" |
492 and "(op= ===> op= ===> alpha_abs_lst) Pair Pair" |
538 begin |
538 begin |
539 |
539 |
540 quotient_definition |
540 quotient_definition |
541 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set" |
541 "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set" |
542 is |
542 is |
543 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
543 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
|
544 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
544 |
545 |
545 lemma permute_Abs_set[simp]: |
546 lemma permute_Abs_set[simp]: |
546 fixes x::"'a::pt" |
547 fixes x::"'a::pt" |
547 shows "(p \<bullet> ([as]set. x)) = [p \<bullet> as]set. (p \<bullet> x)" |
548 shows "(p \<bullet> ([as]set. x)) = [p \<bullet> as]set. (p \<bullet> x)" |
548 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
549 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
560 |
561 |
561 quotient_definition |
562 quotient_definition |
562 "permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res" |
563 "permute_abs_res::perm \<Rightarrow> ('a::pt abs_res) \<Rightarrow> 'a abs_res" |
563 is |
564 is |
564 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
565 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
|
566 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
565 |
567 |
566 lemma permute_Abs_res[simp]: |
568 lemma permute_Abs_res[simp]: |
567 fixes x::"'a::pt" |
569 fixes x::"'a::pt" |
568 shows "(p \<bullet> ([as]res. x)) = [p \<bullet> as]res. (p \<bullet> x)" |
570 shows "(p \<bullet> ([as]res. x)) = [p \<bullet> as]res. (p \<bullet> x)" |
569 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
571 by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"]) |
581 |
583 |
582 quotient_definition |
584 quotient_definition |
583 "permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst" |
585 "permute_abs_lst::perm \<Rightarrow> ('a::pt abs_lst) \<Rightarrow> 'a abs_lst" |
584 is |
586 is |
585 "permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)" |
587 "permute:: perm \<Rightarrow> (atom list \<times> 'a::pt) \<Rightarrow> (atom list \<times> 'a::pt)" |
|
588 by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt) |
586 |
589 |
587 lemma permute_Abs_lst[simp]: |
590 lemma permute_Abs_lst[simp]: |
588 fixes x::"'a::pt" |
591 fixes x::"'a::pt" |
589 shows "(p \<bullet> ([as]lst. x)) = [p \<bullet> as]lst. (p \<bullet> x)" |
592 shows "(p \<bullet> ([as]lst. x)) = [p \<bullet> as]lst. (p \<bullet> x)" |
590 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) |
593 by (lifting permute_prod.simps[where 'a="atom list" and 'b="'a"]) |