| | | B.5.1 flatten: Flatten Propositional Formulas |
flatten
In proving mode.
The command generates a single child state by flattening every suitable propositional formula (assumption or goal) of the current proof state according to the rules listed below. For every formula of the current state, the command looks for an applicable rule (there can be at most one) and, if such a rule exists, applies it to the state; i.e. a rule is applied at most once for every formula (for a repeated application of the rules, see the command decompose). If no rule is applicable at all, no child state is generated.
The applied rules are:
[E] ..., neg(A), ... |- ...
---------------------------
[E] ..., ~A, ... |- ...
[E] ... |- ..., neg(A), ...
---------------------------
[E] ... |- ..., ~A, ...
[E] ..., A, B, ... |- ...
---------------------------
[E] ..., A /\ B, ... |- ...
[E] ... |- ..., A, B, ...
---------------------------
[E] ... |- ..., A \/ B, ...
[E] ..., A |- ..., B, ...
---------------------------
[E] ... |- ..., A => B, ...
[E] ... |- ..., (A=> B) /\ (B => A), ...
----------------------------------------
[E] ... |- ..., A <=> B, ...
[E] ..., (A=> B) /\ (B => A), ... |- ...
----------------------------------------
[E] ..., A <=> B, ... |- ...
[E] ... |- ..., (A => ~B) /\ (B => ~A), ...
-------------------------------------------
[E] ... |- ..., A xor B, ...
[E] ..., (A=> ~B) /\ (B => ~A), ... |- ...
------------------------------------------
[E] ..., A xor B, ... |- ...
An application neg(A) yields a formula which is logically equivalent to A but where negation only occurs at the level of atomic formulas. The operator neg is recursively defined on the syntactic structure of its argument as follows:
neg(~A) := A neg(A /\ B) := neg(A) \/ neg(B) neg(A \/ B) := neg(A) /\ neg(B) neg(A => B) := A /\ neg(B) neg(A <=> B) := A xor B neg(A xor B) := A <=> B neg(let ... in A) := let ... in neg(A) neg(/\ x in T: A) := \/ x in T: neg(A) neg(\/ x \in T: A) := /\ x \in T: neg(A) neg(a = b) := a /= b neg(a /= b) := a = b neg(A) := ~A, for every other A
The effect of this command is subsumed by the effect of the command decompose. The only reason to apply flatten directly is to observe step-by-step how decompose produces its result.
| | | B.5.1 flatten: Flatten Propositional Formulas |