equal
deleted
inserted
replaced
50 next |
50 next |
51 show "eqvt subst_graph" unfolding eqvt_def subst_graph_def |
51 show "eqvt subst_graph" unfolding eqvt_def subst_graph_def |
52 by (rule, perm_simp, rule) |
52 by (rule, perm_simp, rule) |
53 qed |
53 qed |
54 |
54 |
55 termination (eqvt) by lexicographic_order |
55 nominal_termination (eqvt) by lexicographic_order |
56 |
56 |
57 lemma forget[simp]: |
57 lemma forget[simp]: |
58 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
58 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
59 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
59 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
60 (auto simp add: lam.fresh fresh_at_base) |
60 (auto simp add: lam.fresh fresh_at_base) |