155 fun

   156   lookup :: "(name \<times> ty) list \<Rightarrow> name \<Rightarrow> ty"

   157 where

   158   "lookup [] n = Var n"

   159 | "lookup ((p, s) # t) n = (if p = n then s else lookup t n)"

   160 

   161 locale subst_loc =

   162 fixes

   163     subst  :: "(name \<times> ty) list \<Rightarrow> ty \<Rightarrow> ty"

   164 and substs :: "(name \<times> ty) list \<Rightarrow> tys \<Rightarrow> tys"

   165 assumes

   166     s1: "subst \<theta> (Var n) = lookup \<theta> n"

   167 and s2: "subst \<theta> (Fun l r) = Fun (subst \<theta> l) (subst \<theta> r)"

   168 and s3: "fset_to_set (fmap atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All xs t) = All xs (subst \<theta> t)"

   169 begin

   170 

   171 lemma subst_ty:

   172   assumes x: "atom x \<sharp> t"

   173   shows "subst [(x, S)] t = t"

   174   using x

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

   176   by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base)

   177 

   178 lemma subst_tyS:

   179   shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T"

   180   apply (rule strong_induct[of

   181     "\<lambda>a t. True" "\<lambda>d T. (atom (fst d) \<sharp> T \<longrightarrow> substs [d] T = T)" _ "t" "(x, S)", simplified])

   182   apply (rule impI)

   183   apply (subst s3)

   184   apply (simp add: fresh_star_def fresh_Cons fresh_Nil)

   185   apply (case_tac b)

   186   apply clarify

   187   apply (subst subst_ty)

   188   apply simp_all

   189   apply (simp add: fresh_star_prod)

   190   apply clarify

   191   apply (thin_tac "fset_to_set (fmap atom fset) \<sharp>* ba")

   192   apply (drule fresh_star_atom)

   193   apply (unfold fresh_def)

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

   195   apply (subgoal_tac "atom aa \<notin> fset_to_set (fmap atom fset)")

   196   apply blast

   197   apply (metis supp_finite_atom_set finite_fset)

   198   done

   199 

   200 end

   201