Theory Invariants

theory Invariants
  imports Main "FactoredSystem"
begin

definition fdom :: "('a ⇒ 'b) ⇒ 'a set" where 
  "fdom f ≡ {x. ∃y. f x = y}"

― ‹TODO function domain for total function in Isabelle/HOL?›
― ‹TODO why is fm total? Shouldn't it be partial and thus needing the the premise `fm x = Some True` instead of just `fm x`?›
definition invariant :: "('a ⇒ bool) ⇒ bool" where
  "invariant fm ≡ (∀x. (x ∈ fdom fm ∧ fm x) ⟶ False) ∧ (∃x. x ∈ fdom fm ∧ fm x)"

end