AxiomSplit

Split a proof goal into multiple sub-goals, and justify the split through an explicit theory axiom. The action can specify a list of assumptions that are antecedents of the axiom, but already assumed to be present in a goal. Constants in the axiom will be replaced with universally quantified variables.

Linear Supertypes

Serializable, Serializable, Product, Equals, Action, AnyRef, Any

Instance Constructors

new AxiomSplit(assumptions: Seq[Formula], cases: Seq[(Conjunction, Seq[Action])], theory: Theory)

Value Members

final def !=(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def ##(): Int

Definition Classes
AnyRef → Any
final def ==(arg0: Any): Boolean

Definition Classes
AnyRef → Any
final def asInstanceOf[T0]: T0

Definition Classes
Any
val assumptions: Seq[Formula]
val cases: Seq[(Conjunction, Seq[Action])]
def clone(): AnyRef

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
final def eq(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def getClass(): Class[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
final def isInstanceOf[T0]: Boolean

Definition Classes
Any
final def ne(arg0: AnyRef): Boolean

Definition Classes
AnyRef
final def notify(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
final def synchronized[T0](arg0: ⇒ T0): T0

Definition Classes
AnyRef
val theory: Theory
final def wait(arg0: Long, arg1: Int): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Doc: package Plugin

case class AxiomSplit(assumptions: Seq[Formula], cases: Seq[(Conjunction, Seq[Action])], theory: Theory) extends Action with Product with Serializable

Instance Constructors

new AxiomSplit(assumptions: Seq[Formula], cases: Seq[(Conjunction, Seq[Action])], theory: Theory)

Value Members

final def !=(arg0: Any): Boolean

final def ##(): Int

final def ==(arg0: Any): Boolean

final def asInstanceOf[T0]: T0

val assumptions: Seq[Formula]

val cases: Seq[(Conjunction, Seq[Action])]

def clone(): AnyRef

final def eq(arg0: AnyRef): Boolean

final def getClass(): Class[_]

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

final def synchronized[T0](arg0: ⇒ T0): T0

val theory: Theory

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

Deprecated Value Members

def finalize(): Unit

Inherited from Serializable

Inherited from Serializable

Inherited from Product

Inherited from Equals

Inherited from Action

Inherited from AnyRef

Inherited from Any

Ungrouped