diff -r 32bee18c675f -r 900291ee0af8 src/HOL/Matrix/SparseMatrix.thy
--- a/src/HOL/Matrix/SparseMatrix.thy	Mon Mar 07 16:55:36 2005 +0100
+++ b/src/HOL/Matrix/SparseMatrix.thy	Mon Mar 07 18:19:55 2005 +0100
@@ -138,6 +138,14 @@
   apply (simp add: sorted_spvec.simps split:list.split_asm)
   done
 
+lemma sorted_spvec_minus_spvec:
+  "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
+  apply (induct v)
+  apply (simp)
+  apply (frule sorted_spvec_cons1, simp)
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
+  done
+
 lemma sorted_spvec_abs_spvec:
   "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
   apply (induct v)
@@ -233,7 +241,6 @@
   apply (frule_tac as=arr in sorted_spvec_cons1)
   apply (frule_tac as=brr in sorted_spvec_cons1)
   apply (simp)
-  apply (case_tac "a=aa")
   apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
   done
 
@@ -590,6 +597,13 @@
 
 ML {* simp_depth_limit := 2 *}
 
+lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
+   by (simp add: disj_matrices_def)
+
+lemma disj_matrices_contr2: "disj_matrices A B \<Longrightarrow> Rep_matrix B j i \<noteq> 0 \<Longrightarrow> Rep_matrix A j i = 0"
+   by (simp add: disj_matrices_def)
+
+
 lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
   (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group) matrix))"
   apply (auto)
@@ -800,7 +814,7 @@
   apply (induct A)
   apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
   apply (frule_tac sorted_spvec_cons1, simp)
-  apply (subst Rep_matrix_inject[symmetric])
+  apply (simplesubst Rep_matrix_inject[symmetric])
   apply (rule ext)+
   apply auto
   apply (case_tac "x=a")
@@ -858,27 +872,6 @@
 lemma sorted_sparse_matrix_imp_spmat: "sorted_sparse_matrix A \<Longrightarrow> sorted_spmat A"
   by (simp add: sorted_sparse_matrix_def)
 
-lemmas sparse_row_matrix_op_simps =
-  sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
-  sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat
-  sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat
-  sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat
-  sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat
-  sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat
-  le_spmat_iff_sparse_row_le
-
-lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
-
-lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] = 
-  mult_spmat.simps mult_spvec_spmat.simps 
-  addmult_spvec.simps 
-  smult_spvec_empty smult_spvec_cons
-  add_spmat.simps add_spvec.simps
-  minus_spmat.simps minus_spvec.simps
-  abs_spmat.simps abs_spvec.simps
-  diff_spmat_def
-  le_spmat.simps le_spvec.simps
-
 lemmas sorted_sp_simps = 
   sorted_spvec.simps
   sorted_spmat.simps
@@ -898,7 +891,210 @@
 
 lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
 
-lemma spm_linprog_dual_estimate_1:
+consts
+  pprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
+  nprt_spvec :: "('a::{lordered_ab_group}) spvec \<Rightarrow> 'a spvec"
+  pprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
+  nprt_spmat :: "('a::{lordered_ab_group}) spmat \<Rightarrow> 'a spmat"
+
+primrec
+  "pprt_spvec [] = []"
+  "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
+
+primrec
+  "nprt_spvec [] = []"
+  "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
+
+primrec 
+  "pprt_spmat [] = []"
+  "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
+  (*case (pprt_spvec (snd a)) of [] \<Rightarrow> (pprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(pprt_spmat as))"*)
+
+primrec 
+  "nprt_spmat [] = []"
+  "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
+  (*case (nprt_spvec (snd a)) of [] \<Rightarrow> (nprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(nprt_spmat as))"*)
+
+
+lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
+  apply (simp add: pprt_def join_matrix)
+  apply (simp add: Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply simp
+  apply (case_tac "Rep_matrix A x xa \<noteq> 0")
+  apply (simp_all add: disj_matrices_contr1)
+  done
+
+lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
+  apply (simp add: nprt_def meet_matrix)
+  apply (simp add: Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply simp
+  apply (case_tac "Rep_matrix A x xa \<noteq> 0")
+  apply (simp_all add: disj_matrices_contr1)
+  done
+
+lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
+  apply (simp add: pprt_def join_matrix)
+  apply (simp add: Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply simp
+  done
+
+lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
+  apply (simp add: nprt_def meet_matrix)
+  apply (simp add: Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply simp
+  done
+
+lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def)
+
+lemma sparse_row_vector_pprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
+  apply (induct v)
+  apply (simp_all)
+  apply (frule sorted_spvec_cons1, auto)
+  apply (subst pprt_add)
+  apply (subst disj_matrices_commute)
+  apply (rule disj_sparse_row_singleton)
+  apply auto
+  done
+
+lemma sparse_row_vector_nprt: "sorted_spvec v \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
+  apply (induct v)
+  apply (simp_all)
+  apply (frule sorted_spvec_cons1, auto)
+  apply (subst nprt_add)
+  apply (subst disj_matrices_commute)
+  apply (rule disj_sparse_row_singleton)
+  apply auto
+  done
+  
+  
+lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
+  apply (simp add: pprt_def)
+  apply (simp add: join_matrix)
+  apply (simp add: Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply (simp)
+  done
+
+lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
+  apply (simp add: nprt_def)
+  apply (simp add: meet_matrix)
+  apply (simp add: Rep_matrix_inject[symmetric])
+  apply (rule ext)+
+  apply (simp)
+  done
+
+lemma sparse_row_matrix_pprt: "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
+  apply (induct m)
+  apply simp
+  apply simp
+  apply (frule sorted_spvec_cons1)
+  apply (simp add: sparse_row_matrix_cons sparse_row_vector_pprt)
+  apply (subst pprt_add)
+  apply (subst disj_matrices_commute)
+  apply (rule disj_move_sparse_vec_mat)
+  apply auto
+  apply (simp add: sorted_spvec.simps)
+  apply (simp split: list.split)
+  apply auto
+  apply (simp add: pprt_move_matrix)
+  done
+
+lemma sparse_row_matrix_nprt: "sorted_spvec m \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)"
+  apply (induct m)
+  apply simp
+  apply simp
+  apply (frule sorted_spvec_cons1)
+  apply (simp add: sparse_row_matrix_cons sparse_row_vector_nprt)
+  apply (subst nprt_add)
+  apply (subst disj_matrices_commute)
+  apply (rule disj_move_sparse_vec_mat)
+  apply auto
+  apply (simp add: sorted_spvec.simps)
+  apply (simp split: list.split)
+  apply auto
+  apply (simp add: nprt_move_matrix)
+  done
+
+lemma sorted_pprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (pprt_spvec v)"
+  apply (induct v)
+  apply (simp)
+  apply (frule sorted_spvec_cons1)
+  apply simp
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
+  done
+
+lemma sorted_nprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (nprt_spvec v)"
+  apply (induct v)
+  apply (simp)
+  apply (frule sorted_spvec_cons1)
+  apply simp
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
+  done
+
+lemma sorted_spvec_pprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (pprt_spmat m)"
+  apply (induct m)
+  apply (simp)
+  apply (frule sorted_spvec_cons1)
+  apply simp
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
+  done
+
+lemma sorted_spvec_nprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (nprt_spmat m)"
+  apply (induct m)
+  apply (simp)
+  apply (frule sorted_spvec_cons1)
+  apply simp
+  apply (simp add: sorted_spvec.simps split:list.split_asm)
+  done
+
+lemma sorted_spmat_pprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (pprt_spmat m)"
+  apply (induct m)
+  apply (simp_all add: sorted_pprt_spvec)
+  done
+
+lemma sorted_spmat_nprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (nprt_spmat m)"
+  apply (induct m)
+  apply (simp_all add: sorted_nprt_spvec)
+  done
+
+constdefs
+  mult_est_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
+  "mult_est_spmat r1 r2 s1 s2 == 
+  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
+  add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"  
+
+lemmas sparse_row_matrix_op_simps =
+  sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
+  sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat
+  sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat
+  sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat
+  sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat
+  sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat
+  le_spmat_iff_sparse_row_le
+  sparse_row_matrix_pprt sorted_spvec_pprt_spmat sorted_spmat_pprt_spmat
+  sparse_row_matrix_nprt sorted_spvec_nprt_spmat sorted_spmat_nprt_spmat
+
+lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
+
+lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] = 
+  mult_spmat.simps mult_spvec_spmat.simps 
+  addmult_spvec.simps 
+  smult_spvec_empty smult_spvec_cons
+  add_spmat.simps add_spvec.simps
+  minus_spmat.simps minus_spvec.simps
+  abs_spmat.simps abs_spvec.simps
+  diff_spmat_def
+  le_spmat.simps le_spvec.simps
+  pprt_spmat.simps pprt_spvec.simps
+  nprt_spmat.simps nprt_spvec.simps
+  mult_est_spmat_def
+
+
+(*lemma spm_linprog_dual_estimate_1:
   assumes  
   "sorted_sparse_matrix A1"
   "sorted_sparse_matrix A2"
@@ -918,5 +1114,59 @@
   "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b, mult_spmat (add_spmat (add_spmat (mult_spmat y (diff_spmat A2 A1), 
   abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))"
   by (insert prems, simp add: sparse_row_matrix_op_simps linprog_dual_estimate_1[where A=A])
+*)
 
+lemma spm_mult_le_dual_prts: 
+  assumes
+  "sorted_sparse_matrix A1"
+  "sorted_sparse_matrix A2"
+  "sorted_sparse_matrix c1"
+  "sorted_sparse_matrix c2"
+  "sorted_sparse_matrix y"
+  "sorted_sparse_matrix r1"
+  "sorted_sparse_matrix r2"
+  "sorted_spvec b"
+  "le_spmat ([], y)"
+  "sparse_row_matrix A1 \<le> A"
+  "A \<le> sparse_row_matrix A2"
+  "sparse_row_matrix c1 \<le> c"
+  "c \<le> sparse_row_matrix c2"
+  "sparse_row_matrix r1 \<le> x"
+  "x \<le> sparse_row_matrix r2"
+  "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
+  shows
+  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
+  (let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in 
+  add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
+  add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1)))))))"
+  apply (simp add: Let_def)
+  apply (insert prems)
+  apply (simp add: sparse_row_matrix_op_simps ring_eq_simps)  
+  apply (rule mult_le_dual_prts[where A=A, simplified Let_def ring_eq_simps])
+  apply (auto)
+  done
+
+lemma spm_mult_le_dual_prts_no_let: 
+  assumes
+  "sorted_sparse_matrix A1"
+  "sorted_sparse_matrix A2"
+  "sorted_sparse_matrix c1"
+  "sorted_sparse_matrix c2"
+  "sorted_sparse_matrix y"
+  "sorted_sparse_matrix r1"
+  "sorted_sparse_matrix r2"
+  "sorted_spvec b"
+  "le_spmat ([], y)"
+  "sparse_row_matrix A1 \<le> A"
+  "A \<le> sparse_row_matrix A2"
+  "sparse_row_matrix c1 \<le> c"
+  "c \<le> sparse_row_matrix c2"
+  "sparse_row_matrix r1 \<le> x"
+  "x \<le> sparse_row_matrix r2"
+  "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
+  shows
+  "c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b,
+  mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
+  by (simp add: prems mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
+ 
 end