Packages

t

edu.cmu.cs.ls.keymaerax.btactics

UnifyUSCalculus

trait UnifyUSCalculus extends AnyRef

Automatic unification-based Uniform Substitution Calculus with indexing. Provides a tactic framework for automatically applying axioms and axiomatic rules by matching inputs against them by unification according to the axiom's AxiomIndex.

See also

Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.

Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017. arXiv:1601.06183

AxiomIndex

edu.cmu.cs.ls.keymaerax.bellerophon.UnificationMatch

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. UnifyUSCalculus
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Type Members

  1. type ForwardPositionTactic = (Position) ⇒ ForwardTactic

    Forward-style position tactic mapping positions and provables to provables that follow from it.

  2. type ForwardTactic = (ProvableSig) ⇒ ProvableSig

    Forward-style tactic mapping provables to provables that follow from it.

  3. type Subst = RenUSubst

    The (generalized) substitutions used for unification

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def CE(C: Context[Formula]): ForwardTactic

    CE(C) will wrap any equivalence left<->right or equality left=right fact it gets within context C.

    CE(C) will wrap any equivalence left<->right or equality left=right fact it gets within context C. Uses CE or CQ as needed.

        p(x) <-> q(x)
    --------------------- CE
     C{p(x)} <-> C{q(x)}
        f(x) = g(x)
    --------------------- CQ+CE
     c(f(x)) <-> c(g(x))
    To do

    likewise for Context[Term] using CT instead.

    See also

    CMon(Context)

    CEat(Provable)

    CE(PosInExpr

  5. def CE(inEqPos: PosInExpr): DependentTactic

    CE(pos) at the indicated position within an equivalence reduces contextual equivalence C{left}<->C{right}to argument equivalence left<->right.

    CE(pos) at the indicated position within an equivalence reduces contextual equivalence C{left}<->C{right}to argument equivalence left<->right.

        p(x) <-> q(x)
    --------------------- CE
     C{p(x)} <-> C{q(x)}

    Part of the differential dynamic logic Hilbert calculus.

    inEqPos

    the position *within* the two sides of the equivalence at which the context DotFormula occurs.

    See also

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981, 2015.

    Andre Platzer. A uniform substitution calculus for differential dynamic logic. In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, LNCS. Springer, 2015.

    UnifyUSCalculus.CEat(Provable)

    UnifyUSCalculus.CMon(PosInExpr)

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CE(Context)

  6. def CEat(fact: ProvableSig, C: Context[Formula]): DependentPositionTactic

    CEat(fact,C) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning in the given context C at the indicated position to replace right by left in that context (literally, no substitution).

    CEat(fact,C) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning in the given context C at the indicated position to replace right by left in that context (literally, no substitution).

    Examples:
    1. CE(fact, Context("x>0&⎵".asFormula))(p) is equivalent to CE(fact)(p+PosInExpr(1::Nil)). Except that the former has the shape x>0&⎵ for the context starting from position p.

    2. ,
    3. CE(fact, Context("⎵".asFormula)) is equivalent to CE(fact).

    See also

    UnifyUSCalculus.CMon(PosInExpr)

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CE(PosInExpr)

    CE(Context)

    useAt()

    UnifyUSCalculus.CEat(Provable)

  7. def CEat(fact: ProvableSig): DependentPositionTactic

    CEat(fact) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning at the indicated position to replace right by left at indicated position (literally, no substitution).

    CEat(fact) uses the equivalence left<->right or equality left=right or implication left->right fact for congruence reasoning at the indicated position to replace right by left at indicated position (literally, no substitution). Efficient unification-free version of PosInExpr):PositionTactic

                           fact
    G |- C{q(x)}, D    q(x) <-> p(x)
    -------------------------------- CER(fact)
    G |- C{p(x)}, D

    Similarly for antecedents or equality facts or implication facts, e.g.:

                           fact
    C{q(x)}, G |- D    q(x) <-> p(x)
    -------------------------------- CEL(fact)
    C{p(x)}, G |- D
    Example:
    1. CEat(fact) is equivalent to CEat(fact, Context("⎵".asFormula))

    To do

    Optimization: Would direct propositional rules make CEat faster at pos.isTopLevel?

    See also

    UnifyUSCalculus.CMon(PosInExpr)

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CE(PosInExpr)

    CE(Context)

    useAt()

    UnifyUSCalculus.CEat(Provable,Context)

  8. def CMon(C: Context[Formula]): ForwardTactic

    CMon(C) will wrap any implication left->right fact it gets within a (positive or negative) context C by monotonicity.

    CMon(C) will wrap any implication left->right fact it gets within a (positive or negative) context C by monotonicity.

       k |- o
    ------------ CMon if C{⎵} of positive polarity
    C{k} |- C{o}
    Note

    The direction in the conclusion switches for negative polarity C{⎵}

    See also

    CE(Context)

    UnifyUSCalculus.CMon(PosInExpr)

  9. def CMon: DependentPositionTactic

    Convenience CMon with hiding.

  10. def CMon(inEqPos: PosInExpr): DependentTactic

    CMon(pos) at the indicated position within an implication reduces contextual implication C{o}->C{k} to argument implication o->k for positive C.

    CMon(pos) at the indicated position within an implication reduces contextual implication C{o}->C{k} to argument implication o->k for positive C.

    |- o -> k
    ------------------------- for positive C{.}
    |- C{o} -> C{k}
    inEqPos

    the position *within* the two sides of the implication at which the context DotFormula happens.

    See also

    UnifyUSCalculus.CEat())

    UnifyUSCalculus.CMon(Context)

    UnifyUSCalculus.CE(PosInExpr)

    UnifyUSCalculus.CQ(PosInExpr)

  11. def CQ(inEqPos: PosInExpr): DependentTactic

    CQ(pos) at the indicated position within an equivalence reduces contextual equivalence p(left)<->p(right) to argument equality left=right.

    CQ(pos) at the indicated position within an equivalence reduces contextual equivalence p(left)<->p(right) to argument equality left=right. This tactic will use CEat() under the hood as needed.

         f(x) = g(x)
    --------------------- CQ
     c(f(x)) <-> c(g(x))
    inEqPos

    the position *within* the two sides of the equivalence at which the context DotTerm happens.

    See also

    UnifyUSCalculus.CMon(PosInExpr)

    UnifyUSCalculus.CE(PosInExpr)

  12. def US(fact: ProvableSig): DependentTactic

    US(fact) uses a suitable uniform substitution to reduce the proof to the proof of fact.

    US(fact) uses a suitable uniform substitution to reduce the proof to the proof of fact. Unifies the current sequent with fact.conclusion. Use that unifier as a uniform substitution to instantiate fact with.

       fact:
      g |- d
    --------- US where G=s(g) and D=s(d) where s=unify(fact.conclusion, G|-D)
      G |- D
    fact

    the proof to reduce this proof to by a suitable Uniform Substitution.

    See also

    byUS()

  13. def US(subst: USubst): BuiltInTactic
  14. def US(subst: USubst, axiom: String): BuiltInTactic

    US(subst, axiom) reduces the proof to the given axiom, whose uniform substitution instance under subst the current goal is.

  15. def US(subst: USubst, fact: ProvableSig): BuiltInTactic

    US(subst, fact) reduces the proof to a proof of fact, whose uniform substitution instance under subst the current goal is.

    US(subst, fact) reduces the proof to a proof of fact, whose uniform substitution instance under subst the current goal is.

    See also

    edu.cmu.cs.ls.keymaerax.core.Provable.apply(USubst)

  16. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  17. def boundRename(what: Variable, repl: Variable): DependentPositionTactic

    boundRename(what,repl) renames what to repl at the indicated position (or vice versa).

    boundRename(what,repl) renames what to repl at the indicated position (or vice versa).

    See also

    edu.cmu.cs.ls.keymaerax.core.BoundRenaming

  18. def by(name: String, subst: Subst): BelleExpr

    by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.

  19. def by(name: String, subst: USubst): BelleExpr

    by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.

    by(name,subst) uses the given axiom or axiomatic rule under the given substitution to prove the sequent.

     s(a) |- s(b)      a |- b
    ------------- rule(---------) if s(g)=G and s(d)=D
       G  |-  D        g |- d
    name

    the name of the fact to use to prove the sequent

    subst

    what substitution s to use for instantiating the fact called name.

    See also

    byUS()

  20. def by(lemma: Lemma, name: String): BelleExpr
  21. def by(lemma: Lemma): BelleExpr

    by(lemma) uses the given Lemma literally to continue or close the proof (if it fits to what has been proved)

  22. def by(fact: ProvableSig, name: String = "by"): BuiltInTactic

    by(provable) uses the given Provable literally to continue or close the proof (if it fits to what has been proved so far)

  23. def byUS(name: String, inst: (Subst) ⇒ Subst = us=>us): BelleExpr

    rule(name,inst) uses the given axiomatic rule to prove the sequent.

    rule(name,inst) uses the given axiomatic rule to prove the sequent. Unifies the fact's conclusion with the current sequent and proceed to the instantiated premise of fact.

     s(a) |- s(b)      a |- b
    ------------- rule(---------) if s(g)=G and s(d)=D
       G  |-  D        g |- d

    The behavior of rule(Provable) is essentially the same as that of by(Provable) except that the former prefetches the uniform substitution instance during tactics applicability checking.

    name

    the name of the fact to use to prove the sequent

    inst

    Transformation for instantiating additional unmatched symbols that do not occur in the conclusion. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.

    See also

    by()

    byUS()

  24. def byUS(name: String): BelleExpr

    byUS(axiom) proves by a uniform substitution instance of a (derived) axiom or (derived) axiomatic rule.

    byUS(axiom) proves by a uniform substitution instance of a (derived) axiom or (derived) axiomatic rule.

    See also

    UnifyUSCalculus.byUS()

  25. def byUS(lemma: Lemma): BelleExpr

    byUS(lemma) proves by a uniform substitution instance of lemma.

  26. def byUS(provable: ProvableSig): BelleExpr

    byUS(provable) proves by a uniform substitution instance of provable, obtained by unification with the current goal.

    byUS(provable) proves by a uniform substitution instance of provable, obtained by unification with the current goal.

    See also

    UnifyUSCalculus.US()

  27. def chase(keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (String) ⇒ (PosInExpr, List[PosInExpr]) = AxiomIndex.axiomIndex): DependentPositionTactic

    chase: Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.

    chase: Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.

    Chase the expression at the indicated position forward (Hilbert computation constructing the answer by proof). Follows canonical axioms toward all their recursors while there is an applicable simplifier axiom according to keys.

    keys

    maps expressions to a list of axiom names to be used for those expressions. First returned axioms will be favored (if applicable) over further axioms.

    modifier

    will be notified after successful uses of axiom at a position with the result of the use. The result of modifier(ax,pos)(step) will be used instead of step for each step of the chase.

    inst

    Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom _1. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.

    index

    Provides recursors to continue chase after applying an axiom from keys. Defaults to AxiomIndex.axiomIndex.

    Examples:
    1. When applied at 1::Nil, turns [{x'=22}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0->x+1>=1) & (x=0->1>=1))

    2. ,
    3. When applied at Nil, turns [?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into ((x>0->x+1>=1) & (x=0->1>=1))

    4. ,
    5. When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0

    To do

    also implement a backwards chase in tableaux/sequent style based on useAt instead of useFor

    Note

    Chase is search-free and, thus, quite efficient. It directly follows the axiom index information to compute follow-up positions for the chase.

    See also

    chaseFor()

    HilbertCalculus.derive

  28. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): DependentPositionTactic
  29. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String]): DependentPositionTactic
  30. def chase(breadth: Int, giveUp: Int): DependentPositionTactic

    Chase with bounded breadth and giveUp to stop.

    Chase with bounded breadth and giveUp to stop.

    breadth

    how many alternative axioms to pursue locally, using the first applicable one. Equivalent to pruning keys so that all lists longer than giveUp are replaced by Nil, and then all lists are truncated beyond breadth.

    giveUp

    how many alternatives are too much so that the chase stops without trying any for applicability. Equivalent to pruning keys so that all lists longer than giveUp are replaced by Nil.

  31. lazy val chase: DependentPositionTactic

    Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices.

    Chases the expression at the indicated position forward until it is chased away or can't be chased further without critical choices. Unlike TactixLibrary.tacticChase will not branch or use propositional rules, merely transform the chosen formula in place.

  32. def chaseCustom(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): DependentPositionTactic

    chaseCustom: Unrestricted form of chaseFor, where AxiomIndex is not built in, i.e.

    chaseCustom: Unrestricted form of chaseFor, where AxiomIndex is not built in, i.e. it takes keys of the form Expression => List[(Provable,PosInExpr, List[PosInExpr])] This allows customised rewriting

  33. def chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic
  34. def chaseFor(keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (String) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic

    chaseFor: Chases the expression of Provables at given positions forward until it is chased away or can't be chased further without critical choices.

    chaseFor: Chases the expression of Provables at given positions forward until it is chased away or can't be chased further without critical choices.

    Chase the expression at the indicated position forward (Hilbert computation constructing the answer by proof). Follows canonical axioms toward all their recursors while there is an applicable simplifier axiom according to keys.

    keys

    maps expressions to a list of axiom names to be used for those expressions. First returned axioms will be favored (if applicable) over further axioms.

    modifier

    will be notified after successful uses of axiom at a position with the result of the use. The result of modifier(ax,pos)(step) will be used instead of step for each step of the chase.

    inst

    Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom _1. Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.

    Examples:
    1. When applied at 1::Nil, turns [{x'=22}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0->x+1>=1) & (x=0->1>=1))

    2. ,
    3. When applied at Nil, turns [?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into ((x>0->x+1>=1) & (x=0->1>=1))

    4. ,
    5. When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0

    Note

    Chase is search-free and, thus, quite efficient. It directly follows the axiom index information to compute follow-up positions for the chase.

    See also

    UnifyUSCalculus.useFor()

    HilbertCalculus.derive

    chase()

  35. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst, index: (String) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic
  36. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
  37. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic): ForwardPositionTactic
  38. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst, index: (String) ⇒ (PosInExpr, List[PosInExpr])): DependentPositionTactic
  39. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], modifier: (String, Position) ⇒ ForwardTactic, inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
  40. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[String], inst: (String) ⇒ (Subst) ⇒ Subst): DependentPositionTactic
  41. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  42. def commuteEquivFR: ForwardPositionTactic

    commuteEquivFR commutes the equivalence at the given position (for forward tactics).

  43. def cutAt(repl: Expression): DependentPositionTactic

    cutAt(repl) cuts left/right to replace the expression at the indicated position in its context C{.} by repl.

    cutAt(repl) cuts left/right to replace the expression at the indicated position in its context C{.} by repl.

    G |- C{repl}, D   G |- C{repl}->C{c}, D
    --------------------------------------- cutAt(repl)
    G |- C{c}, D
    C{repl}, G |- D   G |- D, C{c}->C{repl}
    --------------------------------------- cutAt(repl)
    C{c}, G |- D
    See also

    UnifyUSCalculus.CEat(Provable)

  44. def either(left: ForwardTactic, right: ForwardTactic): ForwardTactic

    either(left,right) runs left if successful and right otherwise (for forward tactics).

  45. def eitherP(left: ForwardPositionTactic, right: ForwardPositionTactic): ForwardPositionTactic

    eitherP(left,right) runs left if successful and right otherwise (for forward tactics).

  46. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  47. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  48. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  49. def fromAxIndex(s: String): (ProvableSig, PosInExpr, List[PosInExpr])
  50. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  51. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  52. def iden: ForwardTactic

    identity tactic skip that does not no anything (for forward tactics).

  53. def ifThenElse(cond: (ProvableSig) ⇒ Boolean, thenT: ForwardTactic, elseT: ForwardTactic): ForwardTactic

    ifThenElse(cond,thenT,elseT) runs thenT if cond holds and elseT otherwise (for forward tactics).

  54. def ifThenElseP(cond: (Position) ⇒ (ProvableSig) ⇒ Boolean, thenT: ForwardPositionTactic, elseT: ForwardPositionTactic): ForwardPositionTactic

    ifThenElseP(cond,thenT,elseT) runs thenT if cond holds and elseT otherwise (for forward tactics).

  55. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  56. def lazyUseAt(lemmaName: String, key: PosInExpr): DependentPositionTactic
  57. def lazyUseAt(lemmaName: String): DependentPositionTactic

    Lazy useAt of a lemma by name.

    Lazy useAt of a lemma by name. For use with ProveAs.

  58. def let(abbr: Expression, value: Expression, inner: BelleExpr): BelleExpr

    Let(abbr, value, inner) alias let abbr=value in inner abbreviates value by abbr in the provable and proceeds with an internal proof by tactic inner, resuming to the outer proof by a uniform substitution of value for abbr of the resulting provable.

  59. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  60. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  61. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  62. def seqCompose(first: ForwardTactic, second: ForwardTactic): ForwardTactic

    seqCompose(first,second) runs first followed by second (for forward tactics).

  63. def seqComposeP(first: ForwardPositionTactic, second: ForwardPositionTactic): ForwardPositionTactic

    seqComposeP(first,second) runs first followed by second (for forward tactics).

  64. def stepAt(axiomIndex: (Expression) ⇒ Option[String]): DependentPositionTactic

    Make the canonical simplifying proof step based at the indicated position except when an unknown decision needs to be made (e.g.

    Make the canonical simplifying proof step based at the indicated position except when an unknown decision needs to be made (e.g. invariants for loops or for differential equations). Using the provided AxiomIndex.

    Note

    Efficient source-level indexing implementation.

    See also

    AxiomIndex

  65. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  66. def toString(): String
    Definition Classes
    AnyRef → Any
  67. def uniformRename(ur: URename): InputTactic

    uniformRename(ur) renames ur.what to ur.repl uniformly and vice versa.

    uniformRename(ur) renames ur.what to ur.repl uniformly and vice versa.

    See also

    edu.cmu.cs.ls.keymaerax.core.UniformRenaming

  68. def uniformRename(what: Variable, repl: Variable): InputTactic

    uniformRename(what,repl) renames what to repl uniformly and vice versa.

    uniformRename(what,repl) renames what to repl uniformly and vice versa.

    See also

    edu.cmu.cs.ls.keymaerax.core.UniformRenaming

  69. def uniformRenameF(what: Variable, repl: Variable): ForwardTactic

    uniformRenameF(what,repl) renames what to repl uniformly (for forward tactics).

  70. def uniformSubstitute(subst: USubst): BuiltInTactic

    See also

    US()

  71. def useAt(axiom: ProvableInfo, key: PosInExpr): DependentPositionTactic
  72. def useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
  73. def useAt(axiom: String): DependentPositionTactic

    useAt(axiom)(pos) uses the given (derived) axiom at the given position in the sequent (by unifying and equivalence rewriting).

  74. def useAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
  75. def useAt(axiom: String, key: PosInExpr): DependentPositionTactic
  76. def useAt(axiom: String, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic

    useAt(axiom)(pos) uses the given (derived) axiom at the given position in the sequent (by unifying and equivalence rewriting).

    useAt(axiom)(pos) uses the given (derived) axiom at the given position in the sequent (by unifying and equivalence rewriting).

    key

    the optional position of the key in the axiom to unify with. Defaults to AxiomIndex

    inst

    optional transformation augmenting or replacing the uniform substitutions after unification with additional information.

  77. def useAt(lem: Lemma): DependentPositionTactic

    useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).

  78. def useAt(lem: Lemma, key: PosInExpr): DependentPositionTactic
  79. def useAt(lem: Lemma, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic

    useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).

    useAt(lem)(pos) uses the given lemma at the given position in the sequent (by unifying and equivalence rewriting).

    key

    the optional position of the key in the axiom to unify with. Defaults to AxiomIndex

    inst

    optional transformation augmenting or replacing the uniform substitutions after unification with additional information.

  80. def useExpansionAt(axiom: String, inst: (Option[Subst]) ⇒ Subst): DependentPositionTactic
  81. def useExpansionAt(axiom: String): DependentPositionTactic

    useExpansionAt(axiom)(pos) uses the given axiom at the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.

  82. def useExpansionFor(axiom: String): ForwardPositionTactic

    useExpansionFor(axiom) uses the given axiom forward to expand the given position in the sequent (by unifying and equivalence rewriting) in the direction that expands as opposed to simplifies operators.

  83. def useFor(fact: ProvableSig, key: PosInExpr, inst: (Subst) ⇒ Subst = us => us): ForwardPositionTactic

    useFor(fact,key,inst) use the key part of the given fact forward for the selected position in the given Provable to conclude a new Provable Forward Hilbert-style proof analogue of useAt().

    useFor(fact,key,inst) use the key part of the given fact forward for the selected position in the given Provable to conclude a new Provable Forward Hilbert-style proof analogue of useAt().

      G |- C{c}, D
    ------------------ useFor(__l__<->r) if s=unify(c,l)
      G |- C{s(r)}, D

    and accordingly for facts that are l->r facts or conditional p->(l<->r) or p->(l->r) facts and so on, where l indicates the key part of the fact. useAt automatically tries proving the required assumptions/conditions of the fact it is using.

    For facts of the form

    prereq -> (left<->right)

    this tactic currently only uses master to prove prereq globally and otherwise gives up.

    fact

    the Provable fact whose conclusion to use to simplify at the indicated position of the sequent

    key

    the part of the fact's conclusion to unify the indicated position of the sequent with

    inst

    Transformation for instantiating additional unmatched symbols that do not occur in fact.conclusion(key). Defaults to identity transformation, i.e., no change in substitution found by unification. This transformation could also change the substitution if other cases than the most-general unifier are preferred.

    Example:
    1. useFor(Axiom.axiom("[;] compose"), PosInExpr(0::Nil)) applied to the indicated 1::1::Nil of [x:=1;][{x'=22}][x:=2*x;++x:=0;]x>=0 turns it into [x:=1;][{x'=22}] ([x:=2*x;]x>=0 & [x:=0;]x>=0)

    See also

    edu.cmu.cs.ls.keymaerax.btactics

    useAt()

  84. def useFor(axiom: String, key: PosInExpr, inst: (Subst) ⇒ Subst): ForwardPositionTactic

    useFor(axiom, key) use the key part of the given axiom forward for the selected position in the given Provable to conclude a new Provable

    useFor(axiom, key) use the key part of the given axiom forward for the selected position in the given Provable to conclude a new Provable

    key

    the optional position of the key in the axiom to unify with. Defaults to AxiomIndex

    inst

    optional transformation augmenting or replacing the uniform substitutions after unification with additional information.

  85. def useFor(axiom: String, key: PosInExpr): ForwardPositionTactic

    useFor(axiom, key) use the key part of the given axiom forward for the selected position in the given Provable to conclude a new Provable

  86. def useFor(axiom: String): ForwardPositionTactic

    useFor(axiom) use the given axiom forward for the selected position in the given Provable to conclude a new Provable

  87. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  88. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  89. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Inherited from AnyRef

Inherited from Any

Ungrouped