diff options
Diffstat (limited to 'Nominal/Instances.lean')
| -rw-r--r-- | Nominal/Instances.lean | 19 |
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 |