312 \noindent |
316 \noindent |
313 and verify the four simple properties |
317 and verify the four simple properties |
314 |
318 |
315 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
319 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
316 \begin{tabular}{@ {}l} |
320 \begin{tabular}{@ {}l} |
317 @{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\ |
321 i)~~@{thm add_assoc[where a="\<pi>\<^isub>1" and b="\<pi>\<^isub>2" and c="\<pi>\<^isub>3"]}\\ |
318 @{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm} |
322 ii)~~@{thm monoid_add_class.add_0_left[where a="\<pi>::perm"]} \hspace{9mm} |
319 @{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm} |
323 iii)~~@{thm monoid_add_class.add_0_right[where a="\<pi>::perm"]} \hspace{9mm} |
320 @{thm group_add_class.left_minus[where a="\<pi>::perm"]} |
324 iv)~~@{thm group_add_class.left_minus[where a="\<pi>::perm"]} |
321 \end{tabular} |
325 \end{tabular}\hfill\numbered{grouplaws} |
322 \end{isabelle} |
326 \end{isabelle} |
323 |
327 |
324 \noindent |
328 \noindent |
325 The technical importance of this fact is that we can rely on |
329 The technical importance of this fact is that we can rely on |
326 Isabelle/HOL's existing simplification infrastructure for groups, which will |
330 Isabelle/HOL's existing simplification infrastructure for groups, which will |
327 come in handy when we have to do calculations with permutations. |
331 come in handy when we have to do calculations with permutations. |
328 Note that Isabelle/HOL defies standard conventions of mathematical notation |
332 Note that Isabelle/HOL defies standard conventions of mathematical notation |
329 by using additive syntax even for non-commutative groups. Obviously, |
333 by using additive syntax even for non-commutative groups. Obviously, |
330 composition of permutations is not commutative in general, because @{text |
334 composition of permutations is not commutative in general; for example |
331 "\<pi>\<^sub>1 + \<pi>\<^sub>2 \<noteq> \<pi>\<^sub>2 + \<pi>\<^sub>1"}. But since the point of this paper is to implement the |
335 |
|
336 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
337 @{text "(a b) + (b c) \<noteq> (b c) + (a b)"} |
|
338 \end{isabelle} |
|
339 |
|
340 \noindent |
|
341 But since the point of this paper is to implement the |
332 nominal theory as smoothly as possible in Isabelle/HOL, we tolerate |
342 nominal theory as smoothly as possible in Isabelle/HOL, we tolerate |
333 the non-standard notation in order to reuse the existing libraries. |
343 the non-standard notation in order to reuse the existing libraries. |
334 |
344 |
335 A \emph{permutation operation}, written @{text "\<pi> \<bullet> x"}, applies a permutation |
345 A \emph{permutation operation}, written infix as @{text "\<pi> \<bullet> x"}, |
336 @{text "\<pi>"} to an object @{text "x"} of type @{text \<beta>}, say. |
346 applies a permutation @{text "\<pi>"} to an object @{text "x"} of type |
337 This operation has the type |
347 @{text \<beta>}, say. This operation has the type |
338 |
348 |
339 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
349 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
340 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
350 @{text "_ \<bullet> _ :: perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"} |
341 \end{isabelle} |
351 \end{isabelle} |
342 |
352 |
343 \noindent |
353 \noindent |
344 Isabelle/HOL will allow us to give a definition of this operation for |
354 Isabelle/HOL allows us to give a definition of this operation for |
345 `base' types, such as atoms, permutations, booleans and natural numbers, |
355 `base' types, such as atoms, permutations, booleans and natural numbers: |
346 and for type-constructors, such as functions, sets, lists and products. |
|
347 |
356 |
348 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
357 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
349 \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} |
358 \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} |
350 atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\ |
359 atoms: & @{thm permute_atom_def[where p="\<pi>",no_vars, THEN eq_reflection]}\\ |
351 permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\ |
360 permutations: & @{thm permute_perm_def[where p="\<pi>" and q="\<pi>'", THEN eq_reflection]}\\ |
352 booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
361 booleans: & @{thm permute_bool_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
353 nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
362 nats: & @{thm permute_nat_def[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
|
363 \end{tabular}\hfill\numbered{permdefsbase} |
|
364 \end{isabelle} |
|
365 |
|
366 \noindent |
|
367 and for type-constructors, such as functions, sets, lists and products: |
|
368 |
|
369 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
370 \begin{tabular}{@ {}l@ {\hspace{4mm}}l@ {}} |
354 functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\ |
371 functions: & @{text "\<pi> \<bullet> f \<equiv> \<lambda>x. \<pi> \<bullet> (f ((-\<pi>) \<bullet> x))"}\\ |
355 sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
372 sets: & @{thm permute_set_eq[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
356 lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
373 lists: & @{thm permute_list.simps(1)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
357 & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
374 & @{thm permute_list.simps(2)[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
358 products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
375 products: & @{thm permute_prod.simps[where p="\<pi>", no_vars, THEN eq_reflection]}\\ |
359 \end{tabular}\hfill\numbered{permdefs} |
376 \end{tabular}\hfill\numbered{permdefsconstrs} |
360 \end{isabelle} |
377 \end{isabelle} |
361 |
378 |
362 In order to reason abstractly about this operation, |
379 In order to reason abstractly about this operation, |
363 we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two |
380 we use Isabelle/HOL's type classes~\cite{Wenzel04} and state the following two |
364 \emph{permutation properties}: |
381 \emph{permutation properties}: |
445 |
463 |
446 \noindent |
464 \noindent |
447 and establish: |
465 and establish: |
448 |
466 |
449 \begin{theorem} |
467 \begin{theorem} |
450 If @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text "\<beta>\<^isub>2"} are permutation types, |
468 The types @{type atom}, @{type perm}, @{type bool} and @{type nat} |
451 then so are @{text "atom"}, @{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}, |
469 are permutation types, and if @{text \<beta>}, @{text "\<beta>\<^isub>1"} and @{text |
452 @{text perm}, @{term "\<beta> set"}, @{term "\<beta> list"}, @{term "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}, |
470 "\<beta>\<^isub>2"} are permutation types, then so are \mbox{@{text "\<beta>\<^isub>1 \<Rightarrow> \<beta>\<^isub>2"}}, |
453 @{text bool} and @{text "nat"}. |
471 @{text "\<beta> set"}, @{text "\<beta> list"} and @{text "\<beta>\<^isub>1 \<times> \<beta>\<^isub>2"}. |
454 \end{theorem} |
472 \end{theorem} |
455 |
473 |
456 \begin{proof} |
474 \begin{proof} |
457 All statements are by unfolding the definitions of the permutation |
475 All statements are by unfolding the definitions of the permutation |
458 operations and simple calculations involving addition and |
476 operations and simple calculations involving addition and |
459 minus. With permutations for example we have |
477 minus. In case of permutations for example we have |
460 |
478 |
461 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
479 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
462 \begin{tabular}[b]{@ {}rcl} |
480 \begin{tabular}[b]{@ {}rcl} |
463 @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\ |
481 @{text "0 \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "0 + \<pi>' - 0 = \<pi>'"}\\ |
464 @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\ |
482 @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) \<bullet> \<pi>'"} & @{text "\<equiv>"} & @{text "(\<pi>\<^isub>1 + \<pi>\<^isub>2) + \<pi>' - (\<pi>\<^isub>1 + \<pi>\<^isub>2)"}\\ |
528 \end{tabular} |
552 \end{tabular} |
529 \end{isabelle} |
553 \end{isabelle} |
530 |
554 |
531 \noindent |
555 \noindent |
532 using the permutation operation on booleans and property |
556 using the permutation operation on booleans and property |
533 \eqref{permuteequ}. |
557 \eqref{permuteequ}. Lemma~\ref{permutecompose} establishes that the |
534 Lemma~\ref{permutecompose} establishes that the |
|
535 permutation operation is equivariant. The permutation operation for |
558 permutation operation is equivariant. The permutation operation for |
536 lists and products, shown in \eqref{permdefs}, state that the |
559 lists and products, shown in \eqref{permdefsconstrs}, state that the |
537 constructors for products, @{text "Nil"} and @{text Cons} are |
560 constructors for products, @{text "Nil"} and @{text Cons} are |
538 equivariant. Furthermore a simple calculation will show that our |
561 equivariant. Furthermore a simple calculation will show that our |
539 swapping functions are equivariant, that is |
562 swapping functions are equivariant, that is |
540 |
563 |
541 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
564 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
542 \begin{tabular}{@ {}l} |
565 \begin{tabular}{@ {}l} |
543 @{thm swap_eqvt[where p="\<pi>", no_vars]} |
566 @{thm swap_eqvt[where p="\<pi>", no_vars]} |
550 of the permutation operation for booleans. It is also easy to see |
573 of the permutation operation for booleans. It is also easy to see |
551 that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text |
574 that the boolean operators, like @{text "\<and>"}, @{text "\<or>"}, @{text |
552 "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro) |
575 "\<not>"} and @{text "\<longrightarrow>"} are all equivariant (see ??? intro) |
553 |
576 |
554 In contrast, the advantage of Definition \ref{equivariance} is that |
577 In contrast, the advantage of Definition \ref{equivariance} is that |
555 it leads to a simple rewrite system. Consider the following oriented |
578 it leads to a simple rewrite system that allows us to `push' a |
556 versions |
579 permutation towards the leaves in a HOL-term (i.e.~constants and free |
|
580 variables). The permutation disappears in cases where the |
|
581 constants are equivariant. Given a database of equivariant constants, |
|
582 we can implement a decision procedure that helps to find out when |
|
583 a compound term is equivariant. A permutation @{text \<pi>} can be pushed over |
|
584 applications and abstractions in a HOL-term as follows |
|
585 |
|
586 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
587 \begin{tabular}{@ {}lrcl} |
|
588 i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\ |
|
589 ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> x])"}\\ |
|
590 \end{tabular}\hfill\numbered{rewriteapplam} |
|
591 \end{isabelle} |
|
592 |
|
593 \noindent |
|
594 The first rewrite rule we established as equation in \eqref{permutefunapp}; |
|
595 the second follows from the definition of permutations acting on functions |
|
596 and the fact that HOL-terms are considered equal modulo beta-reduction. |
|
597 The inverse permutations that are introduced by the second rewrite rule |
|
598 can be removed using the additional rewrite rule |
557 |
599 |
558 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
600 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
559 \begin{tabular}{@ {}rcl} |
601 \begin{tabular}{@ {}rcl} |
560 @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\\ |
602 @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"} |
561 @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := (-\<pi>) \<bullet> x])"}\\ |
603 \end{tabular}\hfill\numbered{rewriteunpermute} |
562 @{term "\<pi> \<bullet> (- \<pi>) \<bullet> x"} & @{text "\<longmapsto>"} & @{term "x"}\\ |
604 \end{isabelle} |
563 \end{tabular}\hfill\numbered{swapeqvt} |
605 |
564 \end{isabelle} |
606 \noindent |
565 |
607 and permutations in front of equivariant constants can be removed by the |
566 of the equations |
608 rule |
567 |
609 |
568 |
610 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
569 together with the permutation |
611 \begin{tabular}{@ {}rcl} |
|
612 @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"} |
|
613 \end{tabular}\hfill\numbered{rewriteconsts} |
|
614 \end{isabelle} |
|
615 |
|
616 |
|
617 \noindent |
|
618 By a meta-argument, that means one we cannot formalise inside |
|
619 Isabelle/HOL, we can convince ourselves that the rewriting process |
|
620 of first pushing a permutation inside a term using |
|
621 \eqref{rewriteapplam}, then removing permutation in front of bound |
|
622 variables using \eqref{rewriteunpermute} and finally removing all |
|
623 permutations in front of equivariant constants must terminate: the |
|
624 size of the term gets smaller in \eqref{rewriteapplam} if we do not |
|
625 count the inverse permutations introduced by the second rewrite rule |
|
626 and there can only be finitely many bound variables in a term |
|
627 (similarly equivariant constants), therefore only finitely many |
|
628 applications of \eqref{rewriteunpermute} and |
|
629 \eqref{rewriteconsts}. The only problem is that instances where |
|
630 rules (\ref{rewriteapplam}.{\it i}) or rules |
|
631 \eqref{rewriteunpermute} apply `overlap' and potentially our measure |
|
632 increases. Consider for example the term @{term "\<pi> \<bullet> (\<lambda>x. x)"}, |
|
633 whose final reduct should just be \mbox{@{term "\<lambda>x. x"}}. Using |
|
634 (\ref{rewriteapplam}.{\it ii}), the term can reduce to @{term |
|
635 "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"}, to which we can apply \eqref{rewriteunpermute} |
|
636 in order to obtain the desired result. However, the subterm term @{text "(- |
|
637 \<pi>) \<bullet> x"} is also an application (in fact three nested ones). Therefore |
|
638 @{term "\<lambda>x. \<pi> \<bullet> (- \<pi>) \<bullet> x"} can also rewrite |
|
639 to @{text "\<lambda>x. (- (\<pi> \<bullet> \<pi>)) \<bullet> (\<pi> \<bullet> x)"} to which we cannot apply |
|
640 (\ref{rewriteapplam}.{\it i}) directly and even worse our measure |
|
641 increased. In order to distinguish situations where \eqref{rewriteconsts} |
|
642 should apply instead of (\ref{rewriteapplam}.{\it i}) we use a standard |
|
643 trick in HOL. We introduce a separate definition for terms of the form |
|
644 @{text "(- \<pi>) \<bullet> x"}, namely as |
|
645 |
|
646 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
647 @{term "unpermute \<pi> x \<equiv> (- \<pi>) \<bullet> x"} |
|
648 \end{isabelle} |
|
649 |
|
650 \noindent |
|
651 With this trick, we can reformulate our rewrite rules pushing a permutation @{text \<pi>} |
|
652 inside a term as follows |
|
653 |
|
654 \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%% |
|
655 \begin{tabular}{@ {}lrcl} |
|
656 i) & @{text "\<pi> \<bullet> (t\<^isub>1 t\<^isub>2)"} & @{text "\<longmapsto>"} & @{term "(\<pi> \<bullet> t\<^isub>1) (\<pi> \<bullet> t\<^isub>2)"}\hspace{45mm}\mbox{}\\ |
|
657 \multicolumn{4}{r}{provided @{text "t\<^isub>1 t\<^isub>2"} is not of the form @{text "unpermute \<pi> x"}}\smallskip\\ |
|
658 ii) & @{text "\<pi> \<bullet> (\<lambda>x. t)"} & @{text "\<longmapsto>"} & @{text "\<lambda>x. \<pi> \<bullet> (t[x := unpermute \<pi> x])"}\\ |
|
659 iii) & @{text "\<pi> \<bullet> (unpermute \<pi> x)"} & @{text "\<longmapsto>"} & @{term x}\\ |
|
660 iv) & @{term "\<pi> \<bullet> c"} & @{text "\<longmapsto>"} & @{term "c"}\hspace{6mm}provided @{text c} is equivariant\\ |
|
661 \end{tabular} |
|
662 \end{isabelle} |
|
663 |
|
664 \noindent |
|
665 In this rewrite systems no rule overlaps. Taking the measure |
|
666 consisting of lexicographically ordered pairs whose first component |
|
667 is the size of the term (without counting @{text unpermutes}) and |
|
668 the second is the number of occurences of @{text "unpermute \<pi> x"} |
|
669 and @{text "\<pi> \<bullet> c"}, then each rule is strictly decreasing. |
|
670 Consequently the process of applying these rules must terminate. |
|
671 |
|
672 |
|
673 together with the permutation |
570 operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel} |
674 operation for functions and the properties in \eqref{permutefunapp} and \eqref{cancel} |
571 leads to a simple rewrite system that pushes permutations inside a term until they reach |
675 leads to a simple rewrite system that pushes permutations inside a term until they reach |
572 either function constants or variables. The permutations in front of |
676 either function constants or variables. The permutations in front of |
573 equivariant constants disappear. This helps us to establish equivariance |
677 equivariant constants disappear. This helps us to establish equivariance |
574 for any notion in HOL that is defined in terms of more primitive notions. To |
678 for any notion in HOL that is defined in terms of more primitive notions. To |