Rodin Proof Tactics: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older editNewer edit →
imported>Son
imported>Son
Line 430: Line 430:


== eq1 ==
== eq1 ==
== Double Implication Hypothesis ==
== cont Implication Hypothesis ==
== Functional Overriding in Goal ==
== Functional Overriding in Hypothesis ==
== Equality ==
== Modus Tollens ==
== Remove Membership in Hypothesis ==
== Remove Membership in Goal ==
== Remove Inclusion in Hypothesis ==
== Remove Inclusion in Goal ==
== Remove Strict-Inclusion in Hypothesis ==
== Remove Strict-Inclusion in Goal ==
== Inclusion Set Minus Right in Hypothesis ==
== Inclusion Set Minus Right in Goal ==
== Remove Inclusion Universal in Hypothesis ==
== Remove Inclusion Universal in Goal ==
== Implication Introduction ==
== Disjunction to Implication in Hypothesis ==
== Disjunction to Implication in Goal ==
== Forall Modus Ponens ==
== Next Pending Sub-goal ==
== Next Reviewed Sub-goal ==
== impAndHyp ==
== impAndGoal ==
== impOrHyp ==
== impOrGoal ==
== relImgUnionRight Hypothesis ==
== relImgUnionRight Goal ==
== relImgUnionLeft Hypothesis ==
== relImgUnionLeft Goal ==
== Set Equality in Hypothesis ==
== Set Equality in Goal ==
== Equivalent in Hypothesis ==
== Equivalent in Goal ==
== Functional Intersection Image in Hypothesis ==
== Functional Intersection Image in Goal ==
== Functional Set Minus Image in Hypothesis ==
== Functional Set Minus Image in Goal ==
== Functional Singleton Image in Hypothesis ==
== Functional Singleton Image in Goal ==

Revision as of 23:07, 6 March 2010

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.
  • Display: How an application of the tactic is displayed in the proof tree, the auto-tactic preference or the post-tactic preference.
  • 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.
  • 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. No here mean that there is no separate invocation for this specific tactic.
  • Example: 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
  • Display: ⊤ Goal
  • Auto-tactic: Default
  • Post-tactic: Default
  • Interactive: No
  • Example: TODO

False Hypothesis

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

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 Goal

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

Remove Negation in Goal

allE

exE

eq1

Double Implication Hypothesis

cont Implication Hypothesis

Functional Overriding in Goal

Functional Overriding in Hypothesis

Equality

Modus Tollens

Remove Membership in Hypothesis

Remove Membership in Goal

Remove Inclusion in Hypothesis

Remove Inclusion in Goal

Remove Strict-Inclusion in Hypothesis

Remove Strict-Inclusion in Goal

Inclusion Set Minus Right in Hypothesis

Inclusion Set Minus Right in Goal

Remove Inclusion Universal in Hypothesis

Remove Inclusion Universal in Goal

Implication Introduction

Disjunction to Implication in Hypothesis

Disjunction to Implication in Goal

Forall Modus Ponens

Next Pending Sub-goal

Next Reviewed Sub-goal

impAndHyp

impAndGoal

impOrHyp

impOrGoal

relImgUnionRight Hypothesis

relImgUnionRight Goal

relImgUnionLeft Hypothesis

relImgUnionLeft Goal

Set Equality in Hypothesis

Set Equality in Goal

Equivalent in Hypothesis

Equivalent in Goal

Functional Intersection Image in Hypothesis

Functional Intersection Image in Goal

Functional Set Minus Image in Hypothesis

Functional Set Minus Image in Goal

Functional Singleton Image in Hypothesis

Functional Singleton Image in Goal

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