Theory Nominal_Sets

section ‹Nominal sets ›

theory Nominal_Sets 
imports Lambda_Terms
begin

text ‹ This theory introduces pre-nominal sets, and then nominal sets as pre-nominal 
sets 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