Rqe/rqe_list.ml

   1
   2 let aacons_tm = `CONS:A -> A list -> A list` ;;
   3 let HD_CONV conv tm =
   4   let h::rest = dest_list tm in
   5   let ty = type_of h in
   6   let thm = conv h in
   7   let thm2 = REFL (mk_list(rest,ty)) in
   8   let cs = inst [ty,aty] aacons_tm in
   9     MK_COMB ((AP_TERM cs thm),thm2);;
  10
  11 let TL_CONV conv tm =
  12 (*   try *)
  13     let h::t = dest_list tm in
  14     let lty = type_of h in
  15     let cs = inst [lty,aty] aacons_tm in
  16       MK_COMB ((AP_TERM cs (REFL h)), (LIST_CONV conv (mk_list(t,lty))))
  17 (*   with _ -> failwith "TL_CONV" *)
  18
  19 let rec EL_CONV conv i tm =
  20   if i = 0 then HD_CONV conv tm
  21   else
  22     let h::t = dest_list tm in
  23     let lty = type_of h in
  24     let cs = inst [lty,aty] aacons_tm in
  25       MK_COMB ((AP_TERM cs (REFL h)), (EL_CONV conv (i - 1) (mk_list(t,lty))))
  26
  27
  28 (*
  29
  30   let conv = (REWRITE_CONV[ARITH_RULE `x + x = &2 * x`])
  31   let tm = `[&5 + &5; &6 + &6; &7 + &7]`
  32   HD_CONV conv tm
  33   TL_CONV conv tm
  34   HD_CONV(TL_CONV conv) tm
  35   CONS_CONV conv tm
  36   EL_CONV conv 0 tm
  37   EL_CONV conv 1 tm
  38   EL_CONV conv 2 tm
  39
  40 *)
  41
  42 let NOT_CONS = prove_by_refinement(
  43   `!l. (~ ?(h:A) t. (l = CONS h t)) ==> (l = [])`,
  44 (* {{{ Proof *)
  45
  46 [
  47   MESON_TAC[list_CASES];
  48 ]);;
  49
  50 (* }}} *)
  51
  52 let REMOVE = new_recursive_definition list_RECURSION
  53   `(REMOVE x [] = []) /\
  54    (REMOVE x (CONS (h:A) t) =
  55      let rest = REMOVE x t in
  56        if x = h then rest else CONS h rest)`;;
  57
  58 let CHOP_LIST = new_recursive_definition num_RECURSION
  59   `(CHOP_LIST 0 l = [],l) /\
  60    (CHOP_LIST (SUC n) l =
  61      let a,b = CHOP_LIST n (TL l) in
  62       CONS (HD l) a,b)`;;
  63
  64 let REM_NIL = prove(
  65  `REMOVE x [] = []`,
  66  MESON_TAC[REMOVE]);;
  67
  68 let REM_FALSE = prove_by_refinement(
  69  `!x l. ~(MEM x (REMOVE x l))`,
  70 (* {{{ Proof *)
  71 [
  72  STRIP_TAC;
  73  LIST_INDUCT_TAC;
  74  ASM_MESON_TAC[MEM;REM_NIL];
  75  CASES_ON `x = h`;
  76  ASM_REWRITE_TAC[];
  77  ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
  78  ASM_MESON_TAC[];
  79  ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
  80  ASM_MESON_TAC[MEM];
  81 ]);;
  82 (* }}} *)
  83
  84 let MEM_REMOVE = prove_by_refinement(
  85   `!x y z l. MEM x (REMOVE y l) ==> MEM x (REMOVE y (CONS z l))`,
  86 (* {{{ Proof *)
  87 [
  88   REPEAT_N 3 STRIP_TAC;
  89   CASES_ON `y = z`;
  90   ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
  91   ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
  92   ASM_MESON_TAC[MEM];
  93 ]);;
  94 (* }}} *)
  95
  96 let REM_NEQ = prove_by_refinement(
  97   `!x x1 l. MEM x l /\ ~(x = x1) ==> MEM x (REMOVE x1 l)`,
  98 (* {{{ Proof *)
  99 [
 100   STRIP_TAC THEN STRIP_TAC;
 101   LIST_INDUCT_TAC;
 102   MESON_TAC[MEM];
 103   CASES_ON `x = h`;
 104   POP_ASSUM SUBST1_TAC;
 105   STRIP_TAC;
 106   ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF;COND_CLAUSES;MEM];
 107   STRIP_TAC;
 108   CLAIM `MEM x t`;
 109   ASM_MESON_TAC[MEM];
 110   STRIP_TAC;
 111   CLAIM `MEM x (REMOVE x1 t)`;
 112   ASM_MESON_TAC[];
 113   STRIP_TAC;
 114   MATCH_MP_TAC MEM_REMOVE;
 115   FIRST_ASSUM MATCH_ACCEPT_TAC;
 116 ]);;
 117 (* }}} *)
 118
 119
 120 let LAST_SING = prove_by_refinement(
 121   `!h. LAST [h] = h`,
 122 (* {{{ Proof *)
 123
 124 [
 125   MESON_TAC[LAST];
 126 ]);;
 127
 128 (* }}} *)
 129
 130 let LAST_CONS = prove_by_refinement(
 131   `!h t. ~(t = []) ==> (LAST (CONS h t) = LAST t)`,
 132 (* {{{ Proof *)
 133 [
 134   ASM_MESON_TAC[LAST];
 135 ]);;
 136 (* }}} *)
 137
 138
 139 let LAST_CONS_CONS = prove_by_refinement(
 140   `!h1 h2 t. ~(t = []) ==> (LAST (CONS h1 (CONS h2 t)) = LAST (CONS h1 t))`,
 141 (* {{{ Proof *)
 142 [
 143   REWRITE_TAC[LAST;NOT_CONS_NIL];
 144   MESON_TAC[LAST;NOT_CONS_NIL;COND_CLAUSES];
 145 ]);;
 146 (* }}} *)
 147
 148 let HD_APPEND = prove_by_refinement(
 149   `!h t l. HD (APPEND (CONS h t) l) = h`,
 150 (* {{{ Proof *)
 151 [
 152   ASM_MESON_TAC[HD;APPEND];
 153 ]);;
 154 (* }}} *)
 155
 156 let LENGTH_0 = prove_by_refinement(
 157   `!l. (LENGTH l = 0) <=> (l = [])`,
 158 (* {{{ Proof *)
 159 [
 160   LIST_INDUCT_TAC;
 161   REWRITE_TAC[LENGTH];
 162   ASM_MESON_TAC[LENGTH;NOT_CONS_NIL;ARITH_RULE `~(0 = SUC n)`];
 163 ]);;
 164 (* }}} *)
 165
 166 let LENGTH_1 = prove_by_refinement(
 167   `!l. (LENGTH l = 1) <=> ?x. l = [x]`,
 168 (* {{{ Proof *)
 169 [
 170   LIST_INDUCT_TAC;
 171   EQ_TAC;
 172   MESON_TAC[LENGTH;ARITH_RULE `~(1 = 0)`];
 173   MESON_TAC[NOT_CONS_NIL];
 174   EQ_TAC;
 175   REWRITE_TAC[LENGTH;ARITH_RULE `~(0 = 1)`];
 176   REWRITE_TAC[LENGTH];
 177   STRIP_TAC;
 178   CLAIM `LENGTH t = 0`;
 179   POP_ASSUM MP_TAC THEN ARITH_TAC;
 180   STRIP_TAC;
 181   CLAIM `t = []`;
 182   ASM_MESON_TAC[LENGTH_0];
 183   STRIP_TAC;
 184   ASM_REWRITE_TAC[];
 185   ASM_MESON_TAC[];
 186   STRIP_TAC;
 187   ASM_MESON_TAC[LENGTH;ONE];
 188 ]);;
 189 (* }}} *)
 190
 191 let LIST_TRI = prove_by_refinement(
 192   `!p. (p = []) \/ (?x. p = [x:A]) \/ (?x y t. p = CONS x (CONS y t))`,
 193 (* {{{ Proof *)
 194 [
 195   STRIP_TAC;
 196   DISJ_CASES_TAC (ISPEC `p:A list` list_CASES);
 197   ASM_REWRITE_TAC[];
 198   POP_ASSUM MP_TAC THEN STRIP_TAC;
 199   DISJ_CASES_TAC (ISPEC `t:A list` list_CASES);
 200   ASM_MESON_TAC[];
 201   ASM_MESON_TAC[];
 202 ]);;
 203 (* }}} *)
 204
 205 let LENGTH_PAIR = prove_by_refinement(
 206   `!p. (LENGTH p = 2) <=> ?h t. p = [h:A; t]`,
 207 (* {{{ Proof *)
 208 [
 209   STRIP_TAC THEN EQ_TAC;
 210   STRIP_TAC;
 211   MP_TAC (ISPEC `p:A list` list_CASES);
 212   STRIP_TAC;
 213   ASM_MESON_TAC[LENGTH_0;ARITH_RULE `~(2 = 0)`];
 214   MP_TAC (ISPEC `t:A list` list_CASES);
 215   STRIP_TAC;
 216   ASM_MESON_TAC[LENGTH_1;ARITH_RULE `~(1 = 2)`];
 217   MP_TAC (ISPEC `t':A list` list_CASES);
 218   STRIP_TAC;
 219   EXISTS_TAC `h:A`;
 220   EXISTS_TAC `h':A`;
 221   ASM_MESON_TAC[];
 222   CLAIM `p = CONS h (CONS h' (CONS h'' t''))`;
 223   ASM_MESON_TAC[];
 224   STRIP_TAC;
 225   CLAIM `2 < LENGTH p`;
 226   POP_ASSUM SUBST1_TAC;
 227   REWRITE_TAC[LENGTH];
 228   ARITH_TAC;
 229   ASM_MESON_TAC[LT_REFL];
 230   STRIP_TAC;
 231   ASM_REWRITE_TAC[LENGTH];
 232   ARITH_TAC;
 233 ]);;
 234 (* }}} *)
 235
 236 let LENGTH_SING = prove_by_refinement(
 237   `!p. (LENGTH p = 1) <=> ?h. p = [h:A]`,
 238 (* {{{ Proof *)
 239 [
 240   STRIP_TAC THEN EQ_TAC;
 241   STRIP_TAC;
 242   MP_TAC (ISPEC `p:A list` list_CASES);
 243   STRIP_TAC;
 244   ASM_MESON_TAC[LENGTH_0;ARITH_RULE `~(1 = 0)`];
 245   MP_TAC (ISPEC `t:A list` list_CASES);
 246   STRIP_TAC;
 247   EXISTS_TAC `h:A`;
 248   ASM_MESON_TAC[];
 249   CLAIM `p = CONS h (CONS h' t')`;
 250   ASM_MESON_TAC[];
 251   STRIP_TAC;
 252   CLAIM `1 < LENGTH p`;
 253   POP_ASSUM SUBST1_TAC;
 254   REWRITE_TAC[LENGTH];
 255   ARITH_TAC;
 256   ASM_REWRITE_TAC[];
 257   ARITH_TAC;
 258   STRIP_TAC;
 259   ASM_REWRITE_TAC[LENGTH;];
 260   ARITH_TAC;
 261 ]);;
 262 (* }}} *)
 263
 264 let TL_NIL = prove_by_refinement(
 265   `!l. ~(l = []) ==> ((TL l = []) <=> ?x. l = [x])`,
 266 (* {{{ Proof *)
 267 [
 268   REPEAT STRIP_TAC THEN EQ_TAC;
 269   CLAIM `?h t. l = CONS h t`;
 270   ASM_MESON_TAC[list_CASES];
 271   STRIP_TAC;
 272   ASM_REWRITE_TAC[TL];
 273   ASM_MESON_TAC !LIST_REWRITES;
 274   ASM_MESON_TAC !LIST_REWRITES;
 275 ]);;
 276 (* }}} *)
 277
 278 let LAST_TL = prove_by_refinement(
 279   `!l. ~(l = []) /\  ~(TL l = []) ==> (LAST (TL l) = LAST l)`,
 280 (* {{{ Proof *)
 281 [
 282   LIST_INDUCT_TAC;
 283   REWRITE_TAC[];
 284   REWRITE_TAC[TL;LAST];
 285   ASM_MESON_TAC[NOT_CONS_NIL];
 286 ]);;
 287 (* }}} *)
 288
 289 let LENGTH_TL = prove_by_refinement(
 290   `!l. ~(l = []) /\  ~(TL l = []) ==> (LENGTH (TL l) = PRE(LENGTH l))`,
 291 (* {{{ Proof *)
 292 [
 293   LIST_INDUCT_TAC;
 294   REWRITE_TAC[];
 295   REPEAT STRIP_TAC;
 296   LIST_SIMP_TAC;
 297   NUM_SIMP_TAC;
 298 ]);;
 299 (* }}} *)
 300
 301 let LENGTH_NZ = prove_by_refinement(
 302  `!p. 0 < LENGTH p <=> ~(p = [])`,
 303 (* {{{ Proof *)
 304 [
 305   REPEAT STRIP_TAC;
 306   EQ_TAC;
 307   ASM_MESON_TAC[LENGTH;NOT_CONS_NIL;LT_REFL];
 308   REWRITE_TAC[LENGTH;NOT_CONS_NIL;LT_REFL;NOT_NIL];
 309   STRIP_TAC THEN ASM_REWRITE_TAC[];
 310   REWRITE_TAC[LENGTH];
 311   ARITH_TAC;
 312 ]);;
 313 (* }}} *)