fmrisc.ProgramExplorer.Judgements

## Enum Simplification.Tag

• java.lang.Object
• All Implemented Interfaces:
java.io.Serializable, java.lang.Comparable<Simplification.Tag>
Enclosing class:
Simplification

```public static enum Simplification.Tag
extends java.lang.Enum<Simplification.Tag>```
The following simplifications are implemented: o Some "quasi-normalization": (A /\ B) /\ C to A /\ (B /\ C) (A \/ B) \/ C to A \/ (B \/ C) A imp (B imp C) to (A /\ B) imp C This simplifies pretty-printing and further processing. o Pulling negation inside ~~A to A ~(A /\ B) to ~A \/ ~B ~(A \/ B) to ~A /\ ~B ~(A imp B) to A /\ ~B ~(A equiv B) to A xor B ~(A xor B) to A equiv B ~(FORALL x: A) to EXISTS x: ~A ~(EXISTS x: A) to FORALL x: ~A ~(LET ... in A) to LET ... in ~A) ~(x=a) to x /= a, ~(x/=a) to x=a ~(x leq a) to x gt a, ~(x lt a) to x geq a ~(x leq a) to x lt a, ~(x gt a) to x leq a As a consequence, negation can appear only at the level of atomic predicates and IF-THEN-ELSE (for which there is no convenient simplification). o Removing superfluous quantifiers (Q x: A) to A, if x not free in A (let x=... in A) to A, if x not free in A (FORALL x: x=T imp A) to A[T/x], if x occurs at most once in A (EXISTS x: x=T /\ A) to A[T/x], if x occurs at most once in A (let x=T in A) to A[T/x], if x occurs at most once in A o Pulling quantifiers outside Conjunction and disjunction: (FORALL x: A) /\ B to (FORALL y: A[y/x] /\ B) y not free in A or B (if possible, choose y=x to avoid substitution) The same for \/ instead of /\. The same for EXISTS instead of FORALL. The same for both sides switched. Above rule is overridden by: (FORALL x: A) /\ (FORALL y: B) to (FORALL z: A[z/x] /\ B[z/x]) (EXISTS x: A) \/ (EXISTS y: B) to (EXISTS z: A[z/x] \/ B[z/x]) z not free in A or B (if possible, choose z in {x,y} to avoid one substitution) Implication: (FORALL x: A) imp B to (EXISTS y: A[y/x] imp B) (EXISTS x: A) imp B to (FORALL y: A[y/x] imp B) A imp (FORALL x: B) to (FORALL y: A imp B[y/x]) A imp (EXISTS x: B) to (EXISTS y: A imp B[y/x]) No convenient rules for equiv, XOR, IF. Future ideas (not yet implemented): o Sort defining (in)equalities in topological dependence order y = ..x.. /\ x = ... to x = ... /\ y = ..x..
• ### Enum Constant Summary

Enum Constants
Enum Constant and Description
`AND`
`ARRAYTERM`
`EQUALS`
`EXISTS`
`FORALL`
`GREATER`
`GREATEREQUAL`
`IMPLIES`
`LAMBDAFORMULA`
`LAMBDATERM`
`LESS`
`LESSEQUAL`
`NOTEQUALS`
`OR`
`SIMILAR`
• ### Method Summary

All Methods
Modifier and Type Method and Description
`static Simplification.Tag` `valueOf(java.lang.String name)`
Returns the enum constant of this type with the specified name.
`static Simplification.Tag[]` `values()`
Returns an array containing the constants of this enum type, in the order they are declared.
• ### Methods inherited from class java.lang.Enum

`compareTo, equals, getDeclaringClass, hashCode, name, ordinal, toString, valueOf`
• ### Methods inherited from class java.lang.Object

`getClass, notify, notifyAll, wait, wait, wait`
• ### Enum Constant Detail

• #### AND

`public static final Simplification.Tag AND`
• #### OR

`public static final Simplification.Tag OR`
• #### IMPLIES

`public static final Simplification.Tag IMPLIES`
• #### FORALL

`public static final Simplification.Tag FORALL`
• #### EXISTS

`public static final Simplification.Tag EXISTS`
• #### ARRAYTERM

`public static final Simplification.Tag ARRAYTERM`
• #### LAMBDATERM

`public static final Simplification.Tag LAMBDATERM`
• #### LAMBDAFORMULA

`public static final Simplification.Tag LAMBDAFORMULA`
• #### EQUALS

`public static final Simplification.Tag EQUALS`
• #### NOTEQUALS

`public static final Simplification.Tag NOTEQUALS`
• #### LESS

`public static final Simplification.Tag LESS`
• #### LESSEQUAL

`public static final Simplification.Tag LESSEQUAL`
• #### GREATER

`public static final Simplification.Tag GREATER`
• #### GREATEREQUAL

`public static final Simplification.Tag GREATEREQUAL`
• #### SIMILAR

`public static final Simplification.Tag SIMILAR`
• ### Method Detail

• #### values

`public static Simplification.Tag[] values()`
Returns an array containing the constants of this enum type, in the order they are declared. This method may be used to iterate over the constants as follows:
```for (Simplification.Tag c : Simplification.Tag.values())
System.out.println(c);
```
Returns:
an array containing the constants of this enum type, in the order they are declared
• #### valueOf

`public static Simplification.Tag valueOf(java.lang.String name)`
Returns the enum constant of this type with the specified name. The string must match exactly an identifier used to declare an enum constant in this type. (Extraneous whitespace characters are not permitted.)
Parameters:
`name` - the name of the enum constant to be returned.
Returns:
the enum constant with the specified name
Throws:
`java.lang.IllegalArgumentException` - if this enum type has no constant with the specified name
`java.lang.NullPointerException` - if the argument is null