1(*--------------------------------------------------------------------------- 2 Find an element not in a given list. 3 ---------------------------------------------------------------------------*) 4 5val variant_def = 6 Hol_defn "variant" 7 `variant x L = if MEM x L then variant (x+1) L else x`; 8 9(*--------------------------------------------------------------------------- 10 Lemma required in termination proof. 11 ---------------------------------------------------------------------------*) 12 13val LENGTH_FILTER_SUBSET = Q.prove( 14`(!y. P y ==> Q y) ==> !L. LENGTH(FILTER P L) <= LENGTH (FILTER Q L)`, 15DISCH_TAC THEN Induct THEN ZAP_TAC (list_ss && [listTheory.FILTER]) []); 16 17 18(*--------------------------------------------------------------------------- 19 Example of a "do-it-yourself" termination proof for variant. 20 ---------------------------------------------------------------------------*) 21 22Defn.tgoal variant_def; 23 24e (WF_REL_TAC `measure \(x,L). LENGTH(FILTER (\y. x <= y) L)`); 25 26(* Step-by-step way 27b(); 28e (Q.EXISTS_TAC`measure \(x,L). LENGTH(FILTER (\y. x <= y) L)` 29 THEN TotalDefn.TC_SIMP_TAC [] []); 30*) 31e (RW_TAC std_ss [] (* ETA-conv. to be done before induction *) 32 THEN Induct_on `L` 33 THEN RW_TAC list_ss [listTheory.FILTER,listTheory.MEM] 34 THEN RW_TAC arith_ss [DECIDE (Term `x<SUC y = x <= y`), 35 LENGTH_FILTER_SUBSET]); 36 37val [variant_eqns,variant_ind] = CONJUNCTS (top_thm()); 38 39 40(*--------------------------------------------------------------------------- 41 All wrapped up after proof found. 42 ---------------------------------------------------------------------------*) 43 44val (variant_eqn, variant_ind) = 45Defn.tprove 46 (variant_def, 47 WF_REL_TAC `measure \(x,L). LENGTH(FILTER (\y. x<=y) L)` 48 THEN RW_TAC std_ss [] 49 THEN Induct_on `L` 50 THEN RW_TAC list_ss [listTheory.FILTER,listTheory.MEM, 51 DECIDE (Term `x<SUC y = x <= y`), 52 LENGTH_FILTER_SUBSET]); 53 54(*--------------------------------------------------------------------------- 55 Properties. 56 ---------------------------------------------------------------------------*) 57 58val variant_correct = Q.prove( 59`!x L. ~MEM (variant x L) L`, 60recInduct variant_ind 61 THEN RW_TAC std_ss [] 62 THEN ONCE_REWRITE_TAC [variant_eqn] 63 THEN RW_TAC std_ss []); 64 65(*---------------------------------------------------------------------------* 66 * Of all the numbers that aren't in L, variant x L is the * 67 * smallest one that is greater-than-or-equal-to x. * 68 *---------------------------------------------------------------------------*) 69 70val variant_minimal = Q.prove( 71`!x L y. ~MEM y L /\ x<=y ==> variant x L <= y`, 72recInduct variant_ind 73 THEN RW_TAC std_ss [] 74 THEN ONCE_REWRITE_TAC [variant_eqn] 75 THEN RW_TAC std_ss [] 76 THEN `x < y` by PROVE_TAC [arithmeticTheory.LESS_OR_EQ] 77 THEN RW_TAC arith_ss []); 78 79 80(*--------------------------------------------------------------------------- 81 Evaluation of variant with computeLib 82 ---------------------------------------------------------------------------*) 83 84val Eval = EVAL o Term; 85 86Eval `variant 1 [1;2;3;4;5;6;7;8;9;10;11;13;14;15;16;16;16;16;165]`; 87Eval `variant 1 [1;2;3;4;5;6;7;8;9;10;11;12;13;14;15;16;16;16;16;165]`; 88Eval `variant (SUC 0) []`; 89Eval `variant (SUC 0) [SUC(SUC 0)]`; 90