src/FOLP/ex/intro.ML
 author clasohm Thu, 16 Sep 1993 12:20:38 +0200 changeset 0 a5a9c433f639 child 1446 a8387e934fa7 permissions -rw-r--r--
Initial revision
```
(*  Title: 	FOL/ex/intro
ID:         \$Id\$
Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory

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 FOLP.thy "?p: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 FOLP.thy "?p:(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 FOLP.thy "?p:(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 FOLP.thy "?p:(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 FOLP_cs 1);
result();

goal FOLP.thy "?p:ALL x. P(x,f(x)) <-> \
\       (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))";
by (fast_tac FOLP_cs 1);
result();

(**** Derivation of conjunction elimination rule ****)

val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p: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 FOLP.thy "(!!x.x:P ==> f(x):False) ==> ?p:~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 FOLP.thy "[| p:~P;  q: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 FOLP.thy [not_def]
"[| p:~P;  q:P |] ==> ?p:R";
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
result();

writeln"Reached end of file.";
```