# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1313725778 -32400
# Node ID f0fab367453a2528f5f097b62a679b31d89cc497
# Parent  132575f5bd26310a6d24c0b5c43248ca3042e2ec
Use same constructor names as Lambda, remove copies of FCB, remove [eqvt].

diff -r 132575f5bd26 -r f0fab367453a Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Fri Aug 19 11:07:17 2011 +0900
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Fri Aug 19 12:49:38 2011 +0900
@@ -3,111 +3,13 @@
 imports Lt
 begin
 
-lemma Abs_lst_fcb2:
-  fixes as bs :: "atom list"
-    and x y :: "'b :: fs"
-    and c::"'c::fs"
-  assumes eq: "[as]lst. x = [bs]lst. y"
-  and fcb1: "(set as) \<sharp>* c \<Longrightarrow> (set as) \<sharp>* f as x c"
-  and fresh1: "set as \<sharp>* c"
-  and fresh2: "set bs \<sharp>* c"
-  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"
-  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"
-  shows "f as x c = f bs y c"
-proof -
-  have "supp (as, x, c) supports (f as x c)"
-    unfolding  supports_def fresh_def[symmetric]
-    by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)
-  then have fin1: "finite (supp (f as x c))"
-    by (auto intro: supports_finite simp add: finite_supp)
-  have "supp (bs, y, c) supports (f bs y c)"
-    unfolding  supports_def fresh_def[symmetric]
-    by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)
-  then have fin2: "finite (supp (f bs y c))"
-    by (auto intro: supports_finite simp add: finite_supp)
-  obtain q::"perm" where 
-    fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and 
-    fr2: "supp q \<sharp>* Abs_lst as x" and 
-    inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)"
-    using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"]  
-      fin1 fin2
-    by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)
-  have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp
-  also have "\<dots> = Abs_lst as x"
-    by (simp only: fr2 perm_supp_eq)
-  finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp
-  then obtain r::perm where 
-    qq1: "q \<bullet> x = r \<bullet> y" and 
-    qq2: "q \<bullet> as = r \<bullet> bs" and 
-    qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs"
-    apply(drule_tac sym)
-    apply(simp only: Abs_eq_iff2 alphas)
-    apply(erule exE)
-    apply(erule conjE)+
-    apply(drule_tac x="p" in meta_spec)
-    apply(simp add: set_eqvt)
-    apply(blast)
-    done
-  have "(set as) \<sharp>* f as x c" 
-    apply(rule fcb1)
-    apply(rule fresh1)
-    done
-  then have "q \<bullet> ((set as) \<sharp>* f as x c)"
-    by (simp add: permute_bool_def)
-  then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"
-    apply(simp add: fresh_star_eqvt set_eqvt)
-    apply(subst (asm) perm1)
-    using inc fresh1 fr1
-    apply(auto simp add: fresh_star_def fresh_Pair)
-    done
-  then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
-  then have "r \<bullet> ((set bs) \<sharp>* f bs y c)"
-    apply(simp add: fresh_star_eqvt set_eqvt)
-    apply(subst (asm) perm2[symmetric])
-    using qq3 fresh2 fr1
-    apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)
-    done
-  then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def)
-  have "f as x c = q \<bullet> (f as x c)"
-    apply(rule perm_supp_eq[symmetric])
-    using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def)
-  also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" 
-    apply(rule perm1)
-    using inc fresh1 fr1 by (auto simp add: fresh_star_def)
-  also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp
-  also have "\<dots> = r \<bullet> (f bs y c)"
-    apply(rule perm2[symmetric])
-    using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)
-  also have "... = f bs y c"
-    apply(rule perm_supp_eq)
-    using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)
-  finally show ?thesis by simp
-qed
-
-lemma Abs_lst1_fcb2:
-  fixes a b :: "atom"
-    and x y :: "'b :: fs"
-    and c::"'c :: fs"
-  assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)"
-  and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c"
-  and fresh: "{a, b} \<sharp>* c"
-  and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"
-  and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c"
-  shows "f a x c = f b y c"
-using e
-apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"])
-apply(simp_all)
-using fcb1 fresh perm1 perm2
-apply(simp_all add: fresh_star_def)
-done
-
 nominal_primrec
   CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
 where
-  "atom k \<sharp> x \<Longrightarrow> (x~)* = (Abs k ((k~) $ (x~)))"
-| "atom k \<sharp> (x, M) \<Longrightarrow> (Abs x M)* = Abs k (k~ $ Abs x (M*))"
+  "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $ (x~)))"
+| "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $ Lam x (M*))"
 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
-    (M $ N)* = Abs k (M* $ Abs m (N* $ Abs n (m~ $ n~ $ k~)))"
+    (M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))"
 unfolding eqvt_def CPS_graph_def
 apply (rule, perm_simp, rule, rule)
 apply (simp_all add: fresh_Pair_elim)
@@ -123,7 +25,7 @@
 apply (simp add: fresh_Pair_elim fresh_at_base)
 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
 --"-"
-apply(rule_tac s="[[atom ka]]lst. ka~ $ Abs x (CPS_sumC M)" in trans)
+apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
 apply (case_tac "k = ka")
 apply simp
 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
@@ -155,7 +57,7 @@
 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
 
-termination (eqvt) by (relation "measure size") (simp_all)
+termination (eqvt) by lexicographic_order
 
 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
 
@@ -170,7 +72,7 @@
   convert:: "lt => lt" ("_+" [250] 250)
 where
   "(Var x)+ = Var x"
-| "(Abs x M)+ = Abs x (M*)"
+| "(Lam x M)+ = Lam x (M*)"
 | "(M $ N)+ = M $ N"
   unfolding convert_graph_def eqvt_def
   apply (rule, perm_simp, rule, rule)
@@ -195,20 +97,16 @@
   shows "isValue (p \<bullet> (M::lt)) = isValue M"
   by (nominal_induct M rule: lt.strong_induct) auto
 
-lemma [eqvt]:
-  shows "p \<bullet> isValue M = isValue (p \<bullet> M)"
-  by (induct M rule: lt.induct) (perm_simp, rule refl)+
-
 nominal_primrec
   Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)
 where
-  "Kapply (Abs x M) K = K $ (Abs x M)+"
+  "Kapply (Lam x M) K = K $ (Lam x M)+"
 | "Kapply (Var x) K = K $ Var x"
 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"
 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
-    Kapply (M $ N) K = N; (Abs n (M+ $ Var n $ K))"
+    Kapply (M $ N) K = N; (Lam n (M+ $ Var n $ K))"
 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
-    Kapply (M $ N) K = M; (Abs m (N*  $ (Abs n (Var m $ Var n $ K))))"
+    Kapply (M $ N) K = M; (Lam m (N*  $ (Lam n (Var m $ Var n $ K))))"
   unfolding Kapply_graph_def eqvt_def
   apply (rule, perm_simp, rule, rule)
 apply (simp_all)
@@ -225,10 +123,10 @@
 apply (simp add: fresh_Pair_elim fresh_at_base)
 apply (auto simp add: Abs1_eq_iff eqvts)[1]
 apply (rename_tac M N u K)
-apply (subgoal_tac "Abs n (M+ $ n~ $ K) =  Abs u (M+ $ u~ $ K)")
+apply (subgoal_tac "Lam n (M+ $ n~ $ K) =  Lam u (M+ $ u~ $ K)")
 apply (simp only:)
 apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]
-apply (subgoal_tac "Abs m (Na* $ Abs n (m~ $ n~ $ Ka)) = Abs ma (Na* $ Abs na (ma~ $ na~ $ Ka))")
+apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
 apply (simp only:)
 apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)
 apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")
@@ -254,14 +152,14 @@
 lemma value_CPS:
   assumes "isValue V"
   and "atom a \<sharp> V"
-  shows "V* = Abs a (a~ $ V+)"
+  shows "V* = Lam a (a~ $ V+)"
   using assms
 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh)
   fix name :: name and lt aa
-  assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Abs b (b~ $ lt+)"
+  assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $ lt+)"
     "atom aa \<sharp> lt \<or> aa = name"
   obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast
-  show "Abs name lt* = Abs aa (aa~ $ Abs name (lt*))" using a b
+  show "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b
     by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
 qed
 
@@ -269,28 +167,28 @@
 
 lemma CPS_subst_fv:
   assumes *:"isValue V"
-  shows "((M[V/x])* = (M*)[V+/x])"
+  shows "((M[x ::= V])* = (M*)[x ::= V+])"
 using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct)
   case (Var name)
   assume *: "isValue V"
   obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast
-  show "((name~)[V/x])* = (name~)*[V+/x]" using a
+  show "((name~)[x ::= V])* = (name~)*[x ::= V+]" using a
     by (simp add: fresh_at_base * value_CPS)
 next
-  case (Abs name lt V x)
-  assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[b/ba])* = lt*[b+/ba]"
+  case (Lam name lt V x)
+  assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[ba ::= b])* = lt*[ba ::= b+]"
     "isValue V"
-  obtain a :: name where a: "atom a \<sharp> (name, lt, lt[V/x], x, V)" using obtain_fresh by blast
-  show "(Abs name lt[V/x])* = Abs name lt*[V+/x]" using * a
+  obtain a :: name where a: "atom a \<sharp> (name, lt, lt[x ::= V], x, V)" using obtain_fresh by blast
+  show "(Lam name lt[x ::= V])* = Lam name lt*[x ::= V+]" using * a
     by (simp add: fresh_at_base)
 next
   case (App lt1 lt2 V x)
-  assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[b/ba])* = lt1*[b+/ba]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[b/ba])* = lt2*[b+/ba]"
+  assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[ba ::= b])* = lt1*[ba ::= b+]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[ba ::= b])* = lt2*[ba ::= b+]"
     "isValue V"
-  obtain a :: name where a: "atom a \<sharp> (lt1[V/x], lt1, lt2[V/x], lt2, V, x)" using obtain_fresh by blast
-  obtain b :: name where b: "atom b \<sharp> (lt2[V/x], lt2, a, V, x)" using obtain_fresh by blast
+  obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast
+  obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], lt2, a, V, x)" using obtain_fresh by blast
   obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast
-  show "((lt1 $ lt2)[V/x])* = (lt1 $ lt2)*[V+/x]" using * a b c
+  show "((lt1 $ lt2)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c
     by (simp add: fresh_at_base)
 qed
 
@@ -312,7 +210,7 @@
   assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K"
   obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast
   then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis
-  show "Abs name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Abs name (lt*)" using * a b
+  show "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b
     by simp (rule evbeta', simp_all)
 next
   fix lt1 lt2 K
@@ -322,24 +220,24 @@
   obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast
   have d: "atom a \<sharp> lt1" "atom a \<sharp> lt2" "atom a \<sharp> K" "atom b \<sharp> lt1" "atom b \<sharp> lt2" "atom b \<sharp> K" "atom b \<sharp> a"
     "atom c \<sharp> lt1" "atom c \<sharp> lt2" "atom c \<sharp> K" "atom c \<sharp> a" "atom c \<sharp> b" using fresh_Pair a b c by simp_all
-  have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K))" using * d
+  have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d
     by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base)
   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1")
     assume e: "isValue lt1"
-    have "lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (lt2* $ Abs c (b~ $ c~ $ K)) $ lt1+"
+    have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
       using * d e by simp
-    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Abs c (lt1+ $ c~ $ K)"
+    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
       by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base)
     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
       assume f: "isValue lt2"
-      have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
+      have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K"
         by (rule evbeta', simp_all add: d e f)
       finally show ?thesis using * d e f by simp
     next
       assume f: "\<not> isValue lt2"
-      have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs c (lt1+ $ c~ $ K)" using * d e f by simp
-      also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis
+      have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp
+      also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis
       finally show ?thesis using * d e f by simp
     qed
     finally show ?thesis .
@@ -355,11 +253,11 @@
   case (evbeta x V M)
   fix K
   assume a: "isValue K" "isValue V" "atom x \<sharp> V"
-  have "Abs x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M*)[V+/x] $ K)"
+  have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)"
     by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)
-  also have "... = ((M[V/x])* $ K)" by (simp add: CPS_subst_fv a)
-  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (M[V/x] ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
-  finally show "(Abs x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  (M[V/x] ; K)" using a by simp
+  also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a)
+  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
+  finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  ((M[x ::= V]) ; K)" using a by simp
 next
   case (ev1 V M N)
   fix V M N K
@@ -370,7 +268,7 @@
     then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp
   next
     assume n: "isValue N"
-    have c: "M; Abs a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs a (V+ $ a~ $ K) $ N+" using a b by (simp add: n)
+    have c: "M; Lam a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam a (V+ $ a~ $ K) $ N+" using a b by (simp add: n)
     also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n)
     finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n)
   qed
@@ -381,19 +279,19 @@
   obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast
   have d: "atom a \<sharp> K" "atom a \<sharp> M" "atom a \<sharp> N" "atom a \<sharp> M'" "atom b \<sharp> a" "atom b \<sharp> K"
     "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all
-  have "M $ N ; K  \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Abs a (N* $ Abs b (a~ $ b~ $ K))" using * d by simp
+  have "M $ N ; K  \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp
   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'")
     assume "\<not> isValue M'"
     then show ?thesis using * d by (simp_all add: evs1)
   next
     assume e: "isValue M'"
-    then have "M' ; Abs a (N* $ Abs b (a~ $ b~ $ K)) = Abs a (N* $ Abs b (a~ $ b~ $ K)) $ M'+" by simp
-    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Abs b (a~ $ b~ $ K))[M'+/a]"
+    then have "M' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp
+    also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]"
       by (rule evbeta') (simp_all add: fresh_at_base e d)
-    also have "... = N* $ Abs b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base)
+    also have "... = N* $ Lam b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base)
     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N")
       assume f: "isValue N"
-      have "N* $ Abs b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (M'+ $ b~ $ K) $ N+"
+      have "N* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+"
         by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1)
       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1)
       finally show ?thesis .
@@ -415,17 +313,17 @@
 
 lemma
   assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"
-  shows "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
+  shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
 proof-
   obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast
-  have e: "Abs x (x~) = Abs y (y~)"
+  have e: "Lam x (x~) = Lam y (y~)"
     by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
-  have "M* $ Abs x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Abs x (x~)"
+  have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
     by(rule CPS_eval_Kapply,simp_all add: assms)
-  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Abs x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
-  also have "... = V ; Abs y (y~)" using e by (simp only:)
+  also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
+  also have "... = V ; Lam y (y~)" using e by (simp only:)
   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *)
-  finally show "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
+  finally show "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
 qed
 
 end
diff -r 132575f5bd26 -r f0fab367453a Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Fri Aug 19 11:07:17 2011 +0900
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Fri Aug 19 12:49:38 2011 +0900
@@ -7,7 +7,7 @@
   Hole
 | CFun cpsctxt lt
 | CArg lt cpsctxt
-| CAbs x::name c::cpsctxt bind x in c
+| CAbs x::name c::cpsctxt binds x in c
 
 nominal_primrec
   fill   :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt"         ("_<_>" [200, 200] 100)
@@ -15,7 +15,7 @@
   fill_hole : "Hole<M> = M"
 | fill_fun  : "(CFun C N)<M> = (C<M>) $ N"
 | fill_arg  : "(CArg N C)<M> = N $ (C<M>)"
-| fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Abs x (C<M>)"
+| fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
   unfolding eqvt_def fill_graph_def
   apply perm_simp
   apply auto
@@ -29,11 +29,7 @@
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   done
 
-termination
-  by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
-
-lemma [eqvt]: "p \<bullet> fill c t = fill (p \<bullet> c) (p \<bullet> t)"
-  by (nominal_induct c avoiding: t rule: cpsctxt.strong_induct) simp_all
+termination (eqvt) by lexicographic_order
 
 nominal_primrec
   ccomp :: "cpsctxt => cpsctxt => cpsctxt"
@@ -56,20 +52,16 @@
   apply (simp add: eqvt_at_def swap_fresh_fresh)
   done
 
-termination
-  by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
-
-lemma [eqvt]: "p \<bullet> ccomp c c' = ccomp (p \<bullet> c) (p \<bullet> c')"
-  by (nominal_induct c avoiding: c' rule: cpsctxt.strong_induct) simp_all
+termination (eqvt) by lexicographic_order
 
 nominal_primrec
     CPSv :: "lt => lt"
 and CPS :: "lt => cpsctxt" where
   "CPSv (Var x) = x~"
 | "CPS (Var x) = CFun Hole (x~)"
-| "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))"
-| "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))"
-| "CPSv (M $ N) = Abs x (Var x)"
+| "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))"
+| "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))"
+| "CPSv (M $ N) = Lam x (Var x)"
 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole"
 | "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> M \<Longrightarrow> CPS (M $ N) =
      ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))"
@@ -97,8 +89,8 @@
   apply (simp_all add: fresh_Pair)[4]
 --""
   apply (rule_tac x="(y, ya, b, ba, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Abs b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
-  apply (subgoal_tac "Abs ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Abs a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
+  apply (subgoal_tac "Lam b (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(b~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr M))<(a~)>)")
+  apply (subgoal_tac "Lam ba (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(ba~)>) = Lam a (Sum_Type.Projr (CPSv_CPS_sumC (Inr Ma))<(a~)>)")
   apply (simp only:)
   apply (erule Abs_lst1_fcb)
   apply (simp add: Abs_fresh_iff)
diff -r 132575f5bd26 -r f0fab367453a Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Fri Aug 19 11:07:17 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Fri Aug 19 12:49:38 2011 +0900
@@ -7,12 +7,12 @@
   CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
 where
   "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
-| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))"
-| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))"
+| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))"
+| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))"
 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
 | "(x~)^l = l $ (x~)"
 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
-| "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"
+| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
   apply (simp only: eqvt_def CPS1_CPS2_graph_def)
   apply (rule, perm_simp, rule)
   apply auto
@@ -31,7 +31,7 @@
   apply (simp add: fresh_at_base Abs1_eq_iff)
   apply blast
 --"-"
-  apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))")
+  apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
   apply (simp only:)
   apply (simp add: Abs1_eq_iff)
   apply (case_tac "c=ca")
@@ -49,7 +49,7 @@
   apply simp
   apply (thin_tac "eqvt ka")
   apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
+  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "c = a")
@@ -60,7 +60,7 @@
   apply (erule fresh_eqvt_at)
   apply (simp add: supp_Inr finite_supp)
   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
+  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "ca = a")
@@ -85,8 +85,8 @@
   apply (drule sym)
   apply (drule sym)
   apply (simp only:)
-  apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
+  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
+  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
   apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
   apply (simp add: fresh_Pair_elim)
   apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
@@ -133,7 +133,7 @@
   apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
 --"-"
   apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
+  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "c = a")
@@ -144,7 +144,7 @@
   apply (erule fresh_eqvt_at)
   apply (simp add: supp_Inr finite_supp)
   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
+  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "ca = a")
@@ -169,8 +169,8 @@
   apply (drule sym)
   apply (drule sym)
   apply (simp only:)
-  apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
-  apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
+  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))")
+  apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
   apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
   apply (simp add: fresh_Pair_elim)
   apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
@@ -242,7 +242,7 @@
   apply simp
   done
 
-lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Abs n (k (Var n))))"
+lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))"
   by (cases M rule: lt.exhaust) auto
 
 
diff -r 132575f5bd26 -r f0fab367453a Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Fri Aug 19 11:07:17 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Fri Aug 19 12:49:38 2011 +0900
@@ -7,12 +7,12 @@
   CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
 where
   "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
-| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))"
-| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))"
+| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Lam c (k (c~)))))))"
+| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam c (M^(c~))))"
 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
 | "(x~)^l = l $ (x~)"
 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
-| "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"
+| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
   apply (simp only: eqvt_def CPS1_CPS2_graph_def)
   apply (rule, perm_simp, rule)
   apply auto
@@ -31,7 +31,7 @@
   apply (simp add: fresh_at_base Abs1_eq_iff)
   apply blast
 --"-"
-  apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))")
+  apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
   apply (simp only:)
   apply (simp add: Abs1_eq_iff)
   apply (case_tac "c=ca")
@@ -48,7 +48,7 @@
   back
   apply (thin_tac "eqvt ka")
   apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
-  apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
+  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "c = a")
@@ -59,7 +59,7 @@
   apply (erule fresh_eqvt_at)
   apply (simp add: supp_Inr finite_supp)
   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
-  apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
+  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "ca = a")
diff -r 132575f5bd26 -r f0fab367453a Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Fri Aug 19 11:07:17 2011 +0900
+++ b/Nominal/Ex/CPS/Lt.thy	Fri Aug 19 12:49:38 2011 +0900
@@ -7,48 +7,45 @@
 
 nominal_datatype lt =
     Var name       ("_~"  [150] 149)
-  | Abs x::"name" t::"lt"  binds  x in t
+  | Lam x::"name" t::"lt"  binds  x in t
   | App lt lt         (infixl "$" 100)
 
 nominal_primrec
-  subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190)
+  subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)
 where
-  "(y~)[L/x] = (if y = x then L else y~)"
-| "atom y\<sharp>L \<Longrightarrow> atom y\<sharp>x \<Longrightarrow> (Abs y M)[L/x]  = Abs y (M[L/x])"
-| "(M $ N)[L/x] = M[L/x] $ N[L/x]"
+  "(Var x)[y ::= s] = (if x = y then s else (Var x))"
+| "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
+| "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
   unfolding eqvt_def subst_graph_def
-  apply(perm_simp)
-  apply(auto)
+  apply (rule, perm_simp, rule)
+  apply(rule TrueI)
+  apply(auto simp add: lt.distinct lt.eq_iff)
   apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
-  apply(simp_all add: fresh_star_def fresh_Pair)
-  apply blast+
-  apply (erule Abs_lst1_fcb)
-  apply (simp_all add: Abs_fresh_iff)[2]
-  apply(drule_tac a="atom (ya)" in fresh_eqvt_at)
-  apply(simp add: finite_supp fresh_Pair)
-  apply(simp_all add: fresh_Pair Abs_fresh_iff)
-  apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> La = La")
-  apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> xa = xa")
-  apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute)
-  apply (simp_all add: swap_fresh_fresh)
-  done
+  apply blast
+  apply(simp_all add: fresh_star_def fresh_Pair_elim)
+  apply blast
+  apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
+  apply(simp_all add: Abs_fresh_iff)
+  apply(simp add: fresh_star_def fresh_Pair)
+  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)+
+done
 
 termination (eqvt) by lexicographic_order
 
 lemma forget[simp]:
-  shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M"
+  shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M"
   by (nominal_induct M avoiding: x s rule: lt.strong_induct)
      (auto simp add: lt.fresh fresh_at_base)
 
-lemma [simp]: "supp ( M[V/(x::name)] ) <= (supp(M) - {atom x}) Un (supp V)"
+lemma [simp]: "supp (M[x ::= V]) <= (supp(M) - {atom x}) Un (supp V)"
   by (nominal_induct M avoiding: x V rule: lt.strong_induct)
      (auto simp add: lt.supp supp_at_base, blast, blast)
 
-nominal_primrec 
+nominal_primrec
   isValue:: "lt => bool"
 where
   "isValue (Var x) = True"
-| "isValue (Abs y N) = True"
+| "isValue (Lam y N) = True"
 | "isValue (A $ B) = False"
   unfolding eqvt_def isValue_graph_def
   by (perm_simp, auto)
@@ -57,14 +54,10 @@
 termination (eqvt)
   by (relation "measure size") (simp_all)
 
-lemma is_Value_eqvt[eqvt]:
-  shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)"
-  by (induct M rule: lt.induct) (simp_all add: eqvts)
-
 inductive
   eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
   where
-   evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Abs x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[V/x])"
+   evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
 |  ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')"
 |  ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)"
 
@@ -81,7 +74,7 @@
     by (induct, auto simp add: lt.supp)
 
 
-lemma [simp]: "~ ((Abs x M) \<longrightarrow>\<^isub>\<beta> N)"
+lemma [simp]: "~ ((Lam x M) \<longrightarrow>\<^isub>\<beta> N)"
 by (rule, erule eval.cases, simp_all)
 
 lemma [simp]: assumes "M \<longrightarrow>\<^isub>\<beta> N" shows "~ isValue M"
@@ -114,8 +107,8 @@
 
 lemma evbeta':
   fixes x :: name
-  assumes "isValue V" and "atom x\<sharp>V" and "N = (M[V/x])"
-  shows "((Abs x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
+  assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])"
+  shows "((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
   using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
 
 end