172 apply (simp add: fresh_star_permute_iff)

   172 apply (simp add: fresh_star_permute_iff)

   173 apply(perm_simp)

   173 apply(perm_simp)

   174 apply(assumption)

   174 apply(assumption)

   175 apply(simp)

   175 apply(simp)

   176 --"Eqvt done"

   176 --"Eqvt done"

   177 apply (case_tac x)

   178 apply (case_tac x)

   178 apply simp apply clarify 

   179 apply simp apply clarify 

   179 apply (rule_tac y="b" in ty_tys.exhaust(1))

   180 apply (rule_tac y="b" in ty_tys.exhaust(1))

   180 apply (auto)[1]

   181 apply (auto)[1]

   181 apply (auto)[1]

   182 apply (auto)[1]

   342 where

   343 where

   343   "subst \<theta> (Var2 X) = lookup2 \<theta> X"

   344   "subst \<theta> (Var2 X) = lookup2 \<theta> X"

   344 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"

   345 | "subst \<theta> (Fun2 T1 T2) = Fun2 (subst \<theta> T1) (subst \<theta> T2)"

   345   unfolding eqvt_def subst_graph_def

   346   unfolding eqvt_def subst_graph_def

   346   apply (rule, perm_simp, rule)

   347   apply (rule, perm_simp, rule)

   347   apply(case_tac x)

   349   apply(case_tac x)

   348   apply(simp)

   350   apply(simp)

   349   apply(rule_tac y="b" in ty2.exhaust)

   351   apply(rule_tac y="b" in ty2.exhaust)

   350   apply(blast)

   352   apply(blast)

   351   apply(blast)

   353   apply(blast)

   382   substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"

   384   substs :: "(name \<times> ty2) list \<Rightarrow> tys2 \<Rightarrow> tys2"

   383 where

   385 where

   384   "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"

   386   "fset (map_fset atom xs) \<sharp>* \<theta> \<Longrightarrow> substs \<theta> (All2 xs t) = All2 xs (subst \<theta> t)"

   385   unfolding eqvt_def substs_graph_def

   387   unfolding eqvt_def substs_graph_def

   386   apply (rule, perm_simp, rule)

   388   apply (rule, perm_simp, rule)

   388   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)

   390   apply (rule_tac y="b" and c="a" in tys2.strong_exhaust)

   389   apply auto

   391   apply auto

   390   apply (subst (asm) Abs_eq_res_set)

   392   apply (subst (asm) Abs_eq_res_set)

   391   apply (subst (asm) Abs_eq_iff2)

   393   apply (subst (asm) Abs_eq_iff2)

   392   apply (clarify)

   394   apply (clarify)