src/LK/ex/quant.ML
author clasohm
Thu Sep 16 12:20:38 1993 +0200 (1993-09-16)
changeset 0 a5a9c433f639
child 1461 6bcb44e4d6e5
permissions -rw-r--r--
Initial revision
     1 (*  Title: 	LK/ex/quant
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1992  University of Cambridge
     5 
     6 Classical sequent calculus: examples with quantifiers.
     7 *)
     8 
     9 
    10 writeln"LK/ex/quant: Examples with quantifiers";
    11 
    12 goal LK.thy "|- (ALL x. P)  <->  P";
    13 by (fast_tac LK_pack 1);
    14 result(); 
    15 
    16 goal LK.thy "|- (ALL x y.P(x,y))  <->  (ALL y x.P(x,y))";
    17 by (fast_tac LK_pack 1);
    18 result(); 
    19 
    20 goal LK.thy "ALL u.P(u), ALL v.Q(v) |- ALL u v. P(u) & Q(v)";
    21 by (fast_tac LK_pack 1);
    22 result(); 
    23 
    24 writeln"Permutation of existential quantifier.";
    25 goal LK.thy "|- (EX x y.P(x,y)) <-> (EX y x.P(x,y))";
    26 by (fast_tac LK_pack 1);
    27 result(); 
    28 
    29 goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))";
    30 by (fast_tac LK_pack 1);
    31 result(); 
    32 
    33 
    34 (*Converse is invalid*)
    35 goal LK.thy "|- (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x)|Q(x))";
    36 by (fast_tac LK_pack 1);
    37 result(); 
    38 
    39 
    40 writeln"Pushing ALL into an implication.";
    41 goal LK.thy "|- (ALL x. P --> Q(x))  <->  (P --> (ALL x. Q(x)))";
    42 by (fast_tac LK_pack 1);
    43 result(); 
    44 
    45 
    46 goal LK.thy "|- (ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
    47 by (fast_tac LK_pack 1);
    48 result(); 
    49 
    50 
    51 goal LK.thy "|- (EX x. P)  <->  P";
    52 by (fast_tac LK_pack 1);
    53 result(); 
    54 
    55 
    56 writeln"Distribution of EX over disjunction.";
    57 goal LK.thy "|- (EX x. P(x) | Q(x)) <-> (EX x. P(x))  |  (EX x. Q(x))";
    58 by (fast_tac LK_pack 1);
    59 result(); 
    60 (*5 secs*)
    61 
    62 (*Converse is invalid*)
    63 goal LK.thy "|- (EX x. P(x) & Q(x))  -->  (EX x. P(x))  &  (EX x. Q(x))";
    64 by (fast_tac LK_pack 1);
    65 result(); 
    66 
    67 
    68 writeln"Harder examples: classical theorems.";
    69 
    70 goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
    71 by (fast_tac LK_pack 1);
    72 result(); 
    73 (*3 secs*)
    74 
    75 
    76 goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
    77 by (fast_tac LK_pack 1);
    78 result(); 
    79 (*5 secs*)
    80 
    81 
    82 goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
    83 by (fast_tac LK_pack 1);
    84 result(); 
    85 
    86 
    87 writeln"Basic test of quantifier reasoning";
    88 goal LK.thy
    89    "|- (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
    90 by (fast_tac LK_pack 1);
    91 result();  
    92 
    93 
    94 goal LK.thy "|- (ALL x. Q(x))  -->  (EX x. Q(x))";
    95 by (fast_tac LK_pack 1);
    96 result();  
    97 
    98 
    99 writeln"The following are invalid!";
   100 
   101 (*INVALID*)
   102 goal LK.thy "|- (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
   103 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected"; 
   104 (*Check that subgoals remain: proof failed.*)
   105 getgoal 1; 
   106 
   107 (*INVALID*)
   108 goal LK.thy "|- (EX x. Q(x))  -->  (ALL x. Q(x))";
   109 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
   110 getgoal 1; 
   111 
   112 goal LK.thy "|- P(?a) --> (ALL x.P(x))";
   113 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
   114 (*Check that subgoals remain: proof failed.*)
   115 getgoal 1;  
   116 
   117 goal LK.thy "|- (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
   118 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
   119 getgoal 1;  
   120 
   121 
   122 writeln"Back to things that are provable...";
   123 
   124 goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
   125 by (fast_tac LK_pack 1); 
   126 result();  
   127 
   128 (*An example of why exR should be delayed as long as possible*)
   129 goal LK.thy "|- (P--> (EX x.Q(x))) & P--> (EX x.Q(x))";
   130 by (fast_tac LK_pack 1);
   131 result();  
   132 
   133 writeln"Solving for a Var";
   134 goal LK.thy 
   135    "|- (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
   136 by (fast_tac LK_pack 1);
   137 result();
   138 
   139 
   140 writeln"Principia Mathematica *11.53";
   141 goal LK.thy 
   142     "|- (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
   143 by (fast_tac LK_pack 1);
   144 result();
   145 
   146 
   147 writeln"Principia Mathematica *11.55";
   148 goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y.Q(x,y)))";
   149 by (fast_tac LK_pack 1);
   150 result();
   151 
   152 writeln"Principia Mathematica *11.61";
   153 goal LK.thy
   154    "|- (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
   155 by (fast_tac LK_pack 1);
   156 result();
   157 
   158 writeln"Reached end of file.";
   159 
   160 (*21 August 88: loaded in 45.7 secs*)