176 by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base) |
176 by (simp_all add: s1 s2 fresh_def ty_tys.fv[simplified ty_tys.supp] supp_at_base) |
177 |
177 |
178 lemma subst_tyS: |
178 lemma subst_tyS: |
179 shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T" |
179 shows "atom x \<sharp> T \<longrightarrow> substs [(x, S)] T = T" |
180 apply (rule strong_induct[of |
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]) |
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 (rule impI) |
182 apply clarify |
183 apply (subst s3) |
183 apply (subst s3) |
184 apply (simp add: fresh_star_def fresh_Cons fresh_Nil) |
184 apply (simp add: fresh_star_def fresh_Cons fresh_Nil) |
185 apply (case_tac b) |
|
186 apply clarify |
|
187 apply (subst subst_ty) |
185 apply (subst subst_ty) |
188 apply simp_all |
186 apply (simp_all add: fresh_star_prod_elim) |
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) |
187 apply (drule fresh_star_atom) |
193 apply (unfold fresh_def) |
188 apply (simp add: fresh_def ty_tys.fv[simplified ty_tys.supp]) |
194 apply (simp only: ty_tys.fv[simplified ty_tys.supp]) |
189 apply (subgoal_tac "atom a \<notin> fset_to_set (fmap atom fset)") |
195 apply (subgoal_tac "atom aa \<notin> fset_to_set (fmap atom fset)") |
|
196 apply blast |
190 apply blast |
197 apply (metis supp_finite_atom_set finite_fset) |
191 apply (metis supp_finite_atom_set finite_fset) |
198 done |
192 done |
199 |
193 |
200 end |
194 end |