1 header {* CPS transformation of Danvy and Filinski *}

     2 theory DanvyFilinski imports Lt begin

     3 

     4 nominal_primrec

     5   CPS1 :: "lt \<Rightarrow> (lt \<Rightarrow> lt) \<Rightarrow> lt" ("_*_"  [100,100] 100)

     6 and

     7   CPS2 :: "lt \<Rightarrow> lt \<Rightarrow> lt" ("_^_" [100,100] 100)

     8 where

     9   "eqvt k \<Longrightarrow> (x~)*k = k (x~)"

    10 | "eqvt k \<Longrightarrow> (M$N)*k = M*(%m. (N*(%n.((m $ n) $ (Abs c (k (c~)))))))"

    11 | "eqvt k \<Longrightarrow> atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)*k = k (Abs x (Abs c (M^(c~))))"

    12 | "\<not>eqvt k \<Longrightarrow> (CPS1 t k) = t"

    13 | "(x~)^l = l $ (x~)"

    14 | "(M$N)^l = M*(%m. (N*(%n.((m $ n) $ l))))"

    15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Abs x M)^l = l $ (Abs x (Abs c (M^(c~))))"

    16   apply (simp only: eqvt_def CPS1_CPS2_graph_def)

    17   apply (rule, perm_simp, rule)

    18   apply auto

    19   apply (case_tac x)

    20   apply (case_tac a)

    21   apply (case_tac "eqvt b")

    22   apply (rule_tac y="aa" in lt.strong_exhaust)

    23   apply auto[4]

    24   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)

    25   apply (simp add: fresh_at_base Abs1_eq_iff)

    26   apply (case_tac b)

    27   apply (rule_tac y="a" in lt.strong_exhaust)

    28   apply auto[3]

    29   apply blast

    30   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh) 

    31   apply (simp add: fresh_at_base Abs1_eq_iff)

    32   apply blast

    33 --"-"

    34   apply (subgoal_tac "Abs c (ka (c~)) = Abs ca (ka (ca~))")

    35   apply (simp only:)

    36   apply (simp add: Abs1_eq_iff)

    37   apply (case_tac "c=ca")

    38   apply simp_all[2]

    39   apply rule

    40   apply (perm_simp)

    41   apply (simp add: eqvt_def)

    42   apply (simp add: fresh_def)

    43   apply (rule contra_subsetD[OF supp_fun_app])

    44   back

    45   apply (simp add: supp_fun_eqvt lt.supp supp_at_base)

    46 --"-"

    47   apply (rule arg_cong)

    48   back

    49   apply simp

    50   apply (thin_tac "eqvt ka")

    51   apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)

    52   apply (subgoal_tac "eqvt_at CPS1_CPS2_sumC (Inr (Ma, ca~))")

    53   apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")

    54   prefer 2

    55   apply (simp add: Abs1_eq_iff')

    56   apply (case_tac "c = a")

    57   apply simp_all[2]

    58   apply rule

    59   apply (simp add: eqvt_at_def)

    60   apply (simp add: swap_fresh_fresh fresh_Pair_elim)

    61   apply (erule fresh_eqvt_at)

    62   apply (simp add: supp_Inr finite_supp)

    63   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)

    64   apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")

    65   prefer 2

    66   apply (simp add: Abs1_eq_iff')

    67   apply (case_tac "ca = a")

    68   apply simp_all[2]

    69   apply rule

    70   apply (simp add: eqvt_at_def)

    71   apply (simp add: swap_fresh_fresh fresh_Pair_elim)

    72   apply (erule fresh_eqvt_at)

    73   apply (simp add: supp_Inr finite_supp)

    74   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)

    75   apply (simp only: )

    76   apply (erule Abs_lst1_fcb)

    77   apply (simp add: Abs_fresh_iff)

    78   apply (drule sym)

    79   apply (simp only:)

    80   apply (simp add: Abs_fresh_iff lt.fresh)

    81   apply clarify

    82   apply (erule fresh_eqvt_at)

    83   apply (simp add: supp_Inr finite_supp)

    84   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)

    85   apply (drule sym)

    86   apply (drule sym)

    87   apply (drule sym)

    88   apply (simp only:)

    89   apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")

    90   apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")

    91   apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")

    92   apply (simp add: fresh_Pair_elim)

    93   apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])

    94   back

    95   back

    96   back

    97   apply assumption

    98   apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)

    99   apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")

   100   apply simp_all[3]

   101   apply rule

   102   apply (case_tac "c = xa")

   103   apply simp_all[2]

   104   apply (simp add: eqvt_at_def)

   105   apply clarify

   106   apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)

   107   apply (simp add: eqvt_at_def)

   108   apply clarify

   109   apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)

   110   apply (case_tac "c = xa")

   111   apply simp

   112   apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")

   113   apply (simp add: atom_eqvt eqvt_at_def)

   114   apply (simp add: flip_fresh_fresh)

   115   apply (subst fresh_permute_iff)

   116   apply (erule fresh_eqvt_at)

   117   apply (simp add: supp_Inr finite_supp)

   118   apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)

   119   apply simp

   120   apply clarify

   121   apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")

   122   apply (simp add: eqvt_at_def)

   123   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")

   124   apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)

   125   apply (erule fresh_eqvt_at)

   126   apply (simp add: finite_supp supp_Inr)

   127   apply (simp add: fresh_Inr fresh_Pair lt.fresh)

   128   apply rule

   129   apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)

   130   apply (simp add: fresh_def supp_at_base)

   131   apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))

   132 --"-"

   133   prefer 2

   134   apply (rule_tac x="(c, ca, x, xa, M, Ma)" and ?'a="name" in obtain_fresh)

   135   apply (subgoal_tac "eqvt_at CPS1_CPS2_sumC (Inr (Ma, ca~))")

   136   apply (subgoal_tac "Abs c (CPS1_CPS2_sumC (Inr (M, c~))) = Abs a (CPS1_CPS2_sumC (Inr (M, a~)))")

   137   prefer 2

   138   apply (simp add: Abs1_eq_iff')

   139   apply (case_tac "c = a")

   140   apply simp_all[2]

   141   apply rule

   142   apply (simp add: eqvt_at_def)

   143   apply (simp add: swap_fresh_fresh fresh_Pair_elim)

   144   apply (erule fresh_eqvt_at)

   145   apply (simp add: supp_Inr finite_supp)

   146   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)

   147   apply (subgoal_tac "Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~))) = Abs a (CPS1_CPS2_sumC (Inr (Ma, a~)))")

   148   prefer 2

   149   apply (simp add: Abs1_eq_iff')

   150   apply (case_tac "ca = a")

   151   apply simp_all[2]

   152   apply rule

   153   apply (simp add: eqvt_at_def)

   154   apply (simp add: swap_fresh_fresh fresh_Pair_elim)

   155   apply (erule fresh_eqvt_at)

   156   apply (simp add: supp_Inr finite_supp)

   157   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)

   158   apply (simp only: )

   159   apply (erule Abs_lst1_fcb)

   160   apply (simp add: Abs_fresh_iff)

   161   apply (drule sym)

   162   apply (simp only:)

   163   apply (simp add: Abs_fresh_iff lt.fresh)

   164   apply clarify

   165   apply (erule fresh_eqvt_at)

   166   apply (simp add: supp_Inr finite_supp)

   167   apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base)

   168   apply (drule sym)

   169   apply (drule sym)

   170   apply (drule sym)

   171   apply (simp only:)

   172   apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (M, a~))) = Abs c (CPS1_CPS2_sumC (Inr (M, c~)))")

   173   apply (thin_tac "Abs a (CPS1_CPS2_sumC (Inr (Ma, a~))) = Abs ca (CPS1_CPS2_sumC (Inr (Ma, ca~)))")

   174   apply (thin_tac "atom a \<sharp> (c, ca, x, xa, M, Ma)")

   175   apply (simp add: fresh_Pair_elim)

   176   apply (subst iffD1[OF meta_eq_to_obj_eq[OF eqvt_at_def]])

   177   back

   178   back

   179   back

   180   apply assumption

   181   apply (simp add: Abs1_eq_iff' fresh_Pair_elim fresh_at_base swap_fresh_fresh lt.fresh)

   182   apply (case_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> c = ca")

   183   apply simp_all[3]

   184   apply rule

   185   apply (case_tac "c = xa")

   186   apply simp_all[2]

   187   apply (simp add: eqvt_at_def)

   188   apply clarify

   189   apply (smt flip_def permute_flip_at permute_swap_cancel swap_fresh_fresh)

   190   apply (simp add: eqvt_at_def)

   191   apply clarify

   192   apply (smt atom_eq_iff atom_eqvt flip_def fresh_eqvt permute_flip_at permute_swap_cancel swap_at_base_simps(3) swap_fresh_fresh)

   193   apply (case_tac "c = xa")

   194   apply simp

   195   apply (subgoal_tac "((ca \<leftrightarrow> x) \<bullet> (atom x)) \<sharp> (ca \<leftrightarrow> x) \<bullet> CPS1_CPS2_sumC (Inr (Ma, ca~))")

   196   apply (simp add: atom_eqvt eqvt_at_def)

   197   apply (simp add: flip_fresh_fresh)

   198   apply (subst fresh_permute_iff)

   199   apply (erule fresh_eqvt_at)

   200   apply (simp add: supp_Inr finite_supp)

   201   apply (simp add: fresh_Inr lt.fresh fresh_at_base fresh_Pair)

   202   apply simp

   203   apply clarify

   204   apply (subgoal_tac "atom ca \<sharp> (atom x \<rightleftharpoons> atom xa) \<bullet> CPS1_CPS2_sumC (Inr (M, c~))")

   205   apply (simp add: eqvt_at_def)

   206   apply (subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> atom ca \<sharp> CPS1_CPS2_sumC (Inr (M, c~))")

   207   apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)

   208   apply (erule fresh_eqvt_at)

   209   apply (simp add: finite_supp supp_Inr)

   210   apply (simp add: fresh_Inr fresh_Pair lt.fresh)

   211   apply rule

   212   apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2)

   213   apply (simp add: fresh_def supp_at_base)

   214   apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3))

   215 --"Only left subgoals are eqvt for the other side"

   216   oops

   217 

   218 (*termination

   219   sorry

   220 

   221 definition psi:: "lt => lt"

   222   where "psi V == V*(\<lambda>x. x)"

   223 

   224 section {* Simple consequence of CPS *}

   225 

   226 lemma value_eq1 : "isValue V \<Longrightarrow> eqvt k \<Longrightarrow> V*k = k (psi V)"

   227   apply (cases V rule: lt.exhaust)

   228   apply (auto simp add: psi_def)

   229   apply (subst CPS1.simps)

   230   apply (simp add: eqvt_def eqvt_bound eqvt_lambda)

   231   apply rule

   232   apply (rule_tac x="(name, lt)" and ?'a="name" in obtain_fresh)

   233   apply (subst CPS1.simps(3))

   234   apply assumption+

   235   apply (subst CPS1.simps(3))

   236   apply (simp add: eqvt_def eqvt_bound eqvt_lambda)

   237   apply assumption

   238   apply rule

   239   done

   240 *)

   241 

   242 end

   243 

   244 

   245