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