From 7a4e25ebbc9e470650851299659860b4c07bff6b Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Thu, 23 Oct 2025 09:47:09 +0200
Subject: add freshness

---
 Nominal/Support.lean | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 49 insertions(+)

(limited to 'Nominal/Support.lean')

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index 78e8b3e..f2bf90d 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -245,3 +245,52 @@ lemma support_subset_supp {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S 
 end NominalSet
 
 end NominalSet
+
+section Freshness
+
+/-- A predicate quantifying a statement for "suitably fresh" atoms.
+
+We also write И a, P for for_fresh (fun a => P), using the cyrillic letter И.
+
+A proposition holds for "suitably fresh" atoms iff there are infinitely many such "suitably fresh" atoms to choose from. -/
+@[simp] def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop :=
+  {a : 𝔸 | P a}.Infinite
+
+macro "И" x:ident "," t:term : term =>
+  `(NominalSet.ForFresh (fun $x => $t))
+
+/-- We write a # x for a ∉ supp x.
+
+Note: Other conventions extend this meaning to x # y ↔ supp x ∩ supp y = ∅. We will restrict ourselves to x ∈ 𝔸. -/
+def NominalSet.IsFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Type} [NominalSet 𝔸 X] (a : 𝔸) (x : X) : Prop :=
+  a ∉ NominalSet.supp 𝔸 x
+
+infix:50 " # " => NominalSet.IsFresh
+
+namespace NominalSet
+
+variable {X : Type} [NominalSet 𝔸 X]
+
+/-- To show that an atom is fresh, it is enough to show that it doesn't occur in any finite support. -/
+lemma fresh_support {a : 𝔸} {x : X} {S : Set 𝔸} : PermSet.HasSupport 𝔸 x S → S.Finite → a ∉ S → a # x := by
+  intro hsuppS hfinS ha
+  apply Set.notMem_subset
+  · exact support_subset_supp 𝔸 hsuppS hfinS
+  · exact ha
+
+/-- One can always pick a fresh atom. -/
+lemma fresh_exists {x : X} : ∃ (a : 𝔸), a # x := by
+  unfold IsFresh; expose_names
+  have h_inf : Set.univ.Infinite := Set.infinite_univ_iff.mpr inst
+  have h_fin : (supp 𝔸 x).Finite := supp_finite 𝔸
+  obtain ⟨a, ⟨_, ha⟩⟩ := Set.Infinite.exists_notMem_finite h_inf h_fin
+  use a
+
+/-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/
+lemma for_fresh_exists {P : 𝔸 → Prop} : (И a, P a) → (∃ a, P a) := by
+  simp; intro h
+  exact Set.Infinite.nonempty h
+
+end NominalSet
+
+end Freshness
-- 
cgit v1.3.1