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