# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308229252 -32400
# Node ID 9f667f6da04f3013975d833a94c2b82a67df3c86
# Parent a30d0bb7686919a99ac6f209343a97a1f73193ff# Parent bb647489f130627f5ca820f1914fd66503d1a581
merge
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/CPS/CPS1_Plotkin.thy
--- a/Nominal/CPS/CPS1_Plotkin.thy Thu Jun 16 21:23:38 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,366 +0,0 @@
-header {* CPS conversion *}
-theory Plotkin
-imports Lt
-begin
-
-nominal_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_def
-apply (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 simp
-apply(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 simp
-apply (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_fcb)
-apply (simp add: fresh_def supp_Abs)
-apply (drule_tac a="atom xa" in fresh_eqvt_at)
-apply (simp add: finite_supp)
-apply assumption
-apply (simp add: fresh_def supp_Abs)
-apply (simp add: eqvts eqvt_at_def)
-apply simp
---"-"
-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 2
-apply (intro conjI)
-apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+
-apply clarify
-apply (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)
- done
-
-nominal_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 blast
-
-termination
- 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 simp
-
-lemma 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) auto
-
-lemma [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_all
-apply rule
-apply (auto simp add: flip_fresh_fresh[symmetric])
-apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
-done
-
-termination
- 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) auto
-
-section{* lemma related to CPS conversion *}
-
-lemma value_CPS:
- assumes "isValue V"
- and "atom a \<sharp> V"
- shows "V* = Abs a (a~ $ V+)"
- using assms
-proof (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)
-qed
-
-section{* 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)
-qed
-
-lemma [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 a
-proof (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" .
-qed
-
-lemma Kapply_eval:
- assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"
- shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N; K)"
- using assms
-proof (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 simp
-next
- 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)
- qed
-next
- 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 .
-qed
-
-lemma 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+)" .
-qed
-
-end
-
-
-
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/CPS/CPS2_DanvyNielsen.thy
--- a/Nominal/CPS/CPS2_DanvyNielsen.thy Thu Jun 16 21:23:38 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,83 +0,0 @@
-header {* CPS transformation of Danvy and Nielsen *}
-theory DanvyNielsen
-imports Lt
-begin
-
-nominal_datatype cpsctxt =
- Hole
-| CFun cpsctxt lt
-| CArg lt cpsctxt
-| CAbs x::name c::cpsctxt bind x in c
-
-nominal_primrec
- fill :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt" ("_<_>" [200, 200] 100)
-where
- fill_hole : "Hole<M> = M"
-| fill_fun : "(CFun C N)<M> = (C<M>) $ N"
-| fill_arg : "(CArg N C)<M> = N $ (C<M>)"
-| fill_abs : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Abs x (C<M>)"
- unfolding eqvt_def fill_graph_def
- apply perm_simp
- apply auto
- apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
- apply (auto simp add: fresh_star_def)
- apply (erule Abs_lst1_fcb)
- apply (simp_all add: Abs_fresh_iff)
- apply (erule fresh_eqvt_at)
- apply (simp add: finite_supp)
- apply (simp add: fresh_Pair)
- apply (simp add: eqvt_at_def swap_fresh_fresh)
- done
-
-termination
- by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
-
-lemma [eqvt]: "p \<bullet> fill c t = fill (p \<bullet> c) (p \<bullet> t)"
- by (nominal_induct c avoiding: t rule: cpsctxt.strong_induct) simp_all
-
-nominal_primrec
- ccomp :: "cpsctxt => cpsctxt => cpsctxt"
-where
- "ccomp Hole C = C"
-| "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"
-| "ccomp (CArg N C) C' = CArg N (ccomp C C')"
-| "ccomp (CFun C N) C' = CFun (ccomp C C') N"
- unfolding eqvt_def ccomp_graph_def
- apply perm_simp
- apply auto
- apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
- apply (auto simp add: fresh_star_def)
- apply blast+
- apply (erule Abs_lst1_fcb)
- apply (simp_all add: Abs_fresh_iff)
- apply (erule fresh_eqvt_at)
- apply (simp add: finite_supp)
- apply (simp add: fresh_Pair)
- apply (simp add: eqvt_at_def swap_fresh_fresh)
- done
-
-termination
- by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
-
-lemma [eqvt]: "p \<bullet> ccomp c c' = ccomp (p \<bullet> c) (p \<bullet> c')"
- by (nominal_induct c avoiding: c' rule: cpsctxt.strong_induct) simp_all
-
-nominal_primrec
- CPSv :: "lt => lt"
-and CPS :: "lt => cpsctxt" where
- "CPSv (Var x) = x~"
-| "CPS (Var x) = CFun Hole (x~)"
-| "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))"
-| "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))"
-| "CPSv (M $ N) = Abs x (Var x)"
-| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole"
-| "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
- ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))"
-| "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
- ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))"
-| "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) =
- ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))"
- apply auto
- oops --"The goals seem reasonable"
-
-end
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/CPS/CPS3_DanvyFilinski.thy Thu Jun 16 21:23:38 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,240 +0,0 @@
-header {* CPS transformation of Danvy and Filinski *}
-theory DanvyFilinski imports Lt begin
-
-nominal_primrec
- CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100)
-and
- CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
-where
- "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
-| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))"
-| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))"
-| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
-| "(x~)^l = l $ (x~)"
-| "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
-| "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"
- apply (simp only: eqvt_def CPS1_CPS2_graph_def)
- apply (rule, perm_simp, rule)
- apply auto
- apply (case_tac x)
- apply (case_tac a)
- apply (case_tac "eqvt b")
- apply (rule_tac y="aa" in lt.strong_exhaust)
- apply auto[4]
- apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
- apply (simp add: fresh_at_base Abs1_eq_iff)
- apply (case_tac b)
- apply (rule_tac y="a" in lt.strong_exhaust)
- apply auto[3]
- apply blast
- apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
- apply (simp add: fresh_at_base Abs1_eq_iff)
- apply blast
---"-"
- apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))")
- apply (simp only:)
- apply (simp add: Abs1_eq_iff)
- apply (case_tac "c=ca")
- apply simp_all[2]
- apply rule
- apply (perm_simp)
- apply (simp add: eqvt_def)
- apply (simp add: fresh_def)
- apply (rule contra_subsetD[OF supp_fun_app])
- back
- apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
---"-"
- apply (rule arg_cong)
- back
- apply simp
- apply (thin_tac "eqvt ka")
- apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
- apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
- prefer 2
- apply (simp add: Abs1_eq_iff')
- apply (case_tac "c = a")
- apply simp_all[2]
- apply rule
- apply (simp add: eqvt_at_def)
- apply (simp add: swap_fresh_fresh fresh_Pair_elim)
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
- apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
- prefer 2
- apply (simp add: Abs1_eq_iff')
- apply (case_tac "ca = a")
- apply simp_all[2]
- apply rule
- apply (simp add: eqvt_at_def)
- apply (simp add: swap_fresh_fresh fresh_Pair_elim)
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
- apply (simp only: )
- apply (erule Abs_lst1_fcb)
- apply (simp add: Abs_fresh_iff)
- apply (drule sym)
- apply (simp only:)
- apply (simp add: Abs_fresh_iff lt.fresh)
- apply clarify
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
- apply (drule sym)
- apply (drule sym)
- apply (drule sym)
- apply (simp only:)
- apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
- apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
- apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
- apply (simp add: fresh_Pair_elim)
- apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
- back
- back
- back
- apply assumption
- apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
- apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
- apply simp_all[3]
- apply rule
- apply (case_tac "c = xa")
- apply simp_all[2]
- apply (simp add: eqvt_at_def)
- apply clarify
- apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
- apply (simp add: eqvt_at_def)
- apply clarify
- apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
- apply (case_tac "c = xa")
- apply simp
- apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
- apply (simp add: atom_eqvt eqvt_at_def)
- apply (simp add: flip_fresh_fresh)
- apply (subst fresh_permute_iff)
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
- apply simp
- apply clarify
- apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
- apply (simp add: eqvt_at_def)
- apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
- apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
- apply (erule fresh_eqvt_at)
- apply (simp add: finite_supp supp_Inr)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh)
- apply rule
- apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
- apply (simp add: fresh_def supp_at_base)
- apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
---"-"
- apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
- apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
- prefer 2
- apply (simp add: Abs1_eq_iff')
- apply (case_tac "c = a")
- apply simp_all[2]
- apply rule
- apply (simp add: eqvt_at_def)
- apply (simp add: swap_fresh_fresh fresh_Pair_elim)
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
- apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
- prefer 2
- apply (simp add: Abs1_eq_iff')
- apply (case_tac "ca = a")
- apply simp_all[2]
- apply rule
- apply (simp add: eqvt_at_def)
- apply (simp add: swap_fresh_fresh fresh_Pair_elim)
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
- apply (simp only: )
- apply (erule Abs_lst1_fcb)
- apply (simp add: Abs_fresh_iff)
- apply (drule sym)
- apply (simp only:)
- apply (simp add: Abs_fresh_iff lt.fresh)
- apply clarify
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
- apply (drule sym)
- apply (drule sym)
- apply (drule sym)
- apply (simp only:)
- apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
- apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
- apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
- apply (simp add: fresh_Pair_elim)
- apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
- back
- back
- back
- apply assumption
- apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
- apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
- apply simp_all[3]
- apply rule
- apply (case_tac "c = xa")
- apply simp_all[2]
- apply (simp add: eqvt_at_def)
- apply clarify
- apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
- apply (simp add: eqvt_at_def)
- apply clarify
- apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
- apply (case_tac "c = xa")
- apply simp
- apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
- apply (simp add: atom_eqvt eqvt_at_def)
- apply (simp add: flip_fresh_fresh)
- apply (subst fresh_permute_iff)
- apply (erule fresh_eqvt_at)
- apply (simp add: supp_Inr finite_supp)
- apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
- apply simp
- apply clarify
- apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
- apply (simp add: eqvt_at_def)
- apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
- apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
- apply (erule fresh_eqvt_at)
- apply (simp add: finite_supp supp_Inr)
- apply (simp add: fresh_Inr fresh_Pair lt.fresh)
- apply rule
- apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
- apply (simp add: fresh_def supp_at_base)
- apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
- done
-
-termination
- by lexicographic_order
-
-definition psi:: "lt => lt"
- where "psi V == V*(\<lambda>x. x)"
-
-section {* Simple consequence of CPS *}
-
-lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
- apply (cases V rule: lt.exhaust)
- apply (auto simp add: psi_def)
- apply (subst CPS1.simps)
- apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
- apply rule
- apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
- apply (subst CPS1.simps(3))
- apply assumption+
- apply (subst CPS1.simps(3))
- apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
- apply assumption
- apply rule
- done
-
-end
-
-
-
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/CPS/Lt.thy
--- a/Nominal/CPS/Lt.thy Thu Jun 16 21:23:38 2011 +0900
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,131 +0,0 @@
-header {* The Call-by-Value Lambda Calculus *}
-theory Lt
-imports Nominal2
-begin
-
-atom_decl name
-
-nominal_datatype lt =
- Var name ("_~" [150] 149)
- | Abs x::"name" t::"lt" bind x in t
- | App lt lt (infixl "$" 100)
-
-nominal_primrec
- subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190)
-where
- "(y~)[L/x] = (if y = x then L else y~)"
-| "atom y\<sharp>L \<Longrightarrow> atom y\<sharp>x \<Longrightarrow> (Abs y M)[L/x] = Abs y (M[L/x])"
-| "(M $ N)[L/x] = M[L/x] $ N[L/x]"
- unfolding eqvt_def subst_graph_def
- apply(perm_simp)
- apply(auto)
- apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
- apply(simp_all add: fresh_star_def fresh_Pair)
- apply blast+
- apply (erule Abs_lst1_fcb)
- apply (simp_all add: Abs_fresh_iff)[2]
- apply(drule_tac a="atom (ya)" in fresh_eqvt_at)
- apply(simp add: finite_supp fresh_Pair)
- apply(simp_all add: fresh_Pair Abs_fresh_iff)
- apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> La = La")
- apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> xa = xa")
- apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute)
- apply (simp_all add: swap_fresh_fresh)
- done
-
-termination
- by (relation "measure (\<lambda>(t, _, _). size t)")
- (simp_all add: lt.size)
-
-lemma subst_eqvt[eqvt]:
- shows "p\<bullet>(M[V/(x::name)]) = (p\<bullet>M)[(p\<bullet>V)/(p\<bullet>x)]"
- by (induct M V x rule: subst.induct) (simp_all)
-
-lemma forget[simp]:
- shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M"
- by (nominal_induct M avoiding: x s rule: lt.strong_induct)
- (auto simp add: lt.fresh fresh_at_base)
-
-lemma [simp]: "supp ( M[V/(x::name)] ) <= (supp(M) - {atom x}) Un (supp V)"
- by (nominal_induct M avoiding: x V rule: lt.strong_induct)
- (auto simp add: lt.supp supp_at_base, blast, blast)
-
-nominal_primrec
- isValue:: "lt => bool"
-where
- "isValue (Var x) = True"
-| "isValue (Abs y N) = True"
-| "isValue (A $ B) = False"
- unfolding eqvt_def isValue_graph_def
- by (perm_simp, auto)
- (erule lt.exhaust, auto)
-
-termination
- by (relation "measure size")
- (simp_all add: lt.size)
-
-lemma is_Value_eqvt[eqvt]:
- shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)"
- by (induct M rule: lt.induct) (simp_all add: eqvts)
-
-inductive
- eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
- where
- evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Abs x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[V/x])"
-| ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')"
-| ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)"
-
-equivariance eval
-
-nominal_inductive eval
-done
-
-(*lemmas [simp] = lt.supp(2)*)
-
-lemma closedev1: assumes "s \<longrightarrow>\<^isub>\<beta> t"
- shows "supp t <= supp s"
- using assms
- by (induct, auto simp add: lt.supp)
-
-
-lemma [simp]: "~ ((Abs x M) \<longrightarrow>\<^isub>\<beta> N)"
-by (rule, erule eval.cases, simp_all)
-
-lemma [simp]: assumes "M \<longrightarrow>\<^isub>\<beta> N" shows "~ isValue M"
-using assms
-by (cases, auto)
-
-
-inductive
- eval_star :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
- where
- evs1: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
-| evs2: "\<lbrakk>M \<longrightarrow>\<^isub>\<beta> M'; M' \<longrightarrow>\<^isub>\<beta>\<^sup>* M'' \<rbrakk> \<Longrightarrow> M \<longrightarrow>\<^isub>\<beta>\<^sup>* M''"
-
-lemma eval_evs: assumes *: "M \<longrightarrow>\<^isub>\<beta> M'" shows "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M'"
-by (rule evs2, rule *, rule evs1)
-
-lemma eval_trans[trans]:
- assumes "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
- and "M2 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
- shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
- using assms
- by (induct, auto intro: evs2)
-
-lemma evs3[rule_format]: assumes "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
- shows "M2 \<longrightarrow>\<^isub>\<beta> M3 \<longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
- using assms
- by (induct, auto intro: eval_evs evs2)
-
-equivariance eval_star
-
-lemma evbeta':
- fixes x :: name
- assumes "isValue V" and "atom x\<sharp>V" and "N = (M[V/x])"
- shows "((Abs x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
- using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
-
-end
-
-
-
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/Ex/CPS/CPS1_Plotkin.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Thu Jun 16 22:00:52 2011 +0900
@@ -0,0 +1,366 @@
+header {* CPS conversion *}
+theory Plotkin
+imports Lt
+begin
+
+nominal_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_def
+apply (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 simp
+apply(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 simp
+apply (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_fcb)
+apply (simp add: fresh_def supp_Abs)
+apply (drule_tac a="atom xa" in fresh_eqvt_at)
+apply (simp add: finite_supp)
+apply assumption
+apply (simp add: fresh_def supp_Abs)
+apply (simp add: eqvts eqvt_at_def)
+apply simp
+--"-"
+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 2
+apply (intro conjI)
+apply (erule fresh_eqvt_at, simp add: finite_supp, assumption)+
+apply clarify
+apply (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)
+ done
+
+nominal_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 blast
+
+termination
+ 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 simp
+
+lemma 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) auto
+
+lemma [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_all
+apply rule
+apply (auto simp add: flip_fresh_fresh[symmetric])
+apply (metis flip_at_base_simps(3) flip_fresh_fresh permute_flip_at)+
+done
+
+termination
+ 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) auto
+
+section{* lemma related to CPS conversion *}
+
+lemma value_CPS:
+ assumes "isValue V"
+ and "atom a \<sharp> V"
+ shows "V* = Abs a (a~ $ V+)"
+ using assms
+proof (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)
+qed
+
+section{* 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)
+qed
+
+lemma [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 a
+proof (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" .
+qed
+
+lemma Kapply_eval:
+ assumes a: "M \<longrightarrow>\<^isub>\<beta> N" "isValue K"
+ shows "(M; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (N; K)"
+ using assms
+proof (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 simp
+next
+ 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)
+ qed
+next
+ 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 .
+qed
+
+lemma 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+)" .
+qed
+
+end
+
+
+
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Thu Jun 16 22:00:52 2011 +0900
@@ -0,0 +1,83 @@
+header {* CPS transformation of Danvy and Nielsen *}
+theory DanvyNielsen
+imports Lt
+begin
+
+nominal_datatype cpsctxt =
+ Hole
+| CFun cpsctxt lt
+| CArg lt cpsctxt
+| CAbs x::name c::cpsctxt bind x in c
+
+nominal_primrec
+ fill :: "cpsctxt \<Rightarrow> lt \<Rightarrow> lt" ("_<_>" [200, 200] 100)
+where
+ fill_hole : "Hole<M> = M"
+| fill_fun : "(CFun C N)<M> = (C<M>) $ N"
+| fill_arg : "(CArg N C)<M> = N $ (C<M>)"
+| fill_abs : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Abs x (C<M>)"
+ unfolding eqvt_def fill_graph_def
+ apply perm_simp
+ apply auto
+ apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+ apply (auto simp add: fresh_star_def)
+ apply (erule Abs_lst1_fcb)
+ apply (simp_all add: Abs_fresh_iff)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: finite_supp)
+ apply (simp add: fresh_Pair)
+ apply (simp add: eqvt_at_def swap_fresh_fresh)
+ done
+
+termination
+ by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
+
+lemma [eqvt]: "p \<bullet> fill c t = fill (p \<bullet> c) (p \<bullet> t)"
+ by (nominal_induct c avoiding: t rule: cpsctxt.strong_induct) simp_all
+
+nominal_primrec
+ ccomp :: "cpsctxt => cpsctxt => cpsctxt"
+where
+ "ccomp Hole C = C"
+| "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"
+| "ccomp (CArg N C) C' = CArg N (ccomp C C')"
+| "ccomp (CFun C N) C' = CFun (ccomp C C') N"
+ unfolding eqvt_def ccomp_graph_def
+ apply perm_simp
+ apply auto
+ apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+ apply (auto simp add: fresh_star_def)
+ apply blast+
+ apply (erule Abs_lst1_fcb)
+ apply (simp_all add: Abs_fresh_iff)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: finite_supp)
+ apply (simp add: fresh_Pair)
+ apply (simp add: eqvt_at_def swap_fresh_fresh)
+ done
+
+termination
+ by (relation "measure (\<lambda>(x, _). size x)") (auto simp add: cpsctxt.size)
+
+lemma [eqvt]: "p \<bullet> ccomp c c' = ccomp (p \<bullet> c) (p \<bullet> c')"
+ by (nominal_induct c avoiding: c' rule: cpsctxt.strong_induct) simp_all
+
+nominal_primrec
+ CPSv :: "lt => lt"
+and CPS :: "lt => cpsctxt" where
+ "CPSv (Var x) = x~"
+| "CPS (Var x) = CFun Hole (x~)"
+| "atom b \<sharp> M \<Longrightarrow> CPSv (Abs y M) = Abs y (Abs b ((CPS M)<Var b>))"
+| "atom b \<sharp> M \<Longrightarrow> CPS (Abs y M) = CFun Hole (Abs y (Abs b ((CPS M)<Var b>)))"
+| "CPSv (M $ N) = Abs x (Var x)"
+| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> CPS (M $ N) = CArg (CPSv M $ CPSv N) Hole"
+| "isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
+ ccomp (CPS N) (CAbs a (CArg (CPSv M $ Var a) Hole))"
+| "~isValue M \<Longrightarrow> isValue N \<Longrightarrow> atom a \<sharp> N \<Longrightarrow> CPS (M $ N) =
+ ccomp (CPS M) (CAbs a (CArg (Var a $ (CPSv N)) Hole))"
+| "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $ N) =
+ ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $ Var b) Hole))))"
+ apply auto
+ oops --"The goals seem reasonable"
+
+end
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Thu Jun 16 22:00:52 2011 +0900
@@ -0,0 +1,240 @@
+header {* CPS transformation of Danvy and Filinski *}
+theory DanvyFilinski imports Lt begin
+
+nominal_primrec
+ CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_" [100,100] 100)
+and
+ CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)
+where
+ "eqvt k \<Longrightarrow> (x~)*k = k (x~)"
+| "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))"
+| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))"
+| "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"
+| "(x~)^l = l $ (x~)"
+| "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"
+| "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"
+ apply (simp only: eqvt_def CPS1_CPS2_graph_def)
+ apply (rule, perm_simp, rule)
+ apply auto
+ apply (case_tac x)
+ apply (case_tac a)
+ apply (case_tac "eqvt b")
+ apply (rule_tac y="aa" in lt.strong_exhaust)
+ apply auto[4]
+ apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+ apply (simp add: fresh_at_base Abs1_eq_iff)
+ apply (case_tac b)
+ apply (rule_tac y="a" in lt.strong_exhaust)
+ apply auto[3]
+ apply blast
+ apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+ apply (simp add: fresh_at_base Abs1_eq_iff)
+ apply blast
+--"-"
+ apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))")
+ apply (simp only:)
+ apply (simp add: Abs1_eq_iff)
+ apply (case_tac "c=ca")
+ apply simp_all[2]
+ apply rule
+ apply (perm_simp)
+ apply (simp add: eqvt_def)
+ apply (simp add: fresh_def)
+ apply (rule contra_subsetD[OF supp_fun_app])
+ back
+ apply (simp add: supp_fun_eqvt lt.supp supp_at_base)
+--"-"
+ apply (rule arg_cong)
+ back
+ apply simp
+ apply (thin_tac "eqvt ka")
+ apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
+ apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
+ prefer 2
+ apply (simp add: Abs1_eq_iff')
+ apply (case_tac "c = a")
+ apply simp_all[2]
+ apply rule
+ apply (simp add: eqvt_at_def)
+ apply (simp add: swap_fresh_fresh fresh_Pair_elim)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
+ apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
+ prefer 2
+ apply (simp add: Abs1_eq_iff')
+ apply (case_tac "ca = a")
+ apply simp_all[2]
+ apply rule
+ apply (simp add: eqvt_at_def)
+ apply (simp add: swap_fresh_fresh fresh_Pair_elim)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
+ apply (simp only: )
+ apply (erule Abs_lst1_fcb)
+ apply (simp add: Abs_fresh_iff)
+ apply (drule sym)
+ apply (simp only:)
+ apply (simp add: Abs_fresh_iff lt.fresh)
+ apply clarify
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
+ apply (drule sym)
+ apply (drule sym)
+ apply (drule sym)
+ apply (simp only:)
+ apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
+ apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
+ apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
+ apply (simp add: fresh_Pair_elim)
+ apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
+ back
+ back
+ back
+ apply assumption
+ apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
+ apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
+ apply simp_all[3]
+ apply rule
+ apply (case_tac "c = xa")
+ apply simp_all[2]
+ apply (simp add: eqvt_at_def)
+ apply clarify
+ apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
+ apply (simp add: eqvt_at_def)
+ apply clarify
+ apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
+ apply (case_tac "c = xa")
+ apply simp
+ apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
+ apply (simp add: atom_eqvt eqvt_at_def)
+ apply (simp add: flip_fresh_fresh)
+ apply (subst fresh_permute_iff)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
+ apply simp
+ apply clarify
+ apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
+ apply (simp add: eqvt_at_def)
+ apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
+ apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: finite_supp supp_Inr)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh)
+ apply rule
+ apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
+ apply (simp add: fresh_def supp_at_base)
+ apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
+--"-"
+ apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)
+ apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")
+ prefer 2
+ apply (simp add: Abs1_eq_iff')
+ apply (case_tac "c = a")
+ apply simp_all[2]
+ apply rule
+ apply (simp add: eqvt_at_def)
+ apply (simp add: swap_fresh_fresh fresh_Pair_elim)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
+ apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
+ prefer 2
+ apply (simp add: Abs1_eq_iff')
+ apply (case_tac "ca = a")
+ apply simp_all[2]
+ apply rule
+ apply (simp add: eqvt_at_def)
+ apply (simp add: swap_fresh_fresh fresh_Pair_elim)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
+ apply (simp only: )
+ apply (erule Abs_lst1_fcb)
+ apply (simp add: Abs_fresh_iff)
+ apply (drule sym)
+ apply (simp only:)
+ apply (simp add: Abs_fresh_iff lt.fresh)
+ apply clarify
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)
+ apply (drule sym)
+ apply (drule sym)
+ apply (drule sym)
+ apply (simp only:)
+ apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")
+ apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")
+ apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")
+ apply (simp add: fresh_Pair_elim)
+ apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])
+ back
+ back
+ back
+ apply assumption
+ apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)
+ apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")
+ apply simp_all[3]
+ apply rule
+ apply (case_tac "c = xa")
+ apply simp_all[2]
+ apply (simp add: eqvt_at_def)
+ apply clarify
+ apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)
+ apply (simp add: eqvt_at_def)
+ apply clarify
+ apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)
+ apply (case_tac "c = xa")
+ apply simp
+ apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")
+ apply (simp add: atom_eqvt eqvt_at_def)
+ apply (simp add: flip_fresh_fresh)
+ apply (subst fresh_permute_iff)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: supp_Inr finite_supp)
+ apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)
+ apply simp
+ apply clarify
+ apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")
+ apply (simp add: eqvt_at_def)
+ apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")
+ apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
+ apply (erule fresh_eqvt_at)
+ apply (simp add: finite_supp supp_Inr)
+ apply (simp add: fresh_Inr fresh_Pair lt.fresh)
+ apply rule
+ apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)
+ apply (simp add: fresh_def supp_at_base)
+ apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))
+ done
+
+termination
+ by lexicographic_order
+
+definition psi:: "lt => lt"
+ where "psi V == V*(\<lambda>x. x)"
+
+section {* Simple consequence of CPS *}
+
+lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"
+ apply (cases V rule: lt.exhaust)
+ apply (auto simp add: psi_def)
+ apply (subst CPS1.simps)
+ apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
+ apply rule
+ apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)
+ apply (subst CPS1.simps(3))
+ apply assumption+
+ apply (subst CPS1.simps(3))
+ apply (simp add: eqvt_def eqvt_bound eqvt_lambda)
+ apply assumption
+ apply rule
+ done
+
+end
+
+
+
diff -r a30d0bb76869 -r 9f667f6da04f Nominal/Ex/CPS/Lt.thy
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Nominal/Ex/CPS/Lt.thy Thu Jun 16 22:00:52 2011 +0900
@@ -0,0 +1,131 @@
+header {* The Call-by-Value Lambda Calculus *}
+theory Lt
+imports Nominal2
+begin
+
+atom_decl name
+
+nominal_datatype lt =
+ Var name ("_~" [150] 149)
+ | Abs x::"name" t::"lt" bind x in t
+ | App lt lt (infixl "$" 100)
+
+nominal_primrec
+ subst :: "lt \<Rightarrow> lt \<Rightarrow> name \<Rightarrow> lt" ("_[_'/_]" [200,0,0] 190)
+where
+ "(y~)[L/x] = (if y = x then L else y~)"
+| "atom y\<sharp>L \<Longrightarrow> atom y\<sharp>x \<Longrightarrow> (Abs y M)[L/x] = Abs y (M[L/x])"
+| "(M $ N)[L/x] = M[L/x] $ N[L/x]"
+ unfolding eqvt_def subst_graph_def
+ apply(perm_simp)
+ apply(auto)
+ apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
+ apply(simp_all add: fresh_star_def fresh_Pair)
+ apply blast+
+ apply (erule Abs_lst1_fcb)
+ apply (simp_all add: Abs_fresh_iff)[2]
+ apply(drule_tac a="atom (ya)" in fresh_eqvt_at)
+ apply(simp add: finite_supp fresh_Pair)
+ apply(simp_all add: fresh_Pair Abs_fresh_iff)
+ apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> La = La")
+ apply(subgoal_tac "(atom y \<rightleftharpoons> atom ya) \<bullet> xa = xa")
+ apply(simp add: atom_eqvt eqvt_at_def Abs1_eq_iff swap_commute)
+ apply (simp_all add: swap_fresh_fresh)
+ done
+
+termination
+ by (relation "measure (\<lambda>(t, _, _). size t)")
+ (simp_all add: lt.size)
+
+lemma subst_eqvt[eqvt]:
+ shows "p\<bullet>(M[V/(x::name)]) = (p\<bullet>M)[(p\<bullet>V)/(p\<bullet>x)]"
+ by (induct M V x rule: subst.induct) (simp_all)
+
+lemma forget[simp]:
+ shows "atom x \<sharp> M \<Longrightarrow> M[s/x] = M"
+ by (nominal_induct M avoiding: x s rule: lt.strong_induct)
+ (auto simp add: lt.fresh fresh_at_base)
+
+lemma [simp]: "supp ( M[V/(x::name)] ) <= (supp(M) - {atom x}) Un (supp V)"
+ by (nominal_induct M avoiding: x V rule: lt.strong_induct)
+ (auto simp add: lt.supp supp_at_base, blast, blast)
+
+nominal_primrec
+ isValue:: "lt => bool"
+where
+ "isValue (Var x) = True"
+| "isValue (Abs y N) = True"
+| "isValue (A $ B) = False"
+ unfolding eqvt_def isValue_graph_def
+ by (perm_simp, auto)
+ (erule lt.exhaust, auto)
+
+termination
+ by (relation "measure size")
+ (simp_all add: lt.size)
+
+lemma is_Value_eqvt[eqvt]:
+ shows "p\<bullet>(isValue (M::lt)) = isValue (p\<bullet>M)"
+ by (induct M rule: lt.induct) (simp_all add: eqvts)
+
+inductive
+ eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
+ where
+ evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Abs x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[V/x])"
+| ev1: "\<lbrakk>isValue V; M \<longrightarrow>\<^isub>\<beta> M' \<rbrakk> \<Longrightarrow> (V $ M) \<longrightarrow>\<^isub>\<beta> (V $ M')"
+| ev2: "M \<longrightarrow>\<^isub>\<beta> M' \<Longrightarrow> (M $ N) \<longrightarrow>\<^isub>\<beta> (M' $ N)"
+
+equivariance eval
+
+nominal_inductive eval
+done
+
+(*lemmas [simp] = lt.supp(2)*)
+
+lemma closedev1: assumes "s \<longrightarrow>\<^isub>\<beta> t"
+ shows "supp t <= supp s"
+ using assms
+ by (induct, auto simp add: lt.supp)
+
+
+lemma [simp]: "~ ((Abs x M) \<longrightarrow>\<^isub>\<beta> N)"
+by (rule, erule eval.cases, simp_all)
+
+lemma [simp]: assumes "M \<longrightarrow>\<^isub>\<beta> N" shows "~ isValue M"
+using assms
+by (cases, auto)
+
+
+inductive
+ eval_star :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)
+ where
+ evs1: "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M"
+| evs2: "\<lbrakk>M \<longrightarrow>\<^isub>\<beta> M'; M' \<longrightarrow>\<^isub>\<beta>\<^sup>* M'' \<rbrakk> \<Longrightarrow> M \<longrightarrow>\<^isub>\<beta>\<^sup>* M''"
+
+lemma eval_evs: assumes *: "M \<longrightarrow>\<^isub>\<beta> M'" shows "M \<longrightarrow>\<^isub>\<beta>\<^sup>* M'"
+by (rule evs2, rule *, rule evs1)
+
+lemma eval_trans[trans]:
+ assumes "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
+ and "M2 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+ shows "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+ using assms
+ by (induct, auto intro: evs2)
+
+lemma evs3[rule_format]: assumes "M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M2"
+ shows "M2 \<longrightarrow>\<^isub>\<beta> M3 \<longrightarrow> M1 \<longrightarrow>\<^isub>\<beta>\<^sup>* M3"
+ using assms
+ by (induct, auto intro: eval_evs evs2)
+
+equivariance eval_star
+
+lemma evbeta':
+ fixes x :: name
+ assumes "isValue V" and "atom x\<sharp>V" and "N = (M[V/x])"
+ shows "((Abs x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
+ using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
+
+end
+
+
+