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