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   | Abs x::"name" t::"lt"  bind  x in t

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

    12 

    13 nominal_primrec

    14   subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190)

    15 where

    16   "(y~)[L/x] = (if y = x then L else y~)"

    17 | "atom y\<sharp>L \<Longrightarrow> atom y\<sharp>x \<Longrightarrow> (Abs y M)[L/x]  = Abs y (M[L/x])"

    18 | "(M $ N)[L/x] = M[L/x] $ N[L/x]"

    19   unfolding eqvt_def subst_graph_def

    20   apply(perm_simp)

    21   apply(auto)

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

    23   apply(simp_all add: fresh_star_def fresh_Pair)

    24   apply blast+

    25   apply (erule Abs_lst1_fcb)

    26   apply (simp_all add: Abs_fresh_iff)[2]

    27   apply(drule_tac a="atom (ya)" in fresh_eqvt_at)

    28   apply(simp add: finite_supp fresh_Pair)

    29   apply(simp_all add: fresh_Pair Abs_fresh_iff)

    30   apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> La = La")

    31   apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> xa = xa")

    32   apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute)

    33   apply (simp_all add: swap_fresh_fresh)

    34   done

    35 

    36 termination

    37   by (relation "measure (\<lambda>(t, _, _). size t)")

    38      (simp_all add: lt.size)

    39 

    40 lemma subst_eqvt[eqvt]:

    41   shows "p\<bullet>(M[V/(x::name)]) = (p\<bullet>M)[(p\<bullet>V)/(p\<bullet>x)]"

    42   by (induct M V x rule: subst.induct) (simp_all)

    43 

    44 lemma forget[simp]:

    45   shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M"

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

    47      (auto simp add: lt.fresh fresh_at_base)

    48 

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

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

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

    52 

    53 nominal_primrec 

    54   isValue:: "lt => bool"

    55 where

    56   "isValue (Var x) = True"

    57 | "isValue (Abs y N) = True"

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

    59   unfolding eqvt_def isValue_graph_def

    60   by (perm_simp, auto)

    61      (erule lt.exhaust, auto)

    62 

    63 termination

    64   by (relation "measure size")

    65      (simp_all add: lt.size)

    66 

    67 lemma is_Value_eqvt[eqvt]:

    68   shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)"

    69   by (induct M rule: lt.induct) (simp_all add: eqvts)

    70 

    71 inductive

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

    73   where

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

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

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

    77 

    78 equivariance eval

    79 

    80 nominal_inductive eval

    81 done

    82 

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

    84 

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

    86   shows "supp t <= supp s"

    87   using assms

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

    89 

    90 

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

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

    93 

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

    95 using assms

    96 by (cases, auto)

    97 

    98 

    99 inductive

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

   101   where

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

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

   104 

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

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

   107 

   108 lemma eval_trans[trans]:

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

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

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

   112   using assms

   113   by (induct, auto intro: evs2)

   114 

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

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

   117   using assms

   118     by (induct, auto intro: eval_evs evs2)

   119 

   120 equivariance eval_star

   121 

   122 lemma evbeta':

   123   fixes x :: name

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

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

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

   127 

   128 end

   129 

   130 

   131