75   assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)"

    75   assumes a: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z"

    76   and     b: "(cs, y) \<approx>gen R f p2 (ds, z)"

    76   shows "\<lbrakk>(bs, x) \<approx>gen R f p (cs, y); (cs, y) \<approx>gen R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>gen R f (q + p) (ds, z)"

    77   and     c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z"

    77   and   "\<lbrakk>(bs, x) \<approx>res R f p (cs, y); (cs, y) \<approx>res R f q (ds, z)\<rbrakk> \<Longrightarrow> (bs, x) \<approx>res R f (q + p) (ds, z)"

    78   shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)"

    78   and   "\<lbrakk>(es, x) \<approx>lst R f p (gs, y); (gs, y) \<approx>lst R f q (hs, z)\<rbrakk> \<Longrightarrow> (es, x) \<approx>lst R f (q + p) (hs, z)"

    79   using a b c using supp_plus_perm

    79   using a 

    80   apply(simp add: alpha_gen fresh_star_def fresh_def)

    80   unfolding alphas

    81   unfolding fresh_star_def

    82   by (simp_all add: fresh_plus_perm)

    83 

    84 lemma alpha_gen_eqvt:

    85   assumes a: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"

    86   and     b: "p \<bullet> (f x) = f (p \<bullet> x)"

    87   and     c: "p \<bullet> (f y) = f (p \<bullet> y)"

    88   shows "(bs, x) \<approx>gen R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"

    89   and   "(bs, x) \<approx>res R f q (cs, y) \<Longrightarrow> (p \<bullet> bs, p \<bullet> x) \<approx>res R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"

    90   and   "(ds, x) \<approx>lst R f q (es, y) \<Longrightarrow> (p \<bullet> ds, p \<bullet> x) \<approx>lst R f (p \<bullet> q) (p \<bullet> es, p \<bullet> y)" 

    91   unfolding alphas

    92   unfolding set_eqvt[symmetric]

    93   unfolding b[symmetric] c[symmetric]

    94   unfolding Diff_eqvt[symmetric]

    95   unfolding permute_eqvt[symmetric]

    96   using a

    97   by (auto simp add: fresh_star_permute_iff)

    98 

    99 fun

   100   alpha_abs 

   101 where

   102   "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))"

   103 

   104 notation

   105   alpha_abs ("_ \<approx>abs _")

   106 

   107 lemma alpha_abs_swap:

   108   assumes a1: "a \<notin> (supp x) - bs"

   109   and     a2: "b \<notin> (supp x) - bs"

   110   shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"

   111   using a1 a2

   112   unfolding Diff_iff

   113   unfolding alpha_abs.simps

   114   unfolding alphas

   115   unfolding supp_eqvt[symmetric] Diff_eqvt[symmetric]

   116   unfolding fresh_star_def fresh_def

   117   unfolding swap_set_not_in[OF a1 a2] 

   118   by (rule_tac x="(a \<rightleftharpoons> b)" in exI)

   119      (auto simp add: supp_perm swap_atom)

   120 

   121 lemma alpha_gen_swap_fun:

   122   assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)"

   123   assumes a1: "a \<notin> (f x) - bs"

   124   and     a2: "b \<notin> (f x) - bs"

   125   shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)"

   126   apply(rule_tac x="(a \<rightleftharpoons> b)" in exI)

   127   apply(simp add: alpha_gen)

   128   apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric])

   129   apply(simp add: swap_set_not_in[OF a1 a2])

   130   apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")

   131   using a1 a2

   132   apply(simp add: fresh_star_def fresh_def)

    82   done

   134   apply(simp add: supp_swap)

    83 

   135   done

    84 lemma alpha_gen_eqvt:

   136 

    85   assumes a: "(bs, x) \<approx>gen R f q (cs, y)"

   137 fun

    86   and     b: "R (q \<bullet> x) y \<Longrightarrow> R (p \<bullet> (q \<bullet> x)) (p \<bullet> y)"

   138   supp_abs_fun

    87   and     c: "p \<bullet> (f x) = f (p \<bullet> x)"

   139 where

    88   and     d: "p \<bullet> (f y) = f (p \<bullet> y)"

   140   "supp_abs_fun (bs, x) = (supp x) - bs"

    89   shows "(p \<bullet> bs, p \<bullet> x) \<approx>gen R f (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)"

   141 

    90   using a b

   142 

    91   apply(simp add: alpha_gen c[symmetric] d[symmetric] Diff_eqvt[symmetric])

   143 lemma supp_abs_fun_lemma:

    92   apply(simp add: permute_eqvt[symmetric])

   144   assumes a: "x \<approx>abs y" 

    93   apply(simp add: fresh_star_permute_iff)

   145   shows "supp_abs_fun x = supp_abs_fun y"

   146   using a

   147   apply(induct rule: alpha_abs.induct)

   148   apply(simp add: alpha_gen)

   149   done

   150   

   151 

   152 quotient_type 'a abs_gen = "(atom set \<times> 'a::pt)" / "alpha_abs"

   153   apply(rule equivpI)

   154   unfolding reflp_def symp_def transp_def

   155   apply(simp_all)

   156   (* refl *)

   157   apply(clarify)

   158   apply(rule_tac x="0" in exI)

   159   apply(rule alpha_gen_refl)

   160   apply(simp)

   161   (* symm *)

   162   apply(clarify)

   163   apply(rule_tac x="- p" in exI)

   164   apply(rule alpha_gen_sym)

    95   done

   166   apply(assumption)

   167   (* trans *)

   168   apply(clarify)

   169   apply(rule_tac x="pa + p" in exI)

   170   apply(rule alpha_gen_trans)

   171   apply(auto)

   172   done

   173 

   174 quotient_definition

   175   "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen"

   176 is

   177   "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)"

   178 

   179 lemma [quot_respect]:

   180   shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair"

   181   apply(clarsimp)

   182   apply(rule exI)

   183   apply(rule alpha_gen_refl)

   184   apply(simp)

   185   done

   186 

   187 lemma [quot_respect]:

   188   shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute"

   189   apply(clarsimp)

   190   apply(rule exI)

   191   apply(rule alpha_gen_eqvt)

   192   apply(simp_all add: supp_eqvt)

   193   done

   194 

   195 lemma [quot_respect]:

   196   shows "(alpha_abs ===> (op =)) supp_abs_fun supp_abs_fun"

   197   apply(simp add: supp_abs_fun_lemma)

   198   done

   199 

   200 lemma abs_induct:

   201   "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t"

   202   apply(lifting prod.induct[where 'a="atom set" and 'b="'a"])

   203   done

   204 

   205 (* TEST case *)

   206 lemmas abs_induct2 = prod.induct[where 'a="atom set" and 'b="'a::pt", quot_lifted]

   207 thm abs_induct abs_induct2

   208 

   209 instantiation abs_gen :: (pt) pt

   210 begin

   211 

   212 quotient_definition

   213   "permute_abs_gen::perm \<Rightarrow> ('a::pt abs_gen) \<Rightarrow> 'a abs_gen"

   214 is

   215   "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)"

   216 

   217 (* ??? has to be 'a \<dots> 'b does not work *)

   218 lemma permute_ABS [simp]:

   219   fixes x::"'a::pt"  

   220   shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)"

   221   thm permute_prod.simps

   222   by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"])

   223 

   224 instance

   225   apply(default)

   226   apply(induct_tac [!] x rule: abs_induct)

   227   apply(simp_all)

   228   done

   229 

   230 end

   231 

   232 quotient_definition

   233   "supp_Abs_fun :: ('a::pt) abs_gen \<Rightarrow> atom \<Rightarrow> bool"

   234 is

   235   "supp_abs_fun"

   236 

   237 lemma supp_Abs_fun_simp:

   238   shows "supp_Abs_fun (Abs bs x) = (supp x) - bs"

   239   by (lifting supp_abs_fun.simps(1))

   240 

   241 lemma supp_Abs_fun_eqvt [eqvt]:

   242   shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)"

   243   apply(induct_tac x rule: abs_induct)

   244   apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt)

   245   done

   246 

   247 lemma supp_Abs_fun_fresh:

   248   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)"

   249   apply(rule fresh_fun_eqvt_app)

   250   apply(simp add: eqvts_raw)

   251   apply(simp)

   252   done

   253 

   254 lemma Abs_swap:

   255   assumes a1: "a \<notin> (supp x) - bs"

   256   and     a2: "b \<notin> (supp x) - bs"

   257   shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))"

   258   using a1 a2 by (lifting alpha_abs_swap)

   259 

   260 lemma Abs_supports:

   261   shows "((supp x) - as) supports (Abs as x)"

   262   unfolding supports_def

   263   apply(clarify)

   264   apply(simp (no_asm))

   265   apply(subst Abs_swap[symmetric])

   266   apply(simp_all)

   267   done

   268 

   269 lemma finite_supp_Abs_subset1:

   270   assumes "finite (supp x)"

   271   shows "(supp x) - as \<subseteq> supp (Abs as x)"

   272   apply(simp add: supp_conv_fresh)

   273   apply(auto)

   274   apply(drule_tac supp_Abs_fun_fresh)

   275   apply(simp only: supp_Abs_fun_simp)

   276   apply(simp add: fresh_def)

   277   apply(simp add: supp_finite_atom_set assms)

   278   done

   279 

   280 lemma finite_supp_Abs_subset2:

   281   assumes "finite (supp x)"

   282   shows "supp (Abs as x) \<subseteq> (supp x) - as"

   283   apply(rule supp_is_subset)

   284   apply(rule Abs_supports)

   285   apply(simp add: assms)

   286   done

   287 

   288 lemma finite_supp_Abs:

   289   assumes "finite (supp x)"

   290   shows "supp (Abs as x) = (supp x) - as"

   291   apply(rule_tac subset_antisym)

   292   apply(rule finite_supp_Abs_subset2[OF assms])

   293   apply(rule finite_supp_Abs_subset1[OF assms])

   294   done

   295 

   296 lemma supp_Abs:

   297   fixes x::"'a::fs"

   298   shows "supp (Abs as x) = (supp x) - as"

   299   apply(rule finite_supp_Abs)

   300   apply(simp add: finite_supp)

   301   done

   302 

   303 instance abs_gen :: (fs) fs

   304   apply(default)

   305   apply(induct_tac x rule: abs_induct)

   306   apply(simp add: supp_Abs)

   307   apply(simp add: finite_supp)

   308   done

   309 

   310 lemma Abs_fresh_iff:

   311   fixes x::"'a::fs"

   312   shows "a \<sharp> Abs bs x \<longleftrightarrow> a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x)"

   313   apply(simp add: fresh_def)

   314   apply(simp add: supp_Abs)

   315   apply(auto)

   316   done

   317 

   318 lemma Abs_eq_iff:

   319   shows "Abs bs x = Abs cs y \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))"

   320   by (lifting alpha_abs.simps(1))

   321 

   322 

   323 

   324 (* 

   325   below is a construction site for showing that in the

   326   single-binder case, the old and new alpha equivalence 

   327   coincide

   328 *)

   329 

   330 fun

   331   alpha1

   332 where

   333   "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)"

   334 

   335 notation 

   336   alpha1 ("_ \<approx>abs1 _")

   337 

   338 fun

   339   alpha2

   340 where

   341   "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))"

   342 

   343 notation 

   344   alpha2 ("_ \<approx>abs2 _")

   345 

   346 lemma alpha_old_new:

   347   assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b"

   348   shows "({a}, x) \<approx>abs ({b}, y)"

   349 using a

   350 apply(simp)

   351 apply(erule disjE)

   352 apply(simp)

   353 apply(rule exI)

   354 apply(rule alpha_gen_refl)

   355 apply(simp)

   356 apply(rule_tac x="(a \<rightleftharpoons> b)" in  exI)

   357 apply(simp add: alpha_gen)

   358 apply(simp add: fresh_def)

   359 apply(rule conjI)

   360 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in  permute_eq_iff[THEN iffD1])

   361 apply(rule trans)

   362 apply(simp add: Diff_eqvt supp_eqvt)

   363 apply(subst swap_set_not_in)

   364 back

   365 apply(simp)

   366 apply(simp)

   367 apply(simp add: permute_set_eq)

   368 apply(rule conjI)

   369 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1])

   370 apply(simp add: permute_self)

   371 apply(simp add: Diff_eqvt supp_eqvt)

   372 apply(simp add: permute_set_eq)

   373 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}")

   374 apply(simp add: fresh_star_def fresh_def)

   375 apply(blast)

   376 apply(simp add: supp_swap)

   377 apply(simp add: eqvts)

   378 done

   379 

   380 lemma perm_zero:

   381   assumes a: "\<forall>x::atom. p \<bullet> x = x"

   382   shows "p = 0"

   383 using a

   384 by (simp add: expand_perm_eq)

   385 

   386 fun

   387   add_perm 

   388 where

   389   "add_perm [] = 0"

   390 | "add_perm ((a, b) # xs) = (a \<rightleftharpoons> b) + add_perm xs"

   391 

   392 fun

   393   elem_perm

   394 where

   395   "elem_perm [] = {}"

   396 | "elem_perm ((a, b) # xs) = {a, b} \<union> elem_perm xs"

   397 

   398 

   399 lemma add_perm_apend:

   400   shows "add_perm (xs @ ys) = add_perm xs + add_perm ys"

   401 apply(induct xs arbitrary: ys)

   402 apply(auto simp add: add_assoc)

   403 done

   404 

   405 lemma perm_list_exists:

   406   fixes p::perm

   407   shows "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p"

   408 apply(induct p taking: "\<lambda>p::perm. card (supp p)" rule: measure_induct)

   409 apply(rename_tac p)

   410 apply(case_tac "supp p = {}")

   411 apply(simp)

   412 apply(simp add: supp_perm)

   413 apply(drule perm_zero)

   414 apply(simp)

   415 apply(rule_tac x="[]" in exI)

   416 apply(simp add: supp_Nil)

   417 apply(subgoal_tac "\<exists>x. x \<in> supp p")

   418 defer

   419 apply(auto)[1]

   420 apply(erule exE)

   421 apply(drule_tac x="p + (((- p) \<bullet> x) \<rightleftharpoons> x)" in spec)

   422 apply(drule mp)

   423 defer

   424 apply(erule exE)

   425 apply(rule_tac x="xs @ [((- p) \<bullet> x, x)]" in exI)

   426 apply(simp add: add_perm_apend)

   427 apply(erule conjE)

   428 apply(drule sym)

   429 apply(simp)

   430 apply(simp add: expand_perm_eq)

   431 apply(simp add: supp_append)

   432 apply(simp add: supp_perm supp_Cons supp_Nil supp_Pair supp_atom)

   433 apply(rule conjI)

   434 prefer 2

   435 apply(auto)[1]

   436 apply (metis left_minus minus_unique permute_atom_def_raw permute_minus_cancel(2))

   437 defer

   438 apply(rule psubset_card_mono)

   439 apply(simp add: finite_supp)

   440 apply(rule psubsetI)

   441 defer

   442 apply(subgoal_tac "x \<notin> supp (p + (- p \<bullet> x \<rightleftharpoons> x))")

   443 apply(blast)

   444 apply(simp add: supp_perm)

   445 defer

   446 apply(auto simp add: supp_perm)[1]

   447 apply(case_tac "x = xa")

   448 apply(simp)

   449 apply(case_tac "((- p) \<bullet> x) = xa")

   450 apply(simp)

   451 apply(case_tac "sort_of xa = sort_of x")

   452 apply(simp)

   453 apply(auto)[1]

   454 apply(simp)

   455 apply(simp)

   456 apply(subgoal_tac "{a. p \<bullet> (- p \<bullet> x \<rightleftharpoons> x) \<bullet> a \<noteq> a} \<subseteq> {a. p \<bullet> a \<noteq> a}")

   457 apply(blast)

   458 apply(auto simp add: supp_perm)[1]

   459 apply(case_tac "x = xa")

   460 apply(simp)

   461 apply(case_tac "((- p) \<bullet> x) = xa")

   462 apply(simp)

   463 apply(case_tac "sort_of xa = sort_of x")

   464 apply(simp)

   465 apply(auto)[1]

   466 apply(simp)

   467 apply(simp)

   468 done

   469 

   470 lemma tt0:

   471   fixes p::perm

   472   shows "(supp x) \<sharp>* p \<Longrightarrow> \<forall>a \<in> supp p. a \<sharp> x"

   473 apply(auto simp add: fresh_star_def supp_perm fresh_def)

   474 done

   475 

   476 lemma uu0:

   477   shows "(\<forall>a \<in> elem_perm xs. a \<sharp> x) \<Longrightarrow> (add_perm xs \<bullet> x) = x"

   478 apply(induct xs rule: add_perm.induct)

   479 apply(simp)

   480 apply(simp add: swap_fresh_fresh)

   481 done

   482 

   483 lemma yy0:

   484   fixes xs::"(atom \<times> atom) list"

   485   shows "supp xs = elem_perm xs"

   486 apply(induct xs rule: elem_perm.induct)

   487 apply(auto simp add: supp_Nil supp_Cons supp_Pair supp_atom)

   488 done

   489 

   490 lemma tt1:

   491   shows "(supp x) \<sharp>* p \<Longrightarrow> p \<bullet> x = x"

   492 apply(drule tt0)

   493 apply(subgoal_tac "\<exists>xs. p = add_perm xs \<and> supp xs \<subseteq> supp p")

   494 prefer 2

   495 apply(rule perm_list_exists)

   496 apply(erule exE)

   497 apply(simp only: yy0)

   498 apply(rule uu0)

   499 apply(auto)

   500 done

   501 

   502 

   503 lemma perm_induct_test:

   504   fixes P :: "perm => bool"

   505   assumes fin: "finite (supp p)" 

   506   assumes zero: "P 0"

   507   assumes swap: "\<And>a b. \<lbrakk>sort_of a = sort_of b; a \<noteq> b\<rbrakk> \<Longrightarrow> P (a \<rightleftharpoons> b)"

   508   assumes plus: "\<And>p1 p2. \<lbrakk>supp p1 \<inter> supp p2 = {}; P p1; P p2\<rbrakk> \<Longrightarrow> P (p1 + p2)"

   509   shows "P p"

   510 using fin

   511 apply(induct F\<equiv>"supp p" arbitrary: p rule: finite_induct)

   512 apply(simp add: supp_perm)

   513 apply(drule perm_zero)

   514 apply(simp add: zero)

   515 apply(rotate_tac 3)

   516 oops

   517 

   518 lemma ii:

   519   assumes "\<forall>x \<in> A. p \<bullet> x = x"

   520   shows "p \<bullet> A = A"

   521 using assms

   522 apply(auto)

   523 apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_bound inf_Int_eq mem_def mem_permute_iff)

   524 apply (metis Collect_def Collect_mem_eq Int_absorb assms eqvt_apply eqvt_bound eqvt_lambda inf_Int_eq mem_def mem_permute_iff permute_minus_cancel(2) permute_pure)

   525 done

   526 

   527 

   528 

   529 lemma alpha_abs_Pair:

   530   shows "(bs, (x1, x2)) \<approx>gen (\<lambda>(x1,x2) (y1,y2). x1=y1 \<and> x2=y2) (\<lambda>(x,y). supp x \<union> supp y) p (cs, (y1, y2))

   531          \<longleftrightarrow> ((bs, x1) \<approx>gen (op=) supp p (cs, y1) \<and> (bs, x2) \<approx>gen (op=) supp p (cs, y2))"         

   532   apply(simp add: alpha_gen)

   533   apply(simp add: fresh_star_def)

   534   apply(simp add: ball_Un Un_Diff)

   535   apply(rule iffI)

   536   apply(simp)

   537   defer

   538   apply(simp)

   539   apply(rule conjI)

   540   apply(clarify)

   541   apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])

   542   apply(rule sym)

   543   apply(rule ii)

   544   apply(simp add: fresh_def supp_perm)

   545   apply(clarify)

   546   apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric])

   547   apply(simp add: fresh_def supp_perm)

   548   apply(rule sym)

   549   apply(rule ii)

   550   apply(simp)

   551   done

   552 

   553 

   554 lemma yy:

   555   assumes "S1 - {x} = S2 - {x}" "x \<in> S1" "x \<in> S2"

   556   shows "S1 = S2"

   557 using assms

   558 apply (metis insert_Diff_single insert_absorb)

   559 done

   560 

   561 lemma kk:

   562   assumes a: "p \<bullet> x = y"

   563   shows "\<forall>a \<in> supp x. (p \<bullet> a) \<in> supp y"

   564 using a

   565 apply(auto)

   566 apply(rule_tac p="- p" in permute_boolE)

   567 apply(simp add: mem_eqvt supp_eqvt)

   568 done

   569 

   570 lemma ww:

   571   assumes "a \<notin> supp x" "b \<in> supp x" "a \<noteq> b" "sort_of a = sort_of b"

   572   shows "((a \<rightleftharpoons> b) \<bullet> x) \<noteq> x"

   573 apply(subgoal_tac "(supp x) supports x")

   574 apply(simp add: supports_def)

   575 using assms

   576 apply -

   577 apply(drule_tac x="a" in spec)

   578 defer

   579 apply(rule supp_supports)

   580 apply(auto)

   581 apply(rotate_tac 1)

   582 apply(drule_tac p="(a \<rightleftharpoons> b)" in permute_boolI)

   583 apply(simp add: mem_eqvt supp_eqvt)

   584 done

   585 

   586 lemma alpha_abs_sym:

   587   assumes a: "({a}, x) \<approx>abs ({b}, y)"

   588   shows "({b}, y) \<approx>abs ({a}, x)"

   589 using a

   590 apply(simp)

   591 apply(erule exE)

   592 apply(rule_tac x="- p" in exI)

   593 apply(simp add: alpha_gen)

   594 apply(simp add: fresh_star_def fresh_minus_perm)

   595 apply (metis permute_minus_cancel(2))

   596 done

   597 

   598 lemma alpha_abs_trans:

   599   assumes a: "({a1}, x1) \<approx>abs ({a2}, x2)"

   600   assumes b: "({a2}, x2) \<approx>abs ({a3}, x3)"

   601   shows "({a1}, x1) \<approx>abs ({a3}, x3)"

   602 using a b

   603 apply(simp)

   604 apply(erule exE)+

   605 apply(rule_tac x="pa + p" in exI)

   606 apply(simp add: alpha_gen)

   607 apply(simp add: fresh_star_def fresh_plus_perm)

   608 done

   609 

   610 lemma alpha_equal:

   611   assumes a: "({a}, x) \<approx>abs ({a}, y)" 

   612   shows "(a, x) \<approx>abs1 (a, y)"

   613 using a

   614 apply(simp)

   615 apply(erule exE)

   616 apply(simp add: alpha_gen)

   617 apply(erule conjE)+

   618 apply(case_tac "a \<notin> supp x")

   619 apply(simp)

   620 apply(subgoal_tac "supp x \<sharp>* p")

   621 apply(drule tt1)

   622 apply(simp)

   623 apply(simp)

   624 apply(simp)

   625 apply(case_tac "a \<notin> supp y")

   626 apply(simp)

   627 apply(drule tt1)

   628 apply(clarify)

   629 apply(simp (no_asm_use))

   630 apply(simp)

   631 apply(simp)

   632 apply(drule yy)

   633 apply(simp)

   634 apply(simp)

   635 apply(simp)

   636 apply(case_tac "a \<sharp> p")

   637 apply(subgoal_tac "supp y \<sharp>* p")

   638 apply(drule tt1)

   639 apply(clarify)

   640 apply(simp (no_asm_use))

   641 apply(metis)

   642 apply(auto simp add: fresh_star_def)[1]

   643 apply(frule_tac kk)

   644 apply(drule_tac x="a" in bspec)

   645 apply(simp)

   646 apply(simp add: fresh_def)

   647 apply(simp add: supp_perm)

   648 apply(subgoal_tac "((p \<bullet> a) \<sharp> p)")

   649 apply(simp add: fresh_def supp_perm)

   650 apply(simp add: fresh_star_def)

   651 done

   652 

   653 lemma alpha_unequal:

   654   assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" "a \<noteq> b"

   655   shows "(a, x) \<approx>abs1 (b, y)"

   656 using a

   657 apply -

   658 apply(subgoal_tac "a \<notin> supp x - {a}")

   659 apply(subgoal_tac "b \<notin> supp x - {a}")

   660 defer

   661 apply(simp add: alpha_gen)

   662 apply(simp)

   663 apply(drule_tac alpha_abs_swap)

   664 apply(assumption)

   665 apply(simp only: insert_eqvt empty_eqvt swap_atom_simps)

   666 apply(drule alpha_abs_sym)

   667 apply(rotate_tac 4)

   668 apply(drule_tac alpha_abs_trans)

   669 apply(assumption)

   670 apply(drule alpha_equal)

   671 apply(simp)

   672 apply(rule_tac p="(a \<rightleftharpoons> b)" in permute_boolE)

   673 apply(simp add: fresh_eqvt)

   674 apply(simp add: fresh_def)

   675 done

   676 

   677 lemma alpha_new_old:

   678   assumes a: "({a}, x) \<approx>abs ({b}, y)" "sort_of a = sort_of b" 

   679   shows "(a, x) \<approx>abs1 (b, y)"

   680 using a

   681 apply(case_tac "a=b")

   682 apply(simp only: alpha_equal)

   683 apply(drule alpha_unequal)

   684 apply(simp)

   685 apply(simp)

   686 apply(simp)

   687 done

   688 

   689 (* support of concrete atom sets *)

   690 

   691 lemma supp_atom_image:

   692   fixes as::"'a::at_base set"

   693   shows "supp (atom ` as) = supp as"

   694 apply(simp add: supp_def)

   695 apply(simp add: image_eqvt)

   696 apply(simp add: atom_eqvt_raw)

   697 apply(simp add: atom_image_cong)

   698 done

   699 

   700 lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn"

   701   apply (simp add: fresh_def)

   702   apply (simp add: supp_atom_image)

   703   apply (fold fresh_def)

   704   apply (simp add: swap_fresh_fresh)

   705   done

   706 

   707 (* TODO: The following lemmas can be moved somewhere... *)

   708 lemma split_rsp2[quot_respect]: "((R1 ===> R2 ===> prod_rel R1 R2 ===> op =) ===>

   709   prod_rel R1 R2 ===> prod_rel R1 R2 ===> op =) split split"

   710   by auto

   711 

   712 lemma split_prs2[quot_preserve]:

   713   assumes q1: "Quotient R1 Abs1 Rep1"

   714   and q2: "Quotient R2 Abs2 Rep2"

   715   shows "((Abs1 ---> Abs2 ---> prod_fun Abs1 Abs2 ---> id) ---> prod_fun Rep1 Rep2 ---> prod_fun Rep1 Rep2 ---> id) split = split"

   716   by (simp add: expand_fun_eq Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])

   717 

   718 lemma alpha_gen2:

   719   "(bs, x1, x2) \<approx>gen (\<lambda>(x1, y1) (x2, y2). R1 x1 x2 \<and> R2 y1 y2) (\<lambda>(a, b). f1 a \<union> f2 b) pi (cs, y1, y2) =

   720   (f1 x1 \<union> f2 x2 - bs = f1 y1 \<union> f2 y2 - cs \<and> (f1 x1 \<union> f2 x2 - bs) \<sharp>* pi \<and> R1 (pi \<bullet> x1) y1 \<and> R2 (pi \<bullet> x2) y2

   721   \<and> pi \<bullet> bs = cs)"

   722 by (simp add: alpha_gen)

   723