Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
authorpaulson
Mon Feb 10 12:52:11 1997 +0100 (1997-02-10)
changeset 26034988dda71c0b
parent 2602 5ac837d98a85
child 2604 605e54988d50
Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
with Basis Library structure Int
src/FOLP/ex/ROOT.ML
src/FOLP/ex/int.ML
src/FOLP/intprover.ML
src/FOLP/simpdata.ML
     1.1 --- a/src/FOLP/ex/ROOT.ML	Mon Feb 10 12:34:54 1997 +0100
     1.2 +++ b/src/FOLP/ex/ROOT.ML	Mon Feb 10 12:52:11 1997 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  writeln"\n** Intuitionistic examples **\n";
     1.5  time_use     "int.ML";
     1.6  
     1.7 -val thy = IFOLP.thy  and  tac = Int.fast_tac 1;
     1.8 +val thy = IFOLP.thy  and  tac = IntPr.fast_tac 1;
     1.9  time_use     "prop.ML";
    1.10  time_use     "quant.ML";
    1.11  
     2.1 --- a/src/FOLP/ex/int.ML	Mon Feb 10 12:34:54 1997 +0100
     2.2 +++ b/src/FOLP/ex/int.ML	Mon Feb 10 12:52:11 1997 +0100
     2.3 @@ -6,13 +6,13 @@
     2.4  Intuitionistic First-Order Logic
     2.5  
     2.6  Single-step commands:
     2.7 -by (Int.step_tac 1);
     2.8 +by (IntPr.step_tac 1);
     2.9  by (biresolve_tac safe_brls 1);
    2.10  by (biresolve_tac haz_brls 1);
    2.11  by (assume_tac 1);
    2.12 -by (Int.safe_tac 1);
    2.13 -by (Int.mp_tac 1);
    2.14 -by (Int.fast_tac 1);
    2.15 +by (IntPr.safe_tac 1);
    2.16 +by (IntPr.mp_tac 1);
    2.17 +by (IntPr.fast_tac 1);
    2.18  *)
    2.19  
    2.20  writeln"File FOLP/ex/int.ML";
    2.21 @@ -30,34 +30,34 @@
    2.22  *)
    2.23  
    2.24  goal IFOLP.thy "?p : ~~(P&Q) <-> ~~P & ~~Q";
    2.25 -by (Int.fast_tac 1);
    2.26 +by (IntPr.fast_tac 1);
    2.27  result();
    2.28  
    2.29  goal IFOLP.thy "?p : ~~~P <-> ~P";
    2.30 -by (Int.fast_tac 1);
    2.31 +by (IntPr.fast_tac 1);
    2.32  result();
    2.33  
    2.34  goal IFOLP.thy "?p : ~~((P --> Q | R)  -->  (P-->Q) | (P-->R))";
    2.35 -by (Int.fast_tac 1);
    2.36 +by (IntPr.fast_tac 1);
    2.37  result();
    2.38  
    2.39  goal IFOLP.thy "?p : (P<->Q) <-> (Q<->P)";
    2.40 -by (Int.fast_tac 1);
    2.41 +by (IntPr.fast_tac 1);
    2.42  result();
    2.43  
    2.44  
    2.45  writeln"Lemmas for the propositional double-negation translation";
    2.46  
    2.47  goal IFOLP.thy "?p : P --> ~~P";
    2.48 -by (Int.fast_tac 1);
    2.49 +by (IntPr.fast_tac 1);
    2.50  result();
    2.51  
    2.52  goal IFOLP.thy "?p : ~~(~~P --> P)";
    2.53 -by (Int.fast_tac 1);
    2.54 +by (IntPr.fast_tac 1);
    2.55  result();
    2.56  
    2.57  goal IFOLP.thy "?p : ~~P & ~~(P --> Q) --> ~~Q";
    2.58 -by (Int.fast_tac 1);
    2.59 +by (IntPr.fast_tac 1);
    2.60  result();
    2.61  
    2.62  
    2.63 @@ -65,12 +65,12 @@
    2.64  
    2.65  (*The attempt to prove them terminates quickly!*)
    2.66  goal IFOLP.thy "?p : ((P-->Q) --> P)  -->  P";
    2.67 -by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    2.68 +by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    2.69  (*Check that subgoals remain: proof failed.*)
    2.70  getgoal 1;  
    2.71  
    2.72  goal IFOLP.thy "?p : (P&Q-->R)  -->  (P-->R) | (Q-->R)";
    2.73 -by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    2.74 +by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
    2.75  getgoal 1;  
    2.76  
    2.77  
    2.78 @@ -78,100 +78,100 @@
    2.79  
    2.80  writeln"Problem ~~1";
    2.81  goal IFOLP.thy "?p : ~~((P-->Q)  <->  (~Q --> ~P))";
    2.82 -by (Int.fast_tac 1);
    2.83 +by (IntPr.fast_tac 1);
    2.84  result();
    2.85  (*5 secs*)
    2.86  
    2.87  
    2.88  writeln"Problem ~~2";
    2.89  goal IFOLP.thy "?p : ~~(~~P  <->  P)";
    2.90 -by (Int.fast_tac 1);
    2.91 +by (IntPr.fast_tac 1);
    2.92  result();
    2.93  (*1 secs*)
    2.94  
    2.95  
    2.96  writeln"Problem 3";
    2.97  goal IFOLP.thy "?p : ~(P-->Q) --> (Q-->P)";
    2.98 -by (Int.fast_tac 1);
    2.99 +by (IntPr.fast_tac 1);
   2.100  result();
   2.101  
   2.102  writeln"Problem ~~4";
   2.103  goal IFOLP.thy "?p : ~~((~P-->Q)  <->  (~Q --> P))";
   2.104 -by (Int.fast_tac 1);
   2.105 +by (IntPr.fast_tac 1);
   2.106  result();
   2.107  (*9 secs*)
   2.108  
   2.109  writeln"Problem ~~5";
   2.110  goal IFOLP.thy "?p : ~~((P|Q-->P|R) --> P|(Q-->R))";
   2.111 -by (Int.fast_tac 1);
   2.112 +by (IntPr.fast_tac 1);
   2.113  result();
   2.114  (*10 secs*)
   2.115  
   2.116  
   2.117  writeln"Problem ~~6";
   2.118  goal IFOLP.thy "?p : ~~(P | ~P)";
   2.119 -by (Int.fast_tac 1);
   2.120 +by (IntPr.fast_tac 1);
   2.121  result();
   2.122  
   2.123  writeln"Problem ~~7";
   2.124  goal IFOLP.thy "?p : ~~(P | ~~~P)";
   2.125 -by (Int.fast_tac 1);
   2.126 +by (IntPr.fast_tac 1);
   2.127  result();
   2.128  
   2.129  writeln"Problem ~~8.  Peirce's law";
   2.130  goal IFOLP.thy "?p : ~~(((P-->Q) --> P)  -->  P)";
   2.131 -by (Int.fast_tac 1);
   2.132 +by (IntPr.fast_tac 1);
   2.133  result();
   2.134  
   2.135  writeln"Problem 9";
   2.136  goal IFOLP.thy "?p : ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   2.137 -by (Int.fast_tac 1);
   2.138 +by (IntPr.fast_tac 1);
   2.139  result();
   2.140  (*9 secs*)
   2.141  
   2.142  
   2.143  writeln"Problem 10";
   2.144  goal IFOLP.thy "?p : (Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)";
   2.145 -by (Int.fast_tac 1);
   2.146 +by (IntPr.fast_tac 1);
   2.147  result();
   2.148  
   2.149  writeln"11.  Proved in each direction (incorrectly, says Pelletier!!) ";
   2.150  goal IFOLP.thy "?p : P<->P";
   2.151 -by (Int.fast_tac 1);
   2.152 +by (IntPr.fast_tac 1);
   2.153  
   2.154  writeln"Problem ~~12.  Dijkstra's law  ";
   2.155  goal IFOLP.thy "?p : ~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))";
   2.156 -by (Int.fast_tac 1);
   2.157 +by (IntPr.fast_tac 1);
   2.158  result();
   2.159  
   2.160  goal IFOLP.thy "?p : ((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))";
   2.161 -by (Int.fast_tac 1);
   2.162 +by (IntPr.fast_tac 1);
   2.163  result();
   2.164  
   2.165  writeln"Problem 13.  Distributive law";
   2.166  goal IFOLP.thy "?p : P | (Q & R)  <-> (P | Q) & (P | R)";
   2.167 -by (Int.fast_tac 1);
   2.168 +by (IntPr.fast_tac 1);
   2.169  result();
   2.170  
   2.171  writeln"Problem ~~14";
   2.172  goal IFOLP.thy "?p : ~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))";
   2.173 -by (Int.fast_tac 1);
   2.174 +by (IntPr.fast_tac 1);
   2.175  result();
   2.176  
   2.177  writeln"Problem ~~15";
   2.178  goal IFOLP.thy "?p : ~~((P --> Q) <-> (~P | Q))";
   2.179 -by (Int.fast_tac 1);
   2.180 +by (IntPr.fast_tac 1);
   2.181  result();
   2.182  
   2.183  writeln"Problem ~~16";
   2.184  goal IFOLP.thy "?p : ~~((P-->Q) | (Q-->P))";
   2.185 -by (Int.fast_tac 1);
   2.186 +by (IntPr.fast_tac 1);
   2.187  result();
   2.188  
   2.189  writeln"Problem ~~17";
   2.190  goal IFOLP.thy
   2.191    "?p : ~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))";
   2.192 -by (Int.fast_tac 1);
   2.193 +by (IntPr.fast_tac 1);
   2.194  (*over 5 minutes?? -- printing the proof term takes 40 secs!!*)
   2.195  result();
   2.196  
   2.197 @@ -181,23 +181,23 @@
   2.198  writeln"The converse is classical in the following implications...";
   2.199  
   2.200  goal IFOLP.thy "?p : (EX x.P(x)-->Q)  -->  (ALL x.P(x)) --> Q";
   2.201 -by (Int.fast_tac 1); 
   2.202 +by (IntPr.fast_tac 1); 
   2.203  result();  
   2.204  
   2.205  goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)";
   2.206 -by (Int.fast_tac 1); 
   2.207 +by (IntPr.fast_tac 1); 
   2.208  result();  
   2.209  
   2.210  goal IFOLP.thy "?p : ((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))";
   2.211 -by (Int.fast_tac 1); 
   2.212 +by (IntPr.fast_tac 1); 
   2.213  result();  
   2.214  
   2.215  goal IFOLP.thy "?p : (ALL x.P(x)) | Q  -->  (ALL x. P(x) | Q)";
   2.216 -by (Int.fast_tac 1); 
   2.217 +by (IntPr.fast_tac 1); 
   2.218  result();  
   2.219  
   2.220  goal IFOLP.thy "?p : (EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))";
   2.221 -by (Int.fast_tac 1);
   2.222 +by (IntPr.fast_tac 1);
   2.223  result();  
   2.224  
   2.225  
   2.226 @@ -207,24 +207,24 @@
   2.227  (*The attempt to prove them terminates quickly!*)
   2.228  
   2.229  goal IFOLP.thy "?p : ((ALL x.P(x))-->Q) --> (EX x.P(x)-->Q)";
   2.230 -by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.231 +by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.232  getgoal 1; 
   2.233  
   2.234  goal IFOLP.thy "?p : (P --> (EX x.Q(x))) --> (EX x. P-->Q(x))";
   2.235 -by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.236 +by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.237  getgoal 1; 
   2.238  
   2.239  goal IFOLP.thy "?p : (ALL x. P(x) | Q) --> ((ALL x.P(x)) | Q)";
   2.240 -by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.241 +by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.242  getgoal 1; 
   2.243  
   2.244  goal IFOLP.thy "?p : (ALL x. ~~P(x)) --> ~~(ALL x. P(x))";
   2.245 -by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.246 +by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.247  getgoal 1; 
   2.248  
   2.249  (*Classically but not intuitionistically valid.  Proved by a bug in 1986!*)
   2.250  goal IFOLP.thy "?p : EX x. Q(x) --> (ALL x. Q(x))";
   2.251 -by (Int.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.252 +by (IntPr.fast_tac 1) handle ERROR => writeln"Failed, as expected";  
   2.253  getgoal 1; 
   2.254  
   2.255  
   2.256 @@ -244,7 +244,7 @@
   2.257  writeln"Problem 20";
   2.258  goal IFOLP.thy "?p : (ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))     \
   2.259  \   --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))";
   2.260 -by (Int.fast_tac 1); 
   2.261 +by (IntPr.fast_tac 1); 
   2.262  result();
   2.263  
   2.264  writeln"Problem 21";
   2.265 @@ -254,12 +254,12 @@
   2.266  
   2.267  writeln"Problem 22";
   2.268  goal IFOLP.thy "?p : (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))";
   2.269 -by (Int.fast_tac 1); 
   2.270 +by (IntPr.fast_tac 1); 
   2.271  result();
   2.272  
   2.273  writeln"Problem ~~23";
   2.274  goal IFOLP.thy "?p : ~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))";
   2.275 -by (Int.best_tac 1);  
   2.276 +by (IntPr.best_tac 1);  
   2.277  result();
   2.278  
   2.279  writeln"Problem 24";
   2.280 @@ -267,10 +267,10 @@
   2.281  \    (~(EX x.P(x)) --> (EX x.Q(x))) & (ALL x. Q(x)|R(x) --> S(x))  \
   2.282  \   --> ~~(EX x. P(x)&R(x))";
   2.283  (*Not clear why fast_tac, best_tac, ASTAR and ITER_DEEPEN all take forever*)
   2.284 -by Int.safe_tac; 
   2.285 +by IntPr.safe_tac; 
   2.286  by (etac impE 1);
   2.287 -by (Int.fast_tac 1); 
   2.288 -by (Int.fast_tac 1); 
   2.289 +by (IntPr.fast_tac 1); 
   2.290 +by (IntPr.fast_tac 1); 
   2.291  result();
   2.292  
   2.293  writeln"Problem 25";
   2.294 @@ -279,21 +279,21 @@
   2.295  \       (ALL x. P(x) --> (M(x) & L(x))) &   \
   2.296  \       ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))  \
   2.297  \   --> (EX x. Q(x)&P(x))";
   2.298 -by (Int.best_tac 1);
   2.299 +by (IntPr.best_tac 1);
   2.300  result();
   2.301  
   2.302  writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
   2.303  goal IFOLP.thy "?p : (EX x. P(x)) & (EX y. Q(y))  \
   2.304  \   --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->     \
   2.305  \        (ALL x y. P(x) & Q(y) --> R(x) & S(y)))";
   2.306 -by (Int.fast_tac 1); 
   2.307 +by (IntPr.fast_tac 1); 
   2.308  result();
   2.309  
   2.310  writeln"Problem ~~30";
   2.311  goal IFOLP.thy "?p : (ALL x. (P(x) | Q(x)) --> ~ R(x)) & \
   2.312  \       (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
   2.313  \   --> (ALL x. ~~S(x))";
   2.314 -by (Int.fast_tac 1);  
   2.315 +by (IntPr.fast_tac 1);  
   2.316  result();
   2.317  
   2.318  writeln"Problem 31";
   2.319 @@ -301,7 +301,7 @@
   2.320  \       (EX x. L(x) & P(x)) & \
   2.321  \       (ALL x. ~ R(x) --> M(x))  \
   2.322  \   --> (EX x. L(x) & M(x))";
   2.323 -by (Int.fast_tac 1);
   2.324 +by (IntPr.fast_tac 1);
   2.325  result();
   2.326  
   2.327  writeln"Problem 32";
   2.328 @@ -309,18 +309,18 @@
   2.329  \       (ALL x. S(x) & R(x) --> L(x)) & \
   2.330  \       (ALL x. M(x) --> R(x))  \
   2.331  \   --> (ALL x. P(x) & M(x) --> L(x))";
   2.332 -by (Int.best_tac 1);  (*SLOW*)
   2.333 +by (IntPr.best_tac 1);  (*SLOW*)
   2.334  result();
   2.335  
   2.336  writeln"Problem 39";
   2.337  goal IFOLP.thy "?p : ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))";
   2.338 -by (Int.fast_tac 1);
   2.339 +by (IntPr.fast_tac 1);
   2.340  result();
   2.341  
   2.342  writeln"Problem 40.  AMENDED";
   2.343  goal IFOLP.thy "?p : (EX y. ALL x. F(x,y) <-> F(x,x)) -->  \
   2.344  \             ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))";
   2.345 -by (Int.fast_tac 1);
   2.346 +by (IntPr.fast_tac 1);
   2.347  result();
   2.348  
   2.349  writeln"Problem 44";
   2.350 @@ -328,38 +328,38 @@
   2.351  \             (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &       \
   2.352  \             (EX x. j(x) & (ALL y. g(y) --> h(x,y)))                   \
   2.353  \             --> (EX x. j(x) & ~f(x))";
   2.354 -by (Int.fast_tac 1);
   2.355 +by (IntPr.fast_tac 1);
   2.356  result();
   2.357  
   2.358  writeln"Problem 48";
   2.359  goal IFOLP.thy "?p : (a=b | c=d) & (a=c | b=d) --> a=d | b=c";
   2.360 -by (Int.fast_tac 1);
   2.361 +by (IntPr.fast_tac 1);
   2.362  result();
   2.363  
   2.364  writeln"Problem 51";
   2.365  goal IFOLP.thy
   2.366      "?p : (EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->  \
   2.367  \    (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)";
   2.368 -by (Int.best_tac 1);  (*60 seconds*)
   2.369 +by (IntPr.best_tac 1);  (*60 seconds*)
   2.370  result();
   2.371  
   2.372  writeln"Problem 56";
   2.373  goal IFOLP.thy
   2.374      "?p : (ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))";
   2.375 -by (Int.fast_tac 1);
   2.376 +by (IntPr.fast_tac 1);
   2.377  result();
   2.378  
   2.379  writeln"Problem 57";
   2.380  goal IFOLP.thy
   2.381      "?p : P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) & \
   2.382  \    (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))";
   2.383 -by (Int.fast_tac 1);
   2.384 +by (IntPr.fast_tac 1);
   2.385  result();
   2.386  
   2.387  writeln"Problem 60";
   2.388  goal IFOLP.thy
   2.389      "?p : ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
   2.390 -by (Int.fast_tac 1);
   2.391 +by (IntPr.fast_tac 1);
   2.392  result();
   2.393  
   2.394  writeln"Reached end of file.";
     3.1 --- a/src/FOLP/intprover.ML	Mon Feb 10 12:34:54 1997 +0100
     3.2 +++ b/src/FOLP/intprover.ML	Mon Feb 10 12:52:11 1997 +0100
     3.3 @@ -5,12 +5,12 @@
     3.4  
     3.5  A naive prover for intuitionistic logic
     3.6  
     3.7 -BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use Int.fast_tac ...
     3.8 +BEWARE OF NAME CLASHES WITH CLASSICAL TACTICS -- use IntPr.fast_tac ...
     3.9  
    3.10  Completeness (for propositional logic) is proved in 
    3.11  
    3.12  Roy Dyckhoff.
    3.13 -Contraction-Free Sequent Calculi for Intuitionistic Logic.
    3.14 +Contraction-Free Sequent Calculi for IntPruitionistic Logic.
    3.15  J. Symbolic Logic (in press)
    3.16  *)
    3.17  
    3.18 @@ -27,7 +27,7 @@
    3.19    end;
    3.20  
    3.21  
    3.22 -structure Int : INT_PROVER   = 
    3.23 +structure IntPr : INT_PROVER   = 
    3.24  struct
    3.25  
    3.26  (*Negation is treated as a primitive symbol, with rules notI (introduction),
     4.1 --- a/src/FOLP/simpdata.ML	Mon Feb 10 12:34:54 1997 +0100
     4.2 +++ b/src/FOLP/simpdata.ML	Mon Feb 10 12:52:11 1997 +0100
     4.3 @@ -10,7 +10,7 @@
     4.4  
     4.5  fun int_prove_fun_raw s = 
     4.6      (writeln s;  prove_goal IFOLP.thy s
     4.7 -       (fn prems => [ (cut_facts_tac prems 1), (Int.fast_tac 1) ]));
     4.8 +       (fn prems => [ (cut_facts_tac prems 1), (IntPr.fast_tac 1) ]));
     4.9  
    4.10  fun int_prove_fun s = int_prove_fun_raw ("?p : "^s);
    4.11