Rqe/list_rewrites.ml

   1 (* ---------------------------------------------------------------------- *)
   2 (*  List                                                                  *)
   3 (* ---------------------------------------------------------------------- *)
   4
   5 let NOT_NIL = prove_by_refinement(
   6   `!l. ~(l = []) <=> ?(h:A) t. l = CONS h t`,
   7 (* {{{ Proof *)
   8
   9 [
  10   STRIP_TAC THEN EQ_TAC;
  11   MESON_TAC[list_CASES];
  12   STRIP_TAC;
  13   ASM_MESON_TAC[NOT_CONS_NIL];
  14 ]);;
  15
  16 (* }}} *)
  17
  18 let LIST_REWRITES = ref [
  19 NOT_CONS_NIL;
  20 HD;
  21 TL;
  22 CONS_11;
  23 LENGTH;
  24 LAST;
  25 list_CASES;
  26 NOT_NIL;
  27 ];;
  28
  29 let LIST_SIMP_TAC = REWRITE_TAC (
  30   !LIST_REWRITES
  31 );;
  32
  33 let extend_list_rewrites l =
  34   LIST_REWRITES := !LIST_REWRITES @ l;;
  35
  36 BASIC_REWRITES := !LIST_REWRITES @ !BASIC_REWRITES;;