author | wenzelm |
Thu, 07 Apr 2005 09:25:33 +0200 | |
changeset 15661 | 9ef583b08647 |
parent 15531 | 08c8dad8e399 |
child 17480 | fd19f77dcf60 |
permissions | -rw-r--r-- |
1464 | 1 |
(* Title: FOLP/ex/intro.ML |
0 | 2 |
ID: $Id$ |
1446 | 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 |
||
15661
9ef583b08647
reverted renaming of Some/None in comments and strings;
wenzelm
parents:
15531
diff
changeset
|
15 |
(**** Some simple backward proofs ****) |
0 | 16 |
|
17 |
goal FOLP.thy "?p:P|P --> P"; |
|
1446 | 18 |
by (rtac impI 1); |
19 |
by (rtac disjE 1); |
|
0 | 20 |
by (assume_tac 3); |
21 |
by (assume_tac 2); |
|
22 |
by (assume_tac 1); |
|
23 |
val mythm = result(); |
|
24 |
||
25 |
goal FOLP.thy "?p:(P & Q) | R --> (P | R)"; |
|
1446 | 26 |
by (rtac impI 1); |
27 |
by (etac disjE 1); |
|
28 |
by (dtac conjunct1 1); |
|
29 |
by (rtac disjI1 1); |
|
30 |
by (rtac disjI2 2); |
|
0 | 31 |
by (REPEAT (assume_tac 1)); |
32 |
result(); |
|
33 |
||
34 |
(*Correct version, delaying use of "spec" until last*) |
|
3836 | 35 |
goal FOLP.thy "?p:(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"; |
1446 | 36 |
by (rtac impI 1); |
37 |
by (rtac allI 1); |
|
38 |
by (rtac allI 1); |
|
39 |
by (dtac spec 1); |
|
40 |
by (dtac spec 1); |
|
0 | 41 |
by (assume_tac 1); |
42 |
result(); |
|
43 |
||
44 |
||
45 |
(**** Demonstration of fast_tac ****) |
|
46 |
||
47 |
goal FOLP.thy "?p:(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 FOLP_cs 1); |
|
50 |
result(); |
|
51 |
||
52 |
goal FOLP.thy "?p: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 FOLP_cs 1); |
|
55 |
result(); |
|
56 |
||
57 |
||
58 |
(**** Derivation of conjunction elimination rule ****) |
|
59 |
||
60 |
val [major,minor] = goal FOLP.thy "[| p:P&Q; !!x y.[| x:P; y:Q |] ==>f(x,y):R |] ==> ?p:R"; |
|
1446 | 61 |
by (rtac minor 1); |
0 | 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 |
||
3836 | 72 |
val prems = goal FOLP.thy "(!!x. x:P ==> f(x):False) ==> ?p:~P"; |
1446 | 73 |
by (rewtac not_def); |
74 |
by (rtac impI 1); |
|
0 | 75 |
by (resolve_tac prems 1); |
76 |
by (assume_tac 1); |
|
77 |
result(); |
|
78 |
||
79 |
val [major,minor] = goal FOLP.thy "[| p:~P; q:P |] ==> ?p:R"; |
|
1446 | 80 |
by (rtac FalseE 1); |
81 |
by (rtac mp 1); |
|
0 | 82 |
by (resolve_tac [rewrite_rule [not_def] major] 1); |
1446 | 83 |
by (rtac minor 1); |
0 | 84 |
result(); |
85 |
||
86 |
(*Alternative proof of above result*) |
|
87 |
val [major,minor] = goalw FOLP.thy [not_def] |
|
88 |
"[| p:~P; q:P |] ==> ?p:R"; |
|
89 |
by (resolve_tac [minor RS (major RS mp RS FalseE)] 1); |
|
90 |
result(); |
|
91 |
||
92 |
writeln"Reached end of file."; |