diff options
Diffstat (limited to 'Algebra/Terms.lean')
| -rw-r--r-- | Algebra/Terms.lean | 24 |
1 files changed, 7 insertions, 17 deletions
diff --git a/Algebra/Terms.lean b/Algebra/Terms.lean index 997dca4..568f5cb 100644 --- a/Algebra/Terms.lean +++ b/Algebra/Terms.lean @@ -1,7 +1,7 @@ import Mathlib import Nominal -namespace Algebra +namespace NominalAlgebra section Definitions @@ -20,9 +20,9 @@ def Signature.pureArgs (sig : Signature) (f : sig.pure) : Type := sig.args (.inl def Signature.freeArgs (sig : Signature) (f : sig.free) : Type := sig.args (.inr (.inl f)) def Signature.boundArgs (sig : Signature) (f : sig.bound) : Type := sig.args (.inr (.inr f)) -def Signature.pureArgs_fintype (sig : Signature) (f : sig.pure) : Fintype (sig.pureArgs f) := sig.args_fintype (.inl f) -def Signature.freeArgs_fintype (sig : Signature) (f : sig.free) : Fintype (sig.freeArgs f) := sig.args_fintype (.inr (.inl f)) -def Signature.boundArgs_fintype (sig : Signature) (f : sig.bound) : Fintype (sig.boundArgs f) := sig.args_fintype (.inr (.inr f)) +instance Signature.instPureArgsFintype (sig : Signature) (f : sig.pure) : Fintype (sig.pureArgs f) := sig.args_fintype (.inl f) +instance Signature.instFreeArgsFintype (sig : Signature) (f : sig.free) : Fintype (sig.freeArgs f) := sig.args_fintype (.inr (.inl f)) +instance Signature.instBoundArgsFintype (sig : Signature) (f : sig.bound) : Fintype (sig.boundArgs f) := sig.args_fintype (.inr (.inr f)) def Signature.arity (sig : Signature) (f : sig.pure ⊕ sig.free ⊕ sig.bound) : ℕ := (sig.args_fintype f).card def Signature.pureArity (sig : Signature) (f : sig.pure) : ℕ := sig.arity (.inl f) @@ -217,23 +217,13 @@ private def atoms : Term 𝔸 sig X → Set 𝔸 private lemma atoms_finite (t : Term 𝔸 sig X) : t.atoms.Finite := by fun_induction atoms <;> all_goals expose_names · exact NominalSet.supp_finite 𝔸 - · have hfin := (sig.pureArgs_fintype f).finite - apply Set.Finite.sUnion + · apply Set.Finite.sUnion · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range] apply Set.finite_range · intro S ⟨x, hS⟩ rw [← hS] exact ih1 x - · have hfin := (sig.freeArgs_fintype f).finite - apply Set.Finite.union - · exact Set.finite_singleton a - · apply Set.Finite.sUnion - · simp only [Set.setOf_exists, Set.setOf_eq_eq_singleton', Set.iUnion_singleton_eq_range] - apply Set.finite_range - · intro S ⟨x, hS⟩ - rw [← hS] - exact ih1 x - · have hfin := (sig.boundArgs_fintype f).finite + all_goals apply Set.Finite.union · exact Set.finite_singleton a · apply Set.Finite.sUnion @@ -319,4 +309,4 @@ end TermAtDepth end NominalSet -end Algebra +end NominalAlgebra |