equal
deleted
inserted
replaced
527 begin |
527 begin |
528 |
528 |
529 primrec |
529 primrec |
530 permute_sum |
530 permute_sum |
531 where |
531 where |
532 "p \<bullet> (Inl x) = Inl (p \<bullet> x)" |
532 Inl_eqvt: "p \<bullet> (Inl x) = Inl (p \<bullet> x)" |
533 | "p \<bullet> (Inr y) = Inr (p \<bullet> y)" |
533 | Inr_eqvt: "p \<bullet> (Inr y) = Inr (p \<bullet> y)" |
534 |
534 |
535 instance |
535 instance |
536 by (default) (case_tac [!] x, simp_all) |
536 by (default) (case_tac [!] x, simp_all) |
537 |
537 |
538 end |
538 end |
543 begin |
543 begin |
544 |
544 |
545 primrec |
545 primrec |
546 permute_list |
546 permute_list |
547 where |
547 where |
548 "p \<bullet> [] = []" |
548 Nil_eqvt: "p \<bullet> [] = []" |
549 | "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs" |
549 | Cons_eqvt: "p \<bullet> (x # xs) = p \<bullet> x # p \<bullet> xs" |
550 |
550 |
551 instance |
551 instance |
552 by (default) (induct_tac [!] x, simp_all) |
552 by (default) (induct_tac [!] x, simp_all) |
553 |
553 |
554 end |
554 end |
565 begin |
565 begin |
566 |
566 |
567 primrec |
567 primrec |
568 permute_option |
568 permute_option |
569 where |
569 where |
570 "p \<bullet> None = None" |
570 None_eqvt: "p \<bullet> None = None" |
571 | "p \<bullet> (Some x) = Some (p \<bullet> x)" |
571 | Some_eqvt: "p \<bullet> (Some x) = Some (p \<bullet> x)" |
572 |
572 |
573 instance |
573 instance |
574 by (default) (induct_tac [!] x, simp_all) |
574 by (default) (induct_tac [!] x, simp_all) |
575 |
575 |
576 end |
576 end |