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