Theory Partial_Order_Reduction.Functions

section ‹Functions›

theory Functions
imports "../Extensions/Set_Extensions"
begin

  locale bounded_function =
    fixes A :: "'a set"
    fixes B :: "'b set"
    fixes f :: "'a  'b"
    assumes wellformed[intro?, simp]: "x  A  f x  B"

  locale bounded_function_pair =
    f: bounded_function A B f +
    g: bounded_function B A g
    for A :: "'a set"
    and B :: "'b set"
    and f :: "'a  'b"
    and g :: "'b  'a"

  locale injection = bounded_function_pair +
    assumes left_inverse[simp]: "x  A  g (f x) = x"
  begin

    lemma inj_on[intro]: "inj_on f A" using inj_onI left_inverse by metis

    lemma injective_on:
      assumes "x  A" "y  A" "f x = f y"
      shows "x = y"
      using assms left_inverse by metis

  end

  locale injective = bounded_function +
    assumes injection: " g. injection A B f g"
  begin

    definition "g  SOME g. injection A B f g"

    sublocale injection A B f g unfolding g_def using someI_ex[OF injection] by this

  end

  locale surjection = bounded_function_pair +
    assumes right_inverse[simp]: "y  B  f (g y) = y"
  begin

    lemma image_superset[intro]: "f ` A  B"
      using g.wellformed image_iff right_inverse subsetI by metis

    lemma image_eq[simp]: "f ` A = B" using image_superset by auto

  end

  locale surjective = bounded_function +
    assumes surjection: " g. surjection A B f g"
  begin

    definition "g  SOME g. surjection A B f g"

    sublocale surjection A B f g unfolding g_def using someI_ex[OF surjection] by this

  end

  locale bijection = injection + surjection

  lemma inj_on_bijection:
    assumes "inj_on f A"
    shows "bijection A (f ` A) f (inv_into A f)"
  proof
    show " x. x  A  f x  f ` A" using imageI by this
    show " y. y  f ` A  inv_into A f y  A" using inv_into_into by this
    show " x. x  A  inv_into A f (f x) = x" using inv_into_f_f assms by this
    show " y. y  f ` A  f (inv_into A f y) = y" using f_inv_into_f by this
  qed

end