jml2b.pog.lemma
Interface ILemma

All Known Implementing Classes:

Goal, Lemma

public interface ILemma

This interface defines the different operations that are performed on lemma or on goal.

Author:

L. Burdy

Method Summary

void	garbageIdent() Annotates all the fields that appear in the lemma to declare them in the Atelier B files.
void	oldParam(java.util.Vector e) Adds a old param around the element of the enumeration corresponding to the parameter of the method.
boolean	proveObvious(java.util.Vector hyp, boolean atTheEnd) Supress in the lemma the obvious goals.
void	sub(Substitution s) Apply a substitution to the lemma.
void	suppressSpecialOld(int token) Suppress the Called Old expressions.

Method Detail

proveObvious

public boolean proveObvious(java.util.Vector hyp,
                            boolean atTheEnd)

Supress in the lemma the obvious goals.

Returns:

true if the lemma contains only obvious goals, false otherwise.

See Also:

Proofs.proveObvious(boolean, boolean)

oldParam

public void oldParam(java.util.Vector e)

Adds a old param around the element of the enumeration corresponding to the parameter of the method.

Parameters:

e - fields enumeration

See Also:

Theorem#oldParam(Enumeration)

sub

public void sub(Substitution s)

Apply a substitution to the lemma.

Parameters:

s - substitution to apply.

See Also:

Proofs.sub(Substitution)

suppressSpecialOld

public void suppressSpecialOld(int token)

Suppress the Called Old expressions.

See Also:

Theorem#suppressCalledOld()

garbageIdent

public void garbageIdent()

Annotates all the fields that appear in the lemma to declare them in the Atelier B files.

See Also:

Theorem#garbageIdent()