legacy/inequalities/sigmahat.hl

   1
   2
   3 let max_real_symm = prove_by_refinement(
   4   `!a b. max_real a b = max_real b a`,
   5   [
   6   REP_GEN_TAC;
   7   REWRITE_TAC[max_real];
   8   COND_CASES_TAC;
   9   USE 0 (MATCH_MP (REAL_ARITH `a < b ==> ~(b < a)`));
  10   ASM_REWRITE_TAC[];
  11   COND_CASES_TAC;
  12   ASM_REWRITE_TAC[];
  13   UND 0;
  14   UND 1;
  15   REAL_ARITH_TAC;
  16   ]);;
  17
  18
  19 let SIGMAHAT_EQ = prove(
  20   `!x1 x2 x3 x4 x5 x6. sigmahat_x x1 x2 x3 x4 x5 x6 = sigmahat_x' x1 x2 x3 x4 x5 x6`,
  21   REPEAT STRIP_TAC THEN
  22   REWRITE_TAC [sigmahat_x';sigmahat_x] THEN
  23   LET_TAC THEN
  24   LET_TAC THEN
  25   LET_TAC THEN
  26   LET_TAC THEN
  27   LET_TAC THEN
  28   LET_TAC THEN
  29   LET_TAC THEN
  30   LET_TAC THEN
  31   LET_TAC THEN
  32   COND_CASES_TAC THEN
  33   REWRITE_TAC[]
  34   LET_TAC THEN
  35   COND_CASES_TAC THEN REWRITE_TAC[] THEN
  36   COND_CASES_TAC THEN REWRITE_TAC[] THEN
  37   LET_TAC THEN
  38   COND_CASES_TAC THEN REWRITE_TAC[] THEN
  39   LET_TAC THEN
  40   COND_CASES_TAC THEN REWRITE_TAC[] THEN
  41   LET_TAC THEN
  42   COND_CASES_TAC THEN REWRITE_TAC[] THEN
  43   LET_TAC THEN
  44   REWRITE_ALL_TAC[]
  45   ONCE_REWRITE_TAC[MAX_REAL_SYMM]
  46
  47
  48 let TEST = prove(`!x:bool. x = x`,
  49     STRIP_TAC THEN
  50     REWRITE_TAC []);;
  51
  52
  53
  54 (program-get-line)                        let x = 5
  55
  56
  57 e (REPEAT STRIP_TAC)
  58 e (REWRITE_TAC[sigmahat_sean_x;sigmahat_x;LET_DEF;LET_END_DEF])
  59 e (REPEAT COND_CASES_TAC THEN REWRITE_TAC[])
  60 e (MESON_TAC[])
  61