194 lemma subst_lemma_pre:

   195   "z \<sharp> (N,L) \<longrightarrow> z \<sharp> (subst [(y, L)] N)"

   196   apply (induct N rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])

   197   apply (simp add: s1)

   198   apply (auto simp add: fresh_Pair)

   199   apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])[3]

   200   apply (simp add: s2)

   201   apply (auto simp add: fresh_def ty_tys.fv[simplified ty_tys.supp])

   202   done

   203 

   204 lemma substs_lemma_pre:

   205   "atom z \<sharp> (N,L) \<longrightarrow> atom z \<sharp> (substs [(y, L)] N)"

   206   apply (rule strong_induct[of

   207     "\<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])

   208   apply clarify

   209   apply (subst s3)

   210   apply (simp add: fresh_star_def fresh_Cons fresh_Nil fresh_Pair)

   211   apply (simp_all add: fresh_star_prod_elim fresh_Pair)

   212   apply clarify

   213   apply (drule fresh_star_atom)

   214   apply (drule fresh_star_atom)

   215   apply (simp add: fresh_def)

   216   apply (simp only: ty_tys.fv[simplified ty_tys.supp])

   217   apply (subgoal_tac "atom a \<notin> supp (subst [(aa, b)] t)")

   218   apply blast

   219   apply (subgoal_tac "atom a \<notin> supp t")

   220   apply (fold fresh_def)[1]

   221   apply (rule mp[OF subst_lemma_pre])

   222   apply (simp add: fresh_Pair)

   223   apply (subgoal_tac "atom a \<notin> (fset_to_set (fmap atom fset))")

   224   apply blast

   225   apply (metis supp_finite_atom_set finite_fset)

   226   done

   227 

   228 lemma subst_lemma:

   229   shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>

   230     subst [(y, L)] (subst [(x, N)] M) =

   231     subst [(x, (subst [(y, L)] N))] (subst [(y, L)] M)"

   232   apply (induct M rule: ty_tys.induct[of _ "\<lambda>t. True" _ , simplified])

   233   apply (simp_all add: s1 s2)

   234   apply clarify

   235   apply (subst (2) subst_ty)

   236   apply simp_all

   237   done

   238 

   239 lemma substs_lemma:

   240   shows "x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>

   241     substs [(y, L)] (substs [(x, N)] M) =

   242     substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)"

   243   apply (rule strong_induct[of

   244     "\<lambda>a t. True" "\<lambda>(x, y, N, L) M. x \<noteq> y \<and> atom x \<sharp> L \<longrightarrow>

   245     substs [(y, L)] (substs [(x, N)] M) =

   246     substs [(x, (subst [(y, L)] N))] (substs [(y, L)] M)" _ _ "(x, y, N, L)", simplified])

   247   apply clarify

   248   apply (simp_all add: fresh_star_prod_elim fresh_Pair)

   249   apply (subst s3)

   250   apply (unfold fresh_star_def)[1]

   251   apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

   252   apply (subst s3)

   253   apply (unfold fresh_star_def)[1]

   254   apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

   255   apply (subst s3)

   256   apply (unfold fresh_star_def)[1]

   257   apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

   258   apply (subst s3)

   259   apply (unfold fresh_star_def)[1]

   260   apply (simp add: fresh_Cons fresh_Nil fresh_Pair)

   261   apply (rule ballI)

   262   apply (rule mp[OF subst_lemma_pre])

   263   apply (simp add: fresh_Pair)

   264   apply (subst subst_lemma)

   265   apply simp_all

   266   done

   267