1(* load "rich_listTheory"; *)
2open HolKernel boolLib bossLib Q listTheory rich_listTheory arithmeticTheory;
3
4val _ = new_theory "my_list";
5
6(* ------------------------------------------------------------------------- *)
7
8infix \\ << >>
9
10val op \\ = op THEN;
11val op << = op THENL;
12val op >> = op THEN1;
13
14(* ------------------------------------------------------------------------- *)
15
16val LIST_EQ = store_thm("LIST_EQ",
17  `!a b. (LENGTH a = LENGTH b) /\
18         (!x. x < LENGTH a ==> (EL x a = EL x b)) ==>
19         (a = b)`,
20  Induct_on `b` >> SIMP_TAC list_ss [LENGTH_NIL]
21    \\ Induct_on `a` \\ RW_TAC list_ss []
22    >> POP_ASSUM (fn th => PROVE_TAC [(SIMP_RULE list_ss [] o SPEC `0`) th])
23    \\ POP_ASSUM (fn th => PROVE_TAC
24         [(GEN_ALL o SIMP_RULE list_ss [] o SPEC `SUC x`) th]));
25
26val NULL_SNOC = store_thm("NULL_SNOC",
27  `!l x. ~NULL (SNOC x l)`,
28  Cases \\ SIMP_TAC list_ss [SNOC]);
29
30val FILTER_ALL = store_thm("FILTER_ALL",
31  `!l. (!n. n < LENGTH l ==> ~P (EL n l)) ==> (FILTER P l = [])`,
32  Induct \\ RW_TAC list_ss []
33    >> (EXISTS_TAC `0` \\ ASM_SIMP_TAC list_ss [])
34    \\ POP_ASSUM (fn th => PROVE_TAC
35         [(GEN_ALL o SIMP_RULE list_ss [] o SPEC `SUC n`) th]));
36
37val FILTER_NONE = store_thm("FILTER_NONE",
38  `!l. (!n. n < LENGTH l ==> P (EL n l)) ==> (FILTER P l = l)`,
39  Induct \\ RW_TAC list_ss []
40    >> POP_ASSUM (fn th => ASM_SIMP_TAC std_ss
41         [(GEN_ALL o SIMP_RULE list_ss [] o SPEC `SUC n`) th])
42    \\ POP_ASSUM (STRIP_ASSUME_TAC o SIMP_RULE list_ss [] o SPEC `0`));
43
44val MAP_GENLIST = store_thm("MAP_GENLIST",
45  `!f g n. MAP f (GENLIST g n) = GENLIST (f o g) n`,
46  Induct_on `n` \\ ASM_SIMP_TAC list_ss [GENLIST,MAP_SNOC]);
47
48val EL_GENLIST = store_thm("EL_GENLIST",
49  `!f n x. x < n ==> (EL x (GENLIST f n) = f x)`,
50  Induct_on `n` >> SIMP_TAC arith_ss []
51    \\ REPEAT STRIP_TAC \\ REWRITE_TAC [GENLIST]
52    \\ Cases_on `x < n`
53    \\ POP_ASSUM (fn th => ASSUME_TAC
54           (SUBS [(GSYM o SPECL [`f`,`n`]) LENGTH_GENLIST] th)
55              \\ ASSUME_TAC th)
56    >> ASM_SIMP_TAC bool_ss [EL_SNOC]
57    \\ `x = LENGTH (GENLIST f n)` by FULL_SIMP_TAC arith_ss [LENGTH_GENLIST]
58    \\ ASM_SIMP_TAC bool_ss [EL_LENGTH_SNOC]
59    \\ REWRITE_TAC [LENGTH_GENLIST]);
60
61val HD_GENLIST = save_thm("HD_GENLIST",
62  (SIMP_RULE arith_ss [EL] o SPECL [`f`,`SUC n`,`0`]) EL_GENLIST);
63
64val GENLIST_FUN_EQ = store_thm("GENLIST_FUN_EQ",
65  `!n f g. (!x. x < n ==> (f x = g x)) ==> (GENLIST f n = GENLIST g n)`,
66  metisLib.METIS_TAC [LIST_EQ,GSYM EL_GENLIST,LENGTH_GENLIST]);
67
68val EL_BUTFIRSTN = store_thm("EL_BUTFIRSTN",
69  `!m n l. m + n < LENGTH l ==>
70      (EL m (BUTFIRSTN n l) = EL (m + n) l)`,
71  Induct_on `l` \\ RW_TAC list_ss [] \\ Cases_on `n`
72    \\ FULL_SIMP_TAC list_ss [BUTFIRSTN,ADD_CLAUSES]);
73
74val SNOC_EL_FIRSTN = store_thm("SNOC_EL_FIRSTN",
75  `!n l. n < LENGTH l ==> (SNOC (EL n l) (FIRSTN n l) = FIRSTN (SUC n) l)`,
76  Induct \\ Cases_on `l` \\ ASM_SIMP_TAC list_ss [SNOC,FIRSTN]);
77
78val ZIP_FIRSTN_LEQ = store_thm("ZIP_FIRSTN_LEQ",
79  `!n a b. n <= LENGTH a /\ LENGTH a <= LENGTH b ==>
80     (ZIP (FIRSTN n a,FIRSTN n b) = FIRSTN n (ZIP (a,FIRSTN (LENGTH a) b)))`,
81  Induct \\ ASM_SIMP_TAC list_ss [FIRSTN]
82    \\ Cases \\ Cases \\ ASM_SIMP_TAC list_ss [FIRSTN,ZIP]);
83
84val ZIP_FIRSTN = store_thm("ZIP_FIRSTN",
85  `!n a b. n <= LENGTH a /\ (LENGTH a = LENGTH b) ==>
86     (ZIP (FIRSTN n a,FIRSTN n b) = FIRSTN n (ZIP (a,b)))`,
87  SIMP_TAC arith_ss [ZIP_FIRSTN_LEQ,FIRSTN_LENGTH_ID]);
88
89val EL_FIRSTN = store_thm("EL_FIRSTN",
90  `!n x l. x < n /\ n <= LENGTH l ==> (EL x (FIRSTN n l) = EL x l)`,
91  Induct \\ ASM_SIMP_TAC list_ss [FIRSTN]
92    \\ Cases \\ Cases \\ ASM_SIMP_TAC list_ss [FIRSTN]);
93
94val LENGTH_TL = store_thm("LENGTH_TL",
95  `!l. 0 < LENGTH l ==> (LENGTH (TL l) = LENGTH l - 1)`,
96  Cases \\ SIMP_TAC list_ss []);
97
98val ZIP_APPEND = store_thm("ZIP_APPEND",
99  `!a b c d. (LENGTH a = LENGTH b) /\
100             (LENGTH c = LENGTH d) ==>
101             (ZIP (a,b) ++ ZIP (c,d) = ZIP (a ++ c,b ++ d))`,
102  Induct_on `b` >> SIMP_TAC list_ss [LENGTH_NIL]
103    \\ Induct_on `d` >> SIMP_TAC list_ss [LENGTH_NIL]
104    \\ Induct_on `a` >> SIMP_TAC list_ss [LENGTH_NIL]
105    \\ Induct_on `c` >> SIMP_TAC list_ss [LENGTH_NIL]
106    \\ MAP_EVERY X_GEN_TAC [`h1`,`h2`,`h3`,`h4`]
107    \\ RW_TAC list_ss []
108    \\ `LENGTH (h1::c) = LENGTH (h3::d)`
109      by ASM_SIMP_TAC list_ss []
110    \\ `ZIP (a,b) ++ ZIP (h1::c,h3::d) = ZIP (a ++ h1::c,b ++ h3::d)`
111      by ASM_SIMP_TAC list_ss []
112    \\ FULL_SIMP_TAC list_ss []);
113
114val ZIP_GENLIST = store_thm("ZIP_GENLIST",
115  `!l f n. (LENGTH l = n) ==>
116     (ZIP (l,GENLIST f n) = GENLIST (\x. (EL x l,f x)) n)`,
117  REPEAT STRIP_TAC
118    \\ `LENGTH (ZIP (l,GENLIST f n)) = LENGTH (GENLIST (\x. (EL x l,f x)) n)`
119    by metisLib.METIS_TAC [LENGTH_GENLIST,LENGTH_ZIP]
120    \\ IMP_RES_TAC LIST_EQ
121    \\ POP_ASSUM MATCH_MP_TAC
122    \\ RW_TAC arith_ss [LENGTH_GENLIST,LENGTH_ZIP,listTheory.EL_ZIP,EL_GENLIST]
123);
124
125val GENLIST_APPEND = store_thm("GENLIST_APPEND",
126  `!f a b. GENLIST f (a + b) = (GENLIST f b) ++ (GENLIST (\t. f (t + b)) a)`,
127  Induct_on `a`
128    \\ ASM_SIMP_TAC list_ss [GENLIST,APPEND_SNOC,arithmeticTheory.ADD_CLAUSES]
129);
130
131val NULL_LENGTH = store_thm("NULL_LENGTH",
132  `!l. NULL l = (LENGTH l = 0)`,
133  Cases \\ METIS_TAC [LENGTH,NULL,SUC_NOT]);
134
135val APPEND_SNOC1 = store_thm("APPEND_SNOC1",
136  `!l1 x l2. SNOC x l1 ++ l2 = l1 ++ x::l2`,
137  METIS_TAC [SNOC_APPEND,CONS_APPEND, APPEND_ASSOC]);
138
139(* ------------------------------------------------------------------------- *)
140
141val _ = export_theory();
142