development/thales/examples/beta_pair_thm.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definitions: (General definitions file)         *)
   5 (* Chapter: Packings                                                     *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-07-01                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11 (*
  12 Support for functions f {a,b} defined by lambda abstraction.
  13 *)
  14
  15 module Beta_pair = struct
  16
  17
  18 let pre_beta = prove_by_refinement
  19 (`!g u' v'. (?f. (!u v. f { u, v } = (g:A->A->B) u v)) ==>
  20     ((\ { u, v}. g u v) {u',v'} = g u' v')`,
  21 [
  22 REWRITE_TAC[GABS_DEF;GEQ_DEF];
  23 SELECT_ELIM_TAC;
  24 MESON_TAC[];
  25 ]);;
  26
  27 let WELLDEFINED_FUNCTION_2 = prove_by_refinement(
  28 `(?f:C->D. (!x:A y:B.  f(s x y) = t x y)) <=>
  29    (!x x' y y'.  (s x y = s x' y') ==> t x y = t x' y')`,
  30 [
  31   MATCH_MP_TAC EQ_TRANS ;
  32   EXISTS_TAC  `?f:C->D. !z. !x:A y:B. (s x y = z) ==> f z = t x y`;
  33   CONJ_TAC;
  34   MESON_TAC[];
  35   REWRITE_TAC[GSYM SKOLEM_THM];
  36   MESON_TAC[];
  37 ]);;
  38
  39 let well_defined_unordered_pair = prove_by_refinement
  40 (`(?f. (!u v. f { u, v} = (g:A->A->B) u v)) <=>
  41    (! u v. g u v = g v u)`,
  42 [
  43 REWRITE_TAC[WELLDEFINED_FUNCTION_2];
  44 SUBGOAL_THEN `!u v x' y'. ({u,v} = {x',y'}) <=> ((((u:A)=x') /\ (v = y'))\/ ((u= y') /\ (v = x')))` ASSUME_TAC;
  45 SET_TAC[];
  46 ASM_REWRITE_TAC[];
  47 MESON_TAC[];
  48 ]
  49 );;
  50
  51 let BETA_PAIR_THM = prove_by_refinement(
  52 `!g u' v'. (!u v. (g:A->A->B) u v = g v u) ==>
  53     ((\ { u, v}. g u v) {u',v'} = g u' v')`,
  54 [
  55 REPEAT STRIP_TAC;
  56 MATCH_MP_TAC pre_beta;
  57 REWRITE_TAC[well_defined_unordered_pair];
  58 ASM_REWRITE_TAC[];
  59 ]
  60 );;
  61
  62
  63 end;;