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