[STATEMENT]
lemma char_poly_0_column: fixes A :: "'a :: idom mat"
  assumes 0: "\<And> j. j < n \<Longrightarrow> A $$ (j,i) = 0"
  and A: "A \<in> carrier_mat n n"
  and i: "i < n"
shows "char_poly A = monom 1 1 * char_poly (mat_delete A i i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
let ?n = "n - 1"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
let ?A = "mat_delete A i i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
let ?sum = "[:0, 1:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
define Sum where "Sum = ?sum"
[PROOF STATE]
proof (state)
this:
Sum = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
let ?f = "\<lambda> j. Sum $$ (j, i) * cofactor Sum j i"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have Sum: "Sum \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum \<in> carrier_mat n n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. Sum \<in> carrier_mat n n
[PROOF STEP]
unfolding Sum_def
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

goal (1 subgoal):
 1. [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A \<in> carrier_mat n n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Sum \<in> carrier_mat n n

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
A \<in> carrier_mat n n
[PROOF STEP]
have id: "dim_row A = n"
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

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

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have "char_poly A = (\<Sum>j<n. ?f j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. char_poly A = (\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i)
[PROOF STEP]
unfolding char_poly_def[of A] char_poly_matrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A) = (\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i)
[PROOF STEP]
using laplace_expansion_column[OF Sum i]
[PROOF STATE]
proof (prove)
using this:
det Sum = (\<Sum>ia<n. Sum $$ (ia, i) * cofactor Sum ia i)

goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A) = (\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i)
[PROOF STEP]
unfolding Sum_def
[PROOF STATE]
proof (prove)
using this:
det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) = (\<Sum>ia<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (ia, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) ia i)

goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A) = (\<Sum>j<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (j, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) j i)
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) = (\<Sum>ia<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (ia, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) ia i)
A \<in> carrier_mat n n

goal (1 subgoal):
 1. det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row A) + map_mat (\<lambda>a. [:- a:]) A) = (\<Sum>j<n. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (j, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) j i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
char_poly A = (\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
char_poly A = (\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have "\<dots> = ?f i + sum ?f ({..<n} - {i})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i) = Sum $$ (i, i) * cofactor Sum i i + (\<Sum>j\<in>{..<n} - {i}. Sum $$ (j, i) * cofactor Sum j i)
[PROOF STEP]
by (rule sum.remove[of _ i], insert i, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i) = Sum $$ (i, i) * cofactor Sum i i + (\<Sum>j\<in>{..<n} - {i}. Sum $$ (j, i) * cofactor Sum j i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>j<n. Sum $$ (j, i) * cofactor Sum j i) = Sum $$ (i, i) * cofactor Sum i i + (\<Sum>j\<in>{..<n} - {i}. Sum $$ (j, i) * cofactor Sum j i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have "\<dots> = ?f i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum $$ (i, i) * cofactor Sum i i + (\<Sum>j\<in>{..<n} - {i}. Sum $$ (j, i) * cofactor Sum j i) = Sum $$ (i, i) * cofactor Sum i i
[PROOF STEP]
proof (subst sum.neutral, intro ballI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {..<n} - {i} \<Longrightarrow> Sum $$ (x, i) * cofactor Sum x i = 0
 2. Sum $$ (i, i) * cofactor Sum i i + 0 = Sum $$ (i, i) * cofactor Sum i i
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> {..<n} - {i} \<Longrightarrow> Sum $$ (x, i) * cofactor Sum x i = 0
 2. Sum $$ (i, i) * cofactor Sum i i + 0 = Sum $$ (i, i) * cofactor Sum i i
[PROOF STEP]
assume "j \<in> {..<n} - {i}"
[PROOF STATE]
proof (state)
this:
j \<in> {..<n} - {i}

goal (2 subgoals):
 1. \<And>x. x \<in> {..<n} - {i} \<Longrightarrow> Sum $$ (x, i) * cofactor Sum x i = 0
 2. Sum $$ (i, i) * cofactor Sum i i + 0 = Sum $$ (i, i) * cofactor Sum i i
[PROOF STEP]
hence j: "j < n" and ji: "j \<noteq> i"
[PROOF STATE]
proof (prove)
using this:
j \<in> {..<n} - {i}

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

goal (2 subgoals):
 1. \<And>x. x \<in> {..<n} - {i} \<Longrightarrow> Sum $$ (x, i) * cofactor Sum x i = 0
 2. Sum $$ (i, i) * cofactor Sum i i + 0 = Sum $$ (i, i) * cofactor Sum i i
[PROOF STEP]
show "?f j = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum $$ (j, i) * cofactor Sum j i = 0
[PROOF STEP]
unfolding Sum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (j, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) j i = 0
[PROOF STEP]
using ji j i A 0[OF j]
[PROOF STATE]
proof (prove)
using this:
j \<noteq> i
j < n
i < n
A \<in> carrier_mat n n
A $$ (j, i) = (0::'a)

goal (1 subgoal):
 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (j, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) j i = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Sum $$ (j, i) * cofactor Sum j i = 0

goal (1 subgoal):
 1. Sum $$ (i, i) * cofactor Sum i i + 0 = Sum $$ (i, i) * cofactor Sum i i
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
Sum $$ (i, i) * cofactor Sum i i + (\<Sum>j\<in>{..<n} - {i}. Sum $$ (j, i) * cofactor Sum j i) = Sum $$ (i, i) * cofactor Sum i i

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sum $$ (i, i) * cofactor Sum i i + (\<Sum>j\<in>{..<n} - {i}. Sum $$ (j, i) * cofactor Sum j i) = Sum $$ (i, i) * cofactor Sum i i

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have "?f i = [:0, 1:] * (cofactor Sum i i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sum $$ (i, i) * cofactor Sum i i = [:0::'a, 1::'a:] * cofactor Sum i i
[PROOF STEP]
unfolding Sum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i = [:0::'a, 1::'a:] * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i
[PROOF STEP]
using i A 0[OF i]
[PROOF STATE]
proof (prove)
using this:
i < n
A \<in> carrier_mat n n
A $$ (i, i) = (0::'a)

goal (1 subgoal):
 1. ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) $$ (i, i) * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i = [:0::'a, 1::'a:] * cofactor ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Sum $$ (i, i) * cofactor Sum i i = [:0::'a, 1::'a:] * cofactor Sum i i

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Sum $$ (i, i) * cofactor Sum i i = [:0::'a, 1::'a:] * cofactor Sum i i

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have "cofactor Sum i i = det (mat_delete Sum i i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cofactor Sum i i = det (mat_delete Sum i i)
[PROOF STEP]
unfolding cofactor_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- 1) ^ (i + i) * det (mat_delete Sum i i) = det (mat_delete Sum i i)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cofactor Sum i i = det (mat_delete Sum i i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cofactor Sum i i = det (mat_delete Sum i i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have "\<dots> = char_poly ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_delete Sum i i) = char_poly (mat_delete A i i)
[PROOF STEP]
unfolding char_poly_def char_poly_matrix_def Sum_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. det (mat_delete ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i) = det ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat_delete A i i)) + map_mat (\<lambda>a. [:- a:]) (mat_delete A i i))
[PROOF STEP]
proof (rule arg_cong[of _ _ det])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_delete ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat_delete A i i)) + map_mat (\<lambda>a. [:- a:]) (mat_delete A i i)
[PROOF STEP]
show "mat_delete ?sum i i = [:0, 1:] \<cdot>\<^sub>m 1\<^sub>m (dim_row ?A) + map_mat (\<lambda>a. [:- a:]) ?A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_delete ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat_delete A i i)) + map_mat (\<lambda>a. [:- a:]) (mat_delete A i i)
[PROOF STEP]
using i A
[PROOF STATE]
proof (prove)
using this:
i < n
A \<in> carrier_mat n n

goal (1 subgoal):
 1. mat_delete ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat_delete A i i)) + map_mat (\<lambda>a. [:- a:]) (mat_delete A i i)
[PROOF STEP]
by (auto simp: mat_delete_def)
[PROOF STATE]
proof (state)
this:
mat_delete ([:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m n + map_mat (\<lambda>a. [:- a:]) A) i i = [:0::'a, 1::'a:] \<cdot>\<^sub>m 1\<^sub>m (dim_row (mat_delete A i i)) + map_mat (\<lambda>a. [:- a:]) (mat_delete A i i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
det (mat_delete Sum i i) = char_poly (mat_delete A i i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
det (mat_delete Sum i i) = char_poly (mat_delete A i i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
have "[:0, 1:] = (monom 1 1 :: 'a poly)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [:0::'a, 1::'a:] = monom (1::'a) 1
[PROOF STEP]
by (rule x_as_monom)
[PROOF STATE]
proof (state)
this:
[:0::'a, 1::'a:] = monom (1::'a) 1

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)

goal (1 subgoal):
 1. char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
char_poly A = monom (1::'a) 1 * char_poly (mat_delete A i i)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mat_erase_carrier[simp]: "(mat_erase A i j) \<in> carrier_mat nr nc \<longleftrightarrow> A \<in> carrier_mat nr nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_erase A i j \<in> carrier_mat nr nc) = (A \<in> carrier_mat nr nc)
[PROOF STEP]
unfolding mat_erase_def carrier_mat_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat (dim_row A) (dim_col A) (\<lambda>(i', j'). if i' = i \<or> j' = j then 0::'a else A $$ (i', j')) \<in> {m. dim_row m = nr \<and> dim_col m = nc}) = (A \<in> {m. dim_row m = nr \<and> dim_col m = nc})
[PROOF STEP]
by simp


[STATEMENT]
lemma pderiv_char_poly_mat_erase: fixes A :: "'a :: idom mat"
  assumes A: "A \<in> carrier_mat n n"
  shows "monom 1 1 * pderiv (char_poly A) = (\<Sum>i < n. char_poly (mat_erase A i i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom (1::'a) 1 * pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_erase A i i))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. monom (1::'a) 1 * pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_erase A i i))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom (1::'a) 1 * pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_erase A i i))
[PROOF STEP]
unfolding pderiv_char_poly[OF A] sum_distrib_left
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>n<n. monom (1::'a) 1 * char_poly (mat_delete A n n)) = (\<Sum>i<n. char_poly (mat_erase A i i))
[PROOF STEP]
proof (rule sum.cong[OF refl])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> monom (1::'a) 1 * char_poly (mat_delete A x x) = char_poly (mat_erase A x x)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> monom (1::'a) 1 * char_poly (mat_delete A x x) = char_poly (mat_erase A x x)
[PROOF STEP]
assume "i \<in> {..<n}"
[PROOF STATE]
proof (state)
this:
i \<in> {..<n}

goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> monom (1::'a) 1 * char_poly (mat_delete A x x) = char_poly (mat_erase A x x)
[PROOF STEP]
hence i: "i < n"
[PROOF STATE]
proof (prove)
using this:
i \<in> {..<n}

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

goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> monom (1::'a) 1 * char_poly (mat_delete A x x) = char_poly (mat_erase A x x)
[PROOF STEP]
have mA: "mat_erase A i i \<in> carrier_mat n n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_erase A i i \<in> carrier_mat n n
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat n n

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

goal (1 subgoal):
 1. \<And>x. x \<in> {..<n} \<Longrightarrow> monom (1::'a) 1 * char_poly (mat_delete A x x) = char_poly (mat_erase A x x)
[PROOF STEP]
show "monom 1 1 * char_poly (mat_delete A i i) = char_poly (mat_erase A i i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monom (1::'a) 1 * char_poly (mat_delete A i i) = char_poly (mat_erase A i i)
[PROOF STEP]
by (subst char_poly_0_column[OF _ mA i], (insert i A, force simp: mat_erase_def),
      rule arg_cong[of _ _ "\<lambda> x. f * char_poly x" for f],
      auto simp: mat_delete_def mat_erase_def)
[PROOF STATE]
proof (state)
this:
monom (1::'a) 1 * char_poly (mat_delete A i i) = char_poly (mat_erase A i i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
monom (1::'a) 1 * pderiv (char_poly A) = (\<Sum>i<n. char_poly (mat_erase A i i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Quantity_eq_intro:
  assumes "mag x = mag y" "dim x = dim y" "more x = more y"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (simp add: assms eq_unit)


[STATEMENT]
lemma mag_times  [simp]: "mag (x \<cdot> y) = mag x \<cdot> mag y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mag (x \<cdot> y) = mag x \<cdot> mag y
[PROOF STEP]
by (simp add: times_Quantity_ext_def)


[STATEMENT]
lemma dim_times  [simp]: "dim (x \<cdot> y) = dim x \<cdot> dim y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quantity.dim (x \<cdot> y) = Quantity.dim x \<cdot> Quantity.dim y
[PROOF STEP]
by (simp add: times_Quantity_ext_def)


[STATEMENT]
lemma more_times [simp]: "more (x \<cdot> y) = more x \<cdot> more y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. more (x \<cdot> y) = more x \<cdot> more y
[PROOF STEP]
by (simp add: times_Quantity_ext_def)


[STATEMENT]
lemma mag_zero  [simp]:  "mag 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mag 0 = (0::'a)
[PROOF STEP]
by (simp add: zero_Quantity_ext_def)


[STATEMENT]
lemma dim_zero  [simp]:  "dim 0 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quantity.dim 0 = 1
[PROOF STEP]
by (simp add: zero_Quantity_ext_def)


[STATEMENT]
lemma more_zero [simp]: "more 0 = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. more 0 = (0::'a)
[PROOF STEP]
by (simp add: zero_Quantity_ext_def)


[STATEMENT]
lemma mag_one  [simp]: "mag 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mag 1 = (1::'a)
[PROOF STEP]
by (simp add: one_Quantity_ext_def)


[STATEMENT]
lemma dim_one  [simp]: "dim 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quantity.dim 1 = 1
[PROOF STEP]
by (simp add: one_Quantity_ext_def)


[STATEMENT]
lemma more_one [simp]: "more 1 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. more 1 = (1::'a)
[PROOF STEP]
by (simp add: one_Quantity_ext_def)


[STATEMENT]
lemma mag_inverse [simp]: "mag (inverse x) = inverse (mag x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mag (inverse x) = inverse (mag x)
[PROOF STEP]
by (simp add: inverse_Quantity_ext_def)


[STATEMENT]
lemma dim_inverse [simp]: "dim (inverse x) = inverse (dim x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quantity.dim (inverse x) = inverse (Quantity.dim x)
[PROOF STEP]
by (simp add: inverse_Quantity_ext_def)


[STATEMENT]
lemma more_inverse [simp]: "more (inverse x) = inverse (more x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. more (inverse x) = inverse (more x)
[PROOF STEP]
by (simp add: inverse_Quantity_ext_def)


[STATEMENT]
lemma mag_divide [simp]: "mag (x / y) = mag x / mag y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mag (x / y) = mag x / mag y
[PROOF STEP]
by (simp add: divide_Quantity_ext_def)


[STATEMENT]
lemma dim_divide [simp]: "dim (x / y) = dim x / dim y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Quantity.dim (x / y) = Quantity.dim x / Quantity.dim y
[PROOF STEP]
by (simp add: divide_Quantity_ext_def)


[STATEMENT]
lemma more_divide [simp]: "more (x / y) = more x / more y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. more (x / y) = more x / more y
[PROOF STEP]
by (simp add: divide_Quantity_ext_def)


[STATEMENT]
lemma unit_system_intro: "(UNIV::'s set) = {a} \<Longrightarrow> OFCLASS('s, unit_system_class)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. UNIV = {a} \<Longrightarrow> OFCLASS('s, unit_system_class)
[PROOF STEP]
by (simp add: unit_system_class_def, rule unitary_intro)


[STATEMENT]
lemma mmore [simp]: "mmore \<lparr> unit_sys = x, \<dots> = y \<rparr> = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mmore \<lparr>unit_sys = x, \<dots> = y\<rparr> = y
[PROOF STEP]
by (metis Measurement_System.ext_inject Measurement_System.ext_surjective comp_id mmore_def)


[STATEMENT]
lemma mmore_ext [simp]: "\<lparr>unit_sys = unit, \<dots> = mmore a\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lparr>unit_sys = unit, \<dots> = mmore a\<rparr> = a
[PROOF STEP]
apply (case_tac a, rename_tac b, case_tac b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba. \<lbrakk>a = Abs_Measurement_System_ext b; b \<in> UNIV; b = (aa, ba)\<rbrakk> \<Longrightarrow> \<lparr>unit_sys = unit, \<dots> = mmore a\<rparr> = a
[PROOF STEP]
apply (simp add: Measurement_System_ext_def mmore_def Measurement_System_ext_Tuple_Iso_def Record.iso_tuple_snd_def Record.iso_tuple_cons_def Abs_Measurement_System_ext_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>b aa ba. \<lbrakk>a = Abs_Measurement_System_ext (aa, ba); b = (aa, ba)\<rbrakk> \<Longrightarrow> Abs_Measurement_System_ext (unit, ba) = Abs_Measurement_System_ext (aa, ba)
[PROOF STEP]
apply (rename_tac x y z)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>a = Abs_Measurement_System_ext (y, z); x = (y, z)\<rbrakk> \<Longrightarrow> Abs_Measurement_System_ext (unit, z) = Abs_Measurement_System_ext (y, z)
[PROOF STEP]
apply (subgoal_tac "unit = y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x y z. \<lbrakk>a = Abs_Measurement_System_ext (y, z); x = (y, z); unit = y\<rbrakk> \<Longrightarrow> Abs_Measurement_System_ext (unit, z) = Abs_Measurement_System_ext (y, z)
 2. \<And>x y z. \<lbrakk>a = Abs_Measurement_System_ext (y, z); x = (y, z)\<rbrakk> \<Longrightarrow> unit = y
[PROOF STEP]
apply (simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>a = Abs_Measurement_System_ext (y, z); x = (y, z)\<rbrakk> \<Longrightarrow> unit = y
[PROOF STEP]
apply (simp add: eq_unit)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma Measurement_System_eq_intro:
  assumes "mag x = mag y" "dim x = dim y" "more x = more y"
  shows "x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (rule Quantity_eq_intro, simp_all add: assms)
     (metis Measurement_System.surjective Quantity.select_convs(3) assms(3) mmore mmore_ext)


[STATEMENT]
lemma qequiv_refl [simp]: "a \<cong>\<^sub>Q a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cong>\<^sub>Q a
[PROOF STEP]
by (simp add: qequiv_def)


[STATEMENT]
lemma qequiv_sym: "a \<cong>\<^sub>Q b \<Longrightarrow> b \<cong>\<^sub>Q a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<cong>\<^sub>Q b \<Longrightarrow> b \<cong>\<^sub>Q a
[PROOF STEP]
by (simp add: qequiv_def)


[STATEMENT]
lemma qequiv_trans: "\<lbrakk> a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c \<rbrakk> \<Longrightarrow> a \<cong>\<^sub>Q c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<cong>\<^sub>Q b; b \<cong>\<^sub>Q c\<rbrakk> \<Longrightarrow> a \<cong>\<^sub>Q c
[PROOF STEP]
by (simp add: qequiv_def)


[STATEMENT]
theorem qeq_iff_same_dim:
  fixes x y :: "'a['d::dim_type, 's::unit_system]"
  shows "x \<cong>\<^sub>Q y \<longleftrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<cong>\<^sub>Q y) = (x = y)
[PROOF STEP]
by (transfer, simp)


[STATEMENT]
lemma coerceQuant_eq_iff:
  fixes x :: "'a['d\<^sub>1::dim_type, 's::unit_system]"
  assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)"
  shows "(coerceQuantT TYPE('d\<^sub>2) x) \<cong>\<^sub>Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. QCOERCE['d\<^sub>2] x \<cong>\<^sub>Q x
[PROOF STEP]
by (metis qequiv.rep_eq assms coerceQuantT_def toQ_cases toQ_inverse)


[STATEMENT]
lemma coerceQuant_eq_iff2:
  fixes x :: "'a['d\<^sub>1::dim_type, 's::unit_system]"
  assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" and "y = (coerceQuantT TYPE('d\<^sub>2) x)"
  shows "x \<cong>\<^sub>Q y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cong>\<^sub>Q y
[PROOF STEP]
using qequiv_sym assms(1) assms(2) coerceQuant_eq_iff
[PROOF STATE]
proof (prove)
using this:
?a \<cong>\<^sub>Q ?b \<Longrightarrow> ?b \<cong>\<^sub>Q ?a
QD('d\<^sub>1) = QD('d\<^sub>2)
y = QCOERCE['d\<^sub>2] x
QD(?'d\<^sub>1) = QD(?'d\<^sub>2) \<Longrightarrow> QCOERCE[?'d\<^sub>2] ?x \<cong>\<^sub>Q ?x

goal (1 subgoal):
 1. x \<cong>\<^sub>Q y
[PROOF STEP]
by blast


[STATEMENT]
lemma updown_eq_iff:
  fixes x :: "'a['d\<^sub>1::dim_type, 's::unit_system]" fixes y :: "'a['d\<^sub>2::dim_type, 's]"
  assumes "QD('d\<^sub>1) = QD('d\<^sub>2::dim_type)" and "y = (toQ (fromQ x))"
  shows "x \<cong>\<^sub>Q y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cong>\<^sub>Q y
[PROOF STEP]
by (simp add: assms(1) assms(2) coerceQuant_eq_iff2 coerceQuantT_def)


[STATEMENT]
lemma qeq:
  fixes x :: "'a['d\<^sub>1::dim_type, 's::unit_system]" fixes y :: "'a['d\<^sub>2::dim_type, 's]"
  assumes "x \<cong>\<^sub>Q y"
  shows "QD('d\<^sub>1) = QD('d\<^sub>2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. QD('d\<^sub>1) = QD('d\<^sub>2)
[PROOF STEP]
by (metis (full_types) qequiv.rep_eq assms fromQ mem_Collect_eq)


[STATEMENT]
lemma entails_iff_unsatisfiable_single:
  "CC \<TTurnstile>e {E} \<longleftrightarrow> \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})" (is "_ \<longleftrightarrow> _ (_ \<union> ?NegD)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (CC \<TTurnstile>e {E}) = (\<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. CC \<TTurnstile>e {E} \<Longrightarrow> \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})
 2. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}) \<Longrightarrow> CC \<TTurnstile>e {E}
[PROOF STEP]
assume c_ent_e: "CC \<TTurnstile>e {E}"
[PROOF STATE]
proof (state)
this:
CC \<TTurnstile>e {E}

goal (2 subgoals):
 1. CC \<TTurnstile>e {E} \<Longrightarrow> \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})
 2. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}) \<Longrightarrow> CC \<TTurnstile>e {E}
[PROOF STEP]
have "\<not> I \<TTurnstile>s CC \<union> ?NegD" for I
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}
[PROOF STEP]
using c_ent_e[rule_format, of I]
[PROOF STATE]
proof (prove)
using this:
I \<TTurnstile>s CC \<Longrightarrow> I \<TTurnstile>s {E}

goal (1 subgoal):
 1. \<not> I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}
[PROOF STEP]
unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj
[PROOF STATE]
proof (prove)
using this:
\<forall>C\<in>CC. \<exists>L\<in>#C. (is_pos L \<longrightarrow> atm_of L \<in> I) \<and> (is_neg L \<longrightarrow> atm_of L \<notin> I) \<Longrightarrow> \<forall>C\<in>{E}. \<exists>L\<in>#C. (is_pos L \<longrightarrow> atm_of L \<in> I) \<and> (is_neg L \<longrightarrow> atm_of L \<notin> I)

goal (1 subgoal):
 1. \<not> (\<forall>C\<in>CC \<union> {{#- L#} |L. L \<in># E}. \<exists>L\<in>#C. (is_pos L \<longrightarrow> atm_of L \<in> I) \<and> (is_neg L \<longrightarrow> atm_of L \<notin> I))
[PROOF STEP]
by (fastforce simp: ball_Un is_pos_neg_not_is_pos)
[PROOF STATE]
proof (state)
this:
\<not> ?I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}

goal (2 subgoals):
 1. CC \<TTurnstile>e {E} \<Longrightarrow> \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})
 2. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}) \<Longrightarrow> CC \<TTurnstile>e {E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> ?I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}
[PROOF STEP]
show "\<not> satisfiable (CC \<union> ?NegD)"
[PROOF STATE]
proof (prove)
using this:
\<not> ?I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}

goal (1 subgoal):
 1. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})

goal (1 subgoal):
 1. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}) \<Longrightarrow> CC \<TTurnstile>e {E}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}) \<Longrightarrow> CC \<TTurnstile>e {E}
[PROOF STEP]
assume "\<not> satisfiable (CC \<union> ?NegD)"
[PROOF STATE]
proof (state)
this:
\<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})

goal (1 subgoal):
 1. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}) \<Longrightarrow> CC \<TTurnstile>e {E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})
[PROOF STEP]
have "\<not> I \<TTurnstile>s CC \<union> ?NegD" for I
[PROOF STATE]
proof (prove)
using this:
\<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})

goal (1 subgoal):
 1. \<not> I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> ?I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}

goal (1 subgoal):
 1. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}) \<Longrightarrow> CC \<TTurnstile>e {E}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> ?I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}
[PROOF STEP]
show "CC \<TTurnstile>e {E}"
[PROOF STATE]
proof (prove)
using this:
\<not> ?I \<TTurnstile>s CC \<union> {{#- L#} |L. L \<in># E}

goal (1 subgoal):
 1. CC \<TTurnstile>e {E}
[PROOF STEP]
unfolding true_clss_def true_cls_def true_lit_def if_distribR if_bool_eq_conj
[PROOF STATE]
proof (prove)
using this:
\<not> (\<forall>C\<in>CC \<union> {{#- L#} |L. L \<in># E}. \<exists>L\<in>#C. (is_pos L \<longrightarrow> atm_of L \<in> ?I) \<and> (is_neg L \<longrightarrow> atm_of L \<notin> ?I))

goal (1 subgoal):
 1. \<forall>I. (\<forall>C\<in>CC. \<exists>L\<in>#C. (is_pos L \<longrightarrow> atm_of L \<in> I) \<and> (is_neg L \<longrightarrow> atm_of L \<notin> I)) \<longrightarrow> (\<forall>C\<in>{E}. \<exists>L\<in>#C. (is_pos L \<longrightarrow> atm_of L \<in> I) \<and> (is_neg L \<longrightarrow> atm_of L \<notin> I))
[PROOF STEP]
by (fastforce simp: ball_Un is_pos_neg_not_is_pos)
[PROOF STATE]
proof (state)
this:
CC \<TTurnstile>e {E}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma entails_iff_unsatisfiable:
  "CC \<TTurnstile>e EE \<longleftrightarrow> (\<forall>E \<in> EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
have "?lhs \<longleftrightarrow> (\<forall>E \<in> EE. CC \<TTurnstile>e {E})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. CC \<TTurnstile>e {E})
[PROOF STEP]
unfolding true_clss_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>I. Ball CC ((\<TTurnstile>) I) \<longrightarrow> Ball EE ((\<TTurnstile>) I)) = (\<forall>E\<in>EE. \<forall>I. Ball CC ((\<TTurnstile>) I) \<longrightarrow> Ball {E} ((\<TTurnstile>) I))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. CC \<TTurnstile>e {E})

goal (1 subgoal):
 1. (CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. CC \<TTurnstile>e {E})

goal (1 subgoal):
 1. (CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
have "... \<longleftrightarrow> ?rhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>E\<in>EE. CC \<TTurnstile>e {E}) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
unfolding entails_iff_unsatisfiable_single
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E})) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>E\<in>EE. CC \<TTurnstile>e {E}) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))

goal (1 subgoal):
 1. (CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))

goal (1 subgoal):
 1. (CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(CC \<TTurnstile>e EE) = (\<forall>E\<in>EE. \<not> satisfiable (CC \<union> {{#- L#} |L. L \<in># E}))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma true_clss_of_interp_iff_equal[simp]: "J \<TTurnstile>s clss_of_interp I \<longleftrightarrow> J = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (J \<TTurnstile>s clss_of_interp I) = (J = I)
[PROOF STEP]
unfolding clss_of_interp_def true_clss_def true_cls_def true_lit_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>C\<in>{{#(if A \<in> I then Pos else Neg) A#} |A. True}. \<exists>L\<in>#C. (if is_pos L then \<lambda>P. P else Not) (atm_of L \<in> J)) = (J = I)
[PROOF STEP]
by force


[STATEMENT]
lemma entails_iff_models[simp]: "clss_of_interp I \<TTurnstile>e CC \<longleftrightarrow> I \<TTurnstile>s CC"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (clss_of_interp I \<TTurnstile>e CC) = (I \<TTurnstile>s CC)
[PROOF STEP]
by simp


[STATEMENT]
lemma Inf_counterex_reducing:
  assumes
    bot_ni_n: "N \<inter> {{#}} = {}" and
    d_in_n: "D \<in> N" and
    n_ent_d: "\<not> I_of N \<TTurnstile>e {D}" and
    d_min: "\<And>C. C \<in> N \<Longrightarrow> \<not> I_of N \<TTurnstile>e {C} \<Longrightarrow> D \<le> C"
  shows "\<exists>\<iota> \<in> Inf. prems_of \<iota> \<noteq> [] \<and> main_prem_of \<iota> = D \<and> set (side_prems_of \<iota>) \<subseteq> N
    \<and> I_of N \<TTurnstile>e set (side_prems_of \<iota>) \<and> \<not> I_of N \<TTurnstile>e {concl_of \<iota>} \<and> concl_of \<iota> < D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<iota>\<in>Inf. inference.prems_of \<iota> \<noteq> [] \<and> Standard_Redundancy_Criterion.main_prem_of \<iota> = D \<and> set (Standard_Redundancy_Criterion.side_prems_of \<iota>) \<subseteq> N \<and> I_of N \<TTurnstile>e set (Standard_Redundancy_Criterion.side_prems_of \<iota>) \<and> \<not> I_of N \<TTurnstile>e {Calculus.inference.concl_of \<iota>} \<and> Calculus.inference.concl_of \<iota> < D
[PROOF STEP]
using bot_ni_n clausal_Inf_counterex_reducing d_in_n d_min n_ent_d
[PROOF STATE]
proof (prove)
using this:
N \<inter> {{#}} = {}
\<lbrakk>{#} \<notin> ?N; ?D \<in> ?N; \<not> J_of ?N \<TTurnstile> ?D; \<And>C. \<lbrakk>C \<in> ?N; \<not> J_of ?N \<TTurnstile> C\<rbrakk> \<Longrightarrow> ?D \<le> C\<rbrakk> \<Longrightarrow> \<exists>\<iota>\<in>Inf. inference.prems_of \<iota> \<noteq> [] \<and> Standard_Redundancy_Criterion.main_prem_of \<iota> = ?D \<and> set (Standard_Redundancy_Criterion.side_prems_of \<iota>) \<subseteq> ?N \<and> J_of ?N \<TTurnstile>s set (Standard_Redundancy_Criterion.side_prems_of \<iota>) \<and> \<not> J_of ?N \<TTurnstile> Calculus.inference.concl_of \<iota> \<and> Calculus.inference.concl_of \<iota> < ?D
D \<in> N
\<lbrakk>?C \<in> N; \<not> I_of N \<TTurnstile>e {?C}\<rbrakk> \<Longrightarrow> D \<le> ?C
\<not> I_of N \<TTurnstile>e {D}

goal (1 subgoal):
 1. \<exists>\<iota>\<in>Inf. inference.prems_of \<iota> \<noteq> [] \<and> Standard_Redundancy_Criterion.main_prem_of \<iota> = D \<and> set (Standard_Redundancy_Criterion.side_prems_of \<iota>) \<subseteq> N \<and> I_of N \<TTurnstile>e set (Standard_Redundancy_Criterion.side_prems_of \<iota>) \<and> \<not> I_of N \<TTurnstile>e {Calculus.inference.concl_of \<iota>} \<and> Calculus.inference.concl_of \<iota> < D
[PROOF STEP]
by auto


[STATEMENT]
lemma clausal_saturated_model: "saturated N \<Longrightarrow> {#} \<notin> N \<Longrightarrow> J_of N \<TTurnstile>s N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>saturated N; {#} \<notin> N\<rbrakk> \<Longrightarrow> J_of N \<TTurnstile>s N
[PROOF STEP]
by (simp add: saturated_model[simplified])


[STATEMENT]
lemma [code abstract]: "vec_nth (list_to_vec xs) = (%i. xs ! (to_nat i))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (list_to_vec xs) = (\<lambda>i. xs ! mod_type_class.to_nat i)
[PROOF STEP]
unfolding list_to_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>i. xs ! mod_type_class.to_nat i) = (\<lambda>i. xs ! mod_type_class.to_nat i)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma [code abstract]: "vec_nth (list_of_list_to_matrix xs) = (%i. list_to_vec (xs ! (to_nat i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (list_of_list_to_matrix xs) = (\<lambda>i. list_to_vec (xs ! mod_type_class.to_nat i))
[PROOF STEP]
unfolding list_of_list_to_matrix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ($) (\<chi>i. list_to_vec (xs ! mod_type_class.to_nat i)) = (\<lambda>i. list_to_vec (xs ! mod_type_class.to_nat i))
[PROOF STEP]
by auto


[STATEMENT]
lemma [code_post]:
  "int_of_integer (- 1) = - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. int_of_integer (- 1) = - 1
[PROOF STEP]
by simp


[STATEMENT]
lemma [code_abbrev]:
 "(of_rat (- 1) :: real) = - 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat (- 1) = - 1
[PROOF STEP]
by simp


[STATEMENT]
lemma [code_post]:
 "(of_rat (- (1 / numeral k)) :: real) = - 1 / numeral k"
 "(of_rat (- (numeral k / numeral l)) :: real) = - numeral k / numeral l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real_of_rat (- (1 / numeral k)) = - 1 / numeral k &&& real_of_rat (- (numeral k / numeral l)) = - numeral k / numeral l
[PROOF STEP]
by (simp_all add: of_rat_divide of_rat_minus)


[STATEMENT]
lemma less_vecD: assumes "v <\<^sub>v w" and "w \<in> carrier_vec n"
  shows "i < n \<Longrightarrow> v $ i < w $ i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < n \<Longrightarrow> v $ i < w $ i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v <\<^sub>v w
w \<in> carrier_vec n

goal (1 subgoal):
 1. i < n \<Longrightarrow> v $ i < w $ i
[PROOF STEP]
unfolding less_vec_def
[PROOF STATE]
proof (prove)
using this:
dim_vec v = dim_vec w \<and> (\<forall>i<dim_vec w. v $ i < w $ i)
w \<in> carrier_vec n

goal (1 subgoal):
 1. i < n \<Longrightarrow> v $ i < w $ i
[PROOF STEP]
by auto


[STATEMENT]
lemma less_vecI: assumes "v \<in> carrier_vec n" "w \<in> carrier_vec n"
  "\<And> i. i < n \<Longrightarrow> v $ i < w $ i"
shows "v <\<^sub>v w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v <\<^sub>v w
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
w \<in> carrier_vec n
?i < n \<Longrightarrow> v $ ?i < w $ ?i

goal (1 subgoal):
 1. v <\<^sub>v w
[PROOF STEP]
unfolding less_vec_def
[PROOF STATE]
proof (prove)
using this:
v \<in> carrier_vec n
w \<in> carrier_vec n
?i < n \<Longrightarrow> v $ ?i < w $ ?i

goal (1 subgoal):
 1. dim_vec v = dim_vec w \<and> (\<forall>i<dim_vec w. v $ i < w $ i)
[PROOF STEP]
by auto


[STATEMENT]
lemma less_vec_lesseq_vec: "v <\<^sub>v (w :: 'a :: preorder vec) \<Longrightarrow> v \<le> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v <\<^sub>v w \<Longrightarrow> v \<le> w
[PROOF STEP]
unfolding less_vec_def less_eq_vec_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_vec v = dim_vec w \<and> (\<forall>i<dim_vec w. v $ i < w $ i) \<Longrightarrow> dim_vec v = dim_vec w \<and> (\<forall>i<dim_vec w. v $ i \<le> w $ i)
[PROOF STEP]
by (auto simp: less_le_not_le)


[STATEMENT]
lemma floor_of_int_eq[simp]: "x \<in> \<int> \<Longrightarrow> of_int \<lfloor>x\<rfloor> = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> \<int> \<Longrightarrow> of_int \<lfloor>x\<rfloor> = x
[PROOF STEP]
by (metis Ints_cases of_int_floor_cancel)