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>(x, S) T. (atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T)" _ "t" "(x, S)", simplified])

   182   apply clarify

   183   apply (subst s3)

   184   apply (simp add: fresh_star_def fresh_Cons fresh_Nil)

   185   apply (subst subst_ty)

   186   apply (simp_all add: fresh_star_prod_elim)

   187   apply (drule fresh_star_atom)

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

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

   190   apply blast

   191   apply (metis supp_finite_atom_set finite_fset)

   192   done

   193 

   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 

   268 end

   269