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