# HG changeset patch # User Cezary Kaliszyk # Date 1309694467 -32400 # Node ID 3be019a861170b8acb7151c61087aff3aeeb5fba # Parent e8ab8006206175980cd65338835c6e33b1c4b2fc Change CPS1 to FCB2 diff -r e8ab80062061 -r 3be019a86117 Nominal/Ex/CPS/CPS1_Plotkin.thy --- a/Nominal/Ex/CPS/CPS1_Plotkin.thy Sat Jul 02 12:40:59 2011 +0900 +++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy Sun Jul 03 21:01:07 2011 +0900 @@ -3,6 +3,104 @@ imports Lt begin +lemma Abs_lst_fcb2: + fixes as bs :: "atom list" + and x y :: "'b :: fs" + and c::"'c::fs" + assumes eq: "[as]lst. x = [bs]lst. y" + and fcb1: "(set as) \* c \ (set as) \* f as x c" + and fresh1: "set as \* c" + and fresh2: "set bs \* c" + and perm1: "\p. supp p \* c \ p \ (f as x c) = f (p \ as) (p \ x) c" + and perm2: "\p. supp p \* c \ p \ (f bs y c) = f (p \ bs) (p \ y) c" + shows "f as x c = f bs y c" +proof - + have "supp (as, x, c) supports (f as x c)" + unfolding supports_def fresh_def[symmetric] + by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh) + then have fin1: "finite (supp (f as x c))" + by (auto intro: supports_finite simp add: finite_supp) + have "supp (bs, y, c) supports (f bs y c)" + unfolding supports_def fresh_def[symmetric] + by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh) + then have fin2: "finite (supp (f bs y c))" + by (auto intro: supports_finite simp add: finite_supp) + obtain q::"perm" where + fr1: "(q \ (set as)) \* (x, c, f as x c, f bs y c)" and + fr2: "supp q \* Abs_lst as x" and + inc: "supp q \ (set as) \ q \ (set as)" + using at_set_avoiding3[where xs="set as" and c="(x, c, f as x c, f bs y c)" and x="[as]lst. x"] + fin1 fin2 + by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv) + have "Abs_lst (q \ as) (q \ x) = q \ Abs_lst as x" by simp + also have "\ = Abs_lst as x" + by (simp only: fr2 perm_supp_eq) + finally have "Abs_lst (q \ as) (q \ x) = Abs_lst bs y" using eq by simp + then obtain r::perm where + qq1: "q \ x = r \ y" and + qq2: "q \ as = r \ bs" and + qq3: "supp r \ (q \ (set as)) \ set bs" + apply(drule_tac sym) + apply(simp only: Abs_eq_iff2 alphas) + apply(erule exE) + apply(erule conjE)+ + apply(drule_tac x="p" in meta_spec) + apply(simp add: set_eqvt) + apply(blast) + done + have "(set as) \* f as x c" + apply(rule fcb1) + apply(rule fresh1) + done + then have "q \ ((set as) \* f as x c)" + by (simp add: permute_bool_def) + then have "set (q \ as) \* f (q \ as) (q \ x) c" + apply(simp add: fresh_star_eqvt set_eqvt) + apply(subst (asm) perm1) + using inc fresh1 fr1 + apply(auto simp add: fresh_star_def fresh_Pair) + done + then have "set (r \ bs) \* f (r \ bs) (r \ y) c" using qq1 qq2 by simp + then have "r \ ((set bs) \* f bs y c)" + apply(simp add: fresh_star_eqvt set_eqvt) + apply(subst (asm) perm2[symmetric]) + using qq3 fresh2 fr1 + apply(auto simp add: set_eqvt fresh_star_def fresh_Pair) + done + then have fcb2: "(set bs) \* f bs y c" by (simp add: permute_bool_def) + have "f as x c = q \ (f as x c)" + apply(rule perm_supp_eq[symmetric]) + using inc fcb1[OF fresh1] fr1 by (auto simp add: fresh_star_def) + also have "\ = f (q \ as) (q \ x) c" + apply(rule perm1) + using inc fresh1 fr1 by (auto simp add: fresh_star_def) + also have "\ = f (r \ bs) (r \ y) c" using qq1 qq2 by simp + also have "\ = r \ (f bs y c)" + apply(rule perm2[symmetric]) + using qq3 fresh2 fr1 by (auto simp add: fresh_star_def) + also have "... = f bs y c" + apply(rule perm_supp_eq) + using qq3 fr1 fcb2 by (auto simp add: fresh_star_def) + finally show ?thesis by simp +qed + +lemma Abs_lst1_fcb2: + fixes a b :: "atom" + and x y :: "'b :: fs" + and c::"'c :: fs" + assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)" + and fcb1: "a \ c \ a \ f a x c" + and fresh: "{a, b} \* c" + and perm1: "\p. supp p \* c \ p \ (f a x c) = f (p \ a) (p \ x) c" + and perm2: "\p. supp p \* c \ p \ (f b y c) = f (p \ b) (p \ y) c" + shows "f a x c = f b y c" +using e +apply(drule_tac Abs_lst_fcb2[where c="c" and f="\(as::atom list) . f (hd as)"]) +apply(simp_all) +using fcb1 fresh perm1 perm2 +apply(simp_all add: fresh_star_def) +done + nominal_primrec CPS :: "lt \ lt" ("_*" [250] 250) where @@ -43,14 +141,8 @@ apply (metis Abs_fresh_iff(3) atom_eq_iff finite_set fresh_Cons fresh_Nil fresh_atom fresh_eqvt_at fresh_finite_atom_set fresh_set lt.fsupp) --"-" apply (simp add: Abs1_eq(3)) -apply (erule Abs_lst1_fcb) -apply (simp add: fresh_def supp_Abs) -apply (drule_tac a="atom xa" in fresh_eqvt_at) -apply (simp add: finite_supp) -apply assumption -apply (simp add: fresh_def supp_Abs) -apply (simp add: eqvts eqvt_at_def) -apply simp +apply (erule Abs_lst1_fcb2) +apply (simp_all add: Abs_fresh_iff fresh_Nil fresh_star_def eqvt_at_def)[4] --"-" apply (rename_tac k' M N m' n') apply (subgoal_tac "atom k \ CPS_sumC M \ atom k' \ CPS_sumC M \ atom k \ CPS_sumC N \ atom k' \ CPS_sumC N \