1open HolKernel Parse boolLib; 2val _ = new_theory "sequence"; 3 4open bossLib arithmeticTheory extra_numTheory combinTheory HurdUseful; 5 6infixr 0 ++ || ORELSEC; 7infix 1 >>; 8nonfix THEN ORELSE; 9 10val op++ = op THEN; 11val op|| = op ORELSE; 12val op>> = op THEN1; 13 14(* ------------------------------------------------------------------------- *) 15(* Definitions. *) 16(* ------------------------------------------------------------------------- *) 17 18val shd_def = Define `shd (f : num -> 'a) = f 0`; 19 20val stl_def = Define `stl (f : num -> 'a) n = f (SUC n)`; 21 22val scons_def = Define 23 `(scons (h : 'a) (t : num -> 'a) 0 = h) /\ (scons h t (SUC n) = t n)`; 24 25val sdest_def = Define `sdest = \s. (shd s, stl s)`; 26 27val sconst_def = Define `sconst = (K : 'a -> num -> 'a)`; 28 29val stake_def = Define 30 `(stake 0 s = []) /\ (stake (SUC n) s = shd s :: stake n (stl s))`; 31 32val sdrop_def = Define `(sdrop 0 = I) /\ (sdrop (SUC n) = sdrop n o stl)`; 33 34val eventually_def = Define `eventually x y = ?n. sdrop n x = sdrop n y`; 35 36(* ------------------------------------------------------------------------- *) 37(* Theorems. *) 38(* ------------------------------------------------------------------------- *) 39 40val STL_PARTIAL = store_thm 41 ("STL_PARTIAL", 42 ``!f. stl f = f o SUC``, 43 FUN_EQ_TAC 44 ++ RW_TAC std_ss [stl_def, o_DEF]); 45 46val SCONS_SURJ = store_thm 47 ("SCONS_SURJ", 48 ``!x. ?h t. (x = scons h t)``, 49 STRIP_TAC 50 ++ EXISTS_TAC ``shd x`` 51 ++ EXISTS_TAC ``stl x`` 52 ++ FUN_EQ_TAC 53 ++ Cases >> RW_TAC std_ss [scons_def, shd_def] 54 ++ RW_TAC std_ss [scons_def, stl_def]); 55 56val SHD_STL_ISO = store_thm 57 ("SHD_STL_ISO", 58 ``!h t. ?x. (shd x = h) /\ (stl x = t)``, 59 REPEAT STRIP_TAC 60 ++ Q.EXISTS_TAC `\x. num_CASE x h t` 61 ++ RW_TAC arith_ss [shd_def] 62 ++ MATCH_MP_TAC EQ_EXT 63 ++ Cases >> RW_TAC std_ss [stl_def] 64 ++ RW_TAC std_ss [stl_def]); 65 66val SHD_SCONS = store_thm 67 ("SHD_SCONS", 68 ``!h t. shd (scons h t) = h``, 69 RW_TAC arith_ss [shd_def, scons_def]); 70 71val STL_SCONS = store_thm 72 ("STL_SCONS", 73 ``!h t. stl (scons h t) = t``, 74 Suff `!h t n. stl (scons h t) n = t n` >> PROVE_TAC [EQ_EXT] 75 ++ RW_TAC arith_ss [stl_def, scons_def]); 76 77val SHD_SCONST = store_thm 78 ("SHD_SCONST", 79 ``!b. shd (sconst b) = b``, 80 RW_TAC std_ss [sconst_def, K_DEF, shd_def]); 81 82val STL_SCONST = store_thm 83 ("STL_SCONST", 84 ``!b. stl (sconst b) = sconst b``, 85 STRIP_TAC 86 ++ FUN_EQ_TAC 87 ++ RW_TAC std_ss [sconst_def, K_DEF, stl_def]); 88 89val SCONS_SHD_STL = store_thm 90 ("SCONS_SHD_STL", 91 ``!x. scons (shd x) (stl x) = x``, 92 STRIP_TAC 93 ++ FUN_EQ_TAC 94 ++ Cases >> RW_TAC std_ss [scons_def, shd_def] 95 ++ RW_TAC std_ss [scons_def, stl_def]); 96 97val FST_o_SDEST = store_thm 98 ("FST_o_SDEST", 99 ``FST o sdest = shd``, 100 FUN_EQ_TAC 101 ++ RW_TAC std_ss [sdest_def, o_THM]); 102 103val SND_o_SDEST = store_thm 104 ("SND_o_SDEST", 105 ``SND o sdest = stl``, 106 FUN_EQ_TAC 107 ++ RW_TAC std_ss [sdest_def, o_THM]); 108 109val SEQUENCE_DEFINE = store_thm 110 ("SEQUENCE_DEFINE", 111 ``!phd ptl. ?g. 112 (!(x : 'a). shd (g x) = phd x) /\ (!(x : 'a). stl (g x) = g (ptl x))``, 113 RW_TAC std_ss [] 114 ++ Q.EXISTS_TAC `\x n. phd (FUNPOW ptl n x)` 115 ++ FUN_EQ_TAC 116 ++ RW_TAC std_ss [shd_def, stl_def, FUNPOW]); 117 118val SCONS_EQ = store_thm 119 ("SCONS_EQ", 120 ``!x xs y ys. (scons x xs = scons y ys) = (x = y) /\ (xs = ys)``, 121 RW_TAC std_ss [] 122 ++ REVERSE EQ_TAC >> PROVE_TAC [] 123 ++ PROVE_TAC [SHD_SCONS, STL_SCONS]); 124 125val STL_o_SDROP = store_thm 126 ("STL_o_SDROP", 127 ``!n. stl o sdrop n = sdrop (SUC n)``, 128 Induct >> RW_TAC bool_ss [sdrop_def, I_o_ID] 129 ++ RW_TAC bool_ss [sdrop_def, o_ASSOC]); 130 131val SDROP_ADD = store_thm 132 ("SDROP_ADD", 133 ``!s x y. sdrop (x + y) s = sdrop x (sdrop y s)``, 134 Induct_on `y` >> RW_TAC list_ss [sdrop_def, I_THM] 135 ++ RW_TAC std_ss [ADD_CLAUSES, sdrop_def, o_THM]); 136 137val SDROP_EQ_MONO = store_thm 138 ("SDROP_EQ_MONO", 139 ``!m n x y. (sdrop m x = sdrop m y) /\ m <= n ==> (sdrop n x = sdrop n y)``, 140 RW_TAC std_ss [LESS_EQ_EXISTS] 141 ++ Induct_on `p` >> RW_TAC arith_ss [] 142 ++ RW_TAC std_ss [ADD_CLAUSES, GSYM STL_o_SDROP, o_THM]); 143 144val EVENTUALLY_REFL = store_thm 145 ("EVENTUALLY_REFL", 146 ``!x. eventually x x``, 147 RW_TAC std_ss [eventually_def]); 148 149val EVENTUALLY_SYM = store_thm 150 ("EVENTUALLY_SYM", 151 ``!x y. eventually x y = eventually y x``, 152 RW_TAC std_ss [eventually_def] 153 ++ PROVE_TAC []); 154 155val EVENTUALLY_TRANS = store_thm 156 ("EVENTUALLY_TRANS", 157 ``!x y z. eventually x y /\ eventually y z ==> eventually x z``, 158 RW_TAC std_ss [eventually_def] 159 ++ Q.EXISTS_TAC `MAX n n'` 160 ++ PROVE_TAC [X_LE_MAX, LESS_EQ_REFL, SDROP_EQ_MONO]); 161 162val SEQUENCE_DEFINE_ALT = store_thm 163 ("SEQUENCE_DEFINE_ALT", 164 ``!phd ptl. ?g:'a->num->'b. !x. g x = scons (phd x) (g (ptl x))``, 165 RW_TAC std_ss [] 166 ++ MP_TAC (Q.SPECL [`phd`, `ptl`] SEQUENCE_DEFINE) 167 ++ RW_TAC std_ss [] 168 ++ Q.EXISTS_TAC `g` 169 ++ RW_TAC std_ss [] 170 ++ MP_TAC (Q.ISPEC `(g:'a->num->'b) x` SCONS_SURJ) 171 ++ RW_TAC std_ss [] 172 ++ Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 173 ++ Q.PAT_X_ASSUM `!x. P x` (MP_TAC o Q.SPEC `x`) 174 ++ RW_TAC std_ss [SCONS_EQ, SHD_SCONS, STL_SCONS]); 175 176local 177 val th = prove 178 (``?s. !h t x. s h t x = scons (h x) (s h t (t x))``, 179 MP_TAC SEQUENCE_DEFINE_ALT 180 ++ RW_TAC std_ss [SKOLEM_THM]) 181in 182 val siter_def = new_specification ("siter_def", ["siter"], th); 183end; 184 185val SHD_SITER = store_thm 186 ("SHD_SITER", 187 ``!h t x. shd (siter h t x) = h x``, 188 ONCE_REWRITE_TAC [siter_def] 189 ++ RW_TAC std_ss [SHD_SCONS]); 190 191val STL_SITER = store_thm 192 ("STL_SITER", 193 ``!h t x. stl (siter h t x) = siter h t (t x)``, 194 RW_TAC std_ss [] 195 ++ CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [siter_def])) 196 ++ RW_TAC std_ss [STL_SCONS]); 197 198val _ = export_theory (); 199