# 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.0 ≤ e2.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.0 ≤ e2.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