1 (* Title: FOL/ex/intro |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
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 |
|
15 context FOL.thy; |
|
16 |
|
17 (**** Some simple backward proofs ****) |
|
18 |
|
19 Goal "P|P --> P"; |
|
20 by (rtac impI 1); |
|
21 by (rtac disjE 1); |
|
22 by (assume_tac 3); |
|
23 by (assume_tac 2); |
|
24 by (assume_tac 1); |
|
25 qed "mythm"; |
|
26 |
|
27 Goal "(P & Q) | R --> (P | R)"; |
|
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); |
|
33 by (REPEAT (assume_tac 1)); |
|
34 result(); |
|
35 |
|
36 (*Correct version, delaying use of "spec" until last*) |
|
37 Goal "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"; |
|
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); |
|
43 by (assume_tac 1); |
|
44 result(); |
|
45 |
|
46 |
|
47 (**** Demonstration of Fast_tac ****) |
|
48 |
|
49 Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ |
|
50 \ --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; |
|
51 by (Fast_tac 1); |
|
52 result(); |
|
53 |
|
54 Goal "ALL x. P(x,f(x)) <-> \ |
|
55 \ (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; |
|
56 by (Fast_tac 1); |
|
57 result(); |
|
58 |
|
59 |
|
60 (**** Derivation of conjunction elimination rule ****) |
|
61 |
|
62 val [major,minor] = Goal "[| P&Q; [| P; Q |] ==> R |] ==> R"; |
|
63 by (rtac minor 1); |
|
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 |
|
74 val prems = Goal "(P ==> False) ==> ~P"; |
|
75 by (rewtac not_def); |
|
76 by (rtac impI 1); |
|
77 by (resolve_tac prems 1); |
|
78 by (assume_tac 1); |
|
79 result(); |
|
80 |
|
81 val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R"; |
|
82 by (rtac FalseE 1); |
|
83 by (rtac mp 1); |
|
84 by (resolve_tac [rewrite_rule [not_def] major] 1); |
|
85 by (rtac minor 1); |
|
86 result(); |
|
87 |
|
88 (*Alternative proof of the result above*) |
|
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."; |
|