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)"
```