(*<*)

theory Paper imports Lambda_Exec begin

notation (latex output)

      Name ("\<nu>_")

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

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

(*  and atom ("_")*)

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

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

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

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

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

declare [[show_question_marks = false]]

(*>*)

section {* Introduction *}

section {* General Algorithm *}

section {* Executing the Foundations of Nominal Logic *}

subsection {* Executable Permutations *}

text {*

\begin{itemize}

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

  validity of a permutation and equality of permutations

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

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

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

\item Quotient type

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

\item Definitions of composing permutations and inverse permutation as well

  as showing that:

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

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

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

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

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

\end{itemize} *}

subsection {* Sort-respecting Permutations *}

text {*

\begin{itemize}

\item The type of sorted atoms

\item Definition of sort-respecting

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

\item typedef and definitions of the basic operations

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

  code equations can be reused.

\end{itemize}

*}

subsection {* Concrete atom types *}

text {*

\begin{itemize}

\item bijection to natural numbers

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

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

\item @{text "code_datatype"}

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

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

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

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

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

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

\end{itemize}

 *}

section {* Executing the Lambda Terms *}

text {*

\begin{itemize}

\item Defining a representation type: LN

\item Abstraction with an accumulator

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

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

\item Representation, with a helper

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

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

\item A helper function \& proof that equal:

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

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

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

\item Code abstype

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

\item equality and permutations for the abstract type

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

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

\end{itemize}

*}

subsection {* Executing substitution *}

text {*

\begin{itemize}

\item Substitution on the representation:

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

\item equality of substitutions:

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

\end{itemize}

Example of execution:

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

*}

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

subsection {* Future Work *}

text {*

  Efficiency: Use more efficient representation for permutations than

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

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

subsection {* Related Work *}

text {*

  Locally Nameless~\cite{LocallyNameless}

*}

(*<*)

end

(*>*)