diff -r 132575f5bd26 -r f0fab367453a Nominal/Ex/CPS/CPS3_DanvyFilinski.thy --- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy Fri Aug 19 11:07:17 2011 +0900 +++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.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") @@ -49,7 +49,7 @@ 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~)))") + 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") @@ -60,7 +60,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") @@ -85,8 +85,8 @@ 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 "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") + apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam 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]]) @@ -133,7 +133,7 @@ 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~)))") + 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") @@ -144,7 +144,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") @@ -169,8 +169,8 @@ 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 "Lam a (CPS1_CPS2_sumC (Inr (M, a~))) = Lam c (CPS1_CPS2_sumC (Inr (M, c~)))") + apply (thin_tac "Lam a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Lam 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]]) @@ -242,7 +242,7 @@ apply simp done -lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Abs n (k (Var n))))" +lemma value_eq3' : "~isValue M \<Longrightarrow> eqvt k \<Longrightarrow> M*k = (M^(Lam n (k (Var n))))" by (cases M rule: lt.exhaust) auto