--- 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