Rodin Proof Tactics

From Event-B
Revision as of 11:01, 8 March 2010 by imported>Son (→‎False Hypothesis)
Jump to navigationJump to search

This page contains descriptions of the available proof tactics within the RODIN Platform.

For each tactic, the descriptions is as follows:

  • Description: A high-level description of the tactic
  • ID: An unique ID associated with the tactic.
  • Auto-tactic: No: the tactic cannot be added as an auto-tactic. Yes: the tactic can be added as an auto-tactic. Default: the tactic is a default auto-tactic.
  • Post-tactic: No: the tactic cannot be added as a post-tactic. Yes: the tactic can be added as a post-tactic. Default: the tactic is a default post-tactic.
  • Preference display: Information on how an application of the tactic is displayed in the auto-tactic preference or the post-tactic preference.
  • Interactive: No: the tactic cannot be invoked interactively. Global: The tactic can be invoked from the Proof Control. Goal: The tactic can be invoked from the goal view. Hypothesis: The tactic can be invoked from the hypothesis view. If the tactic can be invoked interactively (i.e. either Global, Goal or Hypothesis), more information about how this could be done will be given. Note that since the Post-tactics can be launched manually, any tactics that can be included in the post-tactic in principle can be invoked interactively via the post-tactic. Here No only means that there is no separate invocation for this specific tactic.
  • Proof-tree display: Example(s) on how the tactic can be seen from the RODIN Platform.

True Goal

  • Description: Discharges any sequent whose goal is '⊤' (logical true).
  • ID: org.eventb.core.seqprover.trueGoalTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: True Goal (Discharge)
  • Interactive: No
  • Proof-tree display: ⊤ goal

False Hypothesis

  • Description: Discharges any sequent containing a '⊥' hypothesis
  • ID: org.eventb.core.seqprover.falseHypTac
  • Auto-tactic: Default
  • Post-tactic: Default
  • Preference display: False Hypothesis (Discharge)
  • Interactive: No
  • Proving interface display: ⊥ hyp

Goal in Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Goal Disjunct in Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Functional Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Simplification Rewriter

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Type Rewriter

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Implication Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

For-all Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Exists Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Find Contradictory Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Use Equality Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Shrink Implicative Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Shrink Enumerated Set

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Implicative Hypothesis with Conjunctive RHS

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Implicative Hypothesis with Disjunctive LHS

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Conjunctive Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Clarify Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Functional Overriding in Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Functional Overriding in Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Partition Rewriter

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

One-Point Rule in Goal

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

One-Point Rule in Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Bounded Goal with Finite Hypothesis

  • Description: TODO
  • ID: TODO
  • Display: TODO
  • Auto-tactic: TODO
  • Post-tactic: TODO
  • Interactive: TODO
  • Example: TODO

Falsify Goal

conjI

allI

exI

Remove Negation

Review

Proof by cases

Add Hypothesis

Abstract Expression

Automatic Prover

Post tactic

Lasoo

Back Tracking

Prune

Search Hypothesis

Cache Hypothesis

Previous

Next

Information

Falsify Hypothesis

Modus Ponens

conjE

disjE

allE

exE

eq1

Double Implication Hypothesis

cont Implication Hypothesis

Functional Overriding

Equality

Modus Tollens

Remove Membership

Remove Inclusion

Remove Strict-Inclusion

Inclusion Set Minus Right

Remove Inclusion Universal

Implication Introduction

Disjunction to Implication

Forall Modus Ponens

Next Pending Sub-goal

Next Reviewed Sub-goal

impAndHyp

impAndGoal

impOrHyp

impOrGoal

relImgUnionRight

relImgUnionLeft

Set Equality

Equivalent

Functional Intersection Image

Functional Set Minus Image

Functional Singleton Image

Converse Relation

Domain Distribution to the Left

Domain Distribution to the Right

Range Distribution to the Left

Range Distribution to the Right

Set Minus

Conjunction and Disjunction Distribution

Union Conjunction Distribution

compUnionDist

Domain/Range Union Distribution

Relational Overriding

Composition Image

Domain Composition

Range Composition

Functional Composition Image

Finite Set in Goal

Finite Intersection in Goal

Finite Set Minus in Goal

Finite Relation in Goal

Finite Relation Image in Goal

Finite Domain in Goal

Finite Range in Goal

Finite Function in Goal

Finite Function Converse in Goal

Finite Functional Relational Image in Goal

Finite Functional Range in Goal

Finite Functional Domain in Goal

Finite Minimum in Goal

Finite Maximum in Goal

Finite Negative in Goal

Finite Positive in Goal

Cardinality Comparison in Goal

Cardinality Up to

Partition Rewrite

Arithmetic Rewrite

Total Domain in Hypothesis / Goal

Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Proof_Tactics&oldid=8444’