Nominal/Ex/CPS/CPS1_Plotkin.thy
branchNominal2-Isabelle2011-1
changeset 3071 11f6a561eb4b
parent 3070 4b4742aa43f2
child 3072 7eb352826b42
equal deleted inserted replaced
3070:4b4742aa43f2 3071:11f6a561eb4b
     1 header {* CPS conversion *}
       
     2 theory CPS1_Plotkin
       
     3 imports Lt
       
     4 begin
       
     5 
       
     6 nominal_primrec
       
     7   CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
       
     8 where
       
     9   "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $ (x~)))"
       
    10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $ Lam x (M*))"
       
    11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
       
    12     (M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))"
       
    13 unfolding eqvt_def CPS_graph_def
       
    14 apply (rule, perm_simp, rule, rule)
       
    15 apply (simp_all add: fresh_Pair_elim)
       
    16 apply (rule_tac y="x" in lt.exhaust)
       
    17 apply (auto)
       
    18 apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
       
    19 apply (simp_all add: fresh_at_base)[3]
       
    20 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
       
    21 apply (simp add: fresh_Pair_elim fresh_at_base)[2]
       
    22 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
       
    23 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)
       
    24 apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh)
       
    25 apply (simp add: fresh_Pair_elim fresh_at_base)
       
    26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
       
    27 --"-"
       
    28 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
       
    29 apply (case_tac "k = ka")
       
    30 apply simp
       
    31 apply(simp (no_asm) add: Abs1_eq_iff del:eqvts)
       
    32 apply (simp del: eqvts add: lt.fresh fresh_at_base)
       
    33 apply (simp only: lt.perm_simps(1) lt.perm_simps(3) flip_def[symmetric] lt.eq_iff(3))
       
    34 apply (subst  flip_at_base_simps(2))
       
    35 apply simp
       
    36 apply (intro conjI refl)
       
    37 apply (rule flip_fresh_fresh[symmetric])
       
    38 apply (simp_all add: lt.fresh)
       
    39 apply (metis fresh_eqvt_at lt.fsupp)
       
    40 apply (case_tac "ka = x")
       
    41 apply simp_all[2]
       
    42 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp)
       
    43 apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp)
       
    44 --"-"
       
    45 apply (simp add: Abs1_eq(3))
       
    46 apply (erule Abs_lst1_fcb2)
       
    47 apply (simp_all add: Abs_fresh_iff fresh_Nil fresh_star_def eqvt_at_def)[4]
       
    48 --"-"
       
    49 apply (rename_tac k' M N m' n')
       
    50 apply (subgoal_tac "atom k \<sharp> CPS_sumC M \<and> atom k' \<sharp> CPS_sumC M \<and> atom k \<sharp> CPS_sumC N \<and> atom k' \<sharp> CPS_sumC N \<and>
       
    51                     atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N")
       
    52 prefer 2
       
    53 apply (intro conjI)
       
    54 apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+
       
    55 apply clarify
       
    56 apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'")
       
    57 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)
       
    58 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+
       
    59 
       
    60 termination (eqvt) by lexicographic_order
       
    61 
       
    62 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]
       
    63 
       
    64 lemma [simp]: "supp (M*) = supp M"
       
    65   by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair)
       
    66      (simp_all only: atom_eq_iff[symmetric], blast+)
       
    67 
       
    68 lemma [simp]: "x \<sharp> M* = x \<sharp> M"
       
    69   unfolding fresh_def by simp
       
    70 
       
    71 nominal_primrec
       
    72   convert:: "lt => lt" ("_+" [250] 250)
       
    73 where
       
    74   "(Var x)+ = Var x"
       
    75 | "(Lam x M)+ = Lam x (M*)"
       
    76 | "(M $ N)+ = M $ N"
       
    77   unfolding convert_graph_def eqvt_def
       
    78   apply (rule, perm_simp, rule, rule)
       
    79   apply (erule lt.exhaust)
       
    80   apply (simp_all)
       
    81   apply blast
       
    82   apply (simp add: Abs1_eq_iff CPS.eqvt)
       
    83   by blast
       
    84 
       
    85 termination (eqvt)
       
    86   by (relation "measure size") (simp_all)
       
    87 
       
    88 lemma convert_supp[simp]:
       
    89   shows "supp (M+) = supp M"
       
    90   by (induct M rule: lt.induct, simp_all add: lt.supp)
       
    91 
       
    92 lemma convert_fresh[simp]:
       
    93   shows "x \<sharp> (M+) = x \<sharp> M"
       
    94   unfolding fresh_def by simp
       
    95 
       
    96 lemma [simp]:
       
    97   shows "isValue (p \<bullet> (M::lt)) = isValue M"
       
    98   by (nominal_induct M rule: lt.strong_induct) auto
       
    99 
       
   100 nominal_primrec
       
   101   Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)
       
   102 where
       
   103   "Kapply (Lam x M) K = K $ (Lam x M)+"
       
   104 | "Kapply (Var x) K = K $ Var x"
       
   105 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"
       
   106 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
       
   107     Kapply (M $ N) K = N; (Lam n (M+ $ Var n $ K))"
       
   108 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
       
   109     Kapply (M $ N) K = M; (Lam m (N*  $ (Lam n (Var m $ Var n $ K))))"
       
   110   unfolding Kapply_graph_def eqvt_def
       
   111   apply (rule, perm_simp, rule, rule)
       
   112 apply (simp_all)
       
   113 apply (case_tac x)
       
   114 apply (rule_tac y="a" in lt.exhaust)
       
   115 apply (auto)
       
   116 apply (case_tac "isValue lt1")
       
   117 apply (case_tac "isValue lt2")
       
   118 apply (auto)[1]
       
   119 apply (rule_tac x="(lt1, ba)" and ?'a="name" in obtain_fresh)
       
   120 apply (simp add: fresh_Pair_elim fresh_at_base)
       
   121 apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh)
       
   122 apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh)
       
   123 apply (simp add: fresh_Pair_elim fresh_at_base)
       
   124 apply (auto simp add: Abs1_eq_iff eqvts)[1]
       
   125 apply (rename_tac M N u K)
       
   126 apply (subgoal_tac "Lam n (M+ $ n~ $ K) =  Lam u (M+ $ u~ $ K)")
       
   127 apply (simp only:)
       
   128 apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]
       
   129 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
       
   130 apply (simp only:)
       
   131 apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)
       
   132 apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")
       
   133 apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka")
       
   134 apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka")
       
   135 apply (case_tac "m = ma")
       
   136 apply simp_all
       
   137 apply rule
       
   138 apply (auto simp add: flip_fresh_fresh[symmetric])
       
   139 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
       
   140 done
       
   141 
       
   142 termination (eqvt)
       
   143   by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
       
   144 
       
   145 section{* lemma related to Kapply *}
       
   146 
       
   147 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)"
       
   148   by (nominal_induct V rule: lt.strong_induct) auto
       
   149 
       
   150 section{* lemma related to CPS conversion *}
       
   151 
       
   152 lemma value_CPS:
       
   153   assumes "isValue V"
       
   154   and "atom a \<sharp> V"
       
   155   shows "V* = Lam a (a~ $ V+)"
       
   156   using assms
       
   157 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh)
       
   158   fix name :: name and lt aa
       
   159   assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $ lt+)"
       
   160     "atom aa \<sharp> lt \<or> aa = name"
       
   161   obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast
       
   162   show "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b
       
   163     by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
       
   164 qed
       
   165 
       
   166 section{* first lemma CPS subst *}
       
   167 
       
   168 lemma CPS_subst_fv:
       
   169   assumes *:"isValue V"
       
   170   shows "((M[x ::= V])* = (M*)[x ::= V+])"
       
   171 using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct)
       
   172   case (Var name)
       
   173   assume *: "isValue V"
       
   174   obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast
       
   175   show "((name~)[x ::= V])* = (name~)*[x ::= V+]" using a
       
   176     by (simp add: fresh_at_base * value_CPS)
       
   177 next
       
   178   case (Lam name lt V x)
       
   179   assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[ba ::= b])* = lt*[ba ::= b+]"
       
   180     "isValue V"
       
   181   obtain a :: name where a: "atom a \<sharp> (name, lt, lt[x ::= V], x, V)" using obtain_fresh by blast
       
   182   show "(Lam name lt[x ::= V])* = Lam name lt*[x ::= V+]" using * a
       
   183     by (simp add: fresh_at_base)
       
   184 next
       
   185   case (App lt1 lt2 V x)
       
   186   assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[ba ::= b])* = lt1*[ba ::= b+]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[ba ::= b])* = lt2*[ba ::= b+]"
       
   187     "isValue V"
       
   188   obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast
       
   189   obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], lt2, a, V, x)" using obtain_fresh by blast
       
   190   obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast
       
   191   show "((lt1 $ lt2)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c
       
   192     by (simp add: fresh_at_base)
       
   193 qed
       
   194 
       
   195 lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)"
       
   196   by (nominal_induct V rule: lt.strong_induct, auto)
       
   197 
       
   198 lemma CPS_eval_Kapply:
       
   199   assumes a: "isValue K"
       
   200   shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)"
       
   201   using a
       
   202 proof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all)
       
   203   case (Var name K)
       
   204   assume *: "isValue K"
       
   205   obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast
       
   206   show "(name~)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ name~" using * a
       
   207     by simp (rule evbeta', simp_all add: fresh_at_base)
       
   208 next
       
   209   fix name :: name and lt K
       
   210   assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K"
       
   211   obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast
       
   212   then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis
       
   213   show "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b
       
   214     by simp (rule evbeta', simp_all)
       
   215 next
       
   216   fix lt1 lt2 K
       
   217   assume *: "\<And>b. isValue b \<Longrightarrow>  lt1* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 ; b" "\<And>b. isValue b \<Longrightarrow>  lt2* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; b" "isValue K"
       
   218   obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast
       
   219   obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast
       
   220   obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast
       
   221   have d: "atom a \<sharp> lt1" "atom a \<sharp> lt2" "atom a \<sharp> K" "atom b \<sharp> lt1" "atom b \<sharp> lt2" "atom b \<sharp> K" "atom b \<sharp> a"
       
   222     "atom c \<sharp> lt1" "atom c \<sharp> lt2" "atom c \<sharp> K" "atom c \<sharp> a" "atom c \<sharp> b" using fresh_Pair a b c by simp_all
       
   223   have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d
       
   224     by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base)
       
   225   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1")
       
   226     assume e: "isValue lt1"
       
   227     have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
       
   228       using * d e by simp
       
   229     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
       
   230       by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base)
       
   231     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
       
   232       assume f: "isValue lt2"
       
   233       have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
       
   234       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K"
       
   235         by (rule evbeta', simp_all add: d e f)
       
   236       finally show ?thesis using * d e f by simp
       
   237     next
       
   238       assume f: "\<not> isValue lt2"
       
   239       have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp
       
   240       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis
       
   241       finally show ?thesis using * d e f by simp
       
   242     qed
       
   243     finally show ?thesis .
       
   244   qed (metis Kapply.simps(5) isValue.simps(2) * d)
       
   245   finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" .
       
   246 qed
       
   247 
       
   248 lemma Kapply_eval:
       
   249   assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"
       
   250   shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  (N; K)"
       
   251   using assms
       
   252 proof (induct arbitrary: K rule: eval.induct)
       
   253   case (evbeta x V M)
       
   254   fix K
       
   255   assume a: "isValue K" "isValue V" "atom x \<sharp> V"
       
   256   have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)"
       
   257     by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)
       
   258   also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a)
       
   259   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
       
   260   finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  ((M[x ::= V]) ; K)" using a by simp
       
   261 next
       
   262   case (ev1 V M N)
       
   263   fix V M N K
       
   264   assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K"
       
   265   obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast
       
   266   show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N")
       
   267     assume "\<not> isValue N"
       
   268     then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp
       
   269   next
       
   270     assume n: "isValue N"
       
   271     have c: "M; Lam a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam a (V+ $ a~ $ K) $ N+" using a b by (simp add: n)
       
   272     also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n)
       
   273     finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n)
       
   274   qed
       
   275 next
       
   276   case (ev2 M M' N)
       
   277   assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow>  M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K"
       
   278   obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast
       
   279   obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast
       
   280   have d: "atom a \<sharp> K" "atom a \<sharp> M" "atom a \<sharp> N" "atom a \<sharp> M'" "atom b \<sharp> a" "atom b \<sharp> K"
       
   281     "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all
       
   282   have "M $ N ; K  \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp
       
   283   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'")
       
   284     assume "\<not> isValue M'"
       
   285     then show ?thesis using * d by (simp_all add: evs1)
       
   286   next
       
   287     assume e: "isValue M'"
       
   288     then have "M' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp
       
   289     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]"
       
   290       by (rule evbeta') (simp_all add: fresh_at_base e d)
       
   291     also have "... = N* $ Lam b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base)
       
   292     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N")
       
   293       assume f: "isValue N"
       
   294       have "N* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+"
       
   295         by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1)
       
   296       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1)
       
   297       finally show ?thesis .
       
   298     next
       
   299       assume "\<not> isValue N"
       
   300       then show ?thesis using d e
       
   301         by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2))
       
   302     qed
       
   303     finally show ?thesis .
       
   304   qed
       
   305   finally show ?case .
       
   306 qed
       
   307 
       
   308 lemma Kapply_eval_rtrancl:
       
   309   assumes H: "M \<longrightarrow>\<^isub>\<beta>\<^sup>*  N" and "isValue K"
       
   310   shows "(M;K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N;K)"
       
   311   using H
       
   312   by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+
       
   313 
       
   314 lemma
       
   315   assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"
       
   316   shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
       
   317 proof-
       
   318   obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast
       
   319   have e: "Lam x (x~) = Lam y (y~)"
       
   320     by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
       
   321   have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
       
   322     by(rule CPS_eval_Kapply,simp_all add: assms)
       
   323   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
       
   324   also have "... = V ; Lam y (y~)" using e by (simp only:)
       
   325   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *)
       
   326   finally show "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
       
   327 qed
       
   328 
       
   329 end
       
   330 
       
   331 
       
   332