Theory PartComp

Up to index of Isabelle/HOL/Marvin2002

PartComp = Fun + Map +

consts
  partcomp :: "('a ~=> 'b) => ('b ~=> 'c) => ('a ~=> 'c)" (infixl "o;" 100)

defs
  partcomp_def "f o; g == (%x. if x: dom(f) then g(the (f x)) else None)"

end

theorem dom_partcomp:

  dom (f o; g) = {x. x : dom f & the (f x) : dom g}

theorem dom_partcomp_subs:

  dom (f o; g) <= dom f