Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed dots;
authorwenzelm
Fri, 10 Oct 1997 18:17:17 +0200
changeset 3839 56544d061e1d
parent 3838 a16277522928
child 3840 e0baea4d485a
fixed dots;
src/Sequents/LK.ML file | annotate | diff | comparison | revisions
src/Sequents/LK.thy file | annotate | diff | comparison | revisions
src/Sequents/ex/LK/hardquant.ML file | annotate | diff | comparison | revisions
src/Sequents/ex/LK/quant.ML file | annotate | diff | comparison | revisions 
--- a/src/Sequents/LK.ML	Fri Oct 10 17:38:50 1997 +0200
+++ b/src/Sequents/LK.ML	Fri Oct 10 18:17:17 1997 +0200
@@ -37,11 +37,11 @@
 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
 
 qed_goal "allL_thin" LK.thy 
-    "$H, P(x), $G |- $E ==> $H, ALL x.P(x), $G |- $E"
+    "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
  (fn prems=> [ (rtac allL 1), (rtac thinL 1), (resolve_tac prems 1) ]);
 
 qed_goal "exR_thin" LK.thy 
-    "$H |- $E, P(x), $F ==> $H |- $E, EX x.P(x), $F"
+    "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
  (fn prems=> [ (rtac exR 1), (rtac thinR 1), (resolve_tac prems 1) ]);
 
 (* Symmetry of equality in hypotheses *)
--- a/src/Sequents/LK.thy	Fri Oct 10 17:38:50 1997 +0200
+++ b/src/Sequents/LK.thy	Fri Oct 10 18:17:17 1997 +0200
@@ -59,11 +59,11 @@
 
   (*Quantifiers*)
 
-  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x.P(x), $F"
-  allL  "$H, P(x), $G, ALL x.P(x) |- $E ==> $H, ALL x.P(x), $G |- $E"
+  allR  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F"
+  allL  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E"
 
-  exR   "$H |- $E, P(x), $F, EX x.P(x) ==> $H |- $E, EX x.P(x), $F"
-  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x.P(x), $G |- $E"
+  exR   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F"
+  exL   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E"
 
   (*Equality*)
 
@@ -75,7 +75,7 @@
   (*Descriptions*)
 
   The "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==> 
-          $H |- $E, P(THE x.P(x)), $F"
+          $H |- $E, P(THE x. P(x)), $F"
 end
 
   ML
--- a/src/Sequents/ex/LK/hardquant.ML	Fri Oct 10 17:38:50 1997 +0200
+++ b/src/Sequents/ex/LK/hardquant.ML	Fri Oct 10 18:17:17 1997 +0200
@@ -18,15 +18,15 @@
 by (fast_tac LK_pack 1);
 result(); 
 
-goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
+goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
 by (fast_tac LK_pack 1);
 result(); 
 
-goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
+goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
 by (fast_tac LK_pack 1);
 result(); 
 
-goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
+goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (fast_tac LK_pack 1);
 result(); 
 
@@ -81,7 +81,7 @@
 
 writeln"Problem 24";
 goal LK.thy "|- ~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &  \
-\    ~(EX x.P(x)) --> (EX x.Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
+\    ~(EX x. P(x)) --> (EX x. Q(x)) & (ALL x. Q(x)|R(x) --> S(x))  \
 \   --> (EX x. P(x)&R(x))";
 by (pc_tac LK_pack 1);
 result();
@@ -114,7 +114,7 @@
 writeln"Problem 28.  AMENDED";
 goal LK.thy "|- (ALL x. P(x) --> (ALL x. Q(x))) &   \
 \       ((ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &  \
-\       ((EX x.S(x)) --> (ALL x. L(x) --> M(x)))  \
+\       ((EX x. S(x)) --> (ALL x. L(x) --> M(x)))  \
 \   --> (ALL x. P(x) & L(x) --> M(x))";
 by (pc_tac LK_pack 1);  
 result();
@@ -134,7 +134,7 @@
 result();
 
 writeln"Problem 31";
-goal LK.thy "|- ~(EX x.P(x) & (Q(x) | R(x))) & \
+goal LK.thy "|- ~(EX x. P(x) & (Q(x) | R(x))) & \
 \       (EX x. L(x) & P(x)) & \
 \       (ALL x. ~ R(x) --> M(x))  \
 \   --> (EX x. L(x) & M(x))";
@@ -184,7 +184,7 @@
 
 writeln"Problem 37";
 goal LK.thy "|- (ALL z. EX w. ALL x. EX y. \
-\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u.Q(u,w)))) & \
+\          (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) & \
 \       (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) & \
 \       ((EX x y. Q(x,y)) --> (ALL x. R(x,x)))  \
 \   --> (ALL x. EX y. R(x,y))";
@@ -246,7 +246,7 @@
 
 writeln"Problem 50";  
 goal LK.thy
-    "|- (ALL x. P(a,x) | (ALL y.P(x,y))) --> (EX x. ALL y.P(x,y))";
+    "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))";
 by (best_tac LK_dup_pack 1);
 result();
 
--- a/src/Sequents/ex/LK/quant.ML	Fri Oct 10 17:38:50 1997 +0200
+++ b/src/Sequents/ex/LK/quant.ML	Fri Oct 10 18:17:17 1997 +0200
@@ -13,20 +13,20 @@
 by (fast_tac LK_pack 1);
 result(); 
 
-goal LK.thy "|- (ALL x y.P(x,y))  <->  (ALL y x.P(x,y))";
+goal LK.thy "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))";
 by (fast_tac LK_pack 1);
 result(); 
 
-goal LK.thy "ALL u.P(u), ALL v.Q(v) |- ALL u v. P(u) & Q(v)";
+goal LK.thy "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)";
 by (fast_tac LK_pack 1);
 result(); 
 
 writeln"Permutation of existential quantifier.";
-goal LK.thy "|- (EX x y.P(x,y)) <-> (EX y x.P(x,y))";
+goal LK.thy "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))";
 by (fast_tac LK_pack 1);
 result(); 
 
-goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x.P(x)) & (ALL x.Q(x))";
+goal LK.thy "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))";
 by (fast_tac LK_pack 1);
 result(); 
 
@@ -43,7 +43,7 @@
 result(); 
 
 
-goal LK.thy "|- (ALL x.P(x)-->Q)  <->  ((EX x.P(x)) --> Q)";
+goal LK.thy "|- (ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)";
 by (fast_tac LK_pack 1);
 result(); 
 
@@ -67,19 +67,19 @@
 
 writeln"Harder examples: classical theorems.";
 
-goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x.Q(x)))";
+goal LK.thy "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))";
 by (fast_tac LK_pack 1);
 result(); 
 (*3 secs*)
 
 
-goal LK.thy "|- (EX x.P(x)-->Q)  <->  (ALL x.P(x)) --> Q";
+goal LK.thy "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q";
 by (fast_tac LK_pack 1);
 result(); 
 (*5 secs*)
 
 
-goal LK.thy "|- (ALL x.P(x)) | Q  <->  (ALL x. P(x) | Q)";
+goal LK.thy "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)";
 by (fast_tac LK_pack 1);
 result(); 
 
@@ -109,24 +109,24 @@
 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
 getgoal 1; 
 
-goal LK.thy "|- P(?a) --> (ALL x.P(x))";
+goal LK.thy "|- P(?a) --> (ALL x. P(x))";
 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
 (*Check that subgoals remain: proof failed.*)
 getgoal 1;  
 
-goal LK.thy "|- (P(?a) --> (ALL x.Q(x))) --> (ALL x. P(x) --> Q(x))";
+goal LK.thy "|- (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
 by (fast_tac LK_pack 1) handle ERROR => writeln"Failed, as expected";
 getgoal 1;  
 
 
 writeln"Back to things that are provable...";
 
-goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x.P(x)) --> (EX x.Q(x))";
+goal LK.thy "|- (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
 by (fast_tac LK_pack 1); 
 result();  
 
 (*An example of why exR should be delayed as long as possible*)
-goal LK.thy "|- (P--> (EX x.Q(x))) & P--> (EX x.Q(x))";
+goal LK.thy "|- (P--> (EX x. Q(x))) & P--> (EX x. Q(x))";
 by (fast_tac LK_pack 1);
 result();  
 
@@ -145,7 +145,7 @@
 
 
 writeln"Principia Mathematica *11.55";
-goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y.Q(x,y)))";
+goal LK.thy "|- (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
 by (fast_tac LK_pack 1);
 result();
isabelle