|
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 (**** Some simple backward proofs ****) |
|
16 |
|
17 goal FOL.thy "P|P --> P"; |
|
18 by (resolve_tac [impI] 1); |
|
19 by (resolve_tac [disjE] 1); |
|
20 by (assume_tac 3); |
|
21 by (assume_tac 2); |
|
22 by (assume_tac 1); |
|
23 val mythm = result(); |
|
24 |
|
25 goal FOL.thy "(P & Q) | R --> (P | R)"; |
|
26 by (resolve_tac [impI] 1); |
|
27 by (eresolve_tac [disjE] 1); |
|
28 by (dresolve_tac [conjunct1] 1); |
|
29 by (resolve_tac [disjI1] 1); |
|
30 by (resolve_tac [disjI2] 2); |
|
31 by (REPEAT (assume_tac 1)); |
|
32 result(); |
|
33 |
|
34 (*Correct version, delaying use of "spec" until last*) |
|
35 goal FOL.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; |
|
36 by (resolve_tac [impI] 1); |
|
37 by (resolve_tac [allI] 1); |
|
38 by (resolve_tac [allI] 1); |
|
39 by (dresolve_tac [spec] 1); |
|
40 by (dresolve_tac [spec] 1); |
|
41 by (assume_tac 1); |
|
42 result(); |
|
43 |
|
44 |
|
45 (**** Demonstration of fast_tac ****) |
|
46 |
|
47 goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ |
|
48 \ --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; |
|
49 by (fast_tac FOL_cs 1); |
|
50 result(); |
|
51 |
|
52 goal FOL.thy "ALL x. P(x,f(x)) <-> \ |
|
53 \ (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; |
|
54 by (fast_tac FOL_cs 1); |
|
55 result(); |
|
56 |
|
57 |
|
58 (**** Derivation of conjunction elimination rule ****) |
|
59 |
|
60 val [major,minor] = goal FOL.thy "[| P&Q; [| P; Q |] ==> R |] ==> R"; |
|
61 by (resolve_tac [minor] 1); |
|
62 by (resolve_tac [major RS conjunct1] 1); |
|
63 by (resolve_tac [major RS conjunct2] 1); |
|
64 prth (topthm()); |
|
65 result(); |
|
66 |
|
67 |
|
68 (**** Derived rules involving definitions ****) |
|
69 |
|
70 (** Derivation of negation introduction **) |
|
71 |
|
72 val prems = goal FOL.thy "(P ==> False) ==> ~P"; |
|
73 by (rewrite_goals_tac [not_def]); |
|
74 by (resolve_tac [impI] 1); |
|
75 by (resolve_tac prems 1); |
|
76 by (assume_tac 1); |
|
77 result(); |
|
78 |
|
79 val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R"; |
|
80 by (resolve_tac [FalseE] 1); |
|
81 by (resolve_tac [mp] 1); |
|
82 by (resolve_tac [rewrite_rule [not_def] major] 1); |
|
83 by (resolve_tac [minor] 1); |
|
84 result(); |
|
85 |
|
86 (*Alternative proof of above result*) |
|
87 val [major,minor] = goalw FOL.thy [not_def] |
|
88 "[| ~P; P |] ==> R"; |
|
89 by (resolve_tac [minor RS (major RS mp RS FalseE)] 1); |
|
90 result(); |
|
91 |
|
92 writeln"Reached end of file."; |