src/Sequents/LK/hardquant.ML
changeset 17481 75166ebb619b
parent 7119 02d94b69ae04
     1.1 --- a/src/Sequents/LK/hardquant.ML	Sun Sep 18 14:25:48 2005 +0200
     1.2 +++ b/src/Sequents/LK/hardquant.ML	Sun Sep 18 15:20:08 2005 +0200
     1.3 @@ -12,25 +12,23 @@
     1.4  Uses pc_tac rather than fast_tac when the former is significantly faster.
     1.5  *)
     1.6  
     1.7 -writeln"File LK/ex/hard-quant.";
     1.8 -
     1.9 -context LK.thy;
    1.10 +context (theory "LK");
    1.11  
    1.12  Goal "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))";
    1.13  by (Fast_tac 1);
    1.14 -result(); 
    1.15 +result();
    1.16  
    1.17  Goal "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
    1.18  by (Fast_tac 1);
    1.19 -result(); 
    1.20 +result();
    1.21  
    1.22  Goal "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
    1.23  by (Fast_tac 1);
    1.24 -result(); 
    1.25 +result();
    1.26  
    1.27  Goal "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
    1.28  by (Fast_tac 1);
    1.29 -result(); 
    1.30 +result();
    1.31  
    1.32  writeln"Problems requiring quantifier duplication";
    1.33  
    1.34 @@ -53,7 +51,7 @@
    1.35  writeln"Problem 18";
    1.36  Goal "|- EX y. ALL x. P(y)-->P(x)";
    1.37  by (best_tac LK_dup_pack 1);
    1.38 -result(); 
    1.39 +result();
    1.40  
    1.41  writeln"Problem 19";
    1.42  Goal "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
    1.43 @@ -63,7 +61,7 @@
    1.44  writeln"Problem 20";
    1.45  Goal "|- (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
    1.46  \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
    1.47 -by (Fast_tac 1); 
    1.48 +by (Fast_tac 1);
    1.49  result();
    1.50  
    1.51  writeln"Problem 21";
    1.52 @@ -73,12 +71,12 @@
    1.53  
    1.54  writeln"Problem 22";
    1.55  Goal "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
    1.56 -by (Fast_tac 1); 
    1.57 +by (Fast_tac 1);
    1.58  result();
    1.59  
    1.60  writeln"Problem 23";
    1.61  Goal "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))";
    1.62 -by (best_tac LK_pack 1);  
    1.63 +by (best_tac LK_pack 1);
    1.64  result();
    1.65  
    1.66  writeln"Problem 24";
    1.67 @@ -94,7 +92,7 @@
    1.68  \       (ALL x. P(x) --> (M(x) & L(x))) &   \
    1.69  \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
    1.70  \   --> (EX x. Q(x)&P(x))";
    1.71 -by (best_tac LK_pack 1);  
    1.72 +by (best_tac LK_pack 1);
    1.73  result();
    1.74  
    1.75  writeln"Problem 26";
    1.76 @@ -110,7 +108,7 @@
    1.77  \             (ALL x. M(x) & L(x) --> P(x)) &   \
    1.78  \             ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))  \
    1.79  \         --> (ALL x. M(x) --> ~L(x))";
    1.80 -by (pc_tac LK_pack 1); 
    1.81 +by (pc_tac LK_pack 1);
    1.82  result();
    1.83  
    1.84  writeln"Problem 28.  AMENDED";
    1.85 @@ -118,21 +116,21 @@
    1.86  \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
    1.87  \       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
    1.88  \   --> (ALL x. P(x) & L(x) --> M(x))";
    1.89 -by (pc_tac LK_pack 1);  
    1.90 +by (pc_tac LK_pack 1);
    1.91  result();
    1.92  
    1.93  writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
    1.94  Goal "|- (EX x. P(x)) & (EX y. Q(y))  \
    1.95  \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
    1.96  \        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
    1.97 -by (pc_tac LK_pack 1); 
    1.98 +by (pc_tac LK_pack 1);
    1.99  result();
   1.100  
   1.101  writeln"Problem 30";
   1.102  Goal "|- (ALL x. P(x) | Q(x) --> ~ R(x)) & \
   1.103  \       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
   1.104  \   --> (ALL x. S(x))";
   1.105 -by (Fast_tac 1);  
   1.106 +by (Fast_tac 1);
   1.107  result();
   1.108  
   1.109  writeln"Problem 31";
   1.110 @@ -238,7 +236,7 @@
   1.111  \     (EX x. f(x) & (ALL y. h(x,y) --> l(y))                    \
   1.112  \                  & (ALL y. g(y) & h(x,y) --> j(x,y)))         \
   1.113  \     --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))";
   1.114 -by (best_tac LK_pack 1); 
   1.115 +by (best_tac LK_pack 1);
   1.116  result();
   1.117  
   1.118  
   1.119 @@ -249,7 +247,7 @@
   1.120  by (fast_tac (pack() add_safes [subst]) 1);
   1.121  result();
   1.122  
   1.123 -writeln"Problem 50";  
   1.124 +writeln"Problem 50";
   1.125  Goal "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
   1.126  by (best_tac LK_dup_pack 1);
   1.127  result();
   1.128 @@ -287,7 +285,7 @@
   1.129  writeln"Problem 59";
   1.130  (*Unification works poorly here -- the abstraction %sobj prevents efficient
   1.131    operation of the occurs check*)
   1.132 -Unify.trace_bound := !Unify.search_bound - 1; 
   1.133 +Unify.trace_bound := !Unify.search_bound - 1;
   1.134  Goal "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))";
   1.135  by (best_tac LK_dup_pack 1);
   1.136  result();
   1.137 @@ -304,8 +302,7 @@
   1.138  by (Fast_tac 1);
   1.139  result();
   1.140  
   1.141 -writeln"Reached end of file.";
   1.142 -
   1.143  (*18 June 92: loaded in 372 secs*)
   1.144  (*19 June 92: loaded in 166 secs except #34, using repeat_goal_tac*)
   1.145  (*29 June 92: loaded in 370 secs*)
   1.146 +(*18 September 2005: loaded in 1.809 secs*)