Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Nominal/Ex/CPS/CPS1_Plotkin.thy
changeset 3187 b3d97424b130
parent 3186 425b4c406d80
child 3191 0440bc1a2438 
--- 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
nominal2