doc-src/Intro/quant.txt
author wenzelm
Thu, 17 Jul 1997 15:03:38 +0200
changeset 3524 c02cb15830de
parent 105 216d6ed87399
permissions -rw-r--r--
fixed EqI meta rule;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
105
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     1
(**** quantifier examples -- process using Doc/tout quant.txt  ****)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     3
Pretty.setmargin 72;  (*existing macros just allow this margin*)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     4
print_depth 0;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     5
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     6
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     7
goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     8
by (resolve_tac [impI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
     9
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    10
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    11
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    12
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    13
by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    14
choplev 1;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    15
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    16
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    17
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    18
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    19
by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    20
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    21
choplev 0;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    22
by (REPEAT (assume_tac 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    23
     ORELSE resolve_tac [impI,allI] 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    24
     ORELSE dresolve_tac [spec] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    25
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    26
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    27
- goal Int_Rule.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    28
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    29
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    30
 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    31
val it = [] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    32
- by (resolve_tac [impI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    33
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    34
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    35
 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    36
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    37
- by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    38
Level 2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    39
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    40
 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    41
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    42
- by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    43
Level 3
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    44
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    45
 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    46
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    47
- by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    48
Level 4
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    49
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    50
 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    51
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    52
- by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    53
Level 5
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    54
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    55
 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    56
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    57
- by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    58
by: tactic returned no results
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    59
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    60
uncaught exception ERROR
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    61
- choplev 1;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    62
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    63
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    64
 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    65
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    66
- by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    67
Level 2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    68
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    69
 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    70
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    71
- by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    72
Level 3
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    73
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    74
 1. !!z w. ALL x y. P(x,y) ==> P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    75
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    76
- by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    77
Level 4
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    78
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    79
 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    80
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    81
- by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    82
Level 5
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    83
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    84
 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    85
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    86
- by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    87
Level 6
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    88
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    89
No subgoals!
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    90
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    91
> choplev 0;
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    92
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    93
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    94
 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    95
> by (REPEAT (assume_tac 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    96
#      ORELSE resolve_tac [impI,allI] 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    97
#      ORELSE dresolve_tac [spec] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    98
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
    99
(ALL x y. P(x,y)) --> (ALL z w. P(w,z))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   100
No subgoals!
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   101
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   102
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   103
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   104
goal FOL_thy "ALL x. EX y. x=y";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   105
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   106
by (resolve_tac [exI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   107
by (resolve_tac [refl] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   108
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   109
- goal Int_Rule.thy "ALL x. EX y. x=y";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   110
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   111
ALL x. EX y. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   112
 1. ALL x. EX y. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   113
val it = [] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   114
- by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   115
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   116
ALL x. EX y. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   117
 1. !!x. EX y. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   118
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   119
- by (resolve_tac [exI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   120
Level 2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   121
ALL x. EX y. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   122
 1. !!x. x = ?y1(x)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   123
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   124
- by (resolve_tac [refl] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   125
Level 3
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   126
ALL x. EX y. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   127
No subgoals!
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   128
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   129
-
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   130
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   131
goal FOL_thy "EX y. ALL x. x=y";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   132
by (resolve_tac [exI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   133
by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   134
by (resolve_tac [refl] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   135
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   136
- goal Int_Rule.thy "EX y. ALL x. x=y";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   137
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   138
EX y. ALL x. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   139
 1. EX y. ALL x. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   140
val it = [] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   141
- by (resolve_tac [exI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   142
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   143
EX y. ALL x. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   144
 1. ALL x. x = ?y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   145
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   146
- by (resolve_tac [allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   147
Level 2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   148
EX y. ALL x. x = y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   149
 1. !!x. x = ?y
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   150
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   151
- by (resolve_tac [refl] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   152
by: tactic returned no results
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   153
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   154
uncaught exception ERROR
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   155
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   156
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   157
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   158
goal FOL_thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   159
by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   160
by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   161
by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   162
by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   163
by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   164
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   165
- goal Int_Rule.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   166
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   167
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   168
 1. EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   169
val it = [] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   170
- by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   171
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   172
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   173
 1. ALL x. EX v. ALL y. EX w. P(?u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   174
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   175
- by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   176
Level 2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   177
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   178
 1. !!x. EX v. ALL y. EX w. P(?u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   179
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   180
- by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   181
Level 3
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   182
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   183
 1. !!x. ALL y. EX w. P(?u,x,?v2(x),y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   184
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   185
- by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   186
Level 4
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   187
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   188
 1. !!x y. EX w. P(?u,x,?v2(x),y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   189
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   190
- by (resolve_tac [exI, allI] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   191
Level 5
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   192
EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   193
 1. !!x y. P(?u,x,?v2(x),y,?w4(x,y))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   194
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   195
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   196
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   197
goal FOL_thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   198
by (REPEAT (resolve_tac [impI] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   199
by (eresolve_tac [exE] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   200
by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   201
by (eresolve_tac [mp] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   202
by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   203
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   204
- goal Int_Rule.thy "(ALL x.P(x) --> Q) --> (EX x.P(x))-->Q";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   205
Level 0
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   206
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   207
 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   208
val it = [] : thm list
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   209
- by (REPEAT (resolve_tac [impI] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   210
Level 1
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   211
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   212
 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   213
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   214
- by (eresolve_tac [exE] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   215
Level 2
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   216
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   217
 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   218
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   219
- by (dresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   220
Level 3
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   221
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   222
 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   223
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   224
- by (eresolve_tac [mp] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   225
Level 4
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   226
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   227
 1. !!x. P(x) ==> P(?x3(x))
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   228
val it = () : unit
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   229
- by (assume_tac 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   230
Level 5
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   231
(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   232
No subgoals!
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   233
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   234
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   235
goal FOL_thy "((EX x.P(x)) --> Q) --> (ALL x.P(x)-->Q)";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   236
by (REPEAT (resolve_tac [impI] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   237
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   238
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   239
goal FOL_thy "(EX x.P(x) --> Q) --> (ALL x.P(x))-->Q";
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   240
by (REPEAT (resolve_tac [impI] 1));
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   241
by (eresolve_tac [exE] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   242
by (eresolve_tac [mp] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   243
by (eresolve_tac [spec] 1);
216d6ed87399 Initial revision
lcp
parents:
diff changeset
   244