From 091fd832586627fbf31375fb5487d5e6fa6f7053 Mon Sep 17 00:00:00 2001
From: Hannes Schulze <haschu0103@outlook.de>
Date: Sun, 26 Oct 2025 13:26:57 +0100
Subject: finish name abstraction proofs

---
 Nominal/Support.lean | 18 ++++++++++++++++--
 1 file changed, 16 insertions(+), 2 deletions(-)

(limited to 'Nominal/Support.lean')

diff --git a/Nominal/Support.lean b/Nominal/Support.lean
index d80503f..b8e6809 100644
--- a/Nominal/Support.lean
+++ b/Nominal/Support.lean
@@ -271,9 +271,9 @@ section Freshness
 
 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. -/
+A proposition holds for "suitably fresh" atoms iff the set of atoms that are not "suitably fresh" is finite. -/
 def NominalSet.ForFresh {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (P : 𝔸 → Prop) : Prop :=
-  {a : 𝔸 | P a}.Infinite
+  {a : 𝔸 | P a}ᶜ.Finite
 
 macro "И" x:ident "," t:term : term =>
   `(NominalSet.ForFresh (fun $x => $t))
@@ -318,6 +318,8 @@ lemma fresh_swap_fix {a b : 𝔸} {x : X} : a # x → b # x → ⸨a, b⸩ ∈ P
 /-- 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 only [ForFresh]; intro h
+  apply Set.Finite.infinite_compl at h
+  rw [compl_compl] at h
   exact h.nonempty
 
 /-- Extensionality lemma for the freshness quantifier. -/
@@ -327,6 +329,18 @@ lemma for_fresh_ext {P Q : 𝔸 → Prop} : (∀ a, P a ↔ Q a) → (И a, P a)
   suffices {a | P a} = {a | Q a} by rw [this]
   exact Set.ext h
 
+/-- The freshness quantifier preserves implications. -/
+lemma for_fresh_imp {P Q : 𝔸 → Prop} : (И a, P a) → (∀ a, P a → Q a) → (И a, Q a) := by
+  intro hfin himp
+  apply Set.Finite.subset
+  · exact hfin
+  · simp only [Set.compl_subset_compl, Set.setOf_subset_setOf]
+    exact himp
+
+/-- The freshness quantifier commutes with conjunctions. -/
+lemma for_fresh_and {P Q : 𝔸 → Prop} : (И a, P a) ∧ (И a, Q a) ↔ (И a, P a ∧ Q a) := by
+  simp [ForFresh, Set.setOf_and, Set.compl_inter]
+
 end NominalSet
 
 end Freshness
-- 
cgit v1.3.1