author | wenzelm |
Tue, 13 Sep 2005 22:19:23 +0200 | |
changeset 17339 | ab97ccef124a |
parent 15661 | 9ef583b08647 |
permissions | -rw-r--r-- |
1459 | 1 |
(* Title: FOL/ex/intro |
0 | 2 |
ID: $Id$ |
1459 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
6 |
Examples for the manual "Introduction to Isabelle" |
|
7 |
||
8 |
Derives some inference rules, illustrating the use of definitions |
|
9 |
||
10 |
To generate similar output to manual, execute these commands: |
|
11 |
Pretty.setmargin 72; print_depth 0; |
|
12 |
*) |
|
13 |
||
14 |
||
5204 | 15 |
context FOL.thy; |
16 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
17 |
(**** Some simple backward proofs ****) |
0 | 18 |
|
5204 | 19 |
Goal "P|P --> P"; |
1459 | 20 |
by (rtac impI 1); |
21 |
by (rtac disjE 1); |
|
0 | 22 |
by (assume_tac 3); |
23 |
by (assume_tac 2); |
|
24 |
by (assume_tac 1); |
|
755 | 25 |
qed "mythm"; |
0 | 26 |
|
5204 | 27 |
Goal "(P & Q) | R --> (P | R)"; |
1459 | 28 |
by (rtac impI 1); |
29 |
by (etac disjE 1); |
|
30 |
by (dtac conjunct1 1); |
|
31 |
by (rtac disjI1 1); |
|
32 |
by (rtac disjI2 2); |
|
0 | 33 |
by (REPEAT (assume_tac 1)); |
34 |
result(); |
|
35 |
||
36 |
(*Correct version, delaying use of "spec" until last*) |
|
5204 | 37 |
Goal "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"; |
1459 | 38 |
by (rtac impI 1); |
39 |
by (rtac allI 1); |
|
40 |
by (rtac allI 1); |
|
41 |
by (dtac spec 1); |
|
42 |
by (dtac spec 1); |
|
0 | 43 |
by (assume_tac 1); |
44 |
result(); |
|
45 |
||
46 |
||
2469 | 47 |
(**** Demonstration of Fast_tac ****) |
0 | 48 |
|
5204 | 49 |
Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ |
0 | 50 |
\ --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; |
2469 | 51 |
by (Fast_tac 1); |
0 | 52 |
result(); |
53 |
||
5204 | 54 |
Goal "ALL x. P(x,f(x)) <-> \ |
0 | 55 |
\ (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; |
2469 | 56 |
by (Fast_tac 1); |
0 | 57 |
result(); |
58 |
||
59 |
||
60 |
(**** Derivation of conjunction elimination rule ****) |
|
61 |
||
5204 | 62 |
val [major,minor] = Goal "[| P&Q; [| P; Q |] ==> R |] ==> R"; |
1459 | 63 |
by (rtac minor 1); |
0 | 64 |
by (resolve_tac [major RS conjunct1] 1); |
65 |
by (resolve_tac [major RS conjunct2] 1); |
|
66 |
prth (topthm()); |
|
67 |
result(); |
|
68 |
||
69 |
||
70 |
(**** Derived rules involving definitions ****) |
|
71 |
||
72 |
(** Derivation of negation introduction **) |
|
73 |
||
5204 | 74 |
val prems = Goal "(P ==> False) ==> ~P"; |
1459 | 75 |
by (rewtac not_def); |
76 |
by (rtac impI 1); |
|
0 | 77 |
by (resolve_tac prems 1); |
78 |
by (assume_tac 1); |
|
79 |
result(); |
|
80 |
||
81 |
val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R"; |
|
1459 | 82 |
by (rtac FalseE 1); |
83 |
by (rtac mp 1); |
|
0 | 84 |
by (resolve_tac [rewrite_rule [not_def] major] 1); |
1459 | 85 |
by (rtac minor 1); |
0 | 86 |
result(); |
87 |
||
5204 | 88 |
(*Alternative proof of the result above*) |
0 | 89 |
val [major,minor] = goalw FOL.thy [not_def] |
90 |
"[| ~P; P |] ==> R"; |
|
91 |
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1); |
|
92 |
result(); |
|
93 |
||
94 |
writeln"Reached end of file."; |