Laws for shared IEEE exception flags

These results quantify over every flag state and selected group. They are independent of number format, numerical value, rounding direction, and runtime storage.

theorem FloatLib.Numerics.IEEEStatus.ext_isSet {left right : IEEEStatus} (h : ∀ (exception : IEEEException), left.isSet exception = right.isSet exception) : left = right

Two flag states are equal when every exception has the same state.

theorem FloatLib.Numerics.IEEEStatus.ext_isSet_iff {left right : IEEEStatus} : left = right ↔ ∀ (exception : IEEEException), left.isSet exception = right.isSet exception

@[simp]

theorem FloatLib.Numerics.IEEEStatus.isSet_ofPredicate (selected : IEEEException → Bool) (exception : IEEEException) : (ofPredicate selected).isSet exception = selected exception

Constructing a flag group preserves its membership predicate.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.isSet_empty (exception : IEEEException) : { }.isSet exception = false

The default flag state has no exceptions raised.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.isSet_singleton (selected exception : IEEEException) : (singleton selected).isSet exception = decide (exception = selected)

A singleton selects precisely its named exception.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.isSet_allFlags (exception : IEEEException) : allFlags.isSet exception = true

The all-flags group selects every exception.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.isSet_union (left right : IEEEStatus) (exception : IEEEException) : (left.union right).isSet exception = (left.isSet exception || right.isSet exception)

A flag in a union is raised exactly when either input raises it.

theorem FloatLib.Numerics.IEEEStatus.union_assoc (first second third : IEEEStatus) : (first.union second).union third = first.union (second.union third)

Accumulating exceptions is associative, so operation grouping does not affect flags.

theorem FloatLib.Numerics.IEEEStatus.union_comm (left right : IEEEStatus) : left.union right = right.union left

Flag accumulation is independent of the order in which the same exceptions are raised.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.union_self (flags : IEEEStatus) : flags.union flags = flags

Raising an already raised flag changes nothing.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.union_empty (flags : IEEEStatus) : flags.union { } = flags

An operation with no exceptions preserves the accumulated flags.

theorem FloatLib.Numerics.IEEEStatus.isSet_union_of_left (left right : IEEEStatus) (exception : IEEEException) (h : left.isSet exception = true) : (left.union right).isSet exception = true

Existing flags remain raised when another operation contributes exceptions.

theorem FloatLib.Numerics.IEEEStatus.isSet_union_of_right (left right : IEEEStatus) (exception : IEEEException) (h : right.isSet exception = true) : (left.union right).isSet exception = true

A newly raised exception appears in the accumulated state.

theorem FloatLib.Numerics.IEEEStatus.isSet_raiseFlags (flags group : IEEEStatus) (exception : IEEEException) : (flags.raiseFlags group).isSet exception = (flags.isSet exception || group.isSet exception)

Raising a group affects exactly its members.

theorem FloatLib.Numerics.IEEEStatus.isSet_lowerFlags (flags group : IEEEStatus) (exception : IEEEException) : (flags.lowerFlags group).isSet exception = (flags.isSet exception && !group.isSet exception)

Clearing a group removes precisely the selected flags.

theorem FloatLib.Numerics.IEEEStatus.testFlags_iff (flags group : IEEEStatus) : flags.testFlags group = true ↔ ∃ (exception : IEEEException), flags.isSet exception = true ∧ group.isSet exception = true

Testing a group succeeds exactly when it contains a raised exception.

theorem FloatLib.Numerics.IEEEStatus.testSavedFlags_iff (saved group : IEEEStatus) : saved.testSavedFlags group = true ↔ ∃ (exception : IEEEException), saved.isSet exception = true ∧ group.isSet exception = true

A saved-state test has the same existential meaning as a current-state test.

theorem FloatLib.Numerics.IEEEStatus.isSet_restoreFlags (flags saved group : IEEEStatus) (exception : IEEEException) : (flags.restoreFlags saved group).isSet exception = if group.isSet exception = true then saved.isSet exception else flags.isSet exception

Restoration chooses saved state inside the group and current state outside it.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.lowerFlags_allFlags (flags : IEEEStatus) : flags.lowerFlags allFlags = { }

Clearing all exceptions resets the state.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.restoreFlags_allFlags (flags saved : IEEEStatus) : flags.restoreFlags saved.saveAllFlags allFlags = saved

Restoring the complete saved group recovers the snapshot exactly.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.testFlags_empty (flags : IEEEStatus) : flags.testFlags { } = false

An empty selection never reports an exception.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.lowerFlags_empty (flags : IEEEStatus) : flags.lowerFlags { } = flags

An empty selection leaves all flags unchanged when clearing.

@[simp]

theorem FloatLib.Numerics.IEEEStatus.restoreFlags_empty (flags saved : IEEEStatus) : flags.restoreFlags saved { } = flags

An empty selection leaves all flags unchanged when restoring.