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

     2 theory Lt

     3 imports "../../Nominal2"

     4 begin

     5 

     6 atom_decl name

     7 

     8 nominal_datatype lt =

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

    10   | Lam x::"name" t::"lt"  binds  x in t

    11   | App lt lt         (infixl "$" 100)

    12 

    13 nominal_primrec

    14   subst :: "lt \<Rightarrow> name \<Rightarrow> lt \<Rightarrow> lt"  ("_ [_ ::= _]" [90, 90, 90] 90)

    15 where

    16   "(Var x)[y ::= s] = (if x = y then s else (Var x))"

    17 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"

    18 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"

    19   unfolding eqvt_def subst_graph_def

    20   apply (rule, perm_simp, rule)

    21   apply(rule TrueI)

    22   apply(auto simp add: lt.distinct lt.eq_iff)

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

    24   apply blast

    25   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    26   apply blast

    27   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)

    28   apply(simp_all add: Abs_fresh_iff)

    29   apply(simp add: fresh_star_def fresh_Pair)

    30   apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)+

    31 done

    32 

    33 termination (eqvt) by lexicographic_order

    34 

    35 lemma forget[simp]:

    36   shows "atom x \<sharp> M \<Longrightarrow> M[x ::= s] = M"

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

    38      (auto simp add: lt.fresh fresh_at_base)

    39 

    40 lemma [simp]: "supp (M[x ::= V]) <= (supp(M) - {atom x}) Un (supp V)"

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

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

    43 

    44 nominal_primrec

    45   isValue:: "lt => bool"

    46 where

    47   "isValue (Var x) = True"

    48 | "isValue (Lam y N) = True"

    49 | "isValue (A $ B) = False"

    50   unfolding eqvt_def isValue_graph_def

    51   by (perm_simp, auto)

    52      (erule lt.exhaust, auto)

    53 

    54 termination (eqvt)

    55   by (relation "measure size") (simp_all)

    56 

    57 inductive

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

    59   where

    60    evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"

    61 |  ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')"

    62 |  ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)"

    63 

    64 equivariance eval

    65 

    66 nominal_inductive eval

    67 done

    68 

    69 (*lemmas [simp] = lt.supp(2)*)

    70 

    71 lemma closedev1: assumes "s \<longrightarrow>\<^isub>\<beta> t"

    72   shows "supp t <= supp s"

    73   using assms

    74     by (induct, auto simp add: lt.supp)

    75 

    76 

    77 lemma [simp]: "~ ((Lam x M) \<longrightarrow>\<^isub>\<beta> N)"

    78 by (rule, erule eval.cases, simp_all)

    79 

    80 lemma [simp]: assumes "M \<longrightarrow>\<^isub>\<beta> N" shows "~ isValue M"

    81 using assms

    82 by (cases, auto)

    83 

    84 

    85 inductive

    86   eval_star :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)

    87   where

    88    evs1: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"

    89 |  evs2: "\<lbrakk>M \<longrightarrow>\<^isub>\<beta> M'; M' \<longrightarrow>\<^isub>\<beta>\<^sup>*  M'' \<rbrakk> \<Longrightarrow> M \<longrightarrow>\<^isub>\<beta>\<^sup>*  M''"

    90 

    91 lemma eval_evs: assumes *: "M \<longrightarrow>\<^isub>\<beta> M'" shows "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M'"

    92 by (rule evs2, rule *, rule evs1)

    93 

    94 lemma eval_trans[trans]:

    95   assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"

    96       and "M2  \<longrightarrow>\<^isub>\<beta>\<^sup>*  M3"

    97   shows "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"

    98   using assms

    99   by (induct, auto intro: evs2)

   100 

   101 lemma evs3[rule_format]: assumes "M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"

   102   shows "M2  \<longrightarrow>\<^isub>\<beta> M3 \<longrightarrow> M1  \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"

   103   using assms

   104     by (induct, auto intro: eval_evs evs2)

   105 

   106 equivariance eval_star

   107 

   108 lemma evbeta':

   109   fixes x :: name

   110   assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])"

   111   shows "((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"

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

   113 

   114 end

   115 

   116 

   117