95 apply(rule at_set_avoiding2) |
95 apply(rule at_set_avoiding2) |
96 apply(simp add: finite_supp) |
96 apply(simp add: finite_supp) |
97 apply(simp add: finite_supp) |
97 apply(simp add: finite_supp) |
98 apply(simp add: finite_supp) |
98 apply(simp add: finite_supp) |
99 apply(simp add: trm_assn.fresh fresh_star_def) |
99 apply(simp add: trm_assn.fresh fresh_star_def) |
100 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs, fv_bn assn) \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
100 apply(subgoal_tac "\<exists>q. (q \<bullet> (set (bn assn))) \<sharp>* (c::'a::fs) \<and> supp ([bn assn]lst.trm) \<sharp>* q") |
101 apply(erule exE) |
101 apply(erule exE) |
102 apply(erule conjE) |
102 apply(erule conjE) |
|
103 apply(subgoal_tac "-q \<bullet> (\<forall>assn trm. (set (bn assn) \<sharp>* c \<and> y = Let assn trm) \<longrightarrow> P)") |
|
104 apply(perm_simp add: trm_assn.fv_bn_eqvt) |
|
105 (* HERE *) |
|
106 |
|
107 |
|
108 |
103 apply(simp add: set_eqvt) |
109 apply(simp add: set_eqvt) |
104 apply(subst (asm) tt) |
110 apply(subst (asm) tt) |
105 apply(rule_tac assms(4)) |
111 apply(rule_tac assms(4)) |
106 apply(simp add: fresh_star_prod) |
112 apply(simp add: fresh_star_prod) |
107 apply(erule conjE) |
|
108 apply(assumption) |
|
109 apply(simp) |
113 apply(simp) |
110 apply(simp add: trm_assn.eq_iff) |
114 apply(simp add: trm_assn.eq_iff) |
111 apply(drule supp_perm_eq[symmetric]) |
115 apply(drule supp_perm_eq[symmetric]) |
112 apply(simp) |
116 apply(simp) |
113 apply(simp add: tt uu) |
117 apply(simp add: tt uu) |