# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1274881076 -7200
# Node ID 8732ff59068b2c24a89303c45565f8ed0837c18a
# Parent  9fb315392493f8d1d6905ebe6ecb0d323c3f0068# Parent  1cf20169660c6989bd4076d1e27fbd618f10834f
merged

diff -r 9fb315392493 -r 8732ff59068b Attic/Prove.thy
--- a/Attic/Prove.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Attic/Prove.thy	Wed May 26 15:37:56 2010 +0200
@@ -9,19 +9,18 @@
 ML {*
 let
   fun after_qed thm_name thms lthy =
-       Local_Theory.note (thm_name, (flat thms)) lthy |> snd
-    
-  fun setup_proof (name_spec, (txt, pos)) lthy =
+    Local_Theory.note (thm_name, (flat thms)) lthy |> snd
+  fun setup_proof (name_spec, (txt, _)) lthy =
   let
     val trm = ML_Context.evaluate lthy true ("r", r) txt
   in
     Proof.theorem NONE (after_qed name_spec) [[(trm,[])]] lthy
   end
 
-  val parser = SpecParse.opt_thm_name ":" -- OuterParse.ML_source
+  val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
 in
-  OuterSyntax.local_theory_to_proof "prove" "proving a proposition" 
-    OuterKeyword.thy_goal (parser >> setup_proof)
+  Outer_Syntax.local_theory_to_proof "prove" "proving a proposition" 
+    Keyword.thy_goal (parser >> setup_proof)
 end
 *}
 
diff -r 9fb315392493 -r 8732ff59068b Nominal-General/nominal_atoms.ML
--- a/Nominal-General/nominal_atoms.ML	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal-General/nominal_atoms.ML	Wed May 26 15:37:56 2010 +0200
@@ -71,10 +71,10 @@
 
 (** outer syntax **)
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = Parse and K = Keyword in
 
 val _ =
-  OuterSyntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
+  Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
     ((P.binding -- Scan.option (Args.parens (P.binding))) >>
       (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
 
diff -r 9fb315392493 -r 8732ff59068b Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Wed May 26 15:37:56 2010 +0200
@@ -184,10 +184,10 @@
   equivariance preds raw_induct intrs ctxt |> snd
 end
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = Parse and K = Keyword in
 
 val _ =
-  OuterSyntax.local_theory "equivariance"
+  Outer_Syntax.local_theory "equivariance"
     "Proves equivariance for inductive predicate involving nominal datatypes." 
       K.thy_decl (P.xname >> equivariance_cmd);
 end;
diff -r 9fb315392493 -r 8732ff59068b Nominal-General/nominal_permeq.ML
diff -r 9fb315392493 -r 8732ff59068b Nominal/Ex/Ex2.thy
diff -r 9fb315392493 -r 8732ff59068b Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Wed May 26 15:37:56 2010 +0200
@@ -1,5 +1,5 @@
 theory Lambda
-imports "../NewParser"
+imports "../NewParser" Quotient_Option
 begin
 
 atom_decl name
@@ -456,10 +456,10 @@
 fun prove_strong_ind (pred_name, avoids) ctxt = 
   Proof.theorem NONE (K I) [] ctxt
 
-local structure P = OuterParse and K = OuterKeyword in
+local structure P = Parse and K = Keyword in
 
 val _ =
-  OuterSyntax.local_theory_to_proof "nominal_inductive"
+  Outer_Syntax.local_theory_to_proof "nominal_inductive"
     "proves strong induction theorem for inductive predicate involving nominal datatypes" K.thy_goal
       (P.xname -- (Scan.optional (P.$$$ "avoids" |-- P.enum1 "|" (P.name --
         (P.$$$ ":" |-- P.and_list1 P.term))) []) >>  prove_strong_ind)
@@ -474,113 +474,283 @@
 
 (* Substitution *)
 
-definition new where
-  "new s = (THE x. \<forall>a \<in> s. atom x \<noteq> a)"
-
-lemma size_no_change: "size (p \<bullet> (t :: lam_raw)) = size t"
-  by (induct t) simp_all
+primrec match_Var_raw where
+  "match_Var_raw (Var_raw x) = Some x"
+| "match_Var_raw (App_raw x y) = None"
+| "match_Var_raw (Lam_raw n t) = None"
 
-function
-  subst_raw :: "lam_raw \<Rightarrow> name \<Rightarrow> lam_raw \<Rightarrow> lam_raw"
-where
-  "subst_raw (Var_raw x) y s = (if x=y then s else (Var_raw x))"
-| "subst_raw (App_raw l r) y s = App_raw (subst_raw l y s) (subst_raw r y s)"
-| "subst_raw (Lam_raw x t) y s =
-      Lam_raw (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))
-       (subst_raw ((x \<leftrightarrow> (new ({atom y} \<union> fv_lam_raw s \<union> fv_lam_raw t - {atom x}))) \<bullet> t) y s)"
-by (pat_completeness, auto)
-termination
-  apply (relation "measure (\<lambda>(t, y, s). (size t))")
-  apply (auto simp add: size_no_change)
+quotient_definition
+  "match_Var :: lam \<Rightarrow> name option"
+is match_Var_raw
+
+lemma [quot_respect]: "(alpha_lam_raw ===> op =) match_Var_raw match_Var_raw"
+  apply rule
+  apply (induct_tac a b rule: alpha_lam_raw.induct)
+  apply simp_all
   done
 
-lemma fv_subst[simp]: "fv_lam_raw (subst_raw t y s) =
-  (if (atom y \<in> fv_lam_raw t) then fv_lam_raw s \<union> (fv_lam_raw t - {atom y}) else fv_lam_raw t)"
-  apply (induct t arbitrary: s)
-  apply (auto simp add: supp_at_base)[1]
-  apply (auto simp add: supp_at_base)[1]
-  apply (simp only: fv_lam_raw.simps)
-  apply simp
-  apply (rule conjI)
+lemmas match_Var_simps = match_Var_raw.simps[quot_lifted]
+
+primrec match_App_raw where
+  "match_App_raw (Var_raw x) = None"
+| "match_App_raw (App_raw x y) = Some (x, y)"
+| "match_App_raw (Lam_raw n t) = None"
+
+quotient_definition
+  "match_App :: lam \<Rightarrow> (lam \<times> lam) option"
+is match_App_raw
+
+lemma [quot_respect]:
+  "(alpha_lam_raw ===> option_rel (prod_rel alpha_lam_raw alpha_lam_raw)) match_App_raw match_App_raw"
+  apply (intro fun_relI)
+  apply (induct_tac a b rule: alpha_lam_raw.induct)
+  apply simp_all
+  done
+
+lemmas match_App_simps = match_App_raw.simps[quot_lifted]
+
+definition new where
+  "new (s :: 'a :: fs) = (THE x. \<forall>a \<in> supp s. atom x \<noteq> a)"
+
+definition
+  "match_Lam (S :: 'a :: fs) t = (if (\<exists>n s. (t = Lam n s)) then
+    (let z = new (S, t) in Some (z, THE s. t = Lam z s)) else None)"
+
+lemma lam_half_inj: "(Lam z s = Lam z sa) = (s = sa)"
+  apply auto
+  apply (simp only: lam.eq_iff alphas)
   apply clarify
-  sorry
-
-thm supp_at_base
-lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)"
+  apply (simp add: eqvts)
   sorry
 
-lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)"
-  apply (induct t arbitrary: p y s)
-  apply simp_all
-  apply(perm_simp)
-  apply simp
-  sorry
+lemma match_Lam_simps:
+  "match_Lam S (Var n) = None"
+  "match_Lam S (App l r) = None"
+  "z = new (S, (Lam z s)) \<Longrightarrow> match_Lam S (Lam z s) = Some (z, s)"
+  apply (simp_all add: match_Lam_def)
+  apply (simp add: lam_half_inj)
+  apply auto
+  done
 
-lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x"
-  apply (induct x arbitrary: d)
-  apply (simp_all add: alpha_lam_raw.intros)
-  apply (rule alpha_lam_raw.intros)
-  apply (rule_tac x="(name \<leftrightarrow> new (insert (atom d) (supp d)))" in exI)
-  apply (simp add: alphas)
-  oops
+(*
+lemma match_Lam_simps2:
+  "atom n \<sharp> ((S :: 'a :: fs), Lam n s) \<Longrightarrow> match_Lam S (Lam n s) = Some (n, s)"
+  apply (rule_tac t="Lam n s"
+              and s="Lam (new (S, (Lam n s))) ((n \<leftrightarrow> (new (S, (Lam n s)))) \<bullet> s)" in subst)
+  defer
+  apply (subst match_Lam_simps(3))
+  defer
+  apply simp
+*)
+
+(*primrec match_Lam_raw where
+  "match_Lam_raw (S :: atom set) (Var_raw x) = None"
+| "match_Lam_raw S (App_raw x y) = None"
+| "match_Lam_raw S (Lam_raw n t) = (let z = new (S \<union> (fv_lam_raw t - {atom n})) in Some (z, (n \<leftrightarrow> z) \<bullet> t))"
 
 quotient_definition
-  subst ("_ [ _ ::= _ ]" [100,100,100] 100)
-where
-  "subst :: lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" is "subst_raw"
-
-lemmas fv_rsp = quot_respect(10)[simplified]
+  "match_Lam :: (atom set) \<Rightarrow> lam \<Rightarrow> (name \<times> lam) option"
+is match_Lam_raw
 
-lemma subst_rsp_pre1:
-  assumes a: "alpha_lam_raw a b"
-  shows "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)"
-  using a
-  apply (induct a b arbitrary: c y rule: alpha_lam_raw.induct)
-  apply (simp add: equivp_reflp[OF lam_equivp])
-  apply (simp add: alpha_lam_raw.intros)
-  apply (simp only: alphas)
-  apply clarify
-  apply (simp only: subst_raw.simps)
+lemma swap_fresh:
+  assumes a: "fv_lam_raw t \<sharp>* p"
+  shows "alpha_lam_raw (p \<bullet> t) t"
+  using a apply (induct t)
+  apply (simp add: supp_at_base fresh_star_def)
   apply (rule alpha_lam_raw.intros)
-  apply (simp only: alphas)
-  sorry
-
-lemma subst_rsp_pre2:
-  assumes a: "alpha_lam_raw a b"
-  shows "alpha_lam_raw (subst_raw c y a) (subst_raw c y b)"
-  using a
-  apply (induct c arbitrary: a b y)
-  apply (simp add: equivp_reflp[OF lam_equivp])
-  apply (simp add: alpha_lam_raw.intros)
+  apply (metis Rep_name_inverse atom_eqvt atom_name_def fresh_perm)
+  apply (simp)
+  apply (simp only: fresh_star_union)
+  apply clarify
+  apply (rule alpha_lam_raw.intros)
+  apply simp
+  apply simp
   apply simp
   apply (rule alpha_lam_raw.intros)
   sorry
 
 lemma [quot_respect]:
-  "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw"
-  proof (intro fun_relI, simp)
-    fix a b c d :: lam_raw
-    fix y :: name
-    assume a: "alpha_lam_raw a b"
-    assume b: "alpha_lam_raw c d"
-    have c: "alpha_lam_raw (subst_raw a y c) (subst_raw b y c)" using subst_rsp_pre1 a by simp
-    then have d: "alpha_lam_raw (subst_raw b y c) (subst_raw b y d)" using subst_rsp_pre2 b by simp
-    show "alpha_lam_raw (subst_raw a y c) (subst_raw b y d)"
-      using c d equivp_transp[OF lam_equivp] by blast
+  "(op = ===> alpha_lam_raw ===> option_rel (prod_rel op = alpha_lam_raw)) match_Lam_raw match_Lam_raw"
+  proof (intro fun_relI, clarify)
+    fix S t s
+    assume a: "alpha_lam_raw t s"
+    show "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S t) (match_Lam_raw S s)"
+      using a proof (induct t s rule: alpha_lam_raw.induct)
+      case goal1 show ?case by simp
+    next
+      case goal2 show ?case by simp
+    next
+      case (goal3 x t y s)
+      then obtain p where "({atom x}, t) \<approx>gen (\<lambda>x1 x2. alpha_lam_raw x1 x2 \<and>
+                              option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S x1)
+                               (match_Lam_raw S x2)) fv_lam_raw p ({atom y}, s)" ..
+      then have
+        c: "fv_lam_raw t - {atom x} = fv_lam_raw s - {atom y}" and
+        d: "(fv_lam_raw t - {atom x}) \<sharp>* p" and
+        e: "alpha_lam_raw (p \<bullet> t) s" and
+        f: "option_rel (prod_rel op = alpha_lam_raw) (match_Lam_raw S (p \<bullet> t)) (match_Lam_raw S s)" and
+        g: "p \<bullet> {atom x} = {atom y}" unfolding alphas(1) by - (elim conjE, assumption)+
+      let ?z = "new (S \<union> (fv_lam_raw t - {atom x}))"
+      have h: "?z = new (S \<union> (fv_lam_raw s - {atom y}))" using c by simp
+      show ?case
+        unfolding match_Lam_raw.simps Let_def option_rel.simps prod_rel.simps split_conv
+      proof
+        show "?z = new (S \<union> (fv_lam_raw s - {atom y}))" by (fact h)
+      next
+        have "atom y \<sharp> p" sorry
+        have "fv_lam_raw t \<sharp>* ((x \<leftrightarrow> y) \<bullet> p)" sorry
+        then have "alpha_lam_raw (((x \<leftrightarrow> y) \<bullet> p) \<bullet> t) t" using swap_fresh by auto
+        then have "alpha_lam_raw (p \<bullet> t) ((x \<leftrightarrow> y) \<bullet> t)" sorry
+        have "alpha_lam_raw t ((x \<leftrightarrow> y) \<bullet> s)" sorry
+        then have "alpha_lam_raw ((x \<leftrightarrow> ?z) \<bullet> t) ((y \<leftrightarrow> ?z) \<bullet> s)" using eqvts(15) sorry
+        then show "alpha_lam_raw ((x \<leftrightarrow> new (S \<union> (fv_lam_raw t - {atom x}))) \<bullet> t)
+                  ((y \<leftrightarrow> new (S \<union> (fv_lam_raw s - {atom y}))) \<bullet> s)" unfolding h .
+      qed
+    qed
   qed
 
-lemma simp3:
-  "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> alpha_lam_raw (subst_raw (Lam_raw x t) y s) (Lam_raw x (subst_raw t y s))"
-  apply simp
-  apply (rule alpha_lam_raw.intros)
-  apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) -
-                    {atom x})))" in exI)
-  apply (simp only: alphas)
-  apply simp
+lemmas match_Lam_simps = match_Lam_raw.simps[quot_lifted]
+*)
+
+lemma app_some: "match_App x = Some (a, b) \<Longrightarrow> x = App a b"
+by (induct x rule: lam.induct) (simp_all add: match_App_simps)
+
+lemma lam_some: "match_Lam S x = Some (z, s) \<Longrightarrow> x = Lam z s \<and> atom z \<sharp> S"
+  apply (induct x rule: lam.induct)
+  apply (simp_all add: match_Lam_simps)
+  apply (thin_tac "match_Lam S lam = Some (z, s) \<Longrightarrow> lam = Lam z s \<and> atom z \<sharp> S")
+  apply (simp add: match_Lam_def)
+  apply (subgoal_tac "\<exists>n s. Lam name lam = Lam n s")
+  prefer 2
+  apply auto[1]
+  apply (simp add: Let_def)
+  apply (thin_tac "\<exists>n s. Lam name lam = Lam n s")
+  apply clarify
+  apply (rule conjI)
+  apply (rule_tac t="THE s. Lam name lam = Lam (new (S, Lam name lam)) s" and
+                  s="(name \<leftrightarrow> (new (S, Lam name lam))) \<bullet> lam" in subst)
+  defer
+  apply (simp add: lam.eq_iff)
+  apply (rule_tac x="(name \<leftrightarrow> (new (S, Lam name lam)))" in exI)
+  apply (simp add: alphas)
+  apply (simp add: eqvts)
+  apply (rule conjI)
   sorry
 
-lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars]
-  simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars]
+function subst where
+"subst v s t = (
+  case match_Var t of Some n \<Rightarrow> if n = v then s else Var n | None \<Rightarrow>
+  case match_App t of Some (l, r) \<Rightarrow> App (subst v s l) (subst v s r) | None \<Rightarrow>
+  case match_Lam (v,s) t of Some (n, t) \<Rightarrow> Lam n (subst v s t) | None \<Rightarrow> undefined)"
+by pat_completeness auto
+
+termination apply (relation "measure (\<lambda>(_, _, t). size t)")
+  apply auto[1]
+  apply (case_tac a) apply simp
+  apply (frule lam_some) apply simp
+  apply (case_tac a) apply simp
+  apply (frule app_some) apply simp
+  apply (case_tac a) apply simp
+  apply (frule app_some) apply simp
+done
+
+lemmas lam_exhaust = lam_raw.exhaust[quot_lifted]
+
+lemma subst_eqvt:
+  "p \<bullet> (subst v s t) = subst (p \<bullet> v) (p \<bullet> s) (p \<bullet> t)"
+  proof (induct v s t rule: subst.induct)
+    case (1 v s t)
+    show ?case proof (cases t rule: lam_exhaust)
+      fix n
+      assume "t = Var n"
+      then show ?thesis by (simp add: match_Var_simps)
+    next
+      fix l r
+      assume "t = App l r"
+      then show ?thesis
+        apply (simp only:)
+        apply (subst subst.simps)
+        apply (subst match_Var_simps)
+        apply (simp only: option.cases)
+        apply (subst match_App_simps)
+        apply (simp only: option.cases)
+        apply (simp only: prod.cases)
+        apply (simp only: lam.perm)
+        apply (subst (3) subst.simps)
+        apply (subst match_Var_simps)
+        apply (simp only: option.cases)
+        apply (subst match_App_simps)
+        apply (simp only: option.cases)
+        apply (simp only: prod.cases)
+        apply (subst 1(2)[of "(l, r)" "l" "r"])
+        apply (simp add: match_Var_simps)
+        apply (simp add: match_App_simps)
+        apply (rule refl)
+        apply (subst 1(3)[of "(l, r)" "l" "r"])
+        apply (simp add: match_Var_simps)
+        apply (simp add: match_App_simps)
+        apply (rule refl)
+        apply (rule refl)
+        done
+    next
+      fix n t'
+      assume "t = Lam n t'"
+      then show ?thesis
+        apply (simp only: )
+        apply (simp only: lam.perm)
+        apply (subst subst.simps)
+        apply (subst match_Var_simps)
+        apply (simp only: option.cases)
+        apply (subst match_App_simps)
+        apply (simp only: option.cases)
+        apply (rule_tac t="Lam n t'" and s="Lam (new ((v, s), Lam n t')) ((n \<leftrightarrow> new ((v, s), Lam n t')) \<bullet> t')" in subst)
+        defer
+        apply (subst match_Lam_simps)
+        defer
+        apply (simp only: option.cases)
+        apply (simp only: prod.cases)
+        apply (subst (2) subst.simps)
+        apply (subst match_Var_simps)
+        apply (simp only: option.cases)
+        apply (subst match_App_simps)
+        apply (simp only: option.cases)
+        apply (rule_tac t="Lam (p \<bullet> n) (p \<bullet> t')" and s="Lam (new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) (((p \<bullet> n) \<leftrightarrow> new ((p \<bullet> v, p \<bullet> s), Lam (p \<bullet> n) (p \<bullet> t'))) \<bullet> t')" in subst)
+        defer
+        apply (subst match_Lam_simps)
+        defer
+        apply (simp only: option.cases)
+        apply (simp only: prod.cases)
+        apply (simp only: lam.perm)
+        thm 1(1)
+        sorry
+    qed
+  qed
+
+lemma subst_proper_eqs:
+  "subst y s (Var x) = (if x = y then s else (Var x))"
+  "subst y s (App l r) = App (subst y s l) (subst y s r)"
+  "atom x \<sharp> (t, s) \<Longrightarrow> subst y s (Lam x t) = Lam x (subst y s t)"
+  apply (subst subst.simps)
+  apply (simp only: match_Var_simps)
+  apply (simp only: option.simps)
+  apply (subst subst.simps)
+  apply (simp only: match_App_simps)
+  apply (simp only: option.simps)
+  apply (simp only: prod.simps)
+  apply (simp only: match_Var_simps)
+  apply (simp only: option.simps)
+  apply (subst subst.simps)
+  apply (simp only: match_Var_simps)
+  apply (simp only: option.simps)
+  apply (simp only: match_App_simps)
+  apply (simp only: option.simps)
+  apply (rule_tac t="Lam x t" and s="Lam (new ((y, s), Lam x t)) ((x \<leftrightarrow> new ((y, s), Lam x t)) \<bullet> t)" in subst)
+  defer
+  apply (subst match_Lam_simps)
+  defer
+  apply (simp only: option.simps)
+  apply (simp only: prod.simps)
+  sorry
 
 end
 
diff -r 9fb315392493 -r 8732ff59068b Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Wed May 26 15:37:56 2010 +0200
@@ -152,6 +152,121 @@
   apply auto
   done
 
+fun
+  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+where
+  "lookup [] n = Var n"
+| "lookup ((p, s) # t) n = (if p = n then s else lookup t n)"
+
+locale subst_loc =
+fixes
+    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
+and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
+assumes
+    s1: "subst \<theta> (Var n) = lookup \<theta> n"
+and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)"
+and s3: "fset_to_set (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
+begin
+
+lemma subst_ty:
+  assumes x: "atom x \<sharp> t"
+  shows "subst [(x, S)] t = t"
+  using x
+  apply (induct t rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
+  by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base)
+
+lemma subst_tyS:
+  shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T"
+  apply (rule strong_induct[of
+    "\<lambda>a t. True" "\<lambda>(x, S) T. (atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T)" _ "t" "(x, S)", simplified])
+  apply clarify
+  apply (subst s3)
+  apply (simp add: fresh_star_def fresh_Cons fresh_Nil)
+  apply (subst subst_ty)
+  apply (simp_all add: fresh_star_prod_elim)
+  apply (drule fresh_star_atom)
+  apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
+  apply (subgoal_tac "atom a \<notin> fset_to_set (fmap atom fset)")
+  apply blast
+  apply (metis supp_finite_atom_set finite_fset)
+  done
+
+lemma subst_lemma_pre:
+  "z \<sharp> (N,L) \<longrightarrow> z \<sharp> (subst [(y, L)] N)"
+  apply (induct N rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
+  apply (simp add: s1)
+  apply (auto simp add: fresh_Pair)
+  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])[3]
+  apply (simp add: s2)
+  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
+  done
+
+lemma substs_lemma_pre:
+  "atom z \<sharp> (N,L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N)"
+  apply (rule strong_induct[of
+    "\<lambda>a t. True" "\<lambda>(z, y, L) N. (atom z \<sharp> (N, L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N))" _ _ "(z, y, L)", simplified])
+  apply clarify
+  apply (subst s3)
+  apply (simp add: fresh_star_def fresh_Cons fresh_Nil fresh_Pair)
+  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
+  apply clarify
+  apply (drule fresh_star_atom)
+  apply (drule fresh_star_atom)
+  apply (simp add: fresh_def)
+  apply (simp only: ty_tys.fv[simplified ty_tys.supp])
+  apply (subgoal_tac "atom a \<notin> supp (subst [(aa, b)] t)")
+  apply blast
+  apply (subgoal_tac "atom a \<notin> supp t")
+  apply (fold fresh_def)[1]
+  apply (rule mp[OF subst_lemma_pre])
+  apply (simp add: fresh_Pair)
+  apply (subgoal_tac "atom a \<notin> (fset_to_set (fmap atom fset))")
+  apply blast
+  apply (metis supp_finite_atom_set finite_fset)
+  done
+
+lemma subst_lemma:
+  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
+    subst [(y, L)] (subst [(x, N)] M) =
+    subst [(x, (subst [(y, L)] N))] (subst [(y, L)] M)"
+  apply (induct M rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
+  apply (simp_all add: s1 s2)
+  apply clarify
+  apply (subst (2) subst_ty)
+  apply simp_all
+  done
+
+lemma substs_lemma:
+  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
+    substs [(y, L)] (substs [(x, N)] M) =
+    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)"
+  apply (rule strong_induct[of
+    "\<lambda>a t. True" "\<lambda>(x, y, N, L) M. x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
+    substs [(y, L)] (substs [(x, N)] M) =
+    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" _ _ "(x, y, N, L)", simplified])
+  apply clarify
+  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (rule ballI)
+  apply (rule mp[OF subst_lemma_pre])
+  apply (simp add: fresh_Pair)
+  apply (subst subst_lemma)
+  apply simp_all
+  done
+
+end
+
 (* PROBLEM:
 Type schemes with separate datatypes
 
diff -r 9fb315392493 -r 8732ff59068b Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal/NewParser.thy	Wed May 26 15:37:56 2010 +0200
@@ -12,7 +12,7 @@
 ML {* 
 (* nominal datatype parser *)
 local
-  structure P = OuterParse;
+  structure P = Parse;
   structure S = Scan
 
   fun triple1 ((x, y), z) = (x, y, z)
@@ -21,9 +21,9 @@
   fun tswap (((x, y), z), u) = (x, y, u, z)
 in
 
-val _ = OuterKeyword.keyword "bind"
-val _ = OuterKeyword.keyword "bind_set"
-val _ = OuterKeyword.keyword "bind_res"
+val _ = Keyword.keyword "bind"
+val _ = Keyword.keyword "bind_set"
+val _ = Keyword.keyword "bind_res"
 
 val anno_typ = S.option (P.name --| P.$$$ "::") -- P.typ
 
@@ -42,7 +42,7 @@
 
 (* binding function parser *)
 val bnfun_parser = 
-  S.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([], [])
+  S.optional (P.$$$ "binder" |-- P.fixes -- Parse_Spec.where_alt_specs) ([], [])
 
 (* main parser *)
 val main_parser =
@@ -715,7 +715,7 @@
 
 (* Command Keyword *)
 
-val _ = OuterSyntax.local_theory "nominal_datatype" "test" OuterKeyword.thy_decl
+val _ = Outer_Syntax.local_theory "nominal_datatype" "test" Keyword.thy_decl
   (main_parser >> nominal_datatype2_cmd)
 *}
 
diff -r 9fb315392493 -r 8732ff59068b Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Nominal/Nominal2_FSet.thy	Wed May 26 15:37:56 2010 +0200
@@ -103,5 +103,20 @@
   apply (simp add: supp_at_base)
   done
 
+lemma fresh_star_atom:
+  "fset_to_set s \<sharp>* (a :: _ :: at_base) \<Longrightarrow> atom a \<sharp> fset_to_set s"
+  apply (induct s)
+  apply (simp add: fresh_set_empty)
+  apply simp
+  apply (unfold fresh_def)
+  apply (simp add: supp_atom_insert)
+  apply (rule conjI)
+  apply (unfold fresh_star_def)
+  apply simp
+  apply (unfold fresh_def)
+  apply (simp add: supp_at_base supp_atom)
+  apply clarify
+  apply auto
+  done
 
 end
diff -r 9fb315392493 -r 8732ff59068b Paper/Paper.thy
--- a/Paper/Paper.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Paper/Paper.thy	Wed May 26 15:37:56 2010 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Nominal/Test" "LaTeXsugar"
+imports "../Nominal/Test" "../Nominal/FSet" "LaTeXsugar"
 begin
 
 consts
@@ -85,7 +85,7 @@
   also there one would like to bind multiple variables at once.
 
   Binding multiple variables has interesting properties that cannot be captured
-  easily by iterating single binders. For example in case of type-schemes we do not
+  easily by iterating single binders. For example in the case of type-schemes we do not
   want to make a distinction about the order of the bound variables. Therefore
   we would like to regard the following two type-schemes as alpha-equivalent
   %
@@ -183,10 +183,10 @@
   where the notation @{text "[_]._"} indicates that the list of @{text "x\<^isub>i"}
   becomes bound in @{text s}. In this representation the term 
   \mbox{@{text "\<LET> [x].s [t\<^isub>1, t\<^isub>2]"}} is a perfectly legal
-  instance, but the lengths of two lists do not agree. To exclude such terms, 
+  instance, but the lengths of the two lists do not agree. To exclude such terms, 
   additional predicates about well-formed
   terms are needed in order to ensure that the two lists are of equal
-  length. This can result into very messy reasoning (see for
+  length. This can result in very messy reasoning (see for
   example~\cite{BengtsonParow09}). To avoid this, we will allow type
   specifications for $\mathtt{let}$s as follows
   %
@@ -220,7 +220,7 @@
   inspired by the syntax of the Ott-tool \cite{ott-jfp}.
 
   However, we will not be able to cope with all specifications that are
-  allowed by Ott. One reason is that Ott lets the user to specify ``empty'' 
+  allowed by Ott. One reason is that Ott lets the user specify ``empty'' 
   types like
 
   \begin{center}
@@ -556,7 +556,7 @@
  
   \noindent
   From property \eqref{equivariancedef} and the definition of @{text supp}, we 
-  can be easily deduce that equivariant functions have empty support. There is
+  can easily deduce that equivariant functions have empty support. There is
   also a similar notion for equivariant relations, say @{text R}, namely the property
   that
   %
@@ -593,7 +593,7 @@
 
   Most properties given in this section are described in detail in \cite{HuffmanUrban10}
   and of course all are formalised in Isabelle/HOL. In the next sections we will make 
-  extensively use of these properties in order to define alpha-equivalence in 
+  extensive use of these properties in order to define alpha-equivalence in 
   the presence of multiple binders.
 *}
 
@@ -623,7 +623,7 @@
   variables; moreover there must be a permutation @{text p} such that {\it
   ii)} @{text p} leaves the free variables of @{text x} and @{text y} unchanged, but
   {\it iii)} ``moves'' their bound names so that we obtain modulo a relation,
-  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require {\it iv)} that
+  say \mbox{@{text "_ R _"}}, two equivalent terms. We also require that {\it iv)}
   @{text p} makes the sets of abstracted atoms @{text as} and @{text bs} equal. The
   requirements {\it i)} to {\it iv)} can be stated formally as follows:
   %
@@ -638,7 +638,7 @@
   \end{equation}
 
   \noindent
-  Note that this relation is dependent on the permutation @{text
+  Note that this relation depends on the permutation @{text
   "p"}. Alpha-equivalence between two pairs is then the relation where we
   existentially quantify over this @{text "p"}. Also note that the relation is
   dependent on a free-variable function @{text "fv"} and a relation @{text
@@ -692,20 +692,20 @@
   \noindent
   Now recall the examples shown in \eqref{ex1}, \eqref{ex2} and
   \eqref{ex3}. It can be easily checked that @{text "({x, y}, x \<rightarrow> y)"} and
-  @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to $\approx_{\textit{set}}$ and
-  $\approx_{\textit{res}}$ by taking @{text p} to be the swapping @{term "(x \<rightleftharpoons>
-  y)"}. In case of @{text "x \<noteq> y"}, then @{text "([x, y], x \<rightarrow> y)"}
-  $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"} since there is no permutation
-  that makes the lists @{text "[x, y]"} and @{text "[y, x]"} equal, and also
-  leaves the type \mbox{@{text "x \<rightarrow> y"}} unchanged. Another example is
-  @{text "({x}, x)"} $\approx_{\textit{res}}$ @{text "({x, y}, x)"} which holds by 
-  taking @{text p} to be the
-  identity permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
-  $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no permutation 
-  that makes the
-  sets @{text "{x}"} and @{text "{x, y}"} equal (similarly for $\approx_{\textit{list}}$).
-  It can also relatively easily be shown that all tree notions of alpha-equivalence
-  coincide, if we only abstract a single atom. 
+  @{text "({y, x}, y \<rightarrow> x)"} are alpha-equivalent according to
+  $\approx_{\textit{set}}$ and $\approx_{\textit{res}}$ by taking @{text p} to
+  be the swapping @{term "(x \<rightleftharpoons> y)"}. In case of @{text "x \<noteq> y"}, then @{text
+  "([x, y], x \<rightarrow> y)"} $\not\approx_{\textit{list}}$ @{text "([y, x], x \<rightarrow> y)"}
+  since there is no permutation that makes the lists @{text "[x, y]"} and
+  @{text "[y, x]"} equal, and also leaves the type \mbox{@{text "x \<rightarrow> y"}}
+  unchanged. Another example is @{text "({x}, x)"} $\approx_{\textit{res}}$
+  @{text "({x, y}, x)"} which holds by taking @{text p} to be the identity
+  permutation.  However, if @{text "x \<noteq> y"}, then @{text "({x}, x)"}
+  $\not\approx_{\textit{set}}$ @{text "({x, y}, x)"} since there is no
+  permutation that makes the sets @{text "{x}"} and @{text "{x, y}"} equal
+  (similarly for $\approx_{\textit{list}}$).  It can also relatively easily be
+  shown that all three notions of alpha-equivalence coincide, if we only
+  abstract a single atom.
 
   In the rest of this section we are going to introduce three abstraction 
   types. For this we define 
@@ -941,16 +941,16 @@
   of the specification (the corresponding alpha-equivalence will differ). We will 
   show this later with an example.
   
-  There are some restrictions we need to impose: First, a body can only occur
-  in \emph{one} binding clause of a term constructor. For binders we
-  distinguish between \emph{shallow} and \emph{deep} binders.  Shallow binders
-  are just labels. The restriction we need to impose on them is that in case
-  of \isacommand{bind\_set} and \isacommand{bind\_res} the labels must either
-  refer to atom types or to sets of atom types; in case of \isacommand{bind}
-  the labels must refer to atom types or lists of atom types. Two examples for
-  the use of shallow binders are the specification of lambda-terms, where a
-  single name is bound, and type-schemes, where a finite set of names is
-  bound:
+  There are some restrictions we need to impose on binding clasues: First, a
+  body can only occur in \emph{one} binding clause of a term constructor. For
+  binders we distinguish between \emph{shallow} and \emph{deep} binders.
+  Shallow binders are just labels. The restriction we need to impose on them
+  is that in case of \isacommand{bind\_set} and \isacommand{bind\_res} the
+  labels must either refer to atom types or to sets of atom types; in case of
+  \isacommand{bind} the labels must refer to atom types or lists of atom
+  types. Two examples for the use of shallow binders are the specification of
+  lambda-terms, where a single name is bound, and type-schemes, where a finite
+  set of names is bound:
 
   \begin{center}
   \begin{tabular}{@ {}cc@ {}}
@@ -974,7 +974,7 @@
   \noindent
   Note that for @{text lam} it does not matter which binding mode we use. The
   reason is that we bind only a single @{text name}. However, having
-  \isacommand{bind\_set} or \isacommand{bind} in the second case makes again a
+  \isacommand{bind\_set} or \isacommand{bind} in the second case makes a
   difference to the semantics of the specification. Note also that in
   these specifications @{text "name"} refers to an atom type, and @{text
   "fset"} to the type of finite sets.
@@ -1119,7 +1119,7 @@
   term-constructors so that binders and their bodies are next to each other will 
   result in inadequate representations. Therefore we will first
   extract datatype definitions from the specification and then define 
-  expicitly an alpha-equivalence relation over them.
+  explicitly an alpha-equivalence relation over them.
 
 
   The datatype definition can be obtained by stripping off the 
@@ -1152,7 +1152,7 @@
   @{text "p \<bullet> (C z\<^isub>1 \<dots> z\<^isub>n) = C (p \<bullet> z\<^isub>1) \<dots> (p \<bullet> z\<^isub>n)"}
   \end{equation}
   
-  The first non-trivial step we have to perform is the generation free-variable 
+  The first non-trivial step we have to perform is the generation of free-variable 
   functions from the specifications. For atomic types we define the auxilary
   free variable functions:
 
@@ -1455,7 +1455,7 @@
 
   \begin{proof} 
   The proof is by mutual induction over the definitions. The non-trivial
-  cases involve premises build up by $\approx_{\textit{set}}$, 
+  cases involve premises built up by $\approx_{\textit{set}}$, 
   $\approx_{\textit{res}}$ and $\approx_{\textit{list}}$. They 
   can be dealt with as in Lemma~\ref{alphaeq}.
   \end{proof}
@@ -1526,7 +1526,7 @@
   \end{center} 
 
   \noindent
-  for all @{text "y\<^isub>i"} wherby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties
+  for all @{text "y\<^isub>i"} whereby the variables @{text "P\<^bsub>ty\<AL>\<^esub>\<^isub>i"} stand for properties
   defined over the types @{text "ty\<AL>\<^isub>1 \<dots> ty\<AL>\<^isub>n"}. The premises of 
   these induction principles look
   as follows
@@ -1540,7 +1540,7 @@
   Next we lift the permutation operations defined in \eqref{ceqvt} for
   the raw term-constructors @{text "C"}. These facts contain, in addition 
   to the term-constructors, also permutation operations. In order to make the 
-  lifting to go through, 
+  lifting go through, 
   we have to know that the permutation operations are respectful 
   w.r.t.~alpha-equivalence. This amounts to showing that the 
   alpha-equivalence relations are equivariant, which we already established 
@@ -1567,7 +1567,7 @@
 
   \noindent
   which can be established by induction on @{text "\<approx>ty"}. Whereas the first
-  property is always true by the way how we defined the free-variable
+  property is always true by the way we defined the free-variable
   functions for types, the second and third do \emph{not} hold in general. There is, in principle, 
   the possibility that the user defines @{text "bn\<^isub>k"} so that it returns an already bound
   variable. Then the third property is just not true. However, our 
@@ -1864,7 +1864,7 @@
   \end{center}
 
   \noindent
-  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we are can equally
+  So instead of proving @{text "P\<^bsub>trm\<^esub> c (q \<bullet> Let p t\<^isub>1 t\<^isub>2)"}, we can equally
   establish
 
   \begin{center}
@@ -1894,7 +1894,7 @@
   we can establish our original goals, namely @{text "P\<^bsub>trm\<^esub> c t"} and \mbox{@{text "P\<^bsub>pat\<^esub> c p"}}.
   This completes the proof showing that the strong induction principle derives from
   the weak induction principle. For the moment we can derive the difficult cases of 
-  the strong induction principles only by hand, but they are very schematically 
+  the strong induction principles only by hand, but they are very schematic 
   so that with little effort we can even derive them for 
   Core-Haskell given in Figure~\ref{nominalcorehas}. 
 *}
diff -r 9fb315392493 -r 8732ff59068b Paper/ROOT.ML
--- a/Paper/ROOT.ML	Wed May 26 15:34:54 2010 +0200
+++ b/Paper/ROOT.ML	Wed May 26 15:37:56 2010 +0200
@@ -1,3 +1,3 @@
 quick_and_dirty := true;
-no_document use_thys ["LaTeXsugar"];
+no_document use_thys ["LaTeXsugar", "../Nominal/FSet"];
 use_thys ["Paper"];
\ No newline at end of file
diff -r 9fb315392493 -r 8732ff59068b Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Wed May 26 15:34:54 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Wed May 26 15:37:56 2010 +0200
@@ -1,12 +1,32 @@
 (*<*)
 theory Paper
-imports "Quotient" 
+imports "Quotient"
         "LaTeXsugar"
 begin
 
 notation (latex output)
+  rel_conj ("_ OOO _" [53, 53] 52)
+and
+  fun_map ("_ ---> _" [51, 51] 50)
+and
   fun_rel ("_ ===> _" [51, 51] 50)
 
+ML {*
+fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n;
+fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
+  let
+    val concl =
+      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
+  in
+    case concl of (_ $ l $ r) => proj (l, r)
+    | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
+  end);
+*}
+setup {*
+  Term_Style.setup "rhs1" (style_lhs_rhs (nth_conj 0)) #>
+  Term_Style.setup "rhs2" (style_lhs_rhs (nth_conj 1)) #>
+  Term_Style.setup "rhs3" (style_lhs_rhs (nth_conj 2))
+*}
 (*>*)
 
 section {* Introduction *}
@@ -27,6 +47,8 @@
   For example the integers in Isabelle/HOL are constructed by a quotient construction over 
   the type @{typ "nat \<times> nat"} and the equivalence relation
 
+% I would avoid substraction for natural numbers.
+
   @{text [display] "(n\<^isub>1, n\<^isub>2) \<approx> (m\<^isub>1, m\<^isub>2) \<equiv> n\<^isub>1 - n \<^isub>2 = m\<^isub>1 - m \<^isub>2"}
 
   \noindent
@@ -53,8 +75,9 @@
   surprising, none of them can deal compositions of quotients, for example with 
   lifting theorems about @{text "concat"}:
 
-  @{text [display] "concat definition"}
-  
+  @{thm concat.simps(1)}\\
+  @{thm concat.simps(2)[no_vars]}
+
   \noindent
   One would like to lift this definition to the operation
   
@@ -84,12 +107,9 @@
   \item We allow lifting only some occurrences of quotiented
     types. Rsp/Prs extended. (used in nominal)
 
-  \item We regularize more thanks to new lemmas. (inductions in
-    nominal).
-
   \item The quotient package is very modular. Definitions can be added
     separately, rsp and prs can be proved separately and theorems can
-    be lifted on a need basis. (useful with type-classes).
+    be lifted on a need basis. (useful with type-classes). 
 
   \item Can be used both manually (attribute, separate tactics,
     rsp/prs databases) and programatically (automated definition of
@@ -101,18 +121,73 @@
 
 section {* Quotient Type*}
 
+
+
 text {*
-  Defintion of quotient,
+  In this section we present the definitions of a quotient that follow
+  those by Homeier, the proofs can be found there.
+
+  \begin{definition}[Quotient]
+  A relation $R$ with an abstraction function $Abs$
+  and a representation function $Rep$ is a \emph{quotient}
+  if and only if:
 
-  Equivalence,
+  \begin{enumerate}
+  \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
+  \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
+  \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
+  \end{enumerate}
+
+  \end{definition}
 
-  Relation map and function map
+  \begin{definition}[Relation map and function map]
+  @{thm fun_rel_def[no_vars]}\\
+  @{thm fun_map_def[no_vars]}
+  \end{definition}
+
+  The main theorems for building higher order quotients is:
+  \begin{lemma}[Function Quotient]
+  If @{thm (prem 1) fun_quotient[no_vars]} and @{thm (prem 2) fun_quotient[no_vars]}
+  then @{thm (concl) fun_quotient[no_vars]}
+  \end{lemma}
+
 *}
 
 section {* Constants *}
 
+(* Describe what containers are? *)
+
 text {*
-  Rep and Abs, Rsp and Prs
+  \begin{definition}[Composition of Relations]
+  @{abbrev "rel_conj R1 R2"}
+  \end{definition}
+
+  The first operation that we describe is the generation of
+  aggregate Abs or Rep function for two given compound types.
+  This operation will be used for the constant defnitions
+  and for the translation of theorems statements. It relies on
+  knowing map functions and relation functions for container types.
+  It follows the following algorithm:
+
+  \begin{itemize}
+  \item For equal types or free type variables return identity.
+
+  \item For function types recurse, change the Rep/Abs flag to
+     the opposite one for the domain type and compose the
+     results with @{term "fun_map"}.
+
+  \item For equal type constructors use the appropriate map function
+     applied to the results for the arguments.
+
+  \item For unequal type constructors are unequal, we look in the
+    quotients information for a raw type quotient type pair that
+    matches the given types. We apply the environment to the arguments
+    and recurse composing it with the aggregate map function.
+  \end{itemize}
+
+
+
+  Rsp and Prs
 *}
 
 section {* Lifting Theorems *}
diff -r 9fb315392493 -r 8732ff59068b Quotient-Paper/document/llncs.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Quotient-Paper/document/llncs.cls	Wed May 26 15:37:56 2010 +0200
@@ -0,0 +1,1189 @@
+% LLNCS DOCUMENT CLASS -- version 2.13 (28-Jan-2002)
+% 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}[2002/01/28 v2.13
+^^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@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
+
+\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 Key words:}}
+\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}
+
+\def\hyperhrefextend{\ifx\hyper@anchor\@undefined\else
+{chapter.\thechapter}\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{\@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=\z@ %15\p@
+ \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{%
+  \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}%
+}
+\def\homedir{\~{ }}
+
+\def\subtitle#1{\gdef\@subtitle{#1}}
+\clearheadinfo
+
+\renewcommand\maketitle{\newpage
+  \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
+%    \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
+  {\global\@namedef{the#1}{\@nameuse{the#2}}%
+  \expandafter\xdef\csname #1name\endcsname{#3}%
+  \global\@namedef{#1}{\@spthm{#2}{\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 9fb315392493 -r 8732ff59068b Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Wed May 26 15:34:54 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Wed May 26 15:37:56 2010 +0200
@@ -1,4 +1,5 @@
-\documentclass{svjour3}
+%\documentclass{svjour3}
+\documentclass{llncs}
 \usepackage{times}
 \usepackage{isabelle}
 \usepackage{isabellesym}