--- a/src/FOL/ex/If.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/If.ML Thu Jun 18 18:28:45 1998 +0200
@@ -21,7 +21,7 @@
qed "ifE";
-goal If.thy
+Goal
"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 @@
qed "if_commute";
-goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
+Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))";
by (Blast_tac 1);
qed "nested_ifs";
@@ -47,7 +47,7 @@
(*An invalid formula. High-level rules permit a simpler diagnosis*)
-goal If.thy "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
+Goal "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))";
by (Blast_tac 1) handle ERROR => writeln"Failed, as expected";
(*Check that subgoals remain: proof failed.*)
getgoal 1;
--- a/src/FOL/ex/List.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/List.ML Thu Jun 18 18:28:45 1998 +0200
@@ -17,49 +17,49 @@
hd_eq, tl_eq, forall_nil, forall_cons, list_free,
len_nil, len_cons, at_0, at_succ];
-goal List.thy "~l=[] --> hd(l).tl(l) = l";
+Goal "~l=[] --> hd(l).tl(l) = l";
by (IND_TAC list_exh Simp_tac "l" 1);
result();
-goal List.thy "(l1++l2)++l3 = l1++(l2++l3)";
+Goal "(l1++l2)++l3 = l1++(l2++l3)";
by (IND_TAC list_ind Simp_tac "l1" 1);
qed "append_assoc";
-goal List.thy "l++[] = l";
+Goal "l++[] = l";
by (IND_TAC list_ind Simp_tac "l" 1);
qed "app_nil_right";
-goal List.thy "l1++l2=[] <-> l1=[] & l2=[]";
+Goal "l1++l2=[] <-> l1=[] & l2=[]";
by (IND_TAC list_exh Simp_tac "l1" 1);
qed "app_eq_nil_iff";
-goal List.thy "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
+Goal "forall(l++l',P) <-> forall(l,P) & forall(l',P)";
by (IND_TAC list_ind Simp_tac "l" 1);
qed "forall_app";
-goal List.thy "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
+Goal "forall(l,%x. P(x)&Q(x)) <-> forall(l,P) & forall(l,Q)";
by (IND_TAC list_ind Simp_tac "l" 1);
by (Fast_tac 1);
qed "forall_conj";
-goal List.thy "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
+Goal "~l=[] --> forall(l,P) <-> P(hd(l)) & forall(tl(l),P)";
by (IND_TAC list_ind Simp_tac "l" 1);
qed "forall_ne";
(*** Lists with natural numbers ***)
-goal List.thy "len(l1++l2) = len(l1)+len(l2)";
+Goal "len(l1++l2) = len(l1)+len(l2)";
by (IND_TAC list_ind Simp_tac "l1" 1);
qed "len_app";
-goal List.thy "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
+Goal "i<len(l1) --> at(l1++l2,i) = at(l1,i)";
by (IND_TAC list_ind Simp_tac "l1" 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
qed "at_app1";
-goal List.thy "at(l1++(x . l2), len(l1)) = x";
+Goal "at(l1++(x . l2), len(l1)) = x";
by (IND_TAC list_ind Simp_tac "l1" 1);
qed "at_app_hd2";
--- a/src/FOL/ex/Nat.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/Nat.ML Thu Jun 18 18:28:45 1998 +0200
@@ -11,7 +11,7 @@
open Nat;
-goal Nat.thy "Suc(k) ~= k";
+Goal "Suc(k) ~= k";
by (res_inst_tac [("n","k")] induct 1);
by (rtac notI 1);
by (etac Suc_neq_0 1);
@@ -21,7 +21,7 @@
qed "Suc_n_not_n";
-goal Nat.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
by (rtac induct 1);
back();
@@ -31,29 +31,29 @@
back();
back();
-goalw Nat.thy [add_def] "0+n = n";
+Goalw [add_def] "0+n = n";
by (rtac rec_0 1);
qed "add_0";
-goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)";
+Goalw [add_def] "Suc(m)+n = Suc(m+n)";
by (rtac rec_Suc 1);
qed "add_Suc";
Addsimps [add_0, add_Suc];
-goal Nat.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
by (res_inst_tac [("n","k")] induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "add_assoc";
-goal Nat.thy "m+0 = m";
+Goal "m+0 = m";
by (res_inst_tac [("n","m")] induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "add_0_right";
-goal Nat.thy "m+Suc(n) = Suc(m+n)";
+Goal "m+Suc(n) = Suc(m+n)";
by (res_inst_tac [("n","m")] induct 1);
by (ALLGOALS (Asm_simp_tac));
qed "add_Suc_right";
--- a/src/FOL/ex/Nat2.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/Nat2.ML Thu Jun 18 18:28:45 1998 +0200
@@ -21,91 +21,91 @@
by (REPEAT (resolve_tac (prems@[allI,impI]) 1));
qed "nat_exh";
-goal Nat2.thy "~ n=succ(n)";
+Goal "~ n=succ(n)";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "~ succ(n)=n";
+Goal "~ succ(n)=n";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "~ succ(succ(n))=n";
+Goal "~ succ(succ(n))=n";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "~ n=succ(succ(n))";
+Goal "~ n=succ(succ(n))";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "m+0 = m";
+Goal "m+0 = m";
by (IND_TAC nat_ind Simp_tac "m" 1);
qed "plus_0_right";
-goal Nat2.thy "m+succ(n) = succ(m+n)";
+Goal "m+succ(n) = succ(m+n)";
by (IND_TAC nat_ind Simp_tac "m" 1);
qed "plus_succ_right";
Addsimps [plus_0_right, plus_succ_right];
-goal Nat2.thy "~n=0 --> m+pred(n) = pred(m+n)";
+Goal "~n=0 --> m+pred(n) = pred(m+n)";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "~n=0 --> succ(pred(n))=n";
+Goal "~n=0 --> succ(pred(n))=n";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "m+n=0 <-> m=0 & n=0";
+Goal "m+n=0 <-> m=0 & n=0";
by (IND_TAC nat_ind Simp_tac "m" 1);
result();
-goal Nat2.thy "m <= n --> m <= succ(n)";
+Goal "m <= n --> m <= succ(n)";
by (IND_TAC nat_ind Simp_tac "m" 1);
by (rtac (impI RS allI) 1);
by (ALL_IND_TAC nat_ind Simp_tac 1);
by (Fast_tac 1);
bind_thm("le_imp_le_succ", result() RS mp);
-goal Nat2.thy "n<succ(n)";
+Goal "n<succ(n)";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "~ n<n";
+Goal "~ n<n";
by (IND_TAC nat_ind Simp_tac "n" 1);
result();
-goal Nat2.thy "m < n --> m < succ(n)";
+Goal "m < n --> m < succ(n)";
by (IND_TAC nat_ind Simp_tac "m" 1);
by (rtac (impI RS allI) 1);
by (ALL_IND_TAC nat_ind Simp_tac 1);
by (Fast_tac 1);
result();
-goal Nat2.thy "m <= n --> m <= n+k";
+Goal "m <= n --> m <= n+k";
by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_imp_le_succ]))
"k" 1);
qed "le_plus";
-goal Nat2.thy "succ(m) <= n --> m <= n";
+Goal "succ(m) <= n --> m <= n";
by (res_inst_tac [("x","n")]spec 1);
by (ALL_IND_TAC nat_exh (simp_tac (simpset() addsimps [le_imp_le_succ])) 1);
qed "succ_le";
-goal Nat2.thy "~m<n <-> n<=m";
+Goal "~m<n <-> n<=m";
by (IND_TAC nat_ind Simp_tac "n" 1);
by (rtac (impI RS allI) 1);
by (ALL_IND_TAC nat_ind Asm_simp_tac 1);
qed "not_less";
-goal Nat2.thy "n<=m --> ~m<n";
+Goal "n<=m --> ~m<n";
by (simp_tac (simpset() addsimps [not_less]) 1);
qed "le_imp_not_less";
-goal Nat2.thy "m<n --> ~n<=m";
+Goal "m<n --> ~n<=m";
by (cut_facts_tac [not_less] 1 THEN Fast_tac 1);
qed "not_le";
-goal Nat2.thy "m+k<=n --> m<=n";
+Goal "m+k<=n --> m<=n";
by (IND_TAC nat_ind (K all_tac) "k" 1);
by (Simp_tac 1);
by (rtac (impI RS allI) 1);
@@ -122,14 +122,14 @@
by (ALL_IND_TAC nat_exh Simp_tac 1);
qed "not0";
-goal Nat2.thy "a<=a' & b<=b' --> a+b<=a'+b'";
+Goal "a<=a' & b<=b' --> a+b<=a'+b'";
by (IND_TAC nat_ind (simp_tac (simpset() addsimps [le_plus])) "b" 1);
by (resolve_tac [impI RS allI] 1);
by (resolve_tac [allI RS allI] 1);
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
qed "plus_le_plus";
-goal Nat2.thy "i<=j --> j<=k --> i<=k";
+Goal "i<=j --> j<=k --> i<=k";
by (IND_TAC nat_ind (K all_tac) "i" 1);
by (Simp_tac 1);
by (resolve_tac [impI RS allI] 1);
@@ -139,7 +139,7 @@
by (Fast_tac 1);
qed "le_trans";
-goal Nat2.thy "i < j --> j <=k --> i < k";
+Goal "i < j --> j <=k --> i < k";
by (IND_TAC nat_ind (K all_tac) "j" 1);
by (Simp_tac 1);
by (resolve_tac [impI RS allI] 1);
@@ -149,13 +149,13 @@
by (Fast_tac 1);
qed "less_le_trans";
-goal Nat2.thy "succ(i) <= j <-> i < j";
+Goal "succ(i) <= j <-> i < j";
by (IND_TAC nat_ind Simp_tac "j" 1);
by (resolve_tac [impI RS allI] 1);
by (ALL_IND_TAC nat_exh Asm_simp_tac 1);
qed "succ_le2";
-goal Nat2.thy "i<succ(j) <-> i=j | i<j";
+Goal "i<succ(j) <-> i=j | i<j";
by (IND_TAC nat_ind Simp_tac "j" 1);
by (ALL_IND_TAC nat_exh Simp_tac 1);
by (resolve_tac [impI RS allI] 1);
--- a/src/FOL/ex/NatClass.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/NatClass.ML Thu Jun 18 18:28:45 1998 +0200
@@ -7,7 +7,7 @@
open NatClass;
-goal NatClass.thy "Suc(k) ~= (k::'a::nat)";
+Goal "Suc(k) ~= (k::'a::nat)";
by (res_inst_tac [("n","k")] induct 1);
by (rtac notI 1);
by (etac Suc_neq_0 1);
@@ -17,7 +17,7 @@
qed "Suc_n_not_n";
-goal NatClass.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
prths ([induct] RL [topthm()]); (*prints all 14 next states!*)
by (rtac induct 1);
back();
@@ -27,29 +27,29 @@
back();
back();
-goalw NatClass.thy [add_def] "0+n = n";
+Goalw [add_def] "0+n = n";
by (rtac rec_0 1);
qed "add_0";
-goalw NatClass.thy [add_def] "Suc(m)+n = Suc(m+n)";
+Goalw [add_def] "Suc(m)+n = Suc(m+n)";
by (rtac rec_Suc 1);
qed "add_Suc";
Addsimps [add_0, add_Suc];
-goal NatClass.thy "(k+m)+n = k+(m+n)";
+Goal "(k+m)+n = k+(m+n)";
by (res_inst_tac [("n","k")] induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "add_assoc";
-goal NatClass.thy "m+0 = m";
+Goal "m+0 = m";
by (res_inst_tac [("n","m")] induct 1);
by (Simp_tac 1);
by (Asm_simp_tac 1);
qed "add_0_right";
-goal NatClass.thy "m+Suc(n) = Suc(m+n)";
+Goal "m+Suc(n) = Suc(m+n)";
by (res_inst_tac [("n","m")] induct 1);
by (ALLGOALS (Asm_simp_tac));
qed "add_Suc_right";
--- a/src/FOL/ex/Prolog.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/Prolog.ML Thu Jun 18 18:28:45 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/FOL/ex/prop.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/prop.ML Thu Jun 18 18:28:45 1998 +0200
@@ -11,66 +11,66 @@
writeln"commutative laws of & and | ";
-goal thy "P & Q --> Q & P";
+Goal "P & Q --> Q & P";
by tac;
result();
-goal thy "P | Q --> Q | P";
+Goal "P | Q --> Q | P";
by tac;
result();
writeln"associative laws of & and | ";
-goal thy "(P & Q) & R --> P & (Q & R)";
+Goal "(P & Q) & R --> P & (Q & R)";
by tac;
result();
-goal thy "(P | Q) | R --> P | (Q | R)";
+Goal "(P | Q) | R --> P | (Q | R)";
by tac;
result();
writeln"distributive laws of & and | ";
-goal thy "(P & Q) | R --> (P | R) & (Q | R)";
+Goal "(P & Q) | R --> (P | R) & (Q | R)";
by tac;
result();
-goal thy "(P | R) & (Q | R) --> (P & Q) | R";
+Goal "(P | R) & (Q | R) --> (P & Q) | R";
by tac;
result();
-goal thy "(P | Q) & R --> (P & R) | (Q & R)";
+Goal "(P | Q) & R --> (P & R) | (Q & R)";
by tac;
result();
-goal thy "(P & R) | (Q & R) --> (P | Q) & R";
+Goal "(P & R) | (Q & R) --> (P | Q) & R";
by tac;
result();
writeln"Laws involving implication";
-goal thy "(P-->R) & (Q-->R) <-> (P|Q --> R)";
+Goal "(P-->R) & (Q-->R) <-> (P|Q --> R)";
by tac;
result();
-goal thy "(P & Q --> R) <-> (P--> (Q-->R))";
+Goal "(P & Q --> R) <-> (P--> (Q-->R))";
by tac;
result();
-goal thy "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
+Goal "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R";
by tac;
result();
-goal thy "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
+Goal "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)";
by tac;
result();
-goal thy "(P --> Q & R) <-> (P-->Q) & (P-->R)";
+Goal "(P --> Q & R) <-> (P-->Q) & (P-->R)";
by tac;
result();
@@ -78,22 +78,22 @@
writeln"Propositions-as-types";
(*The combinator K*)
-goal thy "P --> (Q --> P)";
+Goal "P --> (Q --> P)";
by tac;
result();
(*The combinator S*)
-goal thy "(P-->Q-->R) --> (P-->Q) --> (P-->R)";
+Goal "(P-->Q-->R) --> (P-->Q) --> (P-->R)";
by tac;
result();
(*Converse is classical*)
-goal thy "(P-->Q) | (P-->R) --> (P --> Q | R)";
+Goal "(P-->Q) | (P-->R) --> (P --> Q | R)";
by tac;
result();
-goal thy "(P-->Q) --> (~Q --> ~P)";
+Goal "(P-->Q) --> (~Q --> ~P)";
by tac;
result();
@@ -101,39 +101,39 @@
writeln"Schwichtenberg's examples (via T. Nipkow)";
(* stab-imp *)
-goal thy "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
+Goal "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q";
by tac;
result();
(* stab-to-peirce *)
-goal thy "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
+Goal "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q) \
\ --> ((P --> Q) --> P) --> P";
by tac;
result();
(* peirce-imp1 *)
-goal thy "(((Q --> R) --> Q) --> Q) \
+Goal "(((Q --> R) --> Q) --> Q) \
\ --> (((P --> Q) --> R) --> P --> Q) --> P --> Q";
by tac;
result();
(* peirce-imp2 *)
-goal thy "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
+Goal "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P";
by tac;
result();
(* mints *)
-goal thy "((((P --> Q) --> P) --> P) --> Q) --> Q";
+Goal "((((P --> Q) --> P) --> P) --> Q) --> Q";
by tac;
result();
(* mints-solovev *)
-goal thy "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
+Goal "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R";
by tac;
result();
(* tatsuta *)
-goal thy "(((P7 --> P1) --> P10) --> P4 --> P5) \
+Goal "(((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 "(((P8 --> P2) --> P9) --> P3 --> P10) \
+Goal "(((P8 --> P2) --> P9) --> P3 --> P10) \
\ --> (((P3 --> P2) --> P9) --> P4) \
\ --> (((P6 --> P1) --> P2) --> P9) \
\ --> (((P7 --> P1) --> P10) --> P4 --> P5) \
--- a/src/FOL/ex/quant.ML Thu Jun 18 11:22:45 1998 +0200
+++ b/src/FOL/ex/quant.ML Thu Jun 18 18:28:45 1998 +0200
@@ -9,73 +9,73 @@
writeln"File FOL/ex/quant.";
-goal thy "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
+Goal "(ALL x y. P(x,y)) --> (ALL y x. P(x,y))";
by tac;
result();
-goal thy "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
+Goal "(EX x y. P(x,y)) --> (EX y x. P(x,y))";
by tac;
result();
(*Converse is false*)
-goal thy "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
+Goal "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))";
by tac;
result();
-goal thy "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
+Goal "(ALL x. P-->Q(x)) <-> (P--> (ALL x. Q(x)))";
by tac;
result();
-goal thy "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
+Goal "(ALL x. P(x)-->Q) <-> ((EX x. P(x)) --> Q)";
by tac;
result();
writeln"Some harder ones";
-goal thy "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
+Goal "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))";
by tac;
result();
(*6 secs*)
(*Converse is false*)
-goal thy "(EX x. P(x)&Q(x)) --> (EX x. P(x)) & (EX x. Q(x))";
+Goal "(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 "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
+Goal "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
by tac;
result();
-goal thy "(ALL x. Q(x)) --> (EX x. Q(x))";
+Goal "(ALL x. Q(x)) --> (EX x. Q(x))";
by tac;
result();
writeln"The following should fail, as they are false!";
-goal thy "(ALL x. EX y. Q(x,y)) --> (EX y. ALL x. Q(x,y))";
+Goal "(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 "(EX x. Q(x)) --> (ALL x. Q(x))";
+Goal "(EX x. Q(x)) --> (ALL x. Q(x))";
by tac handle ERROR => writeln"Failed, as expected";
getgoal 1;
-goal thy "P(?a) --> (ALL x. P(x))";
+Goal "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(?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 "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))";
+Goal "(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 --> (EX x. Q(x))) & P --> (EX x. Q(x))";
+Goal "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))";
by tac;
result();
-goal thy "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)";
+Goal "(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 "(ALL x. Q(x)) --> (EX x. Q(x))";
+Goal "(ALL x. Q(x)) --> (EX x. Q(x))";
by tac;
result();
@@ -108,19 +108,19 @@
(*Principia Mathematica *11.53 *)
-goal thy "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))";
+Goal "(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 "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))";
+Goal "(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 "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
+Goal "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))";
by tac;
result();
(*3 secs*)