MatchingLogic.EntryIII.SymbolSupport #
The finite set of signature symbols occurring in a pattern.
Equations
- (MatchingLogic.Pattern.var a).symbolSupport = ∅
- MatchingLogic.Pattern.bot.symbolSupport = ∅
- (MatchingLogic.Pattern.app sigma args).symbolSupport = insert sigma (Finset.univ.biUnion fun (i : Fin (S.arity sigma)) => (args i).symbolSupport)
- (phi.imp psi).symbolSupport = phi.symbolSupport ∪ psi.symbolSupport
- (MatchingLogic.Pattern.ex a phi).symbolSupport = phi.symbolSupport
Instances For
theorem
MatchingLogic.Pattern.head_mem_symbolSupport
{S : Signature}
{Var : Type}
[DecidableEq S.Sym]
(sigma : S.Sym)
(args : Fin (S.arity sigma) → Pattern S Var)
:
Every head symbol belongs to the support of its application pattern.
theorem
MatchingLogic.Pattern.argument_symbolSupport_subset
{S : Signature}
{Var : Type}
[DecidableEq S.Sym]
(sigma : S.Sym)
(args : Fin (S.arity sigma) → Pattern S Var)
(i : Fin (S.arity sigma))
:
(args i).symbolSupport ⊆ (app sigma args).symbolSupport
Every symbol of an argument belongs to the support of the whole application.
theorem
MatchingLogic.Pattern.symbolSupport_conj
{S : Signature}
{Var : Type}
[DecidableEq S.Sym]
(l : List (Pattern S Var))
:
(conj l).symbolSupport = List.foldr (fun (p : Pattern S Var) (support : Finset S.Sym) => p.symbolSupport ∪ support) ∅ l
The support of a finite conjunction is the union of the supports of its members.