tuned header;
authorwenzelm
Thu Nov 05 17:58:58 2009 +0100 (2009-11-05)
changeset 33443b9bbd0f3dcdb
parent 33442 5d78b2bd27de
child 33452 c7175a18c090
tuned header;
use plain simultaneous lemma statements -- Pure's &&& should hardly ever occur in user space;
src/HOL/Library/positivstellensatz.ML
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Nov 05 17:02:43 2009 +0100
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Nov 05 17:58:58 2009 +0100
     1.3 @@ -1,7 +1,9 @@
     1.4 -(* Title:      Library/Sum_Of_Squares/positivstellensatz
     1.5 -   Author:     Amine Chaieb, University of Cambridge
     1.6 -   Description: A generic arithmetic prover based on Positivstellensatz certificates --- 
     1.7 -    also implements Fourrier-Motzkin elimination as a special case Fourrier-Motzkin elimination.
     1.8 +(*  Title:      HOL/Library/positivstellensatz.ML
     1.9 +    Author:     Amine Chaieb, University of Cambridge
    1.10 +
    1.11 +A generic arithmetic prover based on Positivstellensatz certificates
    1.12 +--- also implements Fourrier-Motzkin elimination as a special case
    1.13 +Fourrier-Motzkin elimination.
    1.14  *)
    1.15  
    1.16  (* A functor for finite mappings based on Tables *)
    1.17 @@ -187,87 +189,90 @@
    1.18    if exists (curry op aconv (concl_of tha)) (#hyps (rep_thm thb)) 
    1.19    then equal_elim (symmetric (deduct_antisym_rule tha thb)) tha else thb;
    1.20  
    1.21 -fun conjunctions th = case try Conjunction.elim th of
    1.22 -   SOME (th1,th2) => (conjunctions th1) @ conjunctions th2
    1.23 - | NONE => [th];
    1.24 -
    1.25 -val pth = @{lemma "(((x::real) < y) == (y - x > 0)) &&& ((x <= y) == (y - x >= 0)) 
    1.26 -     &&& ((x = y) == (x - y = 0)) &&& ((~(x < y)) == (x - y >= 0)) &&& ((~(x <= y)) == (x - y > 0))
    1.27 -     &&& ((~(x = y)) == (x - y > 0 | -(x - y) > 0))"
    1.28 -  by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)} |> 
    1.29 -conjunctions;
    1.30 +val pth = @{lemma "(((x::real) < y) == (y - x > 0))" and "((x <= y) == (y - x >= 0))" and
    1.31 +     "((x = y) == (x - y = 0))" and "((~(x < y)) == (x - y >= 0))" and
    1.32 +     "((~(x <= y)) == (x - y > 0))" and "((~(x = y)) == (x - y > 0 | -(x - y) > 0))"
    1.33 +  by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)};
    1.34  
    1.35  val pth_final = @{lemma "(~p ==> False) ==> p" by blast}
    1.36  val pth_add = 
    1.37 - @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 ) &&& ( x = 0 ==> y >= 0 ==> x + y >= 0) 
    1.38 -    &&& (x = 0 ==> y > 0 ==> x + y > 0) &&& (x >= 0 ==> y = 0 ==> x + y >= 0) 
    1.39 -    &&& (x >= 0 ==> y >= 0 ==> x + y >= 0) &&& (x >= 0 ==> y > 0 ==> x + y > 0) 
    1.40 -    &&& (x > 0 ==> y = 0 ==> x + y > 0) &&& (x > 0 ==> y >= 0 ==> x + y > 0) 
    1.41 -    &&& (x > 0 ==> y > 0 ==> x + y > 0)"  by simp_all} |> conjunctions ;
    1.42 +  @{lemma "(x = (0::real) ==> y = 0 ==> x + y = 0 )" and "( x = 0 ==> y >= 0 ==> x + y >= 0)" and
    1.43 +    "(x = 0 ==> y > 0 ==> x + y > 0)" and "(x >= 0 ==> y = 0 ==> x + y >= 0)" and
    1.44 +    "(x >= 0 ==> y >= 0 ==> x + y >= 0)" and "(x >= 0 ==> y > 0 ==> x + y > 0)" and
    1.45 +    "(x > 0 ==> y = 0 ==> x + y > 0)" and "(x > 0 ==> y >= 0 ==> x + y > 0)" and
    1.46 +    "(x > 0 ==> y > 0 ==> x + y > 0)" by simp_all};
    1.47  
    1.48  val pth_mul = 
    1.49 -  @{lemma "(x = (0::real) ==> y = 0 ==> x * y = 0) &&& (x = 0 ==> y >= 0 ==> x * y = 0) &&& 
    1.50 -           (x = 0 ==> y > 0 ==> x * y = 0) &&& (x >= 0 ==> y = 0 ==> x * y = 0) &&& 
    1.51 -           (x >= 0 ==> y >= 0 ==> x * y >= 0 ) &&& ( x >= 0 ==> y > 0 ==> x * y >= 0 ) &&&
    1.52 -           (x > 0 ==>  y = 0 ==> x * y = 0 ) &&& ( x > 0 ==> y >= 0 ==> x * y >= 0 ) &&&
    1.53 -           (x > 0 ==>  y > 0 ==> x * y > 0)"
    1.54 +  @{lemma "(x = (0::real) ==> y = 0 ==> x * y = 0)" and "(x = 0 ==> y >= 0 ==> x * y = 0)" and
    1.55 +    "(x = 0 ==> y > 0 ==> x * y = 0)" and "(x >= 0 ==> y = 0 ==> x * y = 0)" and
    1.56 +    "(x >= 0 ==> y >= 0 ==> x * y >= 0)" and "(x >= 0 ==> y > 0 ==> x * y >= 0)" and
    1.57 +    "(x > 0 ==>  y = 0 ==> x * y = 0)" and "(x > 0 ==> y >= 0 ==> x * y >= 0)" and
    1.58 +    "(x > 0 ==>  y > 0 ==> x * y > 0)"
    1.59    by (auto intro: mult_mono[where a="0::real" and b="x" and d="y" and c="0", simplified]
    1.60 -    mult_strict_mono[where b="x" and d="y" and a="0" and c="0", simplified])} |> conjunctions;
    1.61 +    mult_strict_mono[where b="x" and d="y" and a="0" and c="0", simplified])};
    1.62  
    1.63  val pth_emul = @{lemma "y = (0::real) ==> x * y = 0"  by simp};
    1.64  val pth_square = @{lemma "x * x >= (0::real)"  by simp};
    1.65  
    1.66 -val weak_dnf_simps = List.take (simp_thms, 34) 
    1.67 -    @ conjunctions @{lemma "((P & (Q | R)) = ((P&Q) | (P&R))) &&& ((Q | R) & P) = ((Q&P) | (R&P)) &&& (P & Q) = (Q & P) &&& ((P | Q) = (Q | P))" by blast+};
    1.68 +val weak_dnf_simps =
    1.69 +  List.take (simp_thms, 34) @
    1.70 +    @{lemma "((P & (Q | R)) = ((P&Q) | (P&R)))" and "((Q | R) & P) = ((Q&P) | (R&P))" and
    1.71 +      "(P & Q) = (Q & P)" and "((P | Q) = (Q | P))" by blast+};
    1.72  
    1.73 -val nnfD_simps = conjunctions @{lemma "((~(P & Q)) = (~P | ~Q)) &&& ((~(P | Q)) = (~P & ~Q) ) &&& ((P --> Q) = (~P | Q) ) &&& ((P = Q) = ((P & Q) | (~P & ~ Q))) &&& ((~(P = Q)) = ((P & ~ Q) | (~P & Q)) ) &&& ((~ ~(P)) = P)" by blast+}
    1.74 +val nnfD_simps =
    1.75 +  @{lemma "((~(P & Q)) = (~P | ~Q))" and "((~(P | Q)) = (~P & ~Q) )" and
    1.76 +    "((P --> Q) = (~P | Q) )" and "((P = Q) = ((P & Q) | (~P & ~ Q)))" and
    1.77 +    "((~(P = Q)) = ((P & ~ Q) | (~P & Q)) )" and "((~ ~(P)) = P)" by blast+};
    1.78  
    1.79  val choice_iff = @{lemma "(ALL x. EX y. P x y) = (EX f. ALL x. P x (f x))" by metis};
    1.80 -val prenex_simps = map (fn th => th RS sym) ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @ @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
    1.81 +val prenex_simps =
    1.82 +  map (fn th => th RS sym)
    1.83 +    ([@{thm "all_conj_distrib"}, @{thm "ex_disj_distrib"}] @
    1.84 +      @{thms "all_simps"(1-4)} @ @{thms "ex_simps"(1-4)});
    1.85  
    1.86 -val real_abs_thms1 = conjunctions @{lemma
    1.87 -  "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r)) &&&
    1.88 -  ((-1 * abs(x) + a >= r) = (a + -1 * x >= r & a + 1 * x >= r)) &&&
    1.89 -  ((a + -1 * abs(x) >= r) = (a + -1 * x >= r & a + 1 * x >= r)) &&&
    1.90 -  ((a + -1 * abs(x) + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r)) &&&
    1.91 -  ((a + b + -1 * abs(x) >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r)) &&&
    1.92 -  ((a + b + -1 * abs(x) + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r)) &&&
    1.93 -  ((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r)) &&&
    1.94 -  ((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r)) &&&
    1.95 -  ((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r)) &&&
    1.96 -  ((a + -1 * max x y + b >= r) = (a + -1 * x + b >= r & a + -1 * y  + b >= r)) &&&
    1.97 -  ((a + b + -1 * max x y >= r) = (a + b + -1 * x >= r & a + b + -1 * y >= r)) &&&
    1.98 -  ((a + b + -1 * max x y + c >= r) = (a + b + -1 * x + c >= r & a + b + -1 * y  + c >= r)) &&&
    1.99 -  ((1 * min x y >= r) = (1 * x >= r & 1 * y >= r)) &&&
   1.100 -  ((1 * min x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&&
   1.101 -  ((a + 1 * min x y >= r) = (a + 1 * x >= r & a + 1 * y >= r)) &&&
   1.102 -  ((a + 1 * min x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y  + b >= r) )&&&
   1.103 -  ((a + b + 1 * min x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r)) &&&
   1.104 -  ((a + b + 1 * min x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y  + c >= r)) &&&
   1.105 -  ((min x y >= r) = (x >= r &  y >= r)) &&&
   1.106 -  ((min x y + a >= r) = (a + x >= r & a + y >= r)) &&&
   1.107 -  ((a + min x y >= r) = (a + x >= r & a + y >= r)) &&&
   1.108 -  ((a + min x y + b >= r) = (a + x + b >= r & a + y  + b >= r)) &&&
   1.109 -  ((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r) )&&&
   1.110 -  ((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r)) &&&
   1.111 -  ((-1 * abs(x) > r) = (-1 * x > r & 1 * x > r)) &&&
   1.112 -  ((-1 * abs(x) + a > r) = (a + -1 * x > r & a + 1 * x > r)) &&&
   1.113 -  ((a + -1 * abs(x) > r) = (a + -1 * x > r & a + 1 * x > r)) &&&
   1.114 -  ((a + -1 * abs(x) + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r)) &&&
   1.115 -  ((a + b + -1 * abs(x) > r) = (a + b + -1 * x > r & a + b + 1 * x > r)) &&&
   1.116 -  ((a + b + -1 * abs(x) + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r)) &&&
   1.117 -  ((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r)) &&&
   1.118 -  ((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r)) &&&
   1.119 -  ((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r)) &&&
   1.120 -  ((a + -1 * max x y + b > r) = (a + -1 * x + b > r & a + -1 * y  + b > r)) &&&
   1.121 -  ((a + b + -1 * max x y > r) = (a + b + -1 * x > r & a + b + -1 * y > r)) &&&
   1.122 -  ((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r & a + b + -1 * y  + c > r)) &&&
   1.123 -  ((min x y > r) = (x > r &  y > r)) &&&
   1.124 -  ((min x y + a > r) = (a + x > r & a + y > r)) &&&
   1.125 -  ((a + min x y > r) = (a + x > r & a + y > r)) &&&
   1.126 -  ((a + min x y + b > r) = (a + x + b > r & a + y  + b > r)) &&&
   1.127 -  ((a + b + min x y > r) = (a + b + x > r & a + b + y > r)) &&&
   1.128 -  ((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
   1.129 +val real_abs_thms1 = @{lemma
   1.130 +  "((-1 * abs(x::real) >= r) = (-1 * x >= r & 1 * x >= r))" and
   1.131 +  "((-1 * abs(x) + a >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
   1.132 +  "((a + -1 * abs(x) >= r) = (a + -1 * x >= r & a + 1 * x >= r))" and
   1.133 +  "((a + -1 * abs(x) + b >= r) = (a + -1 * x + b >= r & a + 1 * x + b >= r))" and
   1.134 +  "((a + b + -1 * abs(x) >= r) = (a + b + -1 * x >= r & a + b + 1 * x >= r))" and
   1.135 +  "((a + b + -1 * abs(x) + c >= r) = (a + b + -1 * x + c >= r & a + b + 1 * x + c >= r))" and
   1.136 +  "((-1 * max x y >= r) = (-1 * x >= r & -1 * y >= r))" and
   1.137 +  "((-1 * max x y + a >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
   1.138 +  "((a + -1 * max x y >= r) = (a + -1 * x >= r & a + -1 * y >= r))" and
   1.139 +  "((a + -1 * max x y + b >= r) = (a + -1 * x + b >= r & a + -1 * y  + b >= r))" and
   1.140 +  "((a + b + -1 * max x y >= r) = (a + b + -1 * x >= r & a + b + -1 * y >= r))" and
   1.141 +  "((a + b + -1 * max x y + c >= r) = (a + b + -1 * x + c >= r & a + b + -1 * y  + c >= r))" and
   1.142 +  "((1 * min x y >= r) = (1 * x >= r & 1 * y >= r))" and
   1.143 +  "((1 * min x y + a >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and
   1.144 +  "((a + 1 * min x y >= r) = (a + 1 * x >= r & a + 1 * y >= r))" and
   1.145 +  "((a + 1 * min x y + b >= r) = (a + 1 * x + b >= r & a + 1 * y  + b >= r))" and
   1.146 +  "((a + b + 1 * min x y >= r) = (a + b + 1 * x >= r & a + b + 1 * y >= r))" and
   1.147 +  "((a + b + 1 * min x y + c >= r) = (a + b + 1 * x + c >= r & a + b + 1 * y  + c >= r))" and
   1.148 +  "((min x y >= r) = (x >= r &  y >= r))" and
   1.149 +  "((min x y + a >= r) = (a + x >= r & a + y >= r))" and
   1.150 +  "((a + min x y >= r) = (a + x >= r & a + y >= r))" and
   1.151 +  "((a + min x y + b >= r) = (a + x + b >= r & a + y  + b >= r))" and
   1.152 +  "((a + b + min x y >= r) = (a + b + x >= r & a + b + y >= r))" and
   1.153 +  "((a + b + min x y + c >= r) = (a + b + x + c >= r & a + b + y + c >= r))" and
   1.154 +  "((-1 * abs(x) > r) = (-1 * x > r & 1 * x > r))" and
   1.155 +  "((-1 * abs(x) + a > r) = (a + -1 * x > r & a + 1 * x > r))" and
   1.156 +  "((a + -1 * abs(x) > r) = (a + -1 * x > r & a + 1 * x > r))" and
   1.157 +  "((a + -1 * abs(x) + b > r) = (a + -1 * x + b > r & a + 1 * x + b > r))" and
   1.158 +  "((a + b + -1 * abs(x) > r) = (a + b + -1 * x > r & a + b + 1 * x > r))" and
   1.159 +  "((a + b + -1 * abs(x) + c > r) = (a + b + -1 * x + c > r & a + b + 1 * x + c > r))" and
   1.160 +  "((-1 * max x y > r) = ((-1 * x > r) & -1 * y > r))" and
   1.161 +  "((-1 * max x y + a > r) = (a + -1 * x > r & a + -1 * y > r))" and
   1.162 +  "((a + -1 * max x y > r) = (a + -1 * x > r & a + -1 * y > r))" and
   1.163 +  "((a + -1 * max x y + b > r) = (a + -1 * x + b > r & a + -1 * y  + b > r))" and
   1.164 +  "((a + b + -1 * max x y > r) = (a + b + -1 * x > r & a + b + -1 * y > r))" and
   1.165 +  "((a + b + -1 * max x y + c > r) = (a + b + -1 * x + c > r & a + b + -1 * y  + c > r))" and
   1.166 +  "((min x y > r) = (x > r &  y > r))" and
   1.167 +  "((min x y + a > r) = (a + x > r & a + y > r))" and
   1.168 +  "((a + min x y > r) = (a + x > r & a + y > r))" and
   1.169 +  "((a + min x y + b > r) = (a + x + b > r & a + y  + b > r))" and
   1.170 +  "((a + b + min x y > r) = (a + b + x > r & a + b + y > r))" and
   1.171 +  "((a + b + min x y + c > r) = (a + b + x + c > r & a + b + y + c > r))"
   1.172    by auto};
   1.173  
   1.174  val abs_split' = @{lemma "P (abs (x::'a::ordered_idom)) == (x >= 0 & P x | x < 0 & P (-x))"