add freshness

1 files changed, 17 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