Packages

trait HilbertCalculus extends UnifyUSCalculus

Hilbert Calculus for differential dynamic logic.

Provides the axioms and axiomatic proof rules from Figure 2 and Figure 3 in: Andre Platzer. A complete uniform substitution calculus for differential dynamic logic. Journal of Automated Reasoning, 59(2), pp. 219-266, 2017.

See also

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

Andre Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.

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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

Andre Platzer. Differential game logic. ACM Trans. Comput. Log. 17(1), 2015. arXiv 1408.1980

Andre Platzer. Logics of dynamical systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 13-24. IEEE 2012

Andre Platzer. The complete proof theory of hybrid systems. ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pages 541-550. IEEE 2012

HilbertCalculus.stepAt()

HilbertCalculus.derive()

edu.cmu.cs.ls.keymaerax.core.AxiomBase

edu.cmu.cs.ls.keymaerax.btactics.Ax

TactixLibrary

Linear Supertypes
UnifyUSCalculus, AnyRef, Any
Known Subclasses
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. HilbertCalculus
  2. UnifyUSCalculus
  3. AnyRef
  4. 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.

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

    Definition Classes
    UnifyUSCalculus
  2. type ForwardTactic = (ProvableSig) ⇒ ProvableSig

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

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

    Definition Classes
    UnifyUSCalculus
  3. type Subst = RenUSubst

    The (generalized) substitutions used for unification

    The (generalized) substitutions used for unification

    Definition Classes
    UnifyUSCalculus

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))
    Definition Classes
    UnifyUSCalculus
    To do

    likewise for Context[Term] using CT instead.

    See also

    CE(PosInExpr

    CEat(Provable)

    CMon(Context)

  5. def CE(inEqPos: PosInExpr): InputTactic

    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.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$88 , x$87 , x$89 , x$85 , x$86 , x$90 , x$91 , x$92 , x$93 , x$94 , x$95 , x$96 )
    See also

    UnifyUSCalculus.CE(Context)

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CMon(PosInExpr)

    UnifyUSCalculus.CEat(Provable)

    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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

  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).

    Definition Classes
    UnifyUSCalculus
    Examples:
    1. CE(fact, Context("⎵".asFormula)) is equivalent to CE(fact).

    2. ,
    3. 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.

    See also

    UnifyUSCalculus.CEat(Provable)

    useAtImpl()

    CE(Context)

    UnifyUSCalculus.CE(PosInExpr)

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CMon(PosInExpr)

  7. def CEat(fact: ProvableSig, key: PosInExpr): BuiltInPositionTactic

    CEat replacing key with the other expression in the equality/equivalence.

    CEat replacing key with the other expression in the equality/equivalence. @see CEat(ProvableSig)

    Definition Classes
    UnifyUSCalculus
  8. def CEat(fact: ProvableSig): BuiltInPositionTactic

    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
    Definition Classes
    UnifyUSCalculus
    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.CEat(Provable,Context)

    useAtImpl()

    CE(Context)

    UnifyUSCalculus.CE(PosInExpr)

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CMon(PosInExpr)

  9. def CEimp(inEqPos: PosInExpr): InputTactic

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

    CEimply(pos) at the indicated position within an equivalence reduces contextual implication 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.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$99 , x$100 , x$101 , x$97 , x$98 , x$102 , x$103 , x$104 , x$105 , x$106 , x$107 , x$108 )
    See also

    UnifyUSCalculus.CE(Context)

    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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

  10. def CErevimp(inEqPos: PosInExpr): InputTactic

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

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

        q(x) <-> p(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.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$111 , x$112 , x$113 , x$109 , x$110 , x$114 , x$115 , x$116 , x$117 , x$118 , x$119 , x$120 )
    See also

    UnifyUSCalculus.CE(Context)

    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. A uniform substitution calculus for differential dynamic logic. arXiv 1503.01981

  11. 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}
    Definition Classes
    UnifyUSCalculus
    Note

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

    See also

    UnifyUSCalculus.CMon(PosInExpr)

    CE(Context)

  12. def CMon: BuiltInRightTactic

    Convenience CMon first hiding other context.

    Convenience CMon first hiding other context.

      |- o -> k
    ------------------------- for positive C{.}
    G |- C{o} -> C{k}, D
      |- k -> o
    ------------------------- for negative C{.}
    G |- C{o} -> C{k}, D
    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$135 , x$136 , x$137 , x$133 , x$134 , x$138 , x$139 , x$140 , x$141 , x$142 , x$143 , x$144 )
    See also

    CMon()

  13. def CMon(inEqPos: PosInExpr): InputTactic

    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. Contextual monotonicity proof rule.

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

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

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$124 , x$123 , x$125 , x$121 , x$122 , x$126 , x$127 , x$128 , x$129 , x$130 , x$131 , x$132 )
    See also

    UnifyUSCalculus.CQ(PosInExpr)

    UnifyUSCalculus.CE(PosInExpr)

    UnifyUSCalculus.CMon(Context)

    UnifyUSCalculus.CEat())

    HilbertCalculus.monb

    HilbertCalculus.mond

  14. def CQ(inEqPos: PosInExpr): InputTactic

    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.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$51 , x$52 , x$53 , x$49 , x$50 , x$54 , x$55 , x$56 , x$57 , x$58 , x$59 , x$60 )
    See also

    UnifyUSCalculus.CE(PosInExpr)

    UnifyUSCalculus.CMon(PosInExpr)

  15. def CQimp(inEqPos: PosInExpr): InputTactic

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

    CQimply(pos) at the indicated position within an equivalence reduces contextual implication 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.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$63 , x$64 , x$65 , x$61 , x$62 , x$66 , x$67 , x$68 , x$69 , x$70 , x$71 , x$72 )
    See also

    UnifyUSCalculus.CE(PosInExpr)

    UnifyUSCalculus.CMon(PosInExpr)

  16. def CQrevimp(inEqPos: PosInExpr): InputTactic

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

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

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

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

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$75 , x$76 , x$77 , x$73 , x$74 , x$78 , x$79 , x$80 , x$81 , x$82 , x$83 , x$84 )
    See also

    UnifyUSCalculus.CE(PosInExpr)

    UnifyUSCalculus.CMon(PosInExpr)

  17. def DC(invariant: Formula): DependentPositionWithAppliedInputTactic

    DC: Differential Cut a new invariant for a differential equation [{x'=f(x)&q(x)}]p(x) reduces to [{x'=f(x)&q(x)&C(x)}]p(x) with [{x'=f(x)&q(x)}]C(x).

    DC: Differential Cut a new invariant for a differential equation [{x'=f(x)&q(x)}]p(x) reduces to [{x'=f(x)&q(x)&C(x)}]p(x) with [{x'=f(x)&q(x)}]C(x).

    Use:                      Show:
    G |- [x'=f(x)&Q&R]P, D    G |- [x'=f(x)&Q]R, D
    ---------------------------------------------- DC(R)
    G |- [x'=f(x)&Q]P, D
    Use:                         Show:
    G |- A->[x'=f(x)&Q&R]P, D    G |- A->[x'=f(x)&Q]R, D
    ---------------------------------------------- dC(R)
    G |- A->[x'=f(x)&Q]P, D
    Annotations
    @Tactic( x$124 , x$125 , x$126 , x$127 , x$121 , x$128 , x$129 , x$130 , x$131 , x$123 , x$122 , x$132 )
    See also

    DifferentialEquationCalculus.dC()

  18. def DCd(invariant: Formula): DependentPositionWithAppliedInputTactic

    DCd: Diamond Differential Cut a new invariant for a differential equation <{x'=f(x)&q(x)}>p(x) reduces to <{x'=f(x)&q(x)&C(x)}>p(x) with [{x'=f(x)&q(x)}]C(x).

    DCd: Diamond Differential Cut a new invariant for a differential equation <{x'=f(x)&q(x)}>p(x) reduces to <{x'=f(x)&q(x)&C(x)}>p(x) with [{x'=f(x)&q(x)}]C(x).

    Annotations
    @Tactic( x$136 , x$137 , x$138 , x$139 , x$133 , x$140 , x$141 , x$142 , x$143 , x$135 , x$134 , x$144 )
  19. lazy val DE: DependentPositionTactic

    DE: Differential Effect exposes the effect of a differential equation [x'=f(x)]p(x,x') on its differential symbols as [x'=f(x)][x':=f(x)]p(x,x') with its differential assignment x':=f(x).

    DE: Differential Effect exposes the effect of a differential equation [x'=f(x)]p(x,x') on its differential symbols as [x'=f(x)][x':=f(x)]p(x,x') with its differential assignment x':=f(x).

    G |- [{x'=f(||)&H(||)}][x':=f(||);]p(||), D
    -------------------------------------------
    G |- [{x'=f(||)&H(||)}]p(||), D
    Examples:
    1. |- [{x'=1}][x':=1;]x>0
      -----------------------DE(1)
      |- [{x'=1}]x>0
    2. ,
    3. |- [{x'=1, y'=x & x>0}][y':=x;][x':=1;]x>0
      -------------------------------------------DE(1)
      |- [{x'=1, y'=x & x>0}]x>0
  20. lazy val DI: BuiltInPositionTactic

    DI: Differential Invariants are used for proving a formula to be an invariant of a differential equation.

    DI: Differential Invariants are used for proving a formula to be an invariant of a differential equation. [x'=f(x)&q(x)]p(x) reduces to q(x) -> p(x) & [x'=f(x)]p(x)'.

    See also

    DifferentialEquationCalculus.dI()

  21. lazy val DS: BuiltInPositionTactic

    DS: Differential Solution solves a simple differential equation [x'=c&q(x)]p(x) by reduction to \forall t>=0 ((\forall 0<=s<=t q(x+c()*s) -> [x:=x+c()*t;]p(x))

  22. lazy val DW: BuiltInPositionTactic

    DW: Differential Weakening to use evolution domain constraint [{x'=f(x)&q(x)}]p(x) reduces to [{x'=f(x)&q(x)}](q(x)->p(x)).

    DW: Differential Weakening to use evolution domain constraint [{x'=f(x)&q(x)}]p(x) reduces to [{x'=f(x)&q(x)}](q(x)->p(x)).

    G |- [x'=f(x)&Q](Q->P), D
    ------------------------- DW(R)
    G |- [x'=f(x)&Q]P, D
    See also

    DifferentialEquationCalculus.dW()

  23. lazy val DWd: BuiltInPositionTactic

    DWd: Diamond Differential Weakening to use evolution domain constraint <{x'=f(x)&q(x)}>p(x) reduces to <{x'=f(x)&q(x)}>(q(x)&p(x))

  24. lazy val Dassignb: BuiltInPositionTactic

    Dassignb: [':=] Substitute a differential assignment [x':=f]p(x') to p(f)

  25. val G: DependentPositionTactic

    G: Gödel generalization rule reduces a proof of Γ |- [a]p(x), Δ to proving the postcondition |- p(x) in isolation.

    G: Gödel generalization rule reduces a proof of Γ |- [a]p(x), Δ to proving the postcondition |- p(x) in isolation.

      |- p(||)
    --------------- G
    G |- [a]p(||), D

    This rule is a special case of rule monb with p(x)=True by boxTrue.

    Annotations
    @Tactic( x$39 , x$40 , x$41 , x$37 , x$38 , x$42 , x$43 , x$44 , x$45 , x$46 , x$47 , x$48 )
    Note

    Unsound for hybrid games

    See also

    monb with p(x)=True

    boxTrue

  26. lazy val K: BuiltInPositionTactic

    K: modal modus ponens (hybrid systems)

    K: modal modus ponens (hybrid systems)

    Note

    Use with care since limited to hybrid systems. Use monb instead.

    See also

    monb

    mond

  27. def US(fact: ProvableSig): BuiltInTactic

    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.

    Definition Classes
    UnifyUSCalculus
    See also

    byUS()

  28. def US(subst: USubst): BuiltInTactic

    US(subst) uses a uniform substitution of rules to transform an entire provable.

    US(subst) uses a uniform substitution of rules to transform an entire provable.

     G1 |- D1 ... Gn |- Dn              s(G1) |- s(D1) ... s(Gn) |- s(Dn)
    -----------------------     =>     -----------------------------------   (USR)
             G |- D                                s(G) |- s(D)
    subst

    The uniform substitution s (of no free variables) to be used on the premises and conclusion of the provable.

    Definition Classes
    UnifyUSCalculus
    See also

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

    ProvableInfo)

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

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

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

    s(g1) |- s(d1) ... s(gn) |- s(dn)        g1 |- d1 ... gn |- dn
    ---------------------------------   if  ----------------------- fact
            G |- D                                   g |- d
    where G=s(g) and D=s(d)
    subst

    the substitution s that instantiates fact g |- d to the present goal G |- D.

    fact

    the fact g |- d to reduce the proof to. Facts do not have to be proved yet.

    Definition Classes
    UnifyUSCalculus
    See also

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

    ProvableInfo)

  30. def US(subst: USubst, fact: ProvableInfo): BuiltInTactic

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

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

        *              *
    ---------   if  -------- fact
      G |- D         g |- d
    where G=s(g) and D=s(d)

    When fact is an axiomatic rule:

    s(g1) |- s(d1) ... s(gn) |- s(dn)        g1 |- d1 ... gn |- dn
    ---------------------------------   if  ----------------------- fact
            G |- D                                   g |- d
    where G=s(g) and D=s(d)
    subst

    the substitution s that instantiates fact g |- d to the present goal G |- D.

    fact

    the provable for the axiom g |- d to reduce the proof to (accordingly for axiomatic rules).

    Definition Classes
    UnifyUSCalculus
    See also

    US(USubst,ProvableSig)

  31. def USX(S: List[SubstitutionPair]): InputTactic
    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$37 , x$38 , x$41 , x$40 , x$39 , x$42 , x$43 , x$44 , x$45 , x$46 , x$47 , x$48 )
  32. lazy val V: BuiltInPositionTactic

    V: vacuous box [a]p() will be discarded and replaced by p() provided program a does not change values of postcondition p().

    V: vacuous box [a]p() will be discarded and replaced by p() provided program a does not change values of postcondition p().

    Note

    Unsound for hybrid games

  33. lazy val VK: BuiltInPositionTactic

    VK: vacuous box [a]p() will be discarded and replaced by p() provided program a does not change values of postcondition p() and provided [a]true proves, e.g., since a is a hybrid system.

  34. lazy val allDist: BuiltInPositionTactic

    allDist: distribute \forall x p(x) -> \forall x q(x) by replacing it with \forall x (p(x)->q(x)).

    allDist: distribute \forall x p(x) -> \forall x q(x) by replacing it with \forall x (p(x)->q(x)).

    See also

    allDistElim

  35. lazy val allDistElim: BuiltInPositionTactic

    allDistElim: distribute \forall x P -> \forall x Q by replacing it with \forall x (P->Q).

  36. lazy val allV: BuiltInPositionTactic

    allV: vacuous \forall x p() will be discarded and replaced by p() provided x does not occur in p().

  37. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  38. lazy val assignb: BuiltInPositionTactic

    assignb: [:=] simplify assignment [x:=f;]p(x) by substitution p(f) or equation.

    assignb: [:=] simplify assignment [x:=f;]p(x) by substitution p(f) or equation. Box assignment by substitution assignment [v:=t();]p(v) <-> p(t()) (preferred), or by equality assignment [x:=f();]p(||) <-> \forall x (x=f() -> p(||)) as a fallback. Universal quantifiers are skolemized if applied at top-level in the succedent; they remain unhandled in the antecedent and in non-top-level context.

    Annotations
    @Tactic( x$1 , x$4 , x$5 , x$6 , x$3 , x$7 , x$8 , x$9 , x$10 , x$2 , x$11 , x$12 )
    Examples:
    1. |- 1>0
      --------------------assignb(1)
      |- [x:=1;]x>0
    2. ,
    3.        1>0 |-
      --------------------assignb(-1)
      [x:=1;]x>0 |-
    4. ,
    5. x_0=1 |- [{x_0:=x_0+1;}*]x_0>0
      ----------------------------------assignb(1)
            |- [x:=1;][{x:=x+1;}*]x>0
    6. ,
    7. \\forall x_0 (x_0=1 -> [{x_0:=x_0+1;}*]x_0>0) |-
      -------------------------------------------------assignb(-1)
                             [x:=1;][{x:=x+1;}*]x>0 |-
    8. ,
    9. |- [y:=2;]\\forall x_0 (x_0=1 -> x_0=1 -> [{x_0:=x_0+1;}*]x_0>0)
      -----------------------------------------------------------------assignb(1, 1::Nil)
      |- [y:=2;][x:=1;][{x:=x+1;}*]x>0
    See also

    DLBySubst.assignEquality

  39. lazy val assignbDual: BuiltInPositionTactic
    Annotations
    @Tactic( x$109 , x$111 , x$112 , x$113 , x$110 , x$114 , x$115 , x$116 , x$117 , x$118 , x$119 , x$120 )
  40. lazy val assignd: DependentPositionTactic

    assignd: <:=> simplify assignment <x:=f;>p(x) by substitution p(f) or equation

    assignd: <:=> simplify assignment <x:=f;>p(x) by substitution p(f) or equation

    Annotations
    @Tactic( x$73 , x$76 , x$77 , x$78 , x$75 , x$79 , x$80 , x$81 , x$82 , x$74 , x$83 , x$84 )
  41. lazy val assigndDual: BuiltInPositionTactic
  42. def boundRename(what: Variable, repl: Variable): BuiltInPositionTactic

    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).

    Definition Classes
    UnifyUSCalculus
    See also

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

  43. lazy val box: BuiltInPositionTactic

    box: [.] to reduce double-negated diamond !⟨a⟩!p(x) to a box [a]p(x).

  44. lazy val boxAnd: BuiltInPositionTactic

    boxAnd: splits [a](p&q) into [a]p & [a]q

  45. lazy val boxImpliesAnd: BuiltInPositionTactic

    boxImpliesAnd: splits [a](p->q&r) into [a](p->q) & [a](p->r)

  46. lazy val boxTrue: BuiltInPositionTactic

    boxTrue: proves [a]true directly for hybrid systems a that are not hybrid games.

    boxTrue: proves [a]true directly for hybrid systems a that are not hybrid games.

    Annotations
    @Tactic( x$145 , x$148 , x$149 , x$150 , x$146 , x$151 , x$152 , x$147 , x$153 , x$154 , x$155 , x$156 )
  47. lazy val boxd: BuiltInPositionTactic
    Annotations
    @Tactic( x$97 , x$99 , x$100 , x$101 , x$98 , x$102 , x$103 , x$104 , x$105 , x$106 , x$107 , x$108 )
  48. def by(lemma: Lemma, subst: Subst): 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.

    Definition Classes
    UnifyUSCalculus
  49. def by(lemma: Lemma, subst: USubst): BelleExpr
    Definition Classes
    UnifyUSCalculus
  50. def by(pi: ProvableInfo, subst: Subst): BelleExpr
    Definition Classes
    UnifyUSCalculus
  51. def by(pi: ProvableInfo, subst: USubst): BelleExpr

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

    by(pi,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
    pi

    the provable to use to prove the sequent

    subst

    what substitution s to use for instantiating the fact pi.

    Definition Classes
    UnifyUSCalculus
    See also

    byUS()

  52. def by(lemma: Lemma): BelleExpr
    Definition Classes
    UnifyUSCalculus
  53. def by(pi: ProvableInfo): BelleExpr

    by(pi) uses the given provable with its information literally to continue or close the proof (if it fits to what has been proved).

    by(pi) uses the given provable with its information literally to continue or close the proof (if it fits to what has been proved).

    pi

    the information for the Provable to use, e.g., from Ax.

    Definition Classes
    UnifyUSCalculus
  54. def byUS(pi: ProvableInfo, inst: (Subst) ⇒ Subst): BelleExpr

    rule(pi,inst) uses the given axiom or axiomatic rule to prove the sequent.

    rule(pi,inst) uses the given axiom or 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.

    pi

    the provable info for 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 modify the unifier if other cases than the most-general unifier are preferred.

    Definition Classes
    UnifyUSCalculus
    See also

    byUS()

    by()

  55. def byUS(lemma: Lemma): BelleExpr

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

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

    Definition Classes
    UnifyUSCalculus
  56. def byUS(provable: ProvableSig): BuiltInTactic

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

    byUS(pi) proves by a uniform substitution instance of provable (information), obtained by unification with the current goal. Like by(ProvableInfo,USubst) except that the required substitution is automatically obtained by unification.

    Definition Classes
    UnifyUSCalculus
    See also

    UnifyUSCalculus.US()

  57. def byUS(pi: ProvableInfo): BelleExpr

    byUS(pi) proves by a uniform substitution instance of provable (information) or axiom or axiomatic rule, obtained by unification with the current goal.

    byUS(pi) proves by a uniform substitution instance of provable (information) or axiom or axiomatic rule, obtained by unification with the current goal. Like by(ProvableInfo,USubst) except that the required substitution is automatically obtained by unification.

    Definition Classes
    UnifyUSCalculus
    See also

    UnifyUSCalculus.US()

  58. def chase(keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr]) = AxIndex.axiomIndex): BuiltInPositionTactic

    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. Defaults to AxIndex.axiomFor().

    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. Defaults to identity transformation, i.e., no modification in found match.

    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 AxIndex.axiomIndex.

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

    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}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0->x+1>=1) & (x=0->1>=1))

    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

    HilbertCalculus.derive

    chaseFor()

  59. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic): BuiltInPositionTactic
    Definition Classes
    UnifyUSCalculus
  60. def chase(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo]): BuiltInPositionTactic
    Definition Classes
    UnifyUSCalculus
  61. def chase(breadth: Int, giveUp: Int): BuiltInPositionTactic

    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.

    Definition Classes
    UnifyUSCalculus
  62. val chase: BuiltInPositionTactic

    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.chaseAt will not branch or use propositional rules, merely transform the chosen formula in place.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$2 , x$3 , x$1 , x$4 , x$5 , x$6 , x$7 , x$8 , x$9 , x$10 , x$11 , x$12 )
  63. def chaseCustom(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): BuiltInPositionTactic

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

    chaseCustom: Unrestricted form of chase where AxiomIndex is not built in, i.e. it takes keys of the form Expression => List[(Provable,PosInExpr, List[PosInExpr])] This allows customized rewriting using provables derived at runtime

    Definition Classes
    UnifyUSCalculus
  64. def chaseCustomFor(keys: (Expression) ⇒ List[(ProvableSig, PosInExpr, List[PosInExpr])]): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  65. def chaseFor(keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst = ax=>us=>us, index: (ProvableInfo) ⇒ (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 axioms/tactics to be used for those expressions. The first applicable axiom/tactic will be chosen. Defaults to AxIndex.axiomIndex.

    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. Defaults to identity transformation, i.e., no modification in found match.

    inst

    Transformation for instantiating additional unmatched symbols that do not occur when using the given axiom. 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

    The key and recursor information determining (as in AxiomInfo)

    • ._1 which subexpression of the ProvableInfo to match against.
    • ._2 which resulting recursors to continue chasing after in the resulting expression. Defaults to AxIndex.axiomIndex.
    Definition Classes
    UnifyUSCalculus
    Examples:
    1. When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+(x'*y+x*y')>=0

    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}][?x>0;x:=x+1;++?x=0;x:=1;]x>=1 into [{x'=22}]((x>0->x+1>=1) & (x=0->1>=1))

    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

    chase()

    HilbertCalculus.derive

  66. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr])): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  67. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  68. def chaseFor(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  69. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst, index: (ProvableInfo) ⇒ (PosInExpr, List[PosInExpr])): BuiltInPositionTactic
    Definition Classes
    UnifyUSCalculus
  70. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], modifier: (ProvableInfo, Position) ⇒ ForwardTactic, inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): BuiltInPositionTactic
    Definition Classes
    UnifyUSCalculus
  71. def chaseI(breadth: Int, giveUp: Int, keys: (Expression) ⇒ List[ProvableInfo], inst: (ProvableInfo) ⇒ (Subst) ⇒ Subst): BuiltInPositionTactic
    Definition Classes
    UnifyUSCalculus
  72. lazy val choiceb: BuiltInPositionTactic

    choiceb: [++] handles both cases of a nondeterministic choice [a++b]p(x) separately [a]p(x) & [b]p(x)

  73. lazy val choiced: BuiltInPositionTactic

    choiced: <++> handles both cases of a nondeterministic choice ⟨a++b⟩p(x) separately ⟨a⟩p(x) | ⟨b⟩p(x)

  74. def clone(): AnyRef
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )
  75. def commuteEquivFR: ForwardPositionTactic

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

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

    Definition Classes
    UnifyUSCalculus
  76. lazy val composeb: BuiltInPositionTactic

    composeb: [;] handle both parts of a sequential composition [a;b]p(x) one at a time [a][b]p(x)

  77. lazy val composed: BuiltInPositionTactic

    composed: <;> handle both parts of a sequential composition ⟨a;b⟩p(x) one at a time ⟨a⟩⟨b⟩p(x)

  78. def cutAt(repl: Expression): DependentPositionWithAppliedInputTactic

    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
    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$147 , x$148 , x$149 , x$145 , x$146 , x$150 , x$151 , x$152 , x$153 , x$154 , x$155 , x$156 )
    See also

    UnifyUSCalculus.CEat(Provable)

  79. val deepChase: BuiltInPositionTactic

    Chases the expression at the indicated position forward.

    Chases the expression at the indicated position forward. Unlike chase descends into formulas and terms exhaustively.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( x$14 , x$15 , x$13 , x$16 , x$17 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )
  80. lazy val derive: BuiltInPositionTactic

    Derive the differential expression at the indicated position (Hilbert computation deriving the answer by proof) to get rid of the differential operators.

    Derive the differential expression at the indicated position (Hilbert computation deriving the answer by proof) to get rid of the differential operators.

    Annotations
    @Tactic( x$49 , x$51 , x$52 , x$53 , x$54 , x$55 , x$56 , x$57 , x$58 , x$50 , x$59 , x$60 )
    Example:
    1. When applied at 1::Nil, turns [{x'=22}](2*x+x*y>=5)' into [{x'=22}]2*x'+x'*y+x*y'>=0

    See also

    UnifyUSCalculus.chase

  81. lazy val diamond: BuiltInPositionTactic

    diamond: <.> reduce double-negated box ![a]!p(x) to a diamond ⟨a⟩p(x).

  82. lazy val diamondOr: BuiltInPositionTactic

    diamondOr: splits ⟨a⟩(p|q) into ⟨a⟩p | ⟨a⟩q

  83. lazy val diamondd: BuiltInPositionTactic
    Annotations
    @Tactic( x$61 , x$63 , x$64 , x$65 , x$62 , x$66 , x$67 , x$68 , x$69 , x$70 , x$71 , x$72 )
  84. lazy val dualb: BuiltInPositionTactic

    dualb: [d] handle dual game [{a}d]p(x) by ![a]!p(x)

  85. lazy val duald: BuiltInPositionTactic

    duald: <d> handle dual game ⟨{a}d⟩p(x) by !⟨a⟩!p(x)

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

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

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

    Definition Classes
    UnifyUSCalculus
  87. def eitherP(left: ForwardPositionTactic, right: ForwardPositionTactic): ForwardPositionTactic

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

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

    Definition Classes
    UnifyUSCalculus
  88. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  89. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  90. lazy val existsE: BuiltInPositionTactic

    existsE: show \exists x P by showing that it follows from P.

  91. lazy val existsV: BuiltInPositionTactic

    existsV: vacuous \exists x p() will be discarded and replaced by p() provided x does not occur in p().

  92. val fail: BuiltInTactic

    fail is a tactic that always fails as being inapplicable

    fail is a tactic that always fails as being inapplicable

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
    See also

    skip

  93. def finalize(): Unit
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  94. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  95. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  96. def iden: ForwardTactic

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

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

    Definition Classes
    UnifyUSCalculus
  97. 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).

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

    Definition Classes
    UnifyUSCalculus
  98. 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).

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

    Definition Classes
    UnifyUSCalculus
  99. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  100. lazy val iterateb: BuiltInPositionTactic

    iterateb: [*] prove a property of a loop [{a}*]p(x) by unrolling it once p(x) & [a][{a}*]p(x)

  101. lazy val iterated: BuiltInPositionTactic

    iterated: <*> prove a property of a loop ⟨{a}*⟩p(x) by unrolling it once p(x) | ⟨a⟩⟨{a}*⟩p(x)

  102. 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.

    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.

    Definition Classes
    UnifyUSCalculus
  103. lazy val monall: BuiltInTactic

    allG: all generalization rule reduces a proof of \forall x p(x) |- \forall x q(x) to proving p(x) |- q(x) in isolation.

    allG: all generalization rule reduces a proof of \forall x p(x) |- \forall x q(x) to proving p(x) |- q(x) in isolation.

       p(x) |- q(x)
    ---------------------------------
    \forall x p(x) |- \forall x q(x)
    Annotations
    @Tactic( x$87 , x$88 , x$89 , x$85 , x$86 , x$90 , x$91 , x$92 , x$93 , x$94 , x$95 , x$96 )
    See also

    UnifyUSCalculus.CMon()

  104. lazy val monb: BuiltInTactic

    monb: Monotone [a]p(x) |- [a]q(x) reduces to proving p(x) |- q(x).

    monb: Monotone [a]p(x) |- [a]q(x) reduces to proving p(x) |- q(x).

       p(x) |- q(x)
    ------------------- M[.]
    [a]p(x) |- [a]q(x)
    Annotations
    @Tactic( x$27 , x$28 , x$29 , x$25 , x$26 , x$30 , x$31 , x$32 , x$33 , x$34 , x$35 , x$36 )
    See also

    UnifyUSCalculus.CMon()

  105. lazy val mond: BuiltInTactic

    mond: Monotone ⟨a⟩p(x) |- ⟨a⟩q(x) reduces to proving p(x) |- q(x).

    mond: Monotone ⟨a⟩p(x) |- ⟨a⟩q(x) reduces to proving p(x) |- q(x).

       p(x) |- q(x)
    ------------------- M
    ⟨a⟩p(x) |- ⟨a⟩q(x)
    Annotations
    @Tactic( x$15 , x$16 , x$17 , x$13 , x$14 , x$18 , x$19 , x$20 , x$21 , x$22 , x$23 , x$24 )
    See also

    UnifyUSCalculus.CMon()

  106. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  107. val nil: BuiltInTactic

    nil=skip is a no-op tactic that has no effect

    nil=skip is a no-op tactic that has no effect

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
  108. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  109. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  110. lazy val randomb: BuiltInPositionTactic

    randomb: [:*] simplify nondeterministic assignment [x:=*;]p(x) to a universal quantifier \forall x p(x)

  111. lazy val randomd: BuiltInPositionTactic

    randomd: <:*> simplify nondeterministic assignment <x:=*;>p(x) to an existential quantifier \exists x p(x)

  112. def seqCompose(first: ForwardTactic, second: ForwardTactic): ForwardTactic

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

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

    Definition Classes
    UnifyUSCalculus
  113. def seqComposeP(first: ForwardPositionTactic, second: ForwardPositionTactic): ForwardPositionTactic

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

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

    Definition Classes
    UnifyUSCalculus
  114. val skip: BuiltInTactic

    skip is a no-op tactic that has no effect Identical to nil but different name

    skip is a no-op tactic that has no effect Identical to nil but different name

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
    See also

    TactixLibrary.done

  115. def stepAt(axiomIndex: (Expression) ⇒ Option[DerivationInfo]): 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 AxIndex.

    Definition Classes
    UnifyUSCalculus
    Note

    Efficient source-level indexing implementation.

    See also

    AxIndex

    UnifyUSCalculus.chase

    HilbertCalculus.stepAt

  116. val stepAt: DependentPositionTactic

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

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

    Annotations
    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
    Note

    Efficient source-level indexing implementation.

    See also

    AxIndex

  117. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  118. lazy val testb: BuiltInPositionTactic

    testb: [?] simplifies test [?q;]p to an implication q->p

  119. lazy val testd: BuiltInPositionTactic

    testd: <?> simplifies test <?q;>p to a conjunction q&p

  120. def toString(): String
    Definition Classes
    AnyRef → Any
  121. val todo: BuiltInTactic

    A no-op tactic that as no effect but marks an open proof task.

    A no-op tactic that as no effect but marks an open proof task.

    Definition Classes
    UnifyUSCalculus
    Annotations
    @Tactic( macros.this.Tactic.<init>$default$1 , macros.this.Tactic.<init>$default$2 , macros.this.Tactic.<init>$default$3 , macros.this.Tactic.<init>$default$4 , macros.this.Tactic.<init>$default$5 , macros.this.Tactic.<init>$default$6 , macros.this.Tactic.<init>$default$7 , macros.this.Tactic.<init>$default$8 , macros.this.Tactic.<init>$default$9 , ... , ... , ... )
    See also

    skip,nil

  122. def uniformRename(ur: URename): BuiltInTactic

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

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

    Definition Classes
    UnifyUSCalculus
    See also

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

  123. def uniformRename(what: Variable, repl: Variable): BuiltInTactic

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

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

    Definition Classes
    UnifyUSCalculus
    See also

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

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

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

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

    Definition Classes
    UnifyUSCalculus
  125. def uniformSubstitute(subst: USubst): InputTactic

    Definition Classes
    UnifyUSCalculus
    See also

    US()

  126. def useAt(lem: Lemma): BuiltInPositionTactic

    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).

    Definition Classes
    UnifyUSCalculus
  127. def useAt(lem: Lemma, key: PosInExpr): BuiltInPositionTactic
    Definition Classes
    UnifyUSCalculus
  128. def useAt(lem: Lemma, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic

    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.

    inst

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

    Definition Classes
    UnifyUSCalculus
  129. def useAt(axiom: ProvableInfo, key: PosInExpr): BuiltInPositionTactic

    useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), overwriting key.

    useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), overwriting key.

    key

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

    Definition Classes
    UnifyUSCalculus
  130. def useAt(axiom: AxiomInfo, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic

    useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), with a given instantiation augmentation.

    useAt(axiom)(pos) uses the given (derived) axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence rewriting), with a given instantiation augmentation.

    inst

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

    Definition Classes
    UnifyUSCalculus
  131. def useAt(axiom: ProvableInfo, key: PosInExpr, inst: (Option[Subst]) ⇒ Subst): BuiltInPositionTactic

    useAt(axiom)(pos) uses the given axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence/implicational rewriting).

    useAt(axiom)(pos) uses the given axiom/axiomatic rule at the given position in the sequent (by unifying and equivalence/implicational rewriting). Unifies the left or right part of fact with what's found at sequent(pos) and use corresponding instance to make progress by reducing to the other side.

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

    and accordingly for implication facts that are l->r facts or conditional equivalences 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.

    Backward Tableaux-style proof analogue of useFor().

    Tactic specification:

    useAt(fact)(p)(F) = let (C,c)=F(p) in
      case c of {
        s=unify(fact.left,_) => CutRight(C(s(fact.right))(p) ; <(
          "use cut": skip
          "show cut": EquivifyRight(p.top) ; CoHide(p.top) ; CE(C(_)) ; fact
        )
        s=unify(fact.right,_) => accordingly with an extra commuteEquivRightT
      }
    axiom

    describing what fact to use to simplify at the indicated position of the sequent

    key

    the part of the Formula fact to unify the indicated position of the sequent with

    inst

    Transformation for instantiating additional unmatched symbols that do not occur in fact(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.

    Definition Classes
    UnifyUSCalculus
    Example:
    1. useAt(AxiomInfo("[;] choice", PosInExpr(0::Nil))(0, PosInExpr(1::1::Nil)) applied to the indicated 1::1::Nil position 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)

    To do

    could directly use prop rules instead of CE if key close to HereP if more efficient.

    See also

    useFor()

  132. def useAt(axiom: ProvableInfo): BuiltInPositionTactic

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

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

    Definition Classes
    UnifyUSCalculus
  133. def useExpansionAt(axiom: AxiomInfo): BuiltInPositionTactic

    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.

    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.

    Definition Classes
    UnifyUSCalculus
    See also

    useAt(AxiomInfo)

  134. 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 useAtImpl().

    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 useAtImpl().

      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.

    Definition Classes
    UnifyUSCalculus
    Example:
    1. useFor(Axiom.axiom(Ax.composeb), 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

    useAtImpl()

    edu.cmu.cs.ls.keymaerax.btactics

  135. def useFor(axiom: ProvableInfo, inst: (Subst) ⇒ Subst): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  136. def useFor(pi: ProvableInfo, key: PosInExpr, inst: (Subst) ⇒ Subst): ForwardPositionTactic

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

    useFor(pi, key) use the key part of the given axiom or provable info 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 AxiomInfo.theKey

    inst

    optional transformation augmenting or replacing the uniform substitutions after unification with additional information. Defaults to no change.

    Definition Classes
    UnifyUSCalculus
  137. def useFor(axiom: ProvableInfo, key: PosInExpr): ForwardPositionTactic
    Definition Classes
    UnifyUSCalculus
  138. def useFor(axiom: ProvableInfo): ForwardPositionTactic

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

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

    Definition Classes
    UnifyUSCalculus
  139. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  140. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  141. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @throws( ... )

Deprecated Value Members

  1. def by(fact: ⇒ ProvableSig, name: String = TacticFactory.ANON): BuiltInTactic

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

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

    fact

    the Provable to drop into the proof to proceed or close it if proved.

    name

    the name to use/record for the tactic

    Definition Classes
    UnifyUSCalculus
    Annotations
    @deprecated
    Deprecated

    use by(ProvableInfo) instead if possible.

Inherited from UnifyUSCalculus

Inherited from AnyRef

Inherited from Any

Ungrouped