Theory Fixed_Points

section ‹Fixed Points and Cantor's Theorems›

theory Fixed_Points
  imports Axiom_Of_Choice Pred_Logic Cardinality
begin

text ‹The definitions below correspond to Definition 2.6.12 in Halvorson.›
definition fixed_point :: "cfunc ⇒ cfunc ⇒ bool" where
  "fixed_point a g ⟷ (∃ A. g : A → A ∧ a ∈⇩c A ∧ g ∘⇩c a = a)"
definition has_fixed_point :: "cfunc ⇒ bool" where
  "has_fixed_point g ⟷ (∃ a. fixed_point a g)"
definition fixed_point_property :: "cset ⇒ bool" where
  "fixed_point_property A ⟷ (∀ g. g : A → A ⟶ has_fixed_point g)"

lemma fixed_point_def2: 
  assumes "g : A → A" "a ∈⇩c A"
  shows "fixed_point a g = (g ∘⇩c a = a)"
  unfolding fixed_point_def using assms by blast

text ‹The lemma below corresponds to Theorem 2.6.13 in Halvorson.›
lemma Lawveres_fixed_point_theorem:
  assumes p_type[type_rule]: "p : X → A⇗X⇖"
  assumes p_surj: "surjective p"
  shows "fixed_point_property A"
  unfolding fixed_point_property_def has_fixed_point_def
proof(clarify) 
  fix g 
  assume g_type[type_rule]: "g : A → A"
  obtain φ where φ_def: "φ = p⇧♭"
    by auto
  then have φ_type[type_rule]: "φ : X ×⇩c X → A"
    by (simp add: flat_type p_type)
  obtain f where f_def: "f = g ∘⇩c φ ∘⇩c diagonal(X)"
    by auto
  then have f_type[type_rule]:"f : X → A"
    using φ_type comp_type diagonal_type f_def g_type by blast
  obtain x_f where x_f: "metafunc f = p ∘⇩c x_f" and x_f_type[type_rule]: "x_f ∈⇩c X"
    using assms by (typecheck_cfuncs, metis p_surj surjective_def2)
  have "φ⇘[-,x_f]⇙ = f"
  proof(etcs_rule one_separator)
    fix x 
    assume x_type[type_rule]: "x ∈⇩c X"
    have "φ⇘[-,x_f]⇙ ∘⇩c x = φ ∘⇩c ⟨x, x_f⟩"
      by (typecheck_cfuncs, meson right_param_on_el x_f)
    also have "... = ((eval_func A X) ∘⇩c (id X ×⇩f p)) ∘⇩c ⟨x, x_f⟩"
      using assms φ_def inv_transpose_func_def3 by auto
    also have "... = (eval_func A X) ∘⇩c (id X ×⇩f p) ∘⇩c ⟨x, x_f⟩"
      by (typecheck_cfuncs, metis comp_associative2)
    also have "... = (eval_func A X) ∘⇩c ⟨id X  ∘⇩c  x, p ∘⇩c x_f⟩"
      using cfunc_cross_prod_comp_cfunc_prod x_f by (typecheck_cfuncs, force)
    also have "... = (eval_func A X) ∘⇩c ⟨x, metafunc f⟩"
      using id_left_unit2 x_f by (typecheck_cfuncs, auto)
    also have "... = f ∘⇩c x"
      by (simp add: eval_lemma f_type x_type)
    finally show "φ⇘[-,x_f]⇙ ∘⇩c x = f ∘⇩c x".
  qed
  then have "φ⇘[-,x_f]⇙ ∘⇩c x_f = g ∘⇩c φ ∘⇩c diagonal(X) ∘⇩c x_f"
    by (typecheck_cfuncs, smt (z3) cfunc_type_def comp_associative domain_comp f_def x_f)
  then have "φ ∘⇩c ⟨x_f, x_f⟩ = g ∘⇩c φ ∘⇩c ⟨x_f, x_f⟩"
    using  diag_on_elements right_param_on_el x_f by (typecheck_cfuncs, auto)
  then have "fixed_point (φ ∘⇩c ⟨x_f, x_f⟩) g"
    using fixed_point_def2 by (typecheck_cfuncs, auto)
  then show "∃a. fixed_point a g"
    using fixed_point_def by auto
qed

text ‹The theorem below corresponds to Theorem 2.6.14 in Halvorson.›
theorem Cantors_Negative_Theorem:
  "∄ s. s : X → 𝒫 X ∧ surjective s"
proof(rule ccontr, clarify)
  fix s 
  assume s_type: "s : X → 𝒫 X"
  assume s_surj: "surjective s"
  then have Omega_has_ffp: "fixed_point_property Ω"
    using Lawveres_fixed_point_theorem powerset_def s_type by auto
  have Omega_doesnt_have_ffp: "¬(fixed_point_property Ω)"
    unfolding fixed_point_property_def has_fixed_point_def fixed_point_def
  proof    
    assume BWOC: "∀g. g : Ω → Ω ⟶ (∃a A. g : A → A ∧ a ∈⇩c A ∧ g ∘⇩c a = a)"
    have  "NOT : Ω → Ω ∧ (∀a. ∀A. a ∈⇩c A ⟶ NOT : A → A ⟶ NOT ∘⇩c a ≠ a ∨ ¬ a ∈⇩c Ω)"
      by (typecheck_cfuncs, metis AND_complementary AND_idempotent OR_complementary OR_idempotent true_false_distinct)
    then have "∃g. g : Ω → Ω ∧ (∀a. ∀A. a ∈⇩c A ⟶ g : A → A ⟶ g ∘⇩c a ≠ a)"
      by (metis cfunc_type_def)
    then show False
      using BWOC by presburger
  qed
  show False
    using Omega_doesnt_have_ffp Omega_has_ffp by auto
qed

text ‹The theorem below corresponds to Exercise 2.6.15 in Halvorson.›
theorem Cantors_Positive_Theorem:
  "∃m. m : X → Ω⇗X⇖ ∧ injective m"
proof - 
  have eq_pred_sharp_type[type_rule]: "eq_pred X⇧♯ : X →  Ω⇗X⇖"
    by typecheck_cfuncs
  have "injective(eq_pred X⇧♯)"
    unfolding injective_def
  proof (clarify)
    fix x y 
    assume "x ∈⇩c domain (eq_pred X⇧♯)" then have x_type[type_rule]: "x ∈⇩c X"
      using cfunc_type_def eq_pred_sharp_type by auto
    assume "y ∈⇩c domain (eq_pred X⇧♯)" then have y_type[type_rule]:"y ∈⇩c X"
      using cfunc_type_def eq_pred_sharp_type by auto
    assume eq: "eq_pred X⇧♯ ∘⇩c x = eq_pred X⇧♯ ∘⇩c y"
    have "eq_pred X ∘⇩c ⟨x, x⟩ = eq_pred X ∘⇩c ⟨x, y⟩"
    proof - 
      have "eq_pred X ∘⇩c ⟨x, x⟩ = ((eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ) ∘⇩c ⟨x, x⟩"
        using transpose_func_def by (typecheck_cfuncs, presburger)
      also have "... = (eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ∘⇩c ⟨x, x⟩"
        by (typecheck_cfuncs, simp add: comp_associative2)
      also have "... = (eval_func Ω X) ∘⇩c ⟨id X ∘⇩c x, (eq_pred X⇧♯) ∘⇩c x⟩"
        using cfunc_cross_prod_comp_cfunc_prod by (typecheck_cfuncs, force)
      also have "... = (eval_func Ω X) ∘⇩c ⟨id X ∘⇩c x, (eq_pred X⇧♯) ∘⇩c y⟩"
        by (simp add: eq)
      also have "... = (eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ∘⇩c ⟨x, y⟩"
        by (typecheck_cfuncs, simp add: cfunc_cross_prod_comp_cfunc_prod)
      also have "... = ((eval_func Ω X) ∘⇩c (id X ×⇩f (eq_pred X⇧♯)) ) ∘⇩c ⟨x, y⟩"
        using comp_associative2 by (typecheck_cfuncs, blast)
      also have "... = eq_pred X ∘⇩c ⟨x, y⟩"
        using transpose_func_def by (typecheck_cfuncs, presburger)
      finally show ?thesis.
    qed
    then show "x = y"
      by (metis eq_pred_iff_eq x_type y_type)
  qed
  then show "∃m. m : X → Ω⇗X⇖ ∧ injective m"
    using eq_pred_sharp_type injective_imp_monomorphism by blast
qed

text ‹The corollary below corresponds to Corollary 2.6.16 in Halvorson.›
corollary 
  "X ≤⇩c 𝒫 X ∧ ¬ (X ≅ 𝒫 X)"
  using Cantors_Negative_Theorem Cantors_Positive_Theorem
  unfolding is_smaller_than_def is_isomorphic_def powerset_def
  by (metis epi_is_surj injective_imp_monomorphism iso_imp_epi_and_monic)

corollary Generalized_Cantors_Positive_Theorem:
  assumes "¬ terminal_object Y"
  assumes "¬ initial_object Y"
  shows "X  ≤⇩c Y⇗X⇖"
proof - 
  have "Ω ≤⇩c Y"
    by (simp add: assms non_init_non_ter_sets)
  then have fact: "Ω⇗X⇖ ≤⇩c  Y⇗X⇖"
    by (simp add: exp_preserves_card2)
  have "X ≤⇩c Ω⇗X⇖"
    by (meson Cantors_Positive_Theorem CollectI injective_imp_monomorphism is_smaller_than_def)
  then show ?thesis
    using fact set_card_transitive by blast
qed

corollary Generalized_Cantors_Negative_Theorem:
  assumes "¬ initial_object X"
  assumes "¬ terminal_object Y"
  shows "∄ s. s : X → Y⇗X⇖ ∧ surjective s"
proof(rule ccontr, clarify) 
  fix s 
  assume s_type: "s : X → Y⇗X⇖"
  assume s_surj: "surjective s"
  obtain m where m_type: "m : Y⇗X⇖ → X" and m_mono: "monomorphism(m)"
    by (meson epis_give_monos s_surj s_type surjective_is_epimorphism)
  have "nonempty X"
    using is_empty_def assms(1) iso_empty_initial no_el_iff_iso_empty nonempty_def by blast

  then have nonempty: "nonempty (Ω⇗X⇖)"
    using nonempty_def nonempty_to_nonempty true_func_type by blast
  show False
  proof(cases "initial_object Y")
    assume "initial_object Y"
    then have "Y⇗X⇖ ≅ ∅"
      by (simp add: ‹nonempty X› empty_to_nonempty initial_iso_empty no_el_iff_iso_empty)      
    then show False
      by (meson is_empty_def assms(1) comp_type iso_empty_initial no_el_iff_iso_empty s_type) 
  next
    assume "¬ initial_object Y"
    then have "Ω ≤⇩c Y"
      by (simp add: assms(2) non_init_non_ter_sets)
    then obtain n where n_type: "n : Ω⇗X⇖ → Y⇗X⇖" and n_mono: "monomorphism(n)"
      by (meson exp_preserves_card2 is_smaller_than_def)
    then have mn_type: "m ∘⇩c n :  Ω⇗X⇖ → X"
      by (meson comp_type m_type)
    have mn_mono: "monomorphism(m ∘⇩c n)"
      using cfunc_type_def composition_of_monic_pair_is_monic m_mono m_type n_mono n_type by presburger
    then have "∃g. g: X  → Ω⇗X⇖ ∧ epimorphism(g) ∧ g ∘⇩c (m ∘⇩c n) = id (Ω⇗X⇖)"
      by (simp add: mn_type monos_give_epis nonempty)
    then show False
      by (metis Cantors_Negative_Theorem epi_is_surj powerset_def)
  qed
qed

end