[STATEMENT]
lemma Hermite_unique_generalized:
  fixes K::"int^'n::mod_type^'n::mod_type"
  assumes A_PH: "A = P ** H"
  and A_QK: "A = Q ** K"
  and inv_A: "invertible (map_matrix rat_of_int A)" (*The original statement assumes "invertible A",
                                                      that is, invertibility over integers, which is
                                                      more restrictive.*)
  and inv_P: "invertible P"
  and inv_Q: "invertible Q"
  and H: "Hermite associates residues H"
  and K: "Hermite associates residues K"
  shows "H = K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = K
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H = K
[PROOF STEP]
let ?RAT = "map_matrix rat_of_int"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. H = K
[PROOF STEP]
have cs_residues: "Complete_set_residues residues"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Complete_set_residues residues
[PROOF STEP]
using H
[PROOF STATE]
proof (prove)
using this:
Hermite associates residues H

goal (1 subgoal):
 1. Complete_set_residues residues
[PROOF STEP]
unfolding Hermite_def
[PROOF STATE]
proof (prove)
using this:
Complete_set_non_associates associates \<and> Complete_set_residues residues \<and> echelon_form H \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> H $ i $ (LEAST n. H $ i $ n \<noteq> 0) \<in> associates) \<and> (\<forall>i. \<not> is_zero_row i H \<longrightarrow> (\<forall>j<i. H $ j $ (LEAST n. H $ i $ n \<noteq> 0) \<in> residues (H $ i $ (LEAST n. H $ i $ n \<noteq> 0))))

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

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have inv_H: "invertible (?RAT H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (map_matrix rat_of_int H)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible (map_matrix rat_of_int H)
[PROOF STEP]
have "?RAT A = ?RAT P ** ?RAT H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_matrix rat_of_int A = map_matrix rat_of_int P ** map_matrix rat_of_int H
[PROOF STEP]
using A_PH map_matrix_rat_of_int_mult
[PROOF STATE]
proof (prove)
using this:
A = P ** H
map_matrix rat_of_int (?A ** ?B) = map_matrix rat_of_int ?A ** map_matrix rat_of_int ?B

goal (1 subgoal):
 1. map_matrix rat_of_int A = map_matrix rat_of_int P ** map_matrix rat_of_int H
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map_matrix rat_of_int A = map_matrix rat_of_int P ** map_matrix rat_of_int H

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int H)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
map_matrix rat_of_int A = map_matrix rat_of_int P ** map_matrix rat_of_int H

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int H)
[PROOF STEP]
by (metis inv_A invertible_left_inverse matrix_inv(1) matrix_mul_assoc)
[PROOF STATE]
proof (state)
this:
invertible (map_matrix rat_of_int H)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invertible (map_matrix rat_of_int H)

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have inv_K: "invertible (?RAT K)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (map_matrix rat_of_int K)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. invertible (map_matrix rat_of_int K)
[PROOF STEP]
have "?RAT A = ?RAT Q ** ?RAT K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_matrix rat_of_int A = map_matrix rat_of_int Q ** map_matrix rat_of_int K
[PROOF STEP]
using A_QK map_matrix_rat_of_int_mult
[PROOF STATE]
proof (prove)
using this:
A = Q ** K
map_matrix rat_of_int (?A ** ?B) = map_matrix rat_of_int ?A ** map_matrix rat_of_int ?B

goal (1 subgoal):
 1. map_matrix rat_of_int A = map_matrix rat_of_int Q ** map_matrix rat_of_int K
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map_matrix rat_of_int A = map_matrix rat_of_int Q ** map_matrix rat_of_int K

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int K)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
map_matrix rat_of_int A = map_matrix rat_of_int Q ** map_matrix rat_of_int K

goal (1 subgoal):
 1. invertible (map_matrix rat_of_int K)
[PROOF STEP]
by (metis inv_A invertible_left_inverse matrix_inv(1) matrix_mul_assoc)
[PROOF STATE]
proof (state)
this:
invertible (map_matrix rat_of_int K)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
invertible (map_matrix rat_of_int K)

goal (1 subgoal):
 1. H = K
[PROOF STEP]
define U where "U = (matrix_inv P)**Q"
[PROOF STATE]
proof (state)
this:
U = matrix_inv P ** Q

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have inv_U: "invertible U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible U
[PROOF STEP]
by (metis U_def inv_P inv_Q invertible_def invertible_mult matrix_inv_left matrix_inv_right)
[PROOF STATE]
proof (state)
this:
invertible U

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have H_UK: "H = U ** K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H = U ** K
[PROOF STEP]
using A_PH A_QK inv_P
[PROOF STATE]
proof (prove)
using this:
A = P ** H
A = Q ** K
invertible P

goal (1 subgoal):
 1. H = U ** K
[PROOF STEP]
by (metis U_def matrix_inv_left matrix_mul_assoc matrix_mul_lid)
[PROOF STATE]
proof (state)
this:
H = U ** K

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have "Determinants.det K *k U = H ** adjugate K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det K *k U = H ** adjugate K
[PROOF STEP]
unfolding H_UK matrix_mul_assoc[symmetric] mult_adjugate_det matrix_mul_mat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det K *k U = det K *k U
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
det K *k U = H ** adjugate K

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have upper_triangular_H: "upper_triangular H"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular H
[PROOF STEP]
by (metis H Hermite_def echelon_form_imp_upper_triagular)
[PROOF STATE]
proof (state)
this:
upper_triangular H

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have upper_triangular_K: "upper_triangular K"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular K
[PROOF STEP]
by (metis K Hermite_def echelon_form_imp_upper_triagular)
[PROOF STATE]
proof (state)
this:
upper_triangular K

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have upper_triangular_U: "upper_triangular U"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular U
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. upper_triangular U
[PROOF STEP]
have U_H_K: "?RAT U = (?RAT H) ** (matrix_inv (?RAT K))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_matrix rat_of_int U = map_matrix rat_of_int H ** matrix_inv (map_matrix rat_of_int K)
[PROOF STEP]
by (metis H_UK inv_K map_matrix_rat_of_int_mult matrix_inv(2) matrix_mul_assoc matrix_mul_rid)
[PROOF STATE]
proof (state)
this:
map_matrix rat_of_int U = map_matrix rat_of_int H ** matrix_inv (map_matrix rat_of_int K)

goal (1 subgoal):
 1. upper_triangular U
[PROOF STEP]
have up_inv_RAT_K: "upper_triangular (matrix_inv (?RAT K))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular (matrix_inv (map_matrix rat_of_int K))
[PROOF STEP]
using upper_triangular_inverse
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>upper_triangular ?A; invertible ?A\<rbrakk> \<Longrightarrow> upper_triangular (matrix_inv ?A)

goal (1 subgoal):
 1. upper_triangular (matrix_inv (map_matrix rat_of_int K))
[PROOF STEP]
by (simp add: upper_triangular_inverse inv_K upper_triangular_K upper_triangular_Z_eq_Q)
[PROOF STATE]
proof (state)
this:
upper_triangular (matrix_inv (map_matrix rat_of_int K))

goal (1 subgoal):
 1. upper_triangular U
[PROOF STEP]
have "upper_triangular (?RAT U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular (map_matrix rat_of_int U)
[PROOF STEP]
unfolding U_H_K
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. upper_triangular (map_matrix rat_of_int H ** matrix_inv (map_matrix rat_of_int K))
[PROOF STEP]
by (rule upper_triangular_mult[OF _ up_inv_RAT_K],
          auto simp add: upper_triangular_H upper_triangular_Z_eq_Q)
[PROOF STATE]
proof (state)
this:
upper_triangular (map_matrix rat_of_int U)

goal (1 subgoal):
 1. upper_triangular U
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
upper_triangular (map_matrix rat_of_int U)

goal (1 subgoal):
 1. upper_triangular U
[PROOF STEP]
using upper_triangular_Z_eq_Q
[PROOF STATE]
proof (prove)
using this:
upper_triangular (map_matrix rat_of_int U)
upper_triangular (map_matrix rat_of_int ?A) = upper_triangular ?A

goal (1 subgoal):
 1. upper_triangular U
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
upper_triangular U

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
upper_triangular U

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have unit_det_U: "is_unit (det U)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_unit (det U)
[PROOF STEP]
by (metis inv_U invertible_iff_is_unit)
[PROOF STATE]
proof (state)
this:
is_unit (det U)

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have is_unit_diagonal_U: "(\<forall>i. is_unit (U $ i $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. is_unit (U $ i $ i)
[PROOF STEP]
by (rule is_unit_diagonal[OF upper_triangular_U unit_det_U])
[PROOF STATE]
proof (state)
this:
\<forall>i. is_unit (U $ i $ i)

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have Uii_1: "(\<forall>i. (U $ i $ i) = 1)" and Hii_Kii: "(\<forall>i. (H $ i $ i) = (K $ i $ i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i. U $ i $ i = 1 &&& \<forall>i. H $ i $ i = K $ i $ i
[PROOF STEP]
proof (auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. U $ i $ i = 1
 2. \<And>i. H $ i $ i = K $ i $ i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>i. U $ i $ i = 1
 2. \<And>i. H $ i $ i = K $ i $ i
[PROOF STEP]
have Hii: "H $ i $ i \<in> associates"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i \<in> associates
[PROOF STEP]
by (rule diagonal_in_associates[OF H inv_H upper_triangular_H])
[PROOF STATE]
proof (state)
this:
H $ i $ i \<in> associates

goal (2 subgoals):
 1. \<And>i. U $ i $ i = 1
 2. \<And>i. H $ i $ i = K $ i $ i
[PROOF STEP]
have Kii: "K $ i $ i \<in> associates"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K $ i $ i \<in> associates
[PROOF STEP]
by (rule diagonal_in_associates[OF K inv_K upper_triangular_K])
[PROOF STATE]
proof (state)
this:
K $ i $ i \<in> associates

goal (2 subgoals):
 1. \<And>i. U $ i $ i = 1
 2. \<And>i. H $ i $ i = K $ i $ i
[PROOF STEP]
have ass_Hii_Kii: "normalize (H $ i $ i) = normalize (K $ i $ i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. normalize (H $ i $ i) = normalize (K $ i $ i)
[PROOF STEP]
by (metis H_UK is_unit_diagonal_U normalize_mult_unit_left upper_triangular_K upper_triangular_U upper_triangular_mult_diagonal)
[PROOF STATE]
proof (state)
this:
normalize (H $ i $ i) = normalize (K $ i $ i)

goal (2 subgoals):
 1. \<And>i. U $ i $ i = 1
 2. \<And>i. H $ i $ i = K $ i $ i
[PROOF STEP]
show Hii_eq_Kii: "H $ i $ i = K $ i $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i = K $ i $ i
[PROOF STEP]
by (metis Hermite_def Hii K Kii ass_Hii_Kii in_Ass_not_associated)
[PROOF STATE]
proof (state)
this:
H $ i $ i = K $ i $ i

goal (1 subgoal):
 1. \<And>i. U $ i $ i = 1
[PROOF STEP]
have "H $ i $ i = U $ i $ i * K $ i $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ i $ i = U $ i $ i * K $ i $ i
[PROOF STEP]
by (metis H_UK upper_triangular_K upper_triangular_U upper_triangular_mult_diagonal)
[PROOF STATE]
proof (state)
this:
H $ i $ i = U $ i $ i * K $ i $ i

goal (1 subgoal):
 1. \<And>i. U $ i $ i = 1
[PROOF STEP]
thus "U $ i $ i = 1"
[PROOF STATE]
proof (prove)
using this:
H $ i $ i = U $ i $ i * K $ i $ i

goal (1 subgoal):
 1. U $ i $ i = 1
[PROOF STEP]
unfolding Hii_eq_Kii mult_cancel_right1
[PROOF STATE]
proof (prove)
using this:
K $ i $ i = 0 \<or> U $ i $ i = 1

goal (1 subgoal):
 1. U $ i $ i = 1
[PROOF STEP]
using inv_K invertible_and_upper_diagonal_not0 upper_triangular_K
[PROOF STATE]
proof (prove)
using this:
K $ i $ i = 0 \<or> U $ i $ i = 1
invertible (map_matrix rat_of_int K)
\<lbrakk>invertible (map_matrix rat_of_int ?H); upper_triangular ?H\<rbrakk> \<Longrightarrow> ?H $ ?i $ ?i \<noteq> 0
upper_triangular K

goal (1 subgoal):
 1. U $ i $ i = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
U $ i $ i = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i. U $ i $ i = 1
\<forall>i. H $ i $ i = K $ i $ i

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have zero_above: "\<forall>j s. j\<ge>1 \<and> j < ncols A - to_nat s \<longrightarrow> U $ s $ (s + from_nat j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>j s. 1 \<le> j \<and> j < ncols A - mod_type_class.to_nat s \<longrightarrow> U $ s $ (s + mod_type_class.from_nat j) = 0
[PROOF STEP]
proof (clarify)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j s. \<lbrakk>1 \<le> j; j < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat j) = 0
[PROOF STEP]
fix j s
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>j s. \<lbrakk>1 \<le> j; j < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat j) = 0
[PROOF STEP]
assume  "1 \<le> j" and "j < ncols A - (to_nat (s::'n))"
[PROOF STATE]
proof (state)
this:
1 \<le> j
j < ncols A - mod_type_class.to_nat s

goal (1 subgoal):
 1. \<And>j s. \<lbrakk>1 \<le> j; j < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat j) = 0
[PROOF STEP]
thus "U $ s $ (s + from_nat j) = 0"
[PROOF STATE]
proof (prove)
using this:
1 \<le> j
j < ncols A - mod_type_class.to_nat s

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat j) = 0
[PROOF STEP]
proof (induct j rule: less_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; 1 \<le> y; y < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat y) = 0; 1 \<le> x; x < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat x) = 0
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; 1 \<le> y; y < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat y) = 0; 1 \<le> x; x < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat x) = 0
[PROOF STEP]
assume induct_step: "(\<And>y. y < p \<Longrightarrow> 1 \<le> y \<Longrightarrow> y < ncols A - to_nat s \<Longrightarrow> U $ s $ (s + from_nat y) = 0)"
        and p1: "1 \<le> p" and p2: "p < ncols A - to_nat s"
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y1 < p; 1 \<le> ?y1; ?y1 < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat ?y1) = 0
1 \<le> p
p < ncols A - mod_type_class.to_nat s

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; 1 \<le> y; y < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat y) = 0; 1 \<le> x; x < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat x) = 0
[PROOF STEP]
have s_less: "s < s + from_nat p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s < s + mod_type_class.from_nat p
[PROOF STEP]
using p1 p2
[PROOF STATE]
proof (prove)
using this:
1 \<le> p
p < ncols A - mod_type_class.to_nat s

goal (1 subgoal):
 1. s < s + mod_type_class.from_nat p
[PROOF STEP]
unfolding ncols_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> p
p < CARD('n) - mod_type_class.to_nat s

goal (1 subgoal):
 1. s < s + mod_type_class.from_nat p
[PROOF STEP]
by (metis One_nat_def add.commute add_diff_cancel_right' add_lessD1 add_to_nat_def
          from_nat_to_nat_id less_diff_conv neq_iff not_le
          to_nat_from_nat_id to_nat_le zero_less_Suc)
[PROOF STATE]
proof (state)
this:
s < s + mod_type_class.from_nat p

goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<And>y. \<lbrakk>y < x; 1 \<le> y; y < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat y) = 0; 1 \<le> x; x < ncols A - mod_type_class.to_nat s\<rbrakk> \<Longrightarrow> U $ s $ (s + mod_type_class.from_nat x) = 0
[PROOF STEP]
show "U $ s $ (s + from_nat p) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have UNIV_rw: "UNIV = insert s (UNIV-{s})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = insert s (UNIV - {s})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
UNIV = insert s (UNIV - {s})

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have UNIV_s_rw: "UNIV-{s} = insert (s + from_nat p) ((UNIV-{s}) - {s + from_nat p})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV - {s} = insert (s + mod_type_class.from_nat p) (UNIV - {s} - {s + mod_type_class.from_nat p})
[PROOF STEP]
using p1 p2 s_less
[PROOF STATE]
proof (prove)
using this:
1 \<le> p
p < ncols A - mod_type_class.to_nat s
s < s + mod_type_class.from_nat p

goal (1 subgoal):
 1. UNIV - {s} = insert (s + mod_type_class.from_nat p) (UNIV - {s} - {s + mod_type_class.from_nat p})
[PROOF STEP]
unfolding ncols_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> p
p < CARD('n) - mod_type_class.to_nat s
s < s + mod_type_class.from_nat p

goal (1 subgoal):
 1. UNIV - {s} = insert (s + mod_type_class.from_nat p) (UNIV - {s} - {s + mod_type_class.from_nat p})
[PROOF STEP]
by (auto simp: algebra_simps)
[PROOF STATE]
proof (state)
this:
UNIV - {s} = insert (s + mod_type_class.from_nat p) (UNIV - {s} - {s + mod_type_class.from_nat p})

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have sum_rw: "(\<Sum>k\<in>UNIV-{s}. U $ s $ k * K $ k $ (s + from_nat p))
          = U $ s $ (s + from_nat p) * K $ (s + from_nat p) $ (s + from_nat p)
          + (\<Sum>k\<in>(UNIV-{s})-{s + from_nat p}. U $ s $ k * K $ k $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s} - {s + mod_type_class.from_nat p}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))
[PROOF STEP]
using UNIV_s_rw sum.insert
[PROOF STATE]
proof (prove)
using this:
UNIV - {s} = insert (s + mod_type_class.from_nat p) (UNIV - {s} - {s + mod_type_class.from_nat p})
\<lbrakk>finite ?A; ?x \<notin> ?A\<rbrakk> \<Longrightarrow> sum ?g (insert ?x ?A) = ?g ?x + sum ?g ?A

goal (1 subgoal):
 1. (\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s} - {s + mod_type_class.from_nat p}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))
[PROOF STEP]
by (metis (erased, lifting) Diff_iff finite singletonI)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s} - {s + mod_type_class.from_nat p}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have sum_0: "(\<Sum>k\<in>(UNIV-{s})-{s + from_nat p}. U $ s $ k * K $ k $ (s + from_nat p)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>UNIV - {s} - {s + mod_type_class.from_nat p}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = 0
[PROOF STEP]
proof (rule sum.neutral, rule)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV - {s} - {s + mod_type_class.from_nat p} \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> UNIV - {s} - {s + mod_type_class.from_nat p} \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
assume x: "x \<in> UNIV - {s} - {s + from_nat p}"
[PROOF STATE]
proof (state)
this:
x \<in> UNIV - {s} - {s + mod_type_class.from_nat p}

goal (1 subgoal):
 1. \<And>x. x \<in> UNIV - {s} - {s + mod_type_class.from_nat p} \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
show "U $ s $ x * K $ x $ (s + from_nat p) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
proof (cases "x<s")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < s

goal (2 subgoals):
 1. x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x < s

goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
using upper_triangular_U
[PROOF STATE]
proof (prove)
using this:
x < s
upper_triangular U

goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
using this:
x < s
\<forall>i j. j < i \<longrightarrow> U $ i $ j = 0

goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0

goal (1 subgoal):
 1. \<not> x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < s

goal (1 subgoal):
 1. \<not> x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
hence x_g_s: "x>s"
[PROOF STATE]
proof (prove)
using this:
\<not> x < s

goal (1 subgoal):
 1. s < x
[PROOF STEP]
using x
[PROOF STATE]
proof (prove)
using this:
\<not> x < s
x \<in> UNIV - {s} - {s + mod_type_class.from_nat p}

goal (1 subgoal):
 1. s < x
[PROOF STEP]
by (metis Diff_iff neq_iff singletonI)
[PROOF STATE]
proof (state)
this:
s < x

goal (1 subgoal):
 1. \<not> x < s \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
proof (cases "x<s+from_nat p")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x < s + mod_type_class.from_nat p

goal (2 subgoals):
 1. x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
define a where "a = to_nat x - to_nat s"
[PROOF STATE]
proof (state)
this:
a = mod_type_class.to_nat x - mod_type_class.to_nat s

goal (2 subgoals):
 1. x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
from x_g_s
[PROOF STATE]
proof (chain)
picking this:
s < x
[PROOF STEP]
have "to_nat s < to_nat x"
[PROOF STATE]
proof (prove)
using this:
s < x

goal (1 subgoal):
 1. mod_type_class.to_nat s < mod_type_class.to_nat x
[PROOF STEP]
by (rule to_nat_mono)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat s < mod_type_class.to_nat x

goal (2 subgoals):
 1. x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
hence xa: "x=s+(from_nat a)"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat s < mod_type_class.to_nat x

goal (1 subgoal):
 1. x = s + mod_type_class.from_nat a
[PROOF STEP]
unfolding a_def add_to_nat_def
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat s < mod_type_class.to_nat x

goal (1 subgoal):
 1. x = mod_type_class.from_nat (mod_type_class.to_nat s + mod_type_class.to_nat (mod_type_class.from_nat (mod_type_class.to_nat x - mod_type_class.to_nat s)))
[PROOF STEP]
by (simp add: less_imp_diff_less to_nat_less_card algebra_simps to_nat_from_nat_id)
[PROOF STATE]
proof (state)
this:
x = s + mod_type_class.from_nat a

goal (2 subgoals):
 1. x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have "U $ s $ x =0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ s $ x = 0
[PROOF STEP]
proof (unfold xa, rule induct_step)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. a < p
 2. 1 \<le> a
 3. a < ncols A - mod_type_class.to_nat s
[PROOF STEP]
show a_p: "a<p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < p
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat x - mod_type_class.to_nat s < p
[PROOF STEP]
using p2
[PROOF STATE]
proof (prove)
using this:
p < ncols A - mod_type_class.to_nat s

goal (1 subgoal):
 1. mod_type_class.to_nat x - mod_type_class.to_nat s < p
[PROOF STEP]
unfolding ncols_def
[PROOF STATE]
proof (prove)
using this:
p < CARD('n) - mod_type_class.to_nat s

goal (1 subgoal):
 1. mod_type_class.to_nat x - mod_type_class.to_nat s < p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p < CARD('n) - mod_type_class.to_nat s \<Longrightarrow> mod_type_class.to_nat x - mod_type_class.to_nat s < p
[PROOF STEP]
have "x < from_nat (to_nat s + to_nat (from_nat p::'n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x < mod_type_class.from_nat (mod_type_class.to_nat s + mod_type_class.to_nat (mod_type_class.from_nat p))
[PROOF STEP]
by (metis (no_types) True add_to_nat_def)
[PROOF STATE]
proof (state)
this:
x < mod_type_class.from_nat (mod_type_class.to_nat s + mod_type_class.to_nat (mod_type_class.from_nat p))

goal (1 subgoal):
 1. p < CARD('n) - mod_type_class.to_nat s \<Longrightarrow> mod_type_class.to_nat x - mod_type_class.to_nat s < p
[PROOF STEP]
hence "to_nat x - to_nat s < to_nat (from_nat p::'n)"
[PROOF STATE]
proof (prove)
using this:
x < mod_type_class.from_nat (mod_type_class.to_nat s + mod_type_class.to_nat (mod_type_class.from_nat p))

goal (1 subgoal):
 1. mod_type_class.to_nat x - mod_type_class.to_nat s < mod_type_class.to_nat (mod_type_class.from_nat p)
[PROOF STEP]
by (simp add: add.commute less_diff_conv2 less_imp_le to_nat_le x_g_s)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat x - mod_type_class.to_nat s < mod_type_class.to_nat (mod_type_class.from_nat p)

goal (1 subgoal):
 1. p < CARD('n) - mod_type_class.to_nat s \<Longrightarrow> mod_type_class.to_nat x - mod_type_class.to_nat s < p
[PROOF STEP]
thus "to_nat x - to_nat s < p"
[PROOF STATE]
proof (prove)
using this:
mod_type_class.to_nat x - mod_type_class.to_nat s < mod_type_class.to_nat (mod_type_class.from_nat p)

goal (1 subgoal):
 1. mod_type_class.to_nat x - mod_type_class.to_nat s < p
[PROOF STEP]
by (metis (no_types) from_nat_eq_imp_eq from_nat_to_nat_id le_less_trans
                        less_imp_le not_le to_nat_less_card)
[PROOF STATE]
proof (state)
this:
mod_type_class.to_nat x - mod_type_class.to_nat s < p

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a < p

goal (2 subgoals):
 1. 1 \<le> a
 2. a < ncols A - mod_type_class.to_nat s
[PROOF STEP]
show "1 \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> a
[PROOF STEP]
by (auto simp add: a_def p1 p2) (metis Suc_leI to_nat_mono x_g_s zero_less_diff)
[PROOF STATE]
proof (state)
this:
1 \<le> a

goal (1 subgoal):
 1. a < ncols A - mod_type_class.to_nat s
[PROOF STEP]
show "a < ncols A - to_nat s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < ncols A - mod_type_class.to_nat s
[PROOF STEP]
using a_p p2
[PROOF STATE]
proof (prove)
using this:
a < p
p < ncols A - mod_type_class.to_nat s

goal (1 subgoal):
 1. a < ncols A - mod_type_class.to_nat s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
a < ncols A - mod_type_class.to_nat s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U $ s $ x = 0

goal (2 subgoals):
 1. x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
 2. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
U $ s $ x = 0

goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0

goal (1 subgoal):
 1. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> x < s + mod_type_class.from_nat p

goal (1 subgoal):
 1. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
hence "x>s+from_nat p"
[PROOF STATE]
proof (prove)
using this:
\<not> x < s + mod_type_class.from_nat p

goal (1 subgoal):
 1. s + mod_type_class.from_nat p < x
[PROOF STEP]
using x_g_s x
[PROOF STATE]
proof (prove)
using this:
\<not> x < s + mod_type_class.from_nat p
s < x
x \<in> UNIV - {s} - {s + mod_type_class.from_nat p}

goal (1 subgoal):
 1. s + mod_type_class.from_nat p < x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s + mod_type_class.from_nat p < x

goal (1 subgoal):
 1. \<not> x < s + mod_type_class.from_nat p \<Longrightarrow> U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
s + mod_type_class.from_nat p < x

goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
using upper_triangular_K
[PROOF STATE]
proof (prove)
using this:
s + mod_type_class.from_nat p < x
upper_triangular K

goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
using this:
s + mod_type_class.from_nat p < x
\<forall>i j. j < i \<longrightarrow> K $ i $ j = 0

goal (1 subgoal):
 1. U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U $ s $ x * K $ x $ (s + mod_type_class.from_nat p) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>UNIV - {s} - {s + mod_type_class.from_nat p}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = 0

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have "H $ s $ (s + from_nat p) = (\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) = (\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))
[PROOF STEP]
unfolding H_UK matrix_matrix_mult_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<chi>i j. \<Sum>k\<in>UNIV. U $ i $ k * K $ k $ j) $ s $ (s + mod_type_class.from_nat p) = (\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H $ s $ (s + mod_type_class.from_nat p) = (\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
H $ s $ (s + mod_type_class.from_nat p) = (\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have "... = (\<Sum>k\<in>insert s (UNIV-{s}). U $ s $ k * K $ k $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = (\<Sum>k\<in>insert s (UNIV - {s}). U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))
[PROOF STEP]
using UNIV_rw
[PROOF STATE]
proof (prove)
using this:
UNIV = insert s (UNIV - {s})

goal (1 subgoal):
 1. (\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = (\<Sum>k\<in>insert s (UNIV - {s}). U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = (\<Sum>k\<in>insert s (UNIV - {s}). U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>UNIV. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = (\<Sum>k\<in>insert s (UNIV - {s}). U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have "... = U $ s $ s * K $ s $ (s + from_nat p)
          + (\<Sum>k\<in>UNIV-{s}. U $ s $ k * K $ k $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>k\<in>insert s (UNIV - {s}). U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))
[PROOF STEP]
by (rule sum.insert, simp_all)
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>insert s (UNIV - {s}). U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>k\<in>insert s (UNIV - {s}). U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have "... = U $ s $ s * K $ s $ (s + from_nat p)
          + U $ s $ (s + from_nat p) * K $ (s + from_nat p) $ (s + from_nat p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p)
[PROOF STEP]
unfolding sum_rw sum_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + (U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + 0) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + (\<Sum>k\<in>UNIV - {s}. U $ s $ k * K $ k $ (s + mod_type_class.from_nat p)) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
H $ s $ (s + mod_type_class.from_nat p) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p)
[PROOF STEP]
have H_s_sp: "H $ s $ (s + from_nat p)
          = U $ s $ (s + from_nat p) * K $ (s + from_nat p) $ (s + from_nat p) + K $ s $ (s + from_nat p)"
[PROOF STATE]
proof (prove)
using this:
H $ s $ (s + mod_type_class.from_nat p) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + K $ s $ (s + mod_type_class.from_nat p)
[PROOF STEP]
using Uii_1
[PROOF STATE]
proof (prove)
using this:
H $ s $ (s + mod_type_class.from_nat p) = U $ s $ s * K $ s $ (s + mod_type_class.from_nat p) + U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p)
\<forall>i. U $ i $ i = 1

goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + K $ s $ (s + mod_type_class.from_nat p)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
H $ s $ (s + mod_type_class.from_nat p) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + K $ s $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
hence cong_HK: "cong (H $ s $ (s + from_nat p)) (K $ s $ (s + from_nat p)) (K $ (s+from_nat p) $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
using this:
H $ s $ (s + mod_type_class.from_nat p) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + K $ s $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. cong (H $ s $ (s + mod_type_class.from_nat p)) (K $ s $ (s + mod_type_class.from_nat p)) (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
[PROOF STEP]
unfolding cong_def
[PROOF STATE]
proof (prove)
using this:
H $ s $ (s + mod_type_class.from_nat p) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + K $ s $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. \<exists>k. H $ s $ (s + mod_type_class.from_nat p) - K $ s $ (s + mod_type_class.from_nat p) = K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) * k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cong (H $ s $ (s + mod_type_class.from_nat p)) (K $ s $ (s + mod_type_class.from_nat p)) (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have H_s_sp_residues: "(H $ s $ (s + from_nat p)) \<in> residues (K $ (s+from_nat p) $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
[PROOF STEP]
using above_diagonal_in_residues[OF H inv_H upper_triangular_H s_less]
[PROOF STATE]
proof (prove)
using this:
H $ s $ (LEAST n. H $ (s + mod_type_class.from_nat p) $ n \<noteq> 0) \<in> residues (H $ (s + mod_type_class.from_nat p) $ (LEAST n. H $ (s + mod_type_class.from_nat p) $ n \<noteq> 0))

goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
[PROOF STEP]
unfolding diagonal_least_nonzero[OF H inv_H upper_triangular_H]
[PROOF STATE]
proof (prove)
using this:
H $ s $ (s + mod_type_class.from_nat p) \<in> residues (H $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
[PROOF STEP]
by (metis Hii_Kii)
[PROOF STATE]
proof (state)
this:
H $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have K_s_sp_residues: "(K $ s $ (s + from_nat p)) \<in> residues (K $ (s+from_nat p) $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
[PROOF STEP]
using above_diagonal_in_residues[OF K inv_K upper_triangular_K s_less]
[PROOF STATE]
proof (prove)
using this:
K $ s $ (LEAST n. K $ (s + mod_type_class.from_nat p) $ n \<noteq> 0) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (LEAST n. K $ (s + mod_type_class.from_nat p) $ n \<noteq> 0))

goal (1 subgoal):
 1. K $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
[PROOF STEP]
unfolding diagonal_least_nonzero[OF K inv_K upper_triangular_K]
[PROOF STATE]
proof (prove)
using this:
K $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. K $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
K $ s $ (s + mod_type_class.from_nat p) \<in> residues (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have Hs_sp_Ks_sp: "(H $ s $ (s + from_nat p)) = (K $ s $ (s + from_nat p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) = K $ s $ (s + mod_type_class.from_nat p)
[PROOF STEP]
using cong_HK in_Res_not_congruent[OF cs_residues H_s_sp_residues K_s_sp_residues]
[PROOF STATE]
proof (prove)
using this:
cong (H $ s $ (s + mod_type_class.from_nat p)) (K $ s $ (s + mod_type_class.from_nat p)) (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))
H $ s $ (s + mod_type_class.from_nat p) \<noteq> K $ s $ (s + mod_type_class.from_nat p) \<Longrightarrow> \<not> cong (H $ s $ (s + mod_type_class.from_nat p)) (K $ s $ (s + mod_type_class.from_nat p)) (K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p))

goal (1 subgoal):
 1. H $ s $ (s + mod_type_class.from_nat p) = K $ s $ (s + mod_type_class.from_nat p)
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
H $ s $ (s + mod_type_class.from_nat p) = K $ s $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
have "K $ (s + from_nat p) $ (s + from_nat p) \<noteq> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) \<noteq> 0
[PROOF STEP]
using inv_K invertible_and_upper_diagonal_not0 upper_triangular_K
[PROOF STATE]
proof (prove)
using this:
invertible (map_matrix rat_of_int K)
\<lbrakk>invertible (map_matrix rat_of_int ?H); upper_triangular ?H\<rbrakk> \<Longrightarrow> ?H $ ?i $ ?i \<noteq> 0
upper_triangular K

goal (1 subgoal):
 1. K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) \<noteq> 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) \<noteq> 0

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) \<noteq> 0

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
unfolding from_nat_1
[PROOF STATE]
proof (prove)
using this:
K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) \<noteq> 0

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
using H_s_sp
[PROOF STATE]
proof (prove)
using this:
K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) \<noteq> 0
H $ s $ (s + mod_type_class.from_nat p) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + K $ s $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
unfolding Hs_sp_Ks_sp
[PROOF STATE]
proof (prove)
using this:
K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) \<noteq> 0
K $ s $ (s + mod_type_class.from_nat p) = U $ s $ (s + mod_type_class.from_nat p) * K $ (s + mod_type_class.from_nat p) $ (s + mod_type_class.from_nat p) + K $ s $ (s + mod_type_class.from_nat p)

goal (1 subgoal):
 1. U $ s $ (s + mod_type_class.from_nat p) = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U $ s $ (s + mod_type_class.from_nat p) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U $ s $ (s + mod_type_class.from_nat p) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U $ s $ (s + mod_type_class.from_nat j) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>j s. 1 \<le> j \<and> j < ncols A - mod_type_class.to_nat s \<longrightarrow> U $ s $ (s + mod_type_class.from_nat j) = 0

goal (1 subgoal):
 1. H = K
[PROOF STEP]
have "U = mat 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U = mat 1
[PROOF STEP]
proof (unfold mat_def vec_eq_iff, auto)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. U $ ia $ ia = 1
 2. \<And>i ia. i \<noteq> ia \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
fix ia
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ia. U $ ia $ ia = 1
 2. \<And>i ia. i \<noteq> ia \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
show "U $ ia $ ia = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ ia $ ia = 1
[PROOF STEP]
using Uii_1
[PROOF STATE]
proof (prove)
using this:
\<forall>i. U $ i $ i = 1

goal (1 subgoal):
 1. U $ ia $ ia = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
U $ ia $ ia = 1

goal (1 subgoal):
 1. \<And>i ia. i \<noteq> ia \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i ia. i \<noteq> ia \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
assume i_ia: "i \<noteq> ia"
[PROOF STATE]
proof (state)
this:
i \<noteq> ia

goal (1 subgoal):
 1. \<And>i ia. i \<noteq> ia \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
show "U $ i $ ia = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U $ i $ ia = 0
[PROOF STEP]
proof (cases "ia<i")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ia < i \<Longrightarrow> U $ i $ ia = 0
 2. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
ia < i

goal (2 subgoals):
 1. ia < i \<Longrightarrow> U $ i $ ia = 0
 2. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
ia < i

goal (1 subgoal):
 1. U $ i $ ia = 0
[PROOF STEP]
using upper_triangular_U
[PROOF STATE]
proof (prove)
using this:
ia < i
upper_triangular U

goal (1 subgoal):
 1. U $ i $ ia = 0
[PROOF STEP]
unfolding upper_triangular_def
[PROOF STATE]
proof (prove)
using this:
ia < i
\<forall>i j. j < i \<longrightarrow> U $ i $ j = 0

goal (1 subgoal):
 1. U $ i $ ia = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
U $ i $ ia = 0

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> ia < i

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
hence i_less_ia: "i<ia"
[PROOF STATE]
proof (prove)
using this:
\<not> ia < i

goal (1 subgoal):
 1. i < ia
[PROOF STEP]
using i_ia
[PROOF STATE]
proof (prove)
using this:
\<not> ia < i
i \<noteq> ia

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

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
define a where "a = to_nat ia - to_nat i"
[PROOF STATE]
proof (state)
this:
a = mod_type_class.to_nat ia - mod_type_class.to_nat i

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
have ia_eq: "ia = i + from_nat a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = i + mod_type_class.from_nat a
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ia = i + mod_type_class.from_nat (mod_type_class.to_nat ia - mod_type_class.to_nat i)
[PROOF STEP]
by (metis i_less_ia a_def add_to_nat_def dual_order.strict_iff_order from_nat_to_nat_id
            le_add_diff_inverse less_imp_diff_less to_nat_from_nat_id to_nat_less_card to_nat_mono)
[PROOF STATE]
proof (state)
this:
ia = i + mod_type_class.from_nat a

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
have "1 \<le> a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> a
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> mod_type_class.to_nat ia - mod_type_class.to_nat i
[PROOF STEP]
by (metis diff_is_0_eq i_less_ia less_one not_less to_nat_mono)
[PROOF STATE]
proof (state)
this:
1 \<le> a

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
1 \<le> a

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
have "a < ncols A - to_nat i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a < ncols A - mod_type_class.to_nat i
[PROOF STEP]
unfolding a_def ncols_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mod_type_class.to_nat ia - mod_type_class.to_nat i < CARD('n) - mod_type_class.to_nat i
[PROOF STEP]
by (metis False diff_less_mono not_less to_nat_less_card to_nat_mono')
[PROOF STATE]
proof (state)
this:
a < ncols A - mod_type_class.to_nat i

goal (1 subgoal):
 1. \<not> ia < i \<Longrightarrow> U $ i $ ia = 0
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
1 \<le> a
a < ncols A - mod_type_class.to_nat i
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
a < ncols A - mod_type_class.to_nat i

goal (1 subgoal):
 1. U $ i $ ia = 0
[PROOF STEP]
using zero_above
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
a < ncols A - mod_type_class.to_nat i
\<forall>j s. 1 \<le> j \<and> j < ncols A - mod_type_class.to_nat s \<longrightarrow> U $ s $ (s + mod_type_class.from_nat j) = 0

goal (1 subgoal):
 1. U $ i $ ia = 0
[PROOF STEP]
unfolding ia_eq
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
a < ncols A - mod_type_class.to_nat i
\<forall>j s. 1 \<le> j \<and> j < ncols A - mod_type_class.to_nat s \<longrightarrow> U $ s $ (s + mod_type_class.from_nat j) = 0

goal (1 subgoal):
 1. U $ i $ (i + mod_type_class.from_nat a) = 0
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
U $ i $ ia = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U $ i $ ia = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
U = mat 1

goal (1 subgoal):
 1. H = K
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
U = mat 1

goal (1 subgoal):
 1. H = K
[PROOF STEP]
using H_UK matrix_mul_lid
[PROOF STATE]
proof (prove)
using this:
U = mat 1
H = U ** K
mat (1::?'a) ** ?A = ?A

goal (1 subgoal):
 1. H = K
[PROOF STEP]
by fast
[PROOF STATE]
proof (state)
this:
H = K

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_all_fast_exp_7681:
"list_all (\<lambda>l. fast_exp_7681 (3844::int) l \<noteq> 1) [1..<256]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>l. fast_exp_7681 3844 l \<noteq> 1) [1..<256]
[PROOF STEP]
by (subst upt_conv_Cons, simp, subst list_all_simps(1), intro conjI, eval)+
   force


[STATEMENT]
lemma fast_exp_7681_less256:
assumes "0<l" "l<256"
shows "fast_exp_7681 3844 l \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fast_exp_7681 3844 l \<noteq> 1
[PROOF STEP]
using list_all_fast_exp_7681 assms
[PROOF STATE]
proof (prove)
using this:
list_all (\<lambda>l. fast_exp_7681 3844 l \<noteq> 1) [1..<256]
0 < l
l < 256

goal (1 subgoal):
 1. fast_exp_7681 3844 l \<noteq> 1
[PROOF STEP]
by (smt (verit, ccfv_threshold) Ball_set One_nat_def atLeastLessThan_iff
  bot_nat_0.not_eq_extremum fast_exp_7681.elims less_Suc_numeral less_nat_zero_code
  not_less numeral_One numeral_less_iff set_upt)


[STATEMENT]
lemma powr_less256:
assumes "0<l" "l<256"
shows "(3844::fin7681 mod_ring)^l \<noteq> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3844 ^ l \<noteq> 1
[PROOF STEP]
using fast_exp_7681_less256[OF assms]
[PROOF STATE]
proof (prove)
using this:
fast_exp_7681 3844 l \<noteq> 1

goal (1 subgoal):
 1. 3844 ^ l \<noteq> 1
[PROOF STEP]
unfolding fast_exp_7681_to_mod_ring
[PROOF STATE]
proof (prove)
using this:
to_int_mod_ring (of_int_mod_ring 3844 ^ l) \<noteq> 1

goal (1 subgoal):
 1. 3844 ^ l \<noteq> 1
[PROOF STEP]
by (metis of_int_numeral of_int_of_int_mod_ring to_int_mod_ring_hom.hom_one)


[STATEMENT]
lemma infinite_infinite_subsets:
  assumes "infinite A"
  shows   "infinite {X. X \<subseteq> A \<and> infinite X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
have "\<forall>k. \<exists>X. X \<subseteq> A \<and> infinite X \<and> card (A - X) = k" for k :: nat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>k. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
fix k :: nat
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>k. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
obtain Y where "finite Y" "card Y = k" "Y \<subseteq> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>finite Y; card Y = k; Y \<subseteq> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infinite_arbitrarily_large[of A k] assms
[PROOF STATE]
proof (prove)
using this:
infinite A \<Longrightarrow> \<exists>B. finite B \<and> card B = k \<and> B \<subseteq> A
infinite A

goal (1 subgoal):
 1. (\<And>Y. \<lbrakk>finite Y; card Y = k; Y \<subseteq> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite Y
card Y = k
Y \<subseteq> A

goal (1 subgoal):
 1. \<And>k. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
finite Y
card Y = k
Y \<subseteq> A

goal (1 subgoal):
 1. \<And>k. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
finite Y
card Y = k
Y \<subseteq> A
[PROOF STEP]
have "A - (A - Y) = Y"
[PROOF STATE]
proof (prove)
using this:
finite Y
card Y = k
Y \<subseteq> A

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

goal (1 subgoal):
 1. \<And>k. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
finite Y
card Y = k
Y \<subseteq> A
A - (A - Y) = Y
[PROOF STEP]
show "\<exists>X. X \<subseteq> A \<and> infinite X \<and> card (A - X) = k"
[PROOF STATE]
proof (prove)
using this:
finite Y
card Y = k
Y \<subseteq> A
A - (A - Y) = Y

goal (1 subgoal):
 1. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite Y
card Y = k
Y \<subseteq> A
A - (A - Y) = Y
infinite A

goal (1 subgoal):
 1. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k
[PROOF STEP]
by (intro exI[of _ "A - Y"]) auto
[PROOF STATE]
proof (state)
this:
\<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>k. \<exists>X\<subseteq>A. infinite X \<and> card (A - X) = k

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
from choice[OF this]
[PROOF STATE]
proof (chain)
picking this:
\<exists>f. \<forall>x. f x \<subseteq> A \<and> infinite (f x) \<and> card (A - f x) = x
[PROOF STEP]
obtain f
    where f: "\<And>k. f k \<subseteq> A \<and> infinite (f k) \<and> card (A - f k) = k"
[PROOF STATE]
proof (prove)
using this:
\<exists>f. \<forall>x. f x \<subseteq> A \<and> infinite (f x) \<and> card (A - f x) = x

goal (1 subgoal):
 1. (\<And>f. (\<And>k. f k \<subseteq> A \<and> infinite (f k) \<and> card (A - f k) = k) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
f ?k \<subseteq> A \<and> infinite (f ?k) \<and> card (A - f ?k) = ?k

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
have "k = l" if "f k = f l" for k l
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k = l
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> l \<Longrightarrow> False
[PROOF STEP]
assume "k \<noteq> l"
[PROOF STATE]
proof (state)
this:
k \<noteq> l

goal (1 subgoal):
 1. k \<noteq> l \<Longrightarrow> False
[PROOF STEP]
hence "card (A - f k) \<noteq> card (A - f l)"
[PROOF STATE]
proof (prove)
using this:
k \<noteq> l

goal (1 subgoal):
 1. card (A - f k) \<noteq> card (A - f l)
[PROOF STEP]
using f[of k] f[of l]
[PROOF STATE]
proof (prove)
using this:
k \<noteq> l
f k \<subseteq> A \<and> infinite (f k) \<and> card (A - f k) = k
f l \<subseteq> A \<and> infinite (f l) \<and> card (A - f l) = l

goal (1 subgoal):
 1. card (A - f k) \<noteq> card (A - f l)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
card (A - f k) \<noteq> card (A - f l)

goal (1 subgoal):
 1. k \<noteq> l \<Longrightarrow> False
[PROOF STEP]
with \<open>f k = f l\<close>
[PROOF STATE]
proof (chain)
picking this:
f k = f l
card (A - f k) \<noteq> card (A - f l)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
f k = f l
card (A - f k) \<noteq> card (A - f l)

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:
f ?k = f ?l \<Longrightarrow> ?k = ?l

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
hence "inj f"
[PROOF STATE]
proof (prove)
using this:
f ?k = f ?l \<Longrightarrow> ?k = ?l

goal (1 subgoal):
 1. inj f
[PROOF STEP]
by (auto intro: injI)
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj f

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
have "range f \<subseteq> {X. X \<subseteq> A \<and> infinite X}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. range f \<subseteq> {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
f ?k \<subseteq> A \<and> infinite (f ?k) \<and> card (A - f ?k) = ?k

goal (1 subgoal):
 1. range f \<subseteq> {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
range f \<subseteq> {X. X \<subseteq> A \<and> infinite X}

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inj f
range f \<subseteq> {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj f
range f \<subseteq> {X. X \<subseteq> A \<and> infinite X}

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> infinite X}
[PROOF STEP]
by (subst infinite_iff_countable_subset) auto
[PROOF STATE]
proof (state)
this:
infinite {X. X \<subseteq> A \<and> infinite X}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma infinite_card_subsets:
  assumes "infinite A" "k > 0"
  shows   "infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
obtain B where B: "B \<subseteq> A" "finite B" "card B = k - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<subseteq> A; finite B; card B = k - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using infinite_arbitrarily_large[OF assms(1), of "k - 1"]
[PROOF STATE]
proof (prove)
using this:
\<exists>B. finite B \<and> card B = k - 1 \<and> B \<subseteq> A

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<subseteq> A; finite B; card B = k - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B \<subseteq> A
finite B
card B = k - 1

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
define f where "f = (\<lambda>x. insert x B)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>x. insert x B)

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
have "f ` (A - B) \<subseteq> {X. X \<subseteq> A \<and> finite X \<and> card X = k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f ` (A - B) \<subseteq> {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
using assms B
[PROOF STATE]
proof (prove)
using this:
infinite A
0 < k
B \<subseteq> A
finite B
card B = k - 1

goal (1 subgoal):
 1. f ` (A - B) \<subseteq> {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
by (auto simp: f_def)
[PROOF STATE]
proof (state)
this:
f ` (A - B) \<subseteq> {X. X \<subseteq> A \<and> finite X \<and> card X = k}

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f ` (A - B) \<subseteq> {X. X \<subseteq> A \<and> finite X \<and> card X = k}

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
have "inj_on f (A - B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on f (A - B)
[PROOF STEP]
by (auto intro!: inj_onI simp: f_def)
[PROOF STATE]
proof (state)
this:
inj_on f (A - B)

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
hence "infinite (f ` (A - B))"
[PROOF STATE]
proof (prove)
using this:
inj_on f (A - B)

goal (1 subgoal):
 1. infinite (f ` (A - B))
[PROOF STEP]
using assms B
[PROOF STATE]
proof (prove)
using this:
inj_on f (A - B)
infinite A
0 < k
B \<subseteq> A
finite B
card B = k - 1

goal (1 subgoal):
 1. infinite (f ` (A - B))
[PROOF STEP]
by (subst finite_image_iff) auto
[PROOF STATE]
proof (state)
this:
infinite (f ` (A - B))

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
f ` (A - B) \<subseteq> {X. X \<subseteq> A \<and> finite X \<and> card X = k}
infinite (f ` (A - B))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
f ` (A - B) \<subseteq> {X. X \<subseteq> A \<and> finite X \<and> card X = k}
infinite (f ` (A - B))

goal (1 subgoal):
 1. infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}
[PROOF STEP]
by (rule infinite_super)
[PROOF STATE]
proof (state)
this:
infinite {X. X \<subseteq> A \<and> finite X \<and> card X = k}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma comp_bij_eq_iff:
  assumes "bij f"
  shows   "g \<circ> f = h \<circ> f \<longleftrightarrow> g = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ> f = h \<circ> f) = (g = h)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g \<circ> f = h \<circ> f \<Longrightarrow> g = h
 2. g = h \<Longrightarrow> g \<circ> f = h \<circ> f
[PROOF STEP]
assume *: "g \<circ> f = h \<circ> f"
[PROOF STATE]
proof (state)
this:
g \<circ> f = h \<circ> f

goal (2 subgoals):
 1. g \<circ> f = h \<circ> f \<Longrightarrow> g = h
 2. g = h \<Longrightarrow> g \<circ> f = h \<circ> f
[PROOF STEP]
show "g = h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = h
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. g x = h x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. g x = h x
[PROOF STEP]
obtain y where [simp]: "x = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y. x = f y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using bij_is_surj[OF assms]
[PROOF STATE]
proof (prove)
using this:
surj f

goal (1 subgoal):
 1. (\<And>y. x = f y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x = f y

goal (1 subgoal):
 1. \<And>x. g x = h x
[PROOF STEP]
have "(g \<circ> f) y = (h \<circ> f) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g \<circ> f) y = (h \<circ> f) y
[PROOF STEP]
by (simp only: *)
[PROOF STATE]
proof (state)
this:
(g \<circ> f) y = (h \<circ> f) y

goal (1 subgoal):
 1. \<And>x. g x = h x
[PROOF STEP]
thus "g x = h x"
[PROOF STATE]
proof (prove)
using this:
(g \<circ> f) y = (h \<circ> f) y

goal (1 subgoal):
 1. g x = h x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g x = h x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
g = h

goal (1 subgoal):
 1. g = h \<Longrightarrow> g \<circ> f = h \<circ> f
[PROOF STEP]
qed auto


[STATEMENT]
lemma sum_list_replicate [simp]:
  "sum_list (replicate n x) = of_nat n * (x :: 'a :: semiring_1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (replicate n x) = of_nat n * x
[PROOF STEP]
by (induction n) (auto simp: algebra_simps)


[STATEMENT]
lemma ex_subset_of_card:
  assumes "finite A" "card A \<ge> k"
  shows   "\<exists>B. B \<subseteq> A \<and> card B = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B\<subseteq>A. card B = k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite A
k \<le> card A

goal (1 subgoal):
 1. \<exists>B\<subseteq>A. card B = k
[PROOF STEP]
proof (induction arbitrary: k rule: finite_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>k. k \<le> card {} \<Longrightarrow> \<exists>B\<subseteq>{}. card B = k
 2. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. k \<le> card F \<Longrightarrow> \<exists>B\<subseteq>F. card B = k; k \<le> card (insert x F)\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>insert x F. card B = k
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
k \<le> card {}

goal (2 subgoals):
 1. \<And>k. k \<le> card {} \<Longrightarrow> \<exists>B\<subseteq>{}. card B = k
 2. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. k \<le> card F \<Longrightarrow> \<exists>B\<subseteq>F. card B = k; k \<le> card (insert x F)\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>insert x F. card B = k
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
k \<le> card {}

goal (1 subgoal):
 1. \<exists>B\<subseteq>{}. card B = k
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>{}. card B = k

goal (1 subgoal):
 1. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. k \<le> card F \<Longrightarrow> \<exists>B\<subseteq>F. card B = k; k \<le> card (insert x F)\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>insert x F. card B = k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. k \<le> card F \<Longrightarrow> \<exists>B\<subseteq>F. card B = k; k \<le> card (insert x F)\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>insert x F. card B = k
[PROOF STEP]
case (insert x A k)
[PROOF STATE]
proof (state)
this:
finite A
x \<notin> A
?k \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?k
k \<le> card (insert x A)

goal (1 subgoal):
 1. \<And>x F k. \<lbrakk>finite F; x \<notin> F; \<And>k. k \<le> card F \<Longrightarrow> \<exists>B\<subseteq>F. card B = k; k \<le> card (insert x F)\<rbrakk> \<Longrightarrow> \<exists>B\<subseteq>insert x F. card B = k
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
proof (cases "k = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. k = 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
 2. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
k = 0

goal (2 subgoals):
 1. k = 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
 2. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
k = 0

goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
by (intro exI[of _ "{}"]) auto
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>insert x A. card B = k

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
k \<noteq> 0

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
from insert
[PROOF STATE]
proof (chain)
picking this:
finite A
x \<notin> A
?k \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?k
k \<le> card (insert x A)
[PROOF STEP]
have "\<exists>B\<subseteq>A. card B = k - 1"
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
?k \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?k
k \<le> card (insert x A)

goal (1 subgoal):
 1. \<exists>B\<subseteq>A. card B = k - 1
[PROOF STEP]
by (intro insert.IH) auto
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>A. card B = k - 1

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>B\<subseteq>A. card B = k - 1
[PROOF STEP]
obtain B where B: "B \<subseteq> A" "card B = k - 1"
[PROOF STATE]
proof (prove)
using this:
\<exists>B\<subseteq>A. card B = k - 1

goal (1 subgoal):
 1. (\<And>B. \<lbrakk>B \<subseteq> A; card B = k - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<subseteq> A
card B = k - 1

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
with insert
[PROOF STATE]
proof (chain)
picking this:
finite A
x \<notin> A
?k \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?k
k \<le> card (insert x A)
B \<subseteq> A
card B = k - 1
[PROOF STEP]
have [simp]: "x \<notin> B"
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
?k \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?k
k \<le> card (insert x A)
B \<subseteq> A
card B = k - 1

goal (1 subgoal):
 1. x \<notin> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<notin> B

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
have "insert x B \<subseteq> insert x A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert x B \<subseteq> insert x A
[PROOF STEP]
using B insert
[PROOF STATE]
proof (prove)
using this:
B \<subseteq> A
card B = k - 1
finite A
x \<notin> A
?k \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?k
k \<le> card (insert x A)

goal (1 subgoal):
 1. insert x B \<subseteq> insert x A
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
insert x B \<subseteq> insert x A

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
insert x B \<subseteq> insert x A

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
have "card (insert x B) = k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (insert x B) = k
[PROOF STEP]
using insert B finite_subset[of B A] False
[PROOF STATE]
proof (prove)
using this:
finite A
x \<notin> A
?k \<le> card A \<Longrightarrow> \<exists>B\<subseteq>A. card B = ?k
k \<le> card (insert x A)
B \<subseteq> A
card B = k - 1
\<lbrakk>B \<subseteq> A; finite A\<rbrakk> \<Longrightarrow> finite B
k \<noteq> 0

goal (1 subgoal):
 1. card (insert x B) = k
[PROOF STEP]
by (subst card.insert_remove) auto
[PROOF STATE]
proof (state)
this:
card (insert x B) = k

goal (1 subgoal):
 1. k \<noteq> 0 \<Longrightarrow> \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
insert x B \<subseteq> insert x A
card (insert x B) = k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
insert x B \<subseteq> insert x A
card (insert x B) = k

goal (1 subgoal):
 1. \<exists>B\<subseteq>insert x A. card B = k
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>insert x A. card B = k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>B\<subseteq>insert x A. card B = k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_sorted_list_of_set [simp]: "length (sorted_list_of_set A) = card A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (sorted_list_of_set A) = card A
[PROOF STEP]
using distinct_card[of "sorted_list_of_set A"]
[PROOF STATE]
proof (prove)
using this:
distinct (sorted_list_of_set A) \<Longrightarrow> card (set (sorted_list_of_set A)) = length (sorted_list_of_set A)

goal (1 subgoal):
 1. length (sorted_list_of_set A) = card A
[PROOF STEP]
by (cases "finite A") simp_all


[STATEMENT]
lemma upt_add_eq_append': "i \<le> j \<Longrightarrow> j \<le> k \<Longrightarrow> [i..<k] = [i..<j] @ [j..<k]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> [i..<k] = [i..<j] @ [j..<k]
[PROOF STEP]
using upt_add_eq_append[of i j "k - j"]
[PROOF STATE]
proof (prove)
using this:
i \<le> j \<Longrightarrow> [i..<j + (k - j)] = [i..<j] @ [j..<j + (k - j)]

goal (1 subgoal):
 1. \<lbrakk>i \<le> j; j \<le> k\<rbrakk> \<Longrightarrow> [i..<k] = [i..<j] @ [j..<k]
[PROOF STEP]
by simp


[STATEMENT]
lemma minus_closed [simp]: "x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x - y \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x - y \<in> A
[PROOF STEP]
using add_closed[of x "-y"] uminus_closed[of y]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>x \<in> A; - y \<in> A\<rbrakk> \<Longrightarrow> x + - y \<in> A
y \<in> A \<Longrightarrow> - y \<in> A

goal (1 subgoal):
 1. \<lbrakk>x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> x - y \<in> A
[PROOF STEP]
by auto


[STATEMENT]
lemma sum_closed [intro]: "(\<And>x. x \<in> X \<Longrightarrow> f x \<in> A) \<Longrightarrow> sum f X \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> f x \<in> A) \<Longrightarrow> sum f X \<in> A
[PROOF STEP]
by (induction X rule: infinite_finite_induct) auto


[STATEMENT]
lemma power_closed [intro]: "x \<in> A \<Longrightarrow> x ^ n \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> A \<Longrightarrow> x ^ n \<in> A
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma Sum_any_closed [intro]: "(\<And>x. f x \<in> A) \<Longrightarrow> Sum_any f \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x \<in> A) \<Longrightarrow> Sum_any f \<in> A
[PROOF STEP]
unfolding Sum_any.expand_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x \<in> A) \<Longrightarrow> sum f {a. f a \<noteq> (0::'a)} \<in> A
[PROOF STEP]
by (rule sum_closed)


[STATEMENT]
lemma prod_closed [intro]: "(\<And>x. x \<in> X \<Longrightarrow> f x \<in> A) \<Longrightarrow> prod f X \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> X \<Longrightarrow> f x \<in> A) \<Longrightarrow> prod f X \<in> A
[PROOF STEP]
by (induction X rule: infinite_finite_induct) auto


[STATEMENT]
lemma Prod_any_closed [intro]: "(\<And>x. f x \<in> A) \<Longrightarrow> Prod_any f \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x \<in> A) \<Longrightarrow> Prod_any f \<in> A
[PROOF STEP]
unfolding Prod_any.expand_set
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. f x \<in> A) \<Longrightarrow> prod f {a. f a \<noteq> (1::'a)} \<in> A
[PROOF STEP]
by (rule prod_closed)


[STATEMENT]
lemma prod_fun_closed [intro]: "(\<And>x. f x \<in> A) \<Longrightarrow> (\<And>x. g x \<in> A) \<Longrightarrow> prod_fun f g x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. f x \<in> A; \<And>x. g x \<in> A\<rbrakk> \<Longrightarrow> prod_fun f g x \<in> A
[PROOF STEP]
by (auto simp: prod_fun_def when_def intro!: Sum_any_closed mult_closed)


[STATEMENT]
lemma of_int_closed [simp, intro]: "of_int n \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int n \<in> A
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma diff [simp]: "f (x - y) = f x - f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (x - y) = f x - f y
[PROOF STEP]
using add[of x "-y"]
[PROOF STATE]
proof (prove)
using this:
f (x + - y) = f x + f (- y)

goal (1 subgoal):
 1. f (x - y) = f x - f y
[PROOF STEP]
by (simp del: add)


[STATEMENT]
lemma power [simp]: "f (x ^ n) = f x ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (x ^ n) = f x ^ n
[PROOF STEP]
by (induction n) auto


[STATEMENT]
lemma sum [simp]: "f (sum g A) = (\<Sum>x\<in>A. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (sum g A) = (\<Sum>x\<in>A. f (g x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma prod [simp]: "f (prod g A) = (\<Prod>x\<in>A. f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (prod g A) = (\<Prod>x\<in>A. f (g x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) auto


[STATEMENT]
lemma ring_homomorphism_id [intro]: "ring_homomorphism id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism id
[PROOF STEP]
by standard auto


[STATEMENT]
lemma ring_homomorphism_id' [intro]: "ring_homomorphism (\<lambda>x. x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism (\<lambda>x. x)
[PROOF STEP]
by standard auto


[STATEMENT]
lemma ring_homomorphism_of_int [intro]: "ring_homomorphism of_int"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ring_homomorphism of_int
[PROOF STEP]
by standard auto


[STATEMENT]
lemma poly_mapping_nat_ge_0 [simp]: "(m :: nat \<Rightarrow>\<^sub>0 nat) \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> m
[PROOF STEP]
proof (cases "m = 0")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> 0 \<le> m
 2. m \<noteq> 0 \<Longrightarrow> 0 \<le> m
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
m \<noteq> 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> 0 \<le> m
 2. m \<noteq> 0 \<Longrightarrow> 0 \<le> m
[PROOF STEP]
hence "Poly_Mapping.lookup m \<noteq> Poly_Mapping.lookup 0"
[PROOF STATE]
proof (prove)
using this:
m \<noteq> 0

goal (1 subgoal):
 1. lookup m \<noteq> lookup 0
[PROOF STEP]
by transfer auto
[PROOF STATE]
proof (state)
this:
lookup m \<noteq> lookup 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> 0 \<le> m
 2. m \<noteq> 0 \<Longrightarrow> 0 \<le> m
[PROOF STEP]
hence "\<exists>k. Poly_Mapping.lookup m k \<noteq> 0"
[PROOF STATE]
proof (prove)
using this:
lookup m \<noteq> lookup 0

goal (1 subgoal):
 1. \<exists>k. lookup m k \<noteq> 0
[PROOF STEP]
by (auto simp: fun_eq_iff)
[PROOF STATE]
proof (state)
this:
\<exists>k. lookup m k \<noteq> 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> 0 \<le> m
 2. m \<noteq> 0 \<Longrightarrow> 0 \<le> m
[PROOF STEP]
from LeastI_ex[OF this] Least_le[of "\<lambda>k. Poly_Mapping.lookup m k \<noteq> 0"]
[PROOF STATE]
proof (chain)
picking this:
lookup m (LEAST k. lookup m k \<noteq> 0) \<noteq> 0
lookup m ?k \<noteq> 0 \<Longrightarrow> (LEAST x. lookup m x \<noteq> 0) \<le> ?k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup m (LEAST k. lookup m k \<noteq> 0) \<noteq> 0
lookup m ?k \<noteq> 0 \<Longrightarrow> (LEAST x. lookup m x \<noteq> 0) \<le> ?k

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

goal (1 subgoal):
 1. m = 0 \<Longrightarrow> 0 \<le> m
[PROOF STEP]
qed auto


[STATEMENT]
lemma poly_mapping_nat_le_0 [simp]: "(m :: nat \<Rightarrow>\<^sub>0 nat) \<le> 0 \<longleftrightarrow> m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (m \<le> 0) = (m = 0)
[PROOF STEP]
unfolding less_eq_poly_mapping_def poly_mapping_eq_iff less_fun_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_fun lookup (map_fun lookup id) (\<lambda>f g. (\<exists>k. f k < g k \<and> (\<forall>k'<k. f k' = g k')) \<or> f = g) m 0 = (lookup m = lookup 0)
[PROOF STEP]
by auto


[STATEMENT]
lemma of_nat_diff_poly_mapping_nat:
  assumes "m \<ge> n"
  shows   "of_nat (m - n) = (of_nat m - of_nat n :: 'a :: monoid_add \<Rightarrow>\<^sub>0 nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat (m - n) = of_nat m - of_nat n
[PROOF STEP]
by (auto intro!: poly_mapping_eqI simp: lookup_of_nat lookup_minus when_def)


[STATEMENT]
lemma mpoly_coeff_transfer [transfer_rule]:
  "rel_fun cr_mpoly (=) poly_mapping.lookup MPoly_Type.coeff"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun cr_mpoly (=) lookup MPoly_Type.coeff
[PROOF STEP]
unfolding MPoly_Type.coeff_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun cr_mpoly (=) lookup (\<lambda>p. lookup (mapping_of p))
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma mapping_of_sum: "(\<Sum>x\<in>A. mapping_of (f x)) = mapping_of (sum f A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x\<in>A. mapping_of (f x)) = mapping_of (sum f A)
[PROOF STEP]
by (induction A rule: infinite_finite_induct) (auto simp: plus_mpoly.rep_eq zero_mpoly.rep_eq)


[STATEMENT]
lemma mapping_of_eq_0_iff [simp]: "mapping_of p = 0 \<longleftrightarrow> p = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mapping_of p = 0) = (p = 0)
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma Sum_any_mapping_of: "Sum_any (\<lambda>x. mapping_of (f x)) = mapping_of (Sum_any f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x. mapping_of (f x)) = mapping_of (Sum_any f)
[PROOF STEP]
by (simp add: Sum_any.expand_set mapping_of_sum)


[STATEMENT]
lemma Sum_any_parametric_cr_mpoly [transfer_rule]:
  "(rel_fun (rel_fun (=) cr_mpoly) cr_mpoly) Sum_any Sum_any"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_fun (rel_fun (=) cr_mpoly) cr_mpoly Sum_any Sum_any
[PROOF STEP]
by (auto simp: rel_fun_def cr_mpoly_def Sum_any_mapping_of)


[STATEMENT]
lemma lookup_mult_of_nat [simp]: "lookup (of_nat n * m) k = n * lookup m k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
have "of_nat n * m = (\<Sum>i<n. m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_nat n * m = (\<Sum>i<n. m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
of_nat n * m = (\<Sum>i<n. m)

goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
of_nat n * m = (\<Sum>i<n. m)

goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
have "lookup \<dots> k = (\<Sum>i<n. lookup m k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup (\<Sum>i<n. m) k = (\<Sum>i<n. lookup m k)
[PROOF STEP]
by (simp only: lookup_sum)
[PROOF STATE]
proof (state)
this:
lookup (\<Sum>i<n. m) k = (\<Sum>i<n. lookup m k)

goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
lookup (\<Sum>i<n. m) k = (\<Sum>i<n. lookup m k)

goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
have "\<dots> = n * lookup m k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<n. lookup m k) = n * lookup m k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<n. lookup m k) = n * lookup m k

goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
lookup (of_nat n * m) k = n * lookup m k

goal (1 subgoal):
 1. lookup (of_nat n * m) k = n * lookup m k
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
lookup (of_nat n * m) k = n * lookup m k

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma coeff_mpoly_times:
  "MPoly_Type.coeff (p * q) mon = prod_fun (MPoly_Type.coeff p) (MPoly_Type.coeff q) mon"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (p * q) mon = prod_fun (MPoly_Type.coeff p) (MPoly_Type.coeff q) mon
[PROOF STEP]
by (transfer', transfer') auto


[STATEMENT]
lemma (in ring_closed) coeff_mult_closed [intro]:
  "(\<And>x. coeff p x \<in> A) \<Longrightarrow> (\<And>x. coeff q x \<in> A) \<Longrightarrow> coeff (p * q) x \<in> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x. MPoly_Type.coeff p x \<in> A; \<And>x. MPoly_Type.coeff q x \<in> A\<rbrakk> \<Longrightarrow> MPoly_Type.coeff (p * q) x \<in> A
[PROOF STEP]
by (auto simp: coeff_mpoly_times prod_fun_closed)


[STATEMENT]
lemma coeff_notin_vars:
  assumes "\<not>(keys m \<subseteq> vars p)"
  shows   "coeff p m = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff p m = (0::'a)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<not> keys m \<subseteq> vars p

goal (1 subgoal):
 1. MPoly_Type.coeff p m = (0::'a)
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
using this:
\<not> keys m \<subseteq> \<Union> (keys ` keys (mapping_of p))

goal (1 subgoal):
 1. MPoly_Type.coeff p m = (0::'a)
[PROOF STEP]
by transfer' (auto simp: in_keys_iff)


[STATEMENT]
lemma finite_coeff_support [intro]: "finite {m. coeff p m \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {m. MPoly_Type.coeff p m \<noteq> (0::'a)}
[PROOF STEP]
by transfer simp


[STATEMENT]
lemma insertion_altdef:
  "insertion f p = Sum_any (\<lambda>m. coeff p m * Prod_any (\<lambda>i. f i ^ lookup m i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f p = (\<Sum>m. MPoly_Type.coeff p m * (\<Prod>i. f i ^ lookup m i))
[PROOF STEP]
by (transfer', transfer') (simp add: insertion_fun_def)


[STATEMENT]
lemma mpoly_coeff_uminus [simp]: "coeff (-p) m = -coeff p m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (- p) m = - MPoly_Type.coeff p m
[PROOF STEP]
by transfer auto


[STATEMENT]
lemma Sum_any_uminus: "Sum_any (\<lambda>x. -f x :: 'a :: ab_group_add) = -Sum_any f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x. - f x) = - Sum_any f
[PROOF STEP]
by (simp add: Sum_any.expand_set sum_negf)


[STATEMENT]
lemma insertion_uminus [simp]: "insertion f (-p :: 'a :: comm_ring_1 mpoly) = -insertion f p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (- p) = - insertion f p
[PROOF STEP]
by (simp add: insertion_altdef Sum_any_uminus)


[STATEMENT]
lemma Sum_any_lookup: "finite {x. g x \<noteq> 0} \<Longrightarrow> Sum_any (\<lambda>x. lookup (g x) y) = lookup (Sum_any g) y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {x. g x \<noteq> 0} \<Longrightarrow> (\<Sum>x. lookup (g x) y) = lookup (Sum_any g) y
[PROOF STEP]
by (auto simp: Sum_any.expand_set lookup_sum intro!: sum.mono_neutral_left)


[STATEMENT]
lemma Sum_any_diff:
  assumes "finite {x. f x \<noteq> 0}"
  assumes "finite {x. g x \<noteq> 0}"
  shows   "Sum_any (\<lambda>x. f x - g x :: 'a :: ab_group_add) = Sum_any f - Sum_any g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>x. f x - g x) = Sum_any f - Sum_any g
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<Sum>x. f x - g x) = Sum_any f - Sum_any g
[PROOF STEP]
have "{x. f x - g x \<noteq> 0} \<subseteq> {x. f x \<noteq> 0} \<union> {x. g x \<noteq> 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. f x - g x \<noteq> (0::'a)} \<subseteq> {x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{x. f x - g x \<noteq> (0::'a)} \<subseteq> {x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)}

goal (1 subgoal):
 1. (\<Sum>x. f x - g x) = Sum_any f - Sum_any g
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
{x. f x - g x \<noteq> (0::'a)} \<subseteq> {x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)}

goal (1 subgoal):
 1. (\<Sum>x. f x - g x) = Sum_any f - Sum_any g
[PROOF STEP]
have "finite ({x. f x \<noteq> 0} \<union> {x. g x \<noteq> 0})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite ({x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)})
[PROOF STEP]
by (subst finite_Un) (insert assms, auto)
[PROOF STATE]
proof (state)
this:
finite ({x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)})

goal (1 subgoal):
 1. (\<Sum>x. f x - g x) = Sum_any f - Sum_any g
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
{x. f x - g x \<noteq> (0::'a)} \<subseteq> {x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)}
finite ({x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)})
[PROOF STEP]
have "finite {x. f x - g x \<noteq> 0}"
[PROOF STATE]
proof (prove)
using this:
{x. f x - g x \<noteq> (0::'a)} \<subseteq> {x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)}
finite ({x. f x \<noteq> (0::'a)} \<union> {x. g x \<noteq> (0::'a)})

goal (1 subgoal):
 1. finite {x. f x - g x \<noteq> (0::'a)}
[PROOF STEP]
by (rule finite_subset)
[PROOF STATE]
proof (state)
this:
finite {x. f x - g x \<noteq> (0::'a)}

goal (1 subgoal):
 1. (\<Sum>x. f x - g x) = Sum_any f - Sum_any g
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
finite {x. f x \<noteq> (0::'a)}
finite {x. g x \<noteq> (0::'a)}
finite {x. f x - g x \<noteq> (0::'a)}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
finite {x. f x \<noteq> (0::'a)}
finite {x. g x \<noteq> (0::'a)}
finite {x. f x - g x \<noteq> (0::'a)}

goal (1 subgoal):
 1. (\<Sum>x. f x - g x) = Sum_any f - Sum_any g
[PROOF STEP]
by (simp add: algebra_simps Sum_any.distrib [symmetric])
[PROOF STATE]
proof (state)
this:
(\<Sum>x. f x - g x) = Sum_any f - Sum_any g

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_diff:
  "insertion f (p - q :: 'a :: comm_ring_1 mpoly) = insertion f p - insertion f q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (p - q) = insertion f p - insertion f q
[PROOF STEP]
proof (transfer, transfer)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
fix f :: "nat \<Rightarrow> 'a" and p q :: "(nat \<Rightarrow>\<^sub>0 nat) \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
assume fin: "finite {x. p x \<noteq> 0}" "finite {x. q x \<noteq> 0}"
[PROOF STATE]
proof (state)
this:
finite {x. p x \<noteq> (0::'a)}
finite {x. q x \<noteq> (0::'a)}

goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
have "insertion_fun f (\<lambda>x. p x - q x) =
          (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v) - q m * (\<Prod>v. f v ^ lookup m v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion_fun f (\<lambda>x. p x - q x) = (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v) - q m * (\<Prod>v. f v ^ lookup m v))
[PROOF STEP]
by (simp add: insertion_fun_def algebra_simps Sum_any_diff)
[PROOF STATE]
proof (state)
this:
insertion_fun f (\<lambda>x. p x - q x) = (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v) - q m * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
insertion_fun f (\<lambda>x. p x - q x) = (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v) - q m * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
have "\<dots> = (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v)) - (\<Sum>m. q m * (\<Prod>v. f v ^ lookup m v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v) - q m * (\<Prod>v. f v ^ lookup m v)) = (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v)) - (\<Sum>m. q m * (\<Prod>v. f v ^ lookup m v))
[PROOF STEP]
by (subst Sum_any_diff) (auto intro: finite_subset[OF _ fin(1)] finite_subset[OF _ fin(2)])
[PROOF STATE]
proof (state)
this:
(\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v) - q m * (\<Prod>v. f v ^ lookup m v)) = (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v)) - (\<Sum>m. q m * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v) - q m * (\<Prod>v. f v ^ lookup m v)) = (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v)) - (\<Sum>m. q m * (\<Prod>v. f v ^ lookup m v))

goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
have "\<dots> = insertion_fun f p - insertion_fun f q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v)) - (\<Sum>m. q m * (\<Prod>v. f v ^ lookup m v)) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
by (simp add: insertion_fun_def)
[PROOF STATE]
proof (state)
this:
(\<Sum>m. p m * (\<Prod>v. f v ^ lookup m v)) - (\<Sum>m. q m * (\<Prod>v. f v ^ lookup m v)) = insertion_fun f p - insertion_fun f q

goal (1 subgoal):
 1. \<And>f p q. \<lbrakk>finite {x. p x \<noteq> (0::'a)}; finite {x. q x \<noteq> (0::'a)}\<rbrakk> \<Longrightarrow> insertion_fun f (\<lambda>k. p k - q k) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
insertion_fun f (\<lambda>x. p x - q x) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
show "insertion_fun f (\<lambda>x. p x - q x) = \<dots>"
[PROOF STATE]
proof (prove)
using this:
insertion_fun f (\<lambda>x. p x - q x) = insertion_fun f p - insertion_fun f q

goal (1 subgoal):
 1. insertion_fun f (\<lambda>x. p x - q x) = insertion_fun f p - insertion_fun f q
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
insertion_fun f (\<lambda>x. p x - q x) = insertion_fun f p - insertion_fun f q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insertion_power: "insertion f (p ^ n) = insertion f p ^ n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (p ^ n) = insertion f p ^ n
[PROOF STEP]
by (induction n) (simp_all add: insertion_mult)


[STATEMENT]
lemma insertion_sum: "insertion f (sum g A) = (\<Sum>x\<in>A. insertion f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (sum g A) = (\<Sum>x\<in>A. insertion f (g x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) (auto simp: insertion_add)


[STATEMENT]
lemma insertion_prod: "insertion f (prod g A) = (\<Prod>x\<in>A. insertion f (g x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insertion f (prod g A) = (\<Prod>x\<in>A. insertion f (g x))
[PROOF STEP]
by (induction A rule: infinite_finite_induct) (auto simp: insertion_mult)


[STATEMENT]
lemma coeff_Var: "coeff (Var i) m = (1 when m = Poly_Mapping.single i 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MPoly_Type.coeff (Var i) m = ((1::'a) when m = Poly_Mapping.single i 1)
[PROOF STEP]
by transfer' (auto simp: Var\<^sub>0_def lookup_single when_def)


[STATEMENT]
lemma vars_Var: "vars (Var i :: 'a :: {one,zero} mpoly) = (if (0::'a) = 1 then {} else {i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars (Var i) = (if (0::'a) = (1::'a) then {} else {i})
[PROOF STEP]
unfolding vars_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> (keys ` keys (mapping_of (Var i))) = (if (0::'a) = (1::'a) then {} else {i})
[PROOF STEP]
by (auto simp: Var.rep_eq Var\<^sub>0_def)