[STATEMENT]
lemma mahler_approximation_main: assumes "k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm"
    and "c = (-1)^(degree f)"
    and "g = graeffe_poly_impl_main c f k" "dd = d^(2^(Suc k))" "kk = 2^(Suc k)"
  shows "\<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_approximation_main dd c g mm k kk"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm
c = (- 1) ^ degree f
g = graeffe_poly_impl_main c f k
dd = d ^ 2 ^ Suc k
kk = 2 ^ Suc k

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
proof (induct c g mm k kk rule: mahler_approximation_main.induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
case (1 dd c g mm k kk)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = mahler_landau_graeffe_approximation kk dd g; ?xa = (if k = 0 then ?x else min mm ?x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> ?xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) ?xa (Suc k) (2 * kk)
k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm
c = (- 1) ^ degree f
g = graeffe_poly_impl_main c f k
dd = d ^ 2 ^ Suc k
kk = 2 ^ Suc k

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
let ?df = "\<lfloor>real d * mahler_measure f\<rfloor>"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
note dd = 1(5)
[PROOF STATE]
proof (state)
this:
dd = d ^ 2 ^ Suc k

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
note kk = 1(6)
[PROOF STATE]
proof (state)
this:
kk = 2 ^ Suc k

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
note g = 1(4)
[PROOF STATE]
proof (state)
this:
g = graeffe_poly_impl_main c f k

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
note c = 1(3)
[PROOF STATE]
proof (state)
this:
c = (- 1) ^ degree f

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
note mm = 1(2)
[PROOF STATE]
proof (state)
this:
k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
note IH = 1(1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = mahler_landau_graeffe_approximation kk dd g; ?xa = (if k = 0 then ?x else min mm ?x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> ?xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) ?xa (Suc k) (2 * kk)

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
note mahl = mahler_approximation_main.simps[of dd c g mm k kk]
[PROOF STATE]
proof (state)
this:
local.mahler_approximation_main dd c g mm k kk = (let mmm = mahler_landau_graeffe_approximation kk dd g; new_mm = if k = 0 then mmm else min mm mmm in if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk))

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
define mmm where "mmm = mahler_landau_graeffe_approximation kk dd g"
[PROOF STATE]
proof (state)
this:
mmm = mahler_landau_graeffe_approximation kk dd g

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
define new_mm where "new_mm = (if k = 0 then mmm else min mm mmm)"
[PROOF STATE]
proof (state)
this:
new_mm = (if k = 0 then mmm else min mm mmm)

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
let ?cond = "bnd \<le> k"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
have id: "mahler_approximation_main dd c g mm k kk = (if ?cond then new_mm
        else mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.mahler_approximation_main dd c g mm k kk = (if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk))
[PROOF STEP]
unfolding mahl mmm_def[symmetric] Let_def new_mm_def[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)) = (if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.mahler_approximation_main dd c g mm k kk = (if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk))

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
have gg: "g = (graeffe_poly_impl f k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = graeffe_poly_impl f k
[PROOF STEP]
unfolding g graeffe_poly_impl_def c
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_poly_impl_main ((- 1) ^ degree f) f k = graeffe_poly_impl_main ((- 1) ^ degree f) f k
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
g = graeffe_poly_impl f k

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
from mahler_landau_graeffe_approximation[OF gg dd kk, folded mmm_def]
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> mmm
[PROOF STEP]
have mmm: "?df \<le> mmm"
[PROOF STATE]
proof (prove)
using this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> mmm

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> mmm
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> mmm

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
with mm
[PROOF STATE]
proof (chain)
picking this:
k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm
\<lfloor>real d * mahler_measure f\<rfloor> \<le> mmm
[PROOF STEP]
have new_mm: "?df \<le> new_mm"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm
\<lfloor>real d * mahler_measure f\<rfloor> \<le> mmm

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> new_mm
[PROOF STEP]
unfolding new_mm_def
[PROOF STATE]
proof (prove)
using this:
k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm
\<lfloor>real d * mahler_measure f\<rfloor> \<le> mmm

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> (if k = 0 then mmm else min mm mmm)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> new_mm

goal (1 subgoal):
 1. \<And>dd c g mm k kk. \<lbrakk>\<And>x xa. \<lbrakk>x = mahler_landau_graeffe_approximation kk dd g; xa = (if k = 0 then x else min mm x); \<not> bnd \<le> k; Suc k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> xa; c = (- 1) ^ degree f; graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k); dd * dd = d ^ 2 ^ Suc (Suc k); 2 * kk = 2 ^ Suc (Suc k)\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) xa (Suc k) (2 * kk); k \<noteq> 0 \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> mm; c = (- 1) ^ degree f; g = graeffe_poly_impl_main c f k; dd = d ^ 2 ^ Suc k; kk = 2 ^ Suc k\<rbrakk> \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
proof (cases ?cond)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
 2. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
bnd \<le> k

goal (2 subgoals):
 1. bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
 2. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> (if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk))
[PROOF STEP]
using True new_mm
[PROOF STATE]
proof (prove)
using this:
bnd \<le> k
\<lfloor>real d * mahler_measure f\<rfloor> \<le> new_mm

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> (if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk

goal (1 subgoal):
 1. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> bnd \<le> k

goal (1 subgoal):
 1. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
hence id: "mahler_approximation_main dd c g mm k kk =
      mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)"
[PROOF STATE]
proof (prove)
using this:
\<not> bnd \<le> k

goal (1 subgoal):
 1. local.mahler_approximation_main dd c g mm k kk = local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
\<not> bnd \<le> k

goal (1 subgoal):
 1. (if bnd \<le> k then new_mm else local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)) = local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.mahler_approximation_main dd c g mm k kk = local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)

goal (1 subgoal):
 1. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
have id': "graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k)
[PROOF STEP]
unfolding g
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graeffe_one_step c (graeffe_poly_impl_main c f k) = graeffe_poly_impl_main c f (Suc k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
graeffe_one_step c g = graeffe_poly_impl_main c f (Suc k)

goal (1 subgoal):
 1. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
have "dd * dd = d ^ 2 ^ Suc (Suc k)" "2 * kk = 2 ^ Suc (Suc k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dd * dd = d ^ 2 ^ Suc (Suc k) &&& 2 * kk = 2 ^ Suc (Suc k)
[PROOF STEP]
unfolding dd kk
      semiring_normalization_rules(26)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d ^ (2 ^ Suc k + 2 ^ Suc k) = d ^ 2 ^ Suc (Suc k) &&& 2 * 2 ^ Suc k = 2 ^ Suc (Suc k)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dd * dd = d ^ 2 ^ Suc (Suc k)
2 * kk = 2 ^ Suc (Suc k)

goal (1 subgoal):
 1. \<not> bnd \<le> k \<Longrightarrow> \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
from IH[OF mmm_def new_mm_def False new_mm c id' this]
[PROOF STATE]
proof (chain)
picking this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk
[PROOF STEP]
unfolding id
[PROOF STATE]
proof (prove)
using this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)

goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (dd * dd) c (graeffe_one_step c g) new_mm (Suc k) (2 * kk)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main dd c g mm k kk

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mahler_approximation: "\<lfloor>real d * mahler_measure f\<rfloor> \<le> mahler_approximation d f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation d f
[PROOF STEP]
unfolding mahler_approximation_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lfloor>real d * mahler_measure f\<rfloor> \<le> local.mahler_approximation_main (d * d) ((- 1) ^ degree f) f (- 1) 0 2
[PROOF STEP]
by (rule mahler_approximation_main, auto simp: semiring_normalization_rules(29))


[STATEMENT]
lemma det_selection_funD: "det_selection_fun f \<Longrightarrow> xs \<noteq> [] \<Longrightarrow> f xs \<in> fst ` set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_selection_fun f; xs \<noteq> []\<rbrakk> \<Longrightarrow> f xs \<in> fst ` set xs
[PROOF STEP]
unfolding det_selection_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>xs. xs \<noteq> [] \<longrightarrow> f xs \<in> fst ` set xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> f xs \<in> fst ` set xs
[PROOF STEP]
by auto


[STATEMENT]
lemma triangular_columnD [dest]:
  "triangular_column j A \<Longrightarrow> j < i \<Longrightarrow> i < dim_row A \<Longrightarrow> A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.triangular_column j A; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
unfolding triangular_column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i>j. i < dim_row A \<longrightarrow> A $$ (i, j) = (0::'a); j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma triangular_columnI [intro]:
  "(\<And>i. j < i \<Longrightarrow> i < dim_row A \<Longrightarrow> A $$ (i,j) = 0) \<Longrightarrow> triangular_column j A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)) \<Longrightarrow> local.triangular_column j A
[PROOF STEP]
unfolding triangular_column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)) \<Longrightarrow> \<forall>i>j. i < dim_row A \<longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma triangular_to_triangular: "upper_triangular A = triangular_to (dim_row A) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular A = local.triangular_to (dim_row A) A
[PROOF STEP]
unfolding triangular_to_def triangular_column_def upper_triangular_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i<dim_row A. \<forall>j<i. A $$ (i, j) = (0::'a)) = (\<forall>j<dim_row A. \<forall>i>j. i < dim_row A \<longrightarrow> A $$ (i, j) = (0::'a))
[PROOF STEP]
by auto


[STATEMENT]
lemma triangular_toD [dest]:
  "triangular_to k A \<Longrightarrow> j < k \<Longrightarrow> j < i \<Longrightarrow> i < dim_row A \<Longrightarrow> A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.triangular_to k A; j < k; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
unfolding triangular_to_def triangular_column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>j<k. \<forall>i>j. i < dim_row A \<longrightarrow> A $$ (i, j) = (0::'a); j < k; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma triangular_toI [intro]:
  "(\<And>i j. j < k \<Longrightarrow> j < i \<Longrightarrow> i < dim_row A \<Longrightarrow> A $$ (i,j) = 0) \<Longrightarrow> triangular_to k A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>j < k; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)) \<Longrightarrow> local.triangular_to k A
[PROOF STEP]
unfolding triangular_to_def triangular_column_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>j < k; j < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, j) = (0::'a)) \<Longrightarrow> \<forall>j<k. \<forall>i>j. i < dim_row A \<longrightarrow> A $$ (i, j) = (0::'a)
[PROOF STEP]
by auto


[STATEMENT]
lemma triangle_growth:
  assumes tri:"triangular_to k A"
  and col:"triangular_column k A"
  shows "triangular_to (Suc k) A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to (Suc k) A
[PROOF STEP]
unfolding triangular_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j<Suc k. local.triangular_column j A
[PROOF STEP]
proof (intro allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < Suc k \<Longrightarrow> local.triangular_column j A
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j. j < Suc k \<Longrightarrow> local.triangular_column j A
[PROOF STEP]
assume iSk:"i < Suc k"
[PROOF STATE]
proof (state)
this:
i < Suc k

goal (1 subgoal):
 1. \<And>j. j < Suc k \<Longrightarrow> local.triangular_column j A
[PROOF STEP]
show "triangular_column i A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_column i A
[PROOF STEP]
proof (cases "i = k")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i = k \<Longrightarrow> local.triangular_column i A
 2. i \<noteq> k \<Longrightarrow> local.triangular_column i A
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i = k

goal (2 subgoals):
 1. i = k \<Longrightarrow> local.triangular_column i A
 2. i \<noteq> k \<Longrightarrow> local.triangular_column i A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i = k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i = k

goal (1 subgoal):
 1. local.triangular_column i A
[PROOF STEP]
using col
[PROOF STATE]
proof (prove)
using this:
i = k
local.triangular_column k A

goal (1 subgoal):
 1. local.triangular_column i A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_column i A

goal (1 subgoal):
 1. i \<noteq> k \<Longrightarrow> local.triangular_column i A
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. i \<noteq> k \<Longrightarrow> local.triangular_column i A
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
i \<noteq> k

goal (1 subgoal):
 1. i \<noteq> k \<Longrightarrow> local.triangular_column i A
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<noteq> k
[PROOF STEP]
have "i < k"
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k

goal (1 subgoal):
 1. i < k
[PROOF STEP]
using iSk
[PROOF STATE]
proof (prove)
using this:
i \<noteq> k
i < Suc k

goal (1 subgoal):
 1. i < k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. i \<noteq> k \<Longrightarrow> local.triangular_column i A
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i < k

goal (1 subgoal):
 1. local.triangular_column i A
[PROOF STEP]
using tri
[PROOF STATE]
proof (prove)
using this:
i < k
local.triangular_to k A

goal (1 subgoal):
 1. local.triangular_column i A
[PROOF STEP]
unfolding triangular_to_def
[PROOF STATE]
proof (prove)
using this:
i < k
\<forall>j<k. local.triangular_column j A

goal (1 subgoal):
 1. local.triangular_column i A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_column i A

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.triangular_column i A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma triangle_trans: "triangular_to k A \<Longrightarrow> k > k' \<Longrightarrow> triangular_to k' A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.triangular_to k A; k' < k\<rbrakk> \<Longrightarrow> local.triangular_to k' A
[PROOF STEP]
by (intro triangular_toI, elim triangular_toD, auto)


[STATEMENT]
lemma mute_preserves_dimensions:
  assumes "mute q k l (r,A) = (r',A')"
  shows [simp]: "dim_row A' = dim_row A" and [simp]: "dim_col A' = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A' = dim_row A &&& dim_col A' = dim_col A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
mute q k l (r, A) = (r', A')

goal (1 subgoal):
 1. dim_row A' = dim_row A &&& dim_col A' = dim_col A
[PROOF STEP]
by (auto simp: Let_def split: if_splits prod.splits)


[STATEMENT]
lemma mute_makes_0 :
 assumes mute_fun: "mute_fun mf"
 assumes "mute (A $$ (l,l)) k l (r,A) = (r',A')"
 "l < dim_row A"
 "l < dim_col A"
 "k < dim_row A"
 "k \<noteq> l"
 shows "A' $$ (k,l) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
define a where "a = A $$ (l, l)"
[PROOF STATE]
proof (state)
this:
a = A $$ (l, l)

goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
define b where "b = A $$ (k, l)"
[PROOF STATE]
proof (state)
this:
b = A $$ (k, l)

goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
let ?mf = "mf (A $$ (l, l)) (A $$ (k, l))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
obtain q' p' g where id: "?mf = (q',p',g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q' p' g. mf (A $$ (l, l)) (A $$ (k, l)) = (q', p', g) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases ?mf, auto)
[PROOF STATE]
proof (state)
this:
mf (A $$ (l, l)) (A $$ (k, l)) = (q', p', g)

goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
note mf = mute_fun[unfolded mute_fun_def, rule_format, OF id]
[PROOF STATE]
proof (state)
this:
A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> A $$ (l, l) = q' * g \<and> A $$ (k, l) * q' = A $$ (l, l) * p'

goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
mute_fun mf
mute (A $$ (l, l)) k l (r, A) = (r', A')
l < dim_row A
l < dim_col A
k < dim_row A
k \<noteq> l
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
mute_fun mf
mute (A $$ (l, l)) k l (r, A) = (r', A')
l < dim_row A
l < dim_col A
k < dim_row A
k \<noteq> l

goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
unfolding mat_addrow_def
[PROOF STATE]
proof (prove)
using this:
mute_fun mf
mute (A $$ (l, l)) k l (r, A) = (r', A')
l < dim_row A
l < dim_col A
k < dim_row A
k \<noteq> l

goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
using mf id
[PROOF STATE]
proof (prove)
using this:
mute_fun mf
mute (A $$ (l, l)) k l (r, A) = (r', A')
l < dim_row A
l < dim_col A
k < dim_row A
k \<noteq> l
A $$ (k, l) \<noteq> (0::'a) \<Longrightarrow> A $$ (l, l) = q' * g \<and> A $$ (k, l) * q' = A $$ (l, l) * p'
mf (A $$ (l, l)) (A $$ (k, l)) = (q', p', g)

goal (1 subgoal):
 1. A' $$ (k, l) = (0::'a)
[PROOF STEP]
by (auto simp: ac_simps Let_def split: if_splits)
[PROOF STATE]
proof (state)
this:
A' $$ (k, l) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mute_preserves:
  "mute q k l (r,A) = (r',A') \<Longrightarrow>
   i < dim_row A \<Longrightarrow>
   j < dim_col A \<Longrightarrow>
   l < dim_row A \<Longrightarrow>
   k < dim_row A \<Longrightarrow>
   i \<noteq> k \<Longrightarrow>
   A' $$ (i,j) = A $$ (i,j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mute q k l (r, A) = (r', A'); i < dim_row A; j < dim_col A; l < dim_row A; k < dim_row A; i \<noteq> k\<rbrakk> \<Longrightarrow> A' $$ (i, j) = A $$ (i, j)
[PROOF STEP]
by (auto simp: Let_def split: if_splits prod.splits)


[STATEMENT]
lemma mute_preserves_0:
  "mute q k l (r,A) = (r',A') \<Longrightarrow>
   i < dim_row A \<Longrightarrow>
   j < dim_col A \<Longrightarrow>
   l < dim_row A \<Longrightarrow>
   k < dim_row A \<Longrightarrow>
   A $$ (i,j) = 0 \<Longrightarrow>
   A $$ (l,j) = 0 \<Longrightarrow>
   A' $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>mute q k l (r, A) = (r', A'); i < dim_row A; j < dim_col A; l < dim_row A; k < dim_row A; A $$ (i, j) = (0::'a); A $$ (l, j) = (0::'a)\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
by (auto simp: Let_def split: if_splits prod.splits)


[STATEMENT]
lemma mute_preserves_triangle:
 assumes rA' : "mute q k l (r,A) = (r',A')"
 and triA: "triangular_to l A"
 and lk: "l < k"
 and kr: "k < dim_row A"
 and lr: "l < dim_row A"
 and lc: "l < dim_col A"
 shows "triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
proof (rule triangular_toI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
assume jl: "j < l" and ji: "j < i" and ir': "i < dim_row A'"
[PROOF STATE]
proof (state)
this:
j < l
j < i
i < dim_row A'

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < l
j < i
i < dim_row A'
[PROOF STEP]
have A0: "A $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
using this:
j < l
j < i
i < dim_row A'

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
using triA rA'
[PROOF STATE]
proof (prove)
using this:
j < l
j < i
i < dim_row A'
local.triangular_to l A
mute q k l (r, A) = (r', A')

goal (1 subgoal):
 1. A $$ (i, j) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A $$ (i, j) = (0::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
have "A $$ (l,j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (l, j) = (0::'a)
[PROOF STEP]
using triA jl jl lr
[PROOF STATE]
proof (prove)
using this:
local.triangular_to l A
j < l
j < l
l < dim_row A

goal (1 subgoal):
 1. A $$ (l, j) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (l, j) = (0::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
A $$ (l, j) = (0::'a)

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
have jc:"j < dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < dim_col A
[PROOF STEP]
using jl lc
[PROOF STATE]
proof (prove)
using this:
j < l
l < dim_col A

goal (1 subgoal):
 1. j < dim_col A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
j < dim_col A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
j < dim_col A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
have ir: "i < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_row A
[PROOF STEP]
using ir' rA'
[PROOF STATE]
proof (prove)
using this:
i < dim_row A'
mute q k l (r, A) = (r', A')

goal (1 subgoal):
 1. i < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < dim_row A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>j < l; j < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, j) = (0::'a)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
A $$ (i, j) = (0::'a)
A $$ (l, j) = (0::'a)
j < dim_col A
i < dim_row A
[PROOF STEP]
show "A' $$ (i,j) = 0"
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
A $$ (l, j) = (0::'a)
j < dim_col A
i < dim_row A

goal (1 subgoal):
 1. A' $$ (i, j) = (0::'a)
[PROOF STEP]
using mute_preserves_0[OF rA'] lr kr
[PROOF STATE]
proof (prove)
using this:
A $$ (i, j) = (0::'a)
A $$ (l, j) = (0::'a)
j < dim_col A
i < dim_row A
\<lbrakk>?i < dim_row A; ?j < dim_col A; l < dim_row A; k < dim_row A; A $$ (?i, ?j) = (0::'a); A $$ (l, ?j) = (0::'a)\<rbrakk> \<Longrightarrow> A' $$ (?i, ?j) = (0::'a)
l < dim_row A
k < dim_row A

goal (1 subgoal):
 1. A' $$ (i, j) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' $$ (i, j) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub1_preserves_dimensions[simp]:
  "sub1 q k l (r,A) = (r',A') \<Longrightarrow> dim_row A' = dim_row A"
  "sub1 q k l (r,A) = (r',A') \<Longrightarrow> dim_col A' = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A) &&& (sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A)
[PROOF STEP]
proof (induction k arbitrary: r' A')
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_row ?A' = dim_row A
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_col ?A' = dim_col A

goal (4 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_row ?A' = dim_row A
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_col ?A' = dim_col A

goal (4 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
obtain r' A' where rA': "sub1 q k l (r, A) = (r', A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub1 q k l (r, A) = (r', A')

goal (4 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub1 q k l (r, A) = (r', A')

goal (4 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
fix r'' A''
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
assume "sub1 q (Suc k) l (r, A) = (r'', A'')"
[PROOF STATE]
proof (state)
this:
sub1 q (Suc k) l (r, A) = (r'', A'')

goal (4 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
 3. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_row A' = dim_row A
 4. \<And>k r' A'. \<lbrakk>\<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A; \<And>r' A'. sub1 q k l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_row ?A' = dim_row A
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_col ?A' = dim_col A
sub1 q k l (r, A) = (r', A')
sub1 q (Suc k) l (r, A) = (r'', A'')
[PROOF STEP]
show "dim_row A'' = dim_row A" "dim_col A'' = dim_col A"
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_row ?A' = dim_row A
sub1 q k l (r, A) = (?r', ?A') \<Longrightarrow> dim_col ?A' = dim_col A
sub1 q k l (r, A) = (r', A')
sub1 q (Suc k) l (r, A) = (r'', A'')

goal (1 subgoal):
 1. dim_row A'' = dim_row A &&& dim_col A'' = dim_col A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A'' = dim_row A
dim_col A'' = dim_col A

goal (2 subgoals):
 1. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_row A' = dim_row A
 2. \<And>r' A'. sub1 q 0 l (r, A) = (r', A') \<Longrightarrow> dim_col A' = dim_col A
[PROOF STEP]
qed auto


[STATEMENT]
lemma sub1_closed [simp]:
  "sub1 q k l (r,A) = (r',A') \<Longrightarrow> A \<in> carrier_mat m n \<Longrightarrow> A' \<in> carrier_mat m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub1 q k l (r, A) = (r', A'); A \<in> carrier_mat m n\<rbrakk> \<Longrightarrow> A' \<in> carrier_mat m n
[PROOF STEP]
unfolding carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub1 q k l (r, A) = (r', A'); A \<in> {ma. dim_row ma = m \<and> dim_col ma = n}\<rbrakk> \<Longrightarrow> A' \<in> {ma. dim_row ma = m \<and> dim_col ma = n}
[PROOF STEP]
by auto


[STATEMENT]
lemma sub1_preserves_diagnal:
  assumes "sub1 q k l (r,A) = (r',A')"
  and "l < dim_col A"
  and "k + l < dim_row A"
  shows "A' $$ (l,l) = A $$ (l,l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r', A')
l < dim_col A
k + l < dim_row A

goal (1 subgoal):
 1. A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>sub1 q k l (r, A) = (r', A'); l < dim_col A; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
show "k + l < dim_row A \<Longrightarrow> sub1 q k l (r,A) = (r',A') \<Longrightarrow>
    A' $$ (l,l) = A $$ (l,l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
proof (induction k arbitrary: r' A')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>0 + l < dim_row A; sub1 q 0 l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l); Suc k + l < dim_row A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (?r', ?A')\<rbrakk> \<Longrightarrow> ?A' $$ (l, l) = A $$ (l, l)
Suc k + l < dim_row A
sub1 q (Suc k) l (r, A) = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>0 + l < dim_row A; sub1 q 0 l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l); Suc k + l < dim_row A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
obtain r'' A'' where rA''[simp]: "sub1 q k l (r,A) = (r'',A'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r'' A''. sub1 q k l (r, A) = (r'', A'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub1 q k l (r, A) = (r'', A'')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>0 + l < dim_row A; sub1 q 0 l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l); Suc k + l < dim_row A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
have [simp]:"dim_row A'' = dim_row A" and [simp]:"dim_col A'' = dim_col A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A'' = dim_row A &&& dim_col A'' = dim_col A
[PROOF STEP]
using snd_conv sub1_preserves_dimensions[OF rA'']
[PROOF STATE]
proof (prove)
using this:
snd (?x1.0, ?x2.0) = ?x2.0
dim_row A'' = dim_row A
dim_col A'' = dim_col A

goal (1 subgoal):
 1. dim_row A'' = dim_row A &&& dim_col A'' = dim_col A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A'' = dim_row A
dim_col A'' = dim_col A

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>0 + l < dim_row A; sub1 q 0 l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l); Suc k + l < dim_row A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
have "A'' $$ (l,l) = A $$ (l,l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A'' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
using assms Suc
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r', A')
l < dim_col A
k + l < dim_row A
\<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (?r', ?A')\<rbrakk> \<Longrightarrow> ?A' $$ (l, l) = A $$ (l, l)
Suc k + l < dim_row A
sub1 q (Suc k) l (r, A) = (r', A')

goal (1 subgoal):
 1. A'' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A'' $$ (l, l) = A $$ (l, l)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>0 + l < dim_row A; sub1 q 0 l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l); Suc k + l < dim_row A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
have rA': "mute q (l + Suc k) l (r'', A'') = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mute q (l + Suc k) l (r'', A'') = (r', A')
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (?r', ?A')\<rbrakk> \<Longrightarrow> ?A' $$ (l, l) = A $$ (l, l)
Suc k + l < dim_row A
sub1 q (Suc k) l (r, A) = (r', A')

goal (1 subgoal):
 1. mute q (l + Suc k) l (r'', A'') = (r', A')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mute q (l + Suc k) l (r'', A'') = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>0 + l < dim_row A; sub1 q 0 l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l); Suc k + l < dim_row A; sub1 q (Suc k) l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
using subst mute_preserves[OF rA'] Suc assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?s = ?t; ?P ?s\<rbrakk> \<Longrightarrow> ?P ?t
\<lbrakk>?i < dim_row A''; ?j < dim_col A''; l < dim_row A''; l + Suc k < dim_row A''; ?i \<noteq> l + Suc k\<rbrakk> \<Longrightarrow> A' $$ (?i, ?j) = A'' $$ (?i, ?j)
\<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (?r', ?A')\<rbrakk> \<Longrightarrow> ?A' $$ (l, l) = A $$ (l, l)
Suc k + l < dim_row A
sub1 q (Suc k) l (r, A) = (r', A')
sub1 q k l (r, A) = (r', A')
l < dim_col A
k + l < dim_row A

goal (1 subgoal):
 1. A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' $$ (l, l) = A $$ (l, l)

goal (1 subgoal):
 1. \<And>r' A'. \<lbrakk>0 + l < dim_row A; sub1 q 0 l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>k + l < dim_row A; sub1 q k l (r, A) = (r', A')\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub1_preserves_triangle:
  assumes "sub1 q k l (r,A) = (r',A')"
  and tri: "triangular_to l A"
  and lr: "l < dim_row A"
  and lc: "l < dim_col A"
  and lkr: "l + k < dim_row A"
  shows "triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r', A')
local.triangular_to l A
l < dim_row A
l < dim_col A
l + k < dim_row A

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>sub1 q k l (r, A) = (r', A'); local.triangular_to l A; l < dim_row A; l < dim_col A; l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
show "sub1 q k l (r,A) = (r',A') \<Longrightarrow> l + k < dim_row A \<Longrightarrow>
    triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
proof (induction k arbitrary: r' A')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub1 q (Suc k) l (r, A) = (r', A'); l + Suc k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub1 q (Suc k) l (r, A) = (r', A')
l + Suc k < dim_row A

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub1 q (Suc k) l (r, A) = (r', A'); l + Suc k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub1 q (Suc k) l (r, A) = (r', A')
l + Suc k < dim_row A
[PROOF STEP]
have "sub1 q (Suc k) l (r,A) = (r',A')"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub1 q (Suc k) l (r, A) = (r', A')
l + Suc k < dim_row A

goal (1 subgoal):
 1. sub1 q (Suc k) l (r, A) = (r', A')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sub1 q (Suc k) l (r, A) = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub1 q (Suc k) l (r, A) = (r', A'); l + Suc k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sub1 q (Suc k) l (r, A) = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub1 q (Suc k) l (r, A) = (r', A'); l + Suc k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
obtain r'' A''
      where rA'': "sub1 q k l (r, A) = (r'',A'')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r'' A''. sub1 q k l (r, A) = (r'', A'') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub1 q k l (r, A) = (r'', A'')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub1 q (Suc k) l (r, A) = (r', A'); l + Suc k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sub1 q (Suc k) l (r, A) = (r', A')
sub1 q k l (r, A) = (r'', A'')
[PROOF STEP]
have rA': "mute q (Suc (l + k)) l (r'',A'') = (r',A')"
[PROOF STATE]
proof (prove)
using this:
sub1 q (Suc k) l (r, A) = (r', A')
sub1 q k l (r, A) = (r'', A'')

goal (1 subgoal):
 1. mute q (Suc (l + k)) l (r'', A'') = (r', A')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mute q (Suc (l + k)) l (r'', A'') = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub1 q (Suc k) l (r, A) = (r', A'); l + Suc k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
have "triangular_to l A''"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A''
[PROOF STEP]
using rA'' Suc
[PROOF STATE]
proof (prove)
using this:
sub1 q k l (r, A) = (r'', A'')
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub1 q (Suc k) l (r, A) = (r', A')
l + Suc k < dim_row A

goal (1 subgoal):
 1. local.triangular_to l A''
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_to l A''

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'; sub1 q (Suc k) l (r, A) = (r', A'); l + Suc k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
local.triangular_to l A''

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
using Suc assms mute_preserves_triangle[OF rA'] rA''
[PROOF STATE]
proof (prove)
using this:
local.triangular_to l A''
\<lbrakk>sub1 q k l (r, A) = (?r', ?A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l ?A'
sub1 q (Suc k) l (r, A) = (r', A')
l + Suc k < dim_row A
sub1 q k l (r, A) = (r', A')
local.triangular_to l A
l < dim_row A
l < dim_col A
l + k < dim_row A
\<lbrakk>local.triangular_to l A''; l < Suc (l + k); Suc (l + k) < dim_row A''; l < dim_row A''; l < dim_col A''\<rbrakk> \<Longrightarrow> local.triangular_to l A'
sub1 q k l (r, A) = (r'', A'')

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal (1 subgoal):
 1. \<And>r' A'. \<lbrakk>sub1 q 0 l (r, A) = (r', A'); l + 0 < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
[PROOF STEP]
qed (insert assms,auto)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub1 q k l (r, A) = (r', A'); l + k < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub1_makes_0s:
  assumes "sub1 (A $$ (l,l)) k l (r,A) = (r',A')"
  and lr: "l < dim_row A"
  and lc: "l < dim_col A"
  and li: "l < i"
  and "i \<le> k + l"
  and "k + l < dim_row A"
  shows "A' $$ (i,l) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $$ (i, l) = (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sub1 (A $$ (l, l)) k l (r, A) = (r', A')
l < dim_row A
l < dim_col A
l < i
i \<le> k + l
k + l < dim_row A

goal (1 subgoal):
 1. A' $$ (i, l) = (0::'a)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); l < dim_row A; l < dim_col A; l < i; i \<le> k + l; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
show "sub1 (A $$ (l,l)) k l (r,A) = (r',A') \<Longrightarrow> i \<le> k + l \<Longrightarrow> k + l < dim_row A \<Longrightarrow>
    A' $$ (i,l) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
using lr lc li
[PROOF STATE]
proof (prove)
using this:
l < dim_row A
l < dim_col A
l < i

goal (1 subgoal):
 1. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
proof (induction k arbitrary: r' A')
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (?r', ?A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> ?A' $$ (i, l) = (0::'a)
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A')
i \<le> Suc k + l
Suc k + l < dim_row A
l < dim_row A
l < dim_col A
l < i

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
obtain r' A' where rA': "sub1 (A $$ (l,l)) k l (r, A) = (r',A')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>r' A'. sub1 (A $$ (l, l)) k l (r, A) = (r', A') \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
fix r'' A''
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
from sub1_preserves_diagnal[OF rA']
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>l < dim_col A; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
[PROOF STEP]
have AA': "A $$ (l, l) = A' $$ (l, l)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>l < dim_col A; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)

goal (1 subgoal):
 1. A $$ (l, l) = A' $$ (l, l)
[PROOF STEP]
using Suc(2-)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>l < dim_col A; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (l, l) = A $$ (l, l)
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'a__, A'a__)
i \<le> Suc k + l
Suc k + l < dim_row A
l < dim_row A
l < dim_col A
l < i

goal (1 subgoal):
 1. A $$ (l, l) = A' $$ (l, l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (l, l) = A' $$ (l, l)

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
assume "sub1 (A $$ (l,l)) (Suc k) l (r, A) = (r'',A'')"
[PROOF STATE]
proof (state)
this:
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'', A'')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'', A'')
[PROOF STEP]
have rA'': "mute (A $$ (l,l)) (Suc (l + k)) l (r', A') = (r'', A'')"
[PROOF STATE]
proof (prove)
using this:
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'', A'')

goal (1 subgoal):
 1. mute (A $$ (l, l)) (Suc (l + k)) l (r', A') = (r'', A'')
[PROOF STEP]
using rA'
[PROOF STATE]
proof (prove)
using this:
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'', A'')
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (1 subgoal):
 1. mute (A $$ (l, l)) (Suc (l + k)) l (r', A') = (r'', A'')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
mute (A $$ (l, l)) (Suc (l + k)) l (r', A') = (r'', A'')

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
have ir: "i < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_row A
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (?r', ?A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> ?A' $$ (i, l) = (0::'a)
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'a__, A'a__)
i \<le> Suc k + l
Suc k + l < dim_row A
l < dim_row A
l < dim_col A
l < i

goal (1 subgoal):
 1. i < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < dim_row A

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
have il: "i \<noteq> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> l
[PROOF STEP]
using li
[PROOF STATE]
proof (prove)
using this:
l < i

goal (1 subgoal):
 1. i \<noteq> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<noteq> l

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
have lr': "l < dim_row A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < dim_row A'
[PROOF STEP]
using lr rA'
[PROOF STATE]
proof (prove)
using this:
l < dim_row A
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (1 subgoal):
 1. l < dim_row A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < dim_row A'

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
have lc': "l < dim_col A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < dim_col A'
[PROOF STEP]
using lc rA'
[PROOF STATE]
proof (prove)
using this:
l < dim_col A
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (1 subgoal):
 1. l < dim_col A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < dim_col A'

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
have Slkr': "Suc (l+k) < dim_row A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (l + k) < dim_row A'
[PROOF STEP]
using Suc rA'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (?r', ?A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> ?A' $$ (i, l) = (0::'a)
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'a__, A'a__)
i \<le> Suc k + l
Suc k + l < dim_row A
l < dim_row A
l < dim_col A
l < i
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (1 subgoal):
 1. Suc (l + k) < dim_row A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (l + k) < dim_row A'

goal (2 subgoals):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
 2. \<And>k r' A'. \<lbrakk>\<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a); sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r', A'); i \<le> Suc k + l; Suc k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
show "A'' $$ (i,l) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A'' $$ (i, l) = (0::'a)
[PROOF STEP]
proof (cases "Suc(l + k) = i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Suc (l + k) = i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
 2. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Suc (l + k) = i

goal (2 subgoals):
 1. Suc (l + k) = i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
 2. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Suc (l + k) = i

goal (2 subgoals):
 1. Suc (l + k) = i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
 2. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
have l: "Suc (l + k) \<noteq> l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (l + k) \<noteq> l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Suc (l + k) \<noteq> l

goal (2 subgoals):
 1. Suc (l + k) = i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
 2. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A'' $$ (i, l) = (0::'a)
[PROOF STEP]
using mute_makes_0[OF mf rA''[unfolded AA'] lr' lc' Slkr' l] ir il rA'
[PROOF STATE]
proof (prove)
using this:
A'' $$ (Suc (l + k), l) = (0::'a)
i < dim_row A
i \<noteq> l
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (1 subgoal):
 1. A'' $$ (i, l) = (0::'a)
[PROOF STEP]
by (simp add:True)
[PROOF STATE]
proof (state)
this:
A'' $$ (i, l) = (0::'a)

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
A'' $$ (i, l) = (0::'a)

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Suc (l + k) \<noteq> i

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Suc (l + k) \<noteq> i

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Suc (l + k) \<noteq> i
[PROOF STEP]
have ikl: "i \<le> k+l"
[PROOF STATE]
proof (prove)
using this:
Suc (l + k) \<noteq> i

goal (1 subgoal):
 1. i \<le> k + l
[PROOF STEP]
using Suc
[PROOF STATE]
proof (prove)
using this:
Suc (l + k) \<noteq> i
\<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (?r', ?A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> ?A' $$ (i, l) = (0::'a)
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'a__, A'a__)
i \<le> Suc k + l
Suc k + l < dim_row A
l < dim_row A
l < dim_col A
l < i

goal (1 subgoal):
 1. i \<le> k + l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> k + l

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
have ir': "i < dim_row A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < dim_row A'
[PROOF STEP]
using ir rA'
[PROOF STATE]
proof (prove)
using this:
i < dim_row A
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (1 subgoal):
 1. i < dim_row A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < dim_row A'

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
have lc': "l < dim_col A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l < dim_col A'
[PROOF STEP]
using lc rA'
[PROOF STATE]
proof (prove)
using this:
l < dim_col A
sub1 (A $$ (l, l)) k l (r, A) = (r', A')

goal (1 subgoal):
 1. l < dim_col A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l < dim_col A'

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
have IH: "A' $$ (i,l) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $$ (i, l) = (0::'a)
[PROOF STEP]
using rA' Suc False
[PROOF STATE]
proof (prove)
using this:
sub1 (A $$ (l, l)) k l (r, A) = (r', A')
\<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (?r', ?A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> ?A' $$ (i, l) = (0::'a)
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'a__, A'a__)
i \<le> Suc k + l
Suc k + l < dim_row A
l < dim_row A
l < dim_col A
l < i
Suc (l + k) \<noteq> i

goal (1 subgoal):
 1. A' $$ (i, l) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' $$ (i, l) = (0::'a)

goal (1 subgoal):
 1. Suc (l + k) \<noteq> i \<Longrightarrow> A'' $$ (i, l) = (0::'a)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
A' $$ (i, l) = (0::'a)

goal (1 subgoal):
 1. A'' $$ (i, l) = (0::'a)
[PROOF STEP]
using mute_preserves[OF rA'' ir' lc'] rA' False Suc
[PROOF STATE]
proof (prove)
using this:
A' $$ (i, l) = (0::'a)
\<lbrakk>l < dim_row A'; Suc (l + k) < dim_row A'; i \<noteq> Suc (l + k)\<rbrakk> \<Longrightarrow> A'' $$ (i, l) = A' $$ (i, l)
sub1 (A $$ (l, l)) k l (r, A) = (r', A')
Suc (l + k) \<noteq> i
\<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (?r', ?A'); i \<le> k + l; k + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> ?A' $$ (i, l) = (0::'a)
sub1 (A $$ (l, l)) (Suc k) l (r, A) = (r'a__, A'a__)
i \<le> Suc k + l
Suc k + l < dim_row A
l < dim_row A
l < dim_col A
l < i

goal (1 subgoal):
 1. A'' $$ (i, l) = (0::'a)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A'' $$ (i, l) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
A'' $$ (i, l) = (0::'a)

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

goal (1 subgoal):
 1. \<And>r' A'. \<lbrakk>sub1 (A $$ (l, l)) 0 l (r, A) = (r', A'); i \<le> 0 + l; 0 + l < dim_row A; l < dim_row A; l < dim_col A; l < i\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>sub1 (A $$ (l, l)) k l (r, A) = (r', A'); i \<le> k + l; k + l < dim_row A\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub1_triangulizes_column:
  assumes rA': "sub1 (A $$ (l,l)) (dim_row A - Suc l) l (r,A) = (r',A')"
  and tri:"triangular_to l A"
  and r: "dim_row A > 0"
  and lr: "l < dim_row A"
  and lc: "l < dim_col A"
  shows "triangular_column l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
proof (intro triangular_columnI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
assume li: "l < i"
[PROOF STATE]
proof (state)
this:
l < i

goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
assume ir: "i < dim_row A'"
[PROOF STATE]
proof (state)
this:
i < dim_row A'

goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
i < dim_row A'

goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
have "... = dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A' = dim_row A
[PROOF STEP]
using sub1_preserves_dimensions[OF rA']
[PROOF STATE]
proof (prove)
using this:
dim_row A' = dim_row A
dim_col A' = dim_col A

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

goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dim_row A' = dim_row A

goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
have "... = dim_row A - l + l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A = dim_row A - l + l
[PROOF STEP]
using lr li
[PROOF STATE]
proof (prove)
using this:
l < dim_row A
l < i

goal (1 subgoal):
 1. dim_row A = dim_row A - l + l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
dim_row A = dim_row A - l + l

goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
i < dim_row A - l + l
[PROOF STEP]
have ir2: "i \<le> dim_row A - l + l"
[PROOF STATE]
proof (prove)
using this:
i < dim_row A - l + l

goal (1 subgoal):
 1. i \<le> dim_row A - l + l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<le> dim_row A - l + l

goal (1 subgoal):
 1. \<And>i. \<lbrakk>l < i; i < dim_row A'\<rbrakk> \<Longrightarrow> A' $$ (i, l) = (0::'a)
[PROOF STEP]
show "A' $$ (i,l) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A' $$ (i, l) = (0::'a)
[PROOF STEP]
apply (subst sub1_makes_0s[OF rA' lr lc])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. l < i
 2. i \<le> dim_row A - Suc l + l
 3. dim_row A - Suc l + l < dim_row A
 4. (0::'a) = (0::'a)
[PROOF STEP]
using li ir assms
[PROOF STATE]
proof (prove)
using this:
l < i
i < dim_row A'
sub1 (A $$ (l, l)) (dim_row A - Suc l) l (r, A) = (r', A')
local.triangular_to l A
0 < dim_row A
l < dim_row A
l < dim_col A

goal (4 subgoals):
 1. l < i
 2. i \<le> dim_row A - Suc l + l
 3. dim_row A - Suc l + l < dim_row A
 4. (0::'a) = (0::'a)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A' $$ (i, l) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sub1_grows_triangle:
  assumes rA': "sub1 (A $$ (l,l)) (dim_row A - Suc l) l (r,A) = (r',A')"
  and r: "dim_row A > 0"
  and tri:"triangular_to l A"
  and lr: "l < dim_row A"
  and lc: "l < dim_col A"
  shows "triangular_to (Suc l) A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
have "triangular_to l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
using sub1_preserves_triangle[OF rA'] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>local.triangular_to l A; l < dim_row A; l < dim_col A; l + (dim_row A - Suc l) < dim_row A\<rbrakk> \<Longrightarrow> local.triangular_to l A'
sub1 (A $$ (l, l)) (dim_row A - Suc l) l (r, A) = (r', A')
0 < dim_row A
local.triangular_to l A
l < dim_row A
l < dim_col A

goal (1 subgoal):
 1. local.triangular_to l A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
local.triangular_to l A'

goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
have "triangular_column l A'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
using sub1_triangulizes_column[OF rA'] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>local.triangular_to l A; 0 < dim_row A; l < dim_row A; l < dim_col A\<rbrakk> \<Longrightarrow> local.triangular_column l A'
sub1 (A $$ (l, l)) (dim_row A - Suc l) l (r, A) = (r', A')
0 < dim_row A
local.triangular_to l A
l < dim_row A
l < dim_col A

goal (1 subgoal):
 1. local.triangular_column l A'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
local.triangular_column l A'

goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
local.triangular_to l A'
local.triangular_column l A'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
local.triangular_to l A'
local.triangular_column l A'

goal (1 subgoal):
 1. local.triangular_to (Suc l) A'
[PROOF STEP]
by (rule triangle_growth)
[PROOF STATE]
proof (state)
this:
local.triangular_to (Suc l) A'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_non0: assumes sel_fun: "det_selection_fun sel_fun"
  and res: "find_non0 l A = Some m"
  shows "A $$ (m,l) \<noteq> 0" "l < m" "m < dim_row A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $$ (m, l) \<noteq> (0::'a) &&& l < m &&& m < dim_row A
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. A $$ (m, l) \<noteq> (0::'a)
 2. l < m
 3. m < dim_row A
[PROOF STEP]
let ?xs = "filter (\<lambda> (i,Ail). Ail \<noteq> 0) (map (\<lambda> i. (i, A $$ (i,l))) [Suc l..<dim_row A])"
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. A $$ (m, l) \<noteq> (0::'a)
 2. l < m
 3. m < dim_row A
[PROOF STEP]
from res[unfolded find_non0_def Let_def]
[PROOF STATE]
proof (chain)
picking this:
(case filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) of [] \<Rightarrow> None | a # list \<Rightarrow> Some (sel_fun (filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A])))) = Some m
[PROOF STEP]
have xs: "?xs \<noteq> []" and m: "m = sel_fun ?xs"
[PROOF STATE]
proof (prove)
using this:
(case filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) of [] \<Rightarrow> None | a # list \<Rightarrow> Some (sel_fun (filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A])))) = Some m

goal (1 subgoal):
 1. filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) \<noteq> [] &&& m = sel_fun (filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]))
[PROOF STEP]
by (cases ?xs, auto)+
[PROOF STATE]
proof (state)
this:
filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) \<noteq> []
m = sel_fun (filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]))

goal (3 subgoals):
 1. A $$ (m, l) \<noteq> (0::'a)
 2. l < m
 3. m < dim_row A
[PROOF STEP]
from det_selection_funD[OF sel_fun xs, folded m]
[PROOF STATE]
proof (chain)
picking this:
m \<in> fst ` set (filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]))
[PROOF STEP]
show "A $$ (m, l) \<noteq> 0" "l < m" "m < dim_row A"
[PROOF STATE]
proof (prove)
using this:
m \<in> fst ` set (filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]))

goal (1 subgoal):
 1. A $$ (m, l) \<noteq> (0::'a) &&& l < m &&& m < dim_row A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A $$ (m, l) \<noteq> (0::'a)
l < m
m < dim_row A

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma find_non0_all0:
  "find_non0 l A = None \<Longrightarrow> triangular_column l A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. find_non0 l A = None \<Longrightarrow> local.triangular_column l A
[PROOF STEP]
proof (intro triangular_columnI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>find_non0 l A = None; l < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, l) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>find_non0 l A = None; l < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, l) = (0::'a)
[PROOF STEP]
let ?xs = "filter (\<lambda> (i,Ail). Ail \<noteq> 0) (map (\<lambda> i. (i, A $$ (i,l))) [Suc l..<dim_row A])"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. \<lbrakk>find_non0 l A = None; l < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, l) = (0::'a)
[PROOF STEP]
assume none: "find_non0 l A = None" and li: "l < i" "i < dim_row A"
[PROOF STATE]
proof (state)
this:
find_non0 l A = None
l < i
i < dim_row A

goal (1 subgoal):
 1. \<And>i. \<lbrakk>find_non0 l A = None; l < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, l) = (0::'a)
[PROOF STEP]
from none
[PROOF STATE]
proof (chain)
picking this:
find_non0 l A = None
[PROOF STEP]
have xs: "?xs = []"
[PROOF STATE]
proof (prove)
using this:
find_non0 l A = None

goal (1 subgoal):
 1. filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) = []
[PROOF STEP]
unfolding find_non0_def Let_def
[PROOF STATE]
proof (prove)
using this:
(case filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) of [] \<Rightarrow> None | a # list \<Rightarrow> Some (sel_fun (filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A])))) = None

goal (1 subgoal):
 1. filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) = []
[PROOF STEP]
by (cases ?xs, auto)
[PROOF STATE]
proof (state)
this:
filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) = []

goal (1 subgoal):
 1. \<And>i. \<lbrakk>find_non0 l A = None; l < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, l) = (0::'a)
[PROOF STEP]
from li
[PROOF STATE]
proof (chain)
picking this:
l < i
i < dim_row A
[PROOF STEP]
have "(i, A $$ (i,l)) \<in> set (map (\<lambda> i. (i, A $$ (i,l))) [Suc l..<dim_row A])"
[PROOF STATE]
proof (prove)
using this:
l < i
i < dim_row A

goal (1 subgoal):
 1. (i, A $$ (i, l)) \<in> set (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(i, A $$ (i, l)) \<in> set (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A])

goal (1 subgoal):
 1. \<And>i. \<lbrakk>find_non0 l A = None; l < i; i < dim_row A\<rbrakk> \<Longrightarrow> A $$ (i, l) = (0::'a)
[PROOF STEP]
with xs
[PROOF STATE]
proof (chain)
picking this:
filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) = []
(i, A $$ (i, l)) \<in> set (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A])
[PROOF STEP]
show "A $$ (i,l) = 0"
[PROOF STATE]
proof (prove)
using this:
filter (\<lambda>(i, Ail). Ail \<noteq> (0::'a)) (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A]) = []
(i, A $$ (i, l)) \<in> set (map (\<lambda>i. (i, A $$ (i, l))) [Suc l..<dim_row A])

goal (1 subgoal):
 1. A $$ (i, l) = (0::'a)
[PROOF STEP]
by (metis (mono_tags) xs case_prodI filter_empty_conv)
[PROOF STATE]
proof (state)
this:
A $$ (i, l) = (0::'a)

goal:
No subgoals!
[PROOF STEP]
qed