Theory Nominal2_Lemmas

theory Nominal2_Lemmas
  imports Nominal2.Nominal2
begin

declare
  fresh_star_Pair[simp] fresh_star_insert[simp] fresh_Nil[simp] 
  pure_supp[simp] pure_fresh[simp]

lemma fresh_star_Nil[simp]: "{} ♯* t"
  unfolding fresh_star_def by auto

lemma supp_flip[simp]:
  fixes a b :: "_ :: at" 
  shows "supp (a ↔ b) = (if a = b then {} else {atom a, atom b})"
  by (auto simp: flip_def supp_swap)

lemma Collect_imp: "{x. P x ⟶ Q x} = Collect (Not o P) ∪ Collect Q"
  by auto

lemma Abs_lst2_fcb2:
  fixes a b a' b' :: "atom"
  and x y :: "'b :: fs"
  and c::"'c :: fs"
  assumes e: "[[a, a']]lst. x = [[b, b']]lst. y"
  and fcb1: "a ♯ f a a' x c" "a' ♯ f a a' x c"
  and fresh: "{a, b, a', b'} ♯* c"
  and perm1: "⋀p. supp p ♯* c ⟹ p ∙ (f a a' x c) = f (p ∙ a) (p ∙ a') (p ∙ x) c"
  and perm2: "⋀p. supp p ♯* c ⟹ p ∙ (f b b' y c) = f (p ∙ b) (p ∙ b') (p ∙ y) c"
  shows "f a a' x c = f b b' y c"
using e
apply(drule_tac Abs_lst_fcb2[where c="c" and f="λ(as::atom list) . f (hd as) (hd (tl as))"])
using fcb1 fresh perm1 perm2
apply(simp_all)
done

lemma Abs_lst2_fcb2':
  fixes a b a' b' :: "'a::at_base"
    and x y :: "'b :: fs"
    and c::"'c :: fs"
  assumes e: "[[atom a, atom a']]lst. x = [[atom b, atom b']]lst. y"
  and fcb1: "atom a ♯ f a a' x c" "atom a' ♯ f a a' x c"
  and fresh: "{atom a, atom b, atom a', atom b'} ♯* c"
  and perm1: "⋀p. supp p ♯* c ⟹ p ∙ (f a a' x c) = f (p ∙ a) (p ∙ a') (p ∙ x) c"
  and perm2: "⋀p. supp p ♯* c ⟹ p ∙ (f b b' y c) = f (p ∙ b) (p ∙ b') (p ∙ y) c"
  shows "f a a' x c = f b b' y c"
using e
apply(drule_tac Abs_lst2_fcb2[where c="c" and f="λa a'. f ((inv atom) a) ((inv atom) a')"])
using  fcb1 fresh perm1 perm2
apply(simp_all add: inv_f_f inj_on_def atom_eqvt)
done

lemma Abs_lst_eq_flipI:
  fixes a b :: "_ :: at" and t :: "_ :: fs"
  assumes "atom b ♯ t"
  shows "[[atom a]]lst. t = [[atom b]]lst. (a ↔ b) ∙ t"
  apply (auto simp: fresh_Pair)
  by (metis (no_types, lifting) assms flip_commute flip_fresh_fresh flip_triple permute_plus)

lemma Abs_lst2_eq_same_flipI:
  fixes a b :: "_ :: at"
  shows "atom b ♯ t ⟹ [[atom a, atom a]]lst. t = [[atom b, atom b]]lst. (a ↔ b) ∙ t"
  apply (cases "a = b")
   apply simp
  unfolding Abs_eq_iff alphas
  apply (intro exI[of _ "(a ↔ b)"])
  apply (auto simp: fresh_Pair fresh_at_base supp_conv_fresh
    fresh_permute_left flip_def fresh_star_def fresh_perm swap_atom)
  done

lemma Abs_lst2_eq_flipI:
  fixes a b c d :: "'a :: at" and t :: "_ :: fs"
  assumes "atom c ♯ (a, b, t)" "atom d ♯ (a, b, t)" "a = b ⟷ c = d"
  shows "[[atom a, atom b]]lst. t = [[atom c, atom d]]lst. (if a = b then (a ↔ c) else (a ↔ c) + (b ↔ d)) ∙ t"
  apply (cases "a = b")
  using assms Abs_lst2_eq_same_flipI[of d t b] apply simp
  unfolding Abs_eq_iff alphas using assms
  apply (intro exI[of _ "(a ↔ c) + (b ↔ d)"])
  apply (auto simp: fresh_Pair fresh_at_base supp_conv_fresh
    fresh_permute_left flip_def fresh_star_def fresh_perm swap_atom)
  done

lemma atom_not_fresh_eq[simp]:
  assumes "¬ atom a ♯ x"
  shows   "a = x"
  using assms atom_eq_iff fresh_ineq_at_base by blast

lemma fresh_set_fresh_forall:
  shows "atom y ♯ xs = (∀x ∈ set xs. atom y ♯ x)"
  by (induct xs) (simp_all add: fresh_Cons)

lemma finite_fresh_set_fresh_all[simp]:
  fixes S :: "(_ :: fs) set"
  shows "finite S ⟹ atom a ♯ S ⟷ (∀x ∈ S. atom a ♯ x)"
  unfolding fresh_def by (simp add: supp_of_finite_sets)

lemma case_option_eqvt[eqvt]:
  "p ∙ case_option a b opt = case_option (p ∙ a) (p ∙ b) (p ∙ opt)"
  by (cases opt) auto

end