equal
deleted
inserted
replaced
275 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
275 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
276 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
276 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
277 unfolding eqvt_def subst_graph_def |
277 unfolding eqvt_def subst_graph_def |
278 apply (rule, perm_simp, rule) |
278 apply (rule, perm_simp, rule) |
279 apply(rule TrueI) |
279 apply(rule TrueI) |
280 apply(auto simp add: lam.distinct lam.eq_iff) |
280 apply(auto) |
281 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
281 apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
282 apply(blast)+ |
282 apply(blast)+ |
283 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
283 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
284 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
284 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
285 apply(simp_all add: Abs_fresh_iff) |
285 apply(simp_all add: Abs_fresh_iff) |
400 assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2" |
400 assumes a: "t1 \<longrightarrow>1 t2" "s1 \<longrightarrow>1 s2" |
401 shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]" |
401 shows "App (Lam [x]. t1) s1 \<longrightarrow>1 t2[ x ::= s2]" |
402 proof - |
402 proof - |
403 obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh) |
403 obtain y::"name" where fs: "atom y \<sharp> (x, t1, s1, t2, s2)" by (rule obtain_fresh) |
404 have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs |
404 have "App (Lam [x]. t1) s1 = App (Lam [y]. ((y \<leftrightarrow> x) \<bullet> t1)) s1" using fs |
405 by (auto simp add: lam.eq_iff Abs1_eq_iff' flip_def fresh_Pair fresh_at_base) |
405 by (auto simp add: Abs1_eq_iff' flip_def fresh_Pair fresh_at_base) |
406 also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt) |
406 also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt) |
407 also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric]) |
407 also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric]) |
408 finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp |
408 finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp |
409 qed |
409 qed |
410 |
410 |