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

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
proof (induct xs i bezout "(P',A',Q')" arbitrary: P A Q P' A' Q' rule: diagonal_to_Smith_i_PQ_JNF.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i bezout P A Q Pa Aa Qa. \<lbrakk>P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF [] i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
 2. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $$ (i, i) dvd A $$ (j, j); P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $$ (i, i) dvd A $$ (j, j); x = bezout (A $$ (i, i)) (A $$ (j, j)); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step_JNF A i j yc xd; xf = diagonal_step_PQ_JNF A i j bezout; (xg, yd) = xf; xg * P \<in> carrier_mat m m \<and> xe \<in> carrier_mat m n \<and> Q * yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (xg * P, xe, Q * yd) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
case (1 i bezout P A Q)
[PROOF STATE]
proof (state)
this:
Pa__ \<in> carrier_mat m m \<and> Aa__ \<in> carrier_mat m n \<and> Qa__ \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF [] i bezout (Pa__, Aa__, Qa__) = (P, A, Q)

goal (2 subgoals):
 1. \<And>i bezout P A Q Pa Aa Qa. \<lbrakk>P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF [] i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
 2. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $$ (i, i) dvd A $$ (j, j); P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $$ (i, i) dvd A $$ (j, j); x = bezout (A $$ (i, i)) (A $$ (j, j)); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step_JNF A i j yc xd; xf = diagonal_step_PQ_JNF A i j bezout; (xg, yd) = xf; xg * P \<in> carrier_mat m m \<and> xe \<in> carrier_mat m n \<and> Q * yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (xg * P, xe, Q * yd) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Pa__ \<in> carrier_mat m m \<and> Aa__ \<in> carrier_mat m n \<and> Qa__ \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF [] i bezout (Pa__, Aa__, Qa__) = (P, A, Q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Pa__ \<in> carrier_mat m m \<and> Aa__ \<in> carrier_mat m n \<and> Qa__ \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF [] i bezout (Pa__, Aa__, Qa__) = (P, A, Q)

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

goal (1 subgoal):
 1. \<And>j xs i bezout P A Q Pa Aa Qa. \<lbrakk>\<And>Pa Aa Qa. \<lbrakk>A $$ (i, i) dvd A $$ (j, j); P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $$ (i, i) dvd A $$ (j, j); x = bezout (A $$ (i, i)) (A $$ (j, j)); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step_JNF A i j yc xd; xf = diagonal_step_PQ_JNF A i j bezout; (xg, yd) = xf; xg * P \<in> carrier_mat m m \<and> xe \<in> carrier_mat m n \<and> Q * yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (xg * P, xe, Q * yd) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[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 $$ (i, i) dvd A $$ (j, j); P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $$ (i, i) dvd A $$ (j, j); x = bezout (A $$ (i, i)) (A $$ (j, j)); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step_JNF A i j yc xd; xf = diagonal_step_PQ_JNF A i j bezout; (xg, yd) = xf; xg * P \<in> carrier_mat m m \<and> xe \<in> carrier_mat m n \<and> Q * yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (xg * P, xe, Q * yd) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
case (2 j xs i bezout P' A' Q')
[PROOF STATE]
proof (state)
this:
\<lbrakk>A' $$ (i, i) dvd A' $$ (j, j); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P', A', Q') = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
\<lbrakk>\<not> A' $$ (i, i) dvd A' $$ (j, j); ?x = bezout (A' $$ (i, i)) (A' $$ (j, j)); (?xa, ?y) = ?x; (?xb, ?ya) = ?y; (?xc, ?yb) = ?ya; (?xd, ?yc) = ?yb; ?xe = diagonal_step_JNF A' i j ?yc ?xd; ?xf = diagonal_step_PQ_JNF A' i j bezout; (?xg, ?yd) = ?xf; ?xg * P' \<in> carrier_mat m m \<and> ?xe \<in> carrier_mat m n \<and> Q' * ?yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (?xg * P', ?xe, Q' * ?yd) = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (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 $$ (i, i) dvd A $$ (j, j); P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; \<And>x xa y xb ya xc yb xd yc xe xf xg yd Pa Aa Qa. \<lbrakk>\<not> A $$ (i, i) dvd A $$ (j, j); x = bezout (A $$ (i, i)) (A $$ (j, j)); (xa, y) = x; (xb, ya) = y; (xc, yb) = ya; (xd, yc) = yb; xe = diagonal_step_JNF A i j yc xd; xf = diagonal_step_PQ_JNF A i j bezout; (xg, yd) = xf; xg * P \<in> carrier_mat m m \<and> xe \<in> carrier_mat m n \<and> Q * yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (xg * P, xe, Q * yd) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[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> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
 2. \<not> A' $$ (i, i) dvd A' $$ (j, j) \<Longrightarrow> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[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> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
 2. \<not> A' $$ (i, i) dvd A' $$ (j, j) \<Longrightarrow> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A' $$ (i, i) dvd A' $$ (j, j)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
A' $$ (i, i) dvd A' $$ (j, j)

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
A' $$ (i, i) dvd A' $$ (j, j)
\<lbrakk>A' $$ (i, i) dvd A' $$ (j, j); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P', A', Q') = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
\<lbrakk>\<not> A' $$ (i, i) dvd A' $$ (j, j); ?x = bezout (A' $$ (i, i)) (A' $$ (j, j)); (?xa, ?y) = ?x; (?xb, ?ya) = ?y; (?xc, ?yb) = ?ya; (?xd, ?yc) = ?yb; ?xe = diagonal_step_JNF A' i j ?yc ?xd; ?xf = diagonal_step_PQ_JNF A' i j bezout; (?xg, ?yd) = ?xf; ?xg * P' \<in> carrier_mat m m \<and> ?xe \<in> carrier_mat m n \<and> Q' * ?yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (?xg * P', ?xe, Q' * ?yd) = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P', A', Q') = (P, A, Q)

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

goal (1 subgoal):
 1. \<not> A' $$ (i, i) dvd A' $$ (j, j) \<Longrightarrow> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> A' $$ (i, i) dvd A' $$ (j, j) \<Longrightarrow> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[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> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[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> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
let ?A' = "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> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
obtain P'' Q'' where P''Q'': "(P'',Q'') = diagonal_step_PQ_JNF A' i j bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'' Q''. (P'', Q'') = diagonal_step_PQ_JNF A' i j bezout \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis surjective_pairing)
[PROOF STATE]
proof (state)
this:
(P'', Q'') = diagonal_step_PQ_JNF A' i j bezout

goal (1 subgoal):
 1. \<not> A' $$ (i, i) dvd A' $$ (j, j) \<Longrightarrow> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
let ?A' = "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> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
let ?D_JNF = "diagonal_to_Smith_i_PQ_JNF 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> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[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'' * P', diagonal_step_JNF A' i j d v, Q' * Q'')
[PROOF STEP]
using False b P''Q''
[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'', Q'') = 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'' * P', diagonal_step_JNF 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_JNF (j # xs) i bezout (P', A', Q') = diagonal_to_Smith_i_PQ_JNF xs i bezout (P'' * P', diagonal_step_JNF A' i j d v, Q' * Q'')

goal (1 subgoal):
 1. \<not> A' $$ (i, i) dvd A' $$ (j, j) \<Longrightarrow> P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
proof (rule "2.hyps"(2)[OF False b])
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. (?xa, ?y) = (p, q, u, v, d)
 2. (?xb, ?ya) = ?y
 3. (?xc, ?yb) = ?ya
 4. (?xd, ?yc) = ?yb
 5. ?xe = diagonal_step_JNF A' i j ?yc ?xd
 6. ?xf = diagonal_step_PQ_JNF A' i j bezout
 7. (?xg, ?yd) = ?xf
 8. ?xg * P' \<in> carrier_mat m m \<and> ?xe \<in> carrier_mat m n \<and> Q' * ?yd \<in> carrier_mat n n
 9. diagonal_to_Smith_i_PQ_JNF xs i bezout (?xg * P', ?xe, Q' * ?yd) = (P, A, Q)
[PROOF STEP]
show "?D_JNF = (P,A,Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagonal_to_Smith_i_PQ_JNF xs i bezout (P'' * P', diagonal_step_JNF A' i j d v, Q' * Q'') = (P, A, Q)
[PROOF STEP]
using rw_1 2
[PROOF STATE]
proof (prove)
using this:
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P', A', Q') = diagonal_to_Smith_i_PQ_JNF xs i bezout (P'' * P', diagonal_step_JNF A' i j d v, Q' * Q'')
\<lbrakk>A' $$ (i, i) dvd A' $$ (j, j); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P', A', Q') = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
\<lbrakk>\<not> A' $$ (i, i) dvd A' $$ (j, j); ?x = bezout (A' $$ (i, i)) (A' $$ (j, j)); (?xa, ?y) = ?x; (?xb, ?ya) = ?y; (?xc, ?yb) = ?ya; (?xd, ?yc) = ?yb; ?xe = diagonal_step_JNF A' i j ?yc ?xd; ?xf = diagonal_step_PQ_JNF A' i j bezout; (?xg, ?yd) = ?xf; ?xg * P' \<in> carrier_mat m m \<and> ?xe \<in> carrier_mat m n \<and> Q' * ?yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (?xg * P', ?xe, Q' * ?yd) = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P', A', Q') = (P, A, Q)

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

goal (8 subgoals):
 1. (?xa, ?y) = (p, q, u, v, d)
 2. (?xb, ?ya) = ?y
 3. (?xc, ?yb) = ?ya
 4. (?xd, ?yc) = ?yb
 5. diagonal_step_JNF A' i j d v = diagonal_step_JNF A' i j ?yc ?xd
 6. ?xf = diagonal_step_PQ_JNF A' i j bezout
 7. (P'', Q'') = ?xf
 8. P'' * P' \<in> carrier_mat m m \<and> diagonal_step_JNF A' i j d v \<in> carrier_mat m n \<and> Q' * Q'' \<in> carrier_mat n n
[PROOF STEP]
have "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 &&& Q'' \<in> carrier_mat n n
[PROOF STEP]
using diagonal_step_PQ_JNF_dim[OF _ P''Q''[symmetric]] "2.prems"
[PROOF STATE]
proof (prove)
using this:
A' \<in> carrier_mat ?m ?n \<Longrightarrow> P'' \<in> carrier_mat ?m ?m \<and> Q'' \<in> carrier_mat ?n ?n
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P', A', Q') = (P, A, Q)

goal (1 subgoal):
 1. P'' \<in> carrier_mat m m &&& Q'' \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P'' \<in> carrier_mat m m
Q'' \<in> carrier_mat n n

goal (8 subgoals):
 1. (?xa, ?y) = (p, q, u, v, d)
 2. (?xb, ?ya) = ?y
 3. (?xc, ?yb) = ?ya
 4. (?xd, ?yc) = ?yb
 5. diagonal_step_JNF A' i j d v = diagonal_step_JNF A' i j ?yc ?xd
 6. ?xf = diagonal_step_PQ_JNF A' i j bezout
 7. (P'', Q'') = ?xf
 8. P'' * P' \<in> carrier_mat m m \<and> diagonal_step_JNF A' i j d v \<in> carrier_mat m n \<and> Q' * Q'' \<in> carrier_mat n n
[PROOF STEP]
thus "P'' * P' \<in> carrier_mat m m \<and> ?A' \<in> carrier_mat m n \<and> Q' * Q'' \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
using this:
P'' \<in> carrier_mat m m
Q'' \<in> carrier_mat n n

goal (1 subgoal):
 1. P'' * P' \<in> carrier_mat m m \<and> diagonal_step_JNF A' i j d v \<in> carrier_mat m n \<and> Q' * Q'' \<in> carrier_mat n n
[PROOF STEP]
using diagonal_step_JNF_dim 2
[PROOF STATE]
proof (prove)
using this:
P'' \<in> carrier_mat m m
Q'' \<in> carrier_mat n n
?A \<in> carrier_mat ?m ?n \<Longrightarrow> diagonal_step_JNF ?A ?i ?j ?d ?v \<in> carrier_mat ?m ?n
\<lbrakk>A' $$ (i, i) dvd A' $$ (j, j); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (P', A', Q') = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
\<lbrakk>\<not> A' $$ (i, i) dvd A' $$ (j, j); ?x = bezout (A' $$ (i, i)) (A' $$ (j, j)); (?xa, ?y) = ?x; (?xb, ?ya) = ?y; (?xc, ?yb) = ?ya; (?xd, ?yc) = ?yb; ?xe = diagonal_step_JNF A' i j ?yc ?xd; ?xf = diagonal_step_PQ_JNF A' i j bezout; (?xg, ?yd) = ?xf; ?xg * P' \<in> carrier_mat m m \<and> ?xe \<in> carrier_mat m n \<and> Q' * ?yd \<in> carrier_mat n n; diagonal_to_Smith_i_PQ_JNF xs i bezout (?xg * P', ?xe, Q' * ?yd) = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_i_PQ_JNF (j # xs) i bezout (P', A', Q') = (P, A, Q)

goal (1 subgoal):
 1. P'' * P' \<in> carrier_mat m m \<and> diagonal_step_JNF A' i j d v \<in> carrier_mat m n \<and> Q' * Q'' \<in> carrier_mat n n
[PROOF STEP]
by (metis mult_carrier_mat)
[PROOF STATE]
proof (state)
this:
P'' * P' \<in> carrier_mat m m \<and> diagonal_step_JNF A' i j d v \<in> carrier_mat m n \<and> Q' * Q'' \<in> carrier_mat n n

goal (7 subgoals):
 1. (?xa, ?y) = (p, q, u, v, d)
 2. (?xb, ?ya) = ?y
 3. (?xc, ?yb) = ?ya
 4. (?xd, ?yc) = ?yb
 5. diagonal_step_JNF A' i j d v = diagonal_step_JNF A' i j ?yc ?xd
 6. ?xf = diagonal_step_PQ_JNF A' i j bezout
 7. (P'', Q'') = ?xf
[PROOF STEP]
qed (insert P''Q'', auto)
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Diagonal_to_Smith_row_i_PQ_JNF_dim:
  assumes "P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n"
    and "Diagonal_to_Smith_row_i_PQ_JNF i bezout (P',A',Q') = (P,A,Q)"
  shows "P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by (rule diagonal_to_Smith_i_PQ_JNF_dim, insert assms,
      auto simp add: Diagonal_to_Smith_row_i_PQ_JNF_def)


[STATEMENT]
lemma diagonal_to_Smith_aux_PQ_JNF_dim:
  assumes "P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n"
    and "diagonal_to_Smith_aux_PQ_JNF xs bezout (P',A',Q') = (P,A,Q)"
  shows "P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (P, A, Q)

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
proof (induct xs bezout "(P',A',Q')" arbitrary: P A Q P' A' Q' rule: diagonal_to_Smith_aux_PQ_JNF.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>bezout P A Q Pa Aa Qa. \<lbrakk>P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF [] bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
 2. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
case (1 bezout P A Q)
[PROOF STATE]
proof (state)
this:
Pa__ \<in> carrier_mat m m \<and> Aa__ \<in> carrier_mat m n \<and> Qa__ \<in> carrier_mat n n
diagonal_to_Smith_aux_PQ_JNF [] bezout (Pa__, Aa__, Qa__) = (P, A, Q)

goal (2 subgoals):
 1. \<And>bezout P A Q Pa Aa Qa. \<lbrakk>P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF [] bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
 2. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Pa__ \<in> carrier_mat m m \<and> Aa__ \<in> carrier_mat m n \<and> Qa__ \<in> carrier_mat n n
diagonal_to_Smith_aux_PQ_JNF [] bezout (Pa__, Aa__, Qa__) = (P, A, Q)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Pa__ \<in> carrier_mat m m \<and> Aa__ \<in> carrier_mat m n \<and> Qa__ \<in> carrier_mat n n
diagonal_to_Smith_aux_PQ_JNF [] bezout (Pa__, Aa__, Qa__) = (P, A, Q)

goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n

goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
case (2 i xs bezout P' A' Q')
[PROOF STATE]
proof (state)
this:
\<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q') = (?P', ?A', ?Q'); ?P' \<in> carrier_mat m m \<and> ?A' \<in> carrier_mat m n \<and> ?Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (?P', ?A', ?Q') = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P', A', Q') = (P, A, Q)

goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
let ?D="(Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
have "diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P', A', Q') =
      diagonal_to_Smith_aux_PQ_JNF xs bezout ?D"
[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>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
hence *: "... = (P,A,Q)"
[PROOF STATE]
proof (prove)
using 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. diagonal_to_Smith_aux_PQ_JNF xs bezout (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')) = (P, A, Q)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using 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'))
\<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q') = (?P', ?A', ?Q'); ?P' \<in> carrier_mat m m \<and> ?A' \<in> carrier_mat m n \<and> ?Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (?P', ?A', ?Q') = (?P, ?A, ?Q)\<rbrakk> \<Longrightarrow> ?P \<in> carrier_mat m m \<and> ?A \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n
diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P', A', Q') = (P, A, Q)

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

goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
let ?P="fst ?D"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
let ?S="fst (snd ?D)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
let ?Q="snd (snd ?D)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i xs bezout P A Q Pa Aa Qa. \<lbrakk>\<And>P' A' Q' Pa Aa Qa. \<lbrakk>Diagonal_to_Smith_row_i_PQ_JNF i bezout (P, A, Q) = (P', A', Q'); P' \<in> carrier_mat m m \<and> A' \<in> carrier_mat m n \<and> Q' \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF xs bezout (P', A', Q') = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n; P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n; diagonal_to_Smith_aux_PQ_JNF (i # xs) bezout (P, A, Q) = (Pa, Aa, Qa)\<rbrakk> \<Longrightarrow> Pa \<in> carrier_mat m m \<and> Aa \<in> carrier_mat m n \<and> Qa \<in> carrier_mat n n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
proof (rule "2.hyps")
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q') = (?P', ?A', ?Q')
 2. ?P' \<in> carrier_mat m m \<and> ?A' \<in> carrier_mat m n \<and> ?Q' \<in> carrier_mat n n
 3. diagonal_to_Smith_aux_PQ_JNF xs bezout (?P', ?A', ?Q') = (P, A, Q)
[PROOF STEP]
show "Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q') = (?P,?S,?Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q') = (fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')), fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))), snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q') = (fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')), fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))), snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))))

goal (2 subgoals):
 1. fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')) \<in> carrier_mat m m \<and> fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat m n \<and> snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat n n
 2. diagonal_to_Smith_aux_PQ_JNF xs bezout (fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')), fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))), snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')))) = (P, A, Q)
[PROOF STEP]
show "diagonal_to_Smith_aux_PQ_JNF xs bezout (?P, ?S, ?Q) = (P, A, Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. diagonal_to_Smith_aux_PQ_JNF xs bezout (fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')), fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))), snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')))) = (P, A, Q)
[PROOF STEP]
using *
[PROOF STATE]
proof (prove)
using this:
diagonal_to_Smith_aux_PQ_JNF xs bezout (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')) = (P, A, Q)

goal (1 subgoal):
 1. diagonal_to_Smith_aux_PQ_JNF xs bezout (fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')), fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))), snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')))) = (P, A, Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
diagonal_to_Smith_aux_PQ_JNF xs bezout (fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')), fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))), snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')))) = (P, A, Q)

goal (1 subgoal):
 1. fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')) \<in> carrier_mat m m \<and> fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat m n \<and> snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat n n
[PROOF STEP]
show "?P \<in> carrier_mat m m \<and> ?S \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')) \<in> carrier_mat m m \<and> fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat m n \<and> snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat n n
[PROOF STEP]
by (rule Diagonal_to_Smith_row_i_PQ_JNF_dim, insert 2, auto)
[PROOF STATE]
proof (state)
this:
fst (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q')) \<in> carrier_mat m m \<and> fst (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat m n \<and> snd (snd (Diagonal_to_Smith_row_i_PQ_JNF i bezout (P', A', Q'))) \<in> carrier_mat n n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat m m \<and> A \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_dim:
  assumes "A \<in> carrier_mat m n"
    and PSQ: "diagonal_to_Smith_PQ_JNF A bezout = (P,S,Q)"
  shows "P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by (rule diagonal_to_Smith_aux_PQ_JNF_dim, insert assms,
      auto simp add: diagonal_to_Smith_PQ_JNF_def)


[STATEMENT]
lemma HMA_diagonal_to_Smith_PQ_JNF[transfer_rule]:
 "((Mod_Type_Connect.HMA_M) ===> (=) ===> HMA_M3) (diagonal_to_Smith_PQ_JNF) (diagonal_to_Smith_PQ)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Mod_Type_Connect.HMA_M ===> (=) ===> HMA_M3) diagonal_to_Smith_PQ_JNF diagonal_to_Smith_PQ
[PROOF STEP]
proof (intro rel_funI, clarify, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
case (1 A A' _ bezout)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
let ?xs1 = "[0..<min (dim_row A) (dim_col A) - 1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
let ?xs2 = "[0..<min (nrows A') (ncols A') - 1]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
let ?PAQ="(1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
have dr: "dim_row A = CARD('c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A = CARD('c)
[PROOF STEP]
using 1 Mod_Type_Connect.dim_row_transfer_rule
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M A A'
Mod_Type_Connect.HMA_M ?A ?A' \<Longrightarrow> dim_row ?A = CARD(?'nr)

goal (1 subgoal):
 1. dim_row A = CARD('c)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dim_row A = CARD('c)

goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
have dc: "dim_col A = CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_col A = CARD('b)
[PROOF STEP]
using 1 Mod_Type_Connect.dim_col_transfer_rule
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M A A'
Mod_Type_Connect.HMA_M ?A ?A' \<Longrightarrow> dim_col ?A = CARD(?'nc)

goal (1 subgoal):
 1. dim_col A = CARD('b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
dim_col A = CARD('b)

goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
have xs_eq: "?xs1 = ?xs2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [0..<min (dim_row A) (dim_col A) - 1] = [0..<min (nrows A') (ncols A') - 1]
[PROOF STEP]
by (simp add: dc dr ncols_def nrows_def)
[PROOF STATE]
proof (state)
this:
[0..<min (dim_row A) (dim_col A) - 1] = [0..<min (nrows A') (ncols A') - 1]

goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
have j_xs: "\<forall>j\<in>set ?xs1. j < min CARD('c) CARD('b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j\<in>set [0..<min (dim_row A) (dim_col A) - 1]. j < min CARD('c) CARD('b)
[PROOF STEP]
using dc dr less_imp_diff_less
[PROOF STATE]
proof (prove)
using this:
dim_col A = CARD('b)
dim_row A = CARD('c)
?j < ?k \<Longrightarrow> ?j - ?n < ?k

goal (1 subgoal):
 1. \<forall>j\<in>set [0..<min (dim_row A) (dim_col A) - 1]. j < min CARD('c) CARD('b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>j\<in>set [0..<min (dim_row A) (dim_col A) - 1]. j < min CARD('c) CARD('b)

goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
let ?D_JNF = "diagonal_to_Smith_aux_PQ_JNF ?xs1 bezout ?PAQ"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
let ?D_HA = "diagonal_to_Smith_aux_PQ ?xs1 bezout (mat 1, A', mat 1)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
have mat_rel_init: "HMA_M3 ?PAQ (mat 1, A', mat 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))
[PROOF STEP]
have "Mod_Type_Connect.HMA_M (1\<^sub>m (dim_row A)) (mat 1::'a^'c::mod_type^'c::mod_type)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (1\<^sub>m (dim_row A)) (mat (1::'a))
[PROOF STEP]
unfolding dr
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (1\<^sub>m CARD('c)) (mat (1::'a))
[PROOF STEP]
by (transfer_prover_start,transfer_step, auto)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_row A)) (mat (1::'a))

goal (1 subgoal):
 1. HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_row A)) (mat (1::'a))

goal (1 subgoal):
 1. HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))
[PROOF STEP]
have "Mod_Type_Connect.HMA_M (1\<^sub>m (dim_col A)) (mat 1::'a^'b::mod_type^'b::mod_type)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (1\<^sub>m (dim_col A)) (mat (1::'a))
[PROOF STEP]
unfolding dc
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M (1\<^sub>m CARD('b)) (mat (1::'a))
[PROOF STEP]
by (transfer_prover_start,transfer_step, auto)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_col A)) (mat (1::'a))

goal (1 subgoal):
 1. HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_row A)) (mat (1::'a))
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_col A)) (mat (1::'a))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_row A)) (mat (1::'a))
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_col A)) (mat (1::'a))

goal (1 subgoal):
 1. HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_row A)) (mat (1::'a))
Mod_Type_Connect.HMA_M (1\<^sub>m (dim_col A)) (mat (1::'a))
Mod_Type_Connect.HMA_M A A'

goal (1 subgoal):
 1. HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))

goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
have "HMA_M3 ?D_JNF ?D_HA"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))
[PROOF STEP]
using HMA_diagonal_to_Smith_aux_PQ_JNF[OF j_xs] mat_rel_init
[PROOF STATE]
proof (prove)
using this:
((=) ===> HMA_M3 ===> HMA_M3) (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1]) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1])
HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))
[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_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] x xa) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] y ya))
HMA_M3 (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A)) (mat (1::'a), A', mat (1::'a))

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))

goal (1 subgoal):
 1. \<And>x y xa ya. Mod_Type_Connect.HMA_M x y \<Longrightarrow> HMA_M3 (diagonal_to_Smith_PQ_JNF x ya) (diagonal_to_Smith_PQ y ya)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_PQ_JNF A bezout) (diagonal_to_Smith_PQ A' bezout)
[PROOF STEP]
using xs_eq
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))
[0..<min (dim_row A) (dim_col A) - 1] = [0..<min (nrows A') (ncols A') - 1]

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_PQ_JNF A bezout) (diagonal_to_Smith_PQ A' bezout)
[PROOF STEP]
unfolding diagonal_to_Smith_PQ_JNF_def diagonal_to_Smith_PQ_def
[PROOF STATE]
proof (prove)
using this:
HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (dim_row A) (dim_col A) - 1] bezout (mat (1::'a), A', mat (1::'a)))
[0..<min (dim_row A) (dim_col A) - 1] = [0..<min (nrows A') (ncols A') - 1]

goal (1 subgoal):
 1. HMA_M3 (diagonal_to_Smith_aux_PQ_JNF [0..<min (dim_row A) (dim_col A) - 1] bezout (1\<^sub>m (dim_row A), A, 1\<^sub>m (dim_col A))) (diagonal_to_Smith_aux_PQ [0..<min (nrows A') (ncols A') - 1] bezout (mat (1::'a), A', mat (1::'a)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
HMA_M3 (diagonal_to_Smith_PQ_JNF A bezout) (diagonal_to_Smith_PQ A' bezout)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_with_types:
  assumes A: "A \<in> carrier_mat CARD('nr::mod_type) CARD('nc::mod_type)"
  and S: "S \<in> carrier_mat CARD('nr) CARD('nc)"
  and P: "P \<in> carrier_mat CARD('nr) CARD('nr)"
  and Q: "Q \<in> carrier_mat CARD('nc) CARD('nc)"
  and PSQ: "diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q)"
  and d:"isDiagonal_mat A" and ib: "is_bezout_ext bezout"
shows "S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
let ?P = "Mod_Type_Connect.to_hma\<^sub>m P::'a^'nr::mod_type^'nr::mod_type"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
let ?A = "Mod_Type_Connect.to_hma\<^sub>m A::'a^'nc::mod_type^'nr::mod_type"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
let ?Q = "Mod_Type_Connect.to_hma\<^sub>m Q::'a^'nc::mod_type^'nc::mod_type"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
let ?S = "Mod_Type_Connect.to_hma\<^sub>m S::'a^'nc::mod_type^'nr::mod_type"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_M A ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M A (Mod_Type_Connect.to_hma\<^sub>m A)
[PROOF STEP]
by (simp add: Mod_Type_Connect.HMA_M_def A)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M A (Mod_Type_Connect.to_hma\<^sub>m A)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M A (Mod_Type_Connect.to_hma\<^sub>m A)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[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 (Mod_Type_Connect.to_hma\<^sub>m P)
[PROOF STEP]
by (simp add: Mod_Type_Connect.HMA_M_def P)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M P (Mod_Type_Connect.to_hma\<^sub>m P)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M P (Mod_Type_Connect.to_hma\<^sub>m P)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[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 (Mod_Type_Connect.to_hma\<^sub>m Q)
[PROOF STEP]
by (simp add: Mod_Type_Connect.HMA_M_def Q)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M Q (Mod_Type_Connect.to_hma\<^sub>m Q)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M Q (Mod_Type_Connect.to_hma\<^sub>m Q)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
have [transfer_rule]: "Mod_Type_Connect.HMA_M S ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.HMA_M S (Mod_Type_Connect.to_hma\<^sub>m S)
[PROOF STEP]
by (simp add: Mod_Type_Connect.HMA_M_def S)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.HMA_M S (Mod_Type_Connect.to_hma\<^sub>m S)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Mod_Type_Connect.HMA_M A (Mod_Type_Connect.to_hma\<^sub>m A)
Mod_Type_Connect.HMA_M P (Mod_Type_Connect.to_hma\<^sub>m P)
Mod_Type_Connect.HMA_M Q (Mod_Type_Connect.to_hma\<^sub>m Q)
Mod_Type_Connect.HMA_M S (Mod_Type_Connect.to_hma\<^sub>m S)
[PROOF STEP]
have [transfer_rule]: "HMA_M3 (P,S,Q) (?P,?S,?Q)"
[PROOF STATE]
proof (prove)
using this:
Mod_Type_Connect.HMA_M A (Mod_Type_Connect.to_hma\<^sub>m A)
Mod_Type_Connect.HMA_M P (Mod_Type_Connect.to_hma\<^sub>m P)
Mod_Type_Connect.HMA_M Q (Mod_Type_Connect.to_hma\<^sub>m Q)
Mod_Type_Connect.HMA_M S (Mod_Type_Connect.to_hma\<^sub>m S)

goal (1 subgoal):
 1. HMA_M3 (P, S, Q) (Mod_Type_Connect.to_hma\<^sub>m P, Mod_Type_Connect.to_hma\<^sub>m S, Mod_Type_Connect.to_hma\<^sub>m Q)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
HMA_M3 (P, S, Q) (Mod_Type_Connect.to_hma\<^sub>m P, Mod_Type_Connect.to_hma\<^sub>m S, Mod_Type_Connect.to_hma\<^sub>m Q)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
have [transfer_rule]: "bezout = bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bezout = bezout
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
bezout = bezout

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
have PSQ2: "(?P,?S,?Q) = diagonal_to_Smith_PQ ?A bezout"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Mod_Type_Connect.to_hma\<^sub>m P, Mod_Type_Connect.to_hma\<^sub>m S, Mod_Type_Connect.to_hma\<^sub>m Q) = diagonal_to_Smith_PQ (Mod_Type_Connect.to_hma\<^sub>m A) bezout
[PROOF STEP]
by (transfer, insert PSQ, auto)
[PROOF STATE]
proof (state)
this:
(Mod_Type_Connect.to_hma\<^sub>m P, Mod_Type_Connect.to_hma\<^sub>m S, Mod_Type_Connect.to_hma\<^sub>m Q) = diagonal_to_Smith_PQ (Mod_Type_Connect.to_hma\<^sub>m A) bezout

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
have "?S = ?P**?A**?Q \<and> invertible ?P \<and> invertible ?Q \<and> Smith_normal_form ?S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Mod_Type_Connect.to_hma\<^sub>m S = Mod_Type_Connect.to_hma\<^sub>m P ** Mod_Type_Connect.to_hma\<^sub>m A ** Mod_Type_Connect.to_hma\<^sub>m Q \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m P) \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m Q) \<and> Smith_normal_form (Mod_Type_Connect.to_hma\<^sub>m S)
[PROOF STEP]
by (rule diagonal_to_Smith_PQ'[OF _ ib PSQ2], transfer, auto simp add: d)
[PROOF STATE]
proof (state)
this:
Mod_Type_Connect.to_hma\<^sub>m S = Mod_Type_Connect.to_hma\<^sub>m P ** Mod_Type_Connect.to_hma\<^sub>m A ** Mod_Type_Connect.to_hma\<^sub>m Q \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m P) \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m Q) \<and> Smith_normal_form (Mod_Type_Connect.to_hma\<^sub>m S)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
with this[untransferred]
[PROOF STATE]
proof (chain)
picking this:
S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
Mod_Type_Connect.to_hma\<^sub>m S = Mod_Type_Connect.to_hma\<^sub>m P ** Mod_Type_Connect.to_hma\<^sub>m A ** Mod_Type_Connect.to_hma\<^sub>m Q \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m P) \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m Q) \<and> Smith_normal_form (Mod_Type_Connect.to_hma\<^sub>m S)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
Mod_Type_Connect.to_hma\<^sub>m S = Mod_Type_Connect.to_hma\<^sub>m P ** Mod_Type_Connect.to_hma\<^sub>m A ** Mod_Type_Connect.to_hma\<^sub>m Q \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m P) \<and> invertible (Mod_Type_Connect.to_hma\<^sub>m Q) \<and> Smith_normal_form (Mod_Type_Connect.to_hma\<^sub>m S)

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_mod_ring_with_types:
  assumes A: "A \<in> carrier_mat CARD('nr::nontriv mod_ring) CARD('nc::nontriv mod_ring)"
  and S: "S \<in> carrier_mat CARD('nr mod_ring) CARD('nc mod_ring)"
  and P: "P \<in> carrier_mat CARD('nr mod_ring) CARD('nr mod_ring)"
  and Q: "Q \<in> carrier_mat CARD('nc mod_ring) CARD('nc mod_ring)"
  and PSQ: "diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q)"
  and d:"isDiagonal_mat A" and ib: "is_bezout_ext bezout"
shows "S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
by (rule diagonal_to_Smith_PQ_JNF_with_types[OF assms])


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_internalized_first:
  "class.nontriv TYPE('a::type) \<Longrightarrow>
  A \<in> carrier_mat CARD('a) CARD('nc::nontriv) \<Longrightarrow>
  S \<in> carrier_mat CARD('a) CARD('nc) \<Longrightarrow>
  P \<in> carrier_mat CARD('a) CARD('a) \<Longrightarrow>
  Q \<in> carrier_mat CARD('nc) CARD('nc) \<Longrightarrow>
  diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q) \<Longrightarrow>
  isDiagonal_mat A \<Longrightarrow> is_bezout_ext bezout \<Longrightarrow>
  S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.nontriv TYPE('a); A \<in> carrier_mat CARD('a) CARD('nc); S \<in> carrier_mat CARD('a) CARD('nc); P \<in> carrier_mat CARD('a) CARD('a); Q \<in> carrier_mat CARD('nc) CARD('nc); diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q); isDiagonal_mat A; is_bezout_ext bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
using diagonal_to_Smith_PQ_JNF_mod_ring_with_types[unfolded CARD_mod_ring,
      internalize_sort "'nr::nontriv"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>class.nontriv TYPE(?'a); ?A \<in> carrier_mat CARD(?'a) CARD(?'c); ?S \<in> carrier_mat CARD(?'a) CARD(?'c); ?P \<in> carrier_mat CARD(?'a) CARD(?'a); ?Q \<in> carrier_mat CARD(?'c) CARD(?'c); diagonal_to_Smith_PQ_JNF ?A ?bezout = (?P, ?S, ?Q); isDiagonal_mat ?A; is_bezout_ext ?bezout\<rbrakk> \<Longrightarrow> ?S = ?P * ?A * ?Q \<and> invertible_mat ?P \<and> invertible_mat ?Q \<and> Smith_normal_form_mat ?S

goal (1 subgoal):
 1. \<lbrakk>class.nontriv TYPE('a); A \<in> carrier_mat CARD('a) CARD('nc); S \<in> carrier_mat CARD('a) CARD('nc); P \<in> carrier_mat CARD('a) CARD('a); Q \<in> carrier_mat CARD('nc) CARD('nc); diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q); isDiagonal_mat A; is_bezout_ext bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
by blast


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_internalized:
  "class.nontriv TYPE('c::type) \<Longrightarrow>
  class.nontriv TYPE('a::type) \<Longrightarrow>
  A \<in> carrier_mat CARD('a) CARD('c) \<Longrightarrow>
  S \<in> carrier_mat CARD('a) CARD('c) \<Longrightarrow>
  P \<in> carrier_mat CARD('a) CARD('a) \<Longrightarrow>
  Q \<in> carrier_mat CARD('c) CARD('c) \<Longrightarrow>
  diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q) \<Longrightarrow>
  isDiagonal_mat A \<Longrightarrow> is_bezout_ext bezout \<Longrightarrow>
S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.nontriv TYPE('c); class.nontriv TYPE('a); A \<in> carrier_mat CARD('a) CARD('c); S \<in> carrier_mat CARD('a) CARD('c); P \<in> carrier_mat CARD('a) CARD('a); Q \<in> carrier_mat CARD('c) CARD('c); diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q); isDiagonal_mat A; is_bezout_ext bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
using diagonal_to_Smith_PQ_JNF_internalized_first[internalize_sort "'nc::nontriv"]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>class.nontriv TYPE(?'a); class.nontriv TYPE(?'aa); ?A \<in> carrier_mat CARD(?'aa) CARD(?'a); ?S \<in> carrier_mat CARD(?'aa) CARD(?'a); ?P \<in> carrier_mat CARD(?'aa) CARD(?'aa); ?Q \<in> carrier_mat CARD(?'a) CARD(?'a); diagonal_to_Smith_PQ_JNF ?A ?bezout = (?P, ?S, ?Q); isDiagonal_mat ?A; is_bezout_ext ?bezout\<rbrakk> \<Longrightarrow> ?S = ?P * ?A * ?Q \<and> invertible_mat ?P \<and> invertible_mat ?Q \<and> Smith_normal_form_mat ?S

goal (1 subgoal):
 1. \<lbrakk>class.nontriv TYPE('c); class.nontriv TYPE('a); A \<in> carrier_mat CARD('a) CARD('c); S \<in> carrier_mat CARD('a) CARD('c); P \<in> carrier_mat CARD('a) CARD('a); Q \<in> carrier_mat CARD('c) CARD('c); diagonal_to_Smith_PQ_JNF A bezout = (P, S, Q); isDiagonal_mat A; is_bezout_ext bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
[PROOF STEP]
by blast


[STATEMENT]
lemma type_to_set1:
  shows "class.nontriv TYPE('b)" (is ?a) and "m=CARD('b)" (is ?b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.nontriv TYPE('b) &&& m = CARD('b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. class.nontriv TYPE('b)
 2. m = CARD('b)
[PROOF STEP]
from local_typedef1
[PROOF STATE]
proof (chain)
picking this:
\<exists>Rep Abs. type_definition Rep Abs {0..<int m}
[PROOF STEP]
obtain Rep::"('b \<Rightarrow> int)" and Abs
    where t: "type_definition Rep Abs {0..<m :: int}"
[PROOF STATE]
proof (prove)
using this:
\<exists>Rep Abs. type_definition Rep Abs {0..<int m}

goal (1 subgoal):
 1. (\<And>Rep Abs. type_definition Rep Abs {0..<int m} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
type_definition Rep Abs {0..<int m}

goal (2 subgoals):
 1. class.nontriv TYPE('b)
 2. m = CARD('b)
[PROOF STEP]
have "card (UNIV :: 'b set) = card {0..<m}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('b) = card {0..<m}
[PROOF STEP]
using t type_definition.card
[PROOF STATE]
proof (prove)
using this:
type_definition Rep Abs {0..<int m}
type_definition ?Rep ?Abs ?A \<Longrightarrow> CARD(?'b) = card ?A

goal (1 subgoal):
 1. CARD('b) = card {0..<m}
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
CARD('b) = card {0..<m}

goal (2 subgoals):
 1. class.nontriv TYPE('b)
 2. m = CARD('b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
CARD('b) = card {0..<m}

goal (2 subgoals):
 1. class.nontriv TYPE('b)
 2. m = CARD('b)
[PROOF STEP]
have "... = m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {0..<m} = m
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {0..<m} = m

goal (2 subgoals):
 1. class.nontriv TYPE('b)
 2. m = CARD('b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
CARD('b) = m
[PROOF STEP]
show ?b
[PROOF STATE]
proof (prove)
using this:
CARD('b) = m

goal (1 subgoal):
 1. m = CARD('b)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
m = CARD('b)

goal (1 subgoal):
 1. class.nontriv TYPE('b)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = CARD('b)
[PROOF STEP]
show ?a
[PROOF STATE]
proof (prove)
using this:
m = CARD('b)

goal (1 subgoal):
 1. class.nontriv TYPE('b)
[PROOF STEP]
unfolding class.nontriv_def
[PROOF STATE]
proof (prove)
using this:
m = CARD('b)

goal (1 subgoal):
 1. 1 < CARD('b)
[PROOF STEP]
using m
[PROOF STATE]
proof (prove)
using this:
m = CARD('b)
1 < m

goal (1 subgoal):
 1. 1 < CARD('b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
class.nontriv TYPE('b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma type_to_set2:
  shows "class.nontriv TYPE('c)" (is ?a) and "n=CARD('c)" (is ?b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. class.nontriv TYPE('c) &&& n = CARD('c)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. class.nontriv TYPE('c)
 2. n = CARD('c)
[PROOF STEP]
from local_typedef2
[PROOF STATE]
proof (chain)
picking this:
\<exists>Rep Abs. type_definition Rep Abs {0..<int n}
[PROOF STEP]
obtain Rep::"('c \<Rightarrow> int)" and Abs
    where t: "type_definition Rep Abs {0..<n :: int}"
[PROOF STATE]
proof (prove)
using this:
\<exists>Rep Abs. type_definition Rep Abs {0..<int n}

goal (1 subgoal):
 1. (\<And>Rep Abs. type_definition Rep Abs {0..<int n} \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
type_definition Rep Abs {0..<int n}

goal (2 subgoals):
 1. class.nontriv TYPE('c)
 2. n = CARD('c)
[PROOF STEP]
have "card (UNIV :: 'c set) = card {0..<n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. CARD('c) = card {0..<n}
[PROOF STEP]
using t type_definition.card
[PROOF STATE]
proof (prove)
using this:
type_definition Rep Abs {0..<int n}
type_definition ?Rep ?Abs ?A \<Longrightarrow> CARD(?'b) = card ?A

goal (1 subgoal):
 1. CARD('c) = card {0..<n}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
CARD('c) = card {0..<n}

goal (2 subgoals):
 1. class.nontriv TYPE('c)
 2. n = CARD('c)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
CARD('c) = card {0..<n}

goal (2 subgoals):
 1. class.nontriv TYPE('c)
 2. n = CARD('c)
[PROOF STEP]
have "... = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {0..<n} = n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card {0..<n} = n

goal (2 subgoals):
 1. class.nontriv TYPE('c)
 2. n = CARD('c)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
CARD('c) = n
[PROOF STEP]
show ?b
[PROOF STATE]
proof (prove)
using this:
CARD('c) = n

goal (1 subgoal):
 1. n = CARD('c)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
n = CARD('c)

goal (1 subgoal):
 1. class.nontriv TYPE('c)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n = CARD('c)
[PROOF STEP]
show ?a
[PROOF STATE]
proof (prove)
using this:
n = CARD('c)

goal (1 subgoal):
 1. class.nontriv TYPE('c)
[PROOF STEP]
unfolding class.nontriv_def
[PROOF STATE]
proof (prove)
using this:
n = CARD('c)

goal (1 subgoal):
 1. 1 < CARD('c)
[PROOF STEP]
using n
[PROOF STATE]
proof (prove)
using this:
n = CARD('c)
1 < n

goal (1 subgoal):
 1. 1 < CARD('c)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
class.nontriv TYPE('c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_local_typedef:
  assumes A: "isDiagonal_mat A" and ib: "is_bezout_ext bezout"
  and A_dim: "A \<in> carrier_mat m n"
  assumes PSQ: "(P,S,Q) = diagonal_to_Smith_PQ_JNF A bezout"
  shows "S = P*A*Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
  \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
have dim_matrices: "P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by (rule diagonal_to_Smith_PQ_JNF_dim[OF A_dim PSQ[symmetric]])
[PROOF STATE]
proof (state)
this:
P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using diagonal_to_Smith_PQ_JNF_internalized[where ?'c='c, where ?'a='b,
      OF type_to_set2(1) type_to_set(1), of m A S P Q]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>Rep Abs. type_definition Rep Abs {0..<int m}; 1 < m; A \<in> carrier_mat CARD('b) CARD('c); S \<in> carrier_mat CARD('b) CARD('c); P \<in> carrier_mat CARD('b) CARD('b); Q \<in> carrier_mat CARD('c) CARD('c); diagonal_to_Smith_PQ_JNF A ?bezout = (P, S, Q); isDiagonal_mat A; is_bezout_ext ?bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
unfolding type_to_set1(2)[symmetric] type_to_set2(2)[symmetric]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>Rep Abs. type_definition Rep Abs {0..<int m}; 1 < m; A \<in> carrier_mat m n; S \<in> carrier_mat m n; P \<in> carrier_mat m m; Q \<in> carrier_mat n n; diagonal_to_Smith_PQ_JNF A ?bezout = (P, S, Q); isDiagonal_mat A; is_bezout_ext ?bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using assms m dim_matrices local_typedef1
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<exists>Rep Abs. type_definition Rep Abs {0..<int m}; 1 < m; A \<in> carrier_mat m n; S \<in> carrier_mat m n; P \<in> carrier_mat m m; Q \<in> carrier_mat n n; diagonal_to_Smith_PQ_JNF A ?bezout = (P, S, Q); isDiagonal_mat A; is_bezout_ext ?bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
isDiagonal_mat A
is_bezout_ext bezout
A \<in> carrier_mat m n
(P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout
1 < m
P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
\<exists>Rep Abs. type_definition Rep Abs {0..<int m}

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_canceled_first:
  "\<exists>Rep Abs. type_definition Rep Abs {0..<int n} \<Longrightarrow> {0..<int m} \<noteq> {} \<Longrightarrow>
  1 < m \<Longrightarrow> 1 < n \<Longrightarrow> isDiagonal_mat A \<Longrightarrow> is_bezout_ext bezout \<Longrightarrow>
  A \<in> carrier_mat m n \<Longrightarrow> (P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout \<Longrightarrow>
  S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
  \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>Rep Abs. type_definition Rep Abs {0..<int n}; {0..<int m} \<noteq> {}; 1 < m; 1 < n; isDiagonal_mat A; is_bezout_ext bezout; A \<in> carrier_mat m n; (P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using diagonal_to_Smith_PQ_JNF_local_typedef[cancel_type_definition]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{0..<int ?m} \<noteq> {}; \<exists>Rep Abs. type_definition Rep Abs {0..<int ?n}; 1 < ?m; 1 < ?n; isDiagonal_mat ?A; is_bezout_ext ?bezout; ?A \<in> carrier_mat ?m ?n; (?P, ?S, ?Q) = diagonal_to_Smith_PQ_JNF ?A ?bezout\<rbrakk> \<Longrightarrow> ?S = ?P * ?A * ?Q \<and> invertible_mat ?P \<and> invertible_mat ?Q \<and> Smith_normal_form_mat ?S \<and> ?P \<in> carrier_mat ?m ?m \<and> ?S \<in> carrier_mat ?m ?n \<and> ?Q \<in> carrier_mat ?n ?n

goal (1 subgoal):
 1. \<lbrakk>\<exists>Rep Abs. type_definition Rep Abs {0..<int n}; {0..<int m} \<noteq> {}; 1 < m; 1 < n; isDiagonal_mat A; is_bezout_ext bezout; A \<in> carrier_mat m n; (P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by blast


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF_canceled_both:
  "{0..<int n} \<noteq> {} \<Longrightarrow> {0..<int m} \<noteq> {} \<Longrightarrow> 1 < m \<Longrightarrow> 1 < n \<Longrightarrow>
  isDiagonal_mat A \<Longrightarrow> is_bezout_ext bezout \<Longrightarrow> A \<in> carrier_mat m n \<Longrightarrow>
  (P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout \<Longrightarrow> S = P * A * Q \<and>
  invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
  \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{0..<int n} \<noteq> {}; {0..<int m} \<noteq> {}; 1 < m; 1 < n; isDiagonal_mat A; is_bezout_ext bezout; A \<in> carrier_mat m n; (P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using diagonal_to_Smith_PQ_JNF_canceled_first[cancel_type_definition]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{0..<int ?n} \<noteq> {}; {0..<int ?m} \<noteq> {}; 1 < ?m; 1 < ?n; isDiagonal_mat ?A; is_bezout_ext ?bezout; ?A \<in> carrier_mat ?m ?n; (?P, ?S, ?Q) = diagonal_to_Smith_PQ_JNF ?A ?bezout\<rbrakk> \<Longrightarrow> ?S = ?P * ?A * ?Q \<and> invertible_mat ?P \<and> invertible_mat ?Q \<and> Smith_normal_form_mat ?S \<and> ?P \<in> carrier_mat ?m ?m \<and> ?S \<in> carrier_mat ?m ?n \<and> ?Q \<in> carrier_mat ?n ?n

goal (1 subgoal):
 1. \<lbrakk>{0..<int n} \<noteq> {}; {0..<int m} \<noteq> {}; 1 < m; 1 < n; isDiagonal_mat A; is_bezout_ext bezout; A \<in> carrier_mat m n; (P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout\<rbrakk> \<Longrightarrow> S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by blast


[STATEMENT]
lemma diagonal_to_Smith_PQ_JNF:
  assumes A: "isDiagonal_mat A" and ib: "is_bezout_ext bezout"
  and "A \<in> carrier_mat m n"
  and PBQ: "(P,S,Q) = diagonal_to_Smith_PQ_JNF A bezout"
(*The following two assumptions appear since mod_type requires 1<CARD.
Those cases could be treated separately.*)
  and n: "n>1" and m: "m>1"
  shows "S = P*A*Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S
  \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using diagonal_to_Smith_PQ_JNF_canceled_both[OF _ _ m n]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{0..<int n} \<noteq> {}; {0..<int m} \<noteq> {}; isDiagonal_mat ?A; is_bezout_ext ?bezout; ?A \<in> carrier_mat m n; (?P, ?S, ?Q) = diagonal_to_Smith_PQ_JNF ?A ?bezout\<rbrakk> \<Longrightarrow> ?S = ?P * ?A * ?Q \<and> invertible_mat ?P \<and> invertible_mat ?Q \<and> Smith_normal_form_mat ?S \<and> ?P \<in> carrier_mat m m \<and> ?S \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>{0..<int n} \<noteq> {}; {0..<int m} \<noteq> {}; isDiagonal_mat ?A; is_bezout_ext ?bezout; ?A \<in> carrier_mat m n; (?P, ?S, ?Q) = diagonal_to_Smith_PQ_JNF ?A ?bezout\<rbrakk> \<Longrightarrow> ?S = ?P * ?A * ?Q \<and> invertible_mat ?P \<and> invertible_mat ?Q \<and> Smith_normal_form_mat ?S \<and> ?P \<in> carrier_mat m m \<and> ?S \<in> carrier_mat m n \<and> ?Q \<in> carrier_mat n n
isDiagonal_mat A
is_bezout_ext bezout
A \<in> carrier_mat m n
(P, S, Q) = diagonal_to_Smith_PQ_JNF A bezout
1 < n
1 < m

goal (1 subgoal):
 1. S = P * A * Q \<and> invertible_mat P \<and> invertible_mat Q \<and> Smith_normal_form_mat S \<and> P \<in> carrier_mat m m \<and> S \<in> carrier_mat m n \<and> Q \<in> carrier_mat n n
[PROOF STEP]
by force


[STATEMENT]
lemma widen1_acom: "strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c = strip c' \<Longrightarrow> c \<sqsubseteq> c \<nabla>\<^sub>c c'
[PROOF STEP]
by(induct c c' rule: le_acom.induct)(simp_all add: widen1)


[STATEMENT]
lemma widen2_acom: "strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c = strip c' \<Longrightarrow> c' \<sqsubseteq> c \<nabla>\<^sub>c c'
[PROOF STEP]
by(induct c c' rule: le_acom.induct)(simp_all add: widen2)


[STATEMENT]
lemma narrow1_acom: "y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqsubseteq> x \<Longrightarrow> y \<sqsubseteq> x \<triangle>\<^sub>c y
[PROOF STEP]
by(induct y x rule: le_acom.induct) (simp_all add: narrow1)


[STATEMENT]
lemma narrow2_acom: "y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqsubseteq> x \<Longrightarrow> x \<triangle>\<^sub>c y \<sqsubseteq> x
[PROOF STEP]
by(induct y x rule: le_acom.induct) (simp_all add: narrow2)


[STATEMENT]
lemma strip_map2_acom:
 "strip c1 = strip c2 \<Longrightarrow> strip(map2_acom f c1 c2) = strip c1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c1 = strip c2 \<Longrightarrow> strip (map2_acom f c1 c2) = strip c1
[PROOF STEP]
by(induct f c1 c2 rule: map2_acom.induct) simp_all


[STATEMENT]
lemma iter_widen_pfp: "iter_widen f c = Some c' \<Longrightarrow> f c' \<sqsubseteq> c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. iter_widen f c = Some c' \<Longrightarrow> f c' \<sqsubseteq> c'
[PROOF STEP]
by(auto simp add: iter_widen_def dest: while_option_stop)


[STATEMENT]
lemma strip_while: fixes f :: "'a acom \<Rightarrow> 'a acom"
assumes "\<forall>c. strip (f c) = strip c" and "while_option P f c = Some c'"
shows "strip c' = strip c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c' = strip c
[PROOF STEP]
using while_option_rule[where P = "\<lambda>c'. strip c' = strip c", OF _ assms(2)]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>s. \<lbrakk>strip s = strip c; P s\<rbrakk> \<Longrightarrow> strip (f s) = strip c; strip c = strip c\<rbrakk> \<Longrightarrow> strip c' = strip c

goal (1 subgoal):
 1. strip c' = strip c
[PROOF STEP]
by (metis assms(1))


[STATEMENT]
lemma strip_iter_widen: fixes f :: "'a::WN acom \<Rightarrow> 'a acom"
assumes "\<forall>c. strip (f c) = strip c" and "iter_widen f c = Some c'"
shows "strip c' = strip c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip c' = strip c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. strip c' = strip c
[PROOF STEP]
have "\<forall>c. strip(c \<nabla>\<^sub>c f c) = strip c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>c. strip (c \<nabla>\<^sub>c f c) = strip c
[PROOF STEP]
by (metis assms(1) strip_map2_acom)
[PROOF STATE]
proof (state)
this:
\<forall>c. strip (c \<nabla>\<^sub>c f c) = strip c

goal (1 subgoal):
 1. strip c' = strip c
[PROOF STEP]
from strip_while[OF this] assms(2)
[PROOF STATE]
proof (chain)
picking this:
while_option ?P (\<lambda>c. c \<nabla>\<^sub>c f c) ?c = Some ?c' \<Longrightarrow> strip ?c' = strip ?c
iter_widen f c = Some c'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
while_option ?P (\<lambda>c. c \<nabla>\<^sub>c f c) ?c = Some ?c' \<Longrightarrow> strip ?c' = strip ?c
iter_widen f c = Some c'

goal (1 subgoal):
 1. strip c' = strip c
[PROOF STEP]
by(simp add: iter_widen_def)
[PROOF STATE]
proof (state)
this:
strip c' = strip c

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iter_narrow_pfp: assumes "mono f" and "f c0 \<sqsubseteq> c0"
and "iter_narrow f c0 = Some c"
shows "f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0" (is "?P c")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
fix c
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
assume "?P c"
[PROOF STATE]
proof (state)
this:
f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0

goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
note 1 = conjunct1[OF this] and 2 = conjunct2[OF this]
[PROOF STATE]
proof (state)
this:
f c \<sqsubseteq> c
c \<sqsubseteq> c0

goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
let ?c' = "c \<triangle>\<^sub>c f c"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
have "?P ?c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c \<and> c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c
 2. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
have "f ?c' \<sqsubseteq> f c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (c \<triangle>\<^sub>c f c) \<sqsubseteq> f c
[PROOF STEP]
by(rule monoD[OF \<open>mono f\<close> narrow2_acom[OF 1]])
[PROOF STATE]
proof (state)
this:
f (c \<triangle>\<^sub>c f c) \<sqsubseteq> f c

goal (2 subgoals):
 1. f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c
 2. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f (c \<triangle>\<^sub>c f c) \<sqsubseteq> f c

goal (2 subgoals):
 1. f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c
 2. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
have "\<dots> \<sqsubseteq> ?c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f c \<sqsubseteq> c \<triangle>\<^sub>c f c
[PROOF STEP]
by(rule narrow1_acom[OF 1])
[PROOF STATE]
proof (state)
this:
f c \<sqsubseteq> c \<triangle>\<^sub>c f c

goal (2 subgoals):
 1. f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c
 2. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c
[PROOF STEP]
show "f ?c' \<sqsubseteq> ?c'"
[PROOF STATE]
proof (prove)
using this:
f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c

goal (1 subgoal):
 1. f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c

goal (1 subgoal):
 1. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
have "?c' \<sqsubseteq> c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<triangle>\<^sub>c f c \<sqsubseteq> c
[PROOF STEP]
by (rule narrow2_acom[OF 1])
[PROOF STATE]
proof (state)
this:
c \<triangle>\<^sub>c f c \<sqsubseteq> c

goal (1 subgoal):
 1. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
c \<triangle>\<^sub>c f c \<sqsubseteq> c

goal (1 subgoal):
 1. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
have "c \<sqsubseteq> c0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. c \<sqsubseteq> c0
[PROOF STEP]
by(rule 2)
[PROOF STATE]
proof (state)
this:
c \<sqsubseteq> c0

goal (1 subgoal):
 1. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
show "?c' \<sqsubseteq> c0"
[PROOF STATE]
proof (prove)
using this:
c \<triangle>\<^sub>c f c \<sqsubseteq> c0

goal (1 subgoal):
 1. c \<triangle>\<^sub>c f c \<sqsubseteq> c0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
c \<triangle>\<^sub>c f c \<sqsubseteq> c0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
f (c \<triangle>\<^sub>c f c) \<sqsubseteq> c \<triangle>\<^sub>c f c \<and> c \<triangle>\<^sub>c f c \<sqsubseteq> c0

goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
f ?ca2 \<sqsubseteq> ?ca2 \<and> ?ca2 \<sqsubseteq> c0 \<Longrightarrow> f (?ca2 \<triangle>\<^sub>c f ?ca2) \<sqsubseteq> ?ca2 \<triangle>\<^sub>c f ?ca2 \<and> ?ca2 \<triangle>\<^sub>c f ?ca2 \<sqsubseteq> c0

goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
with while_option_rule[where P = ?P, OF _ assms(3)[simplified iter_narrow_def]]
    assms(2) le_refl
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>s. \<lbrakk>f s \<sqsubseteq> s \<and> s \<sqsubseteq> c0; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> f (s \<triangle>\<^sub>c f s) \<sqsubseteq> s \<triangle>\<^sub>c f s \<and> s \<triangle>\<^sub>c f s \<sqsubseteq> c0; f c0 \<sqsubseteq> c0 \<and> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
f c0 \<sqsubseteq> c0
?x \<sqsubseteq> ?x
f ?ca2 \<sqsubseteq> ?ca2 \<and> ?ca2 \<sqsubseteq> c0 \<Longrightarrow> f (?ca2 \<triangle>\<^sub>c f ?ca2) \<sqsubseteq> ?ca2 \<triangle>\<^sub>c f ?ca2 \<and> ?ca2 \<triangle>\<^sub>c f ?ca2 \<sqsubseteq> c0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>s. \<lbrakk>f s \<sqsubseteq> s \<and> s \<sqsubseteq> c0; \<not> s \<sqsubseteq> s \<triangle>\<^sub>c f s\<rbrakk> \<Longrightarrow> f (s \<triangle>\<^sub>c f s) \<sqsubseteq> s \<triangle>\<^sub>c f s \<and> s \<triangle>\<^sub>c f s \<sqsubseteq> c0; f c0 \<sqsubseteq> c0 \<and> c0 \<sqsubseteq> c0\<rbrakk> \<Longrightarrow> f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
f c0 \<sqsubseteq> c0
?x \<sqsubseteq> ?x
f ?ca2 \<sqsubseteq> ?ca2 \<and> ?ca2 \<sqsubseteq> c0 \<Longrightarrow> f (?ca2 \<triangle>\<^sub>c f ?ca2) \<sqsubseteq> ?ca2 \<triangle>\<^sub>c f ?ca2 \<and> ?ca2 \<triangle>\<^sub>c f ?ca2 \<sqsubseteq> c0

goal (1 subgoal):
 1. f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f c \<sqsubseteq> c \<and> c \<sqsubseteq> c0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pfp_wn_pfp:
  "\<lbrakk> mono f;  pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preord_class.mono f; pfp_wn f c = Some c'\<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'
[PROOF STEP]
unfolding pfp_wn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>preord_class.mono f; (case iter_widen f (\<bottom>\<^sub>c c) of None \<Rightarrow> None | Some x \<Rightarrow> iter_narrow f x) = Some c'\<rbrakk> \<Longrightarrow> f c' \<sqsubseteq> c'
[PROOF STEP]
by (auto dest: iter_widen_pfp iter_narrow_pfp split: option.splits)


[STATEMENT]
lemma strip_pfp_wn:
  "\<lbrakk> \<forall>c. strip(f c) = strip c; pfp_wn f c = Some c' \<rbrakk> \<Longrightarrow> strip c' = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>c. strip (f c) = strip c; pfp_wn f c = Some c'\<rbrakk> \<Longrightarrow> strip c' = c
[PROOF STEP]
apply(auto simp add: pfp_wn_def iter_narrow_def split: option.splits)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>\<forall>c. strip (f c) = strip c; iter_widen f (\<bottom>\<^sub>c c) = Some x2; while_option (\<lambda>c. \<not> c \<sqsubseteq> c \<triangle>\<^sub>c f c) (\<lambda>c. c \<triangle>\<^sub>c f c) x2 = Some c'\<rbrakk> \<Longrightarrow> strip c' = c
[PROOF STEP]
by (metis (mono_tags) strip_map2_acom strip_while strip_bot_acom strip_iter_widen)


[STATEMENT]
lemma AI_wn_sound: "AI_wn c = Some c' \<Longrightarrow> CS c \<le> \<gamma>\<^sub>c c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. AI_wn c = Some c' \<Longrightarrow> CS c \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
proof(simp add: CS_def AI_wn_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pfp_wn (local.step' \<top>) c = Some c' \<Longrightarrow> Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
assume 1: "pfp_wn (step' \<top>) c = Some c'"
[PROOF STATE]
proof (state)
this:
pfp_wn (local.step' \<top>) c = Some c'

goal (1 subgoal):
 1. pfp_wn (local.step' \<top>) c = Some c' \<Longrightarrow> Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
from pfp_wn_pfp[OF mono_step'2 1]
[PROOF STATE]
proof (chain)
picking this:
local.step' \<top> c' \<sqsubseteq> c'
[PROOF STEP]
have 2: "step' \<top> c' \<sqsubseteq> c'"
[PROOF STATE]
proof (prove)
using this:
local.step' \<top> c' \<sqsubseteq> c'

goal (1 subgoal):
 1. local.step' \<top> c' \<sqsubseteq> c'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
local.step' \<top> c' \<sqsubseteq> c'

goal (1 subgoal):
 1. pfp_wn (local.step' \<top>) c = Some c' \<Longrightarrow> Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
have 3: "strip (\<gamma>\<^sub>c (step' \<top> c')) = c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. strip (local.\<gamma>\<^sub>c (local.step' \<top> c')) = c
[PROOF STEP]
by(simp add: strip_pfp_wn[OF _ 1])
[PROOF STATE]
proof (state)
this:
strip (local.\<gamma>\<^sub>c (local.step' \<top> c')) = c

goal (1 subgoal):
 1. pfp_wn (local.step' \<top>) c = Some c' \<Longrightarrow> Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
have "lfp (step UNIV) c \<le> \<gamma>\<^sub>c (step' \<top> c')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c (local.step' \<top> c')
[PROOF STEP]
proof(rule lfp_lowerbound[simplified,OF 3])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. step UNIV (local.\<gamma>\<^sub>c (local.step' \<top> c')) \<le> local.\<gamma>\<^sub>c (local.step' \<top> c')
[PROOF STEP]
show "step UNIV (\<gamma>\<^sub>c (step' \<top> c')) \<le> \<gamma>\<^sub>c (step' \<top> c')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. step UNIV (local.\<gamma>\<^sub>c (local.step' \<top> c')) \<le> local.\<gamma>\<^sub>c (local.step' \<top> c')
[PROOF STEP]
proof(rule step_preserves_le[OF _ _])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. UNIV \<subseteq> local.\<gamma>\<^sub>o \<top>
 2. local.\<gamma>\<^sub>c (local.step' \<top> c') \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
show "UNIV \<subseteq> \<gamma>\<^sub>o \<top>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV \<subseteq> local.\<gamma>\<^sub>o \<top>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
UNIV \<subseteq> local.\<gamma>\<^sub>o \<top>

goal (1 subgoal):
 1. local.\<gamma>\<^sub>c (local.step' \<top> c') \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
show "\<gamma>\<^sub>c (step' \<top> c') \<le> \<gamma>\<^sub>c c'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.\<gamma>\<^sub>c (local.step' \<top> c') \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
by(rule mono_gamma_c[OF 2])
[PROOF STATE]
proof (state)
this:
local.\<gamma>\<^sub>c (local.step' \<top> c') \<le> local.\<gamma>\<^sub>c c'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
step UNIV (local.\<gamma>\<^sub>c (local.step' \<top> c')) \<le> local.\<gamma>\<^sub>c (local.step' \<top> c')

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c (local.step' \<top> c')

goal (1 subgoal):
 1. pfp_wn (local.step' \<top>) c = Some c' \<Longrightarrow> Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
from this 2
[PROOF STATE]
proof (chain)
picking this:
Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c (local.step' \<top> c')
local.step' \<top> c' \<sqsubseteq> c'
[PROOF STEP]
show "lfp (step UNIV) c \<le> \<gamma>\<^sub>c c'"
[PROOF STATE]
proof (prove)
using this:
Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c (local.step' \<top> c')
local.step' \<top> c' \<sqsubseteq> c'

goal (1 subgoal):
 1. Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c c'
[PROOF STEP]
by (blast intro: mono_gamma_c order_trans)
[PROOF STATE]
proof (state)
this:
Collecting.lfp (step UNIV) c \<le> local.\<gamma>\<^sub>c c'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma m_ivl_height: "m_ivl ivl \<le> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m_ivl ivl \<le> 2
[PROOF STEP]
by(simp add: m_ivl_def split: ivl.split option.split)


[STATEMENT]
lemma m_ivl_anti_mono: "(y::ivl) \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sqsubseteq> x \<Longrightarrow> m_ivl x \<le> m_ivl y
[PROOF STEP]
by(auto simp: m_ivl_def le_option_def le_ivl_def
        split: ivl.split option.split if_splits)


[STATEMENT]
lemma m_ivl_widen:
  "~ y \<sqsubseteq> x \<Longrightarrow> m_ivl(x \<nabla> y) < m_ivl x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> y \<sqsubseteq> x \<Longrightarrow> m_ivl (x \<nabla> y) < m_ivl x
[PROOF STEP]
by(auto simp: m_ivl_def widen_ivl_def le_option_def le_ivl_def
        split: ivl.splits option.splits if_splits)


[STATEMENT]
lemma Top_less_ivl: "\<top> \<sqsubseteq> x \<Longrightarrow> m_ivl x = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<top> \<sqsubseteq> x \<Longrightarrow> m_ivl x = 0
[PROOF STEP]
by(auto simp: m_ivl_def le_option_def le_ivl_def empty_def Top_ivl_def
        split: ivl.split option.split if_splits)