MatchingLogic.EntryIII.Fresh

def MatchingLogic.Pattern.allVars {S : Signature} {Var : Type} [DecidableEq Var] : Pattern S Var → Finset Var

The finite set of every free or bound variable name occurring in a pattern.

Equations

• (MatchingLogic.Pattern.var x_1).allVars = {x_1}
• MatchingLogic.Pattern.bot.allVars = ∅
• (MatchingLogic.Pattern.app σ args).allVars = Finset.univ.biUnion fun (i : Fin (S.arity σ)) => (args i).allVars
• (phi.imp psi).allVars = phi.allVars ∪ psi.allVars
• (MatchingLogic.Pattern.ex x_1 phi).allVars = insert x_1 phi.allVars

theorem MatchingLogic.Pattern.FV_subset_allVars {S : Signature} {Var : Type} [DecidableEq Var] (p : Pattern S Var) : FV p ⊆ ↑p.allVars

Every free variable occurs in the finite set of all variable names.

def MatchingLogic.Pattern.fresh {S : Signature} (p : Pattern S ℕ) : ℕ

A canonical natural-number variable not occurring anywhere in a pattern.

Equations

• p.fresh = (insert 0 p.allVars).max' ⋯ + 1

theorem MatchingLogic.Pattern.fresh_not_mem_allVars {S : Signature} (p : Pattern S ℕ) : p.fresh ∉ p.allVars

The canonical fresh name does not occur free or bound.

theorem MatchingLogic.Pattern.fresh_not_mem_FV {S : Signature} (p : Pattern S ℕ) : p.fresh ∉ FV p

In particular, the canonical fresh name is not free.