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