# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1283581569 -28800
# Node ID cda25f9aa67884b29e318fd4f48a0c656da9d7d2
# Parent  894599a50af3c42dfb27970d76a2473ef80d4ec5# Parent  1b31d514a087921de5bf6f6d6dcbdb79dcf7fa86
merged

diff -r 1b31d514a087 -r cda25f9aa678 IsaMakefile
--- a/IsaMakefile	Mon Aug 30 15:59:50 2010 +0900
+++ b/IsaMakefile	Sat Sep 04 14:26:09 2010 +0800
@@ -95,7 +95,18 @@
 	cd Slides/generated3 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
 	cp Slides/generated3/root.beamer.pdf Slides/slides3.pdf 
 
-slides: slides1
+session4: Slides/ROOT4.ML \
+         Slides/document/root* \
+         Slides/Slides4.thy
+	@$(USEDIR) -D generated4 -f ROOT4.ML HOL-Nominal Slides
+
+slides4: session4
+	rm -f Slides/generated4/*.aux # otherwise latex will fall over
+	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cd Slides/generated4 ; $(ISABELLE_TOOL) latex -o pdf root.beamer.tex
+	cp Slides/generated4/root.beamer.pdf Slides/slides4.pdf 
+
+slides: slides4
 
 
 
diff -r 1b31d514a087 -r cda25f9aa678 Nominal-General/Atoms.thy
--- a/Nominal-General/Atoms.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/Atoms.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -4,9 +4,41 @@
     Instantiations of concrete atoms 
 *)
 theory Atoms
-imports Nominal2_Atoms
+imports Nominal2_Base
 begin
 
+
+
+section {* @{const nat_of} is an example of a function 
+  without finite support *}
+
+
+lemma not_fresh_nat_of:
+  shows "\<not> a \<sharp> nat_of"
+unfolding fresh_def supp_def
+proof (clarsimp)
+  assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
+  hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
+    by simp
+  then obtain b where
+    b1: "b \<noteq> a" and
+    b2: "sort_of b = sort_of a" and
+    b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
+    by (rule obtain_atom) auto
+  have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
+  also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
+  also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
+  also have "\<dots> = nat_of b" using b2 by simp
+  finally have "nat_of a = nat_of b" by simp
+  with b2 have "a = b" by (simp add: atom_components_eq_iff)
+  with b1 show "False" by simp
+qed
+
+lemma supp_nat_of:
+  shows "supp nat_of = UNIV"
+  using not_fresh_nat_of [unfolded fresh_def] by auto
+
+
 section {* Manual instantiation of class @{text at}. *}
 
 typedef (open) name = "{a. sort_of a = Sort ''name'' []}"
diff -r 1b31d514a087 -r cda25f9aa678 Nominal-General/Nominal2_Atoms.thy
--- a/Nominal-General/Nominal2_Atoms.thy	Mon Aug 30 15:59:50 2010 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,188 +0,0 @@
-(*  Title:      Nominal2_Atoms
-    Authors:    Brian Huffman, Christian Urban
-
-    Definitions for concrete atom types. 
-*)
-theory Nominal2_Atoms
-imports Nominal2_Base
-        Nominal2_Eqvt
-uses ("nominal_atoms.ML")
-begin
-
-section {* Infrastructure for concrete atom types *}
-
-
-section {* A swapping operation for concrete atoms *}
-  
-definition
-  flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
-where
-  "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
-
-lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
-  unfolding flip_def by (rule swap_self)
-
-lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"
-  unfolding flip_def by (rule swap_commute)
-
-lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"
-  unfolding flip_def by (rule minus_swap)
-
-lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"
-  unfolding flip_def by (rule swap_cancel)
-
-lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"
-  unfolding permute_plus [symmetric] add_flip_cancel by simp
-
-lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
-  by (simp add: flip_commute)
-
-lemma flip_eqvt[eqvt]: 
-  fixes a b c::"'a::at_base"
-  shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
-  unfolding flip_def
-  by (simp add: swap_eqvt atom_eqvt)
-
-lemma flip_at_base_simps [simp]:
-  shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"
-  and   "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"
-  and   "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"
-  and   "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"
-  unfolding flip_def
-  unfolding atom_eq_iff [symmetric]
-  unfolding atom_eqvt [symmetric]
-  by simp_all
-
-text {* the following two lemmas do not hold for at_base, 
-  only for single sort atoms from at *}
-
-lemma permute_flip_at:
-  fixes a b c::"'a::at"
-  shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
-  unfolding flip_def
-  apply (rule atom_eq_iff [THEN iffD1])
-  apply (subst atom_eqvt [symmetric])
-  apply (simp add: swap_atom)
-  done
-
-lemma flip_at_simps [simp]:
-  fixes a b::"'a::at"
-  shows "(a \<leftrightarrow> b) \<bullet> a = b" 
-  and   "(a \<leftrightarrow> b) \<bullet> b = a"
-  unfolding permute_flip_at by simp_all
-
-lemma flip_fresh_fresh:
-  fixes a b::"'a::at_base"
-  assumes "atom a \<sharp> x" "atom b \<sharp> x"
-  shows "(a \<leftrightarrow> b) \<bullet> x = x"
-using assms
-by (simp add: flip_def swap_fresh_fresh)
-
-subsection {* Syntax for coercing at-elements to the atom-type *}
-
-syntax
-  "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
-
-translations
-  "_atom_constrain a t" => "CONST atom (_constrain a t)"
-
-
-subsection {* A lemma for proving instances of class @{text at}. *}
-
-setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}
-setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}
-
-text {*
-  New atom types are defined as subtypes of @{typ atom}.
-*}
-
-lemma exists_eq_simple_sort: 
-  shows "\<exists>a. a \<in> {a. sort_of a = s}"
-  by (rule_tac x="Atom s 0" in exI, simp)
-
-lemma exists_eq_sort: 
-  shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"
-  by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
-
-lemma at_base_class:
-  fixes sort_fun :: "'b \<Rightarrow>atom_sort"
-  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
-  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
-  assumes atom_def: "\<And>a. atom a = Rep a"
-  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
-  shows "OFCLASS('a, at_base_class)"
-proof
-  interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)
-  have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp
-  fix a b :: 'a and p p1 p2 :: perm
-  show "0 \<bullet> a = a"
-    unfolding permute_def by (simp add: Rep_inverse)
-  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
-    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
-  show "atom a = atom b \<longleftrightarrow> a = b"
-    unfolding atom_def by (simp add: Rep_inject)
-  show "p \<bullet> atom a = atom (p \<bullet> a)"
-    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
-qed
-
-(*
-lemma at_class:
-  fixes s :: atom_sort
-  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
-  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"
-  assumes atom_def: "\<And>a. atom a = Rep a"
-  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
-  shows "OFCLASS('a, at_class)"
-proof
-  interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)
-  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
-  fix a b :: 'a and p p1 p2 :: perm
-  show "0 \<bullet> a = a"
-    unfolding permute_def by (simp add: Rep_inverse)
-  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
-    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
-  show "sort_of (atom a) = sort_of (atom b)"
-    unfolding atom_def by (simp add: sort_of_Rep)
-  show "atom a = atom b \<longleftrightarrow> a = b"
-    unfolding atom_def by (simp add: Rep_inject)
-  show "p \<bullet> atom a = atom (p \<bullet> a)"
-    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
-qed
-*)
-
-lemma at_class:
-  fixes s :: atom_sort
-  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
-  assumes type: "type_definition Rep Abs {a. sort_of a = s}"
-  assumes atom_def: "\<And>a. atom a = Rep a"
-  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
-  shows "OFCLASS('a, at_class)"
-proof
-  interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
-  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
-  fix a b :: 'a and p p1 p2 :: perm
-  show "0 \<bullet> a = a"
-    unfolding permute_def by (simp add: Rep_inverse)
-  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
-    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
-  show "sort_of (atom a) = sort_of (atom b)"
-    unfolding atom_def by (simp add: sort_of_Rep)
-  show "atom a = atom b \<longleftrightarrow> a = b"
-    unfolding atom_def by (simp add: Rep_inject)
-  show "p \<bullet> atom a = atom (p \<bullet> a)"
-    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
-qed
-
-setup {* Sign.add_const_constraint
-  (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
-setup {* Sign.add_const_constraint
-  (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
-
-section {* Automation for creating concrete atom types *}
-
-text {* at the moment only single-sort concrete atoms are supported *}
-
-use "nominal_atoms.ML"
-
-
-end
diff -r 1b31d514a087 -r cda25f9aa678 Nominal-General/Nominal2_Base.thy
--- a/Nominal-General/Nominal2_Base.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/Nominal2_Base.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -7,6 +7,7 @@
 theory Nominal2_Base
 imports Main Infinite_Set
 uses ("nominal_library.ML")
+     ("nominal_atoms.ML")
 begin
 
 section {* Atoms and Sorts *}
@@ -430,6 +431,24 @@
   shows "p \<bullet> (\<not> A) = (\<not> (p \<bullet> A))"
 by (simp add: permute_bool_def)
 
+lemma conj_eqvt:
+  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+lemma imp_eqvt:
+  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
+  by (simp add: permute_bool_def)
+
+lemma ex_eqvt:
+  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
+  unfolding permute_fun_def permute_bool_def
+  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
+
+lemma all_eqvt:
+  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
+  unfolding permute_fun_def permute_bool_def
+  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
+
 lemma permute_boolE:
   fixes P::"bool"
   shows "p \<bullet> P \<Longrightarrow> P"
@@ -474,6 +493,21 @@
   unfolding permute_set_eq
   using a by (auto simp add: swap_atom)
 
+lemma mem_permute_iff:
+  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
+  unfolding mem_def permute_fun_def permute_bool_def
+  by simp
+
+lemma mem_eqvt:
+  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
+  unfolding mem_def
+  by (simp add: permute_fun_app_eq)
+
+lemma insert_eqvt:
+  shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
+  unfolding permute_set_eq_image image_insert ..
+
+
 subsection {* Permutations for units *}
 
 instantiation unit :: pt
@@ -851,6 +885,7 @@
 
 section {* Support for finite sets of atoms *}
 
+
 lemma supp_finite_atom_set:
   fixes S::"atom set"
   assumes "finite S"
@@ -862,12 +897,6 @@
   apply(simp add: swap_set_in)
 done
 
-lemma supp_atom_insert:
-  fixes S::"atom set"
-  assumes a: "finite S"
-  shows "supp (insert a S) = supp a \<union> supp S"
-  using a by (simp add: supp_finite_atom_set supp_atom)
-
 section {* Type @{typ perm} is finitely-supported. *}
 
 lemma perm_swap_eq:
@@ -987,6 +1016,16 @@
   shows "a \<sharp> (x, y) \<longleftrightarrow> a \<sharp> x \<and> a \<sharp> y"
   by (simp add: fresh_def supp_Pair)
 
+lemma supp_Unit:
+  shows "supp () = {}"
+  by (simp add: supp_def)
+
+lemma fresh_Unit:
+  shows "a \<sharp> ()"
+  by (simp add: fresh_def supp_Unit)
+
+
+
 instance prod :: (fs, fs) fs
 apply default
 apply (induct_tac x)
@@ -1065,7 +1104,8 @@
 apply (simp_all add: supp_Nil supp_Cons finite_supp)
 done
 
-section {* Support and freshness for applications *}
+
+section {* Support and Freshness for Applications *}
 
 lemma fresh_conv_MOST: 
   shows "a \<sharp> x \<longleftrightarrow> (MOST b. (a \<rightleftharpoons> b) \<bullet> x = x)"
@@ -1093,7 +1133,7 @@
   unfolding fresh_def
   by auto
 
-text {* support of equivariant functions *}
+text {* Support of Equivariant Functions *}
 
 lemma supp_fun_eqvt:
   assumes a: "\<And>p. p \<bullet> f = f"
@@ -1112,7 +1152,346 @@
 qed
 
 
-section {* Concrete atoms types *}
+section {* Support of Finite Sets of Finitely Supported Elements *}
+
+lemma Union_fresh:
+  shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
+  unfolding Union_image_eq[symmetric]
+  apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
+  apply(simp add: permute_fun_def UNION_def Collect_def Bex_def ex_eqvt mem_def conj_eqvt)
+  apply(subst permute_fun_app_eq)
+  back
+  apply(simp add: supp_eqvt)
+  apply(assumption)
+  done
+
+lemma Union_supports_set:
+  shows "(\<Union>x \<in> S. supp x) supports S"
+proof -
+  { fix a b
+    have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
+      unfolding permute_set_eq by force
+  }
+  then show "(\<Union>x \<in> S. supp x) supports S"
+    unfolding supports_def 
+    by (simp add: fresh_def[symmetric] swap_fresh_fresh)
+qed
+
+lemma Union_of_fin_supp_sets:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"   
+  shows "finite (\<Union>x\<in>S. supp x)"
+  using fin by (induct) (auto simp add: finite_supp)
+
+lemma Union_included_in_supp:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"
+  shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
+proof -
+  have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
+    by (rule supp_finite_atom_set[symmetric])
+       (rule Union_of_fin_supp_sets[OF fin])
+  also have "\<dots> \<subseteq> supp S"
+    by (rule supp_subset_fresh)
+       (simp add: Union_fresh)
+  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
+qed
+
+lemma supp_of_fin_sets:
+  fixes S::"('a::fs set)"
+  assumes fin: "finite S"
+  shows "(supp S) = (\<Union>x\<in>S. supp x)"
+apply(rule subset_antisym)
+apply(rule supp_is_subset)
+apply(rule Union_supports_set)
+apply(rule Union_of_fin_supp_sets[OF fin])
+apply(rule Union_included_in_supp[OF fin])
+done
+
+lemma supp_of_fin_union:
+  fixes S T::"('a::fs) set"
+  assumes fin1: "finite S"
+  and     fin2: "finite T"
+  shows "supp (S \<union> T) = supp S \<union> supp T"
+  using fin1 fin2
+  by (simp add: supp_of_fin_sets)
+
+lemma supp_of_fin_insert:
+  fixes S::"('a::fs) set"
+  assumes fin:  "finite S"
+  shows "supp (insert x S) = supp x \<union> supp S"
+  using fin
+  by (simp add: supp_of_fin_sets)
+
+
+section {* Fresh-Star *}
+
+
+text {* The fresh-star generalisation of fresh is used in strong
+  induction principles. *}
+
+definition 
+  fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
+where 
+  "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
+
+lemma fresh_star_prod:
+  fixes as::"atom set"
+  shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
+  by (auto simp add: fresh_star_def fresh_Pair)
+
+lemma fresh_star_union:
+  shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
+  by (auto simp add: fresh_star_def)
+
+lemma fresh_star_insert:
+  shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
+  by (auto simp add: fresh_star_def)
+
+lemma fresh_star_Un_elim:
+  "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
+  unfolding fresh_star_def
+  apply(rule)
+  apply(erule meta_mp)
+  apply(auto)
+  done
+
+lemma fresh_star_insert_elim:
+  "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"
+  unfolding fresh_star_def
+  by rule (simp_all add: fresh_star_def)
+
+lemma fresh_star_empty_elim:
+  "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp add: fresh_star_def)
+
+lemma fresh_star_unit_elim: 
+  shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
+  by (simp add: fresh_star_def fresh_Unit) 
+
+lemma fresh_star_prod_elim: 
+  shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
+  by (rule, simp_all add: fresh_star_prod)
+
+lemma fresh_star_zero:
+  shows "as \<sharp>* (0::perm)"
+  unfolding fresh_star_def
+  by (simp add: fresh_zero_perm)
+
+lemma fresh_star_plus:
+  fixes p q::perm
+  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
+  unfolding fresh_star_def
+  by (simp add: fresh_plus_perm)
+
+lemma fresh_star_permute_iff:
+  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
+  unfolding fresh_star_def
+  by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
+
+lemma fresh_star_eqvt:
+  shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
+unfolding fresh_star_def
+unfolding Ball_def
+apply(simp add: all_eqvt)
+apply(subst permute_fun_def)
+apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
+done
+
+
+section {* Induction principle for permutations *}
+
+
+lemma perm_struct_induct[consumes 1, case_names zero swap]:
+  assumes S: "supp p \<subseteq> S"
+  and zero: "P 0"
+  and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+  shows "P p"
+proof -
+  have "finite (supp p)" by (simp add: finite_supp)
+  then show "P p" using S
+  proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
+    case (psubset p)
+    then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
+    have as: "supp p \<subseteq> S" by fact
+    { assume "supp p = {}"
+      then have "p = 0" by (simp add: supp_perm expand_perm_eq)
+      then have "P p" using zero by simp
+    }
+    moreover
+    { assume "supp p \<noteq> {}"
+      then obtain a where a0: "a \<in> supp p" by blast
+      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"
+        using as by (auto simp add: supp_atom supp_perm swap_atom)
+      let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
+      have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
+      moreover
+      have "a \<notin> supp ?q" by (simp add: supp_perm)
+      then have "supp ?q \<noteq> supp p" using a0 by auto
+      ultimately have "supp ?q \<subset> supp p" using a2 by auto
+      then have "P ?q" using ih by simp
+      moreover
+      have "supp ?q \<subseteq> S" using as a2 by simp
+      ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 
+      moreover 
+      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
+      ultimately have "P p" by simp
+    }
+    ultimately show "P p" by blast
+  qed
+qed
+
+lemma perm_simple_struct_induct[case_names zero swap]:
+  assumes zero: "P 0"
+  and     swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
+  shows "P p"
+by (rule_tac S="supp p" in perm_struct_induct)
+   (auto intro: zero swap)
+
+lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
+  assumes S: "supp p \<subseteq> S"
+  assumes zero: "P 0"
+  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
+  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
+  shows "P p"
+using S
+by (induct p rule: perm_struct_induct)
+   (auto intro: zero plus swap simp add: supp_swap)
+
+lemma supp_perm_eq:
+  assumes "(supp x) \<sharp>* p"
+  shows "p \<bullet> x = x"
+proof -
+  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
+    unfolding supp_perm fresh_star_def fresh_def by auto
+  then show "p \<bullet> x = x"
+  proof (induct p rule: perm_struct_induct)
+    case zero
+    show "0 \<bullet> x = x" by simp
+  next
+    case (swap p a b)
+    then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all
+    then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+  qed
+qed
+
+lemma supp_perm_eq_test:
+  assumes "(supp x) \<sharp>* p"
+  shows "p \<bullet> x = x"
+proof -
+  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
+    unfolding supp_perm fresh_star_def fresh_def by auto
+  then show "p \<bullet> x = x"
+  proof (induct p rule: perm_subset_induct)
+    case zero
+    show "0 \<bullet> x = x" by simp
+  next
+    case (swap a b)
+    then have "a \<sharp> x" "b \<sharp> x" by simp_all
+    then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
+  next
+    case (plus p1 p2)
+    have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
+    then show "(p1 + p2) \<bullet> x = x" by simp
+  qed
+qed
+
+
+section {* Avoiding of atom sets *}
+
+text {* 
+  For every set of atoms, there is another set of atoms
+  avoiding a finitely supported c and there is a permutation
+  which 'translates' between both sets.
+*}
+
+lemma at_set_avoiding_aux:
+  fixes Xs::"atom set"
+  and   As::"atom set"
+  assumes b: "Xs \<subseteq> As"
+  and     c: "finite As"
+  shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+proof -
+  from b c have "finite Xs" by (rule finite_subset)
+  then show ?thesis using b
+  proof (induct rule: finite_subset_induct)
+    case empty
+    have "0 \<bullet> {} \<inter> As = {}" by simp
+    moreover
+    have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
+    ultimately show ?case by blast
+  next
+    case (insert x Xs)
+    then obtain p where
+      p1: "(p \<bullet> Xs) \<inter> As = {}" and 
+      p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
+    from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
+    with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
+    hence px: "p \<bullet> x = x" unfolding supp_perm by simp
+    have "finite (As \<union> p \<bullet> Xs)"
+      using `finite As` `finite Xs`
+      by (simp add: permute_set_eq_image)
+    then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
+      by (rule obtain_atom)
+    hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
+      by simp_all
+    let ?q = "(x \<rightleftharpoons> y) + p"
+    have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
+      unfolding insert_eqvt
+      using `p \<bullet> x = x` `sort_of y = sort_of x`
+      using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
+      by (simp add: swap_atom swap_set_not_in)
+    have "?q \<bullet> insert x Xs \<inter> As = {}"
+      using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
+      unfolding q by simp
+    moreover
+    have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
+      using p2 unfolding q
+      by (intro subset_trans [OF supp_plus_perm])
+         (auto simp add: supp_swap)
+    ultimately show ?case by blast
+  qed
+qed
+
+lemma at_set_avoiding:
+  assumes a: "finite Xs"
+  and     b: "finite (supp c)"
+  obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
+  using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
+  unfolding fresh_star_def fresh_def by blast
+
+lemma at_set_avoiding2:
+  assumes "finite xs"
+  and     "finite (supp c)" "finite (supp x)"
+  and     "xs \<sharp>* x"
+  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
+using assms
+apply(erule_tac c="(c, x)" in at_set_avoiding)
+apply(simp add: supp_Pair)
+apply(rule_tac x="p" in exI)
+apply(simp add: fresh_star_prod)
+apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
+apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
+apply(auto simp add: fresh_star_def fresh_def)
+done
+
+lemma at_set_avoiding2_atom:
+  assumes "finite (supp c)" "finite (supp x)"
+  and     b: "a \<sharp> x"
+  shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
+proof -
+  have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
+  obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"
+    using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
+  have c: "(p \<bullet> a) \<sharp> c" using p1
+    unfolding fresh_star_def Ball_def 
+    by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
+  hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
+  then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
+qed
+
+
+section {* Concrete Atoms Types *}
 
 text {*
   Class @{text at_base} allows types containing multiple sorts of atoms.
@@ -1179,44 +1558,363 @@
   thus ?thesis ..
 qed
 
-lemma image_eqvt:
-  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
-  unfolding permute_set_eq_image
-  unfolding permute_fun_def [where f=f]
-  by (simp add: image_image)
-
-lemma atom_image_cong:
-  shows "(atom ` X = atom ` Y) = (X = Y)"
-  apply(rule inj_image_eq_iff)
-  apply(simp add: inj_on_def)
-  done
-
-lemma atom_image_supp:
-  shows "supp S = supp (atom ` S)"
-  apply(simp add: supp_def)
-  apply(simp add: image_eqvt)
-  apply(subst (2) permute_fun_def)
-  apply(simp add: atom_eqvt)
-  apply(simp add: atom_image_cong)
-  done
-
 lemma supp_finite_set_at_base:
   assumes a: "finite S"
   shows "supp S = atom ` S"
-proof -
-  have fin: "finite (atom ` S)" using a by simp
-  have "supp S = supp (atom ` S)" by (rule atom_image_supp)
-  also have "\<dots> = atom ` S" using fin by (simp add: supp_finite_atom_set)
-  finally show "supp S = atom ` S" by simp
+apply(simp add: supp_of_fin_sets[OF a])
+apply(simp add: supp_at_base)
+apply(auto)
+done
+
+section {* Infrastructure for concrete atom types *}
+
+section {* A swapping operation for concrete atoms *}
+  
+definition
+  flip :: "'a::at_base \<Rightarrow> 'a \<Rightarrow> perm" ("'(_ \<leftrightarrow> _')")
+where
+  "(a \<leftrightarrow> b) = (atom a \<rightleftharpoons> atom b)"
+
+lemma flip_self [simp]: "(a \<leftrightarrow> a) = 0"
+  unfolding flip_def by (rule swap_self)
+
+lemma flip_commute: "(a \<leftrightarrow> b) = (b \<leftrightarrow> a)"
+  unfolding flip_def by (rule swap_commute)
+
+lemma minus_flip [simp]: "- (a \<leftrightarrow> b) = (a \<leftrightarrow> b)"
+  unfolding flip_def by (rule minus_swap)
+
+lemma add_flip_cancel: "(a \<leftrightarrow> b) + (a \<leftrightarrow> b) = 0"
+  unfolding flip_def by (rule swap_cancel)
+
+lemma permute_flip_cancel [simp]: "(a \<leftrightarrow> b) \<bullet> (a \<leftrightarrow> b) \<bullet> x = x"
+  unfolding permute_plus [symmetric] add_flip_cancel by simp
+
+lemma permute_flip_cancel2 [simp]: "(a \<leftrightarrow> b) \<bullet> (b \<leftrightarrow> a) \<bullet> x = x"
+  by (simp add: flip_commute)
+
+lemma flip_eqvt: 
+  fixes a b c::"'a::at_base"
+  shows "p \<bullet> (a \<leftrightarrow> b) = (p \<bullet> a \<leftrightarrow> p \<bullet> b)"
+  unfolding flip_def
+  by (simp add: swap_eqvt atom_eqvt)
+
+lemma flip_at_base_simps [simp]:
+  shows "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> a = b"
+  and   "sort_of (atom a) = sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> b = a"
+  and   "\<lbrakk>a \<noteq> c; b \<noteq> c\<rbrakk> \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> c = c"
+  and   "sort_of (atom a) \<noteq> sort_of (atom b) \<Longrightarrow> (a \<leftrightarrow> b) \<bullet> x = x"
+  unfolding flip_def
+  unfolding atom_eq_iff [symmetric]
+  unfolding atom_eqvt [symmetric]
+  by simp_all
+
+text {* the following two lemmas do not hold for at_base, 
+  only for single sort atoms from at *}
+
+lemma permute_flip_at:
+  fixes a b c::"'a::at"
+  shows "(a \<leftrightarrow> b) \<bullet> c = (if c = a then b else if c = b then a else c)"
+  unfolding flip_def
+  apply (rule atom_eq_iff [THEN iffD1])
+  apply (subst atom_eqvt [symmetric])
+  apply (simp add: swap_atom)
+  done
+
+lemma flip_at_simps [simp]:
+  fixes a b::"'a::at"
+  shows "(a \<leftrightarrow> b) \<bullet> a = b" 
+  and   "(a \<leftrightarrow> b) \<bullet> b = a"
+  unfolding permute_flip_at by simp_all
+
+lemma flip_fresh_fresh:
+  fixes a b::"'a::at_base"
+  assumes "atom a \<sharp> x" "atom b \<sharp> x"
+  shows "(a \<leftrightarrow> b) \<bullet> x = x"
+using assms
+by (simp add: flip_def swap_fresh_fresh)
+
+subsection {* Syntax for coercing at-elements to the atom-type *}
+
+syntax
+  "_atom_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic" ("_:::_" [4, 0] 3)
+
+translations
+  "_atom_constrain a t" => "CONST atom (_constrain a t)"
+
+
+subsection {* A lemma for proving instances of class @{text at}. *}
+
+setup {* Sign.add_const_constraint (@{const_name "permute"}, NONE) *}
+setup {* Sign.add_const_constraint (@{const_name "atom"}, NONE) *}
+
+text {*
+  New atom types are defined as subtypes of @{typ atom}.
+*}
+
+lemma exists_eq_simple_sort: 
+  shows "\<exists>a. a \<in> {a. sort_of a = s}"
+  by (rule_tac x="Atom s 0" in exI, simp)
+
+lemma exists_eq_sort: 
+  shows "\<exists>a. a \<in> {a. sort_of a \<in> range sort_fun}"
+  by (rule_tac x="Atom (sort_fun x) y" in exI, simp)
+
+lemma at_base_class:
+  fixes sort_fun :: "'b \<Rightarrow>atom_sort"
+  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range sort_fun}"
+  assumes atom_def: "\<And>a. atom a = Rep a"
+  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+  shows "OFCLASS('a, at_base_class)"
+proof
+  interpret type_definition Rep Abs "{a. sort_of a \<in> range sort_fun}" by (rule type)
+  have sort_of_Rep: "\<And>a. sort_of (Rep a) \<in> range sort_fun" using Rep by simp
+  fix a b :: 'a and p p1 p2 :: perm
+  show "0 \<bullet> a = a"
+    unfolding permute_def by (simp add: Rep_inverse)
+  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+  show "atom a = atom b \<longleftrightarrow> a = b"
+    unfolding atom_def by (simp add: Rep_inject)
+  show "p \<bullet> atom a = atom (p \<bullet> a)"
+    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+qed
+
+(*
+lemma at_class:
+  fixes s :: atom_sort
+  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+  assumes type: "type_definition Rep Abs {a. sort_of a \<in> range (\<lambda>x::unit. s)}"
+  assumes atom_def: "\<And>a. atom a = Rep a"
+  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+  shows "OFCLASS('a, at_class)"
+proof
+  interpret type_definition Rep Abs "{a. sort_of a \<in> range (\<lambda>x::unit. s)}" by (rule type)
+  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
+  fix a b :: 'a and p p1 p2 :: perm
+  show "0 \<bullet> a = a"
+    unfolding permute_def by (simp add: Rep_inverse)
+  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+  show "sort_of (atom a) = sort_of (atom b)"
+    unfolding atom_def by (simp add: sort_of_Rep)
+  show "atom a = atom b \<longleftrightarrow> a = b"
+    unfolding atom_def by (simp add: Rep_inject)
+  show "p \<bullet> atom a = atom (p \<bullet> a)"
+    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
+qed
+*)
+
+lemma at_class:
+  fixes s :: atom_sort
+  fixes Rep :: "'a \<Rightarrow> atom" and Abs :: "atom \<Rightarrow> 'a"
+  assumes type: "type_definition Rep Abs {a. sort_of a = s}"
+  assumes atom_def: "\<And>a. atom a = Rep a"
+  assumes permute_def: "\<And>p a. p \<bullet> a = Abs (p \<bullet> Rep a)"
+  shows "OFCLASS('a, at_class)"
+proof
+  interpret type_definition Rep Abs "{a. sort_of a = s}" by (rule type)
+  have sort_of_Rep: "\<And>a. sort_of (Rep a) = s" using Rep by (simp add: image_def)
+  fix a b :: 'a and p p1 p2 :: perm
+  show "0 \<bullet> a = a"
+    unfolding permute_def by (simp add: Rep_inverse)
+  show "(p1 + p2) \<bullet> a = p1 \<bullet> p2 \<bullet> a"
+    unfolding permute_def by (simp add: Abs_inverse sort_of_Rep)
+  show "sort_of (atom a) = sort_of (atom b)"
+    unfolding atom_def by (simp add: sort_of_Rep)
+  show "atom a = atom b \<longleftrightarrow> a = b"
+    unfolding atom_def by (simp add: Rep_inject)
+  show "p \<bullet> atom a = atom (p \<bullet> a)"
+    unfolding permute_def atom_def by (simp add: Abs_inverse sort_of_Rep)
 qed
 
-lemma supp_at_base_insert:
-  fixes a::"'a::at_base"
-  assumes a: "finite S"
-  shows "supp (insert a S) = supp a \<union> supp S"
-  using a by (simp add: supp_finite_set_at_base supp_at_base)
+setup {* Sign.add_const_constraint
+  (@{const_name "permute"}, SOME @{typ "perm \<Rightarrow> 'a::pt \<Rightarrow> 'a"}) *}
+setup {* Sign.add_const_constraint
+  (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
+
+
+
+section {* The freshness lemma according to Andy Pitts *}
+
+lemma freshness_lemma:
+  fixes h :: "'a::at \<Rightarrow> 'b::pt"
+  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+  shows  "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+proof -
+  from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"
+    by (auto simp add: fresh_Pair)
+  show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+  proof (intro exI allI impI)
+    fix a :: 'a
+    assume a3: "atom a \<sharp> h"
+    show "h a = h b"
+    proof (cases "a = b")
+      assume "a = b"
+      thus "h a = h b" by simp
+    next
+      assume "a \<noteq> b"
+      hence "atom a \<sharp> b" by (simp add: fresh_at_base)
+      with a3 have "atom a \<sharp> h b" 
+        by (rule fresh_fun_app)
+      with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
+        by (rule swap_fresh_fresh)
+      from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
+        by (rule swap_fresh_fresh)
+      from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp
+      also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"
+        by (rule permute_fun_app_eq)
+      also have "\<dots> = h a"
+        using d2 by simp
+      finally show "h a = h b"  by simp
+    qed
+  qed
+qed
+
+lemma freshness_lemma_unique:
+  fixes h :: "'a::at \<Rightarrow> 'b::pt"
+  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+  shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+proof (rule ex_ex1I)
+  from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+    by (rule freshness_lemma)
+next
+  fix x y
+  assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
+  assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
+  from a x y show "x = y"
+    by (auto simp add: fresh_Pair)
+qed
+
+text {* packaging the freshness lemma into a function *}
+
+definition
+  fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
+where
+  "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
+
+lemma fresh_fun_apply:
+  fixes h :: "'a::at \<Rightarrow> 'b::pt"
+  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+  assumes b: "atom a \<sharp> h"
+  shows "fresh_fun h = h a"
+unfolding fresh_fun_def
+proof (rule the_equality)
+  show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
+  proof (intro strip)
+    fix a':: 'a
+    assume c: "atom a' \<sharp> h"
+    from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)
+    with b c show "h a' = h a" by auto
+  qed
+next
+  fix fr :: 'b
+  assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"
+  with b show "fr = h a" by auto
+qed
 
-section {* library functions for the nominal infrastructure *}
+lemma fresh_fun_apply':
+  fixes h :: "'a::at \<Rightarrow> 'b::pt"
+  assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
+  shows "fresh_fun h = h a"
+  apply (rule fresh_fun_apply)
+  apply (auto simp add: fresh_Pair intro: a)
+  done
+
+lemma fresh_fun_eqvt:
+  fixes h :: "'a::at \<Rightarrow> 'b::pt"
+  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+  shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
+  using a
+  apply (clarsimp simp add: fresh_Pair)
+  apply (subst fresh_fun_apply', assumption+)
+  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
+  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
+  apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
+  apply (erule (1) fresh_fun_apply' [symmetric])
+  done
+
+lemma fresh_fun_supports:
+  fixes h :: "'a::at \<Rightarrow> 'b::pt"
+  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
+  shows "(supp h) supports (fresh_fun h)"
+  apply (simp add: supports_def fresh_def [symmetric])
+  apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
+  done
+
+notation fresh_fun (binder "FRESH " 10)
+
+lemma FRESH_f_iff:
+  fixes P :: "'a::at \<Rightarrow> 'b::pure"
+  fixes f :: "'b \<Rightarrow> 'c::pure"
+  assumes P: "finite (supp P)"
+  shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
+proof -
+  obtain a::'a where "atom a \<notin> supp P"
+    using P by (rule obtain_at_base)
+  hence "atom a \<sharp> P"
+    by (simp add: fresh_def)
+  show "(FRESH x. f (P x)) = f (FRESH x. P x)"
+    apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
+    apply (cut_tac `atom a \<sharp> P`)
+    apply (simp add: fresh_conv_MOST)
+    apply (elim MOST_rev_mp, rule MOST_I, clarify)
+    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+    apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+    apply (rule refl)
+    done
+qed
+
+lemma FRESH_binop_iff:
+  fixes P :: "'a::at \<Rightarrow> 'b::pure"
+  fixes Q :: "'a::at \<Rightarrow> 'c::pure"
+  fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"
+  assumes P: "finite (supp P)" 
+  and     Q: "finite (supp Q)"
+  shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
+proof -
+  from assms have "finite (supp P \<union> supp Q)" by simp
+  then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
+    by (rule obtain_at_base)
+  hence "atom a \<sharp> P" and "atom a \<sharp> Q"
+    by (simp_all add: fresh_def)
+  show ?thesis
+    apply (subst fresh_fun_apply' [where a=a, OF _ pure_fresh])
+    apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
+    apply (simp add: fresh_conv_MOST)
+    apply (elim MOST_rev_mp, rule MOST_I, clarify)
+    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
+    apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> P` pure_fresh])
+    apply (subst fresh_fun_apply' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
+    apply (rule refl)
+    done
+qed
+
+lemma FRESH_conj_iff:
+  fixes P Q :: "'a::at \<Rightarrow> bool"
+  assumes P: "finite (supp P)" and Q: "finite (supp Q)"
+  shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"
+using P Q by (rule FRESH_binop_iff)
+
+lemma FRESH_disj_iff:
+  fixes P Q :: "'a::at \<Rightarrow> bool"
+  assumes P: "finite (supp P)" and Q: "finite (supp Q)"
+  shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
+using P Q by (rule FRESH_binop_iff)
+
+
+section {* Library functions for the nominal infrastructure *}
+
 use "nominal_library.ML"
 
+
+section {* Automation for creating concrete atom types *}
+
+text {* at the moment only single-sort concrete atoms are supported *}
+
+use "nominal_atoms.ML"
+
+
+
 end
diff -r 1b31d514a087 -r cda25f9aa678 Nominal-General/Nominal2_Eqvt.thy
--- a/Nominal-General/Nominal2_Eqvt.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/Nominal2_Eqvt.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -20,6 +20,24 @@
 use "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
+
+section {* eqvt lemmas *}
+
+lemmas [eqvt] =
+  conj_eqvt Not_eqvt ex_eqvt all_eqvt imp_eqvt
+  imp_eqvt[folded induct_implies_def]
+  uminus_eqvt
+
+  (* nominal *)
+  supp_eqvt fresh_eqvt fresh_star_eqvt add_perm_eqvt atom_eqvt 
+  swap_eqvt flip_eqvt
+
+  (* datatypes *)
+  Pair_eqvt permute_list.simps
+
+  (* sets *)
+  mem_eqvt insert_eqvt
+
 text {* helper lemmas for the perm_simp *}
 
 definition
@@ -79,36 +97,14 @@
   shows "p \<bullet> False = False"
   unfolding permute_bool_def ..
 
-lemma imp_eqvt[eqvt]:
-  shows "p \<bullet> (A \<longrightarrow> B) = ((p \<bullet> A) \<longrightarrow> (p \<bullet> B))"
-  by (simp add: permute_bool_def)
-
-lemma conj_eqvt[eqvt]:
-  shows "p \<bullet> (A \<and> B) = ((p \<bullet> A) \<and> (p \<bullet> B))"
-  by (simp add: permute_bool_def)
-
 lemma disj_eqvt[eqvt]:
   shows "p \<bullet> (A \<or> B) = ((p \<bullet> A) \<or> (p \<bullet> B))"
   by (simp add: permute_bool_def)
 
-lemma Not_eqvt[eqvt]:
-  shows "p \<bullet> (\<not> A) \<longleftrightarrow> \<not> (p \<bullet> A)"
-  by (simp add: permute_bool_def)
-
-lemma all_eqvt[eqvt]:
-  shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, drule_tac x="p \<bullet> x" in spec, simp)
-
 lemma all_eqvt2:
   shows "p \<bullet> (\<forall>x. P x) = (\<forall>x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)
 
-lemma ex_eqvt[eqvt]:
-  shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. (p \<bullet> P) x)"
-  unfolding permute_fun_def permute_bool_def
-  by (auto, rule_tac x="p \<bullet> x" in exI, simp)
-
 lemma ex_eqvt2:
   shows "p \<bullet> (\<exists>x. P x) = (\<exists>x. p \<bullet> P (- p \<bullet> x))"
   by (perm_simp add: permute_minus_cancel) (rule refl)
@@ -134,16 +130,6 @@
 
 section {* Set Operations *}
 
-lemma mem_permute_iff:
-  shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X"
-  unfolding mem_def permute_fun_def permute_bool_def
-  by simp
-
-lemma mem_eqvt[eqvt]:
-  shows "p \<bullet> (x \<in> A) \<longleftrightarrow> (p \<bullet> x) \<in> (p \<bullet> A)"
-  unfolding mem_def
-  by (perm_simp) (rule refl)
-
 lemma not_mem_eqvt:
   shows "p \<bullet> (x \<notin> A) \<longleftrightarrow> (p \<bullet> x) \<notin> (p \<bullet> A)"
   by (perm_simp) (rule refl)
@@ -207,9 +193,11 @@
   unfolding Compl_eq_Diff_UNIV
   by (perm_simp) (rule refl)
 
-lemma insert_eqvt[eqvt]:
-  shows "p \<bullet> (insert x A) = insert (p \<bullet> x) (p \<bullet> A)"
-  unfolding permute_set_eq_image image_insert ..
+lemma image_eqvt:
+  shows "p \<bullet> (f ` A) = (p \<bullet> f) ` (p \<bullet> A)"
+  unfolding permute_set_eq_image
+  unfolding permute_fun_def [where f=f]
+  by (simp add: image_image)
 
 lemma vimage_eqvt[eqvt]:
   shows "p \<bullet> (f -` A) = (p \<bullet> f) -` (p \<bullet> A)"
@@ -230,6 +218,15 @@
   shows "p \<bullet> finite A = finite (p \<bullet> A)"
   unfolding finite_permute_iff permute_bool_def ..
 
+lemma supp_set:
+  fixes xs :: "('a::fs) list"
+  shows "supp (set xs) = supp xs"
+apply(induct xs)
+apply(simp add: supp_set_empty supp_Nil)
+apply(simp add: supp_Cons supp_of_fin_insert)
+done
+
+
 section {* List Operations *}
 
 lemma append_eqvt[eqvt]:
@@ -285,30 +282,6 @@
   unfolding split_def
   by (perm_simp) (rule refl)
 
-section {* Units *}
-
-lemma supp_unit:
-  shows "supp () = {}"
-  by (simp add: supp_def)
-
-lemma fresh_unit:
-  shows "a \<sharp> ()"
-  by (simp add: fresh_def supp_unit)
-
-section {* additional eqvt lemmas *}
-
-lemmas [eqvt] = 
-  imp_eqvt [folded induct_implies_def]
-
-  (* nominal *)
-  supp_eqvt fresh_eqvt add_perm_eqvt atom_eqvt swap_eqvt uminus_eqvt
-
-  (* datatypes *)
-  Pair_eqvt permute_list.simps
-
-  (* sets *)
-  image_eqvt
-
 
 section {* Test cases *}
 
diff -r 1b31d514a087 -r cda25f9aa678 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Mon Aug 30 15:59:50 2010 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,547 +0,0 @@
-(*  Title:      Nominal2_Supp
-    Authors:    Brian Huffman, Christian Urban
-
-    Supplementary Lemmas and Definitions for 
-    Nominal Isabelle. 
-*)
-theory Nominal2_Supp
-imports Nominal2_Base Nominal2_Eqvt Nominal2_Atoms
-begin
-
-
-section {* Fresh-Star *}
-
-
-text {* The fresh-star generalisation of fresh is used in strong
-  induction principles. *}
-
-definition 
-  fresh_star :: "atom set \<Rightarrow> 'a::pt \<Rightarrow> bool" ("_ \<sharp>* _" [80,80] 80)
-where 
-  "as \<sharp>* x \<equiv> \<forall>a \<in> as. a \<sharp> x"
-
-lemma fresh_star_prod:
-  fixes as::"atom set"
-  shows "as \<sharp>* (x, y) = (as \<sharp>* x \<and> as \<sharp>* y)" 
-  by (auto simp add: fresh_star_def fresh_Pair)
-
-lemma fresh_star_union:
-  shows "(as \<union> bs) \<sharp>* x = (as \<sharp>* x \<and> bs \<sharp>* x)"
-  by (auto simp add: fresh_star_def)
-
-lemma fresh_star_insert:
-  shows "(insert a as) \<sharp>* x = (a \<sharp> x \<and> as \<sharp>* x)"
-  by (auto simp add: fresh_star_def)
-
-lemma fresh_star_Un_elim:
-  "((as \<union> bs) \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (as \<sharp>* x \<Longrightarrow> bs \<sharp>* x \<Longrightarrow> PROP C)"
-  unfolding fresh_star_def
-  apply(rule)
-  apply(erule meta_mp)
-  apply(auto)
-  done
-
-lemma fresh_star_insert_elim:
-  "(insert a as \<sharp>* x \<Longrightarrow> PROP C) \<equiv> (a \<sharp> x \<Longrightarrow> as \<sharp>* x \<Longrightarrow> PROP C)"
-  unfolding fresh_star_def
-  by rule (simp_all add: fresh_star_def)
-
-lemma fresh_star_empty_elim:
-  "({} \<sharp>* x \<Longrightarrow> PROP C) \<equiv> PROP C"
-  by (simp add: fresh_star_def)
-
-lemma fresh_star_unit_elim: 
-  shows "(a \<sharp>* () \<Longrightarrow> PROP C) \<equiv> PROP C"
-  by (simp add: fresh_star_def fresh_unit) 
-
-lemma fresh_star_prod_elim: 
-  shows "(a \<sharp>* (x, y) \<Longrightarrow> PROP C) \<equiv> (a \<sharp>* x \<Longrightarrow> a \<sharp>* y \<Longrightarrow> PROP C)"
-  by (rule, simp_all add: fresh_star_prod)
-
-lemma fresh_star_zero:
-  shows "as \<sharp>* (0::perm)"
-  unfolding fresh_star_def
-  by (simp add: fresh_zero_perm)
-
-lemma fresh_star_plus:
-  fixes p q::perm
-  shows "\<lbrakk>a \<sharp>* p;  a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)"
-  unfolding fresh_star_def
-  by (simp add: fresh_plus_perm)
-
-
-lemma fresh_star_permute_iff:
-  shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x"
-  unfolding fresh_star_def
-  by (metis mem_permute_iff permute_minus_cancel(1) fresh_permute_iff)
-
-lemma fresh_star_eqvt[eqvt]:
-  shows "(p \<bullet> (as \<sharp>* x)) = (p \<bullet> as) \<sharp>* (p \<bullet> x)"
-unfolding fresh_star_def
-unfolding Ball_def
-apply(simp add: all_eqvt)
-apply(subst permute_fun_def)
-apply(simp add: imp_eqvt fresh_eqvt mem_eqvt)
-done
-
-section {* Avoiding of atom sets *}
-
-text {* 
-  For every set of atoms, there is another set of atoms
-  avoiding a finitely supported c and there is a permutation
-  which 'translates' between both sets.
-*}
-
-lemma at_set_avoiding_aux:
-  fixes Xs::"atom set"
-  and   As::"atom set"
-  assumes b: "Xs \<subseteq> As"
-  and     c: "finite As"
-  shows "\<exists>p. (p \<bullet> Xs) \<inter> As = {} \<and> (supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
-proof -
-  from b c have "finite Xs" by (rule finite_subset)
-  then show ?thesis using b
-  proof (induct rule: finite_subset_induct)
-    case empty
-    have "0 \<bullet> {} \<inter> As = {}" by simp
-    moreover
-    have "supp (0::perm) \<subseteq> {} \<union> 0 \<bullet> {}" by (simp add: supp_zero_perm)
-    ultimately show ?case by blast
-  next
-    case (insert x Xs)
-    then obtain p where
-      p1: "(p \<bullet> Xs) \<inter> As = {}" and 
-      p2: "supp p \<subseteq> (Xs \<union> (p \<bullet> Xs))" by blast
-    from `x \<in> As` p1 have "x \<notin> p \<bullet> Xs" by fast
-    with `x \<notin> Xs` p2 have "x \<notin> supp p" by fast
-    hence px: "p \<bullet> x = x" unfolding supp_perm by simp
-    have "finite (As \<union> p \<bullet> Xs)"
-      using `finite As` `finite Xs`
-      by (simp add: permute_set_eq_image)
-    then obtain y where "y \<notin> (As \<union> p \<bullet> Xs)" "sort_of y = sort_of x"
-      by (rule obtain_atom)
-    hence y: "y \<notin> As" "y \<notin> p \<bullet> Xs" "sort_of y = sort_of x"
-      by simp_all
-    let ?q = "(x \<rightleftharpoons> y) + p"
-    have q: "?q \<bullet> insert x Xs = insert y (p \<bullet> Xs)"
-      unfolding insert_eqvt
-      using `p \<bullet> x = x` `sort_of y = sort_of x`
-      using `x \<notin> p \<bullet> Xs` `y \<notin> p \<bullet> Xs`
-      by (simp add: swap_atom swap_set_not_in)
-    have "?q \<bullet> insert x Xs \<inter> As = {}"
-      using `y \<notin> As` `p \<bullet> Xs \<inter> As = {}`
-      unfolding q by simp
-    moreover
-    have "supp ?q \<subseteq> insert x Xs \<union> ?q \<bullet> insert x Xs"
-      using p2 unfolding q
-      by (intro subset_trans [OF supp_plus_perm])
-         (auto simp add: supp_swap)
-    ultimately show ?case by blast
-  qed
-qed
-
-lemma at_set_avoiding:
-  assumes a: "finite Xs"
-  and     b: "finite (supp c)"
-  obtains p::"perm" where "(p \<bullet> Xs)\<sharp>*c" and "(supp p) \<subseteq> (Xs \<union> (p \<bullet> Xs))"
-  using a b at_set_avoiding_aux [where Xs="Xs" and As="Xs \<union> supp c"]
-  unfolding fresh_star_def fresh_def by blast
-
-lemma at_set_avoiding2:
-  assumes "finite xs"
-  and     "finite (supp c)" "finite (supp x)"
-  and     "xs \<sharp>* x"
-  shows "\<exists>p. (p \<bullet> xs) \<sharp>* c \<and> supp x \<sharp>* p"
-using assms
-apply(erule_tac c="(c, x)" in at_set_avoiding)
-apply(simp add: supp_Pair)
-apply(rule_tac x="p" in exI)
-apply(simp add: fresh_star_prod)
-apply(subgoal_tac "\<forall>a \<in> supp p. a \<sharp> x")
-apply(auto simp add: fresh_star_def fresh_def supp_perm)[1]
-apply(auto simp add: fresh_star_def fresh_def)
-done
-
-lemma at_set_avoiding2_atom:
-  assumes "finite (supp c)" "finite (supp x)"
-  and     b: "a \<sharp> x"
-  shows "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p"
-proof -
-  have a: "{a} \<sharp>* x" unfolding fresh_star_def by (simp add: b)
-  obtain p where p1: "(p \<bullet> {a}) \<sharp>* c" and p2: "supp x \<sharp>* p"
-    using at_set_avoiding2[of "{a}" "c" "x"] assms a by blast
-  have c: "(p \<bullet> a) \<sharp> c" using p1
-    unfolding fresh_star_def Ball_def 
-    by(erule_tac x="p \<bullet> a" in allE) (simp add: permute_set_eq)
-  hence "p \<bullet> a \<sharp> c \<and> supp x \<sharp>* p" using p2 by blast
-  then show "\<exists>p. (p \<bullet> a) \<sharp> c \<and> supp x \<sharp>* p" by blast
-qed
-
-
-section {* The freshness lemma according to Andy Pitts *}
-
-lemma freshness_lemma:
-  fixes h :: "'a::at \<Rightarrow> 'b::pt"
-  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-  shows  "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
-proof -
-  from a obtain b where a1: "atom b \<sharp> h" and a2: "atom b \<sharp> h b"
-    by (auto simp add: fresh_Pair)
-  show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
-  proof (intro exI allI impI)
-    fix a :: 'a
-    assume a3: "atom a \<sharp> h"
-    show "h a = h b"
-    proof (cases "a = b")
-      assume "a = b"
-      thus "h a = h b" by simp
-    next
-      assume "a \<noteq> b"
-      hence "atom a \<sharp> b" by (simp add: fresh_at_base)
-      with a3 have "atom a \<sharp> h b" 
-        by (rule fresh_fun_app)
-      with a2 have d1: "(atom b \<rightleftharpoons> atom a) \<bullet> (h b) = (h b)"
-        by (rule swap_fresh_fresh)
-      from a1 a3 have d2: "(atom b \<rightleftharpoons> atom a) \<bullet> h = h"
-        by (rule swap_fresh_fresh)
-      from d1 have "h b = (atom b \<rightleftharpoons> atom a) \<bullet> (h b)" by simp
-      also have "\<dots> = ((atom b \<rightleftharpoons> atom a) \<bullet> h) ((atom b \<rightleftharpoons> atom a) \<bullet> b)"
-        by (rule permute_fun_app_eq)
-      also have "\<dots> = h a"
-        using d2 by simp
-      finally show "h a = h b"  by simp
-    qed
-  qed
-qed
-
-lemma freshness_lemma_unique:
-  fixes h :: "'a::at \<Rightarrow> 'b::pt"
-  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-  shows "\<exists>!x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
-proof (rule ex_ex1I)
-  from a show "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
-    by (rule freshness_lemma)
-next
-  fix x y
-  assume x: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = x"
-  assume y: "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = y"
-  from a x y show "x = y"
-    by (auto simp add: fresh_Pair)
-qed
-
-text {* packaging the freshness lemma into a function *}
-
-definition
-  fresh_fun :: "('a::at \<Rightarrow> 'b::pt) \<Rightarrow> 'b"
-where
-  "fresh_fun h = (THE x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x)"
-
-lemma fresh_fun_app:
-  fixes h :: "'a::at \<Rightarrow> 'b::pt"
-  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-  assumes b: "atom a \<sharp> h"
-  shows "fresh_fun h = h a"
-unfolding fresh_fun_def
-proof (rule the_equality)
-  show "\<forall>a'. atom a' \<sharp> h \<longrightarrow> h a' = h a"
-  proof (intro strip)
-    fix a':: 'a
-    assume c: "atom a' \<sharp> h"
-    from a have "\<exists>x. \<forall>a. atom a \<sharp> h \<longrightarrow> h a = x" by (rule freshness_lemma)
-    with b c show "h a' = h a" by auto
-  qed
-next
-  fix fr :: 'b
-  assume "\<forall>a. atom a \<sharp> h \<longrightarrow> h a = fr"
-  with b show "fr = h a" by auto
-qed
-
-lemma fresh_fun_app':
-  fixes h :: "'a::at \<Rightarrow> 'b::pt"
-  assumes a: "atom a \<sharp> h" "atom a \<sharp> h a"
-  shows "fresh_fun h = h a"
-  apply (rule fresh_fun_app)
-  apply (auto simp add: fresh_Pair intro: a)
-  done
-
-lemma fresh_fun_eqvt:
-  fixes h :: "'a::at \<Rightarrow> 'b::pt"
-  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-  shows "p \<bullet> (fresh_fun h) = fresh_fun (p \<bullet> h)"
-  using a
-  apply (clarsimp simp add: fresh_Pair)
-  apply (subst fresh_fun_app', assumption+)
-  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
-  apply (drule fresh_permute_iff [where p=p, THEN iffD2])
-  apply (simp add: atom_eqvt permute_fun_app_eq [where f=h])
-  apply (erule (1) fresh_fun_app' [symmetric])
-  done
-
-lemma fresh_fun_supports:
-  fixes h :: "'a::at \<Rightarrow> 'b::pt"
-  assumes a: "\<exists>a. atom a \<sharp> (h, h a)"
-  shows "(supp h) supports (fresh_fun h)"
-  apply (simp add: supports_def fresh_def [symmetric])
-  apply (simp add: fresh_fun_eqvt [OF a] swap_fresh_fresh)
-  done
-
-notation fresh_fun (binder "FRESH " 10)
-
-lemma FRESH_f_iff:
-  fixes P :: "'a::at \<Rightarrow> 'b::pure"
-  fixes f :: "'b \<Rightarrow> 'c::pure"
-  assumes P: "finite (supp P)"
-  shows "(FRESH x. f (P x)) = f (FRESH x. P x)"
-proof -
-  obtain a::'a where "atom a \<notin> supp P"
-    using P by (rule obtain_at_base)
-  hence "atom a \<sharp> P"
-    by (simp add: fresh_def)
-  show "(FRESH x. f (P x)) = f (FRESH x. P x)"
-    apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
-    apply (cut_tac `atom a \<sharp> P`)
-    apply (simp add: fresh_conv_MOST)
-    apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
-    apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
-    apply (rule refl)
-    done
-qed
-
-lemma FRESH_binop_iff:
-  fixes P :: "'a::at \<Rightarrow> 'b::pure"
-  fixes Q :: "'a::at \<Rightarrow> 'c::pure"
-  fixes binop :: "'b \<Rightarrow> 'c \<Rightarrow> 'd::pure"
-  assumes P: "finite (supp P)" 
-  and     Q: "finite (supp Q)"
-  shows "(FRESH x. binop (P x) (Q x)) = binop (FRESH x. P x) (FRESH x. Q x)"
-proof -
-  from assms have "finite (supp P \<union> supp Q)" by simp
-  then obtain a::'a where "atom a \<notin> (supp P \<union> supp Q)"
-    by (rule obtain_at_base)
-  hence "atom a \<sharp> P" and "atom a \<sharp> Q"
-    by (simp_all add: fresh_def)
-  show ?thesis
-    apply (subst fresh_fun_app' [where a=a, OF _ pure_fresh])
-    apply (cut_tac `atom a \<sharp> P` `atom a \<sharp> Q`)
-    apply (simp add: fresh_conv_MOST)
-    apply (elim MOST_rev_mp, rule MOST_I, clarify)
-    apply (simp add: permute_fun_def permute_pure expand_fun_eq)
-    apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> P` pure_fresh])
-    apply (subst fresh_fun_app' [where a=a, OF `atom a \<sharp> Q` pure_fresh])
-    apply (rule refl)
-    done
-qed
-
-lemma FRESH_conj_iff:
-  fixes P Q :: "'a::at \<Rightarrow> bool"
-  assumes P: "finite (supp P)" and Q: "finite (supp Q)"
-  shows "(FRESH x. P x \<and> Q x) \<longleftrightarrow> (FRESH x. P x) \<and> (FRESH x. Q x)"
-using P Q by (rule FRESH_binop_iff)
-
-lemma FRESH_disj_iff:
-  fixes P Q :: "'a::at \<Rightarrow> bool"
-  assumes P: "finite (supp P)" and Q: "finite (supp Q)"
-  shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
-using P Q by (rule FRESH_binop_iff)
-
-
-section {* @{const nat_of} is an example of a function 
-  without finite support *}
-
-
-lemma not_fresh_nat_of:
-  shows "\<not> a \<sharp> nat_of"
-unfolding fresh_def supp_def
-proof (clarsimp)
-  assume "finite {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of}"
-  hence "finite ({a} \<union> {b. (a \<rightleftharpoons> b) \<bullet> nat_of \<noteq> nat_of})"
-    by simp
-  then obtain b where
-    b1: "b \<noteq> a" and
-    b2: "sort_of b = sort_of a" and
-    b3: "(a \<rightleftharpoons> b) \<bullet> nat_of = nat_of"
-    by (rule obtain_atom) auto
-  have "nat_of a = (a \<rightleftharpoons> b) \<bullet> (nat_of a)" by (simp add: permute_nat_def)
-  also have "\<dots> = ((a \<rightleftharpoons> b) \<bullet> nat_of) ((a \<rightleftharpoons> b) \<bullet> a)" by (simp add: permute_fun_app_eq)
-  also have "\<dots> = nat_of ((a \<rightleftharpoons> b) \<bullet> a)" using b3 by simp
-  also have "\<dots> = nat_of b" using b2 by simp
-  finally have "nat_of a = nat_of b" by simp
-  with b2 have "a = b" by (simp add: atom_components_eq_iff)
-  with b1 show "False" by simp
-qed
-
-lemma supp_nat_of:
-  shows "supp nat_of = UNIV"
-  using not_fresh_nat_of [unfolded fresh_def] by auto
-
-
-section {* Induction principle for permutations *}
-
-
-lemma perm_struct_induct[consumes 1, case_names zero swap]:
-  assumes S: "supp p \<subseteq> S"
-  and zero: "P 0"
-  and swap: "\<And>p a b. \<lbrakk>P p; supp p \<subseteq> S; a \<in> S; b \<in> S; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
-  shows "P p"
-proof -
-  have "finite (supp p)" by (simp add: finite_supp)
-  then show "P p" using S
-  proof(induct A\<equiv>"supp p" arbitrary: p rule: finite_psubset_induct)
-    case (psubset p)
-    then have ih: "\<And>q. supp q \<subset> supp p \<Longrightarrow> P q" by auto
-    have as: "supp p \<subseteq> S" by fact
-    { assume "supp p = {}"
-      then have "p = 0" by (simp add: supp_perm expand_perm_eq)
-      then have "P p" using zero by simp
-    }
-    moreover
-    { assume "supp p \<noteq> {}"
-      then obtain a where a0: "a \<in> supp p" by blast
-      then have a1: "p \<bullet> a \<in> S" "a \<in> S" "sort_of (p \<bullet> a) = sort_of a" "p \<bullet> a \<noteq> a"
-        using as by (auto simp add: supp_atom supp_perm swap_atom)
-      let ?q = "(p \<bullet> a \<rightleftharpoons> a) + p"
-      have a2: "supp ?q \<subseteq> supp p" unfolding supp_perm by (auto simp add: swap_atom)
-      moreover
-      have "a \<notin> supp ?q" by (simp add: supp_perm)
-      then have "supp ?q \<noteq> supp p" using a0 by auto
-      ultimately have "supp ?q \<subset> supp p" using a2 by auto
-      then have "P ?q" using ih by simp
-      moreover
-      have "supp ?q \<subseteq> S" using as a2 by simp
-      ultimately  have "P ((p \<bullet> a \<rightleftharpoons> a) + ?q)" using as a1 swap by simp 
-      moreover 
-      have "p = (p \<bullet> a \<rightleftharpoons> a) + ?q" by (simp add: expand_perm_eq)
-      ultimately have "P p" by simp
-    }
-    ultimately show "P p" by blast
-  qed
-qed
-
-lemma perm_simple_struct_induct[case_names zero swap]:
-  assumes zero: "P 0"
-  and     swap: "\<And>p a b. \<lbrakk>P p; a \<noteq> b; sort_of a = sort_of b\<rbrakk> \<Longrightarrow> P ((a \<rightleftharpoons> b) + p)"
-  shows "P p"
-by (rule_tac S="supp p" in perm_struct_induct)
-   (auto intro: zero swap)
-
-lemma perm_subset_induct[consumes 1, case_names zero swap plus]:
-  assumes S: "supp p \<subseteq> S"
-  assumes zero: "P 0"
-  assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b; a \<in> S; b \<in> S\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"
-  assumes plus: "\<And>p1 p2. \<lbrakk>P p1; P p2; supp p1 \<subseteq> S; supp p2 \<subseteq> S\<rbrakk> \<Longrightarrow> P (p1 + p2)"
-  shows "P p"
-using S
-by (induct p rule: perm_struct_induct)
-   (auto intro: zero plus swap simp add: supp_swap)
-
-lemma supp_perm_eq:
-  assumes "(supp x) \<sharp>* p"
-  shows "p \<bullet> x = x"
-proof -
-  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
-    unfolding supp_perm fresh_star_def fresh_def by auto
-  then show "p \<bullet> x = x"
-  proof (induct p rule: perm_struct_induct)
-    case zero
-    show "0 \<bullet> x = x" by simp
-  next
-    case (swap p a b)
-    then have "a \<sharp> x" "b \<sharp> x" "p \<bullet> x = x" by simp_all
-    then show "((a \<rightleftharpoons> b) + p) \<bullet> x = x" by (simp add: swap_fresh_fresh)
-  qed
-qed
-
-lemma supp_perm_eq_test:
-  assumes "(supp x) \<sharp>* p"
-  shows "p \<bullet> x = x"
-proof -
-  from assms have "supp p \<subseteq> {a. a \<sharp> x}"
-    unfolding supp_perm fresh_star_def fresh_def by auto
-  then show "p \<bullet> x = x"
-  proof (induct p rule: perm_subset_induct)
-    case zero
-    show "0 \<bullet> x = x" by simp
-  next
-    case (swap a b)
-    then have "a \<sharp> x" "b \<sharp> x" by simp_all
-    then show "(a \<rightleftharpoons> b) \<bullet> x = x" by (simp add: swap_fresh_fresh)
-  next
-    case (plus p1 p2)
-    have "p1 \<bullet> x = x" "p2 \<bullet> x = x" by fact+
-    then show "(p1 + p2) \<bullet> x = x" by simp
-  qed
-qed
-
-
-section {* Support of Finite Sets of Finitely Supported Elements *}
-
-lemma Union_fresh:
-  shows "a \<sharp> S \<Longrightarrow> a \<sharp> (\<Union>x \<in> S. supp x)"
-  unfolding Union_image_eq[symmetric]
-  apply(rule_tac f="\<lambda>S. \<Union> supp ` S" in fresh_fun_eqvt_app)
-  apply(perm_simp)
-  apply(rule refl)
-  apply(assumption)
-  done
-
-lemma Union_supports_set:
-  shows "(\<Union>x \<in> S. supp x) supports S"
-proof -
-  { fix a b
-    have "\<forall>x \<in> S. (a \<rightleftharpoons> b) \<bullet> x = x \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> S = S"
-      unfolding permute_set_eq by force
-  }
-  then show "(\<Union>x \<in> S. supp x) supports S"
-    unfolding supports_def 
-    by (simp add: fresh_def[symmetric] swap_fresh_fresh)
-qed
-
-lemma Union_of_fin_supp_sets:
-  fixes S::"('a::fs set)"
-  assumes fin: "finite S"   
-  shows "finite (\<Union>x\<in>S. supp x)"
-  using fin by (induct) (auto simp add: finite_supp)
-
-lemma Union_included_in_supp:
-  fixes S::"('a::fs set)"
-  assumes fin: "finite S"
-  shows "(\<Union>x\<in>S. supp x) \<subseteq> supp S"
-proof -
-  have "(\<Union>x\<in>S. supp x) = supp (\<Union>x\<in>S. supp x)"
-    by (rule supp_finite_atom_set[symmetric])
-       (rule Union_of_fin_supp_sets[OF fin])
-  also have "\<dots> \<subseteq> supp S"
-    by (rule supp_subset_fresh)
-       (simp add: Union_fresh)
-  finally show "(\<Union>x\<in>S. supp x) \<subseteq> supp S" .
-qed
-
-lemma supp_of_fin_sets:
-  fixes S::"('a::fs set)"
-  assumes fin: "finite S"
-  shows "(supp S) = (\<Union>x\<in>S. supp x)"
-apply(rule subset_antisym)
-apply(rule supp_is_subset)
-apply(rule Union_supports_set)
-apply(rule Union_of_fin_supp_sets[OF fin])
-apply(rule Union_included_in_supp[OF fin])
-done
-
-lemma supp_of_fin_union:
-  fixes S T::"('a::fs) set"
-  assumes fin1: "finite S"
-  and     fin2: "finite T"
-  shows "supp (S \<union> T) = supp S \<union> supp T"
-  using fin1 fin2
-  by (simp add: supp_of_fin_sets)
-
-lemma supp_of_fin_insert:
-  fixes S::"('a::fs) set"
-  assumes fin:  "finite S"
-  shows "supp (insert x S) = supp x \<union> supp S"
-  using fin
-  by (simp add: supp_of_fin_sets)
-
-
-end
diff -r 1b31d514a087 -r cda25f9aa678 Nominal-General/nominal_atoms.ML
--- a/Nominal-General/nominal_atoms.ML	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/nominal_atoms.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -26,7 +26,7 @@
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
   let
-    val _ = Theory.requires thy "Nominal2_Atoms" "nominal logic";
+    val _ = Theory.requires thy "Nominal2_Base" "nominal logic";
     val str = Sign.full_name thy name;
 
     (* typedef *)
diff -r 1b31d514a087 -r cda25f9aa678 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal-General/nominal_library.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -49,6 +49,7 @@
   val mk_append: term * term -> term
   val mk_union: term * term -> term
   val fold_union: term list -> term
+  val fold_append: term list -> term
   val mk_conj: term * term -> term
   val fold_conj: term list -> term
 
@@ -144,6 +145,8 @@
 
 fun mk_diff (@{term "{}::atom set"}, _) = @{term "{}::atom set"}
   | mk_diff (t1, @{term "{}::atom set"}) = t1
+  | mk_diff (@{term "set ([]::atom list)"}, _) = @{term "set ([]::atom list)"}
+  | mk_diff (t1, @{term "set ([]::atom list)"}) = t1
   | mk_diff (t1, t2) = HOLogic.mk_binop @{const_name minus} (t1, t2)
 
 fun mk_append (t1, @{term "[]::atom list"}) = t1
@@ -152,9 +155,12 @@
 
 fun mk_union (t1, @{term "{}::atom set"}) = t1
   | mk_union (@{term "{}::atom set"}, t2) = t2
+  | mk_union (t1, @{term "set ([]::atom list)"}) = t1
+  | mk_union (@{term "set ([]::atom list)"}, t2) = t2
   | mk_union (t1, t2) = HOLogic.mk_binop @{const_name "sup"} (t1, t2)  
  
 fun fold_union trms = fold_rev (curry mk_union) trms @{term "{}::atom set"}
+fun fold_append trms = fold_rev (curry mk_append) trms @{term "[]::atom list"}
 
 fun mk_conj (t1, @{term "True"}) = t1
   | mk_conj (@{term "True"}, t2) = t2
diff -r 1b31d514a087 -r cda25f9aa678 Nominal/Abs.thy
--- a/Nominal/Abs.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Abs.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -1,17 +1,16 @@
 theory Abs
-imports "../Nominal-General/Nominal2_Atoms" 
+imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Eqvt" 
-        "../Nominal-General/Nominal2_Supp" 
         "Quotient" 
         "Quotient_List"
         "Quotient_Product" 
 begin
 
 fun
-  alpha_gen 
+  alpha_set 
 where
-  alpha_gen[simp del]:
-  "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> 
+  alpha_set[simp del]:
+  "alpha_set (bs, x) R f pi (cs, y) \<longleftrightarrow> 
      f x - bs = f y - cs \<and> 
      (f x - bs) \<sharp>* pi \<and> 
      R (pi \<bullet> x) y \<and>
@@ -36,17 +35,17 @@
      R (pi \<bullet> x) y \<and>
      pi \<bullet> bs = cs"
 
-lemmas alphas = alpha_gen.simps alpha_res.simps alpha_lst.simps
+lemmas alphas = alpha_set.simps alpha_res.simps alpha_lst.simps
 
 notation
-  alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) and
+  alpha_set ("_ \<approx>set _ _ _ _" [100, 100, 100, 100, 100] 100) and
   alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) and
   alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) 
 
 section {* Mono *}
 
 lemma [mono]: 
-  shows "R1 \<le> R2 \<Longrightarrow> alpha_gen bs R1 \<le> alpha_gen bs R2"
+  shows "R1 \<le> R2 \<Longrightarrow> alpha_set bs R1 \<le> alpha_set bs R2"
   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) 
@@ -55,7 +54,7 @@
 section {* Equivariance *}
 
 lemma alpha_eqvt[eqvt]:
-  shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
+  shows "(bs, x) \<approx>set R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>set (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst (p \<bullet> R) (p \<bullet> f) (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 
   unfolding alphas
@@ -70,7 +69,7 @@
 
 lemma alpha_refl:
   assumes a: "R x x"
-  shows "(bs, x) \<approx>gen R f 0 (bs, x)"
+  shows "(bs, x) \<approx>set R f 0 (bs, x)"
   and   "(bs, x) \<approx>res R f 0 (bs, x)"
   and   "(cs, x) \<approx>lst R f 0 (cs, x)"
   using a 
@@ -80,7 +79,7 @@
 
 lemma alpha_sym:
   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x"
-  shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)"
+  shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)"
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)"
   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
@@ -89,7 +88,7 @@
 
 lemma alpha_trans:
   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"
-  shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"
+  shows "\<lbrakk>(bs, x) \<approx>set R f p (cs, y); (cs, y) \<approx>set R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>set R f (q + p) (ds, z)"
   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"
   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"
   using a
@@ -99,7 +98,7 @@
 lemma alpha_sym_eqvt:
   assumes a: "R (p \<bullet> x) y \<Longrightarrow> R y (p \<bullet> x)" 
   and     b: "p \<bullet> R = R"
-  shows "(bs, x) \<approx>gen R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>gen R f (- p) (bs, x)" 
+  shows "(bs, x) \<approx>set R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>set R f (- p) (bs, x)" 
   and   "(bs, x) \<approx>res R f p (cs, y) \<Longrightarrow> (cs, y) \<approx>res R f (- p) (bs, x)" 
   and   "(ds, x) \<approx>lst R f p (es, y) \<Longrightarrow> (es, y) \<approx>lst R f (- p) (ds, x)"
 apply(auto intro!: alpha_sym)
@@ -113,12 +112,12 @@
 apply(assumption)
 done
 
-lemma alpha_gen_trans_eqvt:
-  assumes b: "(cs, y) \<approx>gen R f q (ds, z)"
-  and     a: "(bs, x) \<approx>gen R f p (cs, y)" 
+lemma alpha_set_trans_eqvt:
+  assumes b: "(cs, y) \<approx>set R f q (ds, z)"
+  and     a: "(bs, x) \<approx>set R f p (cs, y)" 
   and     d: "q \<bullet> R = R"
   and     c: "\<lbrakk>R (p \<bullet> x) y; R y (- q \<bullet> z)\<rbrakk> \<Longrightarrow> R (p \<bullet> x) (- q \<bullet> z)"
-  shows "(bs, x) \<approx>gen R f (q + p) (ds, z)"
+  shows "(bs, x) \<approx>set R f (q + p) (ds, z)"
 apply(rule alpha_trans)
 defer
 apply(rule a)
@@ -173,16 +172,16 @@
 apply(simp add: permute_eqvt[symmetric])
 done
 
-lemmas alpha_trans_eqvt = alpha_gen_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
+lemmas alpha_trans_eqvt = alpha_set_trans_eqvt alpha_res_trans_eqvt alpha_lst_trans_eqvt
 
 
 section {* General Abstractions *}
 
 fun
-  alpha_abs 
+  alpha_abs_set 
 where
   [simp del]:
-  "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"
+  "alpha_abs_set (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op=) supp p (cs, y))"
 
 fun
   alpha_abs_lst
@@ -197,15 +196,15 @@
   "alpha_abs_res (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op=) supp p (cs, y))"
 
 notation
-  alpha_abs (infix "\<approx>abs" 50) and
+  alpha_abs_set (infix "\<approx>abs'_set" 50) and
   alpha_abs_lst (infix "\<approx>abs'_lst" 50) and
   alpha_abs_res (infix "\<approx>abs'_res" 50)
 
-lemmas alphas_abs = alpha_abs.simps alpha_abs_res.simps alpha_abs_lst.simps
+lemmas alphas_abs = alpha_abs_set.simps alpha_abs_res.simps alpha_abs_lst.simps
 
 
 lemma alphas_abs_refl:
-  shows "(bs, x) \<approx>abs (bs, x)"
+  shows "(bs, x) \<approx>abs_set (bs, x)"
   and   "(bs, x) \<approx>abs_res (bs, x)"
   and   "(cs, x) \<approx>abs_lst (cs, x)" 
   unfolding alphas_abs
@@ -215,7 +214,7 @@
      (simp_all add: fresh_zero_perm)
 
 lemma alphas_abs_sym:
-  shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (cs, y) \<approx>abs (bs, x)"
+  shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_set (bs, x)"
   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (cs, y) \<approx>abs_res (bs, x)"
   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (es, y) \<approx>abs_lst (ds, x)"
   unfolding alphas_abs
@@ -225,7 +224,7 @@
      (auto simp add: fresh_minus_perm)
 
 lemma alphas_abs_trans:
-  shows "\<lbrakk>(bs, x) \<approx>abs (cs, y); (cs, y) \<approx>abs (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs (ds, z)"
+  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)"
   and   "\<lbrakk>(bs, x) \<approx>abs_res (cs, y); (cs, y) \<approx>abs_res (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>abs_res (ds, z)"
   and   "\<lbrakk>(es, x) \<approx>abs_lst (gs, y); (gs, y) \<approx>abs_lst (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>abs_lst (hs, z)"
   unfolding alphas_abs
@@ -236,7 +235,7 @@
   by (simp_all add: fresh_plus_perm)
 
 lemma alphas_abs_eqvt:
-  shows "(bs, x) \<approx>abs (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs (p \<bullet> cs, p \<bullet> y)"
+  shows "(bs, x) \<approx>abs_set (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_set (p \<bullet> cs, p \<bullet> y)"
   and   "(bs, x) \<approx>abs_res (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>abs_res (p \<bullet> cs, p \<bullet> y)"
   and   "(ds, x) \<approx>abs_lst (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>abs_lst (p \<bullet> es, p \<bullet> y)"
   unfolding alphas_abs
@@ -249,7 +248,7 @@
   by (auto simp add: fresh_star_permute_iff permute_eqvt[symmetric])
 
 quotient_type 
-    'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"
+    'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set"
 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res"
 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst"
   apply(rule_tac [!] equivpI)
@@ -257,9 +256,9 @@
   by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:)
 
 quotient_definition
-  Abs ("[_]set. _" [60, 60] 60)
+  Abs_set ("[_]set. _" [60, 60] 60)
 where
-  "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"
+  "Abs_set::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_set"
 is
   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"
 
@@ -278,21 +277,21 @@
   "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)"
 
 lemma [quot_respect]:
-  shows "(op= ===> op= ===> alpha_abs) Pair Pair"
+  shows "(op= ===> op= ===> alpha_abs_set) Pair Pair"
   and   "(op= ===> op= ===> alpha_abs_res) Pair Pair"
   and   "(op= ===> op= ===> alpha_abs_lst) Pair Pair"
   unfolding fun_rel_def
   by (auto intro: alphas_abs_refl)
 
 lemma [quot_respect]:
-  shows "(op= ===> alpha_abs ===> alpha_abs) permute permute"
+  shows "(op= ===> alpha_abs_set ===> alpha_abs_set) permute permute"
   and   "(op= ===> alpha_abs_res ===> alpha_abs_res) permute permute"
   and   "(op= ===> alpha_abs_lst ===> alpha_abs_lst) permute permute"
   unfolding fun_rel_def
   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
 lemma abs_exhausts:
-  shows "(\<And>as (x::'a::pt). y1 = Abs as x \<Longrightarrow> P1) \<Longrightarrow> P1"
+  shows "(\<And>as (x::'a::pt). y1 = Abs_set as x \<Longrightarrow> P1) \<Longrightarrow> P1"
   and   "(\<And>as (x::'a::pt). y2 = Abs_res as x \<Longrightarrow> P2) \<Longrightarrow> P2"
   and   "(\<And>as (x::'a::pt). y3 = Abs_lst as x \<Longrightarrow> P3) \<Longrightarrow> P3"
   by (lifting prod.exhaust[where 'a="atom set" and 'b="'a"]
@@ -300,22 +299,22 @@
               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
 lemma abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)"
+  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (bs, x) \<approx>abs_set (cs, y)"
   and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)"
   and   "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)"
   unfolding alphas_abs by (lifting alphas_abs)
 
-instantiation abs_gen :: (pt) pt
+instantiation abs_set :: (pt) pt
 begin
 
 quotient_definition
-  "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"
+  "permute_abs_set::perm \<Rightarrow> ('a::pt abs_set) \<Rightarrow> 'a abs_set"
 is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
 lemma permute_Abs[simp]:
   fixes x::"'a::pt"  
-  shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"
+  shows "(p \<bullet> (Abs_set as x)) = Abs_set (p \<bullet> as) (p \<bullet> x)"
   by (lifting permute_prod.simps[where 'a="atom set" and 'b="'a"])
 
 instance
@@ -368,13 +367,13 @@
 
 end
 
-lemmas permute_abs = permute_Abs permute_Abs_res permute_Abs_lst
+lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst
 
 
 lemma abs_swap1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
-  shows "Abs bs x = Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
+  shows "Abs_set bs x = Abs_set ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
   and   "Abs_res bs x = Abs_res ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
   unfolding abs_eq_iff
   unfolding alphas_abs
@@ -401,7 +400,7 @@
      (auto simp add: supp_perm swap_atom)
 
 lemma abs_supports:
-  shows "((supp x) - as) supports (Abs as x)"
+  shows "((supp x) - as) supports (Abs_set as x)"
   and   "((supp x) - as) supports (Abs_res as x)"
   and   "((supp x) - set bs) supports (Abs_lst bs x)"
   unfolding supports_def
@@ -409,15 +408,15 @@
   by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
 
 function
-  supp_gen  :: "('a::pt) abs_gen \<Rightarrow> atom set"
+  supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set"
 where
-  "supp_gen (Abs as x) = supp x - as"
+  "supp_set (Abs_set as x) = supp x - as"
 apply(case_tac x rule: abs_exhausts(1))
 apply(simp)
 apply(simp add: abs_eq_iff alphas_abs alphas)
 done
 
-termination supp_gen 
+termination supp_set 
   by (auto intro!: local.termination)
 
 function
@@ -445,7 +444,7 @@
   by (auto intro!: local.termination)
 
 lemma [eqvt]:
-  shows "(p \<bullet> supp_gen x) = supp_gen (p \<bullet> x)"
+  shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"
   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"
   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"
   apply(case_tac x rule: abs_exhausts(1))
@@ -457,15 +456,15 @@
   done
 
 lemma aux_fresh:
-  shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)"
+  shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"
   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"
   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"
   by (rule_tac [!] fresh_fun_eqvt_app)
-     (simp_all add: eqvts_raw)
+     (simp_all only: eqvts_raw)
 
 lemma supp_abs_subset1:
   assumes a: "finite (supp x)"
-  shows "(supp x) - as \<subseteq> supp (Abs as x)"
+  shows "(supp x) - as \<subseteq> supp (Abs_set as x)"
   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"
   and   "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)"
   unfolding supp_conv_fresh
@@ -474,7 +473,7 @@
 
 lemma supp_abs_subset2:
   assumes a: "finite (supp x)"
-  shows "supp (Abs as x) \<subseteq> (supp x) - as"
+  shows "supp (Abs_set as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_res as x) \<subseteq> (supp x) - as"
   and   "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)"
   by (rule_tac [!] supp_is_subset)
@@ -482,7 +481,7 @@
 
 lemma abs_finite_supp:
   assumes a: "finite (supp x)"
-  shows "supp (Abs as x) = (supp x) - as"
+  shows "supp (Abs_set as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
   by (rule_tac [!] subset_antisym)
@@ -490,13 +489,13 @@
 
 lemma supp_abs:
   fixes x::"'a::fs"
-  shows "supp (Abs as x) = (supp x) - as"
+  shows "supp (Abs_set as x) = (supp x) - as"
   and   "supp (Abs_res as x) = (supp x) - as"
   and   "supp (Abs_lst bs x) = (supp x) - (set bs)"
   by (rule_tac [!] abs_finite_supp)
      (simp_all add: finite_supp)
 
-instance abs_gen :: (fs) fs
+instance abs_set :: (fs) fs
   apply(default)
   apply(case_tac x rule: abs_exhausts(1))
   apply(simp add: supp_abs finite_supp)
@@ -516,13 +515,22 @@
 
 lemma abs_fresh_iff:
   fixes x::"'a::fs"
-  shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
+  shows "a \<sharp> Abs_set bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
   and   "a \<sharp> Abs_res bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"
   and   "a \<sharp> Abs_lst cs x \<longleftrightarrow> a \<in> (set cs) \<or> (a \<notin> (set cs) \<and> a \<sharp> x)"
   unfolding fresh_def
   unfolding supp_abs
   by auto
 
+lemma Abs_eq_iff:
+  shows "Abs_set bs x = Abs_set cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>set (op =) supp p (cs, y))"
+  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
+  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
+  by (lifting alphas_abs)
+
+
+section {* Infrastructure for building tuples of relations and functions *}
+
 fun
   prod_fv :: "('a \<Rightarrow> atom set) \<Rightarrow> ('b \<Rightarrow> atom set) \<Rightarrow> ('a \<times> 'b) \<Rightarrow> atom set"
 where
@@ -560,16 +568,5 @@
   by (perm_simp) (rule refl)
 
 
-(* Below seems to be not needed *)
-
-(*
-lemma Abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
-  by (lifting alphas_abs)
-*)
-
-
 end
 
diff -r 1b31d514a087 -r cda25f9aa678 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Ex/SingleLet.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -10,18 +10,17 @@
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind x in t
-| Let a::"assg" t::"trm"  bind (set) "bn a" in t
+| Let a::"assg" t::"trm"  bind "bn a" in t
 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind (set) x in y t t1 t2
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
 | Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
 and assg =
   As "name" x::"name" t::"trm" bind x in t
 binder
-  bn::"assg \<Rightarrow> atom set"
+  bn::"assg \<Rightarrow> atom list"
 where
-  "bn (As x y t) = {atom x}"
+  "bn (As x y t) = [atom x]"
 
-thm Ball_def Bex_def mem_def
 
 thm single_let.distinct
 thm single_let.induct
@@ -35,47 +34,106 @@
 thm single_let.supports
 thm single_let.fsupp
 
+lemma test2:
+  assumes "fv_trm t = supp t" 
+  shows "\<forall>p. fv_trm (p \<bullet> t) = supp (p \<bullet> t)"
+apply(rule allI)
+apply(rule_tac p="-p" in permute_boolE)
+apply(perm_simp add: single_let.fv_bn_eqvt permute_minus_cancel)
+apply(rule assms)
+done
+
+
+lemma supp_fv:
+  "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = {a. infinite {b. \<not>alpha_bn ((a \<rightleftharpoons> b) \<bullet> as) as}}"
+apply(rule single_let.induct)
+apply(simp_all (no_asm_use) only: single_let.fv_defs)[2]
+apply(simp_all (no_asm_use) only: supp_def)[2]
+apply(simp_all (no_asm_use) only: single_let.perm_simps)[2]
+apply(simp_all (no_asm_use) only: single_let.eq_iff)[2]
+apply(simp_all (no_asm_use) only: de_Morgan_conj)[2]
+apply(simp_all (no_asm_use) only: Collect_disj_eq)[2]
+apply(simp_all (no_asm_use) only: finite_Un)[2]
+apply(simp_all (no_asm_use) only: de_Morgan_conj)[2]
+apply(simp_all (no_asm_use) only: Collect_disj_eq)[2]
+apply(simp)
+--" 1 "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)
+apply(simp only:)
+-- " 2 "
+apply(erule conjE)+
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)
+apply(simp only:)
+-- " 3 "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(1)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- " Bar "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- " Baz "
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- "last"
+apply(rule conjI)
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+-- "other case"
+apply(simp only: single_let.fv_defs supp_Pair[symmetric])
+apply(simp only: supp_abs(3)[symmetric])
+apply(simp (no_asm) only: supp_def)
+apply(perm_simp add: single_let.perm_simps single_let.fv_bn_eqvt)
+apply(simp (no_asm) only: single_let.eq_iff Abs_eq_iff)
+apply(simp only: alphas prod_alpha_def prod_fv.simps prod_rel.simps permute_prod_def prod.recs prod.cases prod.inject)
+apply(simp only: de_Morgan_conj Collect_disj_eq finite_Un)?
+apply(drule test2)+
+apply(simp only: supp_Pair Un_assoc conj_assoc)
+done
 
 
 
-(*
-lemma test: 
-  "(\<exists>p. (bs, x) \<approx>lst (op=) f p (cs, y)) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>lst (op=) supp p (cs, y))"
-oops
 
-lemma Abs_eq_iff:
-  shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"
-  and   "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>res (op =) supp p (cs, y))"
-  and   "Abs_lst bsl x = Abs_lst csl y \<longleftrightarrow> (\<exists>p. (bsl, x) \<approx>lst (op =) supp p (csl, y))"
-  by (lifting alphas_abs)
-*)
 
-(*
-lemma supp_fv:
-  "supp t = fv_trm t \<and> supp b = fv_bn b"
-apply(rule single_let.induct)
-apply(simp_all only: single_let.fv_defs)[2]
-apply(simp_all only: supp_def)[2]
-apply(simp_all only: single_let.perm_simps)[2]
-apply(simp_all only: single_let.eq_iff)[2]
-apply(simp_all only: de_Morgan_conj)[2]
-apply(simp_all only: Collect_disj_eq)[2]
-apply(simp_all only: finite_Un)[2]
-apply(simp_all only: de_Morgan_conj)[2]
-apply(simp_all only: Collect_disj_eq)[2]
-apply(subgoal_tac "supp (Lam name trm) = supp (Abs_lst [atom name] trm)")
-apply(simp only: single_let.fv_defs)
-apply(simp only: supp_abs)
-apply(simp)
-apply(simp (no_asm) only: supp_def)
-apply(simp only: single_let.perm_simps)
-apply(simp only: single_let.eq_iff)
-apply(simp only: permute_abs atom_eqvt permute_list.simps)
-apply(simp only: Abs_eq_iff)
-apply(subst test)
-apply(rule refl)
-sorry
-*)
+text {* *}
+
 (*
 consts perm_bn_trm :: "perm \<Rightarrow> trm \<Rightarrow> trm"
 consts perm_bn_assg :: "perm \<Rightarrow> assg \<Rightarrow> assg"
diff -r 1b31d514a087 -r cda25f9aa678 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Ex/TypeSchemes.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -14,15 +14,39 @@
 and tys =
   All xs::"name fset" ty::"ty" bind (res) xs in ty
 
+thm ty_tys.distinct
+thm ty_tys.induct
+thm ty_tys.exhaust
+thm ty_tys.fv_defs
+thm ty_tys.bn_defs
+thm ty_tys.perm_simps
+thm ty_tys.eq_iff
+thm ty_tys.fv_bn_eqvt
+thm ty_tys.size_eqvt
+thm ty_tys.supports
+thm ty_tys.fsupp
 
 nominal_datatype ty2 =
   Var2 "name"
 | Fun2 "ty2" "ty2"
 
-
 nominal_datatype tys2 =
   All2 xs::"name fset" ty::"ty2" bind (res) xs in ty
 
+thm tys2.distinct
+thm tys2.induct
+thm tys2.exhaust
+thm tys2.fv_defs
+thm tys2.bn_defs
+thm tys2.perm_simps
+thm tys2.eq_iff
+thm tys2.fv_bn_eqvt
+thm tys2.size_eqvt
+thm tys2.supports
+thm tys2.fsupp
+
+
+text {* *}
 
 (*
 ML {* Sign.of_sort @{theory} (@{typ ty}, @{sort fs}) *}
diff -r 1b31d514a087 -r cda25f9aa678 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Nominal2.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -2,7 +2,6 @@
 imports 
   "../Nominal-General/Nominal2_Base" 
   "../Nominal-General/Nominal2_Eqvt" 
-  "../Nominal-General/Nominal2_Supp" 
   "Nominal2_FSet"
   "Abs"
 uses ("nominal_dt_rawperm.ML")
diff -r 1b31d514a087 -r cda25f9aa678 Nominal/Nominal2_FSet.thy
--- a/Nominal/Nominal2_FSet.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/Nominal2_FSet.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -1,6 +1,5 @@
 theory Nominal2_FSet
-imports "../Nominal-General/Nominal2_Supp"
-        "../Nominal-General/Nominal2_Atoms" 
+imports "../Nominal-General/Nominal2_Base"
         "../Nominal-General/Nominal2_Eqvt" 
         FSet 
 begin
@@ -9,11 +8,8 @@
   shows "(op = ===> list_eq ===> list_eq) permute permute"
   apply(simp)
   apply(clarify)
-  apply(simp add: eqvts[symmetric])  
-  apply(subst permute_minus_cancel(1)[symmetric, of "xb"])
-  apply(subst mem_eqvt[symmetric])
-  apply(subst (2) permute_minus_cancel(1)[symmetric, of "xb"])
-  apply(subst mem_eqvt[symmetric])
+  apply(rule_tac p="-x" in permute_boolE)
+  apply(perm_simp add: permute_minus_cancel)
   apply(simp)
   done
 
@@ -36,14 +32,12 @@
 
 end
 
-lemma permute_fset[simp]:
+lemma permute_fset[simp, eqvt]:
   fixes S::"('a::pt) fset"
   shows "(p \<bullet> {||}) = ({||} ::('a::pt) fset)"
   and "p \<bullet> finsert x S = finsert (p \<bullet> x) (p \<bullet> S)"
   by (lifting permute_list.simps)
 
-declare permute_fset[eqvt]
-
 lemma fmap_eqvt[eqvt]: 
   shows "p \<bullet> (fmap f S) = fmap (p \<bullet> f) (p \<bullet> S)"
   by (lifting map_eqvt)
@@ -113,7 +107,7 @@
   apply (simp add: fresh_set_empty)
   apply simp
   apply (unfold fresh_def)
-  apply (simp add: supp_atom_insert)
+  apply (simp add: supp_of_fin_insert)
   apply (rule conjI)
   apply (unfold fresh_star_def)
   apply simp
diff -r 1b31d514a087 -r cda25f9aa678 Nominal/nominal_dt_alpha.ML
--- a/Nominal/nominal_dt_alpha.ML	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/nominal_dt_alpha.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -64,7 +64,7 @@
 end
 
 (* generates the compound binder terms *)
-fun mk_binders lthy bmode args bodies = 
+fun mk_binders lthy bmode args binders = 
 let  
   fun bind_set lthy args (NONE, i) = setify lthy (nth args i)
     | bind_set _ args (SOME bn, i) = bn $ (nth args i)
@@ -77,7 +77,7 @@
     | Set => (mk_union,  bind_set)
     | Res => (mk_union,  bind_set)
 in
-  bodies
+  binders
   |> map (bind_fn lthy args)
   |> foldl1 combine_fn 
 end
@@ -88,7 +88,7 @@
   val (alpha_name, binder_ty) = 
     case bmode of
       Lst => (@{const_name "alpha_lst"}, @{typ "atom list"})
-    | Set => (@{const_name "alpha_gen"}, @{typ "atom set"})
+    | Set => (@{const_name "alpha_set"}, @{typ "atom set"})
     | Res => (@{const_name "alpha_res"}, @{typ "atom set"})
   val ty = fastype_of args
   val pair_ty = HOLogic.mk_prodT (binder_ty, ty)
diff -r 1b31d514a087 -r cda25f9aa678 Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Mon Aug 30 15:59:50 2010 +0900
+++ b/Nominal/nominal_dt_rawfuns.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -151,7 +151,7 @@
 
 (** functions that construct the equations for fv and fv_bn **)
 
-fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
+fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (bmode, binders, bodies)) =
 let
   fun mk_fv_body fv_map args i = 
   let
@@ -163,21 +163,33 @@
     | SOME fv => fv $ arg
   end  
 
-  fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = 
+  fun mk_fv_binder lthy fv_bn_map args binders = 
   let
-    val arg = nth args i
+    fun bind_set lthy args (NONE, i) = (setify lthy (nth args i), @{term "{}::atom set"})
+      | bind_set _ args (SOME bn, i) = (bn $ (nth args i), 
+          if  member (op=) bodies i then @{term "{}::atom set"}  
+          else lookup fv_bn_map bn $ (nth args i))
+    fun bind_lst lthy args (NONE, i) = (listify lthy (nth args i), @{term "[]::atom list"})
+      | bind_lst _ args (SOME bn, i) = (bn $ (nth args i),
+          if  member (op=) bodies i then @{term "[]::atom list"}  
+          else lookup fv_bn_map bn $ (nth args i)) 
+  
+    val (combine_fn, bind_fn) =
+      case bmode of
+        Lst => (fold_append, bind_lst) 
+      | Set => (fold_union, bind_set)
+      | Res => (fold_union, bind_set)
   in
-    case bn_option of
-      NONE => (setify lthy arg, @{term "{}::atom set"})
-    | SOME bn => (to_set (bn $ arg), 
-       if  member (op=) bodies i then @{term "{}::atom set"}  
-       else lookup fv_bn_map bn $ arg)
+    binders
+    |> map (bind_fn lthy args)
+    |> split_list
+    |> pairself combine_fn
   end  
 
   val t1 = map (mk_fv_body fv_map args) bodies
-  val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders)
+  val (t2, t3) = mk_fv_binder lthy fv_bn_map args binders
 in 
-  fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
+  mk_union (mk_diff (fold_union t1, to_set t2), to_set t3)
 end
 
 (* in case of fv_bn we have to treat the case special, where an
diff -r 1b31d514a087 -r cda25f9aa678 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Paper/Paper.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Nominal/NewParser" "LaTeXsugar"
+imports "../Nominal/Nominal2" "LaTeXsugar"
 begin
 
 consts
@@ -21,21 +21,21 @@
   supp ("supp _" [78] 73) and
   uminus ("-_" [78] 73) and
   If  ("if _ then _ else _" 10) and
-  alpha_gen ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
+  alpha_set ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{set}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_lst ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{list}}$}}>\<^bsup>_, _, _\<^esup> _") and
   alpha_res ("_ \<approx>\<^raw:\,\raisebox{-1pt}{\makebox[0mm][l]{$_{\textit{res}}$}}>\<^bsup>_, _, _\<^esup> _") and
   abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and
   abs_set2 ("_ \<approx>\<^raw:\raisebox{-1pt}{\makebox[0mm][l]{$\,_{\textit{list}}$}}>\<^bsup>_\<^esup>  _") and
   fv ("fa'(_')" [100] 100) and
   equal ("=") and
-  alpha_abs ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
-  Abs ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
+  alpha_abs_set ("_ \<approx>\<^raw:{$\,_{\textit{abs\_set}}$}> _") and 
+  Abs_set ("[_]\<^bsub>set\<^esub>._" [20, 101] 999) and
   Abs_lst ("[_]\<^bsub>list\<^esub>._") and
   Abs_dist ("[_]\<^bsub>#list\<^esub>._") and
   Abs_res ("[_]\<^bsub>res\<^esub>._") and
   Abs_print ("_\<^bsub>set\<^esub>._") and
   Cons ("_::_" [78,77] 73) and
-  supp_gen ("aux _" [1000] 10) and
+  supp_set ("aux _" [1000] 10) and
   alpha_bn ("_ \<approx>bn _")
 
 consts alpha_trm ::'a
@@ -647,7 +647,7 @@
   %
   \begin{equation}\label{alphaset}
   \begin{array}{@ {\hspace{10mm}}r@ {\hspace{2mm}}l@ {\hspace{4mm}}r}
-  \multicolumn{3}{l}{@{term "(as, x) \<approx>gen R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
+  \multicolumn{3}{l}{@{term "(as, x) \<approx>set R fa p (bs, y)"}\hspace{2mm}@{text "\<equiv>"}}\\[1mm]
               & @{term "fa(x) - as = fa(y) - bs"} & \mbox{\it (i)}\\
   @{text "\<and>"} & @{term "(fa(x) - as) \<sharp>* p"} & \mbox{\it (ii)}\\
   @{text "\<and>"} & @{text "(p \<bullet> x) R y"} & \mbox{\it (iii)}\\
@@ -730,7 +730,7 @@
   types. For this we define 
   %
   \begin{equation}
-  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_gen (as, x) equal supp p (bs, x)"}
+  @{term "abs_set (as, x) (bs, x) \<equiv> \<exists>p. alpha_set (as, x) equal supp p (bs, x)"}
   \end{equation}
   
   \noindent
@@ -762,7 +762,7 @@
   The elements in these types will be, respectively, written as:
 
   \begin{center}
-  @{term "Abs as x"} \hspace{5mm} 
+  @{term "Abs_set as x"} \hspace{5mm} 
   @{term "Abs_res as x"} \hspace{5mm}
   @{term "Abs_lst as x"} 
   \end{center}
@@ -832,7 +832,7 @@
   function @{text aux}, taking an abstraction as argument:
   %
   \begin{center}
-  @{thm supp_gen.simps[THEN eq_reflection, no_vars]}
+  @{thm supp_set.simps[THEN eq_reflection, no_vars]}
   \end{center}
   
   \noindent
@@ -842,7 +842,7 @@
   This in turn means
   %
   \begin{center}
-  @{term "supp (supp_gen (Abs as x)) \<subseteq> supp (Abs as x)"}
+  @{term "supp (supp_gen (Abs_set as x)) \<subseteq> supp (Abs_set as x)"}
   \end{center}
 
   \noindent
@@ -860,7 +860,7 @@
   Theorem~\ref{suppabs}. 
 
   The method of first considering abstractions of the
-  form @{term "Abs as x"} etc is motivated by the fact that 
+  form @{term "Abs_set as x"} etc is motivated by the fact that 
   we can conveniently establish  at the Isabelle/HOL level
   properties about them.  It would be
   laborious to write custom ML-code that derives automatically such properties 
@@ -1489,7 +1489,7 @@
   lets us formally define the premise @{text P} for a non-empty binding clause as:
   %
   \begin{center}
-  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>gen R fa p (B', D')"}}\;.
+  \mbox{@{term "P \<equiv> \<exists>p. (B, D) \<approx>set R fa p (B', D')"}}\;.
   \end{center}
 
   \noindent
diff -r 1b31d514a087 -r cda25f9aa678 Paper/ROOT.ML
--- a/Paper/ROOT.ML	Mon Aug 30 15:59:50 2010 +0900
+++ b/Paper/ROOT.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -1,3 +1,3 @@
 quick_and_dirty := true;
-no_document use_thys ["LaTeXsugar", "../Nominal/NewParser"];
+no_document use_thys ["LaTeXsugar", "../Nominal/Nominal2"];
 use_thys ["Paper"];
\ No newline at end of file
diff -r 1b31d514a087 -r cda25f9aa678 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl-jv/Paper.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -1,9 +1,7 @@
 (*<*)
 theory Paper
 imports "../Nominal-General/Nominal2_Base" 
-        "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt"
-        "../Nominal-General/Nominal2_Supp" 
         "../Nominal-General/Atoms" 
         "LaTeXsugar"
 begin
@@ -44,6 +42,8 @@
 section {* Introduction *}
 
 text {*
+  TODO: write about supp of finite sets
+
   Nominal Isabelle provides a proving infratructure for
   convenient reasoning about programming languages. At its core Nominal
   Isabelle is based on the nominal logic work by Pitts at al
diff -r 1b31d514a087 -r cda25f9aa678 Pearl-jv/ROOT.ML
--- a/Pearl-jv/ROOT.ML	Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl-jv/ROOT.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -1,7 +1,5 @@
 no_document use_thys ["../Nominal-General/Nominal2_Base", 
-                      "../Nominal-General/Nominal2_Atoms", 
                       "../Nominal-General/Nominal2_Eqvt",
-                      "../Nominal-General/Nominal2_Supp",
                       "../Nominal-General/Atoms", 
                       "LaTeXsugar"];
 
diff -r 1b31d514a087 -r cda25f9aa678 Pearl/Paper.thy
--- a/Pearl/Paper.thy	Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl/Paper.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -1,7 +1,6 @@
 (*<*)
 theory Paper
 imports "../Nominal-General/Nominal2_Base" 
-        "../Nominal-General/Nominal2_Atoms" 
         "../Nominal-General/Nominal2_Eqvt" 
         "../Nominal-General/Atoms" 
         "LaTeXsugar"
diff -r 1b31d514a087 -r cda25f9aa678 Pearl/ROOT.ML
--- a/Pearl/ROOT.ML	Mon Aug 30 15:59:50 2010 +0900
+++ b/Pearl/ROOT.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -1,5 +1,4 @@
 no_document use_thys ["../Nominal-General/Nominal2_Base", 
-                      "../Nominal-General/Nominal2_Atoms", 
                       "../Nominal-General/Nominal2_Eqvt",
                       "../Nominal-General/Atoms", 
                       "LaTeXsugar"];
diff -r 1b31d514a087 -r cda25f9aa678 Slides/ROOT4.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/ROOT4.ML	Sat Sep 04 14:26:09 2010 +0800
@@ -0,0 +1,6 @@
+show_question_marks := false;
+quick_and_dirty := true;
+
+no_document use_thy "LaTeXsugar";
+
+use_thy "Slides4"
\ No newline at end of file
diff -r 1b31d514a087 -r cda25f9aa678 Slides/Slides4.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides4.thy	Sat Sep 04 14:26:09 2010 +0800
@@ -0,0 +1,1133 @@
+(*<*)
+theory Slides4
+imports "LaTeXsugar" "Nominal"
+begin
+
+notation (latex output)
+  set ("_") and
+  Cons  ("_::/_" [66,65] 65) 
+
+(*>*)
+
+text_raw {*
+  \renewcommand{\slidecaption}{Nanjing, 31.~August 2010}
+
+  \newcommand{\abst}[2]{#1.#2}% atom-abstraction
+  \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
+  \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
+  \newcommand{\unit}{\langle\rangle}% unit
+  \newcommand{\app}[2]{#1\,#2}% application
+  \newcommand{\eqprob}{\mathrel{{\approx}?}}
+  \newcommand{\freshprob}{\mathrel{\#?}}
+  \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
+  \newcommand{\id}{\varepsilon}% identity substitution
+  
+  \newcommand{\bl}[1]{\textcolor{blue}{#1}}
+  \newcommand{\gr}[1]{\textcolor{gray}{#1}}
+  \newcommand{\rd}[1]{\textcolor{red}{#1}}
+
+  \newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}
+  \newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}
+  \newcommand{\largenotok}{\includegraphics[scale=1]{notok.png}}
+
+  \renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}
+  \newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}
+  \newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}
+  \newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}
+
+  \newcommand{\LL}{$\mathbb{L}\,$}
+
+
+  \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
+  {rgb(0mm)=(0,0,0.9);
+  rgb(0.9mm)=(0,0,0.7);
+  rgb(1.3mm)=(0,0,0.5);
+  rgb(1.4mm)=(1,1,1)}
+
+  \def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}
+    \usebeamercolor[fg]{subitem projected}
+    {\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}
+    \pgftext{%
+      \usebeamerfont*{subitem projected}}
+  \end{pgfpicture}}
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[t]
+  \frametitle{%
+  \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
+  \\
+  \huge Error-Free Programming\\[-1mm] 
+  \huge with Theorem Provers\\[5mm]
+  \end{tabular}}
+  \begin{center}
+  Christian Urban
+  \end{center}
+  \begin{center}
+  \small Technical University of Munich, Germany\\[7mm]
+
+  \small in Nanjing on the kind invitation of\\ Professor Xingyuan Zhang
+  and his group
+  \end{center}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{My Background}
+
+  \begin{itemize}
+  \item researcher in Theoretical Computer Science\medskip
+
+  \item programmer on a \alert<2->{software system} with 800 kloc (though I am 
+  responsible only for 35 kloc)
+  \end{itemize}
+
+  \only<2->{
+  \begin{textblock}{6}(2,11)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\color{darkgray}
+  \begin{minipage}{4cm}\raggedright
+  A theorem prover called {\bf Isabelle}.
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  
+  \only<3>{
+  \begin{textblock}{6}(9,11)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\color{darkgray}
+  \begin{minipage}{4cm}\raggedright
+  Like every other code, this code is very hard to 
+  get correct.
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{Regular Expressions}
+
+  An example many (should) know about:\\ 
+  \rd{\bf Regular Expressions:} 
+
+  \only<2>{
+  \begin{center}
+  \bl{[] $\;\;\;|\;\;\;$ c $\;\;\;|\;\;\;$  r$_1$$|$r$_2$  $\;\;\;|\;\;\;$  
+   r$_1$$\cdot$r$_2$ $\;\;\;|\;\;\;$ r$^*$}
+  \end{center}}
+  \only<3->{
+  \begin{center}
+  \begin{tabular}{@ {}rrll@ {}}
+  \bl{r} & \bl{$::=$}  & \bl{NULL}            & \gr{(matches no string)}\\ 
+         & \bl{$\mid$} & \bl{EMPTY}           & \gr{(matches the empty string, [])}\\ 
+         & \bl{$\mid$} & \bl{CHR c}           & \gr{(matches the character c)}\\ 
+         & \bl{$\mid$} & \bl{ALT r$_1$ r$_2$} & \gr{(alternative, r$_1 |\,$r$_2$)}\\ 
+         & \bl{$\mid$} & \bl{SEQ r$_1$ r$_2$} & \gr{(sequential, r$_1\cdot\,$r$_2$)}\\ 
+         & \bl{$\mid$} & \bl{STAR r}          & \gr{(repeat, r$^*$)}\\
+  \end{tabular}
+  \end{center}\medskip}
+
+  \small
+  \begin{textblock}{14.5}(1,12.5)
+  \only<2->{\gr{(a$\cdot$b)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm} \{[], ab, abab, ababab, \ldots\}}\\}
+  \only<2->{\gr{x$\cdot$(0 $|$ 1 $|$ 2  \ldots  8 $|$ 9)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm} 
+  \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}}
+  \end{textblock}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{RegExp Matcher}
+
+  Let's implement a regular expression matcher:\bigskip
+
+  \begin{center}
+  \begin{tikzpicture}
+  %%\draw[help lines, black] (-3,0) grid (6,3);
+  
+  \draw[line width=1mm, red] (0.0,0.0) rectangle (4,2.3);
+  \node[anchor=base] at (2,1) 
+     {\small\begin{tabular}{@ {}c@ {}}\Large\bf Regular\\ 
+                                      \Large\bf Expression \\ 
+                                      \Large\bf Matcher\end{tabular}};
+  
+  \coordinate (m1) at (0,1.5);
+  \draw (-2,2) node (m2) {\small\begin{tabular}{c}\bl{regular}\\[-1mm] \bl{expression}\end{tabular}};
+  \path[overlay, ->, line width = 1mm, shorten <=-3mm] (m2) edge (m1);
+  
+  \coordinate (s1) at (0,0.5);
+  \draw (-1.8,-0) node (s2) {\small\begin{tabular}{c}\bl{string}\end{tabular}};
+  \path[overlay, ->, line width = 1mm, shorten <=-3mm] (s2) edge (s1);
+
+  \coordinate (r1) at (4,1.2);
+  \draw (6,1.2) node (r2) {\small\begin{tabular}{c}\bl{true}, \bl{false}\end{tabular}};
+  \path[overlay, ->, line width = 1mm, shorten >=-3mm] (r1) edge (r2);
+
+  \end{tikzpicture}
+  \end{center}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{RegExp Matcher}
+  \small
+
+  {\bf input:} a \underline{list} of RegExps and a string \hspace{6mm}{\bf output:} true or false
+
+  \only<2->{
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+  \bl{match [] []}                   & \bl{$=$} & \bl{true}\\
+  \bl{match [] \_}                   & \bl{$=$} & \bl{false}\\
+  \bl{match (NULL::rs) s}            & \bl{$=$} & \bl{false}\\
+  \bl{match (EMPTY::rs) s}           & \bl{$=$} & \bl{match rs s}\\
+  \bl{match (CHR c::rs) (c::s)}      & \bl{$=$} & \bl{match rs s}\\         
+  \bl{match (CHR c::rs) \_}          & \bl{$=$} & \bl{false}\\    
+  \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\
+                                     &          & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\ 
+  \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
+  \bl{match (STAR r::rs) s}          & \bl{$=$} & \bl{match rs s}\\
+                                     &          & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+  \end{tabular}
+  \end{center}}
+
+  \onslide<3->{we start the program with\\
+  \hspace{6mm}\bl{matches r s $=$ match [r] s}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{Program in Scala}
+
+  \bl{\footnotesize
+  \begin{tabular}{l}
+  sealed abstract class Rexp\\ 
+  sealed case class Null extends Rexp\\
+  sealed case class Empty extends Rexp\\
+  sealed case class Chr(c: Char) extends Rexp\\
+  sealed case class Alt(r1 : Rexp, r2 : Rexp) extends Rexp\\
+  sealed case class Seq(r1 : Rexp, r2 : Rexp) extends Rexp\\
+  sealed case class Star(r : Rexp) extends Rexp\medskip\\
+  def match1 (rs : List[Rexp], s : List[Char]) : Boolean = rs match \{\\
+  \hspace{3mm}case Nil @{text "\<Rightarrow>"} if (s == Nil) true else false\\
+  \hspace{3mm}case (Null()::rs) @{text "\<Rightarrow>"} false\\
+  \hspace{3mm}case (Empty()::rs) @{text "\<Rightarrow>"} match1 (rs, s)\\
+  \hspace{3mm}case (Chr(c)::rs) @{text "\<Rightarrow>"} s match \\
+  \hspace{6mm}\{ case Nil @{text "\<Rightarrow>"} false\\
+  \hspace{8mm}case (d::s) @{text "\<Rightarrow>"} if (c==d) match1 (rs,s) else false \}\\
+  \hspace{3mm}case (Alt (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::rs, s) || match1 (r2::rs, s)\\
+  \hspace{3mm}case (Seq (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::r2::rs, s) \\
+  \hspace{3mm}case (Star (r)::rs) @{text "\<Rightarrow>"} match1 (r::rs, s) || match1 (r::Star (r)::rs, s)\\
+  \}
+  \end{tabular}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Testing}
+  
+  \small
+  Every good programmer should do thourough tests: 
+
+
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-20mm}}lcl}
+  \bl{matches (a$\cdot$b)$^*\;$ []}     & \bl{$\mapsto$} & \bl{true}\\
+  \bl{matches (a$\cdot$b)$^*\;$ ab}   & \bl{$\mapsto$} & \bl{true}\\ 
+  \bl{matches (a$\cdot$b)$^*\;$ aba}  & \bl{$\mapsto$} & \bl{false}\\
+  \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ 
+  \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
+  \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x}   & \bl{$\mapsto$} & \bl{true}}\\
+  \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x0}  & \bl{$\mapsto$} & \bl{true}}\\
+  \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}}
+  \end{tabular}
+  \end{center}
+ 
+  \onslide<3->
+  {looks OK \ldots let's ship it to customers\hspace{5mm} 
+   \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{Testing}
+
+  \begin{itemize}
+  \item While testing is an important part in the process of programming development\pause
+
+  \item we can only test a {\bf finite} amount of examples\bigskip\pause
+
+  \begin{center}
+  \colorbox{cream}
+  {\gr{\begin{minipage}{10cm}
+  ``Testing can only show the presence of errors, never their
+  absence'' (Edsger W.~Dijkstra)
+  \end{minipage}}}
+  \end{center}\bigskip\pause
+
+  \item In a theorem prover we can establish properties that apply to 
+  {\bf all} input and {\bf all} output.\pause 
+
+  \item For example we can establish that the matcher terminates 
+  on all input.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{RegExp Matcher}
+
+  \small
+  We need to find a measure that gets smaller in each recursive call.\bigskip
+
+  \onslide<1->{
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-9mm}}l@ {}}
+  \bl{match [] []}                   & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+  \bl{match [] \_}                   & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+  \bl{match (NULL::rs) s}            & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+  \bl{match (EMPTY::rs) s}           & \bl{$=$} & \bl{match rs s} & \onslide<3->{\ok}\\
+  \bl{match (CHR c::rs) (c::s)}      & \bl{$=$} & \bl{match rs s} & \onslide<4->{\ok}\\         
+  \bl{match (CHR c::rs) \_}          & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\    
+  \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s} & \onslide<5->{\ok}\\
+                                     &          & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\ 
+  \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s} & \onslide<6->{\ok}\\
+  \bl{match (STAR r::rs) s}          & \bl{$=$} & \bl{match rs s} & \onslide<7->{\notok}\\
+                                     &          & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+  \end{tabular}
+  \end{center}}
+
+
+  \begin{textblock}{5}(4,4)
+  \begin{tikzpicture}
+  %%\draw[help lines, black] (-3,0) grid (6,3);
+  
+  \coordinate (m1) at (-2,0);
+  \coordinate (m2) at ( 2,0);
+  \path[overlay, ->, line width = 0.6mm, color = red] (m1) edge (m2);
+  \draw (0,0) node[above=-1mm] {\footnotesize\rd{needs to get smaller}};
+  \end{tikzpicture}
+  \end{textblock}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Bug Hunting}
+
+  \only<1>{Several hours later\ldots}\pause
+
+
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-20mm}}lcl}
+  \bl{matches (STAR (EMPTY)) s}     & \bl{$\mapsto$} & loops\\
+  \onslide<4->{\bl{matches (STAR (EMPTY $|$ \ldots)) s}   & \bl{$\mapsto$} & loops\\} 
+  \end{tabular}
+  \end{center}
+
+  \small
+  \onslide<3->{
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+  \ldots\\
+  \bl{match (EMPTY::rs) s}           & \bl{$=$} & \bl{match rs s}\\
+  \ldots\\
+  \bl{match (STAR r::rs) s}          & \bl{$=$} & \bl{match rs s}\\
+                                     &          & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+  \end{tabular}
+  \end{center}}
+  
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{RegExp Matcher}
+  \small
+
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+  \bl{match [] []}                   & \bl{$=$} & \bl{true}\\
+  \bl{match [] \_}                   & \bl{$=$} & \bl{false}\\
+  \bl{match (NULL::rs) s}            & \bl{$=$} & \bl{false}\\
+  \bl{match (EMPTY::rs) s}           & \bl{$=$} & \bl{match rs s}\\
+  \bl{match (CHR c::rs) (c::s)}      & \bl{$=$} & \bl{match rs s}\\         
+  \bl{match (CHR c::rs) \_}          & \bl{$=$} & \bl{false}\\    
+  \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\
+                                     &          & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\ 
+  \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
+  \bl{match (STAR r::rs) s}          & \bl{$=$} & \bl{match rs s}\\
+                                     &          & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+  \end{tabular}
+  \end{center}
+
+  \only<1>{
+  \begin{textblock}{5}(4,4)
+  \largenotok
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{Second Attempt}
+
+  Can a regular expression match the empty string?
+
+  \small
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
+  \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+  \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  & \onslide<2->{\ok}\\
+  \bl{nullable (CHR c)}           & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\         
+  \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)}
+    & \onslide<2->{\ok}\\ 
+  \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)}
+    & \onslide<2->{\ok}\\ 
+  \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+  \end{tabular}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{RegExp Matcher 2}
+
+  If \bl{r} matches \bl{c::s}, which regular expression can match the string \bl{s}?
+
+  \small
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+  \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\
+  \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\
+  \bl{der c (CHR d)}           & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \onslide<3->{\ok}\\
+  \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \onslide<3->{\ok}\\ 
+  \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \onslide<3->{\ok}\\
+       &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
+  \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} & \onslide<3->{\ok}\medskip\\
+  \pause
+
+  \bl{derivative r []}     & \bl{$=$} & \bl{r} & \onslide<3->{\ok}\\
+  \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \onslide<3->{\ok}\\
+  \end{tabular}
+  \end{center}
+
+  we call the program with\\
+  \bl{matches r s $=$ nullable (derivative r s)}
+  
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{But Now What?}
+
+  \begin{center}
+  {\usefont{T1}{ptm}{b}{N}\VERYHuge{\rd{?}}}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Testing}
+  
+  \small
+
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-20mm}}lcl}
+  \bl{matches []$^*$ []} & \bl{$\mapsto$} & \bl{true}\\
+  \bl{matches ([]$|$a)$^*$ a}  & \bl{$\mapsto$} & \bl{true}\medskip\\
+
+  \bl{matches (a$\cdot$b)$^*\;$ []}     & \bl{$\mapsto$} & \bl{true}\\
+  \bl{matches (a$\cdot$b)$^*\;$ ab}   & \bl{$\mapsto$} & \bl{true}\\ 
+  \bl{matches (a$\cdot$b)$^*\;$ aba}  & \bl{$\mapsto$} & \bl{false}\\
+  \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\ 
+  \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
+  
+  \bl{matches x$\cdot$(0$|$1)$^*\;$ x}   & \bl{$\mapsto$} & \bl{true}\\
+  \bl{matches x$\cdot$(0$|$1)$^*\;$ x0}  & \bl{$\mapsto$} & \bl{true}\\
+  \bl{matches x$\cdot$(0$|$1)$^*\;$ x3}  & \bl{$\mapsto$} & \bl{false}
+  \end{tabular}
+  \end{center}
+ 
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{Specification}
+
+  We have to specify what it means for a regular expression to match
+  a string. 
+  %
+  \only<2>{
+  \mbox{}\\[8mm]
+  \bl{(a$\cdot$b)$^*$}\\ 
+  \hspace{7mm}\bl{$\mapsto$\hspace{3mm}\{[], ab, abab, ababab, \ldots\}}\bigskip\\
+  \bl{x$\cdot$(0 $|$ 1 $|$ 2  \ldots  8 $|$ 9 )$^*$}\\ 
+  \hspace{7mm}\bl{$\mapsto$\hspace{3mm} 
+  \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}}
+  %
+  \only<3->{
+  \begin{center}
+  \begin{tabular}{rcl}
+  \bl{\LL (NULL)}            & \bl{$\dn$} & \bl{\{\}}\\
+  \bl{\LL (EMPTY)}           & \bl{$\dn$} & \bl{\{[]\}}\\
+  \bl{\LL (CHR c)}           & \bl{$\dn$} & \bl{\{c\}}\\
+  \bl{\LL (ALT r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<4->{\bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}}\\
+  \bl{\LL (SEQ r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<6->{\bl{\LL (r$_1$) ; \LL (r$_2$)}}\\
+  \bl{\LL (STAR r)}          & \bl{$\dn$} & \onslide<8->{\bl{(\LL (r))$^\star$}}\\
+  \end{tabular}
+  \end{center}}
+
+  \only<5-6>{
+  \begin{textblock}{6}(2.9,13.3)
+  \colorbox{cream}{\bl{S$_1$ ; S$_2$ $\;\dn\;$ \{ s$_1$@s$_2$ $|$ s$_1$$\in$S$_1$ $\wedge$
+                                                          s$_2$$\in$S$_2$ \}}}
+  \end{textblock}}
+
+  \only<7->{
+  \begin{textblock}{9}(4,13)
+  \colorbox{cream}{\bl{$\infer{\mbox{[]} \in \mbox{S}^\star}{}$}}\hspace{3mm}
+  \colorbox{cream}{\bl{$\infer{\mbox{s}_1\mbox{@}\mbox{s}_2 \in \mbox{S}^\star}
+                      {\mbox{s}_1 \in \mbox{S} & \mbox{s}_2 \in \mbox{S}^\star}$}}
+  \end{textblock}}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{Is the Matcher Error-Free?}
+
+  We expect that
+
+  \begin{center}
+  \begin{tabular}{lcl}
+  \bl{matches r s = true}  & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}% 
+  \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\
+  \bl{matches r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
+  \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
+  \end{tabular}
+  \end{center}
+  \pause\pause\bigskip
+  By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
+
+  \begin{tabular}{lrcl}
+  Lemmas:  & \bl{nullable (r)}          & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
+           & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
+  \end{tabular}
+  
+  \only<4->{
+  \begin{textblock}{3}(0.9,4.5)
+  \rd{\huge$\forall$\large{}r s.}
+  \end{textblock}}
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+
+  \mbox{}\\[-2mm]
+
+  \small
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
+  \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} &\\
+  \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  &\\
+  \bl{nullable (CHR c)}           & \bl{$=$} & \bl{false} &\\
+  \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\ 
+  \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\
+  \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \\
+  \end{tabular}\medskip
+
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+  \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \\
+  \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \\
+  \bl{der c (CHR d)}           & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\
+  \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
+  \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
+       &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
+  \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\
+
+  \bl{derivative r []}     & \bl{$=$} & \bl{r} & \\
+  \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
+  \end{tabular}\medskip
+
+  \bl{matches r s $=$ nullable (derivative r s)}
+  
+  \only<2>{
+  \begin{textblock}{8}(1.5,4)
+  \includegraphics[scale=0.3]{approved.png}
+  \end{textblock}}
+  
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Interlude: TCB}
+
+  \begin{itemize}
+  \item The \alert{\bf Trusted Code Base} (TCB) is the code that can make your 
+  program behave in unintended ways (i.e.~cause bugs).\medskip
+
+  \item Typically the TCB includes: CPUs, operating systems, C-libraries,
+  device drivers, (J)VMs\ldots\bigskip
+  \pause
+
+  \item It also includes the compiler.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-3>
+  \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers 
+  \end{tabular}}
+  
+  %Why is it so paramount to have a small trusted code base (TCB)?
+  \bigskip\bigskip
+
+  \begin{columns}
+  \begin{column}{2.7cm}
+  \begin{minipage}{2.5cm}%
+  \begin{tabular}{c@ {}}
+  \includegraphics[scale=0.2]{ken-thompson.jpg}\\[-1.8mm]
+  \footnotesize Ken Thompson\\[-1.8mm]
+  \footnotesize Turing Award, 1983\\
+  \end{tabular}
+  \end{minipage}
+  \end{column}
+  \begin{column}{9cm}
+  \begin{tabular}{l@ {\hspace{1mm}}p{8cm}}
+  \myitemi
+  & Ken Thompson showed how to hide a Trojan Horse in a 
+  compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]
+  \myitemi
+  & No amount of source level verification will protect 
+  you from such Thompson-hacks.\\[2mm]
+
+  \myitemi
+  & Therefore in safety-critical systems it is important to rely 
+  on only a very small TCB.
+  \end{tabular}
+  \end{column}
+  \end{columns}
+
+  \only<2>{
+  \begin{textblock}{6}(4,2)
+  \begin{tikzpicture}
+  \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
+  {\normalsize
+  \begin{minipage}{8cm}
+  \begin{quote}
+  \includegraphics[scale=0.05]{evil.png}
+  \begin{enumerate}
+  \item[1)] Assume you ship the compiler as binary and also with sources.
+  \item[2)] Make the compiler aware when it compiles itself.
+  \item[3)] Add the Trojan horse.
+  \item[4)] Compile.
+  \item[5)] Delete Trojan horse from the sources of the compiler.
+  \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}
+  \end{enumerate}
+  \end{quote}
+  \end{minipage}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{\LARGE\begin{tabular}{c}An Example: Small TCB for\\[-2mm] 
+  A Critical Infrastructure\end{tabular}}
+  \mbox{}\\[-14mm]\mbox{}
+
+  \begin{columns}
+  \begin{column}{0.2\textwidth}
+  \begin{tabular}{@ {} c@ {}}
+  \includegraphics[scale=0.3]{appel.jpg}\\[-2mm] 
+  {\footnotesize Andrew Appel}\\[-2.5mm]
+  {\footnotesize (Princeton)}
+  \end{tabular}
+  \end{column}
+  
+  \begin{column}{0.8\textwidth}
+  \begin{textblock}{10}(4.5,3.95)
+  \begin{block}{Proof-Carrying Code}
+  \begin{center}
+  \begin{tikzpicture}
+  \draw[help lines,cream] (0,0.2) grid (8,4);
+  
+  \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
+  \node[anchor=base] at (6.5,2.8) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  user needs to run untrusted code\end{tabular}};
+
+  \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
+  \node[anchor=base] at (1.5,2.3) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering  code developer/ web server/ Apple 
+  Store\end{tabular}};
+  
+  \onslide<4->{
+  \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
+  \node[anchor=base,white] at (6.5,1.1) 
+     {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
+
+  \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
+  \onslide<3->{
+  \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};
+  \node at (3.8,1.9) {\small certificate};
+  }
+
+  \onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}
+  % Code Developer
+  % User (runs untrusted code)
+  % transmits a proof that the code is safe
+  % 
+  \end{tikzpicture}
+  \end{center}
+  \end{block}
+  \end{textblock}
+  \end{column}
+  \end{columns}
+  
+  \small\mbox{}\\[2.5cm]
+  \begin{itemize}
+  \item<4-> TCB of the checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions; 
+  803 loc in C including 2 library functions)\\[-3mm]
+  \item<5-> 167 loc in C implement a type-checker
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+
+text {*
+  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
+                     draw=black!50, top color=white, bottom color=black!20]
+  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
+                     draw=red!70, top color=white, bottom color=red!50!black!20]
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[squeeze]
+  \frametitle{Type-Checking in LF} 
+  
+  \begin{columns}
+  \begin{column}{0.2\textwidth}
+  \begin{tabular}{@ {\hspace{-4mm}}c@ {}}
+  \\[-4mm]
+  \includegraphics[scale=0.1]{harper.jpg}\\[-2mm] 
+  {\footnotesize Bob Harper}\\[-2.5mm]
+  {\footnotesize (CMU)}\\[2mm]
+
+  \includegraphics[scale=0.3]{pfenning.jpg}\\[-2mm] 
+  {\footnotesize Frank Pfenning}\\[-2.5mm]
+  {\footnotesize (CMU)}\\[2mm]
+
+  \onslide<-6>{
+  {\footnotesize 31 pages in }\\[-2.5mm]
+  {\footnotesize ACM Transact.~on}\\[-2.5mm]
+  {\footnotesize Comp.~Logic.,~2005}\\}
+  \end{tabular}
+  \end{column}
+
+  \begin{column}{0.8\textwidth}
+  \begin{textblock}{0}(3.1,2)
+
+  \begin{tikzpicture}
+  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+  { \&[-10mm] 
+    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+    \node (proof1) [node1] {\large Proof}; \&
+    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+    
+    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&
+    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+     
+    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\
+
+    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+  };
+
+  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+  
+  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+
+  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+  
+  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+
+  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
+  \end{tikzpicture}
+
+  \end{textblock}
+  \end{column}
+  \end{columns}
+
+  \only<2>{%
+  \begin{textblock}{2}(.1,12.85)
+  \begin{tikzpicture}
+  \draw[line width=1mm, red] (0,0) ellipse (1.5cm and 0.88cm);
+  \end{tikzpicture}
+  \end{textblock}
+  }
+
+  \begin{textblock}{3}(14,3.6)
+  \onslide<4->{
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \only<7->{
+  \begin{textblock}{14}(0.6,12.8)
+  \begin{block}{}
+  \small Each time one needs to check $\sim$31pp~of informal paper proofs.
+  You have to be able to keep definitions and proofs consistent.
+  \end{block}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{Theorem Provers}
+
+  \begin{itemize}
+  \item Theorem provers help with keeping large proofs consistent;
+  make them modifiable.\medskip
+  
+  \item They can ensure that all cases are covered.\medskip
+
+  \item Sometimes, tedious reasoning can be automated.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{Theorem Provers}
+
+  \begin{itemize}
+  \item You also pay a (sometimes heavy) price: reasoning can be much, much harder.\medskip
+
+  \item Depending on your domain, suitable reasoning infrastructure
+  might not yet be available.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{Theorem Provers}
+
+  Recently impressive work has been accomplished proving the correctness
+
+  \begin{itemize}
+  \item of a compiler for C-light (compiled code has the same observable
+  behaviour as the original source code),\medskip
+
+  \item a mirco-kernel operating system (absence of certain 
+  bugs\ldots no nil pointers, no buffer overflows).
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{Trust in Theorem Provers}
+
+  \begin{center}
+  Why should we trust theorem provers? 
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{Theorem Provers}
+  
+   \begin{itemize}
+  \item Theorem provers are a \textcolor{red}{special kind} of software.
+  
+  \item We do \textcolor{red}{\bf not} need to trust them; we only need to trust:
+  \end{itemize}
+
+  \begin{quote}
+  \begin{itemize}
+  \item The logic they are based on \textcolor{gray}{(e.g.~HOL)}, and\smallskip
+  \item a proof checker that checks the proofs
+  \textcolor{gray}{(this can be a very small program)}.\smallskip\pause
+  \item To a little extend, we also need to trust our definitions
+  \textcolor{gray}{(this can be mitigated)}.
+  \end{itemize}
+  \end{quote}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{Isabelle}
+  
+  \begin{itemize}
+  \item I am using the Isabelle theorem prover (development since 1990).\bigskip\bigskip\bigskip
+  
+  \item It follows the LCF-approach:
+  
+  \begin{itemize}
+  \item Have a special abstract type \alert{\bf thm}.
+  \item Make the constructors of this abstract type the inference rules 
+  of your logic.
+  \item Implement the theorem prover in a strongly-typed language (e.g.~ML).
+  \end{itemize}
+
+  $\Rightarrow$ everything of type {\bf thm} has been proved (even if we do not
+  have to explicitly generate proofs).
+  \end{itemize}
+  
+  \only<1>{
+  \begin{textblock}{5}(11,2.3)
+  \begin{center}
+  \includegraphics[scale=0.18]{robin-milner.jpg}\\[-0.8mm]
+  \footnotesize Robin Milner\\[-0.8mm]
+  \footnotesize Turing Award, 1991\\
+  \end{center}
+  \end{textblock}}
+
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{
+  \begin{tabular}{c}
+  \mbox{}\\[23mm]
+  \LARGE Demo
+  \end{tabular}}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Future Research}
+  
+  \begin{itemize}
+  \item Make theorem provers more like a programming environment.\medskip\pause 
+
+  \item Use all the computational power we get from the hardware to
+  automate reasoning (GPUs).\medskip\pause
+
+  \item Provide a comprehensive reasoning infrastructure for many domains and 
+  design automated decision procedures. 
+  \end{itemize}\pause
+
+  
+  \begin{center}
+  \colorbox{cream}{
+  \begin{minipage}{10cm} 
+  \color{gray}
+  \small
+  ``Formal methods will never have a significant impact until
+   they can be used by people that don't understand them.''\smallskip\\
+  \mbox{}\footnotesize\hfill attributed to Tom Melham
+  \end{minipage}}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{Conclusion}
+  
+  \begin{itemize}
+  \item The plan is to make this kind of programming the ``future''.\medskip\pause
+
+  \item Though the technology is already there\\ (compiler + micro-kernel os).\medskip\pause
+
+  \item Logic and reasoning (especially induction) are important skills for 
+  Computer Scientists.
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[c]
+  \frametitle{
+  \begin{tabular}{c}
+  \mbox{}\\[23mm]
+  \alert{\LARGE Thank you very much!}\\
+  \alert{\Large Questions?}
+  \end{tabular}}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+(*<*)
+end
+(*>*)
\ No newline at end of file