1 header {* CPS conversion *}

     2 theory 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~)* = (Abs k ((k~) $ (x~)))"

    10 | "atom k \<sharp> (x, M) \<Longrightarrow> (Abs x M)* = Abs k (k~ $ Abs x (M*))"

    11 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>

    12     (M $ N)* = Abs k (M* $ Abs m (N* $ Abs 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~ $ Abs 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_fcb)

    47 apply (simp add: fresh_def supp_Abs)

    48 apply (drule_tac a="atom xa" in fresh_eqvt_at)

    49 apply (simp add: finite_supp)

    50 apply assumption

    51 apply (simp add: fresh_def supp_Abs)

    52 apply (simp add: eqvts eqvt_at_def)

    53 apply simp

    54 --"-"

    55 apply (rename_tac k' M N m' n')

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

    57                     atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N")

    58 prefer 2

    59 apply (intro conjI)

    60 apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+

    61 apply clarify

    62 apply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'")

    63 apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)

    64 by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+

    65 

    66 termination

    67   by (relation "measure size") (simp_all add: lt.size)

    68 

    69 lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]

    70 

    71 lemma [simp]: "supp (M*) = supp M"

    72   by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair)

    73      (simp_all only: atom_eq_iff[symmetric], blast+)

    74 

    75 lemma [simp]: "x \<sharp> M* = x \<sharp> M"

    76   unfolding fresh_def by simp

    77 

    78 (* Will be provided automatically by nominal_primrec *)

    79 lemma CPS_eqvt[eqvt]:

    80   shows "p \<bullet> M* = (p \<bullet> M)*"

    81   apply (induct M rule: lt.induct)

    82   apply (rule_tac x="(name, p \<bullet> name, p)" and ?'a="name" in obtain_fresh)

    83   apply simp

    84   apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric])

    85   apply (metis atom_eqvt flip_fresh_fresh fresh_perm atom_eq_iff fresh_at_base)

    86   apply (rule_tac x="(name, lt, p \<bullet> name, p \<bullet> lt, p)" and ?'a="name" in obtain_fresh)

    87   apply simp

    88   apply (metis atom_eqvt fresh_perm atom_eq_iff)

    89   apply (rule_tac x="(lt1, p \<bullet> lt1, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh)

    90   apply (rule_tac x="(a, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh)

    91   apply (rule_tac x="(a, aa, p)" and ?'a="name" in obtain_fresh)

    92   apply (simp)

    93   apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric])

    94   apply (metis atom_eqvt fresh_perm atom_eq_iff)

    95   done

    96 

    97 nominal_primrec

    98   convert:: "lt => lt" ("_+" [250] 250)

    99 where

   100   "(Var x)+ = Var x"

   101 | "(Abs x M)+ = Abs x (M*)"

   102 | "(M $ N)+ = M $ N"

   103   unfolding convert_graph_def eqvt_def

   104   apply (rule, perm_simp, rule, rule)

   105   apply (erule lt.exhaust)

   106   apply (simp_all)

   107   apply blast

   108   apply (simp add: Abs1_eq_iff CPS_eqvt)

   109   by blast

   110 

   111 termination

   112   by (relation "measure size") (simp_all add: lt.size)

   113 

   114 lemma convert_supp[simp]:

   115   shows "supp (M+) = supp M"

   116   by (induct M rule: lt.induct, simp_all add: lt.supp)

   117 

   118 lemma convert_fresh[simp]:

   119   shows "x \<sharp> (M+) = x \<sharp> M"

   120   unfolding fresh_def by simp

   121 

   122 lemma convert_eqvt[eqvt]:

   123   shows "p \<bullet> (M+) = (p \<bullet> M)+"

   124   by (nominal_induct M rule: lt.strong_induct, auto simp add: CPS_eqvt)

   125 

   126 lemma [simp]:

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

   128   by (nominal_induct M rule: lt.strong_induct) auto

   129 

   130 lemma [eqvt]:

   131   shows "p \<bullet> isValue M = isValue (p \<bullet> M)"

   132   by (induct M rule: lt.induct) (perm_simp, rule refl)+

   133 

   134 nominal_primrec

   135   Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)

   136 where

   137   "Kapply (Abs x M) K = K $ (Abs x M)+"

   138 | "Kapply (Var x) K = K $ Var x"

   139 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"

   140 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>

   141     Kapply (M $ N) K = N; (Abs n (M+ $ Var n $ K))"

   142 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>

   143     Kapply (M $ N) K = M; (Abs m (N*  $ (Abs n (Var m $ Var n $ K))))"

   144   unfolding Kapply_graph_def eqvt_def

   145   apply (rule, perm_simp, rule, rule)

   146 apply (simp_all)

   147 apply (case_tac x)

   148 apply (rule_tac y="a" in lt.exhaust)

   149 apply (auto)

   150 apply (case_tac "isValue lt1")

   151 apply (case_tac "isValue lt2")

   152 apply (auto)[1]

   153 apply (rule_tac x="(lt1, ba)" and ?'a="name" in obtain_fresh)

   154 apply (simp add: fresh_Pair_elim fresh_at_base)

   155 apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh)

   156 apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh)

   157 apply (simp add: fresh_Pair_elim fresh_at_base)

   158 apply (auto simp add: Abs1_eq_iff eqvts)[1]

   159 apply (rename_tac M N u K)

   160 apply (subgoal_tac "Abs n (M+ $ n~ $ K) =  Abs u (M+ $ u~ $ K)")

   161 apply (simp only:)

   162 apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]

   163 apply (subgoal_tac "Abs m (Na* $ Abs n (m~ $ n~ $ Ka)) = Abs ma (Na* $ Abs na (ma~ $ na~ $ Ka))")

   164 apply (simp only:)

   165 apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)

   166 apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")

   167 apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka")

   168 apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka")

   169 apply (case_tac "m = ma")

   170 apply simp_all

   171 apply rule

   172 apply (auto simp add: flip_fresh_fresh[symmetric])

   173 apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+

   174 done

   175 

   176 termination

   177   by (relation "measure (\<lambda>(t, _). size t)") (simp_all add: lt.size)

   178 

   179 section{* lemma related to Kapply *}

   180 

   181 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)"

   182   by (nominal_induct V rule: lt.strong_induct) auto

   183 

   184 section{* lemma related to CPS conversion *}

   185 

   186 lemma value_CPS:

   187   assumes "isValue V"

   188   and "atom a \<sharp> V"

   189   shows "V* = Abs a (a~ $ V+)"

   190   using assms

   191 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh)

   192   fix name :: name and lt aa

   193   assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Abs b (b~ $ lt+)"

   194     "atom aa \<sharp> lt \<or> aa = name"

   195   obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast

   196   show "Abs name lt* = Abs aa (aa~ $ Abs name (lt*))" using a b

   197     by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)

   198 qed

   199 

   200 section{* first lemma CPS subst *}

   201 

   202 lemma CPS_subst_fv:

   203   assumes *:"isValue V"

   204   shows "((M[V/x])* = (M*)[V+/x])"

   205 using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct)

   206   case (Var name)

   207   assume *: "isValue V"

   208   obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast

   209   show "((name~)[V/x])* = (name~)*[V+/x]" using a

   210     by (simp add: fresh_at_base * value_CPS)

   211 next

   212   case (Abs name lt V x)

   213   assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[b/ba])* = lt*[b+/ba]"

   214     "isValue V"

   215   obtain a :: name where a: "atom a \<sharp> (name, lt, lt[V/x], x, V)" using obtain_fresh by blast

   216   show "(Abs name lt[V/x])* = Abs name lt*[V+/x]" using * a

   217     by (simp add: fresh_at_base)

   218 next

   219   case (App lt1 lt2 V x)

   220   assume *: "\<And>b ba. isValue b \<Longrightarrow> (lt1[b/ba])* = lt1*[b+/ba]" "\<And>b ba. isValue b \<Longrightarrow> (lt2[b/ba])* = lt2*[b+/ba]"

   221     "isValue V"

   222   obtain a :: name where a: "atom a \<sharp> (lt1[V/x], lt1, lt2[V/x], lt2, V, x)" using obtain_fresh by blast

   223   obtain b :: name where b: "atom b \<sharp> (lt2[V/x], lt2, a, V, x)" using obtain_fresh by blast

   224   obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast

   225   show "((lt1 $ lt2)[V/x])* = (lt1 $ lt2)*[V+/x]" using * a b c

   226     by (simp add: fresh_at_base)

   227 qed

   228 

   229 lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)"

   230   by (nominal_induct V rule: lt.strong_induct, auto)

   231 

   232 lemma CPS_eval_Kapply:

   233   assumes a: "isValue K"

   234   shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)"

   235   using a

   236 proof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all)

   237   case (Var name K)

   238   assume *: "isValue K"

   239   obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast

   240   show "(name~)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ name~" using * a

   241     by simp (rule evbeta', simp_all add: fresh_at_base)

   242 next

   243   fix name :: name and lt K

   244   assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K"

   245   obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast

   246   then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis

   247   show "Abs name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Abs name (lt*)" using * a b

   248     by simp (rule evbeta', simp_all)

   249 next

   250   fix lt1 lt2 K

   251   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"

   252   obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast

   253   obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast

   254   obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast

   255   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"

   256     "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

   257   have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K))" using * d

   258     by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base)

   259   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1")

   260     assume e: "isValue lt1"

   261     have "lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (lt2* $ Abs c (b~ $ c~ $ K)) $ lt1+"

   262       using * d e by simp

   263     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Abs c (lt1+ $ c~ $ K)"

   264       by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base)

   265     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")

   266       assume f: "isValue lt2"

   267       have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp

   268       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K"

   269         by (rule evbeta', simp_all add: d e f)

   270       finally show ?thesis using * d e f by simp

   271     next

   272       assume f: "\<not> isValue lt2"

   273       have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs c (lt1+ $ c~ $ K)" using * d e f by simp

   274       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis

   275       finally show ?thesis using * d e f by simp

   276     qed

   277     finally show ?thesis .

   278   qed (metis Kapply.simps(5) isValue.simps(2) * d)

   279   finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" .

   280 qed

   281 

   282 lemma Kapply_eval:

   283   assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"

   284   shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  (N; K)"

   285   using assms

   286 proof (induct arbitrary: K rule: eval.induct)

   287   case (evbeta x V M)

   288   fix K

   289   assume a: "isValue K" "isValue V" "atom x \<sharp> V"

   290   have "Abs x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M*)[V+/x] $ K)"

   291     by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)

   292   also have "... = ((M[V/x])* $ K)" by (simp add: CPS_subst_fv a)

   293   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (M[V/x] ; K)" by (rule CPS_eval_Kapply, simp_all add: a)

   294   finally show "(Abs x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  (M[V/x] ; K)" using a by simp

   295 next

   296   case (ev1 V M N)

   297   fix V M N K

   298   assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K"

   299   obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast

   300   show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N")

   301     assume "\<not> isValue N"

   302     then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp

   303   next

   304     assume n: "isValue N"

   305     have c: "M; Abs a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs a (V+ $ a~ $ K) $ N+" using a b by (simp add: n)

   306     also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n)

   307     finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n)

   308   qed

   309 next

   310   case (ev2 M M' N)

   311   assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow>  M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K"

   312   obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast

   313   obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast

   314   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"

   315     "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all

   316   have "M $ N ; K  \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Abs a (N* $ Abs b (a~ $ b~ $ K))" using * d by simp

   317   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'")

   318     assume "\<not> isValue M'"

   319     then show ?thesis using * d by (simp_all add: evs1)

   320   next

   321     assume e: "isValue M'"

   322     then have "M' ; Abs a (N* $ Abs b (a~ $ b~ $ K)) = Abs a (N* $ Abs b (a~ $ b~ $ K)) $ M'+" by simp

   323     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Abs b (a~ $ b~ $ K))[M'+/a]"

   324       by (rule evbeta') (simp_all add: fresh_at_base e d)

   325     also have "... = N* $ Abs b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base)

   326     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N")

   327       assume f: "isValue N"

   328       have "N* $ Abs b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (M'+ $ b~ $ K) $ N+"

   329         by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1)

   330       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1)

   331       finally show ?thesis .

   332     next

   333       assume "\<not> isValue N"

   334       then show ?thesis using d e

   335         by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2))

   336     qed

   337     finally show ?thesis .

   338   qed

   339   finally show ?case .

   340 qed

   341 

   342 lemma Kapply_eval_rtrancl:

   343   assumes H: "M \<longrightarrow>\<^isub>\<beta>\<^sup>*  N" and "isValue K"

   344   shows "(M;K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N;K)"

   345   using H

   346   by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+

   347 

   348 lemma

   349   assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"

   350   shows "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"

   351 proof-

   352   obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast

   353   have e: "Abs x (x~) = Abs y (y~)"

   354     by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)

   355   have "M* $ Abs x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Abs x (x~)"

   356     by(rule CPS_eval_Kapply,simp_all add: assms)

   357   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Abs x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)

   358   also have "... = V ; Abs y (y~)" using e by (simp only:)

   359   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *)

   360   finally show "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .

   361 qed

   362 

   363 end

   364 

   365 

   366