diff -r 0ec94bb9cec4 -r 1393c2340eec src/HOL/Library/positivstellensatz.ML --- a/src/HOL/Library/positivstellensatz.ML Sun Nov 26 13:19:52 2017 +0100 +++ b/src/HOL/Library/positivstellensatz.ML Sun Nov 26 21:08:32 2017 +0100 @@ -177,12 +177,12 @@ if exists (curry op aconv (Thm.concl_of tha)) (Thm.hyps_of thb) (* FIXME !? *) then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb; -val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and - "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and - "((~(x <= y)) == (x - y > 0))" and "((~(x = y)) == (x - y > 0 | -(x - y) > 0))" +val pth = @{lemma "(((x::real) < y) \ (y - x > 0))" and "((x \ y) \ (y - x \ 0))" and + "((x = y) \ (x - y = 0))" and "((\(x < y)) \ (x - y \ 0))" and + "((\(x \ y)) \ (x - y > 0))" and "((\(x = y)) \ (x - y > 0 \ -(x - y) > 0))" by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)}; -val pth_final = @{lemma "(~p ==> False) ==> p" by blast} +val pth_final = @{lemma "(\p \ False) \ p" by blast} val pth_add = @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 )" and "( x = 0 ==> y >= 0 ==> x + y >= 0)" and "(x = 0 ==> y > 0 ==> x + y > 0)" and "(x >= 0 ==> y = 0 ==> x + y >= 0)" and @@ -204,8 +204,8 @@ val weak_dnf_simps = List.take (@{thms simp_thms}, 34) @ - @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and - "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+}; + @{lemma "((P \ (Q \ R)) = ((P\Q) \ (P\R)))" and "((Q \ R) \ P) = ((Q\P) \ (R\P))" and + "(P \ Q) = (Q \ P)" and "((P \ Q) = (Q \ P))" by blast+}; (* val nnfD_simps = @@ -214,65 +214,65 @@ "((~(P = Q)) = ((P & ~ Q) | (~P & Q)) )" and "((~ ~(P)) = P)" by blast+}; *) -val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis}; +val choice_iff = @{lemma "(\x. \y. P x y) = (\f. \x. P x (f x))" by metis}; val prenex_simps = map (fn th => th RS sym) ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @ @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)}); val real_abs_thms1 = @{lemma - "((-1 * \x::real\ >= r) = (-1 * x >= r & 1 * x >= r))" and - "((-1 * \x\ + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and - "((a + -1 * \x\ >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and - "((a + -1 * \x\ + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and - "((a + b + -1 * \x\ >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and - "((a + b + -1 * \x\ + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and - "((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r))" and - "((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and - "((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and - "((a + -1 * max x y + b >= r) = (a + -1 * x + b >= r & a + -1 * y + b >= r))" and - "((a + b + -1 * max x y >= r) = (a + b + -1 * x >= r & a + b + -1 * y >= r))" and - "((a + b + -1 * max x y + c >= r) = (a + b + -1 * x + c >= r & a + b + -1 * y + c >= r))" and - "((1 * min x y >= r) = (1 * x >= r & 1 * y >= r))" and - "((1 * min x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and - "((a + 1 * min x y >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and - "((a + 1 * min x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y + b >= r))" and - "((a + b + 1 * min x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r))" and - "((a + b + 1 * min x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y + c >= r))" and - "((min x y >= r) = (x >= r & y >= r))" and - "((min x y + a >= r) = (a + x >= r & a + y >= r))" and - "((a + min x y >= r) = (a + x >= r & a + y >= r))" and - "((a + min x y + b >= r) = (a + x + b >= r & a + y + b >= r))" and - "((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r))" and - "((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r))" and - "((-1 * \x\ > r) = (-1 * x > r & 1 * x > r))" and - "((-1 * \x\ + a > r) = (a + -1 * x > r & a + 1 * x > r))" and - "((a + -1 * \x\ > r) = (a + -1 * x > r & a + 1 * x > r))" and - "((a + -1 * \x\ + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and - "((a + b + -1 * \x\ > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and - "((a + b + -1 * \x\ + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and - "((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r))" and - "((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r))" and - "((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r))" and - "((a + -1 * max x y + b > r) = (a + -1 * x + b > r & a + -1 * y + b > r))" and - "((a + b + -1 * max x y > r) = (a + b + -1 * x > r & a + b + -1 * y > r))" and - "((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r & a + b + -1 * y + c > r))" and - "((min x y > r) = (x > r & y > r))" and - "((min x y + a > r) = (a + x > r & a + y > r))" and - "((a + min x y > r) = (a + x > r & a + y > r))" and - "((a + min x y + b > r) = (a + x + b > r & a + y + b > r))" and - "((a + b + min x y > r) = (a + b + x > r & a + b + y > r))" and - "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))" + "((-1 * \x::real\ \ r) = (-1 * x \ r \ 1 * x \ r))" and + "((-1 * \x\ + a \ r) = (a + -1 * x \ r \ a + 1 * x \ r))" and + "((a + -1 * \x\ \ r) = (a + -1 * x \ r \ a + 1 * x \ r))" and + "((a + -1 * \x\ + b \ r) = (a + -1 * x + b \ r \ a + 1 * x + b \ r))" and + "((a + b + -1 * \x\ \ r) = (a + b + -1 * x \ r \ a + b + 1 * x \ r))" and + "((a + b + -1 * \x\ + c \ r) = (a + b + -1 * x + c \ r \ a + b + 1 * x + c \ r))" and + "((-1 * max x y \ r) = (-1 * x \ r \ -1 * y \ r))" and + "((-1 * max x y + a \ r) = (a + -1 * x \ r \ a + -1 * y \ r))" and + "((a + -1 * max x y \ r) = (a + -1 * x \ r \ a + -1 * y \ r))" and + "((a + -1 * max x y + b \ r) = (a + -1 * x + b \ r \ a + -1 * y + b \ r))" and + "((a + b + -1 * max x y \ r) = (a + b + -1 * x \ r \ a + b + -1 * y \ r))" and + "((a + b + -1 * max x y + c \ r) = (a + b + -1 * x + c \ r \ a + b + -1 * y + c \ r))" and + "((1 * min x y \ r) = (1 * x \ r \ 1 * y \ r))" and + "((1 * min x y + a \ r) = (a + 1 * x \ r \ a + 1 * y \ r))" and + "((a + 1 * min x y \ r) = (a + 1 * x \ r \ a + 1 * y \ r))" and + "((a + 1 * min x y + b \ r) = (a + 1 * x + b \ r \ a + 1 * y + b \ r))" and + "((a + b + 1 * min x y \ r) = (a + b + 1 * x \ r \ a + b + 1 * y \ r))" and + "((a + b + 1 * min x y + c \ r) = (a + b + 1 * x + c \ r \ a + b + 1 * y + c \ r))" and + "((min x y \ r) = (x \ r \ y \ r))" and + "((min x y + a \ r) = (a + x \ r \ a + y \ r))" and + "((a + min x y \ r) = (a + x \ r \ a + y \ r))" and + "((a + min x y + b \ r) = (a + x + b \ r \ a + y + b \ r))" and + "((a + b + min x y \ r) = (a + b + x \ r \ a + b + y \ r))" and + "((a + b + min x y + c \ r) = (a + b + x + c \ r \ a + b + y + c \ r))" and + "((-1 * \x\ > r) = (-1 * x > r \ 1 * x > r))" and + "((-1 * \x\ + a > r) = (a + -1 * x > r \ a + 1 * x > r))" and + "((a + -1 * \x\ > r) = (a + -1 * x > r \ a + 1 * x > r))" and + "((a + -1 * \x\ + b > r) = (a + -1 * x + b > r \ a + 1 * x + b > r))" and + "((a + b + -1 * \x\ > r) = (a + b + -1 * x > r \ a + b + 1 * x > r))" and + "((a + b + -1 * \x\ + c > r) = (a + b + -1 * x + c > r \ a + b + 1 * x + c > r))" and + "((-1 * max x y > r) = ((-1 * x > r) \ -1 * y > r))" and + "((-1 * max x y + a > r) = (a + -1 * x > r \ a + -1 * y > r))" and + "((a + -1 * max x y > r) = (a + -1 * x > r \ a + -1 * y > r))" and + "((a + -1 * max x y + b > r) = (a + -1 * x + b > r \ a + -1 * y + b > r))" and + "((a + b + -1 * max x y > r) = (a + b + -1 * x > r \ a + b + -1 * y > r))" and + "((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r \ a + b + -1 * y + c > r))" and + "((min x y > r) = (x > r \ y > r))" and + "((min x y + a > r) = (a + x > r \ a + y > r))" and + "((a + min x y > r) = (a + x > r \ a + y > r))" and + "((a + min x y + b > r) = (a + x + b > r \ a + y + b > r))" and + "((a + b + min x y > r) = (a + b + x > r \ a + b + y > r))" and + "((a + b + min x y + c > r) = (a + b + x + c > r \ a + b + y + c > r))" by auto}; -val abs_split' = @{lemma "P \x::'a::linordered_idom\ == (x >= 0 & P x | x < 0 & P (-x))" +val abs_split' = @{lemma "P \x::'a::linordered_idom\ == (x \ 0 \ P x \ x < 0 \ P (-x))" by (atomize (full)) (auto split: abs_split)}; -val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)" - by (atomize (full)) (cases "x <= y", auto simp add: max_def)}; +val max_split = @{lemma "P (max x y) \ ((x::'a::linorder) \ y \ P y \ x > y \ P x)" + by (atomize (full)) (cases "x \ y", auto simp add: max_def)}; -val min_split = @{lemma "P (min x y) == ((x::'a::linorder) <= y & P x | x > y & P y)" - by (atomize (full)) (cases "x <= y", auto simp add: min_def)}; +val min_split = @{lemma "P (min x y) \ ((x::'a::linorder) \ y \ P x \ x > y \ P y)" + by (atomize (full)) (cases "x \ y", auto simp add: min_def)}; (* Miscellaneous *)