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