--- a/Nominal/CPS/Lt.thy	Thu Jun 16 21:23:38 2011 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-header {* The Call-by-Value Lambda Calculus *}
-theory Lt
-imports Nominal2
-begin
-
-atom_decl name
-
-nominal_datatype lt =
-    Var name       ("_~"  [150] 149)
-  | Abs x::"name" t::"lt"  bind  x in t
-  | App lt lt         (infixl "$" 100)
-
-nominal_primrec
-  subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190)
-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]"
-  unfolding eqvt_def subst_graph_def
-  apply(perm_simp)
-  apply(auto)
-  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
-
-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)
-
-lemma forget[simp]:
-  shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = 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)"
-  by (nominal_induct M avoiding: x V rule: lt.strong_induct)
-     (auto simp add: lt.supp supp_at_base, blast, blast)
-
-nominal_primrec 
-  isValue:: "lt => bool"
-where
-  "isValue (Var x) = True"
-| "isValue (Abs y N) = True"
-| "isValue (A $ B) = False"
-  unfolding eqvt_def isValue_graph_def
-  by (perm_simp, auto)
-     (erule lt.exhaust, auto)
-
-termination
-  by (relation "measure size")
-     (simp_all add: lt.size)
-
-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])"
-|  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)"
-
-equivariance eval
-
-nominal_inductive eval
-done
-
-(*lemmas [simp] = lt.supp(2)*)
-
-lemma closedev1: assumes "s \<longrightarrow>\<^isub>\<beta> t"
-  shows "supp t <= supp s"
-  using assms
-    by (induct, auto simp add: lt.supp)
-
-
-lemma [simp]: "~ ((Abs x M) \<longrightarrow>\<^isub>\<beta> N)"
-by (rule, erule eval.cases, simp_all)
-
-lemma [simp]: assumes "M \<longrightarrow>\<^isub>\<beta> N" shows "~ isValue M"
-using assms
-by (cases, auto)
-
-
-inductive
-  eval_star :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
-  where
-   evs1: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
-|  evs2: "\<lbrakk>M \<longrightarrow>\<^isub>\<beta> M'; M' \<longrightarrow>\<^isub>\<beta>\<^sup>*  M'' \<rbrakk> \<Longrightarrow> M \<longrightarrow>\<^isub>\<beta>\<^sup>*  M''"
-
-lemma eval_evs: assumes *: "M \<longrightarrow>\<^isub>\<beta> M'" shows "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M'"
-by (rule evs2, rule *, rule evs1)
-
-lemma eval_trans[trans]:
-  assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
-      and "M2  \<longrightarrow>\<^isub>\<beta>\<^sup>*  M3"
-  shows "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
-  using assms
-  by (induct, auto intro: evs2)
-
-lemma evs3[rule_format]: assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
-  shows "M2  \<longrightarrow>\<^isub>\<beta> M3 \<longrightarrow> M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
-  using assms
-    by (induct, auto intro: eval_evs evs2)
-
-equivariance eval_star
-
-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"
-  using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
-
-end
-
-
-