--- a/Nominal/Ex/TypeSchemes.thy	Tue May 25 17:29:05 2010 +0200
+++ b/Nominal/Ex/TypeSchemes.thy	Tue May 25 18:38:52 2010 +0200
@@ -191,6 +191,80 @@
   apply (metis supp_finite_atom_set finite_fset)
   done
 
+lemma subst_lemma_pre:
+  "z \<sharp> (N,L) \<longrightarrow> z \<sharp> (subst [(y, L)] N)"
+  apply (induct N rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
+  apply (simp add: s1)
+  apply (auto simp add: fresh_Pair)
+  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])[3]
+  apply (simp add: s2)
+  apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])
+  done
+
+lemma substs_lemma_pre:
+  "atom z \<sharp> (N,L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N)"
+  apply (rule strong_induct[of
+    "\<lambda>a t. True" "\<lambda>(z, y, L) N. (atom z \<sharp> (N, L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N))" _ _ "(z, y, L)", simplified])
+  apply clarify
+  apply (subst s3)
+  apply (simp add: fresh_star_def fresh_Cons fresh_Nil fresh_Pair)
+  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
+  apply clarify
+  apply (drule fresh_star_atom)
+  apply (drule fresh_star_atom)
+  apply (simp add: fresh_def)
+  apply (simp only: ty_tys.fv[simplified ty_tys.supp])
+  apply (subgoal_tac "atom a \<notin> supp (subst [(aa, b)] t)")
+  apply blast
+  apply (subgoal_tac "atom a \<notin> supp t")
+  apply (fold fresh_def)[1]
+  apply (rule mp[OF subst_lemma_pre])
+  apply (simp add: fresh_Pair)
+  apply (subgoal_tac "atom a \<notin> (fset_to_set (fmap atom fset))")
+  apply blast
+  apply (metis supp_finite_atom_set finite_fset)
+  done
+
+lemma subst_lemma:
+  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
+    subst [(y, L)] (subst [(x, N)] M) =
+    subst [(x, (subst [(y, L)] N))] (subst [(y, L)] M)"
+  apply (induct M rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])
+  apply (simp_all add: s1 s2)
+  apply clarify
+  apply (subst (2) subst_ty)
+  apply simp_all
+  done
+
+lemma substs_lemma:
+  shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
+    substs [(y, L)] (substs [(x, N)] M) =
+    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)"
+  apply (rule strong_induct[of
+    "\<lambda>a t. True" "\<lambda>(x, y, N, L) M. x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>
+    substs [(y, L)] (substs [(x, N)] M) =
+    substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" _ _ "(x, y, N, L)", simplified])
+  apply clarify
+  apply (simp_all add: fresh_star_prod_elim fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (subst s3)
+  apply (unfold fresh_star_def)[1]
+  apply (simp add: fresh_Cons fresh_Nil fresh_Pair)
+  apply (rule ballI)
+  apply (rule mp[OF subst_lemma_pre])
+  apply (simp add: fresh_Pair)
+  apply (subst subst_lemma)
+  apply simp_all
+  done
+
 end
 
 (* PROBLEM: