src/HOL/ex/svc_test.ML
author obua
Mon Apr 10 16:00:34 2006 +0200 (2006-04-10)
changeset 19404 9bf2cdc9e8e8
parent 15661 9ef583b08647
permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     1 (*  Title:      HOL/ex/svc_test.ML
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson
     4     Copyright   1999  University of Cambridge
     5 
     6 Demonstrating svc_tac: the interface to the Stanford Validity Checker
     7 
     8 SVC is assumed to be present if the environment variable SVC_HOME is non-empty.
     9 
    10 set Svc.trace;
    11 *)
    12 
    13 (** Propositional Logic **)
    14 
    15 (*Blast_tac's runtime for this type of problem appears to be exponential
    16   in its length, though Fast_tac manages*)
    17 Goal "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P";
    18 by (svc_tac 1);
    19 qed "";
    20 
    21 (** Some big tautologies supplied by John Harrison **)
    22 
    23 (*Tautology name: puz013_1.  Auto_tac manages; Blast_tac and Fast_tac take
    24   a minute or more.*)
    25 Goal "~(~v12 & \
    26 \  v0 & \
    27 \  v10 & \
    28 \  (v4 | v5) & \
    29 \  (v9 | v2) & \
    30 \  (v8 | v1) & \
    31 \  (v7 | v0) & \
    32 \  (v3 | v12) & \
    33 \  (v11 | v10) & \
    34 \  (~v12 | ~v6 | v7) & \
    35 \  (~v10 | ~v3 | v1) & \
    36 \  (~v10 | ~v0 | ~v4 | v11) & \
    37 \  (~v5 | ~v2 | ~v8) & \
    38 \  (~v12 | ~v9 | ~v7) & \
    39 \  (~v0 | ~v1 | v4) & \
    40 \  (~v4 | v7 | v2) & \
    41 \  (~v12 | ~v3 | v8) & \
    42 \  (~v4 | v5 | v6) & \
    43 \  (~v7 | ~v8 | v9) & \
    44 \  (~v10 | ~v11 | v12))";
    45 by (svc_tac 1);
    46 qed "";
    47 
    48 (*Tautology name: dk17_be*)
    49 Goal "(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) & \
    50 \   (GE0 <-> GE17 & ~IN5) & \
    51 \   (GE22 <-> ~IN9 & ~IN7 & ~IN6 & IN0) & \
    52 \   (GE19 <-> ~IN5 & ~IN4 & ~IN3 & ~IN0) & \
    53 \   (GE20 <-> ~IN7 & ~IN6) & \
    54 \   (GE18 <-> ~IN6 & ~IN2 & ~IN1 & ~IN0) & \
    55 \   (GE21 <-> IN9 & ~IN7 & IN6 & ~IN0) & \
    56 \   (GE23 <-> GE22 & GE0) & \
    57 \   (GE25 <-> ~IN9 & ~IN7 & IN6 & ~IN0) & \
    58 \   (GE26 <-> IN9 & ~IN7 & ~IN6 & IN0) & \
    59 \   (GE2 <-> GE20 & GE19) & \
    60 \   (GE1 <-> GE18 & ~IN7) & \
    61 \   (GE24 <-> GE23 | GE21 & GE0) & \
    62 \   (GE5 <-> ~IN5 & IN4 | IN5 & ~IN4) & \
    63 \   (GE6 <-> GE0 & IN7 & ~IN6 & ~IN0) & \
    64 \   (GE12 <-> GE26 & GE0 | GE25 & GE0) & \
    65 \   (GE14 <-> GE2 & IN8 & ~IN2 & IN1) & \
    66 \   (GE27 <-> ~IN8 & IN5 & ~IN4 & ~IN3) & \
    67 \   (GE9 <-> GE1 & ~IN5 & ~IN4 & IN3) & \
    68 \   (GE7 <-> GE24 | GE2 & IN2 & ~IN1) & \
    69 \   (GE10 <-> GE6 | GE5 & GE1 & ~IN3) & \
    70 \   (GE15 <-> ~IN8 | IN9) & \
    71 \   (GE16 <-> GE12 | GE14 & ~IN9) & \
    72 \   (GE4 <-> \
    73 \    GE5 & GE1 & IN8 & ~IN3 | \
    74 \    GE0 & ~IN7 & IN6 & ~IN0 | \
    75 \    GE2 & IN2 & ~IN1) & \
    76 \   (GE13 <-> GE27 & GE1) & \
    77 \   (GE11 <-> GE9 | GE6 & ~IN8) & \
    78 \   (GE8 <-> GE1 & ~IN5 & IN4 & ~IN3 | GE2 & ~IN2 & IN1) & \
    79 \   (OUT0 <-> GE7 & ~IN8) & \
    80 \   (OUT1 <-> GE7 & IN8) & \
    81 \   (OUT2 <-> GE8 & ~IN9 | GE10 & IN8) & \
    82 \   (OUT3 <-> GE8 & IN9 & ~IN8 | GE11 & ~IN9 | GE12 & ~IN8) & \
    83 \   (OUT4 <-> GE11 & IN9 | GE12 & IN8) & \
    84 \   (OUT5 <-> GE14 & IN9) & \
    85 \   (OUT6 <-> GE13 & ~IN9) & \
    86 \   (OUT7 <-> GE13 & IN9) & \
    87 \   (OUT8 <-> GE9 & ~IN8 | GE15 & GE6 | GE4 & IN9) & \
    88 \   (OUT9 <-> GE9 & IN8 | ~GE15 & GE10 | GE16) & \
    89 \   (OUT10 <-> GE7) & \
    90 \   (WRES0 <-> ~IN5 & ~IN4 & ~IN3 & ~IN2 & ~IN1) & \
    91 \   (WRES1 <-> ~IN7 & ~IN6 & ~IN2 & ~IN1 & ~IN0) & \
    92 \   (WRES2 <-> ~IN7 & ~IN6 & ~IN5 & ~IN4 & ~IN3 & ~IN0) & \
    93 \   (WRES5 <-> ~IN5 & IN4 | IN5 & ~IN4) & \
    94 \   (WRES6 <-> WRES0 & IN7 & ~IN6 & ~IN0) & \
    95 \   (WRES9 <-> WRES1 & ~IN5 & ~IN4 & IN3) & \
    96 \   (WRES7 <-> \
    97 \    WRES0 & ~IN9 & ~IN7 & ~IN6 & IN0 | \
    98 \    WRES0 & IN9 & ~IN7 & IN6 & ~IN0 | \
    99 \    WRES2 & IN2 & ~IN1) & \
   100 \   (WRES10 <-> WRES6 | WRES5 & WRES1 & ~IN3) & \
   101 \   (WRES12 <-> \
   102 \    WRES0 & IN9 & ~IN7 & ~IN6 & IN0 | \
   103 \    WRES0 & ~IN9 & ~IN7 & IN6 & ~IN0) & \
   104 \   (WRES14 <-> WRES2 & IN8 & ~IN2 & IN1) & \
   105 \   (WRES15 <-> ~IN8 | IN9) & \
   106 \   (WRES4 <-> \
   107 \    WRES5 & WRES1 & IN8 & ~IN3 | \
   108 \    WRES2 & IN2 & ~IN1 | \
   109 \    WRES0 & ~IN7 & IN6 & ~IN0) & \
   110 \   (WRES13 <-> WRES1 & ~IN8 & IN5 & ~IN4 & ~IN3) & \
   111 \   (WRES11 <-> WRES9 | WRES6 & ~IN8) & \
   112 \   (WRES8 <-> WRES1 & ~IN5 & IN4 & ~IN3 | WRES2 & ~IN2 & IN1) \
   113 \   --> (OUT10 <-> WRES7) & \
   114 \       (OUT9 <-> WRES9 & IN8 | WRES12 | WRES14 & ~IN9 | ~WRES15 & WRES10) & \
   115 \       (OUT8 <-> WRES9 & ~IN8 | WRES15 & WRES6 | WRES4 & IN9) & \
   116 \       (OUT7 <-> WRES13 & IN9) & \
   117 \       (OUT6 <-> WRES13 & ~IN9) & \
   118 \       (OUT5 <-> WRES14 & IN9) & \
   119 \       (OUT4 <-> WRES11 & IN9 | WRES12 & IN8) & \
   120 \       (OUT3 <-> WRES8 & IN9 & ~IN8 | WRES11 & ~IN9 | WRES12 & ~IN8) & \
   121 \       (OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) & \
   122 \       (OUT1 <-> WRES7 & IN8) & \
   123 \       (OUT0 <-> WRES7 & ~IN8)";
   124 by (svc_tac 1);
   125 qed "";
   126 
   127 (*Tautology name: sqn_be.  Fast_tac only takes a couple of seconds.*)
   128 Goal "(GE0 <-> IN6 & IN1 | ~IN6 & ~IN1) & \
   129 \  (GE8 <-> ~IN3 & ~IN1) & \
   130 \  (GE5 <-> IN6 | IN5) & \
   131 \  (GE9 <-> ~GE0 | IN2 | ~IN5) & \
   132 \  (GE1 <-> IN3 | ~IN0) & \
   133 \  (GE11 <-> GE8 & IN4) & \
   134 \  (GE3 <-> ~IN4 | ~IN2) & \
   135 \  (GE34 <-> ~GE5 & IN4 | ~GE9) & \
   136 \  (GE2 <-> ~IN4 & IN1) & \
   137 \  (GE14 <-> ~GE1 & ~IN4) & \
   138 \  (GE19 <-> GE11 & ~GE5) & \
   139 \  (GE13 <-> GE8 & ~GE3 & ~IN0) & \
   140 \  (GE20 <-> ~IN5 & IN2 | GE34) & \
   141 \  (GE12 <-> GE2 & ~IN3) & \
   142 \  (GE27 <-> GE14 & IN6 | GE19) & \
   143 \  (GE10 <-> ~IN6 | IN5) & \
   144 \  (GE28 <-> GE13 | GE20 & ~GE1) & \
   145 \  (GE6 <-> ~IN5 | IN6) & \
   146 \  (GE15 <-> GE2 & IN2) & \
   147 \  (GE29 <-> GE27 | GE12 & GE5) & \
   148 \  (GE4 <-> IN3 & ~IN0) & \
   149 \  (GE21 <-> ~GE10 & ~IN1 | ~IN5 & ~IN2) & \
   150 \  (GE30 <-> GE28 | GE14 & IN2) & \
   151 \  (GE31 <-> GE29 | GE15 & ~GE6) & \
   152 \  (GE7 <-> ~IN6 | ~IN5) & \
   153 \  (GE17 <-> ~GE3 & ~IN1) & \
   154 \  (GE18 <-> GE4 & IN2) & \
   155 \  (GE16 <-> GE2 & IN0) & \
   156 \  (GE23 <-> GE19 | GE9 & ~GE1) & \
   157 \  (GE32 <-> GE15 & ~IN6 & ~IN0 | GE21 & GE4 & ~IN4 | GE30 | GE31) & \
   158 \  (GE33 <-> \
   159 \   GE18 & ~GE6 & ~IN4 | \
   160 \   GE17 & ~GE7 & IN3 | \
   161 \   ~GE7 & GE4 & ~GE3 | \
   162 \   GE11 & IN5 & ~IN0) & \
   163 \  (GE25 <-> GE14 & ~GE6 | GE13 & ~GE5 | GE16 & ~IN5 | GE15 & GE1) & \
   164 \  (GE26 <-> \
   165 \   GE12 & IN5 & ~IN2 | \
   166 \   GE10 & GE4 & IN1 | \
   167 \   GE17 & ~GE6 & IN0 | \
   168 \   GE2 & ~IN6) & \
   169 \  (GE24 <-> GE23 | GE16 & GE7) & \
   170 \  (OUT0 <-> \
   171 \   GE6 & IN4 & ~IN1 & IN0 | GE18 & GE0 & ~IN5 | GE12 & ~GE10 | GE24) & \
   172 \  (OUT1 <-> GE26 | GE25 | ~GE5 & GE4 & GE3 | GE7 & ~GE1 & IN1) & \
   173 \  (OUT2 <-> GE33 | GE32) & \
   174 \  (WRES8 <-> ~IN3 & ~IN1) & \
   175 \  (WRES0 <-> IN6 & IN1 | ~IN6 & ~IN1) & \
   176 \  (WRES2 <-> ~IN4 & IN1) & \
   177 \  (WRES3 <-> ~IN4 | ~IN2) & \
   178 \  (WRES1 <-> IN3 | ~IN0) & \
   179 \  (WRES4 <-> IN3 & ~IN0) & \
   180 \  (WRES5 <-> IN6 | IN5) & \
   181 \  (WRES11 <-> WRES8 & IN4) & \
   182 \  (WRES9 <-> ~WRES0 | IN2 | ~IN5) & \
   183 \  (WRES10 <-> ~IN6 | IN5) & \
   184 \  (WRES6 <-> ~IN5 | IN6) & \
   185 \  (WRES7 <-> ~IN6 | ~IN5) & \
   186 \  (WRES12 <-> WRES2 & ~IN3) & \
   187 \  (WRES13 <-> WRES8 & ~WRES3 & ~IN0) & \
   188 \  (WRES14 <-> ~WRES1 & ~IN4) & \
   189 \  (WRES15 <-> WRES2 & IN2) & \
   190 \  (WRES17 <-> ~WRES3 & ~IN1) & \
   191 \  (WRES18 <-> WRES4 & IN2) & \
   192 \  (WRES19 <-> WRES11 & ~WRES5) & \
   193 \  (WRES20 <-> ~IN5 & IN2 | ~WRES5 & IN4 | ~WRES9) & \
   194 \  (WRES21 <-> ~WRES10 & ~IN1 | ~IN5 & ~IN2) & \
   195 \  (WRES16 <-> WRES2 & IN0) \
   196 \  --> (OUT2 <-> \
   197 \       WRES11 & IN5 & ~IN0 | \
   198 \       ~WRES7 & WRES4 & ~WRES3 | \
   199 \       WRES12 & WRES5 | \
   200 \       WRES13 | \
   201 \       WRES14 & IN2 | \
   202 \       WRES14 & IN6 | \
   203 \       WRES15 & ~WRES6 | \
   204 \       WRES15 & ~IN6 & ~IN0 | \
   205 \       WRES17 & ~WRES7 & IN3 | \
   206 \       WRES18 & ~WRES6 & ~IN4 | \
   207 \       WRES20 & ~WRES1 | \
   208 \       WRES21 & WRES4 & ~IN4 | \
   209 \       WRES19) & \
   210 \      (OUT1 <-> \
   211 \       ~WRES5 & WRES4 & WRES3 | \
   212 \       WRES7 & ~WRES1 & IN1 | \
   213 \       WRES2 & ~IN6 | \
   214 \       WRES10 & WRES4 & IN1 | \
   215 \       WRES12 & IN5 & ~IN2 | \
   216 \       WRES13 & ~WRES5 | \
   217 \       WRES14 & ~WRES6 | \
   218 \       WRES15 & WRES1 | \
   219 \       WRES16 & ~IN5 | \
   220 \       WRES17 & ~WRES6 & IN0) & \
   221 \      (OUT0 <-> \
   222 \       WRES6 & IN4 & ~IN1 & IN0 | \
   223 \       WRES9 & ~WRES1 | \
   224 \       WRES12 & ~WRES10 | \
   225 \       WRES16 & WRES7 | \
   226 \       WRES18 & WRES0 & ~IN5 | \
   227 \       WRES19)";
   228 by (svc_tac 1);
   229 qed "";
   230 
   231 
   232 (** Linear arithmetic **)
   233 
   234 Goal "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 & \
   235 \     x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 & \
   236 \     x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)";
   237 by (svc_tac 1);
   238 qed "";
   239 
   240 (*merely to test polarity handling in the presence of biconditionals*)
   241 Goal "(x < (y::int)) = (x+1 <= y)";
   242 by (svc_tac 1);
   243 qed "";
   244 
   245 (** Natural number examples requiring implicit "non-negative" assumptions*)
   246 
   247 Goal "(3::nat)*a <= 2 + 4*b + 6*c  & 11 <= 2*a + b + 2*c & \
   248 \     a + 3*b <= 5 + 2*c  --> 2 + 3*b <= 2*a + 6*c";
   249 by (svc_tac 1);
   250 qed "";
   251 
   252 Goal "(n::nat) < 2 ==> (n = 0) | (n = 1)";
   253 by (svc_tac 1);
   254 qed "";