src/HOL/Matrix/SparseMatrix.thy
author obua
Tue Jun 29 10:07:56 2004 +0200 (2004-06-29)
changeset 15009 8c89f588c7aa
child 15178 5f621aa35c25
permissions -rw-r--r--
support for sparse matrices
obua@15009
     1
theory SparseMatrix = Matrix:
obua@15009
     2
obua@15009
     3
types 
obua@15009
     4
  'a spvec = "(nat * 'a) list"
obua@15009
     5
  'a spmat = "('a spvec) spvec"
obua@15009
     6
obua@15009
     7
consts
obua@15009
     8
  sparse_row_vector :: "('a::lordered_ring) spvec \<Rightarrow> 'a matrix"
obua@15009
     9
  sparse_row_matrix :: "('a::lordered_ring) spmat \<Rightarrow> 'a matrix"
obua@15009
    10
obua@15009
    11
defs
obua@15009
    12
  sparse_row_vector_def : "sparse_row_vector arr == foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
obua@15009
    13
  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"
obua@15009
    14
obua@15009
    15
lemma sparse_row_vector_empty[simp]: "sparse_row_vector [] = 0"
obua@15009
    16
  by (simp add: sparse_row_vector_def)
obua@15009
    17
obua@15009
    18
lemma sparse_row_matrix_empty[simp]: "sparse_row_matrix [] = 0"
obua@15009
    19
  by (simp add: sparse_row_matrix_def)
obua@15009
    20
obua@15009
    21
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))"
obua@15009
    22
  by (induct l, auto)
obua@15009
    23
obua@15009
    24
lemma sparse_row_vector_cons[simp]: "sparse_row_vector (a#arr) = (singleton_matrix 0 (fst a) (snd a)) + (sparse_row_vector arr)"
obua@15009
    25
  apply (induct arr)
obua@15009
    26
  apply (auto simp add: sparse_row_vector_def)
obua@15009
    27
  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"])
obua@15009
    28
  done
obua@15009
    29
obua@15009
    30
lemma sparse_row_vector_append[simp]: "sparse_row_vector (a @ b) = (sparse_row_vector a) + (sparse_row_vector b)"
obua@15009
    31
  by (induct a, auto)
obua@15009
    32
obua@15009
    33
lemma nrows_spvec[simp]: "nrows (sparse_row_vector x) <= (Suc 0)"
obua@15009
    34
  apply (induct x)
obua@15009
    35
  apply (simp_all add: add_nrows)
obua@15009
    36
  done
obua@15009
    37
obua@15009
    38
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"
obua@15009
    39
  apply (induct arr)
obua@15009
    40
  apply (auto simp add: sparse_row_matrix_def)
obua@15009
    41
  apply (simp add: foldl_distrstart[of "\<lambda>m x. m + (move_matrix (sparse_row_vector (snd x)) (int (fst x)) 0)" 
obua@15009
    42
    "% a m. (move_matrix (sparse_row_vector (snd a)) (int (fst a)) 0) + m"])
obua@15009
    43
  done
obua@15009
    44
obua@15009
    45
lemma sparse_row_matrix_append: "sparse_row_matrix (arr@brr) = (sparse_row_matrix arr) + (sparse_row_matrix brr)"
obua@15009
    46
  apply (induct arr)
obua@15009
    47
  apply (auto simp add: sparse_row_matrix_cons)
obua@15009
    48
  done
obua@15009
    49
obua@15009
    50
consts
obua@15009
    51
  sorted_spvec :: "'a spvec \<Rightarrow> bool"
obua@15009
    52
  sorted_spmat :: "'a spmat \<Rightarrow> bool"
obua@15009
    53
obua@15009
    54
primrec
obua@15009
    55
  "sorted_spmat [] = True"
obua@15009
    56
  "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
obua@15009
    57
obua@15009
    58
primrec
obua@15009
    59
  "sorted_spvec [] = True"
obua@15009
    60
sorted_spvec_step:  "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
obua@15009
    61
obua@15009
    62
declare sorted_spvec.simps [simp del]
obua@15009
    63
obua@15009
    64
lemma sorted_spvec_empty[simp]: "sorted_spvec [] = True"
obua@15009
    65
by (simp add: sorted_spvec.simps)
obua@15009
    66
obua@15009
    67
lemma sorted_spvec_cons1: "sorted_spvec (a#as) \<Longrightarrow> sorted_spvec as"
obua@15009
    68
apply (induct as)
obua@15009
    69
apply (auto simp add: sorted_spvec.simps)
obua@15009
    70
done
obua@15009
    71
obua@15009
    72
lemma sorted_spvec_cons2: "sorted_spvec (a#b#t) \<Longrightarrow> sorted_spvec (a#t)"
obua@15009
    73
apply (induct t)
obua@15009
    74
apply (auto simp add: sorted_spvec.simps)
obua@15009
    75
done
obua@15009
    76
obua@15009
    77
lemma sorted_spvec_cons3: "sorted_spvec(a#b#t) \<Longrightarrow> fst a < fst b"
obua@15009
    78
apply (auto simp add: sorted_spvec.simps)
obua@15009
    79
done
obua@15009
    80
obua@15009
    81
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"
obua@15009
    82
apply (induct arr)
obua@15009
    83
apply (auto)
obua@15009
    84
apply (frule sorted_spvec_cons2,simp)+
obua@15009
    85
apply (frule sorted_spvec_cons3, simp)
obua@15009
    86
done
obua@15009
    87
obua@15009
    88
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"
obua@15009
    89
  apply (induct arr)
obua@15009
    90
  apply (auto)
obua@15009
    91
  apply (frule sorted_spvec_cons2, simp)
obua@15009
    92
  apply (frule sorted_spvec_cons3, simp)
obua@15009
    93
  apply (simp add: sparse_row_matrix_cons neg_def)
obua@15009
    94
  done
obua@15009
    95
obua@15009
    96
consts
obua@15009
    97
  smult_spvec :: "('a::lordered_ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" 
obua@15009
    98
  addmult_spvec :: "('a::lordered_ring) * 'a spvec * 'a spvec \<Rightarrow> 'a spvec"
obua@15009
    99
obua@15009
   100
defs
obua@15009
   101
  smult_spvec_def: "smult_spvec y arr == map (% a. (fst a, y * snd a)) arr"  
obua@15009
   102
obua@15009
   103
lemma smult_spvec_empty[simp]: "smult_spvec y [] = []"
obua@15009
   104
  by (simp add: smult_spvec_def)
obua@15009
   105
obua@15009
   106
lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"
obua@15009
   107
  by (simp add: smult_spvec_def)
obua@15009
   108
obua@15009
   109
recdef addmult_spvec "measure (% (y, a, b). length a + (length b))"
obua@15009
   110
  "addmult_spvec (y, arr, []) = arr"
obua@15009
   111
  "addmult_spvec (y, [], brr) = smult_spvec y brr"
obua@15009
   112
  "addmult_spvec (y, a#arr, b#brr) = (
obua@15009
   113
    if (fst a) < (fst b) then (a#(addmult_spvec (y, arr, b#brr))) 
obua@15009
   114
    else (if (fst b < fst a) then ((fst b, y * (snd b))#(addmult_spvec (y, a#arr, brr)))
obua@15009
   115
    else ((fst a, (snd a)+ y*(snd b))#(addmult_spvec (y, arr,brr)))))"
obua@15009
   116
obua@15009
   117
lemma addmult_spvec_empty1[simp]: "addmult_spvec (y, [], a) = smult_spvec y a"
obua@15009
   118
  by (induct a, auto)
obua@15009
   119
obua@15009
   120
lemma addmult_spvec_empty2[simp]: "addmult_spvec (y, a, []) = a"
obua@15009
   121
  by (induct a, auto)
obua@15009
   122
obua@15009
   123
lemma sparse_row_vector_map: "(! x y. f (x+y) = (f x) + (f y)) \<Longrightarrow> (f::'a\<Rightarrow>('a::lordered_ring)) 0 = 0 \<Longrightarrow> 
obua@15009
   124
  sparse_row_vector (map (% x. (fst x, f (snd x))) a) = apply_matrix f (sparse_row_vector a)"
obua@15009
   125
  apply (induct a)
obua@15009
   126
  apply (simp_all add: apply_matrix_add)
obua@15009
   127
  done
obua@15009
   128
obua@15009
   129
lemma sparse_row_vector_smult: "sparse_row_vector (smult_spvec y a) = scalar_mult y (sparse_row_vector a)"
obua@15009
   130
  apply (induct a)
obua@15009
   131
  apply (simp_all add: smult_spvec_cons scalar_mult_add)
obua@15009
   132
  done
obua@15009
   133
obua@15009
   134
lemma sparse_row_vector_addmult_spvec: "sparse_row_vector (addmult_spvec (y::'a::lordered_ring, a, b)) = 
obua@15009
   135
  (sparse_row_vector a) + (scalar_mult y (sparse_row_vector b))"
obua@15009
   136
  apply (rule addmult_spvec.induct[of _ y])
obua@15009
   137
  apply (simp add: scalar_mult_add smult_spvec_cons sparse_row_vector_smult singleton_matrix_add)+
obua@15009
   138
  apply (case_tac "a=aa")
obua@15009
   139
  apply (auto)
obua@15009
   140
  done
obua@15009
   141
obua@15009
   142
lemma sorted_smult_spvec[rule_format]: "sorted_spvec a \<Longrightarrow> sorted_spvec (smult_spvec y a)"
obua@15009
   143
  apply (auto simp add: smult_spvec_def)
obua@15009
   144
  apply (induct a)
obua@15009
   145
  apply (auto simp add: sorted_spvec.simps)
obua@15009
   146
  apply (case_tac list)
obua@15009
   147
  apply (auto)
obua@15009
   148
  done
obua@15009
   149
obua@15009
   150
lemma sorted_spvec_addmult_spvec_helper: "\<lbrakk>sorted_spvec (addmult_spvec (y, (a, b) # arr, brr)); aa < a; sorted_spvec ((a, b) # arr); 
obua@15009
   151
  sorted_spvec ((aa, ba) # brr)\<rbrakk> \<Longrightarrow> sorted_spvec ((aa, y * ba) # addmult_spvec (y, (a, b) # arr, brr))"  
obua@15009
   152
  apply (induct brr)
obua@15009
   153
  apply (auto simp add: sorted_spvec.simps)
obua@15009
   154
  apply (simp split: list.split)
obua@15009
   155
  apply (auto)
obua@15009
   156
  apply (simp split: list.split)
obua@15009
   157
  apply (auto)
obua@15009
   158
  done
obua@15009
   159
obua@15009
   160
lemma sorted_spvec_addmult_spvec_helper2: 
obua@15009
   161
 "\<lbrakk>sorted_spvec (addmult_spvec (y, arr, (aa, ba) # brr)); a < aa; sorted_spvec ((a, b) # arr); sorted_spvec ((aa, ba) # brr)\<rbrakk>
obua@15009
   162
       \<Longrightarrow> sorted_spvec ((a, b) # addmult_spvec (y, arr, (aa, ba) # brr))"
obua@15009
   163
  apply (induct arr)
obua@15009
   164
  apply (auto simp add: smult_spvec_def sorted_spvec.simps)
obua@15009
   165
  apply (simp split: list.split)
obua@15009
   166
  apply (auto)
obua@15009
   167
  done
obua@15009
   168
obua@15009
   169
lemma sorted_spvec_addmult_spvec_helper3[rule_format]:
obua@15009
   170
  "sorted_spvec (addmult_spvec (y, arr, brr)) \<longrightarrow> sorted_spvec ((aa, b) # arr) \<longrightarrow> sorted_spvec ((aa, ba) # brr)
obua@15009
   171
     \<longrightarrow> sorted_spvec ((aa, b + y * ba) # (addmult_spvec (y, arr, brr)))"
obua@15009
   172
  apply (rule addmult_spvec.induct[of _ y arr brr])
obua@15009
   173
  apply (simp_all add: sorted_spvec.simps smult_spvec_def)
obua@15009
   174
  done
obua@15009
   175
obua@15009
   176
lemma sorted_addmult_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (addmult_spvec (y, a, b))"
obua@15009
   177
  apply (rule addmult_spvec.induct[of _ y a b])
obua@15009
   178
  apply (simp_all add: sorted_smult_spvec)
obua@15009
   179
  apply (rule conjI, intro strip)
obua@15009
   180
  apply (case_tac "~(a < aa)")
obua@15009
   181
  apply (simp_all)
obua@15009
   182
  apply (frule_tac as=brr in sorted_spvec_cons1)
obua@15009
   183
  apply (simp add: sorted_spvec_addmult_spvec_helper)
obua@15009
   184
  apply (intro strip | rule conjI)+
obua@15009
   185
  apply (frule_tac as=arr in sorted_spvec_cons1)
obua@15009
   186
  apply (simp add: sorted_spvec_addmult_spvec_helper2)
obua@15009
   187
  apply (intro strip)
obua@15009
   188
  apply (frule_tac as=arr in sorted_spvec_cons1)
obua@15009
   189
  apply (frule_tac as=brr in sorted_spvec_cons1)
obua@15009
   190
  apply (simp)
obua@15009
   191
  apply (case_tac "a=aa")
obua@15009
   192
  apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
obua@15009
   193
  done
obua@15009
   194
obua@15009
   195
consts 
obua@15009
   196
  mult_spvec_spmat :: "('a::lordered_ring) spvec * 'a spvec * 'a spmat  \<Rightarrow> 'a spvec"
obua@15009
   197
obua@15009
   198
recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))"
obua@15009
   199
  "mult_spvec_spmat (c, [], brr) = c"
obua@15009
   200
  "mult_spvec_spmat (c, arr, []) = c"
obua@15009
   201
  "mult_spvec_spmat (c, a#arr, b#brr) = (
obua@15009
   202
     if ((fst a) < (fst b)) then (mult_spvec_spmat (c, arr, b#brr))
obua@15009
   203
     else (if ((fst b) < (fst a)) then (mult_spvec_spmat (c, a#arr, brr)) 
obua@15009
   204
     else (mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))))"
obua@15009
   205
obua@15009
   206
lemma sparse_row_mult_spvec_spmat[rule_format]: "sorted_spvec (a::('a::lordered_ring) spvec) \<longrightarrow> sorted_spvec B \<longrightarrow> 
obua@15009
   207
  sparse_row_vector (mult_spvec_spmat (c, a, B)) = (sparse_row_vector c) + (sparse_row_vector a) * (sparse_row_matrix B)"
obua@15009
   208
proof -
obua@15009
   209
  have comp_1: "!! a b. a < b \<Longrightarrow> Suc 0 <= nat ((int b)-(int a))" by arith
obua@15009
   210
  have not_iff: "!! a b. a = b \<Longrightarrow> (~ a) = (~ b)" by simp
obua@15009
   211
  have max_helper: "!! a b. ~ (a <= max (Suc a) b) \<Longrightarrow> False"
obua@15009
   212
    by arith
obua@15009
   213
  {
obua@15009
   214
    fix a 
obua@15009
   215
    fix v
obua@15009
   216
    assume a:"a < nrows(sparse_row_vector v)"
obua@15009
   217
    have b:"nrows(sparse_row_vector v) <= 1" by simp
obua@15009
   218
    note dummy = less_le_trans[of a "nrows (sparse_row_vector v)" 1, OF a b]   
obua@15009
   219
    then have "a = 0" by simp
obua@15009
   220
  }
obua@15009
   221
  note nrows_helper = this
obua@15009
   222
  show ?thesis
obua@15009
   223
    apply (rule mult_spvec_spmat.induct)
obua@15009
   224
    apply simp+
obua@15009
   225
    apply (rule conjI)
obua@15009
   226
    apply (intro strip)
obua@15009
   227
    apply (frule_tac as=brr in sorted_spvec_cons1)
obua@15009
   228
    apply (simp add: ring_eq_simps sparse_row_matrix_cons)
obua@15009
   229
    apply (subst Rep_matrix_zero_imp_mult_zero) 
obua@15009
   230
    apply (simp)
obua@15009
   231
    apply (intro strip)
obua@15009
   232
    apply (rule disjI2)
obua@15009
   233
    apply (intro strip)
obua@15009
   234
    apply (subst nrows)
obua@15009
   235
    apply (rule  order_trans[of _ 1])
obua@15009
   236
    apply (simp add: comp_1)+
obua@15009
   237
    apply (subst Rep_matrix_zero_imp_mult_zero)
obua@15009
   238
    apply (intro strip)
obua@15009
   239
    apply (case_tac "k <= aa")
obua@15009
   240
    apply (rule_tac m1 = k and n1 = a and a1 = b in ssubst[OF sorted_sparse_row_vector_zero])
obua@15009
   241
    apply (simp_all)
obua@15009
   242
    apply (rule impI)
obua@15009
   243
    apply (rule disjI2)
obua@15009
   244
    apply (rule nrows)
obua@15009
   245
    apply (rule order_trans[of _ 1])
obua@15009
   246
    apply (simp_all add: comp_1)
obua@15009
   247
    
obua@15009
   248
    apply (intro strip | rule conjI)+
obua@15009
   249
    apply (frule_tac as=arr in sorted_spvec_cons1)
obua@15009
   250
    apply (simp add: ring_eq_simps)
obua@15009
   251
    apply (subst Rep_matrix_zero_imp_mult_zero)
obua@15009
   252
    apply (simp)
obua@15009
   253
    apply (rule disjI2)
obua@15009
   254
    apply (intro strip)
obua@15009
   255
    apply (simp add: sparse_row_matrix_cons neg_def)
obua@15009
   256
    apply (case_tac "a <= aa")  
obua@15009
   257
    apply (erule sorted_sparse_row_matrix_zero)  
obua@15009
   258
    apply (simp_all)
obua@15009
   259
    apply (intro strip)
obua@15009
   260
    apply (case_tac "a=aa")
obua@15009
   261
    apply (simp_all)
obua@15009
   262
    apply (frule_tac as=arr in sorted_spvec_cons1)
obua@15009
   263
    apply (frule_tac as=brr in sorted_spvec_cons1)
obua@15009
   264
    apply (simp add: sparse_row_matrix_cons ring_eq_simps sparse_row_vector_addmult_spvec)
obua@15009
   265
    apply (rule_tac B1 = "sparse_row_matrix brr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
obua@15009
   266
    apply (auto)
obua@15009
   267
    apply (rule sorted_sparse_row_matrix_zero)
obua@15009
   268
    apply (simp_all)
obua@15009
   269
    apply (rule_tac A1 = "sparse_row_vector arr" in ssubst[OF Rep_matrix_zero_imp_mult_zero])
obua@15009
   270
    apply (auto)
obua@15009
   271
    apply (rule_tac m=k and n = aa and a = b and arr=arr in sorted_sparse_row_vector_zero)
obua@15009
   272
    apply (simp_all)
obua@15009
   273
    apply (simp add: neg_def)
obua@15009
   274
    apply (drule nrows_notzero)
obua@15009
   275
    apply (drule nrows_helper)
obua@15009
   276
    apply (arith)
obua@15009
   277
    
obua@15009
   278
    apply (subst Rep_matrix_inject[symmetric])
obua@15009
   279
    apply (rule ext)+
obua@15009
   280
    apply (simp)
obua@15009
   281
    apply (subst Rep_matrix_mult)
obua@15009
   282
    apply (rule_tac j1=aa in ssubst[OF foldseq_almostzero])
obua@15009
   283
    apply (simp_all)
obua@15009
   284
    apply (intro strip, rule conjI)
obua@15009
   285
    apply (intro strip)
obua@15009
   286
    apply (drule_tac max_helper)
obua@15009
   287
    apply (simp)
obua@15009
   288
    apply (auto)
obua@15009
   289
    apply (rule zero_imp_mult_zero)
obua@15009
   290
    apply (rule disjI2)
obua@15009
   291
    apply (rule nrows)
obua@15009
   292
    apply (rule order_trans[of _ 1])
obua@15009
   293
    apply (simp)
obua@15009
   294
    apply (simp)
obua@15009
   295
    done
obua@15009
   296
qed
obua@15009
   297
obua@15009
   298
lemma sorted_mult_spvec_spmat[rule_format]: 
obua@15009
   299
  "sorted_spvec (c::('a::lordered_ring) spvec) \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spvec (mult_spvec_spmat (c, a, B))"
obua@15009
   300
  apply (rule mult_spvec_spmat.induct[of _ c a B])
obua@15009
   301
  apply (simp_all add: sorted_addmult_spvec)
obua@15009
   302
  done
obua@15009
   303
obua@15009
   304
consts 
obua@15009
   305
  mult_spmat :: "('a::lordered_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
obua@15009
   306
obua@15009
   307
primrec 
obua@15009
   308
  "mult_spmat [] A = []"
obua@15009
   309
  "mult_spmat (a#as) A = (fst a, mult_spvec_spmat ([], snd a, A))#(mult_spmat as A)"
obua@15009
   310
obua@15009
   311
lemma sparse_row_mult_spmat[rule_format]: 
obua@15009
   312
  "sorted_spmat A \<longrightarrow> sorted_spvec B \<longrightarrow> sparse_row_matrix (mult_spmat A B) = (sparse_row_matrix A) * (sparse_row_matrix B)"
obua@15009
   313
  apply (induct A)
obua@15009
   314
  apply (auto simp add: sparse_row_matrix_cons sparse_row_mult_spvec_spmat ring_eq_simps move_matrix_mult)
obua@15009
   315
  done
obua@15009
   316
obua@15009
   317
lemma sorted_spvec_mult_spmat[rule_format]:
obua@15009
   318
  "sorted_spvec (A::('a::lordered_ring) spmat) \<longrightarrow> sorted_spvec (mult_spmat A B)"
obua@15009
   319
  apply (induct A)
obua@15009
   320
  apply (auto)
obua@15009
   321
  apply (drule sorted_spvec_cons1, simp)
obua@15009
   322
  apply (case_tac list)
obua@15009
   323
  apply (auto simp add: sorted_spvec.simps)
obua@15009
   324
  done
obua@15009
   325
obua@15009
   326
lemma sorted_spmat_mult_spmat[rule_format]:
obua@15009
   327
  "sorted_spmat (B::('a::lordered_ring) spmat) \<longrightarrow> sorted_spmat (mult_spmat A B)"
obua@15009
   328
  apply (induct A)
obua@15009
   329
  apply (auto simp add: sorted_mult_spvec_spmat) 
obua@15009
   330
  done
obua@15009
   331
obua@15009
   332
consts
obua@15009
   333
  add_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> 'a spvec"
obua@15009
   334
  add_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> 'a spmat"
obua@15009
   335
obua@15009
   336
recdef add_spvec "measure (% (a, b). length a + (length b))"
obua@15009
   337
  "add_spvec (arr, []) = arr"
obua@15009
   338
  "add_spvec ([], brr) = brr"
obua@15009
   339
  "add_spvec (a#arr, b#brr) = (
obua@15009
   340
  if (fst a) < (fst b) then (a#(add_spvec (arr, b#brr))) 
obua@15009
   341
     else (if (fst b < fst a) then (b#(add_spvec (a#arr, brr)))
obua@15009
   342
     else ((fst a, (snd a)+(snd b))#(add_spvec (arr,brr)))))"
obua@15009
   343
obua@15009
   344
lemma add_spvec_empty1[simp]: "add_spvec ([], a) = a"
obua@15009
   345
  by (induct a, auto)
obua@15009
   346
obua@15009
   347
lemma add_spvec_empty2[simp]: "add_spvec (a, []) = a"
obua@15009
   348
  by (induct a, auto)
obua@15009
   349
obua@15009
   350
lemma sparse_row_vector_add: "sparse_row_vector (add_spvec (a,b)) = (sparse_row_vector a) + (sparse_row_vector b)"
obua@15009
   351
  apply (rule add_spvec.induct[of _ a b])
obua@15009
   352
  apply (simp_all add: singleton_matrix_add)
obua@15009
   353
  apply (case_tac "a = aa")
obua@15009
   354
  apply (simp_all)
obua@15009
   355
  done
obua@15009
   356
obua@15009
   357
recdef add_spmat "measure (% (A,B). (length A)+(length B))"
obua@15009
   358
  "add_spmat ([], bs) = bs"
obua@15009
   359
  "add_spmat (as, []) = as"
obua@15009
   360
  "add_spmat (a#as, b#bs) = (
obua@15009
   361
  if fst a < fst b then 
obua@15009
   362
    (a#(add_spmat (as, b#bs)))
obua@15009
   363
  else (if fst b < fst a then
obua@15009
   364
    (b#(add_spmat (a#as, bs)))
obua@15009
   365
  else
obua@15009
   366
    ((fst a, add_spvec (snd a, snd b))#(add_spmat (as, bs)))))"
obua@15009
   367
obua@15009
   368
lemma sparse_row_add_spmat: "sparse_row_matrix (add_spmat (A, B)) = (sparse_row_matrix A) + (sparse_row_matrix B)"
obua@15009
   369
  apply (rule add_spmat.induct)
obua@15009
   370
  apply (auto simp add: sparse_row_matrix_cons sparse_row_vector_add move_matrix_add)
obua@15009
   371
  apply (case_tac "a=aa", simp, simp)+
obua@15009
   372
  done
obua@15009
   373
obua@15009
   374
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)))"
obua@15009
   375
  proof - 
obua@15009
   376
    have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spvec (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
obua@15009
   377
      by (rule add_spvec.induct[of _ _ brr], auto)
obua@15009
   378
    then show ?thesis
obua@15009
   379
      by (case_tac brr, auto)
obua@15009
   380
  qed
obua@15009
   381
obua@15009
   382
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)))"
obua@15009
   383
  proof - 
obua@15009
   384
    have "(! x ab a. x = (a,b)#arr \<longrightarrow> add_spmat (x, brr) = (ab, bb) # list \<longrightarrow> (ab = a | (ab = fst (hd brr))))"
obua@15009
   385
      by (rule add_spmat.induct[of _ _ brr], auto)
obua@15009
   386
    then show ?thesis
obua@15009
   387
      by (case_tac brr, auto)
obua@15009
   388
  qed
obua@15009
   389
obua@15009
   390
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)))"
obua@15009
   391
  apply (rule add_spvec.induct[of _ arr brr])
obua@15009
   392
  apply (auto)
obua@15009
   393
  done
obua@15009
   394
obua@15009
   395
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)))"
obua@15009
   396
  apply (rule add_spmat.induct[of _ arr brr])
obua@15009
   397
  apply (auto)
obua@15009
   398
  done
obua@15009
   399
obua@15009
   400
lemma add_spvec_commute: "add_spvec (a, b) = add_spvec (b, a)"
obua@15009
   401
  by (rule add_spvec.induct[of _ a b], auto)
obua@15009
   402
obua@15009
   403
lemma add_spmat_commute: "add_spmat (a, b) = add_spmat (b, a)"
obua@15009
   404
  apply (rule add_spmat.induct[of _ a b])
obua@15009
   405
  apply (simp_all add: add_spvec_commute)
obua@15009
   406
  done
obua@15009
   407
  
obua@15009
   408
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"
obua@15009
   409
  apply (drule sorted_add_spvec_helper1)
obua@15009
   410
  apply (auto)
obua@15009
   411
  apply (case_tac brr)
obua@15009
   412
  apply (simp_all)
obua@15009
   413
  apply (drule_tac sorted_spvec_cons3)
obua@15009
   414
  apply (simp)
obua@15009
   415
  done
obua@15009
   416
obua@15009
   417
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"
obua@15009
   418
  apply (drule sorted_add_spmat_helper1)
obua@15009
   419
  apply (auto)
obua@15009
   420
  apply (case_tac brr)
obua@15009
   421
  apply (simp_all)
obua@15009
   422
  apply (drule_tac sorted_spvec_cons3)
obua@15009
   423
  apply (simp)
obua@15009
   424
  done
obua@15009
   425
obua@15009
   426
lemma sorted_spvec_add_spvec[rule_format]: "sorted_spvec a \<longrightarrow> sorted_spvec b \<longrightarrow> sorted_spvec (add_spvec (a, b))"
obua@15009
   427
  apply (rule add_spvec.induct[of _ a b])
obua@15009
   428
  apply (simp_all)
obua@15009
   429
  apply (rule conjI)
obua@15009
   430
  apply (intro strip)
obua@15009
   431
  apply (simp)
obua@15009
   432
  apply (frule_tac as=brr in sorted_spvec_cons1)
obua@15009
   433
  apply (simp)
obua@15009
   434
  apply (subst sorted_spvec_step)
obua@15009
   435
  apply (simp split: list.split)
obua@15009
   436
  apply (clarify, simp)
obua@15009
   437
  apply (simp add: sorted_add_spvec_helper2)
obua@15009
   438
  apply (clarify)
obua@15009
   439
  apply (rule conjI)
obua@15009
   440
  apply (case_tac "a=aa")
obua@15009
   441
  apply (simp)
obua@15009
   442
  apply (clarify)
obua@15009
   443
  apply (frule_tac as=arr in sorted_spvec_cons1, simp)
obua@15009
   444
  apply (subst sorted_spvec_step)
obua@15009
   445
  apply (simp split: list.split)
obua@15009
   446
  apply (clarify, simp)
obua@15009
   447
  apply (simp add: sorted_add_spvec_helper2 add_spvec_commute)
obua@15009
   448
  apply (case_tac "a=aa")
obua@15009
   449
  apply (simp_all)
obua@15009
   450
  apply (clarify)
obua@15009
   451
  apply (frule_tac as=arr in sorted_spvec_cons1)
obua@15009
   452
  apply (frule_tac as=brr in sorted_spvec_cons1)
obua@15009
   453
  apply (simp)
obua@15009
   454
  apply (subst sorted_spvec_step)
obua@15009
   455
  apply (simp split: list.split)
obua@15009
   456
  apply (clarify, simp)
obua@15009
   457
  apply (drule_tac sorted_add_spvec_helper)
obua@15009
   458
  apply (auto)
obua@15009
   459
  apply (case_tac arr)
obua@15009
   460
  apply (simp_all)
obua@15009
   461
  apply (drule sorted_spvec_cons3)
obua@15009
   462
  apply (simp)
obua@15009
   463
  apply (case_tac brr)
obua@15009
   464
  apply (simp_all)
obua@15009
   465
  apply (drule sorted_spvec_cons3)
obua@15009
   466
  apply (simp)
obua@15009
   467
  done
obua@15009
   468
obua@15009
   469
lemma sorted_spvec_add_spmat[rule_format]: "sorted_spvec A \<longrightarrow> sorted_spvec B \<longrightarrow> sorted_spvec (add_spmat (A, B))"
obua@15009
   470
  apply (rule add_spmat.induct[of _ A B])
obua@15009
   471
  apply (simp_all)
obua@15009
   472
  apply (rule conjI)
obua@15009
   473
  apply (intro strip)
obua@15009
   474
  apply (simp)
obua@15009
   475
  apply (frule_tac as=bs in sorted_spvec_cons1)
obua@15009
   476
  apply (simp)
obua@15009
   477
  apply (subst sorted_spvec_step)
obua@15009
   478
  apply (simp split: list.split)
obua@15009
   479
  apply (clarify, simp)
obua@15009
   480
  apply (simp add: sorted_add_spmat_helper2)
obua@15009
   481
  apply (clarify)
obua@15009
   482
  apply (rule conjI)
obua@15009
   483
  apply (case_tac "a=aa")
obua@15009
   484
  apply (simp)
obua@15009
   485
  apply (clarify)
obua@15009
   486
  apply (frule_tac as=as in sorted_spvec_cons1, simp)
obua@15009
   487
  apply (subst sorted_spvec_step)
obua@15009
   488
  apply (simp split: list.split)
obua@15009
   489
  apply (clarify, simp)
obua@15009
   490
  apply (simp add: sorted_add_spmat_helper2 add_spmat_commute)
obua@15009
   491
  apply (case_tac "a=aa")
obua@15009
   492
  apply (simp_all)
obua@15009
   493
  apply (clarify)
obua@15009
   494
  apply (frule_tac as=as in sorted_spvec_cons1)
obua@15009
   495
  apply (frule_tac as=bs in sorted_spvec_cons1)
obua@15009
   496
  apply (simp)
obua@15009
   497
  apply (subst sorted_spvec_step)
obua@15009
   498
  apply (simp split: list.split)
obua@15009
   499
  apply (clarify, simp)
obua@15009
   500
  apply (drule_tac sorted_add_spmat_helper)
obua@15009
   501
  apply (auto)
obua@15009
   502
  apply (case_tac as)
obua@15009
   503
  apply (simp_all)
obua@15009
   504
  apply (drule sorted_spvec_cons3)
obua@15009
   505
  apply (simp)
obua@15009
   506
  apply (case_tac bs)
obua@15009
   507
  apply (simp_all)
obua@15009
   508
  apply (drule sorted_spvec_cons3)
obua@15009
   509
  apply (simp)
obua@15009
   510
  done
obua@15009
   511
obua@15009
   512
lemma sorted_spmat_add_spmat[rule_format]: "sorted_spmat A \<longrightarrow> sorted_spmat B \<longrightarrow> sorted_spmat (add_spmat (A, B))"
obua@15009
   513
  apply (rule add_spmat.induct[of _ A B])
obua@15009
   514
  apply (simp_all add: sorted_spvec_add_spvec)
obua@15009
   515
  done
obua@15009
   516
obua@15009
   517
consts
obua@15009
   518
  le_spvec :: "('a::lordered_ab_group) spvec * 'a spvec \<Rightarrow> bool" 
obua@15009
   519
  le_spmat :: "('a::lordered_ab_group) spmat * 'a spmat \<Rightarrow> bool" 
obua@15009
   520
obua@15009
   521
recdef le_spvec "measure (% (a,b). (length a) + (length b))" 
obua@15009
   522
  "le_spvec ([], []) = True"
obua@15009
   523
  "le_spvec (a#as, []) = ((snd a <= 0) & (le_spvec (as, [])))"
obua@15009
   524
  "le_spvec ([], b#bs) = ((0 <= snd b) & (le_spvec ([], bs)))"
obua@15009
   525
  "le_spvec (a#as, b#bs) = (
obua@15009
   526
  if (fst a < fst b) then 
obua@15009
   527
    ((snd a <= 0) & (le_spvec (as, b#bs)))
obua@15009
   528
  else (if (fst b < fst a) then
obua@15009
   529
    ((0 <= snd b) & (le_spvec (a#as, bs)))
obua@15009
   530
  else 
obua@15009
   531
    ((snd a <= snd b) & (le_spvec (as, bs)))))"
obua@15009
   532
obua@15009
   533
recdef le_spmat "measure (% (a,b). (length a) + (length b))"
obua@15009
   534
  "le_spmat ([], []) = True"
obua@15009
   535
  "le_spmat (a#as, []) = (le_spvec (snd a, []) & (le_spmat (as, [])))"
obua@15009
   536
  "le_spmat ([], b#bs) = (le_spvec ([], snd b) & (le_spmat ([], bs)))"
obua@15009
   537
  "le_spmat (a#as, b#bs) = (
obua@15009
   538
  if fst a < fst b then
obua@15009
   539
    (le_spvec(snd a,[]) & le_spmat(as, b#bs))
obua@15009
   540
  else (if (fst b < fst a) then 
obua@15009
   541
    (le_spvec([], snd b) & le_spmat(a#as, bs))
obua@15009
   542
  else
obua@15009
   543
    (le_spvec(snd a, snd b) & le_spmat (as, bs))))"
obua@15009
   544
obua@15009
   545
lemma spec2: "! j i. P j i \<Longrightarrow> P j i" by blast
obua@15009
   546
lemma neg_imp: "(\<not> Q \<longrightarrow> \<not> P) \<Longrightarrow> P \<longrightarrow> Q" by blast
obua@15009
   547
obua@15009
   548
constdefs
obua@15009
   549
  disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool"
obua@15009
   550
  "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))"  
obua@15009
   551
obua@15009
   552
ML {* simp_depth_limit := 2 *}
obua@15009
   553
obua@15009
   554
lemma disj_matrices_add: "disj_matrices A B \<Longrightarrow> disj_matrices C D \<Longrightarrow> disj_matrices A D \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
obua@15009
   555
  (A + B <= C + D) = (A <= C & B <= (D::('a::lordered_ab_group) matrix))"
obua@15009
   556
  apply (auto)
obua@15009
   557
  apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
obua@15009
   558
  apply (intro strip)
obua@15009
   559
  apply (erule conjE)+
obua@15009
   560
  apply (drule_tac j=j and i=i in spec2)+
obua@15009
   561
  apply (case_tac "Rep_matrix B j i = 0")
obua@15009
   562
  apply (case_tac "Rep_matrix D j i = 0")
obua@15009
   563
  apply (simp_all)
obua@15009
   564
  apply (simp (no_asm_use) only: le_matrix_def disj_matrices_def)
obua@15009
   565
  apply (intro strip)
obua@15009
   566
  apply (erule conjE)+
obua@15009
   567
  apply (drule_tac j=j and i=i in spec2)+
obua@15009
   568
  apply (case_tac "Rep_matrix A j i = 0")
obua@15009
   569
  apply (case_tac "Rep_matrix C j i = 0")
obua@15009
   570
  apply (simp_all)
obua@15009
   571
  apply (erule add_mono)
obua@15009
   572
  apply (assumption)
obua@15009
   573
  done
obua@15009
   574
obua@15009
   575
lemma disj_matrices_zero1[simp]: "disj_matrices 0 B"
obua@15009
   576
by (simp add: disj_matrices_def)
obua@15009
   577
obua@15009
   578
lemma disj_matrices_zero2[simp]: "disj_matrices A 0"
obua@15009
   579
by (simp add: disj_matrices_def)
obua@15009
   580
obua@15009
   581
lemma disj_matrices_commute: "disj_matrices A B = disj_matrices B A"
obua@15009
   582
by (auto simp add: disj_matrices_def)
obua@15009
   583
obua@15009
   584
lemma disj_matrices_add_le_zero: "disj_matrices A B \<Longrightarrow>
obua@15009
   585
  (A + B <= 0) = (A <= 0 & (B::('a::lordered_ab_group) matrix) <= 0)"
obua@15009
   586
by (rule disj_matrices_add[of A B 0 0, simplified])
obua@15009
   587
 
obua@15009
   588
lemma disj_matrices_add_zero_le: "disj_matrices A B \<Longrightarrow>
obua@15009
   589
  (0 <= A + B) = (0 <= A & 0 <= (B::('a::lordered_ab_group) matrix))"
obua@15009
   590
by (rule disj_matrices_add[of 0 0 A B, simplified])
obua@15009
   591
obua@15009
   592
lemma disj_matrices_add_x_le: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
obua@15009
   593
  (A <= B + C) = (A <= C & 0 <= (B::('a::lordered_ab_group) matrix))"
obua@15009
   594
by (auto simp add: disj_matrices_add[of 0 A B C, simplified])
obua@15009
   595
obua@15009
   596
lemma disj_matrices_add_le_x: "disj_matrices A B \<Longrightarrow> disj_matrices B C \<Longrightarrow> 
obua@15009
   597
  (B + A <= C) = (A <= C &  (B::('a::lordered_ab_group) matrix) <= 0)"
obua@15009
   598
by (auto simp add: disj_matrices_add[of B A 0 C,simplified] disj_matrices_commute)
obua@15009
   599
obua@15009
   600
lemma singleton_le_zero[simp]: "(singleton_matrix j i x <= 0) = (x <= (0::'a::{order,zero}))"
obua@15009
   601
  apply (auto)
obua@15009
   602
  apply (simp add: le_matrix_def)
obua@15009
   603
  apply (drule_tac j=j and i=i in spec2)
obua@15009
   604
  apply (simp)
obua@15009
   605
  apply (simp add: le_matrix_def)
obua@15009
   606
  done
obua@15009
   607
obua@15009
   608
lemma singleton_ge_zero[simp]: "(0 <= singleton_matrix j i x) = ((0::'a::{order,zero}) <= x)"
obua@15009
   609
  apply (auto)
obua@15009
   610
  apply (simp add: le_matrix_def)
obua@15009
   611
  apply (drule_tac j=j and i=i in spec2)
obua@15009
   612
  apply (simp)
obua@15009
   613
  apply (simp add: le_matrix_def)
obua@15009
   614
  done
obua@15009
   615
obua@15009
   616
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)"
obua@15009
   617
  apply (simp add: disj_matrices_def)
obua@15009
   618
  apply (rule conjI)
obua@15009
   619
  apply (rule neg_imp)
obua@15009
   620
  apply (simp)
obua@15009
   621
  apply (intro strip)
obua@15009
   622
  apply (rule sorted_sparse_row_vector_zero)
obua@15009
   623
  apply (simp_all)
obua@15009
   624
  apply (intro strip)
obua@15009
   625
  apply (rule sorted_sparse_row_vector_zero)
obua@15009
   626
  apply (simp_all)
obua@15009
   627
  done 
obua@15009
   628
obua@15009
   629
lemma disj_matrices_x_add: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (A::('a::lordered_ab_group) matrix) (B+C)"
obua@15009
   630
  apply (simp add: disj_matrices_def)
obua@15009
   631
  apply (auto)
obua@15009
   632
  apply (drule_tac j=j and i=i in spec2)+
obua@15009
   633
  apply (case_tac "Rep_matrix B j i = 0")
obua@15009
   634
  apply (case_tac "Rep_matrix C j i = 0")
obua@15009
   635
  apply (simp_all)
obua@15009
   636
  done
obua@15009
   637
obua@15009
   638
lemma disj_matrices_add_x: "disj_matrices A B \<Longrightarrow> disj_matrices A C \<Longrightarrow> disj_matrices (B+C) (A::('a::lordered_ab_group) matrix)" 
obua@15009
   639
  by (simp add: disj_matrices_x_add disj_matrices_commute)
obua@15009
   640
obua@15009
   641
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)" 
obua@15009
   642
  by (auto simp add: disj_matrices_def)
obua@15009
   643
obua@15009
   644
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)"
obua@15009
   645
  apply (rule le_spvec.induct)
obua@15009
   646
  apply (simp_all add: sorted_spvec_cons1 disj_matrices_add_le_zero disj_matrices_add_zero_le disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
obua@15009
   647
  apply (rule conjI, intro strip)
obua@15009
   648
  apply (simp add: sorted_spvec_cons1)
obua@15009
   649
  apply (subst disj_matrices_add_x_le)
obua@15009
   650
  apply (simp add: disj_sparse_row_singleton[OF less_imp_le] disj_matrices_x_add disj_matrices_commute)
obua@15009
   651
  apply (simp add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
obua@15009
   652
  apply (simp, blast)
obua@15009
   653
  apply (intro strip, rule conjI, intro strip)
obua@15009
   654
  apply (simp add: sorted_spvec_cons1)
obua@15009
   655
  apply (subst disj_matrices_add_le_x)
obua@15009
   656
  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)
obua@15009
   657
  apply (blast)
obua@15009
   658
  apply (intro strip)
obua@15009
   659
  apply (simp add: sorted_spvec_cons1)
obua@15009
   660
  apply (case_tac "a=aa", simp_all)
obua@15009
   661
  apply (subst disj_matrices_add)
obua@15009
   662
  apply (simp_all add: disj_sparse_row_singleton[OF order_refl] disj_matrices_commute)
obua@15009
   663
  done
obua@15009
   664
obua@15009
   665
lemma disj_move_sparse_vec_mat[simplified disj_matrices_commute]: 
obua@15009
   666
  "j <= a \<Longrightarrow> sorted_spvec((a,c)#as) \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector b) (int j) i) (sparse_row_matrix as)"
obua@15009
   667
  apply (auto simp add: neg_def disj_matrices_def)
obua@15009
   668
  apply (drule nrows_notzero)
obua@15009
   669
  apply (drule less_le_trans[OF _ nrows_spvec])
obua@15009
   670
  apply (subgoal_tac "ja = j")
obua@15009
   671
  apply (simp add: sorted_sparse_row_matrix_zero)
obua@15009
   672
  apply (arith)
obua@15009
   673
  apply (rule nrows)
obua@15009
   674
  apply (rule order_trans[of _ 1 _])
obua@15009
   675
  apply (simp)
obua@15009
   676
  apply (case_tac "nat (int ja - int j) = 0")
obua@15009
   677
  apply (case_tac "ja = j")
obua@15009
   678
  apply (simp add: sorted_sparse_row_matrix_zero)
obua@15009
   679
  apply arith+
obua@15009
   680
  done
obua@15009
   681
obua@15009
   682
lemma disj_move_sparse_row_vector_twice:
obua@15009
   683
  "j \<noteq> u \<Longrightarrow> disj_matrices (move_matrix (sparse_row_vector a) j i) (move_matrix (sparse_row_vector b) u v)"
obua@15009
   684
  apply (auto simp add: neg_def disj_matrices_def)
obua@15009
   685
  apply (rule nrows, rule order_trans[of _ 1], simp, drule nrows_notzero, drule less_le_trans[OF _ nrows_spvec], arith)+
obua@15009
   686
  done
obua@15009
   687
obua@15009
   688
lemma move_matrix_le_zero[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= 0) = (A <= (0::('a::{order,zero}) matrix))"
obua@15009
   689
  apply (auto simp add: le_matrix_def neg_def)
obua@15009
   690
  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
obua@15009
   691
  apply (auto)
obua@15009
   692
  done
obua@15009
   693
obua@15009
   694
lemma move_matrix_zero_le[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (0 <= move_matrix A j i) = ((0::('a::{order,zero}) matrix) <= A)"
obua@15009
   695
  apply (auto simp add: le_matrix_def neg_def)
obua@15009
   696
  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
obua@15009
   697
  apply (auto)
obua@15009
   698
  done
obua@15009
   699
obua@15009
   700
lemma move_matrix_le_move_matrix_iff[simp]: "0 <= j \<Longrightarrow> 0 <= i \<Longrightarrow> (move_matrix A j i <= move_matrix B j i) = (A <= (B::('a::{order,zero}) matrix))"
obua@15009
   701
  apply (auto simp add: le_matrix_def neg_def)
obua@15009
   702
  apply (drule_tac j="ja+(nat j)" and i="ia+(nat i)" in spec2)
obua@15009
   703
  apply (auto)
obua@15009
   704
  done  
obua@15009
   705
obua@15009
   706
lemma le_spvec_empty2_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec (b,[]) = (sparse_row_vector b <= 0))"
obua@15009
   707
  apply (induct b)
obua@15009
   708
  apply (simp_all add: sorted_spvec_cons1)
obua@15009
   709
  apply (intro strip)
obua@15009
   710
  apply (subst disj_matrices_add_le_zero)
obua@15009
   711
  apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
obua@15009
   712
  apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
obua@15009
   713
  apply (simp_all)
obua@15009
   714
  done
obua@15009
   715
obua@15009
   716
lemma le_spvec_empty1_sparse_row[rule_format]: "(sorted_spvec b) \<longrightarrow> (le_spvec ([],b) = (0 <= sparse_row_vector b))"
obua@15009
   717
  apply (induct b)
obua@15009
   718
  apply (simp_all add: sorted_spvec_cons1)
obua@15009
   719
  apply (intro strip)
obua@15009
   720
  apply (subst disj_matrices_add_zero_le)
obua@15009
   721
  apply (simp add: disj_matrices_commute disj_sparse_row_singleton sorted_spvec_cons1)
obua@15009
   722
  apply (rule_tac y = "snd a" in disj_sparse_row_singleton[OF order_refl])
obua@15009
   723
  apply (simp_all)
obua@15009
   724
  done
obua@15009
   725
obua@15009
   726
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> 
obua@15009
   727
  le_spmat(A, B) = (sparse_row_matrix A <= sparse_row_matrix B)"
obua@15009
   728
  apply (rule le_spmat.induct)
obua@15009
   729
  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] 
obua@15009
   730
    disj_matrices_commute sorted_spvec_cons1 le_spvec_empty2_sparse_row le_spvec_empty1_sparse_row)+ 
obua@15009
   731
  apply (rule conjI, intro strip)
obua@15009
   732
  apply (simp add: sorted_spvec_cons1)
obua@15009
   733
  apply (subst disj_matrices_add_x_le)
obua@15009
   734
  apply (rule disj_matrices_add_x)
obua@15009
   735
  apply (simp add: disj_move_sparse_row_vector_twice)
obua@15009
   736
  apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
obua@15009
   737
  apply (simp add: disj_move_sparse_vec_mat[OF order_refl] disj_matrices_commute)
obua@15009
   738
  apply (simp, blast)
obua@15009
   739
  apply (intro strip, rule conjI, intro strip)
obua@15009
   740
  apply (simp add: sorted_spvec_cons1)
obua@15009
   741
  apply (subst disj_matrices_add_le_x)
obua@15009
   742
  apply (simp add: disj_move_sparse_vec_mat[OF order_refl])
obua@15009
   743
  apply (rule disj_matrices_x_add)
obua@15009
   744
  apply (simp add: disj_move_sparse_row_vector_twice)
obua@15009
   745
  apply (simp add: disj_move_sparse_vec_mat[OF less_imp_le] disj_matrices_commute)
obua@15009
   746
  apply (simp, blast)
obua@15009
   747
  apply (intro strip)
obua@15009
   748
  apply (case_tac "a=aa")
obua@15009
   749
  apply (simp_all)
obua@15009
   750
  apply (subst disj_matrices_add)
obua@15009
   751
  apply (simp_all add: disj_matrices_commute disj_move_sparse_vec_mat[OF order_refl])
obua@15009
   752
  apply (simp add: sorted_spvec_cons1 le_spvec_iff_sparse_row_le)
obua@15009
   753
  done
obua@15009
   754
obua@15009
   755
term smult_spvec
obua@15009
   756
term addmult_spvec
obua@15009
   757
term add_spvec
obua@15009
   758
term mult_spvec_spmat
obua@15009
   759
term mult_spmat
obua@15009
   760
term add_spmat
obua@15009
   761
term le_spvec
obua@15009
   762
term le_spmat
obua@15009
   763
term sorted_spvec
obua@15009
   764
term sorted_spmat
obua@15009
   765
obua@15009
   766
thm sparse_row_mult_spmat
obua@15009
   767
thm sparse_row_add_spmat
obua@15009
   768
thm le_spmat_iff_sparse_row_le
obua@15009
   769
obua@15009
   770
thm sorted_spvec_mult_spmat
obua@15009
   771
thm sorted_spmat_mult_spmat
obua@15009
   772
thm sorted_spvec_add_spmat
obua@15009
   773
thm sorted_spmat_add_spmat
obua@15009
   774
obua@15009
   775
thm smult_spvec_empty
obua@15009
   776
thm smult_spvec_cons
obua@15009
   777
thm addmult_spvec.simps
obua@15009
   778
thm add_spvec.simps
obua@15009
   779
thm add_spmat.simps
obua@15009
   780
thm mult_spvec_spmat.simps
obua@15009
   781
thm mult_spmat.simps
obua@15009
   782
thm le_spvec.simps
obua@15009
   783
thm le_spmat.simps
obua@15009
   784
thm sorted_spvec.simps
obua@15009
   785
thm sorted_spmat.simps
obua@15009
   786
obua@15009
   787
end
obua@15009
   788
obua@15009
   789
obua@15009
   790