src/FOLP/ex/intro.ML
 author haftmann Tue, 10 Jul 2007 17:30:50 +0200 changeset 23709 fd31da8f752a parent 17480 fd19f77dcf60 permissions -rw-r--r--
moved lfp_induct2 here
```
(*  Title:      FOLP/ex/intro.ML
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 (theory "FOLP") "?p:P|P --> P";
by (rtac impI 1);
by (rtac disjE 1);
by (assume_tac 3);
by (assume_tac 2);
by (assume_tac 1);
val mythm = result();

goal (theory "FOLP") "?p:(P & Q) | R  --> (P | R)";
by (rtac impI 1);
by (etac disjE 1);
by (dtac conjunct1 1);
by (rtac disjI1 1);
by (rtac disjI2 2);
by (REPEAT (assume_tac 1));
result();

(*Correct version, delaying use of "spec" until last*)
goal (theory "FOLP") "?p:(ALL x y. P(x,y))  -->  (ALL z w. P(w,z))";
by (rtac impI 1);
by (rtac allI 1);
by (rtac allI 1);
by (dtac spec 1);
by (dtac spec 1);
by (assume_tac 1);
result();

(**** Demonstration of fast_tac ****)

goal (theory "FOLP") "?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 (theory "FOLP") "?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 (theory "FOLP") "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R";
by (rtac 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 (theory "FOLP") "(!!x. x:P ==> f(x):False) ==> ?p:~P";
by (rewtac not_def);
by (rtac impI 1);
by (resolve_tac prems 1);
by (assume_tac 1);
result();

val [major,minor] = goal (theory "FOLP") "[| p:~P;  q:P |] ==> ?p:R";
by (rtac FalseE 1);
by (rtac mp 1);
by (resolve_tac [rewrite_rule [not_def] major] 1);
by (rtac minor 1);
result();

(*Alternative proof of above result*)
val [major,minor] = goalw (theory "FOLP") [not_def]
"[| p:~P;  q:P |] ==> ?p:R";
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1);
result();
```