Theory Pointwise

Up to index of Isabelle/HOL/Marvin2002

Pointwise = Marvin_lemmas +

consts
  PInt :: "('a set ~=> 'a set) => ('a set  ~=> 'a set)
           => ('a set ~=> 'a set )" (infixl 120)
  PUn  :: "('a set ~=> 'a set) => ('a set  ~=> 'a set)
           => ('a set ~=> 'a set )" (infixl 110)

defs
  PInt_def "f PInt g == %x. if (x: dom(f) Int dom(g))
            then (Some ((the (f x)) Int (the (g x))))
            else None"

  PUn_def "f PUn g == %x. if (x: dom(f) Int dom(g))
           then (Some ((the (f x)) Un (the (g x))))
           else None"
end

theorem PInt_empty:

  m PInt empty = empty

theorem dom_PInt:

  dom (m PInt n) = dom n Int dom m

theorem PInt_commute:

  f PInt g = g PInt f

theorem PUn_commute:

  f PUn g = g PUn f

theorem dom_PUn:

  dom (m PUn n) = dom n Int dom m

theorem PInt_assoc:

  f PInt g PInt h = f PInt (g PInt h)

theorem PUn_assoc:

  f PUn g PUn h = f PUn (g PUn h)

theorem distrib_PInt_PUn:

  f PInt (g PUn h) = f PInt g PUn f PInt h

theorem distrib_PUn_PInt:

  f PUn g PInt h = (f PUn g) PInt (f PUn h)

theorem ran_PInt:

  [| ran f <= Pow A; ran g <= Pow A |] ==> ran (f PInt g) <= Pow A

theorem PInt_apply:

  [| x : dom f; x : dom g |] ==> (f PInt g) x = Some (the (f x) Int the (g x))