[STATEMENT]
lemma rref_implies_rref_upt:
fixes A::"'a::{one,zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
shows "reduced_row_echelon_form_upt_k A k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reduced_row_echelon_form_upt_k A k
[PROOF STEP]
proof (rule reduced_row_echelon_form_upt_k_intro)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
 2. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
 3. \<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 4. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
show "\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_condition2[OF rref] is_zero_row_imp_is_zero_row_upt
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
is_zero_row ?i ?A \<Longrightarrow> is_zero_row_upt_k ?i ?k ?A

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)

goal (3 subgoals):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
 2. \<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
 3. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
show "\<forall>i. i < i + 1 \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + 1) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ (i + 1) $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
using rref_condition3[OF rref] is_zero_row_imp_is_zero_row_upt
[PROOF STATE]
proof (prove)
using this:
\<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row i A \<and> \<not> is_zero_row (i + (1::'rows)) A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
is_zero_row ?i ?A \<Longrightarrow> is_zero_row_upt_k ?i ?k ?A

goal (1 subgoal):
 1. \<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. i < i + (1::'rows) \<and> \<not> is_zero_row_upt_k i k A \<and> \<not> is_zero_row_upt_k (i + (1::'rows)) k A \<longrightarrow> (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ (i + (1::'rows)) $ n \<noteq> (0::'a))

goal (2 subgoals):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
 2. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
show "\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> 0) = 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
using rref_condition4[OF rref] is_zero_row_imp_is_zero_row_upt
[PROOF STATE]
proof (prove)
using this:
\<forall>i. \<not> is_zero_row i A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
is_zero_row ?i ?A \<Longrightarrow> is_zero_row_upt_k ?i ?k ?A

goal (1 subgoal):
 1. \<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i. \<not> is_zero_row_upt_k i k A \<longrightarrow> (\<forall>j. i \<noteq> j \<longrightarrow> A $ j $ (LEAST n. A $ i $ n \<noteq> (0::'a)) = (0::'a))

goal (1 subgoal):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
[PROOF STEP]
show "\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)
[PROOF STEP]
proof (auto, rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
fix i j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
assume zero_i_k: "is_zero_row_upt_k i k A" and i_less_j: "i < j"
and not_zero_j_k:"\<not> is_zero_row_upt_k j k A"
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i k A
i < j
\<not> is_zero_row_upt_k j k A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have not_zero_j: "\<not> is_zero_row j A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row j A
[PROOF STEP]
using is_zero_row_imp_is_zero_row_upt not_zero_j_k
[PROOF STATE]
proof (prove)
using this:
is_zero_row ?i ?A \<Longrightarrow> is_zero_row_upt_k ?i ?k ?A
\<not> is_zero_row_upt_k j k A

goal (1 subgoal):
 1. \<not> is_zero_row j A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row j A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
hence not_zero_i: "\<not> is_zero_row i A"
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row j A

goal (1 subgoal):
 1. \<not> is_zero_row i A
[PROOF STEP]
using rref_condition1[OF rref] i_less_j
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row j A
\<forall>i. is_zero_row i A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row j A)
i < j

goal (1 subgoal):
 1. \<not> is_zero_row i A
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row i A

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have Least_less: "(LEAST n. A $ i $ n \<noteq> 0) < (LEAST n. A $ j $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
[PROOF STEP]
by (rule rref_condition3_equiv[OF rref i_less_j not_zero_i not_zero_j])
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
have "(LEAST n. A $ j $ n \<noteq> 0) < (LEAST n. A $ i $ n \<noteq> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ j $ n \<noteq> (0::'a)) < (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
proof (rule LeastI2_ex)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>a. A $ i $ a \<noteq> (0::'a)
 2. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
show "\<exists>a. A $ i $ a \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>a. A $ i $ a \<noteq> (0::'a)
[PROOF STEP]
using not_zero_i
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row i A

goal (1 subgoal):
 1. \<exists>a. A $ i $ a \<noteq> (0::'a)
[PROOF STEP]
unfolding is_zero_row_def is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>j. mod_type_class.to_nat j < ncols A \<longrightarrow> A $ i $ j = (0::'a))

goal (1 subgoal):
 1. \<exists>a. A $ i $ a \<noteq> (0::'a)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
\<exists>a. A $ i $ a \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
assume Aix_not_0: "A $ i $ x \<noteq> 0"
[PROOF STATE]
proof (state)
this:
A $ i $ x \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
have k_less_x: "k \<le> to_nat x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k \<le> mod_type_class.to_nat x
[PROOF STEP]
using zero_i_k Aix_not_0
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i k A
A $ i $ x \<noteq> (0::'a)

goal (1 subgoal):
 1. k \<le> mod_type_class.to_nat x
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < k \<longrightarrow> A $ i $ j = (0::'a)
A $ i $ x \<noteq> (0::'a)

goal (1 subgoal):
 1. k \<le> mod_type_class.to_nat x
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
k \<le> mod_type_class.to_nat x

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
hence k_less_ncols: "k < ncols A"
[PROOF STATE]
proof (prove)
using this:
k \<le> mod_type_class.to_nat x

goal (1 subgoal):
 1. k < ncols A
[PROOF STEP]
unfolding ncols_def
[PROOF STATE]
proof (prove)
using this:
k \<le> mod_type_class.to_nat x

goal (1 subgoal):
 1. k < CARD('cols)
[PROOF STEP]
using to_nat_less_card[of x]
[PROOF STATE]
proof (prove)
using this:
k \<le> mod_type_class.to_nat x
mod_type_class.to_nat x < CARD('cols)

goal (1 subgoal):
 1. k < CARD('cols)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
k < ncols A

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
obtain s where Ajs_not_zero: "A $ j $ s \<noteq> 0" and s_less_k: "to_nat s < k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrakk>A $ j $ s \<noteq> (0::'a); mod_type_class.to_nat s < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using not_zero_j_k
[PROOF STATE]
proof (prove)
using this:
\<not> is_zero_row_upt_k j k A

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>A $ j $ s \<noteq> (0::'a); mod_type_class.to_nat s < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>ja. mod_type_class.to_nat ja < k \<longrightarrow> A $ j $ ja = (0::'a))

goal (1 subgoal):
 1. (\<And>s. \<lbrakk>A $ j $ s \<noteq> (0::'a); mod_type_class.to_nat s < k\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A $ j $ s \<noteq> (0::'a)
mod_type_class.to_nat s < k

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
have "(LEAST n. A $ j $ n \<noteq> 0) \<le> s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ j $ n \<noteq> (0::'a)) \<le> s
[PROOF STEP]
using Ajs_not_zero Least_le
[PROOF STATE]
proof (prove)
using this:
A $ j $ s \<noteq> (0::'a)
?P ?k \<Longrightarrow> (LEAST x. ?P x) \<le> ?k

goal (1 subgoal):
 1. (LEAST n. A $ j $ n \<noteq> (0::'a)) \<le> s
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ j $ n \<noteq> (0::'a)) \<le> s

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ j $ n \<noteq> (0::'a)) \<le> s

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
have "... = from_nat (to_nat s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = mod_type_class.from_nat (mod_type_class.to_nat s)
[PROOF STEP]
unfolding from_nat_to_nat_id
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s = s
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
s = mod_type_class.from_nat (mod_type_class.to_nat s)

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
s = mod_type_class.from_nat (mod_type_class.to_nat s)

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
have "... < from_nat k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat (mod_type_class.to_nat s) < mod_type_class.from_nat k
[PROOF STEP]
by (rule from_nat_mono[OF s_less_k k_less_ncols[unfolded ncols_def]])
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (mod_type_class.to_nat s) < mod_type_class.from_nat k

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat (mod_type_class.to_nat s) < mod_type_class.from_nat k

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
have "... \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.from_nat k \<le> x
[PROOF STEP]
using k_less_x leD not_le_imp_less to_nat_le
[PROOF STATE]
proof (prove)
using this:
k \<le> mod_type_class.to_nat x
?y \<le> ?x \<Longrightarrow> \<not> ?x < ?y
\<not> ?y \<le> ?x \<Longrightarrow> ?x < ?y
?y < mod_type_class.from_nat ?k \<Longrightarrow> mod_type_class.to_nat ?y < ?k

goal (1 subgoal):
 1. mod_type_class.from_nat k \<le> x
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
mod_type_class.from_nat k \<le> x

goal (1 subgoal):
 1. \<And>x. A $ i $ x \<noteq> (0::'a) \<Longrightarrow> (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
show "(LEAST n. A $ j $ n \<noteq> 0) < x"
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ j $ n \<noteq> (0::'a)) < x

goal (1 subgoal):
 1. (LEAST n. A $ j $ n \<noteq> (0::'a)) < x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ j $ n \<noteq> (0::'a)) < x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ j $ n \<noteq> (0::'a)) < (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. \<And>i j. \<lbrakk>is_zero_row_upt_k i k A; i < j; \<not> is_zero_row_upt_k j k A\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
(LEAST n. A $ j $ n \<noteq> (0::'a)) < (LEAST n. A $ i $ n \<noteq> (0::'a))
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ i $ n \<noteq> (0::'a)) < (LEAST n. A $ j $ n \<noteq> (0::'a))
(LEAST n. A $ j $ n \<noteq> (0::'a)) < (LEAST n. A $ i $ n \<noteq> (0::'a))

goal (1 subgoal):
 1. False
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. is_zero_row_upt_k i k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j k A)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rref_first_position_zero_imp_column_0:
fixes A::"'a::{one,zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and A_00: "A $ 0 $ 0 = 0"
shows "column 0 A = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. column (0::'cols) A = 0
[PROOF STEP]
proof (unfold column_def, vector, clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A $ i $ (0::'cols) = (0::'a)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. A $ i $ (0::'cols) = (0::'a)
[PROOF STEP]
have "is_zero_row_upt_k 0 1 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k (0::'rows) 1 A
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < 1 \<longrightarrow> A $ (0::'rows) $ j = (0::'a)
[PROOF STEP]
using A_00
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) = (0::'a)

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < 1 \<longrightarrow> A $ (0::'rows) $ j = (0::'a)
[PROOF STEP]
by (metis One_nat_def less_Suc0 to_nat_eq_0)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k (0::'rows) 1 A

goal (1 subgoal):
 1. \<And>i. A $ i $ (0::'cols) = (0::'a)
[PROOF STEP]
hence "is_zero_row_upt_k i 1 A"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (0::'rows) 1 A

goal (1 subgoal):
 1. is_zero_row_upt_k i 1 A
[PROOF STEP]
using rref_upt_condition1[OF rref_implies_rref_upt[OF rref]]
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (0::'rows) 1 A
\<forall>i. is_zero_row_upt_k i ?k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j ?k A)

goal (1 subgoal):
 1. is_zero_row_upt_k i 1 A
[PROOF STEP]
using least_mod_type less_le
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (0::'rows) 1 A
\<forall>i. is_zero_row_upt_k i ?k A \<longrightarrow> \<not> (\<exists>j>i. \<not> is_zero_row_upt_k j ?k A)
(0::?'a) \<le> ?n
(?x < ?y) = (?x \<le> ?y \<and> ?x \<noteq> ?y)

goal (1 subgoal):
 1. is_zero_row_upt_k i 1 A
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k i 1 A

goal (1 subgoal):
 1. \<And>i. A $ i $ (0::'cols) = (0::'a)
[PROOF STEP]
thus "A $ i $ 0 = 0"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k i 1 A

goal (1 subgoal):
 1. A $ i $ (0::'cols) = (0::'a)
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < 1 \<longrightarrow> A $ i $ j = (0::'a)

goal (1 subgoal):
 1. A $ i $ (0::'cols) = (0::'a)
[PROOF STEP]
using to_nat_eq_0
[PROOF STATE]
proof (prove)
using this:
\<forall>j. mod_type_class.to_nat j < 1 \<longrightarrow> A $ i $ j = (0::'a)
(mod_type_class.to_nat ?x = 0) = (?x = (0::?'a))

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rref_first_element:
fixes A::"'a::{one,zero}^'cols::{mod_type}^'rows::{mod_type}"
assumes rref: "reduced_row_echelon_form A"
and column_not_0: "column 0 A \<noteq> 0"
shows "A $ 0 $ 0 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (1::'a)
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a) \<Longrightarrow> False
[PROOF STEP]
have A_00_not_0: "A $ 0 $ 0 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (0::'a)
[PROOF STEP]
proof (rule ccontr, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (0::'a) \<Longrightarrow> False
[PROOF STEP]
assume A_00: "A $ 0 $ 0 = 0"
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ (0::'cols) = (0::'a)

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (0::'a) \<Longrightarrow> False
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
A $ (0::'rows) $ (0::'cols) = (0::'a)
[PROOF STEP]
obtain i where Ai0: "A $ i $ 0 \<noteq> 0" and i: "i>0"
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) = (0::'a)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>A $ i $ (0::'cols) \<noteq> (0::'a); (0::'rows) < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using column_not_0
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) = (0::'a)
column (0::'cols) A \<noteq> 0

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>A $ i $ (0::'cols) \<noteq> (0::'a); (0::'rows) < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding column_def
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) = (0::'a)
(\<chi>i. A $ i $ (0::'cols)) \<noteq> 0

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>A $ i $ (0::'cols) \<noteq> (0::'a); (0::'rows) < i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis column_def rref rref_first_position_zero_imp_column_0)
[PROOF STATE]
proof (state)
this:
A $ i $ (0::'cols) \<noteq> (0::'a)
(0::'rows) < i

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (0::'a) \<Longrightarrow> False
[PROOF STEP]
have "is_zero_row_upt_k 0 1 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_zero_row_upt_k (0::'rows) 1 A
[PROOF STEP]
unfolding is_zero_row_upt_k_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < 1 \<longrightarrow> A $ (0::'rows) $ j = (0::'a)
[PROOF STEP]
using A_00
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) = (0::'a)

goal (1 subgoal):
 1. \<forall>j. mod_type_class.to_nat j < 1 \<longrightarrow> A $ (0::'rows) $ j = (0::'a)
[PROOF STEP]
by (metis One_nat_def less_Suc0 to_nat_eq_0)
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k (0::'rows) 1 A

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (0::'a) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
is_zero_row_upt_k (0::'rows) 1 A

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (0::'a) \<Longrightarrow> False
[PROOF STEP]
have "\<not> is_zero_row_upt_k i 1 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i 1 A
[PROOF STEP]
using Ai0
[PROOF STATE]
proof (prove)
using this:
A $ i $ (0::'cols) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<not> is_zero_row_upt_k i 1 A
[PROOF STEP]
by (metis is_zero_row_upt_k_def to_nat_0 zero_less_one)
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row_upt_k i 1 A

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (0::'a) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
is_zero_row_upt_k (0::'rows) 1 A
\<not> is_zero_row_upt_k i 1 A
[PROOF STEP]
have "\<not> reduced_row_echelon_form A"
[PROOF STATE]
proof (prove)
using this:
is_zero_row_upt_k (0::'rows) 1 A
\<not> is_zero_row_upt_k i 1 A

goal (1 subgoal):
 1. \<not> reduced_row_echelon_form A
[PROOF STEP]
by (metis A_00 column_not_0 rref_first_position_zero_imp_column_0)
[PROOF STATE]
proof (state)
this:
\<not> reduced_row_echelon_form A

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) = (0::'a) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
\<not> reduced_row_echelon_form A

goal (1 subgoal):
 1. False
[PROOF STEP]
using rref
[PROOF STATE]
proof (prove)
using this:
\<not> reduced_row_echelon_form A
reduced_row_echelon_form A

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ (0::'cols) \<noteq> (0::'a)

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a) \<Longrightarrow> False
[PROOF STEP]
assume A_00_not_1: "A $ 0 $ 0 \<noteq> 1"
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a)

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a) \<Longrightarrow> False
[PROOF STEP]
have Least_eq_0: "(LEAST n. A $ 0 $ n \<noteq> 0) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (0::'cols)
[PROOF STEP]
proof (rule Least_equality)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (0::'a)
 2. \<And>y. A $ (0::'rows) $ y \<noteq> (0::'a) \<Longrightarrow> (0::'cols) \<le> y
[PROOF STEP]
show "A $ 0 $ 0 \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (0::'a)
[PROOF STEP]
by (rule A_00_not_0)
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ (0::'cols) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<And>y. A $ (0::'rows) $ y \<noteq> (0::'a) \<Longrightarrow> (0::'cols) \<le> y
[PROOF STEP]
show "\<And>y. A $ 0 $ y \<noteq> 0 \<Longrightarrow> 0 \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. A $ (0::'rows) $ y \<noteq> (0::'a) \<Longrightarrow> (0::'cols) \<le> y
[PROOF STEP]
using least_mod_type
[PROOF STATE]
proof (prove)
using this:
(0::?'a) \<le> ?n

goal (1 subgoal):
 1. \<And>y. A $ (0::'rows) $ y \<noteq> (0::'a) \<Longrightarrow> (0::'cols) \<le> y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ ?y \<noteq> (0::'a) \<Longrightarrow> (0::'cols) \<le> ?y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (0::'cols)

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a) \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (0::'cols)

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a) \<Longrightarrow> False
[PROOF STEP]
have "\<not> is_zero_row 0 A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> is_zero_row (0::'rows) A
[PROOF STEP]
unfolding is_zero_row_def is_zero_row_upt_k_def ncols_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < CARD('cols) \<longrightarrow> A $ (0::'rows) $ j = (0::'a))
[PROOF STEP]
using A_00_not_0
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) \<noteq> (0::'a)

goal (1 subgoal):
 1. \<not> (\<forall>j. mod_type_class.to_nat j < CARD('cols) \<longrightarrow> A $ (0::'rows) $ j = (0::'a))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> is_zero_row (0::'rows) A

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a) \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (0::'cols)
\<not> is_zero_row (0::'rows) A
[PROOF STEP]
have "A $ 0 $ (LEAST n. A $ 0 $ n \<noteq> 0) = 1"
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (0::'cols)
\<not> is_zero_row (0::'rows) A

goal (1 subgoal):
 1. A $ (0::'rows) $ (LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
using rref_condition2[OF rref]
[PROOF STATE]
proof (prove)
using this:
(LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (0::'cols)
\<not> is_zero_row (0::'rows) A
\<forall>i. \<not> is_zero_row i A \<longrightarrow> A $ i $ (LEAST k. A $ i $ k \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. A $ (0::'rows) $ (LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (1::'a)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
A $ (0::'rows) $ (LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a) \<Longrightarrow> False
[PROOF STEP]
thus False
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (LEAST n. A $ (0::'rows) $ n \<noteq> (0::'a)) = (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
unfolding Least_eq_0
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) = (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
using A_00_not_1
[PROOF STATE]
proof (prove)
using this:
A $ (0::'rows) $ (0::'cols) = (1::'a)
A $ (0::'rows) $ (0::'cols) \<noteq> (1::'a)

goal (1 subgoal):
 1. False
[PROOF STEP]
by contradiction
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weak_mat_gt_mono: assumes sd_n: "sd \<le> n" and
    orient: "\<And> A B. A \<in> carrier_mat n n \<Longrightarrow> B \<in> carrier_mat n n \<Longrightarrow> (A,B) \<in> set ABs \<Longrightarrow> weak_mat_gt sd A B"
   shows "\<exists> gt bound. mono_matrix_carrier gt default bound mono
   \<and> (\<forall> A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
let ?n = "[0 ..< n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
let ?m1x = "[ A $$ (i,j) . A <- map fst ABs, i <- ?n, j <- ?n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
let ?m2y = "[ B $$ (i,j) . B <- map snd ABs, i <- ?n, j <- ?n]"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
let ?pairs = "concat (map (\<lambda> x. map (\<lambda> y. (x,y)) ?m2y) ?m1x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
let ?strict = "filter (\<lambda> (x,y). weak_gt x y) ?pairs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
have "\<forall> x y. (x,y) \<in> set ?strict \<longrightarrow> weak_gt x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. (x, y) \<in> set (filter (\<lambda>(x, y). weak_gt x y) (concat (map (\<lambda>x. map (Pair x) (concat (map (\<lambda>B. concat (map (\<lambda>i. map (\<lambda>j. B $$ (i, j)) [0..<n]) [0..<n])) (map snd ABs)))) (concat (map (\<lambda>A. concat (map (\<lambda>i. map (\<lambda>j. A $$ (i, j)) [0..<n]) [0..<n])) (map fst ABs)))))) \<longrightarrow> weak_gt x y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x y. (x, y) \<in> set (filter (\<lambda>(x, y). weak_gt x y) (concat (map (\<lambda>x. map (Pair x) (concat (map (\<lambda>B. concat (map (\<lambda>i. map (\<lambda>j. B $$ (i, j)) [0..<n]) [0..<n])) (map snd ABs)))) (concat (map (\<lambda>A. concat (map (\<lambda>i. map (\<lambda>j. A $$ (i, j)) [0..<n]) [0..<n])) (map fst ABs)))))) \<longrightarrow> weak_gt x y

goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
from weak_gt_mono[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>x y. (x, y) \<in> set (filter (\<lambda>(x, y). weak_gt x y) (concat (map (\<lambda>x. map (Pair x) (concat (map (\<lambda>B. concat (map (\<lambda>i. map (\<lambda>j. B $$ (i, j)) [0..<n]) [0..<n])) (map snd ABs)))) (concat (map (\<lambda>A. concat (map (\<lambda>i. map (\<lambda>j. A $$ (i, j)) [0..<n]) [0..<n])) (map fst ABs)))))) \<longrightarrow> gt x y)
[PROOF STEP]
obtain gt bound where order: "mono_matrix_carrier gt default bound mono"
    and orient2: "\<And> x y. (x, y) \<in> set ?strict \<Longrightarrow> gt x y"
[PROOF STATE]
proof (prove)
using this:
\<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>x y. (x, y) \<in> set (filter (\<lambda>(x, y). weak_gt x y) (concat (map (\<lambda>x. map (Pair x) (concat (map (\<lambda>B. concat (map (\<lambda>i. map (\<lambda>j. B $$ (i, j)) [0..<n]) [0..<n])) (map snd ABs)))) (concat (map (\<lambda>A. concat (map (\<lambda>i. map (\<lambda>j. A $$ (i, j)) [0..<n]) [0..<n])) (map fst ABs)))))) \<longrightarrow> gt x y)

goal (1 subgoal):
 1. (\<And>gt bound. \<lbrakk>mono_matrix_carrier gt default bound mono; \<And>x y. (x, y) \<in> set (filter (\<lambda>(x, y). weak_gt x y) (concat (map (\<lambda>x. map (Pair x) (concat (map (\<lambda>B. concat (map (\<lambda>i. map (\<lambda>j. B $$ (i, j)) [0..<n]) [0..<n])) (map snd ABs)))) (concat (map (\<lambda>A. concat (map (\<lambda>i. map (\<lambda>j. A $$ (i, j)) [0..<n]) [0..<n])) (map fst ABs)))))) \<Longrightarrow> gt x y\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mono_matrix_carrier gt default bound mono
(?x, ?y) \<in> set (filter (\<lambda>(x, y). weak_gt x y) (concat (map (\<lambda>x. map (Pair x) (concat (map (\<lambda>B. concat (map (\<lambda>i. map (\<lambda>j. B $$ (i, j)) [0..<n]) [0..<n])) (map snd ABs)))) (concat (map (\<lambda>A. concat (map (\<lambda>i. map (\<lambda>j. A $$ (i, j)) [0..<n]) [0..<n])) (map fst ABs)))))) \<Longrightarrow> gt ?x ?y

goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)
[PROOF STEP]
proof (intro exI allI conjI impI, rule order)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>A \<in> carrier_mat n n; B \<in> carrier_mat n n; (A, B) \<in> set ABs\<rbrakk> \<Longrightarrow> mat_gt gt sd A B
[PROOF STEP]
fix A B
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>A B. \<lbrakk>A \<in> carrier_mat n n; B \<in> carrier_mat n n; (A, B) \<in> set ABs\<rbrakk> \<Longrightarrow> mat_gt gt sd A B
[PROOF STEP]
assume A: "A \<in> carrier_mat n n" and B: "B \<in> carrier_mat n n"
      and AB: "(A, B) \<in> set ABs"
[PROOF STATE]
proof (state)
this:
A \<in> carrier_mat n n
B \<in> carrier_mat n n
(A, B) \<in> set ABs

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>A \<in> carrier_mat n n; B \<in> carrier_mat n n; (A, B) \<in> set ABs\<rbrakk> \<Longrightarrow> mat_gt gt sd A B
[PROOF STEP]
from orient[OF this]
[PROOF STATE]
proof (chain)
picking this:
weak_mat_gt sd A B
[PROOF STEP]
have "mat_gt weak_gt sd A B"
[PROOF STATE]
proof (prove)
using this:
weak_mat_gt sd A B

goal (1 subgoal):
 1. weak_mat_gt sd A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
weak_mat_gt sd A B

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>A \<in> carrier_mat n n; B \<in> carrier_mat n n; (A, B) \<in> set ABs\<rbrakk> \<Longrightarrow> mat_gt gt sd A B
[PROOF STEP]
from mat_gtD[OF this]
[PROOF STATE]
proof (chain)
picking this:
A \<ge>\<^sub>m B
\<exists>i<sd. \<exists>j<sd. weak_gt (A $$ (i, j)) (B $$ (i, j))
[PROOF STEP]
obtain i j where
      ge: "A \<ge>\<^sub>m B" and ij: "i < sd" "j < sd" and wgt: "weak_gt (A $$ (i,j)) (B $$ (i,j))"
[PROOF STATE]
proof (prove)
using this:
A \<ge>\<^sub>m B
\<exists>i<sd. \<exists>j<sd. weak_gt (A $$ (i, j)) (B $$ (i, j))

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>A \<ge>\<^sub>m B; i < sd; j < sd; weak_gt (A $$ (i, j)) (B $$ (i, j))\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<ge>\<^sub>m B
i < sd
j < sd
weak_gt (A $$ (i, j)) (B $$ (i, j))

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>A \<in> carrier_mat n n; B \<in> carrier_mat n n; (A, B) \<in> set ABs\<rbrakk> \<Longrightarrow> mat_gt gt sd A B
[PROOF STEP]
from ij \<open>sd \<le> n\<close>
[PROOF STATE]
proof (chain)
picking this:
i < sd
j < sd
sd \<le> n
[PROOF STEP]
have ij': "i < n" "j < n"
[PROOF STATE]
proof (prove)
using this:
i < sd
j < sd
sd \<le> n

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

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>A \<in> carrier_mat n n; B \<in> carrier_mat n n; (A, B) \<in> set ABs\<rbrakk> \<Longrightarrow> mat_gt gt sd A B
[PROOF STEP]
have gt: "gt (A $$ (i,j)) (B $$ (i,j))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gt (A $$ (i, j)) (B $$ (i, j))
[PROOF STEP]
by (rule orient2, insert ij' AB wgt, force)
[PROOF STATE]
proof (state)
this:
gt (A $$ (i, j)) (B $$ (i, j))

goal (1 subgoal):
 1. \<And>A B. \<lbrakk>A \<in> carrier_mat n n; B \<in> carrier_mat n n; (A, B) \<in> set ABs\<rbrakk> \<Longrightarrow> mat_gt gt sd A B
[PROOF STEP]
show "mat_gt gt sd A B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_gt gt sd A B
[PROOF STEP]
using ij gt ge
[PROOF STATE]
proof (prove)
using this:
i < sd
j < sd
gt (A $$ (i, j)) (B $$ (i, j))
A \<ge>\<^sub>m B

goal (1 subgoal):
 1. mat_gt gt sd A B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
mat_gt gt sd A B

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>gt bound. mono_matrix_carrier gt default bound mono \<and> (\<forall>A B. A \<in> carrier_mat n n \<longrightarrow> B \<in> carrier_mat n n \<longrightarrow> (A, B) \<in> set ABs \<longrightarrow> mat_gt gt sd A B)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma int_complexity:
  "mono_matrix_carrier ((>) :: int \<Rightarrow> int \<Rightarrow> bool) 1 nat int_mono"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono_matrix_carrier (\<lambda>x y. y < x) 1 nat int_mono
[PROOF STEP]
proof (unfold_locales)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat b \<le> nat a
 2. \<And>a b. nat (a + b) \<le> nat a + nat b
 3. \<And>a n. 0 \<le> a \<Longrightarrow> nat (a + int n) = nat a + nat (int n)
 4. nat 0 = 0
 5. 1 \<le> nat 1
 6. \<And>a. deriv_bound {(a, b). 0 \<le> b \<and> b < a} a (nat a)
 7. \<And>x y z. \<lbrakk>int_mono x; z < y; 0 \<le> x\<rbrakk> \<Longrightarrow> x * z < x * y
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat b \<le> nat a
 2. \<And>a b. nat (a + b) \<le> nat a + nat b
 3. \<And>a n. 0 \<le> a \<Longrightarrow> nat (a + int n) = nat a + nat (int n)
 4. nat 0 = 0
 5. 1 \<le> nat 1
 6. \<And>a. deriv_bound {(a, b). 0 \<le> b \<and> b < a} a (nat a)
 7. \<And>x y z. \<lbrakk>int_mono x; z < y; 0 \<le> x\<rbrakk> \<Longrightarrow> x * z < x * y
[PROOF STEP]
let ?R = "{(x, y). 0 \<le> (y :: int) \<and> y < x}"
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat b \<le> nat a
 2. \<And>a b. nat (a + b) \<le> nat a + nat b
 3. \<And>a n. 0 \<le> a \<Longrightarrow> nat (a + int n) = nat a + nat (int n)
 4. nat 0 = 0
 5. 1 \<le> nat 1
 6. \<And>a. deriv_bound {(a, b). 0 \<le> b \<and> b < a} a (nat a)
 7. \<And>x y z. \<lbrakk>int_mono x; z < y; 0 \<le> x\<rbrakk> \<Longrightarrow> x * z < x * y
[PROOF STEP]
show "deriv_bound ?R x (nat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv_bound {(x, y). 0 \<le> y \<and> y < x} x (nat x)
[PROOF STEP]
unfolding deriv_bound_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists> y. (x,y) \<in> ?R ^^ Suc (nat x))"
[PROOF STATE]
proof (state)
this:
\<exists>y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x)
[PROOF STEP]
obtain y where xy: "(x,y) \<in> ?R ^^ Suc (nat x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x)

goal (1 subgoal):
 1. (\<And>y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x)
[PROOF STEP]
have y: "0 \<le> y"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x)

goal (1 subgoal):
 1. 0 \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> y

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
obtain n where n: "n = Suc (nat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n = Suc (nat x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = Suc (nat x)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
from xy[unfolded n[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n
[PROOF STEP]
have "x \<ge> y + int n"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n

goal (1 subgoal):
 1. y + int n \<le> x
[PROOF STEP]
proof (induct n arbitrary: x y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ 0 \<Longrightarrow> y + int 0 \<le> x
 2. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> 0 \<le> y \<and> y < x} ^^ 0

goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ 0 \<Longrightarrow> y + int 0 \<le> x
 2. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> 0 \<le> y \<and> y < x} ^^ 0

goal (1 subgoal):
 1. y + int 0 \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + int 0 \<le> x

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(?x, ?y) \<in> {a. case a of (x, y) \<Rightarrow> 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> ?y + int n \<le> ?x
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> 0 \<le> y \<and> y < x} ^^ Suc n

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
from Suc(2)
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> 0 \<le> y \<and> y < x} ^^ Suc n
[PROOF STEP]
obtain z where xz: "(x,z) \<in> ?R ^^ n" and zy: "(z,y) \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> 0 \<le> y \<and> y < x} ^^ Suc n

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>(x, z) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n; (z, y) \<in> {(x, y). 0 \<le> y \<and> y < x}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n
(z, y) \<in> {(x, y). 0 \<le> y \<and> y < x}

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
from Suc(1)[OF xz]
[PROOF STATE]
proof (chain)
picking this:
z + int n \<le> x
[PROOF STEP]
have le: "z + int n \<le> x"
[PROOF STATE]
proof (prove)
using this:
z + int n \<le> x

goal (1 subgoal):
 1. z + int n \<le> x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
z + int n \<le> x

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
from zy
[PROOF STATE]
proof (chain)
picking this:
(z, y) \<in> {(x, y). 0 \<le> y \<and> y < x}
[PROOF STEP]
have le2: "y + 1 \<le> z"
[PROOF STATE]
proof (prove)
using this:
(z, y) \<in> {(x, y). 0 \<le> y \<and> y < x}

goal (1 subgoal):
 1. y + 1 \<le> z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y + 1 \<le> z

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ n \<Longrightarrow> y + int n \<le> x; (x, y) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc n\<rbrakk> \<Longrightarrow> y + int (Suc n) \<le> x
[PROOF STEP]
with le
[PROOF STATE]
proof (chain)
picking this:
z + int n \<le> x
y + 1 \<le> z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z + int n \<le> x
y + 1 \<le> z

goal (1 subgoal):
 1. y + int (Suc n) \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + int (Suc n) \<le> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y + int n \<le> x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
0 \<le> y
y + int n \<le> x
[PROOF STEP]
have nx: "int n \<le> x"
[PROOF STATE]
proof (prove)
using this:
0 \<le> y
y + int n \<le> x

goal (1 subgoal):
 1. int n \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
int n \<le> x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
from nx
[PROOF STATE]
proof (chain)
picking this:
int n \<le> x
[PROOF STEP]
have x0: "x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
int n \<le> x

goal (1 subgoal):
 1. 0 \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 \<le> x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). 0 \<le> y \<and> y < x} ^^ Suc (nat x) \<Longrightarrow> False
[PROOF STEP]
with nx n
[PROOF STATE]
proof (chain)
picking this:
int n \<le> x
n = Suc (nat x)
0 \<le> x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
int n \<le> x
n = Suc (nat x)
0 \<le> x

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv_bound {(x, y). 0 \<le> y \<and> y < x} x (nat x)

goal (6 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat b \<le> nat a
 2. \<And>a b. nat (a + b) \<le> nat a + nat b
 3. \<And>a n. 0 \<le> a \<Longrightarrow> nat (a + int n) = nat a + nat (int n)
 4. nat 0 = 0
 5. 1 \<le> nat 1
 6. \<And>x y z. \<lbrakk>int_mono x; z < y; 0 \<le> x\<rbrakk> \<Longrightarrow> x * z < x * y
[PROOF STEP]
qed (insert int_SN.mono, auto)


[STATEMENT]
lemma int_weak_complexity:
  "weak_complexity_linear_poly_order_carrier (>) 1 int_mono"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. weak_complexity_linear_poly_order_carrier (\<lambda>x y. y < x) 1 int_mono
[PROOF STEP]
by (unfold_locales, intro exI[of _ "(>)"] exI[of _ nat] conjI, rule int_complexity, auto)


[STATEMENT]
lemma delta_complexity:
  assumes d0: "d > 0" and d1: "d \<le> def"
  shows "mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
from d0
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < d
[PROOF STEP]
have d00: "0 \<le> d"
[PROOF STATE]
proof (prove)
using this:
(0::'a) < d

goal (1 subgoal):
 1. (0::'a) \<le> d
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> d

goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
define N where "N = ceiling (1 / d)"
[PROOF STATE]
proof (state)
this:
N = \<lceil>(1::'a) / d\<rceil>

goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
let ?N = "of_int N :: 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
from d0
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < d
[PROOF STEP]
have "1 / d > 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) < d

goal (1 subgoal):
 1. (0::'a) < (1::'a) / d
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
(0::'a) < (1::'a) / d

goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
with ceiling_correct[of "1 / d"]
[PROOF STATE]
proof (chain)
picking this:
of_int \<lceil>(1::'a) / d\<rceil> - (1::'a) < (1::'a) / d \<and> (1::'a) / d \<le> of_int \<lceil>(1::'a) / d\<rceil>
(0::'a) < (1::'a) / d
[PROOF STEP]
have Nd: "1 / d \<le> ?N" and N: "N > 0"
[PROOF STATE]
proof (prove)
using this:
of_int \<lceil>(1::'a) / d\<rceil> - (1::'a) < (1::'a) / d \<and> (1::'a) / d \<le> of_int \<lceil>(1::'a) / d\<rceil>
(0::'a) < (1::'a) / d

goal (1 subgoal):
 1. (1::'a) / d \<le> of_int N &&& 0 < N
[PROOF STEP]
unfolding N_def
[PROOF STATE]
proof (prove)
using this:
of_int \<lceil>(1::'a) / d\<rceil> - (1::'a) < (1::'a) / d \<and> (1::'a) / d \<le> of_int \<lceil>(1::'a) / d\<rceil>
(0::'a) < (1::'a) / d

goal (1 subgoal):
 1. (1::'a) / d \<le> of_int \<lceil>(1::'a) / d\<rceil> &&& 0 < \<lceil>(1::'a) / d\<rceil>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(1::'a) / d \<le> of_int N
0 < N

goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
let ?nat = "\<lambda> x. nat (ceiling (x * ?N))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
let ?gt = "delta_gt d"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
have nn: "delta_bound d = ?nat"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. delta_bound d = (\<lambda>x. nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
unfolding fun_eq_iff N_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. delta_bound d x = nat \<lceil>x * of_int \<lceil>(1::'a) / d\<rceil>\<rceil>
[PROOF STEP]
by (simp add: delta_bound_def)
[PROOF STATE]
proof (state)
this:
delta_bound d = (\<lambda>x. nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
from delta_interpretation[OF d0 d1]
[PROOF STATE]
proof (chain)
picking this:
SN_strict_mono_ordered_semiring_1 def (delta_gt d) delta_mono
[PROOF STEP]
interpret SN_strict_mono_ordered_semiring_1 "def" ?gt delta_mono
[PROOF STATE]
proof (prove)
using this:
SN_strict_mono_ordered_semiring_1 def (delta_gt d) delta_mono

goal (1 subgoal):
 1. SN_strict_mono_ordered_semiring_1 def (delta_gt d) delta_mono
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono
[PROOF STEP]
unfolding nn
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono_matrix_carrier (delta_gt d) def (\<lambda>x. nat \<lceil>x * of_int N\<rceil>) delta_mono
[PROOF STEP]
proof(unfold_locales)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat \<lceil>b * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil>
 2. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 3. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 4. nat \<lceil>(0::'a) * of_int N\<rceil> = 0
 5. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 6. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 7. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
show "?nat 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lceil>(0::'a) * of_int N\<rceil> = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat \<lceil>(0::'a) * of_int N\<rceil> = 0

goal (6 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat \<lceil>b * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil>
 2. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 3. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 4. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 5. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 6. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat \<lceil>b * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil>
 2. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 3. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 4. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 5. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 6. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
fix x y :: 'a
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat \<lceil>b * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil>
 2. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 3. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 4. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 5. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 6. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
assume xy: "x \<ge> y"
[PROOF STATE]
proof (state)
this:
y \<le> x

goal (6 subgoals):
 1. \<And>a b. b \<le> a \<Longrightarrow> nat \<lceil>b * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil>
 2. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 3. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 4. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 5. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 6. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
show "?nat x \<ge> ?nat y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lceil>y * of_int N\<rceil> \<le> nat \<lceil>x * of_int N\<rceil>
[PROOF STEP]
by (rule nat_mono, rule ceiling_mono, insert xy N, auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
nat \<lceil>y * of_int N\<rceil> \<le> nat \<lceil>x * of_int N\<rceil>

goal (5 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 4. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 5. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 4. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 5. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "1 \<le> nat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> nat 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> nat 1

goal (5 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 4. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 5. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 \<le> nat 1

goal (5 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 4. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 5. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "... \<le> ?nat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
proof (rule nat_mono)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
have "1 = ceiling (1 :: rat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 = \<lceil>1\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 = \<lceil>1\<rceil>

goal (1 subgoal):
 1. 1 \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 = \<lceil>1\<rceil>

goal (1 subgoal):
 1. 1 \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
have "... \<le> ceiling (1 * ?N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>1\<rceil> \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
0 < N

goal (1 subgoal):
 1. \<lceil>1\<rceil> \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lceil>1\<rceil> \<le> \<lceil>(1::'a) * of_int N\<rceil>

goal (1 subgoal):
 1. 1 \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
show "1 \<le> ceiling (1 * ?N)"
[PROOF STATE]
proof (prove)
using this:
1 \<le> \<lceil>(1::'a) * of_int N\<rceil>

goal (1 subgoal):
 1. 1 \<le> \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 \<le> \<lceil>(1::'a) * of_int N\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nat 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>

goal (5 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
 4. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 5. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
show "1 \<le> ?nat 1"
[PROOF STATE]
proof (prove)
using this:
1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>

goal (1 subgoal):
 1. 1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 \<le> nat \<lceil>(1::'a) * of_int N\<rceil>

goal (4 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 4. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 4. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
fix x y :: 'a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 4. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "ceiling ((x + y) * ?N) = ceiling (x * ?N + y * ?N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>(x + y) * of_int N\<rceil> = \<lceil>x * of_int N + y * of_int N\<rceil>
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
\<lceil>(x + y) * of_int N\<rceil> = \<lceil>x * of_int N + y * of_int N\<rceil>

goal (4 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 4. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lceil>(x + y) * of_int N\<rceil> = \<lceil>x * of_int N + y * of_int N\<rceil>

goal (4 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 4. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "... \<le> ceiling (x * ?N) + ceiling (y * ?N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>x * of_int N + y * of_int N\<rceil> \<le> \<lceil>x * of_int N\<rceil> + \<lceil>y * of_int N\<rceil>
[PROOF STEP]
by (rule ceiling_add_le)
[PROOF STATE]
proof (state)
this:
\<lceil>x * of_int N + y * of_int N\<rceil> \<le> \<lceil>x * of_int N\<rceil> + \<lceil>y * of_int N\<rceil>

goal (4 subgoals):
 1. \<And>a b. nat \<lceil>(a + b) * of_int N\<rceil> \<le> nat \<lceil>a * of_int N\<rceil> + nat \<lceil>b * of_int N\<rceil>
 2. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 3. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 4. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lceil>(x + y) * of_int N\<rceil> \<le> \<lceil>x * of_int N\<rceil> + \<lceil>y * of_int N\<rceil>
[PROOF STEP]
show "?nat (x + y) \<le> ?nat x + ?nat y"
[PROOF STATE]
proof (prove)
using this:
\<lceil>(x + y) * of_int N\<rceil> \<le> \<lceil>x * of_int N\<rceil> + \<lceil>y * of_int N\<rceil>

goal (1 subgoal):
 1. nat \<lceil>(x + y) * of_int N\<rceil> \<le> nat \<lceil>x * of_int N\<rceil> + nat \<lceil>y * of_int N\<rceil>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nat \<lceil>(x + y) * of_int N\<rceil> \<le> nat \<lceil>x * of_int N\<rceil> + nat \<lceil>y * of_int N\<rceil>

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
fix x :: 'a and n :: nat
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
assume x: "0 \<le> x"
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> x

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
interpret mono_matrix_carrier "(>)" 1 nat int_mono
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono_matrix_carrier (\<lambda>x y. y < x) 1 nat int_mono
[PROOF STEP]
by (rule int_complexity)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "?nat (x + of_nat n) = nat (ceiling (x * ?N + of_nat n * ?N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat \<lceil>(x + of_nat n) * of_int N\<rceil> = nat \<lceil>x * of_int N + of_nat n * of_int N\<rceil>
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
nat \<lceil>(x + of_nat n) * of_int N\<rceil> = nat \<lceil>x * of_int N + of_nat n * of_int N\<rceil>

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nat \<lceil>(x + of_nat n) * of_int N\<rceil> = nat \<lceil>x * of_int N + of_nat n * of_int N\<rceil>

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have id: "of_nat n * ?N = of_int (of_nat (n * nat N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n * of_int N = of_int (int (n * nat N))
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
0 < N

goal (1 subgoal):
 1. of_nat n * of_int N = of_int (int (n * nat N))
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
of_nat n * of_int N = of_int (int (n * nat N))

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat n * of_int N = of_int (int (n * nat N))

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "ceiling (x * ?N + of_int (of_nat (n * nat N))) = ceiling (x * ?N) + of_nat (n * nat N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>x * of_int N + of_int (int (n * nat N))\<rceil> = \<lceil>x * of_int N\<rceil> + int (n * nat N)
[PROOF STEP]
unfolding ceiling_add_of_int
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lceil>x * of_int N\<rceil> + int (n * nat N) = \<lceil>x * of_int N\<rceil> + int (n * nat N)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
\<lceil>x * of_int N + of_int (int (n * nat N))\<rceil> = \<lceil>x * of_int N\<rceil> + int (n * nat N)

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<lceil>x * of_int N + of_int (int (n * nat N))\<rceil> = \<lceil>x * of_int N\<rceil> + int (n * nat N)

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "nat (ceiling (x * ?N) + of_nat (n * nat N)) = ?nat x + nat (int (n * nat N))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (\<lceil>x * of_int N\<rceil> + int (n * nat N)) = nat \<lceil>x * of_int N\<rceil> + nat (int (n * nat N))
[PROOF STEP]
proof (rule bound_plus_of_nat)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 \<le> \<lceil>x * of_int N\<rceil>
[PROOF STEP]
have "x * ?N \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> x * of_int N
[PROOF STEP]
by (rule mult_nonneg_nonneg, insert x N, auto)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> x * of_int N

goal (1 subgoal):
 1. 0 \<le> \<lceil>x * of_int N\<rceil>
[PROOF STEP]
thus "ceiling (x * ?N) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> x * of_int N

goal (1 subgoal):
 1. 0 \<le> \<lceil>x * of_int N\<rceil>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> \<lceil>x * of_int N\<rceil>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
nat (\<lceil>x * of_int N\<rceil> + int (n * nat N)) = nat \<lceil>x * of_int N\<rceil> + nat (int (n * nat N))

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nat (\<lceil>x * of_int N\<rceil> + int (n * nat N)) = nat \<lceil>x * of_int N\<rceil> + nat (int (n * nat N))

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "(nat (int (n * nat N))) = n * nat N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nat (int (n * nat N)) = n * nat N
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
nat (int (n * nat N)) = n * nat N

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
nat (int (n * nat N)) = n * nat N

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
have "n * nat N = ?nat (of_nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n * nat N = nat \<lceil>of_nat n * of_int N\<rceil>
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
0 < N

goal (1 subgoal):
 1. n * nat N = nat \<lceil>of_nat n * of_int N\<rceil>
[PROOF STEP]
by (metis id ceiling_of_int nat_int)
[PROOF STATE]
proof (state)
this:
n * nat N = nat \<lceil>of_nat n * of_int N\<rceil>

goal (3 subgoals):
 1. \<And>a n. (0::'a) \<le> a \<Longrightarrow> nat \<lceil>(a + of_nat n) * of_int N\<rceil> = nat \<lceil>a * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
 2. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 3. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
nat \<lceil>(x + of_nat n) * of_int N\<rceil> = nat \<lceil>x * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
[PROOF STEP]
show "?nat (x + of_nat n) = ?nat x + ?nat (of_nat n)"
[PROOF STATE]
proof (prove)
using this:
nat \<lceil>(x + of_nat n) * of_int N\<rceil> = nat \<lceil>x * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>

goal (1 subgoal):
 1. nat \<lceil>(x + of_nat n) * of_int N\<rceil> = nat \<lceil>x * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
nat \<lceil>(x + of_nat n) * of_int N\<rceil> = nat \<lceil>x * of_int N\<rceil> + nat \<lceil>of_nat n * of_int N\<rceil>

goal (2 subgoals):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 2. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 2. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
fix x y z :: 'a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 2. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
assume *: "delta_mono x" "delta_gt d y z" and x: "0 \<le> x"
[PROOF STATE]
proof (state)
this:
delta_mono x
delta_gt d y z
(0::'a) \<le> x

goal (2 subgoals):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
 2. \<And>x y z. \<lbrakk>delta_mono x; delta_gt d y z; (0::'a) \<le> x\<rbrakk> \<Longrightarrow> delta_gt d (x * y) (x * z)
[PROOF STEP]
from mono[OF * x]
[PROOF STATE]
proof (chain)
picking this:
delta_gt d (x * y) (x * z)
[PROOF STEP]
show "delta_gt d (x * y) (x * z)"
[PROOF STATE]
proof (prove)
using this:
delta_gt d (x * y) (x * z)

goal (1 subgoal):
 1. delta_gt d (x * y) (x * z)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
delta_gt d (x * y) (x * z)

goal (1 subgoal):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
[PROOF STEP]
fix x :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
[PROOF STEP]
let ?R = "{(x,y). 0 \<le> y \<and> ?gt x y}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. deriv_bound {(a, b). (0::'a) \<le> b \<and> delta_gt d a b} a (nat \<lceil>a * of_int N\<rceil>)
[PROOF STEP]
show "deriv_bound ?R x (?nat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deriv_bound {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} x (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
unfolding deriv_bound_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
assume "(\<exists> y. (x,y) \<in> ?R ^^ Suc (?nat x))"
[PROOF STATE]
proof (state)
this:
\<exists>y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
obtain y where xy: "(x,y) \<in> ?R ^^ Suc (?nat x)"
[PROOF STATE]
proof (prove)
using this:
\<exists>y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. (\<And>y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
(x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
from xy
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
have y: "0 \<le> y"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. (0::'a) \<le> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> y

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
obtain n where n: "n = Suc (?nat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n = Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n = Suc (nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
from xy[unfolded n[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n
[PROOF STEP]
have "x \<ge> y + d * of_nat n"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n

goal (1 subgoal):
 1. y + d * of_nat n \<le> x
[PROOF STEP]
proof (induct n arbitrary: x y)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ 0 \<Longrightarrow> y + d * of_nat 0 \<le> x
 2. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> (0::'a) \<le> y \<and> delta_gt d x y} ^^ 0

goal (2 subgoals):
 1. \<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ 0 \<Longrightarrow> y + d * of_nat 0 \<le> x
 2. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> (0::'a) \<le> y \<and> delta_gt d x y} ^^ 0

goal (1 subgoal):
 1. y + d * of_nat 0 \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y + d * of_nat 0 \<le> x

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
(?x, ?y) \<in> {a. case a of (x, y) \<Rightarrow> (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> ?y + d * of_nat n \<le> ?x
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
from Suc(2)
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n
[PROOF STEP]
obtain z where xz: "(x,z) \<in> ?R ^^ n" and zy: "(z,y) \<in> ?R"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> {a. case a of (x, y) \<Rightarrow> (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n

goal (1 subgoal):
 1. (\<And>z. \<lbrakk>(x, z) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n; (z, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y}\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, z) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n
(z, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y}

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
from Suc(1)[OF xz]
[PROOF STATE]
proof (chain)
picking this:
z + d * of_nat n \<le> x
[PROOF STEP]
have le: "z + d * of_nat n \<le> x"
[PROOF STATE]
proof (prove)
using this:
z + d * of_nat n \<le> x

goal (1 subgoal):
 1. z + d * of_nat n \<le> x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
z + d * of_nat n \<le> x

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
from zy[unfolded delta_gt_def]
[PROOF STATE]
proof (chain)
picking this:
(z, y) \<in> {(x, y). (0::'a) \<le> y \<and> d \<le> x - y}
[PROOF STEP]
have le2: "y + d \<le> z"
[PROOF STATE]
proof (prove)
using this:
(z, y) \<in> {(x, y). (0::'a) \<le> y \<and> d \<le> x - y}

goal (1 subgoal):
 1. y + d \<le> z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y + d \<le> z

goal (1 subgoal):
 1. \<And>n x y. \<lbrakk>\<And>x y. (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ n \<Longrightarrow> y + d * of_nat n \<le> x; (x, y) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc n\<rbrakk> \<Longrightarrow> y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
with le
[PROOF STATE]
proof (chain)
picking this:
z + d * of_nat n \<le> x
y + d \<le> z
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
z + d * of_nat n \<le> x
y + d \<le> z

goal (1 subgoal):
 1. y + d * of_nat (Suc n) \<le> x
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
y + d * of_nat (Suc n) \<le> x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
y + d * of_nat n \<le> x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
with y
[PROOF STATE]
proof (chain)
picking this:
(0::'a) \<le> y
y + d * of_nat n \<le> x
[PROOF STEP]
have nx: "d * of_nat n \<le> x"
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> y
y + d * of_nat n \<le> x

goal (1 subgoal):
 1. d * of_nat n \<le> x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d * of_nat n \<le> x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
have "0 \<le> d * of_nat n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> d * of_nat n
[PROOF STEP]
by (rule mult_nonneg_nonneg, insert d00, auto)
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> d * of_nat n

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
with nx
[PROOF STATE]
proof (chain)
picking this:
d * of_nat n \<le> x
(0::'a) \<le> d * of_nat n
[PROOF STEP]
have x0: "x \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
d * of_nat n \<le> x
(0::'a) \<le> d * of_nat n

goal (1 subgoal):
 1. (0::'a) \<le> x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
have xd0: "0 \<le> x / d"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (0::'a) \<le> x / d
[PROOF STEP]
by (rule divide_nonneg_pos[OF x0 d0])
[PROOF STATE]
proof (state)
this:
(0::'a) \<le> x / d

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
from nx[unfolded n]
[PROOF STATE]
proof (chain)
picking this:
d * of_nat (Suc (nat \<lceil>x * of_int N\<rceil>)) \<le> x
[PROOF STEP]
have "d + d * of_nat (?nat x) \<le> x"
[PROOF STATE]
proof (prove)
using this:
d * of_nat (Suc (nat \<lceil>x * of_int N\<rceil>)) \<le> x

goal (1 subgoal):
 1. d + d * of_nat (nat \<lceil>x * of_int N\<rceil>) \<le> x
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
d + d * of_nat (nat \<lceil>x * of_int N\<rceil>) \<le> x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
with d0
[PROOF STATE]
proof (chain)
picking this:
(0::'a) < d
d + d * of_nat (nat \<lceil>x * of_int N\<rceil>) \<le> x
[PROOF STEP]
have less: "d * of_nat (?nat x) < x"
[PROOF STATE]
proof (prove)
using this:
(0::'a) < d
d + d * of_nat (nat \<lceil>x * of_int N\<rceil>) \<le> x

goal (1 subgoal):
 1. d * of_nat (nat \<lceil>x * of_int N\<rceil>) < x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
d * of_nat (nat \<lceil>x * of_int N\<rceil>) < x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
from Nd d0
[PROOF STATE]
proof (chain)
picking this:
(1::'a) / d \<le> of_int N
(0::'a) < d
[PROOF STEP]
have "1 \<le> d * ?N"
[PROOF STATE]
proof (prove)
using this:
(1::'a) / d \<le> of_int N
(0::'a) < d

goal (1 subgoal):
 1. (1::'a) \<le> d * of_int N
[PROOF STEP]
by (auto simp: field_simps)
[PROOF STATE]
proof (state)
this:
(1::'a) \<le> d * of_int N

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
from mult_left_mono[OF this x0]
[PROOF STATE]
proof (chain)
picking this:
x * (1::'a) \<le> x * (d * of_int N)
[PROOF STEP]
have "x \<le> d * (x * ?N)"
[PROOF STATE]
proof (prove)
using this:
x * (1::'a) \<le> x * (d * of_int N)

goal (1 subgoal):
 1. x \<le> d * (x * of_int N)
[PROOF STEP]
by (simp add: ac_simps)
[PROOF STATE]
proof (state)
this:
x \<le> d * (x * of_int N)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
x \<le> d * (x * of_int N)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> \<le> d * of_nat (?nat x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d * (x * of_int N) \<le> d * of_nat (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
proof (rule mult_left_mono[OF _ d00])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x * of_int N \<le> of_nat (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
show "x * ?N \<le> of_nat (nat \<lceil>x * ?N\<rceil>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * of_int N \<le> of_nat (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
using x0 ceiling_correct[of "x * ?N"]
[PROOF STATE]
proof (prove)
using this:
(0::'a) \<le> x
of_int \<lceil>x * of_int N\<rceil> - (1::'a) < x * of_int N \<and> x * of_int N \<le> of_int \<lceil>x * of_int N\<rceil>

goal (1 subgoal):
 1. x * of_int N \<le> of_nat (nat \<lceil>x * of_int N\<rceil>)
[PROOF STEP]
by (metis int_nat_eq le_cases of_int_0_le_iff of_int_of_nat_eq order_trans)
[PROOF STATE]
proof (state)
this:
x * of_int N \<le> of_nat (nat \<lceil>x * of_int N\<rceil>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
d * (x * of_int N) \<le> d * of_nat (nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
d * (x * of_int N) \<le> d * of_nat (nat \<lceil>x * of_int N\<rceil>)

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
have "\<dots> < x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d * of_nat (nat \<lceil>x * of_int N\<rceil>) < x
[PROOF STEP]
using less
[PROOF STATE]
proof (prove)
using this:
d * of_nat (nat \<lceil>x * of_int N\<rceil>) < x

goal (1 subgoal):
 1. d * of_nat (nat \<lceil>x * of_int N\<rceil>) < x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
d * of_nat (nat \<lceil>x * of_int N\<rceil>) < x

goal (1 subgoal):
 1. \<exists>b. (x, b) \<in> {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} ^^ Suc (nat \<lceil>x * of_int N\<rceil>) \<Longrightarrow> False
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
x < x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
x < x

goal (1 subgoal):
 1. False
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
deriv_bound {(x, y). (0::'a) \<le> y \<and> delta_gt d x y} x (nat \<lceil>x * of_int N\<rceil>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mono_matrix_carrier (delta_gt d) def (delta_bound d) delta_mono

goal:
No subgoals!
[PROOF STEP]
qed