334 

   335 ML {* Sign.of_sort @{theory} (@{typ t}, @{sort fs}) *}

   336 ML {* Sign.of_sort @{theory} (@{typ tyS}, @{sort fs}) *}

   337 

   338 lemma supp_fv_t_tyS:

   339   shows "supp T = fv_t T" 

   340   and   "supp S = fv_tyS S"

   341 apply(induct T and S rule: t_tyS_inducts)

   342 apply(simp_all add: t_tyS_fv)

   343 (* VarTS case *)

   344 apply(simp only: supp_def)

   345 apply(simp only: t_tyS_perm)

   346 apply(simp only: t_tyS_inject)

   347 apply(simp only: supp_def[symmetric])

   348 apply(simp only: supp_at_base)

   349 (* FunTS case *)

   350 apply(simp only: supp_def)

   351 apply(simp only: t_tyS_perm)

   352 apply(simp only: t_tyS_inject)

   353 apply(simp only: de_Morgan_conj)

   354 apply(simp only: Collect_disj_eq)

   355 apply(simp only: infinite_Un)

   356 apply(simp only: Collect_disj_eq)

   357 (* All case *)

   358 apply(rule_tac t="supp (All fun t_raw)" and s="supp (Abs (atom ` fun) t_raw)" in subst)

   359 apply(simp (no_asm) only: supp_def)

   360 apply(simp only: t_tyS_perm)

   361 apply(simp only: permute_ABS)

   362 apply(simp only: t_tyS_inject)

   363 apply(simp only: Abs_eq_iff)

   364 apply(simp only: insert_eqvt atom_eqvt empty_eqvt image_eqvt atom_eqvt_raw)

   365 apply(simp only: alpha_gen)

   366 apply(simp only: supp_eqvt[symmetric])

   367 apply(simp only: eqvts)

   368 oops

   369 (*apply(simp only: supp_Abs)

   370 done*)