equal
deleted
inserted
replaced
138 defer |
138 defer |
139 apply(auto simp add: lam.distinct lam.eq_iff) |
139 apply(auto simp add: lam.distinct lam.eq_iff) |
140 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
140 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
141 apply(blast)+ |
141 apply(blast)+ |
142 apply(simp add: fresh_star_def) |
142 apply(simp add: fresh_star_def) |
143 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t \<and> atom x \<sharp> [[atom xa]]lst. ta") |
143 apply(subgoal_tac "atom xa \<sharp> [[atom x]]lst. t") |
144 apply(subst (asm) Abs_eq_iff2) |
144 apply(subst (asm) Abs_eq_iff2) |
145 apply(simp add: alphas atom_eqvt) |
145 apply(simp add: alphas atom_eqvt) |
146 apply(clarify) |
146 apply(clarify) |
147 apply(rule trans) |
147 apply(rule trans) |
148 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
148 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
166 apply(simp add: atom_eqvt eqvt_at_def) |
166 apply(simp add: atom_eqvt eqvt_at_def) |
167 apply(rule perm_supp_eq) |
167 apply(rule perm_supp_eq) |
168 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
168 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
169 apply(rule perm_supp_eq) |
169 apply(rule perm_supp_eq) |
170 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
170 apply(auto simp add: fresh_star_def fresh_Pair)[1] |
171 apply(rule conjI) |
|
172 apply(simp add: Abs_fresh_iff) |
|
173 apply(drule sym) |
|
174 apply(simp add: Abs_fresh_iff) |
171 apply(simp add: Abs_fresh_iff) |
175 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
172 apply(subgoal_tac "\<And>p x r. subst_graph x r \<Longrightarrow> subst_graph (p \<bullet> x) (p \<bullet> r)") |
176 unfolding eqvt_def |
173 unfolding eqvt_def |
177 apply(rule allI) |
174 apply(rule allI) |
178 apply(simp add: permute_fun_def) |
175 apply(simp add: permute_fun_def) |