wneuper/isa: doc-src/Intro/quant.txt@20e3616b2d9c

     1 (**** quantifier examples -- process using Doc/tout quant.txt  ****)

     3 Pretty.setmargin 72;  (*existing macros just allow this margin*)

     4 print_depth 0;

     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);

    21 choplev 0;

    22 by (REPEAT (assume_tac 1

    23      ORELSE resolve_tac [impI,allI] 1

    24      ORELSE dresolve_tac [spec] 1));

    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

    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!

    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!

   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);

   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 -

   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);

   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

   154 uncaught exception ERROR

   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);

   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

   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);

   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!

   235 goal FOL_thy "((EX x.P(x)) --> Q) --> (ALL x.P(x)-->Q)";

   236 by (REPEAT (resolve_tac [impI] 1));

   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);

author	Walther Neuper <neuper@ist.tugraz.at>
	Thu, 12 Aug 2010 15:03:34 +0200
branch	isac-from-Isabelle2009-2
changeset 37913	20e3616b2d9c
parent 105	216d6ed87399
permissions	-rw-r--r--