1 (*<*)

     2 theory Paper imports Lambda_Exec begin

     3 

     4 notation (latex output)

     5       Name ("\<nu>_")

     6   and subst ("_ [_ := _]" [90, 90, 90] 90)

     7   and Lam ("\<^raw:$\lambda$>_. _" [50, 50] 50)

     8 (*  and atom ("_")*)

     9   and swap ("'(_ _')" [1000, 1000] 1000)

    10 (*and Umn ("\<^raw:$U^{\mbox{>_\<^raw:}}_{\mbox{>_\<^raw:}}$>" [205,205] 200)*)

    11   and all (binder "\<forall>" 10)

    12   and fresh ("_ \<FRESH> _" [55, 55] 55)

    13   and Set.empty ("\<emptyset>")

    14 

    15 declare [[show_question_marks = false]]

    16 (*>*)

    17 

    18 section {* Introduction *}

    19 

    20 section {* General Algorithm *}

    21 

    22 section {* Executing the Foundations of Nominal Logic *}

    23 

    24 subsection {* Executable Permutations *}

    25 

    26 text {*

    27 \begin{itemize}

    28 \item Definitions of permutation as a list: application of a permutation,

    29   validity of a permutation and equality of permutations

    30   @{thm [display, indent=5] perm_apply_def}

    31   @{thm [display, indent=5] valid_perm_def}

    32   @{thm [display, indent=5] perm_eq_def}

    33 \item Quotient type

    34   @{text [display, indent=5] "quotient_type 'a gperm = \"('a \<times> 'a) list\" / partial: \"perm_eq\""}

    35 \item Definitions of composing permutations and inverse permutation as well

    36   as showing that:

    37   @{text [display, indent=5] "instantiation gperm :: (type) group_add"}

    38 \item Proper representation and abstraction functions to make the @{text "code_abstype"}

    39   @{thm [display, indent=5] dest_perm_raw_def}

    40   @{thm [display, indent=5] mk_perm_raw_def}

    41 \item Code abstract equations of permutation composition, inverse, zero, swapping etc

    42 \end{itemize} *}

    43 

    44 subsection {* Sort-respecting Permutations *}

    45 

    46 text {*

    47 \begin{itemize}

    48 \item The type of sorted atoms

    49 \item Definition of sort-respecting

    50   @{thm [display, indent=5] sort_respecting_def}

    51 \item typedef and definitions of the basic operations

    52 \item showing that the sort-respecting ones are also a group\_add and that the

    53   code equations can be reused.

    54 \end{itemize}

    55 *}

    56 

    57 subsection {* Concrete atom types *}

    58 

    59 text {*

    60 \begin{itemize}

    61 \item bijection to natural numbers

    62   @{thm [display, indent=5] Name_def}

    63   @{thm [display, indent=5] nat_of_name_def}

    64 \item @{text "code_datatype"}

    65 \item equality of variables and a code equation for concrete variables

    66   @{thm [display, indent=5] equal_name_def}

    67   @{thm [display, indent=5] equal_name_code}

    68 \item code equations for @{term atom} and application of a permutation

    69   @{thm [display, indent=5] atom_name_code}

    70   @{thm [display, indent=5] permute_name_code}

    71 \end{itemize}

    72  *}

    73 

    74 section {* Executing the Lambda Terms *}

    75 

    76 text {*

    77 \begin{itemize}

    78 \item Defining a representation type: LN

    79 \item Abstraction with an accumulator

    80   @{thm [display, indent=5] ln_lam_aux.simps}

    81   @{thm [display, indent=5] ln_lam_def}

    82 \item Representation, with a helper

    83   @{thm [display, indent=5] subst_ln_nat.simps}

    84   @{thm [display, indent=5] lam_ln_ex.simps}

    85 \item A helper function \& proof that equal:

    86   @{thm [display, indent=5] lam_ln_aux.simps}

    87   @{thm [display, indent=5] lam_ln_def}

    88   @{thm [display, indent=5] lam_ln_ex}

    89 \item Code abstype

    90   @{thm [display, indent=5] ln_abstype}

    91 \item equality and permutations for the abstract type

    92   @{thm [display, indent=5] equal_lam_def}

    93   @{thm [display, indent=5] lam_ln_ex.eqvt[symmetric]}

    94 \end{itemize}

    95 *}

    96 

    97 subsection {* Executing substitution *}

    98 

    99 text {*

   100 \begin{itemize}

   101 \item Substitution on the representation:

   102   @{thm [display, indent=5] subst_ln.simps}

   103 \item equality of substitutions:

   104   @{thm [display, indent=5] subst_code}

   105 \end{itemize}

   106 

   107 Example of execution:

   108 

   109 @{text value} @{term "subst ((N0 \<leftrightarrow> N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))) N1 (Var N0)"}

   110 

   111 *}

   112 

   113 section {* Conclusion\label{sec:conclusion} *}

   114 

   115 subsection {* Future Work *}

   116 

   117 text {*

   118   Efficiency: Use more efficient representation for permutations than

   119   lists. Might be useful for bigger permutations, but for permuttaions

   120   of up to 3 elements does not make much sense *}

   121 

   122 subsection {* Related Work *}

   123 

   124 text {*

   125   Locally Nameless~\cite{LocallyNameless}

   126 *}

   127 

   128 (*<*)

   129 end

   130 (*>*)