header {* The Call-by-Value Lambda Calculus *}

theory Lt

imports "../../Nominal2"

begin

atom_decl name

nominal_datatype lt =

    Var name       ("_~"  [150] 149)

  | App lt lt         (infixl "$" 100)

nominal_primrec

where

  unfolding eqvt_def subst_graph_def

  apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)

termination (eqvt) by lexicographic_order

lemma forget[simp]:

  by (nominal_induct M avoiding: x s rule: lt.strong_induct)

     (auto simp add: lt.fresh fresh_at_base)

  by (nominal_induct M avoiding: x V rule: lt.strong_induct)

     (auto simp add: lt.supp supp_at_base, blast, blast)

  isValue:: "lt => bool"

where

  "isValue (Var x) = True"

| "isValue (A $ B) = False"

  unfolding eqvt_def isValue_graph_def

  by (perm_simp, auto)

     (erule lt.exhaust, auto)

termination (eqvt)

  by (relation "measure size") (simp_all)

inductive

  eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)

  where

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

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

  using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)

end