equal
deleted
inserted
replaced
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) \<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 |
|
109 apply(simp add: set_eqvt) |
103 apply(simp add: set_eqvt) |
110 apply(subst (asm) tt) |
104 apply(subst (asm) tt) |
111 apply(rule_tac assms(4)) |
105 apply(rule_tac assms(4)) |
112 apply(simp add: fresh_star_prod) |
|
113 apply(simp) |
106 apply(simp) |
114 apply(simp add: trm_assn.eq_iff) |
107 apply(simp add: trm_assn.eq_iff) |
115 apply(drule supp_perm_eq[symmetric]) |
108 apply(drule supp_perm_eq[symmetric]) |
116 apply(simp) |
109 apply(simp) |
117 apply(simp add: tt uu) |
110 apply(simp add: tt uu) |