Theory Invariants

theory Invariants
  imports Main "FactoredSystem"

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)"