15 where |
15 where |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
16 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])" |
19 unfolding eqvt_def subst_graph_def |
19 unfolding eqvt_def subst_graph_def |
20 apply (rule, perm_simp, rule) |
20 apply (simp) |
21 apply(rule TrueI) |
21 apply(rule TrueI) |
22 apply(auto simp add: lt.distinct lt.eq_iff) |
22 apply(auto simp add: lt.distinct lt.eq_iff) |
23 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
23 apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust) |
24 apply blast |
24 apply blast |
25 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
25 apply(simp_all add: fresh_star_def fresh_Pair_elim) |
26 apply blast |
26 apply blast |
27 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
27 apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2) |
28 apply(simp_all add: Abs_fresh_iff) |
28 apply(simp add: Abs_fresh_iff) |
29 apply(simp add: fresh_star_def fresh_Pair) |
29 apply(simp add: fresh_star_def fresh_Pair) |
30 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)+ |
30 apply(simp add: eqvt_at_def) |
|
31 apply(simp add: perm_supp_eq fresh_star_Pair) |
|
32 apply(simp add: eqvt_at_def) |
|
33 apply(simp add: perm_supp_eq fresh_star_Pair) |
31 done |
34 done |
32 |
35 |
33 termination (eqvt) by lexicographic_order |
36 termination (eqvt) by lexicographic_order |
34 |
37 |
35 lemma forget[simp]: |
38 lemma forget[simp]: |