author | wenzelm |
Tue, 10 Feb 2015 14:48:26 +0100 | |
changeset 59498 | 50b60f501b05 |
parent 58977 | 9576b510f6a2 |
child 60770 | 240563fbf41d |
permissions | -rw-r--r-- |
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 |
||
58889 | 9 |
section "Examples with elimination rules" |
19761 | 10 |
|
11 |
theory Elimination |
|
58974 | 12 |
imports "../CTT" |
19761 | 13 |
begin |
14 |
||
15 |
text "This finds the functions fst and snd!" |
|
16 |
||
58977 | 17 |
schematic_lemma [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A" |
58972 | 18 |
apply pc |
19761 | 19 |
done |
20 |
||
58977 | 21 |
schematic_lemma [folded basic_defs]: "A type \<Longrightarrow> ?a : (A*A) --> A" |
58972 | 22 |
apply pc |
19761 | 23 |
back |
24 |
done |
|
25 |
||
26 |
text "Double negation of the Excluded Middle" |
|
58977 | 27 |
schematic_lemma "A type \<Longrightarrow> ?a : ((A + (A-->F)) --> F) --> F" |
58972 | 28 |
apply intr |
19761 | 29 |
apply (rule ProdE) |
30 |
apply assumption |
|
58972 | 31 |
apply pc |
19761 | 32 |
done |
33 |
||
58977 | 34 |
schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A*B) \<longrightarrow> (B*A)" |
58972 | 35 |
apply pc |
19761 | 36 |
done |
37 |
(*The sequent version (ITT) could produce an interesting alternative |
|
38 |
by backtracking. No longer.*) |
|
39 |
||
40 |
text "Binary sums and products" |
|
58977 | 41 |
schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A+B --> C) --> (A-->C) * (B-->C)" |
58972 | 42 |
apply pc |
19761 | 43 |
done |
44 |
||
45 |
(*A distributive law*) |
|
58977 | 46 |
schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : A * (B+C) --> (A*B + A*C)" |
58972 | 47 |
apply pc |
19761 | 48 |
done |
49 |
||
50 |
(*more general version, same proof*) |
|
36319 | 51 |
schematic_lemma |
19761 | 52 |
assumes "A type" |
58977 | 53 |
and "\<And>x. x:A \<Longrightarrow> B(x) type" |
54 |
and "\<And>x. x:A \<Longrightarrow> C(x) type" |
|
19761 | 55 |
shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))" |
58972 | 56 |
apply (pc assms) |
19761 | 57 |
done |
58 |
||
59 |
text "Construction of the currying functional" |
|
58977 | 60 |
schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A*B --> C) --> (A--> (B-->C))" |
58972 | 61 |
apply pc |
19761 | 62 |
done |
63 |
||
64 |
(*more general goal with same proof*) |
|
36319 | 65 |
schematic_lemma |
19761 | 66 |
assumes "A type" |
58977 | 67 |
and "\<And>x. x:A \<Longrightarrow> B(x) type" |
68 |
and "\<And>z. z: (SUM x:A. B(x)) \<Longrightarrow> C(z) type" |
|
19761 | 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>))" |
|
58972 | 71 |
apply (pc assms) |
19761 | 72 |
done |
73 |
||
74 |
text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)" |
|
58977 | 75 |
schematic_lemma "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> (B-->C)) --> (A*B --> C)" |
58972 | 76 |
apply pc |
19761 | 77 |
done |
78 |
||
79 |
(*more general goal with same proof*) |
|
36319 | 80 |
schematic_lemma |
19761 | 81 |
assumes "A type" |
58977 | 82 |
and "\<And>x. x:A \<Longrightarrow> B(x) type" |
83 |
and "\<And>z. z: (SUM x:A . B(x)) \<Longrightarrow> C(z) type" |
|
19761 | 84 |
shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>)) |
85 |
--> (PROD z : (SUM x:A . B(x)) . C(z))" |
|
58972 | 86 |
apply (pc assms) |
19761 | 87 |
done |
88 |
||
89 |
text "Function application" |
|
58977 | 90 |
schematic_lemma "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A --> B) * A) --> B" |
58972 | 91 |
apply pc |
19761 | 92 |
done |
93 |
||
94 |
text "Basic test of quantifier reasoning" |
|
36319 | 95 |
schematic_lemma |
19761 | 96 |
assumes "A type" |
97 |
and "B type" |
|
58977 | 98 |
and "\<And>x y. \<lbrakk>x:A; y:B\<rbrakk> \<Longrightarrow> C(x,y) type" |
19761 | 99 |
shows |
100 |
"?a : (SUM y:B . PROD x:A . C(x,y)) |
|
101 |
--> (PROD x:A . SUM y:B . C(x,y))" |
|
58972 | 102 |
apply (pc assms) |
19761 | 103 |
done |
104 |
||
105 |
text "Martin-Lof (1984) pages 36-7: the combinator S" |
|
36319 | 106 |
schematic_lemma |
19761 | 107 |
assumes "A type" |
58977 | 108 |
and "\<And>x. x:A \<Longrightarrow> B(x) type" |
109 |
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type" |
|
19761 | 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))" |
|
58972 | 112 |
apply (pc assms) |
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" |
|
58977 | 119 |
and "\<And>z. z: A+B \<Longrightarrow> C(z) type" |
19761 | 120 |
shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) |
121 |
--> (PROD z: A+B. C(z))" |
|
58972 | 122 |
apply (pc assms) |
19761 | 123 |
done |
124 |
||
125 |
(*towards AXIOM OF CHOICE*) |
|
36319 | 126 |
schematic_lemma [folded basic_defs]: |
58977 | 127 |
"\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A --> B*C) --> (A-->B) * (A-->C)" |
58972 | 128 |
apply pc |
19761 | 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" |
58977 | 136 |
and "\<And>x. x:A \<Longrightarrow> B(x) type" |
137 |
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type" |
|
19761 | 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))" |
|
58972 | 140 |
apply (intr assms) |
141 |
prefer 2 apply add_mp |
|
142 |
prefer 2 apply add_mp |
|
19761 | 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) |
|
58972 | 148 |
apply (typechk SumE_fst 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" |
58977 | 154 |
and "\<And>x. x:A \<Longrightarrow> B(x) type" |
155 |
and "\<And>x y. \<lbrakk>x:A; y:B(x)\<rbrakk> \<Longrightarrow> C(x,y) type" |
|
19761 | 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))" |
|
58972 | 158 |
apply (intr assms) |
159 |
(*Must not use add_mp as subst_prodE hides the construction.*) |
|
160 |
apply (rule ProdE [THEN SumE]) |
|
161 |
apply assumption |
|
162 |
apply assumption |
|
163 |
apply assumption |
|
19761 | 164 |
apply (rule replace_type) |
165 |
apply (rule subst_eqtyparg) |
|
166 |
apply (rule comp_rls) |
|
167 |
apply (erule_tac [4] ProdE [THEN SumE]) |
|
58972 | 168 |
apply (typechk assms) |
19761 | 169 |
apply (rule replace_type) |
170 |
apply (rule subst_eqtyparg) |
|
171 |
apply (rule comp_rls) |
|
58972 | 172 |
apply (typechk assms) |
19761 | 173 |
apply assumption |
174 |
done |
|
175 |
||
176 |
text "Example of sequent_style deduction" |
|
177 |
(*When splitting z:A*B, the assumption C(z) is affected; ?a becomes |
|
58977 | 178 |
lam u. split(u,\<lambda>v w.split(v,\<lambda>x y.lam z. <x,<y,z>>) ` w) *) |
36319 | 179 |
schematic_lemma |
19761 | 180 |
assumes "A type" |
181 |
and "B type" |
|
58977 | 182 |
and "\<And>z. z:A*B \<Longrightarrow> C(z) type" |
19761 | 183 |
shows "?a : (SUM z:A*B. C(z)) --> (SUM u:A. SUM v:B. C(<u,v>))" |
184 |
apply (rule intr_rls) |
|
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58977
diff
changeset
|
185 |
apply (tactic {* biresolve_tac @{context} safe_brls 2 *}) |
19761 | 186 |
(*Now must convert assumption C(z) into antecedent C(<kd,ke>) *) |
187 |
apply (rule_tac [2] a = "y" in ProdE) |
|
58972 | 188 |
apply (typechk assms) |
19761 | 189 |
apply (rule SumE, assumption) |
58972 | 190 |
apply intr |
191 |
defer 1 |
|
192 |
apply assumption+ |
|
193 |
apply (typechk assms) |
|
19761 | 194 |
done |
195 |
||
196 |
end |