--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Tue Jun 12 01:23:52 2012 +0100
@@ -6,10 +6,10 @@
nominal_primrec
CPS :: "lt \<Rightarrow> lt" ("_*" [250] 250)
where
- "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $ (x~)))"
-| "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $ Lam x (M*))"
+ "atom k \<sharp> x \<Longrightarrow> (x~)* = (Lam k ((k~) $$ (x~)))"
+| "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))"
| "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
- (M $ N)* = Lam k (M* $ Lam m (N* $ Lam n (m~ $ n~ $ k~)))"
+ (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))"
unfolding eqvt_def CPS_graph_def
apply (rule, perm_simp, rule, rule)
apply (simp_all add: fresh_Pair_elim)
@@ -25,7 +25,7 @@
apply (simp add: fresh_Pair_elim fresh_at_base)[2]
apply (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
--"-"
-apply(rule_tac s="[[atom ka]]lst. ka~ $ Lam x (CPS_sumC M)" in trans)
+apply(rule_tac s="[[atom ka]]lst. ka~ $$ Lam x (CPS_sumC M)" in trans)
apply (case_tac "k = ka")
apply simp
thm Abs1_eq_iff
@@ -78,7 +78,7 @@
where
"(Var x)+ = Var x"
| "(Lam x M)+ = Lam x (M*)"
-| "(M $ N)+ = M $ N"
+| "(M $$ N)+ = M $$ N"
unfolding convert_graph_def eqvt_def
apply (rule, perm_simp, rule, rule)
apply (erule lt.exhaust)
@@ -105,13 +105,13 @@
nominal_primrec
Kapply :: "lt \<Rightarrow> lt \<Rightarrow> lt" (infixl ";" 100)
where
- "Kapply (Lam x M) K = K $ (Lam x M)+"
-| "Kapply (Var x) K = K $ Var x"
-| "isValue M \<Longrightarrow> isValue N \<Longrightarrow> Kapply (M $ N) K = M+ $ N+ $ K"
+ "Kapply (Lam x M) K = K $$ (Lam 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; (Lam n (M+ $ Var n $ K))"
+ Kapply (M $$ N) K = N; (Lam 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; (Lam m (N* $ (Lam n (Var m $ Var n $ K))))"
+ Kapply (M $$ N) K = M; (Lam m (N* $$ (Lam n (Var m $$ Var n $$ K))))"
unfolding Kapply_graph_def eqvt_def
apply (rule, perm_simp, rule, rule)
apply (simp_all)
@@ -128,10 +128,10 @@
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 "Lam n (M+ $ n~ $ K) = Lam u (M+ $ u~ $ K)")
+apply (subgoal_tac "Lam n (M+ $$ n~ $$ K) = Lam u (M+ $$ u~ $$ K)")
apply (simp only:)
apply (auto simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)[1]
-apply (subgoal_tac "Lam m (Na* $ Lam n (m~ $ n~ $ Ka)) = Lam ma (Na* $ Lam na (ma~ $ na~ $ Ka))")
+apply (subgoal_tac "Lam m (Na* $$ Lam n (m~ $$ n~ $$ Ka)) = Lam ma (Na* $$ Lam na (ma~ $$ na~ $$ Ka))")
apply (simp only:)
apply (simp add: Abs1_eq_iff swap_fresh_fresh fresh_at_base)
apply(simp_all add: flip_def[symmetric])
@@ -146,7 +146,7 @@
section{* lemma related to Kapply *}
-lemma [simp]: "isValue V \<Longrightarrow> V; K = K $ (V+)"
+lemma [simp]: "isValue V \<Longrightarrow> V; K = K $$ (V+)"
by (nominal_induct V rule: lt.strong_induct) auto
section{* lemma related to CPS conversion *}
@@ -154,14 +154,14 @@
lemma value_CPS:
assumes "isValue V"
and "atom a \<sharp> V"
- shows "V* = Lam a (a~ $ V+)"
+ shows "V* = Lam 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* = Lam b (b~ $ lt+)"
+ assume a: "atom name \<sharp> aa" "\<And>b. \<lbrakk>isValue lt; atom b \<sharp> lt\<rbrakk> \<Longrightarrow> lt* = Lam 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 "Lam name lt* = Lam aa (aa~ $ Lam name (lt*))" using a b
+ show "Lam name lt* = Lam aa (aa~ $$ Lam name (lt*))" using a b
by (simp add: Abs1_eq_iff fresh_at_base lt.fresh)
qed
@@ -190,7 +190,7 @@
obtain a :: name where a: "atom a \<sharp> (lt1[x ::= V], lt1, lt2[x ::= V], lt2, V, x)" using obtain_fresh by blast
obtain b :: name where b: "atom b \<sharp> (lt2[x ::= V], 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)[x ::= V])* = (lt1 $ lt2)*[x ::= V+]" using * a b c
+ show "((lt1 $$ lt2)[x ::= V])* = (lt1 $$ lt2)*[x ::= V+]" using * a b c
by (simp add: fresh_at_base)
qed
@@ -199,52 +199,52 @@
lemma CPS_eval_Kapply:
assumes a: "isValue K"
- shows "(M* $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* (M ; 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
+ 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"
+ 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 "Lam name lt* $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $ Lam name (lt*)" using * a b
+ show "Lam name lt* $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* K $$ Lam 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"
+ 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* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K))" using * d
+ have "(lt1 $$ lt2)* $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1* $$ Lam b (lt2* $$ Lam 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")
+ also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $$ lt2 ; K" proof (cases "isValue lt1")
assume e: "isValue lt1"
- have "lt1* $ Lam b (lt2* $ Lam c (b~ $ c~ $ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $ Lam c (b~ $ c~ $ K)) $ lt1+"
+ have "lt1* $$ Lam b (lt2* $$ Lam c (b~ $$ c~ $$ K)) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (lt2* $$ Lam c (b~ $$ c~ $$ K)) $$ lt1+"
using * d e by simp
- also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $ Lam c (lt1+ $ c~ $ K)"
+ also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2* $$ Lam c (lt1+ $$ c~ $$ K)"
by (rule evbeta')(simp_all add: * d e)
- also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $ lt2 ; K" proof (cases "isValue lt2")
+ also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $$ lt2 ; K" proof (cases "isValue lt2")
assume f: "isValue lt2"
- have "lt2* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam c (lt1+ $ c~ $ K) $ lt2+" using * d e f by simp
- also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1+ $ lt2+ $ K"
+ have "lt2* $$ Lam c (lt1+ $$ c~ $$ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam 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* $ Lam c (lt1+ $ c~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $ c~ $ K)" using * d e f by simp
- also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam a (lt1+ $ a~ $ K)" using Kapply.simps(4) d e evs1 f by metis
+ have "lt2* $$ Lam c (lt1+ $$ c~ $$ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam c (lt1+ $$ c~ $$ K)" using * d e f by simp
+ also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* lt2 ; Lam 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" .
+ finally show "(lt1 $$ lt2)* $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* lt1 $$ lt2 ; K" .
qed
lemma Kapply_eval:
@@ -255,24 +255,24 @@
case (evbeta x V M)
fix K
assume a: "isValue K" "isValue V" "atom x \<sharp> V"
- have "Lam x (M*) $ V+ $ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $ K)"
+ have "Lam x (M*) $$ V+ $$ K \<longrightarrow>\<^isub>\<beta>\<^sup>* (((M*)[x ::= V+]) $$ K)"
by (rule evs2,rule ev2,rule Lt.evbeta) (simp_all add: fresh_def a[simplified fresh_def] evs1)
- also have "... = ((M[x ::= V])* $ K)" by (simp add: CPS_subst_fv a)
+ also have "... = ((M[x ::= V])* $$ K)" by (simp add: CPS_subst_fv a)
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" by (rule CPS_eval_Kapply, simp_all add: a)
- finally show "(Lam x M $ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; K)" using a by simp
+ finally show "(Lam x M $$ V ; K) \<longrightarrow>\<^isub>\<beta>\<^sup>* ((M[x ::= V]) ; 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")
+ 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
+ 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; Lam a (V+ $ a~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam 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)
+ 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)
+ 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)
@@ -281,21 +281,21 @@
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' ; Lam a (N* $ Lam b (a~ $ b~ $ K))" using * d by simp
- also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* M' $ N ; K" proof (cases "isValue M'")
+ have "M $$ N ; K \<longrightarrow>\<^isub>\<beta>\<^sup>* M' ; Lam a (N* $$ Lam 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' ; Lam a (N* $ Lam b (a~ $ b~ $ K)) = Lam a (N* $ Lam b (a~ $ b~ $ K)) $ M'+" by simp
- also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $ Lam b (a~ $ b~ $ K))[a ::= M'+]"
+ then have "M' ; Lam a (N* $$ Lam b (a~ $$ b~ $$ K)) = Lam a (N* $$ Lam b (a~ $$ b~ $$ K)) $$ M'+" by simp
+ also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (N* $$ Lam b (a~ $$ b~ $$ K))[a ::= M'+]"
by (rule evbeta') (simp_all add: fresh_at_base e d)
- also have "... = N* $ Lam 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")
+ also have "... = N* $$ Lam 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* $ Lam b (M'+ $ b~ $ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam b (M'+ $ b~ $ K) $ N+"
+ have "N* $$ Lam b (M'+ $$ b~ $$ K) \<longrightarrow>\<^isub>\<beta>\<^sup>* Lam 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)
+ 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"
@@ -315,17 +315,17 @@
lemma
assumes "isValue V" "M \<longrightarrow>\<^isub>\<beta>\<^sup>* V"
- shows "M* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
+ shows "M* $$ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* V+"
proof-
obtain y::name where *: "atom y \<sharp> V" using obtain_fresh by blast
have e: "Lam x (x~) = Lam y (y~)"
by (simp add: Abs1_eq_iff lt.fresh fresh_at_base)
- have "M* $ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
+ have "M* $$ Lam x (x~) \<longrightarrow>\<^isub>\<beta>\<^sup>* M ; Lam x (x~)"
by(rule CPS_eval_Kapply,simp_all add: assms)
also have "... \<longrightarrow>\<^isub>\<beta>\<^sup>* (V ; Lam x (x~))" by (rule Kapply_eval_rtrancl, simp_all add: assms)
also have "... = V ; Lam 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* $ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
+ finally show "M* $$ (Lam x (x~)) \<longrightarrow>\<^isub>\<beta>\<^sup>* (V+)" .
qed
end
--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy Tue Jun 12 01:23:52 2012 +0100
@@ -13,8 +13,8 @@
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_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> = Lam x (C<M>)"
unfolding eqvt_def fill_graph_def
apply perm_simp
@@ -64,14 +64,14 @@
| "CPS (Var x) = CFun Hole (x~)"
| "atom b \<sharp> M \<Longrightarrow> CPSv (Lam y M) = Lam y (Lam b ((CPS M)<Var b>))"
| "atom b \<sharp> M \<Longrightarrow> CPS (Lam y M) = CFun Hole (Lam y (Lam b ((CPS M)<Var b>)))"
-| "CPSv (M $ N) = Lam 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> M \<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))))"
+| "CPSv (M $$ N) = Lam 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> M \<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
defer
apply (case_tac x)
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Tue Jun 12 01:23:52 2012 +0100
@@ -7,12 +7,12 @@
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) $ (Lam c (k (c~)))))))"
+| "eqvt k \<Longrightarrow> (M$$N)*k = M*(%m. (N*(%n.((m $$ n) $$ (Lam c (k (c~)))))))"
| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam 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> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
+| "(x~)^l = l $$ (x~)"
+| "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
+| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
apply (simp only: eqvt_def CPS1_CPS2_graph_def)
apply (rule, perm_simp, rule)
apply auto
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy Tue Jun 12 01:23:52 2012 +0100
@@ -9,12 +9,12 @@
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) $ (Lam c (k (c~)))))))"
+| "eqvt k \<Longrightarrow> (M $$ N)*k = M*(%m. (N*(%n.((m $$ n) $$ (Lam c (k (c~)))))))"
| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)*k = k (Lam x (Lam 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> (Lam x M)^l = l $ (Lam x (Lam c (M^(c~))))"
+| "(x~)^l = l $$ (x~)"
+| "(M $$ N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
+| "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
apply (simp only: eqvt_def CPS1_CPS2_graph_def)
apply (rule, perm_simp, rule)
apply (auto simp only:)
--- a/Nominal/Ex/CPS/Lt.thy Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy Tue Jun 12 01:23:52 2012 +0100
@@ -7,7 +7,7 @@
nominal_datatype lt =
Var name ("_~" [150] 149)
- | App lt lt (infixl "$" 100)
+ | App lt lt (infixl "$$" 100)
| Lam x::"name" t::"lt" binds x in t
nominal_primrec
@@ -49,7 +49,7 @@
where
"isValue (Var x) = True"
| "isValue (Lam y N) = True"
-| "isValue (A $ B) = False"
+| "isValue (A $$ B) = False"
unfolding eqvt_def isValue_graph_def
by (perm_simp, auto)
(erule lt.exhaust, auto)
@@ -60,9 +60,9 @@
inductive
eval :: "[lt, lt] \<Rightarrow> bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)
where
- evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
-| 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)"
+ evbeta: "\<lbrakk>atom x\<sharp>V; isValue V\<rbrakk> \<Longrightarrow> ((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta> (M[x ::= V])"
+| 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
@@ -111,7 +111,7 @@
lemma evbeta':
fixes x :: name
assumes "isValue V" and "atom x\<sharp>V" and "N = (M[x ::= V])"
- shows "((Lam x M) $ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
+ shows "((Lam x M) $$ V) \<longrightarrow>\<^isub>\<beta>\<^sup>* N"
using assms by simp (rule evs2, rule evbeta, simp_all add: evs1)
end
--- a/Nominal/Nominal2_Base.thy Mon Jun 11 14:02:57 2012 +0100
+++ b/Nominal/Nominal2_Base.thy Tue Jun 12 01:23:52 2012 +0100
@@ -8,6 +8,7 @@
imports Main
"~~/src/HOL/Library/Infinite_Set"
"~~/src/HOL/Quotient_Examples/FSet"
+ "~~/src/HOL/Library/FinFun_Syntax"
keywords
"atom_decl" "equivariance" :: thy_decl
uses ("nominal_basics.ML")
@@ -654,6 +655,30 @@
by (lifting set_eqvt)
+subsection {* Permutations for @{typ "'a \<Rightarrow>f 'b"} (FinFuns) *}
+
+instantiation finfun :: (pt, pt) pt
+begin
+
+definition "p \<bullet> f = Abs_finfun (p \<bullet> (finfun_apply f))"
+
+lemma Rep_finfun_permute:
+ shows "p \<bullet> finfun_apply f \<in> finfun"
+apply(simp add: permute_fun_comp)
+apply(rule finfun_right_compose)
+apply(rule finfun_left_compose)
+apply(rule finfun_apply)
+apply(simp)
+done
+
+instance
+apply(default)
+apply(simp_all add: permute_finfun_def finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse)
+done
+
+end
+
+
subsection {* Permutations for @{typ char}, @{typ nat}, and @{typ int} *}
instantiation char :: pt
@@ -1190,6 +1215,25 @@
shows "p \<bullet> (map_fset f S) = map_fset (p \<bullet> f) (p \<bullet> S)"
by (lifting map_eqvt)
+subsubsection {* Equivariance for @{typ "'a \<Rightarrow>f 'b"} *}
+
+lemma permute_finfun_update[simp, eqvt]:
+ "(p \<bullet> (finfun_update f a b)) = finfun_update (p \<bullet> f) (p \<bullet> a) (p \<bullet> b)"
+unfolding finfun_update_def
+unfolding permute_finfun_def
+apply(simp add: Abs_finfun_inverse fun_upd_finfun finfun_apply finfun_apply_inverse Rep_finfun_permute)
+apply(simp add: fun_upd_def)
+apply(perm_simp exclude: finfun_apply)
+apply(rule refl)
+done
+
+lemma permute_finfun_const[simp, eqvt]:
+ shows "(p \<bullet> (K$ b)) = (K$ (p \<bullet> b))"
+unfolding finfun_const_def
+unfolding permute_finfun_def
+by (simp add: permute_finfun_def const_finfun finfun_apply_inverse Rep_finfun_permute Abs_finfun_inverse)
+
+
section {* Supp, Freshness and Supports *}
@@ -2187,6 +2231,37 @@
done
+subsection {* Type @{typ "'a \<Rightarrow>f 'b"} is finitely supported *}
+
+lemma fresh_finfun_const:
+ shows "a \<sharp> (K$ b) \<longleftrightarrow> a \<sharp> b"
+ by (simp add: fresh_def supp_def)
+
+lemma fresh_finfun_update:
+ shows "\<lbrakk>a \<sharp> f; a \<sharp> b; a \<sharp> x\<rbrakk> \<Longrightarrow> a \<sharp> f(b $:= x)"
+ unfolding fresh_conv_MOST
+ unfolding permute_finfun_update
+ by (elim MOST_rev_mp) (simp)
+
+lemma supp_finfun_const:
+ "supp (K$ b) = supp(b)"
+ by (simp add: supp_def)
+
+lemma supp_finfun_update:
+ "supp (f(a $:= b)) \<subseteq> supp(f, a, b)"
+using fresh_finfun_update
+by (auto simp add: fresh_def supp_Pair)
+
+instance finfun :: (fs, fs) fs
+ apply(default)
+ apply(induct_tac x rule: finfun_weak_induct)
+ apply(simp add: supp_finfun_const finite_supp)
+ apply(rule finite_subset)
+ apply(rule supp_finfun_update)
+ apply(simp add: supp_Pair finite_supp)
+ done
+
+
section {* Freshness and Fresh-Star *}
lemma fresh_Unit_elim: