--- a/src/FOLP/ex/If.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/FOLP/ex/If.ML Mon Jun 22 15:09:59 1998 +0200
@@ -22,7 +22,7 @@
val ifE = result();
-goal If.thy
+Goal
"?p : if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))";
by (rtac iffI 1);
by (etac ifE 1);
@@ -36,7 +36,7 @@
val if_commute = result();
-goal If.thy "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
+Goal "?p : if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
by (fast_tac if_cs 1);
val nested_ifs = result();
--- a/src/FOLP/ex/Nat.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/FOLP/ex/Nat.ML Mon Jun 22 15:09:59 1998 +0200
@@ -13,7 +13,7 @@
open Nat;
-goal Nat.thy "?p : ~ (Suc(k) = k)";
+Goal "?p : ~ (Suc(k) = k)";
by (res_inst_tac [("n","k")] induct 1);
by (rtac notI 1);
by (etac Suc_neq_0 1);
@@ -23,7 +23,7 @@
val Suc_n_not_n = result();
-goal Nat.thy "?p : (k+m)+n = k+(m+n)";
+Goal "?p : (k+m)+n = k+(m+n)";
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
by (rtac induct 1);
back();
@@ -33,11 +33,11 @@
back();
back();
-goalw Nat.thy [add_def] "?p : 0+n = n";
+Goalw [add_def] "?p : 0+n = n";
by (rtac rec_0 1);
val add_0 = result();
-goalw Nat.thy [add_def] "?p : Suc(m)+n = Suc(m+n)";
+Goalw [add_def] "?p : Suc(m)+n = Suc(m+n)";
by (rtac rec_Suc 1);
val add_Suc = result();
@@ -61,19 +61,19 @@
val add_ss = FOLP_ss addcongs nat_congs
addrews [add_0, add_Suc];
-goal Nat.thy "?p : (k+m)+n = k+(m+n)";
+Goal "?p : (k+m)+n = k+(m+n)";
by (res_inst_tac [("n","k")] induct 1);
by (SIMP_TAC add_ss 1);
by (ASM_SIMP_TAC add_ss 1);
val add_assoc = result();
-goal Nat.thy "?p : m+0 = m";
+Goal "?p : m+0 = m";
by (res_inst_tac [("n","m")] induct 1);
by (SIMP_TAC add_ss 1);
by (ASM_SIMP_TAC add_ss 1);
val add_0_right = result();
-goal Nat.thy "?p : m+Suc(n) = Suc(m+n)";
+Goal "?p : m+Suc(n) = Suc(m+n)";
by (res_inst_tac [("n","m")] induct 1);
by (ALLGOALS (ASM_SIMP_TAC add_ss));
val add_Suc_right = result();
--- a/src/FOLP/ex/Prolog.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/FOLP/ex/Prolog.ML Mon Jun 22 15:09:59 1998 +0200
@@ -8,19 +8,19 @@
open Prolog;
-goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)";
+Goal "app(a:b:c:Nil, d:e:Nil, ?x)";
by (resolve_tac [appNil,appCons] 1);
by (resolve_tac [appNil,appCons] 1);
by (resolve_tac [appNil,appCons] 1);
by (resolve_tac [appNil,appCons] 1);
prth (result());
-goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)";
+Goal "app(?x, c:d:Nil, a:b:c:d:Nil)";
by (REPEAT (resolve_tac [appNil,appCons] 1));
result();
-goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)";
+Goal "app(?x, ?y, a:b:c:d:Nil)";
by (REPEAT (resolve_tac [appNil,appCons] 1));
back();
back();
@@ -32,16 +32,16 @@
(*app([x1,...,xn], y, ?z) requires (n+1) inferences*)
(*rev([x1,...,xn], ?y) requires (n+1)(n+2)/2 inferences*)
-goal Prolog.thy "rev(a:b:c:d:Nil, ?x)";
+Goal "rev(a:b:c:d:Nil, ?x)";
val rules = [appNil,appCons,revNil,revCons];
by (REPEAT (resolve_tac rules 1));
result();
-goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
+Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)";
by (REPEAT (resolve_tac rules 1));
result();
-goal Prolog.thy "rev(?x, a:b:c:Nil)";
+Goal "rev(?x, a:b:c:Nil)";
by (REPEAT (resolve_tac rules 1)); (*does not solve it directly!*)
back();
back();
@@ -53,19 +53,19 @@
by prolog_tac;
result();
-goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
+Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)";
by prolog_tac;
result();
(*rev([a..p], ?w) requires 153 inferences *)
-goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)";
+Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil, ?w)";
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
(*Poly/ML: 4 secs >> 38 lips*)
result();
(*?x has 16, ?y has 32; rev(?y,?w) requires 561 (rather large) inferences;
total inferences = 2 + 1 + 17 + 561 = 581*)
-goal Prolog.thy
+Goal
"a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)";
by (DEPTH_SOLVE (resolve_tac ([refl,conjI]@rules) 1));
(*Poly/ML: 29 secs >> 20 lips*)
--- a/src/FOLP/ex/prop.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/FOLP/ex/prop.ML Mon Jun 22 15:09:59 1998 +0200
@@ -11,66 +11,66 @@
writeln"commutative laws of & and | ";
-goal thy "?p : P & Q --> Q & P";
+Goal "?p : P & Q --> Q & P";
by tac;
result();
-goal thy "?p : P | Q --> Q | P";
+Goal "?p : P | Q --> Q | P";
by tac;
result();
writeln"associative laws of & and | ";
-goal thy "?p : (P & Q) & R --> P & (Q & R)";
+Goal "?p : (P & Q) & R --> P & (Q & R)";
by tac;
result();
-goal thy "?p : (P | Q) | R --> P | (Q | R)";
+Goal "?p : (P | Q) | R --> P | (Q | R)";
by tac;
result();
writeln"distributive laws of & and | ";
-goal thy "?p : (P & Q) | R --> (P | R) & (Q | R)";
+Goal "?p : (P & Q) | R --> (P | R) & (Q | R)";
by tac;
result();
-goal thy "?p : (P | R) & (Q | R) --> (P & Q) | R";
+Goal "?p : (P | R) & (Q | R) --> (P & Q) | R";
by tac;
result();
-goal thy "?p : (P | Q) & R --> (P & R) | (Q & R)";
+Goal "?p : (P | Q) & R --> (P & R) | (Q & R)";
by tac;
result();
-goal thy "?p : (P & R) | (Q & R) --> (P | Q) & R";
+Goal "?p : (P & R) | (Q & R) --> (P | Q) & R";
by tac;
result();
writeln"Laws involving implication";
-goal thy "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)";
+Goal "?p : (P-->R) & (Q-->R) <-> (P|Q --> R)";
by tac;
result();
-goal thy "?p : (P & Q --> R) <-> (P--> (Q-->R))";
+Goal "?p : (P & Q --> R) <-> (P--> (Q-->R))";
by tac;
result();
-goal thy "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
+Goal "?p : ((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
by tac;
result();
-goal thy "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
+Goal "?p : ~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
by tac;
result();
-goal thy "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)";
+Goal "?p : (P --> Q & R) <-> (P-->Q) & (P-->R)";
by tac;
result();
@@ -78,22 +78,22 @@
writeln"Propositions-as-types";
(*The combinator K*)
-goal thy "?p : P --> (Q --> P)";
+Goal "?p : P --> (Q --> P)";
by tac;
result();
(*The combinator S*)
-goal thy "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)";
+Goal "?p : (P-->Q-->R) --> (P-->Q) --> (P-->R)";
by tac;
result();
(*Converse is classical*)
-goal thy "?p : (P-->Q) | (P-->R) --> (P --> Q | R)";
+Goal "?p : (P-->Q) | (P-->R) --> (P --> Q | R)";
by tac;
result();
-goal thy "?p : (P-->Q) --> (~Q --> ~P)";
+Goal "?p : (P-->Q) --> (~Q --> ~P)";
by tac;
result();
@@ -101,39 +101,39 @@
writeln"Schwichtenberg's examples (via T. Nipkow)";
(* stab-imp *)
-goal thy "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
+Goal "?p : (((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
by tac;
result();
(* stab-to-peirce *)
-goal thy "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
+Goal "?p : (((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
\ --> ((P --> Q) --> P) --> P";
by tac;
result();
(* peirce-imp1 *)
-goal thy "?p : (((Q --> R) --> Q) --> Q) \
+Goal "?p : (((Q --> R) --> Q) --> Q) \
\ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
by tac;
result();
(* peirce-imp2 *)
-goal thy "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
+Goal "?p : (((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
by tac;
result();
(* mints *)
-goal thy "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q";
+Goal "?p : ((((P --> Q) --> P) --> P) --> Q) --> Q";
by tac;
result();
(* mints-solovev *)
-goal thy "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
+Goal "?p : (P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
by tac;
result();
(* tatsuta *)
-goal thy "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \
+Goal "?p : (((P7 --> P1) --> P10) --> P4 --> P5) \
\ --> (((P8 --> P2) --> P9) --> P3 --> P10) \
\ --> (P1 --> P8) --> P6 --> P7 \
\ --> (((P3 --> P2) --> P9) --> P4) \
@@ -142,7 +142,7 @@
result();
(* tatsuta1 *)
-goal thy "?p : (((P8 --> P2) --> P9) --> P3 --> P10) \
+Goal "?p : (((P8 --> P2) --> P9) --> P3 --> P10) \
\ --> (((P3 --> P2) --> P9) --> P4) \
\ --> (((P6 --> P1) --> P2) --> P9) \
\ --> (((P7 --> P1) --> P10) --> P4 --> P5) \
--- a/src/FOLP/ex/quant.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/FOLP/ex/quant.ML Mon Jun 22 15:09:59 1998 +0200
@@ -9,73 +9,73 @@
writeln"File FOLP/ex/quant.ML";
-goal thy "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
+Goal "?p : (ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
by tac;
result();
-goal thy "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
+Goal "?p : (EX x y. P(x,y)) --> (EX y x. P(x,y))";
by tac;
result();
(*Converse is false*)
-goal thy "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
+Goal "?p : (ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
by tac;
result();
-goal thy "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
+Goal "?p : (ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
by tac;
result();
-goal thy "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
+Goal "?p : (ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
by tac;
result();
writeln"Some harder ones";
-goal thy "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
+Goal "?p : (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
by tac;
result();
(*6 secs*)
(*Converse is false*)
-goal thy "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
+Goal "?p : (EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
by tac;
result();
writeln"Basic test of quantifier reasoning";
(*TRUE*)
-goal thy "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
+Goal "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
by tac;
result();
-goal thy "?p : (ALL x. Q(x)) --> (EX x. Q(x))";
+Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))";
by tac;
result();
writeln"The following should fail, as they are false!";
-goal thy "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
+Goal "?p : (ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
by tac handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
-goal thy "?p : (EX x. Q(x)) --> (ALL x. Q(x))";
+Goal "?p : (EX x. Q(x)) --> (ALL x. Q(x))";
by tac handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal thy "?p : P(?a) --> (ALL x. P(x))";
+Goal "?p : P(?a) --> (ALL x. P(x))";
by tac handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
-goal thy
+Goal
"?p : (P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))";
by tac handle ERROR => writeln"Failed, as expected";
getgoal 1;
@@ -83,23 +83,23 @@
writeln"Back to things that are provable...";
-goal thy "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
+Goal "?p : (ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
by tac;
result();
(*An example of why exI should be delayed as long as possible*)
-goal thy "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
+Goal "?p : (P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
by tac;
result();
-goal thy "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
+Goal "?p : (ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
by tac;
(*Verify that no subgoals remain.*)
uresult();
-goal thy "?p : (ALL x. Q(x)) --> (EX x. Q(x))";
+Goal "?p : (ALL x. Q(x)) --> (EX x. Q(x))";
by tac;
result();
@@ -108,19 +108,19 @@
(*Principia Mathematica *11.53 *)
-goal thy "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
+Goal "?p : (ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
by tac;
result();
(*6 secs*)
(*Principia Mathematica *11.55 *)
-goal thy "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
+Goal "?p : (EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
by tac;
result();
(*9 secs*)
(*Principia Mathematica *11.61 *)
-goal thy "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
+Goal "?p : (EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
by tac;
result();
(*3 secs*)
--- a/src/LCF/ex/Ex1.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/LCF/ex/Ex1.ML Mon Jun 22 15:09:59 1998 +0200
@@ -15,7 +15,7 @@
bind_thm ("H_strict", H_strict);
Addsimps [H_strict];
-goal thy "ALL x. H(FIX(K,x)) = FIX(K,x)";
+Goal "ALL x. H(FIX(K,x)) = FIX(K,x)";
by (induct_tac "K" 1);
by (Simp_tac 1);
by (simp_tac (simpset() setloop (split_tac [COND_cases_iff])) 1);
--- a/src/LCF/ex/Ex2.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/LCF/ex/Ex2.ML Mon Jun 22 15:09:59 1998 +0200
@@ -3,7 +3,7 @@
Addsimps [F_strict,K];
-goal thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
+Goal "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
by (stac H 1);
by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
by (Simp_tac 1);
--- a/src/LCF/ex/Ex3.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/LCF/ex/Ex3.ML Mon Jun 22 15:09:59 1998 +0200
@@ -3,7 +3,7 @@
Addsimps [p_strict,p_s];
-goal thy "p(FIX(s),y) = FIX(s)";
+Goal "p(FIX(s),y) = FIX(s)";
by (induct_tac "s" 1);
by (Simp_tac 1);
by (Simp_tac 1);
--- a/src/Sequents/ex/ILL/washing.ML Sat Jun 20 20:35:38 1998 +0200
+++ b/src/Sequents/ex/ILL/washing.ML Mon Jun 22 15:09:59 1998 +0200
@@ -12,7 +12,7 @@
(* a load of dirty clothes and two dollars gives you clean clothes *)
-goal thy "dollar , dollar , dirty |- clean";
+Goal "dollar , dollar , dirty |- clean";
by (best_tac (lazy_cs add_safes (changeI @ load1I @ washI @ dryI)) 1);