author | skalberg |
Sun, 13 Feb 2005 17:15:14 +0100 | |
changeset 15531 | 08c8dad8e399 |
parent 9251 | bd57acd44fc1 |
child 15661 | 9ef583b08647 |
permissions | -rw-r--r-- |
1446 | 1 |
(* Title: CTT/ex/elim |
0 | 2 |
ID: $Id$ |
1446 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1991 University of Cambridge |
5 |
||
15531 | 6 |
SOME examples taken from P. Martin-L\"of, Intuitionistic type theory |
1446 | 7 |
(Bibliopolis, 1984). |
0 | 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!"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
18 |
Goal "A type ==> ?a : (A*A) --> A"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
19 |
by (pc_tac [] 1 THEN fold_tac basic_defs); (*puts in fst and snd*) |
0 | 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"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
27 |
Goal "A type ==> ?a : ((A + (A-->F)) --> F) --> F"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
28 |
by (intr_tac []); |
0 | 29 |
by (rtac ProdE 1); |
30 |
by (assume_tac 1); |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
31 |
by (pc_tac [] 1); |
0 | 32 |
result(); |
33 |
||
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
34 |
Goal "[| A type; B type |] ==> ?a : (A*B) --> (B*A)"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
35 |
by (pc_tac [] 1); |
0 | 36 |
result(); |
37 |
(*The sequent version (ITT) could produce an interesting alternative |
|
38 |
by backtracking. No longer.*) |
|
39 |
||
40 |
writeln"Binary sums and products"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
41 |
Goal "[| A type; B type; C type |] ==> ?a : (A+B --> C) --> (A-->C) * (B-->C)"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
42 |
by (pc_tac [] 1); |
0 | 43 |
result(); |
44 |
||
45 |
(*A distributive law*) |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
46 |
Goal "[| A type; B type; C type |] ==> ?a : A * (B+C) --> (A*B + A*C)"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
47 |
by (pc_tac [] 1); |
0 | 48 |
result(); |
49 |
||
50 |
(*more general version, same proof*) |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
51 |
val prems = Goal |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
52 |
"[| A type; !!x. x:A ==> B(x) type; !!x. x:A ==> C(x) type|] ==> \ |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
53 |
\ ?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"; |
0 | 54 |
by (pc_tac prems 1); |
55 |
result(); |
|
56 |
||
57 |
writeln"Construction of the currying functional"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
58 |
Goal "[| A type; B type; C type |] ==> ?a : (A*B --> C) --> (A--> (B-->C))"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
59 |
by (pc_tac [] 1); |
0 | 60 |
result(); |
61 |
||
62 |
(*more general goal with same proof*) |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
63 |
val prems = Goal |
1446 | 64 |
"[| A type; !!x. x:A ==> B(x) type; \ |
65 |
\ !!z. z: (SUM x:A. B(x)) ==> C(z) type \ |
|
66 |
\ |] ==> ?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). \ |
|
281
f1f96b9e6285
CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD
lcp
parents:
0
diff
changeset
|
67 |
\ (PROD x:A . PROD y:B(x) . C(<x,y>))"; |
0 | 68 |
by (pc_tac prems 1); |
69 |
result(); |
|
70 |
||
71 |
writeln"Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
72 |
Goal "[| A type; B type; C type |] ==> ?a : (A --> (B-->C)) --> (A*B --> C)"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
73 |
by (pc_tac [] 1); |
0 | 74 |
result(); |
75 |
||
76 |
(*more general goal with same proof*) |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
77 |
val prems = Goal |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
78 |
"[| A type; !!x. x:A ==> B(x) type; !!z. z: (SUM x:A . B(x)) ==> C(z) type|] \ |
0 | 79 |
\ ==> ?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) \ |
80 |
\ --> (PROD z : (SUM x:A . B(x)) . C(z))"; |
|
81 |
by (pc_tac prems 1); |
|
82 |
result(); |
|
83 |
||
84 |
writeln"Function application"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
85 |
Goal "[| A type; B type |] ==> ?a : ((A --> B) * A) --> B"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
86 |
by (pc_tac [] 1); |
0 | 87 |
result(); |
88 |
||
89 |
writeln"Basic test of quantifier reasoning"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
90 |
val prems = Goal |
0 | 91 |
"[| A type; B type; !!x y.[| x:A; y:B |] ==> C(x,y) type |] ==> \ |
92 |
\ ?a : (SUM y:B . PROD x:A . C(x,y)) \ |
|
93 |
\ --> (PROD x:A . SUM y:B . C(x,y))"; |
|
94 |
by (pc_tac prems 1); |
|
95 |
result(); |
|
96 |
||
97 |
(*faulty proof attempt, stripping the quantifiers in wrong sequence |
|
98 |
by (intr_tac[]); |
|
99 |
by (pc_tac prems 1); ...fails!! *) |
|
100 |
||
101 |
writeln"Martin-Lof (1984) pages 36-7: the combinator S"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
102 |
val prems = Goal |
0 | 103 |
"[| A type; !!x. x:A ==> B(x) type; \ |
104 |
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type |] \ |
|
105 |
\ ==> ?a : (PROD x:A. PROD y:B(x). C(x,y)) \ |
|
106 |
\ --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
|
107 |
by (pc_tac prems 1); |
|
108 |
result(); |
|
109 |
||
110 |
writeln"Martin-Lof (1984) page 58: the axiom of disjunction elimination"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
111 |
val prems = Goal |
0 | 112 |
"[| A type; B type; !!z. z: A+B ==> C(z) type|] ==> \ |
113 |
\ ?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) \ |
|
114 |
\ --> (PROD z: A+B. C(z))"; |
|
115 |
by (pc_tac prems 1); |
|
116 |
result(); |
|
117 |
||
118 |
(*towards AXIOM OF CHOICE*) |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
119 |
Goal "[| A type; B type; C type |] ==> ?a : (A --> B*C) --> (A-->B) * (A-->C)"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
120 |
by (pc_tac [] 1); |
0 | 121 |
by (fold_tac basic_defs); (*puts in fst and snd*) |
122 |
result(); |
|
123 |
||
124 |
(*Martin-Lof (1984) page 50*) |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
125 |
writeln"AXIOM OF CHOICE! Delicate use of elimination rules"; |
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
126 |
val prems = Goal |
1446 | 127 |
"[| A type; !!x. x:A ==> B(x) type; \ |
128 |
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ |
|
129 |
\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ |
|
281
f1f96b9e6285
CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD
lcp
parents:
0
diff
changeset
|
130 |
\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
0 | 131 |
by (intr_tac prems); |
132 |
by (add_mp_tac 2); |
|
133 |
by (add_mp_tac 1); |
|
134 |
by (etac SumE_fst 1); |
|
135 |
by (rtac replace_type 1); |
|
136 |
by (rtac subst_eqtyparg 1); |
|
137 |
by (resolve_tac comp_rls 1); |
|
138 |
by (rtac SumE_snd 4); |
|
139 |
by (typechk_tac (SumE_fst::prems)); |
|
140 |
result(); |
|
141 |
||
142 |
writeln"Axiom of choice. Proof without fst, snd. Harder still!"; |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
143 |
val prems = Goal |
3837 | 144 |
"[| A type; !!x. x:A ==> B(x) type; \ |
1446 | 145 |
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \ |
146 |
\ |] ==> ?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). \ |
|
281
f1f96b9e6285
CTT/ex/elim.ML: in the two proofs of Axiom of Choice, changed X-->Y to PROD
lcp
parents:
0
diff
changeset
|
147 |
\ (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"; |
0 | 148 |
by (intr_tac prems); |
149 |
(*Must not use add_mp_tac as subst_prodE hides the construction.*) |
|
150 |
by (resolve_tac [ProdE RS SumE] 1 THEN assume_tac 1); |
|
151 |
by (TRYALL assume_tac); |
|
152 |
by (rtac replace_type 1); |
|
153 |
by (rtac subst_eqtyparg 1); |
|
154 |
by (resolve_tac comp_rls 1); |
|
155 |
by (etac (ProdE RS SumE) 4); |
|
156 |
by (typechk_tac prems); |
|
157 |
by (rtac replace_type 1); |
|
158 |
by (rtac subst_eqtyparg 1); |
|
159 |
by (resolve_tac comp_rls 1); |
|
160 |
by (typechk_tac prems); |
|
161 |
by (assume_tac 1); |
|
162 |
by (fold_tac basic_defs); (*puts in fst and snd*) |
|
163 |
result(); |
|
164 |
||
165 |
writeln"Example of sequent_style deduction"; |
|
166 |
(*When splitting z:A*B, the assumption C(z) is affected; ?a becomes |
|
167 |
lam u. split(u,%v w.split(v,%x y.lam z. <x,<y,z>>) ` w) *) |
|
9251
bd57acd44fc1
more tidying. also generalized some tactics to prove "Type A" and
paulson
parents:
3837
diff
changeset
|
168 |
val prems = Goal |
0 | 169 |
"[| A type; B type; !!z. z:A*B ==> C(z) type |] ==> \ |
170 |
\ ?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))"; |
|
171 |
by (resolve_tac intr_rls 1); |
|
172 |
by (biresolve_tac safe_brls 2); |
|
173 |
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *) |
|
174 |
by (res_inst_tac [ ("a","y") ] ProdE 2); |
|
175 |
by (typechk_tac prems); |
|
176 |
by (rtac SumE 1 THEN assume_tac 1); |
|
177 |
by (intr_tac[]); |
|
178 |
by (TRYALL assume_tac); |
|
179 |
by (typechk_tac prems); |
|
180 |
result(); |
|
181 |
||
182 |
writeln"Reached end of file."; |