# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1285676507 14400
# Node ID 93a73eabbffc8ae359c8243bb4a715ec6821c1f3
# Parent  11133eb76f61a524f47bd31ddd1e36ce39a10bfd# Parent  1c18f2cf39238301749d1a329a07707e7307170d
merged

diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/Abs.thy
--- a/Nominal/Abs.thy	Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Abs.thy	Tue Sep 28 08:21:47 2010 -0400
@@ -293,7 +293,13 @@
   unfolding fun_rel_def
   by (auto intro: alphas_abs_eqvt simp only: Pair_eqvt)
 
-lemma abs_exhausts:
+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)
+
+lemma Abs_exhausts:
   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"
@@ -301,12 +307,6 @@
               prod.exhaust[where 'a="atom set" and 'b="'a"]
               prod.exhaust[where 'a="atom list" and 'b="'a"])
 
-lemma abs_eq_iff:
-  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_set :: (pt) pt
 begin
 
@@ -315,14 +315,14 @@
 is
   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"
 
-lemma permute_Abs[simp]:
+lemma permute_Abs_set[simp]:
   fixes x::"'a::pt"  
   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
   apply(default)
-  apply(case_tac [!] x rule: abs_exhausts(1))
+  apply(case_tac [!] x rule: Abs_exhausts(1))
   apply(simp_all)
   done
 
@@ -343,7 +343,7 @@
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: abs_exhausts(2))
+  apply(case_tac [!] x rule: Abs_exhausts(2))
   apply(simp_all)
   done
 
@@ -364,22 +364,21 @@
 
 instance
   apply(default)
-  apply(case_tac [!] x rule: abs_exhausts(3))
+  apply(case_tac [!] x rule: Abs_exhausts(3))
   apply(simp_all)
   done
 
 end
 
-lemmas permute_abs[eqvt] = permute_Abs permute_Abs_res permute_Abs_lst
+lemmas permute_Abs[eqvt] = permute_Abs_set permute_Abs_res permute_Abs_lst
 
 
-lemma abs_swap1:
+lemma Abs_swap1:
   assumes a1: "a \<notin> (supp x) - bs"
   and     a2: "b \<notin> (supp x) - bs"
   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
+  unfolding Abs_eq_iff
   unfolding alphas
   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] 
   unfolding fresh_star_def fresh_def
@@ -388,12 +387,11 @@
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
      (auto simp add: supp_perm swap_atom)
 
-lemma abs_swap2:
+lemma Abs_swap2:
   assumes a1: "a \<notin> (supp x) - (set bs)"
   and     a2: "b \<notin> (supp x) - (set bs)"
   shows "Abs_lst bs x = Abs_lst ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x)"
-  unfolding abs_eq_iff
-  unfolding alphas_abs
+  unfolding Abs_eq_iff
   unfolding alphas
   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric] set_eqvt[symmetric]
   unfolding fresh_star_def fresh_def
@@ -402,21 +400,21 @@
   by (rule_tac [!] x="(a \<rightleftharpoons> b)" in exI)
      (auto simp add: supp_perm swap_atom)
 
-lemma abs_supports:
+lemma Abs_supports:
   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
-  unfolding permute_abs
-  by (simp_all add: abs_swap1[symmetric] abs_swap2[symmetric])
+  unfolding permute_Abs
+  by (simp_all add: Abs_swap1[symmetric] Abs_swap2[symmetric])
 
 function
   supp_set  :: "('a::pt) abs_set \<Rightarrow> atom set"
 where
   "supp_set (Abs_set as x) = supp x - as"
-apply(case_tac x rule: abs_exhausts(1))
+apply(case_tac x rule: Abs_exhausts(1))
 apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_set 
@@ -426,9 +424,9 @@
   supp_res :: "('a::pt) abs_res \<Rightarrow> atom set"
 where
   "supp_res (Abs_res as x) = supp x - as"
-apply(case_tac x rule: abs_exhausts(2))
+apply(case_tac x rule: Abs_exhausts(2))
 apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_res 
@@ -438,9 +436,9 @@
   supp_lst :: "('a::pt) abs_lst \<Rightarrow> atom set"
 where
   "supp_lst (Abs_lst cs x) = (supp x) - (set cs)"
-apply(case_tac x rule: abs_exhausts(3))
+apply(case_tac x rule: Abs_exhausts(3))
 apply(simp)
-apply(simp add: abs_eq_iff alphas_abs alphas)
+apply(simp add: Abs_eq_iff alphas_abs alphas)
 done
 
 termination supp_lst 
@@ -450,86 +448,88 @@
   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))
+  apply(case_tac x rule: Abs_exhausts(1))
   apply(simp add: supp_eqvt Diff_eqvt)
-  apply(case_tac y rule: abs_exhausts(2))
+  apply(case_tac y rule: Abs_exhausts(2))
   apply(simp add: supp_eqvt Diff_eqvt)
-  apply(case_tac z rule: abs_exhausts(3))
+  apply(case_tac z rule: Abs_exhausts(3))
   apply(simp add: supp_eqvt Diff_eqvt set_eqvt)
   done
 
-lemma aux_fresh:
+lemma Abs_fresh_aux:
   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 only: eqvts_raw)
 
-lemma supp_abs_subset1:
+lemma Abs_supp_subset1:
   assumes a: "finite (supp 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
-  by (auto dest!: aux_fresh)
+  by (auto dest!: Abs_fresh_aux)
      (simp_all add: fresh_def supp_finite_atom_set a)
 
-lemma supp_abs_subset2:
+lemma Abs_supp_subset2:
   assumes a: "finite (supp x)"
   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)
-     (simp_all add: abs_supports a)
+     (simp_all add: Abs_supports a)
 
-lemma abs_finite_supp:
+lemma Abs_finite_supp:
   assumes a: "finite (supp x)"
   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)
-     (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a])
+     (simp_all add: Abs_supp_subset1[OF a] Abs_supp_subset2[OF a])
 
-lemma supp_abs:
+lemma supp_Abs:
   fixes x::"'a::fs"
   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)
+  by (rule_tac [!] Abs_finite_supp)
      (simp_all add: finite_supp)
 
 instance abs_set :: (fs) fs
   apply(default)
-  apply(case_tac x rule: abs_exhausts(1))
-  apply(simp add: supp_abs finite_supp)
+  apply(case_tac x rule: Abs_exhausts(1))
+  apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_res :: (fs) fs
   apply(default)
-  apply(case_tac x rule: abs_exhausts(2))
-  apply(simp add: supp_abs finite_supp)
+  apply(case_tac x rule: Abs_exhausts(2))
+  apply(simp add: supp_Abs finite_supp)
   done
 
 instance abs_lst :: (fs) fs
   apply(default)
-  apply(case_tac x rule: abs_exhausts(3))
-  apply(simp add: supp_abs finite_supp)
+  apply(case_tac x rule: Abs_exhausts(3))
+  apply(simp add: supp_Abs finite_supp)
   done
 
-lemma abs_fresh_iff:
+lemma Abs_fresh_iff:
   fixes x::"'a::fs"
   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
+  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)
+lemma Abs_fresh_star:
+  fixes x::"'a::fs"
+  shows "as \<sharp>* Abs_set as x"
+  and   "as \<sharp>* Abs_res as x"
+  and   "set bs \<sharp>* Abs_lst bs x"
+  unfolding fresh_star_def
+  by(simp_all add: Abs_fresh_iff)
 
 
 section {* Infrastructure for building tuples of relations and functions *}
@@ -570,6 +570,16 @@
   unfolding prod_fv.simps
   by (perm_simp) (rule refl)
 
+lemma prod_fv_supp:
+  shows "prod_fv supp supp = supp"
+by (rule ext)
+   (auto simp add: prod_fv.simps supp_Pair)
+
+lemma prod_alpha_eq:
+  shows "prod_alpha (op=) (op=) = (op=)"
+unfolding prod_alpha_def
+by (auto intro!: ext)
+
 
 end
 
diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/Ex/Foo1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Foo1.thy	Tue Sep 28 08:21:47 2010 -0400
@@ -0,0 +1,49 @@
+theory Foo1
+imports "../Nominal2" 
+begin
+
+(* 
+  Contrived example that has more than one
+  binding function for a datatype
+*)
+
+atom_decl name
+
+nominal_datatype foo: trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"  bind x in t
+| Let1 a::"assg" t::"trm"  bind "bn1 a" in t
+| Let2 a::"assg" t::"trm"  bind "bn2 a" in t
+| Let3 a::"assg" t::"trm"  bind "bn3 a" in t
+and assg =
+  As "name" "name" "trm"
+binder
+  bn1::"assg \<Rightarrow> atom list" and
+  bn2::"assg \<Rightarrow> atom list" and
+  bn3::"assg \<Rightarrow> atom list"
+where
+  "bn1 (As x y t) = [atom x]"
+| "bn2 (As x y t) = [atom y]"
+| "bn3 (As x y t) = [atom x, atom y]"
+
+thm foo.distinct
+thm foo.induct
+thm foo.inducts
+thm foo.exhaust
+thm foo.fv_defs
+thm foo.bn_defs
+thm foo.perm_simps
+thm foo.eq_iff
+thm foo.fv_bn_eqvt
+thm foo.size_eqvt
+thm foo.supports
+thm foo.fsupp
+thm foo.supp
+thm foo.fresh
+
+
+end
+
+
+
diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/Ex/Let.thy
--- a/Nominal/Ex/Let.thy	Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Ex/Let.thy	Tue Sep 28 08:21:47 2010 -0400
@@ -2,41 +2,252 @@
 imports "../Nominal2" 
 begin
 
-text {* example 3 or example 5 from Terms.thy *}
-
 atom_decl name
 
-declare [[STEPS = 29]]
-
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
 | Lam x::"name" t::"trm"  bind  x in t
-| Let a::"lts" t::"trm"   bind "bn a" in t
-and lts =
-  Lnil
-| Lcons "name" "trm" "lts"
+| Let as::"assn" t::"trm"   bind "bn as" in t
+and assn =
+  ANil
+| ACons "name" "trm" "assn"
 binder
   bn
 where
-  "bn Lnil = []"
-| "bn (Lcons x t l) = (atom x) # (bn l)"
+  "bn ANil = []"
+| "bn (ACons x t as) = (atom x) # (bn as)"
+
+thm at_set_avoiding2
+thm trm_assn.fv_defs
+thm trm_assn.eq_iff 
+thm trm_assn.bn_defs
+thm trm_assn.perm_simps
+thm trm_assn.induct
+thm trm_assn.inducts
+thm trm_assn.distinct
+thm trm_assn.supp
+thm trm_assn.fresh
+
+
+lemma fin_bn:
+  shows "finite (set (bn l))"
+  apply(induct l rule: trm_assn.inducts(2))
+  apply(simp_all)
+  done
+
+primrec
+  permute_bn_raw
+where
+  "permute_bn_raw p (ANil_raw) = ANil_raw"
+| "permute_bn_raw p (ACons_raw a t l) = ACons_raw (p \<bullet> a) t (permute_bn_raw p l)"
+
+quotient_definition
+  "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
+is
+  "permute_bn_raw"
+
+lemma [quot_respect]: "((op =) ===> alpha_assn_raw ===> alpha_assn_raw) permute_bn_raw permute_bn_raw"
+  apply simp
+  apply clarify
+  apply (erule alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.inducts)
+  apply (rule TrueI)+
+  apply simp_all
+  apply (rule_tac [!] alpha_trm_raw_alpha_assn_raw_alpha_bn_raw.intros)
+  apply simp_all
+  done
+
+lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
+
+lemma uu:
+  shows "alpha_bn (permute_bn p as) as"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+apply(simp add: permute_bn)
+apply(simp add: trm_assn.eq_iff)
+done
+
+lemma tt:
+  shows "(p \<bullet> bn as) = bn (permute_bn p as)"
+apply(induct as rule: trm_assn.inducts(2))
+apply(auto)[4]
+apply(simp add: permute_bn trm_assn.bn_defs)
+apply(simp add: permute_bn trm_assn.bn_defs)
+apply(simp add: atom_eqvt)
+done
+
+thm trm_assn.supp
+
+lemma "as \<sharp>* x \<longleftrightarrow> (\<forall>a\<in>as. a \<sharp> x)"
+apply(simp add: fresh_def)
+apply(simp add: fresh_star_def)
+oops
+
+inductive
+    test_trm :: "trm \<Rightarrow> bool"
+and test_assn :: "assn \<Rightarrow> bool"
+where
+  "test_trm (Var x)"
+| "\<lbrakk>test_trm t1; test_trm t2\<rbrakk> \<Longrightarrow> test_trm (App t1 t2)"
+| "\<lbrakk>test_trm t; {atom x} \<sharp>* Lam x t\<rbrakk> \<Longrightarrow> test_trm (Lam x t)"
+| "\<lbrakk>test_assn as; test_trm t; set (bn as) \<sharp>* Let as t\<rbrakk> \<Longrightarrow> test_trm (Let as t)"
+| "test_assn ANil"
+| "\<lbrakk>test_trm t; test_assn as\<rbrakk> \<Longrightarrow> test_assn (ACons x t as)"
+
+declare trm_assn.fv_bn_eqvt[eqvt]
+equivariance test_trm
+
+lemma 
+  fixes p::"perm"
+  shows "test_trm (p \<bullet> t)" and "test_assn (p \<bullet> as)"
+apply(induct t and as arbitrary: p and p rule: trm_assn.inducts)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(assumption)
+apply(assumption)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(assumption)
+apply(simp add: trm_assn.fresh fresh_star_def)
+apply(simp)
+defer
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(simp)
+apply(rule test_trm_test_assn.intros)
+apply(assumption)
+apply(assumption)
+apply(subgoal_tac "finite (set (bn (p \<bullet> assn)))")
+apply(subgoal_tac "set (bn (p \<bullet> assn)) \<sharp>* (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm))")
+apply(drule_tac c="()" in at_set_avoiding2)
+apply(simp add: supp_Unit)
+prefer 2
+apply(assumption)
+apply(simp add: finite_supp)
+apply(erule exE)
+apply(erule conjE)
+apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" and
+               s = "Let (permute_bn pa (p \<bullet> assn)) (pa \<bullet> (p \<bullet> trm))" in subst)
+apply(rule trm_assn.eq_iff(4)[THEN iffD2])
+apply(simp add: uu)
+apply(drule supp_perm_eq)
+apply(simp add: tt)
+apply(rule test_trm_test_assn.intros(4))
+defer
+apply(subst permute_plus[symmetric])
+apply(blast)
+oops
+
+
+(* 
+lemma 
+  fixes t::trm
+  and   as::assn
+  and   c::"'a::fs"
+  assumes a1: "\<And>x c. P1 c (Var x)"
+  and     a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)"
+  and     a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)"
+  and     a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)"
+  and     a5: "\<And>c. P2 c ANil"
+  and     a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)"
+  shows "P1 c t" and "P2 c as"
+proof -
+  have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" 
+   and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)"
+    apply(induct rule: trm_assn.inducts)
+    apply(simp)
+    apply(rule a1)
+    apply(simp)
+    apply(rule a2)
+    apply(assumption)
+    apply(assumption)
+    -- "lam case"
+    apply(simp)
+    apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(erule conjE)
+    apply(drule supp_perm_eq[symmetric])
+    apply(simp)
+    apply(thin_tac "?X = ?Y")
+    apply(rule a3)
+    apply(simp add: atom_eqvt permute_set_eq)
+    apply(simp only: permute_plus[symmetric])
+    apply(rule at_set_avoiding2)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: freshs fresh_star_def)
+    --"let case"
+    apply(simp)
+    thm trm_assn.eq_iff
+    thm eq_iffs
+    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q")
+    apply(erule exE)
+    apply(erule conjE)
+    prefer 2
+    apply(rule at_set_avoiding2)
+    apply(rule fin_bn)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: abs_fresh)
+    apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst)
+    prefer 2
+    apply(rule a4)
+    prefer 4
+    apply(simp add: eq_iffs)
+    apply(rule conjI)
+    prefer 2
+    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    prefer 2
+    apply(simp add: eq_iffs)
+    thm eq_iffs
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(simp add: supps)
+    apply(simp add: fresh_star_def freshs)
+    apply(drule supp_perm_eq[symmetric])
+    apply(simp)
+    apply(simp add: eq_iffs)
+    apply(simp)
+    apply(thin_tac "?X = ?Y")
+    apply(rule a4) 
+    apply(simp add: set_eqvt trm_assn.fv_bn_eqvt)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(subst permute_plus[symmetric])
+    apply(blast)
+    apply(simp add: supps)
+    thm at_set_avoiding2
+    --"HERE"
+    apply(rule at_set_avoiding2)
+    apply(rule fin_bn)
+    apply(simp add: finite_supp)
+    apply(simp add: finite_supp)
+    apply(simp add: fresh_star_def freshs)
+    apply(rule ballI)
+    apply(simp add: eqvts permute_bn)
+    apply(rule a5)
+    apply(simp add: permute_bn)
+    apply(rule a6)
+    apply simp
+    apply simp
+    done
+  then have a: "P1 c (0 \<bullet> t)" by blast
+  have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast
+  then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all
+qed
+*)
 
 text {* *}
 
 (*
 
-thm trm_lts.fv
-thm trm_lts.eq_iff
-thm trm_lts.bn
-thm trm_lts.perm
-thm trm_lts.induct[no_vars]
-thm trm_lts.inducts[no_vars]
-thm trm_lts.distinct
-thm trm_lts.supp
-thm trm_lts.fv[simplified trm_lts.supp(1-2)]
-
-
 primrec
   permute_bn_raw
 where
diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Ex/SingleLet.thy	Tue Sep 28 08:21:47 2010 -0400
@@ -13,7 +13,7 @@
 | 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 (set) x in t1, bind (set) x in t2 
+| Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2 
 and assg =
   As "name" x::"name" t::"trm" bind x in t
 binder
@@ -22,6 +22,7 @@
   "bn (As x y t) = [atom x]"
 
 
+
 thm single_let.distinct
 thm single_let.induct
 thm single_let.inducts
@@ -35,9 +36,7 @@
 thm single_let.supports
 thm single_let.fsupp
 thm single_let.supp
-thm single_let.size
-
-
+thm single_let.fresh
 
 
 end
diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Ex/TypeSchemes.thy	Tue Sep 28 08:21:47 2010 -0400
@@ -24,7 +24,8 @@
 thm ty_tys.fv_bn_eqvt
 thm ty_tys.size_eqvt
 thm ty_tys.supports
-thm ty_tys.fsupp
+thm ty_tys.supp
+thm ty_tys.fresh
 
 (* defined as two separate nominal datatypes *)
 
@@ -45,8 +46,8 @@
 thm tys2.fv_bn_eqvt
 thm tys2.size_eqvt
 thm tys2.supports
-thm tys2.fsupp
-
+thm tys2.supp
+thm tys2.fresh
 
 
 text {* *}
diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/Nominal2.thy	Tue Sep 28 08:21:47 2010 -0400
@@ -568,7 +568,27 @@
       qperm_simps qfv_qbn_eqvts qinduct (flat raw_bclauses) lthyC
     else []
 
- 
+  (* postprocessing of eq and fv theorems *)
+
+  val qeq_iffs' = qeq_iffs
+    |> map (simplify (HOL_basic_ss addsimps qfv_supp_thms))
+    |> map (simplify (HOL_basic_ss addsimps @{thms prod_fv_supp prod_alpha_eq Abs_eq_iff[symmetric]}))
+
+  val qsupp_constrs = qfv_defs
+    |> map (simplify (HOL_basic_ss addsimps (take (length qfvs) qfv_supp_thms)))
+
+  val transform_thm = @{lemma "x = y \<Longrightarrow> a \<notin> x \<longleftrightarrow> a \<notin> y" by simp}
+  val transform_thms = 
+    [ @{lemma "a \<notin> (S \<union> T) \<longleftrightarrow> a \<notin> S \<and> a \<notin> T" by simp}, 
+      @{lemma "a \<notin> (S - T) \<longleftrightarrow> a \<notin> S \<or> a \<in> T" by simp}, 
+      @{lemma "(lhs = (a \<notin> {})) \<longleftrightarrow> lhs" by simp}, 
+      @{thm fresh_def[symmetric]}]
+
+  val qfresh_constrs = qsupp_constrs
+    |> map (fn thm => thm RS transform_thm) 
+    |> map (simplify (HOL_basic_ss addsimps transform_thms))
+
+
   (* noting the theorems *)  
 
   (* generating the prefix for the theorem names *)
@@ -578,7 +598,7 @@
 
   val (_, lthy9') = lthyC
      |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
-     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs)
+     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
@@ -590,7 +610,8 @@
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
-     ||>> Local_Theory.note ((thms_suffix "supp", []), qfv_supp_thms)
+     ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)
+     ||>> Local_Theory.note ((thms_suffix "fresh", []), qfresh_constrs)
 in
   (0, lthy9')
 end handle TEST ctxt => (0, ctxt)
diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/ROOT.ML
--- a/Nominal/ROOT.ML	Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/ROOT.ML	Tue Sep 28 08:21:47 2010 -0400
@@ -18,5 +18,6 @@
     "Ex/Modules",
     "Ex/SingleLet",
     "Ex/TypeSchemes",
-    "Ex/TypeVarsTest"
+    "Ex/TypeVarsTest",
+    "Ex/Foo1"
     ];
diff -r 1c18f2cf3923 -r 93a73eabbffc Nominal/nominal_dt_supp.ML
--- a/Nominal/nominal_dt_supp.ML	Sun Sep 26 17:57:30 2010 -0400
+++ b/Nominal/nominal_dt_supp.ML	Tue Sep 28 08:21:47 2010 -0400
@@ -20,8 +20,6 @@
 structure Nominal_Dt_Supp: NOMINAL_DT_SUPP =
 struct
 
-fun lookup xs x = the (AList.lookup (op=) xs x)
-
 (* supports lemmas for constructors *)
 
 fun mk_supports_goal ctxt qtrm =
@@ -122,13 +120,13 @@
 fun symmetric thms = 
   map (fn thm => thm RS @{thm sym}) thms
 
-val supp_abs_set = @{thms supp_abs(1)[symmetric]}
-val supp_abs_res = @{thms supp_abs(2)[symmetric]}
-val supp_abs_lst = @{thms supp_abs(3)[symmetric]}
+val supp_Abs_set = @{thms supp_Abs(1)[symmetric]}
+val supp_Abs_res = @{thms supp_Abs(2)[symmetric]}
+val supp_Abs_lst = @{thms supp_Abs(3)[symmetric]}
 
-fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_set 
-  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_res
-  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_abs_lst
+fun mk_supp_abs ctxt (BC (Set, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_set 
+  | mk_supp_abs ctxt (BC (Res, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_res
+  | mk_supp_abs ctxt (BC (Lst, _, _)) = EqSubst.eqsubst_tac ctxt [1] supp_Abs_lst
 
 fun mk_supp_abs_tac ctxt [] = []
   | mk_supp_abs_tac ctxt (BC (_, [], _)::xs) = mk_supp_abs_tac ctxt xs
@@ -139,8 +137,8 @@
   |> fastype_of
   |> body_type
   |> (fn ty => case ty of
-        @{typ "atom set"}  => simp_tac (add_ss supp_abs_set)
-      | @{typ "atom list"} => simp_tac (add_ss supp_abs_lst)
+        @{typ "atom set"}  => simp_tac (add_ss supp_Abs_set)
+      | @{typ "atom list"} => simp_tac (add_ss supp_Abs_lst)
       | _ => raise TERM ("mk_bn_supp_abs_tac", [trm]))
 
 
@@ -186,6 +184,8 @@
         end)
   in
     induct_prove qtys (goals1 @ goals2) qinduct tac ctxt
+    |> map atomize
+    |> map (simplify (HOL_basic_ss addsimps @{thms fun_eq_iff[symmetric]}))
   end