src/HOL/Matrix/SparseMatrix.thy
author haftmann
Mon Apr 27 10:11:44 2009 +0200 (2009-04-27)
changeset 31001 7e6ffd8f51a9
parent 29667 53103fc8ffa3
child 31816 ffaf6dd53045
permissions -rw-r--r--
cleaned up theory power further
     1 (*  Title:      HOL/Matrix/SparseMatrix.thy
     2     ID:         $Id$
     3     Author:     Steven Obua
     4 *)
     5 
     6 theory SparseMatrix
     7 imports Matrix
     8 begin
     9 
    10 types 
    11   'a spvec = "(nat * 'a) list"
    12   'a spmat = "('a spvec) spvec"
    13 
    14 definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix" where
    15   sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
    16 
    17 definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix" where
    18   sparse_row_matrix_def: "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
    19 
    20 code_datatype sparse_row_vector sparse_row_matrix
    21 
    22 lemma sparse_row_vector_empty [simp]: "sparse_row_vector [] = 0"
    23   by (simp add: sparse_row_vector_def)
    24 
    25 lemma sparse_row_matrix_empty [simp]: "sparse_row_matrix [] = 0"
    26   by (simp add: sparse_row_matrix_def)
    27 
    28 lemmas [code] = sparse_row_vector_empty [symmetric]
    29 
    30 lemma foldl_distrstart[rule_format]: "! a x y. (f (g x y) a = g x (f y a)) \<Longrightarrow> ! x y. (foldl f (g x y) l = g x (foldl f y l))"
    31   by (induct l, auto)
    32 
    33 lemma sparse_row_vector_cons[simp]:
    34   "sparse_row_vector (a # arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
    35   apply (induct arr)
    36   apply (auto simp add: sparse_row_vector_def)
    37   apply (simp add: foldl_distrstart [of "\<lambda>m x. m + singleton_matrix 0 (fst x) (snd x)" "\<lambda>x m. singleton_matrix 0 (fst x) (snd x) + m"])
    38   done
    39 
    40 lemma sparse_row_vector_append[simp]:
    41   "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
    42   by (induct a) auto
    43 
    44 lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)"
    45   apply (induct x)
    46   apply (simp_all add: add_nrows)
    47   done
    48 
    49 lemma sparse_row_matrix_cons: "sparse_row_matrix (a#arr) = ((move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0)) + sparse_row_matrix arr"
    50   apply (induct arr)
    51   apply (auto simp add: sparse_row_matrix_def)
    52   apply (simp add: foldl_distrstart[of "\<lambda>m x. m + (move_matrix (sparse_row_vector (snd x)) (int (fst x)) 0)" 
    53     "% a m. (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0) + m"])
    54   done
    55 
    56 lemma sparse_row_matrix_append: "sparse_row_matrix (arr@brr) = (sparse_row_matrix arr) + (sparse_row_matrix brr)"
    57   apply (induct arr)
    58   apply (auto simp add: sparse_row_matrix_cons)
    59   done
    60 
    61 primrec sorted_spvec :: "'a spvec \<Rightarrow> bool" where
    62   "sorted_spvec [] = True"
    63   | sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
    64 
    65 primrec sorted_spmat :: "'a spmat \<Rightarrow> bool" where
    66   "sorted_spmat [] = True"
    67   | "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
    68 
    69 declare sorted_spvec.simps [simp del]
    70 
    71 lemma sorted_spvec_empty[simp]: "sorted_spvec [] = True"
    72 by (simp add: sorted_spvec.simps)
    73 
    74 lemma sorted_spvec_cons1: "sorted_spvec (a#as) \<Longrightarrow> sorted_spvec as"
    75 apply (induct as)
    76 apply (auto simp add: sorted_spvec.simps)
    77 done
    78 
    79 lemma sorted_spvec_cons2: "sorted_spvec (a#b#t) \<Longrightarrow> sorted_spvec (a#t)"
    80 apply (induct t)
    81 apply (auto simp add: sorted_spvec.simps)
    82 done
    83 
    84 lemma sorted_spvec_cons3: "sorted_spvec(a#b#t) \<Longrightarrow> fst a < fst b"
    85 apply (auto simp add: sorted_spvec.simps)
    86 done
    87 
    88 lemma sorted_sparse_row_vector_zero[rule_format]: "m <= n \<longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_vector arr) j m = 0"
    89 apply (induct arr)
    90 apply (auto)
    91 apply (frule sorted_spvec_cons2,simp)+
    92 apply (frule sorted_spvec_cons3, simp)
    93 done
    94 
    95 lemma sorted_sparse_row_matrix_zero[rule_format]: "m <= n \<longrightarrow> sorted_spvec ((n,a)#arr) \<longrightarrow> Rep_matrix (sparse_row_matrix arr) m j = 0"
    96   apply (induct arr)
    97   apply (auto)
    98   apply (frule sorted_spvec_cons2, simp)
    99   apply (frule sorted_spvec_cons3, simp)
   100   apply (simp add: sparse_row_matrix_cons neg_def)
   101   done
   102 
   103 primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec" where
   104   "minus_spvec [] = []"
   105   | "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
   106 
   107 primrec abs_spvec ::  "('a::lordered_ab_group_add_abs) spvec \<Rightarrow> 'a spvec" where
   108   "abs_spvec [] = []"
   109   | "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
   110 
   111 lemma sparse_row_vector_minus: 
   112   "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
   113   apply (induct v)
   114   apply (simp_all add: sparse_row_vector_cons)
   115   apply (simp add: Rep_matrix_inject[symmetric])
   116   apply (rule ext)+
   117   apply simp
   118   done
   119 
   120 instance matrix :: (lordered_ab_group_add_abs) lordered_ab_group_add_abs
   121 apply default
   122 unfolding abs_matrix_def .. (*FIXME move*)
   123 
   124 lemma sparse_row_vector_abs:
   125   "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (abs_spvec v) = abs (sparse_row_vector v)"
   126   apply (induct v)
   127   apply simp_all
   128   apply (frule_tac sorted_spvec_cons1, simp)
   129   apply (simp only: Rep_matrix_inject[symmetric])
   130   apply (rule ext)+
   131   apply auto
   132   apply (subgoal_tac "Rep_matrix (sparse_row_vector v) 0 a = 0")
   133   apply (simp)
   134   apply (rule sorted_sparse_row_vector_zero)
   135   apply auto
   136   done
   137 
   138 lemma sorted_spvec_minus_spvec:
   139   "sorted_spvec v \<Longrightarrow> sorted_spvec (minus_spvec v)"
   140   apply (induct v)
   141   apply (simp)
   142   apply (frule sorted_spvec_cons1, simp)
   143   apply (simp add: sorted_spvec.simps split:list.split_asm)
   144   done
   145 
   146 lemma sorted_spvec_abs_spvec:
   147   "sorted_spvec v \<Longrightarrow> sorted_spvec (abs_spvec v)"
   148   apply (induct v)
   149   apply (simp)
   150   apply (frule sorted_spvec_cons1, simp)
   151   apply (simp add: sorted_spvec.simps split:list.split_asm)
   152   done
   153   
   154 definition
   155   "smult_spvec y = map (% a. (fst a, y * snd a))"  
   156 
   157 lemma smult_spvec_empty[simp]: "smult_spvec y [] = []"
   158   by (simp add: smult_spvec_def)
   159 
   160 lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"
   161   by (simp add: smult_spvec_def)
   162 
   163 consts addmult_spvec :: "('a::ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
   164 recdef addmult_spvec "measure (% (y, a, b). length a + (length b))"
   165   "addmult_spvec (y, arr, []) = arr"
   166   "addmult_spvec (y, [], brr) = smult_spvec y brr"
   167   "addmult_spvec (y, a#arr, b#brr) = (
   168     if (fst a) < (fst b) then (a#(addmult_spvec (y, arr, b#brr))) 
   169     else (if (fst b < fst a) then ((fst b, y * (snd b))#(addmult_spvec (y, a#arr, brr)))
   170     else ((fst a, (snd a)+ y*(snd b))#(addmult_spvec (y, arr,brr)))))"
   171 
   172 lemma addmult_spvec_empty1[simp]: "addmult_spvec (y, [], a) = smult_spvec y a"
   173   by (induct a) auto
   174 
   175 lemma addmult_spvec_empty2[simp]: "addmult_spvec (y, a, []) = a"
   176   by (induct a) auto
   177 
   178 lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \<Longrightarrow> (f::'a\<Rightarrow>('a::lordered_ring)) 0 = 0 \<Longrightarrow> 
   179   sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)"
   180   apply (induct a)
   181   apply (simp_all add: apply_matrix_add)
   182   done
   183 
   184 lemma sparse_row_vector_smult: "sparse_row_vector (smult_spvec y a) = scalar_mult y (sparse_row_vector a)"
   185   apply (induct a)
   186   apply (simp_all add: smult_spvec_cons scalar_mult_add)
   187   done
   188 
   189 lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring, a, b)) = 
   190   (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
   191   apply (rule addmult_spvec.induct[of _ y])
   192   apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+
   193   done
   194 
   195 lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
   196   apply (auto simp add: smult_spvec_def)
   197   apply (induct a)
   198   apply (auto simp add: sorted_spvec.simps split:list.split_asm)
   199   done
   200 
   201 lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); 
   202   sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec (y, (a, b) # arr, brr))"  
   203   apply (induct brr)
   204   apply (auto simp add: sorted_spvec.simps)
   205   apply (simp split: list.split)
   206   apply (auto)
   207   apply (simp split: list.split)
   208   apply (auto)
   209   done
   210 
   211 lemma sorted_spvec_addmult_spvec_helper2: 
   212  "\<lbrakk>sorted_spvec (addmult_spvec (y, arr, (aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\<rbrakk>
   213        \<Longrightarrow> sorted_spvec ((a, b) # addmult_spvec (y, arr, (aa, ba) # brr))"
   214   apply (induct arr)
   215   apply (auto simp add: smult_spvec_def sorted_spvec.simps)
   216   apply (simp split: list.split)
   217   apply (auto)
   218   done
   219 
   220 lemma sorted_spvec_addmult_spvec_helper3[rule_format]:
   221   "sorted_spvec (addmult_spvec (y, arr, brr)) \<longrightarrow> sorted_spvec ((aa, b) # arr) \<longrightarrow> sorted_spvec ((aa, ba) # brr)
   222      \<longrightarrow> sorted_spvec ((aa, b + y * ba) # (addmult_spvec (y, arr, brr)))"
   223   apply (rule addmult_spvec.induct[of _ y arr brr])
   224   apply (simp_all add: sorted_spvec.simps smult_spvec_def)
   225   done
   226 
   227 lemma sorted_addmult_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (addmult_spvec (y, a, b))"
   228   apply (rule addmult_spvec.induct[of _ y a b])
   229   apply (simp_all add: sorted_smult_spvec)
   230   apply (rule conjI, intro strip)
   231   apply (case_tac "~(a < aa)")
   232   apply (simp_all)
   233   apply (frule_tac as=brr in sorted_spvec_cons1)
   234   apply (simp add: sorted_spvec_addmult_spvec_helper)
   235   apply (intro strip | rule conjI)+
   236   apply (frule_tac as=arr in sorted_spvec_cons1)
   237   apply (simp add: sorted_spvec_addmult_spvec_helper2)
   238   apply (intro strip)
   239   apply (frule_tac as=arr in sorted_spvec_cons1)
   240   apply (frule_tac as=brr in sorted_spvec_cons1)
   241   apply (simp)
   242   apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
   243   done
   244 
   245 consts 
   246   mult_spvec_spmat :: "('a::lordered_ring) spvec * 'a spvec * 'a spmat  \<Rightarrow> 'a spvec"
   247 recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))"
   248   "mult_spvec_spmat (c, [], brr) = c"
   249   "mult_spvec_spmat (c, arr, []) = c"
   250   "mult_spvec_spmat (c, a#arr, b#brr) = (
   251      if ((fst a) < (fst b)) then (mult_spvec_spmat (c, arr, b#brr))
   252      else (if ((fst b) < (fst a)) then (mult_spvec_spmat (c, a#arr, brr)) 
   253      else (mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))))"
   254 
   255 lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \<longrightarrow> sorted_spvec B \<longrightarrow> 
   256   sparse_row_vector (mult_spvec_spmat (c, a, B)) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
   257 proof -
   258   have comp_1: "!! a b. a < b \<Longrightarrow> Suc 0 <= nat ((int b)-(int a))" by arith
   259   have not_iff: "!! a b. a = b \<Longrightarrow> (~ a) = (~ b)" by simp
   260   have max_helper: "!! a b. ~ (a <= max (Suc a) b) \<Longrightarrow> False"
   261     by arith
   262   {
   263     fix a 
   264     fix v
   265     assume a:"a < nrows(sparse_row_vector v)"
   266     have b:"nrows(sparse_row_vector v) <= 1" by simp
   267     note dummy = less_le_trans[of a "nrows (sparse_row_vector v)" 1, OF a b]   
   268     then have "a = 0" by simp
   269   }
   270   note nrows_helper = this
   271   show ?thesis
   272     apply (rule mult_spvec_spmat.induct)
   273     apply simp+
   274     apply (rule conjI)
   275     apply (intro strip)
   276     apply (frule_tac as=brr in sorted_spvec_cons1)
   277     apply (simp add: algebra_simps sparse_row_matrix_cons)
   278     apply (simplesubst Rep_matrix_zero_imp_mult_zero) 
   279     apply (simp)
   280     apply (intro strip)
   281     apply (rule disjI2)
   282     apply (intro strip)
   283     apply (subst nrows)
   284     apply (rule  order_trans[of _ 1])
   285     apply (simp add: comp_1)+
   286     apply (subst Rep_matrix_zero_imp_mult_zero)
   287     apply (intro strip)
   288     apply (case_tac "k <= aa")
   289     apply (rule_tac m1 = k and n1 = a and a1 = b in ssubst[OF sorted_sparse_row_vector_zero])
   290     apply (simp_all)
   291     apply (rule impI)
   292     apply (rule disjI2)
   293     apply (rule nrows)
   294     apply (rule order_trans[of _ 1])
   295     apply (simp_all add: comp_1)
   296     
   297     apply (intro strip | rule conjI)+
   298     apply (frule_tac as=arr in sorted_spvec_cons1)
   299     apply (simp add: algebra_simps)
   300     apply (subst Rep_matrix_zero_imp_mult_zero)
   301     apply (simp)
   302     apply (rule disjI2)
   303     apply (intro strip)
   304     apply (simp add: sparse_row_matrix_cons neg_def)
   305     apply (case_tac "a <= aa")  
   306     apply (erule sorted_sparse_row_matrix_zero)  
   307     apply (simp_all)
   308     apply (intro strip)
   309     apply (case_tac "a=aa")
   310     apply (simp_all)
   311     apply (frule_tac as=arr in sorted_spvec_cons1)
   312     apply (frule_tac as=brr in sorted_spvec_cons1)
   313     apply (simp add: sparse_row_matrix_cons algebra_simps sparse_row_vector_addmult_spvec)
   314     apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
   315     apply (auto)
   316     apply (rule sorted_sparse_row_matrix_zero)
   317     apply (simp_all)
   318     apply (rule_tac A1 = "sparse_row_vector arr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
   319     apply (auto)
   320     apply (rule_tac m=k and n = aa and a = b and arr=arr in sorted_sparse_row_vector_zero)
   321     apply (simp_all)
   322     apply (simp add: neg_def)
   323     apply (drule nrows_notzero)
   324     apply (drule nrows_helper)
   325     apply (arith)
   326     
   327     apply (subst Rep_matrix_inject[symmetric])
   328     apply (rule ext)+
   329     apply (simp)
   330     apply (subst Rep_matrix_mult)
   331     apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
   332     apply (simp_all)
   333     apply (intro strip, rule conjI)
   334     apply (intro strip)
   335     apply (drule_tac max_helper)
   336     apply (simp)
   337     apply (auto)
   338     apply (rule zero_imp_mult_zero)
   339     apply (rule disjI2)
   340     apply (rule nrows)
   341     apply (rule order_trans[of _ 1])
   342     apply (simp)
   343     apply (simp)
   344     done
   345 qed
   346 
   347 lemma sorted_mult_spvec_spmat[rule_format]: 
   348   "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat (c, a, B))"
   349   apply (rule mult_spvec_spmat.induct[of _ c a B])
   350   apply (simp_all add: sorted_addmult_spvec)
   351   done
   352 
   353 consts 
   354   mult_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   355 
   356 primrec 
   357   "mult_spmat [] A = []"
   358   "mult_spmat (a#as) A = (fst a, mult_spvec_spmat ([], snd a, A))#(mult_spmat as A)"
   359 
   360 lemma sparse_row_mult_spmat[rule_format]: 
   361   "sorted_spmat A \<longrightarrow> sorted_spvec B \<longrightarrow> sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)"
   362   apply (induct A)
   363   apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat algebra_simps move_matrix_mult)
   364   done
   365 
   366 lemma sorted_spvec_mult_spmat[rule_format]:
   367   "sorted_spvec (A::('a::lordered_ring) spmat) \<longrightarrow> sorted_spvec (mult_spmat A B)"
   368   apply (induct A)
   369   apply (auto)
   370   apply (drule sorted_spvec_cons1, simp)
   371   apply (case_tac A)
   372   apply (auto simp add: sorted_spvec.simps)
   373   done
   374 
   375 lemma sorted_spmat_mult_spmat[rule_format]:
   376   "sorted_spmat (B::('a::lordered_ring) spmat) \<longrightarrow> sorted_spmat (mult_spmat A B)"
   377   apply (induct A)
   378   apply (auto simp add: sorted_mult_spvec_spmat) 
   379   done
   380 
   381 consts
   382   add_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> 'a spvec"
   383   add_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> 'a spmat"
   384 
   385 recdef add_spvec "measure (% (a, b). length a + (length b))"
   386   "add_spvec (arr, []) = arr"
   387   "add_spvec ([], brr) = brr"
   388   "add_spvec (a#arr, b#brr) = (
   389   if (fst a) < (fst b) then (a#(add_spvec (arr, b#brr))) 
   390      else (if (fst b < fst a) then (b#(add_spvec (a#arr, brr)))
   391      else ((fst a, (snd a)+(snd b))#(add_spvec (arr,brr)))))"
   392 
   393 lemma add_spvec_empty1[simp]: "add_spvec ([], a) = a"
   394   by (induct a, auto)
   395 
   396 lemma add_spvec_empty2[simp]: "add_spvec (a, []) = a"
   397   by (induct a, auto)
   398 
   399 lemma sparse_row_vector_add: "sparse_row_vector (add_spvec (a,b)) = (sparse_row_vector a) + (sparse_row_vector b)"
   400   apply (rule add_spvec.induct[of _ a b])
   401   apply (simp_all add: singleton_matrix_add)
   402   done
   403 
   404 recdef add_spmat "measure (% (A,B). (length A)+(length B))"
   405   "add_spmat ([], bs) = bs"
   406   "add_spmat (as, []) = as"
   407   "add_spmat (a#as, b#bs) = (
   408   if fst a < fst b then 
   409     (a#(add_spmat (as, b#bs)))
   410   else (if fst b < fst a then
   411     (b#(add_spmat (a#as, bs)))
   412   else
   413     ((fst a, add_spvec (snd a, snd b))#(add_spmat (as, bs)))))"
   414 
   415 lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat (A, B)) = (sparse_row_matrix A) + (sparse_row_matrix B)"
   416   apply (rule add_spmat.induct)
   417   apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
   418   done
   419 
   420 lemmas [code] = sparse_row_add_spmat [symmetric]
   421 lemmas [code] = sparse_row_vector_add [symmetric]
   422 
   423 lemma sorted_add_spvec_helper1[rule_format]: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
   424   proof - 
   425     have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spvec (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
   426       by (rule add_spvec.induct[of _ _ brr], auto)
   427     then show ?thesis
   428       by (case_tac brr, auto)
   429   qed
   430 
   431 lemma sorted_add_spmat_helper1[rule_format]: "add_spmat ((a,b)#arr, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (brr \<noteq> [] & ab = fst (hd brr)))"
   432   proof - 
   433     have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spmat (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
   434       by (rule add_spmat.induct[of _ _ brr], auto)
   435     then show ?thesis
   436       by (case_tac brr, auto)
   437   qed
   438 
   439 lemma sorted_add_spvec_helper[rule_format]: "add_spvec (arr, brr) = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
   440   apply (rule add_spvec.induct[of _ arr brr])
   441   apply (auto)
   442   done
   443 
   444 lemma sorted_add_spmat_helper[rule_format]: "add_spmat (arr, brr) = (ab, bb) # list \<longrightarrow> ((arr \<noteq> [] & ab = fst (hd arr)) | (brr \<noteq> [] & ab = fst (hd brr)))"
   445   apply (rule add_spmat.induct[of _ arr brr])
   446   apply (auto)
   447   done
   448 
   449 lemma add_spvec_commute: "add_spvec (a, b) = add_spvec (b, a)"
   450   by (rule add_spvec.induct[of _ a b], auto)
   451 
   452 lemma add_spmat_commute: "add_spmat (a, b) = add_spmat (b, a)"
   453   apply (rule add_spmat.induct[of _ a b])
   454   apply (simp_all add: add_spvec_commute)
   455   done
   456   
   457 lemma sorted_add_spvec_helper2: "add_spvec ((a,b)#arr, brr) = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
   458   apply (drule sorted_add_spvec_helper1)
   459   apply (auto)
   460   apply (case_tac brr)
   461   apply (simp_all)
   462   apply (drule_tac sorted_spvec_cons3)
   463   apply (simp)
   464   done
   465 
   466 lemma sorted_add_spmat_helper2: "add_spmat ((a,b)#arr, brr) = (ab, bb) # list \<Longrightarrow> aa < a \<Longrightarrow> sorted_spvec ((aa, ba) # brr) \<Longrightarrow> aa < ab"
   467   apply (drule sorted_add_spmat_helper1)
   468   apply (auto)
   469   apply (case_tac brr)
   470   apply (simp_all)
   471   apply (drule_tac sorted_spvec_cons3)
   472   apply (simp)
   473   done
   474 
   475 lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (add_spvec (a, b))"
   476   apply (rule add_spvec.induct[of _ a b])
   477   apply (simp_all)
   478   apply (rule conjI)
   479   apply (intro strip)
   480   apply (simp)
   481   apply (frule_tac as=brr in sorted_spvec_cons1)
   482   apply (simp)
   483   apply (subst sorted_spvec_step)
   484   apply (simp split: list.split)
   485   apply (clarify, simp)
   486   apply (simp add: sorted_add_spvec_helper2)
   487   apply (clarify)
   488   apply (rule conjI)
   489   apply (case_tac "a=aa")
   490   apply (simp)
   491   apply (clarify)
   492   apply (frule_tac as=arr in sorted_spvec_cons1, simp)
   493   apply (subst sorted_spvec_step)
   494   apply (simp split: list.split)
   495   apply (clarify, simp)
   496   apply (simp add: sorted_add_spvec_helper2 add_spvec_commute)
   497   apply (case_tac "a=aa")
   498   apply (simp_all)
   499   apply (clarify)
   500   apply (frule_tac as=arr in sorted_spvec_cons1)
   501   apply (frule_tac as=brr in sorted_spvec_cons1)
   502   apply (simp)
   503   apply (subst sorted_spvec_step)
   504   apply (simp split: list.split)
   505   apply (clarify, simp)
   506   apply (drule_tac sorted_add_spvec_helper)
   507   apply (auto)
   508   apply (case_tac arr)
   509   apply (simp_all)
   510   apply (drule sorted_spvec_cons3)
   511   apply (simp)
   512   apply (case_tac brr)
   513   apply (simp_all)
   514   apply (drule sorted_spvec_cons3)
   515   apply (simp)
   516   done
   517 
   518 lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \<longrightarrow> sorted_spvec B \<longrightarrow> sorted_spvec (add_spmat (A, B))"
   519   apply (rule add_spmat.induct[of _ A B])
   520   apply (simp_all)
   521   apply (rule conjI)
   522   apply (intro strip)
   523   apply (simp)
   524   apply (frule_tac as=bs in sorted_spvec_cons1)
   525   apply (simp)
   526   apply (subst sorted_spvec_step)
   527   apply (simp split: list.split)
   528   apply (clarify, simp)
   529   apply (simp add: sorted_add_spmat_helper2)
   530   apply (clarify)
   531   apply (rule conjI)
   532   apply (case_tac "a=aa")
   533   apply (simp)
   534   apply (clarify)
   535   apply (frule_tac as=as in sorted_spvec_cons1, simp)
   536   apply (subst sorted_spvec_step)
   537   apply (simp split: list.split)
   538   apply (clarify, simp)
   539   apply (simp add: sorted_add_spmat_helper2 add_spmat_commute)
   540   apply (case_tac "a=aa")
   541   apply (simp_all)
   542   apply (clarify)
   543   apply (frule_tac as=as in sorted_spvec_cons1)
   544   apply (frule_tac as=bs in sorted_spvec_cons1)
   545   apply (simp)
   546   apply (subst sorted_spvec_step)
   547   apply (simp split: list.split)
   548   apply (clarify, simp)
   549   apply (drule_tac sorted_add_spmat_helper)
   550   apply (auto)
   551   apply (case_tac as)
   552   apply (simp_all)
   553   apply (drule sorted_spvec_cons3)
   554   apply (simp)
   555   apply (case_tac bs)
   556   apply (simp_all)
   557   apply (drule sorted_spvec_cons3)
   558   apply (simp)
   559   done
   560 
   561 lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spmat (add_spmat (A, B))"
   562   apply (rule add_spmat.induct[of _ A B])
   563   apply (simp_all add: sorted_spvec_add_spvec)
   564   done
   565 
   566 consts
   567   le_spvec :: "('a::lordered_ab_group_add) spvec * 'a spvec \<Rightarrow> bool" 
   568   le_spmat :: "('a::lordered_ab_group_add) spmat * 'a spmat \<Rightarrow> bool" 
   569 
   570 recdef le_spvec "measure (% (a,b). (length a) + (length b))" 
   571   "le_spvec ([], []) = True"
   572   "le_spvec (a#as, []) = ((snd a <= 0) & (le_spvec (as, [])))"
   573   "le_spvec ([], b#bs) = ((0 <= snd b) & (le_spvec ([], bs)))"
   574   "le_spvec (a#as, b#bs) = (
   575   if (fst a < fst b) then 
   576     ((snd a <= 0) & (le_spvec (as, b#bs)))
   577   else (if (fst b < fst a) then
   578     ((0 <= snd b) & (le_spvec (a#as, bs)))
   579   else 
   580     ((snd a <= snd b) & (le_spvec (as, bs)))))"
   581 
   582 recdef le_spmat "measure (% (a,b). (length a) + (length b))"
   583   "le_spmat ([], []) = True"
   584   "le_spmat (a#as, []) = (le_spvec (snd a, []) & (le_spmat (as, [])))"
   585   "le_spmat ([], b#bs) = (le_spvec ([], snd b) & (le_spmat ([], bs)))"
   586   "le_spmat (a#as, b#bs) = (
   587   if fst a < fst b then
   588     (le_spvec(snd a,[]) & le_spmat(as, b#bs))
   589   else (if (fst b < fst a) then 
   590     (le_spvec([], snd b) & le_spmat(a#as, bs))
   591   else
   592     (le_spvec(snd a, snd b) & le_spmat (as, bs))))"
   593 
   594 constdefs
   595   disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
   596   "disj_matrices A B == (! j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))"  
   597 
   598 declare [[simp_depth_limit = 6]]
   599 
   600 lemma disj_matrices_contr1: "disj_matrices A B \<Longrightarrow> Rep_matrix A j i \<noteq> 0 \<Longrightarrow> Rep_matrix B j i = 0"
   601    by (simp add: disj_matrices_def)
   602 
   603 lemma disj_matrices_contr2: "disj_matrices A B \<Longrightarrow> Rep_matrix B j i \<noteq> 0 \<Longrightarrow> Rep_matrix A j i = 0"
   604    by (simp add: disj_matrices_def)
   605 
   606 
   607 lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
   608   (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group_add) matrix))"
   609   apply (auto)
   610   apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
   611   apply (intro strip)
   612   apply (erule conjE)+
   613   apply (drule_tac j=j and i=i in spec2)+
   614   apply (case_tac "Rep_matrix B j i = 0")
   615   apply (case_tac "Rep_matrix D j i = 0")
   616   apply (simp_all)
   617   apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
   618   apply (intro strip)
   619   apply (erule conjE)+
   620   apply (drule_tac j=j and i=i in spec2)+
   621   apply (case_tac "Rep_matrix A j i = 0")
   622   apply (case_tac "Rep_matrix C j i = 0")
   623   apply (simp_all)
   624   apply (erule add_mono)
   625   apply (assumption)
   626   done
   627 
   628 lemma disj_matrices_zero1[simp]: "disj_matrices 0 B"
   629 by (simp add: disj_matrices_def)
   630 
   631 lemma disj_matrices_zero2[simp]: "disj_matrices A 0"
   632 by (simp add: disj_matrices_def)
   633 
   634 lemma disj_matrices_commute: "disj_matrices A B = disj_matrices B A"
   635 by (auto simp add: disj_matrices_def)
   636 
   637 lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
   638   (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group_add) matrix) <= 0)"
   639 by (rule disj_matrices_add[of A B 0 0, simplified])
   640  
   641 lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
   642   (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group_add) matrix))"
   643 by (rule disj_matrices_add[of 0 0 A B, simplified])
   644 
   645 lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
   646   (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group_add) matrix))"
   647 by (auto simp add: disj_matrices_add[of 0 A B C, simplified])
   648 
   649 lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
   650   (B + A <= C) = (A <= C &  (B::('a::lordered_ab_group_add) matrix) <= 0)"
   651 by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
   652 
   653 lemma disj_sparse_row_singleton: "i <= j \<Longrightarrow> sorted_spvec((j,y)#v) \<Longrightarrow> disj_matrices (sparse_row_vector v) (singleton_matrix 0 i x)"
   654   apply (simp add: disj_matrices_def)
   655   apply (rule conjI)
   656   apply (rule neg_imp)
   657   apply (simp)
   658   apply (intro strip)
   659   apply (rule sorted_sparse_row_vector_zero)
   660   apply (simp_all)
   661   apply (intro strip)
   662   apply (rule sorted_sparse_row_vector_zero)
   663   apply (simp_all)
   664   done 
   665 
   666 lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lordered_ab_group_add) matrix) (B+C)"
   667   apply (simp add: disj_matrices_def)
   668   apply (auto)
   669   apply (drule_tac j=j and i=i in spec2)+
   670   apply (case_tac "Rep_matrix B j i = 0")
   671   apply (case_tac "Rep_matrix C j i = 0")
   672   apply (simp_all)
   673   done
   674 
   675 lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lordered_ab_group_add) matrix)" 
   676   by (simp add: disj_matrices_x_add disj_matrices_commute)
   677 
   678 lemma disj_singleton_matrices[simp]: "disj_matrices (singleton_matrix j i x) (singleton_matrix u v y) = (j \<noteq> u | i \<noteq> v | x = 0 | y = 0)" 
   679   by (auto simp add: disj_matrices_def)
   680 
   681 lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]: 
   682   "j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
   683   apply (auto simp add: neg_def disj_matrices_def)
   684   apply (drule nrows_notzero)
   685   apply (drule less_le_trans[OF _ nrows_spvec])
   686   apply (subgoal_tac "ja = j")
   687   apply (simp add: sorted_sparse_row_matrix_zero)
   688   apply (arith)
   689   apply (rule nrows)
   690   apply (rule order_trans[of _ 1 _])
   691   apply (simp)
   692   apply (case_tac "nat (int ja - int j) = 0")
   693   apply (case_tac "ja = j")
   694   apply (simp add: sorted_sparse_row_matrix_zero)
   695   apply arith+
   696   done
   697 
   698 lemma disj_move_sparse_row_vector_twice:
   699   "j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)"
   700   apply (auto simp add: neg_def disj_matrices_def)
   701   apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
   702   done
   703 
   704 lemma le_spvec_iff_sparse_row_le[rule_format]: "(sorted_spvec a) \<longrightarrow> (sorted_spvec b) \<longrightarrow> (le_spvec (a,b)) = (sparse_row_vector a <= sparse_row_vector b)"
   705   apply (rule le_spvec.induct)
   706   apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le 
   707     disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
   708   apply (rule conjI, intro strip)
   709   apply (simp add: sorted_spvec_cons1)
   710   apply (subst disj_matrices_add_x_le)
   711   apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute)
   712   apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
   713   apply (simp, blast)
   714   apply (intro strip, rule conjI, intro strip)
   715   apply (simp add: sorted_spvec_cons1)
   716   apply (subst disj_matrices_add_le_x)
   717   apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_sparse_row_singleton[OF less_imp_le] disj_matrices_commute disj_matrices_x_add)
   718   apply (blast)
   719   apply (intro strip)
   720   apply (simp add: sorted_spvec_cons1)
   721   apply (case_tac "a=aa", simp_all)
   722   apply (subst disj_matrices_add)
   723   apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
   724   done
   725 
   726 lemma le_spvec_empty2_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec (b,[]) = (sparse_row_vector b <= 0))"
   727   apply (induct b)
   728   apply (simp_all add: sorted_spvec_cons1)
   729   apply (intro strip)
   730   apply (subst disj_matrices_add_le_zero)
   731   apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
   732   apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
   733   apply (simp_all)
   734   done
   735 
   736 lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec ([],b) = (0 <= sparse_row_vector b))"
   737   apply (induct b)
   738   apply (simp_all add: sorted_spvec_cons1)
   739   apply (intro strip)
   740   apply (subst disj_matrices_add_zero_le)
   741   apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
   742   apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
   743   apply (simp_all)
   744   done
   745 
   746 lemma le_spmat_iff_sparse_row_le[rule_format]: "(sorted_spvec A) \<longrightarrow> (sorted_spmat A) \<longrightarrow> (sorted_spvec B) \<longrightarrow> (sorted_spmat B) \<longrightarrow> 
   747   le_spmat(A, B) = (sparse_row_matrix A <= sparse_row_matrix B)"
   748   apply (rule le_spmat.induct)
   749   apply (simp add: sparse_row_matrix_cons disj_matrices_add_le_zero disj_matrices_add_zero_le disj_move_sparse_vec_mat[OF order_refl] 
   750     disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)+ 
   751   apply (rule conjI, intro strip)
   752   apply (simp add: sorted_spvec_cons1)
   753   apply (subst disj_matrices_add_x_le)
   754   apply (rule disj_matrices_add_x)
   755   apply (simp add: disj_move_sparse_row_vector_twice)
   756   apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
   757   apply (simp add: disj_move_sparse_vec_mat[OF order_refl] disj_matrices_commute)
   758   apply (simp, blast)
   759   apply (intro strip, rule conjI, intro strip)
   760   apply (simp add: sorted_spvec_cons1)
   761   apply (subst disj_matrices_add_le_x)
   762   apply (simp add: disj_move_sparse_vec_mat[OF order_refl])
   763   apply (rule disj_matrices_x_add)
   764   apply (simp add: disj_move_sparse_row_vector_twice)
   765   apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
   766   apply (simp, blast)
   767   apply (intro strip)
   768   apply (case_tac "a=aa")
   769   apply (simp_all)
   770   apply (subst disj_matrices_add)
   771   apply (simp_all add: disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl])
   772   apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le)
   773   done
   774 
   775 declare [[simp_depth_limit = 999]]
   776 
   777 consts 
   778    abs_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
   779    minus_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat"
   780 
   781 primrec
   782   "abs_spmat [] = []"
   783   "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)"
   784 
   785 primrec
   786   "minus_spmat [] = []"
   787   "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)"
   788 
   789 lemma sparse_row_matrix_minus:
   790   "sparse_row_matrix (minus_spmat A) = - (sparse_row_matrix A)"
   791   apply (induct A)
   792   apply (simp_all add: sparse_row_vector_minus sparse_row_matrix_cons)
   793   apply (subst Rep_matrix_inject[symmetric])
   794   apply (rule ext)+
   795   apply simp
   796   done
   797 
   798 lemma Rep_sparse_row_vector_zero: "x \<noteq> 0 \<Longrightarrow> Rep_matrix (sparse_row_vector v) x y = 0"
   799 proof -
   800   assume x:"x \<noteq> 0"
   801   have r:"nrows (sparse_row_vector v) <= Suc 0" by (rule nrows_spvec)
   802   show ?thesis
   803     apply (rule nrows)
   804     apply (subgoal_tac "Suc 0 <= x")
   805     apply (insert r)
   806     apply (simp only:)
   807     apply (insert x)
   808     apply arith
   809     done
   810 qed
   811     
   812 lemma sparse_row_matrix_abs:
   813   "sorted_spvec A \<Longrightarrow> sorted_spmat A \<Longrightarrow> sparse_row_matrix (abs_spmat A) = abs (sparse_row_matrix A)"
   814   apply (induct A)
   815   apply (simp_all add: sparse_row_vector_abs sparse_row_matrix_cons)
   816   apply (frule_tac sorted_spvec_cons1, simp)
   817   apply (simplesubst Rep_matrix_inject[symmetric])
   818   apply (rule ext)+
   819   apply auto
   820   apply (case_tac "x=a")
   821   apply (simp)
   822   apply (simplesubst sorted_sparse_row_matrix_zero)
   823   apply auto
   824   apply (simplesubst Rep_sparse_row_vector_zero)
   825   apply (simp_all add: neg_def)
   826   done
   827 
   828 lemma sorted_spvec_minus_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (minus_spmat A)"
   829   apply (induct A)
   830   apply (simp)
   831   apply (frule sorted_spvec_cons1, simp)
   832   apply (simp add: sorted_spvec.simps split:list.split_asm)
   833   done 
   834 
   835 lemma sorted_spvec_abs_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec (abs_spmat A)" 
   836   apply (induct A)
   837   apply (simp)
   838   apply (frule sorted_spvec_cons1, simp)
   839   apply (simp add: sorted_spvec.simps split:list.split_asm)
   840   done
   841 
   842 lemma sorted_spmat_minus_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (minus_spmat A)"
   843   apply (induct A)
   844   apply (simp_all add: sorted_spvec_minus_spvec)
   845   done
   846 
   847 lemma sorted_spmat_abs_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat (abs_spmat A)"
   848   apply (induct A)
   849   apply (simp_all add: sorted_spvec_abs_spvec)
   850   done
   851 
   852 constdefs
   853   diff_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   854   "diff_spmat A B == add_spmat (A, minus_spmat B)"
   855 
   856 lemma sorted_spmat_diff_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (diff_spmat A B)"
   857   by (simp add: diff_spmat_def sorted_spmat_minus_spmat sorted_spmat_add_spmat)
   858 
   859 lemma sorted_spvec_diff_spmat: "sorted_spvec A \<Longrightarrow> sorted_spvec B \<Longrightarrow> sorted_spvec (diff_spmat A B)"
   860   by (simp add: diff_spmat_def sorted_spvec_minus_spmat sorted_spvec_add_spmat)
   861 
   862 lemma sparse_row_diff_spmat: "sparse_row_matrix (diff_spmat A B ) = (sparse_row_matrix A) - (sparse_row_matrix B)"
   863   by (simp add: diff_spmat_def sparse_row_add_spmat sparse_row_matrix_minus)
   864 
   865 constdefs
   866   sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool"
   867   "sorted_sparse_matrix A == (sorted_spvec A) & (sorted_spmat A)"
   868 
   869 lemma sorted_sparse_matrix_imp_spvec: "sorted_sparse_matrix A \<Longrightarrow> sorted_spvec A"
   870   by (simp add: sorted_sparse_matrix_def)
   871 
   872 lemma sorted_sparse_matrix_imp_spmat: "sorted_sparse_matrix A \<Longrightarrow> sorted_spmat A"
   873   by (simp add: sorted_sparse_matrix_def)
   874 
   875 lemmas sorted_sp_simps = 
   876   sorted_spvec.simps
   877   sorted_spmat.simps
   878   sorted_sparse_matrix_def
   879 
   880 lemma bool1: "(\<not> True) = False"  by blast
   881 lemma bool2: "(\<not> False) = True"  by blast
   882 lemma bool3: "((P\<Colon>bool) \<and> True) = P" by blast
   883 lemma bool4: "(True \<and> (P\<Colon>bool)) = P" by blast
   884 lemma bool5: "((P\<Colon>bool) \<and> False) = False" by blast
   885 lemma bool6: "(False \<and> (P\<Colon>bool)) = False" by blast
   886 lemma bool7: "((P\<Colon>bool) \<or> True) = True" by blast
   887 lemma bool8: "(True \<or> (P\<Colon>bool)) = True" by blast
   888 lemma bool9: "((P\<Colon>bool) \<or> False) = P" by blast
   889 lemma bool10: "(False \<or> (P\<Colon>bool)) = P" by blast
   890 lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10
   891 
   892 lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
   893 
   894 consts
   895   pprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
   896   nprt_spvec :: "('a::{lordered_ab_group_add}) spvec \<Rightarrow> 'a spvec"
   897   pprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
   898   nprt_spmat :: "('a::{lordered_ab_group_add}) spmat \<Rightarrow> 'a spmat"
   899 
   900 primrec
   901   "pprt_spvec [] = []"
   902   "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
   903 
   904 primrec
   905   "nprt_spvec [] = []"
   906   "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
   907 
   908 primrec 
   909   "pprt_spmat [] = []"
   910   "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
   911   (*case (pprt_spvec (snd a)) of [] \<Rightarrow> (pprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(pprt_spmat as))"*)
   912 
   913 primrec 
   914   "nprt_spmat [] = []"
   915   "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
   916   (*case (nprt_spvec (snd a)) of [] \<Rightarrow> (nprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(nprt_spmat as))"*)
   917 
   918 
   919 lemma pprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
   920   apply (simp add: pprt_def sup_matrix_def)
   921   apply (simp add: Rep_matrix_inject[symmetric])
   922   apply (rule ext)+
   923   apply simp
   924   apply (case_tac "Rep_matrix A x xa \<noteq> 0")
   925   apply (simp_all add: disj_matrices_contr1)
   926   done
   927 
   928 lemma nprt_add: "disj_matrices A (B::(_::lordered_ring) matrix) \<Longrightarrow> nprt (A+B) = nprt A + nprt B"
   929   apply (simp add: nprt_def inf_matrix_def)
   930   apply (simp add: Rep_matrix_inject[symmetric])
   931   apply (rule ext)+
   932   apply simp
   933   apply (case_tac "Rep_matrix A x xa \<noteq> 0")
   934   apply (simp_all add: disj_matrices_contr1)
   935   done
   936 
   937 lemma pprt_singleton[simp]: "pprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (pprt x)"
   938   apply (simp add: pprt_def sup_matrix_def)
   939   apply (simp add: Rep_matrix_inject[symmetric])
   940   apply (rule ext)+
   941   apply simp
   942   done
   943 
   944 lemma nprt_singleton[simp]: "nprt (singleton_matrix j i (x::_::lordered_ring)) = singleton_matrix j i (nprt x)"
   945   apply (simp add: nprt_def inf_matrix_def)
   946   apply (simp add: Rep_matrix_inject[symmetric])
   947   apply (rule ext)+
   948   apply simp
   949   done
   950 
   951 lemma less_imp_le: "a < b \<Longrightarrow> a <= (b::_::order)" by (simp add: less_def)
   952 
   953 lemma sparse_row_vector_pprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (pprt_spvec v) = pprt (sparse_row_vector v)"
   954   apply (induct v)
   955   apply (simp_all)
   956   apply (frule sorted_spvec_cons1, auto)
   957   apply (subst pprt_add)
   958   apply (subst disj_matrices_commute)
   959   apply (rule disj_sparse_row_singleton)
   960   apply auto
   961   done
   962 
   963 lemma sparse_row_vector_nprt: "sorted_spvec (v :: 'a::lordered_ring spvec) \<Longrightarrow> sparse_row_vector (nprt_spvec v) = nprt (sparse_row_vector v)"
   964   apply (induct v)
   965   apply (simp_all)
   966   apply (frule sorted_spvec_cons1, auto)
   967   apply (subst nprt_add)
   968   apply (subst disj_matrices_commute)
   969   apply (rule disj_sparse_row_singleton)
   970   apply auto
   971   done
   972   
   973   
   974 lemma pprt_move_matrix: "pprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (pprt A) j i"
   975   apply (simp add: pprt_def)
   976   apply (simp add: sup_matrix_def)
   977   apply (simp add: Rep_matrix_inject[symmetric])
   978   apply (rule ext)+
   979   apply (simp)
   980   done
   981 
   982 lemma nprt_move_matrix: "nprt (move_matrix (A::('a::lordered_ring) matrix) j i) = move_matrix (nprt A) j i"
   983   apply (simp add: nprt_def)
   984   apply (simp add: inf_matrix_def)
   985   apply (simp add: Rep_matrix_inject[symmetric])
   986   apply (rule ext)+
   987   apply (simp)
   988   done
   989 
   990 lemma sparse_row_matrix_pprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (pprt_spmat m) = pprt (sparse_row_matrix m)"
   991   apply (induct m)
   992   apply simp
   993   apply simp
   994   apply (frule sorted_spvec_cons1)
   995   apply (simp add: sparse_row_matrix_cons sparse_row_vector_pprt)
   996   apply (subst pprt_add)
   997   apply (subst disj_matrices_commute)
   998   apply (rule disj_move_sparse_vec_mat)
   999   apply auto
  1000   apply (simp add: sorted_spvec.simps)
  1001   apply (simp split: list.split)
  1002   apply auto
  1003   apply (simp add: pprt_move_matrix)
  1004   done
  1005 
  1006 lemma sparse_row_matrix_nprt: "sorted_spvec (m :: 'a::lordered_ring spmat) \<Longrightarrow> sorted_spmat m \<Longrightarrow> sparse_row_matrix (nprt_spmat m) = nprt (sparse_row_matrix m)"
  1007   apply (induct m)
  1008   apply simp
  1009   apply simp
  1010   apply (frule sorted_spvec_cons1)
  1011   apply (simp add: sparse_row_matrix_cons sparse_row_vector_nprt)
  1012   apply (subst nprt_add)
  1013   apply (subst disj_matrices_commute)
  1014   apply (rule disj_move_sparse_vec_mat)
  1015   apply auto
  1016   apply (simp add: sorted_spvec.simps)
  1017   apply (simp split: list.split)
  1018   apply auto
  1019   apply (simp add: nprt_move_matrix)
  1020   done
  1021 
  1022 lemma sorted_pprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (pprt_spvec v)"
  1023   apply (induct v)
  1024   apply (simp)
  1025   apply (frule sorted_spvec_cons1)
  1026   apply simp
  1027   apply (simp add: sorted_spvec.simps split:list.split_asm)
  1028   done
  1029 
  1030 lemma sorted_nprt_spvec: "sorted_spvec v \<Longrightarrow> sorted_spvec (nprt_spvec v)"
  1031   apply (induct v)
  1032   apply (simp)
  1033   apply (frule sorted_spvec_cons1)
  1034   apply simp
  1035   apply (simp add: sorted_spvec.simps split:list.split_asm)
  1036   done
  1037 
  1038 lemma sorted_spvec_pprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (pprt_spmat m)"
  1039   apply (induct m)
  1040   apply (simp)
  1041   apply (frule sorted_spvec_cons1)
  1042   apply simp
  1043   apply (simp add: sorted_spvec.simps split:list.split_asm)
  1044   done
  1045 
  1046 lemma sorted_spvec_nprt_spmat: "sorted_spvec m \<Longrightarrow> sorted_spvec (nprt_spmat m)"
  1047   apply (induct m)
  1048   apply (simp)
  1049   apply (frule sorted_spvec_cons1)
  1050   apply simp
  1051   apply (simp add: sorted_spvec.simps split:list.split_asm)
  1052   done
  1053 
  1054 lemma sorted_spmat_pprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (pprt_spmat m)"
  1055   apply (induct m)
  1056   apply (simp_all add: sorted_pprt_spvec)
  1057   done
  1058 
  1059 lemma sorted_spmat_nprt_spmat: "sorted_spmat m \<Longrightarrow> sorted_spmat (nprt_spmat m)"
  1060   apply (induct m)
  1061   apply (simp_all add: sorted_nprt_spvec)
  1062   done
  1063 
  1064 constdefs
  1065   mult_est_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
  1066   "mult_est_spmat r1 r2 s1 s2 == 
  1067   add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2), add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2), 
  1068   add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1), mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"  
  1069 
  1070 lemmas sparse_row_matrix_op_simps =
  1071   sorted_sparse_matrix_imp_spmat sorted_sparse_matrix_imp_spvec
  1072   sparse_row_add_spmat sorted_spvec_add_spmat sorted_spmat_add_spmat
  1073   sparse_row_diff_spmat sorted_spvec_diff_spmat sorted_spmat_diff_spmat
  1074   sparse_row_matrix_minus sorted_spvec_minus_spmat sorted_spmat_minus_spmat
  1075   sparse_row_mult_spmat sorted_spvec_mult_spmat sorted_spmat_mult_spmat
  1076   sparse_row_matrix_abs sorted_spvec_abs_spmat sorted_spmat_abs_spmat
  1077   le_spmat_iff_sparse_row_le
  1078   sparse_row_matrix_pprt sorted_spvec_pprt_spmat sorted_spmat_pprt_spmat
  1079   sparse_row_matrix_nprt sorted_spvec_nprt_spmat sorted_spmat_nprt_spmat
  1080 
  1081 lemma zero_eq_Numeral0: "(0::_::number_ring) = Numeral0" by simp
  1082 
  1083 lemmas sparse_row_matrix_arith_simps[simplified zero_eq_Numeral0] = 
  1084   mult_spmat.simps mult_spvec_spmat.simps 
  1085   addmult_spvec.simps 
  1086   smult_spvec_empty smult_spvec_cons
  1087   add_spmat.simps add_spvec.simps
  1088   minus_spmat.simps minus_spvec.simps
  1089   abs_spmat.simps abs_spvec.simps
  1090   diff_spmat_def
  1091   le_spmat.simps le_spvec.simps
  1092   pprt_spmat.simps pprt_spvec.simps
  1093   nprt_spmat.simps nprt_spvec.simps
  1094   mult_est_spmat_def
  1095 
  1096 
  1097 (*lemma spm_linprog_dual_estimate_1:
  1098   assumes  
  1099   "sorted_sparse_matrix A1"
  1100   "sorted_sparse_matrix A2"
  1101   "sorted_sparse_matrix c1"
  1102   "sorted_sparse_matrix c2"
  1103   "sorted_sparse_matrix y"
  1104   "sorted_spvec b"
  1105   "sorted_spvec r"
  1106   "le_spmat ([], y)"
  1107   "A * x \<le> sparse_row_matrix (b::('a::lordered_ring) spmat)"
  1108   "sparse_row_matrix A1 <= A"
  1109   "A <= sparse_row_matrix A2"
  1110   "sparse_row_matrix c1 <= c"
  1111   "c <= sparse_row_matrix c2"
  1112   "abs x \<le> sparse_row_matrix r"
  1113   shows
  1114   "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), 
  1115   abs_spmat (diff_spmat (mult_spmat y A1) c1)), diff_spmat c2 c1)) r))"
  1116   by (insert prems, simp add: sparse_row_matrix_op_simps linprog_dual_estimate_1[where A=A])
  1117 *)
  1118 
  1119 end