1 (* (c) Copyright, Bill Richter 2013 *)
2 (* Distributed under the same license as HOL Light *)
4 (* Definitions of FunctionSpace and FunctionComposition. A proof that the *)
5 (* Cartesian product satisfies the universal property that given functions *)
6 (* α ∈ M → A and β ∈ M → B, there is a unique γ ∈ M → A ∏ B whose *)
7 (* projections to A and B are f and g. *)
9 needs "RichterHilbertAxiomGeometry/readable.ml";;
11 ParseAsInfix("∉",(11, "right"));;
12 ParseAsInfix("∏",(20, "right"));;
13 ParseAsInfix("∘",(20, "right"));;
14 ParseAsInfix("→",(13,"right"));;
17 ∉ |- ∀a l. a ∉ l ⇔ ¬(a ∈ l)
20 |- ∀X Y. X ∏ Y = {x,y | x ∈ X ∧ y ∈ Y}
22 FUNCTION |- ∀α. FUNCTION α ⇔
24 (∀x. x ∈ s ⇒ f x ∈ t) ∧ (∀x. x ∉ s ⇒ f x = (@y. T)))
26 SOURCE |- ∀α. SOURCE α = SND (SND α)
28 FUN |- ∀α. FUN α = FST (SND α)
30 TARGET |- ∀α. TARGET α = FST α
33 |- ∀s t. s → t = {α | FUNCTION α ∧ s = SOURCE α ∧ t = TARGET α}
36 |- ∀t f s. makeFunction t f s = t,(λx. if x ∈ s then f x else @y. T),s
39 |- ∀X Y. Pi1 X Y = makeFunction X FST (X ∏ Y)
42 |- ∀X Y. Pi2 X Y = makeFunction Y SND (X ∏ Y)
45 |- ∀α β. α ∘ β = makeFunction (TARGET α) (FUN α o FUN β) (SOURCE β)
48 |- ∀X Y x y. x,y ∈ X ∏ Y ⇔ x ∈ X ∧ y ∈ Y
51 |- ∀pair. pair ∈ X ∏ Y ⇒ FST pair ∈ X ∧ SND pair ∈ Y
54 |- ∀α β. FUNCTION α ∧ FUNCTION β ∧ SOURCE α = SOURCE β ∧ FUN α = FUN β ∧
55 TARGET α = TARGET β ⇒ α = β
58 |- ∀s t α. α ∈ s → t ⇔
59 FUNCTION α ∧ s = SOURCE α ∧ t = TARGET α
62 |- ∀f g s t. (∀x. x ∈ s ⇒ f x = g x)
63 ⇒ makeFunction t f s = makeFunction t g s
66 |- ∀α g t f s. α = makeFunction t f s ∧ g = FUN α
67 ⇒ ∀x. x ∈ s ⇒ f x = g x
71 α = makeFunction t f s ∧ β = makeFunction t g s ∧
72 (∀x. x ∈ s ⇒ f x = g x) ⇒ α = β
75 |- ∀α f s t. α ∈ s → t ∧ f = FUN α ⇒ (∀x. x ∈ s ⇒ f x ∈ t)
77 FunctionSpaceOnOffSource
78 |- ∀α f s t. α ∈ s → t ∧ f = FUN α
79 ⇒ (∀x. x ∈ s ⇒ f x ∈ t) ∧ (∀x. x ∉ s ⇒ f x = (@y. T))
81 ImpliesTruncatedFunctionSpace
83 α = makeFunction t f s ∧ (∀x. x ∈ s ⇒ f x ∈ t)
86 FunFunctionSpaceImplyFunction
87 |- ∀α s t f. α ∈ s → t ∧ f = FUN α ⇒ α = makeFunction t f s
89 UseFunctionComposition
91 α = makeFunction u f t ∧ β = makeFunction t g s ∧ β ∈ s → t
92 ⇒ α ∘ β = makeFunction u (f o g) s
94 PairProjectionFunctions
95 |- ∀X Y. Pi1 X Y ∈ X ∏ Y → X ∧ Pi2 X Y ∈ X ∏ Y → Y
97 UniversalPropertyProduct
98 |- ∀M A B α β. α ∈ M → A ∧ β ∈ M → B
99 ⇒ (∃!γ. γ ∈ M → A ∏ B ∧
100 Pi1 A B ∘ γ = α ∧ Pi2 A B ∘ γ = β)
104 let NOTIN = NewDefinition `;
105 ∀a l. a ∉ l ⇔ ¬(a ∈ l)`;;
107 let CartesianProduct = NewDefinition `;
108 ∀X Y. X ∏ Y = {x,y | x ∈ X ∧ y ∈ Y}`;;
110 let FUNCTION = NewDefinition `;
111 FUNCTION α ⇔ ∃f s t. α = (t, f, s) ∧
112 (∀x. x IN s ⇒ f x IN t) ∧ ∀x. x ∉ s ⇒ f x = @y. T`;;
114 let SOURCE = NewDefinition `;
115 SOURCE α = SND (SND α)`;;
117 let FUN = NewDefinition `;
118 FUN α = FST (SND α)`;;
120 let TARGET = NewDefinition `;
123 let FunctionSpace = NewDefinition `;
124 ∀s t. s → t = {α | FUNCTION α ∧ s = SOURCE α ∧ t = TARGET α}`;;
126 let makeFunction = NewDefinition `;
127 ∀t f s. makeFunction t f s = (t, (λx. if x ∈ s then f x else @y. T), s)`;;
129 let Projection1Function = NewDefinition `;
130 Pi1 X Y = makeFunction X FST (X ∏ Y)`;;
132 let Projection2Function = NewDefinition `;
133 Pi2 X Y = makeFunction Y SND (X ∏ Y)`;;
135 let FunctionComposition = NewDefinition `;
136 ∀α β. α ∘ β = makeFunction (TARGET α) (FUN α o FUN β) (SOURCE β)`;;
138 let IN_CartesianProduct = theorem `;
139 ∀X Y x y. x,y ∈ X ∏ Y ⇔ x ∈ X ∧ y ∈ Y
142 rewrite IN_ELIM_THM CartesianProduct; fol PAIR_EQ; qed;
145 let IN_CartesianProduct = theorem `;
146 ∀X Y x y. x,y ∈ X ∏ Y ⇔ x ∈ X ∧ y ∈ Y
149 rewrite IN_ELIM_THM CartesianProduct; fol PAIR_EQ; qed;
152 let CartesianFstSnd = theorem `;
153 ∀pair. pair ∈ X ∏ Y ⇒ FST pair ∈ X ∧ SND pair ∈ Y
154 by rewrite FORALL_PAIR_THM PAIR_EQ IN_CartesianProduct`;;
156 let FUNCTION_EQ = theorem `;
157 ∀α β. FUNCTION α ∧ FUNCTION β ∧ SOURCE α = SOURCE β ∧
158 FUN α = FUN β ∧ TARGET α = TARGET β
160 by simplify FORALL_PAIR_THM FUNCTION SOURCE TARGET FUN PAIR_EQ`;;
162 let IN_FunctionSpace = theorem `;
164 ⇔ FUNCTION α ∧ s = SOURCE α ∧ t = TARGET α
165 by rewrite IN_ELIM_THM FunctionSpace`;;
167 let makeFunction_EQ = theorem `;
168 ∀f g s t. (∀x. x ∈ s ⇒ f x = g x)
169 ⇒ makeFunction t f s = makeFunction t g s
170 by simplify makeFunction ∉ FUN_EQ_THM`;;
172 let makeFunctionyieldsFUN = theorem `;
173 ∀α g t f s. α = makeFunction t f s ∧ g = FUN α
174 ⇒ ∀x. x ∈ s ⇒ f x = g x
175 by simplify makeFunction FORALL_PAIR_THM FUN PAIR_EQ`;;
177 let makeFunctionEq = theorem `;
178 ∀α β f g s t. α = makeFunction t f s ∧ β = makeFunction t g s ∧
179 (∀x. x ∈ s ⇒ f x = g x) ⇒ α = β
180 by simplify FORALL_PAIR_THM makeFunction PAIR_EQ`;;
182 let FunctionSpaceOnSource = theorem `;
183 ∀α f s t. α ∈ s → t ∧ f = FUN α
184 ⇒ ∀x. x ∈ s ⇒ f x ∈ t
187 rewrite FORALL_PAIR_THM IN_FunctionSpace FUNCTION SOURCE TARGET PAIR_EQ FUN;
191 let FunctionSpaceOnOffSource = theorem `;
192 ∀α f s t. α ∈ s → t ∧ f = FUN α
193 ⇒ (∀x. x ∈ s ⇒ f x ∈ t) ∧ ∀x. x ∉ s ⇒ f x = @y. T
196 rewrite FORALL_PAIR_THM IN_FunctionSpace FUNCTION SOURCE TARGET PAIR_EQ FUN;
200 let ImpliesTruncatedFunctionSpace = theorem `;
201 ∀α s t f. α = makeFunction t f s ∧ (∀x. x ∈ s ⇒ f x ∈ t)
205 rewrite FORALL_PAIR_THM IN_FunctionSpace makeFunction FUNCTION SOURCE TARGET NOTIN PAIR_EQ;
210 let FunFunctionSpaceImplyFunction = theorem `;
211 ∀α s t f. α ∈ s → t ∧ f = FUN α ⇒ α = makeFunction t f s
214 rewrite FORALL_PAIR_THM IN_FunctionSpace makeFunction FUNCTION SOURCE TARGET FUN NOTIN PAIR_EQ;
219 let UseFunctionComposition = theorem `;
220 ∀α β u f t g s. α = makeFunction u f t ∧
221 β = makeFunction t g s ∧ β ∈ s → t
222 ⇒ α _o_ β = makeFunction u (f o g) s
225 rewrite FORALL_PAIR_THM makeFunction FunctionComposition SOURCE TARGET FUN BETA_THM o_THM IN_FunctionSpace FUNCTION SOURCE TARGET NOTIN PAIR_EQ;
226 X_genl_TAC u' f' t' t1 g1 s1 u f t g s;
227 intro_TAC Hα Hβ Hβ_st Hs Ht;
228 (∀x. x ∈ s ⇒ g x ∈ t) [g_st] by fol Hβ_st Hβ;
229 simplify Hα GSYM Hs Hβ g_st;
233 let PairProjectionFunctions = theorem `;
234 ∀X Y. Pi1 X Y ∈ X ∏ Y → X ∧ Pi2 X Y ∈ X ∏ Y → Y
238 ∀pair. pair ∈ X ∏ Y ⇒ FST pair ∈ X ∧ SND pair ∈ Y [] by fol CartesianFstSnd;
239 fol Projection1Function Projection2Function - ImpliesTruncatedFunctionSpace;
243 let UniversalPropertyProduct = theorem `;
244 ∀M A B α β. α ∈ M → A ∧ β ∈ M → B
245 ⇒ ∃!γ. γ ∈ M → A ∏ B ∧ Pi1 A B ∘ γ = α ∧ Pi2 A B ∘ γ = β
248 intro_TAC ∀M A B α β, H1;
249 consider f g such that f = FUN α ∧ g = FUN β [fgExist] by fol;
250 consider h such that h = λx. (f x,g x) [hExists] by fol;
251 ∀x. x ∈ M ⇒ h x ∈ A ∏ B [hProd] by fol hExists IN_CartesianProduct H1 fgExist FunctionSpaceOnSource;
252 consider γ such that γ = makeFunction (A ∏ B) h M [γExists] by fol;
253 γ ∈ M → A ∏ B [γFunSpace] by fol - hProd ImpliesTruncatedFunctionSpace;
254 ∀x. x ∈ M ⇒ (FST o h) x = f x ∧ (SND o h) x = g x [h_fg] by simplify hExists PAIR o_THM;
255 Pi1 A B ∘ γ = makeFunction A (FST o h) M ∧
256 Pi2 A B ∘ γ = makeFunction B (SND o h) M [] by fol Projection1Function Projection2Function γExists γFunSpace UseFunctionComposition;
257 Pi1 A B ∘ γ = α ∧ Pi2 A B ∘ γ = β [γWorks] by fol - h_fg makeFunction_EQ H1 fgExist FunFunctionSpaceImplyFunction;
258 ∀θ. θ ∈ M → A ∏ B ∧ Pi1 A B ∘ θ = α ∧ Pi2 A B ∘ θ = β ⇒ θ = γ []
260 intro_TAC ∀θ, θWorks;
261 consider k such that k = FUN θ [kExists] by fol;
262 θ = makeFunction (A ∏ B) k M [θFUNk] by fol θWorks - FunFunctionSpaceImplyFunction;
263 α = makeFunction A (FST o k) M ∧ β = makeFunction B (SND o k) M [] by fol Projection1Function Projection2Function θFUNk θWorks UseFunctionComposition;
264 ∀x. x ∈ M ⇒ f x = (FST o k) x ∧ g x = (SND o k) x [fg_k] by fol ISPECL [α; f; A; (FST o k); M] makeFunctionyieldsFUN ISPECL [β; g; B; (SND o k); M] makeFunctionyieldsFUN - fgExist;
265 ∀x. x ∈ M ⇒ k x = ((FST o k) x, (SND o k) x) [] by fol PAIR o_THM;
266 ∀x. x ∈ M ⇒ k x = (f x, g x) [] by fol - fg_k PAIR_EQ;
267 fol hExists θFUNk γExists - makeFunctionEq;
269 fol γFunSpace γWorks - EXISTS_UNIQUE_THM;