src/FOLP/ex/quant.ML
changeset 3836 f1a1817659e6
parent 1464 a608f83e3421
child 5061 f947332d5465
equal deleted inserted replaced
3835:9a5a4e123859 3836:f1a1817659e6
     7 Needs declarations of the theory "thy" and the tactic "tac"
     7 Needs declarations of the theory "thy" and the tactic "tac"
     8 *)
     8 *)
     9 
     9 
    10 writeln"File FOLP/ex/quant.ML";
    10 writeln"File FOLP/ex/quant.ML";
    11 
    11 
    12 goal thy "?p : (ALL x y.P(x,y))  -->  (ALL y x.P(x,y))";
    12 goal thy "?p : (ALL x y. P(x,y))  -->  (ALL y x. P(x,y))";
    13 by tac;
    13 by tac;
    14 result();  
    14 result();  
    15 
    15 
    16 
    16 
    17 goal thy "?p : (EX x y.P(x,y)) --> (EX y x.P(x,y))";
    17 goal thy "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
    18 by tac;
    18 by tac;
    19 result();  
    19 result();  
    20 
    20 
    21 
    21 
    22 (*Converse is false*)
    22 (*Converse is false*)
    23 goal thy "?p : (ALL x.P(x)) | (ALL x.Q(x)) --> (ALL x. P(x) | Q(x))";
    23 goal thy "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
    24 by tac;
    24 by tac;
    25 result();  
    25 result();  
    26 
    26 
    27 goal thy "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x.Q(x)))";
    27 goal thy "?p : (ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))";
    28 by tac;
    28 by tac;
    29 result();  
    29 result();  
    30 
    30 
    31 
    31 
    32 goal thy "?p : (ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
    32 goal thy "?p : (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
    33 by tac;
    33 by tac;
    34 result();  
    34 result();  
    35 
    35 
    36 
    36 
    37 writeln"Some harder ones";
    37 writeln"Some harder ones";
    38 
    38 
    39 goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x.P(x)) | (EX x.Q(x))";
    39 goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
    40 by tac;
    40 by tac;
    41 result();  
    41 result();  
    42 (*6 secs*)
    42 (*6 secs*)
    43 
    43 
    44 (*Converse is false*)
    44 (*Converse is false*)
    45 goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x.P(x))  &  (EX x.Q(x))";
    45 goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))";
    46 by tac;
    46 by tac;
    47 result();  
    47 result();  
    48 
    48 
    49 
    49 
    50 writeln"Basic test of quantifier reasoning";
    50 writeln"Basic test of quantifier reasoning";
    68 
    68 
    69 goal thy "?p : (EX x. Q(x))  -->  (ALL x. Q(x))";
    69 goal thy "?p : (EX x. Q(x))  -->  (ALL x. Q(x))";
    70 by tac handle ERROR => writeln"Failed, as expected";  
    70 by tac handle ERROR => writeln"Failed, as expected";  
    71 getgoal 1; 
    71 getgoal 1; 
    72 
    72 
    73 goal thy "?p : P(?a) --> (ALL x.P(x))";
    73 goal thy "?p : P(?a) --> (ALL x. P(x))";
    74 by tac handle ERROR => writeln"Failed, as expected";
    74 by tac handle ERROR => writeln"Failed, as expected";
    75 (*Check that subgoals remain: proof failed.*)
    75 (*Check that subgoals remain: proof failed.*)
    76 getgoal 1;  
    76 getgoal 1;  
    77 
    77 
    78 goal thy
    78 goal thy
    79     "?p : (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
    79     "?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
    80 by tac handle ERROR => writeln"Failed, as expected";
    80 by tac handle ERROR => writeln"Failed, as expected";
    81 getgoal 1;  
    81 getgoal 1;  
    82 
    82 
    83 
    83 
    84 writeln"Back to things that are provable...";
    84 writeln"Back to things that are provable...";
    85 
    85 
    86 goal thy "?p : (ALL x.P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
    86 goal thy "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
    87 by tac;  
    87 by tac;  
    88 result();  
    88 result();  
    89 
    89 
    90 
    90 
    91 (*An example of why exI should be delayed as long as possible*)
    91 (*An example of why exI should be delayed as long as possible*)
    92 goal thy "?p : (P --> (EX x.Q(x))) & P --> (EX x.Q(x))";
    92 goal thy "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
    93 by tac;  
    93 by tac;  
    94 result();  
    94 result();  
    95 
    95 
    96 goal thy "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
    96 goal thy "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
    97 by tac; 
    97 by tac;