Rqe/dedmatrix_thms.ml

   1 let le_lem = prove_by_refinement(
   2  `(!y. y <= Y ==> P y) ==>
   3   (!y. y < Y ==> P y) /\
   4   (!y. (y = Y) ==> P y)`,
   5 (* {{{ Proof *)
   6 [
   7   REPEAT STRIP_TAC;
   8   FIRST_ASSUM MATCH_MP_TAC;
   9   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  10   FIRST_ASSUM MATCH_MP_TAC;
  11   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  12 ]);;
  13 (* }}} *)
  14
  15
  16 let lt_int_lem = prove_by_refinement(
  17  `(!y. y < Y ==> P y) ==> X < Y ==>
  18   (!y. X < y /\ y < Y ==> P y)`,
  19 (* {{{ Proof *)
  20 [
  21   REPEAT STRIP_TAC;
  22   FIRST_ASSUM MATCH_MP_TAC;
  23   FIRST_ASSUM MATCH_ACCEPT_TAC;
  24 ]);;
  25 (* }}} *)
  26
  27 let ge_lem = prove_by_refinement(
  28  `(!y. Y <= y ==> P y) ==>
  29   (!y. Y < y ==> P y) /\
  30   (!y. (y = Y) ==> P y)`,
  31 (* {{{ Proof *)
  32 [
  33   REPEAT STRIP_TAC;
  34   FIRST_ASSUM MATCH_MP_TAC;
  35   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  36   FIRST_ASSUM MATCH_MP_TAC;
  37   POP_ASSUM MP_TAC THEN REAL_ARITH_TAC;
  38 ]);;
  39 (* }}} *)
  40
  41 let gt_int_lem = prove_by_refinement(
  42  `(!y. Y < y ==> P y) ==> Y < X ==>
  43   (!y. Y < y /\ y < X ==> P y)`,
  44 (* {{{ Proof *)
  45 [
  46   REPEAT STRIP_TAC;
  47   FIRST_ASSUM MATCH_MP_TAC;
  48   FIRST_ASSUM MATCH_ACCEPT_TAC;
  49 ]);;
  50 (* }}} *)
  51
  52 let rest_lt_lem = prove_by_refinement(
  53   `Y < X ==> (!x. x < X ==> P x) ==> (!x. x < Y ==> P x)`,
  54 (* {{{ Proof *)
  55 [
  56   REPEAT STRIP_TAC;
  57   FIRST_ASSUM MATCH_MP_TAC;
  58   ASM_MESON_TAC[REAL_LT_TRANS;real_gt];
  59 ]);;
  60 (* }}} *)
  61
  62 let rest_gt_lem = prove_by_refinement(
  63   `X < Y ==> (!x. X < x ==> P x) ==> (!x. Y < x ==> P x)`,
  64 (* {{{ Proof *)
  65 [
  66   REPEAT STRIP_TAC;
  67   FIRST_ASSUM MATCH_MP_TAC;
  68   ASM_MESON_TAC[REAL_LT_TRANS;real_gt];
  69 ]);;
  70 (* }}} *)
  71
  72 let rest_eq_lt_lem = prove_by_refinement(
  73   `Y < X ==> (!x. x < X ==> P x) ==> (!x. (x = Y) ==> P x)`,
  74 (* {{{ Proof *)
  75 [
  76   REPEAT STRIP_TAC;
  77   FIRST_ASSUM MATCH_MP_TAC;
  78   ASM_MESON_TAC[REAL_LT_TRANS];
  79 ]);;
  80 (* }}} *)
  81
  82 let rest_eq_gt_lem = prove_by_refinement(
  83   `X < Y ==> (!x. X < x ==> P x) ==> (!x. (x = Y) ==> P x)`,
  84 (* {{{ Proof *)
  85 [
  86   REPEAT STRIP_TAC;
  87   FIRST_ASSUM MATCH_MP_TAC;
  88   ASM_MESON_TAC[REAL_LT_TRANS];
  89 ]);;
  90 (* }}} *)
  91
  92 let rest_int_lt_lem = prove_by_refinement(
  93   `Y < X ==> (!x. x < X ==> P x) ==> (!x. Y < x /\ x < X ==> P x)`,
  94 (* {{{ Proof *)
  95 [
  96   REPEAT STRIP_TAC;
  97   FIRST_ASSUM MATCH_MP_TAC;
  98   ASM_MESON_TAC[REAL_LT_TRANS];
  99 ]);;
 100 (* }}} *)
 101
 102 let rest_int_gt_lem = prove_by_refinement(
 103   `X < Y ==> (!x. X < x ==> P x) ==> (!x. X < x /\ x < Y ==> P x)`,
 104 (* {{{ Proof *)
 105 [
 106   REPEAT STRIP_TAC;
 107   FIRST_ASSUM MATCH_MP_TAC;
 108   ASM_MESON_TAC[REAL_LT_TRANS];
 109 ]);;
 110 (* }}} *)
 111
 112
 113 let INTERPSIGN_SUBSET = prove_by_refinement(
 114   `!P Q p s. interpsign P p s  /\ Q SUBSET P ==> interpsign Q p s`,
 115 (* {{{ Proof *)
 116 [
 117   REWRITE_TAC[SUBSET;IN];
 118   REPEAT_N 4 STRIP_TAC;
 119   STRUCT_CASES_TAC (ISPEC `s:sign` SIGN_CASES) THEN
 120   REWRITE_TAC[interpsign] THEN MESON_TAC[];
 121 ]);;
 122 (* }}} *)
 123
 124 let INTERPSIGNS_SUBSET = prove_by_refinement(
 125   `!P Q ps ss. interpsigns ps P ss  /\ Q SUBSET P ==> interpsigns ps Q ss`,
 126 (* {{{ Proof *)
 127 [
 128   REWRITE_TAC[SUBSET;IN];
 129   REPEAT_N 2 STRIP_TAC;
 130   LIST_INDUCT_TAC;
 131   LIST_INDUCT_TAC;
 132   REWRITE_TAC[ALL2;interpsigns;interpsign];
 133   REWRITE_TAC[ALL2;interpsigns;interpsign];
 134   LIST_INDUCT_TAC;
 135   REWRITE_TAC[ALL2;interpsigns;interpsign];
 136   REWRITE_TAC[ALL2;interpsigns;interpsign];
 137   (* save *)
 138   REPEAT STRIP_TAC;
 139   MATCH_MP_TAC INTERPSIGN_SUBSET;
 140   ASM_MESON_TAC[SUBSET;IN];
 141   REWRITE_ASSUMS[ALL2;interpsigns;interpsign];
 142   FIRST_ASSUM MATCH_MP_TAC;
 143   ASM_REWRITE_TAC[];
 144 ]);;
 145 (* }}} *)
 146
 147 let NOPOINT_LEM = prove_by_refinement(
 148   `!pl sl. interpsigns pl (\x. T) sl  ==>
 149    (interpsigns pl (\x. x < &0) sl  /\
 150     interpsigns pl (\x. x = &0) sl  /\
 151     interpsigns pl (\x. &0 < x) sl)`,
 152 (* {{{ Proof *)
 153
 154 [
 155   REPEAT STRIP_TAC THEN MATCH_MP_TAC INTERPSIGNS_SUBSET THEN ASM_MESON_TAC[SUBSET;IN]
 156 ]);;
 157
 158 (* }}} *)