# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1381698561 -7200
# Node ID cf451e182bf0a3ab98b78d066f7280621c85caa1
# Parent  c9a1c6f50ff5fc3d55d5cedc06978206fb3b59dd
added slides

diff -r c9a1c6f50ff5 -r cf451e182bf0 Nominal/Nominal2_Abs.thy
--- a/Nominal/Nominal2_Abs.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Nominal/Nominal2_Abs.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -51,7 +51,7 @@
   and   "R1 \<le> R2 \<Longrightarrow> alpha_res bs R1 \<le> alpha_res bs R2"
   and   "R1 \<le> R2 \<Longrightarrow> alpha_lst cs R1 \<le> alpha_lst cs R2"
   by (case_tac [!] bs, case_tac [!] cs) 
-     (auto simp add: le_fun_def le_bool_def alphas)
+     (auto simp: le_fun_def le_bool_def alphas)
 
 section {* Equivariance *}
 
@@ -87,7 +87,7 @@
   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
   unfolding alphas fresh_star_def
   using a
-  by (auto simp add: fresh_minus_perm)
+  by (auto simp: fresh_minus_perm)
 
 lemma alpha_trans:
   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
@@ -204,7 +204,7 @@
   unfolding alphas
   unfolding fresh_star_def
   by (erule_tac [!] exE, rule_tac [!] x="-p" in exI)
-     (auto simp add: fresh_minus_perm)
+     (auto simp: fresh_minus_perm)
 
 lemma alphas_abs_trans:
   shows "\<lbrakk>(bs, x) \<approx>abs_set (cs, y); (cs, y) \<approx>abs_set (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_set (ds, z)"
@@ -278,9 +278,9 @@
     using set_renaming_perm2 by blast
   from * have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from 0 have 1: "(supp x - as) \<sharp>* p" using *
-    by (auto simp add: fresh_star_def fresh_perm)
+    by (auto simp: fresh_star_def fresh_perm)
   then have 2: "(supp x - as) \<inter> supp p = {}"
-    by (auto simp add: fresh_star_def fresh_def)
+    by (auto simp: fresh_star_def fresh_def)
   have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
   have "supp p \<subseteq> supp x \<union> p' \<bullet> supp x" using ** by simp
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as)))" 
@@ -303,7 +303,7 @@
 lemma alpha_abs_res_minimal:
   assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
   shows "(as \<inter> supp x, x) \<approx>res (op =) supp p (as' \<inter> supp x', x')"
-  using asm unfolding alpha_res by (auto simp add: Diff_Int)
+  using asm unfolding alpha_res by (auto simp: Diff_Int)
 
 lemma alpha_abs_res_abs_set:
   assumes asm: "(as, x) \<approx>res (op =) supp p (as', x')"
@@ -323,7 +323,7 @@
 lemma alpha_abs_set_abs_res:
   assumes asm: "(as \<inter> supp x, x) \<approx>set (op =) supp p (as' \<inter> supp x', x')"
   shows "(as, x) \<approx>res (op =) supp p (as', x')"
-  using asm unfolding alphas by (auto simp add: Diff_Int)
+  using asm unfolding alphas by (auto simp: Diff_Int)
 
 lemma alpha_abs_res_stronger1:
   assumes asm: "(as, x) \<approx>res (op =) supp p' (as', x')"
@@ -344,15 +344,15 @@
   then have a: "p \<bullet> x = p' \<bullet> x" using supp_perm_perm_eq by auto
   from * have "\<forall>b \<in> as. p \<bullet> b = p' \<bullet> b" by blast
   then have zb: "p \<bullet> as = p' \<bullet> as" 
-    apply(auto simp add: permute_set_def)
+    apply(auto simp: permute_set_def)
     apply(rule_tac x="xa" in exI)
     apply(simp)
     done
   have zc: "p' \<bullet> as = as'" using asm by (simp add: alphas)
   from 0 have 1: "(supp x - as) \<sharp>* p" using *
-    by (auto simp add: fresh_star_def fresh_perm)
+    by (auto simp: fresh_star_def fresh_perm)
   then have 2: "(supp x - as) \<inter> supp p = {}"
-    by (auto simp add: fresh_star_def fresh_def)
+    by (auto simp: fresh_star_def fresh_def)
   have b: "supp x = (supp x - as) \<union> (supp x \<inter> as)" by auto
   have "supp p \<subseteq> supp x \<union> as \<union> p' \<bullet> supp x \<union> p' \<bullet> as" using ** using union_eqvt by blast
   also have "\<dots> = (supp x - as) \<union> (supp x \<inter> as) \<union> as \<union> (p' \<bullet> ((supp x - as) \<union> (supp x \<inter> as))) \<union> p' \<bullet> as" 
@@ -390,9 +390,9 @@
   then have zb: "p \<bullet> as = p' \<bullet> as" by (induct as) (auto)
   have zc: "p' \<bullet> set as = set as'" using asm by (simp add: alphas set_eqvt)
   from 0 have 1: "(supp x - set as) \<sharp>* p" using *
-    by (auto simp add: fresh_star_def fresh_perm)
+    by (auto simp: fresh_star_def fresh_perm)
   then have 2: "(supp x - set as) \<inter> supp p = {}"
-    by (auto simp add: fresh_star_def fresh_def)
+    by (auto simp: fresh_star_def fresh_def)
   have b: "supp x = (supp x - set as) \<union> (supp x \<inter> set as)" by auto
   have "supp p \<subseteq> supp x \<union> set as \<union> p' \<bullet> supp x \<union> p' \<bullet> set as" using ** using union_eqvt by blast
   also have "\<dots> = (supp x - set as) \<union> (supp x \<inter> set as) \<union> set as \<union> 
@@ -420,14 +420,14 @@
   and   "(bs, x) \<approx>abs_lst (bs', x') \<longleftrightarrow> 
    (\<exists>p. (bs, x) \<approx>lst (op =) supp p (bs', x') \<and> supp p \<subseteq> set bs \<union> set bs')"
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_set_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs alpha_abs_set_stronger1)[1]
+apply(auto simp: alphas_abs)[1]
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_res_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs alpha_abs_res_stronger1)[1]
+apply(auto simp: alphas_abs)[1]
 apply(rule iffI)
-apply(auto simp add: alphas_abs alpha_abs_lst_stronger1)[1]
-apply(auto simp add: alphas_abs)[1]
+apply(auto simp: alphas_abs alpha_abs_lst_stronger1)[1]
+apply(auto simp: alphas_abs)[1]
 done
 
 lemma alpha_res_alpha_set:
@@ -603,7 +603,7 @@
   unfolding swap_set_not_in[OF a1 a2] 
   using a1 a2
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
+     (auto simp: supp_perm swap_atom)
 
 lemma Abs_swap2:
   assumes a1: "a \<notin> (supp x) - (set bs)"
@@ -616,7 +616,7 @@
   unfolding swap_set_not_in[OF a1 a2]
   using a1 a2
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
-     (auto simp add: supp_perm swap_atom)
+     (auto simp: supp_perm swap_atom)
 
 lemma Abs_supports:
   shows "((supp x) - as) supports ([as]set. x)"
@@ -732,7 +732,7 @@
   and   "as \<sharp>* ([bs]res. x) \<longleftrightarrow> (as - bs) \<sharp>* x"
   and   "as \<sharp>* ([cs]lst. x) \<longleftrightarrow> (as - set cs) \<sharp>* x"
   unfolding fresh_star_def
-  by (auto simp add: Abs_fresh_iff)
+  by (auto simp: Abs_fresh_iff)
 
 lemma Abs_fresh_star:
   fixes x::"'a::fs"
@@ -740,7 +740,7 @@
   and   "as \<subseteq> as' \<Longrightarrow> as \<sharp>* ([as']res. x)"
   and   "bs \<subseteq> set bs' \<Longrightarrow> bs \<sharp>* ([bs']lst. x)"
   unfolding fresh_star_def
-  by(auto simp add: Abs_fresh_iff)
+  by(auto simp: Abs_fresh_iff)
 
 lemma Abs_fresh_star2:
   fixes x::"'a::fs"
@@ -760,7 +760,7 @@
   and   "[{atom a}]res. x = [{atom a}]res. y \<longleftrightarrow> x = y"
   and   "[[atom a]]lst. x = [[atom a]]lst. y \<longleftrightarrow> x = y"
 unfolding Abs_eq_iff2 alphas
-by (auto simp add: supp_perm_singleton fresh_star_def fresh_zero_perm)
+by (auto simp: supp_perm_singleton fresh_star_def fresh_zero_perm)
 
 lemma Abs1_eq_iff_fresh:
   fixes x y::"'a::fs"
@@ -808,28 +808,28 @@
   fixes x y::"'a::fs"
   and z::"'c::fs"
   and a b::"'b::at"
-  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
-  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
-  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> (a, b, x, y, z) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
+  and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (\<forall>c. atom c \<sharp> z \<longrightarrow> atom c \<sharp> (a, b, x, y) \<longrightarrow> (a \<leftrightarrow> c) \<bullet> x = (b \<leftrightarrow> c) \<bullet> y)"
 apply(auto) 
 apply(simp add: Abs1_eq_iff_fresh(1)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(1))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(2)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(2))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 apply(simp add: Abs1_eq_iff_fresh(3)[symmetric])
 apply(rule_tac ?'a="'b::at" and x="(a, b, x, y, z)" in obtain_fresh)
 apply(drule_tac x="aa" in spec)
 apply(simp)
 apply(subst Abs1_eq_iff_fresh(3))
-apply(auto simp add: fresh_Pair)[2]
+apply(auto simp: fresh_Pair)[2]
 done
 
 lemma Abs1_eq_iff:
@@ -918,7 +918,7 @@
   shows "[{atom a}]set. x = [{atom b}]set. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
   and   "[{atom a}]res. x = [{atom b}]res. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
   and   "[[atom a]]lst. x = [[atom b]]lst. y \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> (b \<leftrightarrow> a) \<bullet> x = y \<and> atom b \<sharp> x)"
-using assms by (auto simp add: Abs1_eq_iff fresh_permute_left)
+using assms by (auto simp: Abs1_eq_iff fresh_permute_left)
 
 
 ML {*
@@ -1078,7 +1078,7 @@
 lemma prod_fv_supp:
   shows "prod_fv supp supp = supp"
 by (rule ext)
-   (auto simp add: supp_Pair)
+   (auto simp: supp_Pair)
 
 lemma prod_alpha_eq:
   shows "prod_alpha (op=) (op=) = (op=)"
diff -r c9a1c6f50ff5 -r cf451e182bf0 ROOT
--- a/ROOT	Fri Sep 06 10:06:41 2013 +0100
+++ b/ROOT	Sun Oct 13 23:09:21 2013 +0200
@@ -69,4 +69,39 @@
      "~~/src/HOL/Library/LaTeXsugar"
    theories 
      "Paper"
-   files "document/root.bib" "document/root.tex" 
\ No newline at end of file
+   files "document/root.bib" "document/root.tex"
+
+session Slides1 in "Slides" = Nominal2 +
+  options [document = pdf, document_output= "..", document_variants = "slides1"]
+  theories
+    "Slides1"
+
+session Slides2 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides2"]
+  theories
+    "Slides2"
+
+session Slides3 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides3"]
+  theories
+    "Slides3"
+
+session Slides4 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides4"]
+  theories
+    "Slides4"
+
+session Slides5 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides5"]
+  theories
+    "Slides5"
+
+session Slides9 in "Slides" = Nominal2 +
+  options [quick_and_dirty, document = pdf, document_output= "..", document_variants = "slides9"]
+  theories
+    "Slides9"
+
+session SlidesB in "Slides" = Nominal2 +
+  options [document = pdf, document_output= "..", document_variants = "slidesb"]
+  theories
+    "SlidesB" 
\ No newline at end of file
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides1.thy
--- a/Slides/Slides1.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides1.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides1
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides2.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides2
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)
@@ -385,7 +385,7 @@
 
   {\small\begin{tabular}{rcl}
   @{text "sort_ty (TVar x)"}  & @{text "\<equiv>"} & @{text "Sort ''TVar'' [Sort x []]"} \\
-  @{text "sort_ty (\<tau>\<^isub>1 \<rightarrow> \<tau>\<^isub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^isub>1, sort_ty \<tau>\<^isub>2]"}\\
+  @{text "sort_ty (\<tau>\<^sub>1 \<rightarrow> \<tau>\<^sub>2)"} & @{text "\<equiv>"} & @{text "Sort ''Fun'' [sort_ty \<tau>\<^sub>1, sort_ty \<tau>\<^sub>2]"}\\
   \end{tabular}}
   \pause
   \isanewline\isanewline
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides3.thy
--- a/Slides/Slides3.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides3.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides3
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 declare [[show_question_marks = false]]
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides4.thy
--- a/Slides/Slides4.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides4.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides4
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 declare [[show_question_marks = false]]
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides5.thy
--- a/Slides/Slides5.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides5.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides5
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/Slides9.thy
--- a/Slides/Slides9.thy	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/Slides9.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory Slides9
-imports "~~/src/HOL/Library/LaTeXsugar" "Nominal"
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
 begin
 
 notation (latex output)
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/SlidesB.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/SlidesB.thy	Sun Oct 13 23:09:21 2013 +0200
@@ -0,0 +1,735 @@
+(*<*)
+theory SlidesB
+imports "~~/src/HOL/Library/LaTeXsugar" "../Nominal/Nominal2"
+begin
+
+notation (latex output)
+  set ("_") and
+  Cons  ("_::/_" [66,65] 65) 
+
+(*>*)
+
+
+text_raw {*
+  %% was \begin{colormixin}{20!averagebackgroundcolor}
+  %% 
+  %% is \begin{colormixin}{50!averagebackgroundcolor}
+  \renewcommand{\slidecaption}{Dagstuhl, 14 October 2013}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{%
+  \begin{tabular}{@ {}c@ {}}
+  \Huge Nominal Isabelle\\[0mm]
+  \Large or, How Not to be Intimidated by\\[-3mm]
+  \Large the Variable Convention\\[-5mm]
+  \end{tabular}}
+  
+  \begin{center}
+  Christian Urban\\[1mm]
+  King's College London\\[-6mm]\mbox{}
+  \end{center}
+ 
+  \begin{center}
+  \begin{block}{}
+  \color{gray}
+  \small
+  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 
+  If $M_1,\ldots,M_n$ occur in a certain mathematical context
+  (e.g. definition, proof), then in these terms all bound variables 
+  are chosen to be different from the free variables.\\[2mm]
+  
+  \footnotesize\hfill Henk Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
+  \end{block}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{}
+
+  \begin{itemize}
+  \item \normalsize Aim: develop Nominal Isabelle for reasoning about programming languages\\[-10mm]\mbox{}
+  \end{itemize}
+  
+  \begin{center}
+  \begin{block}{}
+  \color{gray}
+  \footnotesize
+  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] 
+  If $M_1,\ldots,M_n$ occur in a certain mathematical context
+  (e.g. definition, proof), then in these terms all bound variables 
+  are chosen to be different from the free variables.\hfill ---Henk Barendregt
+  \end{block}
+  \end{center}\pause
+
+  \mbox{}\\[-19mm]\mbox{}
+
+  \begin{itemize}
+  \item found an error in an ACM journal paper by Bob Harper and Frank Pfenning 
+  about LF (and fixed it in three ways)
+  \item found also fixable errors in my Ph.D.-thesis about cut-elimination
+  (examined by Henk Barendregt and Andy Pitts)
+  \item found the variable convention can in principle be used for proving false
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Nominal Techniques}
+
+  \begin{itemize}
+  \item Andy Pitts showed me that permutations\\ preserve $\alpha$-equivalence:
+  \begin{center}
+  \smath{t_1 \approx_{\alpha} t_2 \quad \Rightarrow\quad \pi \act t_1 \approx_{\alpha} \pi \act t_2} 
+  \end{center}
+
+  \item also permutations and substitutions commute, if you suspend permutations
+  in front of variables
+  \begin{center}
+  \smath{\pi\act\sigma(t) = \sigma(\pi\act t)}
+  \end{center}\medskip\medskip
+
+  \item this allowed us to define as simple Nominal Unification algorithm\medskip
+  \begin{center}
+  \smath{\nabla \vdash t \approx^?_{\alpha} t'}\hspace{2cm}
+  \smath{\nabla \vdash a \fresh^? t}
+  \end{center}
+  \end{itemize}
+
+  %\begin{textblock}{3}(13.1,1.3)
+  %\includegraphics[scale=0.26]{andrewpitts.jpg}
+  %\end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Nominal Isabelle}
+
+  \begin{itemize}
+  \item a general theory about atoms and permutations\medskip
+  \begin{itemize}
+  \item sorted atoms and
+  \item sort-respecting permutations
+  \end{itemize}
+  
+  \item support and freshness
+  \begin{center}
+  \begin{tabular}{l}
+  \smath{\textit{supp}(x) \dn \{ a \mid \textit{infinite}\,\{ b \mid \swap{a}{b}\act x \not= x\}\}}\\
+  \smath{a \fresh x \dn a \notin \textit{supp}(x)}
+  \end{tabular}
+  \end{center}\bigskip\pause
+
+  \item allow users to reason about alpha-equivalence classes like about 
+  syntax trees
+  %
+  %\item $\alpha$-equivalence
+  %\begin{center}
+  %\begin{tabular}{l}
+  %\smath{as.x \approx_\alpha bs.y \dn}\\[2mm]
+  %\hspace{2cm}\smath{\exists \pi.\;\text{supp}(x) - as = \text{supp}(y) - bs}\\ 
+  %\hspace{2cm}\smath{\;\wedge\; \text{supp}(x) - as \fresh \pi}\\
+  %\hspace{2cm}\smath{\;\wedge\; \pi \act x = y}
+  %\end{tabular}
+  %\end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-7>
+  \frametitle{New Types in HOL}
+
+   \begin{center}
+  \begin{tikzpicture}[scale=1.5]
+  %%%\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \onslide<2-4,6->{\draw[very thick] (0.7,0.4) circle (4.25mm);}
+  \onslide<1-4,6->{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
+  \onslide<3-5,6->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
+  
+  \onslide<3-4,6->{\draw (-2.0, 0.845) --  (0.7,0.845);}
+  \onslide<3-4,6->{\draw (-2.0,-0.045)  -- (0.7,-0.045);}
+
+  \onslide<4-4,6->{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
+  \onslide<4-5,6->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
+  \onslide<1-4,6->{\draw (1.8, 0.48) node[right=-0.1mm]
+    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<4-4,6->{\alert{(sets of raw terms)}}\end{tabular}};}
+  \onslide<2-4,6->{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
+  \onslide<3-5,6->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
+  
+  \onslide<3-4,6->{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
+  \onslide<3-4,6->{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
+
+  \onslide<6->{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+  \end{tikzpicture}
+  \end{center}
+  
+  \begin{center}
+  \textcolor{red}{\large\bf\onslide<6->{define \boldmath$\alpha$-equivalence}}
+  \end{center}
+
+  \begin{textblock}{9}(2.8,12.5)
+  \only<7>{
+  \begin{tikzpicture}
+  \draw (0,0) node[fill=cream, text width=8cm, thick, draw=red, rounded corners=1mm] (nn)
+  {The ``new types'' are the reason why there is no Nominal Coq.};
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>[c]
+  \frametitle{HOL vs.~Nominal}
+
+  \begin{itemize}
+  \item Nominal logic by Pitts are incompatible 
+  with choice principles\medskip
+
+  \item HOL includes Hilbert's epsilon\pause\bigskip
+
+  \item The solution: Do not require that everything has finite support\medskip
+
+  \begin{center}
+  \smath{\onslide<1-2>{\textit{finite}(\textit{supp}(x))  \quad\Rightarrow\quad} a \fresh a.x}
+  \end{center}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-5>
+  \frametitle{\begin{tabular}{c}Our Work\end{tabular}}
+  \mbox{}\\[-6mm]
+
+    \begin{center}
+  \begin{tikzpicture}[scale=1.5]
+  %%%\draw[step=2mm] (-4,-1) grid (4,1);
+  
+  \onslide<1>{\draw[very thick] (0.7,0.4) circle (4.25mm);}
+  \onslide<1>{\draw[rounded corners=1mm, very thick] ( 0.0,-0.8) rectangle ( 1.8, 0.9);}
+  \onslide<1->{\draw[rounded corners=1mm, very thick] (-1.95,0.85) rectangle (-2.85,-0.05);}
+  
+  \onslide<1>{\draw (-2.0, 0.845) --  (0.7,0.845);}
+  \onslide<1>{\draw (-2.0,-0.045)  -- (0.7,-0.045);}
+
+  \onslide<1>{\alert{\draw ( 0.7, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-\\[-1mm]classes\end{tabular}};}}
+  \onslide<1->{\alert{\draw (-2.4, 0.4) node {\footnotesize\begin{tabular}{@ {}c@ {}}$\alpha$-eq.\\[-1mm]terms\end{tabular}};}}
+  \onslide<1>{\draw (1.8, 0.48) node[right=-0.1mm]
+    {\footnotesize\begin{tabular}{@ {}l@ {}}existing\\[-1mm] type\\ \onslide<1>{\alert{(sets of raw terms)}}\end{tabular}};}
+  \onslide<1>{\draw (0.9, -0.35) node {\footnotesize\begin{tabular}{@ {}l@ {}}non-empty\\[-1mm]subset\end{tabular}};}
+  \onslide<1->{\draw (-3.25, 0.55) node {\footnotesize\begin{tabular}{@ {}l@ {}}new\\[-1mm]type\end{tabular}};}
+  
+  \onslide<1>{\draw[<->, very thick] (-1.8, 0.3) -- (-0.1,0.3);}
+  \onslide<1>{\draw (-0.95, 0.3) node[above=0mm] {\footnotesize{}isomorphism};}
+
+  \onslide<1>{\draw[->, line width=2mm, red] (-1.0,-0.4) -- (0.35,0.16);}
+  \end{tikzpicture}
+  \end{center}
+  
+  \begin{textblock}{9.5}(6,3.5)
+  \begin{itemize}
+  \item<1-> defined fv and $\alpha$
+  \item<2-> built quotient / new type
+  \item<3-> derived a reasoning infrastructure ($\fresh$, distinctness, injectivity, cases,\ldots) 
+  \item<4-> derive a {\bf stronger} cases lemma
+  \item<5-> from this, a {\bf stronger} induction principle (Barendregt variable convention built in)\\
+  \begin{center}
+  \textcolor{blue}{Foo ($\lambda x. \lambda y. t$) ($\lambda u. \lambda v. s$)} 
+  \end{center}
+  \end{itemize}
+  \end{textblock}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{Nominal Isabelle} 
+
+  \begin{itemize}
+  \item Users can define lambda-terms as:
+  \end{itemize}
+*}
+      
+ atom_decl name   text_raw {*\medskip\isanewline *}
+	nominal_datatype lam =
+	    Var "name"
+	  | App "lam" "lam" 
+	  | Lam x::"name" t::"lam" binds x in t ("Lam _. _")
+
+
+text_raw {*
+  \mbox{}\bigskip
+
+  \begin{itemize}
+  \item These are \underline{\bf named} alpha-equivalence classes, for example
+  \end{itemize}
+
+  \begin{center}
+  \gb{@{text "Lam a.(Var a)"}} \alert{$\,=\,$} \gb{@{text "Lam b.(Var b)"}}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{\Large (Weak) Induction Principles} 
+
+  \begin{itemize}
+  \item The usual induction principle for lambda-terms is as follows:
+
+  \begin{center}
+  \mbox{}\hspace{-1mm}\begin{beamercolorbox}[sep=1mm, wd=9cm]{boxcolor}
+  \centering\smath{%
+  \infer{P\,t}
+  {\begin{array}{l}
+  \forall x.\;P\,x\\[2mm]
+  \forall t_1\,t_2.\;P\,t_1\wedge P\,t_2\Rightarrow P\,(t_1\;t_2)\\[2mm]
+  \forall x\,t.\;P\,t\Rightarrow P\,(\lambda x.t)\\
+  \end{array}
+  }}
+  \end{beamercolorbox}
+  \end{center}
+
+  \item It requires us in the lambda-case to show the property \smath{P} for
+  all binders \smath{x}.\smallskip\\ 
+
+  (This nearly always requires renamings and they can be 
+  tricky to automate.)
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{\Large Strong Induction Principles} 
+
+  \begin{itemize}
+  \item Therefore we introduced the following strong induction principle:
+
+  \begin{center}
+  \mbox{}\hspace{-2mm}\begin{beamercolorbox}[sep=1mm, wd=11.5cm]{boxcolor}
+  \centering\smath{%
+  \infer{\tikz[remember picture] \node[inner sep=1mm] (n1a) {\alert<4>{$P$}};%
+         \tikz[remember picture] \node[inner sep=1mm] (n2a) {\alert<3>{$c$}};%
+         \tikz[remember picture] \node[inner sep=1mm] (n3a) {\alert<2>{$t$}};}
+  {\begin{array}{l}
+  \forall x\,c.\;P\,c\;x\\[2mm]
+  \forall t_1\,t_2\,c.\;(\forall d.\,P d\,t_1)\wedge (\forall d. P\,d\,t_2)
+  \Rightarrow P\,c\;(t_1\,t_2)\\[2mm]
+  \forall x\,t\,c.\;\alert<1>{x\fresh \alert<3>{c}} 
+  \wedge (\forall d. P\,d\,t)\Rightarrow P\,c\;(\lambda x.t)
+  \end{array}
+  }}
+  \end{beamercolorbox}
+  \end{center}
+  \end{itemize}
+
+  \begin{textblock}{11}(0.9,10.9)
+  \only<2>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=10.5cm, thick, draw=red, rounded corners=1mm] (n3b)
+  { The variable over which the induction proceeds:\\[2mm]
+    \hspace{3mm}``\ldots By induction over the structure of \smath{M}\ldots''};
+
+  \path[overlay, ->, ultra thick, red] (n3b) edge[out=90, in=-110] (n3a);
+  \end{tikzpicture}}
+
+  \only<3>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n2b)
+  {The {\bf context} of the induction; i.e.~what the binder should be fresh for
+   $\quad\Rightarrow$ \smath{(x,y,N,L)}:\\[2mm]
+   ``\ldots By the variable convention we can assume \mbox{\smath{z\not\equiv x,y}} 
+     and \smath{z} not free in \smath{N}$\!$,\,\smath{L}\ldots''};
+
+  \path[overlay, ->, ultra thick, red] (n2b) edge[out=90, in=-100] (n2a);
+  \end{tikzpicture}}
+
+  \only<4>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=11cm, thick, draw=red, rounded corners=1mm] (n1b)
+  {The property to be proved by induction:\\[-3mm]
+  \begin{center}\small
+  \begin{tabular}{l}
+  \smath{\!\!\lambda
+  (x,\!y,\!N\!,\!L).\,\lambda M.\;\,x\not=y\,\wedge\,x\fresh L\,\Rightarrow}\\[1mm]
+  \hspace{8mm}
+  \smath{M[x\!:=\!N][y\!:=\!L] = M[y\!:=\!L][x\!:=\!N[y\!:=\!L]]}  
+  \end{tabular}
+  \end{center}};
+
+  \path[overlay, ->, ultra thick, red] (n1b) edge[out=90, in=-70] (n1a);
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-4>
+  \frametitle{\begin{tabular}{c}Binding Sets of Names\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item binding sets of names has some interesting properties:\medskip
+  
+  \begin{center}
+  \begin{tabular}{l}
+  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{y, x\}.\, y \rightarrow x$}
+  \bigskip\smallskip\\
+
+  \onslide<2->{%
+  \textcolor{blue}{$\forall\{x, y\}.\, x \rightarrow y \;\;\not\approx_\alpha\;\; \forall\{z\}.\, z \rightarrow z$}
+  }\bigskip\smallskip\\
+
+  \onslide<3->{%
+  \textcolor{blue}{$\forall\{x\}.\, x \rightarrow y \;\;\approx_\alpha\;\; \forall\{x, \alert{z}\}.\, x \rightarrow y$}
+  }\medskip\\
+  \onslide<3->{\hspace{4cm}\small provided $z$ is fresh for the type}
+  \end{tabular}
+  \end{center}
+  \end{itemize}
+  
+  \begin{textblock}{8}(2,14.5)
+  \footnotesize $^*$ $x$, $y$, $z$ are assumed to be distinct
+  \end{textblock}
+
+  \only<4>{
+  \begin{textblock}{6}(2.5,4)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\normalsize\color{darkgray}
+  \begin{minipage}{8cm}\raggedright
+  For type-schemes the order of bound names does not matter, and
+  $\alpha$-equivalence is preserved under \alert{vacuous} binders.
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{\begin{tabular}{c}Other Binding Modes\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item alpha-equivalence being preserved under vacuous binders is \underline{not} always
+  wanted:\bigskip\bigskip\normalsize
+  
+  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
+  $\text{let}\;x = 3\;\text{and}\;y = 2\;\text{in}\;x - y\;\text{end}$\medskip\\
+  \onslide<2->{$\;\;\;\only<2>{\approx_\alpha}\only<3>{\alert{\not\approx_\alpha}}
+   \text{let}\;y = 2\;\text{and}\;x = 3\only<3->{\alert{\;\text{and}
+    \;z = \text{loop}}}\;\text{in}\;x - y\;\text{end}$}
+  \end{tabular}}
+  
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>
+  \frametitle{\begin{tabular}{c}\Large{}Even Another Binding Mode\end{tabular}}
+  \mbox{}\\[-3mm]
+
+  \begin{itemize}
+  \item sometimes one wants to abstract more than one name, but the order \underline{does} matter\bigskip
+  
+  \begin{center}
+  \textcolor{blue}{\begin{tabular}{@ {\hspace{-8mm}}l}
+  $\text{let}\;(x, y) = (3, 2)\;\text{in}\;x - y\;\text{end}$\medskip\\
+  $\;\;\;\not\approx_\alpha
+   \text{let}\;(y, x) = (3, 2)\;\text{in}\;x - y\;\text{end}$
+  \end{tabular}}
+  \end{center}
+  
+
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<2-3>
+  \frametitle{\begin{tabular}{c}Specification of Binding\end{tabular}}
+  \mbox{}\\[-6mm]
+
+  \mbox{}\hspace{10mm}
+  \begin{tabular}{ll}
+  \multicolumn{2}{l}{\isacommand{nominal\_datatype} trm $=$}\\
+  \hspace{5mm}\phantom{$|$} Var name\\
+  \hspace{5mm}$|$ App trm trm\\
+  \hspace{5mm}$|$ Lam \only<2->{x::}name \only<2->{t::}trm
+  & \onslide<2->{\isacommand{bind} x \isacommand{in} t}\\
+  \hspace{5mm}$|$ Let \only<2->{as::}assns \only<2->{t::}trm
+  & \onslide<2->{\isacommand{bind} bn(as) \isacommand{in} t}\\
+  \multicolumn{2}{l}{\isacommand{and} assns $=$}\\
+  \multicolumn{2}{l}{\hspace{5mm}\phantom{$|$} ANil}\\
+  \multicolumn{2}{l}{\hspace{5mm}$|$ ACons name trm assns}\\
+  \multicolumn{2}{l}{\onslide<3->{\isacommand{binder} bn \isacommand{where}}}\\
+  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}\phantom{$|$} bn(ANil) $=$ $[]$}}\\
+  \multicolumn{2}{l}{\onslide<3->{\hspace{5mm}$|$ bn(ACons a t as) $=$ $[$a$]$ @ bn(as)}}\\
+  \end{tabular}
+
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{So Far So Good}
+
+  \begin{itemize}
+  \item A Faulty Lemma with the Variable Convention?\\[-8mm]\mbox{}
+  \end{itemize}
+
+  \begin{center}
+  \begin{block}{}
+  \color{gray}
+  \small%
+  {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[1mm] 
+  If $M_1,\ldots,M_n$ occur in a certain mathematical context
+  (e.g. definition, proof), then in these terms all bound variables 
+  are chosen to be different from the free variables.\\[2mm]
+  
+  \footnotesize\hfill Barendregt in ``The Lambda-Calculus: Its Syntax and Semantics''
+  \end{block}
+  \end{center}
+
+  \mbox{}\\[-18mm]\mbox{}
+
+  \begin{columns}
+  \begin{column}[t]{4.7cm}
+  Inductive Definitions:\\
+  \begin{center}
+  \smath{\infer{\text{concl}}{\text{prem}_1 \ldots \text{prem}_n\;\text{scs}}}
+  \end{center}
+  \end{column}
+  \begin{column}[t]{7cm}
+  Rule Inductions:\\[2mm]
+  \begin{tabular}{l@ {\hspace{2mm}}p{5.5cm}}
+  1.) & Assume the property for\\ & the premises. Assume \\ & the side-conditions.\\[1mm]
+  2.) & Show the property for\\ & the conclusion.\\
+  \end{tabular}
+  \end{column}
+  \end{columns}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \setbeamerfont{itemize/enumerate subbody}{size=\normalsize}
+  \begin{frame}[sqeeze]
+  \frametitle{Faulty Reasoning} 
+
+  %\mbox{}
+
+  \begin{itemize}
+  \item Consider the two-place relation \smath{\text{foo}}:\medskip
+  \begin{center}
+  \begin{tabular}{ccc}
+  \raisebox{2.5mm}{\colorbox{cream}{%
+  \smath{\;\infer{x\mapsto x}{}}}}\hspace{2mm}
+  &
+  \raisebox{2mm}{\colorbox{cream}{%
+  \smath{\infer{t_1\;t_2\mapsto t_1\;t_2}{}}}}\hspace{2mm}
+  &
+  \colorbox{cream}{%
+  \smath{\infer{\lambda x.t\mapsto t'}{t\mapsto t'}}}\\[5mm]
+  \end{tabular}
+  \end{center}
+
+  \pause
+
+  \item The lemma we going to prove:\smallskip
+  \begin{center}
+  Let \smath{t\mapsto t'}. If \smath{y\fresh t} then \smath{y\fresh t'}.
+  \end{center}\bigskip
+
+  \only<3>{
+  \item Cases 1 and 2 are trivial:\medskip
+  \begin{itemize}
+  \item If \smath{y\fresh x} then \smath{y\fresh x}.
+  \item If \smath{y\fresh t_1\,t_2} then \smath{y\fresh t_1\,t_2}.
+  \end{itemize}
+  }
+
+  \only<4->{
+  \item Case 3:
+  \begin{itemize}
+  \item We know \tikz[remember picture,baseline=(ta.base)] \node (ta) {\smath{y\fresh \lambda x.t}.}; 
+  We have to show \smath{y\fresh t'}.$\!\!\!\!$ 
+  \item The IH says: if \smath{y\fresh t} then \smath{y\fresh t'}.
+  \item<7,8> So we have \smath{y\fresh t}. Hence \smath{y\fresh t'} by IH. Done!
+  \end{itemize}
+  }
+  \end{itemize}
+  
+  \begin{textblock}{11.3}(0.7,0.6)
+  \only<5-7>{
+  \begin{tikzpicture}
+  \draw (0,0) node[fill=cream, text width=11.2cm, thick, draw=red, rounded corners=1mm] (nn)
+  {{\bf Variable Convention:}\\[2mm] 
+  \small
+   If $M_1,\ldots,M_n$ occur in a certain mathematical context
+   (e.g. definition, proof), then in these terms all bound variables 
+   are chosen to be different from the free variables.\smallskip
+
+  \normalsize
+   {\bf In our case:}\\[2mm]
+   The free variables are \smath{y} and \smath{t'}; the bound one is 
+   \smath{x}.\medskip
+          
+   By the variable convention we conclude that \smath{x\not= y}.
+  };
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \begin{textblock}{9.2}(3.6,9)
+  \only<6,7>{
+  \begin{tikzpicture}[remember picture]
+  \draw (0,0) node[fill=cream, text width=9cm, thick, draw=red, rounded corners=1mm] (tb)
+  {\small\smath{y\!\not\in\! \text{fv}(\lambda x.t) \Longleftrightarrow
+          y\!\not\in\! \text{fv}(t)\!-\!\{x\}
+          \stackrel{x\not=y}{\Longleftrightarrow}
+          y\!\not\in\! \text{fv}(t)}};
+
+  \path[overlay, ->, ultra thick, red] (tb) edge[out=-120, in=75] (ta);
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{Conclusions} 
+
+  \begin{itemize}
+  \item The user does not see anything of the ``raw'' level.
+  \item The Nominal Isabelle automatically derives the strong structural
+  induction principle for \underline{\bf all} nominal datatypes (not just the 
+  lambda-calculus)
+
+  \item They are easy to use: you just have to think carefully what the variable
+  convention should be.
+
+  \item We can explore the \colorbox{black}{\textcolor{white}{dark}} corners 
+  of the variable convention: when and where it can be used safely.
+  
+  \item<2> \alert{\bf Main Point:} Actually these proofs using the
+  variable convention are all trivial / obvious / routine\ldots {\bf provided} 
+  you use Nominal Isabelle. ;o)
+ 
+  \end{itemize}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[b]
+  \frametitle{
+  \begin{tabular}{c}
+  \mbox{}\\[13mm]
+  \alert{\LARGE Thank you very much!}\\
+  \alert{\Large Questions?}
+  \end{tabular}}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/document/beamerthemeplaincu.sty
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/document/beamerthemeplaincu.sty	Sun Oct 13 23:09:21 2013 +0200
@@ -0,0 +1,118 @@
+%%\Providespackage{beamerthemeplainculight}[2003/11/07 ver 0.93]
+\NeedsTeXFormat{LaTeX2e}[1995/12/01]
+
+% Copyright 2003 by Till Tantau <tantau@cs.tu-berlin.de>.
+%
+% This program can be redistributed and/or modified under the terms
+% of the LaTeX Project Public License Distributed from CTAN
+% archives in directory macros/latex/base/lppl.txt.
+ 
+\newcommand{\slidecaption}{}
+
+\mode<presentation>
+
+\usepackage{fontspec}
+\usefonttheme{serif}
+\defaultfontfeatures{Ligatures=TeX}
+\setromanfont{Hoefler Text}
+\setmonofont[Scale=MatchLowercase]{Consolas}
+\newfontfamily{\consolas}{Consolas}
+\newcommand{\tttext}[1]{{\consolas{#1}}}
+%%\setttfont{Lucida Console}
+%%\setmainfont[Mapping=tex-text]{Hoefler Text}
+
+%%\renewcommand\ttdefault{lmtt}
+
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% comic fonts fonts
+%\DeclareFontFamily{T1}{comic}{}%
+%\DeclareFontShape{T1}{comic}{m}{n}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{it}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{sc}{<->s*[.9]comic8t}{}%
+%\DeclareFontShape{T1}{comic}{b}{n}{<->s*[.9]comicbd8t}{}%
+%\DeclareFontShape{T1}{comic}{b}{it}{<->s*[.9]comicbd8t}{}%
+%\DeclareFontShape{T1}{comic}{m}{sl}{<->ssub * comic/m/it}{}%
+%\DeclareFontShape{T1}{comic}{b}{sc}{<->sub * comic/m/sc}{}%
+%\DeclareFontShape{T1}{comic}{b}{sl}{<->ssub * comic/b/it}{}%
+%\DeclareFontShape{T1}{comic}{bx}{n}{<->ssub * comic/b/n}{}%
+%\DeclareFontShape{T1}{comic}{bx}{it}{<->ssub * comic/b/it}{}%
+%\DeclareFontShape{T1}{comic}{bx}{sc}{<->sub * comic/m/sc}{}%
+%\DeclareFontShape{T1}{comic}{bx}{sl}{<->ssub * comic/b/it}{}%
+%
+%\renewcommand{\rmdefault}{comic}%
+%\renewcommand{\sfdefault}{comic}%
+\renewcommand{\mathfamilydefault}{cmr}% mathfont should be still the old one
+%
+\DeclareMathVersion{bold}% mathfont needs to be bold
+\DeclareSymbolFont{operators}{OT1}{cmr}{b}{n}%
+\SetSymbolFont{operators}{bold}{OT1}{cmr}{b}{n}%
+\DeclareSymbolFont{letters}{OML}{cmm}{b}{it}%
+\SetSymbolFont{letters}{bold}{OML}{cmm}{b}{it}%
+\DeclareSymbolFont{symbols}{OMS}{cmsy}{b}{n}%
+\SetSymbolFont{symbols}{bold}{OMS}{cmsy}{b}{n}%
+\DeclareSymbolFont{largesymbols}{OMX}{cmex}{b}{n}%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Frametitles
+
+\setbeamerfont{frametitle}{size={\LARGE}}
+\setbeamerfont{frametitle}{family={\fontspec{Hoefler Text Black}}}
+%\setbeamerfont{frametitle}{family={\usefont{T1}{ptm}{b}{n}}
+\setbeamercolor{frametitle}{fg=ProcessBlue,bg=white}
+
+\setbeamertemplate{frametitle}{%
+\vskip 2mm  % distance from the top margin
+\hskip -3mm % distance from left margin
+\vbox{%
+\begin{minipage}{1.05\textwidth}%
+\centering%
+\insertframetitle%
+\end{minipage}}%
+}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Foot
+%
+\setbeamertemplate{navigation symbols}{} 
+\usefoottemplate{%
+\vbox{%
+  \tinyline{%
+    \tiny\hfill\textcolor{gray!50}{\slidecaption{} --
+      p.~\insertframenumber/\inserttotalframenumber}}}%
+}
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\beamertemplateballitem
+\setlength\leftmargini{2mm}
+\setlength\leftmarginii{0.6cm}
+\setlength\leftmarginiii{1.5cm}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% blocks
+%\definecolor{cream}{rgb}{1,1,.65}
+\definecolor{cream}{rgb}{1,1,.8}
+\setbeamerfont{block title}{size=\normalsize}
+\setbeamercolor{block title}{fg=black,bg=cream}
+\setbeamercolor{block body}{fg=black,bg=cream}
+
+\setbeamertemplate{blocks}[rounded][shadow=true]
+
+\setbeamercolor{boxcolor}{fg=black,bg=cream}
+
+\mode
+<all>
+
+
+
+
+
+
diff -r c9a1c6f50ff5 -r cf451e182bf0 Slides/document/root.tex
--- a/Slides/document/root.tex	Fri Sep 06 10:06:41 2013 +0100
+++ b/Slides/document/root.tex	Sun Oct 13 23:09:21 2013 +0200
@@ -1,9 +1,9 @@
-\usepackage{beamerthemeplainculight}
-
-\usepackage[T1]{fontenc}
+\documentclass[dvipsnames,14pt,t]{beamer}
+\usepackage{beamerthemeplaincu}
+%%%\usepackage[T1]{fontenc}
 \usepackage{proof}
 \usepackage{german}
-\usepackage[latin1]{inputenc}
+%%%\usepackage[latin1]{inputenc}
 \usepackage{isabelle}
 \usepackage{isabellesym}
 \usepackage{mathpartir}
@@ -31,7 +31,7 @@
 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
 \newcommand{\dnn}{\stackrel{\mbox{\Large def}}{=}}
 \renewcommand{\emptyset}{\varnothing}% nice round empty set
-\renewcommand{\Gamma}{\varGamma} 
+%%\renewcommand{\Gamma}{\varGamma} 
 \DeclareRobustCommand{\flqq}{\mbox{\guillemotleft}}
 \DeclareRobustCommand{\frqq}{\mbox{\guillemotright}}
 \newcommand{\smath}[1]{\textcolor{blue}{\ensuremath{#1}}}
diff -r c9a1c6f50ff5 -r cf451e182bf0 slides1.pdf
Binary file slides1.pdf has changed
diff -r c9a1c6f50ff5 -r cf451e182bf0 slides2.pdf
Binary file slides2.pdf has changed
diff -r c9a1c6f50ff5 -r cf451e182bf0 slides3.pdf
Binary file slides3.pdf has changed
diff -r c9a1c6f50ff5 -r cf451e182bf0 slides4.pdf
Binary file slides4.pdf has changed
diff -r c9a1c6f50ff5 -r cf451e182bf0 slides5.pdf
Binary file slides5.pdf has changed
diff -r c9a1c6f50ff5 -r cf451e182bf0 slides9.pdf
Binary file slides9.pdf has changed
diff -r c9a1c6f50ff5 -r cf451e182bf0 slidesb.pdf
Binary file slidesb.pdf has changed