# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1339460632 -3600
# Node ID b3d97424b13096272233ca96df584b743b239088
# Parent  425b4c406d8028e0f3091f9284e27f3b7141757c
added finfun-type to Nominal

diff -r 425b4c406d80 -r b3d97424b130 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- 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
diff -r 425b4c406d80 -r b3d97424b130 Nominal/Ex/CPS/CPS2_DanvyNielsen.thy
--- 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)
diff -r 425b4c406d80 -r b3d97424b130 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- 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
diff -r 425b4c406d80 -r b3d97424b130 Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy
--- 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:)
diff -r 425b4c406d80 -r b3d97424b130 Nominal/Ex/CPS/Lt.thy
--- 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
diff -r 425b4c406d80 -r b3d97424b130 Nominal/Nominal2_Base.thy
--- 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: