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