isabelle: src/HOL/Matrix/Cplex.thy@cce7e6197a46 (annotated)

41959 b460124855b8 tuned headers; wenzelm parents: 37764 diff changeset	1	(* Title: HOL/Matrix/Cplex.thy
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	2	Author: Steven Obua
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	3	*)
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	4
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	5	theory Cplex
32491 d5d8bea0cd94 reorganized Compute theories for HOL-Matrix -- avoiding theory files within main HOL/Tools; wenzelm parents: 31816 diff changeset	6	imports SparseMatrix LP ComputeFloat ComputeNumeral
28637 7aabaf1ba263 reactivated HOL-Matrix; wenzelm parents: 27484 diff changeset	7	uses "Cplex_tools.ML" "CplexMatrixConverter.ML" "FloatSparseMatrixBuilder.ML"
7aabaf1ba263 reactivated HOL-Matrix; wenzelm parents: 27484 diff changeset	8	"fspmlp.ML" ("matrixlp.ML")
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	9	begin
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	10
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	11	lemma spm_mult_le_dual_prts:
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	12	assumes
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	13	"sorted_sparse_matrix A1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	14	"sorted_sparse_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	15	"sorted_sparse_matrix c1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	16	"sorted_sparse_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	17	"sorted_sparse_matrix y"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	18	"sorted_sparse_matrix r1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	19	"sorted_sparse_matrix r2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	20	"sorted_spvec b"
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	21	"le_spmat [] y"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	22	"sparse_row_matrix A1 \<le> A"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	23	"A \<le> sparse_row_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	24	"sparse_row_matrix c1 \<le> c"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	25	"c \<le> sparse_row_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	26	"sparse_row_matrix r1 \<le> x"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	27	"x \<le> sparse_row_matrix r2"
35028 108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS haftmann parents: 32491 diff changeset	28	"A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	29	shows
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	30	"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	31	(let s1 = diff_spmat c1 (mult_spmat y A2); s2 = diff_spmat c2 (mult_spmat y A1) in
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	32	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: 29804 diff changeset	33	(add_spmat (mult_spmat (nprt_spmat s2) (pprt_spmat r1)) (mult_spmat (nprt_spmat s1) (nprt_spmat r1))))))"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	34	apply (simp add: Let_def)
28637 7aabaf1ba263 reactivated HOL-Matrix; wenzelm parents: 27484 diff changeset	35	apply (insert assms)
29667 53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps; nipkow parents: 28637 diff changeset	36	apply (simp add: sparse_row_matrix_op_simps algebra_simps)
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps; nipkow parents: 28637 diff changeset	37	apply (rule mult_le_dual_prts[where A=A, simplified Let_def algebra_simps])
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	38	apply (auto)
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	39	done
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	40
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	41	lemma spm_mult_le_dual_prts_no_let:
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	42	assumes
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	43	"sorted_sparse_matrix A1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	44	"sorted_sparse_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	45	"sorted_sparse_matrix c1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	46	"sorted_sparse_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	47	"sorted_sparse_matrix y"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	48	"sorted_sparse_matrix r1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	49	"sorted_sparse_matrix r2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	50	"sorted_spvec b"
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	51	"le_spmat [] y"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	52	"sparse_row_matrix A1 \<le> A"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	53	"A \<le> sparse_row_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	54	"sparse_row_matrix c1 \<le> c"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	55	"c \<le> sparse_row_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	56	"sparse_row_matrix r1 \<le> x"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	57	"x \<le> sparse_row_matrix r2"
35028 108662d50512 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS haftmann parents: 32491 diff changeset	58	"A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	59	shows
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	60	"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	61	(mult_est_spmat r1 r2 (diff_spmat c1 (mult_spmat y A2)) (diff_spmat c2 (mult_spmat y A1))))"
28637 7aabaf1ba263 reactivated HOL-Matrix; wenzelm parents: 27484 diff changeset	62	by (simp add: assms mult_est_spmat_def spm_mult_le_dual_prts[where A=A, simplified Let_def])
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	63
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	64	use "matrixlp.ML"
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	65
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	66	end

author	huffman
	Tue, 27 Dec 2011 12:49:03 +0100
changeset 45999	cce7e6197a46
parent 41959	b460124855b8
child 46543	c7c289ce9ad2
permissions	-rw-r--r--