isabelle: src/HOL/Matrix_LP/Cplex.thy@b249fab48c76 (annotated)

47455 26315a545e26 updated headers; wenzelm parents: 46988 diff changeset	1	(* Title: HOL/Matrix_LP/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
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	7	begin
92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	8
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	9	ML_file "Cplex_tools.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	10	ML_file "CplexMatrixConverter.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	11	ML_file "FloatSparseMatrixBuilder.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	12	ML_file "fspmlp.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	13
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	14	lemma spm_mult_le_dual_prts:
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	15	assumes
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	16	"sorted_sparse_matrix A1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	17	"sorted_sparse_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	18	"sorted_sparse_matrix c1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	19	"sorted_sparse_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	20	"sorted_sparse_matrix y"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	21	"sorted_sparse_matrix r1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	22	"sorted_sparse_matrix r2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	23	"sorted_spvec b"
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	24	"le_spmat [] y"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	25	"sparse_row_matrix A1 \<le> A"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	26	"A \<le> sparse_row_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	27	"sparse_row_matrix c1 \<le> c"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	28	"c \<le> sparse_row_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	29	"sparse_row_matrix r1 \<le> x"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	30	"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	31	"A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	32	shows
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	33	"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	34	(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	35	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	36	(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	37	apply (simp add: Let_def)
28637 7aabaf1ba263 reactivated HOL-Matrix; wenzelm parents: 27484 diff changeset	38	apply (insert assms)
29667 53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps; nipkow parents: 28637 diff changeset	39	apply (simp add: sparse_row_matrix_op_simps algebra_simps)
53103fc8ffa3 Replaced group_ and ring_simps by algebra_simps; nipkow parents: 28637 diff changeset	40	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	41	apply (auto)
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	42	done
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	43
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	44	lemma spm_mult_le_dual_prts_no_let:
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	45	assumes
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	46	"sorted_sparse_matrix A1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	47	"sorted_sparse_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	48	"sorted_sparse_matrix c1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	49	"sorted_sparse_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	50	"sorted_sparse_matrix y"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	51	"sorted_sparse_matrix r1"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	52	"sorted_sparse_matrix r2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	53	"sorted_spvec b"
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	54	"le_spmat [] y"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	55	"sparse_row_matrix A1 \<le> A"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	56	"A \<le> sparse_row_matrix A2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	57	"sparse_row_matrix c1 \<le> c"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	58	"c \<le> sparse_row_matrix c2"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	59	"sparse_row_matrix r1 \<le> x"
dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	60	"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	61	"A * x \<le> sparse_row_matrix (b::('a::lattice_ring) spmat)"
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	62	shows
31816 ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	63	"c * x \<le> sparse_row_matrix (add_spmat (mult_spmat y b)
ffaf6dd53045 replaced recdefs by funs nipkow parents: 29804 diff changeset	64	(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	65	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	66
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 47455 diff changeset	67	ML_file "matrixlp.ML"
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: diff changeset	68
27484 dbb9981c3d18 added marginal setup for code generation haftmann parents: 23665 diff changeset	69	end
46543 c7c289ce9ad2 tuned whitespace haftmann parents: 41959 diff changeset	70

author	paulson <lp15@cam.ac.uk>
	Wed, 02 May 2018 12:47:56 +0100
changeset 68064	b249fab48c76
parent 48891	c0eafbd55de3
child 69605	a96320074298
permissions	-rw-r--r--