Theory Involutions2Squares

theory Involutions2Squares
imports Main
begin


section ‹A few basic properties›

lemma nat_sqr : 
  shows "nat(n⇧2) = (nat(abs n))⇧2"
  by(rule int_int_eq[THEN iffD1], simp)


lemma nat_mod_int : 
  assumes "n mod m = k" 
  shows "int n mod int m = int k"
  by (metis assms of_nat_mod)


lemma sqr_geq_nat : 
  shows "(n::nat) ≤ n⇧2"
  using power2_nat_le_imp_le by simp


lemma sqr_geq_abs : 
  shows "abs(n::int) ≤ n⇧2"
proof(rule nat_le_eq_zle[THEN iffD1], simp)
  show "nat ¦n¦ ≤ nat (n⇧2)"
    using nat_sqr sqr_geq_nat by presburger
qed


lemma sqr_fix_nat :
  assumes "(n::nat) = n⇧2"
  shows "n = 0 ∨ n = 1"
  using assms numeral_2_eq_2 by fastforce


lemma card1 :
  shows "(card{a, b} = Suc 0) = (a = b)"
  using singleton_insert_inj_eq' by fastforce

lemma card2 :
  shows "card{a, b} ≥ Suc 0 ∧ card{a, b} ≤ 2"
  by (simp add: card_insert_if) 




section ‹The relevant properties of involutions›

definition "involution_on A φ = (φ ` A ⊆ A ∧ (∀x∈A. φ(φ x) = x))"


lemma involution_bij :
  assumes "involution_on A φ"
  shows "bij_betw φ A A"
  using assms bij_betw_byWitness involution_on_def by fast


lemma involution_sub_bij :
  assumes "involution_on A φ" 
      and "S ⊆ A" 
      and "∀x∈A. (x ∈ S) = (φ x ∉ S)"
 shows "bij_betw φ S (A - S)"
proof(simp add: bij_betw_def, rule conjI)
  show "inj_on φ S"
    by (meson assms bij_betw_def inj_on_subset involution_bij) 
next
  show "φ ` S = A - S"
  proof(rule set_eqI, clarsimp)
    fix x show "(x ∈ φ ` S) = (x ∈ A ∧ x ∉ S)" (is "?L = ?R")
    proof
      assume ?L thus ?R
        by(metis assms bij_betw_imp_surj_on f_inv_into_f image_eqI inv_into_into involution_bij subset_iff)
    next
      assume ?R thus ?L
        by (metis assms(1) assms(3) image_iff involution_on_def)  
    qed
  qed
qed



lemma involution_sub_card :
  assumes "involution_on A φ"
      and "finite A"
      and "S ⊆ A" 
      and "∀x∈A. (x ∈ S) = (φ x ∉ S)"
    shows "2 * card S = card A"
proof -
  have "card S = card (A - S)"
    using assms bij_betw_same_card involution_sub_bij by blast

  also have "... = card A - card S"
    by (meson assms card_Diff_subset rev_finite_subset)

  finally show ?thesis by simp
qed




subsection ‹Unions of preimage/image sets, fixed points›

definition "preimg_img_on A φ = (⋃x∈A. {{x, φ x}})"
definition "fixpoints_on A φ = {x∈A. φ x = x}"


lemma preimg_img_on_Union :
  assumes "φ ` A ⊆ A"
  shows "A = ⋃(preimg_img_on A φ)"
  using assms by(fastforce simp: preimg_img_on_def) 

lemma preimg_img_on_finite :
  assumes "finite A"
  shows "finite (preimg_img_on A φ)"
  by(simp add: assms preimg_img_on_def)

lemma fixpoints_on_finite :
  assumes "finite A"
  shows "finite (fixpoints_on A φ)"
  by(simp add: assms fixpoints_on_def)

lemma preimg_img_on_card :
  assumes "x ∈ preimg_img_on A φ"
  shows "1 ≤ card x ∧ card x ≤ 2"
  using assms by(fastforce simp: preimg_img_on_def card2)



corollary preimg_img_on_eq :
  shows "preimg_img_on A φ = {x ∈ preimg_img_on A φ. card x = 1} ∪ 
                              {x ∈ preimg_img_on A φ. card x = 2}"
proof(rule equalityI[rotated 1], clarsimp+)
  fix x assume "card x ≠ 2" and "x ∈ preimg_img_on A φ"
  thus "card x = Suc 0"
    using preimg_img_on_card by fastforce
qed


lemma fixpoints_on_card_eq :
  shows "card(fixpoints_on A φ) = card {x ∈ preimg_img_on A φ. card x = 1}"
proof -
  have "bij_betw (λx. {x}) (fixpoints_on A φ) 
                           {x. x ∈ preimg_img_on A φ ∧ card x = 1}"
    by(fastforce simp: bij_betw_def fixpoints_on_def preimg_img_on_def card1)
  thus ?thesis by(rule bij_betw_same_card)
qed


lemma preimg_img_on_disjoint :
  assumes "involution_on A φ"
  shows "pairwise disjnt (preimg_img_on A φ)"
proof(clarsimp simp: pairwise_def disjnt_def preimg_img_on_def)
  fix u v assume b: "u ∈ A" and c: "v ∈ A" and d: "{u, φ u} ≠ {v, φ v}"
  hence e: "u ≠ v" by clarsimp
  with b and c have f: "φ u ≠ φ v" by (metis assms involution_on_def) 
  have "(φ v = u) = (v = φ u)" by (metis assms b c involution_on_def) 
  with d have "φ v ≠ u ∧ v ≠ φ u" by fastforce 
  with e and f show "v ≠ u ∧ v ≠ φ u ∧ φ v ≠ u ∧ φ v ≠ φ u" by simp
qed



theorem involution_dom_card_sum :
  assumes "involution_on A φ"
      and "finite A"
    shows "card A = card (fixpoints_on A φ) + 
                    2 * card {x ∈ preimg_img_on A φ. card x = 2}" 
proof -
  have eq: "{x ∈ preimg_img_on A φ. card x = Suc 0} ∩ 
           {x ∈ preimg_img_on A φ. card x = 2} = {}"
    by fastforce

  have f1 : "finite {x ∈ preimg_img_on A φ. card x = 1}"
    by (simp add: assms preimg_img_on_finite)
  have f2 : "finite {x ∈ preimg_img_on A φ. card x = 2}"
    by (simp add: assms preimg_img_on_finite)

  have "card A = card (⋃(preimg_img_on A φ))"
    by (metis assms(1) involution_on_def preimg_img_on_Union) 

  also have "... = sum card (preimg_img_on A φ)"
    by (metis assms(1) card_Union_disjoint card_eq_0_iff not_one_le_zero preimg_img_on_card 
        preimg_img_on_disjoint)

  also have "... = sum card ({x ∈ preimg_img_on A φ. card x = 1} ∪ 
                             {x ∈ preimg_img_on A φ. card x = 2})"
    by (metis preimg_img_on_eq)

  also have "... = sum card {x ∈ preimg_img_on A φ. card x = 1} + 
                   sum card {x ∈ preimg_img_on A φ. card x = 2}"
    by (metis (no_types, lifting) Collect_cong One_nat_def eq f1 f2 sum.union_disjoint)

  also have "... = card (fixpoints_on A φ) + 
                   2 * card {x ∈ preimg_img_on A φ. card x = 2}"
    by(simp add: fixpoints_on_card_eq)

  finally show ?thesis .
qed


corollary involution_dom_fixpoints_parity :
  assumes "involution_on A φ" 
      and "finite A"
 shows "odd(card A) = odd(card(fixpoints_on A φ))"
  using assms involution_dom_card_sum by fastforce




section ‹Primes and the two squares theorem›

definition "is_prime (n :: nat) = (n > 1 ∧ (∀d. d dvd n ⟶ d = 1 ∨ d = n))"

lemma prime_factors :
  assumes "is_prime p"
      and "p = n * m" 
    shows "(n = 1 ∧ m = p) ∨ (n = p ∧ m = 1)"
using assms proof(clarsimp simp: is_prime_def)
  assume "∀d. d dvd n * m ⟶ d = Suc 0 ∨ d = n * m"
  hence a: "n = Suc 0 ∨ n = n * m ∧ m = Suc 0 ∨ m = n * m"
    by (meson dvd_triv_left dvd_triv_right)
  assume "0 < n ∧ Suc 0 ≠ m ∨ m ≠ Suc 0" and "Suc 0 < n*m"
  with a show "n = Suc 0 ∧ (m = 0 ∨ Suc 0 = n)" by fastforce
qed

lemma prime_not_sqr : 
  assumes "is_prime p"
  shows "p ≠ n⇧2"
  by (metis assms is_prime_def order_less_irrefl power2_eq_square prime_factors)

lemma int_prime_not_sqr : 
  assumes "is_prime p"
  shows "int p ≠ n⇧2"
  by (metis assms nat_int nat_sqr prime_not_sqr)

lemma prime_gr4 :
  assumes "is_prime p"
      and "p mod 4 = 1"
    shows "p > 4"
proof(rule ccontr, drule leI)
  assume "p ≤ 4"
  thus False
    by (metis assms dvd_imp_mod_0 dvd_triv_left is_prime_def mod_less mult.right_neutral 
        order_less_le zero_neq_one) 
qed




theorem two_squares :
  assumes a: "is_prime p" 
      and b: "p mod 4 = 1"
    shows "∃n m. p = n⇧2 + m⇧2"
proof -
  let ?S  =  "{(u, v, w). int p = 4 * u * v + w⇧2 ∧ u > 0 ∧ v > 0}"
  let ?T  =  "?S ∩ {(u, v, w). w > 0}"
  let ?U  =  "?S ∩ {(u, v, w). u - v + w > 0}"
  let ?f  =  "λ(u, v, w). (v, u, -w)"
  let ?g  =  "λ(u, v, w). (u - v + w, v, 2 * v - w)"
  let ?h  =  "λ(u, v, w). (v, u, w)"

  have w_neq0 : "∀u v w. (u, v, w) ∈ ?S ⟶ w ≠ 0" 
  proof clarsimp
    fix u v assume "int p = 4 * u * v" 
    hence "4 dvd int p" by simp
    hence "4 dvd p" by presburger
    with b show False by simp
  qed

  have fin_S : "finite ?S"
  proof -
    have uv_comm : "∀u v w. (u, v, w) ∈ ?S ⟶ (v, u, w) ∈ ?S" by simp

    have bound1 : "∀u v w. (u, v, w) ∈ ?S ⟶ u ≤ (int p - 1) div 4"
    proof clarsimp
      fix u v w assume 1: "int p = 4 * u * v + w⇧2" and 2: "(0::int) < v" and 3: "(0::int) < u"
      with 2 and 3 have 4: "4 * u ≤ 4 * u * v" by simp
      have "w ≠ (0::int)" using 1 2 3 w_neq0 by simp
      hence "1 ≤ w⇧2"
        by (metis add_0 linorder_not_le power2_less_eq_zero_iff zless_imp_add1_zle)
      with 4 have 5: "4 * u ≤ 4 * u * v + w⇧2 - 1" by simp
      note zdiv_mono1[OF 5, where b="4::int", simplified]
      thus "u ≤ (4 * u * v + w⇧2 - 1) div 4" .
    qed

    have bound2 : "∀u v w. (u, v, w) ∈ ?S ⟶ v ≤ (int p - 1) div 4"
      using bound1 uv_comm by blast

    have bound3 : "∀u v w. (u, v, w) ∈ ?S ⟶ ¦w¦ ≤ int p"
    proof clarsimp
      fix u v w::int 
      have 1: "¦w¦ ≤ w⇧2" by(rule sqr_geq_abs)
      assume "(0::int) < u" and "(0::int) < v"
      hence "0 < u * v" by(rule mult_pos_pos)
      hence "0 ≤ u * v" by simp
      hence "w⇧2 ≤ 4 * u * v + w⇧2" by simp 
      with 1 show "¦w¦ ≤ 4 * u * v + w⇧2" by simp 
    qed

    let ?prod = "{1..(int p - 1) div 4} × {1..(int p - 1) div 4} × {- int p..int p}"

    have prod: "∀u v w. (u, v, w) ∈ ?S ⟶ (u, v, w) ∈ ?prod"
    proof(intro allI)
      fix u v w show "(u, v, w) ∈ ?S ⟶ (u, v, w) ∈ ?prod"
      proof(rule impI)
        assume 1: "(u, v, w) ∈ ?S"
        note bound1[rule_format, OF 1] and
             bound2[rule_format, OF 1] 
        with 1 show "(u, v, w) ∈ ?prod" 
        proof simp
          have "¦w¦ ≤ int p" by(rule bound3[rule_format, OF 1])
          hence "w ≤ int p ∧ -w ≤ int p" by(rule abs_le_iff[THEN iffD1])
          with 1 show "- (4 * u * v) - w⇧2 ≤ w ∧ w ≤ 4 * u * v + w⇧2" by simp
        qed
      qed
    qed

    show ?thesis
    proof(rule_tac B="?prod" in finite_subset)
      show "?S ⊆ ?prod" using prod by fast
    next
      show "finite ?prod" by simp
    qed
  qed

  have inv1 : "involution_on ?S ?f"
    by(clarsimp simp: involution_on_def)

  have inv2 : "involution_on ?U ?g"
    by(fastforce simp: involution_on_def int_distrib power2_diff power2_eq_square)

  have inv3 : "involution_on ?T ?h"
    by(fastforce simp: involution_on_def)

  have part1 : "∀x∈?S. (x ∈ ?T) = (?f x ∉ ?T)"
  proof clarsimp
    fix u v w assume 1: "int p = 4 * u * v + w⇧2" and 2: "(0::int) < v" and 3: "(0::int) < u"
    have "w ≠ 0" 
    proof(rule w_neq0[rule_format])
      from 1 2 3 show "(u, v, w) ∈ ?S" by simp
    qed
    thus "(0 < w) = (¬ w < 0)" by fastforce
  qed
  
  have part2 : "∀x∈?S. (x ∈ ?U) = (?f x ∉ ?U)"
  proof clarsimp
    fix u v w assume 1: "int p = 4 * u * v + w⇧2" and 2: "u > 0" and 3: "v > 0" 
    show "(0 < u - v + w) = (¬ w < v - u)" (is "?L = ?R")
    proof
      assume ?L with 2 and 3 show ?R by fastforce 
    next
      assume ?R hence 4: "v - u ≤ w" by simp
      show ?L
      proof(rule ccontr)
        assume "¬ ?L" with 4 have "w = v - u" by fastforce
        with 1 have "int p = 4 * u * v + (v - u)⇧2" by fast
        then have sqr : "int p = (v + u)⇧2" by(simp add: power2_diff power2_sum)
        with int_prime_not_sqr[OF a] show False ..
      qed
    qed
  qed

  have card_eq : "card ?T = card ?U"
  proof -
    have 1: "2*card ?T = card ?S"
      by (smt (verit, ccfv_SIG) Int_iff fin_S inv1 involution_sub_card part1 subsetI)
    have "2*card ?U = card ?S"
      by (smt (verit, ccfv_SIG) Int_iff fin_S inv1 involution_sub_card part2 subsetI)
    with 1 show ?thesis by simp
  qed

  have fixp: "fixpoints_on ?U ?g = {((int p - 1) div 4, 1, 1)}" (is "?L = ?R")
  proof
    show "?L ⊆ ?R"
    proof(clarsimp simp: fixpoints_on_def)
      fix u v assume 1: "int p = 4 * u * v + v⇧2" and 2: "0 < u" and 3: "0 < v"
      then have 4: "int p = v * (4 * u + v)" 
        by(simp add: power2_eq_square int_distrib)
      have 5: "p = nat v * (4 * nat u + nat v)" 
      proof(rule int_int_eq[THEN iffD1])
        show "int p = int (nat v * (4 * nat u + nat v))"
          using 2 3 proof(simp add: 4)
        qed
      qed
      note prime_factors[OF a 5]
      then show "u = (4 * u * v + v⇧2 - 1) div 4 ∧ v = 1"
      proof
        assume "nat v = 1 ∧ 4 * nat u + nat v = p"
        with 2 and 3 have "v = 1 ∧ 4 * u + v = int p" by fastforce
        thus ?thesis by simp
      next
        assume "nat v = p ∧ 4 * nat u + nat v = 1"
        with 2 have False by fastforce
        thus ?thesis ..
      qed
    qed
  next
    show "?R ⊆ ?L"
    proof(clarsimp simp: fixpoints_on_def, rule conjI)
      show "int p = 4 * ((int p - 1) div 4) + 1"
      proof(subst dvd_mult_div_cancel)
        show "4 dvd int p - 1"
        proof(subst mod_eq_dvd_iff[THEN sym])
          show "int p mod 4 = 1 mod 4" by(simp add: nat_mod_int[OF b, simplified])
        qed
      next
        show "int p = int p - 1 + 1" by simp
      qed
    next
      show "0 < (int p - 1) div 4"
        using a b prime_gr4 by fastforce
    qed
  qed

  have cardS1 : "odd(card ?T)"
  proof(subst card_eq)
    show "odd(card ?U)"
      using add_diff_cancel_right' fin_S fixp inv2 involution_dom_fixpoints_parity by fastforce
  qed

  have fixp_ex : "∃x. x ∈ fixpoints_on ?T ?h"
  proof(rule ccontr)
    assume "¬ ?thesis" hence 1: "fixpoints_on ?T ?h = {}" by fast
    note involution_dom_card_sum[OF inv3, simplified 1]
    hence "even(card ?T)" by (simp add: fin_S) 
    with cardS1 show False ..
  qed

  note fixp_ex then have "∃u w. u > 0 ∧ w > 0 ∧ int p = 4 * u * u + w⇧2" 
    by(clarsimp simp: fixpoints_on_def, fast)
  then obtain u w where c: "u > 0 ∧ w > 0 ∧ int p = (2 * u)⇧2 + w⇧2"
    by(fastforce simp: power2_eq_square)
  hence "p = (nat(2 * u))⇧2 + (nat w)⇧2"
    by (smt (verit) int_nat_eq nat_int nat_int_add of_nat_power)
  thus ?thesis by fast

qed



end