# HG changeset patch
# User Cezary Kaliszyk <cezarykaliszyk@gmail.com>
# Date 1337691358 -7200
# Node ID 9876d73adb2bd754d83c01fcb256e0d4ea4a8f18
# Parent  4cf3a4d367991307abc644189de15683abf2c53c
Executing Lambda Terms

diff -r 4cf3a4d36799 -r 9876d73adb2b .hgignore
--- a/.hgignore	Tue May 22 14:00:59 2012 +0200
+++ b/.hgignore	Tue May 22 14:55:58 2012 +0200
@@ -27,3 +27,10 @@
 Pearl/document.pdf
 pearl.pdf
 
+Nominal/Ex/SFT/generated
+Nominal/Ex/SFT/document.pdf
+sft-paper.pdf
+
+Nominal/Ex/Exec/generated
+Nominal/Ex/Exec/document.pdf
+exec-paper.pdf
diff -r 4cf3a4d36799 -r 9876d73adb2b IsaMakefile
--- a/IsaMakefile	Tue May 22 14:00:59 2012 +0200
+++ b/IsaMakefile	Tue May 22 14:55:58 2012 +0200
@@ -86,6 +86,26 @@
 	$(ISABELLE_TOOL) document -o pdf Quotient-Paper-jv/generated
 	@cp Quotient-Paper-jv/document.pdf qpaper-jv.pdf
 
+## SFT Paper
+
+sft-paper: $(LOG)/Nominal-SFT-Paper.gz
+
+$(LOG)/Nominal-SFT-Paper.gz: Nominal/Ex/SFT/ROOT.ML Nominal/Ex/SFT/document/root.* Nominal/Ex/SFT/*.thy
+	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/SFT
+	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/SFT/generated
+	@cp Nominal/Ex/SFT/document.pdf sft-paper.pdf
+
+
+## Exec Paper
+
+exec-paper: $(LOG)/Nominal-Exec-Paper.gz
+
+$(LOG)/Nominal-Exec-Paper.gz: Nominal/Ex/Exec/ROOT.ML Nominal/Ex/Exec/document/root.* Nominal/Ex/Exec/*.thy
+	@$(USEDIR) -f ROOT.ML -D generated Nominal2 Nominal/Ex/Exec
+	$(ISABELLE_TOOL) document -o pdf  Nominal/Ex/Exec/generated
+	@cp Nominal/Ex/Exec/document.pdf exec-paper.pdf
+
+
 ## Nominal Functions paper
 
 fnpaper: $(LOG)/HOL-FnPaper.gz
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/Lambda_Exec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/Lambda_Exec.thy	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,468 @@
+theory Lambda_Exec
+imports Name_Exec
+begin
+
+nominal_datatype lam =
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" l::"lam"  binds x in l ("Lam [_]. _" [100, 100] 100)
+
+nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_ [_ ::= _]" [90, 90, 90] 90)
+where
+  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
+| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])"
+proof auto
+  fix a b :: lam and aa :: name and P
+  assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P"
+    "\<And>t1 t2 y s. a = App t1 t2 \<and> aa = y \<and> b = s \<Longrightarrow> P"
+    "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = Lam [x]. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P"
+  then show "P"
+    by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
+       (blast, blast, simp add: fresh_star_def)
+next
+  fix x :: name and t and xa :: name and ya sa ta
+  assume *: "eqvt_at subst_sumC (t, ya, sa)"
+    "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)"
+    "[[atom x]]lst. t = [[atom xa]]lst. ta"
+  then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)"
+    apply -
+    apply (erule Abs_lst1_fcb)
+    apply(simp (no_asm) add: Abs_fresh_iff)
+    apply(drule_tac a="atom xa" in fresh_eqvt_at)
+    apply(simp add: finite_supp)
+    apply(simp_all add: fresh_Pair_elim Abs_fresh_iff Abs1_eq_iff)
+    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya")
+    apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa")
+    apply(simp add: atom_eqvt eqvt_at_def)
+    apply(rule perm_supp_eq, simp add: supp_swap fresh_star_def fresh_Pair)+
+    done
+next
+  show "eqvt subst_graph" unfolding eqvt_def subst_graph_def
+    by (rule, perm_simp, rule)
+qed
+
+termination (eqvt) by lexicographic_order
+
+datatype ln =
+  LNBnd nat
+| LNVar name
+| LNApp ln ln
+| LNLam ln
+
+instantiation ln :: pt begin
+fun
+  permute_ln
+where
+  "p \<bullet> LNBnd n = LNBnd (p \<bullet> n)"
+| "p \<bullet> LNVar v = LNVar (p \<bullet> v)"
+| "p \<bullet> LNApp d1 d2 = LNApp (p \<bullet> d1) (p \<bullet> d2)"
+| "p \<bullet> LNLam d = LNLam (p \<bullet> d)"
+instance
+  by (default, induct_tac [!] x) simp_all
+end
+
+lemmas [eqvt] = permute_ln.simps
+
+lemma ln_supports:
+  "supp (n) supports LNBnd n"
+  "supp (v) supports LNVar v"
+  "supp (za, z) supports LNApp z za"
+  "supp (z) supports LNLam z"
+  by (simp_all add: supports_def fresh_def[symmetric])
+     (perm_simp, simp add: swap_fresh_fresh fresh_Pair)+
+
+instance ln :: fs
+  apply default
+  apply (induct_tac x)
+  apply (rule supports_finite, rule ln_supports, simp add: finite_supp supp_Pair)+
+  done
+
+lemma ln_supp:
+  "supp (LNBnd n) = supp n"
+  "supp (LNVar name) = supp name"
+  "supp (LNApp ln1 ln2) = supp ln1 \<union> supp ln2"
+  "supp (LNLam ln) = supp ln"
+  unfolding supp_Pair[symmetric]
+  by (simp_all add: supp_def)
+
+lemma ln_fresh:
+  "x \<sharp> LNBnd n \<longleftrightarrow> True"
+  "x \<sharp> LNVar name \<longleftrightarrow> x \<sharp> name"
+  "x \<sharp> LNApp ln1 ln2 \<longleftrightarrow> x \<sharp> ln1 \<and> x \<sharp> ln2"
+  "x \<sharp> LNLam ln = x \<sharp> ln"
+  unfolding fresh_def
+  by (simp_all add: ln_supp pure_supp)
+
+fun
+  lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln"
+where
+  "lookup [] n x = LNVar x"
+| "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))"
+
+lemma supp_lookup:
+  shows "supp (lookup xs n x) \<subseteq> {atom x}"
+  by (induct arbitrary: n rule: lookup.induct)
+     (simp_all add: supp_at_base ln_supp pure_supp)
+
+lemma supp_lookup_in:
+  shows "x \<in> set xs \<Longrightarrow> supp (lookup xs n x) = {}"
+  by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln_supp pure_supp)
+
+lemma supp_lookup_notin:
+  shows "x \<notin> set xs \<Longrightarrow> supp (lookup xs n x) = {atom x}"
+  by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln_supp pure_supp supp_at_base)
+
+lemma supp_lookup_fresh:
+  shows "atom ` set xs \<sharp>* lookup xs n x"
+  by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin)
+
+lemma lookup_eqvt[eqvt]:
+  shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)"
+  by (induct xs arbitrary: n) (simp_all add: permute_pure)
+
+nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y")
+  lam_ln_aux :: "lam \<Rightarrow> name list \<Rightarrow> ln"
+where
+  "lam_ln_aux (Var x) xs = lookup xs 0 x"
+| "lam_ln_aux (App t1 t2) xs = LNApp (lam_ln_aux t1 xs) (lam_ln_aux t2 xs)"
+| "atom x \<sharp> xs \<Longrightarrow> lam_ln_aux (Lam [x]. t) xs = LNLam (lam_ln_aux t (x # xs))"
+  apply (simp add: eqvt_def lam_ln_aux_graph_def)
+  apply (rule, perm_simp, rule)
+  apply (erule lam_ln_aux_graph.induct)
+  apply (auto simp add: ln_supp)[3]
+  apply (simp add: supp_lookup_fresh)
+  apply (simp add: fresh_star_def ln_supp fresh_def)
+  apply (simp add: ln_supp fresh_def fresh_star_def)
+  apply (case_tac x)
+  apply (rule_tac y="a" and c="b" in lam.strong_exhaust)
+  apply (auto simp add: fresh_star_def)[3]
+  apply(simp_all)
+  apply(erule conjE)
+  apply (erule_tac c="xsa" in Abs_lst1_fcb2')
+  apply (simp_all add: fresh_star_def)[2]
+  apply (simp_all add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)
+  done
+
+termination (eqvt) by lexicographic_order
+
+definition lam_ln where "lam_ln t \<equiv> lam_ln_aux t []"
+
+fun nth_or_def where
+  "nth_or_def [] _ d = d"
+| "nth_or_def (h # t) 0 d = h"
+| "nth_or_def (h # t) (Suc n) d = nth_or_def t n d"
+
+lemma nth_or_def_eqvt [eqvt]:
+  "p \<bullet> (nth_or_def l n d) = nth_or_def (p \<bullet> l) (p \<bullet> n) (p \<bullet> d)"
+  apply (cases l)
+  apply auto
+  apply (induct n arbitrary: list)
+  apply (auto simp add: permute_pure)
+  apply (case_tac list)
+  apply simp_all
+  done
+
+nominal_primrec
+  ln_lam_aux :: "ln \<Rightarrow> name list \<Rightarrow> lam"
+where
+  "ln_lam_aux (LNBnd n) ns = (nth_or_def (map Var ns) n (Lam [x]. Var x))"
+| "ln_lam_aux (LNVar v) ns = Var v"
+| "ln_lam_aux (LNApp l1 l2) ns = App (ln_lam_aux l1 ns) (ln_lam_aux l2 ns)"
+| "atom x \<sharp> (ns, l) \<Longrightarrow> ln_lam_aux (LNLam l) ns = Lam [x]. (ln_lam_aux l (x # ns))"
+  apply (simp add: eqvt_def ln_lam_aux_graph_def)
+  apply (rule, perm_simp, rule)
+  apply rule
+  apply(auto)[1]
+  apply (rule_tac y="a" in ln.exhaust)
+  apply (auto simp add: fresh_star_def)[4]
+  using obtain_fresh apply metis
+  apply (auto simp add: fresh_Pair_elim)
+  apply (subgoal_tac "Lam [x]. Var x = Lam [xa]. Var xa")
+  apply (simp del: lam.eq_iff)
+  apply (simp add: Abs1_eq_iff lam.fresh fresh_at_base)
+  apply (simp add: Abs1_eq_iff)
+  apply (case_tac "x=xa")
+  apply simp_all
+  apply rule
+  apply (auto simp add: eqvt_at_def swap_fresh_fresh)[1]
+  apply (erule fresh_eqvt_at)
+  apply (simp add: supp_Pair finite_supp)
+  apply (simp add: fresh_Pair fresh_Cons fresh_at_base)
+  done
+
+termination (eqvt)
+  by lexicographic_order
+
+definition ln_lam where "ln_lam t \<equiv> ln_lam_aux t []"
+
+lemma l_fresh_lam_ln_aux: "atom ` set l \<sharp>* lam_ln_aux t l"
+  apply (nominal_induct t avoiding: l rule: lam.strong_induct)
+  apply (simp_all add: fresh_def ln_supp pure_supp)
+  apply (auto simp add: fresh_star_def)[1]
+  apply (case_tac "a = name")
+  apply (auto simp add: supp_lookup_in fresh_def)[1]
+  apply (simp add: fresh_def)
+  using supp_lookup
+  apply (metis (lifting) atom_eq_iff equals0D singletonE supp_lookup_in supp_lookup_notin)
+  apply (simp add: fresh_star_def fresh_def ln_supp)+
+  done
+
+lemma supp_lam_ln_aux: "supp (lam_ln_aux t l) \<subseteq> supp t"
+proof -
+  have "eqvt lam_ln_aux" unfolding eqvt_def using eqvts_raw by simp
+  then have "supp lam_ln_aux = {}" using supp_fun_eqvt by auto
+  then have "supp (lam_ln_aux t) \<subseteq> supp t" using supp_fun_app by auto
+  then have "supp (lam_ln_aux t l) \<subseteq> supp t \<union> supp l" using supp_fun_app by auto
+  moreover have "\<forall>x \<in> supp l. x \<notin> supp (lam_ln_aux t l)"
+    using l_fresh_lam_ln_aux unfolding fresh_star_def fresh_def
+    by (metis finite_set supp_finite_set_at_base supp_set)
+  ultimately show "supp (lam_ln_aux t l) \<subseteq> supp t" by blast
+qed
+
+lemma lookup_flip: "x \<noteq> y \<Longrightarrow> y \<noteq> a \<Longrightarrow> lookup ((x \<leftrightarrow> a) \<bullet> xs) n y = lookup xs n y"
+  apply (induct xs arbitrary: n)
+  apply simp
+  apply (simp only: Cons_eqvt)
+  apply (simp only: lookup.simps)
+  apply (subgoal_tac "y = (x \<leftrightarrow> a) \<bullet> aa \<longleftrightarrow> y = aa")
+  apply simp
+  by (metis permute_flip_at)
+
+lemma lookup_append_flip: "x \<noteq> y \<Longrightarrow> lookup (l @ a # (x \<leftrightarrow> a) \<bullet> xs) n y = lookup (l @ a # xs) n y"
+  by (induct l arbitrary: n) (auto simp add: lookup_flip)
+
+lemma lam_ln_aux_flip: "atom x \<sharp> t \<Longrightarrow> lam_ln_aux t (l @ a # (x \<leftrightarrow> a) \<bullet> xs) = lam_ln_aux t (l @ a # xs)"
+  apply (nominal_induct t avoiding: x a xs l rule: lam.strong_induct)
+  apply (simp_all add: lam_ln_aux.eqvt lam.fresh lookup_append_flip fresh_at_base)[2]
+  apply (simp add: lam.fresh fresh_at_base)
+  apply (subst lam_ln_aux.simps)
+  apply (simp add: fresh_Cons fresh_at_base fresh_append)
+  apply (metis atom_eqvt atom_name_def flip_at_base_simps(3) flip_commute fresh_permute_iff)
+  apply (subst lam_ln_aux.simps)
+  apply (simp add: fresh_Cons fresh_at_base fresh_append)
+  apply simp
+  apply (drule_tac x="x" in meta_spec)
+  apply (drule_tac x="a" in meta_spec)
+  apply (drule_tac x="xs" in meta_spec)
+  apply (drule_tac x="name # l" in meta_spec)
+  apply simp
+  done
+
+lemma lam_ln_aux4: "lam_ln_aux (Lam [x]. t) xs = LNLam (lam_ln_aux t (x # xs))"
+  apply (rule_tac 'a="name" and x="(xs, x, t)" in obtain_fresh)
+  apply (simp add: fresh_Pair_elim)
+  apply (rule_tac t="Lam [x]. t" and s="Lam [a]. ((x \<leftrightarrow> a) \<bullet> t)" in subst)
+  apply (auto simp add: Abs1_eq_iff lam.fresh flip_def swap_commute)[1]
+  apply simp
+  apply (rule_tac s="(x \<leftrightarrow> a) \<bullet> lam_ln_aux t (x # xs)" in trans)
+  apply (simp add: lam_ln_aux.eqvt)
+  apply (subst lam_ln_aux_flip[of _ _ "[]", simplified])
+  apply (metis atom_eqvt flip_at_simps(2) fresh_permute_iff)
+  apply rule
+  apply (rule flip_fresh_fresh)
+  apply (simp add: l_fresh_lam_ln_aux[of "x # xs", simplified fresh_star_def, simplified])
+  apply (simp add: fresh_def)
+  apply (metis set_rev_mp supp_lam_ln_aux)
+  done
+
+lemma lookup_in: "n \<notin> set l \<Longrightarrow> lookup l i n = LNVar n"
+  by (induct l arbitrary: i n) simp_all
+
+lemma lookup_in2: "n \<in> set l \<Longrightarrow> \<exists>i. lookup l j n = LNBnd i"
+  by (induct l arbitrary: j n) auto
+
+lemma lookup_in2': "lookup l j n = LNBnd i \<Longrightarrow> lookup l (Suc j) n = LNBnd (Suc i)"
+  by (induct l arbitrary: j n) auto
+
+lemma ln_lam_Var: "ln_lam_aux (lookup l (0\<Colon>nat) n) l = Var n"
+  apply (cases "n \<in> set l")
+  apply (simp_all add: lookup_in)
+  apply (induct l arbitrary: n)
+  apply simp
+  apply (case_tac "a = n")
+  apply (simp_all add: ln_lam_aux.simps(1)[of _ _ "Name 0"] )[2]
+  apply (drule_tac x="n" in meta_spec)
+  apply (frule lookup_in2[of _ _ 0])
+  apply (erule exE)
+  apply simp
+  apply (frule lookup_in2')
+  apply simp
+  apply (simp_all add: ln_lam_aux.simps(1)[of _ _ "Name 0"] )
+  done
+
+lemma ln_lam_ln_aux: "ln_lam_aux (lam_ln_aux t l) l = t"
+  apply (nominal_induct t avoiding: l rule: lam.strong_induct)
+  apply (simp_all add: ln_lam_Var)
+  apply (subst ln_lam_aux.simps(4)[of name])
+  apply (simp add: fresh_Pair)
+  apply (subgoal_tac "atom ` set (name # l) \<sharp>* lam_ln_aux lam (name # l)")
+  apply (simp add: fresh_star_def)
+  apply (rule l_fresh_lam_ln_aux)
+  apply simp
+  done
+
+fun subst_ln_nat where
+  "subst_ln_nat (LNBnd n) x _ = LNBnd n"
+| "subst_ln_nat (LNVar v) x n = (if x = v then LNBnd n else LNVar v)"
+| "subst_ln_nat (LNApp l r) x n = LNApp (subst_ln_nat l x n) (subst_ln_nat r x n)"
+| "subst_ln_nat (LNLam l) x n = LNLam (subst_ln_nat l x (n + 1))"
+
+lemma subst_ln_nat_eqvt[eqvt]:
+  shows "(p \<bullet> subst_ln_nat t x n) = subst_ln_nat (p \<bullet> t) (p \<bullet> x) (p \<bullet> n)"
+  by (induct t arbitrary: n) (simp_all add: permute_pure)
+
+lemma supp_subst_ln_nat:
+  "supp (subst_ln_nat t x n) = supp t - {atom x}"
+  by (induct t arbitrary: n) (auto simp add: permute_pure ln_supp pure_supp supp_at_base)
+
+lemma fresh_subst_ln_nat:
+  "atom y \<sharp> subst_ln_nat t x n \<longleftrightarrow> y = x \<or> atom y \<sharp> t"
+  unfolding fresh_def supp_subst_ln_nat by auto
+
+nominal_primrec
+  lam_ln_ex :: "lam \<Rightarrow> ln"
+where
+  "lam_ln_ex (Var x) = LNVar x"
+| "lam_ln_ex (App t1 t2) = LNApp (lam_ln_ex t1) (lam_ln_ex t2)"
+| "lam_ln_ex (Lam [x]. t) = LNLam (subst_ln_nat (lam_ln_ex t) x 0)"
+  apply (simp add: eqvt_def lam_ln_ex_graph_def)
+  apply (rule, perm_simp, rule)
+  apply rule
+  apply (rule_tac y="x" in lam.exhaust)
+  apply (auto simp add: fresh_star_def)[3]
+  apply(simp_all)
+  apply (erule_tac Abs_lst1_fcb)
+  apply (simp add: fresh_subst_ln_nat)
+  apply (simp add: fresh_subst_ln_nat)
+  apply (erule fresh_eqvt_at)
+  apply (simp add: finite_supp)
+  apply assumption
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq
+    subst_ln_nat_eqvt permute_pure)
+  apply simp
+  done
+
+termination (eqvt) by lexicographic_order
+
+lemma lookup_in3: "lookup l j n = LNBnd i \<Longrightarrow> lookup (l @ l2) j n = LNBnd i"
+  by (induct l arbitrary: j n) auto
+
+lemma lookup_in4: "n \<notin> set l \<Longrightarrow> lookup (l @ [n]) j n = LNBnd (length l + j)"
+  by (induct l arbitrary: j n) auto
+
+lemma subst_ln_nat_lam_ln_aux: "subst_ln_nat (lam_ln_aux l ns) n (List.length ns) = lam_ln_aux l (ns @ [n])"
+  apply (nominal_induct l avoiding: n ns rule: lam.strong_induct)
+  apply simp defer
+  apply simp
+  apply (simp add: fresh_Nil fresh_Cons fresh_append)
+  apply (drule_tac x="n" in meta_spec)
+  apply (drule_tac x="name # ns" in meta_spec)
+  apply simp
+  apply (case_tac "name \<in> set ns")
+  apply (simp_all add: lookup_in)
+  apply (frule lookup_in2[of _ _ 0])
+  apply (erule exE)
+  apply (simp add: lookup_in3)
+  apply (simp add: lookup_in4)
+  done
+
+lemma lam_ln_ex: "lam_ln_ex t = lam_ln t"
+  apply (induct t rule: lam.induct)
+  apply (simp_all add: lam_ln_def fresh_Nil)
+  by (metis (lifting) list.size(3) self_append_conv2 subst_ln_nat_lam_ln_aux)
+
+(* Lambda terms as a code-abstype *)
+lemma ln_abstype[code abstype]:
+  "ln_lam (lam_ln_ex t) = t"
+  by (simp add: ln_lam_def lam_ln_ex lam_ln_def ln_lam_ln_aux)
+
+lemmas [code abstract] = lam_ln_ex.simps
+
+(* Equality for lambda-terms *)
+instantiation lam :: equal begin
+
+definition equal_lam_def: "equal_lam a b \<longleftrightarrow> lam_ln_ex a = lam_ln_ex b"
+
+instance
+  by default
+    (metis equal_lam_def lam_ln_def lam_ln_ex ln_lam_ln_aux)
+
+end
+
+(* Execute permutations *)
+lemmas [code abstract] = lam_ln_ex.eqvt[symmetric]
+
+fun subst_ln where
+  "subst_ln (LNBnd n) _ _ = LNBnd n"
+| "subst_ln (LNVar v) x t = (if x = v then t else LNVar v)"
+| "subst_ln (LNApp l r) x t = LNApp (subst_ln l x t) (subst_ln r x t)"
+| "subst_ln (LNLam l) x t = LNLam (subst_ln l x t)"
+
+lemma subst_ln_nat_id[simp]:
+  "atom name \<sharp> s \<Longrightarrow> name \<noteq> y \<Longrightarrow> subst_ln_nat s name n = s"
+  by (induct s arbitrary: n) (simp_all add: ln_fresh fresh_at_base)
+
+lemma subst_ln_nat_subst_ln_commute:
+  assumes "name \<noteq> y" and "atom name \<sharp> s"
+  shows "subst_ln_nat (subst_ln ln y s) name n = subst_ln (subst_ln_nat ln name n) y s"
+  using assms by (induct ln arbitrary: n) auto
+
+lemma supp_lam_ln_ex: "supp (lam_ln_ex t) = supp t"
+  by (induct t rule: lam.induct) (simp_all add: lam.supp ln_supp supp_subst_ln_nat)
+
+lemma subst_code[code abstract]:
+  "lam_ln_ex (subst t y s) = subst_ln (lam_ln_ex t) y (lam_ln_ex s)"
+  apply (nominal_induct t avoiding: y s rule: lam.strong_induct)
+  apply simp_all
+  apply (subst subst_ln_nat_subst_ln_commute)
+  apply (simp_all add: fresh_at_base supp_lam_ln_ex fresh_def)
+  done
+
+(*definition "I0 \<equiv> Lam [N0]. (Var N0)"
+definition "I1 \<equiv> Lam [N1]. (Var N1)"
+definition "ppp = (atom N0 \<rightleftharpoons> atom N1)"
+definition "pp \<equiv> ppp \<bullet> I1 = I0"
+
+export_code pp in SML*)
+
+lemma subst_ln_nat_funpow[simp]:
+  "subst_ln_nat ((LNLam^^p) l) x n = (LNLam ^^ p) (subst_ln_nat l x (n + p))"
+  by (induct p arbitrary: n) simp_all
+
+(*
+
+Tests:
+
+fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam"
+where
+  "Umn 0 n = Lam [Name 0]. Var (Name n)"
+| "Umn (Suc m) n = Lam [Name (Suc m)]. Umn m n"
+
+lemma Umn_faster:
+  "lam_ln_ex (Umn m n) = (LNLam ^^ (Suc m)) (if n \<le> m then LNBnd n else LNVar (Name n))"
+  apply (induct m)
+  apply (auto simp add: Umn.simps)
+  apply (simp_all add: Name_def Abs_name_inject le_SucE)
+  apply (erule le_SucE)
+  apply simp_all
+  done
+
+definition "Bla = Umn 2 2"
+
+definition vara where "vara \<equiv> Lam [N0]. Lam [N1]. (App (Var N1) (App (Umn 2 2) (App (Var N0) (Var N1))))"
+
+export_code ln_lam_aux nth_or_def ln_lam subst vara in SML
+
+value "(atom N0 \<rightleftharpoons> atom N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))"
+value "subst ((N0 \<leftrightarrow> N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))) N1 (Var N0)"*)
+
+lemma [eqvt]:
+  "p \<bullet> Let x y = Let (p \<bullet> x) (p \<bullet> y)"
+  unfolding Let_def permute_fun_app_eq ..
+
+end
+
+
+
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/Name_Exec.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/Name_Exec.thy	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,56 @@
+theory Name_Exec
+imports "../../Nominal2"
+begin
+
+atom_decl name
+
+definition Name :: "nat \<Rightarrow> name" where "Name n = Abs_name (Atom (Sort ''Name_Exec.name'' []) n)"
+
+definition "nat_of_name n = nat_of (Rep_name n)"
+
+code_datatype Name
+
+definition [code]: "N0 = Name 0"
+definition [code]: "N1 = Name 1"
+definition [code]: "N2 = Name 2"
+
+instantiation name :: equal begin
+
+definition equal_name_def: "equal_name a b \<longleftrightarrow> nat_of_name a = nat_of_name b"
+
+instance
+  by default
+    (metis (lifting) Rep_name_inject atom_components_eq_iff atom_name_def equal_name_def nat_of_name_def sort_of_atom_eq)
+
+end
+
+lemma [simp]: "nat_of_name (Name n) = n"
+  unfolding nat_of_name_def Name_def
+  by (simp add: Abs_name_inverse)
+
+lemma equal_name_code [code]: "(equal_class.equal (Name x) (Name y)) \<longleftrightarrow> (x = y)"
+  by (auto simp add: equal_name_def)
+
+lemma atom_name_code[code]:
+  "atom (Name n) = Atom (Sort ''Name_Exec.name'' []) n"
+  by (simp add: Abs_name_inject[symmetric] Name_def)
+     (simp add: atom_name_def Rep_name_inverse)
+
+lemma permute_name_code[code]: "p \<bullet> n = Name (nat_of (p \<bullet> (atom n)))"
+  apply (simp add: atom_eqvt)
+  apply (simp add: atom_name_def Name_def)
+  by (metis Rep_name_inverse atom_name_def atom_name_sort nat_of.simps sort_of.simps atom.exhaust)
+
+(*
+Test:
+definition "t \<longleftrightarrow> 0 = (N0 \<leftrightarrow> N1)"
+
+export_code t in SML
+
+value "(N0 \<leftrightarrow> N1) + (N1 \<leftrightarrow> N0) = 0"
+*)
+
+end
+
+
+
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/Paper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/Paper.thy	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,130 @@
+(*<*)
+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
+(*>*)
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/ROOT.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/ROOT.ML	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,4 @@
+(* quick_and_dirty := true; *)
+no_document use_thys ["~~/src/HOL/Library/LaTeXsugar",
+                      "Name_Exec", "Lambda_Exec"];
+use_thys ["Paper"];
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/document/llncs.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/document/llncs.cls	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,1207 @@
+% LLNCS DOCUMENT CLASS -- version 2.17 (12-Jul-2010)
+% Springer Verlag LaTeX2e support for Lecture Notes in Computer Science
+%
+%%
+%% \CharacterTable
+%%  {Upper-case    \A\B\C\D\E\F\G\H\I\J\K\L\M\N\O\P\Q\R\S\T\U\V\W\X\Y\Z
+%%   Lower-case    \a\b\c\d\e\f\g\h\i\j\k\l\m\n\o\p\q\r\s\t\u\v\w\x\y\z
+%%   Digits        \0\1\2\3\4\5\6\7\8\9
+%%   Exclamation   \!     Double quote  \"     Hash (number) \#
+%%   Dollar        \$     Percent       \%     Ampersand     \&
+%%   Acute accent  \'     Left paren    \(     Right paren   \)
+%%   Asterisk      \*     Plus          \+     Comma         \,
+%%   Minus         \-     Point         \.     Solidus       \/
+%%   Colon         \:     Semicolon     \;     Less than     \<
+%%   Equals        \=     Greater than  \>     Question mark \?
+%%   Commercial at \@     Left bracket  \[     Backslash     \\
+%%   Right bracket \]     Circumflex    \^     Underscore    \_
+%%   Grave accent  \`     Left brace    \{     Vertical bar  \|
+%%   Right brace   \}     Tilde         \~}
+%%
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+\ProvidesClass{llncs}[2010/07/12 v2.17
+^^J LaTeX document class for Lecture Notes in Computer Science]
+% Options
+\let\if@envcntreset\iffalse
+\DeclareOption{envcountreset}{\let\if@envcntreset\iftrue}
+\DeclareOption{citeauthoryear}{\let\citeauthoryear=Y}
+\DeclareOption{oribibl}{\let\oribibl=Y}
+\let\if@custvec\iftrue
+\DeclareOption{orivec}{\let\if@custvec\iffalse}
+\let\if@envcntsame\iffalse
+\DeclareOption{envcountsame}{\let\if@envcntsame\iftrue}
+\let\if@envcntsect\iffalse
+\DeclareOption{envcountsect}{\let\if@envcntsect\iftrue}
+\let\if@runhead\iffalse
+\DeclareOption{runningheads}{\let\if@runhead\iftrue}
+
+\let\if@openright\iftrue
+\let\if@openbib\iffalse
+\DeclareOption{openbib}{\let\if@openbib\iftrue}
+
+% languages
+\let\switcht@@therlang\relax
+\def\ds@deutsch{\def\switcht@@therlang{\switcht@deutsch}}
+\def\ds@francais{\def\switcht@@therlang{\switcht@francais}}
+
+\DeclareOption*{\PassOptionsToClass{\CurrentOption}{article}}
+
+\ProcessOptions
+
+\LoadClass[twoside]{article}
+\RequirePackage{multicol} % needed for the list of participants, index
+\RequirePackage{aliascnt}
+
+\setlength{\textwidth}{12.2cm}
+\setlength{\textheight}{19.3cm}
+\renewcommand\@pnumwidth{2em}
+\renewcommand\@tocrmarg{3.5em}
+%
+\def\@dottedtocline#1#2#3#4#5{%
+  \ifnum #1>\c@tocdepth \else
+    \vskip \z@ \@plus.2\p@
+    {\leftskip #2\relax \rightskip \@tocrmarg \advance\rightskip by 0pt plus 2cm
+               \parfillskip -\rightskip \pretolerance=10000
+     \parindent #2\relax\@afterindenttrue
+     \interlinepenalty\@M
+     \leavevmode
+     \@tempdima #3\relax
+     \advance\leftskip \@tempdima \null\nobreak\hskip -\leftskip
+     {#4}\nobreak
+     \leaders\hbox{$\m@th
+        \mkern \@dotsep mu\hbox{.}\mkern \@dotsep
+        mu$}\hfill
+     \nobreak
+     \hb@xt@\@pnumwidth{\hfil\normalfont \normalcolor #5}%
+     \par}%
+  \fi}
+%
+\def\switcht@albion{%
+\def\abstractname{Abstract.}
+\def\ackname{Acknowledgement.}
+\def\andname{and}
+\def\lastandname{\unskip, and}
+\def\appendixname{Appendix}
+\def\chaptername{Chapter}
+\def\claimname{Claim}
+\def\conjecturename{Conjecture}
+\def\contentsname{Table of Contents}
+\def\corollaryname{Corollary}
+\def\definitionname{Definition}
+\def\examplename{Example}
+\def\exercisename{Exercise}
+\def\figurename{Fig.}
+\def\keywordname{{\bf Keywords:}}
+\def\indexname{Index}
+\def\lemmaname{Lemma}
+\def\contriblistname{List of Contributors}
+\def\listfigurename{List of Figures}
+\def\listtablename{List of Tables}
+\def\mailname{{\it Correspondence to\/}:}
+\def\noteaddname{Note added in proof}
+\def\notename{Note}
+\def\partname{Part}
+\def\problemname{Problem}
+\def\proofname{Proof}
+\def\propertyname{Property}
+\def\propositionname{Proposition}
+\def\questionname{Question}
+\def\remarkname{Remark}
+\def\seename{see}
+\def\solutionname{Solution}
+\def\subclassname{{\it Subject Classifications\/}:}
+\def\tablename{Table}
+\def\theoremname{Theorem}}
+\switcht@albion
+% Names of theorem like environments are already defined
+% but must be translated if another language is chosen
+%
+% French section
+\def\switcht@francais{%\typeout{On parle francais.}%
+ \def\abstractname{R\'esum\'e.}%
+ \def\ackname{Remerciements.}%
+ \def\andname{et}%
+ \def\lastandname{ et}%
+ \def\appendixname{Appendice}
+ \def\chaptername{Chapitre}%
+ \def\claimname{Pr\'etention}%
+ \def\conjecturename{Hypoth\`ese}%
+ \def\contentsname{Table des mati\`eres}%
+ \def\corollaryname{Corollaire}%
+ \def\definitionname{D\'efinition}%
+ \def\examplename{Exemple}%
+ \def\exercisename{Exercice}%
+ \def\figurename{Fig.}%
+ \def\keywordname{{\bf Mots-cl\'e:}}
+ \def\indexname{Index}
+ \def\lemmaname{Lemme}%
+ \def\contriblistname{Liste des contributeurs}
+ \def\listfigurename{Liste des figures}%
+ \def\listtablename{Liste des tables}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Note ajout\'ee \`a l'\'epreuve}%
+ \def\notename{Remarque}%
+ \def\partname{Partie}%
+ \def\problemname{Probl\`eme}%
+ \def\proofname{Preuve}%
+ \def\propertyname{Caract\'eristique}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Question}%
+ \def\remarkname{Remarque}%
+ \def\seename{voir}
+ \def\solutionname{Solution}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tableau}%
+ \def\theoremname{Th\'eor\`eme}%
+}
+%
+% German section
+\def\switcht@deutsch{%\typeout{Man spricht deutsch.}%
+ \def\abstractname{Zusammenfassung.}%
+ \def\ackname{Danksagung.}%
+ \def\andname{und}%
+ \def\lastandname{ und}%
+ \def\appendixname{Anhang}%
+ \def\chaptername{Kapitel}%
+ \def\claimname{Behauptung}%
+ \def\conjecturename{Hypothese}%
+ \def\contentsname{Inhaltsverzeichnis}%
+ \def\corollaryname{Korollar}%
+%\def\definitionname{Definition}%
+ \def\examplename{Beispiel}%
+ \def\exercisename{\"Ubung}%
+ \def\figurename{Abb.}%
+ \def\keywordname{{\bf Schl\"usselw\"orter:}}
+ \def\indexname{Index}
+%\def\lemmaname{Lemma}%
+ \def\contriblistname{Mitarbeiter}
+ \def\listfigurename{Abbildungsverzeichnis}%
+ \def\listtablename{Tabellenverzeichnis}%
+ \def\mailname{{\it Correspondence to\/}:}
+ \def\noteaddname{Nachtrag}%
+ \def\notename{Anmerkung}%
+ \def\partname{Teil}%
+%\def\problemname{Problem}%
+ \def\proofname{Beweis}%
+ \def\propertyname{Eigenschaft}%
+%\def\propositionname{Proposition}%
+ \def\questionname{Frage}%
+ \def\remarkname{Anmerkung}%
+ \def\seename{siehe}
+ \def\solutionname{L\"osung}%
+ \def\subclassname{{\it Subject Classifications\/}:}
+ \def\tablename{Tabelle}%
+%\def\theoremname{Theorem}%
+}
+
+% Ragged bottom for the actual page
+\def\thisbottomragged{\def\@textbottom{\vskip\z@ plus.0001fil
+\global\let\@textbottom\relax}}
+
+\renewcommand\small{%
+   \@setfontsize\small\@ixpt{11}%
+   \abovedisplayskip 8.5\p@ \@plus3\p@ \@minus4\p@
+   \abovedisplayshortskip \z@ \@plus2\p@
+   \belowdisplayshortskip 4\p@ \@plus2\p@ \@minus2\p@
+   \def\@listi{\leftmargin\leftmargini
+               \parsep 0\p@ \@plus1\p@ \@minus\p@
+               \topsep 8\p@ \@plus2\p@ \@minus4\p@
+               \itemsep0\p@}%
+   \belowdisplayskip \abovedisplayskip
+}
+
+\frenchspacing
+\widowpenalty=10000
+\clubpenalty=10000
+
+\setlength\oddsidemargin   {63\p@}
+\setlength\evensidemargin  {63\p@}
+\setlength\marginparwidth  {90\p@}
+
+\setlength\headsep   {16\p@}
+
+\setlength\footnotesep{7.7\p@}
+\setlength\textfloatsep{8mm\@plus 2\p@ \@minus 4\p@}
+\setlength\intextsep   {8mm\@plus 2\p@ \@minus 2\p@}
+
+\setcounter{secnumdepth}{2}
+
+\newcounter {chapter}
+\renewcommand\thechapter      {\@arabic\c@chapter}
+
+\newif\if@mainmatter \@mainmattertrue
+\newcommand\frontmatter{\cleardoublepage
+            \@mainmatterfalse\pagenumbering{Roman}}
+\newcommand\mainmatter{\cleardoublepage
+       \@mainmattertrue\pagenumbering{arabic}}
+\newcommand\backmatter{\if@openright\cleardoublepage\else\clearpage\fi
+      \@mainmatterfalse}
+
+\renewcommand\part{\cleardoublepage
+                 \thispagestyle{empty}%
+                 \if@twocolumn
+                     \onecolumn
+                     \@tempswatrue
+                   \else
+                     \@tempswafalse
+                 \fi
+                 \null\vfil
+                 \secdef\@part\@spart}
+
+\def\@part[#1]#2{%
+    \ifnum \c@secnumdepth >-2\relax
+      \refstepcounter{part}%
+      \addcontentsline{toc}{part}{\thepart\hspace{1em}#1}%
+    \else
+      \addcontentsline{toc}{part}{#1}%
+    \fi
+    \markboth{}{}%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \ifnum \c@secnumdepth >-2\relax
+       \huge\bfseries \partname~\thepart
+       \par
+       \vskip 20\p@
+     \fi
+     \Huge \bfseries #2\par}%
+    \@endpart}
+\def\@spart#1{%
+    {\centering
+     \interlinepenalty \@M
+     \normalfont
+     \Huge \bfseries #1\par}%
+    \@endpart}
+\def\@endpart{\vfil\newpage
+              \if@twoside
+                \null
+                \thispagestyle{empty}%
+                \newpage
+              \fi
+              \if@tempswa
+                \twocolumn
+              \fi}
+
+\newcommand\chapter{\clearpage
+                    \thispagestyle{empty}%
+                    \global\@topnum\z@
+                    \@afterindentfalse
+                    \secdef\@chapter\@schapter}
+\def\@chapter[#1]#2{\ifnum \c@secnumdepth >\m@ne
+                       \if@mainmatter
+                         \refstepcounter{chapter}%
+                         \typeout{\@chapapp\space\thechapter.}%
+                         \addcontentsline{toc}{chapter}%
+                                  {\protect\numberline{\thechapter}#1}%
+                       \else
+                         \addcontentsline{toc}{chapter}{#1}%
+                       \fi
+                    \else
+                      \addcontentsline{toc}{chapter}{#1}%
+                    \fi
+                    \chaptermark{#1}%
+                    \addtocontents{lof}{\protect\addvspace{10\p@}}%
+                    \addtocontents{lot}{\protect\addvspace{10\p@}}%
+                    \if@twocolumn
+                      \@topnewpage[\@makechapterhead{#2}]%
+                    \else
+                      \@makechapterhead{#2}%
+                      \@afterheading
+                    \fi}
+\def\@makechapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \ifnum \c@secnumdepth >\m@ne
+      \if@mainmatter
+        \large\bfseries \@chapapp{} \thechapter
+        \par\nobreak
+        \vskip 20\p@
+      \fi
+    \fi
+    \interlinepenalty\@M
+    \Large \bfseries #1\par\nobreak
+    \vskip 40\p@
+  }}
+\def\@schapter#1{\if@twocolumn
+                   \@topnewpage[\@makeschapterhead{#1}]%
+                 \else
+                   \@makeschapterhead{#1}%
+                   \@afterheading
+                 \fi}
+\def\@makeschapterhead#1{%
+% \vspace*{50\p@}%
+  {\centering
+    \normalfont
+    \interlinepenalty\@M
+    \Large \bfseries  #1\par\nobreak
+    \vskip 40\p@
+  }}
+
+\renewcommand\section{\@startsection{section}{1}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {12\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\large\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {8\p@ \@plus 4\p@ \@minus 4\p@}%
+                       {\normalfont\normalsize\bfseries\boldmath
+                        \rightskip=\z@ \@plus 8em\pretolerance=10000 }}
+\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
+                       {-18\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\bfseries\boldmath}}
+\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
+                       {-12\p@ \@plus -4\p@ \@minus -4\p@}%
+                       {-0.5em \@plus -0.22em \@minus -0.1em}%
+                       {\normalfont\normalsize\itshape}}
+\renewcommand\subparagraph[1]{\typeout{LLNCS warning: You should not use
+                  \string\subparagraph\space with this class}\vskip0.5cm
+You should not use \verb|\subparagraph| with this class.\vskip0.5cm}
+
+\DeclareMathSymbol{\Gamma}{\mathalpha}{letters}{"00}
+\DeclareMathSymbol{\Delta}{\mathalpha}{letters}{"01}
+\DeclareMathSymbol{\Theta}{\mathalpha}{letters}{"02}
+\DeclareMathSymbol{\Lambda}{\mathalpha}{letters}{"03}
+\DeclareMathSymbol{\Xi}{\mathalpha}{letters}{"04}
+\DeclareMathSymbol{\Pi}{\mathalpha}{letters}{"05}
+\DeclareMathSymbol{\Sigma}{\mathalpha}{letters}{"06}
+\DeclareMathSymbol{\Upsilon}{\mathalpha}{letters}{"07}
+\DeclareMathSymbol{\Phi}{\mathalpha}{letters}{"08}
+\DeclareMathSymbol{\Psi}{\mathalpha}{letters}{"09}
+\DeclareMathSymbol{\Omega}{\mathalpha}{letters}{"0A}
+
+\let\footnotesize\small
+
+\if@custvec
+\def\vec#1{\mathchoice{\mbox{\boldmath$\displaystyle#1$}}
+{\mbox{\boldmath$\textstyle#1$}}
+{\mbox{\boldmath$\scriptstyle#1$}}
+{\mbox{\boldmath$\scriptscriptstyle#1$}}}
+\fi
+
+\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
+\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
+\penalty50\hskip1em\null\nobreak\hfil\squareforqed
+\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
+
+\def\getsto{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr\gets\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr\gets
+\cr\to\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+\gets\cr\to\cr}}}}}
+\def\lid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr<\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr<\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr<\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+<\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\gid{\mathrel{\mathchoice {\vcenter{\offinterlineskip\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr>\cr
+\noalign{\vskip1.2pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr>\cr
+\noalign{\vskip1pt}=\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr
+\noalign{\vskip0.9pt}=\cr}}}}}
+\def\grole{\mathrel{\mathchoice {\vcenter{\offinterlineskip
+\halign{\hfil
+$\displaystyle##$\hfil\cr>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\textstyle##$\hfil\cr
+>\cr\noalign{\vskip-1pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.8pt}<\cr}}}
+{\vcenter{\offinterlineskip\halign{\hfil$\scriptscriptstyle##$\hfil\cr
+>\cr\noalign{\vskip-0.3pt}<\cr}}}}}
+\def\bbbr{{\rm I\!R}} %reelle Zahlen
+\def\bbbm{{\rm I\!M}}
+\def\bbbn{{\rm I\!N}} %natuerliche Zahlen
+\def\bbbf{{\rm I\!F}}
+\def\bbbh{{\rm I\!H}}
+\def\bbbk{{\rm I\!K}}
+\def\bbbp{{\rm I\!P}}
+\def\bbbone{{\mathchoice {\rm 1\mskip-4mu l} {\rm 1\mskip-4mu l}
+{\rm 1\mskip-4.5mu l} {\rm 1\mskip-5mu l}}}
+\def\bbbc{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm C$}\hbox{\hbox
+to0pt{\kern0.4\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbq{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.8\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm Q$}\hbox{\raise
+0.15\ht0\hbox to0pt{\kern0.4\wd0\vrule height0.7\ht0\hss}\box0}}}}
+\def\bbbt{{\mathchoice {\setbox0=\hbox{$\displaystyle\rm
+T$}\hbox{\hbox to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm T$}\hbox{\hbox
+to0pt{\kern0.3\wd0\vrule height0.9\ht0\hss}\box0}}}}
+\def\bbbs{{\mathchoice
+{\setbox0=\hbox{$\displaystyle     \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\textstyle        \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\hbox
+to0pt{\kern0.55\wd0\vrule height0.5\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptstyle      \rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.35\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.5\wd0\vrule height0.45\ht0\hss}\box0}}
+{\setbox0=\hbox{$\scriptscriptstyle\rm S$}\hbox{\raise0.5\ht0\hbox
+to0pt{\kern0.4\wd0\vrule height0.45\ht0\hss}\raise0.05\ht0\hbox
+to0pt{\kern0.55\wd0\vrule height0.45\ht0\hss}\box0}}}}
+\def\bbbz{{\mathchoice {\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\textstyle Z\kern-0.4em Z$}}
+{\hbox{$\mathsf\scriptstyle Z\kern-0.3em Z$}}
+{\hbox{$\mathsf\scriptscriptstyle Z\kern-0.2em Z$}}}}
+
+\let\ts\,
+
+\setlength\leftmargini  {17\p@}
+\setlength\leftmargin    {\leftmargini}
+\setlength\leftmarginii  {\leftmargini}
+\setlength\leftmarginiii {\leftmargini}
+\setlength\leftmarginiv  {\leftmargini}
+\setlength  \labelsep  {.5em}
+\setlength  \labelwidth{\leftmargini}
+\addtolength\labelwidth{-\labelsep}
+
+\def\@listI{\leftmargin\leftmargini
+            \parsep 0\p@ \@plus1\p@ \@minus\p@
+            \topsep 8\p@ \@plus2\p@ \@minus4\p@
+            \itemsep0\p@}
+\let\@listi\@listI
+\@listi
+\def\@listii {\leftmargin\leftmarginii
+              \labelwidth\leftmarginii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus2\p@ \@minus\p@}
+\def\@listiii{\leftmargin\leftmarginiii
+              \labelwidth\leftmarginiii
+              \advance\labelwidth-\labelsep
+              \topsep    0\p@ \@plus\p@\@minus\p@
+              \parsep    \z@
+              \partopsep \p@ \@plus\z@ \@minus\p@}
+
+\renewcommand\labelitemi{\normalfont\bfseries --}
+\renewcommand\labelitemii{$\m@th\bullet$}
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\def\tableofcontents{\chapter*{\contentsname\@mkboth{{\contentsname}}%
+                                                    {{\contentsname}}}
+ \def\authcount##1{\setcounter{auco}{##1}\setcounter{@auth}{1}}
+ \def\lastand{\ifnum\value{auco}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{auco}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \@starttoc{toc}\if@restonecol\twocolumn\fi}
+
+\def\l@part#1#2{\addpenalty{\@secpenalty}%
+   \addvspace{2em plus\p@}%  % space above part line
+   \begingroup
+     \parindent \z@
+     \rightskip \z@ plus 5em
+     \hrule\vskip5pt
+     \large               % same size as for a contribution heading
+     \bfseries\boldmath   % set line in boldface
+     \leavevmode          % TeX command to enter horizontal mode.
+     #1\par
+     \vskip5pt
+     \hrule
+     \vskip1pt
+     \nobreak             % Never break after part entry
+   \endgroup}
+
+\def\@dotsep{2}
+
+\let\phantomsection=\relax
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{}\fi}
+
+\def\addnumcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{\protect\numberline
+                     {\thechapter}#3}{\thepage}\hyperhrefextend}}%
+\def\addcontentsmark#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{\thepage}\hyperhrefextend}}%
+\def\addcontentsmarkwop#1#2#3{%
+\addtocontents{#1}{\protect\contentsline{#2}{#3}{0}\hyperhrefextend}}%
+
+\def\@adcmk[#1]{\ifcase #1 \or
+\def\@gtempa{\addnumcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmark}%
+  \or    \def\@gtempa{\addcontentsmarkwop}%
+  \fi\@gtempa{toc}{chapter}%
+}
+\def\addtocmark{%
+\phantomsection
+\@ifnextchar[{\@adcmk}{\@adcmk[3]}%
+}
+
+\def\l@chapter#1#2{\addpenalty{-\@highpenalty}
+ \vskip 1.0em plus 1pt \@tempdima 1.5em \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ {\large\bfseries\boldmath#1}\ifx0#2\hfil\null
+ \else
+      \nobreak
+      \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+      \@dotsep mu$}\hfill
+      \nobreak\hbox to\@pnumwidth{\hss #2}%
+ \fi\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@title#1#2{\addpenalty{-\@highpenalty}
+ \addvspace{8pt plus 1pt}
+ \@tempdima \z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \parfillskip -\rightskip \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima \hskip -\leftskip
+ #1\nobreak
+ \leaders\hbox{$\m@th \mkern \@dotsep mu.\mkern
+ \@dotsep mu$}\hfill
+ \nobreak\hbox to\@pnumwidth{\hss #2}\par
+ \penalty\@highpenalty \endgroup}
+
+\def\l@author#1#2{\addpenalty{\@highpenalty}
+ \@tempdima=15\p@ %\z@
+ \begingroup
+ \parindent \z@ \rightskip \@tocrmarg
+ \advance\rightskip by 0pt plus 2cm
+ \pretolerance=10000
+ \leavevmode \advance\leftskip\@tempdima %\hskip -\leftskip
+ \textit{#1}\par
+ \penalty\@highpenalty \endgroup}
+
+\setcounter{tocdepth}{0}
+\newdimen\tocchpnum
+\newdimen\tocsecnum
+\newdimen\tocsectotal
+\newdimen\tocsubsecnum
+\newdimen\tocsubsectotal
+\newdimen\tocsubsubsecnum
+\newdimen\tocsubsubsectotal
+\newdimen\tocparanum
+\newdimen\tocparatotal
+\newdimen\tocsubparanum
+\tocchpnum=\z@            % no chapter numbers
+\tocsecnum=15\p@          % section 88. plus 2.222pt
+\tocsubsecnum=23\p@       % subsection 88.8 plus 2.222pt
+\tocsubsubsecnum=27\p@    % subsubsection 88.8.8 plus 1.444pt
+\tocparanum=35\p@         % paragraph 88.8.8.8 plus 1.666pt
+\tocsubparanum=43\p@      % subparagraph 88.8.8.8.8 plus 1.888pt
+\def\calctocindent{%
+\tocsectotal=\tocchpnum
+\advance\tocsectotal by\tocsecnum
+\tocsubsectotal=\tocsectotal
+\advance\tocsubsectotal by\tocsubsecnum
+\tocsubsubsectotal=\tocsubsectotal
+\advance\tocsubsubsectotal by\tocsubsubsecnum
+\tocparatotal=\tocsubsubsectotal
+\advance\tocparatotal by\tocparanum}
+\calctocindent
+
+\def\l@section{\@dottedtocline{1}{\tocchpnum}{\tocsecnum}}
+\def\l@subsection{\@dottedtocline{2}{\tocsectotal}{\tocsubsecnum}}
+\def\l@subsubsection{\@dottedtocline{3}{\tocsubsectotal}{\tocsubsubsecnum}}
+\def\l@paragraph{\@dottedtocline{4}{\tocsubsubsectotal}{\tocparanum}}
+\def\l@subparagraph{\@dottedtocline{5}{\tocparatotal}{\tocsubparanum}}
+
+\def\listoffigures{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listfigurename\@mkboth{{\listfigurename}}{{\listfigurename}}}
+ \@starttoc{lof}\if@restonecol\twocolumn\fi}
+\def\l@figure{\@dottedtocline{1}{0em}{1.5em}}
+
+\def\listoftables{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
+ \fi\section*{\listtablename\@mkboth{{\listtablename}}{{\listtablename}}}
+ \@starttoc{lot}\if@restonecol\twocolumn\fi}
+\let\l@table\l@figure
+
+\renewcommand\listoffigures{%
+    \section*{\listfigurename
+      \@mkboth{\listfigurename}{\listfigurename}}%
+    \@starttoc{lof}%
+    }
+
+\renewcommand\listoftables{%
+    \section*{\listtablename
+      \@mkboth{\listtablename}{\listtablename}}%
+    \@starttoc{lot}%
+    }
+
+\ifx\oribibl\undefined
+\ifx\citeauthoryear\undefined
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \def\@biblabel##1{##1.}
+      \small
+      \list{\@biblabel{\@arabic\c@enumiv}}%
+           {\settowidth\labelwidth{\@biblabel{#1}}%
+            \leftmargin\labelwidth
+            \advance\leftmargin\labelsep
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{\@arabic\c@enumiv}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+\def\@lbibitem[#1]#2{\item[{[#1]}\hfill]\if@filesw
+     {\let\protect\noexpand\immediate
+     \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+\newcount\@tempcntc
+\def\@citex[#1]#2{\if@filesw\immediate\write\@auxout{\string\citation{#2}}\fi
+  \@tempcnta\z@\@tempcntb\m@ne\def\@citea{}\@cite{\@for\@citeb:=#2\do
+    {\@ifundefined
+       {b@\@citeb}{\@citeo\@tempcntb\m@ne\@citea\def\@citea{,}{\bfseries
+        ?}\@warning
+       {Citation `\@citeb' on page \thepage \space undefined}}%
+    {\setbox\z@\hbox{\global\@tempcntc0\csname b@\@citeb\endcsname\relax}%
+     \ifnum\@tempcntc=\z@ \@citeo\@tempcntb\m@ne
+       \@citea\def\@citea{,}\hbox{\csname b@\@citeb\endcsname}%
+     \else
+      \advance\@tempcntb\@ne
+      \ifnum\@tempcntb=\@tempcntc
+      \else\advance\@tempcntb\m@ne\@citeo
+      \@tempcnta\@tempcntc\@tempcntb\@tempcntc\fi\fi}}\@citeo}{#1}}
+\def\@citeo{\ifnum\@tempcnta>\@tempcntb\else
+               \@citea\def\@citea{,\,\hskip\z@skip}%
+               \ifnum\@tempcnta=\@tempcntb\the\@tempcnta\else
+               {\advance\@tempcnta\@ne\ifnum\@tempcnta=\@tempcntb \else
+                \def\@citea{--}\fi
+      \advance\@tempcnta\m@ne\the\@tempcnta\@citea\the\@tempcntb}\fi\fi}
+\else
+\renewenvironment{thebibliography}[1]
+     {\section*{\refname}
+      \small
+      \list{}%
+           {\settowidth\labelwidth{}%
+            \leftmargin\parindent
+            \itemindent=-\parindent
+            \labelsep=\z@
+            \if@openbib
+              \advance\leftmargin\bibindent
+              \itemindent -\bibindent
+              \listparindent \itemindent
+              \parsep \z@
+            \fi
+            \usecounter{enumiv}%
+            \let\p@enumiv\@empty
+            \renewcommand\theenumiv{}}%
+      \if@openbib
+        \renewcommand\newblock{\par}%
+      \else
+        \renewcommand\newblock{\hskip .11em \@plus.33em \@minus.07em}%
+      \fi
+      \sloppy\clubpenalty4000\widowpenalty4000%
+      \sfcode`\.=\@m}
+     {\def\@noitemerr
+       {\@latex@warning{Empty `thebibliography' environment}}%
+      \endlist}
+      \def\@cite#1{#1}%
+      \def\@lbibitem[#1]#2{\item[]\if@filesw
+        {\def\protect##1{\string ##1\space}\immediate
+      \write\@auxout{\string\bibcite{#2}{#1}}}\fi\ignorespaces}
+   \fi
+\else
+\@cons\@openbib@code{\noexpand\small}
+\fi
+
+\def\idxquad{\hskip 10\p@}% space that divides entry from number
+
+\def\@idxitem{\par\hangindent 10\p@}
+
+\def\subitem{\par\setbox0=\hbox{--\enspace}% second order
+                \noindent\hangindent\wd0\box0}% index entry
+
+\def\subsubitem{\par\setbox0=\hbox{--\,--\enspace}% third
+                \noindent\hangindent\wd0\box0}% order index entry
+
+\def\indexspace{\par \vskip 10\p@ plus5\p@ minus3\p@\relax}
+
+\renewenvironment{theindex}
+               {\@mkboth{\indexname}{\indexname}%
+                \thispagestyle{empty}\parindent\z@
+                \parskip\z@ \@plus .3\p@\relax
+                \let\item\par
+                \def\,{\relax\ifmmode\mskip\thinmuskip
+                             \else\hskip0.2em\ignorespaces\fi}%
+                \normalfont\small
+                \begin{multicols}{2}[\@makeschapterhead{\indexname}]%
+                }
+                {\end{multicols}}
+
+\renewcommand\footnoterule{%
+  \kern-3\p@
+  \hrule\@width 2truecm
+  \kern2.6\p@}
+  \newdimen\fnindent
+  \fnindent1em
+\long\def\@makefntext#1{%
+    \parindent \fnindent%
+    \leftskip \fnindent%
+    \noindent
+    \llap{\hb@xt@1em{\hss\@makefnmark\ }}\ignorespaces#1}
+
+\long\def\@makecaption#1#2{%
+  \small
+  \vskip\abovecaptionskip
+  \sbox\@tempboxa{{\bfseries #1.} #2}%
+  \ifdim \wd\@tempboxa >\hsize
+    {\bfseries #1.} #2\par
+  \else
+    \global \@minipagefalse
+    \hb@xt@\hsize{\hfil\box\@tempboxa\hfil}%
+  \fi
+  \vskip\belowcaptionskip}
+
+\def\fps@figure{htbp}
+\def\fnum@figure{\figurename\thinspace\thefigure}
+\def \@floatboxreset {%
+        \reset@font
+        \small
+        \@setnobreak
+        \@setminipage
+}
+\def\fps@table{htbp}
+\def\fnum@table{\tablename~\thetable}
+\renewenvironment{table}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@float{table}}
+               {\end@float}
+\renewenvironment{table*}
+               {\setlength\abovecaptionskip{0\p@}%
+                \setlength\belowcaptionskip{10\p@}%
+                \@dblfloat{table}}
+               {\end@dblfloat}
+
+\long\def\@caption#1[#2]#3{\par\addcontentsline{\csname
+  ext@#1\endcsname}{#1}{\protect\numberline{\csname
+  the#1\endcsname}{\ignorespaces #2}}\begingroup
+    \@parboxrestore
+    \@makecaption{\csname fnum@#1\endcsname}{\ignorespaces #3}\par
+  \endgroup}
+
+% LaTeX does not provide a command to enter the authors institute
+% addresses. The \institute command is defined here.
+
+\newcounter{@inst}
+\newcounter{@auth}
+\newcounter{auco}
+\newdimen\instindent
+\newbox\authrun
+\newtoks\authorrunning
+\newtoks\tocauthor
+\newbox\titrun
+\newtoks\titlerunning
+\newtoks\toctitle
+
+\def\clearheadinfo{\gdef\@author{No Author Given}%
+                   \gdef\@title{No Title Given}%
+                   \gdef\@subtitle{}%
+                   \gdef\@institute{No Institute Given}%
+                   \gdef\@thanks{}%
+                   \global\titlerunning={}\global\authorrunning={}%
+                   \global\toctitle={}\global\tocauthor={}}
+
+\def\institute#1{\gdef\@institute{#1}}
+
+\def\institutename{\par
+ \begingroup
+ \parskip=\z@
+ \parindent=\z@
+ \setcounter{@inst}{1}%
+ \def\and{\par\stepcounter{@inst}%
+ \noindent$^{\the@inst}$\enspace\ignorespaces}%
+ \setbox0=\vbox{\def\thanks##1{}\@institute}%
+ \ifnum\c@@inst=1\relax
+   \gdef\fnnstart{0}%
+ \else
+   \xdef\fnnstart{\c@@inst}%
+   \setcounter{@inst}{1}%
+   \noindent$^{\the@inst}$\enspace
+ \fi
+ \ignorespaces
+ \@institute\par
+ \endgroup}
+
+\def\@fnsymbol#1{\ensuremath{\ifcase#1\or\star\or{\star\star}\or
+   {\star\star\star}\or \dagger\or \ddagger\or
+   \mathchar "278\or \mathchar "27B\or \|\or **\or \dagger\dagger
+   \or \ddagger\ddagger \else\@ctrerr\fi}}
+
+\def\inst#1{\unskip$^{#1}$}
+\def\fnmsep{\unskip$^,$}
+\def\email#1{{\tt#1}}
+\AtBeginDocument{\@ifundefined{url}{\def\url#1{#1}}{}%
+\@ifpackageloaded{babel}{%
+\@ifundefined{extrasenglish}{}{\addto\extrasenglish{\switcht@albion}}%
+\@ifundefined{extrasfrenchb}{}{\addto\extrasfrenchb{\switcht@francais}}%
+\@ifundefined{extrasgerman}{}{\addto\extrasgerman{\switcht@deutsch}}%
+}{\switcht@@therlang}%
+\providecommand{\keywords}[1]{\par\addvspace\baselineskip
+\noindent\keywordname\enspace\ignorespaces#1}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+%
+%%% to avoid hyperref warnings
+\providecommand*{\toclevel@author}{999}
+%%% to make title-entry parent of section-entries
+\providecommand*{\toclevel@title}{0}
+%
+\renewcommand\maketitle{\newpage
+\phantomsection
+  \refstepcounter{chapter}%
+  \stepcounter{section}%
+  \setcounter{section}{0}%
+  \setcounter{subsection}{0}%
+  \setcounter{figure}{0}
+  \setcounter{table}{0}
+  \setcounter{equation}{0}
+  \setcounter{footnote}{0}%
+  \begingroup
+    \parindent=\z@
+    \renewcommand\thefootnote{\@fnsymbol\c@footnote}%
+    \if@twocolumn
+      \ifnum \col@number=\@ne
+        \@maketitle
+      \else
+        \twocolumn[\@maketitle]%
+      \fi
+    \else
+      \newpage
+      \global\@topnum\z@   % Prevents figures from going at top of page.
+      \@maketitle
+    \fi
+    \thispagestyle{empty}\@thanks
+%
+    \def\\{\unskip\ \ignorespaces}\def\inst##1{\unskip{}}%
+    \def\thanks##1{\unskip{}}\def\fnmsep{\unskip}%
+    \instindent=\hsize
+    \advance\instindent by-\headlineindent
+    \if!\the\toctitle!\addcontentsline{toc}{title}{\@title}\else
+       \addcontentsline{toc}{title}{\the\toctitle}\fi
+    \if@runhead
+       \if!\the\titlerunning!\else
+         \edef\@title{\the\titlerunning}%
+       \fi
+       \global\setbox\titrun=\hbox{\small\rm\unboldmath\ignorespaces\@title}%
+       \ifdim\wd\titrun>\instindent
+          \typeout{Title too long for running head. Please supply}%
+          \typeout{a shorter form with \string\titlerunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\titrun=\hbox{\small\rm
+          Title Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@title{\copy\titrun}%
+    \fi
+%
+    \if!\the\tocauthor!\relax
+      {\def\and{\noexpand\protect\noexpand\and}%
+      \protected@xdef\toc@uthor{\@author}}%
+    \else
+      \def\\{\noexpand\protect\noexpand\newline}%
+      \protected@xdef\scratch{\the\tocauthor}%
+      \protected@xdef\toc@uthor{\scratch}%
+    \fi
+    \addtocontents{toc}{\noexpand\protect\noexpand\authcount{\the\c@auco}}%
+    \addcontentsline{toc}{author}{\toc@uthor}%
+    \if@runhead
+       \if!\the\authorrunning!
+         \value{@inst}=\value{@auth}%
+         \setcounter{@auth}{1}%
+       \else
+         \edef\@author{\the\authorrunning}%
+       \fi
+       \global\setbox\authrun=\hbox{\small\unboldmath\@author\unskip}%
+       \ifdim\wd\authrun>\instindent
+          \typeout{Names of authors too long for running head. Please supply}%
+          \typeout{a shorter form with \string\authorrunning\space prior to
+                   \string\maketitle}%
+          \global\setbox\authrun=\hbox{\small\rm
+          Authors Suppressed Due to Excessive Length}%
+       \fi
+       \xdef\@author{\copy\authrun}%
+       \markboth{\@author}{\@title}%
+     \fi
+  \endgroup
+  \setcounter{footnote}{\fnnstart}%
+  \clearheadinfo}
+%
+\def\@maketitle{\newpage
+ \markboth{}{}%
+ \def\lastand{\ifnum\value{@inst}=2\relax
+                 \unskip{} \andname\
+              \else
+                 \unskip \lastandname\
+              \fi}%
+ \def\and{\stepcounter{@auth}\relax
+          \ifnum\value{@auth}=\value{@inst}%
+             \lastand
+          \else
+             \unskip,
+          \fi}%
+ \begin{center}%
+ \let\newline\\
+ {\Large \bfseries\boldmath
+  \pretolerance=10000
+  \@title \par}\vskip .8cm
+\if!\@subtitle!\else {\large \bfseries\boldmath
+  \vskip -.65cm
+  \pretolerance=10000
+  \@subtitle \par}\vskip .8cm\fi
+ \setbox0=\vbox{\setcounter{@auth}{1}\def\and{\stepcounter{@auth}}%
+ \def\thanks##1{}\@author}%
+ \global\value{@inst}=\value{@auth}%
+ \global\value{auco}=\value{@auth}%
+ \setcounter{@auth}{1}%
+{\lineskip .5em
+\noindent\ignorespaces
+\@author\vskip.35cm}
+ {\small\institutename}
+ \end{center}%
+ }
+
+% definition of the "\spnewtheorem" command.
+%
+% Usage:
+%
+%     \spnewtheorem{env_nam}{caption}[within]{cap_font}{body_font}
+% or  \spnewtheorem{env_nam}[numbered_like]{caption}{cap_font}{body_font}
+% or  \spnewtheorem*{env_nam}{caption}{cap_font}{body_font}
+%
+% New is "cap_font" and "body_font". It stands for
+% fontdefinition of the caption and the text itself.
+%
+% "\spnewtheorem*" gives a theorem without number.
+%
+% A defined spnewthoerem environment is used as described
+% by Lamport.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\def\@thmcountersep{}
+\def\@thmcounterend{.}
+
+\def\spnewtheorem{\@ifstar{\@sthm}{\@Sthm}}
+
+% definition of \spnewtheorem with number
+
+\def\@spnthm#1#2{%
+  \@ifnextchar[{\@spxnthm{#1}{#2}}{\@spynthm{#1}{#2}}}
+\def\@Sthm#1{\@ifnextchar[{\@spothm{#1}}{\@spnthm{#1}}}
+
+\def\@spxnthm#1#2[#3]#4#5{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}\@addtoreset{#1}{#3}%
+   \expandafter\xdef\csname the#1\endcsname{\expandafter\noexpand
+     \csname the#3\endcsname \noexpand\@thmcountersep \@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+                              \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\@definecounter{#1}%
+   \expandafter\xdef\csname the#1\endcsname{\@thmcounter{#1}}%
+   \expandafter\xdef\csname #1name\endcsname{#2}%
+   \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#3}{#4}}%
+                               \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@spothm#1[#2]#3#4#5{%
+  \@ifundefined{c@#2}{\@latexerr{No theorem environment `#2' defined}\@eha}%
+  {\expandafter\@ifdefinable\csname #1\endcsname
+  {\newaliascnt{#1}{#2}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#1}{\csname #1name\endcsname}{#4}{#5}}%
+  \global\@namedef{end#1}{\@endtheorem}}}}
+
+\def\@spthm#1#2#3#4{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\refstepcounter{#1}%
+\@ifnextchar[{\@spythm{#1}{#2}{#3}{#4}}{\@spxthm{#1}{#2}{#3}{#4}}}
+
+\def\@spxthm#1#2#3#4{\@spbegintheorem{#2}{\csname the#1\endcsname}{#3}{#4}%
+                    \ignorespaces}
+
+\def\@spythm#1#2#3#4[#5]{\@spopargbegintheorem{#2}{\csname
+       the#1\endcsname}{#5}{#3}{#4}\ignorespaces}
+
+\def\@spbegintheorem#1#2#3#4{\trivlist
+                 \item[\hskip\labelsep{#3#1\ #2\@thmcounterend}]#4}
+
+\def\@spopargbegintheorem#1#2#3#4#5{\trivlist
+      \item[\hskip\labelsep{#4#1\ #2}]{#4(#3)\@thmcounterend\ }#5}
+
+% definition of \spnewtheorem* without number
+
+\def\@sthm#1#2{\@Ynthm{#1}{#2}}
+
+\def\@Ynthm#1#2#3#4{\expandafter\@ifdefinable\csname #1\endcsname
+   {\global\@namedef{#1}{\@Thm{\csname #1name\endcsname}{#3}{#4}}%
+    \expandafter\xdef\csname #1name\endcsname{#2}%
+    \global\@namedef{end#1}{\@endtheorem}}}
+
+\def\@Thm#1#2#3{\topsep 7\p@ \@plus2\p@ \@minus4\p@
+\@ifnextchar[{\@Ythm{#1}{#2}{#3}}{\@Xthm{#1}{#2}{#3}}}
+
+\def\@Xthm#1#2#3{\@Begintheorem{#1}{#2}{#3}\ignorespaces}
+
+\def\@Ythm#1#2#3[#4]{\@Opargbegintheorem{#1}
+       {#4}{#2}{#3}\ignorespaces}
+
+\def\@Begintheorem#1#2#3{#3\trivlist
+                           \item[\hskip\labelsep{#2#1\@thmcounterend}]}
+
+\def\@Opargbegintheorem#1#2#3#4{#4\trivlist
+      \item[\hskip\labelsep{#3#1}]{#3(#2)\@thmcounterend\ }}
+
+\if@envcntsect
+   \def\@thmcountersep{.}
+   \spnewtheorem{theorem}{Theorem}[section]{\bfseries}{\itshape}
+\else
+   \spnewtheorem{theorem}{Theorem}{\bfseries}{\itshape}
+   \if@envcntreset
+      \@addtoreset{theorem}{section}
+   \else
+      \@addtoreset{theorem}{chapter}
+   \fi
+\fi
+
+%definition of divers theorem environments
+\spnewtheorem*{claim}{Claim}{\itshape}{\rmfamily}
+\spnewtheorem*{proof}{Proof}{\itshape}{\rmfamily}
+\if@envcntsame % alle Umgebungen wie Theorem.
+   \def\spn@wtheorem#1#2#3#4{\@spothm{#1}[theorem]{#2}{#3}{#4}}
+\else % alle Umgebungen mit eigenem Zaehler
+   \if@envcntsect % mit section numeriert
+      \def\spn@wtheorem#1#2#3#4{\@spxnthm{#1}{#2}[section]{#3}{#4}}
+   \else % nicht mit section numeriert
+      \if@envcntreset
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{section}}
+      \else
+         \def\spn@wtheorem#1#2#3#4{\@spynthm{#1}{#2}{#3}{#4}
+                                   \@addtoreset{#1}{chapter}}%
+      \fi
+   \fi
+\fi
+\spn@wtheorem{case}{Case}{\itshape}{\rmfamily}
+\spn@wtheorem{conjecture}{Conjecture}{\itshape}{\rmfamily}
+\spn@wtheorem{corollary}{Corollary}{\bfseries}{\itshape}
+\spn@wtheorem{definition}{Definition}{\bfseries}{\itshape}
+\spn@wtheorem{example}{Example}{\itshape}{\rmfamily}
+\spn@wtheorem{exercise}{Exercise}{\itshape}{\rmfamily}
+\spn@wtheorem{lemma}{Lemma}{\bfseries}{\itshape}
+\spn@wtheorem{note}{Note}{\itshape}{\rmfamily}
+\spn@wtheorem{problem}{Problem}{\itshape}{\rmfamily}
+\spn@wtheorem{property}{Property}{\itshape}{\rmfamily}
+\spn@wtheorem{proposition}{Proposition}{\bfseries}{\itshape}
+\spn@wtheorem{question}{Question}{\itshape}{\rmfamily}
+\spn@wtheorem{solution}{Solution}{\itshape}{\rmfamily}
+\spn@wtheorem{remark}{Remark}{\itshape}{\rmfamily}
+
+\def\@takefromreset#1#2{%
+    \def\@tempa{#1}%
+    \let\@tempd\@elt
+    \def\@elt##1{%
+        \def\@tempb{##1}%
+        \ifx\@tempa\@tempb\else
+            \@addtoreset{##1}{#2}%
+        \fi}%
+    \expandafter\expandafter\let\expandafter\@tempc\csname cl@#2\endcsname
+    \expandafter\def\csname cl@#2\endcsname{}%
+    \@tempc
+    \let\@elt\@tempd}
+
+\def\theopargself{\def\@spopargbegintheorem##1##2##3##4##5{\trivlist
+      \item[\hskip\labelsep{##4##1\ ##2}]{##4##3\@thmcounterend\ }##5}
+                  \def\@Opargbegintheorem##1##2##3##4{##4\trivlist
+      \item[\hskip\labelsep{##3##1}]{##3##2\@thmcounterend\ }}
+      }
+
+\renewenvironment{abstract}{%
+      \list{}{\advance\topsep by0.35cm\relax\small
+      \leftmargin=1cm
+      \labelwidth=\z@
+      \listparindent=\z@
+      \itemindent\listparindent
+      \rightmargin\leftmargin}\item[\hskip\labelsep
+                                    \bfseries\abstractname]}
+    {\endlist}
+
+\newdimen\headlineindent             % dimension for space between
+\headlineindent=1.166cm              % number and text of headings.
+
+\def\ps@headings{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \leftmark\hfil}
+   \def\@oddhead{\normalfont\small\hfil\rightmark\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\def\ps@titlepage{\let\@mkboth\@gobbletwo
+   \let\@oddfoot\@empty\let\@evenfoot\@empty
+   \def\@evenhead{\normalfont\small\rlap{\thepage}\hspace{\headlineindent}%
+                  \hfil}
+   \def\@oddhead{\normalfont\small\hfil\hspace{\headlineindent}%
+                 \llap{\thepage}}
+   \def\chaptermark##1{}%
+   \def\sectionmark##1{}%
+   \def\subsectionmark##1{}}
+
+\if@runhead\ps@headings\else
+\ps@empty\fi
+
+\setlength\arraycolsep{1.4\p@}
+\setlength\tabcolsep{1.4\p@}
+
+\endinput
+%end of file llncs.cls
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/document/mathpartir.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/document/mathpartir.sty	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,388 @@
+%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+%  Copyright (C) 2001, 2002, 2003 Didier Rémy
+%
+%  Author         : Didier Remy 
+%  Version        : 1.1.1
+%  Bug Reports    : to author
+%  Web Site       : http://pauillac.inria.fr/~remy/latex/
+% 
+%  WhizzyTeX is free software; you can redistribute it and/or modify
+%  it under the terms of the GNU General Public License as published by
+%  the Free Software Foundation; either version 2, or (at your option)
+%  any later version.
+%  
+%  Mathpartir is distributed in the hope that it will be useful,
+%  but WITHOUT ANY WARRANTY; without even the implied warranty of
+%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%  GNU General Public License for more details 
+%  (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%  File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+    [2003/07/10 version 1.1.1 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+\newdimen \mpr@tmpdim
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing 
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+  \edef \MathparNormalpar
+     {\noexpand \lineskiplimit \the\lineskiplimit
+      \noexpand \lineskip \the\lineskip}%
+  }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+  \let \and \mpr@andcr
+  \let \par \mpr@andcr
+  \let \\\mpr@cr
+  \let \eqno \mpr@eqno
+  \let \hva \mpr@hva
+  } 
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+     \noindent $\displaystyle\fi
+     \MathparBindings}
+  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
+  \vbox \bgroup \tabskip 0em \let \+ \cr
+  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+  \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \+\qquad $#1$}\ifnum \wd0 < \hsize
+      \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\+{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\+{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \+#1\+#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\+#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+   \mpr@lista {\+}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
+   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+     \mpr@flatten \mpr@all \mpr@to \mpr@one
+     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+     \mpr@all \mpr@stripend  
+     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+     \ifx 1\mpr@isempty
+   \repeat
+}
+
+%% Part III -- Type inference rules
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+   \def \+##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+   \setbox \mpr@hlist
+      \hbox {\strut
+             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+             \unhbox \mpr@hlist}%
+   \setbox \mpr@vlist
+      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+             \else \unvbox \mpr@vlist \box \mpr@hlist
+             \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+%    \setbox \mpr@hlist
+%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+%    \setbox \mpr@vlist
+%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+%              \else \unvbox \mpr@vlist \box \mpr@hlist
+%              \fi}%
+% }
+
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+  \bgroup
+  \ifx #1T\@premissetrue
+  \else \ifx #1B\@premissefalse
+  \else
+     \PackageError{mathpartir}
+       {Premisse orientation should either be P or B}
+       {Fatal error in Package}%
+  \fi \fi
+  \def \@test {#2}\ifx \@test \mpr@blank\else
+  \setbox \mpr@hlist \hbox {}%
+  \setbox \mpr@vlist \vbox {}%
+  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+  \let \@hvlist \empty \let \@rev \empty
+  \mpr@tmpdim 0em
+  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+  \def \+##1{%
+     \def \@test {##1}\ifx \@test \empty
+        \mpr@htovlist
+        \mpr@tmpdim 0em %%% last bug fix not extensively checked
+     \else
+      \setbox0 \hbox{$\displaystyle {##1}$}\relax
+      \advance \mpr@tmpdim by \wd0
+      %\mpr@tmpdim 1.02\mpr@tmpdim
+      \ifnum \mpr@tmpdim < \hsize
+         \ifnum \wd\mpr@hlist > 0
+           \if@premisse
+             \setbox \mpr@hlist 
+                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+           \else
+             \setbox \mpr@hlist
+                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
+           \fi
+         \else 
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+         \fi
+      \else
+         \ifnum \wd \mpr@hlist > 0
+            \mpr@htovlist 
+            \mpr@tmpdim \wd0
+         \fi
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+      \fi
+      \advance \mpr@tmpdim by \mpr@sep
+   \fi
+   }%
+   \@rev
+   \mpr@htovlist
+   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+   \fi
+   \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+    \let\@@over\over % fallback if amsmath is not loaded
+    \let\@@overwithdelims\overwithdelims
+    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+  }{}
+
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\@@over #2}$}}
+\let \mpr@fraction \mpr@@fraction
+\def \mpr@@reduce #1#2{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+  {\bgroup
+     \ifnum \linewidth<\hsize \hsize \linewidth\fi
+     \mpr@rulelineskip
+     \let \and \qquad
+     \let \hva \mpr@hva
+     \let \@rulename \mpr@empty
+     \let \@rule@options \mpr@empty
+     \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+  {\everymath={\displaystyle}%       
+   \def \@test {#2}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+   \else 
+   \def \@test {#3}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+   \else
+   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+   \fi \fi
+   \def \@test {#1}\ifx \@test\empty \box0
+   \else \vbox 
+%%% Suggestion de Francois pour les etiquettes longues
+%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+      {\hbox {\RefTirName {#1}}\box0}\fi
+   \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \+
+% Each \+ produces a break, attempting horizontal breaks if possible, 
+% and  vertical breaks if needed. 
+% 
+% An empty element obtained by \+\+ produces a vertical break in all cases. 
+%
+% The former rule is aligned on the fraction bar. 
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+% 
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%       
+%  width                set the width of the rule to val
+%  narrower             set the width of the rule to val\hsize
+%  before               execute val at the beginning/left
+%  lab                  put a label [Val] on top of the rule
+%  lskip                add negative skip on the right
+%  left                 put a left label [Val]
+%  Left                 put a left label [Val],  ignoring its width 
+%  right                put a right label [Val]
+%  Right                put a right label [Val], ignoring its width
+%  leftskip             skip negative space on the left-hand side
+%  rightskip            skip negative space on the right-hand side
+%  vdots                lift the rule by val and fill vertical space with dots
+%  after                execute val at the end/right
+%  
+%  Note that most options must come in this order to avoid strange
+%  typesetting (in particular  leftskip must preceed left and Left and
+%  rightskip must follow Right or right; vdots must come last 
+%  or be only followed by rightskip. 
+%  
+
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\def \mprset #1{\setkeys{mprset}{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newdimen \rule@dimen
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+         \setbox \mpr@right \hbox{}%
+         $\setkeys{mpr}{#1}%
+          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+          \box \mpr@right \mpr@vdots$}
+  \setbox1 \hbox {\strut}
+  \rule@dimen \dp0 \advance \rule@dimen by -\dp1
+  \raise \rule@dimen \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode 
+    \let \@do \mpr@inferstar@
+  \else 
+    \let \@do \mpr@err@skipargs
+    \PackageError {mathpartir}
+      {\string\inferrule* can only be used in math mode}{}%
+  \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \tir@name #1{\hbox {\small \sc #1}}
+\let \TirName \tir@name
+\let \RefTirName \tir@name
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/document/root.bib	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,76 @@
+@inproceedings{HuffmanUrban10,
+  author = 	 {B.~Huffman and C.~Urban},
+  title = 	 {{P}roof {P}earl: {A} {N}ew {F}oundation for {N}ominal {I}sabelle},
+  booktitle = {Proc.~of the 1st Conference on  Interactive Theorem Proving (ITP'10)}, 
+  pages = {35--50},
+  volume = {6172},
+  series = {LNCS},
+  year = 	 {2010}
+}
+@inproceedings{Sac11,
+  author    = {Cezary Kaliszyk and
+               Christian Urban},
+  title     = {Quotients revisited for {I}sabelle/{HOL}},
+  booktitle = {Proc. of the 26th ACM Symposium on Applied Computing (SAC'11)},
+  year      = {2011},
+  pages     = {1639-1644},
+  publisher = {ACM},
+  editor    = {William C. Chu and W. Eric Wong and Mathew J. Palakal and Chih-Cheng Hung},
+}
+@inproceedings{Esop11,
+  author    = {Christian Urban and
+               Cezary Kaliszyk},
+  title     = {General Bindings and Alpha-Equivalence in {N}ominal {I}sabelle},
+  year      = {2011},
+  pages     = {480-500},
+  booktitle     = {Proc. of the 20th European Symposium on Programming (ESOP'11)},
+  publisher = {Springer Verlag},
+  series    = {LNCS},
+  volume    = {6602},
+  editor    = {Gilles Barthe},
+}
+
+@book{LambdaBook,
+  author = {Hendrik Pieter Barendregt},
+  title={{The Lambda Calculus: Its Syntax and Semantics}},
+  year={2001},
+  publisher={Elsevier},
+  volume  = {103},
+  series  = {Studies in Logic and the Foundations of Mathematics},
+}
+
+@article{Pitts03,
+  author =	 {Andrew M.~Pitts},
+  title =	 {{N}ominal {L}ogic, {A} {F}irst {O}rder {T}heory of {N}ames and
+                  {B}inding},
+  journal =	 {Information and Computation},
+  year =	 {2003},
+  volume =	 {183},
+  pages =	 {165--193}
+}
+
+@Article{Norrish06,
+  author =       {Michael Norrish},
+  title =        {Mechanising $\lambda$-Calculus Using a Classical First Order
+                  Theory of Terms with Permutations},
+  journal =      {Higher-Order and Symbolic Computation},
+  year =         2006,
+  volume =       19,
+  pages =        {169--195},
+  doi =          {10.1007/s10990-006-8745-7}
+}
+
+@Inproceedings{NominalLambda,
+    author = {Christian Urban},
+    title = {{Nominal techniques in Isabelle/HOL}},
+    booktitle = {Proceedings of the 20th International Conference on Automated Deduction (CADE'05)},
+    year = {2005},
+    pages = {38--53},
+    publisher = {Springer}
+}
+@article{LocallyNameless,
+  author    = {Randy Pollack and Masahiko Sato and Wilmer Ricciotti},
+  title     = {A Canonical Locally Named Representation of Binding},
+  journal   = {Journal of Automated Reasoning},
+  year      = {2011},
+}
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Ex/Exec/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Exec/document/root.tex	Tue May 22 14:55:58 2012 +0200
@@ -0,0 +1,81 @@
+\documentclass{llncs}
+\usepackage[utf8]{inputenc}
+\usepackage{lineno}
+\usepackage{url}
+\usepackage{amsmath,amssymb}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+%\usepackage{boxedminipage}
+
+\allowdisplaybreaks
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+\DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
+\DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymbullet}{{\raisebox{0.2mm}{\small$\bullet$}}}
+\renewcommand{\isasymintegral}{$\lambda$}
+\renewcommand{\isasymlbrace}{$\ulcorner$}
+\renewcommand{\isasymrbrace}{$\urcorner$}
+%\renewcommand{\isasymguillemotleft}{}
+%\renewcommand{\isasymguillemotright}{}
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{=}
+%%\renewcommand{\isasymiota}{}
+\renewcommand{\isasymxi}{$..$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\newcommand{\isasymnotapprox}{$\not\approx$}
+\newcommand{\isasymLET}{$\mathtt{let}$}
+\newcommand{\isasymAND}{$\mathtt{and}$}
+\newcommand{\isasymIN}{$\mathtt{in}$}
+\newcommand{\isasymEND}{$\mathtt{end}$}
+\newcommand{\isasymBIND}{$\mathtt{bind}$}
+\newcommand{\isasymANIL}{$\mathtt{anil}$}
+\newcommand{\isasymACONS}{$\mathtt{acons}$}
+\newcommand{\isasymCASE}{$\mathtt{case}$}
+\newcommand{\isasymOF}{$\mathtt{of}$}
+\newcommand{\isasymAL}{\makebox[0mm][l]{$^\alpha$}}
+\newcommand{\isasymPRIME}{\makebox[0mm][l]{$'$}}
+\newcommand{\isasymFRESH}{\#}
+\newcommand{\LET}{\;\mathtt{let}\;}
+\newcommand{\IN}{\;\mathtt{in}\;}
+\newcommand{\END}{\;\mathtt{end}\;}
+\newcommand{\AND}{\;\mathtt{and}\;}
+\newcommand{\fv}{\mathit{fv}}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+\newenvironment{proof-of}[1]{{\em Proof of #1:}}{}
+
+\begin{document}
+
+\title{Execution modulo alpha-equivalence}
+\author{...\inst{1} \and ...\inst{2}}
+\institute{... \and ...}
+
+\maketitle
+
+\begin{abstract}
+  In this paper we show how a formal specification defined modulo
+  alpha-equivalence can be programatically made executable.
+  We show a general algorithm and we present examples of
+  executed calculi, which we implement in Nominal Isabelle.
+\end{abstract}
+
+\input{session}
+
+%\begin{spacing}{0.9}
+\bibliographystyle{abbrv}
+\bibliography{root}
+%\end{spacing}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/GPerm.thy
--- a/Nominal/GPerm.thy	Tue May 22 14:00:59 2012 +0200
+++ b/Nominal/GPerm.thy	Tue May 22 14:55:58 2012 +0200
@@ -162,10 +162,6 @@
   "x \<approx> y \<Longrightarrow> map swap_pair x \<approx> map swap_pair y"
   by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx>) uminus_perm_raw uminus_perm_raw"
-  by (auto intro!: fun_relI simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
-
 lemma fst_snd_map_pair[simp]:
   "fst ` map_pair f g ` set l = f ` fst ` set l"
   "snd ` map_pair f g ` set l = g ` snd ` set l"
@@ -240,29 +236,20 @@
   "x \<approx> y \<Longrightarrow> xa \<approx> ya \<Longrightarrow> perm_add_raw x xa \<approx> perm_add_raw y ya"
   by (simp add: fun_eq_iff perm_add_apply perm_eq_def)
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op \<approx> ===> op \<approx>) perm_add_raw perm_add_raw"
-  by (auto intro!: fun_relI simp add: perm_add_raw_rsp)
-
 lemma [simp]:
   "a \<approx> a \<longleftrightarrow> valid_perm a"
   by (simp_all add: perm_eq_def)
 
-lemma [quot_respect]: "[] \<approx> []"
-  by auto
-
-lemmas [simp] = in_respects
-
 instantiation gperm :: (type) group_add
 begin
 
-quotient_definition "0 :: 'a gperm" is "[] :: ('a \<times> 'a) list"
+lift_definition zero_gperm :: "'a gperm" is "[]" by simp
 
-quotient_definition "uminus :: 'a gperm \<Rightarrow> 'a gperm" is
-  "uminus_perm_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
+lift_definition uminus_gperm :: "'a gperm \<Rightarrow> 'a gperm" is uminus_perm_raw
+  by (auto simp add: fun_eq_iff perm_apply_minus[symmetric] perm_eq_def)
 
-quotient_definition "(op +) :: 'a gperm \<Rightarrow> 'a gperm \<Rightarrow> 'a gperm" is
-  "perm_add_raw :: ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list \<Rightarrow> ('a \<times> 'a) list"
+lift_definition plus_gperm :: "'a gperm \<Rightarrow> 'a gperm \<Rightarrow> 'a gperm" is perm_add_raw
+  by simp
 
 definition
   minus_perm_def: "(p1::'a gperm) - p2 = p1 + - p2"
@@ -270,23 +257,17 @@
 instance
   apply default
   unfolding minus_perm_def
-  by (partiality_descending, simp add: perm_add_apply perm_eq_def fun_eq_iff valid_perm_add_minus)+
+  by (transfer,simp add: perm_add_apply perm_eq_def fun_eq_iff valid_perm_add_minus)+
 
 end
 
 definition "mk_perm_raw l = (if valid_perm l then l else [])"
 
-quotient_definition "mk_perm :: ('a \<times> 'a) list \<Rightarrow> 'a gperm"
-  is "mk_perm_raw"
+lift_definition mk_perm :: "('a \<times> 'a) list \<Rightarrow> 'a gperm" is "mk_perm_raw"
+  by (simp add: mk_perm_raw_def)
 
 definition "dest_perm_raw p = sort [x\<leftarrow>p. fst x \<noteq> snd x]"
 
-quotient_definition "dest_perm :: ('a :: linorder) gperm \<Rightarrow> ('a \<times> 'a) list"
-  is "dest_perm_raw"
-
-lemma [quot_respect]: "(op = ===> op \<approx>) mk_perm_raw mk_perm_raw"
-  by (auto intro!: fun_relI simp add: mk_perm_raw_def)
-
 lemma distinct_fst_distinct[simp]: "distinct (map fst x) \<Longrightarrow> distinct x"
   by (induct x) auto
 
@@ -341,14 +322,13 @@
   by (rule sorted_distinct_set_unique)
      (simp_all add: distinct_filter valid_perm_def perm_eq_not_eq_same[simplified perm_eq_def, simplified])
 
-lemma [quot_respect]:
-  "(op \<approx> ===> op =) dest_perm_raw dest_perm_raw"
-  by (auto intro!: fun_relI simp add: perm_eq_def)
+lift_definition dest_perm :: "('a :: linorder) gperm \<Rightarrow> ('a \<times> 'a) list"
+  is "dest_perm_raw"
+  by (simp add: perm_eq_def)
 
 lemma dest_perm_mk_perm[simp]:
   "dest_perm (mk_perm xs) = sort [x\<leftarrow>mk_perm_raw xs. fst x \<noteq> snd x]"
-  by (partiality_descending)
-     (simp add: dest_perm_raw_def)
+  by transfer (simp add: dest_perm_raw_def)
 
 lemma valid_perm_filter_id[simp]:
   "valid_perm p \<Longrightarrow> valid_perm [x\<leftarrow>p. fst x \<noteq> snd x]"
@@ -397,7 +377,7 @@
 
 lemma mk_perm_dest_perm[code abstype]:
   "mk_perm (dest_perm p) = p"
-  by (partiality_descending)
+  by transfer
      (auto simp add: mk_perm_raw_def)
 
 instantiation gperm :: (linorder) equal begin
@@ -407,51 +387,46 @@
 instance
   apply default
   unfolding equal_gperm_def
-  by partiality_descending simp
+  by transfer simp
 
 end
 
 lemma [code abstract]:
   "dest_perm 0 = []"
-  by (partiality_descending) (simp add: dest_perm_raw_def)
+  by transfer (simp add: dest_perm_raw_def)
 
 lemma [code abstract]:
   "dest_perm (-a) = dest_perm_raw (uminus_perm_raw (dest_perm a))"
-  by (partiality_descending) (auto)
+  by transfer auto
 
 lemma [code abstract]:
   "dest_perm (a + b) = dest_perm_raw (perm_add_raw (dest_perm a) (dest_perm b))"
-  by (partiality_descending) auto
+  by transfer auto
 
-quotient_definition "gpermute :: 'a gperm \<Rightarrow> 'a \<Rightarrow> 'a"
-is perm_apply
-
-lemma [quot_respect]: "(op \<approx> ===> op =) perm_apply perm_apply"
-  by (auto intro!: fun_relI simp add: perm_eq_def)
+lift_definition gpermute :: "'a gperm \<Rightarrow> 'a \<Rightarrow> 'a"
+  is perm_apply
+  by (simp add: perm_eq_def)
 
 lemma gpermute_zero[simp]:
   "gpermute 0 x = x"
-  by descending simp
+  by transfer simp
 
 lemma gpermute_add[simp]:
   "gpermute (p + q) x = gpermute p (gpermute q x)"
-  by descending (simp add: perm_add_apply)
-
-definition [simp]:"swap_raw a b = (if a = b then [] else [(a, b), (b, a)])"
+  by transfer (simp add: perm_add_apply)
 
-lemma [quot_respect]: "(op = ===> op = ===> op \<approx>) swap_raw swap_raw"
-  by (auto intro!: fun_relI simp add: valid_perm_def)
+definition [simp]: "swap_raw a b = (if a = b then [] else [(a, b), (b, a)])"
 
-quotient_definition "gswap :: 'a \<Rightarrow> 'a \<Rightarrow> 'a gperm"
-is swap_raw
+lift_definition gswap :: "'a \<Rightarrow> 'a \<Rightarrow> 'a gperm" is swap_raw
+  by (auto simp add: valid_perm_def)
 
 lemma [code abstract]:
   "dest_perm (gswap a b) = (if (a, b) \<le> (b, a) then swap_raw a b else swap_raw b a)"
-  by (partiality_descending) (auto simp add: dest_perm_raw_def)
+  by transfer (auto simp add: dest_perm_raw_def)
 
 lemma swap_self [simp]:
   "gswap a a = 0"
-  by (partiality_descending, auto)
+  by transfer simp
 
 lemma [simp]: "a \<noteq> b \<Longrightarrow> valid_perm [(a, b), (b, a)]"
   unfolding valid_perm_def by auto
@@ -459,35 +434,35 @@
 lemma swap_cancel [simp]:
   "gswap a b + gswap a b = 0"
   "gswap a b + gswap b a = 0"
-  by (descending, auto simp add: perm_eq_def perm_add_apply)+
+  by (transfer, auto simp add: perm_eq_def perm_add_apply)+
 
 lemma minus_swap [simp]:
   "- gswap a b = gswap a b"
-  by (partiality_descending, auto simp add: perm_eq_def)
+  by transfer (auto simp add: perm_eq_def)
 
 lemma swap_commute:
   "gswap a b = gswap b a"
-  by (partiality_descending, auto simp add: perm_eq_def)
+  by transfer (auto simp add: perm_eq_def)
 
 lemma swap_triple:
   assumes "a \<noteq> b" "c \<noteq> b"
   shows "gswap a c + gswap b c + gswap a c = gswap a b"
   using assms
-  by descending (auto simp add: perm_eq_def fun_eq_iff perm_add_apply)
+  by transfer (auto simp add: perm_eq_def fun_eq_iff perm_add_apply)
 
 lemma gpermute_gswap[simp]:
   "b \<noteq> a \<Longrightarrow> gpermute (gswap a b) b = a"
   "a \<noteq> b \<Longrightarrow> gpermute (gswap a b) a = b"
   "c \<noteq> b \<Longrightarrow> c \<noteq> a \<Longrightarrow> gpermute (gswap a b) c = c"
-  by (descending, auto)+
+  by (transfer, auto)+
 
 lemma gperm_eq:
   "(p = q) = (\<forall>a. gpermute p a = gpermute q a)"
-  by (partiality_descending) (auto simp add: perm_eq_def)
+  by transfer (auto simp add: perm_eq_def)
 
 lemma finite_gpermute_neq:
   "finite {a. gpermute p a \<noteq> a}"
-  apply descending
+  apply transfer
   apply (rule_tac B="fst ` set p" in finite_subset)
   apply auto
   by (metis perm_apply_outset)
diff -r 4cf3a4d36799 -r 9876d73adb2b Nominal/Nominal2_Base_Exec.thy
--- a/Nominal/Nominal2_Base_Exec.thy	Tue May 22 14:00:59 2012 +0200
+++ b/Nominal/Nominal2_Base_Exec.thy	Tue May 22 14:55:58 2012 +0200
@@ -9,6 +9,12 @@
         "~~/src/HOL/Library/Infinite_Set"
         "~~/src/HOL/Quotient_Examples/FSet"
         "GPerm"
+  "~~/src/HOL/Library/List_lexord"
+  "~~/src/HOL/Library/Product_ord"
+  "~~/src/HOL/Library/Efficient_Nat"
+  "~~/src/HOL/Library/Char_ord"
+  "~~/src/HOL/Library/Code_Char_chr"
+  "~~/src/HOL/Library/Code_Char_ord"
 keywords
   "atom_decl" "equivariance" :: thy_decl
 uses ("nominal_basics.ML")
@@ -95,73 +101,70 @@
 typedef (open) perm = "{p::atom gperm. sort_respecting p}"
   by (auto intro: exI[of _ "0"])
 
+setup_lifting type_definition_perm
+
 lemma perm_eq_rep:
   "p = q \<longleftrightarrow> Rep_perm p = Rep_perm q"
   by (simp add: Rep_perm_inject)
 
-definition mk_perm :: "atom gperm \<Rightarrow> perm" where
-  "mk_perm p = Abs_perm (if sort_respecting p then p else 0)"
-
-lemma sort_respecting_Rep_perm [simp, intro]:
+lift_definition mk_perm :: "atom gperm \<Rightarrow> perm" is
+  "\<lambda>p. if sort_respecting p then p else 0" by simp
+
+(*lemma sort_respecting_Rep_perm [simp, intro]:
   "sort_respecting (Rep_perm p)"
-  using Rep_perm [of p] by simp
+  using Rep_perm [of p] by simp*)
 
 lemma Rep_perm_mk_perm [simp]:
   "Rep_perm (mk_perm p) = (if sort_respecting p then p else 0)"
   by (simp add: mk_perm_def Abs_perm_inverse)
 
-lemma mk_perm_Rep_perm [simp, code abstype]:
+(*lemma mk_perm_Rep_perm [simp, code abstype]:
   "mk_perm (Rep_perm dxs) = dxs"
-  by (simp add: mk_perm_def Rep_perm_inverse)
+  by (simp add: mk_perm_def Rep_perm_inverse)*)
 
 instance perm :: size ..
 
 instantiation perm :: group_add
 begin
 
-definition "(0 :: perm) = mk_perm 0"
-
-definition "uminus p = mk_perm (uminus (Rep_perm p))"
-
-definition "p + q = mk_perm ((Rep_perm p) + (Rep_perm q))"
+lift_definition zero_perm :: "perm" is "0" by simp
+
+lift_definition uminus_perm :: "perm \<Rightarrow> perm" is "uminus"
+  unfolding sort_respecting_def
+  by transfer (auto, metis perm_apply_minus)
+
+lift_definition plus_perm :: "perm \<Rightarrow> perm \<Rightarrow> perm" is "plus"
+  unfolding sort_respecting_def
+  by transfer (simp add: perm_add_apply)
 
 definition "(p :: perm) - q = p + - q"
 
-lemma [simp]:
-  "sort_respecting x \<Longrightarrow> sort_respecting y \<Longrightarrow> sort_respecting (x + y)"
-  unfolding sort_respecting_def
-  by descending (simp add: perm_add_apply)
-
-lemma [simp]:
-  "sort_respecting y \<Longrightarrow> sort_respecting (- y)"
-  unfolding sort_respecting_def
-  by partiality_descending
-     (auto, metis perm_apply_minus)
-
 lemma Rep_perm_0 [simp, code abstract]:
   "Rep_perm 0 = 0"
-  by (simp add: zero_perm_def)
+  by (metis (mono_tags) zero_perm.rep_eq)
 
 lemma Rep_perm_uminus [simp, code abstract]:
   "Rep_perm (- p) = - (Rep_perm p)"
-  by (simp add: uminus_perm_def)
+  by (metis uminus_perm.rep_eq)
 
 lemma Rep_perm_add [simp, code abstract]:
   "Rep_perm (p + q) = (Rep_perm p) + (Rep_perm q)"
-  by (simp add: plus_perm_def)
+  by (simp add: plus_perm.rep_eq)
 
 instance
-  by default (auto simp add: perm_eq_rep add_assoc minus_perm_def)
+  apply default
+  unfolding minus_perm_def
+  by (transfer, simp add: add_assoc)+
 
 end
 
-definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm"  ("'(_ \<rightleftharpoons> _')")
-where "swap a b = (if sort_of a = sort_of b then mk_perm (gswap a b) else 0)"
+lift_definition swap :: "atom \<Rightarrow> atom \<Rightarrow> perm"  ("'(_ \<rightleftharpoons> _')")
+  is "(\<lambda>a b. (if sort_of a = sort_of b then mk_perm (gswap a b) else 0))" .
 
 lemma sort_respecting_swap [simp]:
   "sort_of a = sort_of b \<Longrightarrow> sort_respecting (gswap a b)"
   unfolding sort_respecting_def
-  by descending auto
+  by transfer auto
 
 lemma Rep_swap [simp, code abstract]:
   "Rep_perm (swap a b) = (if sort_of a = sort_of b then gswap a b else 0)"
@@ -268,7 +271,7 @@
 
 lemma sort_of_permute [simp]:
   shows "sort_of (p \<bullet> a) = sort_of a"
-  by (metis sort_respecting_Rep_perm sort_respecting_def permute_atom_def)
+  by (metis Rep_perm mem_Collect_eq sort_respecting_def permute_atom_def)
 
 lemma swap_atom:
   shows "(a \<rightleftharpoons> b) \<bullet> c =
@@ -542,11 +545,6 @@
 
 subsection {* Permutations for @{typ "'a fset"} *}
 
-lemma permute_fset_rsp[quot_respect]:
-  shows "(op = ===> list_eq ===> list_eq) permute permute"
-  unfolding fun_rel_def
-  by (simp add: set_eqvt[symmetric])
-
 instantiation fset :: (pt) pt
 begin
 
@@ -554,8 +552,9 @@
   "permute_fset :: perm \<Rightarrow> 'a fset \<Rightarrow> 'a fset"
 is
   "permute :: perm \<Rightarrow> 'a list \<Rightarrow> 'a list"
-
-instance 
+  by (simp add: set_eqvt[symmetric])
+
+instance
 proof
   fix x :: "'a fset" and p q :: "perm"
   have lst: "\<And>l :: 'a list. 0 \<bullet> l = l" by simp
@@ -3167,7 +3166,86 @@
 
 use "nominal_eqvt.ML"
 
-
-
+instantiation atom_sort :: ord begin
+
+fun less_atom_sort where
+  "less_atom_sort (Sort s1 l1) (Sort s2 []) \<longleftrightarrow> s1 < s2"
+| "less_atom_sort (Sort s1 []) (Sort s2 (h # t)) \<longleftrightarrow> s1 \<le> s2"
+| "less_atom_sort (Sort s1 (h1 # t1)) (Sort s2 (h2 # t2)) \<longleftrightarrow> s1 < s2 \<or> s1 \<le> s2 \<and> ((less_atom_sort h1 h2) \<or> (h1 = h2 \<and> less_atom_sort (Sort s1 t1) (Sort s2 t2)))"
+
+definition less_eq_atom_sort where
+  less_eq_atom_sort_def: "less_eq_atom_sort (x :: atom_sort) y \<longleftrightarrow> x < y \<or> x = y"
+
+instance ..
 
 end
+
+lemma less_st_less: "(Sort s1 l1) < (Sort s2 l2) \<longleftrightarrow> s1 < s2 \<or> s1 \<le> s2 \<and> l1 < l2"
+  by (induct l1 l2 rule: list_induct2') auto
+
+lemma not_as_le_as: "\<not>((x :: atom_sort) < x)"
+  apply (rule less_atom_sort.induct[of "\<lambda>x y. x = y \<longrightarrow> \<not>x < y" "x" "x", simplified]) ..
+
+instance atom_sort :: linorder
+proof (default, auto simp add: less_eq_atom_sort_def not_as_le_as)
+  fix x y :: atom_sort
+  assume x: "x < y" "y < x"
+  then show False
+    by (induct x y rule: less_atom_sort.induct) (case_tac l1, auto)
+  with x show "x = y"
+    by (induct x y rule: less_atom_sort.induct) (case_tac l1, auto)
+next
+  fix x y z :: atom_sort
+  assume "x < y" "y < z"
+  then show "x < z"
+    apply (induct x z arbitrary: y rule: less_atom_sort.induct)
+    apply (case_tac [!] y) apply auto
+    apply (case_tac [!] list2) apply auto
+    apply (case_tac l1) apply auto[2]
+    done
+next
+  fix x y :: atom_sort
+  assume x: "\<not>x < y" "y \<noteq> x"
+  then show "y < x"
+    apply (induct x y rule: less_atom_sort.induct)
+    apply auto
+    apply (case_tac [!] l1)
+    apply auto
+    done
+qed
+
+instantiation atom :: linorder begin
+
+definition less_eq_atom where
+  [simp]: "less_eq_atom x y \<longleftrightarrow> sort_of x < sort_of y \<or> sort_of x \<le> sort_of y \<and> nat_of x \<le> nat_of y"
+
+definition less_atom where
+  [simp]: "less_atom x y \<longleftrightarrow> sort_of x < sort_of y \<or> sort_of x \<le> sort_of y \<and> nat_of x < nat_of y"
+
+instance apply default
+  apply auto
+  apply (case_tac x, case_tac y)
+  apply auto
+  done
+
+end
+
+lemma [code]:
+  "gpermute p = perm_apply (dest_perm p)"
+  apply transfer
+  unfolding Rel_def
+  by (auto, metis perm_eq_def valid_dest_perm_raw_eq(2))
+
+instantiation perm :: equal begin
+
+definition "equal_perm a b \<longleftrightarrow> Rep_perm a = Rep_perm b"
+
+instance
+  apply default
+  unfolding equal_perm_def perm_eq_rep ..
+
+end
+
+(* Test: export_code swap in SML *)
+
+end