src/HOL/Library/positivstellensatz.ML
changeset 61945 1135b8de26c3
parent 61609 77b453bd616f
child 62177 3a578ee55bff
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Dec 28 01:26:34 2015 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Dec 28 01:28:28 2015 +0100
     1.3 @@ -221,12 +221,12 @@
     1.4        @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
     1.5  
     1.6  val real_abs_thms1 = @{lemma
     1.7 -  "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
     1.8 -  "((-1 * abs(x) + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
     1.9 -  "((a + -1 * abs(x) >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
    1.10 -  "((a + -1 * abs(x) + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
    1.11 -  "((a + b + -1 * abs(x) >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
    1.12 -  "((a + b + -1 * abs(x) + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
    1.13 +  "((-1 * \<bar>x::real\<bar> >= r) = (-1 * x >= r & 1 * x >= r))" and
    1.14 +  "((-1 * \<bar>x\<bar> + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
    1.15 +  "((a + -1 * \<bar>x\<bar> >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
    1.16 +  "((a + -1 * \<bar>x\<bar> + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
    1.17 +  "((a + b + -1 * \<bar>x\<bar> >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
    1.18 +  "((a + b + -1 * \<bar>x\<bar> + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
    1.19    "((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r))" and
    1.20    "((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
    1.21    "((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
    1.22 @@ -245,12 +245,12 @@
    1.23    "((a + min x y + b >= r) = (a + x + b >= r & a + y  + b >= r))" and
    1.24    "((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r))" and
    1.25    "((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r))" and
    1.26 -  "((-1 * abs(x) > r) = (-1 * x > r & 1 * x > r))" and
    1.27 -  "((-1 * abs(x) + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
    1.28 -  "((a + -1 * abs(x) > r) = (a + -1 * x > r & a + 1 * x > r))" and
    1.29 -  "((a + -1 * abs(x) + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
    1.30 -  "((a + b + -1 * abs(x) > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
    1.31 -  "((a + b + -1 * abs(x) + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
    1.32 +  "((-1 * \<bar>x\<bar> > r) = (-1 * x > r & 1 * x > r))" and
    1.33 +  "((-1 * \<bar>x\<bar> + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
    1.34 +  "((a + -1 * \<bar>x\<bar> > r) = (a + -1 * x > r & a + 1 * x > r))" and
    1.35 +  "((a + -1 * \<bar>x\<bar> + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
    1.36 +  "((a + b + -1 * \<bar>x\<bar> > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
    1.37 +  "((a + b + -1 * \<bar>x\<bar> + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
    1.38    "((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r))" and
    1.39    "((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r))" and
    1.40    "((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r))" and
    1.41 @@ -265,7 +265,7 @@
    1.42    "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
    1.43    by auto};
    1.44  
    1.45 -val abs_split' = @{lemma "P (abs (x::'a::linordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"
    1.46 +val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
    1.47    by (atomize (full)) (auto split add: abs_split)};
    1.48  
    1.49  val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"