1 theory Nominal2_FCB

     2 imports "Nominal2_Abs" 

     3 begin

     4 

     5 

     6 lemma Abs_lst1_fcb:

     7   fixes x y :: "'a :: at_base"

     8     and S T :: "'b :: fs"

     9   assumes e: "(Abs_lst [atom x] T) = (Abs_lst [atom y] S)"

    10   and f1: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom x \<sharp> f x T"

    11   and f2: "\<lbrakk>x \<noteq> y; atom y \<sharp> T; atom x \<sharp> (atom y \<rightleftharpoons> atom x) \<bullet> T\<rbrakk> \<Longrightarrow> atom y \<sharp> f x T"

    12   and p: "\<lbrakk>S = (atom x \<rightleftharpoons> atom y) \<bullet> T; x \<noteq> y; atom y \<sharp> T; atom x \<sharp> S\<rbrakk> 

    13     \<Longrightarrow> (atom x \<rightleftharpoons> atom y) \<bullet> (f x T) = f y S"

    14   and s: "sort_of (atom x) = sort_of (atom y)"

    15   shows "f x T = f y S"

    16   using e

    17   apply(case_tac "atom x \<sharp> S")

    18   apply(simp add: Abs1_eq_iff'[OF s s])

    19   apply(elim conjE disjE)

    20   apply(simp)

    21   apply(rule trans)

    22   apply(rule_tac p="(atom x \<rightleftharpoons> atom y)" in supp_perm_eq[symmetric])

    23   apply(rule fresh_star_supp_conv)

    24   apply(simp add: supp_swap fresh_star_def s f1 f2)

    25   apply(simp add: swap_commute p)

    26   apply(simp add: Abs1_eq_iff[OF s s])

    27   done

    28 

    29 lemma Abs_lst_fcb:

    30   fixes xs ys :: "'a :: fs"

    31     and S T :: "'b :: fs"

    32   assumes e: "(Abs_lst (ba xs) T) = (Abs_lst (ba ys) S)"

    33     and f1: "\<And>x. x \<in> set (ba xs) \<Longrightarrow> x \<sharp> f xs T"

    34     and f2: "\<And>x. \<lbrakk>supp T - set (ba xs) = supp S - set (ba ys); x \<in> set (ba ys)\<rbrakk> \<Longrightarrow> x \<sharp> f xs T"

    35     and eqv: "\<And>p. \<lbrakk>p \<bullet> T = S; p \<bullet> ba xs = ba ys; supp p \<subseteq> set (ba xs) \<union> set (ba ys)\<rbrakk> 

    36       \<Longrightarrow> p \<bullet> (f xs T) = f ys S"

    37   shows "f xs T = f ys S"

    38   using e apply -

    39   apply(subst (asm) Abs_eq_iff2)

    40   apply(simp add: alphas)

    41   apply(elim exE conjE)

    42   apply(rule trans)

    43   apply(rule_tac p="p" in supp_perm_eq[symmetric])

    44   apply(rule fresh_star_supp_conv)

    45   apply(drule fresh_star_perm_set_conv)

    46   apply(rule finite_Diff)

    47   apply(rule finite_supp)

    48   apply(subgoal_tac "(set (ba xs) \<union> set (ba ys)) \<sharp>* f xs T")

    49   apply(metis Un_absorb2 fresh_star_Un)

    50   apply(subst fresh_star_Un)

    51   apply(rule conjI)

    52   apply(simp add: fresh_star_def f1)

    53   apply(simp add: fresh_star_def f2)

    54   apply(simp add: eqv)

    55   done

    56 

    57 lemma Abs_set_fcb:

    58   fixes xs ys :: "'a :: fs"

    59     and S T :: "'b :: fs"

    60   assumes e: "(Abs_set (ba xs) T) = (Abs_set (ba ys) S)"

    61     and f1: "\<And>x. x \<in> ba xs \<Longrightarrow> x \<sharp> f xs T"

    62     and f2: "\<And>x. \<lbrakk>supp T - ba xs = supp S - ba ys; x \<in> ba ys\<rbrakk> \<Longrightarrow> x \<sharp> f xs T"

    63     and eqv: "\<And>p. \<lbrakk>p \<bullet> T = S; p \<bullet> ba xs = ba ys; supp p \<subseteq> ba xs \<union> ba ys\<rbrakk> \<Longrightarrow> p \<bullet> (f xs T) = f ys S"

    64   shows "f xs T = f ys S"

    65   using e apply -

    66   apply(subst (asm) Abs_eq_iff2)

    67   apply(simp add: alphas)

    68   apply(elim exE conjE)

    69   apply(rule trans)

    70   apply(rule_tac p="p" in supp_perm_eq[symmetric])

    71   apply(rule fresh_star_supp_conv)

    72   apply(drule fresh_star_perm_set_conv)

    73   apply(rule finite_Diff)

    74   apply(rule finite_supp)

    75   apply(subgoal_tac "(ba xs \<union> ba ys) \<sharp>* f xs T")

    76   apply(metis Un_absorb2 fresh_star_Un)

    77   apply(subst fresh_star_Un)

    78   apply(rule conjI)

    79   apply(simp add: fresh_star_def f1)

    80   apply(simp add: fresh_star_def f2)

    81   apply(simp add: eqv)

    82   done

    83 

    84 lemma Abs_res_fcb:

    85   fixes xs ys :: "('a :: at_base) set"

    86     and S T :: "'b :: fs"

    87   assumes e: "(Abs_res (atom ` xs) T) = (Abs_res (atom ` ys) S)"

    88     and f1: "\<And>x. x \<in> atom ` xs \<Longrightarrow> x \<in> supp T \<Longrightarrow> x \<sharp> f xs T"

    89     and f2: "\<And>x. \<lbrakk>supp T - atom ` xs = supp S - atom ` ys; x \<in> atom ` ys; x \<in> supp S\<rbrakk> \<Longrightarrow> x \<sharp> f xs T"

    90     and eqv: "\<And>p. \<lbrakk>p \<bullet> T = S; supp p \<subseteq> atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S;

    91       p \<bullet> (atom ` xs \<inter> supp T) = atom ` ys \<inter> supp S\<rbrakk> \<Longrightarrow> p \<bullet> (f xs T) = f ys S"

    92   shows "f xs T = f ys S"

    93   using e apply -

    94   apply(subst (asm) Abs_eq_res_set)

    95   apply(subst (asm) Abs_eq_iff2)

    96   apply(simp add: alphas)

    97   apply(elim exE conjE)

    98   apply(rule trans)

    99   apply(rule_tac p="p" in supp_perm_eq[symmetric])

   100   apply(rule fresh_star_supp_conv)

   101   apply(drule fresh_star_perm_set_conv)

   102   apply(rule finite_Diff)

   103   apply(rule finite_supp)

   104   apply(subgoal_tac "(atom ` xs \<inter> supp T \<union> atom ` ys \<inter> supp S) \<sharp>* f xs T")

   105   apply(metis Un_absorb2 fresh_star_Un)

   106   apply(subst fresh_star_Un)

   107   apply(rule conjI)

   108   apply(simp add: fresh_star_def f1)

   109   apply(subgoal_tac "supp T - atom ` xs = supp S - atom ` ys")

   110   apply(simp add: fresh_star_def f2)

   111   apply(blast)

   112   apply(simp add: eqv)

   113   done

   114 

   115 

   116 

   117 lemma Abs_set_fcb2:

   118   fixes as bs :: "atom set"

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

   120     and c::"'c::fs"

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

   122   and fin: "finite as" "finite bs"

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

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

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

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

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

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

   129 proof -

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

   131     unfolding  supports_def fresh_def[symmetric]

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

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

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

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

   136     unfolding  supports_def fresh_def[symmetric]

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

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

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

   140   obtain q::"perm" where 

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

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

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

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

   145       fin1 fin2 fin

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

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

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

   149     by (simp only: fr2 perm_supp_eq)

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

   151   then obtain r::perm where 

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

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

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

   155     apply(drule_tac sym)

   156     apply(simp only: Abs_eq_iff2 alphas)

   157     apply(erule exE)

   158     apply(erule conjE)+

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

   160     apply(simp add: set_eqvt)

   161     apply(blast)

   162     done

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

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

   165     by (simp add: permute_bool_def)

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

   167     apply(simp add: fresh_star_eqvt set_eqvt)

   168     apply(subst (asm) perm1)

   169     using inc fresh1 fr1

   170     apply(auto simp add: fresh_star_def fresh_Pair)

   171     done

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

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

   174     apply(simp add: fresh_star_eqvt set_eqvt)

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

   176     using qq3 fresh2 fr1

   177     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   178     done

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

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

   181     apply(rule perm_supp_eq[symmetric])

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

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

   184     apply(rule perm1)

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

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

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

   188     apply(rule perm2[symmetric])

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

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

   191     apply(rule perm_supp_eq)

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

   193   finally show ?thesis by simp

   194 qed

   195 

   196 

   197 text {* NOT DONE 

   198 lemma Abs_res_fcb2:

   199   fixes as bs :: "atom set"

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

   201     and c::"'c::fs"

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

   203   and fin: "finite as" "finite bs"

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

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

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

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

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

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

   210 proof -

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

   212     unfolding  supports_def fresh_def[symmetric]

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

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

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

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

   217     unfolding  supports_def fresh_def[symmetric]

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

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

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

   221   obtain q::"perm" where 

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

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

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

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

   226       fin1 fin2 fin

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

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

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

   230     by (simp only: fr2 perm_supp_eq)

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

   232   then obtain r::perm where 

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

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

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

   236     apply(drule_tac sym)

   237     apply(subst(asm) Abs_eq_res_set)

   238     apply(simp only: Abs_eq_iff2 alphas)

   239     apply(erule exE)

   240     apply(erule conjE)+

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

   242     apply(simp add: set_eqvt)

   243     done

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

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

   246     by (simp add: permute_bool_def)

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

   248     apply(simp add: fresh_star_eqvt set_eqvt)

   249     sorry (* perm? *)

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

   251     apply (simp add: inter_eqvt)

   252     sorry

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

   254   show ?thesis sorry

   255 qed

   256 *}

   257 

   258 

   259 lemma Abs_lst_fcb2:

   260   fixes as bs :: "atom list"

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

   262     and c::"'c::fs"

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

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

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

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

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

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

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

   270 proof -

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

   272     unfolding  supports_def fresh_def[symmetric]

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

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

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

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

   277     unfolding  supports_def fresh_def[symmetric]

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

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

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

   281   obtain q::"perm" where 

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

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

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

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

   286       fin1 fin2

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

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

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

   290     by (simp only: fr2 perm_supp_eq)

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

   292   then obtain r::perm where 

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

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

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

   296     apply(drule_tac sym)

   297     apply(simp only: Abs_eq_iff2 alphas)

   298     apply(erule exE)

   299     apply(erule conjE)+

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

   301     apply(simp add: set_eqvt)

   302     apply(blast)

   303     done

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

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

   306     by (simp add: permute_bool_def)

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

   308     apply(simp add: fresh_star_eqvt set_eqvt)

   309     apply(subst (asm) perm1)

   310     using inc fresh1 fr1

   311     apply(auto simp add: fresh_star_def fresh_Pair)

   312     done

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

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

   315     apply(simp add: fresh_star_eqvt set_eqvt)

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

   317     using qq3 fresh2 fr1

   318     apply(auto simp add: set_eqvt fresh_star_def fresh_Pair)

   319     done

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

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

   322     apply(rule perm_supp_eq[symmetric])

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

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

   325     apply(rule perm1)

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

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

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

   329     apply(rule perm2[symmetric])

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

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

   332     apply(rule perm_supp_eq)

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

   334   finally show ?thesis by simp

   335 qed

   336 

   337 lemma Abs_lst1_fcb2:

   338   fixes a b :: "atom"

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

   340     and c::"'c :: fs"

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

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

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

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

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

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

   347 using e

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

   349 apply(simp_all)

   350 using fcb1 fresh perm1 perm2

   351 apply(simp_all add: fresh_star_def)

   352 done

   353 

   354 lemma Abs_lst1_fcb2':

   355   fixes a b :: "'a::at"

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

   357     and c::"'c :: fs"

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

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

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

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

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

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

   364 using e

   365 apply(drule_tac Abs_lst1_fcb2[where c="c" and f="\<lambda>a . f ((inv atom) a)"])

   366 using  fcb1 fresh perm1 perm2

   367 apply(simp_all add: fresh_star_def inv_f_f inj_on_def atom_eqvt)

   368 done

   369 

   370 end