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  AX⇖"
  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 YX⇖"
proof - 
  have "Ω c Y"
    by (simp add: assms non_init_non_ter_sets)
  then have fact: "ΩXc  YX⇖"
    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  YX surjective s"
proof(rule ccontr, clarify) 
  fix s 
  assume s_type: "s : X  YX⇖"
  assume s_surj: "surjective s"
  obtain m where m_type: "m : YX 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 "YX "
      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 YX⇖" 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