--- 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
*}
--- 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)));
--- 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;
--- 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
--- 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
--- 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)
*}
--- 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
--- 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}.
*}
--- 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
--- 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 *}
--- /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
--- 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}