Theory NU_Atoms

(*<*)
theory NU_Atoms 
imports NU_Terms
begin
(*>*)

section ‹Facts about Atoms Occurring in Swappings›

fun atms :: "(string × string) list ⇒ string set" where
"atms [] = {}" | 
"atms (x#xs) = ((atms xs) ∪  {fst(x),snd(x)})"

lemma atms_append[simp]: 
  shows "atms (xs@ys) = atms xs ∪ atms ys"
  by (induct xs) auto

lemma atms_rev[simp]: 
  shows "atms (rev pi) = atms pi"
  by (induct pi) auto

lemma a_not_in_atms: 
  assumes "a ∉ atms pi"
  shows "a = swapas pi a"
  using assms by (induct pi) auto

lemma swapas_pi_ineq_a: 
  assumes  "swapas pi a ≠ a"
  shows "a ∈ atms pi"
  using a_not_in_atms assms by force

lemma a_ineq_swapas_pi: 
  assumes "a ≠ swapas pi a"
  shows "a ∈ atms pi"
  using a_not_in_atms assms by blast

lemma swapas_pi_in_atms: 
  assumes "a ∈ atms pi" 
  shows"swapas pi a ∈ atms pi"
  using assms by (metis a_not_in_atms swapas_rev_pi_a)

(*<*)
end
(*>*)