[STATEMENT]
lemma HMA_diagonal_to_Smith_i_PQ_aux: "HMA_M3 (P,A,Q)
  (P' :: 'a :: bezout_ring ^ 'nr :: mod_type ^ 'nr :: mod_type,
   A' :: 'a :: bezout_ring ^ 'nc :: mod_type ^ 'nr :: mod_type,
   Q' :: 'a :: bezout_ring ^ 'nc :: mod_type ^ 'nc :: mod_type)
  \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P,A,Q))
             (diagonal_to_Smith_i_PQ xs i bezout (P',A',Q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (P, A, Q) (P', A', Q') \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ xs i bezout (P', A', Q'))
[PROOF STEP]
using i xs
[PROOF STATE]
proof (prove)
using this:
i < min CARD('nr) CARD('nc)
\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. HMA_M3 (P, A, Q) (P', A', Q') \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ xs i bezout (P', A', Q'))
[PROOF STEP]
proof (induct xs i bezout "(P',A',Q')" arbitrary: P' A' Q' P A Q rule: diagonal_to_Smith_i_PQ.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i bezout P A Q Pa Aa Qa. \<lbrakk>HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set []. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF [] i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ [] i bezout (P, A, Q))
 2. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
case (1 i bezout P' A' Q')
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, A, Q) (P', A', Q')
i < min CARD('nr) CARD('nc)
\<forall>j\<in>set []. j < min CARD('nr) CARD('nc)

goal (2 subgoals):
 1. \<And>i bezout P A Q Pa Aa Qa. \<lbrakk>HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set []. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF [] i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ [] i bezout (P, A, Q))
 2. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
HMA_M3 (P, A, Q) (P', A', Q')
i < min CARD('nr) CARD('nc)
\<forall>j\<in>set []. j < min CARD('nr) CARD('nc)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (P, A, Q) (P', A', Q')
i < min CARD('nr) CARD('nc)
\<forall>j\<in>set []. j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF [] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [] i bezout (P', A', Q'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF [] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [] i bezout (P', A', Q'))

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
case (2 j xs i bezout P' A' Q')
[PROOF STATE]
proof (state)
this:
\<lbrakk>A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j; HMA_M3 (?P, ?A, ?Q) (P', A', Q'); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (?P, ?A, ?Q)) (diagonal_to_Smith_i_PQ xs i bezout (P', A', Q'))
\<lbrakk>\<not> A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j; ?x = bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat j $h from_nat j); (?xa, ?y) = ?x; (?xb, ?ya) = ?y; (?xc, ?yb) = ?ya; (?xd, ?yc) = ?yb; ?xe = diagonal_step A' i j ?yc ?xd; ?xf = diagonal_step_PQ A' i j bezout; (?xg, ?yd) = ?xf; HMA_M3 (?P, ?A, ?Q) (?xg ** P', ?xe, Q' ** ?yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (?P, ?A, ?Q)) (diagonal_to_Smith_i_PQ xs i bezout (?xg ** P', ?xe, Q' ** ?yd))
HMA_M3 (P, A, Q) (P', A', Q')
i < min CARD('nr) CARD('nc)
\<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
note HMA_M3[transfer_rule] = "2.prems"(1)
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
note i = 2(4)
[PROOF STATE]
proof (state)
this:
i < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
note j = 2(5)
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
note IH1="2.hyps"(1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j; HMA_M3 (?P, ?A, ?Q) (P', A', Q'); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (?P, ?A, ?Q)) (diagonal_to_Smith_i_PQ xs i bezout (P', A', Q'))

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
note IH2="2.hyps"(2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<not> A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j; ?x = bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat j $h from_nat j); (?xa, ?y) = ?x; (?xb, ?ya) = ?y; (?xc, ?yb) = ?ya; (?xd, ?yc) = ?yb; ?xe = diagonal_step A' i j ?yc ?xd; ?xf = diagonal_step_PQ A' i j bezout; (?xg, ?yd) = ?xf; HMA_M3 (?P, ?A, ?Q) (?xg ** P', ?xe, Q' ** ?yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (?P, ?A, ?Q)) (diagonal_to_Smith_i_PQ xs i bezout (?xg ** P', ?xe, Q' ** ?yd))

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
have j_min: "j < min CARD('nr) CARD('nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < min CARD('nr) CARD('nc)
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. j < min CARD('nr) CARD('nc)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
have HMA_M_AA'[transfer_rule]: "Mod_Type_Connect.HMA_M A A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M A A'
[PROOF STEP]
using HMA_M3
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M A A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_I j (from_nat j::'nc)"
    and [transfer_rule]: "Mod_Type_Connect.HMA_I j (from_nat j::'nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_I j (from_nat j) &&& Mod_Type_Connect.HMA_I j (from_nat j)
[PROOF STEP]
by (metis Mod_Type_Connect.HMA_I_def j_min min.strict_boundedE to_nat_from_nat_id)+
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_I j (from_nat j)
Mod_Type_Connect.HMA_I j (from_nat j)

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_I i (from_nat i::'nc)"
    and [transfer_rule]: "Mod_Type_Connect.HMA_I i (from_nat i::'nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_I i (from_nat i) &&& Mod_Type_Connect.HMA_I i (from_nat i)
[PROOF STEP]
by (metis Mod_Type_Connect.HMA_I_def i min.strict_boundedE to_nat_from_nat_id)+
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_I i (from_nat i)
Mod_Type_Connect.HMA_I i (from_nat i)

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
have [transfer_rule]: "A $$ (i, i) = A' $h from_nat i $h from_nat i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
have "A $$ (i,i) = index_hma A' (from_nat i) (from_nat i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (i, i) = index_hma A' (from_nat i) (from_nat i)
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = index_hma A' (from_nat i) (from_nat i)

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = index_hma A' (from_nat i) (from_nat i)

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
have "... = A' $h from_nat i $h from_nat i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index_hma A' (from_nat i) (from_nat i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
unfolding index_hma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $h from_nat i $h from_nat i = A' $h from_nat i $h from_nat i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index_hma A' (from_nat i) (from_nat i) = A' $h from_nat i $h from_nat i

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A $$ (i, i) = A' $h from_nat i $h from_nat i

goal (1 subgoal):
 1. A $$ (i, i) = A' $h from_nat i $h from_nat i
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = A' $h from_nat i $h from_nat i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $$ (i, i) = A' $h from_nat i $h from_nat i

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
have [transfer_rule]: "A $$ (j, j) = A' $h from_nat j $h from_nat j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (j, j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $$ (j, j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
have "A $$ (j,j) = index_hma A' (from_nat j) (from_nat j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (j, j) = index_hma A' (from_nat j) (from_nat j)
[PROOF STEP]
by (transfer, simp)
[PROOF STATE]
proof (state)
this:
A $$ (j, j) = index_hma A' (from_nat j) (from_nat j)

goal (1 subgoal):
 1. A $$ (j, j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
A $$ (j, j) = index_hma A' (from_nat j) (from_nat j)

goal (1 subgoal):
 1. A $$ (j, j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
have "... = A' $h from_nat j $h from_nat j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. index_hma A' (from_nat j) (from_nat j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
unfolding index_hma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $h from_nat j $h from_nat j = A' $h from_nat j $h from_nat j
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
index_hma A' (from_nat j) (from_nat j) = A' $h from_nat j $h from_nat j

goal (1 subgoal):
 1. A $$ (j, j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
A $$ (j, j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A $$ (j, j) = A' $h from_nat j $h from_nat j

goal (1 subgoal):
 1. A $$ (j, j) = A' $h from_nat j $h from_nat j
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $$ (j, j) = A' $h from_nat j $h from_nat j

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $$ (j, j) = A' $h from_nat j $h from_nat j

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (P, A, Q)); \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $h from_nat i $h from_nat i dvd A $h from_nat j $h from_nat j; x = bezout (A $h from_nat i $h from_nat i) (A $h from_nat j $h from_nat j); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step A i j yc xd; xf = diagonal_step_PQ A i j bezout; (xg, yd) = xf; HMA_M3 (Pa, Aa, Qa) (xg ** P, xe, Q ** yd); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ xs i bezout (xg ** P, xe, Q ** yd)); HMA_M3 (Pa, Aa, Qa) (P, A, Q); i < min CARD('nr) CARD('nc); \<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (Pa, Aa, Qa)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P, A, Q))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
proof (cases "A $$ (i, i) dvd A $$ (j, j)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
 2. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
A $$ (i, i) dvd A $$ (j, j)

goal (2 subgoals):
 1. A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
 2. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
hence "A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, i) dvd A $$ (j, j)

goal (1 subgoal):
 1. A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j
[PROOF STEP]
by transfer
[PROOF STATE]
proof (state)
this:
A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j

goal (2 subgoals):
 1. A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
 2. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
using True IH1 HMA_M3 i j
[PROOF STATE]
proof (prove)
using this:
A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j
A $$ (i, i) dvd A $$ (j, j)
\<lbrakk>A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j; HMA_M3 (?P, ?A, ?Q) (P', A', Q'); i < min CARD('nr) CARD('nc); \<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (?P, ?A, ?Q)) (diagonal_to_Smith_i_PQ xs i bezout (P', A', Q'))
HMA_M3 (P, A, Q) (P', A', Q')
i < min CARD('nr) CARD('nc)
\<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> A $$ (i, i) dvd A $$ (j, j)

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
obtain p q u v d where b: "(p, q, u, v, d) = bezout (A $$ (i,i)) (A $$ (j,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p q u v d. (p, q, u, v, d) = bezout (A $$ (i, i)) (A $$ (j, j)) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis prod_cases5)
[PROOF STATE]
proof (state)
this:
(p, q, u, v, d) = bezout (A $$ (i, i)) (A $$ (j, j))

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
let ?A'_JNF = "diagonal_step_JNF A i j d v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
obtain P''_JNF Q''_JNF where P''Q''_JNF: "(P''_JNF,Q''_JNF) = diagonal_step_PQ_JNF A i j bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P''_JNF Q''_JNF. (P''_JNF, Q''_JNF) = diagonal_step_PQ_JNF A i j bezout \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surjective_pairing)
[PROOF STATE]
proof (state)
this:
(P''_JNF, Q''_JNF) = diagonal_step_PQ_JNF A i j bezout

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
have not_dvd: "\<not> A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
\<not> A $$ (i, i) dvd A $$ (j, j)

goal (1 subgoal):
 1. \<not> A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j
[PROOF STEP]
by transfer
[PROOF STATE]
proof (state)
this:
\<not> A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
let ?A' = "diagonal_step A' i j d v"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
obtain P'' Q'' where P''Q'': "(P'',Q'') = diagonal_step_PQ A' i j bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'' Q''. (P'', Q'') = diagonal_step_PQ A' i j bezout \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surjective_pairing)
[PROOF STATE]
proof (state)
this:
(P'', Q'') = diagonal_step_PQ A' i j bezout

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
have b2: "(p, q, u, v, d) = bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat j $h from_nat j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p, q, u, v, d) = bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat j $h from_nat j)
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
(p, q, u, v, d) = bezout (A $$ (i, i)) (A $$ (j, j))

goal (1 subgoal):
 1. (p, q, u, v, d) = bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat j $h from_nat j)
[PROOF STEP]
by (transfer,auto)
[PROOF STATE]
proof (state)
this:
(p, q, u, v, d) = bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat j $h from_nat j)

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
let ?D_HA = "diagonal_to_Smith_i_PQ xs i bezout (P''**P',?A',Q'**Q'')"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
let ?D_JNF = "diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF*P,?A'_JNF,Q*Q''_JNF)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
have rw_1: "diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = ?D_JNF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)
[PROOF STEP]
using False b P''Q''_JNF
[PROOF STATE]
proof (prove)
using this:
\<not> A $$ (i, i) dvd A $$ (j, j)
(p, q, u, v, d) = bezout (A $$ (i, i)) (A $$ (j, j))
(P''_JNF, Q''_JNF) = diagonal_step_PQ_JNF A i j bezout

goal (1 subgoal):
 1. diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)
[PROOF STEP]
by (auto, unfold split_beta, metis fst_conv snd_conv)
[PROOF STATE]
proof (state)
this:
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
have rw_2: "diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q') = ?D_HA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q') = diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q'')
[PROOF STEP]
using not_dvd b2 P''Q''
[PROOF STATE]
proof (prove)
using this:
\<not> A' $h from_nat i $h from_nat i dvd A' $h from_nat j $h from_nat j
(p, q, u, v, d) = bezout (A' $h from_nat i $h from_nat i) (A' $h from_nat j $h from_nat j)
(P'', Q'') = diagonal_step_PQ A' i j bezout

goal (1 subgoal):
 1. diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q') = diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q'')
[PROOF STEP]
by (auto, unfold split_beta, metis fst_conv snd_conv)
[PROOF STATE]
proof (state)
this:
diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q') = diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q'')

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
have "HMA_M3 ?D_JNF ?D_HA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)) (diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q''))
[PROOF STEP]
proof (rule IH2[OF not_dvd b2], auto)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')
 3. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
 4. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 5. i < CARD('nr)
 6. i < CARD('nc)
 7. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 8. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
have j: "j < min CARD('nr) CARD('nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < min CARD('nr) CARD('nc)
[PROOF STEP]
using j
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>set (j # xs). j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. j < min CARD('nr) CARD('nc)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < min CARD('nr) CARD('nc)

goal (8 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')
 3. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
 4. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 5. i < CARD('nr)
 6. i < CARD('nc)
 7. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 8. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
have [transfer_rule]: "rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M
       (diagonal_step_PQ_JNF A i j bezout) (diagonal_step_PQ A' i j bezout)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i j bezout) (diagonal_step_PQ A' i j bezout)
[PROOF STEP]
using HMA_diagonal_step_PQ[OF i j] HMA_M_AA'
[PROOF STATE]
proof (prove)
using this:
(Mod_Type_Connect.HMA_M ===> (=) ===> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M) (\<lambda>A. diagonal_step_PQ_JNF A i j) (\<lambda>A. diagonal_step_PQ A i j)
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i j bezout) (diagonal_step_PQ A' i j bezout)
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. Mod_Type_Connect.HMA_M x y \<longrightarrow> (\<forall>xa ya. xa = ya \<longrightarrow> rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF x i j xa) (diagonal_step_PQ y i j ya))
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i j bezout) (diagonal_step_PQ A' i j bezout)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i j bezout) (diagonal_step_PQ A' i j bezout)

goal (8 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')
 3. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
 4. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 5. i < CARD('nr)
 6. i < CARD('nc)
 7. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 8. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
hence [transfer_rule]: "Mod_Type_Connect.HMA_M P''_JNF P''"
        and [transfer_rule]: "Mod_Type_Connect.HMA_M Q''_JNF Q''"
[PROOF STATE]
proof (prove)
using this:
rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i j bezout) (diagonal_step_PQ A' i j bezout)

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M P''_JNF P'' &&& Mod_Type_Connect.HMA_M Q''_JNF Q''
[PROOF STEP]
using P''Q'' P''Q''_JNF
[PROOF STATE]
proof (prove)
using this:
rel_prod Mod_Type_Connect.HMA_M Mod_Type_Connect.HMA_M (diagonal_step_PQ_JNF A i j bezout) (diagonal_step_PQ A' i j bezout)
(P'', Q'') = diagonal_step_PQ A' i j bezout
(P''_JNF, Q''_JNF) = diagonal_step_PQ_JNF A i j bezout

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M P''_JNF P'' &&& Mod_Type_Connect.HMA_M Q''_JNF Q''
[PROOF STEP]
unfolding rel_prod_conv split_beta
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M (fst (diagonal_step_PQ_JNF A i j bezout)) (fst (diagonal_step_PQ A' i j bezout)) \<and> Mod_Type_Connect.HMA_M (snd (diagonal_step_PQ_JNF A i j bezout)) (snd (diagonal_step_PQ A' i j bezout))
(P'', Q'') = diagonal_step_PQ A' i j bezout
(P''_JNF, Q''_JNF) = diagonal_step_PQ_JNF A i j bezout

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M P''_JNF P'' &&& Mod_Type_Connect.HMA_M Q''_JNF Q''
[PROOF STEP]
by (metis fst_conv, metis snd_conv)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M P''_JNF P''
Mod_Type_Connect.HMA_M Q''_JNF Q''

goal (8 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')
 3. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
 4. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 5. i < CARD('nr)
 6. i < CARD('nc)
 7. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 8. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_M P P'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M P P'
[PROOF STEP]
using HMA_M3
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M P P'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M P P'

goal (8 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')
 3. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
 4. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 5. i < CARD('nr)
 6. i < CARD('nc)
 7. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 8. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
show "Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')
[PROOF STEP]
(* apply (transfer, auto) does not finish the goal*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')
[PROOF STEP]
by (transfer_prover_start, transfer_step+, auto)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')

goal (7 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
 3. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 4. i < CARD('nr)
 5. i < CARD('nc)
 6. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 7. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
(* note HMA_diagonal_step[OF i j,transfer_rule]*)
     (*transfer does not work for the following goal*)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (P''_JNF * P) (P'' ** P')

goal (7 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
 3. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 4. i < CARD('nr)
 5. i < CARD('nc)
 6. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 7. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
show "Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
[PROOF STEP]
using HMA_diagonal_step[OF i j] HMA_M_AA'
[PROOF STATE]
proof (prove)
using this:
(Mod_Type_Connect.HMA_M ===> (=) ===> (=) ===> Mod_Type_Connect.HMA_M) (\<lambda>A. diagonal_step_JNF A i j) (\<lambda>B. diagonal_step B i j)
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. Mod_Type_Connect.HMA_M x y \<longrightarrow> (\<forall>xa ya. xa = ya \<longrightarrow> (\<forall>xb yb. xb = yb \<longrightarrow> Mod_Type_Connect.HMA_M (diagonal_step_JNF x i j xa xb) (diagonal_step y i j ya yb)))
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (diagonal_step_JNF A i j d v) (diagonal_step A' i j d v)

goal (6 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 3. i < CARD('nr)
 4. i < CARD('nc)
 5. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 6. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_M Q Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M Q Q'
[PROOF STEP]
using HMA_M3
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M Q Q'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M Q Q'

goal (6 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
 3. i < CARD('nr)
 4. i < CARD('nc)
 5. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 6. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
show "Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')
[PROOF STEP]
by (transfer_prover_start, transfer_step+, auto)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (Q * Q''_JNF) (Q' ** Q'')

goal (5 subgoals):
 1. (P'', Q'') = diagonal_step_PQ A' i j bezout
 2. i < CARD('nr)
 3. i < CARD('nc)
 4. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nr)
 5. \<And>j. j \<in> set xs \<Longrightarrow> j < CARD('nc)
[PROOF STEP]
qed (insert i j P''Q'', auto)
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)) (diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q''))

goal (1 subgoal):
 1. \<not> A $$ (i, i) dvd A $$ (j, j) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)) (diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q''))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)) (diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q''))

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
using rw_1 rw_2
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)) (diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q''))
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = diagonal_to_Smith_i_PQ_JNF xs i bezout (P''_JNF * P, diagonal_step_JNF A i j d v, Q * Q''_JNF)
diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q') = diagonal_to_Smith_i_PQ xs i bezout (P'' ** P', diagonal_step A' i j d v, Q' ** Q'')

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ (j # xs) i bezout (P', A', Q'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HMA_diagonal_to_Smith_i_PQ[transfer_rule]:
  "((=)
  ===> (HMA_M3 :: (_ \<Rightarrow> (_\<times>('a :: bezout_ring ^ 'nc :: mod_type ^ 'nr :: mod_type) \<times> _) \<Rightarrow>_))
  ===> HMA_M3) (diagonal_to_Smith_i_PQ_JNF xs i) (diagonal_to_Smith_i_PQ xs i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> HMA_M3 ===> HMA_M3) (diagonal_to_Smith_i_PQ_JNF xs i) (diagonal_to_Smith_i_PQ xs i)
[PROOF STEP]
proof (intro rel_funI, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; HMA_M3 xa ya\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i x xa) (diagonal_to_Smith_i_PQ xs i y ya)
[PROOF STEP]
case (1 x y bezout bezout')
[PROOF STATE]
proof (state)
this:
x = y
HMA_M3 bezout bezout'

goal (1 subgoal):
 1. \<And>x y xa ya. \<lbrakk>x = y; HMA_M3 xa ya\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i x xa) (diagonal_to_Smith_i_PQ xs i y ya)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x = y
HMA_M3 bezout bezout'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
x = y
HMA_M3 bezout bezout'

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i x bezout) (diagonal_to_Smith_i_PQ xs i y bezout')
[PROOF STEP]
using HMA_diagonal_to_Smith_i_PQ_aux
[PROOF STATE]
proof (prove)
using this:
x = y
HMA_M3 bezout bezout'
HMA_M3 (?P, ?A, ?Q) (?P', ?A', ?Q') \<Longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i ?bezout (?P, ?A, ?Q)) (diagonal_to_Smith_i_PQ xs i ?bezout (?P', ?A', ?Q'))

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i x bezout) (diagonal_to_Smith_i_PQ xs i y bezout')
[PROOF STEP]
by (auto, smt HMA_M3.elims(2))
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF xs i x bezout) (diagonal_to_Smith_i_PQ xs i y bezout')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HMA_Diagonal_to_Smith_row_i_PQ[transfer_rule]:
  "((=) ===> (HMA_M3 :: (_ \<Rightarrow> (_ \<times> ('a::bezout_ring^'nc::mod_type^'nr::mod_type) \<times> _) \<Rightarrow> _)) ===> HMA_M3)
  (Diagonal_to_Smith_row_i_PQ_JNF i) (Diagonal_to_Smith_row_i_PQ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> HMA_M3 ===> HMA_M3) (Diagonal_to_Smith_row_i_PQ_JNF i) (Diagonal_to_Smith_row_i_PQ i)
[PROOF STEP]
proof (intro rel_funI, clarify, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
case (1 _ bezout P A Q P' A' Q')
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
note HMA_M3[transfer_rule] = 1
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
let ?xs1="[i + 1..<min (dim_row A) (dim_col A)]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
let ?xs2="[i + 1..<min (nrows A') (ncols A')]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
have xs_eq[transfer_rule]: "?xs1 = ?xs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [i + 1..<min (dim_row A) (dim_col A)] = [i + 1..<min (nrows A') (ncols A')]
[PROOF STEP]
using HMA_M3
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. [i + 1..<min (dim_row A) (dim_col A)] = [i + 1..<min (nrows A') (ncols A')]
[PROOF STEP]
by (auto intro: arg_cong2[where f = upt]
        simp: Mod_Type_Connect.dim_col_transfer_rule Mod_Type_Connect.dim_row_transfer_rule
        nrows_def ncols_def)
[PROOF STATE]
proof (state)
this:
[i + 1..<min (dim_row A) (dim_col A)] = [i + 1..<min (nrows A') (ncols A')]

goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
have j_xs: "\<forall>j\<in>set ?xs1. j < min CARD('nr) CARD('nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>set [i + 1..<min (dim_row A) (dim_col A)]. j < min CARD('nr) CARD('nc)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
i < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. \<forall>j\<in>set [i + 1..<min (dim_row A) (dim_col A)]. j < min CARD('nr) CARD('nc)
[PROOF STEP]
by (metis atLeastLessThan_iff ncols_def nrows_def set_upt xs_eq)
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>set [i + 1..<min (dim_row A) (dim_col A)]. j < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
have rel: "HMA_M3 (diagonal_to_Smith_i_PQ_JNF ?xs1 i bezout (P,A,Q))
            (diagonal_to_Smith_i_PQ ?xs1 i bezout (P',A',Q'))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i bezout (P', A', Q'))
[PROOF STEP]
using HMA_diagonal_to_Smith_i_PQ[OF i j_xs] HMA_M3
[PROOF STATE]
proof (prove)
using this:
((=) ===> HMA_M3 ===> HMA_M3) (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i)
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i bezout (P', A', Q'))
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x = y \<longrightarrow> (\<forall>xa ya. HMA_M3 xa ya \<longrightarrow> HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i x xa) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i y ya))
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i bezout (P', A', Q'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i bezout (P', A', Q'))

goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i y (a, aa, b)) (Diagonal_to_Smith_row_i_PQ i y (ab, ac, ba))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i bezout (P', A', Q'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i bezout (P', A', Q'))

goal (1 subgoal):
 1. HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))
[PROOF STEP]
unfolding Diagonal_to_Smith_row_i_PQ_JNF_def Diagonal_to_Smith_row_i_PQ_def
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (dim_row A) (dim_col A)] i bezout (P', A', Q'))

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_i_PQ_JNF [i + 1..<min (dim_row A) (dim_col A)] i bezout (P, A, Q)) (diagonal_to_Smith_i_PQ [i + 1..<min (nrows A') (ncols A')] i bezout (P', A', Q'))
[PROOF STEP]
by (metis Suc_eq_plus1 xs_eq)
[PROOF STATE]
proof (state)
this:
HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma HMA_diagonal_to_Smith_aux_PQ_JNF[transfer_rule]:
  "((=) ===> (HMA_M3 :: (_ \<Rightarrow> (_ \<times> ('a::bezout_ring^'nc::mod_type^'nr::mod_type) \<times> _) \<Rightarrow> _)) ===> HMA_M3)
  (diagonal_to_Smith_aux_PQ_JNF xs) (diagonal_to_Smith_aux_PQ xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> HMA_M3 ===> HMA_M3) (diagonal_to_Smith_aux_PQ_JNF xs) (diagonal_to_Smith_aux_PQ xs)
[PROOF STEP]
proof (intro rel_funI, clarify, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs y (a, aa, b)) (diagonal_to_Smith_aux_PQ xs y (ab, ac, ba))
[PROOF STEP]
case (1 _ bezout P A Q P' A' Q')
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs y (a, aa, b)) (diagonal_to_Smith_aux_PQ xs y (ab, ac, ba))
[PROOF STEP]
note HMA_M3[transfer_rule] = 1
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. \<And>x y a aa b ab ac ba. HMA_M3 (a, aa, b) (ab, ac, ba) \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs y (a, aa, b)) (diagonal_to_Smith_aux_PQ xs y (ab, ac, ba))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q'))
[PROOF STEP]
using xs HMA_M3
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc)
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q'))
[PROOF STEP]
proof (induct xs arbitrary: P' A' Q' P A Q)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set []. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [] bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ [] bezout (P', A', Q'))
 2. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>set []. j < min CARD('nr) CARD('nc)
HMA_M3 (P, A, Q) (P', A', Q')

goal (2 subgoals):
 1. \<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set []. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [] bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ [] bezout (P', A', Q'))
 2. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>j\<in>set []. j < min CARD('nr) CARD('nc)
HMA_M3 (P, A, Q) (P', A', Q')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>set []. j < min CARD('nr) CARD('nc)
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [] bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ [] bezout (P', A', Q'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [] bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ [] bezout (P', A', Q'))

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
case (Cons i xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (?P, ?A, ?Q) (?P', ?A', ?Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (?P, ?A, ?Q)) (diagonal_to_Smith_aux_PQ xs bezout (?P', ?A', ?Q'))
\<forall>j\<in>set (i # xs). j < min CARD('nr) CARD('nc)
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
note IH = Cons(1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (?P, ?A, ?Q) (?P', ?A', ?Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (?P, ?A, ?Q)) (diagonal_to_Smith_aux_PQ xs bezout (?P', ?A', ?Q'))

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
note HMA_M3 = Cons.prems(2)
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
have i: "i < min CARD('nr) CARD('nc)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < min CARD('nr) CARD('nc)
[PROOF STEP]
using Cons.prems
[PROOF STATE]
proof (prove)
using this:
\<forall>j\<in>set (i # xs). j < min CARD('nr) CARD('nc)
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. i < min CARD('nr) CARD('nc)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < min CARD('nr) CARD('nc)

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
let ?D_JNF = "(Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
let ?D_HA = "(Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
have rw_1: "diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q)
        = diagonal_to_Smith_aux_PQ_JNF xs bezout ?D_JNF"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = diagonal_to_Smith_aux_PQ_JNF xs bezout (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = diagonal_to_Smith_aux_PQ_JNF xs bezout (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q))

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
have rw_2: "diagonal_to_Smith_aux_PQ (i # xs) bezout (P', A', Q')
        = diagonal_to_Smith_aux_PQ xs bezout ?D_HA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagonal_to_Smith_aux_PQ (i # xs) bezout (P', A', Q') = diagonal_to_Smith_aux_PQ xs bezout (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
diagonal_to_Smith_aux_PQ (i # xs) bezout (P', A', Q') = diagonal_to_Smith_aux_PQ xs bezout (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
have "HMA_M3 ?D_JNF ?D_HA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))
[PROOF STEP]
using HMA_Diagonal_to_Smith_row_i_PQ[OF i] HMA_M3
[PROOF STATE]
proof (prove)
using this:
((=) ===> HMA_M3 ===> HMA_M3) (Diagonal_to_Smith_row_i_PQ_JNF i) (Diagonal_to_Smith_row_i_PQ i)
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))
[PROOF STEP]
unfolding rel_fun_def
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. x = y \<longrightarrow> (\<forall>xa ya. HMA_M3 xa ya \<longrightarrow> HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i x xa) (Diagonal_to_Smith_row_i_PQ i y ya))
HMA_M3 (P, A, Q) (P', A', Q')

goal (1 subgoal):
 1. HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))

goal (1 subgoal):
 1. \<And>a xs P' A' Q' P A Q. \<lbrakk>\<And>P' A' Q' P A Q. \<lbrakk>\<forall>j\<in>set xs. j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q')); \<forall>j\<in>set (a # xs). j < min CARD('nr) CARD('nc); HMA_M3 (P, A, Q) (P', A', Q')\<rbrakk> \<Longrightarrow> HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (a # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (a # xs) bezout (P', A', Q'))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q)) (Diagonal_to_Smith_row_i_PQ i bezout (P', A', Q'))

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (i # xs) bezout (P', A', Q'))
[PROOF STEP]
by (auto, smt Cons.hyps HMA_M3.elims(2) list.set_intros(2) local.Cons(2))
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ (i # xs) bezout (P', A', Q'))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF xs bezout (P, A, Q)) (diagonal_to_Smith_aux_PQ xs bezout (P', A', Q'))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_step_PQ_JNF_dim:
  assumes A: "A \<in> carrier_mat m n"
    and d: "diagonal_step_PQ_JNF A i j bezout = (P,Q)"
  shows "P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using A d
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat m n
diagonal_step_PQ_JNF A i j bezout = (P, Q)

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n
[PROOF STEP]
unfolding diagonal_step_PQ_JNF_def split_beta Let_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat m n
(addrow (- fst (snd (snd (snd (bezout (A $$ (i, i)) (A $$ (j, j))))))) j i (swaprows i j (addrow (fst (bezout (A $$ (i, i)) (A $$ (j, j)))) j i (1\<^sub>m (dim_row A)))), multcol j (- (1::'a)) (addcol (fst (snd (snd (bezout (A $$ (i, i)) (A $$ (j, j)))))) j i (addcol (fst (snd (bezout (A $$ (i, i)) (A $$ (j, j))))) i j (1\<^sub>m (dim_col A))))) = (P, Q)

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by auto


[STATEMENT]
lemma diagonal_step_JNF_dim:
  assumes A: "A \<in> carrier_mat m n"
  shows "diagonal_step_JNF A i j d v \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagonal_step_JNF A i j d v \<in> carrier_mat m n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat m n

goal (1 subgoal):
 1. diagonal_step_JNF A i j d v \<in> carrier_mat m n
[PROOF STEP]
unfolding diagonal_step_JNF_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat m n

goal (1 subgoal):
 1. Matrix.mat (dim_row A) (dim_col A) (\<lambda>(a, b). if a = i \<and> b = i then d else if a = j \<and> b = j then v * A $$ (j, j) else A $$ (a, b)) \<in> carrier_mat m n
[PROOF STEP]
by auto