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