Packages

final case class USubstOne(subsDefsInput: Seq[SubstitutionPair]) extends (Expression) ⇒ Expression with Product with Serializable

A Uniform Substitution with its one-pass application mechanism. A Uniform Substitution uniformly replaces all occurrences of a given predicate p(.) by a formula in (.). It can also replace all occurrences of a function symbol f(.) by a term in (.) and all occurrences of a predicational / quantifier symbols C(-) by a formula in (-) and all occurrences of program constant symbol b by a hybrid program.

This type implements the application of uniform substitutions to terms, formulas, programs, and sequents.

Since

4.7

Note

Implements the one-pass version that checks admissibility on the fly and checking upon occurrence. Faster than the alternative USubstChurch. Main ingredient of prover core.

,

soundness-critical

See also

Andre Platzer. Uniform substitution at one fell swoop. In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE'19, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425-441. Springer, 2019.

edu.cmu.cs.ls.keymaerax.core.Provable.apply(subst:edu\.cmu\.cs\.ls\.keymaerax\.core\.USubstOne):edu\.cmu\.cs\.ls\.keymaerax\.core\.Provable*

USubstChurch

Linear Supertypes
Serializable, Serializable, Product, Equals, (Expression) ⇒ Expression, AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. USubstOne
  2. Serializable
  3. Serializable
  4. Product
  5. Equals
  6. Function1
  7. AnyRef
  8. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new USubstOne(subsDefsInput: Seq[SubstitutionPair])

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. def ++(other: USubstOne): USubstOne

    Union of uniform substitutions, i.e., both replacement lists merged.

    Union of uniform substitutions, i.e., both replacement lists merged.

    Note

    Convenience method not used in the core, but used for stapling uniform substitutions together during unification etc.

  4. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  5. def andThen[A](g: (Expression) ⇒ A): (Expression) ⇒ A
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  6. def apply(s: Sequent): Sequent

    Apply uniform substitution everywhere in the sequent.

    Apply uniform substitution everywhere in the sequent.

    Exceptions thrown

    SubstitutionClashException if this substitution is not admissible for s.

  7. def apply(p: DifferentialProgram): DifferentialProgram

    apply this uniform substitution everywhere in a differential program

    apply this uniform substitution everywhere in a differential program

    Exceptions thrown

    SubstitutionClashException if this substitution is not admissible for p.

  8. def apply(p: Program): Program

    apply this uniform substitution everywhere in a program

    apply this uniform substitution everywhere in a program

    Exceptions thrown

    SubstitutionClashException if this substitution is not admissible for p.

  9. def apply(f: Formula): Formula

    apply this uniform substitution everywhere in a formula

    apply this uniform substitution everywhere in a formula

    Exceptions thrown

    SubstitutionClashException if this substitution is not admissible for f.

  10. def apply(t: Term): Term

    apply this uniform substitution everywhere in a term

    apply this uniform substitution everywhere in a term

    Exceptions thrown

    SubstitutionClashException if this substitution is not admissible for t.

  11. def apply(e: Expression): Expression
    Definition Classes
    USubstOne → Function1
  12. def applyAllTaboo(s: Sequent): Sequent

    Apply uniform substitution everywhere in the sequent with SetLattice.allVars as taboos.

    Apply uniform substitution everywhere in the sequent with SetLattice.allVars as taboos.

    Exceptions thrown

    SubstitutionClashException if this substitution is not admissible for s (e.g. because it introduces any free variables).

  13. def applyAllTaboo(f: Formula): Formula

    apply this uniform substitution everywhere in a formula with SetLattice.allVars as taboos.

    apply this uniform substitution everywhere in a formula with SetLattice.allVars as taboos.

    Exceptions thrown

    SubstitutionClashException if this substitution is not admissible for f (e.g. because it introduces any free variables).

  14. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  15. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  16. def compose[A](g: (A) ⇒ Expression): (A) ⇒ Expression
    Definition Classes
    Function1
    Annotations
    @unspecialized()
  17. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  18. def finalize(): scala.Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  19. lazy val freeVars: SetLattice[Variable]

    The (new) free variables that this substitution introduces (without DotTerm/DotFormula arguments).

    The (new) free variables that this substitution introduces (without DotTerm/DotFormula arguments). That is the (new) free variables introduced by this substitution, i.e. free variables of all repl that are not bound as arguments in what.

    returns

    union of the freeVars of all our substitution pairs.

    Note

    unused

  20. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  21. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  22. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  23. final def notify(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  24. final def notifyAll(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  25. val subsDefsInput: Seq[SubstitutionPair]
  26. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  27. def toString(): String
    Definition Classes
    USubstOne → Function1 → AnyRef → Any
  28. final def wait(): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  29. final def wait(arg0: Long, arg1: Int): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  30. final def wait(arg0: Long): scala.Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from (Expression) ⇒ Expression

Inherited from AnyRef

Inherited from Any

Ungrouped