Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/CPS/CPS1_Plotkin.thy
changeset 3187 b3d97424b130
parent 3186 425b4c406d80
child 3191 0440bc1a2438
equal deleted inserted replaced
3186:425b4c406d80 3187:b3d97424b130 
     4 begin
 
     4 begin
 
     5 
     5 
     6 nominal_primrec
 
     6 nominal_primrec
 
     7   CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
 
     7   CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
 
     8 where
 
     8 where
 
     9   "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $ (x~)))"
 
     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*))"
 
    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>
 
    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~)))"
 
    12     (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))"
 
    13 unfolding eqvt_def CPS_graph_def
 
    13 unfolding eqvt_def CPS_graph_def
 
    14 apply (rule, perm_simp, rule, rule)
 
    14 apply (rule, perm_simp, rule, rule)
 
    15 apply (simp_all add: fresh_Pair_elim)
 
    15 apply (simp_all add: fresh_Pair_elim)
 
    16 apply (rule_tac y="x" in lt.exhaust)
 
    16 apply (rule_tac y="x" in lt.exhaust)
 
    17 apply (auto)[3]
 
    17 apply (auto)[3]
 
    23 apply (simp add: fresh_Pair_elim fresh_at_base)
 
    23 apply (simp add: fresh_Pair_elim fresh_at_base)
 
    24 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
 
    24 apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
 
    25 apply (simp add: fresh_Pair_elim fresh_at_base)[2]
 
    25 apply (simp add: fresh_Pair_elim fresh_at_base)[2]
 
    26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
 
    26 apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
 
    27 --"-"
 
    27 --"-"
 
    28 apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
 
    28 apply(rule_tac s="[[atom ka]]lst. ka~ $$ Lam x (CPS_sumC M)" in trans)
 
    29 apply (case_tac "k = ka")
 
    29 apply (case_tac "k = ka")
 
    30 apply simp
 
    30 apply simp
 
    31 thm Abs1_eq_iff
 
    31 thm Abs1_eq_iff
 
    32 apply(subst Abs1_eq_iff)
 
    32 apply(subst Abs1_eq_iff)
 
    33 apply(auto)[2]
 
    33 apply(auto)[2]
 
    76 nominal_primrec
 
    76 nominal_primrec
 
    77   convert:: "lt => lt" ("_+" [250] 250)
 
    77   convert:: "lt => lt" ("_+" [250] 250)
 
    78 where
 
    78 where
 
    79   "(Var x)+ = Var x"
 
    79   "(Var x)+ = Var x"
 
    80 | "(Lam x M)+ = Lam x (M*)"
 
    80 | "(Lam x M)+ = Lam x (M*)"
 
    81 | "(M $ N)+ = M $ N"
 
    81 | "(M $$ N)+ = M $$ N"
 
    82   unfolding convert_graph_def eqvt_def
 
    82   unfolding convert_graph_def eqvt_def
 
    83   apply (rule, perm_simp, rule, rule)
 
    83   apply (rule, perm_simp, rule, rule)
 
    84   apply (erule lt.exhaust)
 
    84   apply (erule lt.exhaust)
 
    85   apply (simp_all)
 
    85   apply (simp_all)
 
    86   apply blast
 
    86   apply blast
 
   103   by (nominal_induct M rule: lt.strong_induct) auto
 
   103   by (nominal_induct M rule: lt.strong_induct) auto
 
   104 
   104 
   105 nominal_primrec
 
   105 nominal_primrec
 
   106   Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)
 
   106   Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt"       (infixl ";" 100)
 
   107 where
 
   107 where
 
   108   "Kapply (Lam x M) K = K $ (Lam x M)+"
 
   108   "Kapply (Lam x M) K = K $$ (Lam x M)+"
 
   109 | "Kapply (Var x) K = K $ Var x"
 
   109 | "Kapply (Var x) K = K $$ Var x"
 
   110 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"
 
   110 | "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $$ N) K = M+ $$ N+ $$ K"
 
   111 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
 
   111 | "isValue M \<Longrightarrow> \<not>isValue N \<Longrightarrow> atom n \<sharp> M \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
 
   112     Kapply (M $ N) K = N; (Lam n (M+ $ Var n $ K))"
 
   112     Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))"
 
   113 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
 
   113 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
 
   114     Kapply (M $ N) K = M; (Lam m (N*  $ (Lam n (Var m $ Var n $ K))))"
 
   114     Kapply (M $$ N) K = M; (Lam m (N*  $$ (Lam n (Var m $$ Var n $$ K))))"
 
   115   unfolding Kapply_graph_def eqvt_def
 
   115   unfolding Kapply_graph_def eqvt_def
 
   116   apply (rule, perm_simp, rule, rule)
 
   116   apply (rule, perm_simp, rule, rule)
 
   117 apply (simp_all)
 
   117 apply (simp_all)
 
   118 apply (case_tac x)
 
   118 apply (case_tac x)
 
   119 apply (rule_tac y="a" in lt.exhaust)
 
   119 apply (rule_tac y="a" in lt.exhaust)
 
   126 apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh)
 
   126 apply (rule_tac x="(lt2, ba)" and ?'a="name" in obtain_fresh)
 
   127 apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh)
 
   127 apply (rule_tac x="(a, ba)" and ?'a="name" in obtain_fresh)
 
   128 apply (simp add: fresh_Pair_elim fresh_at_base)
 
   128 apply (simp add: fresh_Pair_elim fresh_at_base)
 
   129 apply (auto simp add: Abs1_eq_iff eqvts)[1]
 
   129 apply (auto simp add: Abs1_eq_iff eqvts)[1]
 
   130 apply (rename_tac M N u K)
 
   130 apply (rename_tac M N u K)
 
   131 apply (subgoal_tac "Lam n (M+ $ n~ $ K) =  Lam u (M+ $ u~ $ K)")
 
   131 apply (subgoal_tac "Lam n (M+ $$ n~ $$ K) =  Lam u (M+ $$ u~ $$ K)")
 
   132 apply (simp only:)
 
   132 apply (simp only:)
 
   133 apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1]
 
   133 apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1]
 
   134 apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
 
   134 apply (subgoal_tac "Lam m (Na* $$ Lam n (m~ $$ n~ $$ Ka)) = Lam ma (Na* $$ Lam na (ma~ $$ na~ $$ Ka))")
 
   135 apply (simp only:)
 
   135 apply (simp only:)
 
   136 apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)
 
   136 apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)
 
   137 apply(simp_all add: flip_def[symmetric])
 
   137 apply(simp_all add: flip_def[symmetric])
 
   138 apply (case_tac "m = ma")
 
   138 apply (case_tac "m = ma")
 
   139 apply simp_all
 
   139 apply simp_all
 
   144 termination (eqvt)
 
   144 termination (eqvt)
 
   145   by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
 
   145   by (relation "measure (\<lambda>(t, _). size t)") (simp_all)
 
   146 
   146 
   147 section{* lemma related to Kapply *}
 
   147 section{* lemma related to Kapply *}
 
   148 
   148 
   149 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)"
 
   149 lemma [simp]: "isValue V \<Longrightarrow> V; K = K $$ (V+)"
 
   150   by (nominal_induct V rule: lt.strong_induct) auto
 
   150   by (nominal_induct V rule: lt.strong_induct) auto
 
   151 
   151 
   152 section{* lemma related to CPS conversion *}
 
   152 section{* lemma related to CPS conversion *}
 
   153 
   153 
   154 lemma value_CPS:
 
   154 lemma value_CPS:
 
   155   assumes "isValue V"
 
   155   assumes "isValue V"
 
   156   and "atom a \<sharp> V"
 
   156   and "atom a \<sharp> V"
 
   157   shows "V* = Lam a (a~ $ V+)"
 
   157   shows "V* = Lam a (a~ $$ V+)"
 
   158   using assms
 
   158   using assms
 
   159 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh)
 
   159 proof (nominal_induct V avoiding: a rule: lt.strong_induct, simp_all add: lt.fresh)
 
   160   fix name :: name and lt aa
 
   160   fix name :: name and lt aa
 
   161   assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $ lt+)"
 
   161   assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam b (b~ $$ lt+)"
 
   162     "atom aa \<sharp> lt \<or> aa = name"
 
   162     "atom aa \<sharp> lt \<or> aa = name"
 
   163   obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast
 
   163   obtain ab :: name where b: "atom ab \<sharp> (name, lt, a)" using obtain_fresh by blast
 
   164   show "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b
 
   164   show "Lam name lt* = Lam aa (aa~ $$ Lam name (lt*))" using a b
 
   165     by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
 
   165     by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
 
   166 qed
 
   166 qed
 
   167 
   167 
   168 section{* first lemma CPS subst *}
 
   168 section{* first lemma CPS subst *}
 
   169 
   169 
   188   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+]"
 
   188   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+]"
 
   189     "isValue V"
 
   189     "isValue V"
 
   190   obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast
 
   190   obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast
 
   191   obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], lt2, a, V, x)" using obtain_fresh by blast
 
   191   obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], lt2, a, V, x)" using obtain_fresh by blast
 
   192   obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast
 
   192   obtain c :: name where c: "atom c \<sharp> (a, b, V, x)" using obtain_fresh by blast
 
   193   show "((lt1 $ lt2)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c
 
   193   show "((lt1 $$ lt2)[x ::= V])* = (lt1 $$ lt2)*[x ::= V+]" using * a b c
 
   194     by (simp add: fresh_at_base)
 
   194     by (simp add: fresh_at_base)
 
   195 qed
 
   195 qed
 
   196 
   196 
   197 lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)"
 
   197 lemma [simp]: "isValue V \<Longrightarrow> isValue (V+)"
 
   198   by (nominal_induct V rule: lt.strong_induct, auto)
 
   198   by (nominal_induct V rule: lt.strong_induct, auto)
 
   199 
   199 
   200 lemma CPS_eval_Kapply:
 
   200 lemma CPS_eval_Kapply:
 
   201   assumes a: "isValue K"
 
   201   assumes a: "isValue K"
 
   202   shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)"
 
   202   shows "(M* $$ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; K)"
 
   203   using a
 
   203   using a
 
   204 proof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all)
 
   204 proof (nominal_induct M avoiding: K rule: lt.strong_induct, simp_all)
 
   205   case (Var name K)
 
   205   case (Var name K)
 
   206   assume *: "isValue K"
 
   206   assume *: "isValue K"
 
   207   obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast
 
   207   obtain a :: name where a: "atom a \<sharp> (name, K)" using obtain_fresh by blast
 
   208   show "(name~)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ name~" using * a
 
   208   show "(name~)* $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $$ name~" using * a
 
   209     by simp (rule evbeta', simp_all add: fresh_at_base)
 
   209     by simp (rule evbeta', simp_all add: fresh_at_base)
 
   210 next
 
   210 next
 
   211   fix name :: name and lt K
 
   211   fix name :: name and lt K
 
   212   assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K"
 
   212   assume *: "atom name \<sharp> K" "\<And>b. isValue b \<Longrightarrow> lt* $$ b \<longrightarrow>\<^isub>\<beta>\<^sup>* lt ; b" "isValue K"
 
   213   obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast
 
   213   obtain a :: name where a: "atom a \<sharp> (name, K, lt)" using obtain_fresh by blast
 
   214   then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis
 
   214   then have b: "atom name \<sharp> a" using fresh_PairD(1) fresh_at_base atom_eq_iff by metis
 
   215   show "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b
 
   215   show "Lam name lt* $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $$ Lam name (lt*)" using * a b
 
   216     by simp (rule evbeta', simp_all)
 
   216     by simp (rule evbeta', simp_all)
 
   217 next
 
   217 next
 
   218   fix lt1 lt2 K
 
   218   fix lt1 lt2 K
 
   219   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"
 
   219   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"
 
   220   obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast
 
   220   obtain a :: name where a: "atom a \<sharp> (lt1, lt2, K)" using obtain_fresh by blast
 
   221   obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast
 
   221   obtain b :: name where b: "atom b \<sharp> (lt1, lt2, K, a)" using obtain_fresh by blast
 
   222   obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast
 
   222   obtain c :: name where c: "atom c \<sharp> (lt1, lt2, K, a, b)" using obtain_fresh by blast
 
   223   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"
 
   223   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"
 
   224     "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
 
   224     "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
 
   225   have "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d
 
   225   have "(lt1 $$ lt2)* $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $$ Lam b (lt2* $$ Lam c (b~ $$ c~ $$ K))" using * d
 
   226     by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base)
 
   226     by (simp add: fresh_at_base) (rule evbeta', simp_all add: fresh_at_base)
 
   227   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt1")
 
   227   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $$ lt2 ; K" proof (cases "isValue lt1")
 
   228     assume e: "isValue lt1"
 
   228     assume e: "isValue lt1"
 
   229     have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
 
   229     have "lt1* $$ Lam b (lt2* $$ Lam c (b~ $$ c~ $$ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $$ Lam c (b~ $$ c~ $$ K)) $$ lt1+"
 
   230       using * d e by simp
 
   230       using * d e by simp
 
   231     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
 
   231     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $$ Lam c (lt1+ $$ c~ $$ K)"
 
   232       by (rule evbeta')(simp_all add: * d e)
 
   232       by (rule evbeta')(simp_all add: * d e)
 
   233     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
 
   233     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $$ lt2 ; K" proof (cases "isValue lt2")
 
   234       assume f: "isValue lt2"
 
   234       assume f: "isValue lt2"
 
   235       have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
 
   235       have "lt2* $$ Lam c (lt1+ $$ c~ $$ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $$ c~ $$ K) $$ lt2+" using * d e f by simp
 
   236       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K"
 
   236       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $$ lt2+ $$ K"
 
   237         by (rule evbeta', simp_all add: d e f)
 
   237         by (rule evbeta', simp_all add: d e f)
 
   238       finally show ?thesis using * d e f by simp
 
   238       finally show ?thesis using * d e f by simp
 
   239     next
 
   239     next
 
   240       assume f: "\<not> isValue lt2"
 
   240       assume f: "\<not> isValue lt2"
 
   241       have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp
 
   241       have "lt2* $$ Lam c (lt1+ $$ c~ $$ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $$ c~ $$ K)" using * d e f by simp
 
   242       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis
 
   242       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $$ a~ $$ K)" using Kapply.simps(4) d e evs1 f by metis
 
   243       finally show ?thesis using * d e f by simp
 
   243       finally show ?thesis using * d e f by simp
 
   244     qed
 
   244     qed
 
   245     finally show ?thesis .
 
   245     finally show ?thesis .
 
   246   qed (metis Kapply.simps(5) isValue.simps(2) * d)
 
   246   qed (metis Kapply.simps(5) isValue.simps(2) * d)
 
   247   finally show "(lt1 $ lt2)* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" .
 
   247   finally show "(lt1 $$ lt2)* $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $$ lt2 ; K" .
 
   248 qed
 
   248 qed
 
   249 
   249 
   250 lemma Kapply_eval:
 
   250 lemma Kapply_eval:
 
   251   assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"
 
   251   assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"
 
   252   shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  (N; K)"
 
   252   shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  (N; K)"
 
   253   using assms
 
   253   using assms
 
   254 proof (induct arbitrary: K rule: eval.induct)
 
   254 proof (induct arbitrary: K rule: eval.induct)
 
   255   case (evbeta x V M)
 
   255   case (evbeta x V M)
 
   256   fix K
 
   256   fix K
 
   257   assume a: "isValue K" "isValue V" "atom x \<sharp> V"
 
   257   assume a: "isValue K" "isValue V" "atom x \<sharp> V"
 
   258   have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)"
 
   258   have "Lam x (M*) $$ V+ $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $$ K)"
 
   259     by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)
 
   259     by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)
 
   260   also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a)
 
   260   also have "... = ((M[x ::= V])* $$ K)" by (simp add: CPS_subst_fv a)
 
   261   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
 
   261   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
 
   262   finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  ((M[x ::= V]) ; K)" using a by simp
 
   262   finally show "(Lam x M $$ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>*  ((M[x ::= V]) ; K)" using a by simp
 
   263 next
 
   263 next
 
   264   case (ev1 V M N)
 
   264   case (ev1 V M N)
 
   265   fix V M N K
 
   265   fix V M N K
 
   266   assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K"
 
   266   assume a: "isValue V" "M \<longrightarrow>\<^isub>\<beta> N" "\<And>K. isValue K \<Longrightarrow> M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* N ; K" "isValue K"
 
   267   obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast
 
   267   obtain a :: name where b: "atom a \<sharp> (V, K, M, N)" using obtain_fresh by blast
 
   268   show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" proof (cases "isValue N")
 
   268   show "V $$ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $$ N ; K" proof (cases "isValue N")
 
   269     assume "\<not> isValue N"
 
   269     assume "\<not> isValue N"
 
   270     then show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by simp
 
   270     then show "V $$ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $$ N ; K" using a b by simp
 
   271   next
 
   271   next
 
   272     assume n: "isValue N"
 
   272     assume n: "isValue N"
 
   273     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)
 
   273     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)
 
   274     also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $ N+ $ K" by (rule evbeta') (simp_all add: a b n)
 
   274     also have d: "... \<longrightarrow>\<^isub>\<beta>\<^sup>* V+ $$ N+ $$ K" by (rule evbeta') (simp_all add: a b n)
 
   275     finally show "V $ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $ N ; K" using a b by (simp add: n)
 
   275     finally show "V $$ M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* V $$ N ; K" using a b by (simp add: n)
 
   276   qed
 
   276   qed
 
   277 next
 
   277 next
 
   278   case (ev2 M M' N)
 
   278   case (ev2 M M' N)
 
   279   assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow>  M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K"
 
   279   assume *: "M \<longrightarrow>\<^isub>\<beta> M'" "\<And>K. isValue K \<Longrightarrow>  M ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; K" "isValue K"
 
   280   obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast
 
   280   obtain a :: name where a: "atom a \<sharp> (K, M, N, M')" using obtain_fresh by blast
 
   281   obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast
 
   281   obtain b :: name where b: "atom b \<sharp> (a, K, M, N, M', N+)" using obtain_fresh by blast
 
   282   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"
 
   282   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"
 
   283     "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all
 
   283     "atom b \<sharp> M" "atom b \<sharp> N" "atom b \<sharp> M'" using a b fresh_Pair by simp_all
 
   284   have "M $ N ; K  \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp
 
   284   have "M $$ N ; K  \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $$ Lam b (a~ $$ b~ $$ K))" using * d by simp
 
   285   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'")
 
   285   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $$ N ; K" proof (cases "isValue M'")
 
   286     assume "\<not> isValue M'"
 
   286     assume "\<not> isValue M'"
 
   287     then show ?thesis using * d by (simp_all add: evs1)
 
   287     then show ?thesis using * d by (simp_all add: evs1)
 
   288   next
 
   288   next
 
   289     assume e: "isValue M'"
 
   289     assume e: "isValue M'"
 
   290     then have "M' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp
 
   290     then have "M' ; Lam a (N* $$ Lam b (a~ $$ b~ $$ K)) = Lam a (N* $$ Lam b (a~ $$ b~ $$ K)) $$ M'+" by simp
 
   291     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]"
 
   291     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $$ Lam b (a~ $$ b~ $$ K))[a ::= M'+]"
 
   292       by (rule evbeta') (simp_all add: fresh_at_base e d)
 
   292       by (rule evbeta') (simp_all add: fresh_at_base e d)
 
   293     also have "... = N* $ Lam b (M'+ $ b~ $ K)" using * d by (simp add: fresh_at_base)
 
   293     also have "... = N* $$ Lam b (M'+ $$ b~ $$ K)" using * d by (simp add: fresh_at_base)
 
   294     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue N")
 
   294     also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $$ N ; K" proof (cases "isValue N")
 
   295       assume f: "isValue N"
 
   295       assume f: "isValue N"
 
   296       have "N* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+"
 
   296       have "N* $$ Lam b (M'+ $$ b~ $$ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $$ b~ $$ K) $$ N+"
 
   297         by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1)
 
   297         by (rule eval_trans, rule CPS_eval_Kapply) (simp_all add: d e f * evs1)
 
   298       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" by (rule evbeta') (simp_all add: d e f evs1)
 
   298       also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $$ N ; K" by (rule evbeta') (simp_all add: d e f evs1)
 
   299       finally show ?thesis .
 
   299       finally show ?thesis .
 
   300     next
 
   300     next
 
   301       assume "\<not> isValue N"
 
   301       assume "\<not> isValue N"
 
   302       then show ?thesis using d e
 
   302       then show ?thesis using d e
 
   303         by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2))
 
   303         by (metis CPS_eval_Kapply Kapply.simps(4) isValue.simps(2))
 
   313   using H
 
   313   using H
 
   314   by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+
 
   314   by (induct) (metis Kapply_eval assms(2) eval_trans evs1)+
 
   315 
   315 
   316 lemma
 
   316 lemma
 
   317   assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"
 
   317   assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"
 
   318   shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
 
   318   shows "M* $$ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
 
   319 proof-
 
   319 proof-
 
   320   obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast
 
   320   obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast
 
   321   have e: "Lam x (x~) = Lam y (y~)"
 
   321   have e: "Lam x (x~) = Lam y (y~)"
 
   322     by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
 
   322     by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
 
   323   have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
 
   323   have "M* $$ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
 
   324     by(rule CPS_eval_Kapply,simp_all add: assms)
 
   324     by(rule CPS_eval_Kapply,simp_all add: assms)
 
   325   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
 
   325   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
 
   326   also have "... = V ; Lam y (y~)" using e by (simp only:)
 
   326   also have "... = V ; Lam y (y~)" using e by (simp only:)
 
   327   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *)
 
   327   also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" by (simp add: assms, rule evbeta') (simp_all add: assms *)
 
   328   finally show "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
 
   328   finally show "M* $$ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
 
   329 qed
 
   329 qed
 
   330 
   330 
   331 end
 
   331 end
 
   332 
   332 
   333 
   333
nominal2