Theory Alternative_Proofs

theory Alternative_Proofs
  imports Smith_Normal_Form.Admits_SNF_From_Diagonal_Iff_Bezout_Ring
          Smith_Normal_Form.Elementary_Divisor_Rings
begin


text ‹Theorem 2: (C) ==> (A)›

lemma diagonal_2x2_admits_SNF_imp_bezout_ring_JNF:
  assumes admits_SNF: "A. (A::'a mat)  carrier_mat 2 2  isDiagonal_mat A
   (P Q. P  carrier_mat 2 2  Q  carrier_mat 2 2  invertible_mat P  invertible_mat Q 
       Smith_normal_form_mat (P*A*Q))"
  shows "OFCLASS('a::comm_ring_1, bezout_ring_class)"
proof (intro_classes)
  fix a b::'a
  show "p q d. p * a + q * b = d  d dvd a  d dvd b  (d'. d' dvd a  d' dvd b  d' dvd d)"
  proof (cases "a=b")
    case True
    show ?thesis
      by (metis True add.right_neutral comm_semiring_class.distrib dvd_refl mult_1)
  next
    case False note a_not_b = False
    let ?A = "Matrix.mat 2 2 (λ(i,j). if i = 0  j = 0 then a else if i = 1  j = 1 then b else 0)"
    have A_carrier: "?A  carrier_mat 2 2" by auto
    moreover have diag_A: "isDiagonal_mat ?A" by (simp add: isDiagonal_mat_def)
    ultimately obtain P Q where P: "P  carrier_mat 2 2" 
        and Q: "Q  carrier_mat 2 2" and inv_P: "invertible_mat P" and inv_Q: "invertible_mat Q"
        and SNF_PAQ: "Smith_normal_form_mat (P*?A*Q)" 
      using admits_SNF by blast 
    let ?p = "P$$(0,0)*Q$$(0,0)"
    let ?q = "P$$(0,1)*Q$$(1,0)"
    let ?d = "(P*?A*Q) $$ (0,0)"
    let ?d' = "(P*?A*Q) $$ (1,1)"
    have d_dvd_d': "?d dvd ?d'" 
      by (metis (no_types, lifting) A_carrier One_nat_def P Q SNF_PAQ SNF_first_divides_all bot_nat_0.not_eq_extremum
          less_Suc_numeral mult_carrier_mat pred_numeral_simps(2) zero_neq_numeral)
    have pa_qb_d: "?p*a + ?q * b = ?d"
    proof -
      let ?U = "P*?A"
      have "?U $$ (0, 0) = P $$ (0,0)* ?A $$ (0,0) + P $$ (0,1)* ?A $$ (1,0)" 
        by (rule mat_mult2_00, insert P, auto)
      also have "... = P $$ (0,0) * a" by auto
      finally have 1: "(P*?A) $$ (0, 0) = P $$ (0,0) * a" .
      have "?U $$ (0, 1) = P $$ (0,0)* ?A $$ (0,1) + P $$ (0,1)* ?A $$ (1,1)"
        by (rule mat_mult2_01, insert P, auto)
      hence 2: "(P*?A) $$ (0, 1)= P $$ (0,1)* b" by auto
      have "?d = ?U $$ (0, 0) * Q $$ (0, 0) + ?U $$ (0, 1) * Q $$ (1, 0)"
        by (rule mat_mult2_00, insert Q P, auto)
      also have "... = ?p*a + ?q * b" unfolding 1 unfolding 2 by auto
      finally show ?thesis ..
    qed    
    have i: "ideal_generated {a, b} = ideal_generated {?d}" 
    proof
      show "ideal_generated {?d}  ideal_generated {a, b}"
      proof (rule ideal_generated_subset2, rule ballI, simp)
        fix x 
        let ?f = "λx. if x = a then ?p else ?q"
        show "?d  ideal_generated {a, b}"        
          unfolding ideal_explicit 
          by simp (rule exI[of _ ?f], rule exI[of _ "{a,b}"], 
                  insert a_not_b One_nat_def pa_qb_d, auto)  
      qed
      show "ideal_generated {a, b}   ideal_generated {?d}" 
      proof -
        obtain P' where inverts_mat_P': "inverts_mat P P'  inverts_mat P' P" 
            using inv_P unfolding invertible_mat_def by auto
          have P': "P'  carrier_mat 2 2" 
            using inverts_mat_P' 
            unfolding carrier_mat_def inverts_mat_def
            by (auto,metis P carrier_matD index_mult_mat(3) one_carrier_mat)+
          obtain Q' where inverts_mat_Q': "inverts_mat Q Q'  inverts_mat Q' Q"
            using inv_Q unfolding invertible_mat_def by auto
          have Q': "Q'  carrier_mat 2 2" 
            using inverts_mat_Q'
            unfolding carrier_mat_def inverts_mat_def
            by (auto,metis Q carrier_matD index_mult_mat(3) one_carrier_mat)+
          have rw_PAQ: "(P'*(P*?A*Q)*Q') $$ (i, i) = ?A $$ (i,i)" for i 
            using inv_P'PAQQ'[OF A_carrier P _ _ Q P' Q'] inverts_mat_P' inverts_mat_Q' by auto
          have diag_PAQ: "isDiagonal_mat (P*?A*Q)" 
            using SNF_PAQ unfolding Smith_normal_form_mat_def by auto
          have PAQ_carrier: "(P*?A*Q)  carrier_mat 2 2" using P Q by auto
          have z1: "0<(2::nat)" and z2: "1<(2::nat)" by auto        
          obtain f where f: "(P'*(P*?A*Q)*Q') $$ (0, 0) = (iset (diag_mat (P*?A*Q)). f i * i)"          
            using exists_f_PAQ_Aii[OF diag_PAQ P' PAQ_carrier Q' z1] by blast
          obtain g where g: "(P'*(P*?A*Q)*Q') $$ (1, 1) = (iset (diag_mat (P*?A*Q)). g i * i)"          
            using exists_f_PAQ_Aii[OF diag_PAQ P' PAQ_carrier Q' z2] by blast
          have A00: "?A $$ (0, 0) = (iset (diag_mat (P*?A*Q)). f i * i)"
            using rw_PAQ[of 0] using f by presburger
          have A11: "?A $$ (1, 1) = (iset (diag_mat (P*?A*Q)). g i * i)"
            using rw_PAQ[of 1] using g by presburger
          have d_dvd_a: "?d dvd a" using A00 d_dvd_d'
            by (auto, smt (verit, best) A00 A_carrier P Q S00_dvd_all_A SNF_PAQ inv_P inv_Q 
                numeral_2_eq_2 zero_less_Suc)
          have d_dvd_b: "?d dvd b" using A11 d_dvd_d'
            by (smt (verit, ccfv_threshold) A_carrier One_nat_def P Q S00_dvd_all_A SNF_PAQ 
                index_mat(1) inv_P inv_Q lessI nat.simps(3) numeral_2_eq_2 split_conv)
        have 1: "a  ideal_generated {?d}" and 2: "b  ideal_generated {?d}"
          using d_dvd_a d_dvd_b dvd_ideal_generated_singleton' ideal_generated_subset_generator
          by blast+
        show ?thesis by (rule ideal_generated_subset2, insert 1 2, auto)
      qed
    qed
    have " p q. p * a + q * b = ?d" by (rule ideal_generated_pair_exists[OF i])
    moreover have d_dvd_a: "?d dvd a" and d_dvd_b: "?d dvd b"
      using i ideal_generated_singleton_dvd by blast+
    moreover have "(d'. d' dvd a  d' dvd b  d' dvd ?d)" using ideal_generated_dvd[OF i] by auto
    ultimately show ?thesis
      by blast
  qed
qed


text ‹Theorem 2: (A) ==> (C)›

lemma bezout_ring_imp_diagonal_2x2_admits_SNF_JNF:
  assumes c: "OFCLASS('a::comm_ring_1, bezout_ring_class)"
  shows "A. (A::'a mat)  carrier_mat 2 2  isDiagonal_mat A
   (P Q. P  carrier_mat 2 2  Q  carrier_mat 2 2 
       invertible_mat P  invertible_mat Q  Smith_normal_form_mat (P*A*Q))"  
  using bezout_ring_imp_diagonal_admits_SNF_JNF
      [OF OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a, OF c]]
  unfolding admits_SNF_JNF_def
  using A. admits_SNF_JNF A admits_SNF_JNF_alt_def by blast


text ‹Theorem 2: (A) <==> (C)›

lemma diagonal_2x2_admits_SNF_iff_bezout_ring: 
  shows "OFCLASS('a::comm_ring_1, bezout_ring_class) 
     (A::'a mat. A  carrier_mat 2 2  admits_SNF_JNF A)" (is "?lhs  ?rhs")
proof 
  fix A::"'a mat"
  assume c: "OFCLASS('a, bezout_ring_class)"
  show "A  carrier_mat 2 2  admits_SNF_JNF A"
    using bezout_ring_imp_diagonal_admits_SNF_JNF
          [OF OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a, OF c]]
    unfolding admits_SNF_JNF_def by blast
next
  assume rhs: "(A::'a mat. A  carrier_mat 2 2  admits_SNF_JNF A)"
  show "OFCLASS('a::comm_ring_1, bezout_ring_class)"
    by (rule diagonal_2x2_admits_SNF_imp_bezout_ring_JNF, insert rhs, simp add: admits_SNF_JNF_def) 
qed

text ‹Theorem 2: (B) <==> (C)›
lemma diagonal_2x2_admits_SNF_iff_diagonal_admits_SNF:
  shows "((A::'a::comm_ring_1 mat). admits_SNF_JNF A) =
      ((A::'a mat)  carrier_mat 2 2. admits_SNF_JNF A)"
proof 
 assume "A::'a mat. admits_SNF_JNF A"
  thus "(A::'a mat)carrier_mat 2 2. admits_SNF_JNF A" 
    by (insert admits_SNF_JNF_alt_def, blast)
next
  assume "A::'a mat carrier_mat 2 2. admits_SNF_JNF A "
  hence H: "OFCLASS('a, bezout_ring_class)"
    using diagonal_2x2_admits_SNF_iff_bezout_ring[where ?'a = 'a] by auto  
  show "A::'a mat. admits_SNF_JNF A" 
    using bezout_ring_imp_diagonal_admits_SNF_JNF
      [OF OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a, OF H]]
    by simp
qed

text ‹Theorem 2: final statements›

theorem Theorem2_final:
  shows A_imp_B: "OFCLASS('a::comm_ring_1, bezout_ring_class) 
     (A::'a mat. admits_SNF_JNF A)"
  and B_imp_C: "(A::'a mat. admits_SNF_JNF A)  
      ((A::'a mat)  carrier_mat 2 2. admits_SNF_JNF A)"
  and C_imp_A: "((A::'a mat)  carrier_mat 2 2. admits_SNF_JNF A) 
     OFCLASS('a::comm_ring_1, bezout_ring_class)"
proof
  fix A::"'a mat"
  assume H: "OFCLASS('a, bezout_ring_class)"
  show "admits_SNF_JNF A"
    using bezout_ring_imp_diagonal_admits_SNF_JNF[OF OFCLASS_bezout_ring_imp_class_bezout_ring[where ?'a='a, OF H]]
    by simp
next
  assume "A::'a mat. admits_SNF_JNF A"
  thus "(A::'a mat)carrier_mat 2 2. admits_SNF_JNF A" 
    by (insert admits_SNF_JNF_alt_def, blast)
next
  assume "(A::'a mat)carrier_mat 2 2. admits_SNF_JNF A" 
  thus "OFCLASS('a, bezout_ring_class)"
    using diagonal_2x2_admits_SNF_iff_bezout_ring[where ?'a = 'a] by auto
qed


theorem Theorem2_final':
  shows A_eq_B: "OFCLASS('a::comm_ring_1, bezout_ring_class)  (A::'a mat. admits_SNF_JNF A)"
  and A_eq_C: "OFCLASS('a::comm_ring_1, bezout_ring_class) 
      ((A::'a mat). A  carrier_mat 2 2  admits_SNF_JNF A)"
  and B_eq_C: "((A::'a::comm_ring_1 mat). admits_SNF_JNF A) =
      ((A::'a mat)  carrier_mat 2 2. admits_SNF_JNF A)"
  using diagonal_admits_SNF_iff_bezout_ring' 
  using diagonal_2x2_admits_SNF_iff_bezout_ring
  using diagonal_2x2_admits_SNF_iff_diagonal_admits_SNF by auto

text ‹Theorem 2: final statement in HA. (A) <==> (C).›

theorem Theorem2_A_eq_C_HA:
   "OFCLASS('a::comm_ring_1, bezout_ring_class)  ((A::'a^2^2). admits_SNF_HA A)"
proof 
  fix A::"'a^2^2"
  assume H: "OFCLASS('a, bezout_ring_class)"
  let ?A = "Mod_Type_Connect.from_hmam A" 
  have A: "?A  carrier_mat 2 2" by auto
  have [transfer_rule]: "Mod_Type_Connect.HMA_M ?A A" 
    unfolding Mod_Type_Connect.HMA_M_def A by auto
  have "admits_SNF_JNF ?A" using A_imp_B[OF H] by auto
  thus "admits_SNF_HA A" by transfer'
next
  assume a: "(A::'a^2^2. admits_SNF_HA A)"
  have [transfer_rule]: "Mod_Type_Connect.HMA_M (Mod_Type_Connect.from_hmam A) A" for A::"'a^2^2" 
    unfolding Mod_Type_Connect.HMA_M_def by auto
  have a': "(A::'a^2^2. admits_SNF_JNF (Mod_Type_Connect.from_hmam A))" 
  proof -
    fix A::"'a^2^2"
    have ad: "admits_SNF_HA A" using a by simp
    let ?A = "Mod_Type_Connect.from_hmam A" 
    have A: "?A  carrier_mat 2 2" by auto
    have [transfer_rule]: "Mod_Type_Connect.HMA_M ?A A" 
      unfolding Mod_Type_Connect.HMA_M_def A by auto
    show "admits_SNF_JNF (Mod_Type_Connect.from_hmam A)" using ad by transfer'
  qed
  have "(A::'a^2^2. admits_SNF_JNF (Mod_Type_Connect.from_hmam A)) 
    = ((A::'a mat)carrier_mat 2 2. admits_SNF_JNF A)" 
  proof (auto)
    fix A::"'a mat" assume a1: "A::'a^2^2. admits_SNF_JNF (Mod_Type_Connect.from_hmam A)" 
      and "A  carrier_mat 2 2" 
    thus "admits_SNF_JNF A" by (metis Mod_Type_Connect.from_hma_to_hmam One_nat_def  UNIV_1 a1 
          card.empty card.insert card_bit0 empty_iff finite mult.right_neutral)
  next
    fix A::"'a^2^2" assume "Acarrier_mat 2 2. admits_SNF_JNF A"
    have ad: "admits_SNF_HA A" using a by simp
    let ?A = "Mod_Type_Connect.from_hmam A" 
    have A: "?A  carrier_mat 2 2" by auto
    have [transfer_rule]: "Mod_Type_Connect.HMA_M ?A A" 
      unfolding Mod_Type_Connect.HMA_M_def A by auto
    show "admits_SNF_JNF (Mod_Type_Connect.from_hmam A)" using ad by transfer'
  qed
  hence "(A::'a mat. A  carrier_mat 2 2  admits_SNF_JNF A)" using a' by auto
  thus "OFCLASS('a, bezout_ring_class)" using Theorem2_final'[where ?'a='a] by auto
qed


text ‹Hermite implies Bezout›

text ‹Theorem 3, proof for 1x2 matrices›
lemma theorem3_restricted_12_part1:
  assumes T: "(a b::'a::comm_ring_1.  a1 b1 d. a = a1*d  b = b1*d 
     ideal_generated {a1,b1} = ideal_generated {1})"
  shows "(A::'a mat)  carrier_mat 1 2. admits_triangular_reduction A"
proof (rule)
  fix A::"'a mat"
  assume A: "A  carrier_mat 1 2"
  let ?a = "A $$ (0,0)"
  let ?b = "A $$ (0,1)"
  obtain a1 b1 d where a: "?a = a1*d" and b: "?b = b1*d" 
    and i: "ideal_generated {a1,b1} = ideal_generated {1}" 
    using T by blast
  obtain s t where sa1tb1:"s*a1+t*b1=1" using ideal_generated_pair_exists_pq1[OF i[simplified]] by blast
  let ?Q = "Matrix.mat 2 2 (λ(i,j). if i = 0  j = 0 then s else
                                    if  i = 0  j = 1 then -b1 else
                                    if  i = 1  j = 0 then t else a1)"
  have Q: "?Q  carrier_mat 2 2" by auto
  have det_Q: "Determinant.det ?Q = 1" unfolding det_2[OF Q] 
    using sa1tb1 by (simp add: mult.commute)
  hence inv_Q: "invertible_mat ?Q" using invertible_iff_is_unit_JNF[OF Q] by auto
  have lower_AQ: "lower_triangular (A*?Q)" 
  proof -
    have "Matrix.row A 0 $v Suc 0 * a1 = Matrix.row A 0 $v 0 * b1" if j2: "j<2" and j0: "0<j" for j
      by (metis A One_nat_def a b carrier_matD(1) carrier_matD(2) index_row(1) lessI 
          more_arith_simps(11) mult.commute numeral_2_eq_2 pos2)
    thus ?thesis unfolding lower_triangular_def using A 
      by (auto simp add: scalar_prod_def sum_two_rw)
  qed
  show "admits_triangular_reduction A" 
    unfolding admits_triangular_reduction_def using lower_AQ inv_Q Q A by force    
qed


lemma theorem3_restricted_12_part2:
  assumes 1: "(A::'a::comm_ring_1 mat)  carrier_mat 1 2. admits_triangular_reduction A"
  shows "a b::'a.  a1 b1 d. a = a1*d  b = b1*d  ideal_generated {a1,b1} = ideal_generated {1}"
proof (rule allI)+
  fix a b::'a
  let ?A = "Matrix.mat 1 2 (λ(i,j). if i = 0  j = 0 then a else b)"
  obtain Q where AQ: "lower_triangular (?A*Q)" and inv_Q: "invertible_mat Q"
    and Q: "Q  carrier_mat 2 2"
    using 1 unfolding admits_triangular_reduction_def by fastforce
  hence [simp]: "dim_col Q = 2" and [simp]: "dim_row Q = 2" by auto
  let ?s = "Q $$ (0,0)"
  let ?t = "Q $$ (1,0)"
  let ?a1 = "Q $$ (1,1)"
  let ?b1 = "-(Q $$ (0,1))"
  let ?d = "(?A*Q) $$ (0,0)"
  have ab1_ba1: "a*?b1 = b*?a1"
  proof -     
    have  "(?A*Q) $$ (0,1) =  (i = 0..<2. (if i = 0 then a else b) * Q $$ (i, Suc 0))"
      unfolding times_mat_def col_def scalar_prod_def by auto
    also have "... = (i  {0,1}. (if i = 0 then a else b) * Q $$ (i, Suc 0))" 
      by (rule sum.cong, auto)
    also have "... = - a*?b1 + b*?a1" by auto
    finally have "(?A*Q) $$ (0,1) = - a*?b1 + b*?a1" by simp
    moreover have "(?A*Q) $$ (0,1) = 0" using AQ unfolding lower_triangular_def by auto  
    ultimately show ?thesis
      by (metis add_left_cancel more_arith_simps(3) more_arith_simps(7))    
  qed
  have sa_tb_d: "?s*a+?t*b = ?d"
  proof -
    have "?d = (i = 0..<2. (if i = 0 then a else b) * Q $$ (i, 0))"
      unfolding times_mat_def col_def scalar_prod_def by auto
    also have "... = (i  {0,1}. (if i = 0 then a else b) * Q $$ (i, 0))" by (rule sum.cong, auto)
    also have "... = ?s*a+?t*b" by auto
    finally show ?thesis by simp
  qed
  have det_Q_dvd_1: "(Determinant.det Q dvd 1)"
    using invertible_iff_is_unit_JNF[OF Q] inv_Q by auto
  moreover have det_Q_eq: "Determinant.det Q = ?s*?a1 + ?t*?b1" unfolding det_2[OF Q] by simp
  ultimately have "?s*?a1 + ?t*?b1 dvd 1" by auto
  from this obtain u where u_eq: "?s*?a1 + ?t*?b1 = u" and u: "u dvd 1" by auto
  hence eq1: "?s*?a1*a + ?t*?b1*a = u*a"
    by (metis ring_class.ring_distribs(2))
  hence "?s*?a1*a + ?t*?a1*b = u*a"
    by (metis (no_types, lifting) ab1_ba1 mult.assoc mult.commute)
  hence a1d_ua:"?a1*?d=u*a"
    by (smt Groups.mult_ac(2) distrib_left more_arith_simps(11) sa_tb_d)
  hence b1d_ub: "?b1*?d=u*b"
    by (smt Groups.mult_ac(2) Groups.mult_ac(3) ab1_ba1 distrib_right sa_tb_d u_eq)
  obtain inv_u where inv_u: "inv_u * u = 1" using u unfolding dvd_def
    by (metis mult.commute)
  hence inv_u_dvd_1: "inv_u dvd 1" unfolding dvd_def by auto
  have cond1: "(inv_u*?b1)*?d = b" using b1d_ub inv_u
    by (metis (no_types, lifting) Groups.mult_ac(3) more_arith_simps(11) more_arith_simps(6))
  have cond2: "(inv_u*?a1)*?d = a" using a1d_ua inv_u
    by (metis (no_types, lifting) Groups.mult_ac(3) more_arith_simps(11) more_arith_simps(6))
  have "ideal_generated {inv_u*?a1, inv_u*?b1} = ideal_generated {?a1,?b1}"
    by (rule ideal_generated_mult_unit2[OF inv_u_dvd_1])    
  also have "... = UNIV" using ideal_generated_pair_UNIV[OF u_eq u] by simp
  finally have cond3: "ideal_generated {inv_u*?a1, inv_u*?b1} = ideal_generated {1}" by auto
  show "a1 b1 d. a = a1 * d  b = b1 * d  ideal_generated {a1, b1} = ideal_generated {1}"
    by (rule exI[of _ "inv_u*?a1"], rule exI[of _ "inv_u*?b1"], rule exI[of _ ?d],
        insert cond1 cond2 cond3, auto)
qed


lemma Hermite_ring_imp_Bezout_ring:
  assumes H: "OFCLASS('a::comm_ring_1, Hermite_ring_class)"
  shows "OFCLASS('a::comm_ring_1, bezout_ring_class)"
proof (intro_classes)
  fix a b::'a
  let ?A = "Matrix.mat 1 2 (λ(i,j). if i = 0  j = 0 then a else b)"
  have *: "((A::'a::comm_ring_1 mat). admits_triangular_reduction A)"
    using OFCLASS_Hermite_ring_def[where ?'a='a] H by auto
  have "admits_triangular_reduction ?A"
    using H unfolding OFCLASS_Hermite_ring_def by auto
  have " a1 b1 d. a = a1*d  b = b1*d  ideal_generated {a1,b1} = ideal_generated {1}"
    using theorem3_restricted_12_part2 * by auto
  from this obtain a1 b1 d where a_a'd: "a = a1*d" and b_b'd: "b = b1*d"
    and a'b'_1: "ideal_generated {a1,b1} = ideal_generated {1}"
    by blast
  obtain p q where "p * a1 + q * b1 = 1" using a'b'_1
    using ideal_generated_pair_exists_UNIV by blast
  hence pa_qb_d: "p * a + q * b = d" unfolding a_a'd b_b'd
    by (metis mult.assoc mult_1 ring_class.ring_distribs(2))
  moreover have d_dvd_a: "d dvd a" using a_a'd by auto
  moreover have d_dvd_b: "d dvd b" using b_b'd by auto    
  moreover have "(d'. d' dvd a  d' dvd b  d' dvd d)" using pa_qb_d by force
  ultimately show "p q d. p * a + q * b = d  d dvd a  d dvd b
         (d'. d' dvd a  d' dvd b  d' dvd d)" by blast
qed

end