--- a/LMCS-Paper/Paper.thy	Thu Dec 29 18:05:13 2011 +0000
+++ b/LMCS-Paper/Paper.thy	Mon Jan 02 16:13:16 2012 +0000
@@ -114,7 +114,11 @@
   and the @{text "\<forall>"}-quantification binds a finite (possibly empty) set of
   type-variables.  While it is possible to implement this kind of more general
   binders by iterating single binders, this leads to a rather clumsy
-  formalisation of W. The need of iterating single binders is also one reason
+  formalisation of W. 
+
+  {\bf add example about W}
+
+  The need of iterating single binders is also one reason
   why Nominal Isabelle and similar theorem provers that only provide
   mechanisms for binding single variables have not fared extremely well with
   the more advanced tasks in the POPLmark challenge \cite{challenge05},

--- a/LMCS-Review	Thu Dec 29 18:05:13 2011 +0000
+++ b/LMCS-Review	Mon Jan 02 16:13:16 2012 +0000
@@ -49,7 +49,11 @@
 > algorithm W [...]."  But there is no analysis in the paper of what was
 > hard in algorithm W coded with single binders, or explanation of how
 > it would be done in the new system reported in this paper showing why
-> the new approach works better in practice.  Although this example is
+> the new approach works better in practice.  
+
+Added
+
+> Although this example is
 > one of the main motivations given for the work, there is apparently no
 > formalization of algorithm W in the library of examples that comes
 > with Nominal2 described in this paper.  I think that should be
@@ -59,24 +63,35 @@
 > binding single variables have not fared extremely well with the more
 > advanced tasks in the POPLmark challenge [2], because also there one
 > would like to bind multiple variables at once.").
->
+
+No time to provide full examples yet. They will be provided
+once Nominal2 becomes more mature and people are using it
+and help to provide theories.
+
 > The new Isabelle package "Nominal2", described in this paper, is not
 > ready for users without a lot of hand-holding from the Nominal2
 > developers.  This paper would have more impact if interested users
 > could try the tool without so much difficulty.
->
+
+The plan is to have Nominal Isabelle be part of the next stable 
+release of Isabelle, which should be out before the summer 2012.
+At the moment it can be downloaded as a bundle and is ready
+to be used (we have confirmation from two groups for this). 
+
 > A few more specific points:
 >
 > Bottom of p.7: I don't understand the paragraph containing equations
 > (2.4) and (2.5).
->
+
+
 > Bottom of p.9: The parameters R and fa of the alpha equivalence
 > relation are dropped in the examples, so the examples are not clear.
 > I think there is a typo in the first example: "It can be easily
 > checked that ({x,y},x->y) and ({y,x},y->x) are alpha-equivalent [...]"
 > Did you mean "({x,y},x->y) and ({y,x},x->y) are alpha-equivalent"?
->
->
+
+
+
 > Referee no 2:
 >
 >  * The paper can be accepted for Logical Methods in Computer Science 

--- a/Nominal/Ex/TypeSchemes.thy	Thu Dec 29 18:05:13 2011 +0000
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,441 +0,0 @@
-theory TypeSchemes
-imports "../Nominal2"
-begin
-
-section {*** Type Schemes ***}
-
-atom_decl name 
-
-(* defined as a single nominal datatype *)
-
-nominal_datatype ty =
-  Var "name"
-| Fun "ty" "ty"
-and tys =
-  All xs::"name fset" ty::"ty" binds (set+) xs in ty
-
-ML {*
-get_all_info @{context}
-*}
-
-ML {*
-get_info @{context} "TypeSchemes.ty"
-*}
-
-ML {*
-#strong_exhaust (the_info @{context} "TypeSchemes.tys")
-*}
-
-thm ty_tys.distinct
-thm ty_tys.induct
-thm ty_tys.inducts
-thm ty_tys.exhaust 
-thm ty_tys.strong_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.supp
-thm ty_tys.fresh
-
-fun
-  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
-where
-  "lookup [] Y = Var Y"
-| "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
-
-lemma lookup_eqvt[eqvt]:
-  shows "(p \<bullet> lookup Ts T) = lookup (p \<bullet> Ts) (p \<bullet> T)"
-apply(induct Ts T rule: lookup.induct)
-apply(simp_all)
-done
-
-lemma TEST1:
-  assumes "x = Inl y"
-  shows "(p \<bullet> Sum_Type.Projl x) = Sum_Type.Projl (p \<bullet> x)"
-using assms by simp
-
-lemma TEST2:
-  assumes "x = Inr y"
-  shows "(p \<bullet> Sum_Type.Projr x) = Sum_Type.Projr (p \<bullet> x)"
-using assms by simp
-
-lemma test:
-  assumes a: "\<exists>y. f x = Inl y"
-  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl ((p \<bullet> f) (p \<bullet> x))"
-using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
-
-lemma test2:
-  assumes a: "\<exists>y. f x = Inl y"
-  shows "(p \<bullet> (Sum_Type.Projl (f x))) = Sum_Type.Projl (p \<bullet> (f x))"
-using a
-apply clarify
-apply(frule_tac p="p" in permute_boolI)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst (asm) permute_fun_app_eq)
-back
-apply(simp)
-done
-
-nominal_primrec (default "sum_case (\<lambda>x. Inl undefined) (\<lambda>x. Inr undefined)")
-    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
-and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
-where
-  "subst \<theta> (Var X) = lookup \<theta> X"
-| "subst \<theta> (Fun T1 T2) = Fun (subst \<theta> T1) (subst \<theta> T2)"
-| "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs T) = All xs (subst \<theta> T)"
-(*unfolding subst_substs_graph_def eqvt_def
-apply rule
-apply perm_simp
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply (subst test3)
-defer
-apply rule*)
-thm subst_substs_graph.intros
-apply(subgoal_tac "\<And>p x r. subst_substs_graph x r \<Longrightarrow> subst_substs_graph (p \<bullet> x) (p \<bullet> r)")
-apply(simp add: eqvt_def)
-apply(rule allI)
-apply(simp add: permute_fun_def permute_bool_def)
-apply(rule ext)
-apply(rule ext)
-apply(rule iffI)
-apply(drule_tac x="p" in meta_spec)
-apply(drule_tac x="- p \<bullet> x" in meta_spec)
-apply(drule_tac x="- p \<bullet> xa" in meta_spec)
-apply(simp)
-apply(drule_tac x="-p" in meta_spec)
-apply(drule_tac x="x" in meta_spec)
-apply(drule_tac x="xa" in meta_spec)
-apply(simp)
---"Eqvt One way"
-apply(erule subst_substs_graph.induct)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(rotate_tac 1)
-apply(erule subst_substs_graph.cases)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(subst test)
-back
-apply (rule exI)
-apply(assumption)
-apply(perm_simp)
-apply(rule subst_substs_graph.intros)
-apply(assumption)
-apply(assumption)
-apply(simp)
---"A"
-apply(simp)
-apply(erule subst_substs_graph.cases)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp (no_asm_use) only: eqvts)
-apply(subst test)
-back
-back
-apply (rule exI)
-apply(assumption)
-apply(rule subst_substs_graph.intros)
-apply (simp add: eqvts)
-apply (subgoal_tac "(p \<bullet> (atom ` fset xs)) \<sharp>* (p \<bullet> \<theta>)")
-apply (simp add: image_eqvt eqvts_raw eqvts)
-apply (simp add: fresh_star_permute_iff)
-apply(perm_simp)
-apply(assumption)
-apply(simp)
---"Eqvt done"
-apply(rule TrueI)
-apply (case_tac x)
-apply simp apply clarify 
-apply (rule_tac y="b" in ty_tys.exhaust(1))
-apply (auto)[1]
-apply (auto)[1]
-apply simp apply clarify 
-apply (rule_tac ya="b" and c="a" in ty_tys.strong_exhaust(2))
-apply (auto)[1]
-apply (auto)[5]
---"LAST GOAL"
-apply (simp add: meta_eq_to_obj_eq[OF subst_def, symmetric, unfolded fun_eq_iff])
-apply (subgoal_tac "eqvt_at (\<lambda>(l, r). subst l r) (\<theta>', T)")
-apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', T))")
-apply (thin_tac "eqvt_at subst_substs_sumC (Inl (\<theta>', Ta))")
-prefer 2
-apply (simp add: eqvt_at_def subst_def)
-apply rule
-apply (subst test2)
-apply (simp add: subst_substs_sumC_def)
-apply (simp add: THE_default_def)
-apply (case_tac "Ex1 (subst_substs_graph (Inl (\<theta>', T)))")
-prefer 2
-apply simp
-apply (simp add: the1_equality)
-apply auto[1]
-apply (erule_tac x="x" in allE)
-apply simp
-apply(cases rule: subst_substs_graph.cases)
-apply assumption
-apply (rule_tac x="lookup \<theta> X" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply (rule_tac x="(Fun (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T1))))
-                  (Sum_Type.Projl (subst_substs_sum (Inl (\<theta>, T2)))))" in exI)
-apply clarify
-apply (rule the1_equality)
-apply blast apply assumption
-apply clarify
-apply simp
---"-"
-apply clarify
-  apply (frule supp_eqvt_at)
-  apply (simp add: finite_supp)
-  apply (erule Abs_res_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply (simp add: Abs_fresh_iff)
-  apply auto[1]
-  apply (simp add: fresh_def fresh_star_def)
-  apply (erule contra_subsetD)
-  apply (simp add: supp_Pair)
-  apply blast
-  apply clarify
-  apply (simp)
-  apply (simp add: eqvt_at_def)
-  apply (subst Abs_eq_iff)
-  apply (rule_tac x="0::perm" in exI)
-  apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
-  apply (simp add: alphas fresh_star_zero)
-  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
-  apply blast
-  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
-  apply (simp add: supp_Pair eqvts eqvts_raw)
-  apply auto[1]
-  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
-  apply (simp add: fresh_star_def fresh_def)
-  apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
-  apply (simp add: eqvts eqvts_raw)
-  apply (simp add: fresh_star_def fresh_def)
-  apply (simp (no_asm) only: supp_eqvt[symmetric] Pair_eqvt[symmetric])
-  apply (subgoal_tac "p \<bullet> supp (subst \<theta>' T) \<subseteq> p \<bullet> supp (\<theta>', T)")
-  apply (erule subsetD)
-  apply (simp add: supp_eqvt)
-  apply (metis le_eqvt permute_boolI)
-  apply (rule perm_supp_eq)
-  apply (simp add: fresh_def fresh_star_def)
-  apply blast
-  done
-
-
-termination (eqvt) by lexicographic_order
-
-
-section {* defined as two separate nominal datatypes *}
-
-nominal_datatype ty2 =
-  Var2 "name"
-| Fun2 "ty2" "ty2"
-
-nominal_datatype tys2 =
-  All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty
-
-thm tys2.distinct
-thm tys2.induct tys2.strong_induct
-thm tys2.exhaust tys2.strong_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.supp
-thm tys2.fresh
-
-fun
-  lookup2 :: "(name \<times> ty2) list \<Rightarrow> name \<Rightarrow> ty2"
-where
-  "lookup2 [] Y = Var2 Y"
-| "lookup2 ((X, T) # Ts) Y = (if X = Y then T else lookup2 Ts Y)"
-
-lemma lookup2_eqvt[eqvt]:
-  shows "(p \<bullet> lookup2 Ts T) = lookup2 (p \<bullet> Ts) (p \<bullet> T)"
-  by (induct Ts T rule: lookup2.induct) simp_all
-
-nominal_primrec
-  subst2  :: "(name \<times> ty2) list \<Rightarrow> ty2 \<Rightarrow> ty2"
-where
-  "subst2 \<theta> (Var2 X) = lookup2 \<theta> X"
-| "subst2 \<theta> (Fun2 T1 T2) = Fun2 (subst2 \<theta> T1) (subst2 \<theta> T2)"
-  unfolding eqvt_def subst2_graph_def
-  apply (rule, perm_simp, rule)
-  apply(rule TrueI)
-  apply(case_tac x)
-  apply(rule_tac y="b" in ty2.exhaust)
-  apply(blast)
-  apply(blast)
-  apply(simp_all add: ty2.distinct)
-  done
-
-termination (eqvt)
-  by lexicographic_order
-
-
-lemma supp_fun_app2_eqvt:
-  assumes e: "eqvt f"
-  shows "supp (f a b) \<subseteq> supp a \<union> supp b"
-  using supp_fun_app_eqvt[OF e] supp_fun_app
-  by blast
- 
-lemma supp_subst:
-  "supp (subst2 \<theta> t) \<subseteq> supp \<theta> \<union> supp t"
-  apply (rule supp_fun_app2_eqvt)
-  unfolding eqvt_def by (simp add: eqvts_raw)
- 
-lemma fresh_star_inter1:
-  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
-  unfolding fresh_star_def by blast
-
-nominal_primrec
-  substs2 :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"
-where
-  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs2 \<theta> (All2 xs t) = All2 xs (subst2 \<theta> t)"
-  unfolding eqvt_def substs2_graph_def
-  apply (rule, perm_simp, rule)
-  apply auto[2]
-  apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)
-  apply auto[1]
-  apply(simp)
-  apply(erule conjE)
-  apply (erule Abs_res_fcb)
-  apply (simp add: Abs_fresh_iff)
-  apply(simp add: fresh_def)
-  apply(simp add: supp_Abs)
-  apply(rule impI)
-  apply(subgoal_tac "x \<notin> supp \<theta>")
-  prefer 2
-  apply(auto simp add: fresh_star_def fresh_def)[1]
-  apply(subgoal_tac "x \<in> supp t")
-  using supp_subst
-  apply(blast)
-  using supp_subst
-  apply(blast)
-  apply clarify
-  apply (simp add: subst2.eqvt)
-  apply (subst Abs_eq_iff)
-  apply (rule_tac x="0::perm" in exI)
-  apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
-  apply (simp add: alphas fresh_star_zero)
-  apply (subgoal_tac "\<And>x. x \<in> supp (subst2 \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
-  apply blast
-  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
-  apply (simp add: supp_Pair eqvts eqvts_raw)
-  apply auto[1]
-  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
-  apply (simp add: fresh_star_def fresh_def)
-  apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
-  apply (simp add: eqvts eqvts_raw)
-  apply (simp add: fresh_star_def fresh_def)
-  apply (drule subsetD[OF supp_subst])
-  apply (simp add: supp_Pair)
-  apply (rule perm_supp_eq)
-  apply (simp add: fresh_def fresh_star_def)
-  apply blast
-  done
-
-text {* Some Tests about Alpha-Equality *}
-
-lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
-  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def ty_tys.supp 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 Abs_eq_iff)
-  apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
-  apply(simp add: alphas fresh_star_def supp_at_base ty_tys.supp)
-  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 Abs_eq_iff)
-  apply(rule_tac x="0::perm" in exI)
-  apply(simp add: alphas fresh_star_def ty_tys.supp supp_at_base)
-done
-
-lemma
-  assumes a: "a \<noteq> b"
-  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
-  using a
-  apply(simp add: ty_tys.eq_iff Abs_eq_iff)
-  apply(clarify)
-  apply(simp add: alphas fresh_star_def ty_tys.eq_iff ty_tys.supp supp_at_base)
-  apply auto
-  done
-
-
-
-
-end

--- a/Nominal/Ex/TypeSchemes1.thy	Thu Dec 29 18:05:13 2011 +0000
+++ b/Nominal/Ex/TypeSchemes1.thy	Mon Jan 02 16:13:16 2012 +0000
@@ -8,10 +8,10 @@
 
 nominal_datatype ty =
   Var "name"
-| Fun "ty" "ty"
+| Fun "ty" "ty" ("_ \<rightarrow> _")
 
 nominal_datatype tys =
-  All xs::"name fset" ty::"ty" binds (set+) xs in ty
+  All xs::"name fset" ty::"ty" binds (set+) xs in ty ("All [_]._")
 
 thm tys.distinct
 thm tys.induct tys.strong_induct
@@ -26,9 +26,13 @@
 thm tys.supp
 thm tys.fresh
 
+subsection {* Substitution function for types and type schemes *}
+
+type_synonym 
+  Subst = "(name \<times> ty) list"
 
 fun
-  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+  lookup :: "Subst \<Rightarrow> name \<Rightarrow> ty"
 where
   "lookup [] Y = Var Y"
 | "lookup ((X, T) # Ts) Y = (if X = Y then T else lookup Ts Y)"
@@ -41,10 +45,10 @@
 
 
 nominal_primrec
-  subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
+  subst  :: "Subst \<Rightarrow> ty \<Rightarrow> ty" ("_<_>" [100,60] 120)
 where
-  "subst \<theta> (Var X) = lookup \<theta> X"
-| "subst \<theta> (Fun T1 T) = Fun (subst \<theta> T1) (subst \<theta> T)"
+  "\<theta><Var X> = lookup \<theta> X"
+| "\<theta><T1 \<rightarrow> T2> = (\<theta><T1>) \<rightarrow> (\<theta><T2>)"
   unfolding eqvt_def subst_graph_def
   apply (rule, perm_simp, rule)
   apply(rule TrueI)
@@ -58,7 +62,6 @@
 termination (eqvt)
   by lexicographic_order
 
-
 lemma supp_fun_app_eqvt:
   assumes e: "eqvt f"
   shows "supp (f a b) \<subseteq> supp a \<union> supp b"
@@ -71,14 +74,10 @@
   unfolding eqvt_def 
   by (simp add: permute_fun_def subst.eqvt)
  
-lemma fresh_star_inter1:
-  "xs \<sharp>* z \<Longrightarrow> (xs \<inter> ys) \<sharp>* z"
-  unfolding fresh_star_def by blast
-
 nominal_primrec
-  substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
+  substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys" ("_<_>" [100,60] 120)
 where
-  "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
+  "fset (map_fset atom Xs) \<sharp>* \<theta> \<Longrightarrow> \<theta><All [Xs].T> = All [Xs].(\<theta><T>)"
   unfolding eqvt_def substs_graph_def
   apply (rule, perm_simp, rule)
   apply auto[2]
@@ -94,7 +93,7 @@
   apply(subgoal_tac "x \<notin> supp \<theta>")
   prefer 2
   apply(auto simp add: fresh_star_def fresh_def)[1]
-  apply(subgoal_tac "x \<in> supp t")
+  apply(subgoal_tac "x \<in> supp T")
   using supp_subst
   apply(blast)
   using supp_subst
@@ -105,12 +104,12 @@
   apply (rule_tac x="0::perm" in exI)
   apply (subgoal_tac "p \<bullet> \<theta>' = \<theta>'")
   apply (simp add: alphas fresh_star_zero)
-  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> t)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset xs \<longleftrightarrow> x \<in> atom ` fset xsa")
+  apply (subgoal_tac "\<And>x. x \<in> supp (subst \<theta>' (p \<bullet> T)) \<Longrightarrow> x \<in> p \<bullet> atom ` fset Xs \<longleftrightarrow> x \<in> atom ` fset Xsa")
   apply blast
-  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> t)")
+  apply (subgoal_tac "x \<in> supp(p \<bullet> \<theta>', p \<bullet> T)")
   apply (simp add: supp_Pair eqvts eqvts_raw)
   apply auto[1]
-  apply (subgoal_tac "(atom ` fset (p \<bullet> xs)) \<sharp>* \<theta>'")
+  apply (subgoal_tac "(atom ` fset (p \<bullet> Xs)) \<sharp>* \<theta>'")
   apply (simp add: fresh_star_def fresh_def)
   apply(drule_tac p1="p" in iffD2[OF fresh_star_permute_iff])
   apply (simp add: eqvts eqvts_raw)
@@ -125,21 +124,21 @@
 text {* Some Tests about Alpha-Equality *}
 
 lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|b, a|} (Fun (Var a) (Var b))"
+  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|b, a|}]. ((Var a) \<rightarrow> (Var b))"
   apply(simp add: Abs_eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
   done
 
 lemma
-  shows "All {|a, b|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var b) (Var a))"
+  shows "All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var b) \<rightarrow> (Var a))"
   apply(simp add: Abs_eq_iff)
   apply(rule_tac x="(atom a \<rightleftharpoons> atom b)" in exI)
   apply(simp add: alphas fresh_star_def supp_at_base ty.supp)
   done
 
 lemma
-  shows "All {|a, b, c|} (Fun (Var a) (Var b)) = All {|a, b|} (Fun (Var a) (Var b))"
+  shows "All [{|a, b, c|}].((Var a) \<rightarrow> (Var b)) = All [{|a, b|}].((Var a) \<rightarrow> (Var b))"
   apply(simp add: Abs_eq_iff)
   apply(rule_tac x="0::perm" in exI)
   apply(simp add: alphas fresh_star_def ty.supp supp_at_base)
@@ -147,7 +146,7 @@
 
 lemma
   assumes a: "a \<noteq> b"
-  shows "\<not>(All {|a, b|} (Fun (Var a) (Var b)) = All {|c|} (Fun (Var c) (Var c)))"
+  shows "\<not>(All [{|a, b|}].((Var a) \<rightarrow> (Var b)) = All [{|c|}].((Var c) \<rightarrow> (Var c)))"
   using a
   apply(simp add: Abs_eq_iff)
   apply(clarify)
@@ -156,6 +155,215 @@
   done
 
 
+text {* HERE *}
+
+fun 
+  compose::"Subst \<Rightarrow> Subst \<Rightarrow> Subst" ("_ \<circ> _" [100,100] 100)
+where
+  "\<theta>\<^isub>1 \<circ> [] = \<theta>\<^isub>1"
+| "\<theta>\<^isub>1 \<circ> ((X,T)#\<theta>\<^isub>2) = (X,\<theta>\<^isub>1<T>)#(\<theta>\<^isub>1 \<circ> \<theta>\<^isub>2)"
+
+lemma compose_eqvt:
+  fixes  \<theta>1 \<theta>2::"Subst"
+  shows "(p \<bullet> (\<theta>1 \<circ> \<theta>2)) = ((p \<bullet> \<theta>1) \<circ> (p \<bullet> \<theta>2))"
+apply(induct \<theta>2) 
+apply(auto simp add: subst.eqvt)
+done
+
+lemma compose_ty:
+  fixes  \<theta>1 :: "Subst"
+  and    \<theta>2 :: "Subst"
+  and    T :: "ty"
+  shows "\<theta>1<\<theta>2<T>> = (\<theta>1\<circ>\<theta>2)<T>"
+proof (induct T rule: ty.induct)
+  case (Var X) 
+  have "\<theta>1<lookup \<theta>2 X> = lookup (\<theta>1\<circ>\<theta>2) X" 
+    by (induct \<theta>2) (auto)
+  then show ?case by simp
+next
+  case (Fun T1 T2)
+  then show ?case by simp
+qed
+
+fun
+  dom :: "Subst \<Rightarrow> name fset"
+where
+  "dom [] = {||}"
+| "dom ((X,T)#\<theta>) = {|X|} |\<union>| dom \<theta>"
+
+lemma dom_eqvt[eqvt]:
+  shows "(p \<bullet> dom \<theta>) = dom (p \<bullet> \<theta>)"
+apply(induct \<theta> rule: dom.induct)
+apply(simp_all)
+done
+
+nominal_primrec
+  ftv  :: "ty \<Rightarrow> name fset"
+where
+  "ftv (Var X) = {|X|}"
+| "ftv (T1 \<rightarrow> T2) = (ftv T1) |\<union>| (ftv T2)"
+  unfolding eqvt_def ftv_graph_def
+  apply (rule, perm_simp, rule)
+  apply(auto)[2]
+  apply(rule_tac y="x" in ty.exhaust)
+  apply(blast)
+  apply(blast)
+  apply(simp_all)
+  done
+
+termination (eqvt)
+  by lexicographic_order
+
+lemma s1:
+  fixes T::"ty"
+  shows "(X \<leftrightarrow> Y) \<bullet> T = [(X, Var Y),(Y, Var X)]<T>"
+apply(induct T rule: ty.induct)
+apply(simp_all)
+done
+
+lemma s2:
+  fixes T::"ty"
+  shows "[]<T> = T"
+apply(induct T rule: ty.induct)
+apply(simp_all)
+done
+
+lemma perm_struct_induct_name[case_names pure zero swap]:
+  assumes pure: "supp p \<subseteq> atom ` (UNIV::name set)"
+  and     zero: "P 0"
+  and     swap: "\<And>p a b::name. \<lbrakk>P p; a \<noteq> b\<rbrakk> \<Longrightarrow> P ((a \<leftrightarrow> b) + p)"
+  shows "P p"
+apply(rule_tac S="supp p \<inter> atom ` (UNIV::name set)" in perm_struct_induct)
+using pure
+apply(auto)[1]
+apply(rule zero)
+apply(auto)
+apply(simp add: flip_def[symmetric])
+apply(rule swap)
+apply(auto)
+done
+
+lemma s3:
+  fixes T::"ty"
+  assumes "supp p \<subseteq> atom ` (UNIV::name set)"
+  shows "\<exists>\<theta>. p \<bullet> T = \<theta><T>"
+apply(induct p rule: perm_struct_induct_name)
+apply(rule assms)
+apply(simp)
+apply(rule_tac x="[]" in exI)
+apply(simp add: s2)
+apply(clarify)
+apply(simp) 
+apply(rule_tac x="[(a, Var b),(b, Var a)] \<circ> \<theta>" in exI)
+apply(simp add: compose_ty[symmetric])
+apply(simp add: s1)
+done
+
+lemma s4:
+  fixes x::"'a::fs"
+  assumes "supp x \<subseteq> atom ` (UNIV::name set)"
+  shows "\<exists>q. p \<bullet> x = q \<bullet> x \<and> supp q \<subseteq> atom ` (UNIV::name set)"
+apply(induct p rule: perm_simple_struct_induct)
+apply(rule_tac x="0" in exI)
+apply(auto)[1]
+apply(simp add: supp_zero_perm)
+apply(auto)[1]
+apply(case_tac "supp (a \<rightleftharpoons> b) \<subseteq> range atom")
+apply(rule_tac x="(a \<rightleftharpoons> b) + q" in exI)
+apply(simp)
+apply(rule subset_trans)
+apply(rule supp_plus_perm)
+apply(simp)
+apply(rule_tac x="q" in exI)
+apply(simp)
+apply(rule swap_fresh_fresh)
+apply(simp add: fresh_permute_left)
+apply(subst perm_supp_eq)
+apply(simp add: supp_swap)
+apply(simp add: supp_minus_perm)
+apply(simp add: fresh_star_def fresh_def)
+apply(simp add: supp_atom)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+apply(simp add: supp_swap)
+using assms
+apply(simp add: fresh_def)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+apply(simp add: fresh_permute_left)
+apply(subst perm_supp_eq)
+apply(simp add: supp_swap)
+apply(simp add: supp_minus_perm)
+apply(simp add: fresh_star_def fresh_def)
+apply(simp add: supp_atom)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+apply(simp add: supp_swap)
+using assms
+apply(simp add: fresh_def)
+apply(auto)[1]
+apply (metis atom_eqvt image_iff rangeI subsetD swap_atom_simps(2))
+done
+
+lemma s5:
+  fixes T::"ty"
+  shows "supp T \<subseteq> atom ` (UNIV::name set)"
+apply(induct T rule: ty.induct)
+apply(auto simp add: ty.supp supp_at_base)
+done
+
+function
+  generalises :: "ty \<Rightarrow> tys \<Rightarrow> bool" ("_ \<prec>\<prec> _")
+where
+  "T \<prec>\<prec> All [Xs].T' \<longleftrightarrow> (\<exists>\<theta>. \<theta><T'> = T)"
+  apply auto[1]
+  apply (rule_tac y="b" in tys.exhaust)
+  apply auto[1]
+  apply(simp)
+  apply(clarify)
+  apply(rule iffI)
+  apply(clarify)
+  apply(drule sym)
+  apply(simp add: Abs_eq_iff2)
+  apply(simp add: alphas)
+  apply(clarify)
+  using s4[OF s5]
+  apply -
+  apply(drule_tac x="p" in meta_spec)
+  apply(drule_tac x="T'a" in meta_spec)
+  apply(clarify)
+  apply(simp)
+  using s3
+  apply -
+  apply(drule_tac x="q" in meta_spec)
+  apply(drule_tac x="T'a" in meta_spec)
+  apply(drule meta_mp)
+  apply(simp)
+  apply(clarify)
+  apply(simp)
+  apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI)
+  apply(simp add: compose_ty)
+  apply(auto)
+  apply(simp add: Abs_eq_iff2)
+  apply(simp add: alphas)
+  apply(clarify)
+  apply(drule_tac x="p" in meta_spec)
+  apply(drule_tac x="T'" in meta_spec)
+  apply(clarify)
+  apply(simp)
+  apply(drule_tac x="q" in meta_spec)
+  apply(drule_tac x="T'" in meta_spec)
+  apply(drule meta_mp)
+  apply(simp)
+  apply(clarify)
+  apply(simp)
+  apply(rule_tac x="\<theta> \<circ> \<theta>'" in exI)
+  apply(simp add: compose_ty)
+  done
+
+
+
+
 
 
 end