1 (* Title: FOL/ex/foundn.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Intuitionistic FOL: Examples from The Foundation of a Generic Theorem Prover |
|
7 *) |
|
8 |
|
9 goal IFOL.thy "A&B --> (C-->A&C)"; |
|
10 by (rtac impI 1); |
|
11 by (rtac impI 1); |
|
12 by (rtac conjI 1); |
|
13 by (assume_tac 2); |
|
14 by (rtac conjunct1 1); |
|
15 by (assume_tac 1); |
|
16 result(); |
|
17 |
|
18 (*A form of conj-elimination*) |
|
19 val prems = |
|
20 goal IFOL.thy "A&B ==> ([| A; B |] ==> C) ==> C"; |
|
21 by (resolve_tac prems 1); |
|
22 by (rtac conjunct1 1); |
|
23 by (resolve_tac prems 1); |
|
24 by (rtac conjunct2 1); |
|
25 by (resolve_tac prems 1); |
|
26 result(); |
|
27 |
|
28 |
|
29 val prems = |
|
30 goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B"; |
|
31 by (resolve_tac prems 1); |
|
32 by (rtac notI 1); |
|
33 by (res_inst_tac [ ("P", "~B") ] notE 1); |
|
34 by (rtac notI 2); |
|
35 by (res_inst_tac [ ("P", "B | ~B") ] notE 2); |
|
36 by (assume_tac 2); |
|
37 by (rtac disjI1 2); |
|
38 by (assume_tac 2); |
|
39 by (rtac notI 1); |
|
40 by (res_inst_tac [ ("P", "B | ~B") ] notE 1); |
|
41 by (assume_tac 1); |
|
42 by (rtac disjI2 1); |
|
43 by (assume_tac 1); |
|
44 result(); |
|
45 |
|
46 |
|
47 val prems = |
|
48 goal IFOL.thy "(!!A. ~ ~A ==> A) ==> B | ~B"; |
|
49 by (resolve_tac prems 1); |
|
50 by (rtac notI 1); |
|
51 by (rtac notE 1); |
|
52 by (rtac notI 2); |
|
53 by (etac notE 2); |
|
54 by (etac disjI1 2); |
|
55 by (rtac notI 1); |
|
56 by (etac notE 1); |
|
57 by (etac disjI2 1); |
|
58 result(); |
|
59 |
|
60 |
|
61 val prems = |
|
62 goal IFOL.thy "[| A | ~A; ~ ~A |] ==> A"; |
|
63 by (rtac disjE 1); |
|
64 by (resolve_tac prems 1); |
|
65 by (assume_tac 1); |
|
66 by (rtac FalseE 1); |
|
67 by (res_inst_tac [ ("P", "~A") ] notE 1); |
|
68 by (resolve_tac prems 1); |
|
69 by (assume_tac 1); |
|
70 result(); |
|
71 |
|
72 |
|
73 writeln"Examples with quantifiers"; |
|
74 |
|
75 val prems = |
|
76 goal IFOL.thy "ALL z. G(z) ==> ALL z. G(z)|H(z)"; |
|
77 by (rtac allI 1); |
|
78 by (rtac disjI1 1); |
|
79 by (resolve_tac (prems RL [spec]) 1); |
|
80 (*can use instead |
|
81 by (rtac spec 1); by (resolve_tac prems 1); *) |
|
82 result(); |
|
83 |
|
84 |
|
85 goal IFOL.thy "ALL x. EX y. x=y"; |
|
86 by (rtac allI 1); |
|
87 by (rtac exI 1); |
|
88 by (rtac refl 1); |
|
89 result(); |
|
90 |
|
91 |
|
92 goal IFOL.thy "EX y. ALL x. x=y"; |
|
93 by (rtac exI 1); |
|
94 by (rtac allI 1); |
|
95 by (rtac refl 1) handle ERROR _ => writeln"Failed, as expected"; |
|
96 getgoal 1; |
|
97 |
|
98 |
|
99 (*Parallel lifting example. *) |
|
100 goal IFOL.thy "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"; |
|
101 by (resolve_tac [exI, allI] 1); |
|
102 by (resolve_tac [exI, allI] 1); |
|
103 by (resolve_tac [exI, allI] 1); |
|
104 by (resolve_tac [exI, allI] 1); |
|
105 by (resolve_tac [exI, allI] 1); |
|
106 |
|
107 |
|
108 val prems = |
|
109 goal IFOL.thy "(EX z. F(z)) & B ==> (EX z. F(z) & B)"; |
|
110 by (rtac conjE 1); |
|
111 by (resolve_tac prems 1); |
|
112 by (rtac exE 1); |
|
113 by (assume_tac 1); |
|
114 by (rtac exI 1); |
|
115 by (rtac conjI 1); |
|
116 by (assume_tac 1); |
|
117 by (assume_tac 1); |
|
118 result(); |
|
119 |
|
120 |
|
121 (*A bigger demonstration of quantifiers -- not in the paper*) |
|
122 goal IFOL.thy "(EX y. ALL x. Q(x,y)) --> (ALL x. EX y. Q(x,y))"; |
|
123 by (rtac impI 1); |
|
124 by (rtac allI 1); |
|
125 by (rtac exE 1 THEN assume_tac 1); |
|
126 by (rtac exI 1); |
|
127 by (rtac allE 1 THEN assume_tac 1); |
|
128 by (assume_tac 1); |
|
129 result(); |
|