header {* CPS conversion *}theory CPS1_Plotkinimports Ltbeginlemma Abs_lst_fcb2: fixes as bs :: "atom list" and x y :: "'b :: fs" and c::"'c::fs" assumes eq: "[as]lst. x = [bs]lst. y" and fcb1: "(set as) \<sharp>* c \<Longrightarrow> (set as) \<sharp>* f as x c" and fresh1: "set as \<sharp>* c" and fresh2: "set bs \<sharp>* c" and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c" and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c" shows "f as x c = f bs y c"proof - have "supp (as, x, c) supports (f as x c)" unfolding supports_def fresh_def[symmetric] by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) then have fin1: "finite (supp (f as x c))" by (auto intro: supports_finite simp add: finite_supp) have "supp (bs, y, c) supports (f bs y c)" unfolding supports_def fresh_def[symmetric] by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) then have fin2: "finite (supp (f bs y c))" by (auto intro: supports_finite simp add: finite_supp) obtain q::"perm" where fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and fr2: "supp q \<sharp>* Abs_lst as x" and inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)" using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] fin1 fin2 by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp also have "\<dots> = Abs_lst as x" by (simp only: fr2 perm_supp_eq) finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp then obtain r::perm where qq1: "q \<bullet> x = r \<bullet> y" and qq2: "q \<bullet> as = r \<bullet> bs" and qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs" apply(drule_tac sym) apply(simp only: Abs_eq_iff2 alphas) apply(erule exE) apply(erule conjE)+ apply(drule_tac x="p" in meta_spec) apply(simp add: set_eqvt) apply(blast) done have "(set as) \<sharp>* f as x c" apply(rule fcb1) apply(rule fresh1) done then have "q \<bullet> ((set as) \<sharp>* f as x c)" by (simp add: permute_bool_def) then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c" apply(simp add: fresh_star_eqvt set_eqvt) apply(subst (asm) perm1) using inc fresh1 fr1 apply(auto simp add: fresh_star_def fresh_Pair) done then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp then have "r \<bullet> ((set bs) \<sharp>* f bs y c)" apply(simp add: fresh_star_eqvt set_eqvt) apply(subst (asm) perm2[symmetric]) using qq3 fresh2 fr1 apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) done then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def) have "f as x c = q \<bullet> (f as x c)" apply(rule perm_supp_eq[symmetric]) using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def) also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" apply(rule perm1) using inc fresh1 fr1 by (auto simp add: fresh_star_def) also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp also have "\<dots> = r \<bullet> (f bs y c)" apply(rule perm2[symmetric]) using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) also have "... = f bs y c" apply(rule perm_supp_eq) using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) finally show ?thesis by simpqedlemma Abs_lst1_fcb2: fixes a b :: "atom" and x y :: "'b :: fs" and c::"'c :: fs" assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" and fcb1: "a \<sharp> c \<Longrightarrow> a \<sharp> f a x c" and fresh: "{a, b} \<sharp>* c" and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c" and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c" shows "f a x c = f b y c"using eapply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"])apply(simp_all)using fcb1 fresh perm1 perm2apply(simp_all add: fresh_star_def)donenominal_primrec CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)where "atom k \<sharp> x \<Longrightarrow> (x~)* = (Abs k ((k~) $ (x~)))"| "atom k \<sharp> (x, M) \<Longrightarrow> (Abs x M)* = Abs k (k~ $ Abs x (M*))"| "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow> (M $ N)* = Abs k (M* $ Abs m (N* $ Abs n (m~ $ n~ $ k~)))"unfolding eqvt_def CPS_graph_defapply (rule, perm_simp, rule, rule)apply (simp_all add: fresh_Pair_elim)apply (rule_tac y="x" in lt.exhaust)apply (auto)apply (rule_tac x="name" and ?'a="name" in obtain_fresh)apply (simp_all add: fresh_at_base)[3]apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)apply (simp add: fresh_Pair_elim fresh_at_base)[2]apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)apply (rule_tac x="(a, aa)" and ?'a="name" in obtain_fresh)apply (simp add: fresh_Pair_elim fresh_at_base)apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)--"-"apply(rule_tac s="[[atom ka]]lst. ka~ $ Abs x (CPS_sumC M)" in trans)apply (case_tac "k = ka")apply simpapply(simp (no_asm) add: Abs1_eq_iff del:eqvts)apply (simp del: eqvts add: lt.fresh fresh_at_base)apply (simp only: lt.perm_simps(1) lt.perm_simps(3) flip_def[symmetric] lt.eq_iff(3))apply (subst flip_at_base_simps(2))apply simpapply (intro conjI refl)apply (rule flip_fresh_fresh[symmetric])apply (simp_all add: lt.fresh)apply (metis fresh_eqvt_at lt.fsupp)apply (case_tac "ka = x")apply simp_all[2]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)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)--"-"apply (simp add: Abs1_eq(3))apply (erule Abs_lst1_fcb2)apply (simp_all add: Abs_fresh_iff fresh_Nil fresh_star_def eqvt_at_def)[4]--"-"apply (rename_tac k' M N m' n')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> atom m \<sharp> CPS_sumC N \<and> atom m' \<sharp> CPS_sumC N")prefer 2apply (intro conjI)apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+apply clarifyapply (case_tac "k = k'", case_tac [!] "m' = k",case_tac [!]"m = k'",case_tac[!] "m = m'")apply (simp_all add: Abs1_eq_iff lt.fresh flip_def[symmetric] fresh_at_base flip_fresh_fresh permute_eq_iff)by (metis flip_at_base_simps(3) flip_at_simps(2) flip_commute permute_flip_at)+termination by (relation "measure size") (simp_all add: lt.size)lemmas [simp] = fresh_Pair_elim CPS.simps(2,3)[simplified fresh_Pair_elim]lemma [simp]: "supp (M*) = supp M" by (induct rule: CPS.induct, simp_all add: lt.supp supp_at_base fresh_at_base fresh_def supp_Pair) (simp_all only: atom_eq_iff[symmetric], blast+)lemma [simp]: "x \<sharp> M* = x \<sharp> M" unfolding fresh_def by simp(* Will be provided automatically by nominal_primrec *)lemma CPS_eqvt[eqvt]: shows "p \<bullet> M* = (p \<bullet> M)*" apply (induct M rule: lt.induct) apply (rule_tac x="(name, p \<bullet> name, p)" and ?'a="name" in obtain_fresh) apply simp apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric]) apply (metis atom_eqvt flip_fresh_fresh fresh_perm atom_eq_iff fresh_at_base) apply (rule_tac x="(name, lt, p \<bullet> name, p \<bullet> lt, p)" and ?'a="name" in obtain_fresh) apply simp apply (metis atom_eqvt fresh_perm atom_eq_iff) apply (rule_tac x="(lt1, p \<bullet> lt1, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh) apply (rule_tac x="(a, lt2, p \<bullet> lt2, p)" and ?'a="name" in obtain_fresh) apply (rule_tac x="(a, aa, p)" and ?'a="name" in obtain_fresh) apply (simp) apply (simp add: Abs1_eq_iff lt.fresh flip_def[symmetric]) apply (metis atom_eqvt fresh_perm atom_eq_iff) donenominal_primrec convert:: "lt => lt" ("_+" [250] 250)where "(Var x)+ = Var x"| "(Abs x M)+ = Abs x (M*)"| "(M $ N)+ = M $ N" unfolding convert_graph_def eqvt_def apply (rule, perm_simp, rule, rule) apply (erule lt.exhaust) apply (simp_all) apply blast apply (simp add: Abs1_eq_iff CPS_eqvt) by blasttermination by (relation "measure size") (simp_all add: lt.size)lemma convert_supp[simp]: shows "supp (M+) = supp M" by (induct M rule: lt.induct, simp_all add: lt.supp)lemma convert_fresh[simp]: shows "x \<sharp> (M+) = x \<sharp> M" unfolding fresh_def by simplemma convert_eqvt[eqvt]: shows "p \<bullet> (M+) = (p \<bullet> M)+" by (nominal_induct M rule: lt.strong_induct, auto simp add: CPS_eqvt)lemma [simp]: shows "isValue (p \<bullet> (M::lt)) = isValue M" by (nominal_induct M rule: lt.strong_induct) autolemma [eqvt]: shows "p \<bullet> isValue M = isValue (p \<bullet> M)" by (induct M rule: lt.induct) (perm_simp, rule refl)+nominal_primrec Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100)where "Kapply (Abs x M) K = K $ (Abs x M)+"| "Kapply (Var x) K = K $ Var x"| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"| "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> Kapply (M $ N) K = N; (Abs n (M+ $ Var n $ K))"| "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow> Kapply (M $ N) K = M; (Abs m (N* $ (Abs n (Var m $ Var n $ K))))" unfolding Kapply_graph_def eqvt_def apply (rule, perm_simp, rule, rule)apply (simp_all)apply (case_tac x)apply (rule_tac y="a" in lt.exhaust)apply (auto)apply (case_tac "isValue lt1")apply (case_tac "isValue lt2")apply (auto)[1]apply (rule_tac x="(lt1, ba)" and ?'a="name" in obtain_fresh)apply (simp add: fresh_Pair_elim fresh_at_base)apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh)apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh)apply (simp add: fresh_Pair_elim fresh_at_base)apply (auto simp add: Abs1_eq_iff eqvts)[1]apply (rename_tac M N u K)apply (subgoal_tac "Abs n (M+ $ n~ $ K) = Abs u (M+ $ u~ $ K)")apply (simp only:)apply (auto simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base flip_fresh_fresh[symmetric])[1]apply (subgoal_tac "Abs m (Na* $ Abs n (m~ $ n~ $ Ka)) = Abs ma (Na* $ Abs na (ma~ $ na~ $ Ka))")apply (simp only:)apply (simp add: Abs1_eq_iff flip_def[symmetric] lt.fresh fresh_at_base)apply (subgoal_tac "Ka = (n \<leftrightarrow> na) \<bullet> Ka")apply (subgoal_tac "Ka = (m \<leftrightarrow> ma) \<bullet> Ka")apply (subgoal_tac "Ka = (n \<leftrightarrow> (m \<leftrightarrow> ma) \<bullet> na) \<bullet> Ka")apply (case_tac "m = ma")apply simp_allapply ruleapply (auto simp add: flip_fresh_fresh[symmetric])apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+donetermination by (relation "measure (\<lambda>(t, _). size t)") (simp_all add: lt.size)section{* lemma related to Kapply *}lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)" by (nominal_induct V rule: lt.strong_induct) autosection{* lemma related to CPS conversion *}lemma value_CPS: assumes "isValue V" and "atom a \<sharp> V" shows "V* = Abs a (a~ $ V+)" using assmsproof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh) fix name :: name and lt aa assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Abs b (b~ $ lt+)" "atom aa \<sharp> lt \<or> aa = name" obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast show "Abs name lt* = Abs aa (aa~ $ Abs name (lt*))" using a b by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)qedsection{* first lemma CPS subst *}lemma CPS_subst_fv: assumes *:"isValue V" shows "((M[V/x])* = (M*)[V+/x])"using * proof (nominal_induct M avoiding: V x rule: lt.strong_induct) case (Var name) assume *: "isValue V" obtain a :: name where a: "atom a \<sharp> (x, name, V)" using obtain_fresh by blast show "((name~)[V/x])* = (name~)*[V+/x]" using a by (simp add: fresh_at_base * value_CPS)next case (Abs name lt V x) assume *: "atom name \<sharp> V" "atom name \<sharp> x" "\<And>b ba. isValue b \<Longrightarrow> (lt[b/ba])* = lt*[b+/ba]" "isValue V" obtain a :: name where a: "atom a \<sharp> (name, lt, lt[V/x], x, V)" using obtain_fresh by blast show "(Abs name lt[V/x])* = Abs name lt*[V+/x]" using * a by (simp add: fresh_at_base)next case (App lt1 lt2 V x) 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]" "isValue V" obtain a :: name where a: "atom a \<sharp> (lt1[V/x], lt1, lt2[V/x], lt2, V, x)" using obtain_fresh by blast obtain b :: name where b: "atom b \<sharp> (lt2[V/x], lt2, a, V, x)" using obtain_fresh by blast obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast show "((lt1 $ lt2)[V/x])* = (lt1 $ lt2)*[V+/x]" using * a b c by (simp add: fresh_at_base)qedlemma [simp]: "isValue V \<Longrightarrow> isValue (V+)" by (nominal_induct V rule: lt.strong_induct, auto)lemma CPS_eval_Kapply: assumes a: "isValue K" shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)" using aproof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all) case (Var name K) assume *: "isValue K" obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast show "(name~)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ name~" using * a by simp (rule evbeta', simp_all add: fresh_at_base)next fix name :: name and lt K assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K" obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis show "Abs name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Abs name (lt*)" using * a b by simp (rule evbeta', simp_all)next fix lt1 lt2 K 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" obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast 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" "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 have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K))" using * d by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base) also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1") assume e: "isValue lt1" have "lt1* $ Abs b (lt2* $ Abs c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (lt2* $ Abs c (b~ $ c~ $ K)) $ lt1+" using * d e by simp also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Abs c (lt1+ $ c~ $ K)" by (rule evbeta', simp_all add: * d e, metis d(12) fresh_at_base) also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2") assume f: "isValue lt2" have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K" by (rule evbeta', simp_all add: d e f) finally show ?thesis using * d e f by simp next assume f: "\<not> isValue lt2" have "lt2* $ Abs c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs c (lt1+ $ c~ $ K)" using * d e f by simp also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Abs a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis finally show ?thesis using * d e f by simp qed finally show ?thesis . qed (metis Kapply.simps(5) isValue.simps(2) * d) finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" .qedlemma Kapply_eval: assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K" shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N; K)" using assmsproof (induct arbitrary: K rule: eval.induct) case (evbeta x V M) fix K assume a: "isValue K" "isValue V" "atom x \<sharp> V" have "Abs x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M*)[V+/x] $ K)" by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1) also have "... = ((M[V/x])* $ K)" by (simp add: CPS_subst_fv a) also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (M[V/x] ; K)" by (rule CPS_eval_Kapply, simp_all add: a) finally show "(Abs x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M[V/x] ; K)" using a by simpnext case (ev1 V M N) fix V M N K assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K" obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N") assume "\<not> isValue N" then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp next assume n: "isValue N" 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) also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n) finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n) qednext case (ev2 M M' N) assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K" obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast 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" "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all have "M $ N ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Abs a (N* $ Abs b (a~ $ b~ $ K))" using * d by simp also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'") assume "\<not> isValue M'" then show ?thesis using * d by (simp_all add: evs1) next assume e: "isValue M'" then have "M' ; Abs a (N* $ Abs b (a~ $ b~ $ K)) = Abs a (N* $ Abs b (a~ $ b~ $ K)) $ M'+" by simp also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Abs b (a~ $ b~ $ K))[M'+/a]" by (rule evbeta') (simp_all add: fresh_at_base e d) also have "... = N* $ Abs b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base) also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N") assume f: "isValue N" have "N* $ Abs b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Abs b (M'+ $ b~ $ K) $ N+" by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1) also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1) finally show ?thesis . next assume "\<not> isValue N" then show ?thesis using d e by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2)) qed finally show ?thesis . qed finally show ?case .qedlemma Kapply_eval_rtrancl: assumes H: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* N" and "isValue K" shows "(M;K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N;K)" using H by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+lemma assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V" shows "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"proof- obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast have e: "Abs x (x~) = Abs y (y~)" by (simp add: Abs1_eq_iff lt.fresh fresh_at_base) have "M* $ Abs x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Abs x (x~)" by(rule CPS_eval_Kapply,simp_all add: assms) also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Abs x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms) also have "... = V ; Abs y (y~)" using e by (simp only:) also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *) finally show "M* $ (Abs x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .qedend