399 

   400 lemma 

   401   fixes t1 s1::"'a::fs"

   402   and   t2 s2::"'b::fs"

   403   shows "Abs as (t1, t2) = Abs as (s1, s2) \<longrightarrow> (Abs as t1 = Abs as s1 \<and>  Abs as t2 = Abs as s2)"

   404 apply(subst abs_eq_iff)

   405 apply(subst alphas_abs)

   406 apply(subst alphas)

   407 apply(rule impI)

   408 apply(erule exE)

   409 apply(simp add: supp_Pair)

   410 apply(simp add: Un_Diff)

   411 apply(simp add: fresh_star_union)

   412 apply(erule conjE)+

   413 apply(rule conjI)

   414 apply(rule trans)

   415 apply(rule sym)

   416 apply(rule_tac p="p" in supp_perm_eq)

   417 apply(simp add: supp_abs)

   418 apply(simp)

   419 apply(rule trans)

   420 apply(rule sym)

   421 apply(rule_tac p="p" in supp_perm_eq)

   422 apply(simp add: supp_abs)

   423 apply(simp)

   424 done

   425 

   426 lemma 

   427   fixes t1 s1::"'a::fs"

   428   and   t2 s2::"'b::fs"

   429   shows "Abs as (t1, t2) = Abs bs (s1, s2) \<longrightarrow> (Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2)"

   430 apply(subst abs_eq_iff)

   431 apply(subst alphas_abs)

   432 apply(subst alphas)

   433 apply(rule impI)

   434 apply(erule exE)

   435 apply(simp add: supp_Pair)

   436 apply(simp add: Un_Diff)

   437 apply(simp add: fresh_star_union)

   438 apply(erule conjE)+

   439 apply(rule conjI)

   440 apply(rule trans)

   441 apply(rule sym)

   442 apply(rule_tac p="p" in supp_perm_eq)

   443 apply(simp add: supp_abs)

   444 apply(simp)

   445 apply(rule trans)

   446 apply(rule sym)

   447 apply(rule_tac p="p" in supp_perm_eq)

   448 apply(simp add: supp_abs)

   449 apply(simp)

   450 done

   451 

   452 lemma fresh_star_eq:

   453   assumes a: "as \<sharp>* p"

   454   shows "\<forall>a \<in> as. p \<bullet> a = a"

   455 using a by (simp add: fresh_star_def fresh_def supp_perm)

   456 

   457 lemma fresh_star_set_eq:

   458   assumes a: "as \<sharp>* p"

   459   shows "p \<bullet> as = as"

   460 using a 

   461 apply(simp add: fresh_star_def fresh_def supp_perm permute_set_eq)

   462 apply(auto)

   463 by (metis permute_atom_def)

   464 

   465 lemma 

   466   fixes t1 s1::"'a::fs"

   467   and   t2 s2::"'b::fs"

   468   shows "Abs as t1 = Abs bs s1 \<longrightarrow> Abs (as \<union> cs) t1 = Abs (bs \<union> cs) s1"

   469 apply(subst abs_eq_iff)

   470 apply(subst abs_eq_iff)

   471 apply(subst alphas_abs)

   472 apply(subst alphas_abs)

   473 apply(subst alphas)

   474 apply(subst alphas)

   475 apply(rule impI)

   476 apply(erule exE | erule conjE)+

   477 apply(rule_tac x="p" in exI)

   478 apply(simp)

   479 apply(rule conjI)

   480 apply(auto)[1]

   481 apply(rule conjI)

   482 apply(auto)[1]

   483 apply(simp add: fresh_star_def)

   484 apply(auto)[1]

   485 apply(simp add: union_eqvt)

   486 oops

   487 

   488 

   489 lemma 

   490   fixes t1 s1::"'a::fs"

   491   and   t2 s2::"'b::fs"

   492   shows "(Abs as t1 = Abs bs s1 \<and>  Abs as t2 = Abs bs s2) \<longrightarrow> Abs as (t1, t2) = Abs bs (s1, s2)"

   493 apply(subst abs_eq_iff)

   494 apply(subst abs_eq_iff)

   495 apply(subst alphas_abs)

   496 apply(subst alphas_abs)

   497 apply(subst alphas)

   498 apply(subst alphas)

   499 apply(rule impI)

   500 apply(erule exE | erule conjE)+

   501 apply(simp add: abs_eq_iff)

   502 apply(simp add: alphas_abs)

   503 apply(simp add: alphas)

   504 apply(rule conjI)

   505 apply(simp add: supp_Pair Un_Diff)

   506 oops

   507 

   508 

   509 

   510 (* support of concrete atom sets *)

   511 

   512 lemma

   513   shows "Abs as t = Abs (supp t \<inter> as) t"

   514 apply(simp add: abs_eq_iff)

   515 apply(simp add: alphas_abs)

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

   517 apply(simp add: alphas)

   518 apply(auto)

   519 oops

   520 

   521 lemma

   522   assumes "finite S"

   523   shows "\<exists>q. supp q \<subseteq> S \<union> p \<bullet> S \<and> (\<forall>a \<in> S. q \<bullet> a = p \<bullet> a)"

   524 using assms

   525 apply(induct)

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

   527 apply(simp add: supp_zero_perm)

   528 apply(auto)

   529 apply(simp add: insert_eqvt)

   530 apply(rule_tac x="((p \<bullet> x) \<rightleftharpoons> x) + q" in exI)

   531 apply(rule conjI)

   532 apply(rule subset_trans)

   533 apply(rule supp_plus_perm)

   534 apply(simp add: supp_swap)

   535 apply(auto)[1]

   536 apply(simp)

   537 apply(rule conjI)

   538 apply(case_tac "q \<bullet> x = x")

   539 apply(simp)

   540 apply(simp add: supp_perm)

   541 apply(case_tac "x \<in> p \<bullet> F")

   542 sorry