src/FOL/ex/Classical.thy
author haftmann
Tue, 10 Jul 2007 17:30:50 +0200
changeset 23709 fd31da8f752a
parent 16417 9bc16273c2d4
child 26342 0f65fa163304
permissions -rw-r--r--
moved lfp_induct2 here
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14236
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     1
(*  Title:      FOL/ex/Classical
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     2
    ID:         $Id$
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     4
    Copyright   1994  University of Cambridge
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     5
*)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     6
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     7
header{*Classical Predicate Calculus Problems*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
     8
16417
9bc16273c2d4 migrated theory headers to new format
haftmann
parents: 14236
diff changeset
     9
theory Classical imports FOL begin
14236
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    10
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    11
lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    12
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    13
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    14
text{*If and only if*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    15
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    16
lemma "(P<->Q) <-> (Q<->P)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    17
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    18
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    19
lemma "~ (P <-> ~P)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    20
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    21
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    22
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    23
text{*Sample problems from 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    24
  F. J. Pelletier, 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    25
  Seventy-Five Problems for Testing Automatic Theorem Provers,
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    26
  J. Automated Reasoning 2 (1986), 191-216.
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    27
  Errata, JAR 4 (1988), 236-236.
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    28
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    29
The hardest problems -- judging by experience with several theorem provers,
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    30
including matrix ones -- are 34 and 43.
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    31
*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    32
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    33
subsection{*Pelletier's examples*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    34
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    35
text{*1*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    36
lemma "(P-->Q)  <->  (~Q --> ~P)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    37
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    38
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    39
text{*2*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    40
lemma "~ ~ P  <->  P"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    41
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    42
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    43
text{*3*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    44
lemma "~(P-->Q) --> (Q-->P)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    45
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    46
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    47
text{*4*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    48
lemma "(~P-->Q)  <->  (~Q --> P)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    49
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    50
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    51
text{*5*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    52
lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    53
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    54
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    55
text{*6*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    56
lemma "P | ~ P"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    57
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    58
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    59
text{*7*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    60
lemma "P | ~ ~ ~ P"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    61
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    62
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    63
text{*8.  Peirce's law*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    64
lemma "((P-->Q) --> P)  -->  P"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    65
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    66
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    67
text{*9*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    68
lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    69
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    70
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    71
text{*10*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    72
lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    73
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    74
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    75
text{*11.  Proved in each direction (incorrectly, says Pelletier!!)  *}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    76
lemma "P<->P"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    77
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    78
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    79
text{*12.  "Dijkstra's law"*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    80
lemma "((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    81
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    82
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    83
text{*13.  Distributive law*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    84
lemma "P | (Q & R)  <-> (P | Q) & (P | R)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    85
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    86
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    87
text{*14*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    88
lemma "(P <-> Q) <-> ((Q | ~P) & (~Q|P))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    89
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    90
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    91
text{*15*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    92
lemma "(P --> Q) <-> (~P | Q)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    93
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    94
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    95
text{*16*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    96
lemma "(P-->Q) | (Q-->P)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    97
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    98
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
    99
text{*17*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   100
lemma "((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   101
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   102
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   103
subsection{*Classical Logic: examples with quantifiers*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   104
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   105
lemma "(\<forall>x. P(x) & Q(x)) <-> (\<forall>x. P(x))  &  (\<forall>x. Q(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   106
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   107
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   108
lemma "(\<exists>x. P-->Q(x))  <->  (P --> (\<exists>x. Q(x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   109
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   110
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   111
lemma "(\<exists>x. P(x)-->Q)  <->  (\<forall>x. P(x)) --> Q"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   112
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   113
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   114
lemma "(\<forall>x. P(x)) | Q  <->  (\<forall>x. P(x) | Q)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   115
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   116
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   117
text{*Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   118
  JAR 10 (265-281), 1993.  Proof is trivial!*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   119
lemma "~((\<exists>x.~P(x)) & ((\<exists>x. P(x)) | (\<exists>x. P(x) & Q(x))) & ~ (\<exists>x. P(x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   120
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   121
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   122
subsection{*Problems requiring quantifier duplication*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   123
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   124
text{*Theorem B of Peter Andrews, Theorem Proving via General Matings, 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   125
  JACM 28 (1981).*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   126
lemma "(\<exists>x. \<forall>y. P(x) <-> P(y)) --> ((\<exists>x. P(x)) <-> (\<forall>y. P(y)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   127
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   128
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   129
text{*Needs multiple instantiation of ALL.*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   130
lemma "(\<forall>x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   131
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   132
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   133
text{*Needs double instantiation of the quantifier*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   134
lemma "\<exists>x. P(x) --> P(a) & P(b)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   135
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   136
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   137
lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   138
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   139
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   140
lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   141
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   142
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   143
text{*V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23.  NOT PROVED*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   144
lemma "\<exists>x x'. \<forall>y. \<exists>z z'.  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   145
                (~P(y,y) | P(x,x) | ~S(z,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   146
                (S(x,y) | ~S(y,z) | Q(z',z'))  &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   147
                (Q(x',y) | ~Q(y,z') | S(x',x'))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   148
oops
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   149
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   150
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   151
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   152
subsection{*Hard examples with quantifiers*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   153
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   154
text{*18*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   155
lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   156
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   157
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   158
text{*19*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   159
lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   160
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   161
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   162
text{*20*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   163
lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w)))      
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   164
    --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   165
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   166
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   167
text{*21*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   168
lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P<->Q(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   169
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   170
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   171
text{*22*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   172
lemma "(\<forall>x. P <-> Q(x))  -->  (P <-> (\<forall>x. Q(x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   173
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   174
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   175
text{*23*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   176
lemma "(\<forall>x. P | Q(x))  <->  (P | (\<forall>x. Q(x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   177
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   178
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   179
text{*24*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   180
lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) &   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   181
      (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   182
    --> (\<exists>x. P(x)&R(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   183
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   184
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   185
text{*25*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   186
lemma "(\<exists>x. P(x)) &   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   187
      (\<forall>x. L(x) --> ~ (M(x) & R(x))) &   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   188
      (\<forall>x. P(x) --> (M(x) & L(x))) &    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   189
      ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x)))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   190
    --> (\<exists>x. Q(x)&P(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   191
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   192
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   193
text{*26*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   194
lemma "((\<exists>x. p(x)) <-> (\<exists>x. q(x))) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   195
      (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) <-> s(y)))    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   196
  --> ((\<forall>x. p(x)-->r(x)) <-> (\<forall>x. q(x)-->s(x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   197
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   198
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   199
text{*27*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   200
lemma "(\<exists>x. P(x) & ~Q(x)) &    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   201
      (\<forall>x. P(x) --> R(x)) &    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   202
      (\<forall>x. M(x) & L(x) --> P(x)) &    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   203
      ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x)))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   204
  --> (\<forall>x. M(x) --> ~L(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   205
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   206
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   207
text{*28.  AMENDED*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   208
lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) &    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   209
        ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) &   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   210
        ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x)))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   211
    --> (\<forall>x. P(x) & L(x) --> M(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   212
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   213
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   214
text{*29.  Essentially the same as Principia Mathematica *11.71*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   215
lemma "(\<exists>x. P(x)) & (\<exists>y. Q(y))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   216
    --> ((\<forall>x. P(x)-->R(x)) & (\<forall>y. Q(y)-->S(y))   <->      
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   217
         (\<forall>x y. P(x) & Q(y) --> R(x) & S(y)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   218
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   219
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   220
text{*30*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   221
lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   222
      (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   223
    --> (\<forall>x. S(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   224
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   225
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   226
text{*31*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   227
lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   228
        (\<exists>x. L(x) & P(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   229
        (\<forall>x. ~ R(x) --> M(x))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   230
    --> (\<exists>x. L(x) & M(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   231
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   232
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   233
text{*32*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   234
lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   235
      (\<forall>x. S(x) & R(x) --> L(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   236
      (\<forall>x. M(x) --> R(x))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   237
      --> (\<forall>x. P(x) & M(x) --> L(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   238
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   239
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   240
text{*33*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   241
lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c))  <->     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   242
      (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   243
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   244
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   245
text{*34  AMENDED (TWICE!!).  Andrews's challenge*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   246
lemma "((\<exists>x. \<forall>y. p(x) <-> p(y))  <->                 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   247
       ((\<exists>x. q(x)) <-> (\<forall>y. p(y))))     <->         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   248
      ((\<exists>x. \<forall>y. q(x) <-> q(y))  <->                 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   249
       ((\<exists>x. p(x)) <-> (\<forall>y. q(y))))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   250
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   251
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   252
text{*35*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   253
lemma "\<exists>x y. P(x,y) -->  (\<forall>u v. P(u,v))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   254
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   255
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   256
text{*36*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   257
lemma "(\<forall>x. \<exists>y. J(x,y)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   258
      (\<forall>x. \<exists>y. G(x,y)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   259
      (\<forall>x y. J(x,y) | G(x,y) --> (\<forall>z. J(y,z) | G(y,z) --> H(x,z)))    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   260
  --> (\<forall>x. \<exists>y. H(x,y))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   261
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   262
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   263
text{*37*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   264
lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   265
           (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (\<exists>u. Q(u,w)))) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   266
      (\<forall>x z. ~P(x,z) --> (\<exists>y. Q(y,z))) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   267
      ((\<exists>x y. Q(x,y)) --> (\<forall>x. R(x,x)))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   268
      --> (\<forall>x. \<exists>y. R(x,y))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   269
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   270
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   271
text{*38*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   272
lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r(x,y))) -->         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   273
             (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z)))  <->          
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   274
      (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))) &     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   275
              (~p(a) | ~(\<exists>y. p(y) & r(x,y)) |                           
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   276
              (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   277
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   278
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   279
text{*39*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   280
lemma "~ (\<exists>x. \<forall>y. F(y,x) <-> ~F(y,y))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   281
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   282
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   283
text{*40.  AMENDED*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   284
lemma "(\<exists>y. \<forall>x. F(x,y) <-> F(x,x)) -->   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   285
              ~(\<forall>x. \<exists>y. \<forall>z. F(z,y) <-> ~ F(z,x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   286
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   287
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   288
text{*41*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   289
lemma "(\<forall>z. \<exists>y. \<forall>x. f(x,y) <-> f(x,z) & ~ f(x,x))         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   290
          --> ~ (\<exists>z. \<forall>x. f(x,z))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   291
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   292
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   293
text{*42*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   294
lemma "~ (\<exists>y. \<forall>x. p(x,y) <-> ~ (\<exists>z. p(x,z) & p(z,x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   295
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   296
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   297
text{*43*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   298
lemma "(\<forall>x. \<forall>y. q(x,y) <-> (\<forall>z. p(z,x) <-> p(z,y)))      
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   299
          --> (\<forall>x. \<forall>y. q(x,y) <-> q(y,x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   300
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   301
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   302
(*Other proofs: Can use auto, which cheats by using rewriting!  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   303
  Deepen_tac alone requires 253 secs.  Or
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   304
  by (mini_tac 1 THEN Deepen_tac 5 1) *)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   305
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   306
text{*44*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   307
lemma "(\<forall>x. f(x) --> (\<exists>y. g(y) & h(x,y) & (\<exists>y. g(y) & ~ h(x,y)))) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   308
      (\<exists>x. j(x) & (\<forall>y. g(y) --> h(x,y)))                    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   309
      --> (\<exists>x. j(x) & ~f(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   310
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   311
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   312
text{*45*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   313
lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h(x,y) --> j(x,y))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   314
                      --> (\<forall>y. g(y) & h(x,y) --> k(y))) &     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   315
      ~ (\<exists>y. l(y) & k(y)) &                                    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   316
      (\<exists>x. f(x) & (\<forall>y. h(x,y) --> l(y))                     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   317
                  & (\<forall>y. g(y) & h(x,y) --> j(x,y)))           
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   318
      --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h(x,y)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   319
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   320
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   321
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   322
text{*46*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   323
lemma "(\<forall>x. f(x) & (\<forall>y. f(y) & h(y,x) --> g(y)) --> g(x)) &       
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   324
      ((\<exists>x. f(x) & ~g(x)) -->                                     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   325
       (\<exists>x. f(x) & ~g(x) & (\<forall>y. f(y) & ~g(y) --> j(x,y)))) &     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   326
      (\<forall>x y. f(x) & f(y) & h(x,y) --> ~j(y,x))                     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   327
       --> (\<forall>x. f(x) --> g(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   328
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   329
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   330
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   331
subsection{*Problems (mainly) involving equality or functions*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   332
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   333
text{*48*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   334
lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   335
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   336
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   337
text{*49  NOT PROVED AUTOMATICALLY.  Hard because it involves substitution
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   338
  for Vars
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   339
  the type constraint ensures that x,y,z have the same type as a,b,u. *}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   340
lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & a~=b  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   341
                --> (\<forall>u::'a. P(u))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   342
apply safe
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   343
apply (rule_tac x = a in allE, assumption)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   344
apply (rule_tac x = b in allE, assumption, fast)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   345
       --{*blast's treatment of equality can't do it*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   346
done
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   347
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   348
text{*50.  (What has this to do with equality?) *}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   349
lemma "(\<forall>x. P(a,x) | (\<forall>y. P(x,y))) --> (\<exists>x. \<forall>y. P(x,y))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   350
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   351
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   352
text{*51*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   353
lemma "(\<exists>z w. \<forall>x y. P(x,y) <->  (x=z & y=w)) -->   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   354
      (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) <-> y=w) <-> x=z)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   355
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   356
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   357
text{*52*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   358
text{*Almost the same as 51. *}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   359
lemma "(\<exists>z w. \<forall>x y. P(x,y) <->  (x=z & y=w)) -->   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   360
      (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) <-> x=z) <-> y=w)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   361
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   362
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   363
text{*55*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   364
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   365
(*Original, equational version by Len Schubert, via Pelletier *** NOT PROVED
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   366
Goal "(\<exists>x. lives(x) & killed(x,agatha)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   367
   lives(agatha) & lives(butler) & lives(charles) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   368
   (\<forall>x. lives(x) --> x=agatha | x=butler | x=charles) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   369
   (\<forall>x y. killed(x,y) --> hates(x,y)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   370
   (\<forall>x y. killed(x,y) --> ~richer(x,y)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   371
   (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   372
   (\<forall>x. ~ x=butler --> hates(agatha,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   373
   (\<forall>x. ~richer(x,agatha) --> hates(butler,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   374
   (\<forall>x. hates(agatha,x) --> hates(butler,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   375
   (\<forall>x. \<exists>y. ~hates(x,y)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   376
   ~ agatha=butler -->  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   377
   killed(?who,agatha)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   378
by Safe_tac;
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   379
by (dres_inst_tac [("x1","x")] (spec RS mp) 1);
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   380
by (assume_tac 1);
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   381
by (etac (spec RS exE) 1);
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   382
by (REPEAT (etac allE 1));
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   383
by (Blast_tac 1);
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   384
result();
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   385
****)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   386
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   387
text{*Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   388
  fast DISCOVERS who killed Agatha. *}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   389
lemma "lives(agatha) & lives(butler) & lives(charles) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   390
   (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   391
   (\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   392
   (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   393
   (hates(agatha,agatha) & hates(agatha,charles)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   394
   (\<forall>x. lives(x) & ~richer(x,agatha) --> hates(butler,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   395
   (\<forall>x. hates(agatha,x) --> hates(butler,x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   396
   (\<forall>x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) -->  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   397
    killed(?who,agatha)"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   398
by fast --{*MUCH faster than blast*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   399
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   400
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   401
text{*56*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   402
lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) <-> (\<forall>x. P(x) --> P(f(x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   403
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   404
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   405
text{*57*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   406
lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   407
     (\<forall>x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   408
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   409
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   410
text{*58  NOT PROVED AUTOMATICALLY*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   411
lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   412
by (slow elim: subst_context)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   413
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   414
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   415
text{*59*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   416
lemma "(\<forall>x. P(x) <-> ~P(f(x))) --> (\<exists>x. P(x) & ~P(f(x)))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   417
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   418
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   419
text{*60*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   420
lemma "\<forall>x. P(x,f(x)) <-> (\<exists>y. (\<forall>z. P(z,y) --> P(z,f(x))) & P(x,y))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   421
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   422
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   423
text{*62 as corrected in JAR 18 (1997), page 135*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   424
lemma "(\<forall>x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->      
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   425
      (\<forall>x. (~p(a) | p(x) | p(f(f(x)))) &                       
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   426
              (~p(a) | ~p(f(x)) | p(f(f(x)))))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   427
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   428
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   429
text{*From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   430
  fast indeed copes!*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   431
lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   432
              (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) &    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   433
              (\<forall>x. K(x) --> ~G(x))  -->  (\<exists>x. K(x) & J(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   434
by fast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   435
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   436
text{*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   437
  It does seem obvious!*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   438
lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   439
      (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y)))  &         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   440
      (\<forall>x. K(x) --> ~G(x))   -->   (\<exists>x. K(x) --> ~G(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   441
by fast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   442
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   443
text{*Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   444
	author U. Egly*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   445
lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->                
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   446
   (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))                   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   447
  &                                                                      
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   448
  (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->                 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   449
        (\<forall>y z.                                                        
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   450
            (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &                    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   451
            (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))                    
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   452
  &                                                                      
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   453
  (\<forall>w. C(w) &                                                         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   454
    (\<forall>y z.                                                            
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   455
        (C(y) & P(y,z) --> Q(w,y,z) & OO(w,g)) &                         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   456
        (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))) -->                     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   457
    (\<exists>v. C(v) &                                                        
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   458
          (\<forall>y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) &            
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   459
                  ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   460
   -->                   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   461
   ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   462
by (tactic{*Blast.depth_tac (claset ()) 12 1*})
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   463
   --{*Needed because the search for depths below 12 is very slow*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   464
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   465
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   466
text{*Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   467
lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->        
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   468
   (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))           
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   469
  &                                                              
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   470
  (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->         
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   471
        (\<forall>y z.                                                
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   472
            (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &           
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   473
            (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))          
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   474
  &                                                              
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   475
  ((\<exists>w. C(w) & (\<forall>y. (C(y) &  P(y,y) --> Q(w,y,y) & OO(w,g)) & 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   476
                         (C(y) & ~P(y,y) --> Q(w,y,y) & OO(w,b))))  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   477
   -->                                                             
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   478
   (\<exists>v. C(v) & (\<forall>y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   479
                         (C(y) & ~P(y,y) --> P(v,y) & OO(v,b)))))  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   480
  -->                                                              
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   481
  ((\<exists>v. C(v) & (\<forall>y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   482
                         (C(y) & ~P(y,y) --> P(v,y) & OO(v,b))))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   483
   -->                                                             
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   484
   (\<exists>u. C(u) & (\<forall>y. (C(y) &  P(y,y) --> ~P(u,y)) &     
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   485
                         (C(y) & ~P(y,y) --> P(u,y) & OO(u,b)))))  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   486
   -->                                                             
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   487
   ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   488
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   489
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   490
text{* Challenge found on info-hol *}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   491
lemma "\<forall>x. \<exists>v w. \<forall>y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   492
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   493
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   494
text{*Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   495
can be deleted.*}
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   496
lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   497
      ~ (\<exists>x. grocer(x) & healthy(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   498
      (\<forall>x. industrious(x) & grocer(x) --> honest(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   499
      (\<forall>x. cyclist(x) --> industrious(x)) &  
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   500
      (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x))   
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   501
      --> (\<forall>x. grocer(x) --> ~cyclist(x))"
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   502
by blast
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   503
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   504
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   505
(*Runtimes for old versions of this file:
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   506
Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   507
Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac] 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   508
Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   509
Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions] 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   510
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   511
Further runtimes on a Sun-4
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   512
Tue Mar  4 1997: loaded in 93s (version 94-7) 
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   513
Tue Mar  4 1997: loaded in 89s
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   514
Thu Apr  3 1997: loaded in 44s--using mostly Blast_tac
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   515
Thu Apr  3 1997: loaded in 96s--addition of two Halting Probs
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   516
Thu Apr  3 1997: loaded in 98s--using lim-1 for all haz rules
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   517
Tue Dec  2 1997: loaded in 107s--added 46; new equalSubst
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   518
Fri Dec 12 1997: loaded in 91s--faster proof reconstruction
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   519
Thu Dec 18 1997: loaded in 94s--two new "obvious theorems" (??)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   520
*)
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   521
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   522
end
c73d62ce9d1c partial conversion to Isar scripts
paulson
parents:
diff changeset
   523