diff -r 000000000000 -r a5a9c433f639 src/FOL/ex/intro.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/FOL/ex/intro.ML	Thu Sep 16 12:20:38 1993 +0200
@@ -0,0 +1,92 @@
+(*  Title: 	FOL/ex/intro
+    ID:         $Id$
+    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Copyright   1992  University of Cambridge
+
+Examples for the manual "Introduction to Isabelle"
+
+Derives some inference rules, illustrating the use of definitions
+
+To generate similar output to manual, execute these commands:
+    Pretty.setmargin 72; print_depth 0;
+*)
+
+
+(**** Some simple backward proofs ****)
+
+goal FOL.thy "P|P --> P";
+by (resolve_tac [impI] 1);
+by (resolve_tac [disjE] 1);
+by (assume_tac 3);
+by (assume_tac 2);
+by (assume_tac 1);
+val mythm = result();
+
+goal FOL.thy "(P & Q) | R  --> (P | R)";
+by (resolve_tac [impI] 1);
+by (eresolve_tac [disjE] 1);
+by (dresolve_tac [conjunct1] 1);
+by (resolve_tac [disjI1] 1);
+by (resolve_tac [disjI2] 2);
+by (REPEAT (assume_tac 1));
+result();
+
+(*Correct version, delaying use of "spec" until last*)
+goal FOL.thy "(ALL x y.P(x,y))  -->  (ALL z w.P(w,z))";
+by (resolve_tac [impI] 1);
+by (resolve_tac [allI] 1);
+by (resolve_tac [allI] 1);
+by (dresolve_tac [spec] 1);
+by (dresolve_tac [spec] 1);
+by (assume_tac 1);
+result();
+
+
+(**** Demonstration of fast_tac ****)
+
+goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x))  \
+\       -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))";
+by (fast_tac FOL_cs 1);
+result();
+
+goal FOL.thy "ALL x. P(x,f(x)) <-> \
+\       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
+by (fast_tac FOL_cs 1);
+result();
+
+
+(**** Derivation of conjunction elimination rule ****)
+
+val [major,minor] = goal FOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R";
+by (resolve_tac [minor] 1);
+by (resolve_tac [major RS conjunct1] 1);
+by (resolve_tac [major RS conjunct2] 1);
+prth (topthm());
+result();
+
+
+(**** Derived rules involving definitions ****)
+
+(** Derivation of negation introduction **)
+
+val prems = goal FOL.thy "(P ==> False) ==> ~P";
+by (rewrite_goals_tac [not_def]);
+by (resolve_tac [impI] 1);
+by (resolve_tac prems 1);
+by (assume_tac 1);
+result();
+
+val [major,minor] = goal FOL.thy "[| ~P;  P |] ==> R";
+by (resolve_tac [FalseE] 1);
+by (resolve_tac [mp] 1);
+by (resolve_tac [rewrite_rule [not_def] major] 1);
+by (resolve_tac [minor] 1);
+result();
+
+(*Alternative proof of above result*)
+val [major,minor] = goalw FOL.thy [not_def]
+    "[| ~P;  P |] ==> R";
+by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
+result();
+
+writeln"Reached end of file.";