RichterHilbertAxiomGeometry/UniversalPropCartProd.ml

   1 (*                (c) Copyright, Bill Richter 2013                           *)
   2 (*          Distributed under the same license as HOL Light                  *)
   3 (*                                                                           *)
   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.                                       *)
   8
   9 needs "RichterHilbertAxiomGeometry/readable.ml";;
  10
  11 ParseAsInfix("∉",(11, "right"));;
  12 ParseAsInfix("∏",(20, "right"));;
  13 ParseAsInfix("∘",(20, "right"));;
  14 ParseAsInfix("→",(13,"right"));;
  15
  16 (*
  17 ∉ |- ∀a l. a ∉ l ⇔ ¬(a ∈ l)
  18
  19 CartesianProduct
  20   |- ∀X Y. X ∏ Y = {x,y | x ∈ X ∧ y ∈ Y}
  21
  22 FUNCTION |- ∀α. FUNCTION α ⇔
  23              (∃f s t.  α = t,f,s ∧
  24                   (∀x. x ∈ s ⇒ f x ∈ t) ∧ (∀x. x ∉ s ⇒ f x = (@y. T)))
  25
  26 SOURCE |- ∀α. SOURCE α = SND (SND α)
  27
  28 FUN |- ∀α. FUN α = FST (SND α)
  29
  30 TARGET |- ∀α. TARGET α = FST α
  31
  32 FunctionSpace
  33   |- ∀s t.  s → t = {α | FUNCTION α ∧ s = SOURCE α ∧ t = TARGET α}
  34
  35 makeFunction
  36   |- ∀t f s. makeFunction t f s = t,(λx. if x ∈ s then f x else @y. T),s
  37
  38 Projection1Function
  39   |- ∀X Y. Pi1 X Y = makeFunction X FST (X ∏ Y)
  40
  41 Projection2Function
  42   |- ∀X Y. Pi2 X Y = makeFunction Y SND (X ∏ Y)
  43
  44 FunctionComposition
  45   |- ∀α β.  α ∘ β = makeFunction (TARGET α) (FUN α o FUN β) (SOURCE β)
  46
  47 IN_CartesianProduct
  48   |- ∀X Y x y. x,y ∈ X ∏ Y ⇔ x ∈ X ∧ y ∈ Y
  49
  50 CartesianFstSnd
  51   |- ∀pair. pair ∈ X ∏ Y ⇒ FST pair ∈ X ∧ SND pair ∈ Y
  52
  53 FUNCTION_EQ
  54   |- ∀α β.  FUNCTION α ∧ FUNCTION β ∧ SOURCE α = SOURCE β ∧ FUN α = FUN β ∧
  55         TARGET α = TARGET β  ⇒  α = β
  56
  57 IN_FunctionSpace
  58   |- ∀s t α.  α ∈ s → t ⇔
  59          FUNCTION α ∧ s = SOURCE α ∧ t = TARGET α
  60
  61 makeFunction_EQ
  62   |- ∀f g s t.  (∀x. x ∈ s ⇒ f x = g x)
  63          ⇒ makeFunction t f s = makeFunction t g s
  64
  65 makeFunctionyieldsFUN
  66   |- ∀α g t f s.  α = makeFunction t f s ∧ g = FUN α
  67          ⇒ ∀x. x ∈ s ⇒ f x = g x
  68
  69 makeFunctionEq
  70   |- ∀α β f g s t.
  71          α = makeFunction t f s ∧ β = makeFunction t g s ∧
  72          (∀x. x ∈ s ⇒ f x = g x)  ⇒  α = β
  73
  74 FunctionSpaceOnSource
  75   |- ∀α f s t.  α ∈ s → t ∧ f = FUN α  ⇒  (∀x. x ∈ s ⇒ f x ∈ t)
  76
  77 FunctionSpaceOnOffSource
  78   |- ∀α f s t.  α ∈ s → t ∧ f = FUN α
  79          ⇒ (∀x. x ∈ s ⇒ f x ∈ t) ∧ (∀x. x ∉ s ⇒ f x = (@y. T))
  80
  81 ImpliesTruncatedFunctionSpace
  82   |- ∀α s t f.
  83          α = makeFunction t f s ∧ (∀x. x ∈ s ⇒ f x ∈ t)
  84          ⇒ α ∈ s → t
  85
  86 FunFunctionSpaceImplyFunction
  87   |- ∀α s t f.  α ∈ s → t ∧ f = FUN α  ⇒  α = makeFunction t f s
  88
  89 UseFunctionComposition
  90   |- ∀α β u f t g s.
  91          α = makeFunction u f t ∧ β = makeFunction t g s ∧ β ∈ s → t
  92          ⇒ α ∘ β = makeFunction u (f o g) s
  93
  94 PairProjectionFunctions
  95   |- ∀X Y. Pi1 X Y ∈ X ∏ Y → X ∧ Pi2 X Y ∈ X ∏ Y → Y
  96
  97 UniversalPropertyProduct
  98   |- ∀M A B α β.  α ∈ M → A ∧ β ∈ M → B
  99                     ⇒ (∃!γ. γ ∈ M → A ∏ B ∧
 100                        Pi1 A B ∘ γ = α ∧ Pi2 A B ∘ γ = β)
 101
 102 *)
 103
 104 let NOTIN = NewDefinition `;
 105   ∀a l. a ∉ l ⇔ ¬(a ∈ l)`;;
 106
 107 let CartesianProduct = NewDefinition `;
 108   ∀X Y. X ∏ Y = {x,y | x ∈ X ∧ y ∈ Y}`;;
 109
 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`;;
 113
 114 let SOURCE = NewDefinition `;
 115   SOURCE α = SND (SND α)`;;
 116
 117 let FUN = NewDefinition `;
 118   FUN α = FST (SND α)`;;
 119
 120 let TARGET = NewDefinition `;
 121   TARGET α = FST α`;;
 122
 123 let FunctionSpace = NewDefinition `;
 124   ∀s t. s → t = {α | FUNCTION α  ∧  s = SOURCE α  ∧ t = TARGET α}`;;
 125
 126 let makeFunction = NewDefinition `;
 127   ∀t f s. makeFunction t f s = (t, (λx. if x ∈ s then f x else @y. T), s)`;;
 128
 129 let Projection1Function = NewDefinition `;
 130   Pi1 X Y = makeFunction X FST (X ∏ Y)`;;
 131
 132 let Projection2Function = NewDefinition `;
 133   Pi2 X Y = makeFunction Y SND (X ∏ Y)`;;
 134
 135 let FunctionComposition = NewDefinition `;
 136   ∀α β.  α ∘ β = makeFunction (TARGET α) (FUN α o FUN β) (SOURCE β)`;;
 137
 138 let IN_CartesianProduct = theorem `;
 139   ∀X Y x y. x,y ∈ X ∏ Y  ⇔  x ∈ X ∧ y ∈ Y
 140
 141   proof
 142     rewrite IN_ELIM_THM CartesianProduct;     fol PAIR_EQ;     qed;
 143 `;;
 144
 145 let IN_CartesianProduct = theorem `;
 146   ∀X Y x y. x,y ∈ X ∏ Y  ⇔  x ∈ X ∧ y ∈ Y
 147
 148   proof
 149     rewrite IN_ELIM_THM CartesianProduct;     fol PAIR_EQ;     qed;
 150 `;;
 151
 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`;;
 155
 156 let FUNCTION_EQ = theorem `;
 157   ∀α β. FUNCTION α  ∧  FUNCTION β  ∧  SOURCE α = SOURCE β  ∧
 158     FUN α = FUN β  ∧  TARGET α = TARGET β
 159     ⇒ α = β
 160   by simplify FORALL_PAIR_THM FUNCTION SOURCE TARGET FUN PAIR_EQ`;;
 161
 162 let IN_FunctionSpace = theorem `;
 163   ∀s t α. α ∈ s → t
 164     ⇔  FUNCTION α  ∧  s = SOURCE α  ∧  t = TARGET α
 165   by rewrite IN_ELIM_THM FunctionSpace`;;
 166
 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`;;
 171
 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`;;
 176
 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`;;
 181
 182 let FunctionSpaceOnSource = theorem `;
 183   ∀α f s t.  α ∈ s → t  ∧  f = FUN α
 184     ⇒  ∀x. x ∈ s ⇒ f x ∈ t
 185
 186   proof
 187     rewrite FORALL_PAIR_THM IN_FunctionSpace FUNCTION SOURCE TARGET PAIR_EQ FUN;
 188     fol;     qed;
 189 `;;
 190
 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
 194
 195   proof
 196     rewrite FORALL_PAIR_THM IN_FunctionSpace FUNCTION SOURCE TARGET PAIR_EQ FUN;
 197     fol;     qed;
 198 `;;
 199
 200 let ImpliesTruncatedFunctionSpace = theorem `;
 201   ∀α s t f.  α = makeFunction t f s  ∧  (∀x. x ∈ s ⇒ f x ∈ t)
 202     ⇒ α ∈ s → t
 203
 204   proof
 205     rewrite FORALL_PAIR_THM IN_FunctionSpace makeFunction FUNCTION SOURCE TARGET NOTIN PAIR_EQ;
 206     fol;
 207   qed;
 208 `;;
 209
 210 let FunFunctionSpaceImplyFunction = theorem `;
 211   ∀α s t f.  α ∈ s → t  ∧  f = FUN α  ⇒  α = makeFunction t f s
 212
 213   proof
 214     rewrite FORALL_PAIR_THM IN_FunctionSpace makeFunction FUNCTION SOURCE TARGET FUN NOTIN PAIR_EQ;
 215     fol FUN_EQ_THM;
 216   qed;
 217 `;;
 218
 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
 223
 224   proof
 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;
 230   qed;
 231 `;;
 232
 233 let PairProjectionFunctions = theorem `;
 234   ∀X Y. Pi1 X Y ∈ X ∏ Y → X  ∧  Pi2 X Y ∈ X ∏ Y → Y
 235
 236   proof
 237     intro_TAC ∀X Y;
 238     ∀pair. pair ∈ X ∏ Y  ⇒  FST pair ∈ X  ∧ SND pair ∈ Y     [] by fol CartesianFstSnd;
 239     fol Projection1Function Projection2Function - ImpliesTruncatedFunctionSpace;
 240   qed;
 241 `;;
 242
 243 let UniversalPropertyProduct = theorem `;
 244   ∀M A B α β.  α ∈ M → A  ∧  β ∈ M → B
 245       ⇒  ∃!γ.  γ ∈ M → A ∏ B  ∧  Pi1 A B ∘ γ = α  ∧  Pi2 A B ∘ γ = β
 246
 247   proof
 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 ∘ θ = β  ⇒ θ = γ     []
 259      proof
 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;
 268      qed;
 269      fol γFunSpace γWorks - EXISTS_UNIQUE_THM;
 270   qed;
 271 `;;