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