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