development/thales/examples/workshop2010_beta_pair_thm.hl

   1
   2 let pre_beta = prove_by_refinement
   3 (`!g u' v'. (?f. (!u v. f { u, v } = (g:A->A->B) u v)) ==>
   4     ((\ { u, v}. g u v) {u',v'} = g u' v')`,
   5 [
   6 REWRITE_TAC[GABS_DEF;GEQ_DEF];
   7 SELECT_ELIM_TAC;
   8 MESON_TAC[];
   9 ]);;
  10
  11 let WELLDEFINED_FUNCTION_2 = prove_by_refinement(
  12 `(?f:C->D. (!x:A y:B.  f(s x y) = t x y)) <=>
  13    (!x x' y y'.  (s x y = s x' y') ==> t x y = t x' y')`,
  14 [
  15   MATCH_MP_TAC EQ_TRANS ;
  16   EXISTS_TAC  `?f:C->D. !z. !x:A y:B. (s x y = z) ==> f z = t x y`;
  17   CONJ_TAC;
  18   MESON_TAC[];
  19   REWRITE_TAC[GSYM SKOLEM_THM];
  20   MESON_TAC[];
  21 ]);;
  22
  23 let well_defined_unordered_pair = prove_by_refinement
  24 (`(?f. (!u v. f { u, v} = (g:A->A->B) u v)) <=>
  25    (! u v. g u v = g v u)`,
  26 [
  27 REWRITE_TAC[WELLDEFINED_FUNCTION_2];
  28 SUBGOAL_THEN `!u v x' y'. ({u,v} = {x',y'}) <=> ((((u:A)=x') /\ (v = y'))\/ ((u= y') /\ (v = x')))` ASSUME_TAC;
  29 SET_TAC[];
  30 ASM_REWRITE_TAC[];
  31 MESON_TAC[];
  32 ]
  33 );;
  34
  35 let BETA_PAIR_THM = prove_by_refinement(
  36 `!g u' v'. (!u v. (g:A->A->B) u v = g v u) ==>
  37     ((\ { u, v}. g u v) {u',v'} = g u' v')`,
  38 [
  39 REPEAT STRIP_TAC;
  40 MATCH_MP_TAC pre_beta;
  41 REWRITE_TAC[well_defined_unordered_pair];
  42 ASM_REWRITE_TAC[];
  43 ]
  44 );;