--- a/Nominal/Ex/CPS/Lt.thy Fri Jul 22 11:52:12 2011 +0100
+++ b/Nominal/Ex/CPS/Lt.thy Sun Jul 24 07:54:54 2011 +0200
@@ -33,13 +33,7 @@
apply (simp_all add: swap_fresh_fresh)
done
-termination
- by (relation "measure (\<lambda>(t, _, _). size t)")
- (simp_all add: lt.size)
-
-lemma subst_eqvt[eqvt]:
- shows "p\<bullet>(M[V/(x::name)]) = (p\<bullet>M)[(p\<bullet>V)/(p\<bullet>x)]"
- by (induct M V x rule: subst.induct) (simp_all)
+termination (eqvt) by lexicographic_order
lemma forget[simp]:
shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M"
@@ -60,9 +54,8 @@
by (perm_simp, auto)
(erule lt.exhaust, auto)
-termination
- by (relation "measure size")
- (simp_all add: lt.size)
+termination (eqvt)
+ by (relation "measure size") (simp_all)
lemma is_Value_eqvt[eqvt]:
shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)"