diff options
Diffstat (limited to 'Nominal/Instances')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 30 |
1 files changed, 9 insertions, 21 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index ba2fbf9..052f604 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -46,31 +46,19 @@ instance : PermSet ๐ธ (NameAbstraction' ๐ธ X) where one_smul := by intro _; ext <;> simp [one_smul] mul_smul := by intro _ _ _; ext <;> simp [mul_smul] -private def ofPair (x : (๐ธ ร X)) : NameAbstraction' ๐ธ X := โจx.fst, x.sndโฉ - -private lemma ofPair_injective : Function.Injective (ofPair ๐ธ X) := by - intro x y hxy - simp only [ofPair, mk.injEq] at hxy - ext - ยท exact hxy.left - ยท exact hxy.right - -private lemma ofPair_surjective : Function.Surjective (ofPair ๐ธ X) := by - intro x - use โจx.atom, x.bodyโฉ - simp [ofPair] - -private lemma ofPair_equivariant : Function.Equivariant ๐ธ (ofPair ๐ธ X) := by - intro x ฯ - ext <;> simp [ofPair] +private def equiv : EquivariantEquiv ๐ธ (NameAbstraction' ๐ธ X) (๐ธ ร X) := + { toFun x := โจx.atom, x.bodyโฉ + invFun x := โจx.fst, x.sndโฉ + toFun_equivariant := by intro x ฯ; ext <;> simp + } instance : NominalSet ๐ธ (NameAbstraction' ๐ธ X) := - NominalSet.fromEquivariantSurjective ๐ธ (ofPair ๐ธ X) (ofPair_equivariant ๐ธ X) (ofPair_surjective ๐ธ X) + NominalSet.fromEquivariantEquiv ๐ธ (equiv ๐ธ X) @[simp] lemma supp {x : NameAbstraction' ๐ธ X} : NominalSet.supp ๐ธ x = NominalSet.supp ๐ธ x.body โช {x.atom} := by - have h : NominalSet.supp ๐ธ (ofPair ๐ธ X (x.atom, x.body)) = NominalSet.supp ๐ธ (x.atom, x.body) := - Function.Equivariant.supp_eq_if_inj ๐ธ (ofPair_equivariant ๐ธ X) (ofPair_injective ๐ธ X) - simp only [Prod.supp, NominalSet.supp_atom, ofPair] at h + have h : NominalSet.supp ๐ธ x = NominalSet.supp ๐ธ (x.atom, x.body) := + EquivariantEquiv.supp_eq ๐ธ (equiv ๐ธ X) x + simp only [Prod.supp, NominalSet.supp_atom] at h rwa [Set.union_comm] at h @[simp] lemma fresh {a : ๐ธ} {x : NameAbstraction' ๐ธ X} : a # x โ a โ x.atom โง a # x.body := by |