src/HOL/Library/positivstellensatz.ML
changeset 67091 1393c2340eec
parent 63667 24126c564d8a
child 67232 a00f5a71e672
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -177,12 +177,12 @@
     1.4    if exists (curry op aconv (Thm.concl_of tha)) (Thm.hyps_of thb)  (* FIXME !? *)
     1.5    then Thm.equal_elim (Thm.symmetric (deduct_antisym_rule tha thb)) tha else thb;
     1.6  
     1.7 -val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
     1.8 -     "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and
     1.9 -     "((~(x <= y)) == (x - y > 0))" and "((~(x = y)) == (x - y > 0 | -(x - y) > 0))"
    1.10 +val pth = @{lemma "(((x::real) < y) \<equiv> (y - x > 0))" and "((x \<le> y) \<equiv> (y - x \<ge> 0))" and
    1.11 +     "((x = y) \<equiv> (x - y = 0))" and "((\<not>(x < y)) \<equiv> (x - y \<ge> 0))" and
    1.12 +     "((\<not>(x \<le> y)) \<equiv> (x - y > 0))" and "((\<not>(x = y)) \<equiv> (x - y > 0 \<or> -(x - y) > 0))"
    1.13    by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)};
    1.14  
    1.15 -val pth_final = @{lemma "(~p ==> False) ==> p" by blast}
    1.16 +val pth_final = @{lemma "(\<not>p \<Longrightarrow> False) \<Longrightarrow> p" by blast}
    1.17  val pth_add =
    1.18    @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 )" and "( x = 0 ==> y >= 0 ==> x + y >= 0)" and
    1.19      "(x = 0 ==> y > 0 ==> x + y > 0)" and "(x >= 0 ==> y = 0 ==> x + y >= 0)" and
    1.20 @@ -204,8 +204,8 @@
    1.21  
    1.22  val weak_dnf_simps =
    1.23    List.take (@{thms simp_thms}, 34) @
    1.24 -    @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
    1.25 -      "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
    1.26 +    @{lemma "((P \<and> (Q \<or> R)) = ((P\<and>Q) \<or> (P\<and>R)))" and "((Q \<or> R) \<and> P) = ((Q\<and>P) \<or> (R\<and>P))" and
    1.27 +      "(P \<and> Q) = (Q \<and> P)" and "((P \<or> Q) = (Q \<or> P))" by blast+};
    1.28  
    1.29  (*
    1.30  val nnfD_simps =
    1.31 @@ -214,65 +214,65 @@
    1.32      "((~(P = Q)) = ((P & ~ Q) | (~P & Q)) )" and "((~ ~(P)) = P)" by blast+};
    1.33  *)
    1.34  
    1.35 -val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis};
    1.36 +val choice_iff = @{lemma "(\<forall>x. \<exists>y. P x y) = (\<exists>f. \<forall>x. P x (f x))" by metis};
    1.37  val prenex_simps =
    1.38    map (fn th => th RS sym)
    1.39      ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @
    1.40        @{thms "HOL.all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
    1.41  
    1.42  val real_abs_thms1 = @{lemma
    1.43 -  "((-1 * \<bar>x::real\<bar> >= r) = (-1 * x >= r & 1 * x >= r))" and
    1.44 -  "((-1 * \<bar>x\<bar> + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
    1.45 -  "((a + -1 * \<bar>x\<bar> >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
    1.46 -  "((a + -1 * \<bar>x\<bar> + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
    1.47 -  "((a + b + -1 * \<bar>x\<bar> >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
    1.48 -  "((a + b + -1 * \<bar>x\<bar> + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
    1.49 -  "((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r))" and
    1.50 -  "((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
    1.51 -  "((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
    1.52 -  "((a + -1 * max x y + b >= r) = (a + -1 * x + b >= r & a + -1 * y  + b >= r))" and
    1.53 -  "((a + b + -1 * max x y >= r) = (a + b + -1 * x >= r & a + b + -1 * y >= r))" and
    1.54 -  "((a + b + -1 * max x y + c >= r) = (a + b + -1 * x + c >= r & a + b + -1 * y  + c >= r))" and
    1.55 -  "((1 * min x y >= r) = (1 * x >= r & 1 * y >= r))" and
    1.56 -  "((1 * min x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and
    1.57 -  "((a + 1 * min x y >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and
    1.58 -  "((a + 1 * min x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y  + b >= r))" and
    1.59 -  "((a + b + 1 * min x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r))" and
    1.60 -  "((a + b + 1 * min x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y  + c >= r))" and
    1.61 -  "((min x y >= r) = (x >= r &  y >= r))" and
    1.62 -  "((min x y + a >= r) = (a + x >= r & a + y >= r))" and
    1.63 -  "((a + min x y >= r) = (a + x >= r & a + y >= r))" and
    1.64 -  "((a + min x y + b >= r) = (a + x + b >= r & a + y  + b >= r))" and
    1.65 -  "((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r))" and
    1.66 -  "((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r))" and
    1.67 -  "((-1 * \<bar>x\<bar> > r) = (-1 * x > r & 1 * x > r))" and
    1.68 -  "((-1 * \<bar>x\<bar> + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
    1.69 -  "((a + -1 * \<bar>x\<bar> > r) = (a + -1 * x > r & a + 1 * x > r))" and
    1.70 -  "((a + -1 * \<bar>x\<bar> + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
    1.71 -  "((a + b + -1 * \<bar>x\<bar> > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
    1.72 -  "((a + b + -1 * \<bar>x\<bar> + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
    1.73 -  "((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r))" and
    1.74 -  "((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r))" and
    1.75 -  "((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r))" and
    1.76 -  "((a + -1 * max x y + b > r) = (a + -1 * x + b > r & a + -1 * y  + b > r))" and
    1.77 -  "((a + b + -1 * max x y > r) = (a + b + -1 * x > r & a + b + -1 * y > r))" and
    1.78 -  "((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r & a + b + -1 * y  + c > r))" and
    1.79 -  "((min x y > r) = (x > r &  y > r))" and
    1.80 -  "((min x y + a > r) = (a + x > r & a + y > r))" and
    1.81 -  "((a + min x y > r) = (a + x > r & a + y > r))" and
    1.82 -  "((a + min x y + b > r) = (a + x + b > r & a + y  + b > r))" and
    1.83 -  "((a + b + min x y > r) = (a + b + x > r & a + b + y > r))" and
    1.84 -  "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
    1.85 +  "((-1 * \<bar>x::real\<bar> \<ge> r) = (-1 * x \<ge> r \<and> 1 * x \<ge> r))" and
    1.86 +  "((-1 * \<bar>x\<bar> + a \<ge> r) = (a + -1 * x \<ge> r \<and> a + 1 * x \<ge> r))" and
    1.87 +  "((a + -1 * \<bar>x\<bar> \<ge> r) = (a + -1 * x \<ge> r \<and> a + 1 * x \<ge> r))" and
    1.88 +  "((a + -1 * \<bar>x\<bar> + b \<ge> r) = (a + -1 * x + b \<ge> r \<and> a + 1 * x + b \<ge> r))" and
    1.89 +  "((a + b + -1 * \<bar>x\<bar> \<ge> r) = (a + b + -1 * x \<ge> r \<and> a + b + 1 * x \<ge> r))" and
    1.90 +  "((a + b + -1 * \<bar>x\<bar> + c \<ge> r) = (a + b + -1 * x + c \<ge> r \<and> a + b + 1 * x + c \<ge> r))" and
    1.91 +  "((-1 * max x y \<ge> r) = (-1 * x \<ge> r \<and> -1 * y \<ge> r))" and
    1.92 +  "((-1 * max x y + a \<ge> r) = (a + -1 * x \<ge> r \<and> a + -1 * y \<ge> r))" and
    1.93 +  "((a + -1 * max x y \<ge> r) = (a + -1 * x \<ge> r \<and> a + -1 * y \<ge> r))" and
    1.94 +  "((a + -1 * max x y + b \<ge> r) = (a + -1 * x + b \<ge> r \<and> a + -1 * y  + b \<ge> r))" and
    1.95 +  "((a + b + -1 * max x y \<ge> r) = (a + b + -1 * x \<ge> r \<and> a + b + -1 * y \<ge> r))" and
    1.96 +  "((a + b + -1 * max x y + c \<ge> r) = (a + b + -1 * x + c \<ge> r \<and> a + b + -1 * y  + c \<ge> r))" and
    1.97 +  "((1 * min x y \<ge> r) = (1 * x \<ge> r \<and> 1 * y \<ge> r))" and
    1.98 +  "((1 * min x y + a \<ge> r) = (a + 1 * x \<ge> r \<and> a + 1 * y \<ge> r))" and
    1.99 +  "((a + 1 * min x y \<ge> r) = (a + 1 * x \<ge> r \<and> a + 1 * y \<ge> r))" and
   1.100 +  "((a + 1 * min x y + b \<ge> r) = (a + 1 * x + b \<ge> r \<and> a + 1 * y  + b \<ge> r))" and
   1.101 +  "((a + b + 1 * min x y \<ge> r) = (a + b + 1 * x \<ge> r \<and> a + b + 1 * y \<ge> r))" and
   1.102 +  "((a + b + 1 * min x y + c \<ge> r) = (a + b + 1 * x + c \<ge> r \<and> a + b + 1 * y  + c \<ge> r))" and
   1.103 +  "((min x y \<ge> r) = (x \<ge> r \<and> y \<ge> r))" and
   1.104 +  "((min x y + a \<ge> r) = (a + x \<ge> r \<and> a + y \<ge> r))" and
   1.105 +  "((a + min x y \<ge> r) = (a + x \<ge> r \<and> a + y \<ge> r))" and
   1.106 +  "((a + min x y + b \<ge> r) = (a + x + b \<ge> r \<and> a + y  + b \<ge> r))" and
   1.107 +  "((a + b + min x y \<ge> r) = (a + b + x \<ge> r \<and> a + b + y \<ge> r))" and
   1.108 +  "((a + b + min x y + c \<ge> r) = (a + b + x + c \<ge> r \<and> a + b + y + c \<ge> r))" and
   1.109 +  "((-1 * \<bar>x\<bar> > r) = (-1 * x > r \<and> 1 * x > r))" and
   1.110 +  "((-1 * \<bar>x\<bar> + a > r) = (a + -1 * x > r \<and> a + 1 * x > r))" and
   1.111 +  "((a + -1 * \<bar>x\<bar> > r) = (a + -1 * x > r \<and> a + 1 * x > r))" and
   1.112 +  "((a + -1 * \<bar>x\<bar> + b > r) = (a + -1 * x + b > r \<and> a + 1 * x + b > r))" and
   1.113 +  "((a + b + -1 * \<bar>x\<bar> > r) = (a + b + -1 * x > r \<and> a + b + 1 * x > r))" and
   1.114 +  "((a + b + -1 * \<bar>x\<bar> + c > r) = (a + b + -1 * x + c > r \<and> a + b + 1 * x + c > r))" and
   1.115 +  "((-1 * max x y > r) = ((-1 * x > r) \<and> -1 * y > r))" and
   1.116 +  "((-1 * max x y + a > r) = (a + -1 * x > r \<and> a + -1 * y > r))" and
   1.117 +  "((a + -1 * max x y > r) = (a + -1 * x > r \<and> a + -1 * y > r))" and
   1.118 +  "((a + -1 * max x y + b > r) = (a + -1 * x + b > r \<and> a + -1 * y  + b > r))" and
   1.119 +  "((a + b + -1 * max x y > r) = (a + b + -1 * x > r \<and> a + b + -1 * y > r))" and
   1.120 +  "((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r \<and> a + b + -1 * y  + c > r))" and
   1.121 +  "((min x y > r) = (x > r \<and> y > r))" and
   1.122 +  "((min x y + a > r) = (a + x > r \<and> a + y > r))" and
   1.123 +  "((a + min x y > r) = (a + x > r \<and> a + y > r))" and
   1.124 +  "((a + min x y + b > r) = (a + x + b > r \<and> a + y  + b > r))" and
   1.125 +  "((a + b + min x y > r) = (a + b + x > r \<and> a + b + y > r))" and
   1.126 +  "((a + b + min x y + c > r) = (a + b + x + c > r \<and> a + b + y + c > r))"
   1.127    by auto};
   1.128  
   1.129 -val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x >= 0 & P x | x < 0 & P (-x))"
   1.130 +val abs_split' = @{lemma "P \<bar>x::'a::linordered_idom\<bar> == (x \<ge> 0 \<and> P x \<or> x < 0 \<and> P (-x))"
   1.131    by (atomize (full)) (auto split: abs_split)};
   1.132  
   1.133 -val max_split = @{lemma "P (max x y) == ((x::'a::linorder) <= y & P y | x > y & P x)"
   1.134 -  by (atomize (full)) (cases "x <= y", auto simp add: max_def)};
   1.135 +val max_split = @{lemma "P (max x y) \<equiv> ((x::'a::linorder) \<le> y \<and> P y \<or> x > y \<and> P x)"
   1.136 +  by (atomize (full)) (cases "x \<le> y", auto simp add: max_def)};
   1.137  
   1.138 -val min_split = @{lemma "P (min x y) == ((x::'a::linorder) <= y & P x | x > y & P y)"
   1.139 -  by (atomize (full)) (cases "x <= y", auto simp add: min_def)};
   1.140 +val min_split = @{lemma "P (min x y) \<equiv> ((x::'a::linorder) \<le> y \<and> P x \<or> x > y \<and> P y)"
   1.141 +  by (atomize (full)) (cases "x \<le> y", auto simp add: min_def)};
   1.142  
   1.143  
   1.144           (* Miscellaneous *)