[STATEMENT]
lemma farkas_lemma_matrix: fixes A :: "rat mat"
  assumes A: "A \<in> carrier_mat nr nc"
  and b: "b \<in> carrier_vec nr"
shows "(\<exists> x \<in> carrier_vec nc. A *\<^sub>v x \<le> b) \<longleftrightarrow>
  (\<forall> y. y \<ge> 0\<^sub>v nr \<longrightarrow> mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> y \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
define cs where "cs = constraints_of_mat_vec A b"
[PROOF STATE]
proof (state)
this:
cs = constraints_of_mat_vec A b

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have fin: "finite {0 ..< nr}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {0..<nr}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {0..<nr}

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have dim: "dim_row A = nr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dim_row A = nr
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

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

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have sum_id: "(\<Sum> i = 0..<nr. f i) = sum_list (map f [0..<nr])" for f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum f {0..<nr} = sum_list (map f [0..<nr])
[PROOF STEP]
by (subst sum_list_distinct_conv_sum_set, auto)
[PROOF STATE]
proof (state)
this:
sum ?f1 {0..<nr} = sum_list (map ?f1 [0..<nr])

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "(\<exists> x \<in> carrier_vec nc. A *\<^sub>v x \<le> b) =
   (\<not> (\<nexists> v. \<forall> c \<in> cs. v \<Turnstile>\<^sub>l\<^sub>e c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<not> (\<nexists>v. \<forall>c\<in>cs. v \<Turnstile>\<^sub>l\<^sub>e c))
[PROOF STEP]
unfolding constraints_of_mat_vec_solution[OF assms] cs_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>v. Ball (constraints_of_mat_vec A b) ((\<Turnstile>\<^sub>l\<^sub>e) v)) = (\<not> (\<nexists>v. \<forall>c\<in>constraints_of_mat_vec A b. v \<Turnstile>\<^sub>l\<^sub>e c))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<not> (\<nexists>v. \<forall>c\<in>cs. v \<Turnstile>\<^sub>l\<^sub>e c))

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<not> (\<nexists>v. \<forall>c\<in>cs. v \<Turnstile>\<^sub>l\<^sub>e c))

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (\<nexists>v. \<forall>c\<in>cs. v \<Turnstile>\<^sub>l\<^sub>e c)) = (\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)))
[PROOF STEP]
unfolding cs_def constraints_of_mat_vec_def dim
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (\<nexists>v. \<forall>c\<in>(\<lambda>i. Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)) ` {0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e c)) = (\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<not> (\<nexists>v. \<forall>c\<in>cs. v \<Turnstile>\<^sub>l\<^sub>e c)) = (\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)))

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<not> (\<nexists>v. \<forall>c\<in>cs. v \<Turnstile>\<^sub>l\<^sub>e c)) = (\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i)))

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<nexists>C.
        (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and>
         (\<Sum>i = 0..<nr. (C i *R poly_of_vec (row A i))) = 0 \<and>
         (\<Sum>i = 0..<nr. (C i * b $ i)) < 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i))) = (\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0)
[PROOF STEP]
unfolding Farkas'_Lemma_indexed[OF
        lec_rec_constraints_of_mat_vec[unfolded constraints_of_mat_vec_def], of A b,
        unfolded dim, OF fin] sum_id sum_list_lec le_constraint.simps
        sum_list_Leq_Rel map_map o_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nexists>C const. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> ((\<forall>x\<in>set [0..<nr]. lec_rel (Le_Constraint Leq_Rel (C x *R lec_poly (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))) (C x *R lec_const (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x)))) = Leq_Rel) \<and> (\<Sum>x\<leftarrow>[0..<nr]. lec_poly (Le_Constraint Leq_Rel (C x *R lec_poly (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))) (C x *R lec_const (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))))) = 0 \<and> (\<Sum>x\<leftarrow>[0..<nr]. lec_const (Le_Constraint Leq_Rel (C x *R lec_poly (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))) (C x *R lec_const (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))))) = const) \<and> const < 0) = (\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i\<leftarrow>[0..<nr]. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i\<leftarrow>[0..<nr]. C i * b $ i) < 0)
[PROOF STEP]
unfolding sum_id[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nexists>C const. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> ((\<forall>x\<in>set [0..<nr]. lec_rel (Le_Constraint Leq_Rel (C x *R lec_poly (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))) (C x *R lec_const (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x)))) = Leq_Rel) \<and> (\<Sum>x = 0..<nr. lec_poly (Le_Constraint Leq_Rel (C x *R lec_poly (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))) (C x *R lec_const (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))))) = 0 \<and> (\<Sum>x = 0..<nr. lec_const (Le_Constraint Leq_Rel (C x *R lec_poly (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))) (C x *R lec_const (Le_Constraint Leq_Rel (poly_of_vec (row A x)) (b $ x))))) = const) \<and> const < 0) = (\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i))) = (\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0)

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<not> (\<nexists>v. \<forall>i\<in>{0..<nr}. v \<Turnstile>\<^sub>l\<^sub>e Le_Constraint Leq_Rel (poly_of_vec (row A i)) (b $ i))) = (\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0)

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall> C. (\<forall>i\<in> {0..<nr}. 0 \<le> C i) \<longrightarrow>
         (\<Sum>i = 0..<nr. (C i *R poly_of_vec (row A i))) = 0 \<longrightarrow>
         (\<Sum>i = 0..<nr. (C i * b $ i)) \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0) = (\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i))
[PROOF STEP]
using not_less
[PROOF STATE]
proof (prove)
using this:
(\<not> ?x < ?y) = (?y \<le> ?x)

goal (1 subgoal):
 1. (\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0) = (\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0) = (\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i))

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<nexists>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<and> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<and> (\<Sum>i = 0..<nr. C i * b $ i) < 0) = (\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i))

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall> y. y \<ge> 0\<^sub>v nr \<longrightarrow> mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> y \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
proof ((standard; intro allI impI), goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i); 0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
case *: (1 y)
[PROOF STATE]
proof (state)
this:
\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
0\<^sub>v nr \<le> y
mat_of_row y * A = 0\<^sub>m 1 nc

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i); 0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
define C where "C = (\<lambda> i. y $ i)"
[PROOF STATE]
proof (state)
this:
C = ($) y

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i); 0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
note main = *(1)[rule_format, of C]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>i. i \<in> {0..<nr} \<Longrightarrow> 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i); 0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
from *(2)
[PROOF STATE]
proof (chain)
picking this:
0\<^sub>v nr \<le> y
[PROOF STEP]
have y: "y \<in> carrier_vec nr" and nonneg: "\<And>i. i \<in> {0..<nr} \<Longrightarrow> 0 \<le> C i"
[PROOF STATE]
proof (prove)
using this:
0\<^sub>v nr \<le> y

goal (1 subgoal):
 1. y \<in> carrier_vec nr &&& (\<And>i. i \<in> {0..<nr} \<Longrightarrow> 0 \<le> C i)
[PROOF STEP]
unfolding less_eq_vec_def C_def
[PROOF STATE]
proof (prove)
using this:
dim_vec (0\<^sub>v nr) = dim_vec y \<and> (\<forall>i<dim_vec y. 0\<^sub>v nr $ i \<le> y $ i)

goal (1 subgoal):
 1. y \<in> carrier_vec nr &&& (\<And>i. i \<in> {0..<nr} \<Longrightarrow> 0 \<le> y $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> carrier_vec nr
?i1 \<in> {0..<nr} \<Longrightarrow> 0 \<le> C ?i1

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i); 0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
have sum_0: "(\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0
[PROOF STEP]
unfolding C_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. y $ i *R poly_of_vec (row A i)) = 0
[PROOF STEP]
unfolding zero_coeff_zero coeff_sum
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
fix v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
have "(\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) =
            (\<Sum>i < nr. y $ i * coeff (poly_of_vec (row A i)) v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v)
[PROOF STEP]
by (rule sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v)

goal (1 subgoal):
 1. \<And>v. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v)

goal (1 subgoal):
 1. \<And>v. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
proof (cases "v < nc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
 2. \<not> v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> v < nc

goal (2 subgoals):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
 2. \<not> v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
have "(\<Sum>i < nr. y $ i * coeff (poly_of_vec (row A i)) v) =
              (\<Sum>i < nr. y $ i * 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * 0)
[PROOF STEP]
by (rule sum.cong[OF refl], rule arg_cong[of _ _ "\<lambda> x. _ * x"], insert A False, transfer, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * 0)

goal (2 subgoals):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
 2. \<not> v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * 0)

goal (2 subgoals):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
 2. \<not> v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * 0) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * 0) = 0

goal (2 subgoals):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
 2. \<not> v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0

goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0

goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
v < nc

goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
have "(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) =
              (\<Sum>i<nr. y $ i * row A i $ v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * row A i $ v)
[PROOF STEP]
by (rule sum.cong[OF refl], rule arg_cong[of _ _ "\<lambda> x. _ * x"], insert A True, transfer, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * row A i $ v)

goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = (\<Sum>i<nr. y $ i * row A i $ v)

goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
have "\<dots> = (mat_of_row y * A) $$ (0,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * row A i $ v) = (mat_of_row y * A) $$ (0, v)
[PROOF STEP]
unfolding times_mat_def scalar_prod_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * row A i $ v) = mat (dim_row (mat_of_row y)) (dim_col A) (\<lambda>(i, j). \<Sum>ia = 0..<dim_vec (col A j). row (mat_of_row y) i $ ia * col A j $ ia) $$ (0, v)
[PROOF STEP]
using A y True
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc
y \<in> carrier_vec nr
v < nc

goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * row A i $ v) = mat (dim_row (mat_of_row y)) (dim_col A) (\<lambda>(i, j). \<Sum>ia = 0..<dim_vec (col A j). row (mat_of_row y) i $ ia * col A j $ ia) $$ (0, v)
[PROOF STEP]
by (auto intro: sum.cong)
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * row A i $ v) = (mat_of_row y * A) $$ (0, v)

goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * row A i $ v) = (mat_of_row y * A) $$ (0, v)

goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
have "\<dots> = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (mat_of_row y * A) $$ (0, v) = 0
[PROOF STEP]
unfolding *(3)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>m 1 nc $$ (0, v) = 0
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
v < nc

goal (1 subgoal):
 1. 0\<^sub>m 1 nc $$ (0, v) = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(mat_of_row y * A) $$ (0, v) = 0

goal (1 subgoal):
 1. v < nc \<Longrightarrow> (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0

goal (1 subgoal):
 1. (\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i<nr. y $ i * coeff (poly_of_vec (row A i)) v) = 0

goal (1 subgoal):
 1. \<And>v. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
show "(\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0

goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<nr. coeff (y $ i *R poly_of_vec (row A i)) v) = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i); 0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
from main[OF nonneg sum_0]
[PROOF STATE]
proof (chain)
picking this:
(\<And>i. i \<in> {0..<nr} \<Longrightarrow> i \<in> {0..<nr}) \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
have le: "0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)"
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i \<in> {0..<nr} \<Longrightarrow> i \<in> {0..<nr}) \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i); 0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)

goal (1 subgoal):
 1. 0 \<le> y \<bullet> b
[PROOF STEP]
using y b
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
y \<in> carrier_vec nr
b \<in> carrier_vec nr

goal (1 subgoal):
 1. 0 \<le> y \<bullet> b
[PROOF STEP]
unfolding scalar_prod_def C_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i = 0..<nr. y $ i * b $ i)
y \<in> carrier_vec nr
b \<in> carrier_vec nr

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i = 0..<dim_vec b. y $ i * b $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> y \<bullet> b

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
case *: (2 C)
[PROOF STATE]
proof (state)
this:
\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b
\<forall>i\<in>{0..<nr}. 0 \<le> C i
(\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
define y where "y = vec nr C"
[PROOF STATE]
proof (state)
this:
y = vec nr C

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
have y: "y \<in> carrier_vec nr"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<in> carrier_vec nr
[PROOF STEP]
unfolding y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vec nr C \<in> carrier_vec nr
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<in> carrier_vec nr

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
note main = *(1)[rule_format, of y]
[PROOF STATE]
proof (state)
this:
\<lbrakk>0\<^sub>v nr \<le> y; mat_of_row y * A = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
from *(2)
[PROOF STATE]
proof (chain)
picking this:
\<forall>i\<in>{0..<nr}. 0 \<le> C i
[PROOF STEP]
have y0: "y \<ge> 0\<^sub>v nr"
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<nr}. 0 \<le> C i

goal (1 subgoal):
 1. 0\<^sub>v nr \<le> y
[PROOF STEP]
unfolding less_eq_vec_def y_def
[PROOF STATE]
proof (prove)
using this:
\<forall>i\<in>{0..<nr}. 0 \<le> C i

goal (1 subgoal):
 1. dim_vec (0\<^sub>v nr) = dim_vec (vec nr C) \<and> (\<forall>i<dim_vec (vec nr C). 0\<^sub>v nr $ i \<le> vec nr C $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0\<^sub>v nr \<le> y

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
have prod0: "mat_of_row y * A = 0\<^sub>m 1 nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
fix j
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
assume j: "j < nc"
[PROOF STATE]
proof (state)
this:
j < nc

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
from arg_cong[OF *(3), of "\<lambda> x. coeff x j", unfolded coeff_sum]
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i = 0..<nr. coeff (C i *R poly_of_vec (row A i)) j) = coeff 0 j
[PROOF STEP]
have "0 = (\<Sum>i = 0..<nr. C i * coeff (poly_of_vec (row A i)) j)"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i = 0..<nr. coeff (C i *R poly_of_vec (row A i)) j) = coeff 0 j

goal (1 subgoal):
 1. 0 = (\<Sum>i = 0..<nr. C i * coeff (poly_of_vec (row A i)) j)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 = (\<Sum>i = 0..<nr. C i * coeff (poly_of_vec (row A i)) j)

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 = (\<Sum>i = 0..<nr. C i * coeff (poly_of_vec (row A i)) j)

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
have "\<dots> = (\<Sum>i = 0..<nr. C i * row A i $ j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. C i * coeff (poly_of_vec (row A i)) j) = (\<Sum>i = 0..<nr. C i * row A i $ j)
[PROOF STEP]
by (rule sum.cong[OF refl], rule arg_cong[of _ _ "\<lambda> x. _ * x"], insert A j, transfer, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<nr. C i * coeff (poly_of_vec (row A i)) j) = (\<Sum>i = 0..<nr. C i * row A i $ j)

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<nr. C i * coeff (poly_of_vec (row A i)) j) = (\<Sum>i = 0..<nr. C i * row A i $ j)

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
have "\<dots> = y \<bullet> col A j"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. C i * row A i $ j) = y \<bullet> col A j
[PROOF STEP]
unfolding scalar_prod_def y_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. C i * row A i $ j) = (\<Sum>i = 0..<dim_vec (col A j). vec nr C $ i * col A j $ i)
[PROOF STEP]
using A j
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc
j < nc

goal (1 subgoal):
 1. (\<Sum>i = 0..<nr. C i * row A i $ j) = (\<Sum>i = 0..<dim_vec (col A j). vec nr C $ i * col A j $ i)
[PROOF STEP]
by (intro sum.cong, auto)
[PROOF STATE]
proof (state)
this:
(\<Sum>i = 0..<nr. C i * row A i $ j) = y \<bullet> col A j

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
0 = y \<bullet> col A j
[PROOF STEP]
have "y \<bullet> col A j = 0"
[PROOF STATE]
proof (prove)
using this:
0 = y \<bullet> col A j

goal (1 subgoal):
 1. y \<bullet> col A j = 0
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
y \<bullet> col A j = 0

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?j3 < nc \<Longrightarrow> y \<bullet> col A ?j3 = 0

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?j3 < nc \<Longrightarrow> y \<bullet> col A ?j3 = 0

goal (1 subgoal):
 1. mat_of_row y * A = 0\<^sub>m 1 nc
[PROOF STEP]
by (intro eq_matI, insert A y, auto)
[PROOF STATE]
proof (state)
this:
mat_of_row y * A = 0\<^sub>m 1 nc

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
mat_of_row y * A = 0\<^sub>m 1 nc

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
from main[OF y0 prod0]
[PROOF STATE]
proof (chain)
picking this:
0 \<le> y \<bullet> b
[PROOF STEP]
have "0 \<le> y \<bullet> b"
[PROOF STATE]
proof (prove)
using this:
0 \<le> y \<bullet> b

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

goal (1 subgoal):
 1. \<And>C. \<lbrakk>\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b; \<forall>i\<in>{0..<nr}. 0 \<le> C i; (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0\<rbrakk> \<Longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
0 \<le> y \<bullet> b

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
unfolding scalar_prod_def y_def
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i = 0..<dim_vec b. vec nr C $ i * b $ i)

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
0 \<le> (\<Sum>i = 0..<dim_vec b. vec nr C $ i * b $ i)
b \<in> carrier_vec nr

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>C. (\<forall>i\<in>{0..<nr}. 0 \<le> C i) \<longrightarrow> (\<Sum>i = 0..<nr. C i *R poly_of_vec (row A i)) = 0 \<longrightarrow> 0 \<le> (\<Sum>i = 0..<nr. C i * b $ i)) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. A *\<^sub>v x \<le> b) = (\<forall>y\<ge>0\<^sub>v nr. mat_of_row y * A = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma farkas_lemma_matrix': fixes A :: "rat mat"
  assumes A: "A \<in> carrier_mat nr nc"
  and b: "b \<in> carrier_vec nr"
shows "(\<exists> x \<ge> 0\<^sub>v nc. A *\<^sub>v x = b) \<longleftrightarrow>
  (\<forall> y \<in> carrier_vec nr. mat_of_row y * A \<ge> 0\<^sub>m 1 nc \<longrightarrow> y \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
define B where "B = (- 1\<^sub>m nc) @\<^sub>r (A @\<^sub>r -A)"
[PROOF STATE]
proof (state)
this:
B = - 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
define b' where "b' = 0\<^sub>v nc @\<^sub>v (b @\<^sub>v -b)"
[PROOF STATE]
proof (state)
this:
b' = 0\<^sub>v nc @\<^sub>v b @\<^sub>v - b

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
define n where "n = nc + (nr + nr)"
[PROOF STATE]
proof (state)
this:
n = nc + (nr + nr)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have id0: "0\<^sub>v (nc + (nr + nr)) = 0\<^sub>v nc @\<^sub>v (0\<^sub>v nr @\<^sub>v 0\<^sub>v nr)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v (nc + (nr + nr)) = 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr
[PROOF STEP]
by (intro eq_vecI, auto)
[PROOF STATE]
proof (state)
this:
0\<^sub>v (nc + (nr + nr)) = 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have B: "B \<in> carrier_mat n nc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B \<in> carrier_mat n nc
[PROOF STEP]
unfolding B_def n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A \<in> carrier_mat (nc + (nr + nr)) nc
[PROOF STEP]
using A
[PROOF STATE]
proof (prove)
using this:
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. - 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A \<in> carrier_mat (nc + (nr + nr)) nc
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
B \<in> carrier_mat n nc

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have b': "b' \<in> carrier_vec n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b' \<in> carrier_vec n
[PROOF STEP]
unfolding b'_def n_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0\<^sub>v nc @\<^sub>v b @\<^sub>v - b \<in> carrier_vec (nc + (nr + nr))
[PROOF STEP]
using b
[PROOF STATE]
proof (prove)
using this:
b \<in> carrier_vec nr

goal (1 subgoal):
 1. 0\<^sub>v nc @\<^sub>v b @\<^sub>v - b \<in> carrier_vec (nc + (nr + nr))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b' \<in> carrier_vec n

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "(\<exists> x \<ge> 0\<^sub>v nc. A *\<^sub>v x = b) = (\<exists> x. x \<in> carrier_vec nc \<and> x \<ge> 0\<^sub>v nc \<and> A *\<^sub>v x = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<exists>x. x \<in> carrier_vec nc \<and> 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b)
[PROOF STEP]
by (rule arg_cong[of _ _ Ex], intro ext, insert A b, auto simp: less_eq_vec_def)
[PROOF STATE]
proof (state)
this:
(\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<exists>x. x \<in> carrier_vec nc \<and> 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<exists>x. x \<in> carrier_vec nc \<and> 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<exists> x \<in> carrier_vec nc. x \<ge> 0\<^sub>v nc \<and> A *\<^sub>v x = b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x. x \<in> carrier_vec nc \<and> 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b) = (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<exists>x. x \<in> carrier_vec nc \<and> 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b) = (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x. x \<in> carrier_vec nc \<and> 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b) = (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<exists> x \<in> carrier_vec nc. 1\<^sub>m nc *\<^sub>v x \<ge> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> A *\<^sub>v x \<ge> b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b) = (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> 1\<^sub>m nc *\<^sub>v x \<and> A *\<^sub>v x \<le> b \<and> b \<le> A *\<^sub>v x)
[PROOF STEP]
by (rule bex_cong[OF refl], insert A b, auto)
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b) = (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> 1\<^sub>m nc *\<^sub>v x \<and> A *\<^sub>v x \<le> b \<and> b \<le> A *\<^sub>v x)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> x \<and> A *\<^sub>v x = b) = (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> 1\<^sub>m nc *\<^sub>v x \<and> A *\<^sub>v x \<le> b \<and> b \<le> A *\<^sub>v x)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<exists> x \<in> carrier_vec nc. (- 1\<^sub>m nc) *\<^sub>v x \<le> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> (- A) *\<^sub>v x \<le> -b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> 1\<^sub>m nc *\<^sub>v x \<and> A *\<^sub>v x \<le> b \<and> b \<le> A *\<^sub>v x) = (\<exists>x\<in>carrier_vec nc. - 1\<^sub>m nc *\<^sub>v x \<le> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> - A *\<^sub>v x \<le> - b)
[PROOF STEP]
by (rule bex_cong[OF refl], insert A b, auto simp: less_eq_vec_def)
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> 1\<^sub>m nc *\<^sub>v x \<and> A *\<^sub>v x \<le> b \<and> b \<le> A *\<^sub>v x) = (\<exists>x\<in>carrier_vec nc. - 1\<^sub>m nc *\<^sub>v x \<le> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> - A *\<^sub>v x \<le> - b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. 0\<^sub>v nc \<le> 1\<^sub>m nc *\<^sub>v x \<and> A *\<^sub>v x \<le> b \<and> b \<le> A *\<^sub>v x) = (\<exists>x\<in>carrier_vec nc. - 1\<^sub>m nc *\<^sub>v x \<le> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> - A *\<^sub>v x \<le> - b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<exists> x \<in> carrier_vec nc. B *\<^sub>v x \<le> b')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. - 1\<^sub>m nc *\<^sub>v x \<le> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> - A *\<^sub>v x \<le> - b) = (\<exists>x\<in>carrier_vec nc. B *\<^sub>v x \<le> b')
[PROOF STEP]
by (rule bex_cong[OF refl], insert A b, unfold B_def b'_def,
      subst append_rows_le[of _ ], (auto)[4], intro conj_cong[OF refl], subst append_rows_le, auto)
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. - 1\<^sub>m nc *\<^sub>v x \<le> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> - A *\<^sub>v x \<le> - b) = (\<exists>x\<in>carrier_vec nc. B *\<^sub>v x \<le> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. - 1\<^sub>m nc *\<^sub>v x \<le> 0\<^sub>v nc \<and> A *\<^sub>v x \<le> b \<and> - A *\<^sub>v x \<le> - b) = (\<exists>x\<in>carrier_vec nc. B *\<^sub>v x \<le> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y\<ge>0\<^sub>v n. mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> y \<bullet> b' \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>x\<in>carrier_vec nc. B *\<^sub>v x \<le> b') = (\<forall>y\<ge>0\<^sub>v n. mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')
[PROOF STEP]
by (rule farkas_lemma_matrix[OF B b'])
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. B *\<^sub>v x \<le> b') = (\<forall>y\<ge>0\<^sub>v n. mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<exists>x\<in>carrier_vec nc. B *\<^sub>v x \<le> b') = (\<forall>y\<ge>0\<^sub>v n. mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall> y. y \<in> carrier_vec n \<longrightarrow> y\<ge>0\<^sub>v n \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> y \<bullet> b' \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y\<ge>0\<^sub>v n. mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y. y \<in> carrier_vec n \<longrightarrow> 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')
[PROOF STEP]
by (intro arg_cong[of _ _ All], intro ext, auto simp: less_eq_vec_def)
[PROOF STATE]
proof (state)
this:
(\<forall>y\<ge>0\<^sub>v n. mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y. y \<in> carrier_vec n \<longrightarrow> 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y\<ge>0\<^sub>v n. mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y. y \<in> carrier_vec n \<longrightarrow> 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall> y \<in> carrier_vec n. y\<ge>0\<^sub>v n \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> y \<bullet> b' \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y. y \<in> carrier_vec n \<longrightarrow> 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y\<in>carrier_vec n. 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>y. y \<in> carrier_vec n \<longrightarrow> 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y\<in>carrier_vec n. 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y. y \<in> carrier_vec n \<longrightarrow> 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y\<in>carrier_vec n. 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b')

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y1 \<in>carrier_vec nc. \<forall>y2 \<in>carrier_vec nr. \<forall>y3 \<in>carrier_vec nr.
              0\<^sub>v nc @\<^sub>v (0\<^sub>v nr @\<^sub>v 0\<^sub>v nr) \<le> y1 @\<^sub>v y2 @\<^sub>v y3  \<longrightarrow>
              mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * ((- 1\<^sub>m nc) @\<^sub>r (A @\<^sub>r -A)) = 0\<^sub>m 1 nc
              \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v (b @\<^sub>v -b)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y\<in>carrier_vec n. 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> y1 @\<^sub>v y2 @\<^sub>v y3 \<longrightarrow> mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b))
[PROOF STEP]
unfolding n_def all_vec_append id0 b'_def B_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x1\<in>carrier_vec nc. \<forall>x1a\<in>carrier_vec nr. \<forall>x2\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> x1 @\<^sub>v x1a @\<^sub>v x2 \<longrightarrow> mat_of_row (x1 @\<^sub>v x1a @\<^sub>v x2) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (x1 @\<^sub>v x1a @\<^sub>v x2) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b)) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> y1 @\<^sub>v y2 @\<^sub>v y3 \<longrightarrow> mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>y\<in>carrier_vec n. 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> y1 @\<^sub>v y2 @\<^sub>v y3 \<longrightarrow> mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b))

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y\<in>carrier_vec n. 0\<^sub>v n \<le> y \<longrightarrow> mat_of_row y * B = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y \<bullet> b') = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> y1 @\<^sub>v y2 @\<^sub>v y3 \<longrightarrow> mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b))

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y1 \<in>carrier_vec nc. \<forall>y2 \<in>carrier_vec nr. \<forall>y3 \<in>carrier_vec nr.
              0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow>
              (- mat_of_row y1) +
              (mat_of_row y2 * A - (mat_of_row y3 * A)) = 0\<^sub>m 1 nc
              \<longrightarrow> y2 \<bullet> b - y3 \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> y1 @\<^sub>v y2 @\<^sub>v y3 \<longrightarrow> mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b)) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b)
[PROOF STEP]
by (intro ball_cong[OF refl], subst append_vec_le, (auto)[2], subst append_vec_le, (auto)[2], insert A b,
      subst scalar_prod_append, (auto)[4], subst scalar_prod_append, (auto)[4],
      subst mat_of_row_mult_append_rows, (auto)[4],
      subst mat_of_row_mult_append_rows, (auto)[4],
      subst add_uminus_minus_mat[symmetric], auto)
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> y1 @\<^sub>v y2 @\<^sub>v y3 \<longrightarrow> mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b)) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc @\<^sub>v 0\<^sub>v nr @\<^sub>v 0\<^sub>v nr \<le> y1 @\<^sub>v y2 @\<^sub>v y3 \<longrightarrow> mat_of_row (y1 @\<^sub>v y2 @\<^sub>v y3) * (- 1\<^sub>m nc @\<^sub>r A @\<^sub>r - A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> (y1 @\<^sub>v y2 @\<^sub>v y3) \<bullet> (0\<^sub>v nc @\<^sub>v b @\<^sub>v - b)) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y1 \<in>carrier_vec nc. \<forall>y2 \<in>carrier_vec nr. \<forall>y3 \<in>carrier_vec nr.
              0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow>
              mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A
              \<longrightarrow> y2 \<bullet> b - y3 \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b)
[PROOF STEP]
proof ((intro ball_cong[OF refl] arg_cong2[of _ _ _ _ "(\<longrightarrow>)"] refl, standard), goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A
 2. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A\<rbrakk> \<Longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
case (1 y1 y2 y3)
[PROOF STATE]
proof (state)
this:
y1 \<in> carrier_vec nc
y2 \<in> carrier_vec nr
y3 \<in> carrier_vec nr
- mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc

goal (2 subgoals):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc\<rbrakk> \<Longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A
 2. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A\<rbrakk> \<Longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
from arg_cong[OF 1(4), of "\<lambda> x. mat_of_row y1 + x"]
[PROOF STATE]
proof (chain)
picking this:
mat_of_row y1 + (- mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A)) = mat_of_row y1 + 0\<^sub>m 1 nc
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
mat_of_row y1 + (- mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A)) = mat_of_row y1 + 0\<^sub>m 1 nc

goal (1 subgoal):
 1. mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A
[PROOF STEP]
using 1(1-3) A
[PROOF STATE]
proof (prove)
using this:
mat_of_row y1 + (- mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A)) = mat_of_row y1 + 0\<^sub>m 1 nc
y1 \<in> carrier_vec nc
y2 \<in> carrier_vec nr
y3 \<in> carrier_vec nr
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A
[PROOF STEP]
by (subst (asm) assoc_add_mat[symmetric], (auto)[3],
        subst (asm) add_uminus_minus_mat, (auto)[1],
        subst (asm) minus_r_inv_mat, force,
        subst (asm) right_add_zero_mat, force,
        subst (asm) left_add_zero_mat, force, auto)
[PROOF STATE]
proof (state)
this:
mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A

goal (1 subgoal):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A\<rbrakk> \<Longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A\<rbrakk> \<Longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
case (2 y1 y2 y3)
[PROOF STATE]
proof (state)
this:
y1 \<in> carrier_vec nc
y2 \<in> carrier_vec nr
y3 \<in> carrier_vec nr
mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A

goal (1 subgoal):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A\<rbrakk> \<Longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
unfolding 2(4)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - (mat_of_row y2 * A - mat_of_row y3 * A) + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
using 2(1-3) A
[PROOF STATE]
proof (prove)
using this:
y1 \<in> carrier_vec nc
y2 \<in> carrier_vec nr
y3 \<in> carrier_vec nr
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. - (mat_of_row y2 * A - mat_of_row y3 * A) + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc
[PROOF STEP]
by (intro eq_matI, auto)
[PROOF STATE]
proof (state)
this:
- mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> - mat_of_row y1 + (mat_of_row y2 * A - mat_of_row y3 * A) = 0\<^sub>m 1 nc \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y1 \<in>carrier_vec nc. \<forall>y2 \<in>carrier_vec nr. \<forall>y3 \<in>carrier_vec nr.
              0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow>
              mat_of_row y1 = mat_of_row (y2 - y3) * A
              \<longrightarrow> (y2 - y3) \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)
[PROOF STEP]
by (intro ball_cong[OF refl] imp_cong refl
      arg_cong2[of _ _ _ _ "(\<le>)"] arg_cong2[of _ _ _ _ "(=)"],
      subst minus_mult_distrib_mat[symmetric], insert A b, auto
      simp: minus_scalar_prod_distrib mat_of_rows_def
      intro!: arg_cong[of _ _ "\<lambda> x. x * _"])
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row y2 * A - mat_of_row y3 * A \<longrightarrow> 0 \<le> y2 \<bullet> b - y3 \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y1 \<in>carrier_vec nc. \<forall>y2 \<in>carrier_vec nr. \<forall>y3 \<in>carrier_vec nr.
              0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow>
              y1 = row (mat_of_row (y2 - y3) * A) 0
              \<longrightarrow> (y2 - y3) \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)
[PROOF STEP]
proof (intro ball_cong[OF refl] arg_cong2[of _ _ _ _ "(\<longrightarrow>)"] refl, standard, goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; mat_of_row y1 = mat_of_row (y2 - y3) * A\<rbrakk> \<Longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0
 2. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; y1 = row (mat_of_row (y2 - y3) * A) 0\<rbrakk> \<Longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A
[PROOF STEP]
case (1 y1 y2 y3)
[PROOF STATE]
proof (state)
this:
y1 \<in> carrier_vec nc
y2 \<in> carrier_vec nr
y3 \<in> carrier_vec nr
mat_of_row y1 = mat_of_row (y2 - y3) * A

goal (2 subgoals):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; mat_of_row y1 = mat_of_row (y2 - y3) * A\<rbrakk> \<Longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0
 2. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; y1 = row (mat_of_row (y2 - y3) * A) 0\<rbrakk> \<Longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A
[PROOF STEP]
from arg_cong[OF 1(4), of "\<lambda> x. row x 0"] 1(1-3) A
[PROOF STATE]
proof (chain)
picking this:
row (mat_of_row y1) 0 = row (mat_of_row (y2 - y3) * A) 0
y1 \<in> carrier_vec nc
y2 \<in> carrier_vec nr
y3 \<in> carrier_vec nr
A \<in> carrier_mat nr nc
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
row (mat_of_row y1) 0 = row (mat_of_row (y2 - y3) * A) 0
y1 \<in> carrier_vec nc
y2 \<in> carrier_vec nr
y3 \<in> carrier_vec nr
A \<in> carrier_mat nr nc

goal (1 subgoal):
 1. y1 = row (mat_of_row (y2 - y3) * A) 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y1 = row (mat_of_row (y2 - y3) * A) 0

goal (1 subgoal):
 1. \<And>y1 y2 y3. \<lbrakk>y1 \<in> carrier_vec nc; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; y1 = row (mat_of_row (y2 - y3) * A) 0\<rbrakk> \<Longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A
[PROOF STEP]
qed (insert A, auto)
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> mat_of_row y1 = mat_of_row (y2 - y3) * A \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y2 \<in>carrier_vec nr. \<forall>y3 \<in>carrier_vec nr.
              0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow>
              row (mat_of_row (y2 - y3) * A) 0 \<in> carrier_vec nc
              \<longrightarrow> (y2 - y3) \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> row (mat_of_row (y2 - y3) * A) 0 \<in> carrier_vec nc \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> row (mat_of_row (y2 - y3) * A) 0 \<in> carrier_vec nc \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y1\<in>carrier_vec nc. \<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> y1 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> y1 = row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> row (mat_of_row (y2 - y3) * A) 0 \<in> carrier_vec nc \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall>y2 \<in>carrier_vec nr. \<forall>y3 \<in>carrier_vec nr.
              0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3
              \<longrightarrow> (y2 - y3) \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> row (mat_of_row (y2 - y3) * A) 0 \<in> carrier_vec nc \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)
[PROOF STEP]
by (intro ball_cong[OF refl] arg_cong2[of _ _ _ _ "(\<longrightarrow>)"] refl, insert A,
        auto simp: row_def)
[PROOF STATE]
proof (state)
this:
(\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> row (mat_of_row (y2 - y3) * A) 0 \<in> carrier_vec nc \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> row (mat_of_row (y2 - y3) * A) 0 \<in> carrier_vec nc \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall> y \<in> carrier_vec nr. row (mat_of_row y * A) 0 \<ge> 0\<^sub>v nc \<longrightarrow> y \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
proof ((standard; intro ballI impI), goal_cases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b; y \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row y * A) 0\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>y2 y3. \<lbrakk>\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0; 0\<^sub>v nr \<le> y2; 0\<^sub>v nr \<le> y3\<rbrakk> \<Longrightarrow> 0 \<le> (y2 - y3) \<bullet> b
[PROOF STEP]
case (1 y)
[PROOF STATE]
proof (state)
this:
\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b
y \<in> carrier_vec nr
0\<^sub>v nc \<le> row (mat_of_row y * A) 0

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b; y \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row y * A) 0\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>y2 y3. \<lbrakk>\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0; 0\<^sub>v nr \<le> y2; 0\<^sub>v nr \<le> y3\<rbrakk> \<Longrightarrow> 0 \<le> (y2 - y3) \<bullet> b
[PROOF STEP]
define y2 where "y2 = vec nr (\<lambda> i. if y $ i \<ge> 0 then y $ i else 0)"
[PROOF STATE]
proof (state)
this:
y2 = vec nr (\<lambda>i. if 0 \<le> y $ i then y $ i else 0)

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b; y \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row y * A) 0\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>y2 y3. \<lbrakk>\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0; 0\<^sub>v nr \<le> y2; 0\<^sub>v nr \<le> y3\<rbrakk> \<Longrightarrow> 0 \<le> (y2 - y3) \<bullet> b
[PROOF STEP]
define y3 where "y3 = vec nr (\<lambda> i. if y $ i \<ge> 0 then 0 else - y $ i)"
[PROOF STATE]
proof (state)
this:
y3 = vec nr (\<lambda>i. if 0 \<le> y $ i then 0 else - y $ i)

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b; y \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row y * A) 0\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>y2 y3. \<lbrakk>\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0; 0\<^sub>v nr \<le> y2; 0\<^sub>v nr \<le> y3\<rbrakk> \<Longrightarrow> 0 \<le> (y2 - y3) \<bullet> b
[PROOF STEP]
have y: "y = y2 - y3"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = y2 - y3
[PROOF STEP]
unfolding y2_def y3_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y = vec nr (\<lambda>i. if 0 \<le> y $ i then y $ i else 0) - vec nr (\<lambda>i. if 0 \<le> y $ i then 0 else - y $ i)
[PROOF STEP]
using 1(2)
[PROOF STATE]
proof (prove)
using this:
y \<in> carrier_vec nr

goal (1 subgoal):
 1. y = vec nr (\<lambda>i. if 0 \<le> y $ i then y $ i else 0) - vec nr (\<lambda>i. if 0 \<le> y $ i then 0 else - y $ i)
[PROOF STEP]
by (intro eq_vecI, auto)
[PROOF STATE]
proof (state)
this:
y = y2 - y3

goal (2 subgoals):
 1. \<And>y. \<lbrakk>\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b; y \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row y * A) 0\<rbrakk> \<Longrightarrow> 0 \<le> y \<bullet> b
 2. \<And>y2 y3. \<lbrakk>\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0; 0\<^sub>v nr \<le> y2; 0\<^sub>v nr \<le> y3\<rbrakk> \<Longrightarrow> 0 \<le> (y2 - y3) \<bullet> b
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<le> y \<bullet> b
[PROOF STEP]
by (rule 1(1)[rule_format, of y2 y3, folded y, OF _ _ 1(3)],
       auto simp: y2_def y3_def less_eq_vec_def)
[PROOF STATE]
proof (state)
this:
0 \<le> y \<bullet> b

goal (1 subgoal):
 1. \<And>y2 y3. \<lbrakk>\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b; y2 \<in> carrier_vec nr; y3 \<in> carrier_vec nr; 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0; 0\<^sub>v nr \<le> y2; 0\<^sub>v nr \<le> y3\<rbrakk> \<Longrightarrow> 0 \<le> (y2 - y3) \<bullet> b
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
(\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<forall>y2\<in>carrier_vec nr. \<forall>y3\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row (y2 - y3) * A) 0 \<longrightarrow> 0\<^sub>v nr \<le> y2 \<longrightarrow> 0\<^sub>v nr \<le> y3 \<longrightarrow> 0 \<le> (y2 - y3) \<bullet> b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
have "\<dots> = (\<forall> y \<in> carrier_vec nr. mat_of_row y * A \<ge> 0\<^sub>m 1 nc \<longrightarrow> y \<bullet> b \<ge> 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
by (intro ball_cong arg_cong2[of _ _ _ _ "(\<longrightarrow>)"] refl,
      insert A, auto simp: less_eq_vec_def less_eq_mat_def)
[PROOF STATE]
proof (state)
this:
(\<forall>y\<in>carrier_vec nr. 0\<^sub>v nc \<le> row (mat_of_row y * A) 0 \<longrightarrow> 0 \<le> y \<bullet> b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)

goal (1 subgoal):
 1. (\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<exists>x\<ge>0\<^sub>v nc. A *\<^sub>v x = b) = (\<forall>y\<in>carrier_vec nr. 0\<^sub>m 1 nc \<le> mat_of_row y * A \<longrightarrow> 0 \<le> y \<bullet> b)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in lgroup) less_eq_inf_2: "(x \<le> y) = (inf y x = x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<le> y) = (y \<sqinter> x = x)
[PROOF STEP]
by (simp add: le_iff_inf inf_commute)


[STATEMENT]
lemma [simp]: "sup (Rep_G a - u + Rep_G b) 0 \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a - u + Rep_G b \<squnion> (0::'b) \<in> G
[PROOF STEP]
apply (cut_tac x = a in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<in> G \<Longrightarrow> Rep_G a - u + Rep_G b \<squnion> (0::'b) \<in> G
[PROOF STEP]
apply (cut_tac x = b in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_G a \<in> G; Rep_G b \<in> G\<rbrakk> \<Longrightarrow> Rep_G a - u + Rep_G b \<squnion> (0::'b) \<in> G
[PROOF STEP]
apply (unfold G_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_G a \<in> {a. (0::'b) \<le> a \<and> a \<le> u}; Rep_G b \<in> {a. (0::'b) \<le> a \<and> a \<le> u}\<rbrakk> \<Longrightarrow> Rep_G a - u + Rep_G b \<squnion> (0::'b) \<in> {a. (0::'b) \<le> a \<and> a \<le> u}
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) \<le> Rep_G a - u + Rep_G b \<squnion> (0::'b)
 2. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> Rep_G a - u + Rep_G b \<squnion> (0::'b) \<le> u
[PROOF STEP]
apply (simp_all add: diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> Rep_G a + - u + Rep_G b \<le> u
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> u + - Rep_G b
[PROOF STEP]
apply (rule_tac y = 0 in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> Rep_G a + - u \<le> (0::'b)
 2. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) \<le> u + - Rep_G b
[PROOF STEP]
apply (rule right_move_to_right)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> Rep_G a \<le> (0::'b) + - (- u)
 2. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) \<le> u + - Rep_G b
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) \<le> u + - Rep_G b
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) + - (- Rep_G b) \<le> u
[PROOF STEP]
by simp


[STATEMENT]
lemma [simp]: "inf (u - Rep_G a + Rep_G b) u \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u - Rep_G a + Rep_G b) \<sqinter> u \<in> G
[PROOF STEP]
apply (cut_tac x = a in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G a \<in> G \<Longrightarrow> (u - Rep_G a + Rep_G b) \<sqinter> u \<in> G
[PROOF STEP]
apply (cut_tac x = b in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_G a \<in> G; Rep_G b \<in> G\<rbrakk> \<Longrightarrow> (u - Rep_G a + Rep_G b) \<sqinter> u \<in> G
[PROOF STEP]
apply (unfold G_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_G a \<in> {a. (0::'b) \<le> a \<and> a \<le> u}; Rep_G b \<in> {a. (0::'b) \<le> a \<and> a \<le> u}\<rbrakk> \<Longrightarrow> (u - Rep_G a + Rep_G b) \<sqinter> u \<in> {a. (0::'b) \<le> a \<and> a \<le> u}
[PROOF STEP]
apply (simp_all add: diff_minus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a \<and> Rep_G a \<le> u; (0::'b) \<le> Rep_G b \<and> Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) \<le> u + - Rep_G a + Rep_G b
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) \<le> u + - Rep_G a + Rep_G b
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) + - Rep_G b \<le> u + - Rep_G a
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> (0::'b) + - Rep_G b + - (- Rep_G a) \<le> u
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> - Rep_G b + Rep_G a \<le> u
[PROOF STEP]
apply (rule left_move_to_right)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> Rep_G a \<le> - (- Rep_G b) + u
[PROOF STEP]
apply (rule_tac y = u in order_trans)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> Rep_G a \<le> u
 2. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> u \<le> - (- Rep_G b) + u
[PROOF STEP]
apply  simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> u \<le> Rep_G b + u
[PROOF STEP]
apply (rule right_move_to_left)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(0::'b) \<le> Rep_G a; Rep_G a \<le> u; (0::'b) \<le> Rep_G b; Rep_G b \<le> u\<rbrakk> \<Longrightarrow> u + - u \<le> Rep_G b
[PROOF STEP]
by simp_all


[STATEMENT]
lemma [simp]: "(u::'a) \<in> G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u \<in> G
[PROOF STEP]
by (simp add: G_def)


[STATEMENT]
lemma [simp]: "(1::'a G) * a = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 * a = a
[PROOF STEP]
apply (simp add: one_def times_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_G (Rep_G (Abs_G u) - u + Rep_G a \<squnion> (0::'a)) = a
[PROOF STEP]
apply (cut_tac y = "u::'a" in Abs_G_inverse)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. u \<in> G
 2. Rep_G (Abs_G u) = u \<Longrightarrow> Abs_G (Rep_G (Abs_G u) - u + Rep_G a \<squnion> (0::'a)) = a
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G (Abs_G u) = u \<Longrightarrow> Abs_G (Rep_G a \<squnion> (0::'a)) = a
[PROOF STEP]
apply (subgoal_tac "sup (Rep_G a) (0::'a) = Rep_G a")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<squnion> (0::'a) = Rep_G a\<rbrakk> \<Longrightarrow> Abs_G (Rep_G a \<squnion> (0::'a)) = a
 2. Rep_G (Abs_G u) = u \<Longrightarrow> Rep_G a \<squnion> (0::'a) = Rep_G a
[PROOF STEP]
apply (simp add: Rep_G_inverse)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_G (Abs_G u) = u \<Longrightarrow> Rep_G a \<squnion> (0::'a) = Rep_G a
[PROOF STEP]
apply (cut_tac x = a in Rep_G)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<squnion> (0::'a) = Rep_G a
[PROOF STEP]
apply (rule antisym)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<squnion> (0::'a) \<le> Rep_G a
 2. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<le> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
apply (simp add: G_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Rep_G (Abs_G u) = u; Rep_G a \<in> G\<rbrakk> \<Longrightarrow> Rep_G a \<le> Rep_G a \<squnion> (0::'a)
[PROOF STEP]
by simp