isabelle: src/HOL/Library/Sum_of_Squares.thy@19e062fbfea0 (annotated)

41474 60d091240485 renamed Sum_Of_Squares to Sum_of_Squares; wenzelm parents: 38805 diff changeset	1	(* Title: HOL/Library/Sum_of_Squares.thy
32949 aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref; wenzelm parents: 32645 diff changeset	2	Author: Amine Chaieb, University of Cambridge
aa6c470a962a eliminated slightly odd get/set operations in favour of Unsynchronized.ref; wenzelm parents: 32645 diff changeset	3	Author: Philipp Meyer, TU Muenchen
31119 2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	4	*)
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	5
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	6	header {* A decision method for universal multivariate real arithmetic with addition,
32333 d4cb904cc63c tuned header; wenzelm parents: 32332 diff changeset	7	multiplication and ordering using semidefinite programming *}
32271 378ebd64447d sos comments modified nipkow parents: 32268 diff changeset	8
41474 60d091240485 renamed Sum_Of_Squares to Sum_of_Squares; wenzelm parents: 38805 diff changeset	9	theory Sum_of_Squares
38136 bd4965bb7bdc tuned headers -- more precise load path; wenzelm parents: 33041 diff changeset	10	imports Complex_Main
32332 bc5cec7b2be6 misc changes to SOS by Philipp Meyer: wenzelm parents: 32271 diff changeset	11	begin
31119 2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	12
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	13	ML_file "positivstellensatz.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	14	ML_file "Sum_of_Squares/sum_of_squares.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	15	ML_file "Sum_of_Squares/positivstellensatz_tools.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	16	ML_file "Sum_of_Squares/sos_wrapper.ML"
c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 46593 diff changeset	17
32333 d4cb904cc63c tuned header; wenzelm parents: 32332 diff changeset	18	text {*
41950 134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	19	Proof method sos invocations:
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	20	\begin{itemize}
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	21
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	22	\item remote solver: @{text "(sos remote_csdp)"}
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	23
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	24	\item local solver: @{text "(sos csdp)"}
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	25
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	26	The latter requires a local executable from
54703 499f92dc6e45 more antiquotations; wenzelm parents: 48891 diff changeset	27	@{url "https://projects.coin-or.org/Csdp"} and the Isabelle settings variable
41950 134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	28	variable @{text ISABELLE_CSDP} pointing to it.
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	29
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	30	\end{itemize}
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	31
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	32	By default, method sos calls @{text remote_csdp}. This can take of
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	33	the order of a minute for one sos call, because sos calls CSDP
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	34	repeatedly. If you install CSDP locally, sos calls typically takes
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	35	only a few seconds.
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	36
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	37	The sos method generates a certificate which can be used to repeat
134131d519c0 clarified ISABELLE_CSDP setting (formerly CSDP_EXE); wenzelm parents: 41474 diff changeset	38	the proof without calling an external prover.
32333 d4cb904cc63c tuned header; wenzelm parents: 32332 diff changeset	39	*}
d4cb904cc63c tuned header; wenzelm parents: 32332 diff changeset	40
31119 2532bb2d65c7 A decision method for universal multivariate real arithmetic with add chaieb parents: diff changeset	41	end

author	wenzelm
	Sun, 05 Oct 2014 13:16:24 +0200
changeset 58542	19e062fbfea0
parent 58418	a04b242a7a01
child 58630	71cdb885b3bb
permissions	-rw-r--r--