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