1open HolKernel Parse bossLib boolLib pred_setTheory 2 3val _ = new_theory "word" 4 5val _ = Datatype` word = WORD (num -> 'a set)`; 6 7val suff_def = Define `suff (WORD f) n = WORD (\x. f (n+x))`; 8 9val at_def = Define `at (WORD f) n = f n`; 10 11val word_range_def = Define `word_range w = {x | ?i. at w i = x }`; 12 13val AT_SUFF_LEMM = store_thm 14 ("AT_SUFF_LEMM", 15 ``!w n i. at (suff w n) i = at w (i + n)``, 16 rw[] >> Cases_on `w` 17 >> fs[at_def, suff_def] 18 ); 19 20val SUFF_SUFF_LEMM = store_thm 21 ("SUFF_SUFF_LEMM", 22 ``!w t1 t2. suff (suff w t1) t2 = suff w (t1+t2)``, 23 Cases_on `w` >> SIMP_TAC arith_ss [suff_def]); 24 25val SUFF_0_LEMM = store_thm 26 ("SUFF_0_LEMM", 27 ``!w. suff w 0 = w``, 28 Cases_on `w` >> SIMP_TAC arith_ss [suff_def, ETA_THM]); 29 30val WORD_RANGE_SUFF_LEMM = store_thm 31 ("WORD_RANGE_SUFF_LEMM", 32 ``!w n. word_range (suff w n) ��� word_range w``, 33 fs[word_range_def, SUBSET_DEF] >> metis_tac[AT_SUFF_LEMM] 34 ); 35 36val AT_WORD_RANGE = store_thm 37 ("AT_WORD_RANGE", 38 ``!w i. at w i ��� word_range w``, 39 rw[word_range_def] >> metis_tac[word_range_def] 40 ); 41 42val _ = export_theory(); 43