section ‹Nominal sets ›

theory Nominal_Sets 
imports Lambda_Terms
begin

text ‹ This theory introduces pre-nominal sets, and then nominal sets as pre-nominal
  of finite support.
 ›

locale Pre_Nominal_Set = 
fixes swapA :: "'A → var → var → 'A"
assumes 
swapA_id: "∧a x. swapA a x x = a"
and 
swapA_invol: "∧a x y. swapA (swapA a x y) x y = a"
and 
swapA_cmp: 
"∧x y a z1 z2. swapA (swapA a x y) z1 z2 =
  swapA (swapA a z1 z2) (sw x z1 z2) (sw y z1 z2)"
begin

(* freshness: *)
definition freshA where "freshA x a ≡ finite {y. swapA a y x ≠ a}"

end (* context Pre_Nominal_Set *)


locale Nominal_Set = Pre_Nominal_Set swapA 
for swapA :: "'A → var → var → 'A" 
+
assumes cofinite_freshA: "∧a. finite {x. ¬ freshA x a}"


locale Nominal_Morphism = 
A: Nominal_Set swapA + B: Nominal_Set swapB
for swapA :: "'A → var → var → 'A" and swapB :: "'B → var → var → 'B"
+
fixes f :: "'A → 'B"
assumes f_swapA_swapB: "∧a z1 z2. f (swapA a z1 z2) = swapB (f a) z1 z2"


end