Theory Nine_Unknowns_N_Z

theory Nine_Unknowns_N_Z 
  imports "../Coding_Theorem/Coding_Theorem" "../Bridge_Theorem/Bridge_Theorem"
          "../Coding_Theorem/Lemma_2_2" "../Coding_Theorem/Lower_Bounds"
          Nine_Unknowns_N_Z_Definitions Matiyasevich_Polynomial
begin

subsection ‹Proof of the Nine Unknowns Theorem›

theorem theorem_III_new_statement:
  fixes A :: "nat set"
    and P
  defines "φ a z⇩1 z⇩2 z⇩3 z⇩4 z⇩5 z⇩6 z⇩7 z⇩8 z⇩9 ≡ λfn. fn (int a) z⇩1 z⇩2 z⇩3 z⇩4 z⇩5 z⇩6 z⇩7 z⇩8 z⇩9"
  assumes "is_diophantine_over_N_with A P"
  shows "a ∈ A = (∃z⇩1 z⇩2 z⇩3 z⇩4 z⇩5 z⇩6 z⇩7 z⇩8 z⇩9. z⇩9 ≥ 0 ∧
                  φ a z⇩1 z⇩2 z⇩3 z⇩4 z⇩5 z⇩6 z⇩7 z⇩8 z⇩9 (combined_variables.Q P) = 0)"
    (is "_ = ?Pa_zero")
proof -
  interpret thm3: combined_variables P
    by unfold_locales

  show ?thesis 
proof (rule iffI) (* Indentation is 2 spaces less than usual on purpose! *)  
  assume "a ∈ A"

  then obtain ys⇩0 where ys⇩0_insertion: "insertion (ys⇩0(0 := int a)) P = 0" and 
                        ys⇩0_nonnegative: "is_nonnegative ys⇩0"
    using ‹is_diophantine_over_N_with A P› unfolding is_diophantine_over_N_with_def by auto

  obtain ys where ys_insertion: "insertion (ys(0 := int a)) (thm3.P⇩1) = 0"
              and ys_nonzero_unknown: "∃i∈{1..fresh_var P}. 0 < ys i" 
              and ys_zero: "∀i>fresh_var P. ys i = 0"
              and ys_nonnegative: "is_nonnegative ys"
    unfolding thm3.P⇩1_def
    using suitable_for_coding_exists_positive_unknown[of A P a ys⇩0,
              OF ‹is_diophantine_over_N_with A P› ‹a ∈ A› ys⇩0_insertion ys⇩0_nonnegative]
    by auto

  define ys' where "ys' ≡ ys(0 := int a)" 

  hence ys': "insertion ys' thm3.P⇩1 = 0"
    using ys_insertion by auto

  have vars_ne: "vars thm3.P⇩1 ≠ {}"
    unfolding thm3.P⇩1_def suitable_for_coding_degree_vars
    by auto
  have max_vars_P: "max_vars thm3.P⇩1 = fresh_var P"
    unfolding max_vars_of_nonempty[OF vars_ne] 
    unfolding thm3.P⇩1_def suitable_for_coding_degree_vars
    unfolding fresh_var_def 
    apply simp
    using ‹max_vars thm3.P⇩1 = Max (vars thm3.P⇩1)› combined_variables.P⇩1_def
      fresh_var_def suitable_for_coding_degree_vars(2) suitable_for_coding_max_vars
    by force

  define ys_max :: int where "ys_max = Max (ys' ` {0..fresh_var P})"
  
  have "ys_max ≥ 0"
  proof - 
    have "ys_max ≥ ys' 0"
      unfolding ys_max_def by auto
    thus ?thesis 
      unfolding ys'_def by simp
  qed

  have "ys' i ≤ ys_max" for i
  proof (cases "i ≤ fresh_var P")
    case True
    then show ?thesis
      unfolding ys_max_def ys'_def by auto
  next
    case False
    then show ?thesis
      using ys_zero ‹ys_max ≥ 0›
      unfolding ys_max_def ys'_def
      by simp
  qed

  define b⇩0 where "b⇩0 ≡ coding_variables.b a"
  have "∃f. f > 0 ∧ is_square (b⇩0 f) ∧ is_power2 (b⇩0 f) ∧ b⇩0 f > ys_max"
    using lemma_2_2_useful
    unfolding b⇩0_def thm3.b_def coding_variables.b_def
    using insertion_mult insertion_add insertion_Var insertion_Const ‹ys_max ≥ 0› by auto

  then obtain f where "f > 0" and "is_square (b⇩0 f)" and "is_power2 (b⇩0 f)"
                  and "b⇩0 f > ys_max"
    by auto

interpret coding: coding_theorem thm3.P⇩1 a f
  proof (unfold_locales)
    show "0 ≤ int a" by simp

    show "0 < f"
      using ‹0 < f› by auto

    show "is_power2 (coding_variables.b (int a) f)"
      using ‹is_power2 (b⇩0 f)› unfolding b⇩0_def
      unfolding coding_variables.b_def
      by auto

    show "0 < coding_variables.δ thm3.P⇩1"
      unfolding thm3.P⇩1_def coding_variables.δ_def
      using suitable_for_coding_total_degree by auto
  qed

  have p0: "coding.P_coeff (replicate (coding.ν + 1) 0) > 0"
    using suitable_for_coding_coeff0[of P]
    unfolding coding.P_coeff_def thm3.P⇩1_def coding_variables.P_coeff_def
              coding_variables.ν_def
    by simp

  have coding_1: "coding.statement1_strong ys'"
    unfolding coding.statement1_strong_def coding.statement1_weak_def 
  proof (intro conjI allI)
    show "ys' 0 = int a"
      unfolding ys'_def by auto

    show "0 ≤ ys' i" for i
      using ys_nonnegative unfolding is_nonnegative_def ys'_def by auto
    
    show "ys' i < coding.b" for i
      using ‹b⇩0 f > ys_max› ‹ys' i ≤ ys_max›
      unfolding b⇩0_def 
      by (auto simp: coding.b_def)

    show "insertion ys' thm3.P⇩1 = 0"
      using ys' by auto 

    show "∃i∈{1..coding.ν}. ys' i ≠ 0" 
    proof -
      from ys_nonzero_unknown obtain i where "i ∈ {1..fresh_var P}" and ys_i: "ys i > 0" by auto
      hence "ys' i ≠ 0" unfolding ys'_def by auto
      thus ?thesis
        using ‹i ∈ {1..fresh_var P}› ‹vars thm3.P⇩1 ≠ {}›
        unfolding coding.ν_def by (auto simp: max_vars_P)
    qed
  qed

  (* Application of Coding Theorem *)
  hence "∃g. coding.statement2_strong g"
    using coding_theorem.coding_theorem_direct[OF coding.coding_theorem_axioms] by auto
  
  then obtain g :: int where g: "coding.statement2_strong g" by auto

  define b where "b ≡ thm3.b a f g 0 0 0 0 0 0 0"
  define X where "X ≡ thm3.X a f g 0 0 0 0 0 0 0"
  define Y where "Y ≡ thm3.Y a f g 0 0 0 0 0 0 0"

  from g have "g ≥ b"
    unfolding coding.statement2_strong_def
    unfolding b_def thm3.b_def
    by (auto simp: le_trans coding.b_def)
  from g have "g < coding.γ * b ^ coding.α"
    unfolding coding.statement2_strong_def
    unfolding b_def thm3.b_def
    by (auto simp: le_trans coding.b_def)

  have "is_square b"
    using ‹is_square (b⇩0 f)›
    unfolding b⇩0_def b_def thm3.b_def
    by auto

  have "is_power2 b"
    using ‹is_power2 (b⇩0 f)›
    unfolding b⇩0_def b_def thm3.b_def
    by simp

  have 1: "b ≥ 0"
    using ‹is_square b› unfolding is_square_def
    by auto

  have "b ≥ 1"
    using ‹b⇩0 f > ys_max› ‹ys_max ≥ 0›
    unfolding coding.statement1_strong_def b⇩0_def b_def thm3.b_def
    by auto

  have 4: "1 ≤ g"
    using g ‹b ≥ 1›
    unfolding coding.statement2_strong_def b_def thm3.b_def 
    by (auto simp: le_trans coding.b_def)
  hence "0 < g" by auto

  (* Application of Bridge Theorem *)
  have "bridge_variables.statement2a b Y X g" 
  proof -
    from ‹0 < g› have "0 ≤ g" by auto
    have "0 ≤ int a" by auto
    have 2: "b ≤ Y ∧ 2 ^ 8 ≤ Y"
      using coding.lower_bounds[OF ‹0 ≤ int a› ‹0 < f› ‹0 ≤ g› coding.δ_pos p0]
      unfolding b_def Y_def thm3.b_def thm3.Y_def by auto

    have 3: "3 * b ≤ X"
      using coding.lower_bounds[OF ‹0 ≤ int a› ‹0 < f› ‹0 ≤ g› coding.δ_pos p0]
      unfolding b_def X_def thm3.b_def thm3.X_def coding.b_def 
      by (auto simp: coding.b_def)

    have "Y dvd int (2 * nat X choose nat X)" 
    proof - 
      have "coding.Y dvd int (2 * nat (coding.X g) choose nat (coding.X g))"
        using g unfolding coding.statement2_strong_def by auto

      thus ?thesis
        unfolding Y_def thm3.Y_def X_def thm3.X_def by auto 
    qed

    hence statement1: "bridge_variables.statement1 b Y X" 
      unfolding bridge_variables.statement1_def
      using ‹is_power2 b› by simp

    show ?thesis
      using bridge_variables.theorem_II_1_3[of b Y X g, OF 1 2 3 4 statement1] by auto
  qed

  then obtain h k l w x y where thm2:
    "bridge_variables.d2a l w h x y g Y X ∧
    bridge_variables.d2b k l w x g Y X ∧
    bridge_variables.d2c l w h b g Y X ∧
    bridge_variables.d2e k l w h g Y X ∧
    b ≤ h ∧ b ≤ k ∧ b ≤ l ∧ b ≤ w ∧ b ≤ x ∧ b ≤ y"
    using bridge_variables.statement2a_def[of b Y X g] by metis

  (* The last slot is for n -- which we will obtain momentarily --,
     but z_0 doesn't actually depend on n *)
  define z⇩0 where "z⇩0 ≡ λfn. fn (int a) f g h k l w x y (0 :: int) :: int"

  define S where "S ≡ z⇩0 thm3.S"
  define T where "T ≡ z⇩0 thm3.T"
  define R where "R ≡ z⇩0 thm3.R"
  define A⇩1 where "A⇩1 ≡ z⇩0 thm3.A⇩1"
  define A⇩2 where "A⇩2 ≡ z⇩0 thm3.A⇩2"
  define A⇩3 where "A⇩3 ≡ z⇩0 thm3.A⇩3"
  
  define γ' where
    "γ' ≡ λ(n :: int) fn. fn A⇩1 A⇩2 A⇩3 S T R n :: int"

  (* Application of the relation combining lemma *)
  have "∃n≥0. γ' n thm3.M3 = 0"
  proof -
    have thm3_Y: "thm3.Y (int a) f g h k l w x y 0 = Y"
      unfolding thm3.Y_def Y_def ..
    have thm3_X: "thm3.X (int a) f g h k l w x y 0 = X"
      unfolding thm3.X_def X_def ..
    have thm3_b: "thm3.b (int a) f g h k l w x y 0 = b"
      unfolding thm3.b_def b_def ..

    from thm2 have d2a: "bridge_variables.d2a l w h x y g Y X" by simp
    from thm2 have d2b: "bridge_variables.d2b k l w x g Y X" by simp
    from thm2 have d2c: "bridge_variables.d2c l w h b g Y X" by simp
    from thm2 have d2e: "bridge_variables.d2e k l w h g Y X" by simp

    have "S ≠ 0"
      unfolding S_def z⇩0_def thm3.S_def bridge_variables.S_def by presburger

    have "S dvd T" 
      using d2c unfolding bridge_variables.d2c_def S_def T_def thm3.S_def thm3.T_def z⇩0_def
      by (simp add: thm3_Y thm3_X thm3_b)

    have "R > 0"
    proof - 
      have "l > 0" using thm2 ‹b ≥ 1› by auto
      have "x > 0" using thm2 ‹b ≥ 1› by auto

      have "g < thm3.μ (int a) f g h k l w x y 0"
        unfolding thm3.μ_def coding.b_def
        using ‹g < coding.γ * b ^ coding.α›
        unfolding b_def thm3.b_def .

      show ?thesis 
        using thm3.R_gt_0_necessary_condition[OF ‹f > 0› ‹x > 0› ‹l > 0› ‹g > 0›
                                                 ‹g < thm3.μ (int a) f g h k l w x y 0›]
        unfolding R_def z⇩0_def  
        using d2e unfolding X_def Y_def thm3.Y_def thm3.X_def by auto
    qed

    have "is_square A⇩1"
      unfolding A⇩1_def z⇩0_def thm3.A⇩1_def thm3_b 
      using ‹is_square b›
      by simp
    have "is_square A⇩2"
      unfolding A⇩2_def z⇩0_def thm3.A⇩2_def
      using d2a unfolding bridge_variables.d2a_def thm3.D_def thm3.I_def thm3.F_def
      by (simp add: thm3_Y thm3_X thm3_b)
    have "is_square A⇩3"
      unfolding A⇩3_def z⇩0_def thm3.A⇩3_def
      using d2b unfolding bridge_variables.d2b_def thm3.U_def thm3.V_def thm3.K_def
      by (simp add: thm3_Y thm3_X thm3_b)

    obtain n where n_def: "n≥0 ∧ section5.M3 A⇩1 A⇩2 A⇩3 S T R n = 0"
      using matiyasevich_polynomial.relation_combining[of S T R A⇩1 A⇩2 A⇩3, OF ‹S ≠ 0›]
      using ‹S dvd T› ‹R > 0› ‹is_square A⇩1› ‹is_square A⇩2› ‹is_square A⇩3› 
      by auto

    show ?thesis 
      apply (rule exI[of _ n], simp add: n_def)
      unfolding thm3.M3_def γ'_def apply simp   
      unfolding section5.M3_correct
      by (auto simp: n_def nth0_Cons)
  qed

  then obtain n where insertion_M3: "γ' n thm3.M3 = 0" and "n≥0"
    by auto

  hence "n ≥ 0" by auto

  (* Now we can define the final insertion map *)
  define z where "z ≡ φ a f g h k l w x y n"

  have insertion_Pa: "z thm3.Q = 0"
  proof -
    have γ_eq_z_comp_σ: "γ' n = z ∘ thm3.σ"
      unfolding γ'_def thm3.σ_def comp_def z_def φ_def
      unfolding A⇩1_def A⇩2_def A⇩3_def S_def T_def R_def z⇩0_def
      unfolding thm3.A⇩1_def thm3.A⇩2_def thm3.A⇩3_def thm3.S_def thm3.T_def thm3.R_def thm3.m_def
      unfolding thm3.μ_def
      unfolding thm3.L_def thm3.U_def thm3.V_def thm3.A_def thm3.C_def thm3.D_def thm3.F_def 
                thm3.I_def thm3.W_def thm3.K_def
      unfolding thm3.b_def thm3.X_def thm3.Y_def
      ..

    show ?thesis
      unfolding thm3.Q_alt fun_cong[OF γ_eq_z_comp_σ[symmetric, unfolded comp_def]]
      using insertion_M3 .
  qed

  show ?Pa_zero 
    using insertion_Pa ‹n≥0› unfolding z_def by metis
next 
  assume ?Pa_zero

  then obtain f g h k l w x y n where insertion_Q: 
    "φ a f g h k l w x y n thm3.Q = 0" and "n ≥ 0"
    unfolding thm3.Q_def by auto

  define z where "z ≡ φ a f g h k l w x y n"

  define S where "S ≡ z thm3.S"
  define T where "T ≡ z thm3.T"
  define R where "R ≡ z thm3.R"
  define A⇩1 where "A⇩1 ≡ z thm3.A⇩1"
  define A⇩2 where "A⇩2 ≡ z thm3.A⇩2"
  define A⇩3 where "A⇩3 ≡ z thm3.A⇩3"

  (* Application of the relation combining lemma *)
  have "S dvd T" and "0 < R" and "is_square A⇩1" and "is_square A⇩2" and "is_square A⇩3"
  proof - 
    have "S ≠ 0"
      unfolding S_def z_def φ_def thm3.S_def bridge_variables.S_def by presburger

    have "section5.M3 A⇩1 A⇩2 A⇩3 S T R n = 0"
      using insertion_Q
      unfolding φ_def thm3.Q_def thm3.M3_def
      apply (simp add: section5.M3_correct nth0_def)
      unfolding A⇩1_def A⇩2_def A⇩3_def S_def T_def R_def z_def φ_def 
      by (auto simp add: thm3.m_def) 

    thus "S dvd T" and "0 < R" and "is_square A⇩1" and "is_square A⇩2" and "is_square A⇩3"
      using matiyasevich_polynomial.relation_combining[of S T R A⇩1 A⇩2 A⇩3, OF ‹S ≠ 0›] ‹n≥0› 
      unfolding thm3.M3_def φ_def by auto
  qed

  define b where "b ≡ thm3.b a f g h k l w x y n"
  define X where "X ≡ thm3.X a f g h k l w x y n"
  define Y where "Y ≡ thm3.Y a f g h k l w x y n"

  have "b ≥ 0" 
    using ‹is_square A⇩1› unfolding A⇩1_def thm3.A⇩1_def thm3.b_def b_def z_def φ_def 
    unfolding is_square_def by auto

  have "thm3.R τ > 0" using ‹R > 0› unfolding thm3.R_def R_def z_def φ_def by auto
  have "thm3.b τ ≥ 0" using ‹b ≥ 0› unfolding thm3.b_def b_def z_def φ_def by auto

  have "f > 0"
    proof - 
      have "f ≠ 0" using ‹R > 0› unfolding R_def thm3.R_def z_def φ_def by auto

      show ?thesis
      using ‹b ≥ 0› unfolding b_def thm3.b_def coding_variables.b_def 
        using ‹f ≠ 0› apply simp
      by (smt (verit) mult_le_cancel_right1 of_nat_less_0_iff)
    qed

  have "g ≥ 1"
    using thm3.R_gt_0_consequences(1)[OF ‹thm3.R τ > 0› ‹thm3.b τ ≥ 0› ‹f > 0›] by simp

  have p0: "coding_variables.P_coeff thm3.P⇩1
                (replicate (coding_variables.ν thm3.P⇩1 + 1) 0) > 0"
    using suitable_for_coding_coeff0[of P]
    unfolding thm3.P⇩1_def coding_variables.P_coeff_def coding_variables.ν_def
    by simp

  (* Application of the Bridge Theorem *)
  have "bridge_variables.statement1 b Y X"
  proof - 
    have "g ≥ 0" using ‹g ≥ 1› by auto (* for convenience *)

    have "int a ≥ 0"
      by auto
    have delta: "coding_variables.δ thm3.P⇩1 > 0"
      by (simp add: suitable_for_coding_total_degree coding_variables.δ_def thm3.P⇩1_def)

    have Y: "b ≤ Y ∧ 2 ^ 8 ≤ Y "
      using coding_variables.lower_bounds(2-3)[OF ‹int a ≥ 0› ‹0 < f› ‹g ≥ 0› delta p0]
      unfolding b_def Y_def thm3.b_def thm3.Y_def by auto

    have X: "X ≥ 3 * b"
      using coding_variables.lower_bounds(1)[OF ‹int a ≥ 0› ‹0 < f› ‹g ≥ 0› delta p0]
      unfolding b_def X_def thm3.b_def thm3.X_def by auto

    have "bridge_variables.statement2 b Y X g"
    proof - 
      have "l * x ≠ 0"
        using ‹R > 0› unfolding R_def thm3.R_def z_def φ_def by auto

      have d2a: "bridge_variables.d2a l w h x y g Y X"
        using ‹is_square A⇩2› 
        unfolding bridge_variables.d2a_def A⇩2_def z_def thm3.A⇩2_def φ_def 
                  thm3.D_def thm3.I_def thm3.F_def Y_def X_def by auto
        
      have d2b: "bridge_variables.d2b k l w x g Y X"
        using ‹is_square A⇩3› 
        unfolding bridge_variables.d2b_def A⇩3_def z_def thm3.A⇩3_def φ_def
                  thm3.U_def Y_def X_def thm3.V_def thm3.K_def by auto
      
      have d2c: "bridge_variables.d2c l w h b g Y X"
        using ‹S dvd T› unfolding bridge_variables.d2c_def S_def T_def 
                                  thm3.S_def thm3.T_def z_def φ_def Y_def X_def b_def 
        by auto
      
      have d2f: "bridge_variables.d2f k l w h g Y X"
        using thm3.R_gt_0_consequences(4)[OF ‹thm3.R τ > 0› ‹thm3.b τ ≥ 0› ‹f > 0›] 
        unfolding X_def Y_def by simp
      
      show ?thesis 
        unfolding bridge_variables.statement2_def
        using ‹l * x ≠ 0› d2a d2b d2c d2f by metis
    qed

    thus ?thesis 
      using bridge_variables.theorem_II_2_1[of b Y X g, OF ‹b ≥ 0› Y X ‹g≥1›] by auto
  qed

  hence "is_power2 b" and Y_dvd: "Y dvd int (2 * nat X choose nat X)"
    unfolding bridge_variables.statement1_def by auto

  interpret coding: coding_theorem thm3.P⇩1 "int a" f
  proof (unfold_locales)
    show "0 ≤ int a" by simp

    show "0 < f" using ‹f > 0› by auto

    show "is_power2 (coding_variables.b (int a) f)" 
      using ‹is_power2 b› unfolding b_def thm3.b_def by auto

    show "0 < coding_variables.δ thm3.P⇩1"
      unfolding thm3.P⇩1_def coding_variables.δ_def
      using suitable_for_coding_total_degree by auto
  qed

  have "∃y. coding.statement1_weak y"
  proof - 
    have "0 ≤ g" using ‹g ≥ 1› by auto

    have g_bound: "g < 2 * int coding.γ * coding.b ^ coding.α" 
      using thm3.R_gt_0_consequences(2)[OF ‹thm3.R τ > 0› ‹thm3.b τ ≥ 0› ‹f > 0›] 
      unfolding thm3.μ_def thm3.b_def by auto
      
    have dvd_choose: "coding.Y dvd int (2 * nat (coding.X g) choose nat (coding.X g))"
      using Y_dvd unfolding Y_def X_def thm3.Y_def thm3.X_def by auto

    show ?thesis
      using coding.coding_theorem_reverse[of g] unfolding coding.statement2_weak_def
      using ‹g≥0› g_bound dvd_choose
      by (metis)
  qed

  then obtain y where y_0: "y 0 = int a"
                  and y_i: "∀i. 0 ≤ y i ∧ y i < coding.b"
                  and insertion_y: "insertion y thm3.P⇩1 = 0"
    unfolding coding.statement1_weak_def by auto

  have "is_nonnegative y"
    using y_i unfolding is_nonnegative_def by auto

  have "insertion (y(0 := int a)) thm3.P⇩1 = 0"
  proof - 
    have y_eq: "(y(0 := int a)) = y"
      using y_0 by auto

    show ?thesis using insertion_y unfolding y_eq by auto
  qed

  hence "∃y⇩0. insertion (y⇩0(0 := int a)) P = 0 ∧ is_nonnegative y⇩0" 
    using suitable_for_coding_diophantine_equivalent ‹is_nonnegative y›
    unfolding thm3.P⇩1_def by auto 

  thus "a ∈ A"
    using assms(2) unfolding is_diophantine_over_N_with_def by auto
qed

qed

theorem theorem_III:
  fixes A :: "nat set" and P :: "int mpoly"
  assumes "is_diophantine_over_N_with A P"
  shows "a ∈ A = (∃f g h k l w x y n. n ≥ 0 ∧
                 insertion ((!) [int a, f, g, h, k, l, w, x, y, n])
                 (combined_variables.Q_poly P) = 0)"
  unfolding combined_variables.Q_correct
  unfolding theorem_III_new_statement[of A P a, OF assms(1)]
  by simp

theorem nine_unknowns_over_Z_and_N: 
  fixes P :: "int mpoly"
  shows "(∃z :: nat ⇒ int. is_nonnegative z ∧ 
              insertion (z(0 := int a)) P = 0) 
       = (∃f g h k l w x y n. n ≥ 0 ∧
              insertion ((!) [int a, f, g, h, k, l, w, x, y, n])
              (combined_variables.Q_poly P) = 0)"
proof - 
  define A where "A ≡ {a. ∃z. insertion (z(0 := int a)) P = 0 ∧ is_nonnegative z}"

  show ?thesis
    using theorem_III[of A P] unfolding A_def is_diophantine_over_N_with_def 
    by fastforce
qed

end