modernized some specifications;
authorwenzelm
Wed Aug 11 12:40:08 2010 +0200 (2010-08-11)
changeset 38273d31a34569542
parent 38272 dc53026c6350
child 38326 01d2ef471ffe
modernized some specifications;
src/HOL/Matrix/ComputeFloat.thy
src/HOL/Matrix/ComputeHOL.thy
src/HOL/Matrix/ComputeNumeral.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Matrix/SparseMatrix.thy
     1.1 --- a/src/HOL/Matrix/ComputeFloat.thy	Wed Aug 11 00:47:09 2010 +0200
     1.2 +++ b/src/HOL/Matrix/ComputeFloat.thy	Wed Aug 11 12:40:08 2010 +0200
     1.3 @@ -9,13 +9,11 @@
     1.4  uses "~~/src/Tools/float.ML" ("~~/src/HOL/Tools/float_arith.ML")
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  pow2 :: "int \<Rightarrow> real" where
     1.9 -  "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
    1.10 +definition pow2 :: "int \<Rightarrow> real"
    1.11 +  where "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
    1.12  
    1.13 -definition
    1.14 -  float :: "int * int \<Rightarrow> real" where
    1.15 -  "float x = real (fst x) * pow2 (snd x)"
    1.16 +definition float :: "int * int \<Rightarrow> real"
    1.17 +  where "float x = real (fst x) * pow2 (snd x)"
    1.18  
    1.19  lemma pow2_0[simp]: "pow2 0 = 1"
    1.20  by (simp add: pow2_def)
    1.21 @@ -99,13 +97,11 @@
    1.22  lemma "float (a, e) + float (b, e) = float (a + b, e)"
    1.23  by (simp add: float_def algebra_simps)
    1.24  
    1.25 -definition
    1.26 -  int_of_real :: "real \<Rightarrow> int" where
    1.27 -  "int_of_real x = (SOME y. real y = x)"
    1.28 +definition int_of_real :: "real \<Rightarrow> int"
    1.29 +  where "int_of_real x = (SOME y. real y = x)"
    1.30  
    1.31 -definition
    1.32 -  real_is_int :: "real \<Rightarrow> bool" where
    1.33 -  "real_is_int x = (EX (u::int). x = real u)"
    1.34 +definition real_is_int :: "real \<Rightarrow> bool"
    1.35 +  where "real_is_int x = (EX (u::int). x = real u)"
    1.36  
    1.37  lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
    1.38  by (auto simp add: real_is_int_def int_of_real_def)
    1.39 @@ -345,15 +341,11 @@
    1.40  lemma float_mult_r0: "x * float (0, e) = float (0, 0)"
    1.41    by (simp add: float_def)
    1.42  
    1.43 -definition 
    1.44 -  lbound :: "real \<Rightarrow> real"
    1.45 -where
    1.46 -  "lbound x = min 0 x"
    1.47 +definition lbound :: "real \<Rightarrow> real"
    1.48 +  where "lbound x = min 0 x"
    1.49  
    1.50 -definition
    1.51 -  ubound :: "real \<Rightarrow> real"
    1.52 -where
    1.53 -  "ubound x = max 0 x"
    1.54 +definition ubound :: "real \<Rightarrow> real"
    1.55 +  where "ubound x = max 0 x"
    1.56  
    1.57  lemma lbound: "lbound x \<le> x"   
    1.58    by (simp add: lbound_def)
     2.1 --- a/src/HOL/Matrix/ComputeHOL.thy	Wed Aug 11 00:47:09 2010 +0200
     2.2 +++ b/src/HOL/Matrix/ComputeHOL.thy	Wed Aug 11 12:40:08 2010 +0200
     2.3 @@ -62,10 +62,8 @@
     2.4  lemma compute_None_None_eq: "(None = None) = True" by auto
     2.5  lemma compute_Some_Some_eq: "(Some x = Some y) = (x = y)" by auto
     2.6  
     2.7 -definition
     2.8 -   option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
     2.9 -where
    2.10 -   "option_case_compute opt a f = option_case a f opt"
    2.11 +definition option_case_compute :: "'b option \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a"
    2.12 +  where "option_case_compute opt a f = option_case a f opt"
    2.13  
    2.14  lemma option_case_compute: "option_case = (\<lambda> a f opt. option_case_compute opt a f)"
    2.15    by (simp add: option_case_compute_def)
    2.16 @@ -96,10 +94,8 @@
    2.17  
    2.18  (*** compute_list_case ***)
    2.19  
    2.20 -definition
    2.21 -  list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
    2.22 -where
    2.23 -  "list_case_compute l a f = list_case a f l"
    2.24 +definition list_case_compute :: "'b list \<Rightarrow> 'a \<Rightarrow> ('b \<Rightarrow> 'b list \<Rightarrow> 'a) \<Rightarrow> 'a"
    2.25 +  where "list_case_compute l a f = list_case a f l"
    2.26  
    2.27  lemma list_case_compute: "list_case = (\<lambda> (a::'a) f (l::'b list). list_case_compute l a f)"
    2.28    apply (rule ext)+
     3.1 --- a/src/HOL/Matrix/ComputeNumeral.thy	Wed Aug 11 00:47:09 2010 +0200
     3.2 +++ b/src/HOL/Matrix/ComputeNumeral.thy	Wed Aug 11 12:40:08 2010 +0200
     3.3 @@ -20,8 +20,7 @@
     3.4  lemmas bitiszero = iszero1 iszero2 iszero3 iszero4
     3.5  
     3.6  (* lezero for bit strings *)
     3.7 -definition
     3.8 -  "lezero x == (x \<le> 0)"
     3.9 +definition "lezero x \<longleftrightarrow> x \<le> 0"
    3.10  lemma lezero1: "lezero Int.Pls = True" unfolding Int.Pls_def lezero_def by auto
    3.11  lemma lezero2: "lezero Int.Min = True" unfolding Int.Min_def lezero_def by auto
    3.12  lemma lezero3: "lezero (Int.Bit0 x) = lezero x" unfolding Int.Bit0_def lezero_def by auto
    3.13 @@ -60,8 +59,7 @@
    3.14  
    3.15  lemmas bitarith = bitnorm bitiszero bitneg bitlezero biteq bitless bitle bitsucc bitpred bituminus bitadd bitmul 
    3.16  
    3.17 -definition
    3.18 -  "nat_norm_number_of (x::nat) == x"
    3.19 +definition "nat_norm_number_of (x::nat) = x"
    3.20  
    3.21  lemma nat_norm_number_of: "nat_norm_number_of (number_of w) = (if lezero w then 0 else number_of w)"
    3.22    apply (simp add: nat_norm_number_of_def)
    3.23 @@ -104,8 +102,7 @@
    3.24    by (auto simp add: number_of_is_id lezero_def nat_number_of_def)
    3.25  
    3.26  fun natfac :: "nat \<Rightarrow> nat"
    3.27 -where
    3.28 -   "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
    3.29 +  where "natfac n = (if n = 0 then 1 else n * (natfac (n - 1)))"
    3.30  
    3.31  lemmas compute_natarith = bitarith natnorm natsuc natadd natsub natmul nateq natless natle natfac.simps
    3.32  
     4.1 --- a/src/HOL/Matrix/Matrix.thy	Wed Aug 11 00:47:09 2010 +0200
     4.2 +++ b/src/HOL/Matrix/Matrix.thy	Wed Aug 11 12:40:08 2010 +0200
     4.3 @@ -367,15 +367,15 @@
     4.4  definition zero_closed :: "(('a::zero) \<Rightarrow> ('b::zero) \<Rightarrow> ('c::zero)) \<Rightarrow> bool" where
     4.5    "zero_closed f == (!x. f x 0 = 0) & (!y. f 0 y = 0)"
     4.6  
     4.7 -consts foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
     4.8 -primrec
     4.9 +primrec foldseq :: "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
    4.10 +where
    4.11    "foldseq f s 0 = s 0"
    4.12 -  "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
    4.13 +| "foldseq f s (Suc n) = f (s 0) (foldseq f (% k. s(Suc k)) n)"
    4.14  
    4.15 -consts foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
    4.16 -primrec
    4.17 +primrec foldseq_transposed ::  "('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a"
    4.18 +where
    4.19    "foldseq_transposed f s 0 = s 0"
    4.20 -  "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
    4.21 +| "foldseq_transposed f s (Suc n) = f (foldseq_transposed f s n) (s (Suc n))"
    4.22  
    4.23  lemma foldseq_assoc : "associative f \<Longrightarrow> foldseq f = foldseq_transposed f"
    4.24  proof -
     5.1 --- a/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 11 00:47:09 2010 +0200
     5.2 +++ b/src/HOL/Matrix/SparseMatrix.thy	Wed Aug 11 12:40:08 2010 +0200
     5.3 @@ -10,11 +10,11 @@
     5.4    'a spvec = "(nat * 'a) list"
     5.5    'a spmat = "('a spvec) spvec"
     5.6  
     5.7 -definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix" where
     5.8 -  sparse_row_vector_def: "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
     5.9 +definition sparse_row_vector :: "('a::ab_group_add) spvec \<Rightarrow> 'a matrix"
    5.10 +  where "sparse_row_vector arr = foldl (% m x. m + (singleton_matrix 0 (fst x) (snd x))) 0 arr"
    5.11  
    5.12 -definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix" where
    5.13 -  sparse_row_matrix_def: "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
    5.14 +definition sparse_row_matrix :: "('a::ab_group_add) spmat \<Rightarrow> 'a matrix"
    5.15 +  where "sparse_row_matrix arr = foldl (% m r. m + (move_matrix (sparse_row_vector (snd r)) (int (fst r)) 0)) 0 arr"
    5.16  
    5.17  code_datatype sparse_row_vector sparse_row_matrix
    5.18  
    5.19 @@ -57,13 +57,15 @@
    5.20    apply (auto simp add: sparse_row_matrix_cons)
    5.21    done
    5.22  
    5.23 -primrec sorted_spvec :: "'a spvec \<Rightarrow> bool" where
    5.24 +primrec sorted_spvec :: "'a spvec \<Rightarrow> bool"
    5.25 +where
    5.26    "sorted_spvec [] = True"
    5.27 -  | sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
    5.28 +| sorted_spvec_step: "sorted_spvec (a#as) = (case as of [] \<Rightarrow> True | b#bs \<Rightarrow> ((fst a < fst b) & (sorted_spvec as)))" 
    5.29  
    5.30 -primrec sorted_spmat :: "'a spmat \<Rightarrow> bool" where
    5.31 +primrec sorted_spmat :: "'a spmat \<Rightarrow> bool"
    5.32 +where
    5.33    "sorted_spmat [] = True"
    5.34 -  | "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
    5.35 +| "sorted_spmat (a#as) = ((sorted_spvec (snd a)) & (sorted_spmat as))"
    5.36  
    5.37  declare sorted_spvec.simps [simp del]
    5.38  
    5.39 @@ -99,13 +101,15 @@
    5.40    apply (simp add: sparse_row_matrix_cons neg_def)
    5.41    done
    5.42  
    5.43 -primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec" where
    5.44 +primrec minus_spvec :: "('a::ab_group_add) spvec \<Rightarrow> 'a spvec"
    5.45 +where
    5.46    "minus_spvec [] = []"
    5.47 -  | "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
    5.48 +| "minus_spvec (a#as) = (fst a, -(snd a))#(minus_spvec as)"
    5.49  
    5.50 -primrec abs_spvec ::  "('a::lattice_ab_group_add_abs) spvec \<Rightarrow> 'a spvec" where
    5.51 +primrec abs_spvec :: "('a::lattice_ab_group_add_abs) spvec \<Rightarrow> 'a spvec"
    5.52 +where
    5.53    "abs_spvec [] = []"
    5.54 -  | "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
    5.55 +| "abs_spvec (a#as) = (fst a, abs (snd a))#(abs_spvec as)"
    5.56  
    5.57  lemma sparse_row_vector_minus: 
    5.58    "sparse_row_vector (minus_spvec v) = - (sparse_row_vector v)"
    5.59 @@ -150,8 +154,7 @@
    5.60    apply (simp add: sorted_spvec.simps split:list.split_asm)
    5.61    done
    5.62    
    5.63 -definition
    5.64 -  "smult_spvec y = map (% a. (fst a, y * snd a))"  
    5.65 +definition "smult_spvec y = map (% a. (fst a, y * snd a))"  
    5.66  
    5.67  lemma smult_spvec_empty[simp]: "smult_spvec y [] = []"
    5.68    by (simp add: smult_spvec_def)
    5.69 @@ -159,10 +162,11 @@
    5.70  lemma smult_spvec_cons: "smult_spvec y (a#arr) = (fst a, y * (snd a)) # (smult_spvec y arr)"
    5.71    by (simp add: smult_spvec_def)
    5.72  
    5.73 -fun addmult_spvec :: "('a::ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
    5.74 -  "addmult_spvec y arr [] = arr" |
    5.75 -  "addmult_spvec y [] brr = smult_spvec y brr" |
    5.76 -  "addmult_spvec y ((i,a)#arr) ((j,b)#brr) = (
    5.77 +fun addmult_spvec :: "('a::ring) \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec"
    5.78 +where
    5.79 +  "addmult_spvec y arr [] = arr"
    5.80 +| "addmult_spvec y [] brr = smult_spvec y brr"
    5.81 +| "addmult_spvec y ((i,a)#arr) ((j,b)#brr) = (
    5.82      if i < j then ((i,a)#(addmult_spvec y arr ((j,b)#brr))) 
    5.83      else (if (j < i) then ((j, y * b)#(addmult_spvec y ((i,a)#arr) brr))
    5.84      else ((i, a + y*b)#(addmult_spvec y arr brr))))"
    5.85 @@ -235,11 +239,12 @@
    5.86    apply (simp_all add: sorted_spvec_addmult_spvec_helper3)
    5.87    done
    5.88  
    5.89 -fun mult_spvec_spmat :: "('a::lattice_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat  \<Rightarrow> 'a spvec" where
    5.90 +fun mult_spvec_spmat :: "('a::lattice_ring) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spmat  \<Rightarrow> 'a spvec"
    5.91 +where
    5.92  (* recdef mult_spvec_spmat "measure (% (c, arr, brr). (length arr) + (length brr))" *)
    5.93 -  "mult_spvec_spmat c [] brr = c" |
    5.94 -  "mult_spvec_spmat c arr [] = c" |
    5.95 -  "mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = (
    5.96 +  "mult_spvec_spmat c [] brr = c"
    5.97 +| "mult_spvec_spmat c arr [] = c"
    5.98 +| "mult_spvec_spmat c ((i,a)#arr) ((j,b)#brr) = (
    5.99       if (i < j) then mult_spvec_spmat c arr ((j,b)#brr)
   5.100       else if (j < i) then mult_spvec_spmat c ((i,a)#arr) brr 
   5.101       else mult_spvec_spmat (addmult_spvec a c b) arr brr)"
   5.102 @@ -342,12 +347,10 @@
   5.103    apply (simp_all add: sorted_addmult_spvec)
   5.104    done
   5.105  
   5.106 -consts 
   5.107 -  mult_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   5.108 -
   5.109 -primrec 
   5.110 +primrec mult_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   5.111 +where
   5.112    "mult_spmat [] A = []"
   5.113 -  "mult_spmat (a#as) A = (fst a, mult_spvec_spmat [] (snd a) A)#(mult_spmat as A)"
   5.114 +| "mult_spmat (a#as) A = (fst a, mult_spvec_spmat [] (snd a) A)#(mult_spmat as A)"
   5.115  
   5.116  lemma sparse_row_mult_spmat: 
   5.117    "sorted_spmat A \<Longrightarrow> sorted_spvec B \<Longrightarrow>
   5.118 @@ -372,12 +375,13 @@
   5.119    done
   5.120  
   5.121  
   5.122 -fun add_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec" where
   5.123 +fun add_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> 'a spvec"
   5.124 +where
   5.125  (* "measure (% (a, b). length a + (length b))" *)
   5.126 -  "add_spvec arr [] = arr" |
   5.127 -  "add_spvec [] brr = brr" |
   5.128 -  "add_spvec ((i,a)#arr) ((j,b)#brr) = (
   5.129 -  if i < j then (i,a)#(add_spvec arr ((j,b)#brr)) 
   5.130 +  "add_spvec arr [] = arr"
   5.131 +| "add_spvec [] brr = brr"
   5.132 +| "add_spvec ((i,a)#arr) ((j,b)#brr) = (
   5.133 +     if i < j then (i,a)#(add_spvec arr ((j,b)#brr)) 
   5.134       else if (j < i) then (j,b) # add_spvec ((i,a)#arr) brr
   5.135       else (i, a+b) # add_spvec arr brr)"
   5.136  
   5.137 @@ -389,17 +393,18 @@
   5.138    apply (simp_all add: singleton_matrix_add)
   5.139    done
   5.140  
   5.141 -fun add_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
   5.142 +fun add_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   5.143 +where
   5.144  (* "measure (% (A,B). (length A)+(length B))" *)
   5.145 -  "add_spmat [] bs = bs" |
   5.146 -  "add_spmat as [] = as" |
   5.147 -  "add_spmat ((i,a)#as) ((j,b)#bs) = (
   5.148 -  if i < j then 
   5.149 -    (i,a) # add_spmat as ((j,b)#bs)
   5.150 -  else if j < i then
   5.151 -    (j,b) # add_spmat ((i,a)#as) bs
   5.152 -  else
   5.153 -    (i, add_spvec a b) # add_spmat as bs)"
   5.154 +  "add_spmat [] bs = bs"
   5.155 +| "add_spmat as [] = as"
   5.156 +| "add_spmat ((i,a)#as) ((j,b)#bs) = (
   5.157 +    if i < j then 
   5.158 +      (i,a) # add_spmat as ((j,b)#bs)
   5.159 +    else if j < i then
   5.160 +      (j,b) # add_spmat ((i,a)#as) bs
   5.161 +    else
   5.162 +      (i, add_spvec a b) # add_spmat as bs)"
   5.163  
   5.164  lemma add_spmat_Nil2[simp]: "add_spmat as [] = as"
   5.165  by(cases as) auto
   5.166 @@ -532,28 +537,31 @@
   5.167    apply (simp_all add: sorted_spvec_add_spvec)
   5.168    done
   5.169  
   5.170 -fun le_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> bool" where
   5.171 +fun le_spvec :: "('a::lattice_ab_group_add) spvec \<Rightarrow> 'a spvec \<Rightarrow> bool"
   5.172 +where
   5.173  (* "measure (% (a,b). (length a) + (length b))" *)
   5.174 -  "le_spvec [] [] = True" |
   5.175 -  "le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])" |
   5.176 -  "le_spvec [] ((_,b)#bs) = (0 <= b & le_spvec [] bs)" |
   5.177 -  "le_spvec ((i,a)#as) ((j,b)#bs) = (
   5.178 -  if (i < j) then a <= 0 & le_spvec as ((j,b)#bs)
   5.179 -  else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs
   5.180 -  else a <= b & le_spvec as bs)"
   5.181 +  "le_spvec [] [] = True"
   5.182 +| "le_spvec ((_,a)#as) [] = (a <= 0 & le_spvec as [])"
   5.183 +| "le_spvec [] ((_,b)#bs) = (0 <= b & le_spvec [] bs)"
   5.184 +| "le_spvec ((i,a)#as) ((j,b)#bs) = (
   5.185 +    if (i < j) then a <= 0 & le_spvec as ((j,b)#bs)
   5.186 +    else if (j < i) then 0 <= b & le_spvec ((i,a)#as) bs
   5.187 +    else a <= b & le_spvec as bs)"
   5.188  
   5.189 -fun le_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> bool" where
   5.190 +fun le_spmat :: "('a::lattice_ab_group_add) spmat \<Rightarrow> 'a spmat \<Rightarrow> bool"
   5.191 +where
   5.192  (* "measure (% (a,b). (length a) + (length b))" *)
   5.193 -  "le_spmat [] [] = True" |
   5.194 -  "le_spmat ((i,a)#as) [] = (le_spvec a [] & le_spmat as [])" |
   5.195 -  "le_spmat [] ((j,b)#bs) = (le_spvec [] b & le_spmat [] bs)" |
   5.196 -  "le_spmat ((i,a)#as) ((j,b)#bs) = (
   5.197 -  if i < j then (le_spvec a [] & le_spmat as ((j,b)#bs))
   5.198 -  else if j < i then (le_spvec [] b & le_spmat ((i,a)#as) bs)
   5.199 -  else (le_spvec a b & le_spmat as bs))"
   5.200 +  "le_spmat [] [] = True"
   5.201 +| "le_spmat ((i,a)#as) [] = (le_spvec a [] & le_spmat as [])"
   5.202 +| "le_spmat [] ((j,b)#bs) = (le_spvec [] b & le_spmat [] bs)"
   5.203 +| "le_spmat ((i,a)#as) ((j,b)#bs) = (
   5.204 +    if i < j then (le_spvec a [] & le_spmat as ((j,b)#bs))
   5.205 +    else if j < i then (le_spvec [] b & le_spmat ((i,a)#as) bs)
   5.206 +    else (le_spvec a b & le_spmat as bs))"
   5.207  
   5.208  definition disj_matrices :: "('a::zero) matrix \<Rightarrow> 'a matrix \<Rightarrow> bool" where
   5.209 -  "disj_matrices A B == (! j i. (Rep_matrix A j i \<noteq> 0) \<longrightarrow> (Rep_matrix B j i = 0)) & (! j i. (Rep_matrix B j i \<noteq> 0) \<longrightarrow> (Rep_matrix A j i = 0))"  
   5.210 +  "disj_matrices A B \<longleftrightarrow>
   5.211 +    (! 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))"  
   5.212  
   5.213  declare [[simp_depth_limit = 6]]
   5.214  
   5.215 @@ -730,13 +738,15 @@
   5.216  
   5.217  declare [[simp_depth_limit = 999]]
   5.218  
   5.219 -primrec abs_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat" where
   5.220 -  "abs_spmat [] = []" |
   5.221 -  "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)"
   5.222 +primrec abs_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat"
   5.223 +where
   5.224 +  "abs_spmat [] = []"
   5.225 +| "abs_spmat (a#as) = (fst a, abs_spvec (snd a))#(abs_spmat as)"
   5.226  
   5.227 -primrec minus_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat" where
   5.228 -  "minus_spmat [] = []" |
   5.229 -  "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)"
   5.230 +primrec minus_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat"
   5.231 +where
   5.232 +  "minus_spmat [] = []"
   5.233 +| "minus_spmat (a#as) = (fst a, minus_spvec (snd a))#(minus_spmat as)"
   5.234  
   5.235  lemma sparse_row_matrix_minus:
   5.236    "sparse_row_matrix (minus_spmat A) = - (sparse_row_matrix A)"
   5.237 @@ -801,8 +811,8 @@
   5.238    apply (simp_all add: sorted_spvec_abs_spvec)
   5.239    done
   5.240  
   5.241 -definition diff_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
   5.242 -  "diff_spmat A B == add_spmat A (minus_spmat B)"
   5.243 +definition diff_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat"
   5.244 +  where "diff_spmat A B = add_spmat A (minus_spmat B)"
   5.245  
   5.246  lemma sorted_spmat_diff_spmat: "sorted_spmat A \<Longrightarrow> sorted_spmat B \<Longrightarrow> sorted_spmat (diff_spmat A B)"
   5.247    by (simp add: diff_spmat_def sorted_spmat_minus_spmat sorted_spmat_add_spmat)
   5.248 @@ -813,8 +823,8 @@
   5.249  lemma sparse_row_diff_spmat: "sparse_row_matrix (diff_spmat A B ) = (sparse_row_matrix A) - (sparse_row_matrix B)"
   5.250    by (simp add: diff_spmat_def sparse_row_add_spmat sparse_row_matrix_minus)
   5.251  
   5.252 -definition sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool" where
   5.253 -  "sorted_sparse_matrix A == (sorted_spvec A) & (sorted_spmat A)"
   5.254 +definition sorted_sparse_matrix :: "'a spmat \<Rightarrow> bool"
   5.255 +  where "sorted_sparse_matrix A \<longleftrightarrow> sorted_spvec A & sorted_spmat A"
   5.256  
   5.257  lemma sorted_sparse_matrix_imp_spvec: "sorted_sparse_matrix A \<Longrightarrow> sorted_spvec A"
   5.258    by (simp add: sorted_sparse_matrix_def)
   5.259 @@ -841,29 +851,25 @@
   5.260  
   5.261  lemma if_case_eq: "(if b then x else y) = (case b of True => x | False => y)" by simp
   5.262  
   5.263 -consts
   5.264 -  pprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
   5.265 -  nprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
   5.266 -  pprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
   5.267 -  nprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
   5.268 +primrec pprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
   5.269 +where
   5.270 +  "pprt_spvec [] = []"
   5.271 +| "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
   5.272  
   5.273 -primrec
   5.274 -  "pprt_spvec [] = []"
   5.275 -  "pprt_spvec (a#as) = (fst a, pprt (snd a)) # (pprt_spvec as)"
   5.276 -
   5.277 -primrec
   5.278 +primrec nprt_spvec :: "('a::{lattice_ab_group_add}) spvec \<Rightarrow> 'a spvec"
   5.279 +where
   5.280    "nprt_spvec [] = []"
   5.281 -  "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
   5.282 +| "nprt_spvec (a#as) = (fst a, nprt (snd a)) # (nprt_spvec as)"
   5.283  
   5.284 -primrec 
   5.285 +primrec pprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
   5.286 +where
   5.287    "pprt_spmat [] = []"
   5.288 -  "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
   5.289 -  (*case (pprt_spvec (snd a)) of [] \<Rightarrow> (pprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(pprt_spmat as))"*)
   5.290 +| "pprt_spmat (a#as) = (fst a, pprt_spvec (snd a))#(pprt_spmat as)"
   5.291  
   5.292 -primrec 
   5.293 +primrec nprt_spmat :: "('a::{lattice_ab_group_add}) spmat \<Rightarrow> 'a spmat"
   5.294 +where
   5.295    "nprt_spmat [] = []"
   5.296 -  "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
   5.297 -  (*case (nprt_spvec (snd a)) of [] \<Rightarrow> (nprt_spmat as) | y#ys \<Rightarrow> (fst a, y#ys)#(nprt_spmat as))"*)
   5.298 +| "nprt_spmat (a#as) = (fst a, nprt_spvec (snd a))#(nprt_spmat as)"
   5.299  
   5.300  
   5.301  lemma pprt_add: "disj_matrices A (B::(_::lattice_ring) matrix) \<Longrightarrow> pprt (A+B) = pprt A + pprt B"
   5.302 @@ -1012,7 +1018,7 @@
   5.303    done
   5.304  
   5.305  definition mult_est_spmat :: "('a::lattice_ring) spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat \<Rightarrow> 'a spmat" where
   5.306 -  "mult_est_spmat r1 r2 s1 s2 == 
   5.307 +  "mult_est_spmat r1 r2 s1 s2 =
   5.308    add_spmat (mult_spmat (pprt_spmat s2) (pprt_spmat r2)) (add_spmat (mult_spmat (pprt_spmat s1) (nprt_spmat r2)) 
   5.309    (add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))"  
   5.310