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