|
1 (* Title: CTT/ex/elim |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1991 University of Cambridge |
|
5 |
|
6 Some examples taken from P. Martin-L\"of, Intuitionistic type theory |
|
7 (Bibliopolis, 1984). |
|
8 |
|
9 by (safe_tac prems 1); |
|
10 by (step_tac prems 1); |
|
11 by (pc_tac prems 1); |
|
12 *) |
|
13 |
|
14 writeln"Examples with elimination rules"; |
|
15 |
|
16 |
|
17 writeln"This finds the functions fst and snd!"; |
|
18 val prems = goal CTT.thy "A type ==> ?a : (A*A) --> A"; |
|
19 by (pc_tac prems 1 THEN fold_tac basic_defs); (*puts in fst and snd*) |
|
20 result(); |
|
21 writeln"first solution is fst; backtracking gives snd"; |
|
22 back(); |
|
23 back() handle ERROR => writeln"And there are indeed no others"; |
|
24 |
|
25 |
|
26 writeln"Double negation of the Excluded Middle"; |
|
27 val prems = goal CTT.thy "A type ==> ?a : ((A + (A-->F)) --> F) --> F"; |
|
28 by (intr_tac prems); |
|
29 by (rtac ProdE 1); |
|
30 by (assume_tac 1); |
|
31 by (pc_tac prems 1); |
|
32 result(); |
|
33 |
|
34 val prems = goal CTT.thy |
|
35 "[| A type; B type |] ==> ?a : (A*B) --> (B*A)"; |
|
36 by (pc_tac prems 1); |
|
37 result(); |
|
38 (*The sequent version (ITT) could produce an interesting alternative |
|
39 by backtracking. No longer.*) |
|
40 |
|
41 writeln"Binary sums and products"; |
|
42 val prems = goal CTT.thy |
|
43 "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"; |
|
44 by (pc_tac prems 1); |
|
45 result(); |
|
46 |
|
47 (*A distributive law*) |
|
48 val prems = goal CTT.thy |
|
49 "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)"; |
|
50 by (pc_tac prems 1); |
|
51 result(); |
|
52 |
|
53 (*more general version, same proof*) |
|
54 val prems = goal CTT.thy |
|
55 "[| A type; !!x. x:A ==> B(x) type; !!x. x:A ==> C(x) type|] ==> \ |
|
56 \ ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"; |
|
57 by (pc_tac prems 1); |
|
58 result(); |
|
59 |
|
60 writeln"Construction of the currying functional"; |
|
61 val prems = goal CTT.thy |
|
62 "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"; |
|
63 by (pc_tac prems 1); |
|
64 result(); |
|
65 |
|
66 (*more general goal with same proof*) |
|
67 val prems = goal CTT.thy |
|
68 "[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A. B(x)) ==> C(z) type|] \ |
|
69 \ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \ |
|
70 \ --> (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
|
71 by (pc_tac prems 1); |
|
72 result(); |
|
73 |
|
74 writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"; |
|
75 val prems = goal CTT.thy |
|
76 "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"; |
|
77 by (pc_tac prems 1); |
|
78 result(); |
|
79 |
|
80 (*more general goal with same proof*) |
|
81 val prems = goal CTT.thy |
|
82 "[| A type; !!x. x:A ==> B(x) type; !!z. z : (SUM x:A . B(x)) ==> C(z) type|] \ |
|
83 \ ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \ |
|
84 \ --> (PROD z : (SUM x:A . B(x)) . C(z))"; |
|
85 by (pc_tac prems 1); |
|
86 result(); |
|
87 |
|
88 writeln"Function application"; |
|
89 val prems = goal CTT.thy |
|
90 "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B"; |
|
91 by (pc_tac prems 1); |
|
92 result(); |
|
93 |
|
94 writeln"Basic test of quantifier reasoning"; |
|
95 val prems = goal CTT.thy |
|
96 "[| A type; B type; !!x y.[| x:A; y:B |] ==> C(x,y) type |] ==> \ |
|
97 \ ?a : (SUM y:B . PROD x:A . C(x,y)) \ |
|
98 \ --> (PROD x:A . SUM y:B . C(x,y))"; |
|
99 by (pc_tac prems 1); |
|
100 result(); |
|
101 |
|
102 (*faulty proof attempt, stripping the quantifiers in wrong sequence |
|
103 by (intr_tac[]); |
|
104 by (pc_tac prems 1); ...fails!! *) |
|
105 |
|
106 writeln"Martin-Lof (1984) pages 36-7: the combinator S"; |
|
107 val prems = goal CTT.thy |
|
108 "[| A type; !!x. x:A ==> B(x) type; \ |
|
109 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \ |
|
110 \ ==> ?a : (PROD x:A. PROD y:B(x). C(x,y)) \ |
|
111 \ --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
|
112 by (pc_tac prems 1); |
|
113 result(); |
|
114 |
|
115 writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination"; |
|
116 val prems = goal CTT.thy |
|
117 "[| A type; B type; !!z. z: A+B ==> C(z) type|] ==> \ |
|
118 \ ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) \ |
|
119 \ --> (PROD z: A+B. C(z))"; |
|
120 by (pc_tac prems 1); |
|
121 result(); |
|
122 |
|
123 (*towards AXIOM OF CHOICE*) |
|
124 val prems = goal CTT.thy |
|
125 "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"; |
|
126 by (pc_tac prems 1); |
|
127 by (fold_tac basic_defs); (*puts in fst and snd*) |
|
128 result(); |
|
129 |
|
130 (*Martin-Lof (1984) page 50*) |
|
131 writeln"AXIOM OF CHOICE!!! Delicate use of elimination rules"; |
|
132 val prems = goal CTT.thy |
|
133 "[| A type; !!x. x:A ==> B(x) type; \ |
|
134 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type|] \ |
|
135 \ ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ |
|
136 \ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
|
137 by (intr_tac prems); |
|
138 by (add_mp_tac 2); |
|
139 by (add_mp_tac 1); |
|
140 by (etac SumE_fst 1); |
|
141 by (rtac replace_type 1); |
|
142 by (rtac subst_eqtyparg 1); |
|
143 by (resolve_tac comp_rls 1); |
|
144 by (rtac SumE_snd 4); |
|
145 by (typechk_tac (SumE_fst::prems)); |
|
146 result(); |
|
147 |
|
148 writeln"Axiom of choice. Proof without fst, snd. Harder still!"; |
|
149 val prems = goal CTT.thy |
|
150 "[| A type; !!x.x:A ==> B(x) type; \ |
|
151 \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type|] \ |
|
152 \ ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \ |
|
153 \ --> (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
|
154 by (intr_tac prems); |
|
155 (*Must not use add_mp_tac as subst_prodE hides the construction.*) |
|
156 by (resolve_tac [ProdE RS SumE] 1 THEN assume_tac 1); |
|
157 by (TRYALL assume_tac); |
|
158 by (rtac replace_type 1); |
|
159 by (rtac subst_eqtyparg 1); |
|
160 by (resolve_tac comp_rls 1); |
|
161 by (etac (ProdE RS SumE) 4); |
|
162 by (typechk_tac prems); |
|
163 by (rtac replace_type 1); |
|
164 by (rtac subst_eqtyparg 1); |
|
165 by (resolve_tac comp_rls 1); |
|
166 by (typechk_tac prems); |
|
167 by (assume_tac 1); |
|
168 by (fold_tac basic_defs); (*puts in fst and snd*) |
|
169 result(); |
|
170 |
|
171 writeln"Example of sequent_style deduction"; |
|
172 (*When splitting z:A*B, the assumption C(z) is affected; ?a becomes |
|
173 lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w) *) |
|
174 val prems = goal CTT.thy |
|
175 "[| A type; B type; !!z. z:A*B ==> C(z) type |] ==> \ |
|
176 \ ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"; |
|
177 by (resolve_tac intr_rls 1); |
|
178 by (biresolve_tac safe_brls 2); |
|
179 (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *) |
|
180 by (res_inst_tac [ ("a","y") ] ProdE 2); |
|
181 by (typechk_tac prems); |
|
182 by (rtac SumE 1 THEN assume_tac 1); |
|
183 by (intr_tac[]); |
|
184 by (TRYALL assume_tac); |
|
185 by (typechk_tac prems); |
|
186 result(); |
|
187 |
|
188 writeln"Reached end of file."; |