Theory Reduction

theory Reduction

imports 
  Main
begin 

section ‹Reduction Function›
text ‹This definition was taken from the developements at 
  \url{https://github.com/wimmers/poly-reductions}
  ``Karp21/Reductions.thy''.
  TODO: When this repo comes into the AFP, link to original definition.›
definition is_reduction :: "('a ⇒ 'b) ⇒ 'a set ⇒ 'b set ⇒ bool" where
  "is_reduction f A B ≡ ∀a. a ∈ A ⟷ f a ∈ B "
end