equal
deleted
inserted
replaced
167 where |
167 where |
168 "(Var x)[y ::== s] = (if x = y then s else (Var x))" |
168 "(Var x)[y ::== s] = (if x = y then s else (Var x))" |
169 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])" |
169 | "(App t1 t2)[y ::== s] = App (t1[y ::== s]) (t2[y ::== s])" |
170 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])" |
170 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::== s] = Lam [x].(t[y ::== (App (Var y) s)])" |
171 apply(simp add: eqvt_def subst'_graph_def) |
171 apply(simp add: eqvt_def subst'_graph_def) |
172 apply (rule, perm_simp, rule) |
172 apply(perm_simp, simp) |
173 apply(rule TrueI) |
173 apply(rule TrueI) |
174 apply(case_tac x) |
174 apply(case_tac x) |
175 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
175 apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust) |
176 apply(auto simp add: fresh_star_def)[3] |
176 apply(auto simp add: fresh_star_def)[3] |
177 apply(simp_all) |
177 apply(simp_all) |