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/Instances.lean | 19 +++++++++++++++++--
 Nominal/Support.lean   | 49 +++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 66 insertions(+), 2 deletions(-)

(limited to 'Nominal')

diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean
index dcf079f..215f3f9 100644
--- a/Nominal/Instances.lean
+++ b/Nominal/Instances.lean
@@ -25,7 +25,7 @@ instance : NominalSet 𝔸 𝔸 where
     intro a; use {a}
     exact ⟨NominalSet.supp_atom' 𝔸, Set.finite_singleton a⟩
 
-lemma NominalSet.supp_atom {a : 𝔸} : supp 𝔸 a = {a} := by
+@[simp] lemma NominalSet.supp_atom {a : 𝔸} : supp 𝔸 a = {a} := by
   ext b; constructor
   · apply support_subset_supp 𝔸
     · exact NominalSet.supp_atom' 𝔸
@@ -46,6 +46,9 @@ lemma NominalSet.supp_atom {a : 𝔸} : supp 𝔸 a = {a} := by
     rw [h₁] at h₂
     exact hc.left h₂
 
+@[simp] lemma NominalSet.fresh_atom {a b : 𝔸} : a # b ↔ a ≠ b := by
+  simp [IsFresh]
+
 end Atoms
 
 /-!
@@ -66,13 +69,16 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet 𝔸 X where
     · intro π hπ; simp [PermSet.fix']; rfl
     · exact Set.finite_empty
 
-lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
+@[simp] lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {x : X} : supp 𝔸 x = ∅ := by
   rw [← Set.subset_empty_iff]
   apply Set.sInter_subset_of_mem
   constructor
   · intro π hπ; simp [PermSet.fix', DiscreteNominalSet.is_discrete]
   · exact Set.finite_empty
 
+@[simp] lemma NominalSet.fresh_discrete {X : Type} [DiscreteNominalSet 𝔸 X] {a : 𝔸} {x : X} : a # x := by
+  simp [IsFresh]
+
 /-- We consider Unit a discrete nominal set. -/
 instance : DiscreteNominalSet 𝔸 Unit := NominalSet.discrete 𝔸 Unit
 
@@ -121,6 +127,9 @@ instance : NominalSet 𝔸 (X × Y) where
         suffices π ∈ PermSet.fix' 𝔸 (x, y) by simp [PermSet.fix'] at this; exact this.right
         exact (hS.out.left hπ).out
 
+@[simp] lemma NominalSet.fresh_product {a : 𝔸} {x : X} {y : Y} : a # (x, y) ↔ a # x ∧ a # y := by
+  simp [IsFresh]
+
 lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp 𝔸 (x, y) = supp 𝔸 (y, x) := by
   simp; apply Set.union_comm
 
@@ -176,4 +185,10 @@ instance : NominalSet 𝔸 (X ⊕ Y) where
     suffices π ∈ PermSet.fix' 𝔸 (.inr y : X ⊕ Y) by simp [PermSet.fix'] at this; exact this
     exact (hS.out.left hπ).out
 
+@[simp] lemma NominalSet.fresh_coproduct₁ {a : 𝔸} {x : X} : a # (.inl x : X ⊕ Y) ↔ a # x := by
+  simp [IsFresh]
+
+@[simp] lemma NominalSet.fresh_coproduct₂ {a : 𝔸} {y : Y} : a # (.inr y : X ⊕ Y) ↔ a # y := by
+  simp [IsFresh]
+
 end Coproducts
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