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   | App lt lt         (infixl "$$" 100)

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

    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_aux_def

    20   apply (simp)

    21   apply(rule TrueI)

    22   using [[simproc del: alpha_lst]]

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

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

    25   apply blast

    26   apply(simp_all add: fresh_star_def fresh_Pair_elim)

    27   apply blast

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

    29   apply(simp add: Abs_fresh_iff)

    30   apply(simp add: fresh_star_def fresh_Pair)

    31   apply(simp add: eqvt_at_def)

    32   apply(simp add: perm_supp_eq fresh_star_Pair)

    33   apply(simp add: eqvt_at_def)

    34   apply(simp add: perm_supp_eq fresh_star_Pair)

    35 done

    36 

    37 termination (eqvt) by lexicographic_order

    38 

    39 lemma forget[simp]:

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

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

    42      (auto simp add: lt.fresh fresh_at_base)

    43 

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

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

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

    47 

    48 nominal_primrec

    49   isValue:: "lt => bool"

    50 where

    51   "isValue (Var x) = True"

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

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

    54   unfolding eqvt_def isValue_graph_aux_def

    55   by (auto)

    56      (erule lt.exhaust, auto)

    57 

    58 termination (eqvt)

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

    60 

    61 inductive

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

    63   where

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

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

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

    67 

    68 equivariance eval

    69 

    70 nominal_inductive eval

    71 done

    72 

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

    74 

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

    76   shows "supp t <= supp s"

    77   using assms

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

    79 

    80 

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

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

    83 

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

    85 using assms

    86 by (cases, auto)

    87 

    88 

    89 inductive

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

    91   where

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

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

    94 

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

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

    97 

    98 lemma eval_trans[trans]:

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

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

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

   102   using assms

   103   by (induct, auto intro: evs2)

   104 

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

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

   107   using assms

   108     by (induct, auto intro: eval_evs evs2)

   109 

   110 equivariance eval_star

   111 

   112 lemma evbeta':

   113   fixes x :: name

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

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

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

   117 

   118 end

   119 

   120 

   121