Rodin Proof Tactics
From Event-B
Revision as of 11:04, 8 March 2010 by imported>Son (→True Goal)
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.
Contents
- 1 True Goal
- 2 False Hypothesis
- 3 Goal in Hypothesis
- 4 Goal Disjunct in Hypothesis
- 5 Functional Goal
- 6 Simplification Rewriter
- 7 Type Rewriter
- 8 Implication Goal
- 9 For-all Goal
- 10 Exists Hypothesis
- 11 Find Contradictory Hypothesis
- 12 Use Equality Hypothesis
- 13 Shrink Implicative Hypothesis
- 14 Shrink Enumerated Set
- 15 Implicative Hypothesis with Conjunctive RHS
- 16 Implicative Hypothesis with Disjunctive LHS
- 17 Conjunctive Goal
- 18 Clarify Goal
- 19 Functional Overriding in Goal
- 20 Functional Overriding in Hypothesis
- 21 Partition Rewriter
- 22 One-Point Rule in Goal
- 23 One-Point Rule in Hypothesis
- 24 Bounded Goal with Finite Hypothesis
- 25 Falsify Goal
- 26 conjI
- 27 allI
- 28 exI
- 29 Remove Negation
- 30 Review
- 31 Proof by cases
- 32 Add Hypothesis
- 33 Abstract Expression
- 34 Automatic Prover
- 35 Post tactic
- 36 Lasoo
- 37 Back Tracking
- 38 Prune
- 39 Search Hypothesis
- 40 Cache Hypothesis
- 41 Previous
- 42 Next
- 43 Information
- 44 Falsify Hypothesis
- 45 Modus Ponens
- 46 conjE
- 47 disjE
- 48 allE
- 49 exE
- 50 eq1
- 51 Double Implication Hypothesis
- 52 cont Implication Hypothesis
- 53 Functional Overriding
- 54 Equality
- 55 Modus Tollens
- 56 Remove Membership
- 57 Remove Inclusion
- 58 Remove Strict-Inclusion
- 59 Inclusion Set Minus Right
- 60 Remove Inclusion Universal
- 61 Implication Introduction
- 62 Disjunction to Implication
- 63 Forall Modus Ponens
- 64 Next Pending Sub-goal
- 65 Next Reviewed Sub-goal
- 66 impAndHyp
- 67 impAndGoal
- 68 impOrHyp
- 69 impOrGoal
- 70 relImgUnionRight
- 71 relImgUnionLeft
- 72 Set Equality
- 73 Equivalent
- 74 Functional Intersection Image
- 75 Functional Set Minus Image
- 76 Functional Singleton Image
- 77 Converse Relation
- 78 Domain Distribution to the Left
- 79 Domain Distribution to the Right
- 80 Range Distribution to the Left
- 81 Range Distribution to the Right
- 82 Set Minus
- 83 Conjunction and Disjunction Distribution
- 84 Union Conjunction Distribution
- 85 compUnionDist
- 86 Domain/Range Union Distribution
- 87 Relational Overriding
- 88 Composition Image
- 89 Domain Composition
- 90 Range Composition
- 91 Functional Composition Image
- 92 Finite Set in Goal
- 93 Finite Intersection in Goal
- 94 Finite Set Minus in Goal
- 95 Finite Relation in Goal
- 96 Finite Relation Image in Goal
- 97 Finite Domain in Goal
- 98 Finite Range in Goal
- 99 Finite Function in Goal
- 100 Finite Function Converse in Goal
- 101 Finite Functional Relational Image in Goal
- 102 Finite Functional Range in Goal
- 103 Finite Functional Domain in Goal
- 104 Finite Minimum in Goal
- 105 Finite Maximum in Goal
- 106 Finite Negative in Goal
- 107 Finite Positive in Goal
- 108 Cardinality Comparison in Goal
- 109 Cardinality Up to
- 110 Partition Rewrite
- 111 Arithmetic Rewrite
- 112 Total Domain in Hypothesis / Goal
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
- Proving interface 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