49 

    50 lemma Abs_set_fcb2:

    51   fixes as bs :: "atom set"

    52     and x y :: "'b :: fs"

    53     and c::"'c::fs"

    54   assumes eq: "[as]set. x = [bs]set. y"

    55   and fin: "finite as" "finite bs"

    56   and fcb1: "as \<sharp>* f as x c"

    57   and fresh1: "as \<sharp>* c"

    58   and fresh2: "bs \<sharp>* c"

    59   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"

    60   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"

    61   shows "f as x c = f bs y c"

    62 proof -

    63   have "supp (as, x, c) supports (f as x c)"

    64     unfolding  supports_def fresh_def[symmetric]

    65     by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)

    66   then have fin1: "finite (supp (f as x c))"

    67     using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)

    68   have "supp (bs, y, c) supports (f bs y c)"

    69     unfolding  supports_def fresh_def[symmetric]

    70     by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)

    71   then have fin2: "finite (supp (f bs y c))"

    72     using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)

    73   obtain q::"perm" where 

    74     fr1: "(q \<bullet> as) \<sharp>* (x, c, f as x c, f bs y c)" and 

    75     fr2: "supp q \<sharp>* ([as]set. x)" and 

    76     inc: "supp q \<subseteq> as \<union> (q \<bullet> as)"

    77     using at_set_avoiding3[where xs="as" and c="(x, c, f as x c, f bs y c)" and x="[as]set. x"]  

    78       fin1 fin2 fin

    79     by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)

    80   have "[q \<bullet> as]set. (q \<bullet> x) = q \<bullet> ([as]set. x)" by simp

    81   also have "\<dots> = [as]set. x"

    82     by (simp only: fr2 perm_supp_eq)

    83   finally have "[q \<bullet> as]set. (q \<bullet> x) = [bs]set. y" using eq by simp

    84   then obtain r::perm where 

    85     qq1: "q \<bullet> x = r \<bullet> y" and 

    86     qq2: "q \<bullet> as = r \<bullet> bs" and 

    87     qq3: "supp r \<subseteq> (q \<bullet> as) \<union> bs"

    88     apply(drule_tac sym)

    89     apply(simp only: Abs_eq_iff2 alphas)

    90     apply(erule exE)

    91     apply(erule conjE)+

    92     apply(drule_tac x="p" in meta_spec)

    93     apply(simp add: set_eqvt)

    94     apply(blast)

    95     done

    96   have "as \<sharp>* f as x c" by (rule fcb1)

    97   then have "q \<bullet> (as \<sharp>* f as x c)"

    98     by (simp add: permute_bool_def)

    99   then have "(q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"

   100     apply(simp add: fresh_star_eqvt set_eqvt)

   101     apply(subst (asm) perm1)

   102     using inc fresh1 fr1

   103     apply(auto simp add: fresh_star_def fresh_Pair)

   104     done

   105   then have "(r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp

   106   then have "r \<bullet> (bs \<sharp>* f bs y c)"

   107     apply(simp add: fresh_star_eqvt set_eqvt)

   108     apply(subst (asm) perm2[symmetric])

   109     using qq3 fresh2 fr1

   110     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   111     done

   112   then have fcb2: "bs \<sharp>* f bs y c" by (simp add: permute_bool_def)

   113   have "f as x c = q \<bullet> (f as x c)"

   114     apply(rule perm_supp_eq[symmetric])

   115     using inc fcb1 fr1 by (auto simp add: fresh_star_def)

   116   also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" 

   117     apply(rule perm1)

   118     using inc fresh1 fr1 by (auto simp add: fresh_star_def)

   119   also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp

   120   also have "\<dots> = r \<bullet> (f bs y c)"

   121     apply(rule perm2[symmetric])

   122     using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)

   123   also have "... = f bs y c"

   124     apply(rule perm_supp_eq)

   125     using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)

   126   finally show ?thesis by simp

   127 qed

   128 

   129 lemma Abs_res_fcb2:

   130   fixes as bs :: "atom set"

   131     and x y :: "'b :: fs"

   132     and c::"'c::fs"

   133   assumes eq: "[as]res. x = [bs]res. y"

   134   and fin: "finite as" "finite bs"

   135   and fcb1: "as \<sharp>* f as x c"

   136   and fresh1: "as \<sharp>* c"

   137   and fresh2: "bs \<sharp>* c"

   138   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"

   139   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"

   140   shows "f as x c = f bs y c"

   141 proof -

   142   have "supp (as, x, c) supports (f as x c)"

   143     unfolding  supports_def fresh_def[symmetric]

   144     by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)

   145   then have fin1: "finite (supp (f as x c))"

   146     using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)

   147   have "supp (bs, y, c) supports (f bs y c)"

   148     unfolding  supports_def fresh_def[symmetric]

   149     by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)

   150   then have fin2: "finite (supp (f bs y c))"

   151     using fin by (auto intro: supports_finite simp add: finite_supp supp_of_finite_sets supp_Pair)

   152   obtain q::"perm" where 

   153     fr1: "(q \<bullet> as) \<sharp>* (x, c, f as x c, f bs y c)" and 

   154     fr2: "supp q \<sharp>* ([as]res. x)" and 

   155     inc: "supp q \<subseteq> as \<union> (q \<bullet> as)"

   156     using at_set_avoiding3[where xs="as" and c="(x, c, f as x c, f bs y c)" and x="[as]res. x"]  

   157       fin1 fin2 fin

   158     by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)

   159   have "[q \<bullet> as]res. (q \<bullet> x) = q \<bullet> ([as]res. x)" by simp

   160   also have "\<dots> = [as]res. x"

   161     by (simp only: fr2 perm_supp_eq)

   162   finally have "[q \<bullet> as]res. (q \<bullet> x) = [bs]res. y" using eq by simp

   163   then obtain r::perm where 

   164     qq1: "q \<bullet> x = r \<bullet> y" and 

   165     qq2: "(q \<bullet> as \<inter> supp (q \<bullet> x)) = r \<bullet> (bs \<inter> supp y)" and 

   166     qq3: "supp r \<subseteq> bs \<inter> supp y \<union> q \<bullet> as \<inter> supp (q \<bullet> x)"

   167     apply(drule_tac sym)

   168     apply(subst(asm) Abs_eq_res_set)

   169     apply(simp only: Abs_eq_iff2 alphas)

   170     apply(erule exE)

   171     apply(erule conjE)+

   172     apply(drule_tac x="p" in meta_spec)

   173     apply(simp add: set_eqvt)

   174     done

   175   have "(as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c" sorry (* FCB? *)

   176   then have "q \<bullet> ((as \<inter> supp x) \<sharp>* f (as \<inter> supp x) x c)"

   177     by (simp add: permute_bool_def)

   178   then have "(q \<bullet> (as \<inter> supp x)) \<sharp>* f (q \<bullet> (as \<inter> supp x)) (q \<bullet> x) c"

   179     apply(simp add: fresh_star_eqvt set_eqvt)

   180     sorry (* perm? *)

   181   then have "r \<bullet> (bs \<inter> supp y) \<sharp>* f (r \<bullet> (bs \<inter> supp y)) (r \<bullet> y) c" using qq2 

   182     apply (simp add: inter_eqvt)

   183     sorry

   184   (* rest similar reversing it other way around... *)

   185   show ?thesis sorry

   186 qed

   187 

   188 

   189 

   190 lemma Abs_lst_fcb2:

   191   fixes as bs :: "atom list"

   192     and x y :: "'b :: fs"

   193     and c::"'c::fs"

   194   assumes eq: "[as]lst. x = [bs]lst. y"

   195   and fcb1: "(set as) \<sharp>* f as x c"

   196   and fresh1: "set as \<sharp>* c"

   197   and fresh2: "set bs \<sharp>* c"

   198   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f as x c) = f (p \<bullet> as) (p \<bullet> x) c"

   199   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f bs y c) = f (p \<bullet> bs) (p \<bullet> y) c"

   200   shows "f as x c = f bs y c"

   201 proof -

   202   have "supp (as, x, c) supports (f as x c)"

   203     unfolding  supports_def fresh_def[symmetric]

   204     by (simp add: fresh_Pair perm1 fresh_star_def supp_swap swap_fresh_fresh)

   205   then have fin1: "finite (supp (f as x c))"

   206     by (auto intro: supports_finite simp add: finite_supp)

   207   have "supp (bs, y, c) supports (f bs y c)"

   208     unfolding  supports_def fresh_def[symmetric]

   209     by (simp add: fresh_Pair perm2 fresh_star_def supp_swap swap_fresh_fresh)

   210   then have fin2: "finite (supp (f bs y c))"

   211     by (auto intro: supports_finite simp add: finite_supp)

   212   obtain q::"perm" where 

   213     fr1: "(q \<bullet> (set as)) \<sharp>* (x, c, f as x c, f bs y c)" and 

   214     fr2: "supp q \<sharp>* Abs_lst as x" and 

   215     inc: "supp q \<subseteq> (set as) \<union> q \<bullet> (set as)"

   216     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"]  

   217       fin1 fin2

   218     by (auto simp add: supp_Pair finite_supp Abs_fresh_star dest: fresh_star_supp_conv)

   219   have "Abs_lst (q \<bullet> as) (q \<bullet> x) = q \<bullet> Abs_lst as x" by simp

   220   also have "\<dots> = Abs_lst as x"

   221     by (simp only: fr2 perm_supp_eq)

   222   finally have "Abs_lst (q \<bullet> as) (q \<bullet> x) = Abs_lst bs y" using eq by simp

   223   then obtain r::perm where 

   224     qq1: "q \<bullet> x = r \<bullet> y" and 

   225     qq2: "q \<bullet> as = r \<bullet> bs" and 

   226     qq3: "supp r \<subseteq> (q \<bullet> (set as)) \<union> set bs"

   227     apply(drule_tac sym)

   228     apply(simp only: Abs_eq_iff2 alphas)

   229     apply(erule exE)

   230     apply(erule conjE)+

   231     apply(drule_tac x="p" in meta_spec)

   232     apply(simp add: set_eqvt)

   233     apply(blast)

   234     done

   235   have "(set as) \<sharp>* f as x c" by (rule fcb1)

   236   then have "q \<bullet> ((set as) \<sharp>* f as x c)"

   237     by (simp add: permute_bool_def)

   238   then have "set (q \<bullet> as) \<sharp>* f (q \<bullet> as) (q \<bullet> x) c"

   239     apply(simp add: fresh_star_eqvt set_eqvt)

   240     apply(subst (asm) perm1)

   241     using inc fresh1 fr1

   242     apply(auto simp add: fresh_star_def fresh_Pair)

   243     done

   244   then have "set (r \<bullet> bs) \<sharp>* f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp

   245   then have "r \<bullet> ((set bs) \<sharp>* f bs y c)"

   246     apply(simp add: fresh_star_eqvt set_eqvt)

   247     apply(subst (asm) perm2[symmetric])

   248     using qq3 fresh2 fr1

   249     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   250     done

   251   then have fcb2: "(set bs) \<sharp>* f bs y c" by (simp add: permute_bool_def)

   252   have "f as x c = q \<bullet> (f as x c)"

   253     apply(rule perm_supp_eq[symmetric])

   254     using inc fcb1 fr1 by (auto simp add: fresh_star_def)

   255   also have "\<dots> = f (q \<bullet> as) (q \<bullet> x) c" 

   256     apply(rule perm1)

   257     using inc fresh1 fr1 by (auto simp add: fresh_star_def)

   258   also have "\<dots> = f (r \<bullet> bs) (r \<bullet> y) c" using qq1 qq2 by simp

   259   also have "\<dots> = r \<bullet> (f bs y c)"

   260     apply(rule perm2[symmetric])

   261     using qq3 fresh2 fr1 by (auto simp add: fresh_star_def)

   262   also have "... = f bs y c"

   263     apply(rule perm_supp_eq)

   264     using qq3 fr1 fcb2 by (auto simp add: fresh_star_def)

   265   finally show ?thesis by simp

   266 qed

   267 

   268 lemma Abs_lst1_fcb2:

   269   fixes a b :: "atom"

   270     and x y :: "'b :: fs"

   271     and c::"'c :: fs"

   272   assumes e: "(Abs_lst [a] x) = (Abs_lst [b] y)"

   273   and fcb1: "a \<sharp> f a x c"

   274   and fresh: "{a, b} \<sharp>* c"

   275   and perm1: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f a x c) = f (p \<bullet> a) (p \<bullet> x) c"

   276   and perm2: "\<And>p. supp p \<sharp>* c \<Longrightarrow> p \<bullet> (f b y c) = f (p \<bullet> b) (p \<bullet> y) c"

   277   shows "f a x c = f b y c"

   278 using e

   279 apply(drule_tac Abs_lst_fcb2[where c="c" and f="\<lambda>(as::atom list) . f (hd as)"])

   280 apply(simp_all)

   281 using fcb1 fresh perm1 perm2

   282 apply(simp_all add: fresh_star_def)

   283 done

   284 

   285 lemma supp_zero_perm_zero:

   286   shows "supp (p :: perm) = {} \<longleftrightarrow> p = 0"

   287   by (metis supp_perm_singleton supp_zero_perm)

   288 

   289 lemma permute_atom_list_id:

   290   shows "p \<bullet> l = l \<longleftrightarrow> supp p \<inter> set l = {}"

   291   by (induct l) (auto simp add: supp_Nil supp_perm)

   292 

   293 lemma permute_length_eq:

   294   shows "p \<bullet> xs = ys \<Longrightarrow> length xs = length ys"

   295   by (auto simp add: length_eqvt[symmetric] permute_pure)

   296 

   297 lemma Abs_lst_binder_length:

   298   shows "[xs]lst. T = [ys]lst. S \<Longrightarrow> length xs = length ys"

   299   by (auto simp add: Abs_eq_iff alphas length_eqvt[symmetric] permute_pure)

   300 

   301 lemma Abs_lst_binder_eq:

   302   shows "Abs_lst l T = Abs_lst l S \<longleftrightarrow> T = S"

   303   by (rule, simp_all add: Abs_eq_iff2 alphas)

   304      (metis fresh_star_zero inf_absorb1 permute_atom_list_id supp_perm_eq

   305        supp_zero_perm_zero)

   306 

   307 lemma in_permute_list:

   308   shows "py \<bullet> p \<bullet> xs = px \<bullet> xs \<Longrightarrow>  x \<in> set xs \<Longrightarrow> py \<bullet> p \<bullet> x = px \<bullet> x"

   309   by (induct xs) auto

   310 

   311