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/CPS3_DanvyFilinski_FCB2.thy
changeset 2998 f0fab367453a
parent 2965 d8a6b424f80a
child 3186 425b4c406d80 
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Fri Aug 19 11:07:17 2011 +0900
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski_FCB2.thy	Fri Aug 19 12:49:38 2011 +0900
@@ -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) $ (Abs c (k (c~)))))))"
-| "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(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> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"
+| "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
@@ -31,7 +31,7 @@
   apply (simp add: fresh_at_base Abs1_eq_iff)
   apply blast
 --"-"
-  apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))")
+  apply (subgoal_tac "Lam c (ka (c~)) = Lam ca (ka (ca~))")
   apply (simp only:)
   apply (simp add: Abs1_eq_iff)
   apply (case_tac "c=ca")
@@ -48,7 +48,7 @@
   back
   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~)))")
+  apply (subgoal_tac "Lam c (CPS1_CPS2_sumC (Inr (M, c~))) = Lam a (CPS1_CPS2_sumC (Inr (M, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "c = a")
@@ -59,7 +59,7 @@
   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~)))")
+  apply (subgoal_tac "Lam ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Lam a (CPS1_CPS2_sumC (Inr (Ma, a~)))")
   prefer 2
   apply (simp add: Abs1_eq_iff')
   apply (case_tac "ca = a")
nominal2