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