Up to index of Isabelle/HOL/HOL-Complex/HOL-Complex-Matrix
theory MatrixLP(* 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