diff -r fb201e383f1b -r da575186d492 Nominal/Ex/Exec/Paper.thy
--- a/Nominal/Ex/Exec/Paper.thy	Tue Feb 19 05:38:46 2013 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,130 +0,0 @@
-(*<*)
-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
-(*>*)