src/FOLP/ex/quant.ML
changeset 17480 fd19f77dcf60
parent 15661 9ef583b08647
child 18678 dd0c569fa43d
     1.1 --- a/src/FOLP/ex/quant.ML	Sat Sep 17 20:49:14 2005 +0200
     1.2 +++ b/src/FOLP/ex/quant.ML	Sun Sep 18 14:25:48 2005 +0200
     1.3 @@ -7,101 +7,99 @@
     1.4  Needs declarations of the theory "thy" and the tactic "tac"
     1.5  *)
     1.6  
     1.7 -writeln"File FOLP/ex/quant.ML";
     1.8 -
     1.9  Goal "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
    1.10  by tac;
    1.11 -result();  
    1.12 +result();
    1.13  
    1.14  
    1.15  Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
    1.16  by tac;
    1.17 -result();  
    1.18 +result();
    1.19  
    1.20  
    1.21  (*Converse is false*)
    1.22  Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
    1.23  by tac;
    1.24 -result();  
    1.25 +result();
    1.26  
    1.27  Goal "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
    1.28  by tac;
    1.29 -result();  
    1.30 +result();
    1.31  
    1.32  
    1.33  Goal "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
    1.34  by tac;
    1.35 -result();  
    1.36 +result();
    1.37  
    1.38  
    1.39  writeln"Some harder ones";
    1.40  
    1.41  Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
    1.42  by tac;
    1.43 -result();  
    1.44 +result();
    1.45  (*6 secs*)
    1.46  
    1.47  (*Converse is false*)
    1.48  Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
    1.49  by tac;
    1.50 -result();  
    1.51 +result();
    1.52  
    1.53  
    1.54  writeln"Basic test of quantifier reasoning";
    1.55  (*TRUE*)
    1.56  Goal "?p : (EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))";
    1.57 -by tac;  
    1.58 -result();  
    1.59 +by tac;
    1.60 +result();
    1.61  
    1.62  
    1.63  Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
    1.64 -by tac;  
    1.65 -result();  
    1.66 +by tac;
    1.67 +result();
    1.68  
    1.69  
    1.70  writeln"The following should fail, as they are false!";
    1.71  
    1.72  Goal "?p : (ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))";
    1.73 -by tac handle ERROR => writeln"Failed, as expected";  
    1.74 +by tac handle ERROR => writeln"Failed, as expected";
    1.75  (*Check that subgoals remain: proof failed.*)
    1.76 -getgoal 1; 
    1.77 +getgoal 1;
    1.78  
    1.79  Goal "?p : (EX x. Q(x))  -->  (ALL x. Q(x))";
    1.80 -by tac handle ERROR => writeln"Failed, as expected";  
    1.81 -getgoal 1; 
    1.82 +by tac handle ERROR => writeln"Failed, as expected";
    1.83 +getgoal 1;
    1.84  
    1.85  Goal "?p : P(?a) --> (ALL x. P(x))";
    1.86  by tac handle ERROR => writeln"Failed, as expected";
    1.87  (*Check that subgoals remain: proof failed.*)
    1.88 -getgoal 1;  
    1.89 +getgoal 1;
    1.90  
    1.91  Goal
    1.92      "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
    1.93  by tac handle ERROR => writeln"Failed, as expected";
    1.94 -getgoal 1;  
    1.95 +getgoal 1;
    1.96  
    1.97  
    1.98  writeln"Back to things that are provable...";
    1.99  
   1.100  Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
   1.101 -by tac;  
   1.102 -result();  
   1.103 +by tac;
   1.104 +result();
   1.105  
   1.106  
   1.107  (*An example of why exI should be delayed as long as possible*)
   1.108  Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
   1.109 -by tac;  
   1.110 -result();  
   1.111 +by tac;
   1.112 +result();
   1.113  
   1.114  Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
   1.115 -by tac; 
   1.116 -(*Verify that no subgoals remain.*) 
   1.117 -uresult();  
   1.118 +by tac;
   1.119 +(*Verify that no subgoals remain.*)
   1.120 +uresult();
   1.121  
   1.122  
   1.123  Goal "?p : (ALL x. Q(x))  -->  (EX x. Q(x))";
   1.124  by tac;
   1.125 -result();  
   1.126 +result();
   1.127  
   1.128  
   1.129  writeln"Some slow ones";
   1.130 @@ -110,20 +108,17 @@
   1.131  (*Principia Mathematica *11.53  *)
   1.132  Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
   1.133  by tac;
   1.134 -result();  
   1.135 +result();
   1.136  (*6 secs*)
   1.137  
   1.138  (*Principia Mathematica *11.55  *)
   1.139  Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
   1.140  by tac;
   1.141 -result();  
   1.142 +result();
   1.143  (*9 secs*)
   1.144  
   1.145  (*Principia Mathematica *11.61  *)
   1.146  Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
   1.147  by tac;
   1.148 -result();  
   1.149 +result();
   1.150  (*3 secs*)
   1.151 -
   1.152 -writeln"Reached end of file.";
   1.153 -