Tutorial/Sets_and_functions.ml

   1 let SURJECTIVE_IFF_RIGHT_INVERSE = prove
   2  (`(!y. ?x. g x = y) <=> (?f. g o f = I)`,
   3   REWRITE_TAC[FUN_EQ_THM; o_DEF; I_DEF] THEN MESON_TAC[]);;
   4
   5 let INJECTIVE_IFF_LEFT_INVERSE = prove
   6  (`(!x y. f x = f y ==> x = y) <=> (?g. g o f = I)`,
   7   let lemma = MESON[]
   8    `(!x x'. f x = f x' ==> x = x') <=> (!y:B. ?u:A. !x. f x = y ==> u = x)` in
   9   REWRITE_TAC[lemma; FUN_EQ_THM; o_DEF; I_DEF] THEN MESON_TAC[]);;
  10
  11 let cantor = new_definition
  12  `cantor(x,y) = ((x + y) EXP 2 + 3 * x + y) DIV 2`;;
  13
  14 (**** Needs external SDP solver
  15
  16 needs "Examples/sos.ml";;
  17
  18 let CANTOR_LEMMA = prove
  19  (`cantor(x,y) = cantor(x',y') ==> x + y = x' + y'`,
  20   REWRITE_TAC[cantor] THEN CONV_TAC SOS_RULE);;
  21
  22 ****)
  23
  24 let CANTOR_LEMMA_LEMMA = prove
  25  (`x + y < x' + y' ==> cantor(x,y) < cantor(x',y')`,
  26   REWRITE_TAC[ARITH_RULE `x + y < z <=> x + y + 1 <= z`] THEN DISCH_TAC THEN
  27   REWRITE_TAC[cantor; ARITH_RULE `3 * x + y = (x + y) + 2 * x`] THEN
  28   MATCH_MP_TAC(ARITH_RULE `x + 2 <= y ==> x DIV 2 < y DIV 2`) THEN
  29   MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `(x + y + 1) EXP 2 + (x + y + 1)` THEN
  30   CONJ_TAC THENL [ARITH_TAC; ALL_TAC] THEN
  31   MATCH_MP_TAC(ARITH_RULE `a:num <= b /\ c <= d ==> a + c <= b + d + e`) THEN
  32   ASM_SIMP_TAC[EXP_2; LE_MULT2]);;
  33
  34 let CANTOR_LEMMA = prove
  35  (`cantor(x,y) = cantor(x',y') ==> x + y = x' + y'`,
  36   MESON_TAC[LT_CASES; LT_REFL; CANTOR_LEMMA_LEMMA]);;
  37
  38 let CANTOR_INJ = prove
  39  (`!w z. cantor w = cantor z ==> w = z`,
  40   REWRITE_TAC[FORALL_PAIR_THM; PAIR_EQ] THEN REPEAT GEN_TAC THEN
  41   DISCH_THEN(fun th -> MP_TAC th THEN ASSUME_TAC(MATCH_MP CANTOR_LEMMA th)) THEN
  42   ASM_REWRITE_TAC[cantor; ARITH_RULE `3 * x + y = (x + y) + 2 * x`] THEN
  43   REWRITE_TAC[ARITH_RULE `(a + b + 2 * x) DIV 2 = (a + b) DIV 2 + x`] THEN
  44   POP_ASSUM MP_TAC THEN ARITH_TAC);;
  45
  46 let CANTOR_THM = prove
  47  (`~(?f:(A->bool)->A. (!x y. f(x) = f(y) ==> x = y))`,
  48   REWRITE_TAC[INJECTIVE_IFF_LEFT_INVERSE; FUN_EQ_THM; I_DEF; o_DEF] THEN
  49   STRIP_TAC THEN FIRST_ASSUM(MP_TAC o SPEC `\x:A. ~(g x x)`) THEN
  50   MESON_TAC[]);;