src/HOL/Library/Sum_of_Squares.thy
author wenzelm
Wed, 17 Jun 2015 11:03:05 +0200
changeset 60500 903bb1495239
parent 58881 b9556a055632
child 69605 a96320074298
permissions -rw-r--r--
isabelle update_cartouches;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
60500
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     6
section \<open>A decision procedure for universal multivariate real arithmetic
903bb1495239 isabelle update_cartouches;
wenzelm
parents: 58881
diff changeset
     7
  with addition, multiplication and ordering using semidefinite programming\<close>
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
31119
2532bb2d65c7 A decision method for universal multivariate real arithmetic with add
chaieb
parents:
diff changeset
    18
end