Theory MatrixLP

Up to index of Isabelle/HOL/HOL-Complex/HOL-Complex-Matrix

theory MatrixLP
imports Cplex
uses [MatrixLP.ML]
begin

(*  Title:      HOL/Matrix/cplex/MatrixLP.thy
    ID:         $Id: MatrixLP.thy,v 1.1 2005/07/19 14:16:54 obua Exp $
    Author:     Steven Obua
*)

theory MatrixLP 
imports Cplex
begin

constdefs
  list_case_compute :: "'b list => 'a => ('b => 'b list => 'a) => 'a"
  "list_case_compute l a f == list_case a f l"

lemma list_case_compute: "list_case = (λ (a::'a) f (l::'b list). list_case_compute l a f)"
  apply (rule ext)+
  apply (simp add: list_case_compute_def)
  done

lemma list_case_compute_empty: "list_case_compute ([]::'b list) = (λ (a::'a) f. a)"
  apply (rule ext)+
  apply (simp add: list_case_compute_def)
  done

lemma list_case_compute_cons: "list_case_compute (u#v) = (λ (a::'a) f. (f (u::'b) v))"
  apply (rule ext)+
  apply (simp add: list_case_compute_def)
  done

lemma If_True: "(If True) = (λ x y. x)"
  apply (rule ext)+
  apply auto
  done

lemma If_False: "(If False) = (λ x y. y)"
  apply (rule ext)+
  apply auto
  done

lemma Let_compute: "Let (x::'a) f = ((f x)::'b)"
  by (simp add: Let_def)

lemma fst_compute: "fst (a::'a, b::'b) = a"
  by auto

lemma snd_compute: "snd (a::'a, b::'b) = b"
  by auto

lemma bool1: "(¬ True) = False"  by blast
lemma bool2: "(¬ False) = True"  by blast
lemma bool3: "((P::bool) ∧ True) = P" by blast
lemma bool4: "(True ∧ (P::bool)) = P" by blast
lemma bool5: "((P::bool) ∧ False) = False" by blast
lemma bool6: "(False ∧ (P::bool)) = False" by blast
lemma bool7: "((P::bool) ∨ True) = True" by blast
lemma bool8: "(True ∨ (P::bool)) = True" by blast
lemma bool9: "((P::bool) ∨ False) = P" by blast
lemma bool10: "(False ∨ (P::bool)) = P" by blast
lemmas boolarith = bool1 bool2 bool3 bool4 bool5 bool6 bool7 bool8 bool9 bool10

lemmas float_arith = Float.arith
lemmas sparse_row_matrix_arith_simps = SparseMatrix.sparse_row_matrix_arith_simps
lemmas sorted_sp_simps = SparseMatrix.sorted_sp_simps
lemmas fst_snd_conv = Product_Type.fst_conv Product_Type.snd_conv

end


lemma list_case_compute:

  list_case = (%a f l. list_case_compute l a f)

lemma list_case_compute_empty:

  list_case_compute [] = (%a f. a)

lemma list_case_compute_cons:

  list_case_compute (u # v) = (%a f. f u v)

lemma If_True:

  If True = (%x y. x)

lemma If_False:

  If False = (%x y. y)

lemma Let_compute:

  Let x f = f x

lemma fst_compute:

  fst (a, b) = a

lemma snd_compute:

  snd (a, b) = b

lemma bool1:

  (¬ True) = False

lemma bool2:

  (¬ False) = True

lemma bool3:

  (P ∧ True) = P

lemma bool4:

  (True ∧ P) = P

lemma bool5:

  (P ∧ False) = False

lemma bool6:

  (False ∧ P) = False

lemma bool7:

  (P ∨ True) = True

lemma bool8:

  (True ∨ P) = True

lemma bool9:

  (P ∨ False) = P

lemma bool10:

  (False ∨ P) = P

lemmas boolarith:

  (¬ True) = False
  (¬ False) = True
  (P ∧ True) = P
  (True ∧ P) = P
  (P ∧ False) = False
  (False ∧ P) = False
  (P ∨ True) = True
  (True ∨ P) = True
  (P ∨ False) = P
  (False ∨ P) = P

lemmas boolarith:

  (¬ True) = False
  (¬ False) = True
  (P ∧ True) = P
  (True ∧ P) = P
  (P ∧ False) = False
  (False ∧ P) = False
  (P ∨ True) = True
  (True ∨ P) = True
  (P ∨ False) = P
  (False ∨ P) = P

lemmas float_arith:

  Numeral.Pls BIT bit.B0 = Numeral.Pls
  Numeral.Min BIT bit.B1 = Numeral.Min
  bin_pred Numeral.Pls = Numeral.Min
  bin_pred Numeral.Min = Numeral.Min BIT bit.B0
  bin_pred (w BIT bit.B1) = w BIT bit.B0
  bin_pred (w BIT bit.B0) = bin_pred w BIT bit.B1
  bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1
  bin_succ Numeral.Min = Numeral.Pls
  bin_succ (w BIT bit.B1) = bin_succ w BIT bit.B0
  bin_succ (w BIT bit.B0) = w BIT bit.B1
  bin_add Numeral.Pls w = w
  bin_add Numeral.Min w = bin_pred w
  bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y
  bin_add (v BIT bit.B1) (w BIT bit.B0) = bin_add v w BIT bit.B1
  bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0
  bin_minus Numeral.Pls = Numeral.Pls
  bin_minus Numeral.Min = Numeral.Pls BIT bit.B1
  bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1
  bin_minus (w BIT bit.B0) = bin_minus w BIT bit.B0
  bin_mult Numeral.Pls w = Numeral.Pls
  bin_mult Numeral.Min w = bin_minus w
  bin_mult (v BIT bit.B1) w = bin_add (bin_mult v w BIT bit.B0) w
  bin_mult (v BIT bit.B0) w = bin_mult v w BIT bit.B0
  bin_add w Numeral.Pls = w
  bin_add w Numeral.Min = bin_pred w
  number_of v + number_of w = number_of (bin_add v w)
  - number_of v = number_of (bin_minus v)
  number_of v - number_of w = number_of (bin_add v (bin_minus w))
  number_of v * number_of w = number_of (bin_mult v w)
  (number_of v = number_of w) = iszero (number_of (bin_add v (bin_minus w)))
  iszero Numeral0 = True
  iszero -1 = False
  iszero (number_of (w BIT bit.B0)) = iszero (number_of w)
  (¬ iszero (number_of (w1 BIT bit.B1))) = True
  (number_of x < number_of y) = neg (number_of (bin_add x (bin_minus y)))
  neg Numeral0 = False
  neg -1 = True
  neg (number_of (w BIT x)) = neg (number_of w)
  (number_of x ≤ number_of y) = (¬ neg (number_of (bin_add y (bin_minus x))))
  number_of v + number_of v' =
  (if neg (number_of v) then number_of v'
   else if neg (number_of v') then number_of v else number_of (bin_add v v'))
  number_of v - number_of v' =
  (if neg (number_of v') then number_of v
   else let d = number_of (bin_add v (bin_minus v'))
        in if neg d then 0 else nat d)
  number_of v * number_of v' =
  (if neg (number_of v) then 0 else number_of (bin_mult v v'))
  (number_of v = number_of v') =
  (if neg (number_of v) then iszero (number_of v') ∨ neg (number_of v')
   else if neg (number_of v') then iszero (number_of v)
        else iszero (number_of (bin_add v (bin_minus v'))))
  (number_of v < number_of v') =
  (if neg (number_of v) then neg (number_of (bin_minus v'))
   else neg (number_of (bin_add v (bin_minus v'))))
  nat (number_of w) = number_of w
  z ^ number_of (w BIT bit.B0) = (let w = z ^ number_of w in w * w)
  z ^ number_of (w BIT bit.B1) =
  (if Numeral0 ≤ number_of w then let w = z ^ number_of w in z * w * w
   else Numeral1)
  z ^ Numeral0 = Numeral1
  z ^ -1 = Numeral1
  float (a1.0, e1.0) + float (a2.0, e2.0) =
  (if e1.0e2.0 then float (a1.0 + a2.0 * 2 ^ nat (e2.0 - e1.0), e1.0)
   else float (a1.0 * 2 ^ nat (e1.0 - e2.0) + a2.0, e2.0))
  float (a1.0, e1.0) * float (a2.0, e2.0) = float (a1.0 * a2.0, e1.0 + e2.0)
  - float (a, b) = float (- a, b)
  ¦float (a, b)¦ = (if Numeral0 ≤ a then float (a, b) else float (- a, b))
  (Numeral0 ≤ float (a, b)) = (Numeral0 ≤ a)
  pprt (float (a, b)) =
  (if Numeral0 ≤ a then float (a, b) else float (Numeral0, b))
  nprt (float (a, b)) =
  (if Numeral0 ≤ a then float (Numeral0, b) else float (a, b))
  (¬ False) = True
  (¬ True) = False

lemmas float_arith:

  Numeral.Pls BIT bit.B0 = Numeral.Pls
  Numeral.Min BIT bit.B1 = Numeral.Min
  bin_pred Numeral.Pls = Numeral.Min
  bin_pred Numeral.Min = Numeral.Min BIT bit.B0
  bin_pred (w BIT bit.B1) = w BIT bit.B0
  bin_pred (w BIT bit.B0) = bin_pred w BIT bit.B1
  bin_succ Numeral.Pls = Numeral.Pls BIT bit.B1
  bin_succ Numeral.Min = Numeral.Pls
  bin_succ (w BIT bit.B1) = bin_succ w BIT bit.B0
  bin_succ (w BIT bit.B0) = w BIT bit.B1
  bin_add Numeral.Pls w = w
  bin_add Numeral.Min w = bin_pred w
  bin_add (v BIT bit.B0) (w BIT y) = bin_add v w BIT y
  bin_add (v BIT bit.B1) (w BIT bit.B0) = bin_add v w BIT bit.B1
  bin_add (v BIT bit.B1) (w BIT bit.B1) = bin_add v (bin_succ w) BIT bit.B0
  bin_minus Numeral.Pls = Numeral.Pls
  bin_minus Numeral.Min = Numeral.Pls BIT bit.B1
  bin_minus (w BIT bit.B1) = bin_pred (bin_minus w) BIT bit.B1
  bin_minus (w BIT bit.B0) = bin_minus w BIT bit.B0
  bin_mult Numeral.Pls w = Numeral.Pls
  bin_mult Numeral.Min w = bin_minus w
  bin_mult (v BIT bit.B1) w = bin_add (bin_mult v w BIT bit.B0) w
  bin_mult (v BIT bit.B0) w = bin_mult v w BIT bit.B0
  bin_add w Numeral.Pls = w
  bin_add w Numeral.Min = bin_pred w
  number_of v + number_of w = number_of (bin_add v w)
  - number_of v = number_of (bin_minus v)
  number_of v - number_of w = number_of (bin_add v (bin_minus w))
  number_of v * number_of w = number_of (bin_mult v w)
  (number_of v = number_of w) = iszero (number_of (bin_add v (bin_minus w)))
  iszero Numeral0 = True
  iszero -1 = False
  iszero (number_of (w BIT bit.B0)) = iszero (number_of w)
  (¬ iszero (number_of (w1 BIT bit.B1))) = True
  (number_of x < number_of y) = neg (number_of (bin_add x (bin_minus y)))
  neg Numeral0 = False
  neg -1 = True
  neg (number_of (w BIT x)) = neg (number_of w)
  (number_of x ≤ number_of y) = (¬ neg (number_of (bin_add y (bin_minus x))))
  number_of v + number_of v' =
  (if neg (number_of v) then number_of v'
   else if neg (number_of v') then number_of v else number_of (bin_add v v'))
  number_of v - number_of v' =
  (if neg (number_of v') then number_of v
   else let d = number_of (bin_add v (bin_minus v'))
        in if neg d then 0 else nat d)
  number_of v * number_of v' =
  (if neg (number_of v) then 0 else number_of (bin_mult v v'))
  (number_of v = number_of v') =
  (if neg (number_of v) then iszero (number_of v') ∨ neg (number_of v')
   else if neg (number_of v') then iszero (number_of v)
        else iszero (number_of (bin_add v (bin_minus v'))))
  (number_of v < number_of v') =
  (if neg (number_of v) then neg (number_of (bin_minus v'))
   else neg (number_of (bin_add v (bin_minus v'))))
  nat (number_of w) = number_of w
  z ^ number_of (w BIT bit.B0) = (let w = z ^ number_of w in w * w)
  z ^ number_of (w BIT bit.B1) =
  (if Numeral0 ≤ number_of w then let w = z ^ number_of w in z * w * w
   else Numeral1)
  z ^ Numeral0 = Numeral1
  z ^ -1 = Numeral1
  float (a1.0, e1.0) + float (a2.0, e2.0) =
  (if e1.0e2.0 then float (a1.0 + a2.0 * 2 ^ nat (e2.0 - e1.0), e1.0)
   else float (a1.0 * 2 ^ nat (e1.0 - e2.0) + a2.0, e2.0))
  float (a1.0, e1.0) * float (a2.0, e2.0) = float (a1.0 * a2.0, e1.0 + e2.0)
  - float (a, b) = float (- a, b)
  ¦float (a, b)¦ = (if Numeral0 ≤ a then float (a, b) else float (- a, b))
  (Numeral0 ≤ float (a, b)) = (Numeral0 ≤ a)
  pprt (float (a, b)) =
  (if Numeral0 ≤ a then float (a, b) else float (Numeral0, b))
  nprt (float (a, b)) =
  (if Numeral0 ≤ a then float (Numeral0, b) else float (a, b))
  (¬ False) = True
  (¬ True) = False

lemmas sparse_row_matrix_arith_simps:

  mult_spmat [] A = []
  mult_spmat (a # as) A =
  (fst a, mult_spvec_spmat ([], snd a, A)) # mult_spmat as A
  mult_spvec_spmat (c, [], brr) = c
  mult_spvec_spmat (c, y # z, []) = c
  mult_spvec_spmat (c, a # arr, b # brr) =
  (if fst a < fst b then mult_spvec_spmat (c, arr, b # brr)
   else if fst b < fst a then mult_spvec_spmat (c, a # arr, brr)
        else mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))
  addmult_spvec (y, arr, []) = arr
  addmult_spvec (y, [], ae # af) = smult_spvec y (ae # af)
  addmult_spvec (y, a # arr, b # brr) =
  (if fst a < fst b then a # addmult_spvec (y, arr, b # brr)
   else if fst b < fst a then (fst b, y * snd b) # addmult_spvec (y, a # arr, brr)
        else (fst a, snd a + y * snd b) # addmult_spvec (y, arr, brr))
  smult_spvec y [] = []
  smult_spvec y (a # arr) = (fst a, y * snd a) # smult_spvec y arr
  add_spmat ([], bs) = bs
  add_spmat (w # x, []) = w # x
  add_spmat (a # as, b # bs) =
  (if fst a < fst b then a # add_spmat (as, b # bs)
   else if fst b < fst a then b # add_spmat (a # as, bs)
        else (fst a, add_spvec (snd a, snd b)) # add_spmat (as, bs))
  add_spvec (arr, []) = arr
  add_spvec ([], ab # ac) = ab # ac
  add_spvec (a # arr, b # brr) =
  (if fst a < fst b then a # add_spvec (arr, b # brr)
   else if fst b < fst a then b # add_spvec (a # arr, brr)
        else (fst a, snd a + snd b) # add_spvec (arr, brr))
  minus_spmat [] = []
  minus_spmat (a # as) = (fst a, minus_spvec (snd a)) # minus_spmat as
  minus_spvec [] = []
  minus_spvec (a # as) = (fst a, - snd a) # minus_spvec as
  abs_spmat [] = []
  abs_spmat (a # as) = (fst a, abs_spvec (snd a)) # abs_spmat as
  abs_spvec [] = []
  abs_spvec (a # as) = (fst a, ¦snd a¦) # abs_spvec as
  diff_spmat A B == add_spmat (A, minus_spmat B)
  le_spmat ([], []) = True
  le_spmat (a # as, []) = (le_spvec (snd a, []) ∧ le_spmat (as, []))
  le_spmat ([], b # bs) = (le_spvec ([], snd b) ∧ le_spmat ([], bs))
  le_spmat (a # as, b # bs) =
  (if fst a < fst b then le_spvec (snd a, []) ∧ le_spmat (as, b # bs)
   else if fst b < fst a then le_spvec ([], snd b) ∧ le_spmat (a # as, bs)
        else le_spvec (snd a, snd b) ∧ le_spmat (as, bs))
  le_spvec ([], []) = True
  le_spvec (a # as, []) = (snd a ≤ (0::'a) ∧ le_spvec (as, []))
  le_spvec ([], b # bs) = ((0::'a) ≤ snd b ∧ le_spvec ([], bs))
  le_spvec (a # as, b # bs) =
  (if fst a < fst b then snd a ≤ (0::'a) ∧ le_spvec (as, b # bs)
   else if fst b < fst a then (0::'a) ≤ snd b ∧ le_spvec (a # as, bs)
        else snd a ≤ snd b ∧ le_spvec (as, bs))
  pprt_spmat [] = []
  pprt_spmat (a # as) = (fst a, pprt_spvec (snd a)) # pprt_spmat as
  pprt_spvec [] = []
  pprt_spvec (a # as) = (fst a, pprt (snd a)) # pprt_spvec as
  nprt_spmat [] = []
  nprt_spmat (a # as) = (fst a, nprt_spvec (snd a)) # nprt_spmat as
  nprt_spvec [] = []
  nprt_spvec (a # as) = (fst a, nprt (snd a)) # nprt_spvec as
  mult_est_spmat r1.0 r2.0 s1.0 s2.0 ==
  add_spmat
   (mult_spmat (pprt_spmat s2.0) (pprt_spmat r2.0),
    add_spmat
     (mult_spmat (pprt_spmat s1.0) (nprt_spmat r2.0),
      add_spmat
       (mult_spmat (nprt_spmat s2.0) (pprt_spmat r1.0),
        mult_spmat (nprt_spmat s1.0) (nprt_spmat r1.0))))

lemmas sparse_row_matrix_arith_simps:

  mult_spmat [] A = []
  mult_spmat (a # as) A =
  (fst a, mult_spvec_spmat ([], snd a, A)) # mult_spmat as A
  mult_spvec_spmat (c, [], brr) = c
  mult_spvec_spmat (c, y # z, []) = c
  mult_spvec_spmat (c, a # arr, b # brr) =
  (if fst a < fst b then mult_spvec_spmat (c, arr, b # brr)
   else if fst b < fst a then mult_spvec_spmat (c, a # arr, brr)
        else mult_spvec_spmat (addmult_spvec (snd a, c, snd b), arr, brr))
  addmult_spvec (y, arr, []) = arr
  addmult_spvec (y, [], ae # af) = smult_spvec y (ae # af)
  addmult_spvec (y, a # arr, b # brr) =
  (if fst a < fst b then a # addmult_spvec (y, arr, b # brr)
   else if fst b < fst a then (fst b, y * snd b) # addmult_spvec (y, a # arr, brr)
        else (fst a, snd a + y * snd b) # addmult_spvec (y, arr, brr))
  smult_spvec y [] = []
  smult_spvec y (a # arr) = (fst a, y * snd a) # smult_spvec y arr
  add_spmat ([], bs) = bs
  add_spmat (w # x, []) = w # x
  add_spmat (a # as, b # bs) =
  (if fst a < fst b then a # add_spmat (as, b # bs)
   else if fst b < fst a then b # add_spmat (a # as, bs)
        else (fst a, add_spvec (snd a, snd b)) # add_spmat (as, bs))
  add_spvec (arr, []) = arr
  add_spvec ([], ab # ac) = ab # ac
  add_spvec (a # arr, b # brr) =
  (if fst a < fst b then a # add_spvec (arr, b # brr)
   else if fst b < fst a then b # add_spvec (a # arr, brr)
        else (fst a, snd a + snd b) # add_spvec (arr, brr))
  minus_spmat [] = []
  minus_spmat (a # as) = (fst a, minus_spvec (snd a)) # minus_spmat as
  minus_spvec [] = []
  minus_spvec (a # as) = (fst a, - snd a) # minus_spvec as
  abs_spmat [] = []
  abs_spmat (a # as) = (fst a, abs_spvec (snd a)) # abs_spmat as
  abs_spvec [] = []
  abs_spvec (a # as) = (fst a, ¦snd a¦) # abs_spvec as
  diff_spmat A B == add_spmat (A, minus_spmat B)
  le_spmat ([], []) = True
  le_spmat (a # as, []) = (le_spvec (snd a, []) ∧ le_spmat (as, []))
  le_spmat ([], b # bs) = (le_spvec ([], snd b) ∧ le_spmat ([], bs))
  le_spmat (a # as, b # bs) =
  (if fst a < fst b then le_spvec (snd a, []) ∧ le_spmat (as, b # bs)
   else if fst b < fst a then le_spvec ([], snd b) ∧ le_spmat (a # as, bs)
        else le_spvec (snd a, snd b) ∧ le_spmat (as, bs))
  le_spvec ([], []) = True
  le_spvec (a # as, []) = (snd a ≤ (0::'a) ∧ le_spvec (as, []))
  le_spvec ([], b # bs) = ((0::'a) ≤ snd b ∧ le_spvec ([], bs))
  le_spvec (a # as, b # bs) =
  (if fst a < fst b then snd a ≤ (0::'a) ∧ le_spvec (as, b # bs)
   else if fst b < fst a then (0::'a) ≤ snd b ∧ le_spvec (a # as, bs)
        else snd a ≤ snd b ∧ le_spvec (as, bs))
  pprt_spmat [] = []
  pprt_spmat (a # as) = (fst a, pprt_spvec (snd a)) # pprt_spmat as
  pprt_spvec [] = []
  pprt_spvec (a # as) = (fst a, pprt (snd a)) # pprt_spvec as
  nprt_spmat [] = []
  nprt_spmat (a # as) = (fst a, nprt_spvec (snd a)) # nprt_spmat as
  nprt_spvec [] = []
  nprt_spvec (a # as) = (fst a, nprt (snd a)) # nprt_spvec as
  mult_est_spmat r1.0 r2.0 s1.0 s2.0 ==
  add_spmat
   (mult_spmat (pprt_spmat s2.0) (pprt_spmat r2.0),
    add_spmat
     (mult_spmat (pprt_spmat s1.0) (nprt_spmat r2.0),
      add_spmat
       (mult_spmat (nprt_spmat s2.0) (pprt_spmat r1.0),
        mult_spmat (nprt_spmat s1.0) (nprt_spmat r1.0))))

lemmas sorted_sp_simps:

  sorted_spvec [] = True
  sorted_spvec (a # as) =
  (case as of [] => True | b # bs => fst a < fst b ∧ sorted_spvec as)
  sorted_spmat [] = True
  sorted_spmat (a # as) = (sorted_spvec (snd a) ∧ sorted_spmat as)
  sorted_sparse_matrix A == sorted_spvec A ∧ sorted_spmat A

lemmas sorted_sp_simps:

  sorted_spvec [] = True
  sorted_spvec (a # as) =
  (case as of [] => True | b # bs => fst a < fst b ∧ sorted_spvec as)
  sorted_spmat [] = True
  sorted_spmat (a # as) = (sorted_spvec (snd a) ∧ sorted_spmat as)
  sorted_sparse_matrix A == sorted_spvec A ∧ sorted_spmat A

lemmas fst_snd_conv:

  fst (a, b) = a
  snd (a, b) = b

lemmas fst_snd_conv:

  fst (a, b) = a
  snd (a, b) = b