Rodin Proof Tactics - Revision history

imported>Nicolas: added todo success failure

2012-02-21T17:25:00Z

added todo success failure

← Older revision		Revision as of 17:25, 21 February 2012
Line 18:		Line 18:

	* '''Proving interface display''': Example(s) on how applications of this tactic can be seen from the [[The Proving Perspective (Rodin User Manual)\|proving interface]] of the RODIN Platform.		* '''Proving interface display''': Example(s) on how applications of this tactic can be seen from the [[The Proving Perspective (Rodin User Manual)\|proving interface]] of the RODIN Platform.

			{{TODO\|add conditions of success/failure}}

	== True Goal ==		== True Goal ==

imported>Nicolas: /* allI */

2011-02-18T16:53:59Z

allI

← Older revision		Revision as of 16:53, 18 February 2011
Line 722:		Line 722:
	== allI ==		== allI ==

	* '''Description''':		* '''Description''': Simplifies any sequent with a universally quantified goal by freeing all its bound variables.

	* '''Additional details''':		* '''Additional details''':

	{{InfRule\|\| <math></math> }}		{{InfRule\|ALL_R\| <math>\frac{\textbf{H}\; \; \vdash \; \; \textbf{P(x)} }{ \textbf{H} \; \; \vdash \; \; \forall \textbf{x}\, \qdot\, \textbf{P(x)} }</math> }}

	* '''ID''':		* '''ID''': org.eventb.core.seqprover.forallGoalTac

	* '''Auto-tactic''':		* '''Auto-tactic''': ''No''

	* '''Post-tactic''':		* '''Post-tactic''': ''Yes''

	* '''Preference Display''':		* '''Preference Display''': For-all Goal (Simplify)

	* '''Interactive''':		* '''Interactive''': ''Goal''

	* '''Proving Interface Display''':		* '''Proving Interface Display''': ''Forall instantiation''

	Before [[Image: allIBefore.png]]		Before [[Image: allIBefore.png]]

imported>Nicolas: prepared image names

2011-02-18T16:04:48Z

prepared image names

Show changes

imported>Nicolas: prepared for rules everywhere

2011-02-18T15:47:23Z

prepared for rules everywhere

Show changes

imported>Nicolas at 15:41, 18 February 2011

2011-02-18T15:41:45Z

← Older revision		Revision as of 15:41, 18 February 2011
Line 725:		Line 725:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 747:		Line 749:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 769:		Line 773:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 791:		Line 797:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 813:		Line 821:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 835:		Line 845:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 857:		Line 869:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 879:		Line 893:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 901:		Line 917:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 923:		Line 941:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 945:		Line 965:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 967:		Line 989:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 989:		Line 1,013:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 1,011:		Line 1,037:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 1,033:		Line 1,061:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 1,055:		Line 1,085:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 1,077:		Line 1,109:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 1,099:		Line 1,133:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':
Line 1,121:		Line 1,157:

	* '''Additional details''':		* '''Additional details''':

			{{InfRule\|\| <math></math> }}

	* '''ID''':		* '''ID''':

imported>Nicolas: /* conjI */

2011-02-18T15:30:23Z

conjI

← Older revision		Revision as of 15:30, 18 February 2011
Line 716:		Line 716:
	* '''Proving Interface Display''': "Conjunction introduction" for manual application, "''<math>\land</math> goal''" in proof tree		* '''Proving Interface Display''': "Conjunction introduction" for manual application, "''<math>\land</math> goal''" in proof tree

	Before [[Image: ]]		Before [[Image: conjIBefore.png]]

	After [[Image: ]]		After [[Image: conjIAfter.png]]

	== allI ==		== allI ==

imported>Nicolas: /* conjI */

2011-02-18T15:29:06Z

conjI

← Older revision		Revision as of 15:29, 18 February 2011
Line 702:		Line 702:
	* '''Additional details''':		* '''Additional details''':

	AND_R <math>\frac{\textbf{H} \; \; \vdash \; \; \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \; \textbf{P} \; \land \; \textbf{Q}}</math>		{{InfRule\|AND_R\| <math>\frac{\textbf{H} \; \; \vdash \; \; \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \; \textbf{P} \; \land \; \textbf{Q}}</math> }}

	* '''ID''': org.eventb.core.seqprover.impI		* '''ID''': org.eventb.core.seqprover.impI

imported>Nicolas: /* conjI */

2011-02-18T15:27:09Z

conjI

← Older revision		Revision as of 15:27, 18 February 2011
Line 698:		Line 698:
	== conjI ==		== conjI ==

	* '''Description''':		* '''Description''': Splits a sequent with a conjunctive goal into multiple subgoals.

	* '''Additional details''':		* '''Additional details''':

	* '''ID''':		AND_R <math>\frac{\textbf{H} \; \; \vdash \; \; \textbf{P} \qquad \textbf{H} \; \; \vdash \; \; \textbf{Q}}{\textbf{H} \; \; \vdash \; \; \textbf{P} \; \land \; \textbf{Q}}</math>

	* '''~~Auto-tactic~~''':		* '''ID''': org.eventb.core.seqprover.impI

	* '''~~Post~~-tactic''':		* '''Auto-tactic''': ''No''

	* '''~~Preference Display~~''':		* '''Post-tactic''': ''Yes''

	* '''~~Interactive~~''':		* '''Preference Display''': Conjunctive Goal (Split)

	* '''Proving Interface Display''':		* '''Interactive''': ''No''

			* '''Proving Interface Display''': "Conjunction introduction" for manual application, "''<math>\land</math> goal''" in proof tree

	Before [[Image: ]]		Before [[Image: ]]

imported>Nicolas: /* Falsify Hypothesis */

2011-02-18T14:56:18Z

Falsify Hypothesis

← Older revision		Revision as of 14:56, 18 February 2011
Line 693:		Line 693:

	After [[Image: ctHypAfter.png]]		After [[Image: ctHypAfter.png]]

			''ct'' has been applied to hypothesis ''card(S)=1''.

	== conjI ==		== conjI ==

imported>Nicolas at 14:28, 18 February 2011

2011-02-18T14:28:35Z

@@ Line 671: / Line 671: @@
 After [[Image: ctGoalAfter.png]]
 == conjI ==
@@ Line 1,047: / Line 1,069: @@
 == Information ==
 * '''Description''':