Difference between revisions of "Rodin Proof Tactics"

From Event-B
Jump to navigationJump to search
imported>Son
imported>Son
Line 33: Line 33:
  
 
== False Hypothesis ==
 
== False Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Goal in Hypothesis ==
 
== Goal in Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Goal Disjunct in Hypothesis ==
 
== Goal Disjunct in Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Functional Goal ==
 
== Functional Goal ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Simplification Rewriter ==
 
== Simplification Rewriter ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Type Rewriter ==
 
== Type Rewriter ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Implication Goal ==
 
== Implication Goal ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== For-all Goal ==
 
== For-all Goal ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Exists Hypothesis ==
 
== Exists Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Find Contradictory Hypothesis ==
 
== Find Contradictory Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Use Equality Hypothesis ==
 
== Use Equality Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Shrink Implicative Hypothesis ==
 
== Shrink Implicative Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Shrink Enumerated Set ==
 
== Shrink Enumerated Set ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Implicative Hypothesis with Conjunctive RHS ==
 
== 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 ==
 
== Implicative Hypothesis with Disjunctive LHS ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Conjunctive Goal ==
 
== Conjunctive Goal ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Clarify Goal ==
 
== Clarify Goal ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Functional Overriding in Goal ==
 
== Functional Overriding in Goal ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Functional Overriding in Hypothesis ==
 
== Functional Overriding in Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== Partition Rewriter ==
 
== Partition Rewriter ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO
  
 
== One-Point Rule in Goal ==
 
== 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 ==
 
== 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 ==
 
== Bounded Goal with Finite Hypothesis ==
 +
* '''Description''': TODO
 +
 +
* '''ID''': TODO
 +
 +
* '''Display''': TODO
 +
 +
* '''Auto-tactic''': TODO
 +
 +
* '''Post-tactic''': TODO
 +
 +
* '''Interactive''': TODO
 +
 +
* '''Example''': TODO

Revision as of 22:38, 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
Retrieved from ‘https://wiki.event-b.org/index.php?title=Rodin_Proof_Tactics&oldid=8431’