xref: /seL4-l4v-10.1.1/HOL4/src/quotient/examples/more_listScript.sml

open HolKernel Parse boolLib;
infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->;
infixr -->;


val _ = new_theory "more_list";


(*
app load [
          "numTheory", "listTheory", "rich_listTheory", "listLib", "pred_setLib",
          "more_setTheory",
          "arithLib", "Psyntax" ];
*)

open combinTheory numTheory arithmeticTheory
     listTheory rich_listTheory listLib more_setTheory
     numLib Psyntax ;


open tactics;



val MAP2_APPEND = store_thm
   ("MAP2_APPEND",
    ���!s1 s2 t1 t2 (f:'a->'b->'c).
          (LENGTH s1 = LENGTH s2) ==>
          (MAP2 f (APPEND s1 t1) (APPEND s2 t2) =
          APPEND (MAP2 f s1 s2) (MAP2 f t1 t2))���,
    LIST_INDUCT_TAC
    THENL
       [ LIST_INDUCT_TAC
         THEN REWRITE_TAC[LENGTH,APPEND,MAP2,SUC_NOT],

         GEN_TAC
         THEN LIST_INDUCT_TAC
         THEN REWRITE_TAC[LENGTH,NOT_SUC]
         THEN REWRITE_TAC[ADD1,EQ_MONO_ADD_EQ]
         THEN REWRITE_TAC[APPEND,MAP2]
         THEN REPEAT GEN_TAC
         THEN DISCH_TAC
         THEN RES_TAC
         THEN ASM_REWRITE_TAC[]
      ]
   );

val AND_EL = store_thm
   ("AND_EL",
    ���(AND_EL [] = T) /\
        (!x l. AND_EL (CONS x l) = (x /\ AND_EL l))���,
    REWRITE_TAC[AND_EL_DEF]
    THEN REWRITE_TAC[ALL_EL]
    THEN REWRITE_TAC[combinTheory.I_THM]
   );

val AND_EL_APPEND = store_thm
   ("AND_EL_APPEND",
    ���!s t. AND_EL (APPEND s t) = (AND_EL s /\ AND_EL t)���,
    REWRITE_TAC[AND_EL_DEF]
    THEN LIST_INDUCT_TAC
    THEN REWRITE_TAC[APPEND,ALL_EL]
    THEN ASM_REWRITE_TAC[CONJ_ASSOC]
   );

(* =============================================================== *)
(* LENGTH_FILTER says that if we filter a list into two using P    *)
(* as a predicate, then the sum of the lengths of the two parts    *)
(* must equal the length of the whole.                             *)
(* =============================================================== *)

val LENGTH_FILTER = store_thm
   ("LENGTH_FILTER",
    ���!(l:'a list) P.
          LENGTH (FILTER P l) + LENGTH (FILTER ($~ o P) l) = LENGTH l���,
    LIST_INDUCT_TAC
    THEN REWRITE_TAC[FILTER]
    THENL
       [ REWRITE_TAC[LENGTH,ADD_0],

         REWRITE_TAC[o_THM]
         THEN REPEAT GEN_TAC
         THEN COND_CASES_TAC
         THEN ASM_REWRITE_TAC[LENGTH,ADD_CLAUSES]
      ]
   );

(* =============================================================== *)
(* Applying LENGTH_FILTER to a specific filter, we can calculate   *)
(* the length of the partitions of num lists where the partition   *)
(* separates the bottom of a range from the larger members.        *)
(* For all lists of numbers l, the number of elements of value n   *)
(* or more equals the number of elements of value n plus the       *)
(* number of elements of value more than n.                        *)
(* =============================================================== *)

val LENGTH_FILTER_LESS_EQ = store_thm
   ("LENGTH_FILTER_LESS_EQ",
    ���!l n.  LENGTH (FILTER (\y. n = y) l) +
               LENGTH (FILTER (\y. n < y) l) =
               LENGTH (FILTER (\y. n <= y) l)���,
    REWRITE_TAC
    [(GENL [���l:num list���,���n:num���]
      o REWRITE_RULE[ARITH_PROVE ��� (n=y) /\ (n <= y) = (n = y)���,
                     ARITH_PROVE ���~(n=y) /\ (n <= y) = (n < y)���]
      o CONV_RULE (DEPTH_CONV BETA_CONV)
      o REWRITE_RULE[FILTER_FILTER,o_THM]
      o ISPECL[���FILTER (\y. n <= y) l���,���\y:num. n = y���])
     LENGTH_FILTER]
   );


(*
FILTER_MAP;
    |- !f1 f2 l. FILTER f1 (MAP f2 l) = MAP f2 (FILTER (f1 o f2) l)
*)


val SL =
    new_recursive_definition
      {rec_axiom = listTheory.list_Axiom,
       name      = "SL",
       def       = ���(SL NIL = {}) /\
                       (SL (CONS (y:'a) l) = y INSERT (SL l))���};


val SL_APPEND = store_thm
  ("SL_APPEND",
 ���!(l1: 'a list) l2. SL (APPEND l1 l2) = (SL l1 UNION SL l2)���,
    LIST_INDUCT_TAC
    THEN ASM_REWRITE_TAC[APPEND,SL,UNION]
   );


val SL_FLAT = store_thm
  ("SL_FLAT",
 ���!(l: 'a list list). SL (FLAT l) = UNION_SET (SL (MAP SL l))���,
    LIST_INDUCT_TAC
    THEN REWRITE_TAC[FLAT,MAP,SL,UNION_SET]
    THEN ASM_REWRITE_TAC[SL_APPEND]
   );

val SL_MAP = store_thm
  ("SL_MAP",
 ���!l (f: 'a->'b). SL (MAP f l) = IMAGE f (SL l)���,
    LIST_INDUCT_TAC
    THEN ASM_REWRITE_TAC[MAP,SL,IMAGE]
   );

val DELETE_DIFF_SL =
 store_thm
  ("DELETE_DIFF_SL",
   ���!xs s (e:'a).
        s DELETE e DIFF SL xs = s DIFF SL (e::xs)���,
   LIST_INDUCT_TAC
   THEN REWRITE_TAC[SL,DIFFF]
  );


val DL =
    new_recursive_definition
      {rec_axiom = listTheory.list_Axiom,
       name      = "DL",
       def       = ���(DL NIL = T) /\
                       (DL (CONS (y:'a) l) = (~(y IN SL l) /\ DL l))���};



val _ = export_theory();

val _ = print_theory_to_file "-" "more_list.lst";

val _ = html_theory "more_list";