(*<*)
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
(*>*)