1(*---------------------------------------------------------------------------
2
3      Examples (some typed in by Ken Friis Larsen) from 
4
5        "The Size-Change Principle for Program Termination",
6           Lee, Jones, Ben-Amram, Proceedings of POPL 2001
7 ---------------------------------------------------------------------------*)
8
9(*---------------------------------------------------------------------------
10  1.   Reverse function, with accumulating parameter. Automatic.
11 ---------------------------------------------------------------------------*)
12
13val REV = 
14 Define 
15   `(REV [] A = A) /\
16    (REV (h::t) A = REV t (h::A))`;
17
18(*---------------------------------------------------------------------------
19  2.   Program with indirect recursion. We treat this as mutual recursion.
20       Need to define a type of s-expressions for this to be well-typed.
21       Not easy for TFL currently.
22 ---------------------------------------------------------------------------*)
23
24Hol_datatype `sexp = Nil | Cons of sexp => sexp`;
25
26val indirect_def =
27 tDefine
28   "indirect"
29      `(f Nil x = x)
30   /\  (f (Cons h t) x = g t x (Cons h t))
31   /\  (g a b c = f a (Cons b c))`
32(WF_REL_TAC `inv_image ($< LEX $<)
33     (\s. (sum_case (\(x,y). sexp_size x) (\(a,b,c). sexp_size a) s,
34           sum_case (\v.0) (\v.1) s))`);
35
36
37(*---------------------------------------------------------------------------
38  3.   Function with lexically ordered parameters. Automatic.
39 ---------------------------------------------------------------------------*)
40
41val ack_def = 
42 Define
43      `(ack (0,n) = n+1)
44   /\  (ack (SUC m,0) = ack(m,1))
45   /\  (ack (SUC m, SUC n) = ack(m,ack(SUC m,n)))`;
46
47(*---------------------------------------------------------------------------
48  4.   Program with permuted parameters. Automatic.
49 ---------------------------------------------------------------------------*)
50
51val pparam = 
52 Define 
53   `pparam m n r = 
54      if r > 0 then pparam m (r-1) n else
55      if n > 0 then pparam r (n-1) m 
56               else m`;
57
58(*---------------------------------------------------------------------------
59  5.   Program with permuted and possibly discarded parameters.
60       Not easy for TFL currently. (measure function courtesy of Joe Hurd.)
61 ---------------------------------------------------------------------------*)
62
63val perm_def = tDefine
64   "perm"
65  `(perm x []       = x) /\ 
66   (perm [] (y::ys) = perm (y::ys) ys) /\ 
67   (perm (h::xs) z  = perm z xs)`
68 (WF_REL_TAC 
69    `measure \(l1,l2). 
70        if NULL l1 then 2 * LENGTH l2 else LENGTH l1 + LENGTH l2`
71  THEN RW_TAC list_ss []);
72
73
74(*---------------------------------------------------------------------------
75  6.  Program with late-starting sequence of descending parameter 
76      values. Automatic.
77
78      Note: late_g and late_g are defined in the reverse order in 
79            the paper. We do it that way with multiDefine as well.
80 ---------------------------------------------------------------------------*)
81
82val late_g = 
83    Define
84        `  (late_g [] d      = d)
85        /\ (late_g (c::cs) d = late_g cs (c :: d))`; 
86
87val late_f = 
88    Define
89        `  (late_f a []      = late_g a [])
90        /\ (late_f a (x::xs) = late_f (x::a) xs)`;
91
92TotalDefn.multiDefine
93  `(late_f a []      = late_g a []) /\
94   (late_f a (x::xs) = late_f (x::a) xs) /\
95   (late_g [] d      = d) /\ 
96   (late_g (c::cs) d = late_g cs (c :: d))`;
97
98