add freshness

2 files changed, 66 insertions, 2 deletions

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