# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1454667370 0
# Node ID a33d3040bf7e10c9d809d71dcd6dd4a87b40e87e
# Parent  5b01f7c233f87ddd42063ee19257f98a41ff1275
started a paper and moved cruft to Attic

diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/Chap03.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Chap03.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,295 @@
+theory Chap03
+imports Main
+begin
+
+(* 2.5.6 Case Study: Boolean Expressions *)
+
+datatype boolex = Const bool | Var nat | Neg boolex
+| And boolex boolex
+
+primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
+"value2 (Const b)  env = b" |
+"value2 (Var x)    env = env x" |
+"value2 (Neg b)    env = (\<not> value2 b env)" |
+"value2 (And b c)  env = (value2 b env \<and> value2 c env)"
+
+value "Const true"
+value "Var (Suc(0))"
+value "value2 (Const False) (\<lambda>x. False)"
+value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)"
+value "value2 (Var 11) (\<lambda>x. True )"
+
+definition
+  "en1 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"
+  
+abbreviation
+  "en2 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"
+  
+value "value2 (And (Var 10) (Var 11)) en2"
+
+lemma "value2 (And (Var 10) (Var 11)) en2 = True"
+apply(simp)
+done
+
+datatype ifex = 
+  CIF bool 
+| VIF nat 
+| IF ifex ifex ifex
+
+primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
+"valif (CIF b)    env = b" |
+"valif (VIF x)    env = env x" |
+"valif (IF b t e) env = (if valif b env then valif t env else valif e env)"
+
+abbreviation "vif1 \<equiv> valif (CIF False) (\<lambda>x. False)"
+abbreviation "vif2 \<equiv> valif (VIF 11) (\<lambda>x. False)"
+abbreviation "vif3 \<equiv> valif (VIF 13) (\<lambda>x. True)"
+
+value "valif (CIF False) (\<lambda>x. False)"
+value "valif (VIF 11) (\<lambda>x. True)"
+value "valif (IF (CIF False) (CIF True) (CIF True))"
+
+primrec bool2if :: "boolex \<Rightarrow> ifex" where
+"bool2if (Const b)  = CIF b" |
+"bool2if (Var x)    = VIF x" |
+"bool2if (Neg b)    = IF (bool2if b) (CIF False) (CIF True)" |
+"bool2if (And b c)  = IF (bool2if b) (bool2if c) (CIF False)"
+
+lemma "valif (bool2if b) env = value2 b env"
+apply(induct_tac b)
+apply(auto)
+done
+
+primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where
+"normif (CIF b)     t e = IF (CIF b) t e" |
+"normif (VIF x)     t e = IF (VIF x) t e" |
+"normif (IF b t e)  u f = normif b (normif t u f) (normif e u f)"
+
+primrec norm :: "ifex \<Rightarrow> ifex" where
+"norm (CIF b)     = CIF b" |
+"norm (VIF x)     = VIF x" |
+"norm (IF b t e)  = normif b (norm t) (norm e)"  
+
+(***************   CHAPTER-3   ********************************)
+
+lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
+apply simp
+done
+
+lemma "\<forall> x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"
+apply (simp (no_asm))
+done
+
+definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
+"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"
+
+lemma "xor A (\<not>A)"
+apply(simp only: xor_def)
+apply(simp add: xor_def)
+done
+
+lemma "(let xs = [] in xs@ys@xs) = ys"
+apply(simp only: Let_def)
+apply(simp add: Let_def)
+done
+
+(* 3.1.8 Conditioal Simplification Rules  *)
+
+lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
+using [[simp_trace=true]]
+apply(case_tac xs)
+apply(simp)
+apply(simp)
+done
+
+lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"
+apply(case_tac xs)
+using [[simp_trace=true]]
+apply(simp)
+apply(simp)
+done
+
+(* 3.1.9 Automatic Case Splits  *)
+
+lemma "\<forall> xs. if xs = [] then rev xs = [] else rev xs \<noteq> []"
+apply(split split_if)
+apply(simp)
+done
+
+lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"
+apply(split list.split)
+apply(simp split: list.split)
+done
+
+lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
+apply(split split_if_asm)
+apply(simp)
+apply(auto)
+done
+
+(* 3.2 Induction Heuristics  *)
+
+primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"itrev [] ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
+
+lemma "itrev xs [] = rev xs"
+apply(induct_tac xs)
+apply(simp)
+apply(auto)
+oops
+
+lemma "itrev xs ys = rev xs @ ys"
+apply(induct_tac xs)
+apply(simp_all)
+oops
+
+lemma "\<forall> ys. itrev xs ys = rev xs @ ys"
+apply(induct_tac xs)
+apply(simp)
+apply(simp)
+done
+
+primrec add1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add1 m 0 = m" |
+"add1 m (Suc n) = add1 (Suc m) n"
+
+primrec add2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add2 m 0 = m" |
+"add2 m (Suc n) = Suc (add2 m n)"
+
+value "add1 1 3"
+value "1 + 3"
+
+lemma abc [simp]: "add1 m 0 = m"
+apply(induction m)
+apply(simp)
+apply(simp)
+done
+
+lemma abc2: "\<forall>m. add1 m n = m + n"
+apply(induction n)
+apply(simp)
+apply(simp del: add1.simps)
+apply(simp (no_asm) only: add1.simps)
+apply(simp only: )
+apply(simp)
+done
+
+thm abc2
+
+lemma abc3: "add1 m n = m + n"
+apply(induction n arbitrary: m)
+apply(simp)
+apply(simp del: add1.simps)
+apply(simp (no_asm) only: add1.simps)
+apply(simp only: )
+done
+
+thm abc3
+
+lemma abc4: "add1 m n = add2 m n"
+apply(induction n arbitrary: m)
+apply(simp)
+apply(simp add: abc3)
+done
+
+find_theorems "_ \<and> _ "
+
+(* added anottest *)
+
+lemma abc5: "add2 m n = m + n"
+apply(induction n)
+apply(simp)
+apply(simp)
+done
+
+
+(* 3.3 Case Study: Compiling Expressions  *)
+
+type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
+datatype ('a, 'v)expr = 
+  Cex 'v
+| Vex 'a
+| Bex "'v binop" "('a,'v)expr" "('a,'v)expr"
+
+primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where
+"value (Cex v) env = v" |
+"value (Vex a) env = env a" |
+"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
+
+value "value (Cex a) (\<lambda>x. True)"
+
+datatype ('a,'v)instr = 
+  Const 'v
+| Load 'a
+| Apply "'v binop"
+
+primrec exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list" where
+"exec [] s vs = vs" |
+"exec (i#is) s vs = (case i of
+    Const v \<Rightarrow> exec is s (v#vs)
+  | Load a \<Rightarrow> exec is s ((s a)#vs)
+  | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"
+  
+primrec compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" where
+"compile (Cex v) = [Const v]" |
+"compile (Vex a) = [Load a]" |
+"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"
+
+theorem "exec (compile e) s [] = [value e s]"
+(*the theorem needs to be generalized*)
+oops
+
+(*more generalized theorem*)
+theorem "\<forall> vs. exec (compile e) s vs = (value e s) # vs"
+apply(induct_tac e)
+apply(simp)
+apply(simp)
+oops
+
+lemma exec_app[simp]: "\<forall> vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"
+apply(induct_tac xs)
+apply(simp)
+apply(simp)
+apply(simp split: instr.split)
+done
+
+(* 3.4 Advanced Datatypes  *)
+
+datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" 
+                | Sum "'a aexp" "'a aexp"
+                | Diff "'a aexp" "'a aexp"
+                | Var 'a
+                | Num nat
+and      'a bexp = Less "'a aexp" "'a aexp"
+                | And "'a bexp" "'a bexp"
+                | Neg "'a bexp"
+                
+(*  Total Recursive Functions: Fun  *)
+(*  3.5.1 Definition    *)
+
+fun fib :: "nat \<Rightarrow> nat" where
+"fib 0 = 0" |
+"fib (Suc 0) = 1" |
+"fib (Suc(Suc x)) = fib x + fib (Suc x)"
+
+value "fib (Suc(Suc(Suc(Suc(Suc 0)))))"
+
+fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"sep a [] = []" |
+"sep a [x] = [x]" |
+"sep a (x#y#zs) = x # a # sep a (y#zs)"
+
+fun last :: "'a list \<Rightarrow> 'a" where
+"last [x] = x" |
+"last (_#y#zs) = last (y#zs)"
+
+fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
+"sep1 _ xs = xs"
+
+fun swap12:: "'a list \<Rightarrow> 'a list" where
+"swap12 (x#y#zs) = y#x#zs" |
+"swap12 zs = zs"
+
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/CountSnoc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/CountSnoc.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,39 @@
+theory CountSnoc
+imports Main
+begin
+
+
+datatype 'a myList = Nil | Cons 'a "'a myList"
+
+fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where
+"app_list Nil ys = ys" |
+"app_list (Cons x xs) ys = Cons x (app_list xs ys)"
+
+fun rev_list :: "'a myList \<Rightarrow> 'a myList" where
+"rev_list Nil = Nil" |
+"rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"
+
+fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
+"count_list x [] = 0" |
+"count_list x (y#xs) = (
+  if x = y then Suc(count_list x xs) 
+  else count_list x xs)"
+
+value "count_list (1::nat) [1,1,1]"
+value "count_list (1::nat) [2,2,2]"
+value "count_list (2::nat) [2,2,1]"
+
+lemma count1: "count_list n (xs @ ys) = count_list n xs + count_list n ys"
+apply(induct xs)
+apply(auto)
+done
+ 
+thm count1
+thm refl
+thm conjI[OF refl[of "a"] refl[of "b"]]
+thm conjI[OF conjI]
+ 
+
+
+
+
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/MyFirst.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/MyFirst.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,189 @@
+theory MyFirst
+imports Main
+begin
+
+datatype 'a list = Nil | Cons 'a "'a list"
+
+fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"app Nil ys = ys" |
+"app (Cons x xs) ys = Cons x (app xs ys)"
+
+fun rev :: "'a list \<Rightarrow> 'a list" where
+"rev Nil = Nil" |
+"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
+
+value "rev(Cons True (Cons False Nil))"
+
+value "1 + (2::nat)"
+value "1 + (2::int)"
+value "1 - (2::nat)"
+value "1 - (2::int)"
+
+lemma app_Nil2 [simp]: "app xs Nil = xs"
+apply(induction xs)
+apply(auto)
+done
+
+lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
+apply(induction xs)
+apply(auto)
+done
+
+lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
+apply (induction xs)
+apply (auto)
+done
+
+theorem rev_rev [simp]: "rev(rev xs) = xs"
+apply (induction xs)
+apply (auto)
+done
+
+fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"add 0 n = n" |
+"add (Suc m) n = Suc(add m n)"
+
+lemma add_02: "add m 0 = m"
+apply(induction m)
+apply(auto)
+done
+
+value "add 2 3"
+
+
+(**commutative-associative**)
+lemma add_04: "add m (add n k) = add (add m n) k"
+apply(induct m)
+apply(simp_all)
+done
+
+lemma add_zero: "add n 0 = n"
+apply(induct n)
+apply(auto)
+done
+
+lemma add_Suc: "add m (Suc n) = Suc (add m n)"
+apply(induct m)
+apply(metis add.simps(1))
+apply(auto)
+done
+
+lemma add_comm: "add m n = add n m"
+apply(induct m)
+apply(simp add: add_zero)
+apply(simp add: add_Suc)
+done
+
+lemma add_odd: "add m (add n k) = add k (add m n)"
+apply(subst add_04)
+apply(subst (2) add_comm)
+apply(simp)
+done
+
+
+fun dub :: "nat \<Rightarrow> nat" where
+"dub 0 = 0" |
+"dub m = add m m"
+
+lemma dub_01: "dub 0 = 0"
+apply(induct)
+apply(auto)
+done
+
+lemma dub_02: "dub m = add m m"
+apply(induction m)
+apply(auto)
+done
+
+value "dub 2"
+
+fun trip :: "nat \<Rightarrow> nat" where
+"trip 0 = 0" |
+"trip m = add m (add m m)"
+
+lemma trip_01: "trip 0 = 0"
+apply(induct)
+apply(auto)
+done
+
+lemma trip_02: "trip m = add m (add m m)"
+apply(induction m)
+apply(auto)
+done
+
+value "trip 1"
+value "trip 2"
+
+fun sum :: "nat \<Rightarrow> nat" where
+  "sum 0 = 0"
+| "sum (Suc n) = (Suc n) + sum n"
+
+function sum1 :: "nat \<Rightarrow> nat" where
+  "sum1 0 = 0"
+| "n \<noteq> 0 \<Longrightarrow> sum1 n = n + sum1 (n - 1)"
+apply(auto)
+done
+
+termination sum1
+by (smt2 "termination" diff_less less_than_iff not_gr0 wf_less_than zero_neq_one)
+
+lemma "sum n = sum1 n"
+apply(induct n)
+apply(auto)
+done
+
+lemma "sum n = (\<Sum>i \<le> n. i)"
+apply(induct n)
+apply(simp_all)
+done
+
+fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+"mull 0 0 = 0" |
+"mull m 0 = 0" |
+"mull m 1 = m" | 
+(**"mull m (1::nat) = m" | **)
+(**"mull m (suc(0)) = m" | **)
+"mull m n = mull m (n-(1::nat))" 
+apply(pat_completeness)
+apply(auto)
+
+done
+
+  "mull 0 n = 0"
+| "mull (Suc m) n = add n (mull m n)" 
+
+lemma test: "mull m n = m * n"
+sorry
+
+fun poww :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "poww 0 n = 1"
+| "poww (Suc m) n = mull n (poww m n)" 
+
+
+"mull 0 0 = 0" |
+"mull m 0 = 0" |
+(**"mull m 1 = m" | **)
+(**"mull m (1::nat) = m" | **)
+(**"mull m (suc(0)) = m" | **)
+"mull m n = mull m (n-(1::nat))" 
+
+(**Define a function that counts the
+number of occurrences of an element in a list **)
+(**
+fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
+"count  "
+**)
+
+
+(* prove n = n * (n + 1) div 2  *)
+
+
+
+
+
+
+
+
+
+
+
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/MyInduction.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/MyInduction.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,19 @@
+theory MyInduction
+imports Main
+begin
+
+fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+"itrev [] ys = ys" |
+"itrev (x#xs) ys = itrev xs (x#ys)"
+
+lemma "itrev xs [] = rev xs"
+apply(induction xs)
+apply(auto)
+oops
+
+lemma "itrev xs ys = rev xs @ ys"
+apply(induction xs arbitrary: ys)
+apply auto
+done
+
+
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/MySimplification.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/MySimplification.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,3 @@
+theory MySimplification
+imports Main
+begin
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/MyTree.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/MyTree.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,42 @@
+theory MyTree
+imports Main
+begin
+
+datatype 
+  'a tree = Tip | 
+  Node " 'a tree" 'a " 'a tree"
+
+fun mirror :: " 'a tree \<Rightarrow> 'a tree" where
+  "mirror Tip = Tip" |
+  "mirror (Node l a r) = Node (mirror r) a (mirror l)"
+
+lemma "mirror(mirror t) = t"
+  apply(induction t)
+  apply(auto)
+  done
+
+datatype 'a option = None | Some 'a
+
+fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
+  "lookup [] x = None" |
+  "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
+
+definition sq :: "nat \<Rightarrow> nat" where
+  "sq n = n * n"
+ 
+abbreviation sq' :: "nat \<Rightarrow> nat" where
+  "sq' n \<equiv> n * n"
+
+fun div2 :: "nat \<Rightarrow> nat" where
+  "div2 0 = 0" |
+  "div2 (Suc 0) = 0" |
+  "div2 (Suc(Suc n)) = Suc(div2 n)"
+
+lemma "div2(n) = n div 2"
+apply(induction n rule: div2.induct)
+apply(auto)
+done
+
+value "div2 8"
+
+
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/PosixTest.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/PosixTest.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,8 @@
+theory PosixTest
+imports Main
+begin
+
+
+
+
+end
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/Pr.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/Pr.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,105 @@
+theory Pr
+imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"
+begin
+
+fun 
+  add :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
+where
+  "add 0 n = n" |
+  "add (Suc m) n = Suc (add m n)"
+
+fun 
+  doub :: "nat \<Rightarrow> nat" 
+where
+  "doub 0 = 0" |
+  "doub n = n + n"
+
+lemma add_lem:
+  "add m n = m + n"
+apply(induct m arbitrary: )
+apply(auto)
+done
+
+fun 
+  count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
+where
+  "count n Nil = 0" |
+  "count n (x # xs) = (if n = x then (add 1 (count n xs)) else count n xs)"
+
+value "count 3 [1,2,3,3,4,3,5]"
+
+fun 
+  count2 :: "nat \<Rightarrow> nat list \<Rightarrow> nat" 
+where
+"count2 n Nil = 0" |
+"count2 n (Cons x xs) = (if n = x then (add 1 (count2 n xs)) else count2 n xs)"
+
+value "count2 (2::nat) [2,2,3::nat]"
+
+lemma
+  "count2 x xs \<le> length xs"
+apply(induct xs)
+apply(simp)
+apply(simp)
+apply(auto)
+done
+
+fun 
+  sum :: "nat \<Rightarrow> nat"
+where
+  "sum 0 = 0"
+| "sum (Suc n) = (Suc n) + sum n"
+
+lemma
+  "sum n = (n * (Suc n)) div 2"
+apply(induct n)
+apply(auto)
+done
+
+
+lemma
+  "doub n = add n n"
+apply(induct n)
+apply(simp)
+apply(simp add: add_lem)
+done
+
+lemma 
+  fixes a b::nat
+  shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"
+apply(simp add: power2_sum)
+done
+
+lemma
+  fixes a b c::"real"
+  assumes eq: "a * c \<le> b * c" and ineq: "b < a"
+  shows "c \<le> 0"
+proof -
+  {
+    assume  "0 < c" 
+    then have "b * c < a * c" using ineq by(auto)
+    then have "False" using eq by auto
+  } then show "c \<le> 0" by (auto simp add: not_le[symmetric]) 
+qed
+    
+
+
+
+lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))"
+by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85))
+
+
+
+lemma 
+ fixes n::"nat"
+ assumes a: "n > 1"
+    and  b: "\<not>(prime n)"
+ shows "\<not>(prime ((2 ^ n) - 1))"   
+using a b
+apply(induct n)
+apply(simp)
+apply(simp)
+
+
+
+end
\ No newline at end of file
diff -r 5b01f7c233f8 -r a33d3040bf7e Attic/ProofAutomation.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Attic/ProofAutomation.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,36 @@
+theory ProofAutomation
+imports Main
+begin
+
+lemma "\<forall>x. \<exists>y. x = y"
+by auto
+
+lemma "A \<subseteq> B \<inter> C \<Longrightarrow> A \<subseteq> B \<union> C"
+by auto
+
+lemma "\<lbrakk> \<forall> xs \<in> A. \<exists> ys. xs = ys @ ys; us \<in> A \<rbrakk> \<Longrightarrow> \<exists>n. length us = n+n"
+by fastforce
+
+lemma "\<lbrakk>xs @ ys = ys @ xs; length xs = length ys \<rbrakk> \<Longrightarrow> xs = ys"
+by auto
+
+lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c\<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c"
+by arith
+
+lemma "\<lbrakk> (a::nat) \<le> b; b \<le> c; c \<le> d; d \<le> e \<rbrakk> \<Longrightarrow> a \<le> e"
+by (blast intro: le_trans)
+
+lemma "Suc(Suc(Suc a)) \<le> b \<Longrightarrow> a \<le> b"
+by(blast dest: Suc_leD)
+
+inductive ev :: "nat \<Rightarrow> bool" where
+ev0: "ev 0" |
+evSS: "ev n \<Longrightarrow> ev (n + 2)"
+
+fun even :: "nat \<Rightarrow> bool" where
+"even 0 = True" |
+"even (Suc 0) = False" |
+"even (Suc(Suc n)) = even n"
+
+lemma "ev m \<Longrightarrow> even m"
+
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Chap03.thy
--- a/thys/Chap03.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,295 +0,0 @@
-theory Chap03
-imports Main
-begin
-
-(* 2.5.6 Case Study: Boolean Expressions *)
-
-datatype boolex = Const bool | Var nat | Neg boolex
-| And boolex boolex
-
-primrec "value2" :: "boolex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
-"value2 (Const b)  env = b" |
-"value2 (Var x)    env = env x" |
-"value2 (Neg b)    env = (\<not> value2 b env)" |
-"value2 (And b c)  env = (value2 b env \<and> value2 c env)"
-
-value "Const true"
-value "Var (Suc(0))"
-value "value2 (Const False) (\<lambda>x. False)"
-value "value2 (Var 11) (\<lambda>x. if (x = 10 | x = 11) then True else False)"
-value "value2 (Var 11) (\<lambda>x. True )"
-
-definition
-  "en1 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"
-  
-abbreviation
-  "en2 \<equiv>  (\<lambda>x. if x = 10 | x = 11 then True else False)"
-  
-value "value2 (And (Var 10) (Var 11)) en2"
-
-lemma "value2 (And (Var 10) (Var 11)) en2 = True"
-apply(simp)
-done
-
-datatype ifex = 
-  CIF bool 
-| VIF nat 
-| IF ifex ifex ifex
-
-primrec valif :: "ifex \<Rightarrow> (nat \<Rightarrow> bool) \<Rightarrow> bool" where
-"valif (CIF b)    env = b" |
-"valif (VIF x)    env = env x" |
-"valif (IF b t e) env = (if valif b env then valif t env else valif e env)"
-
-abbreviation "vif1 \<equiv> valif (CIF False) (\<lambda>x. False)"
-abbreviation "vif2 \<equiv> valif (VIF 11) (\<lambda>x. False)"
-abbreviation "vif3 \<equiv> valif (VIF 13) (\<lambda>x. True)"
-
-value "valif (CIF False) (\<lambda>x. False)"
-value "valif (VIF 11) (\<lambda>x. True)"
-value "valif (IF (CIF False) (CIF True) (CIF True))"
-
-primrec bool2if :: "boolex \<Rightarrow> ifex" where
-"bool2if (Const b)  = CIF b" |
-"bool2if (Var x)    = VIF x" |
-"bool2if (Neg b)    = IF (bool2if b) (CIF False) (CIF True)" |
-"bool2if (And b c)  = IF (bool2if b) (bool2if c) (CIF False)"
-
-lemma "valif (bool2if b) env = value2 b env"
-apply(induct_tac b)
-apply(auto)
-done
-
-primrec normif :: "ifex \<Rightarrow> ifex \<Rightarrow> ifex \<Rightarrow> ifex" where
-"normif (CIF b)     t e = IF (CIF b) t e" |
-"normif (VIF x)     t e = IF (VIF x) t e" |
-"normif (IF b t e)  u f = normif b (normif t u f) (normif e u f)"
-
-primrec norm :: "ifex \<Rightarrow> ifex" where
-"norm (CIF b)     = CIF b" |
-"norm (VIF x)     = VIF x" |
-"norm (IF b t e)  = normif b (norm t) (norm e)"  
-
-(***************   CHAPTER-3   ********************************)
-
-lemma "\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \<rbrakk> \<Longrightarrow> ys = zs"
-apply simp
-done
-
-lemma "\<forall> x. f x = g (f (g x)) \<Longrightarrow> f [] = f [] @ []"
-apply (simp (no_asm))
-done
-
-definition xor :: "bool \<Rightarrow> bool \<Rightarrow> bool" where
-"xor A B \<equiv> (A \<and> \<not>B) \<or> (\<not>A \<and> B)"
-
-lemma "xor A (\<not>A)"
-apply(simp only: xor_def)
-apply(simp add: xor_def)
-done
-
-lemma "(let xs = [] in xs@ys@xs) = ys"
-apply(simp only: Let_def)
-apply(simp add: Let_def)
-done
-
-(* 3.1.8 Conditioal Simplification Rules  *)
-
-lemma hd_Cons_tl: "xs \<noteq> [] \<Longrightarrow> hd xs # tl xs = xs"
-using [[simp_trace=true]]
-apply(case_tac xs)
-apply(simp)
-apply(simp)
-done
-
-lemma "xs \<noteq> [] \<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs"
-apply(case_tac xs)
-using [[simp_trace=true]]
-apply(simp)
-apply(simp)
-done
-
-(* 3.1.9 Automatic Case Splits  *)
-
-lemma "\<forall> xs. if xs = [] then rev xs = [] else rev xs \<noteq> []"
-apply(split split_if)
-apply(simp)
-done
-
-lemma "(case xs of [] \<Rightarrow> zs | y#ys \<Rightarrow> y#(ys@zs)) = xs@zs"
-apply(split list.split)
-apply(simp split: list.split)
-done
-
-lemma "if xs = [] then ys \<noteq> [] else ys = [] \<Longrightarrow> xs @ ys \<noteq> []"
-apply(split split_if_asm)
-apply(simp)
-apply(auto)
-done
-
-(* 3.2 Induction Heuristics  *)
-
-primrec itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"itrev [] ys = ys" |
-"itrev (x#xs) ys = itrev xs (x#ys)"
-
-lemma "itrev xs [] = rev xs"
-apply(induct_tac xs)
-apply(simp)
-apply(auto)
-oops
-
-lemma "itrev xs ys = rev xs @ ys"
-apply(induct_tac xs)
-apply(simp_all)
-oops
-
-lemma "\<forall> ys. itrev xs ys = rev xs @ ys"
-apply(induct_tac xs)
-apply(simp)
-apply(simp)
-done
-
-primrec add1 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-"add1 m 0 = m" |
-"add1 m (Suc n) = add1 (Suc m) n"
-
-primrec add2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-"add2 m 0 = m" |
-"add2 m (Suc n) = Suc (add2 m n)"
-
-value "add1 1 3"
-value "1 + 3"
-
-lemma abc [simp]: "add1 m 0 = m"
-apply(induction m)
-apply(simp)
-apply(simp)
-done
-
-lemma abc2: "\<forall>m. add1 m n = m + n"
-apply(induction n)
-apply(simp)
-apply(simp del: add1.simps)
-apply(simp (no_asm) only: add1.simps)
-apply(simp only: )
-apply(simp)
-done
-
-thm abc2
-
-lemma abc3: "add1 m n = m + n"
-apply(induction n arbitrary: m)
-apply(simp)
-apply(simp del: add1.simps)
-apply(simp (no_asm) only: add1.simps)
-apply(simp only: )
-done
-
-thm abc3
-
-lemma abc4: "add1 m n = add2 m n"
-apply(induction n arbitrary: m)
-apply(simp)
-apply(simp add: abc3)
-done
-
-find_theorems "_ \<and> _ "
-
-(* added anottest *)
-
-lemma abc5: "add2 m n = m + n"
-apply(induction n)
-apply(simp)
-apply(simp)
-done
-
-
-(* 3.3 Case Study: Compiling Expressions  *)
-
-type_synonym 'v binop = "'v \<Rightarrow> 'v \<Rightarrow> 'v"
-datatype ('a, 'v)expr = 
-  Cex 'v
-| Vex 'a
-| Bex "'v binop" "('a,'v)expr" "('a,'v)expr"
-
-primrec "value" :: "('a,'v)expr \<Rightarrow> ('a \<Rightarrow> 'v) \<Rightarrow> 'v" where
-"value (Cex v) env = v" |
-"value (Vex a) env = env a" |
-"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"
-
-value "value (Cex a) (\<lambda>x. True)"
-
-datatype ('a,'v)instr = 
-  Const 'v
-| Load 'a
-| Apply "'v binop"
-
-primrec exec :: "('a,'v)instr list \<Rightarrow> ('a\<Rightarrow>'v) \<Rightarrow> 'v list \<Rightarrow> 'v list" where
-"exec [] s vs = vs" |
-"exec (i#is) s vs = (case i of
-    Const v \<Rightarrow> exec is s (v#vs)
-  | Load a \<Rightarrow> exec is s ((s a)#vs)
-  | Apply f \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"
-  
-primrec compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list" where
-"compile (Cex v) = [Const v]" |
-"compile (Vex a) = [Load a]" |
-"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"
-
-theorem "exec (compile e) s [] = [value e s]"
-(*the theorem needs to be generalized*)
-oops
-
-(*more generalized theorem*)
-theorem "\<forall> vs. exec (compile e) s vs = (value e s) # vs"
-apply(induct_tac e)
-apply(simp)
-apply(simp)
-oops
-
-lemma exec_app[simp]: "\<forall> vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"
-apply(induct_tac xs)
-apply(simp)
-apply(simp)
-apply(simp split: instr.split)
-done
-
-(* 3.4 Advanced Datatypes  *)
-
-datatype 'a aexp = IF "'a bexp" "'a aexp" "'a aexp" 
-                | Sum "'a aexp" "'a aexp"
-                | Diff "'a aexp" "'a aexp"
-                | Var 'a
-                | Num nat
-and      'a bexp = Less "'a aexp" "'a aexp"
-                | And "'a bexp" "'a bexp"
-                | Neg "'a bexp"
-                
-(*  Total Recursive Functions: Fun  *)
-(*  3.5.1 Definition    *)
-
-fun fib :: "nat \<Rightarrow> nat" where
-"fib 0 = 0" |
-"fib (Suc 0) = 1" |
-"fib (Suc(Suc x)) = fib x + fib (Suc x)"
-
-value "fib (Suc(Suc(Suc(Suc(Suc 0)))))"
-
-fun sep :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"sep a [] = []" |
-"sep a [x] = [x]" |
-"sep a (x#y#zs) = x # a # sep a (y#zs)"
-
-fun last :: "'a list \<Rightarrow> 'a" where
-"last [x] = x" |
-"last (_#y#zs) = last (y#zs)"
-
-fun sep1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"sep1 a (x#y#zs) = x # a # sep1 a (y#zs)" |
-"sep1 _ xs = xs"
-
-fun swap12:: "'a list \<Rightarrow> 'a list" where
-"swap12 (x#y#zs) = y#x#zs" |
-"swap12 zs = zs"
-
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/CountSnoc.thy
--- a/thys/CountSnoc.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-theory CountSnoc
-imports Main
-begin
-
-
-datatype 'a myList = Nil | Cons 'a "'a myList"
-
-fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where
-"app_list Nil ys = ys" |
-"app_list (Cons x xs) ys = Cons x (app_list xs ys)"
-
-fun rev_list :: "'a myList \<Rightarrow> 'a myList" where
-"rev_list Nil = Nil" |
-"rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"
-
-fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
-"count_list x [] = 0" |
-"count_list x (y#xs) = (
-  if x = y then Suc(count_list x xs) 
-  else count_list x xs)"
-
-value "count_list (1::nat) [1,1,1]"
-value "count_list (1::nat) [2,2,2]"
-value "count_list (2::nat) [2,2,1]"
-
-lemma count1: "count_list n (xs @ ys) = count_list n xs + count_list n ys"
-apply(induct xs)
-apply(auto)
-done
- 
-thm count1
-thm refl
-thm conjI[OF refl[of "a"] refl[of "b"]]
-thm conjI[OF conjI]
- 
-
-
-
-
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/MyFirst.thy
--- a/thys/MyFirst.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,189 +0,0 @@
-theory MyFirst
-imports Main
-begin
-
-datatype 'a list = Nil | Cons 'a "'a list"
-
-fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"app Nil ys = ys" |
-"app (Cons x xs) ys = Cons x (app xs ys)"
-
-fun rev :: "'a list \<Rightarrow> 'a list" where
-"rev Nil = Nil" |
-"rev (Cons x xs) = app (rev xs) (Cons x Nil)"
-
-value "rev(Cons True (Cons False Nil))"
-
-value "1 + (2::nat)"
-value "1 + (2::int)"
-value "1 - (2::nat)"
-value "1 - (2::int)"
-
-lemma app_Nil2 [simp]: "app xs Nil = xs"
-apply(induction xs)
-apply(auto)
-done
-
-lemma app_assoc [simp]: "app (app xs ys) zs = app xs (app ys zs)"
-apply(induction xs)
-apply(auto)
-done
-
-lemma rev_app [simp]: "rev(app xs ys) = app (rev ys) (rev xs)"
-apply (induction xs)
-apply (auto)
-done
-
-theorem rev_rev [simp]: "rev(rev xs) = xs"
-apply (induction xs)
-apply (auto)
-done
-
-fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-"add 0 n = n" |
-"add (Suc m) n = Suc(add m n)"
-
-lemma add_02: "add m 0 = m"
-apply(induction m)
-apply(auto)
-done
-
-value "add 2 3"
-
-
-(**commutative-associative**)
-lemma add_04: "add m (add n k) = add (add m n) k"
-apply(induct m)
-apply(simp_all)
-done
-
-lemma add_zero: "add n 0 = n"
-apply(induct n)
-apply(auto)
-done
-
-lemma add_Suc: "add m (Suc n) = Suc (add m n)"
-apply(induct m)
-apply(metis add.simps(1))
-apply(auto)
-done
-
-lemma add_comm: "add m n = add n m"
-apply(induct m)
-apply(simp add: add_zero)
-apply(simp add: add_Suc)
-done
-
-lemma add_odd: "add m (add n k) = add k (add m n)"
-apply(subst add_04)
-apply(subst (2) add_comm)
-apply(simp)
-done
-
-
-fun dub :: "nat \<Rightarrow> nat" where
-"dub 0 = 0" |
-"dub m = add m m"
-
-lemma dub_01: "dub 0 = 0"
-apply(induct)
-apply(auto)
-done
-
-lemma dub_02: "dub m = add m m"
-apply(induction m)
-apply(auto)
-done
-
-value "dub 2"
-
-fun trip :: "nat \<Rightarrow> nat" where
-"trip 0 = 0" |
-"trip m = add m (add m m)"
-
-lemma trip_01: "trip 0 = 0"
-apply(induct)
-apply(auto)
-done
-
-lemma trip_02: "trip m = add m (add m m)"
-apply(induction m)
-apply(auto)
-done
-
-value "trip 1"
-value "trip 2"
-
-fun sum :: "nat \<Rightarrow> nat" where
-  "sum 0 = 0"
-| "sum (Suc n) = (Suc n) + sum n"
-
-function sum1 :: "nat \<Rightarrow> nat" where
-  "sum1 0 = 0"
-| "n \<noteq> 0 \<Longrightarrow> sum1 n = n + sum1 (n - 1)"
-apply(auto)
-done
-
-termination sum1
-by (smt2 "termination" diff_less less_than_iff not_gr0 wf_less_than zero_neq_one)
-
-lemma "sum n = sum1 n"
-apply(induct n)
-apply(auto)
-done
-
-lemma "sum n = (\<Sum>i \<le> n. i)"
-apply(induct n)
-apply(simp_all)
-done
-
-fun mull :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-"mull 0 0 = 0" |
-"mull m 0 = 0" |
-"mull m 1 = m" | 
-(**"mull m (1::nat) = m" | **)
-(**"mull m (suc(0)) = m" | **)
-"mull m n = mull m (n-(1::nat))" 
-apply(pat_completeness)
-apply(auto)
-
-done
-
-  "mull 0 n = 0"
-| "mull (Suc m) n = add n (mull m n)" 
-
-lemma test: "mull m n = m * n"
-sorry
-
-fun poww :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
-  "poww 0 n = 1"
-| "poww (Suc m) n = mull n (poww m n)" 
-
-
-"mull 0 0 = 0" |
-"mull m 0 = 0" |
-(**"mull m 1 = m" | **)
-(**"mull m (1::nat) = m" | **)
-(**"mull m (suc(0)) = m" | **)
-"mull m n = mull m (n-(1::nat))" 
-
-(**Define a function that counts the
-number of occurrences of an element in a list **)
-(**
-fun count :: "'a\<Rightarrow>'a list\<Rightarrow>nat" where
-"count  "
-**)
-
-
-(* prove n = n * (n + 1) div 2  *)
-
-
-
-
-
-
-
-
-
-
-
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/MyInduction.thy
--- a/thys/MyInduction.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-theory MyInduction
-imports Main
-begin
-
-fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"itrev [] ys = ys" |
-"itrev (x#xs) ys = itrev xs (x#ys)"
-
-lemma "itrev xs [] = rev xs"
-apply(induction xs)
-apply(auto)
-oops
-
-lemma "itrev xs ys = rev xs @ ys"
-apply(induction xs arbitrary: ys)
-apply auto
-done
-
-
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/MySimplification.thy
--- a/thys/MySimplification.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,3 +0,0 @@
-theory MySimplification
-imports Main
-begin
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/MyTree.thy
--- a/thys/MyTree.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,42 +0,0 @@
-theory MyTree
-imports Main
-begin
-
-datatype 
-  'a tree = Tip | 
-  Node " 'a tree" 'a " 'a tree"
-
-fun mirror :: " 'a tree \<Rightarrow> 'a tree" where
-  "mirror Tip = Tip" |
-  "mirror (Node l a r) = Node (mirror r) a (mirror l)"
-
-lemma "mirror(mirror t) = t"
-  apply(induction t)
-  apply(auto)
-  done
-
-datatype 'a option = None | Some 'a
-
-fun lookup :: "('a * 'b) list \<Rightarrow> 'a \<Rightarrow> 'b option" where
-  "lookup [] x = None" |
-  "lookup ((a,b) # ps) x = (if a = x then Some b else lookup ps x)"
-
-definition sq :: "nat \<Rightarrow> nat" where
-  "sq n = n * n"
- 
-abbreviation sq' :: "nat \<Rightarrow> nat" where
-  "sq' n \<equiv> n * n"
-
-fun div2 :: "nat \<Rightarrow> nat" where
-  "div2 0 = 0" |
-  "div2 (Suc 0) = 0" |
-  "div2 (Suc(Suc n)) = Suc(div2 n)"
-
-lemma "div2(n) = n div 2"
-apply(induction n rule: div2.induct)
-apply(auto)
-done
-
-value "div2 8"
-
-
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Paper/Paper.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Paper/Paper.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,24 @@
+(*<*)
+theory Paper
+imports "../ReStar" "~~/src/HOL/Library/LaTeXsugar"
+begin
+(*>*)
+
+section {* Introduction *}
+
+ 
+
+text {*
+  %\noindent
+  %{\bf Acknowledgements:}
+  %We are grateful for the comments we received from anonymous
+  %referees.
+
+  \bibliographystyle{plain}
+  \bibliography{root}
+*}
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Paper/document/llncs.cls
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Paper/document/llncs.cls	Fri Feb 05 10:16:10 2016 +0000
@@ -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 5b01f7c233f8 -r a33d3040bf7e thys/Paper/document/mathpartir.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Paper/document/mathpartir.sty	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,446 @@
+%  Mathpartir --- Math Paragraph for Typesetting Inference Rules
+%
+%  Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy
+%
+%  Author         : Didier Remy 
+%  Version        : 1.2.0
+%  Bug Reports    : to author
+%  Web Site       : http://pauillac.inria.fr/~remy/latex/
+% 
+%  Mathpartir is free software; you can redistribute it and/or modify
+%  it under the terms of the GNU General Public License as published by
+%  the Free Software Foundation; either version 2, or (at your option)
+%  any later version.
+%  
+%  Mathpartir is distributed in the hope that it will be useful,
+%  but WITHOUT ANY WARRANTY; without even the implied warranty of
+%  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+%  GNU General Public License for more details 
+%  (http://pauillac.inria.fr/~remy/license/GPL).
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%  File mathpartir.sty (LaTeX macros)
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\NeedsTeXFormat{LaTeX2e}
+\ProvidesPackage{mathpartir}
+    [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules]
+
+%%
+
+%% Identification
+%% Preliminary declarations
+
+\RequirePackage {keyval}
+
+%% Options
+%% More declarations
+
+%% PART I: Typesetting maths in paragraphe mode
+
+%% \newdimen \mpr@tmpdim
+%% Dimens are a precious ressource. Uses seems to be local.
+\let \mpr@tmpdim \@tempdima
+
+% To ensure hevea \hva compatibility, \hva should expands to nothing 
+% in mathpar or in inferrule
+\let \mpr@hva \empty
+
+%% normal paragraph parametters, should rather be taken dynamically
+\def \mpr@savepar {%
+  \edef \MathparNormalpar
+     {\noexpand \lineskiplimit \the\lineskiplimit
+      \noexpand \lineskip \the\lineskip}%
+  }
+
+\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em}
+\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em}
+\def \mpr@lineskip  {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em}
+\let \MathparLineskip \mpr@lineskip
+\def \mpr@paroptions {\MathparLineskip}
+\let \mpr@prebindings \relax
+
+\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em
+
+\def \mpr@goodbreakand
+   {\hskip -\mpr@andskip  \penalty -1000\hskip \mpr@andskip}
+\def \mpr@and {\hskip \mpr@andskip}
+\def \mpr@andcr {\penalty 50\mpr@and}
+\def \mpr@cr {\penalty -10000\mpr@and}
+\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10}
+
+\def \mpr@bindings {%
+  \let \and \mpr@andcr
+  \let \par \mpr@andcr
+  \let \\\mpr@cr
+  \let \eqno \mpr@eqno
+  \let \hva \mpr@hva
+  } 
+\let \MathparBindings \mpr@bindings
+
+% \@ifundefined {ignorespacesafterend}
+%    {\def \ignorespacesafterend {\aftergroup \ignorespaces}
+
+\newenvironment{mathpar}[1][]
+  {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering
+     \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else
+     \noindent $\displaystyle\fi
+     \MathparBindings}
+  {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend}
+
+\newenvironment{mathparpagebreakable}[1][]
+  {\begingroup 
+   \par
+   \mpr@savepar \parskip 0em \hsize \linewidth \centering
+      \mpr@prebindings \mpr@paroptions #1%
+      \vskip \abovedisplayskip \vskip -\lineskip%
+     \ifmmode  \else  $\displaystyle\fi
+     \MathparBindings
+  }
+  {\unskip
+   \ifmmode $\fi \par\endgroup
+   \vskip \belowdisplayskip
+   \noindent
+  \ignorespacesafterend}
+
+% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum
+%     \wd0 < \hsize  $$\box0$$\else \bmathpar #1\emathpar \fi}
+
+%%% HOV BOXES
+
+\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip 
+  \vbox \bgroup \tabskip 0em \let \\ \cr
+  \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup
+  \egroup}
+
+\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize
+      \box0\else \mathvbox {#1}\fi}
+
+
+%% Part II -- operations on lists
+
+\newtoks \mpr@lista
+\newtoks \mpr@listb
+
+\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@lista \the \mpr@listb}}
+
+\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter
+{#2}\edef #2{\the \mpr@listb\the\mpr@lista}}
+
+\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb
+\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}}
+
+\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2}
+\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}}
+
+\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2}
+\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}}
+
+\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}%
+   \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the
+   \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty 
+   \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop
+     \mpr@flatten \mpr@all \mpr@to \mpr@one
+     \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof
+     \mpr@all \mpr@stripend  
+     \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi
+     \ifx 1\mpr@isempty
+   \repeat
+}
+
+\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty
+   \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp}
+
+%% Part III -- Type inference rules
+
+\newif \if@premisse
+\newbox \mpr@hlist
+\newbox \mpr@vlist
+\newif \ifmpr@center \mpr@centertrue
+\def \mpr@htovlist {%
+   \setbox \mpr@hlist
+      \hbox {\strut
+             \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi
+             \unhbox \mpr@hlist}%
+   \setbox \mpr@vlist
+      \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+             \else \unvbox \mpr@vlist \box \mpr@hlist
+             \fi}%
+}
+% OLD version
+% \def \mpr@htovlist {%
+%    \setbox \mpr@hlist
+%       \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}%
+%    \setbox \mpr@vlist
+%       \vbox {\if@premisse  \box \mpr@hlist \unvbox \mpr@vlist
+%              \else \unvbox \mpr@vlist \box \mpr@hlist
+%              \fi}%
+% }
+
+\def \mpr@item #1{$\displaystyle #1$}
+\def \mpr@sep{2em}
+\def \mpr@blank { }
+\def \mpr@hovbox #1#2{\hbox
+  \bgroup
+  \ifx #1T\@premissetrue
+  \else \ifx #1B\@premissefalse
+  \else
+     \PackageError{mathpartir}
+       {Premisse orientation should either be T or B}
+       {Fatal error in Package}%
+  \fi \fi
+  \def \@test {#2}\ifx \@test \mpr@blank\else
+  \setbox \mpr@hlist \hbox {}%
+  \setbox \mpr@vlist \vbox {}%
+  \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi
+  \let \@hvlist \empty \let \@rev \empty
+  \mpr@tmpdim 0em
+  \expandafter \mpr@makelist #2\mpr@to \mpr@flat
+  \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi
+  \def \\##1{%
+     \def \@test {##1}\ifx \@test \empty
+        \mpr@htovlist
+        \mpr@tmpdim 0em %%% last bug fix not extensively checked
+     \else
+      \setbox0 \hbox{\mpr@item {##1}}\relax
+      \advance \mpr@tmpdim by \wd0
+      %\mpr@tmpdim 1.02\mpr@tmpdim
+      \ifnum \mpr@tmpdim < \hsize
+         \ifnum \wd\mpr@hlist > 0
+           \if@premisse
+             \setbox \mpr@hlist 
+                \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}%
+           \else
+             \setbox \mpr@hlist
+                \hbox {\unhbox \mpr@hlist  \hskip \mpr@sep \unhbox0}%
+           \fi
+         \else 
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+         \fi
+      \else
+         \ifnum \wd \mpr@hlist > 0
+            \mpr@htovlist 
+            \mpr@tmpdim \wd0
+         \fi
+         \setbox \mpr@hlist \hbox {\unhbox0}%
+      \fi
+      \advance \mpr@tmpdim by \mpr@sep
+   \fi
+   }%
+   \@rev
+   \mpr@htovlist
+   \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist
+   \fi
+   \egroup
+}
+
+%%% INFERENCE RULES
+
+\@ifundefined{@@over}{%
+    \let\@@over\over % fallback if amsmath is not loaded
+    \let\@@overwithdelims\overwithdelims
+    \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims
+    \let\@@above\above \let\@@abovewithdelims\abovewithdelims
+  }{}
+
+%% The default
+
+\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\mpr@over #2}$}}
+\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em
+    $\displaystyle {#1\@@atop #2}$}}
+
+\let \mpr@fraction \mpr@@fraction
+
+%% A generic solution to arrow
+
+\def \mpr@make@fraction #1#2#3#4#5{\hbox {%
+     \def \mpr@tail{#1}%
+     \def \mpr@body{#2}%
+     \def \mpr@head{#3}%
+     \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}%
+     \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}%
+     \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}%
+     \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax
+     \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax
+     \setbox0=\hbox {$\box1 \@@atop \box2$}%
+     \dimen0=\wd0\box0
+     \box0 \hskip -\dimen0\relax
+     \hbox to \dimen0 {$%
+       \mathrel{\mpr@tail}\joinrel
+       \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}%
+     $}}}
+
+%% Old stuff should be removed in next version
+\def \mpr@@nothing #1#2
+    {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$}
+\def \mpr@@reduce #1#2{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}}
+\def \mpr@@rewrite #1#2#3{\hbox
+    {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}}
+\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}}
+
+\def \mpr@empty {}
+\def \mpr@inferrule
+  {\bgroup
+     \ifnum \linewidth<\hsize \hsize \linewidth\fi
+     \mpr@rulelineskip
+     \let \and \qquad
+     \let \hva \mpr@hva
+     \let \@rulename \mpr@empty
+     \let \@rule@options \mpr@empty
+     \let \mpr@over \@@over
+     \mpr@inferrule@}
+\newcommand {\mpr@inferrule@}[3][]
+  {\everymath={\displaystyle}%       
+   \def \@test {#2}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}%
+   \else 
+   \def \@test {#3}\ifx \empty \@test
+      \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}%
+   \else
+   \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}%
+   \fi \fi
+   \def \@test {#1}\ifx \@test\empty \box0
+   \else \vbox 
+%%% Suggestion de Francois pour les etiquettes longues
+%%%   {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi
+      {\hbox {\RefTirName {#1}}\box0}\fi
+   \egroup}
+
+\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}}
+
+% They are two forms
+% \inferrule [label]{[premisses}{conclusions}
+% or
+% \inferrule* [options]{[premisses}{conclusions}
+%
+% Premisses and conclusions are lists of elements separated by \\
+% Each \\ produces a break, attempting horizontal breaks if possible, 
+% and  vertical breaks if needed. 
+% 
+% An empty element obtained by \\\\ produces a vertical break in all cases. 
+%
+% The former rule is aligned on the fraction bar. 
+% The optional label appears on top of the rule
+% The second form to be used in a derivation tree is aligned on the last
+% line of its conclusion
+% 
+% The second form can be parameterized, using the key=val interface. The
+% folloiwng keys are recognized:
+%       
+%  width                set the width of the rule to val
+%  narrower             set the width of the rule to val\hsize
+%  before               execute val at the beginning/left
+%  lab                  put a label [Val] on top of the rule
+%  lskip                add negative skip on the right
+%  left                 put a left label [Val]
+%  Left                 put a left label [Val],  ignoring its width 
+%  right                put a right label [Val]
+%  Right                put a right label [Val], ignoring its width
+%  leftskip             skip negative space on the left-hand side
+%  rightskip            skip negative space on the right-hand side
+%  vdots                lift the rule by val and fill vertical space with dots
+%  after                execute val at the end/right
+%  
+%  Note that most options must come in this order to avoid strange
+%  typesetting (in particular  leftskip must preceed left and Left and
+%  rightskip must follow Right or right; vdots must come last 
+%  or be only followed by rightskip. 
+%  
+
+%% Keys that make sence in all kinds of rules
+\def \mprset #1{\setkeys{mprset}{#1}}
+\define@key {mprset}{andskip}[]{\mpr@andskip=#1}
+\define@key {mprset}{lineskip}[]{\lineskip=#1}
+\define@key {mprset}{flushleft}[]{\mpr@centerfalse}
+\define@key {mprset}{center}[]{\mpr@centertrue}
+\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction}
+\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mprset}{sep}{\def\mpr@sep{#1}}
+
+\newbox \mpr@right
+\define@key {mpr}{flushleft}[]{\mpr@centerfalse}
+\define@key {mpr}{center}[]{\mpr@centertrue}
+\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite}
+\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1}
+\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{width}{\hsize #1}
+\define@key {mpr}{sep}{\def\mpr@sep{#1}}
+\define@key {mpr}{before}{#1}
+\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}}
+\define@key {mpr}{narrower}{\hsize #1\hsize}
+\define@key {mpr}{leftskip}{\hskip -#1}
+\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce}
+\define@key {mpr}{rightskip}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}}
+\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax
+     \advance \hsize by -\wd0\box0}
+\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}}
+\define@key {mpr}{right}
+  {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{RIGHT}
+  {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0
+   \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}}
+\define@key {mpr}{Right}
+  {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}}
+\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}}
+\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}}
+
+\newcommand \mpr@inferstar@ [3][]{\setbox0
+  \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax
+         \setbox \mpr@right \hbox{}%
+         $\setkeys{mpr}{#1}%
+          \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else
+          \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi
+          \box \mpr@right \mpr@vdots$}
+  \setbox1 \hbox {\strut}
+  \@tempdima \dp0 \advance \@tempdima by -\dp1
+  \raise \@tempdima \box0}
+
+\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}}
+\newcommand \mpr@err@skipargs[3][]{}
+\def \mpr@inferstar*{\ifmmode 
+    \let \@do \mpr@inferstar@
+  \else 
+    \let \@do \mpr@err@skipargs
+    \PackageError {mathpartir}
+      {\string\inferrule* can only be used in math mode}{}%
+  \fi \@do}
+
+
+%%% Exports
+
+% Envirnonment mathpar
+
+\let \inferrule \mpr@infer
+
+% make a short name \infer is not already defined
+\@ifundefined {infer}{\let \infer \mpr@infer}{}
+
+\def \TirNameStyle #1{\small \textsc{#1}}
+\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}}
+\let \TirName \tir@name
+\let \DefTirName \TirName
+\let \RefTirName \TirName
+
+%%% Other Exports
+
+% \let \listcons \mpr@cons
+% \let \listsnoc \mpr@snoc
+% \let \listhead \mpr@head
+% \let \listmake \mpr@makelist
+
+
+
+
+\endinput
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Paper/document/root.bib
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Paper/document/root.bib	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,331 @@
+@inproceedings{Sulzmann2014,
+  author    = {M.~Sulzmann and K.~Lu},
+  title     = {{POSIX} {R}egular {E}xpression {P}arsing with {D}erivatives},
+  booktitle = {Proc.~of the 12th International Conference on Functional and Logic Programming (FLOPS)},
+  pages     = {203--220},
+  year      = {2014},
+  volume =    {8475},
+  series =    {LNCS}
+}
+
+@Misc{Kuklewicz,
+  author = 	 {C.~Kuklewicz},
+  title = 	 {{R}egex {P}osix},
+  howpublished = "\url{https://wiki.haskell.org/Regex_Posix}"
+}
+
+@InProceedings{Asperti12,
+  author =       {A.~Asperti},
+  title =        {{A} {C}ompact {P}roof of {D}ecidability for {R}egular {E}xpression {E}quivalence},
+  booktitle = {Proc.~of the 3rd International Conference on Interactive Theorem Proving (ITP)},
+  pages =     {283--298},
+  year =      {2012},
+  volume =    {7406},
+  series =    {LNCS}
+}
+
+@inproceedings{Frisch2004,
+  author    = {A.~Frisch and L.~Cardelli},
+  title     = {{G}reedy {R}egular {E}xpression {M}atching},
+  booktitle = {Proc.~of the 31st International Conference on Automata, Languages and Programming (ICALP)},
+  pages     = {618--629},
+  year      = {2004},
+  volume =    {3142},
+  series =    {LNCS}
+}
+
+@ARTICLE{Antimirov95,
+    author = {V.~Antimirov},
+    title = {{P}artial {D}erivatives of {R}egular {E}xpressions and 
+     {F}inite {A}utomata {C}onstructions},
+    journal = {Theoretical Computer Science},
+    year = {1995},
+    volume = {155},
+    pages = {291--319}
+}
+
+@inproceedings{Nipkow98,
+ author={T.~Nipkow},
+ title={{V}erified {L}exical {A}nalysis},
+ booktitle={Proc.~of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs)},
+ series={LNCS},
+ volume=1479,
+ pages={1--15},
+ year=1998
+}
+
+@article{Brzozowski1964,
+  author    = {J.~A.~Brzozowski},
+  title     = {{D}erivatives of {R}egular {E}xpressions},
+  journal   = {Journal of the {ACM}},
+  volume    = {11},
+  number    = {4},
+  pages     = {481--494},
+  year      = {1964}
+}
+
+@article{Leroy2009,
+  author = {X.~Leroy},
+  title = {{F}ormal {V}erification of a {R}ealistic {C}ompiler},
+  journal = {Communications of the ACM},
+  year = 2009,
+  volume = 52,
+  number = 7,
+  pages = {107--115}
+}
+
+@InProceedings{Paulson2015,
+  author = 	 {L.~C.~Paulson},
+  title = 	 {{A} {F}ormalisation of {F}inite {A}utomata {U}sing {H}ereditarily {F}inite {S}ets},
+  booktitle = {Proc.~of the 25th International Conference on Automated Deduction (CADE)},
+  pages = 	 {231--245},
+  year = 	 {2015},
+  volume = 	 {9195},
+  series = 	 {LNAI}
+}
+
+@Article{Wu2014,
+  author = 	 {C.~Wu and X.~Zhang and C.~Urban},
+  title = 	 {{A} {F}ormalisation of the {M}yhill-{N}erode {T}heorem based on {R}egular {E}xpressions},
+  journal = 	 {Journal of Automatic Reasoning},
+  year = 	 {2014},
+  volume = 	 {52},
+  number = 	 {4},
+  pages = 	 {451--480}
+}
+
+@InProceedings{Regehr2011,
+  author = 	 {X.~Yang and Y.~Chen and E.~Eide and J.~Regehr},
+  title = 	 {{F}inding and {U}nderstanding {B}ugs in {C} {C}ompilers},
+  pages = 	 {283--294},
+  year = 	 {2011},
+  booktitle =    {Proc.~of the 32nd ACM SIGPLAN Conference on Programming Language Design and 
+                  Implementation (PLDI)}
+}
+
+@Article{Norrish2014,
+  author = 	 {A.~Barthwal and M.~Norrish},
+  title = 	 {{A} {M}echanisation of {S}ome {C}ontext-{F}ree {L}anguage {T}heory in {HOL4}},
+  journal          = {Journal of Computer and System Sciences},
+  year = 	 {2014},
+  volume = 	 {80},
+  number = 	 {2},
+  pages = 	 {346--362}
+}
+
+@Article{Thompson1968,
+ author = {K.~Thompson},
+ title = {{P}rogramming {T}echniques: {R}egular {E}xpression {S}earch {A}lgorithm},
+ journal = {Communications of the ACM},
+ issue_date = {June 1968},
+ volume = {11},
+ number = {6},
+ year = {1968},
+ pages = {419--422}
+}
+
+@article{Owens2009,
+  author    = {S.~Owens and J.~H.~Reppy and A.~Turon},
+  title     = {{R}egular-{E}xpression {D}erivatives {R}e-{E}xamined},
+  journal   = {Journal of Functinal Programming},
+  volume    = {19},
+  number    = {2},
+  pages     = {173--190},
+  year      = {2009}
+}
+
+@inproceedings{Sulzmann2015,
+  author    = {M.~Sulzmann and P.~Thiemann},
+  title     = {{D}erivatives for {R}egular {S}huffle {E}xpressions},
+  booktitle = {Proc.~of the 9th International Conference on Language and Automata Theory 
+               and Applications (LATA)},
+  pages     = {275--286},
+  year      = {2015},
+  volume = 	 {8977},
+  series = 	 {LNCS}
+}
+
+@inproceedings{Chen2012,
+  author    = {H.~Chen and S.~Yu},
+  title     = {{D}erivatives of {R}egular {E}xpressions and an {A}pplication},
+  booktitle = {Proc.~in the International Workshop on Theoretical
+               Computer Science (WTCS)},
+  pages     = {343--356},
+  year      = {2012},
+  volume = 	 {7160},
+  series = 	 {LNCS}
+}
+
+@article{Krauss2011,
+  author={A.~Krauss and T.~Nipkow},
+  title={{P}roof {P}earl: {R}egular {E}xpression {E}quivalence and {R}elation {A}lgebra},
+  journal={Journal of Automated Reasoning},
+  volume=49,
+  pages={95--106},
+  year=2012
+}
+
+@InProceedings{Traytel2015,
+  author =	{D.~Traytel},
+  title =	{{A} {C}oalgebraic {D}ecision {P}rocedure for {WS1S}},
+  booktitle =	{Proc.~of the 24th Annual Conference on Computer Science Logic (CSL)},
+  pages =	{487--503},
+  series =	{LIPIcs},
+  year =	{2015},
+  volume =	{41}
+}
+
+@inproceedings{Traytel2013,
+  author={D.~Traytel and T.~Nipkow},
+  title={{A} {V}erified {D}ecision {P}rocedure for {MSO} on 
+         {W}ords {B}ased on {D}erivatives of {R}egular {E}xpressions},
+  booktitle={Proc.~of the 18th ACM SIGPLAN International Conference on Functional Programming (ICFP)},
+  pages={3-12},
+  year=2013
+}
+
+@InProceedings{Coquand2012,
+  author =       {T.~Coquand and V.~Siles},
+  title =        {{A} {D}ecision {P}rocedure for {R}egular {E}xpression {E}quivalence in {T}ype {T}heory},
+  booktitle = {Proc.~of the 1st Conference on Certified Programs and Proofs (CPP)},
+  pages =     {119--134},
+  year =      {2011},
+  volume =    {7086},
+  series =    {LNCS}
+}
+
+@InProceedings{Almeidaetal10,
+  author =       {J.~B.~Almeida and N.~Moriera and D.~Pereira and S.~M.~de Sousa},
+  title =        {{P}artial {D}erivative {A}utomata {F}ormalized in {C}oq},
+  booktitle =    {Proc.~of the 15th International Conference on Implementation
+                  and Application of Automata (CIAA)},
+  pages =        {59-68},
+  year =         {2010},
+  volume =       {6482},
+  series =       {LNCS}
+}
+
+@book{Michaelson,
+  title={An introduction to functional programming through lambda calculus},
+  author={Michaelson, Greg},
+  year={2011},
+  publisher={Courier Corporation}
+}
+
+@article{Owens2008,
+  author    = {S.~Owens and K.~Slind},
+  title     = {{A}dapting {F}unctional {P}rograms to {H}igher {O}rder {L}ogic},
+  journal   = {Higher-Order and Symbolic Computation},
+  volume    = {21},
+  number    = {4},
+  year      = {2008},
+  pages     = {377--409}
+}
+
+
+@book{Velleman,
+  title={How to prove it: a structured approach},
+  author={Velleman, Daniel J},
+  year={2006},
+  publisher={Cambridge University Press}
+}
+
+@book{Jones,
+  title={Implementing functional languages:[a tutorial]},
+  author={Jones, Simon L Peyton and Lester, David R},
+  volume={124},
+  year={1992},
+  publisher={Prentice Hall Reading}
+}
+
+@article{Cardelli,
+  title={Type systems},
+  author={Cardelli, Luca},
+  journal={ACM Computing Surveys},
+  volume={28},
+  number={1},
+  pages={263--264},
+  year={1996}
+}
+
+@article{Morrisett,
+  author    = {J. Gregory Morrisett and
+               Karl Crary and
+               Neal Glew and
+               David Walker},
+  title     = {Stack-based typed assembly language},
+  journal   = {J. Funct. Program.},
+  volume    = {13},
+  number    = {5},
+  pages     = {957--959},
+  year      = {2003},
+  url       = {http://dx.doi.org/10.1017/S0956796802004446},
+  doi       = {10.1017/S0956796802004446},
+  timestamp = {Fri, 19 Mar 2004 13:48:27 +0100},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/jfp/MorrisettCGW03},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@book{Nipkow,
+  title={Concrete Semantics: With Isabelle/HOL},
+  author={Nipkow, Tobias and Klein, Gerwin},
+  year={2014},
+  publisher={Springer}
+}
+
+@article{Dube,
+  author    = {Danny Dub{\'{e}} and
+               Marc Feeley},
+  title     = {Efficiently building a parse tree from a regular expression},
+  journal   = {Acta Inf.},
+  volume    = {37},
+  number    = {2},
+  pages     = {121--144},
+  year      = {2000},
+  url       = {http://link.springer.de/link/service/journals/00236/bibs/0037002/00370121.htm},
+  timestamp = {Tue, 25 Nov 2003 14:51:21 +0100},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/acta/DubeF00},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@article{Morrisett2,
+  author    = {J. Gregory Morrisett and
+               David Walker and
+               Karl Crary and
+               Neal Glew},
+  title     = {From system {F} to typed assembly language},
+  journal   = {{ACM} Trans. Program. Lang. Syst.},
+  volume    = {21},
+  number    = {3},
+  pages     = {527--568},
+  year      = {1999},
+  url       = {http://doi.acm.org/10.1145/319301.319345},
+  doi       = {10.1145/319301.319345},
+  timestamp = {Wed, 26 Nov 2003 14:26:46 +0100},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/toplas/MorrisettWCG99},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@article{Owens2,
+  author    = {Scott Owens and
+               Konrad Slind},
+  title     = {Adapting functional programs to higher order logic},
+  journal   = {Higher-Order and Symbolic Computation},
+  volume    = {21},
+  number    = {4},
+  pages     = {377--409},
+  year      = {2008},
+  url       = {http://dx.doi.org/10.1007/s10990-008-9038-0},
+  doi       = {10.1007/s10990-008-9038-0},
+  timestamp = {Wed, 16 Dec 2009 13:51:02 +0100},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/lisp/OwensS08},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+
+@misc{PCRE,
+  title = "{PCRE - Perl Compatible Regular Expressions}",
+  url = {http://www.pcre.org},
+}
+
+
+
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Paper/document/root.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/Paper/document/root.tex	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,53 @@
+\documentclass[runningheads]{llncs}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{mathpartir}
+\usepackage{tikz}
+\usepackage{pgf}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+\usepackage{stmaryrd}
+\usepackage{url}
+\usepackage{color}
+
+\titlerunning{BLA BLA}
+
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+
+\definecolor{mygrey}{rgb}{.80,.80,.80}
+
+\begin{document}
+
+\title{RegEx}
+\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}}
+\institute{King's College London, United Kingdom \and 
+           St Andrews}
+\maketitle
+
+\begin{abstract}
+BLA BLA  Sulzmann and Lu \cite{Sulzmann2014}
+
+{\bf Keywords:} 
+\end{abstract}
+
+\input{session}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/PosixTest.thy
--- a/thys/PosixTest.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-theory PosixTest
-imports Main
-begin
-
-
-
-
-end
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Pr.thy
--- a/thys/Pr.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-theory Pr
-imports Main "~~/src/HOL/Number_Theory/Primes" "~~/src/HOL/Real"
-begin
-
-fun 
-  add :: "nat \<Rightarrow> nat \<Rightarrow> nat" 
-where
-  "add 0 n = n" |
-  "add (Suc m) n = Suc (add m n)"
-
-fun 
-  doub :: "nat \<Rightarrow> nat" 
-where
-  "doub 0 = 0" |
-  "doub n = n + n"
-
-lemma add_lem:
-  "add m n = m + n"
-apply(induct m arbitrary: )
-apply(auto)
-done
-
-fun 
-  count :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
-where
-  "count n Nil = 0" |
-  "count n (x # xs) = (if n = x then (add 1 (count n xs)) else count n xs)"
-
-value "count 3 [1,2,3,3,4,3,5]"
-
-fun 
-  count2 :: "nat \<Rightarrow> nat list \<Rightarrow> nat" 
-where
-"count2 n Nil = 0" |
-"count2 n (Cons x xs) = (if n = x then (add 1 (count2 n xs)) else count2 n xs)"
-
-value "count2 (2::nat) [2,2,3::nat]"
-
-lemma
-  "count2 x xs \<le> length xs"
-apply(induct xs)
-apply(simp)
-apply(simp)
-apply(auto)
-done
-
-fun 
-  sum :: "nat \<Rightarrow> nat"
-where
-  "sum 0 = 0"
-| "sum (Suc n) = (Suc n) + sum n"
-
-lemma
-  "sum n = (n * (Suc n)) div 2"
-apply(induct n)
-apply(auto)
-done
-
-
-lemma
-  "doub n = add n n"
-apply(induct n)
-apply(simp)
-apply(simp add: add_lem)
-done
-
-lemma 
-  fixes a b::nat
-  shows "(a + b) ^ 2 = a ^ 2 + 2 * a * b + b ^ 2"
-apply(simp add: power2_sum)
-done
-
-lemma
-  fixes a b c::"real"
-  assumes eq: "a * c \<le> b * c" and ineq: "b < a"
-  shows "c \<le> 0"
-proof -
-  {
-    assume  "0 < c" 
-    then have "b * c < a * c" using ineq by(auto)
-    then have "False" using eq by auto
-  } then show "c \<le> 0" by (auto simp add: not_le[symmetric]) 
-qed
-    
-
-
-
-lemma "n > 1 \<Longrightarrow> \<not>(prime (2 * n))"
-by (metis One_nat_def Suc_leI less_Suc0 not_le numeral_eq_one_iff prime_product semiring_norm(85))
-
-
-
-lemma 
- fixes n::"nat"
- assumes a: "n > 1"
-    and  b: "\<not>(prime n)"
- shows "\<not>(prime ((2 ^ n) - 1))"   
-using a b
-apply(induct n)
-apply(simp)
-apply(simp)
-
-
-
-end
\ No newline at end of file
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/ProofAutomation.thy
--- a/thys/ProofAutomation.thy	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-theory ProofAutomation
-imports Main
-begin
-
-lemma "\<forall>x. \<exists>y. x = y"
-by auto
-
-lemma "A \<subseteq> B \<inter> C \<Longrightarrow> A \<subseteq> B \<union> C"
-by auto
-
-lemma "\<lbrakk> \<forall> xs \<in> A. \<exists> ys. xs = ys @ ys; us \<in> A \<rbrakk> \<Longrightarrow> \<exists>n. length us = n+n"
-by fastforce
-
-lemma "\<lbrakk>xs @ ys = ys @ xs; length xs = length ys \<rbrakk> \<Longrightarrow> xs = ys"
-by auto
-
-lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c\<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c"
-by arith
-
-lemma "\<lbrakk> (a::nat) \<le> b; b \<le> c; c \<le> d; d \<le> e \<rbrakk> \<Longrightarrow> a \<le> e"
-by (blast intro: le_trans)
-
-lemma "Suc(Suc(Suc a)) \<le> b \<Longrightarrow> a \<le> b"
-by(blast dest: Suc_leD)
-
-inductive ev :: "nat \<Rightarrow> bool" where
-ev0: "ev 0" |
-evSS: "ev n \<Longrightarrow> ev (n + 2)"
-
-fun even :: "nat \<Rightarrow> bool" where
-"even 0 = True" |
-"even (Suc 0) = False" |
-"even (Suc(Suc n)) = even n"
-
-lemma "ev m \<Longrightarrow> even m"
-
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/README
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/README	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,23 @@
+Theories:
+=========
+
+ ReStar.thy
+
+The repository can be checked using Isabelle 2014.
+
+  isabelle build -c -v -d . Lex
+
+  isabelle build -c -v -d . Paper
+
+Othe directories are:
+=====================
+
+  Paper
+  Literature
+  
+
+
+
+
+
+
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys/ROOT	Fri Feb 05 10:16:10 2016 +0000
@@ -0,0 +1,13 @@
+session "Lex" = HOL +
+  theories [document = false, quick_and_dirty]
+	"ReStar" 
+
+session Paper in "Paper" = Lex +
+  options [document = pdf, document_output = "..", document_variants="paper"]
+  theories 
+    "~~/src/HOL/Library/LaTeXsugar"
+    "Paper"
+  document_files
+    "root.bib"
+    "root.tex" 
+
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/ReStar.thy
--- a/thys/ReStar.thy	Tue Feb 02 02:27:16 2016 +0000
+++ b/thys/ReStar.thy	Fri Feb 05 10:16:10 2016 +0000
@@ -540,8 +540,8 @@
   "Values (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   "Values (ALT r1 r2) s = {Left v | v. v \<in> Values r1 s} \<union> {Right v | v. v \<in> Values r2 s}"
   "Values (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> Values r1 s \<and> v2 \<in> Values r2 (rest v1 s)}"
-  "Values (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> 
-                                                               Star vs \<in> Values (STAR r) (rest v s)}"
+  "Values (STAR r) s = 
+      {Star []} \<union> {Star (v # vs) | v vs. v \<in> Values r s \<and> Star vs \<in> Values (STAR r) (rest v s)}"
 unfolding Values_def
 apply(auto)
 (*NULL*)
@@ -589,8 +589,8 @@
   "NValues (CHAR c) s = (if [c] \<sqsubseteq> s then {Char c} else {})" 
   "NValues (ALT r1 r2) s = {Left v | v. v \<in> NValues r1 s} \<union> {Right v | v. v \<in> NValues r2 s}"
   "NValues (SEQ r1 r2) s = {Seq v1 v2 | v1 v2. v1 \<in> NValues r1 s \<and> v2 \<in> NValues r2 (rest v1 s)}"
-  "NValues (STAR r) s = {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and> 
-                                                               Star vs \<in> NValues (STAR r) (rest v s)}"
+  "NValues (STAR r) s = 
+  {Star []} \<union> {Star (v # vs) | v vs. v \<in> NValues r s \<and> flat v \<noteq> [] \<and>  Star vs \<in> NValues (STAR r) (rest v s)}"
 unfolding NValues_def
 apply(auto)
 (*NULL*)
@@ -1217,6 +1217,15 @@
 
 lemma lex_correct4:
   assumes "s \<in> L r"
+  shows "\<exists>v. lex r s = Some(v) \<and> \<Turnstile> v : r \<and> flat v = s"
+using lex_correct3[OF assms]
+apply(auto)
+apply (metis PMatch1N)
+by (metis PMatch1(2))
+
+
+lemma lex_correct5:
+  assumes "s \<in> L r"
   shows "s \<in> r \<rightarrow> (lex2 r s)"
 using assms
 apply(induct s arbitrary: r)
@@ -1243,6 +1252,7 @@
 
 thm PMatch.intros
 
+(*
 inductive ValOrd :: "string \<Rightarrow> val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<turnstile> _ \<succ>_ _" [100, 100, 100, 100] 100)
 where
   "\<lbrakk>s2 \<turnstile> v2 \<succ>r2 v2'; flat v1 = s1\<rbrakk> \<Longrightarrow> (s1 @ s2) \<turnstile> (Seq v1 v2) \<succ>(SEQ r1 r2) (Seq v1 v2')" 
@@ -1253,7 +1263,7 @@
 | "s \<turnstile> v1 \<succ>r1 v1' \<Longrightarrow> s \<turnstile> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 | "s \<turnstile> Void \<succ>EMPTY Void"
 | "(c#s) \<turnstile> (Char c) \<succ>(CHAR c) (Char c)"
-
+*)
 
 inductive ValOrd :: "val \<Rightarrow> rexp \<Rightarrow> val \<Rightarrow> bool" ("_ \<succ>_ _" [100, 100, 100] 100)
 where
@@ -1265,6 +1275,13 @@
 | "v1 \<succ>r1 v1' \<Longrightarrow> (Left v1) \<succ>(ALT r1 r2) (Left v1')"
 | "Void \<succ>EMPTY Void"
 | "(Char c) \<succ>(CHAR c) (Char c)"
+| "flat (Star (v # vs)) = [] \<Longrightarrow> (Star []) \<succ>(STAR r) (Star (v # vs))"
+| "flat (Star (v # vs)) \<noteq> [] \<Longrightarrow> (Star (v # vs)) \<succ>(STAR r) (Star [])"
+| "v1 \<succ>r v2 \<Longrightarrow> (Star (v1 # vs1)) \<succ>(STAR r) (Star (v2 # vs2))"
+| "(Star vs1) \<succ>(STAR r) (Star vs2) \<Longrightarrow> (Star (v # vs1)) \<succ>(STAR r) (Star (v # vs2))"
+| "(Star []) \<succ>(STAR r) (Star [])"
+
+(*
 
 lemma ValOrd_PMatch:
   assumes "s \<in> r \<rightarrow> v1" "\<turnstile> v2 : r" "flat v2  \<sqsubseteq> s"
@@ -1272,30 +1289,55 @@
 using assms
 apply(induct r arbitrary: s v1 v2 rule: rexp.induct)
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis ValOrd.intros(7))
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis ValOrd.intros(8))
 defer
 apply(erule Prf.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis ValOrd.intros(6))
 apply (metis PMatch1(2) Prf_flat_L ValOrd.intros(4) length_sprefix sprefix_def)
 apply(clarify)
 apply(erule PMatch.cases)
-apply(simp_all)[5]
+apply(simp_all)[7]
 apply (metis PMatch1(2) ValOrd.intros(3) length_sprefix less_imp_le_nat order_refl sprefix_def)
 apply(clarify)
 apply (metis ValOrd.intros(5))
+(* Star case *)
+apply(erule Prf.cases)
+apply(simp_all)[7]
+apply(erule PMatch.cases)
+apply(simp_all)
+apply (metis Nil_is_append_conv ValOrd.intros(10) flat.simps(7))
+apply (metis ValOrd.intros(13))
+apply(clarify)
+apply(erule PMatch.cases)
+apply(simp_all)
+prefer 2
+apply(rule ValOrd.intros)
+apply(simp add: prefix_def)
+apply(rule ValOrd.intros)
+apply(drule_tac x="s1" in meta_spec)
+apply(drule_tac x="va" in meta_spec)
+apply(drule_tac x="v" in meta_spec)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(simp)
+apply(drule_tac meta_mp)
+apply(simp add: prefix_def)
+apply(auto)[1]
+prefer 3
 (* Seq case *)
 apply(erule Prf.cases)
 apply(simp_all)[5]
@@ -2870,4 +2912,7 @@
 apply(auto simp add: POSIX_def)[1]
 apply(erule Prf.cases)
 apply(simp_all)[5]
-oops
\ No newline at end of file
+oops
+*)
+
+end
\ No newline at end of file
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/Test.txt
--- a/thys/Test.txt	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,7 +0,0 @@
-<<<<<<< local
-test2
-=======
-test
-test file
-
->>>>>>> other
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/new test
--- a/thys/new test	Tue Feb 02 02:27:16 2016 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-ssh://fahad@talisker.inf.kcl.ac.uk//Users/urbanc/HGREPOS/lexing
diff -r 5b01f7c233f8 -r a33d3040bf7e thys/paper.pdf
Binary file thys/paper.pdf has changed