--- a/src/FOLP/ex/foundn.ML Sat Sep 17 20:49:14 2005 +0200
+++ b/src/FOLP/ex/foundn.ML Sun Sep 18 14:25:48 2005 +0200
@@ -6,9 +6,7 @@
Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover
*)
-writeln"File FOLP/ex/foundn.ML";
-
-goal IFOLP.thy "?p : A&B --> (C-->A&C)";
+goal (theory "IFOLP") "?p : A&B --> (C-->A&C)";
by (rtac impI 1);
by (rtac impI 1);
by (rtac conjI 1);
@@ -19,7 +17,7 @@
(*A form of conj-elimination*)
val prems =
-goal IFOLP.thy "p : A&B ==> (!!x y.[| x:A; y:B |] ==> f(x,y):C) ==> ?p:C";
+goal (theory "IFOLP") "p : A&B ==> (!!x y.[| x:A; y:B |] ==> f(x,y):C) ==> ?p:C";
by (resolve_tac prems 1);
by (rtac conjunct1 1);
by (resolve_tac prems 1);
@@ -29,7 +27,7 @@
val prems =
-goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
+goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
by (rtac notI 1);
by (res_inst_tac [ ("P", "~B") ] notE 1);
@@ -47,7 +45,7 @@
val prems =
-goal IFOLP.thy "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
+goal (theory "IFOLP") "(!!A x. x:~ ~A ==> cla(x):A) ==> ?p:B | ~B";
by (resolve_tac prems 1);
by (rtac notI 1);
by (rtac notE 1);
@@ -61,7 +59,7 @@
val prems =
-goal IFOLP.thy "[| p:A | ~A; q:~ ~A |] ==> ?p:A";
+goal (theory "IFOLP") "[| p:A | ~A; q:~ ~A |] ==> ?p:A";
by (rtac disjE 1);
by (resolve_tac prems 1);
by (assume_tac 1);
@@ -75,7 +73,7 @@
writeln"Examples with quantifiers";
val prems =
-goal IFOLP.thy "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
+goal (theory "IFOLP") "p : ALL z. G(z) ==> ?p:ALL z. G(z)|H(z)";
by (rtac allI 1);
by (rtac disjI1 1);
by (resolve_tac (prems RL [spec]) 1);
@@ -84,14 +82,14 @@
result();
-goal IFOLP.thy "?p : ALL x. EX y. x=y";
+goal (theory "IFOLP") "?p : ALL x. EX y. x=y";
by (rtac allI 1);
by (rtac exI 1);
by (rtac refl 1);
result();
-goal IFOLP.thy "?p : EX y. ALL x. x=y";
+goal (theory "IFOLP") "?p : EX y. ALL x. x=y";
by (rtac exI 1);
by (rtac allI 1);
by (rtac refl 1) handle ERROR => writeln"Failed, as expected";
@@ -99,7 +97,7 @@
(*Parallel lifting example. *)
-goal IFOLP.thy "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
+goal (theory "IFOLP") "?p : EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)";
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
by (resolve_tac [exI, allI] 1);
@@ -108,7 +106,7 @@
val prems =
-goal IFOLP.thy "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
+goal (theory "IFOLP") "p : (EX z. F(z)) & B ==> ?p:(EX z. F(z) & B)";
by (rtac conjE 1);
by (resolve_tac prems 1);
by (rtac exE 1);
@@ -121,7 +119,7 @@
(*A bigger demonstration of quantifiers -- not in the paper*)
-goal IFOLP.thy "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
+goal (theory "IFOLP") "?p : (EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac exE 1 THEN assume_tac 1);
@@ -129,6 +127,3 @@
by (rtac allE 1 THEN assume_tac 1);
by (assume_tac 1);
result();
-
-
-writeln"Reached end of file.";