1app load ["bossLib"];  open bossLib;
2
3(*---------------------------------------------------------------------------
4            An APL-style "iota" function.
5 ---------------------------------------------------------------------------*)
6
7val iota_def = 
8  Hol_defn "iota" 
9           `iota bot top = if bot > top then [] else bot::iota (bot+1) top`;
10
11
12val (iota_eqn, iota_ind) =
13  Defn.tprove 
14    (iota_def, 
15     WF_REL_TAC `measure \(b,t). SUC t - b` THEN DECIDE_TAC);
16
17
18(*---------------------------------------------------------------------------*
19 * A couple of properties.                                                   *
20 *---------------------------------------------------------------------------*)
21
22val iota_bounds = Q.prove
23(`!bot top n. MEM n (iota bot top) ==> bot <= n /\ n <= top`,
24 recInduct iota_ind
25  THEN REPEAT GEN_TAC THEN NTAC 2 STRIP_TAC
26  THEN ONCE_REWRITE_TAC [iota_eqn]
27  THEN RW_TAC list_ss [listTheory.MEM]
28  THENL [DECIDE_TAC, 
29         DECIDE_TAC, 
30         PROVE_TAC [DECIDE (Term`x+y <= z ==> x<=z`)],
31         PROVE_TAC[]]);
32
33
34val iota_length = Q.prove
35(`!bot top. bot <= top ==> (LENGTH(iota bot top) = (top-bot)+1)`,
36 recInduct iota_ind
37  THEN REPEAT GEN_TAC THEN NTAC 2 STRIP_TAC
38  THEN ONCE_REWRITE_TAC [iota_eqn]
39  THEN RW_TAC std_ss [listTheory.LENGTH]
40  THENL [DECIDE_TAC,
41         RW_TAC std_ss [arithmeticTheory.ONE,arithmeticTheory.ADD_CLAUSES] 
42           THEN RW_TAC std_ss [arithmeticTheory.ADD1] THEN
43           Cases_on `bot = top` THENL 
44            [RW_TAC std_ss [] 
45               THEN ONCE_REWRITE_TAC [iota_eqn] THEN RW_TAC list_ss [],
46             `bot+1 <= top` by DECIDE_TAC THEN
47             `LENGTH (iota (bot+1) top) = (top - (bot+1)) + 1` by RES_TAC
48               THEN Q.PAT_ASSUM `x = y` SUBST_ALL_TAC
49               THEN WEAKEN_TAC(fn tm => is_imp tm andalso not(is_neg tm))
50               THEN DECIDE_TAC]]);
51
52(*---------------------------------------------------------------------------
53      Some computations with iota.
54 ---------------------------------------------------------------------------*)
55
56val Eval = EVAL o Term;
57
58Eval `iota 0 0`;
59Eval `iota 0 12`;
60Eval `iota 12 10`;
61Eval `iota 12 100`;
62Eval `iota 250 351`;
63Eval `iota 0 1000`;
64