# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272982687 -7200
# Node ID 8bd75f2fd7b0f6856f55d4286f1d117e2684a777
# Parent  38bbccdf9ff9d9a581481519decdd2a9c70dbd8c# Parent  20be95dce64369c67a259e1fadac6d5d021bd681
merge

diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal-General/Nominal2_Supp.thy
--- a/Nominal-General/Nominal2_Supp.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal-General/Nominal2_Supp.thy	Tue May 04 16:18:07 2010 +0200
@@ -539,4 +539,5 @@
   using fin
   by (simp add: supp_of_fin_sets)
 
+
 end
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Equivp.thy
--- a/Nominal/Equivp.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Equivp.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,5 +1,5 @@
 theory Equivp
-imports "NewFv" "Tacs" "Rsp" "NewFv"
+imports "NewFv" "Tacs" "Rsp"
 begin
 
 ML {*
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/Classical.thy
--- a/Nominal/Ex/Classical.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Classical.thy	Tue May 04 16:18:07 2010 +0200
@@ -12,6 +12,10 @@
 atom_decl name
 atom_decl coname
 
+ML {* val _ = cheat_alpha_eqvt := true *}
+ML {* val _ = cheat_equivp := true *}
+ML {* val _ = cheat_fv_rsp := true *}
+
 nominal_datatype trm =
    Ax "name" "coname"
 |  Cut n::"coname" t1::"trm" c::"coname" t2::"trm"              bind n in t1, bind c in t2
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/Ex2.thy
--- a/Nominal/Ex/Ex2.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Ex2.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,35 +1,31 @@
 theory Ex2
-imports "../Parser"
+imports "../NewParser"
 begin
 
 text {* example 2 *}
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
-nominal_datatype trm' =
+nominal_datatype trm =
   Var "name"
-| App "trm'" "trm'"
-| Lam x::"name" t::"trm'"          bind x in t
-| Let p::"pat'" "trm'" t::"trm'"   bind "f p" in t
-and pat' =
+| App "trm" "trm"
+| Lam x::"name" t::"trm"          bind_set x in t
+| Let p::"pat" "trm" t::"trm"   bind_set "f p" in t
+and pat =
   PN
 | PS "name"
 | PD "name" "name"
 binder
-  f::"pat' \<Rightarrow> atom set"
+  f::"pat \<Rightarrow> atom set"
 where
   "f PN = {}"
 | "f (PD x y) = {atom x, atom y}"
 | "f (PS x) = {atom x}"
-
-thm trm'_pat'.fv
-thm trm'_pat'.eq_iff
-thm trm'_pat'.bn
-thm trm'_pat'.perm
-thm trm'_pat'.induct
-thm trm'_pat'.distinct
-thm trm'_pat'.fv[simplified trm'_pat'.supp]
+thm trm_pat.bn
+thm trm_pat.perm
+thm trm_pat.induct
+thm trm_pat.distinct
+thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
 end
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/Ex3.thy
--- a/Nominal/Ex/Ex3.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Ex3.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,35 +1,34 @@
 theory Ex3
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* Example 3, identical to example 1 from Terms.thy *)
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
-nominal_datatype trm0 =
-  Var0 "name"
-| App0 "trm0" "trm0"
-| Lam0 x::"name" t::"trm0"          bind x in t
-| Let0 p::"pat0" "trm0" t::"trm0"   bind "f0 p" in t
-and pat0 =
-  PN0
-| PS0 "name"
-| PD0 "pat0" "pat0"
+nominal_datatype trm =
+  Var "name"
+| App "trm" "trm"
+| Lam x::"name" t::"trm"        bind_set x in t
+| Let p::"pat" "trm" t::"trm"   bind_set "f p" in t
+and pat =
+  PN
+| PS "name"
+| PD "pat" "pat"
 binder
-  f0::"pat0 \<Rightarrow> atom set"
+  f::"pat \<Rightarrow> atom set"
 where
-  "f0 PN0 = {}"
-| "f0 (PS0 x) = {atom x}"
-| "f0 (PD0 p1 p2) = (f0 p1) \<union> (f0 p2)"
+  "f PN = {}"
+| "f (PS x) = {atom x}"
+| "f (PD p1 p2) = (f p1) \<union> (f p2)"
 
-thm trm0_pat0.fv
-thm trm0_pat0.eq_iff
-thm trm0_pat0.bn
-thm trm0_pat0.perm
-thm trm0_pat0.induct
-thm trm0_pat0.distinct
-thm trm0_pat0.fv[simplified trm0_pat0.supp,no_vars]
+thm trm_pat.fv
+thm trm_pat.eq_iff
+thm trm_pat.bn
+thm trm_pat.perm
+thm trm_pat.induct
+thm trm_pat.distinct
+thm trm_pat.fv[simplified trm_pat.supp(1-2)]
 
 end
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/ExCoreHaskell.thy
--- a/Nominal/Ex/ExCoreHaskell.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExCoreHaskell.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,23 +1,15 @@
 theory ExCoreHaskell
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* core haskell *)
 
-ML {* val _ = recursive := false *}
-(* this should not be an equivariance rule *)
-(* for the moment, we force it to be       *)
-setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
-thm eqvts
-(*declare permute_pure[eqvt]*)
-
 atom_decl var
 atom_decl cvar
 atom_decl tvar
 
 (* there are types, coercion types and regular types list-data-structure *)
 
-ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype tkind =
   KStar
 | KFun "tkind" "tkind"
@@ -28,7 +20,7 @@
 | TC "string"
 | TApp "ty" "ty"
 | TFun "string" "ty_lst"
-| TAll tv::"tvar" "tkind" T::"ty"  bind tv in T
+| TAll tv::"tvar" "tkind" T::"ty"  bind_set tv in T
 | TEq "ckind" "ty"
 and ty_lst =
   TsNil
@@ -38,7 +30,7 @@
 | CConst "string"
 | CApp "co" "co"
 | CFun "string" "co_lst"
-| CAll cv::"cvar" "ckind" C::"co"  bind cv in C
+| CAll cv::"cvar" "ckind" C::"co"  bind_set cv in C
 | CEq "ckind" "co"
 | CRefl "ty"
 | CSym "co"
@@ -56,13 +48,13 @@
 and trm =
   Var "var"
 | K "string"
-| LAMT tv::"tvar" "tkind" t::"trm" bind tv in t
-| LAMC cv::"cvar" "ckind" t::"trm" bind cv in t
+| LAMT tv::"tvar" "tkind" t::"trm" bind_set tv in t
+| LAMC cv::"cvar" "ckind" t::"trm" bind_set cv in t
 | AppT "trm" "ty"
 | AppC "trm" "co"
-| Lam v::"var" "ty" t::"trm"       bind v in t
+| Lam v::"var" "ty" t::"trm"       bind_set v in t
 | App "trm" "trm"
-| Let x::"var" "ty" "trm" t::"trm" bind x in t
+| Let x::"var" "ty" "trm" t::"trm" bind_set x in t
 | Case "trm" "assoc_lst"
 | Cast "trm" "ty"                  --"ty is supposed to be a coercion type only"
 and assoc_lst =
@@ -93,86 +85,6 @@
 | "bv_cvs CvsNil = []"
 | "bv_cvs (CvsCons v k t) = (atom v) # bv_cvs t"
 
-(*
-function
-rfv_tkind_raw and rfv_ckind_raw and rfv_ty_raw and rfv_ty_lst_raw and rfv_co_raw and rfv_co_lst_raw and rfv_trm_raw and rfv_assoc_lst_raw and rfv_bv_raw and rfv_bv_vs_raw and rfv_bv_tvs_raw and rfv_bv_cvs_raw and rfv_pat_raw and rfv_vars_raw and rfv_tvars_raw and rfv_cvars_raw
-where
-  "rfv_tkind_raw KStar_raw = {}"
-| "rfv_tkind_raw (KFun_raw tkind_raw1 tkind_raw2) = rfv_tkind_raw tkind_raw1 \<union> rfv_tkind_raw tkind_raw2"
-| "rfv_ckind_raw (CKEq_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2"
-| "rfv_ty_raw (TVar_raw tvar) = {atom tvar}"
-| "rfv_ty_raw (TC_raw list) = {}"
-| "rfv_ty_raw (TApp_raw ty_raw1 ty_raw2) = rfv_ty_raw ty_raw1 \<union> rfv_ty_raw ty_raw2"
-| "rfv_ty_raw (TFun_raw list ty_lst_raw) = rfv_ty_lst_raw ty_lst_raw"
-| "rfv_ty_raw (TAll_raw tvar tkind_raw ty_raw) =
- rfv_tkind_raw tkind_raw \<union> (rfv_ty_raw ty_raw - {atom tvar})"
-| "rfv_ty_raw (TEq_raw ckind_raw ty_raw) = rfv_ckind_raw ckind_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_ty_lst_raw TsNil_raw = {}"
-| "rfv_ty_lst_raw (TsCons_raw ty_raw ty_lst_raw) = rfv_ty_raw ty_raw \<union> rfv_ty_lst_raw ty_lst_raw"
-| "rfv_co_raw (CVar_raw cvar) = {atom cvar}"
-| "rfv_co_raw (CConst_raw list) = {}"
-| "rfv_co_raw (CApp_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_raw (CFun_raw list co_lst_raw) = rfv_co_lst_raw co_lst_raw"
-| "rfv_co_raw (CAll_raw cvar ckind_raw co_raw) =
- rfv_ckind_raw ckind_raw \<union> (rfv_co_raw co_raw - {atom cvar})"
-| "rfv_co_raw (CEq_raw ckind_raw co_raw) = rfv_ckind_raw ckind_raw \<union> rfv_co_raw co_raw"
-| "rfv_co_raw (CRefl_raw ty_raw) = rfv_ty_raw ty_raw"
-| "rfv_co_raw (CSym_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CCir_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_raw (CAt_raw co_raw ty_raw) = rfv_co_raw co_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_co_raw (CLeft_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CRight_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CSim_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_raw (CRightc_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CLeftc_raw co_raw) = rfv_co_raw co_raw"
-| "rfv_co_raw (CCoe_raw co_raw1 co_raw2) = rfv_co_raw co_raw1 \<union> rfv_co_raw co_raw2"
-| "rfv_co_lst_raw CsNil_raw = {}"
-| "rfv_co_lst_raw (CsCons_raw co_raw co_lst_raw) = rfv_co_raw co_raw \<union> rfv_co_lst_raw co_lst_raw"
-| "rfv_trm_raw (Var_raw var) = {atom var}"
-| "rfv_trm_raw (K_raw list) = {}"
-| "rfv_trm_raw (LAMT_raw tvar tkind_raw trm_raw) =
- rfv_tkind_raw tkind_raw \<union> (rfv_trm_raw trm_raw - {atom tvar})"
-| "rfv_trm_raw (LAMC_raw cvar ckind_raw trm_raw) =
- rfv_ckind_raw ckind_raw \<union> (rfv_trm_raw trm_raw - {atom cvar})"
-| "rfv_trm_raw (AppT_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_trm_raw (AppC_raw trm_raw co_raw) = rfv_trm_raw trm_raw \<union> rfv_co_raw co_raw"
-| "rfv_trm_raw (Lam_raw var ty_raw trm_raw) = rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw - {atom var})"
-| "rfv_trm_raw (App_raw trm_raw1 trm_raw2) = rfv_trm_raw trm_raw1 \<union> rfv_trm_raw trm_raw2"
-| "rfv_trm_raw (Let_raw var ty_raw trm_raw1 trm_raw2) =
- rfv_ty_raw ty_raw \<union> (rfv_trm_raw trm_raw1 \<union> (rfv_trm_raw trm_raw2 - {atom var}))"
-| "rfv_trm_raw (Case_raw trm_raw assoc_lst_raw) = rfv_trm_raw trm_raw \<union> rfv_assoc_lst_raw assoc_lst_raw"
-| "rfv_trm_raw (Cast_raw trm_raw ty_raw) = rfv_trm_raw trm_raw \<union> rfv_ty_raw ty_raw"
-| "rfv_assoc_lst_raw ANil_raw = {}"
-| "rfv_assoc_lst_raw (ACons_raw pat_raw trm_raw assoc_lst_raw) =
- rfv_bv_raw pat_raw \<union> (rfv_trm_raw trm_raw - set (bv_raw pat_raw) \<union> rfv_assoc_lst_raw assoc_lst_raw)"
-| "rfv_bv_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) =
- rfv_bv_tvs_raw tvars_raw \<union> (rfv_bv_cvs_raw cvars_raw \<union> rfv_bv_vs_raw vars_raw)"
-| "rfv_bv_vs_raw VsNil_raw = {}"
-| "rfv_bv_vs_raw (VsCons_raw var ty_raw vars_raw) = rfv_ty_raw ty_raw \<union> rfv_bv_vs_raw vars_raw"
-| "rfv_bv_tvs_raw TvsNil_raw = {}"
-| "rfv_bv_tvs_raw (TvsCons_raw tvar tkind_raw tvars_raw) =
- rfv_tkind_raw tkind_raw \<union> rfv_bv_tvs_raw tvars_raw"
-| "rfv_bv_cvs_raw CvsNil_raw = {}"
-| "rfv_bv_cvs_raw (CvsCons_raw cvar ckind_raw cvars_raw) =
- rfv_ckind_raw ckind_raw \<union> rfv_bv_cvs_raw cvars_raw"
-| "rfv_pat_raw (Kpat_raw list tvars_raw cvars_raw vars_raw) =
- rfv_tvars_raw tvars_raw \<union> (rfv_cvars_raw cvars_raw \<union> rfv_vars_raw vars_raw)"
-| "rfv_vars_raw VsNil_raw = {}"
-| "rfv_vars_raw (VsCons_raw var ty_raw vars_raw) =
- {atom var} \<union> (rfv_ty_raw ty_raw \<union> rfv_vars_raw vars_raw)"
-| "rfv_tvars_raw TvsNil_raw = {}"
-| "rfv_tvars_raw (TvsCons_raw tvar tkind_raw tvars_raw) =
- {atom tvar} \<union> (rfv_tkind_raw tkind_raw \<union> rfv_tvars_raw tvars_raw)"
-| "rfv_cvars_raw CvsNil_raw = {}"
-| "rfv_cvars_raw (CvsCons_raw cvar ckind_raw cvars_raw) =
- {atom cvar} \<union> (rfv_ckind_raw ckind_raw \<union> rfv_cvars_raw cvars_raw)"
-apply pat_completeness
-apply auto
-done
-termination
-by lexicographic_order
-*)
-
 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.supp(1-9,11,13,15)
 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.fv[simplified fv_supp]
 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.perm
@@ -213,9 +125,7 @@
  "alpha_cvars_raw e b \<Longrightarrow> alpha_cvars_raw (permute_bv_cvs_raw x e) (permute_bv_cvs_raw x b)"
  "alpha_vars_raw f c \<Longrightarrow> alpha_vars_raw (permute_bv_vs_raw x f) (permute_bv_vs_raw x c)"
  apply (erule_tac [!] alpha_inducts)
- apply simp_all
- apply (rule_tac [!] alpha_intros)
- apply simp_all
+ apply (simp_all only: alpha_intros perm permute_bv_tvs_raw.simps permute_bv_cvs_raw.simps permute_bv_vs_raw.simps)
  done
 
 lemma [quot_respect]:
@@ -252,27 +162,23 @@
   "p \<bullet> bv_tvs c = bv_tvs (permute_bv_tvs p c)"
   "p \<bullet> bv_vs d = bv_vs (permute_bv_vs p d)"
   apply(induct b rule: inducts(12))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct c rule: inducts(11))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct d rule: inducts(10))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   done
 
 lemma perm_bv2:
   "p \<bullet> bv l = bv (permute_bv p l)"
   apply(induct l rule: inducts(9))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv)
   apply(simp add: perm_bv1[symmetric])
   apply(simp add: eqvts)
   done
 
 lemma alpha_perm_bn1:
- " alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
+ "alpha_bv_tvs tvars (permute_bv_tvs q tvars)"
  "alpha_bv_cvs cvars (permute_bv_cvs q cvars)"
  "alpha_bv_vs vars (permute_bv_vs q vars)"
   apply(induct tvars rule: inducts(11))
@@ -292,13 +198,13 @@
 lemma ACons_subst:
   "supp (Abs_lst (bv pat) trm) \<sharp>* q \<Longrightarrow> (ACons pat trm al) = ACons (permute_bv q pat) (q \<bullet> trm) al"
   apply (simp only: eq_iff)
+  apply (simp add: alpha_perm_bn)
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
   apply (simp add: perm_bv2[symmetric])
   apply (simp add: eqvts[symmetric])
   apply (simp add: supp_abs)
   apply (simp add: fv_supp)
-  apply (simp add: alpha_perm_bn)
   apply (rule supp_perm_eq[symmetric])
   apply (subst supp_finite_atom_set)
   apply (rule finite_Diff)
@@ -311,34 +217,27 @@
   "permute_bv_tvs 0 c = c"
   "permute_bv_vs 0 d = d"
   apply(induct b rule: inducts(12))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct c rule: inducts(11))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   apply(induct d rule: inducts(10))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts)
   done
 
 lemma permute_bv_zero2:
   "permute_bv 0 a = a"
   apply(induct a rule: inducts(9))
-  apply(rule TrueI)
   apply(simp_all add:permute_bv eqvts permute_bv_zero1)
   done
 
 lemma fv_alpha1: "fv_bv_tvs x \<sharp>* pa \<Longrightarrow> alpha_bv_tvs (pa \<bullet> x) x"
-apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: eq_iff fresh_star_union)
-apply (subst supp_perm_eq)
-apply (simp_all add: fv_supp)
-done
+  apply (induct x rule: inducts(11))
+  apply (simp_all add: eq_iff fresh_star_union)
+  done
 
 lemma fv_alpha2: "fv_bv_cvs x \<sharp>* pa \<Longrightarrow> alpha_bv_cvs (pa \<bullet> x) x"
 apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (rule TrueI)+
 apply (simp_all add: eq_iff fresh_star_union)
 apply (subst supp_perm_eq)
 apply (simp_all add: fv_supp)
@@ -346,70 +245,65 @@
 
 lemma fv_alpha3: "fv_bv_vs x \<sharp>* pa \<Longrightarrow> alpha_bv_vs (pa \<bullet> x) x"
 apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp_all add: eq_iff fresh_star_union)
+apply (rule TrueI)+
+apply (simp_all add: fresh_star_union eq_iff)
 apply (subst supp_perm_eq)
 apply (simp_all add: fv_supp)
 done
 
 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x"
 apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (rule TrueI)+
 apply (simp_all add: eq_iff fresh_star_union)
 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3)
-apply (simp add: eqvts)
+apply (subst supp_perm_eq)
+apply (simp_all add: fv_supp)
 done
 
 lemma fin1: "finite (fv_bv_tvs x)"
 apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin2: "finite (fv_bv_cvs x)"
 apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin3: "finite (fv_bv_vs x)"
 apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin_fv_bv: "finite (fv_bv x)"
 apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
+apply (rule TrueI)+
+defer
+apply (rule TrueI)+
 apply (simp add: fin1 fin2 fin3)
+apply (rule finite_supp)
 done
 
 lemma finb1: "finite (set (bv_tvs x))"
 apply (induct x rule: inducts(11))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma finb2: "finite (set (bv_cvs x))"
 apply (induct x rule: inducts(12))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma finb3: "finite (set (bv_vs x))"
 apply (induct x rule: inducts(10))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
 apply (simp_all add: fv_supp finite_supp)
 done
 
 lemma fin_bv: "finite (set (bv x))"
 apply (induct x rule: inducts(9))
-apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *})
-apply (simp add: finb1 finb2 finb3)
+apply (simp_all add: finb1 finb2 finb3)
 done
 
-thm tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vars_tvars_cvars.induct
-
 lemma strong_induction_principle:
   assumes a01: "\<And>b. P1 b KStar"
   and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)"
@@ -494,7 +388,7 @@
     apply (simp only: perm)
     apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)"
                and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}"
@@ -534,7 +428,7 @@
     apply (simp only: perm)
     apply(rule_tac t="CAll (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> co)"
                and s="CAll (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> cvar)}"
@@ -575,7 +469,7 @@
     apply (simp only: perm)
     apply(rule_tac t="LAMT (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> trm)"
                and s="LAMT (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> tvar)}"
@@ -615,7 +509,7 @@
     apply (simp only: perm)
     apply(rule_tac t="LAMC (p \<bullet> cvar) (p \<bullet> ckind) (p \<bullet> trm)"
                and s="LAMC (pa \<bullet> p \<bullet> cvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> cvar)}"
@@ -656,7 +550,7 @@
     apply (simp only: perm)
     apply(rule_tac t="Lam (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm)"
                and s="Lam (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (pa \<bullet> p \<bullet> trm)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - {atom (pa \<bullet> p \<bullet> var)}"
@@ -697,7 +591,7 @@
     apply (simp only: perm)
     apply(rule_tac t="Let (p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (p \<bullet> trm2)"
                and s="Let (pa \<bullet> p \<bullet> var) (p \<bullet> ty) (p \<bullet> trm1) (pa \<bullet> p \<bullet> trm2)" in subst)
-    apply (simp only: eq_iff)
+    apply (simp add: eq_iff)
     apply (rule_tac x="-pa" in exI)
     apply (simp add: alphas eqvts eqvts_raw supp_abs fv_supp)
     apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm2) - {atom (pa \<bullet> p \<bullet> var)}"
@@ -760,6 +654,12 @@
 
 section {* test about equivariance for alpha *}
 
+(* this should not be an equivariance rule *)
+(* for the moment, we force it to be       *)
+
+(*declare permute_pure[eqvt]*)
+(*setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+
 thm eqvts
 thm eqvts_raw
 
@@ -769,7 +669,7 @@
 equivariance alpha_tkind_raw
 
 thm eqvts
-thm eqvts_raw
+thm eqvts_raw*)
 
 end
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/ExLeroy.thy
--- a/Nominal/Ex/ExLeroy.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExLeroy.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,21 +1,20 @@
 theory ExLeroy
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example form Leroy 96 about modules; OTT *)
 
 atom_decl name
 
-ML {* val _ = recursive := false  *}
 nominal_datatype mexp =
   Acc "path"
 | Stru "body"
-| Funct x::"name" "sexp" m::"mexp"    bind x in m
+| Funct x::"name" "sexp" m::"mexp"    bind_set x in m
 | FApp "mexp" "path"
 | Ascr "mexp" "sexp"
 and body =
   Empty
-| Seq c::defn d::"body"     bind "cbinders c" in d
+| Seq c::defn d::"body"     bind_set "cbinders c" in d
 and defn =
   Type "name" "tyty"
 | Dty "name"
@@ -26,7 +25,7 @@
 | SFunc "name" "sexp" "sexp"
 and sbody =
   SEmpty
-| SSeq C::spec D::sbody    bind "Cbinders C" in D
+| SSeq C::spec D::sbody    bind_set "Cbinders C" in D
 and spec =
   Type1 "name"
 | Type2 "name" "tyty"
@@ -42,7 +41,7 @@
 and trmtrm =
   Tref1 "name"
 | Tref2 "path" "name"
-| Lam' v::"name" "tyty" M::"trmtrm"  bind v in M
+| Lam' v::"name" "tyty" M::"trmtrm"  bind_set v in M
 | App' "trmtrm" "trmtrm"
 | Let' "body" "trmtrm"
 binder
@@ -65,8 +64,8 @@
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.induct
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.distinct
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp
-thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp]
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.fv[simplified mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm.supp(1-3,5-7,9-10)]
 
 end
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/ExLet.thy
--- a/Nominal/Ex/ExLet.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExLet.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,17 +1,15 @@
 theory ExLet
-imports "../Parser" "../../Attic/Prove"
+imports "../NewParser" "../../Attic/Prove"
 begin
 
 text {* example 3 or example 5 from Terms.thy *}
 
 atom_decl name
 
-ML {* val _ = recursive := false *}
-ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind x in t
+| Lm x::"name" t::"trm"  bind_set x in t
 | Lt a::"lts" t::"trm"   bind "bn a" in t
 (*| L a::"lts" t1::"trm" t2::"trm"  bind "bn a" in t1, bind "bn a" in t2*)
 and lts =
@@ -52,11 +50,10 @@
   apply simp
   apply clarify
   apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
+  apply (rule TrueI)+
   apply simp_all
-  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
-  apply simp
-  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
-  apply simp
+  apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp_all
   done
 
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
@@ -64,8 +61,8 @@
 lemma permute_bn_zero:
   "permute_bn 0 a = a"
   apply(induct a rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
+  apply(rule TrueI)+
+  apply(simp_all add:permute_bn)
   done
 
 lemma permute_bn_add:
@@ -74,37 +71,29 @@
 
 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
   apply(induct lts rule: trm_lts.inducts(2))
-  apply(rule TrueI)
+  apply(rule TrueI)+
   apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
   done
 
 lemma perm_bn:
   "p \<bullet> bn l = bn(permute_bn p l)"
   apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
+  apply(rule TrueI)+
   apply(simp_all add:permute_bn eqvts)
   done
 
 lemma fv_perm_bn:
   "fv_bn l = fv_bn (permute_bn p l)"
   apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
+  apply(rule TrueI)+
   apply(simp_all add:permute_bn eqvts)
   done
 
-lemma fv_fv_bn:
-  "fv_bn l - set (bn l) = fv_lts l - set (bn l)"
-  apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
-  by blast
-
 lemma Lt_subst:
   "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
-  apply (simp only: trm_lts.eq_iff)
+  apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn)
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
-  apply (simp add: permute_bn_alpha_bn)
   apply (simp add: perm_bn[symmetric])
   apply (simp add: eqvts[symmetric])
   apply (simp add: supp_abs)
@@ -204,8 +193,7 @@
   "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
   apply (simp add: trm_lts.eq_iff)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alphas)
-  apply (simp add: fresh_star_def eqvts)
+  apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
   done
 
 lemma lets_ok3:
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/ExLetRec.thy
--- a/Nominal/Ex/ExLetRec.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExLetRec.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,5 +1,5 @@
 theory ExLetRec
-imports "../Parser"
+imports "../NewParser"
 begin
 
 
@@ -7,13 +7,11 @@
 
 atom_decl name
 
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind x in t
-| Lt a::"lts" t::"trm"   bind "bn a" in t
+| Lm x::"name" t::"trm"  bind_set x in t
+| Lt a::"lts" t::"trm"   bind "bn a" in a t
 and lts =
   Lnil
 | Lcons "name" "trm" "lts"
@@ -38,13 +36,13 @@
 
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
-  by (simp add: trm_lts.eq_iff alphas2 set_sub)
+  by (simp add: trm_lts.eq_iff alphas2 set_sub supp_at_base)
 
 lemma lets_ok:
   "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
   apply (simp add: trm_lts.eq_iff)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alphas2 fresh_star_def eqvts)
+  apply (simp_all add: alphas2 fresh_star_def eqvts supp_at_base)
   done
 
 lemma lets_ok3:
@@ -72,7 +70,7 @@
 lemma lets_ok4:
   "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
    (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
-  apply (simp add: alphas trm_lts.eq_iff)
+  apply (simp add: alphas trm_lts.eq_iff supp_at_base)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
   apply (simp add: atom_eqvt fresh_star_def)
   done
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/ExPS7.thy
--- a/Nominal/Ex/ExPS7.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/ExPS7.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,17 +1,16 @@
 theory ExPS7
-imports "../Parser"
+imports "../NewParser"
 begin
 
 (* example 7 from Peter Sewell's bestiary *)
 
 atom_decl name
 
-ML {* val _ = recursive := true  *}
 nominal_datatype exp7 =
   EVar name
 | EUnit
 | EPair exp7 exp7
-| ELetRec l::"lrbs" e::"exp7" bind "b7s l" in e
+| ELetRec l::"lrbs" e::"exp7" bind_set "b7s l" in l e
 and lrb =
   Assign name exp7
 and lrbs =
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,5 +1,5 @@
 theory Lambda
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
@@ -7,7 +7,7 @@
 nominal_datatype lam =
   Var "name"
 | App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
+| Lam x::"name" l::"lam"  bind_set x in l
 
 thm lam.fv
 thm lam.supp
@@ -17,7 +17,7 @@
 
 section {* Strong Induction Principles*}
 
-(* 
+(*
   Old way of establishing strong induction
   principles by chosing a fresh name.
 *)
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/SingleLet.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,16 +1,14 @@
 theory SingleLet
-imports "../Parser"
+imports "../NewParser"
 begin
 
 atom_decl name
 
-ML {* val _ = recursive := false *}
-
 nominal_datatype trm =
   Var "name"
 | App "trm" "trm"
-| Lam x::"name" t::"trm"  bind x in t
-| Let a::"assg" t::"trm"  bind "bn a" in t
+| Lam x::"name" t::"trm"  bind_set x in t
+| Let a::"assg" t::"trm"  bind_set "bn a" in t
 and assg =
   As "name" "trm"
 binder
@@ -18,19 +16,23 @@
 where
   "bn (As x t) = {atom x}"
 
-print_theorems
-thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
-
 thm trm_assg.fv
 thm trm_assg.supp
-thm trm_assg.eq_iff[simplified alphas_abs[symmetric]]
+thm trm_assg.eq_iff
 thm trm_assg.bn
 thm trm_assg.perm
 thm trm_assg.induct
 thm trm_assg.inducts
 thm trm_assg.distinct
 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *}
-thm trm_assg.fv[simplified trm_assg.supp]
+thm trm_assg.fv[simplified trm_assg.supp(1-2)]
+
+(*
+setup {* Context.theory_map (Nominal_ThmDecls.add_thm @{thm "permute_pure"}) *}
+declare permute_trm_raw_permute_assg_raw.simps[eqvt]
+declare alpha_gen_eqvt[eqvt]
+equivariance alpha_trm_raw
+*)
 
 end
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/Term8.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/Term8.thy	Tue May 04 16:18:07 2010 +0200
@@ -0,0 +1,23 @@
+theory Term8
+imports "../NewParser"
+begin
+
+(* example 8 from Terms.thy *)
+
+atom_decl name
+
+nominal_datatype foo =
+  Foo0 "name"
+| Foo1 b::"bar" f::"foo" bind_set "bv b" in f
+and bar =
+  Bar0 "name"
+| Bar1 "name" s::"name" b::"bar" bind_set s in b
+binder
+  bv
+where
+  "bv (Bar0 x) = {}"
+| "bv (Bar1 v x b) = {atom v}"
+
+end
+
+
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/Test.thy
--- a/Nominal/Ex/Test.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/Test.thy	Tue May 04 16:18:07 2010 +0200
@@ -20,23 +20,6 @@
 thm fv_trm4_raw_fv_trm4_raw_list.simps[no_vars]
 *)
 
-(* example 8 from Terms.thy *)
-
-(* Binding in a term under a bn, needs to fail *)
-(*
-nominal_datatype foo8 =
-  Foo0 "name"
-| Foo1 b::"bar8" f::"foo8" bind "bv8 b" in f --"check fo error if this is called foo"
-and bar8 =
-  Bar0 "name"
-| Bar1 "name" s::"name" b::"bar8" bind s in b
-binder
-  bv8
-where
-  "bv8 (Bar0 x) = {}"
-| "bv8 (Bar1 v x b) = {atom v}"
-*)
-
 end
 
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Ex/TypeSchemes.thy
--- a/Nominal/Ex/TypeSchemes.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,18 +1,16 @@
 theory TypeSchemes
-imports "../Parser"
+imports "../NewParser"
 begin
 
 section {*** Type Schemes ***}
 
 atom_decl name
 
-ML {* val _ = alpha_type := AlphaRes *}
-
 nominal_datatype ty =
   Var "name"
 | Fun "ty" "ty"
 and tys =
-  All xs::"name fset" ty::"ty" bind xs in ty
+  All xs::"name fset" ty::"ty" bind_res xs in ty
 
 lemmas ty_tys_supp = ty_tys.fv[simplified ty_tys.supp]
 
@@ -125,21 +123,21 @@
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alphas)
-  apply(simp add: fresh_star_def fresh_zero_perm)
+  apply(simp add: fresh_star_def fresh_zero_perm supp_at_base)
   done
 
 lemma
   shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alphas fresh_star_def eqvts)
+  apply(simp add: alphas fresh_star_def eqvts supp_at_base)
   done
 
 lemma
   shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
   apply(simp add: ty_tys.eq_iff)
   apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
 done
 
 lemma
@@ -148,7 +146,7 @@
   using a
   apply(simp add: ty_tys.eq_iff)
   apply(clarify)
-  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff)
+  apply(simp add: alphas fresh_star_def eqvts ty_tys.eq_iff supp_at_base)
   apply auto
   done
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Fv.thy	Tue May 04 16:18:07 2010 +0200
@@ -650,4 +650,29 @@
 end
 *}
 
+
+ML {*
+fun define_fv_alpha_export dt binds bns ctxt =
+let
+  val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
+    define_fv dt binds bns ctxt;
+  val (alpha, ctxt'') =
+    define_alpha dt binds bns fv_ts_loc ctxt';
+  val alpha_ts_loc = #preds alpha
+  val alpha_induct_loc = #induct alpha
+  val alpha_intros_loc = #intrs alpha;
+  val alpha_cases_loc = #elims alpha
+  val morphism = ProofContext.export_morphism ctxt'' ctxt;
+  val fv_ts = map (Morphism.term morphism) fv_ts_loc;
+  val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
+  val fv_def = Morphism.fact morphism fv_def_loc;
+  val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
+  val alpha_induct = Morphism.thm morphism alpha_induct_loc;
+  val alpha_intros = Morphism.fact morphism alpha_intros_loc
+  val alpha_cases = Morphism.fact morphism alpha_cases_loc
+in
+  ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')
+end;
+*}
+
 end
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Lift.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,8 +1,8 @@
 theory Lift
-imports "../Nominal-General/Nominal2_Atoms" 
-        "../Nominal-General/Nominal2_Eqvt" 
-        "../Nominal-General/Nominal2_Supp" 
-        "Abs" "Perm" "Equivp" "Rsp" "Attic/Fv"
+imports "../Nominal-General/Nominal2_Atoms"
+        "../Nominal-General/Nominal2_Eqvt"
+        "../Nominal-General/Nominal2_Supp"
+        "Abs" "Perm" "Equivp" "Rsp"
 begin
 
 
@@ -66,32 +66,5 @@
 end
 *}
 
-
-
-
-ML {*
-fun define_fv_alpha_export dt binds bns ctxt =
-let
-  val (((fv_ts_loc, fv_def_loc), ord_fv_ts_loc), ctxt') =
-    define_fv dt binds bns ctxt;
-  val (alpha, ctxt'') =
-    define_alpha dt binds bns fv_ts_loc ctxt';
-  val alpha_ts_loc = #preds alpha
-  val alpha_induct_loc = #induct alpha
-  val alpha_intros_loc = #intrs alpha;
-  val alpha_cases_loc = #elims alpha
-  val morphism = ProofContext.export_morphism ctxt'' ctxt;
-  val fv_ts = map (Morphism.term morphism) fv_ts_loc;
-  val ord_fv_ts = map (Morphism.term morphism) ord_fv_ts_loc;
-  val fv_def = Morphism.fact morphism fv_def_loc;
-  val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
-  val alpha_induct = Morphism.thm morphism alpha_induct_loc;
-  val alpha_intros = Morphism.fact morphism alpha_intros_loc
-  val alpha_cases = Morphism.fact morphism alpha_cases_loc
-in
-  ((((fv_ts, ord_fv_ts), fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt'')
-end;
-*}
-
 end
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/NewFv.thy	Tue May 04 16:18:07 2010 +0200
@@ -4,6 +4,8 @@
 begin
 
 ML {*
+(* binding modes *)
+
 datatype bmodes =
    BEmy of int
 |  BLst of ((term option * int) list) * (int list)
@@ -243,18 +245,19 @@
 *}
 
 ML {*
-fun define_raw_fv (dt_info : Datatype_Aux.info) bn_funs bclausesss lthy =
+fun define_raw_fv dt_descr sorts bn_funs bclausesss lthy =
 let
   val thy = ProofContext.theory_of lthy;
-  val {descr as dt_descr, sorts, ...} = dt_info;
 
   val fv_names = prefix_dt_names dt_descr sorts "fv_"
-  val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr;
+  val fv_types = map (fn (i, _) => nth_dtyp dt_descr sorts i --> @{typ "atom set"}) dt_descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
 
+  (* free variables for the bn-functions *)
   val (bn_fvbn, fv_bn_names, fv_bn_eqs) =
     fv_bns thy dt_descr sorts fv_frees bn_funs bclausesss;
 
+  
   val fv_bns = map snd bn_fvbn;
   val fv_nums = 0 upto (length fv_frees - 1)
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/NewParser.thy	Tue May 04 16:18:07 2010 +0200
@@ -159,8 +159,9 @@
 end
 *}
 
-text {* What does the prep_bn code do? Cezary's Function? *}
-
+(* strip_bn_fun takes a bn function defined by the user as a union or
+   append of elements and returns those elements together with bn functions
+   applied *)
 ML {*
 fun strip_bn_fun t =
   case t of
@@ -258,6 +259,31 @@
 end
 *}
 
+lemma equivp_hack: "equivp x"
+sorry
+ML {*
+fun equivp_hack ctxt rel =
+let
+  val thy = ProofContext.theory_of ctxt
+  val ty = domain_type (fastype_of rel)
+  val cty = ctyp_of thy ty
+  val ct = cterm_of thy rel
+in
+  Drule.instantiate' [SOME cty] [SOME ct] @{thm equivp_hack}
+end
+*}
+
+ML {* val cheat_alpha_eqvt = Unsynchronized.ref false *}
+ML {* val cheat_equivp = Unsynchronized.ref false *}
+ML {* val cheat_fv_rsp = Unsynchronized.ref false *}
+ML {* val cheat_alpha_bn_rsp = Unsynchronized.ref false *}
+ML {* val cheat_supp_eq = Unsynchronized.ref false *}
+
+ML {*
+fun remove_loop t =
+  let val _ = HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of t)) in t end
+  handle TERM _ => @{thm eqTrueI} OF [t]
+*}
 
 text {* 
   nominal_datatype2 does the following things in order:
@@ -324,31 +350,45 @@
  29) prove supp = fv
 *}
 
+ML {*
+(* for testing porposes - to exit the procedure early *)
+exception TEST of Proof.context
+
+val STEPS = 10
+*}
 
 ML {*
 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy =
 let
   (* definition of the raw datatype and raw bn-functions *)
   val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) =
-    raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+    if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
+    else raise TEST lthy
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
-  val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
+  val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
+  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 
-  val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
-  val inject = flat (map #inject dtinfos);
-  val distincts = flat (map #distinct dtinfos);
-  val rel_dtinfos = List.take (dtinfos, (length dts));
-  val rel_distinct = map #distinct rel_dtinfos;
-  val induct = #induct dtinfo;
-  val exhausts = map #exhaust dtinfos;
+  
+  (* what is the difference between raw_dt_names and all_full_tnames ? *)
+  (* what is the purpose of dtinfo and dtinfos ? *)
+  val _ = tracing ("raw_dt_names " ^ commas raw_dt_names)
+  val _ = tracing ("all_full_tnames " ^ commas all_full_tnames)
+
+  val inject_thms = flat (map #inject dtinfos);
+  val distinct_thms = flat (map #distinct dtinfos);
+  val rel_dtinfos = List.take (dtinfos, (length dts)); 
+  val rel_distinct = map #distinct rel_dtinfos;  (* thm list list *)
+  val induct_thm = #induct dtinfo;
+  val exhaust_thms = map #exhaust dtinfos;
 
   (* definitions of raw permutations *)
   val ((raw_perm_def, raw_perm_simps, perms), lthy2) =
-    Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy1;
+    if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1
+    else raise TEST lthy1
 
   val morphism_2_0 = ProofContext.export_morphism lthy2 lthy
   fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l);
@@ -362,11 +402,18 @@
   val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls;
 
   (* definition of raw fv_functions *)
-  val ((fv, fvbn), fv_def, lthy3a) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses)
+  val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls)
+  val ((fv, fvbn), fv_def, lthy3a) = 
+    if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3
+    else raise TEST lthy3
   
+
   (* definition of raw alphas *)
   val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) =
-    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a;
+    if STEPS > 4 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a
+    else raise TEST lthy3a
+  
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts
   
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
@@ -379,22 +426,27 @@
     ((map (fn i => nth rel_distinct i) bn_nos) ~~ alpha_ts_bn))
   
   (* definition of raw_alpha_eq_iff  lemmas *)
-  val alpha_eq_iff = build_rel_inj alpha_intros (inject @ distincts) alpha_cases lthy4
-  
+  val alpha_eq_iff = build_rel_inj alpha_intros (inject_thms @ distinct_thms) alpha_cases lthy4
+  val alpha_eq_iff_simp = map remove_loop alpha_eq_iff;
+  val _ = map tracing (map PolyML.makestring alpha_eq_iff_simp);
+
   (* proving equivariance lemmas *)
   val _ = warning "Proving equivariance";
-  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
-  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
-  fun alpha_eqvt_tac' _ = Skip_Proof.cheat_tac thy
+  val (bv_eqvt, lthy5) = prove_eqvt raw_tys induct_thm (raw_bn_eqs @ raw_perm_def) (map fst bns) lthy4
+  val (fv_eqvt, lthy6) = prove_eqvt raw_tys induct_thm (fv_def @ raw_perm_def) (fv @ fvbn) lthy5
+  fun alpha_eqvt_tac' _ =
+    if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
+    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_eq_iff_simp) lthy6 1
   val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
 
-  (* provind alpha equivalence *)
+  (* proving alpha equivalence *)
   val _ = warning "Proving equivalence";
   val fv_alpha_all = combine_fv_alpha_bns (fv, fvbn) (alpha_ts_nobn, alpha_ts_bn) bn_nos;
-  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct alpha_eq_iff lthy6;
+  val reflps = build_alpha_refl fv_alpha_all alpha_ts induct_thm alpha_eq_iff_simp lthy6;
   val alpha_equivp =
-    build_equivps alpha_ts reflps alpha_induct
-      inject alpha_eq_iff distincts alpha_cases alpha_eqvt lthy6;
+    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts
+    else build_equivps alpha_ts reflps alpha_induct
+      inject_thms alpha_eq_iff_simp distinct_thms alpha_cases alpha_eqvt lthy6;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
@@ -403,8 +455,8 @@
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
       map (fn (cname, dts) =>
-        Const (cname, map (typ_of_dtyp descr sorts) dts --->
-          typ_of_dtyp descr sorts (DtRec i))) l) descr);
+        Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+          Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = warning "Proving respects";
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
@@ -412,8 +464,9 @@
     fn (bn_t, _) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
-  (*val _ = map tracing (map PolyML.makestring fv_alpha_all);*)
-  fun fv_rsp_tac _ = Skip_Proof.cheat_tac thy
+
+  fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
+    else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
     (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
@@ -421,11 +474,14 @@
   val fv_rsp = flat (map snd fv_rsp_pre);
   val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
+  fun alpha_bn_rsp_tac _ = if !cheat_alpha_bn_rsp then Skip_Proof.cheat_tac thy
+    else
+      let val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff_simp @ rel_dists @ rel_dists_bn) alpha_equivp exhaust_thms alpha_ts_bn lthy11 in asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1 end;
   val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
-        (fn _ => Skip_Proof.cheat_tac thy)) alpha_ts_bn lthy11
+    alpha_bn_rsp_tac) alpha_ts_bn lthy11
   fun const_rsp_tac _ =
-    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
-      in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
+    let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff_simp alpha_ts_bn lthy11a
+      in constr_rsp_tac alpha_eq_iff_simp (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
     val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (fv @ fvbn)
@@ -445,7 +501,7 @@
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = warning "Lifting induction";
   val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
-  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct);
+  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct_thm);
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
   fun note_simp_suffix s th ctxt =
@@ -463,7 +519,7 @@
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = warning "Lifting eq-iff";
   (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
-  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
+  val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff_simp
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
   val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
@@ -487,11 +543,14 @@
   val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
   val (names, supp_eq_t) = supp_eq fv_alpha_all;
   val _ = warning "Support Equations";
-  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
+  fun supp_eq_tac' _ = if !cheat_supp_eq then Skip_Proof.cheat_tac thy else
+    supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1;
+  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t supp_eq_tac') handle e =>
+    let val _ = warning ("Support eqs failed") in [] end;
   val lthy23 = note_suffix "supp" q_supp lthy22;
 in
   (0, lthy23)
-end
+end handle TEST ctxt => (0, ctxt)
 *}
 
 section {* Preparing and parsing of the specification *}
@@ -660,6 +719,7 @@
   (main_parser >> nominal_datatype2_cmd)
 *}
 
+(*
 atom_decl name
 
 nominal_datatype lam =
@@ -676,6 +736,10 @@
   "bn (P1 x) = {atom x}"
 | "bn (P2 p1 p2) = bn p1 \<union> bn p2"
 
+find_theorems Var_raw
+
+
+
 thm lam_pt.bn
 thm lam_pt.fv[simplified lam_pt.supp(1-2)]
 thm lam_pt.eq_iff
@@ -740,7 +804,7 @@
 thm ty_tys.fv[simplified ty_tys.supp]
 thm ty_tys.eq_iff
 
-
+*)
 
 (* some further tests *)
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Parser.thy	Tue May 04 16:18:07 2010 +0200
@@ -1,8 +1,8 @@
 theory Parser
-imports "../Nominal-General/Nominal2_Atoms" 
-        "../Nominal-General/Nominal2_Eqvt" 
-        "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Equivp" "Rsp" "Lift"
+imports "../Nominal-General/Nominal2_Atoms"
+        "../Nominal-General/Nominal2_Eqvt"
+        "../Nominal-General/Nominal2_Supp"
+        "Perm" "Equivp" "Rsp" "Lift" "Fv"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -372,9 +372,9 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i);
   val raw_tys = map (fn (i, _) => nth_dtyp i) descr;
-  val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
+  val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames;
   val rel_dtinfos = List.take (dtinfos, (length dts));
@@ -423,8 +423,8 @@
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
       map (fn (cname, dts) =>
-        Const (cname, map (typ_of_dtyp descr sorts) dts --->
-          typ_of_dtyp descr sorts (DtRec i))) l) descr);
+        Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+          Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = tracing "Proving respects";
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
@@ -483,7 +483,7 @@
   val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
-  val _ = map tracing (map PolyML.makestring alpha_eq_iff);
+(*  val _ = map tracing (map PolyML.makestring alpha_eq_iff);*)
   val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas3}) alpha_eq_iff
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) eq_iff_unfolded0
   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas} ) eq_iff_unfolded1
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Perm.thy
--- a/Nominal/Perm.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Perm.thy	Tue May 04 16:18:07 2010 +0200
@@ -32,29 +32,29 @@
 
          permute_fn p arg
 
-    - in case the argument is non-recursive it will build
+    - in case the argument is non-recursive it will return
 
          p o arg
 
 *)
-fun perm_arg permute_fns pi (arg_dty, arg) =
+fun perm_arg permute_fn_frees p (arg_dty, arg) =
   if Datatype_Aux.is_rec_type arg_dty 
-  then Free (nth permute_fns (Datatype_Aux.body_index arg_dty)) $ pi $ arg
-  else mk_perm pi arg
+  then (nth permute_fn_frees (Datatype_Aux.body_index arg_dty)) $ p $ arg
+  else mk_perm p arg
 *}
 
 ML {*
-(* equation for permutation function for one constructor;
-   i is the index of the correspodning datatype *)
-fun perm_eq_constr dt_descr sorts permute_fns i (cnstr_name, dts) =
+(* generates the equation for the permutation function for one constructor;
+   i is the index of the corresponding datatype *)
+fun perm_eq_constr dt_descr sorts permute_fn_frees i (cnstr_name, dts) =
 let
-  val pi = Free ("p", @{typ perm})
+  val p = Free ("p", @{typ perm})
   val arg_tys = map (Datatype_Aux.typ_of_dtyp dt_descr sorts) dts
   val arg_names = Name.variant_list ["p"] (Datatype_Prop.make_tnames arg_tys)
   val args = map Free (arg_names ~~ arg_tys)
   val cnstr = Const (cnstr_name, arg_tys ---> (nth_dtyp dt_descr sorts i))
-  val lhs = Free (nth permute_fns i) $ pi $ list_comb (cnstr, args)
-  val rhs = list_comb (cnstr, map (perm_arg permute_fns pi) (dts ~~ args))
+  val lhs = (nth permute_fn_frees i) $ p $ list_comb (cnstr, args)
+  val rhs = list_comb (cnstr, map (perm_arg permute_fn_frees p) (dts ~~ args))
   val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 in
   (Attrib.empty_binding, eq)
@@ -87,13 +87,13 @@
 ML {*
 fun prove_permute_plus lthy induct perm_defs perm_fns =
 let
-  val pi1 = Free ("p", @{typ perm})
-  val pi2 = Free ("q", @{typ perm})
+  val p = Free ("p", @{typ perm})
+  val q = Free ("q", @{typ perm})
   val perm_types = map (body_type o fastype_of) perm_fns
   val perm_indnames = Datatype_Prop.make_tnames perm_types
   
-  fun single_goal ((perm, T), x) = HOLogic.mk_eq 
-      (perm $ (mk_plus pi1 pi2) $ Free (x, T), perm $ pi1 $ (perm $ pi2 $ Free (x, T)))
+  fun single_goal ((perm_fn, T), x) = HOLogic.mk_eq 
+      (perm_fn $ (mk_plus p q) $ Free (x, T), perm_fn $ p $ (perm_fn $ q $ Free (x, T)))
 
   val goals =
     HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj
@@ -113,37 +113,34 @@
 (* defines the permutation functions for raw datatypes and
    proves that they are instances of pt
 
-   dt_nos refers to the number of "un-unfolded" datatypes
+   user_dt_nos refers to the number of "un-unfolded" datatypes
    given by the user
 *)
-fun define_raw_perms (dt_info : Datatype_Aux.info) dt_nos thy =
+fun define_raw_perms dt_descr sorts induct_thm user_dt_nos thy =
 let
-  val {descr as dt_descr, induct, sorts, ...} = dt_info;
   val all_full_tnames = map (fn (_, (n, _, _)) => n) dt_descr;
-  val full_tnames = List.take (all_full_tnames, dt_nos);
+  val user_full_tnames = List.take (all_full_tnames, user_dt_nos);
 
   val perm_fn_names = prefix_dt_names dt_descr sorts "permute_"
-
-  val perm_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
-
-  val permute_fns = perm_fn_names ~~ perm_types
+  val perm_fn_types = map (fn (i, _) => perm_ty (nth_dtyp dt_descr sorts i)) dt_descr
+  val perm_fn_frees = map Free (perm_fn_names ~~ perm_fn_types)
 
   fun perm_eq (i, (_, _, constrs)) = 
-    map (perm_eq_constr dt_descr sorts permute_fns i) constrs;
+    map (perm_eq_constr dt_descr sorts perm_fn_frees i) constrs;
 
   val perm_eqs = maps perm_eq dt_descr;
 
   val lthy =
-    Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
+    Theory_Target.instantiation (user_full_tnames, [], @{sort pt}) thy;
    
-  val ((perm_fns, perm_ldef), lthy') =
+  val ((perm_funs, perm_eq_thms), lthy') =
     Primrec.add_primrec
       (map (fn s => (Binding.name s, NONE, NoSyn)) perm_fn_names) perm_eqs lthy;
     
-  val perm_zero_thms = prove_permute_zero lthy' induct perm_ldef perm_fns
-  val perm_plus_thms = prove_permute_plus lthy' induct perm_ldef perm_fns
-  val perm_zero_thms' = List.take (perm_zero_thms, dt_nos);
-  val perm_plus_thms' = List.take (perm_plus_thms, dt_nos)
+  val perm_zero_thms = prove_permute_zero lthy' induct_thm perm_eq_thms perm_funs
+  val perm_plus_thms = prove_permute_plus lthy' induct_thm perm_eq_thms perm_funs
+  val perm_zero_thms' = List.take (perm_zero_thms, user_dt_nos);
+  val perm_plus_thms' = List.take (perm_plus_thms, user_dt_nos)
   val perms_name = space_implode "_" perm_fn_names
   val perms_zero_bind = Binding.name (perms_name ^ "_zero")
   val perms_plus_bind = Binding.name (perms_name ^ "_plus")
@@ -158,10 +155,14 @@
   |> snd o (Local_Theory.note ((perms_zero_bind, []), perm_zero_thms'))
   |> snd o (Local_Theory.note ((perms_plus_bind, []), perm_plus_thms'))
   |> Class_Target.prove_instantiation_exit_result morphism tac 
-       (perm_ldef, perm_zero_thms' @ perm_plus_thms', perm_fns)
+       (perm_eq_thms, perm_zero_thms' @ perm_plus_thms', perm_funs)
 end
 *}
 
+
+
+
+
 (* permutations for quotient types *)
 
 ML {*
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Nominal/Rsp.thy
--- a/Nominal/Rsp.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Nominal/Rsp.thy	Tue May 04 16:18:07 2010 +0200
@@ -97,7 +97,7 @@
 ML {*
 fun alpha_eqvt_tac induct simps ctxt =
   rel_indtac induct THEN_ALL_NEW
-  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW
+  simp_tac (HOL_basic_ss addsimps simps) THEN_ALL_NEW split_conj_tac THEN_ALL_NEW
   REPEAT o etac @{thm exi[of _ _ "p"]} THEN' split_conj_tac THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps (all_eqvts ctxt @ simps)) THEN_ALL_NEW
   asm_full_simp_tac (HOL_ss addsimps 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Pearl-jv/Paper.thy
--- a/Pearl-jv/Paper.thy	Tue May 04 16:17:46 2010 +0200
+++ b/Pearl-jv/Paper.thy	Tue May 04 16:18:07 2010 +0200
@@ -2,7 +2,8 @@
 theory Paper
 imports "../Nominal-General/Nominal2_Base" 
         "../Nominal-General/Nominal2_Atoms" 
-        "../Nominal-General/Nominal2_Eqvt" 
+        "../Nominal-General/Nominal2_Eqvt"
+        "../Nominal-General/Nominal2_Supp" 
         "../Nominal-General/Atoms" 
         "LaTeXsugar"
 begin
@@ -43,24 +44,22 @@
 section {* Introduction *}
 
 text {*
+  The purpose of Nominal Isabelle is to provide a proving infratructure
+  for conveninet reasoning about programming languages. At its core
+  Nominal Isabelle is based on nominal logic by Pitts at al
+  \cite{GabbayPitts02,Pitts03}.  
+ 
   Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem
   prover providing a proving infrastructure for convenient reasoning about
-  programming languages. It has been used to formalise an equivalence checking
-  algorithm for LF \cite{UrbanCheneyBerghofer08}, 
-  Typed Scheme~\cite{TobinHochstadtFelleisen08}, several calculi for concurrency
-  \cite{BengtsonParrow07} and a strong normalisation result for
-  cut-elimination in classical logic \cite{UrbanZhu08}. It has also been used
-  by Pollack for formalisations in the locally-nameless approach to binding
-  \cite{SatoPollack10}.
+  programming languages. At its core Nominal Isabelle is based on the nominal
+  logic work of Pitts et al \cite{GabbayPitts02,Pitts03}.  The most basic
+  notion in this work is a sort-respecting permutation operation defined over
+  a countably infinite collection of sorted atoms. The atoms are used for
+  representing variables that might be bound. Multiple sorts are necessary for
+  being able to represent different kinds of variables. For example, in the
+  language Mini-ML there are bound term variables and bound type variables;
+  each kind needs to be represented by a different sort of atoms.
 
-  At its core Nominal Isabelle is based on the nominal logic work of Pitts et
-  al \cite{GabbayPitts02,Pitts03}.  The most basic notion in this work is a
-  sort-respecting permutation operation defined over a countably infinite
-  collection of sorted atoms. The atoms are used for representing variables
-  that might be bound. Multiple sorts are necessary for being
-  able to represent different kinds of variables. For example, in the language
-  Mini-ML there are bound term variables and bound type variables; each kind
-  needs to be represented by a different sort of atoms.
 
   Unfortunately, the type system of Isabelle/HOL is not a good fit for the way
   atoms and sorts are used in the original formulation of the nominal logic work.
@@ -858,9 +857,41 @@
   Cheney \cite{Cheney06} gives similar examples for constructions that have infinite support.
 *}
 
+section {* Support of Finite Sets *}
+
+text {*
+  Sets is one instance of a type that is not generally finitely supported. 
+  However, it can be easily derived that finite sets of atoms are finitely
+  supported, because their support can be characterised as:
+
+  \begin{lemma}\label{finatomsets}
+  If @{text S} is a finite set of atoms, then @{thm (concl) supp_finite_atom_set[no_vars]}.
+  \end{lemma}
+
+  \begin{proof}
+  finite-supp-unique
+  \end{proof}
+
+  More difficult is it to establish that finite sets of finitely 
+  supported objects are finitely supported. 
+*}
+
+
 section {* Induction Principles *}
 
+text {*
+  While the use of functions as permutation provides us with a unique
+  representation for permutations (for example @{term "(a \<rightleftharpoons> b)"} and 
+  @{term "(b \<rightleftharpoons> a)"} are equal permutations), this representation has 
+  one draw back: it does not come readily with an induction principle. 
+  Such an induction principle is handy for deriving properties like
+  
+  @{thm [display, indent=10] supp_perm_eq}
 
+  \noindent
+  However, it is not too difficult to derive an induction principle, 
+  given the fact that we allow only permutations with a finite domain. 
+*}
 
 
 section {* Concrete Atom Types *}
@@ -1167,6 +1198,12 @@
   HOL-based languages.
 *}
 
+section {* Related Work *}
+
+text {*
+  Add here comparison with old work.
+*}
+
 
 section {* Conclusion *}
 
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Pearl-jv/ROOT.ML
--- a/Pearl-jv/ROOT.ML	Tue May 04 16:17:46 2010 +0200
+++ b/Pearl-jv/ROOT.ML	Tue May 04 16:18:07 2010 +0200
@@ -1,6 +1,7 @@
 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 38bbccdf9ff9 -r 8bd75f2fd7b0 Pearl-jv/document/root.tex
--- a/Pearl-jv/document/root.tex	Tue May 04 16:17:46 2010 +0200
+++ b/Pearl-jv/document/root.tex	Tue May 04 16:18:07 2010 +0200
@@ -24,28 +24,21 @@
 
 \begin{document}
 
-\title{Proof Pearl: A New Foundation for Nominal Isabelle}
+\title{Implementing the Nominal Logic Work in Isabelle/HOL}
 \author{Brian Huffman\inst{1} and Christian Urban\inst{2}}
 \institute{Portland State University \and Technical University of Munich}
 \maketitle
 
 \begin{abstract}
 Pitts et al introduced a beautiful theory about names and binding based on the
-notions of permutation and support. The engineering challenge is to smoothly
-adapt this theory to a theorem prover environment, in our case Isabelle/HOL.
-We present a formalisation of this work that differs from our earlier approach
-in two important respects: First, instead of representing permutations as
-lists of pairs of atoms, we now use a more abstract representation based on
-functions.  Second, whereas the earlier work modeled different sorts of atoms
-using different types, we now introduce a unified atom type that includes all
-sorts of atoms. Interestingly, we allow swappings, that is permutations build from
-two atoms, to be ill-sorted.  As a result of these design changes, we can iron
-out inconveniences for the user, considerably simplify proofs and also
-drastically reduce the amount of custom ML-code. Furthermore we can extend the
-capabilities of Nominal Isabelle to deal with variables that carry additional
-information. We end up with a pleasing and formalised theory of permutations
-and support, on which we can build an improved and more powerful version of
-Nominal Isabelle.
+notions of atoms, permutations and support. The engineering challenge
+is to smoothly adapt this theory to a theorem prover environment, in our case
+Isabelle/HOL.  We present a formalisation of this work that is based on a
+unified atom type (that includes all sorts of atoms) and that represents
+permutations by bijective functions from atoms to atoms. Interestingly, we
+allow swappings, which are permutations build from two atoms, to be
+ill-sorted.  Furthermore we can extend the nominal logic with names that carry
+additional information.
 \end{abstract}
 
 % generated text of all theories
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 Quotient-Paper/document/root.tex
--- a/Quotient-Paper/document/root.tex	Tue May 04 16:17:46 2010 +0200
+++ b/Quotient-Paper/document/root.tex	Tue May 04 16:18:07 2010 +0200
@@ -13,13 +13,15 @@
 
 \begin{document}
 
-\title{Quotients Revisited}
+\title{Quotients Revisited for Isabelle/HOL}
 \author{Cezary Kaliszyk$^*$ and Christian Urban$^*$}
 \institute{$^*$ Technical University of Munich, Germany}
 \maketitle
 
 \begin{abstract}
-TBD
+Higher-order logic (HOL) is based on a safe logic kernel, which 
+can only be extended by introducing new definitions and new types. 
+
 \end{abstract}
 
 % generated text of all theories
diff -r 38bbccdf9ff9 -r 8bd75f2fd7b0 TODO
--- a/TODO	Tue May 04 16:17:46 2010 +0200
+++ b/TODO	Tue May 04 16:18:07 2010 +0200
@@ -14,6 +14,7 @@
 - types of bindings match types of binding functions
 - fsets are not bound in lst bindings
 - bound arguments are not datatypes
+- binder is referred to by name and not by type
 
 Smaller things: