--- a/Nominal/Ex/TypeSchemes.thy	Tue May 25 17:01:37 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 25 17:09:29 2010 +0200
@@ -152,6 +152,53 @@
   apply auto
   done
 
+fun
+  lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"
+where
+  "lookup [] n = Var n"
+| "lookup ((p, s) # t) n = (if p = n then s else lookup t n)"
+
+locale subst_loc =
+fixes
+    subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"
+and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"
+assumes
+    s1: "subst \<theta> (Var n) = lookup \<theta> n"
+and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)"
+and s3: "fset_to_set (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"
+begin
+
+lemma subst_ty:
+  assumes x: "atom x \<sharp> t"
+  shows "subst [(x, S)] t = t"
+  using x
+  apply (induct t rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
+  by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base)
+
+lemma subst_tyS:
+  shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T"
+  apply (rule strong_induct[of
+    "\<lambda>a t. True" "\<lambda>d T. (atom (fst d) \<sharp> T \<longrightarrow> substs [d] T = T)" _ "t" "(x, S)", simplified])
+  apply (rule impI)
+  apply (subst s3)
+  apply (simp add: fresh_star_def fresh_Cons fresh_Nil)
+  apply (case_tac b)
+  apply clarify
+  apply (subst subst_ty)
+  apply simp_all
+  apply (simp add: fresh_star_prod)
+  apply clarify
+  apply (thin_tac "fset_to_set (fmap atom fset) \<sharp>* ba")
+  apply (drule fresh_star_atom)
+  apply (unfold fresh_def)
+  apply (simp only: ty_tys.fv[simplified ty_tys.supp])
+  apply (subgoal_tac "atom aa \<notin> fset_to_set (fmap atom fset)")
+  apply blast
+  apply (metis supp_finite_atom_set finite_fset)
+  done
+
+end
+
 (* PROBLEM:
 Type schemes with separate datatypes